(set-logic QF_LIA) (declare-fun x1() Int) (assert (and (>= x1 0) (<= x1 1))) (declare-fun x2() Int) (assert (and (>= x2 2) (<= x2 3))) (declare-fun x3() Int) (assert (and (>= x3 4) (<= x3 5))) (declare-fun x4() Int) (assert (and (>= x4 6) (<= x4 7))) (declare-fun x5() Int) (assert (and (>= x5 8) (<= x5 9))) (declare-fun x6() Int) (assert (and (>= x6 10) (<= x6 11))) (declare-fun x7() Int) (assert (and (>= x7 12) (<= x7 13))) (declare-fun x8() Int) (assert (and (>= x8 14) (<= x8 16))) (declare-fun x9() Int) (assert (and (>= x9 17) (<= x9 19))) (declare-fun x10() Int) (assert (and (>= x10 20) (<= x10 23))) (declare-fun x11() Int) (assert (and (>= x11 24) (<= x11 33))) (declare-fun x12() Int) (assert (and (>= x12 34) (<= x12 43))) (assert (or (not (= x4 7)) (not (= x8 14)))) (assert (or (not (= x1 1)) (not (= x8 15)))) (assert (or (not (= x2 2)) (not (= x7 13)))) (assert (or (not (= x2 2)) (not (= x4 7)))) (assert (or (not (= x7 13)) (not (= x8 15)))) (assert (or (not (= x4 7)) (not (= x8 15)))) (check-sat)