(set-logic QF_LIA) (declare-fun x1() Int) (assert (and (>= x1 0) (<= x1 2))) (declare-fun x2() Int) (assert (and (>= x2 3) (<= x2 5))) (declare-fun x3() Int) (assert (and (>= x3 6) (<= x3 8))) (declare-fun x4() Int) (assert (and (>= x4 9) (<= x4 11))) (declare-fun x5() Int) (assert (and (>= x5 12) (<= x5 19))) (declare-fun x6() Int) (assert (and (>= x6 20) (<= x6 27))) (declare-fun x7() Int) (assert (and (>= x7 28) (<= x7 32))) (declare-fun x8() Int) (assert (and (>= x8 33) (<= x8 37))) (declare-fun x9() Int) (assert (and (>= x9 38) (<= x9 47))) (declare-fun x10() Int) (assert (and (>= x10 48) (<= x10 57))) (declare-fun x11() Int) (assert (and (>= x11 58) (<= x11 59))) (declare-fun x12() Int) (assert (and (>= x12 60) (<= x12 61))) (declare-fun x13() Int) (assert (and (>= x13 62) (<= x13 63))) (assert (or (not (= x3 7)) (not (= x10 49)) (not (= x9 40)))) (assert (or (not (= x7 31)) (not (= x2 4)) (not (= x8 34)))) (assert (or (not (= x10 48)) (not (= x10 56)) (not (= x4 9)))) (assert (or (not (= x10 48)) (not (= x10 55)) (not (= x4 9)))) (assert (or (not (= x5 18)) (not (= x2 3)) (not (= x7 28)))) (assert (or (not (= x3 7)) (not (= x10 49)) (not (= x10 48)))) (assert (or (not (= x3 7)) (not (= x10 48)) (not (= x10 53)))) (assert (or (not (= x10 57)) (not (= x9 40)) (not (= x3 8)))) (assert (or (not (= x6 20)) (not (= x6 22)) (not (= x2 3)))) (assert (or (not (= x6 20)) (not (= x6 22)) (not (= x1 1)))) (assert (or (not (= x3 7)) (not (= x10 57)) (not (= x10 48)))) (assert (or (not (= x9 47)) (not (= x3 7)) (not (= x10 55)))) (assert (or (not (= x5 13)) (not (= x1 2)) (not (= x6 25)))) (assert (or (not (= x10 55)) (not (= x3 8)) (not (= x9 44)))) (assert (or (not (= x6 21)) (not (= x6 20)) (not (= x1 1)))) (assert (or (not (= x10 57)) (not (= x9 40)) (not (= x4 9)))) (assert (or (not (= x6 26)) (not (= x1 2)) (not (= x5 17)))) (assert (or (not (= x1 2)) (not (= x5 16)) (not (= x7 28)))) (assert (or (not (= x8 35)) (not (= x7 32)) (not (= x3 6)))) (assert (or (not (= x3 7)) (not (= x10 48)) (not (= x10 54)))) (assert (or (not (= x9 39)) (not (= x10 54)) (not (= x3 8)))) (assert (or (not (= x9 39)) (not (= x10 54)) (not (= x4 9)))) (assert (or (not (= x6 20)) (not (= x6 23)) (not (= x1 1)))) (assert (or (not (= x9 43)) (not (= x3 7)) (not (= x10 51)))) (assert (or (not (= x6 20)) (not (= x6 23)) (not (= x2 3)))) (assert (or (not (= x9 47)) (not (= x3 7)) (not (= x10 56)))) (assert (or (not (= x7 31)) (not (= x3 6)) (not (= x8 34)))) (assert (or (not (= x7 30)) (not (= x9 38)) (not (= x3 6)))) (assert (or (not (= x8 35)) (not (= x8 33)) (not (= x3 6)))) (assert (or (not (= x9 41)) (not (= x10 57)) (not (= x3 8)))) (assert (or (not (= x2 5)) (not (= x8 37)) (not (= x7 32)))) (assert (or (not (= x8 35)) (not (= x8 33)) (not (= x2 4)))) (assert (or (not (= x10 55)) (not (= x4 9)) (not (= x9 44)))) (assert (or (not (= x2 5)) (not (= x8 37)) (not (= x7 31)))) (assert (or (not (= x10 51)) (not (= x9 40)) (not (= x4 9)))) (assert (or (not (= x6 26)) (not (= x2 3)) (not (= x5 17)))) (assert (or (not (= x6 21)) (not (= x5 14)) (not (= x1 1)))) (assert (or (not (= x10 51)) (not (= x9 40)) (not (= x3 8)))) (assert (or (not (= x9 47)) (not (= x3 7)) (not (= x10 57)))) (assert (or (not (= x5 14)) (not (= x2 3)) (not (= x6 27)))) (assert (or (not (= x3 7)) (not (= x10 48)) (not (= x10 50)))) (assert (or (not (= x9 41)) (not (= x10 55)) (not (= x4 9)))) (assert (or (not (= x9 41)) (not (= x10 55)) (not (= x3 8)))) (assert (or (not (= x5 18)) (not (= x1 2)) (not (= x7 28)))) (assert (or (not (= x9 45)) (not (= x11 58)) (not (= x4 9)))) (assert (or (not (= x9 45)) (not (= x11 58)) (not (= x3 8)))) (assert (or (not (= x6 20)) (not (= x6 21)) (not (= x2 3)))) (assert (or (not (= x9 41)) (not (= x10 57)) (not (= x4 9)))) (assert (or (not (= x5 14)) (not (= x1 2)) (not (= x6 27)))) (assert (or (not (= x9 46)) (not (= x10 52)) (not (= x4 9)))) (assert (or (not (= x9 39)) (not (= x11 58)) (not (= x4 9)))) (assert (or (not (= x9 39)) (not (= x11 58)) (not (= x3 8)))) (assert (or (not (= x9 43)) (not (= x3 7)) (not (= x10 50)))) (assert (or (not (= x5 15)) (not (= x2 3)) (not (= x7 28)))) (assert (or (not (= x3 7)) (not (= x10 48)) (not (= x10 56)))) (assert (or (not (= x9 46)) (not (= x11 58)) (not (= x3 8)))) (assert (or (not (= x9 46)) (not (= x11 58)) (not (= x4 9)))) (assert (or (not (= x9 43)) (not (= x10 50)) (not (= x4 9)))) (assert (or (not (= x11 58)) (not (= x9 40)) (not (= x4 9)))) (assert (or (not (= x11 58)) (not (= x9 40)) (not (= x3 8)))) (assert (or (not (= x5 19)) (not (= x6 25)) (not (= x1 1)))) (assert (or (not (= x5 19)) (not (= x6 25)) (not (= x2 3)))) (assert (or (not (= x9 43)) (not (= x3 7)) (not (= x10 49)))) (assert (or (not (= x6 24)) (not (= x1 2)) (not (= x5 16)))) (assert (or (not (= x5 15)) (not (= x1 2)) (not (= x7 28)))) (assert (or (not (= x7 30)) (not (= x8 36)) (not (= x2 5)))) (assert (or (not (= x7 30)) (not (= x8 36)) (not (= x3 6)))) (assert (or (not (= x8 35)) (not (= x7 31)) (not (= x2 4)))) (assert (or (not (= x8 35)) (not (= x7 31)) (not (= x3 6)))) (assert (or (not (= x5 13)) (not (= x2 3)) (not (= x6 27)))) (assert (or (not (= x10 55)) (not (= x3 8)) (not (= x9 42)))) (assert (or (not (= x9 40)) (not (= x10 50)) (not (= x3 8)))) (assert (or (not (= x8 36)) (not (= x7 32)) (not (= x3 6)))) (assert (or (not (= x9 43)) (not (= x10 53)) (not (= x3 8)))) (assert (or (not (= x9 45)) (not (= x10 55)) (not (= x3 8)))) (assert (or (not (= x9 45)) (not (= x3 7)) (not (= x10 55)))) (assert (or (not (= x5 15)) (not (= x2 3)) (not (= x6 27)))) (assert (or (not (= x5 13)) (not (= x1 2)) (not (= x6 27)))) (assert (or (not (= x10 55)) (not (= x4 9)) (not (= x9 42)))) (assert (or (not (= x6 22)) (not (= x1 1)) (not (= x5 17)))) (assert (or (not (= x3 7)) (not (= x10 49)) (not (= x9 42)))) (assert (or (not (= x9 45)) (not (= x3 7)) (not (= x10 54)))) (assert (or (not (= x6 20)) (not (= x6 24)) (not (= x1 1)))) (assert (or (not (= x6 20)) (not (= x6 24)) (not (= x2 3)))) (assert (or (not (= x9 41)) (not (= x10 56)) (not (= x4 9)))) (assert (or (not (= x7 30)) (not (= x8 35)) (not (= x2 5)))) (assert (or (not (= x7 30)) (not (= x8 35)) (not (= x2 4)))) (assert (or (not (= x9 41)) (not (= x10 56)) (not (= x3 8)))) (assert (or (not (= x3 7)) (not (= x10 52)) (not (= x9 44)))) (assert (or (not (= x5 15)) (not (= x1 2)) (not (= x6 27)))) (assert (or (not (= x10 49)) (not (= x10 48)) (not (= x4 9)))) (assert (or (not (= x9 41)) (not (= x10 54)) (not (= x4 9)))) (assert (or (not (= x5 13)) (not (= x6 23)) (not (= x2 3)))) (assert (or (not (= x5 13)) (not (= x6 23)) (not (= x1 2)))) (assert (or (not (= x6 24)) (not (= x2 3)) (not (= x5 17)))) (assert (or (not (= x11 58)) (not (= x3 8)) (not (= x9 42)))) (assert (or (not (= x9 41)) (not (= x10 54)) (not (= x3 8)))) (assert (or (not (= x9 39)) (not (= x10 50)) (not (= x4 9)))) (assert (or (not (= x9 39)) (not (= x10 50)) (not (= x3 8)))) (assert (or (not (= x2 5)) (not (= x8 33)) (not (= x9 38)))) (assert (or (not (= x9 43)) (not (= x10 51)) (not (= x4 9)))) (assert (or (not (= x8 36)) (not (= x2 4)) (not (= x7 32)))) (assert (or (not (= x9 45)) (not (= x3 7)) (not (= x10 53)))) (assert (or (not (= x9 46)) (not (= x3 7)) (not (= x10 53)))) (assert (or (not (= x10 57)) (not (= x10 48)) (not (= x4 9)))) (assert (or (not (= x9 47)) (not (= x11 58)) (not (= x4 9)))) (assert (or (not (= x9 43)) (not (= x10 52)) (not (= x4 9)))) (assert (or (not (= x9 47)) (not (= x11 58)) (not (= x3 8)))) (assert (or (not (= x6 23)) (not (= x2 3)) (not (= x5 17)))) (assert (or (not (= x5 14)) (not (= x1 2)) (not (= x6 25)))) (assert (or (not (= x5 15)) (not (= x1 2)) (not (= x6 25)))) (assert (or (not (= x1 2)) (not (= x6 25)) (not (= x5 17)))) (assert (or (not (= x3 7)) (not (= x10 50)) (not (= x9 40)))) (assert (or (not (= x9 38)) (not (= x7 32)) (not (= x3 6)))) (assert (or (not (= x10 57)) (not (= x3 8)) (not (= x9 44)))) (assert (or (not (= x2 3)) (not (= x5 17)) (not (= x7 28)))) (assert (or (not (= x9 46)) (not (= x3 7)) (not (= x10 51)))) (assert (or (not (= x5 13)) (not (= x6 25)) (not (= x2 3)))) (assert (or (not (= x9 41)) (not (= x10 53)) (not (= x4 9)))) (assert (or (not (= x3 7)) (not (= x10 53)) (not (= x9 44)))) (assert (or (not (= x9 41)) (not (= x10 53)) (not (= x3 8)))) (assert (or (not (= x9 46)) (not (= x3 7)) (not (= x10 54)))) (assert (or (not (= x5 14)) (not (= x6 25)) (not (= x2 3)))) (assert (or (not (= x9 41)) (not (= x10 49)) (not (= x4 9)))) (assert (or (not (= x3 7)) (not (= x10 54)) (not (= x9 44)))) (assert (or (not (= x6 24)) (not (= x1 1)) (not (= x5 17)))) (assert (or (not (= x5 13)) (not (= x6 24)) (not (= x2 3)))) (assert (or (not (= x5 13)) (not (= x6 24)) (not (= x1 2)))) (assert (or (not (= x5 14)) (not (= x6 24)) (not (= x1 2)))) (assert (or (not (= x8 36)) (not (= x7 31)) (not (= x2 4)))) (assert (or (not (= x9 45)) (not (= x10 52)) (not (= x4 9)))) (assert (or (not (= x3 7)) (not (= x10 52)) (not (= x9 42)))) (assert (or (not (= x10 57)) (not (= x3 8)) (not (= x9 42)))) (assert (or (not (= x5 14)) (not (= x6 24)) (not (= x2 3)))) (assert (or (not (= x6 26)) (not (= x5 13)) (not (= x1 2)))) (assert (or (not (= x10 56)) (not (= x3 8)) (not (= x9 44)))) (assert (or (not (= x9 46)) (not (= x3 7)) (not (= x10 52)))) (assert (or (not (= x9 47)) (not (= x10 50)) (not (= x4 9)))) (assert (or (not (= x9 45)) (not (= x3 7)) (not (= x10 52)))) (assert (or (not (= x6 23)) (not (= x1 1)) (not (= x5 17)))) (assert (or (not (= x3 7)) (not (= x10 49)) (not (= x9 44)))) (assert (or (not (= x6 26)) (not (= x5 13)) (not (= x2 3)))) (assert (or (not (= x8 33)) (not (= x8 37)) (not (= x2 4)))) (assert (or (not (= x8 33)) (not (= x8 37)) (not (= x3 6)))) (assert (or (not (= x10 52)) (not (= x4 9)) (not (= x9 44)))) (assert (or (not (= x10 56)) (not (= x9 40)) (not (= x3 8)))) (assert (or (not (= x9 43)) (not (= x10 54)) (not (= x4 9)))) (assert (or (not (= x10 53)) (not (= x9 40)) (not (= x3 8)))) (assert (or (not (= x9 43)) (not (= x10 54)) (not (= x3 8)))) (assert (or (not (= x10 53)) (not (= x9 40)) (not (= x4 9)))) (assert (or (not (= x10 56)) (not (= x9 40)) (not (= x4 9)))) (assert (or (not (= x9 47)) (not (= x10 52)) (not (= x4 9)))) (assert (or (not (= x9 47)) (not (= x10 51)) (not (= x4 9)))) (assert (or (not (= x7 29)) (not (= x2 5)) (not (= x9 38)))) (assert (or (not (= x10 57)) (not (= x4 9)) (not (= x9 42)))) (assert (or (not (= x10 56)) (not (= x4 9)) (not (= x9 44)))) (assert (or (not (= x7 29)) (not (= x9 38)) (not (= x3 6)))) (assert (or (not (= x9 45)) (not (= x3 7)) (not (= x10 51)))) (assert (or (not (= x9 43)) (not (= x3 7)) (not (= x10 53)))) (assert (or (not (= x2 3)) (not (= x5 16)) (not (= x7 28)))) (assert (or (not (= x9 46)) (not (= x3 7)) (not (= x10 56)))) (assert (or (not (= x5 18)) (not (= x1 2)) (not (= x6 27)))) (assert (or (not (= x1 2)) (not (= x5 16)) (not (= x6 27)))) (assert (or (not (= x6 26)) (not (= x5 18)) (not (= x1 1)))) (assert (or (not (= x6 26)) (not (= x5 18)) (not (= x1 2)))) (assert (or (not (= x1 2)) (not (= x5 17)) (not (= x7 28)))) (assert (or (not (= x10 48)) (not (= x10 50)) (not (= x4 9)))) (assert (or (not (= x3 7)) (not (= x10 50)) (not (= x9 44)))) (assert (or (not (= x9 38)) (not (= x7 31)) (not (= x3 6)))) (assert (or (not (= x6 26)) (not (= x5 14)) (not (= x2 3)))) (assert (or (not (= x9 47)) (not (= x10 49)) (not (= x4 9)))) (assert (or (not (= x6 26)) (not (= x5 14)) (not (= x1 2)))) (assert (or (not (= x3 7)) (not (= x11 58)) (not (= x10 48)))) (assert (or (not (= x8 36)) (not (= x7 29)) (not (= x3 6)))) (assert (or (not (= x8 36)) (not (= x7 29)) (not (= x2 5)))) (assert (or (not (= x9 45)) (not (= x10 51)) (not (= x4 9)))) (assert (or (not (= x3 7)) (not (= x10 50)) (not (= x9 42)))) (assert (or (not (= x9 43)) (not (= x3 7)) (not (= x10 52)))) (assert (or (not (= x3 7)) (not (= x9 39)) (not (= x10 49)))) (assert (or (not (= x9 41)) (not (= x10 50)) (not (= x4 9)))) (assert (or (not (= x9 45)) (not (= x10 50)) (not (= x4 9)))) (assert (or (not (= x10 57)) (not (= x4 9)) (not (= x9 44)))) (assert (or (not (= x9 45)) (not (= x10 57)) (not (= x4 9)))) (assert (or (not (= x9 45)) (not (= x10 56)) (not (= x3 8)))) (assert (or (not (= x9 45)) (not (= x10 57)) (not (= x3 8)))) (assert (or (not (= x9 45)) (not (= x10 56)) (not (= x4 9)))) (assert (or (not (= x6 25)) (not (= x1 1)) (not (= x5 17)))) (assert (or (not (= x10 52)) (not (= x3 8)) (not (= x9 42)))) (assert (or (not (= x9 46)) (not (= x3 7)) (not (= x10 55)))) (assert (or (not (= x5 18)) (not (= x2 3)) (not (= x6 27)))) (assert (or (not (= x9 41)) (not (= x3 7)) (not (= x10 50)))) (assert (or (not (= x5 13)) (not (= x6 22)) (not (= x1 2)))) (assert (or (not (= x5 13)) (not (= x6 22)) (not (= x2 3)))) (assert (or (not (= x10 52)) (not (= x9 40)) (not (= x4 9)))) (assert (or (not (= x10 52)) (not (= x9 40)) (not (= x3 8)))) (assert (or (not (= x9 41)) (not (= x3 7)) (not (= x10 49)))) (assert (or (not (= x5 15)) (not (= x6 22)) (not (= x2 3)))) (assert (or (not (= x7 29)) (not (= x2 5)) (not (= x8 37)))) (assert (or (not (= x9 47)) (not (= x10 55)) (not (= x4 9)))) (assert (or (not (= x9 39)) (not (= x10 49)) (not (= x3 8)))) (assert (or (not (= x5 15)) (not (= x6 22)) (not (= x1 1)))) (assert (or (not (= x5 13)) (not (= x6 21)) (not (= x1 2)))) (assert (or (not (= x5 13)) (not (= x6 21)) (not (= x1 1)))) (assert (or (not (= x10 53)) (not (= x4 9)) (not (= x9 44)))) (assert (or (not (= x5 15)) (not (= x6 21)) (not (= x2 3)))) (assert (or (not (= x5 19)) (not (= x6 24)) (not (= x2 3)))) (assert (or (not (= x5 19)) (not (= x6 24)) (not (= x1 1)))) (assert (or (not (= x9 47)) (not (= x10 57)) (not (= x3 8)))) (assert (or (not (= x9 47)) (not (= x3 7)) (not (= x10 50)))) (assert (or (not (= x5 18)) (not (= x6 24)) (not (= x1 1)))) (assert (or (not (= x5 15)) (not (= x6 21)) (not (= x1 1)))) (assert (or (not (= x5 18)) (not (= x6 24)) (not (= x2 3)))) (assert (or (not (= x10 54)) (not (= x3 8)) (not (= x9 44)))) (assert (or (not (= x5 13)) (not (= x1 2)) (not (= x7 28)))) (assert (or (not (= x6 20)) (not (= x1 2)) (not (= x7 28)))) (assert (or (not (= x5 19)) (not (= x2 3)) (not (= x7 28)))) (assert (or (not (= x10 54)) (not (= x3 8)) (not (= x9 42)))) (assert (or (not (= x9 46)) (not (= x10 49)) (not (= x4 9)))) (assert (or (not (= x7 30)) (not (= x2 5)) (not (= x9 38)))) (assert (or (not (= x7 29)) (not (= x2 4)) (not (= x8 34)))) (assert (or (not (= x5 14)) (not (= x1 2)) (not (= x7 28)))) (assert (or (not (= x9 43)) (not (= x11 58)) (not (= x4 9)))) (assert (or (not (= x9 43)) (not (= x11 58)) (not (= x3 8)))) (assert (or (not (= x2 3)) (not (= x5 16)) (not (= x6 27)))) (assert (or (not (= x9 39)) (not (= x10 57)) (not (= x4 9)))) (assert (or (not (= x5 13)) (not (= x2 3)) (not (= x7 28)))) (assert (or (not (= x6 20)) (not (= x1 1)) (not (= x7 28)))) (assert (or (not (= x9 39)) (not (= x10 57)) (not (= x3 8)))) (assert (or (not (= x10 54)) (not (= x4 9)) (not (= x9 42)))) (assert (or (not (= x5 19)) (not (= x1 2)) (not (= x7 28)))) (assert (or (not (= x7 29)) (not (= x2 5)) (not (= x8 34)))) (assert (or (not (= x9 45)) (not (= x10 49)) (not (= x4 9)))) (assert (or (not (= x5 14)) (not (= x2 3)) (not (= x7 28)))) (assert (or (not (= x5 19)) (not (= x6 23)) (not (= x2 3)))) (assert (or (not (= x5 19)) (not (= x6 23)) (not (= x1 1)))) (assert (or (not (= x6 21)) (not (= x5 19)) (not (= x2 3)))) (assert (or (not (= x6 21)) (not (= x5 19)) (not (= x1 1)))) (assert (or (not (= x9 43)) (not (= x10 56)) (not (= x3 8)))) (assert (or (not (= x6 20)) (not (= x6 25)) (not (= x1 1)))) (assert (or (not (= x9 43)) (not (= x10 56)) (not (= x4 9)))) (assert (or (not (= x6 20)) (not (= x6 25)) (not (= x2 3)))) (assert (or (not (= x9 46)) (not (= x3 7)) (not (= x10 49)))) (assert (or (not (= x8 36)) (not (= x2 5)) (not (= x7 31)))) (assert (or (not (= x4 10)) (not (= x12 61)) (not (= x12 60)))) (assert (or (not (= x4 10)) (not (= x12 61)) (not (= x11 59)))) (assert (or (not (= x6 26)) (not (= x6 20)) (not (= x1 1)))) (assert (or (not (= x10 54)) (not (= x9 40)) (not (= x4 9)))) (assert (or (not (= x10 54)) (not (= x9 40)) (not (= x3 8)))) (assert (or (not (= x6 26)) (not (= x6 20)) (not (= x2 3)))) (assert (or (not (= x6 21)) (not (= x5 18)) (not (= x1 1)))) (assert (or (not (= x6 22)) (not (= x5 18)) (not (= x2 3)))) (assert (or (not (= x11 58)) (not (= x4 9)) (not (= x9 42)))) (assert (or (not (= x5 14)) (not (= x6 22)) (not (= x1 1)))) (assert (or (not (= x5 14)) (not (= x6 22)) (not (= x1 2)))) (assert (or (not (= x6 22)) (not (= x5 18)) (not (= x1 1)))) (assert (or (not (= x6 21)) (not (= x5 18)) (not (= x2 3)))) (assert (or (not (= x10 56)) (not (= x4 9)) (not (= x9 42)))) (assert (or (not (= x5 15)) (not (= x6 26)) (not (= x1 2)))) (assert (or (not (= x3 7)) (not (= x10 51)) (not (= x9 42)))) (assert (or (not (= x6 23)) (not (= x5 18)) (not (= x1 1)))) (assert (or (not (= x5 14)) (not (= x6 21)) (not (= x2 3)))) (assert (or (not (= x5 15)) (not (= x6 24)) (not (= x1 2)))) (assert (or (not (= x5 15)) (not (= x6 24)) (not (= x2 3)))) (assert (or (not (= x8 33)) (not (= x3 6)) (not (= x8 34)))) (assert (or (not (= x5 15)) (not (= x6 26)) (not (= x2 3)))) (assert (or (not (= x9 46)) (not (= x3 7)) (not (= x10 50)))) (assert (or (not (= x5 19)) (not (= x1 2)) (not (= x6 27)))) (assert (or (not (= x9 47)) (not (= x10 56)) (not (= x4 9)))) (assert (or (not (= x9 46)) (not (= x10 57)) (not (= x3 8)))) (assert (or (not (= x9 46)) (not (= x10 57)) (not (= x4 9)))) (assert (or (not (= x5 15)) (not (= x6 25)) (not (= x2 3)))) (assert (or (not (= x9 47)) (not (= x10 54)) (not (= x4 9)))) (assert (or (not (= x9 43)) (not (= x10 57)) (not (= x4 9)))) (assert (or (not (= x6 21)) (not (= x2 3)) (not (= x5 16)))) (assert (or (not (= x9 43)) (not (= x10 57)) (not (= x3 8)))) (assert (or (not (= x10 56)) (not (= x3 8)) (not (= x9 42)))) (assert (or (not (= x9 47)) (not (= x3 7)) (not (= x10 49)))) (assert (or (not (= x9 47)) (not (= x10 53)) (not (= x4 9)))) (assert (or (not (= x11 58)) (not (= x3 8)) (not (= x9 44)))) (assert (or (not (= x5 19)) (not (= x1 1)) (not (= x6 27)))) (assert (or (not (= x6 22)) (not (= x5 19)) (not (= x1 1)))) (assert (or (not (= x9 41)) (not (= x10 52)) (not (= x3 8)))) (assert (or (not (= x9 41)) (not (= x10 52)) (not (= x4 9)))) (assert (or (not (= x8 37)) (not (= x2 4)) (not (= x7 32)))) (assert (or (not (= x5 15)) (not (= x6 23)) (not (= x1 2)))) (assert (or (not (= x5 18)) (not (= x6 23)) (not (= x2 3)))) (assert (or (not (= x5 15)) (not (= x6 23)) (not (= x1 1)))) (assert (or (not (= x8 33)) (not (= x2 4)) (not (= x8 34)))) (assert (or (not (= x9 43)) (not (= x10 55)) (not (= x3 8)))) (assert (or (not (= x11 58)) (not (= x4 9)) (not (= x9 44)))) (assert (or (not (= x9 43)) (not (= x10 55)) (not (= x4 9)))) (assert (or (not (= x13 62)) (not (= x3 6)) (not (= x4 9)) (not (= x12 60)))) (assert (or (not (= x5 14)) (not (= x6 23)) (not (= x2 3)))) (assert (or (not (= x5 14)) (not (= x6 23)) (not (= x1 2)))) (assert (or (not (= x6 23)) (not (= x1 1)) (not (= x5 16)))) (assert (or (not (= x13 62)) (not (= x4 11)) (not (= x11 59)))) (assert (or (not (= x13 62)) (not (= x4 11)) (not (= x12 60)))) (assert (or (not (= x7 30)) (not (= x3 6)) (not (= x8 34)))) (assert (or (not (= x3 7)) (not (= x10 51)) (not (= x9 44)))) (assert (or (not (= x9 47)) (not (= x3 7)) (not (= x10 52)))) (assert (or (not (= x10 49)) (not (= x9 40)) (not (= x4 9)))) (assert (or (not (= x6 26)) (not (= x1 2)) (not (= x5 16)))) (assert (or (not (= x7 30)) (not (= x2 5)) (not (= x8 37)))) (assert (or (not (= x6 21)) (not (= x1 1)) (not (= x5 16)))) (assert (or (not (= x13 62)) (not (= x5 12)) (not (= x11 59)))) (assert (or (not (= x6 22)) (not (= x2 3)) (not (= x5 17)))) (assert (or (not (= x2 3)) (not (= x5 17)) (not (= x6 27)))) (assert (or (not (= x9 46)) (not (= x10 54)) (not (= x4 9)))) (assert (or (not (= x10 51)) (not (= x10 48)) (not (= x4 9)))) (assert (or (not (= x9 41)) (not (= x11 58)) (not (= x4 9)))) (assert (or (not (= x9 47)) (not (= x3 7)) (not (= x10 51)))) (assert (or (not (= x9 41)) (not (= x11 58)) (not (= x3 8)))) (assert (or (not (= x1 2)) (not (= x5 17)) (not (= x6 27)))) (assert (or (not (= x6 21)) (not (= x2 3)) (not (= x5 17)))) (assert (or (not (= x12 61)) (not (= x5 12)) (not (= x12 60)))) (assert (or (not (= x4 11)) (not (= x12 61)) (not (= x11 59)))) (assert (or (not (= x3 7)) (not (= x10 55)) (not (= x10 48)))) (assert (or (not (= x10 50)) (not (= x4 9)) (not (= x9 44)))) (assert (or (not (= x10 52)) (not (= x9 39)) (not (= x3 8)))) (assert (or (not (= x10 52)) (not (= x9 39)) (not (= x4 9)))) (assert (or (not (= x3 7)) (not (= x10 51)) (not (= x10 48)))) (assert (or (not (= x9 39)) (not (= x10 53)) (not (= x3 8)))) (assert (or (not (= x9 39)) (not (= x10 53)) (not (= x4 9)))) (assert (or (not (= x10 52)) (not (= x10 48)) (not (= x4 9)))) (assert (or (not (= x7 29)) (not (= x8 37)) (not (= x3 6)))) (assert (or (not (= x10 55)) (not (= x9 40)) (not (= x4 9)))) (assert (or (not (= x10 55)) (not (= x9 40)) (not (= x3 8)))) (assert (or (not (= x7 30)) (not (= x8 37)) (not (= x3 6)))) (assert (or (not (= x8 35)) (not (= x2 4)) (not (= x7 32)))) (assert (or (not (= x9 41)) (not (= x10 51)) (not (= x3 8)))) (assert (or (not (= x1 2)) (not (= x6 25)) (not (= x5 16)))) (assert (or (not (= x9 39)) (not (= x10 55)) (not (= x4 9)))) (assert (or (not (= x8 37)) (not (= x7 31)) (not (= x3 6)))) (assert (or (not (= x9 39)) (not (= x10 55)) (not (= x3 8)))) (assert (or (not (= x10 51)) (not (= x4 9)) (not (= x9 44)))) (assert (or (not (= x13 62)) (not (= x4 10)) (not (= x12 60)))) (assert (or (not (= x9 38)) (not (= x8 33)) (not (= x2 4)))) (assert (or (not (= x10 48)) (not (= x11 58)) (not (= x3 8)))) (assert (or (not (= x8 36)) (not (= x8 33)) (not (= x3 6)))) (assert (or (not (= x6 21)) (not (= x1 1)) (not (= x5 17)))) (assert (or (not (= x9 45)) (not (= x10 54)) (not (= x4 9)))) (assert (or (not (= x8 36)) (not (= x8 33)) (not (= x2 4)))) (assert (or (not (= x6 24)) (not (= x1 1)) (not (= x5 16)))) (assert (or (not (= x2 4)) (not (= x7 32)) (not (= x8 34)))) (assert (or (not (= x9 46)) (not (= x10 51)) (not (= x4 9)))) (assert (or (not (= x9 43)) (not (= x10 49)) (not (= x4 9)))) (assert (or (not (= x7 30)) (not (= x2 4)) (not (= x8 34)))) (assert (or (not (= x9 45)) (not (= x10 53)) (not (= x4 9)))) (assert (or (not (= x6 22)) (not (= x1 1)) (not (= x5 16)))) (assert (or (not (= x6 26)) (not (= x5 19)) (not (= x2 3)))) (assert (or (not (= x9 46)) (not (= x10 50)) (not (= x4 9)))) (assert (or (not (= x6 26)) (not (= x5 19)) (not (= x1 1)))) (assert (or (not (= x9 45)) (not (= x3 7)) (not (= x10 50)))) (assert (or (not (= x6 20)) (not (= x2 3)) (not (= x6 27)))) (assert (or (not (= x9 41)) (not (= x3 7)) (not (= x10 51)))) (assert (or (not (= x3 6)) (not (= x12 61)) (not (= x4 9)) (not (= x11 59)))) (assert (or (not (= x5 19)) (not (= x6 22)) (not (= x2 3)))) (assert (or (not (= x7 29)) (not (= x8 35)) (not (= x2 5)))) (assert (or (not (= x10 50)) (not (= x4 9)) (not (= x9 42)))) (assert (or (not (= x7 29)) (not (= x8 35)) (not (= x3 6)))) (assert (or (not (= x10 51)) (not (= x9 39)) (not (= x4 9)))) (assert (or (not (= x10 51)) (not (= x9 39)) (not (= x3 8)))) (assert (or (not (= x9 47)) (not (= x3 7)) (not (= x10 54)))) (assert (or (not (= x7 32)) (not (= x3 6)) (not (= x8 34)))) (assert (or (not (= x10 48)) (not (= x10 54)) (not (= x4 9)))) (assert (or (not (= x10 48)) (not (= x10 53)) (not (= x4 9)))) (assert (or (not (= x10 49)) (not (= x4 9)) (not (= x9 44)))) (assert (or (not (= x10 53)) (not (= x3 8)) (not (= x9 42)))) (assert (or (not (= x9 46)) (not (= x10 53)) (not (= x4 9)))) (assert (or (not (= x6 25)) (not (= x2 3)) (not (= x5 16)))) (assert (or (not (= x2 5)) (not (= x9 38)) (not (= x7 31)))) (assert (or (not (= x9 46)) (not (= x10 56)) (not (= x3 8)))) (assert (or (not (= x9 47)) (not (= x3 7)) (not (= x10 53)))) (assert (or (not (= x6 20)) (not (= x1 1)) (not (= x6 27)))) (assert (or (not (= x6 22)) (not (= x2 3)) (not (= x5 16)))) (assert (or (not (= x6 23)) (not (= x2 3)) (not (= x5 16)))) (assert (or (not (= x9 46)) (not (= x10 55)) (not (= x4 9)))) (assert (or (not (= x9 39)) (not (= x10 56)) (not (= x4 9)))) (assert (or (not (= x10 53)) (not (= x4 9)) (not (= x9 42)))) (assert (or (not (= x5 18)) (not (= x6 25)) (not (= x2 3)))) (assert (or (not (= x5 18)) (not (= x6 25)) (not (= x1 1)))) (assert (or (not (= x9 39)) (not (= x10 56)) (not (= x3 8)))) (assert (or (not (= x10 51)) (not (= x4 9)) (not (= x9 42)))) (assert (or (not (= x10 49)) (not (= x4 9)) (not (= x9 42)))) (assert (or (not (= x3 7)) (not (= x10 52)) (not (= x10 48)))) (assert (or (not (= x6 26)) (not (= x2 3)) (not (= x5 16)))) (assert (or (not (= x9 45)) (not (= x3 7)) (not (= x10 49)))) (assert (or (not (= x2 5)) (not (= x9 38)) (not (= x7 32)))) (assert (or (not (= x1 2)) (not (= x7 28)))) (assert (or (not (= x3 8)) (not (= x9 39)))) (assert (or (not (= x2 5)) (not (= x9 38)))) (assert (or (not (= x2 5)) (not (= x7 29)))) (assert (or (not (= x1 1)) (not (= x6 20)))) (assert (or (not (= x3 7)) (not (= x10 48)))) (assert (or (not (= x3 7)) (not (= x10 49)))) (assert (or (not (= x4 10)) (not (= x12 60)))) (assert (or (not (= x4 11)) (not (= x13 62)))) (assert (or (not (= x2 4)) (not (= x8 34)))) (assert (or (not (= x2 4)) (not (= x8 33)))) (assert (or (not (= x1 2)) (not (= x5 13)))) (assert (or (not (= x4 11)) (not (= x11 59)))) (assert (or (not (= x4 10)) (not (= x12 61)))) (assert (or (not (= x1 1)) (not (= x6 21)))) (assert (or (not (= x3 8)) (not (= x11 58)))) (check-sat)