1 #2 := false |
|
2 #9 := 0::int |
|
3 decl uf_3 :: int |
|
4 #21 := uf_3 |
|
5 #130 := -1::int |
|
6 #131 := (* -1::int uf_3) |
|
7 #154 := (>= uf_3 0::int) |
|
8 #161 := (ite #154 uf_3 #131) |
|
9 #648 := (* -1::int #161) |
|
10 #651 := (+ #131 #648) |
|
11 #657 := (<= #651 0::int) |
|
12 #341 := (= #131 #161) |
|
13 #155 := (not #154) |
|
14 #649 := (+ uf_3 #648) |
|
15 #650 := (<= #649 0::int) |
|
16 #254 := (= uf_3 #161) |
|
17 #646 := [hypothesis]: #154 |
|
18 #255 := (or #155 #254) |
|
19 #342 := [def-axiom]: #255 |
|
20 #652 := [unit-resolution #342 #646]: #254 |
|
21 #290 := (not #254) |
|
22 #653 := (or #290 #650) |
|
23 #655 := [th-lemma]: #653 |
|
24 #295 := [unit-resolution #655 #652]: #650 |
|
25 #346 := (>= #161 0::int) |
|
26 #274 := (not #346) |
|
27 decl uf_2 :: (-> T1 int) |
|
28 decl uf_1 :: (-> int T1) |
|
29 #166 := (uf_1 #161) |
|
30 #169 := (uf_2 #166) |
|
31 #172 := (= #161 #169) |
|
32 #175 := (not #172) |
|
33 #23 := (- uf_3) |
|
34 #22 := (< uf_3 0::int) |
|
35 #24 := (ite #22 #23 uf_3) |
|
36 #25 := (uf_1 #24) |
|
37 #26 := (uf_2 #25) |
|
38 #27 := (= #26 #24) |
|
39 #28 := (not #27) |
|
40 #178 := (iff #28 #175) |
|
41 #134 := (ite #22 #131 uf_3) |
|
42 #137 := (uf_1 #134) |
|
43 #140 := (uf_2 #137) |
|
44 #146 := (= #134 #140) |
|
45 #151 := (not #146) |
|
46 #176 := (iff #151 #175) |
|
47 #173 := (iff #146 #172) |
|
48 #170 := (= #140 #169) |
|
49 #167 := (= #137 #166) |
|
50 #164 := (= #134 #161) |
|
51 #158 := (ite #155 #131 uf_3) |
|
52 #162 := (= #158 #161) |
|
53 #163 := [rewrite]: #162 |
|
54 #159 := (= #134 #158) |
|
55 #156 := (iff #22 #155) |
|
56 #157 := [rewrite]: #156 |
|
57 #160 := [monotonicity #157]: #159 |
|
58 #165 := [trans #160 #163]: #164 |
|
59 #168 := [monotonicity #165]: #167 |
|
60 #171 := [monotonicity #168]: #170 |
|
61 #174 := [monotonicity #165 #171]: #173 |
|
62 #177 := [monotonicity #174]: #176 |
|
63 #152 := (iff #28 #151) |
|
64 #149 := (iff #27 #146) |
|
65 #143 := (= #140 #134) |
|
66 #147 := (iff #143 #146) |
|
67 #148 := [rewrite]: #147 |
|
68 #144 := (iff #27 #143) |
|
69 #135 := (= #24 #134) |
|
70 #132 := (= #23 #131) |
|
71 #133 := [rewrite]: #132 |
|
72 #136 := [monotonicity #133]: #135 |
|
73 #141 := (= #26 #140) |
|
74 #138 := (= #25 #137) |
|
75 #139 := [monotonicity #136]: #138 |
|
76 #142 := [monotonicity #139]: #141 |
|
77 #145 := [monotonicity #142 #136]: #144 |
|
78 #150 := [trans #145 #148]: #149 |
|
79 #153 := [monotonicity #150]: #152 |
|
80 #179 := [trans #153 #177]: #178 |
|
81 #129 := [asserted]: #28 |
|
82 #180 := [mp #129 #179]: #175 |
|
83 #10 := (:var 0 int) |
|
84 #12 := (uf_1 #10) |
|
85 #678 := (pattern #12) |
|
86 #70 := (>= #10 0::int) |
|
87 #71 := (not #70) |
|
88 #13 := (uf_2 #12) |
|
89 #52 := (= #10 #13) |
|
90 #77 := (or #52 #71) |
|
91 #679 := (forall (vars (?x2 int)) (:pat #678) #77) |
|
92 #82 := (forall (vars (?x2 int)) #77) |
|
93 #682 := (iff #82 #679) |
|
94 #680 := (iff #77 #77) |
|
95 #681 := [refl]: #680 |
|
96 #683 := [quant-intro #681]: #682 |
|
97 #183 := (~ #82 #82) |
|
98 #195 := (~ #77 #77) |
|
99 #196 := [refl]: #195 |
|
100 #181 := [nnf-pos #196]: #183 |
|
101 #14 := (= #13 #10) |
|
102 #11 := (<= 0::int #10) |
|
103 #15 := (implies #11 #14) |
|
104 #16 := (forall (vars (?x2 int)) #15) |
|
105 #85 := (iff #16 #82) |
|
106 #59 := (not #11) |
|
107 #60 := (or #59 #52) |
|
108 #65 := (forall (vars (?x2 int)) #60) |
|
109 #83 := (iff #65 #82) |
|
110 #80 := (iff #60 #77) |
|
111 #74 := (or #71 #52) |
|
112 #78 := (iff #74 #77) |
|
113 #79 := [rewrite]: #78 |
|
114 #75 := (iff #60 #74) |
|
115 #72 := (iff #59 #71) |
|
116 #68 := (iff #11 #70) |
|
117 #69 := [rewrite]: #68 |
|
118 #73 := [monotonicity #69]: #72 |
|
119 #76 := [monotonicity #73]: #75 |
|
120 #81 := [trans #76 #79]: #80 |
|
121 #84 := [quant-intro #81]: #83 |
|
122 #66 := (iff #16 #65) |
|
123 #63 := (iff #15 #60) |
|
124 #56 := (implies #11 #52) |
|
125 #61 := (iff #56 #60) |
|
126 #62 := [rewrite]: #61 |
|
127 #57 := (iff #15 #56) |
|
128 #54 := (iff #14 #52) |
|
129 #55 := [rewrite]: #54 |
|
130 #58 := [monotonicity #55]: #57 |
|
131 #64 := [trans #58 #62]: #63 |
|
132 #67 := [quant-intro #64]: #66 |
|
133 #86 := [trans #67 #84]: #85 |
|
134 #51 := [asserted]: #16 |
|
135 #87 := [mp #51 #86]: #82 |
|
136 #197 := [mp~ #87 #181]: #82 |
|
137 #684 := [mp #197 #683]: #679 |
|
138 #321 := (not #679) |
|
139 #451 := (or #321 #172 #274) |
|
140 #327 := (or #172 #274) |
|
141 #658 := (or #321 #327) |
|
142 #333 := (iff #658 #451) |
|
143 #665 := [rewrite]: #333 |
|
144 #332 := [quant-inst]: #658 |
|
145 #666 := [mp #332 #665]: #451 |
|
146 #296 := [unit-resolution #666 #684 #180]: #274 |
|
147 #656 := [th-lemma #646 #296 #295]: false |
|
148 #654 := [lemma #656]: #155 |
|
149 #256 := (or #154 #341) |
|
150 #343 := [def-axiom]: #256 |
|
151 #644 := [unit-resolution #343 #654]: #341 |
|
152 #366 := (not #341) |
|
153 #367 := (or #366 #657) |
|
154 #368 := [th-lemma]: #367 |
|
155 #369 := [unit-resolution #368 #644]: #657 |
|
156 #647 := (<= #161 0::int) |
|
157 #262 := (or #647 #346) |
|
158 #639 := [th-lemma]: #262 |
|
159 #640 := [unit-resolution #639 #296]: #647 |
|
160 [th-lemma #654 #640 #369]: false |
|
161 unsat |
|