(define x1::int) (assert (and (>= x1 0) (<= x1 1))) (define x2::int) (assert (and (>= x2 2) (<= x2 3))) (define x3::int) (assert (and (>= x3 4) (<= x3 5))) (define x4::int) (assert (and (>= x4 6) (<= x4 7))) (define x5::int) (assert (and (>= x5 8) (<= x5 9))) (define x6::int) (assert (and (>= x6 10) (<= x6 11))) (define x7::int) (assert (and (>= x7 12) (<= x7 13))) (define x8::int) (assert (and (>= x8 14) (<= x8 16))) (define x9::int) (assert (and (>= x9 17) (<= x9 19))) (define x10::int) (assert (and (>= x10 20) (<= x10 23))) (define x11::int) (assert (and (>= x11 24) (<= x11 33))) (define x12::int) (assert (and (>= x12 34) (<= x12 43))) (define c1::bool (or (/= x4 7) (/= x8 14))) (define c2::bool (or (/= x1 1) (/= x8 15))) (define c3::bool (or (/= x2 2) (/= x7 13))) (define c4::bool (or (/= x2 2) (/= x4 7))) (define c5::bool (or (/= x7 13) (/= x8 15))) (define c6::bool (or (/= x4 7) (/= x8 15))) (assert c1) (assert c2) (assert c3) (assert c4) (assert c5) (assert c6) (check)