(define x::int) (define y::int) (define z::int) (assert (or (= (+ (* 3 x) (* 3 y)) 1) (and (= (+ (* 3 x) (* 6 y) (* 2 z)) 2) (= z 1)))) (check)