(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 15))) (declare-fun x9() Int) (assert (and (>= x9 16) (<= x9 17))) (declare-fun x10() Int) (assert (and (>= x10 18) (<= x10 19))) (declare-fun x11() Int) (assert (and (>= x11 20) (<= x11 21))) (declare-fun x12() Int) (assert (and (>= x12 22) (<= x12 23))) (declare-fun x13() Int) (assert (and (>= x13 24) (<= x13 25))) (declare-fun x14() Int) (assert (and (>= x14 26) (<= x14 28))) (assert (or (not (= x6 10)) (not (= x5 8)))) (assert (or (not (= x6 10)) (not (= x7 12)))) (assert (or (not (= x6 10)) (not (= x8 14)))) (assert (or (not (= x6 10)) (not (= x9 16)))) (assert (or (not (= x6 10)) (not (= x10 18)))) (assert (or (not (= x6 10)) (not (= x11 20)))) (assert (or (not (= x6 10)) (not (= x12 22)))) (assert (or (not (= x7 12)) (not (= x5 8)))) (assert (or (not (= x7 12)) (not (= x6 10)))) (assert (or (not (= x7 12)) (not (= x8 14)))) (assert (or (not (= x7 12)) (not (= x9 16)))) (assert (or (not (= x7 12)) (not (= x10 18)))) (assert (or (not (= x7 12)) (not (= x11 20)))) (assert (or (not (= x7 12)) (not (= x12 22)))) (assert (or (not (= x8 14)) (not (= x5 8)))) (assert (or (not (= x8 14)) (not (= x6 10)))) (assert (or (not (= x8 14)) (not (= x7 12)))) (assert (or (not (= x8 14)) (not (= x9 16)))) (assert (or (not (= x8 14)) (not (= x10 18)))) (assert (or (not (= x8 14)) (not (= x11 20)))) (assert (or (not (= x8 14)) (not (= x12 22)))) (assert (or (not (= x9 16)) (not (= x5 8)))) (assert (or (not (= x9 16)) (not (= x6 10)))) (assert (or (not (= x9 16)) (not (= x7 12)))) (assert (or (not (= x9 16)) (not (= x8 14)))) (assert (or (not (= x9 16)) (not (= x10 18)))) (assert (or (not (= x9 16)) (not (= x11 20)))) (assert (or (not (= x9 16)) (not (= x12 22)))) (assert (or (not (= x10 18)) (not (= x5 8)))) (assert (or (not (= x10 18)) (not (= x6 10)))) (assert (or (not (= x10 18)) (not (= x7 12)))) (assert (or (not (= x10 18)) (not (= x8 14)))) (assert (or (not (= x10 18)) (not (= x9 16)))) (assert (or (not (= x10 18)) (not (= x11 20)))) (assert (or (not (= x10 18)) (not (= x12 22)))) (assert (or (not (= x11 20)) (not (= x5 8)))) (assert (or (not (= x11 20)) (not (= x6 10)))) (assert (or (not (= x11 20)) (not (= x7 12)))) (assert (or (not (= x11 20)) (not (= x8 14)))) (assert (or (not (= x11 20)) (not (= x9 16)))) (assert (or (not (= x11 20)) (not (= x10 18)))) (assert (or (not (= x11 20)) (not (= x12 22)))) (assert (or (not (= x12 22)) (not (= x5 8)))) (assert (or (not (= x12 22)) (not (= x6 10)))) (assert (or (not (= x12 22)) (not (= x7 12)))) (assert (or (not (= x12 22)) (not (= x8 14)))) (assert (or (not (= x12 22)) (not (= x9 16)))) (assert (or (not (= x12 22)) (not (= x10 18)))) (assert (or (not (= x12 22)) (not (= x11 20)))) (assert (or (not (= x13 24)) (not (= x5 8)))) (assert (or (not (= x13 24)) (not (= x6 10)))) (assert (or (not (= x13 24)) (not (= x7 12)))) (assert (or (not (= x13 24)) (not (= x8 14)))) (assert (or (not (= x13 24)) (not (= x9 16)))) (assert (or (not (= x13 24)) (not (= x10 18)))) (assert (or (not (= x13 24)) (not (= x11 20)))) (assert (or (not (= x13 24)) (not (= x12 22)))) (assert (or (not (= x14 26)) (not (= x3 4)))) (assert (or (not (= x14 27)) (= x3 4))) (assert (or (not (= x14 28)))) (assert (or (not (= x1 1)) (not (= x2 3)) (not (= x3 5)) (not (= x4 7)) (not (= x5 9)) (not (= x6 11)) (not (= x7 13)) (not (= x8 15)) (not (= x9 17)) (not (= x10 19)) (not (= x11 21)) (not (= x12 23)) (not (= x13 25)))) (check-sat)