task: THEORY
BEGIN



lala:  THEOREM
FORALL (k : nat): 
  (EXISTS (n: nat): k = 3 * n) OR
  (EXISTS (n: nat): k = 3 * n + 1) OR
  (EXISTS (n: nat): k = 3 * n + 2)
END task