(define x::int)
(define y::int)
(define z::int)

(assert (or 
         (= (+ (* 3 x) (* 3 y)) 1)
         (= (+ (* 3 x) (* 3 y)) 2)))
(check)