(define x1::int) (assert (and (>= x1 0) (<= x1 2))) (define x2::int) (assert (and (>= x2 3) (<= x2 5))) (define x3::int) (assert (and (>= x3 6) (<= x3 9))) (define x4::int) (assert (and (>= x4 10) (<= x4 15))) (define x5::int) (assert (and (>= x5 16) (<= x5 23))) (define x6::int) (assert (and (>= x6 24) (<= x6 27))) (define x7::int) (assert (and (>= x7 28) (<= x7 30))) (define x8::int) (assert (and (>= x8 31) (<= x8 32))) (define x9::int) (assert (and (>= x9 33) (<= x9 37))) (define c1::bool (or (/= x3 6) (= x2 3))) (define c2::bool (or (/= x3 6) (= x1 0) (= x1 2))) (define c3::bool (or (/= x3 7) (= x2 4))) (define c4::bool (or (/= x3 7) (= x1 0) (= x1 2))) (define c5::bool (or (/= x3 8) (= x2 3))) (define c6::bool (or (/= x3 8) (= x1 0) (= x1 2))) (define c7::bool (or (/= x4 10) (= x2 3))) (define c8::bool (or (/= x4 10) (= x3 9))) (define c9::bool (or (/= x4 10) (= x1 0) (= x1 2))) (define c10::bool (or (/= x4 11) (= x2 4))) (define c11::bool (or (/= x4 11) (= x3 9))) (define c12::bool (or (/= x4 11) (= x1 0) (= x1 2))) (define c13::bool (or (/= x4 12) (= x2 4))) (define c14::bool (or (/= x4 12) (= x3 9))) (define c15::bool (or (/= x4 12) (= x1 0) (= x1 2))) (define c16::bool (or (/= x4 13) (= x2 4))) (define c17::bool (or (/= x4 13) (= x3 9))) (define c18::bool (or (/= x4 13) (= x1 0) (= x1 2))) (define c19::bool (or (/= x4 14) (= x2 3))) (define c20::bool (or (/= x5 16) (= x1 0))) (define c21::bool (or (/= x5 16) (= x2 3) (= x2 4))) (define c22::bool (or (/= x5 16) (= x3 9))) (define c23::bool (or (/= x5 17) (= x1 2))) (define c24::bool (or (/= x5 17) (= x2 3) (= x2 4))) (define c25::bool (or (/= x5 17) (= x3 9))) (define c26::bool (or (/= x5 18) (= x1 0))) (define c27::bool (or (/= x5 18) (= x2 3) (= x2 4))) (define c28::bool (or (/= x5 18) (= x3 9))) (define c29::bool (or (/= x5 19) (= x1 2))) (define c30::bool (or (/= x5 19) (= x2 3) (= x2 4))) (define c31::bool (or (/= x5 19) (= x3 9))) (define c32::bool (or (/= x5 20) (= x1 0))) (define c33::bool (or (/= x5 20) (= x2 3) (= x2 4))) (define c34::bool (or (/= x5 20) (= x3 9))) (define c35::bool (or (/= x5 21) (= x1 2))) (define c36::bool (or (/= x5 21) (= x2 3) (= x2 4))) (define c37::bool (or (/= x5 21) (= x3 9))) (define c38::bool (or (/= x5 22) (= x2 3))) (define c39::bool (or (/= x6 24) (= x1 0))) (define c40::bool (or (/= x6 24) (= x5 16) (= x5 17) (= x5 18) (= x5 19) (= x5 20) (= x5 21))) (define c41::bool (or (/= x6 25) (= x1 2))) (define c42::bool (or (/= x6 25) (= x5 16) (= x5 17) (= x5 18) (= x5 19) (= x5 20) (= x5 21))) (define c43::bool (or (/= x6 26) (= x5 16) (= x5 17) (= x5 18) (= x5 19) (= x5 20) (= x5 21))) (define c44::bool (or (/= x7 28) (= x1 0))) (define c45::bool (or (/= x7 28) (= x2 3) (= x2 4))) (define c46::bool (or (/= x7 29) (= x1 2))) (define c47::bool (or (/= x7 29) (= x2 3) (= x2 4))) (define c48::bool (or (/= x8 31) (= x1 0) (= x1 2))) (define c49::bool (or (/= x8 31) (= x2 3) (= x2 4))) (define c50::bool (or (/= x9 33) (= x8 31))) (define c51::bool (or (/= x9 33) (= x5 16) (= x5 17) (= x5 18) (= x5 19) (= x5 20) (= x5 21))) (define c52::bool (or (/= x9 34) (= x7 28) (= x7 29))) (define c53::bool (or (/= x9 34) (= x8 31))) (define c54::bool (or (/= x9 35) (= x1 0))) (define c55::bool (or (/= x9 35) (= x8 31))) (define c56::bool (or (/= x9 35) (= x5 16) (= x5 17) (= x5 18) (= x5 19) (= x5 20) (= x5 21))) (define c57::bool (or (/= x9 36) (= x1 2))) (define c58::bool (or (/= x9 36) (= x7 28) (= x7 29))) (define c59::bool (or (/= x9 36) (= x8 31))) (define c60::bool (or (/= x4 15) (/= x2 3))) (define c61::bool (or (/= x4 15) (/= x3 9) (/= x1 0) (/= x2 4))) (define c62::bool (or (/= x4 15) (/= x3 9) (/= x1 2) (/= x2 4))) (define c63::bool (or (/= x4 15) (/= x3 9) (/= x1 0) (/= x2 5))) (define c64::bool (or (/= x4 15) (/= x3 9) (/= x1 2) (/= x2 5))) (define c65::bool (or (/= x5 23) (/= x2 3))) (define c66::bool (or (/= x5 23) (/= x3 9) (/= x1 0) (/= x2 4))) (define c67::bool (or (/= x5 23) (/= x3 9) (/= x1 2) (/= x2 4))) (define c68::bool (or (/= x5 23) (/= x3 9) (/= x1 0) (/= x2 5))) (define c69::bool (or (/= x5 23) (/= x3 9) (/= x1 2) (/= x2 5))) (define c70::bool (or (/= x6 27) (/= x5 16))) (define c71::bool (or (/= x6 27) (/= x5 17))) (define c72::bool (or (/= x6 27) (/= x5 18))) (define c73::bool (or (/= x6 27) (/= x5 19))) (define c74::bool (or (/= x6 27) (/= x5 20))) (define c75::bool (or (/= x6 27) (/= x5 21))) (define c76::bool (or (/= x9 37) (/= x5 16) (/= x8 31))) (define c77::bool (or (/= x9 37) (/= x5 17) (/= x8 31))) (define c78::bool (or (/= x9 37) (/= x5 18) (/= x8 31))) (define c79::bool (or (/= x9 37) (/= x5 19) (/= x8 31))) (define c80::bool (or (/= x9 37) (/= x5 20) (/= x8 31))) (define c81::bool (or (/= x9 37) (/= x5 21) (/= x8 31))) (define c82::bool (or (/= x9 37) (/= x7 28) (/= x8 31))) (define c83::bool (or (/= x9 37) (/= x7 29) (/= x8 31))) (assert c1) (assert c2) (assert c3) (assert c4) (assert c5) (assert c6) (assert c7) (assert c8) (assert c9) (assert c10) (assert c11) (assert c12) (assert c13) (assert c14) (assert c15) (assert c16) (assert c17) (assert c18) (assert c19) (assert c20) (assert c21) (assert c22) (assert c23) (assert c24) (assert c25) (assert c26) (assert c27) (assert c28) (assert c29) (assert c30) (assert c31) (assert c32) (assert c33) (assert c34) (assert c35) (assert c36) (assert c37) (assert c38) (assert c39) (assert c40) (assert c41) (assert c42) (assert c43) (assert c44) (assert c45) (assert c46) (assert c47) (assert c48) (assert c49) (assert c50) (assert c51) (assert c52) (assert c53) (assert c54) (assert c55) (assert c56) (assert c57) (assert c58) (assert c59) (assert c60) (assert c61) (assert c62) (assert c63) (assert c64) (assert c65) (assert c66) (assert c67) (assert c68) (assert c69) (assert c70) (assert c71) (assert c72) (assert c73) (assert c74) (assert c75) (assert c76) (assert c77) (assert c78) (assert c79) (assert c80) (assert c81) (assert c82) (assert c83) (check)