(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 13))) (declare-fun x5() Int) (assert (and (>= x5 14) (<= x5 15))) (declare-fun x6() Int) (assert (and (>= x6 16) (<= x6 18))) (declare-fun x7() Int) (assert (and (>= x7 19) (<= x7 24))) (declare-fun x8() Int) (assert (and (>= x8 25) (<= x8 27))) (declare-fun x9() Int) (assert (and (>= x9 28) (<= x9 33))) (declare-fun x10() Int) (assert (and (>= x10 34) (<= x10 38))) (declare-fun x11() Int) (assert (and (>= x11 39) (<= x11 40))) (declare-fun x12() Int) (assert (and (>= x12 41) (<= x12 43))) (declare-fun x13() Int) (assert (and (>= x13 44) (<= x13 53))) (declare-fun x14() Int) (assert (and (>= x14 54) (<= x14 56))) (declare-fun x15() Int) (assert (and (>= x15 57) (<= x15 61))) (declare-fun x16() Int) (assert (and (>= x16 62) (<= x16 63))) (declare-fun x17() Int) (assert (and (>= x17 64) (<= x17 66))) (declare-fun x18() Int) (assert (and (>= x18 67) (<= x18 76))) (declare-fun x19() Int) (assert (and (>= x19 77) (<= x19 84))) (declare-fun x20() Int) (assert (and (>= x20 85) (<= x20 95))) (declare-fun x21() Int) (assert (and (>= x21 96) (<= x21 104))) (declare-fun x22() Int) (assert (and (>= x22 105) (<= x22 106))) (declare-fun x23() Int) (assert (and (>= x23 107) (<= x23 108))) (assert (or (not (= x18 74)) (not (= x13 53)))) (assert (or (not (= x13 45)) (not (= x19 77)))) (assert (or (not (= x19 83)) (not (= x21 104)))) (assert (or (not (= x19 83)) (not (= x21 102)))) (assert (or (not (= x19 83)) (not (= x21 103)))) (assert (or (not (= x20 89)) (not (= x20 85)))) (assert (or (not (= x19 83)) (not (= x21 100)))) (assert (or (not (= x19 83)) (not (= x21 101)))) (assert (or (not (= x18 74)) (not (= x13 45)))) (assert (or (not (= x19 83)) (not (= x21 98)))) (assert (or (not (= x20 89)) (not (= x19 79)))) (assert (or (not (= x18 74)) (not (= x13 46)))) (assert (or (not (= x19 83)) (not (= x21 99)))) (assert (or (not (= x10 34)) (not (= x7 24)))) (assert (or (not (= x19 84)) (not (= x21 96)))) (assert (or (not (= x20 89)) (not (= x19 81)))) (assert (or (not (= x18 74)) (not (= x13 47)))) (assert (or (not (= x19 81)) (not (= x20 87)))) (assert (or (not (= x18 74)) (not (= x13 48)))) (assert (or (not (= x10 34)) (not (= x7 22)))) (assert (or (not (= x20 89)) (not (= x19 80)))) (assert (or (not (= x19 81)) (not (= x20 91)))) (assert (or (not (= x18 74)) (not (= x13 52)))) (assert (or (not (= x21 101)) (not (= x20 85)))) (assert (or (not (= x20 95)) (not (= x20 85)))) (assert (or (not (= x20 88)) (not (= x20 85)))) (assert (or (not (= x19 82)) (not (= x21 99)))) (assert (or (not (= x19 82)) (not (= x21 100)))) (assert (or (not (= x7 23)) (not (= x9 33)))) (assert (or (not (= x19 82)) (not (= x21 101)))) (assert (or (not (= x20 88)) (not (= x19 81)))) (assert (or (not (= x7 23)) (not (= x10 34)))) (assert (or (not (= x19 82)) (not (= x21 102)))) (assert (or (not (= x20 88)) (not (= x19 80)))) (assert (or (not (= x20 88)) (not (= x19 79)))) (assert (or (not (= x3 7)) (not (= x2 3)))) (assert (or (not (= x13 48)) (not (= x18 75)))) (assert (or (not (= x1 1)) (not (= x3 8)))) (assert (or (not (= x18 72)) (not (= x13 51)))) (assert (or (not (= x18 72)) (not (= x13 52)))) (assert (or (not (= x18 72)) (not (= x13 53)))) (assert (or (not (= x13 48)) (not (= x18 73)))) (assert (or (not (= x13 47)) (not (= x19 77)))) (assert (or (not (= x18 72)) (not (= x13 48)))) (assert (or (not (= x20 91)) (not (= x19 79)))) (assert (or (not (= x19 79)) (not (= x20 87)))) (assert (or (not (= x13 47)) (not (= x18 75)))) (assert (or (not (= x13 47)) (not (= x18 76)))) (assert (or (not (= x13 47)) (not (= x18 68)))) (assert (or (not (= x20 90)) (not (= x20 85)))) (assert (or (not (= x13 47)) (not (= x18 72)))) (assert (or (not (= x13 46)) (not (= x19 77)))) (assert (or (not (= x13 47)) (not (= x18 73)))) (assert (or (not (= x18 73)) (not (= x13 52)))) (assert (or (not (= x13 47)) (not (= x18 71)))) (assert (or (not (= x18 73)) (not (= x13 51)))) (assert (or (not (= x19 80)) (not (= x20 91)))) (assert (or (not (= x19 77)) (not (= x13 52)))) (assert (or (not (= x18 73)) (not (= x13 49)))) (assert (or (not (= x20 90)) (not (= x19 81)))) (assert (or (not (= x20 90)) (not (= x19 80)))) (assert (or (not (= x19 80)) (not (= x20 87)))) (assert (or (not (= x20 90)) (not (= x19 79)))) (assert (or (not (= x19 78)) (not (= x21 96)))) (assert (or (not (= x13 53)) (not (= x19 77)))) (assert (or (not (= x9 29)) (not (= x7 24)))) (assert (or (not (= x13 46)) (not (= x18 76)))) (assert (or (not (= x13 46)) (not (= x18 75)))) (assert (or (not (= x13 46)) (not (= x18 73)))) (assert (or (not (= x9 30)) (not (= x7 20)))) (assert (or (not (= x22 105)) (not (= x19 79)))) (assert (or (not (= x20 85)) (not (= x20 91)))) (assert (or (not (= x22 105)) (not (= x19 81)))) (assert (or (not (= x20 93)) (not (= x20 85)))) (assert (or (not (= x22 105)) (not (= x19 80)))) (assert (or (not (= x9 30)) (not (= x7 24)))) (assert (or (not (= x20 93)) (not (= x19 79)))) (assert (or (not (= x20 93)) (not (= x19 80)))) (assert (or (not (= x20 93)) (not (= x19 81)))) (assert (or (not (= x13 46)) (not (= x18 72)))) (assert (or (not (= x13 46)) (not (= x18 71)))) (assert (or (not (= x20 85)) (not (= x20 87)))) (assert (or (not (= x13 45)) (not (= x18 76)))) (assert (or (not (= x13 45)) (not (= x18 72)))) (assert (or (not (= x13 45)) (not (= x18 73)))) (assert (or (not (= x13 45)) (not (= x18 75)))) (assert (or (not (= x21 97)) (not (= x19 78)))) (assert (or (not (= x21 97)) (not (= x20 85)))) (assert (or (not (= x21 97)) (not (= x19 84)))) (assert (or (not (= x21 97)) (not (= x19 83)))) (assert (or (not (= x21 97)) (not (= x19 82)))) (assert (or (not (= x9 31)) (not (= x7 20)))) (assert (or (not (= x20 92)) (not (= x19 81)))) (assert (or (not (= x20 92)) (not (= x19 79)))) (assert (or (not (= x9 31)) (not (= x7 24)))) (assert (or (not (= x20 92)) (not (= x19 80)))) (assert (or (not (= x14 54)) (not (= x18 73)))) (assert (or (not (= x13 45)) (not (= x18 71)))) (assert (or (not (= x19 78)) (not (= x21 100)))) (assert (or (not (= x19 78)) (not (= x21 99)))) (assert (or (not (= x13 45)) (not (= x18 69)))) (assert (or (not (= x19 78)) (not (= x21 102)))) (assert (or (not (= x19 78)) (not (= x21 101)))) (assert (or (not (= x20 92)) (not (= x20 85)))) (assert (or (not (= x2 3)) (not (= x3 8)))) (assert (or (not (= x19 78)) (not (= x21 103)))) (assert (or (not (= x19 78)) (not (= x21 104)))) (assert (or (not (= x21 98)) (not (= x19 78)))) (assert (or (not (= x21 98)) (not (= x19 82)))) (assert (or (not (= x13 53)) (not (= x18 73)))) (assert (or (not (= x13 51)) (not (= x19 77)))) (assert (or (not (= x13 53)) (not (= x18 75)))) (assert (or (not (= x21 98)) (not (= x20 85)))) (assert (or (not (= x20 95)) (not (= x19 79)))) (assert (or (not (= x20 95)) (not (= x19 80)))) (assert (or (not (= x20 95)) (not (= x19 81)))) (assert (or (not (= x21 103)) (not (= x19 82)))) (assert (or (not (= x7 23)) (not (= x9 31)))) (assert (or (not (= x7 23)) (not (= x9 29)))) (assert (or (not (= x7 23)) (not (= x9 30)))) (assert (or (not (= x21 103)) (not (= x20 85)))) (assert (or (not (= x19 83)) (not (= x21 96)))) (assert (or (not (= x20 85)) (not (= x21 99)))) (assert (or (not (= x18 76)) (not (= x13 48)))) (assert (or (not (= x20 85)) (not (= x21 100)))) (assert (or (not (= x20 85)) (not (= x21 102)))) (assert (or (not (= x13 48)) (not (= x19 77)))) (assert (or (not (= x18 69)) (not (= x13 47)))) (assert (or (not (= x20 94)) (not (= x19 81)))) (assert (or (not (= x20 94)) (not (= x19 79)))) (assert (or (not (= x21 104)) (not (= x19 82)))) (assert (or (not (= x20 94)) (not (= x19 80)))) (assert (or (not (= x20 94)) (not (= x20 85)))) (assert (or (not (= x21 104)) (not (= x20 85)))) (assert (or (not (= x19 84)) (not (= x21 100)))) (assert (or (not (= x19 82)) (not (= x21 96)))) (assert (or (not (= x22 105)) (not (= x23 107)))) (assert (or (not (= x19 84)) (not (= x21 99)))) (assert (or (not (= x19 84)) (not (= x21 98)))) (assert (or (not (= x19 84)) (not (= x21 104)))) (assert (or (not (= x20 86)) (not (= x19 79)))) (assert (or (not (= x19 84)) (not (= x21 103)))) (assert (or (not (= x7 21)) (not (= x9 31)))) (assert (or (not (= x20 86)) (not (= x19 80)))) (assert (or (not (= x19 84)) (not (= x21 102)))) (assert (or (not (= x10 34)) (not (= x7 21)))) (assert (or (not (= x18 72)) (not (= x14 54)))) (assert (or (not (= x20 86)) (not (= x19 81)))) (assert (or (not (= x19 84)) (not (= x21 101)))) (assert (or (not (= x10 34)) (not (= x7 20)))) (assert (or (not (= x20 86)) (not (= x20 85)))) (assert (or (not (= x20 86)) (not (= x23 107)))) (assert (or (not (= x20 93)) (not (= x21 102)))) (assert (or (not (= x20 93)) (not (= x21 103)))) (assert (or (not (= x20 89)) (not (= x21 101)))) (assert (or (not (= x20 89)) (not (= x21 97)))) (assert (or (not (= x20 86)) (not (= x21 103)))) (assert (or (not (= x20 94)) (not (= x21 103)))) (assert (or (not (= x20 91)) (not (= x21 101)))) (assert (or (not (= x20 86)) (not (= x21 101)))) (assert (or (not (= x20 95)) (not (= x21 101)))) (assert (or (not (= x20 92)) (not (= x23 107)))) (assert (or (not (= x20 94)) (not (= x21 102)))) (assert (or (not (= x20 91)) (not (= x21 97)))) (assert (or (not (= x20 88)) (not (= x21 101)))) (assert (or (not (= x20 89)) (not (= x21 98)))) (assert (or (not (= x20 87)) (not (= x21 97)))) (assert (or (not (= x20 89)) (not (= x21 103)))) (assert (or (not (= x20 95)) (not (= x21 98)))) (assert (or (not (= x20 93)) (not (= x23 107)))) (assert (or (not (= x20 90)) (not (= x21 99)))) (assert (or (not (= x20 92)) (not (= x21 102)))) (assert (or (not (= x20 89)) (not (= x21 100)))) (assert (or (not (= x20 94)) (not (= x21 99)))) (assert (or (not (= x20 86)) (not (= x21 99)))) (assert (or (not (= x20 91)) (not (= x23 107)))) (assert (or (not (= x20 92)) (not (= x21 103)))) (assert (or (not (= x20 94)) (not (= x21 97)))) (assert (or (not (= x20 92)) (not (= x21 98)))) (assert (or (not (= x20 94)) (not (= x23 107)))) (assert (or (not (= x20 88)) (not (= x21 98)))) (assert (or (not (= x20 86)) (not (= x21 102)))) (assert (or (not (= x20 86)) (not (= x21 97)))) (assert (or (not (= x19 83)) (not (= x23 107)))) (assert (or (not (= x20 88)) (not (= x21 97)))) (assert (or (not (= x20 91)) (not (= x21 100)))) (assert (or (not (= x20 85)) (not (= x23 107)))) (assert (or (not (= x20 92)) (not (= x21 99)))) (assert (or (not (= x20 87)) (not (= x21 104)))) (assert (or (not (= x20 92)) (not (= x21 104)))) (assert (or (not (= x20 90)) (not (= x21 97)))) (assert (or (not (= x19 84)) (not (= x23 107)))) (assert (or (not (= x20 93)) (not (= x21 99)))) (assert (or (not (= x20 93)) (not (= x21 100)))) (assert (or (not (= x20 90)) (not (= x21 104)))) (assert (or (not (= x19 78)) (not (= x23 107)))) (assert (or (not (= x20 95)) (not (= x21 104)))) (assert (or (not (= x20 90)) (not (= x21 98)))) (assert (or (not (= x20 93)) (not (= x21 101)))) (assert (or (not (= x20 92)) (not (= x21 101)))) (assert (or (not (= x20 88)) (not (= x23 107)))) (assert (or (not (= x20 95)) (not (= x21 103)))) (assert (or (not (= x20 87)) (not (= x21 101)))) (assert (or (not (= x20 90)) (not (= x21 103)))) (assert (or (not (= x20 90)) (not (= x21 100)))) (assert (or (not (= x20 95)) (not (= x21 97)))) (assert (or (not (= x20 87)) (not (= x21 100)))) (assert (or (not (= x20 92)) (not (= x21 97)))) (assert (or (not (= x20 91)) (not (= x21 98)))) (assert (or (not (= x20 95)) (not (= x23 107)))) (assert (or (not (= x20 91)) (not (= x21 103)))) (assert (or (not (= x20 86)) (not (= x21 104)))) (assert (or (not (= x20 94)) (not (= x21 100)))) (assert (or (not (= x20 94)) (not (= x21 101)))) (assert (or (not (= x20 90)) (not (= x21 101)))) (assert (or (not (= x20 94)) (not (= x21 98)))) (assert (or (not (= x20 87)) (not (= x21 98)))) (assert (or (not (= x20 88)) (not (= x21 99)))) (assert (or (not (= x20 89)) (not (= x23 107)))) (assert (or (not (= x20 94)) (not (= x21 104)))) (assert (or (not (= x20 87)) (not (= x23 107)))) (assert (or (not (= x20 91)) (not (= x21 104)))) (assert (or (not (= x20 86)) (not (= x21 98)))) (assert (or (not (= x20 89)) (not (= x21 102)))) (assert (or (not (= x20 93)) (not (= x21 97)))) (assert (or (not (= x20 88)) (not (= x21 102)))) (assert (or (not (= x20 92)) (not (= x21 100)))) (assert (or (not (= x20 90)) (not (= x21 102)))) (assert (or (not (= x20 93)) (not (= x21 98)))) (assert (or (not (= x20 88)) (not (= x21 100)))) (assert (or (not (= x20 91)) (not (= x21 102)))) (assert (or (not (= x20 95)) (not (= x21 99)))) (assert (or (not (= x20 91)) (not (= x21 99)))) (assert (or (not (= x20 90)) (not (= x23 107)))) (assert (or (not (= x20 88)) (not (= x21 103)))) (assert (or (not (= x20 87)) (not (= x21 103)))) (assert (or (not (= x20 87)) (not (= x21 99)))) (assert (or (not (= x20 87)) (not (= x21 102)))) (assert (or (not (= x20 88)) (not (= x21 104)))) (assert (or (not (= x20 86)) (not (= x21 100)))) (assert (or (not (= x20 95)) (not (= x21 100)))) (assert (or (not (= x20 89)) (not (= x21 104)))) (assert (or (not (= x20 93)) (not (= x21 104)))) (assert (or (not (= x20 95)) (not (= x21 102)))) (assert (or (not (= x20 89)) (not (= x21 99)))) (assert (or (not (= x19 82)) (not (= x23 107)))) (check-sat)