(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 6))) (declare-fun x4() Int) (assert (and (>= x4 7) (<= x4 9))) (declare-fun x5() Int) (assert (and (>= x5 10) (<= x5 11))) (declare-fun x6() Int) (assert (and (>= x6 12) (<= x6 13))) (declare-fun x7() Int) (assert (and (>= x7 14) (<= x7 15))) (declare-fun x8() Int) (assert (and (>= x8 16) (<= x8 17))) (declare-fun x9() Int) (assert (and (>= x9 18) (<= x9 22))) (assert (or (not (= x2 2)) (not (= x3 5)))) (assert (or (= x3 6) (not (= x4 7)))) (assert (or (not (= x4 8)) (= x3 6))) (assert (or (not (= x4 8)) (not (= x2 2)))) (assert (or (not (= x5 10)) (not (= x3 5)))) (assert (or (not (= x5 10)) (not (= x4 8)))) (assert (or (not (= x6 12)) (not (= x3 5)))) (assert (or (not (= x6 12)) (not (= x4 8)))) (assert (or (not (= x7 14)) (= x3 6))) (assert (or (not (= x7 14)) (= x4 9))) (assert (or (not (= x8 16)) (= x4 9))) (assert (or (not (= x8 16)) (= x3 6))) (check-sat)