33010
|
1 |
#2 := false
|
|
2 |
#43 := 0::int
|
|
3 |
decl ?x1!0 :: int
|
|
4 |
#78 := ?x1!0
|
|
5 |
#56 := -2::int
|
|
6 |
#113 := (* -2::int ?x1!0)
|
|
7 |
decl uf_1 :: int
|
|
8 |
#6 := uf_1
|
|
9 |
#8 := 2::int
|
|
10 |
#10 := (* 2::int uf_1)
|
|
11 |
#114 := (+ #10 #113)
|
|
12 |
#115 := (<= #114 0::int)
|
|
13 |
#120 := (not #115)
|
|
14 |
#41 := -1::int
|
|
15 |
#100 := (* -1::int ?x1!0)
|
|
16 |
#101 := (+ uf_1 #100)
|
|
17 |
#102 := (<= #101 0::int)
|
|
18 |
#123 := (or #102 #120)
|
|
19 |
#126 := (not #123)
|
|
20 |
#59 := (* -2::int uf_1)
|
|
21 |
#79 := (* 2::int ?x1!0)
|
|
22 |
#80 := (+ #79 #59)
|
|
23 |
#81 := (>= #80 0::int)
|
|
24 |
#82 := (not #81)
|
|
25 |
#45 := (* -1::int uf_1)
|
|
26 |
#83 := (+ ?x1!0 #45)
|
|
27 |
#84 := (>= #83 0::int)
|
|
28 |
#85 := (or #84 #82)
|
|
29 |
#86 := (not #85)
|
|
30 |
#127 := (iff #86 #126)
|
|
31 |
#124 := (iff #85 #123)
|
|
32 |
#121 := (iff #82 #120)
|
|
33 |
#118 := (iff #81 #115)
|
|
34 |
#107 := (+ #59 #79)
|
|
35 |
#110 := (>= #107 0::int)
|
|
36 |
#116 := (iff #110 #115)
|
|
37 |
#117 := [rewrite]: #116
|
|
38 |
#111 := (iff #81 #110)
|
|
39 |
#108 := (= #80 #107)
|
|
40 |
#109 := [rewrite]: #108
|
|
41 |
#112 := [monotonicity #109]: #111
|
|
42 |
#119 := [trans #112 #117]: #118
|
|
43 |
#122 := [monotonicity #119]: #121
|
|
44 |
#105 := (iff #84 #102)
|
|
45 |
#94 := (+ #45 ?x1!0)
|
|
46 |
#97 := (>= #94 0::int)
|
|
47 |
#103 := (iff #97 #102)
|
|
48 |
#104 := [rewrite]: #103
|
|
49 |
#98 := (iff #84 #97)
|
|
50 |
#95 := (= #83 #94)
|
|
51 |
#96 := [rewrite]: #95
|
|
52 |
#99 := [monotonicity #96]: #98
|
|
53 |
#106 := [trans #99 #104]: #105
|
|
54 |
#125 := [monotonicity #106 #122]: #124
|
|
55 |
#128 := [monotonicity #125]: #127
|
|
56 |
#4 := (:var 0 int)
|
|
57 |
#5 := (pattern #4)
|
|
58 |
#9 := (* 2::int #4)
|
|
59 |
#60 := (+ #9 #59)
|
|
60 |
#58 := (>= #60 0::int)
|
|
61 |
#57 := (not #58)
|
|
62 |
#46 := (+ #4 #45)
|
|
63 |
#44 := (>= #46 0::int)
|
|
64 |
#63 := (or #44 #57)
|
|
65 |
#66 := (forall (vars (?x1 int)) (:pat #5) #63)
|
|
66 |
#69 := (not #66)
|
|
67 |
#87 := (~ #69 #86)
|
|
68 |
#88 := [sk]: #87
|
|
69 |
#11 := (< #9 #10)
|
|
70 |
#7 := (< #4 uf_1)
|
|
71 |
#12 := (implies #7 #11)
|
|
72 |
#13 := (forall (vars (?x1 int)) (:pat #5) #12)
|
|
73 |
#14 := (not #13)
|
|
74 |
#72 := (iff #14 #69)
|
|
75 |
#31 := (not #7)
|
|
76 |
#32 := (or #31 #11)
|
|
77 |
#35 := (forall (vars (?x1 int)) (:pat #5) #32)
|
|
78 |
#38 := (not #35)
|
|
79 |
#70 := (iff #38 #69)
|
|
80 |
#67 := (iff #35 #66)
|
|
81 |
#64 := (iff #32 #63)
|
|
82 |
#61 := (iff #11 #57)
|
|
83 |
#62 := [rewrite]: #61
|
|
84 |
#54 := (iff #31 #44)
|
|
85 |
#42 := (not #44)
|
|
86 |
#49 := (not #42)
|
|
87 |
#52 := (iff #49 #44)
|
|
88 |
#53 := [rewrite]: #52
|
|
89 |
#50 := (iff #31 #49)
|
|
90 |
#47 := (iff #7 #42)
|
|
91 |
#48 := [rewrite]: #47
|
|
92 |
#51 := [monotonicity #48]: #50
|
|
93 |
#55 := [trans #51 #53]: #54
|
|
94 |
#65 := [monotonicity #55 #62]: #64
|
|
95 |
#68 := [quant-intro #65]: #67
|
|
96 |
#71 := [monotonicity #68]: #70
|
|
97 |
#39 := (iff #14 #38)
|
|
98 |
#36 := (iff #13 #35)
|
|
99 |
#33 := (iff #12 #32)
|
|
100 |
#34 := [rewrite]: #33
|
|
101 |
#37 := [quant-intro #34]: #36
|
|
102 |
#40 := [monotonicity #37]: #39
|
|
103 |
#73 := [trans #40 #71]: #72
|
|
104 |
#30 := [asserted]: #14
|
|
105 |
#74 := [mp #30 #73]: #69
|
|
106 |
#91 := [mp~ #74 #88]: #86
|
|
107 |
#92 := [mp #91 #128]: #126
|
|
108 |
#130 := [not-or-elim #92]: #115
|
|
109 |
#93 := (not #102)
|
|
110 |
#129 := [not-or-elim #92]: #93
|
|
111 |
[th-lemma #129 #130]: false
|
|
112 |
unsat
|