1 #2 := false |
|
2 decl uf_2 :: (-> T2 T3 T3) |
|
3 decl uf_4 :: T3 |
|
4 #15 := uf_4 |
|
5 decl uf_6 :: (-> int T2) |
|
6 #48 := 2::int |
|
7 #49 := (uf_6 2::int) |
|
8 #50 := (uf_2 #49 uf_4) |
|
9 #23 := 1::int |
|
10 #44 := (uf_6 1::int) |
|
11 #51 := (uf_2 #44 #50) |
|
12 decl uf_1 :: (-> T1 T3 T3) |
|
13 #45 := (uf_2 #44 uf_4) |
|
14 #31 := 0::int |
|
15 #43 := (uf_6 0::int) |
|
16 #46 := (uf_2 #43 #45) |
|
17 decl uf_5 :: T1 |
|
18 #19 := uf_5 |
|
19 #47 := (uf_1 uf_5 #46) |
|
20 #52 := (= #47 #51) |
|
21 #266 := (uf_1 uf_5 #45) |
|
22 decl uf_3 :: (-> T1 T2 T2) |
|
23 #352 := (uf_3 uf_5 #43) |
|
24 #267 := (uf_2 #352 #266) |
|
25 #797 := (= #267 #51) |
|
26 #795 := (= #51 #267) |
|
27 #758 := (= #50 #266) |
|
28 #521 := (uf_1 uf_5 uf_4) |
|
29 #522 := (uf_3 uf_5 #44) |
|
30 #523 := (uf_2 #522 #521) |
|
31 #756 := (= #523 #266) |
|
32 #616 := (= #266 #523) |
|
33 #6 := (:var 0 T3) |
|
34 #4 := (:var 2 T1) |
|
35 #10 := (uf_1 #4 #6) |
|
36 #5 := (:var 1 T2) |
|
37 #9 := (uf_3 #4 #5) |
|
38 #11 := (uf_2 #9 #10) |
|
39 #683 := (pattern #11) |
|
40 #7 := (uf_2 #5 #6) |
|
41 #8 := (uf_1 #4 #7) |
|
42 #682 := (pattern #8) |
|
43 #12 := (= #8 #11) |
|
44 #684 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3)) (:pat #682 #683) #12) |
|
45 #13 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3)) #12) |
|
46 #687 := (iff #13 #684) |
|
47 #685 := (iff #12 #12) |
|
48 #686 := [refl]: #685 |
|
49 #688 := [quant-intro #686]: #687 |
|
50 #195 := (~ #13 #13) |
|
51 #193 := (~ #12 #12) |
|
52 #194 := [refl]: #193 |
|
53 #196 := [nnf-pos #194]: #195 |
|
54 #69 := [asserted]: #13 |
|
55 #197 := [mp~ #69 #196]: #13 |
|
56 #689 := [mp #197 #688]: #684 |
|
57 #345 := (not #684) |
|
58 #604 := (or #345 #616) |
|
59 #606 := [quant-inst]: #604 |
|
60 #277 := [unit-resolution #606 #689]: #616 |
|
61 #757 := [symm #277]: #756 |
|
62 #754 := (= #50 #523) |
|
63 #569 := (= uf_4 #521) |
|
64 #14 := (:var 0 T1) |
|
65 #16 := (uf_1 #14 uf_4) |
|
66 #690 := (pattern #16) |
|
67 #71 := (= uf_4 #16) |
|
68 #691 := (forall (vars (?x4 T1)) (:pat #690) #71) |
|
69 #74 := (forall (vars (?x4 T1)) #71) |
|
70 #694 := (iff #74 #691) |
|
71 #692 := (iff #71 #71) |
|
72 #693 := [refl]: #692 |
|
73 #695 := [quant-intro #693]: #694 |
|
74 #180 := (~ #74 #74) |
|
75 #198 := (~ #71 #71) |
|
76 #199 := [refl]: #198 |
|
77 #178 := [nnf-pos #199]: #180 |
|
78 #17 := (= #16 uf_4) |
|
79 #18 := (forall (vars (?x4 T1)) #17) |
|
80 #75 := (iff #18 #74) |
|
81 #72 := (iff #17 #71) |
|
82 #73 := [rewrite]: #72 |
|
83 #76 := [quant-intro #73]: #75 |
|
84 #70 := [asserted]: #18 |
|
85 #79 := [mp #70 #76]: #74 |
|
86 #200 := [mp~ #79 #178]: #74 |
|
87 #696 := [mp #200 #695]: #691 |
|
88 #572 := (not #691) |
|
89 #573 := (or #572 #569) |
|
90 #574 := [quant-inst]: #573 |
|
91 #282 := [unit-resolution #574 #696]: #569 |
|
92 #752 := (= #49 #522) |
|
93 decl uf_7 :: (-> T2 int) |
|
94 #666 := (uf_7 #44) |
|
95 #595 := (+ 1::int #666) |
|
96 #597 := (uf_6 #595) |
|
97 #748 := (= #597 #522) |
|
98 #605 := (= #522 #597) |
|
99 #20 := (:var 0 T2) |
|
100 #22 := (uf_7 #20) |
|
101 #698 := (pattern #22) |
|
102 #21 := (uf_3 uf_5 #20) |
|
103 #697 := (pattern #21) |
|
104 #78 := (+ 1::int #22) |
|
105 #82 := (uf_6 #78) |
|
106 #85 := (= #21 #82) |
|
107 #699 := (forall (vars (?x5 T2)) (:pat #697 #698) #85) |
|
108 #88 := (forall (vars (?x5 T2)) #85) |
|
109 #702 := (iff #88 #699) |
|
110 #700 := (iff #85 #85) |
|
111 #701 := [refl]: #700 |
|
112 #703 := [quant-intro #701]: #702 |
|
113 #181 := (~ #88 #88) |
|
114 #201 := (~ #85 #85) |
|
115 #202 := [refl]: #201 |
|
116 #182 := [nnf-pos #202]: #181 |
|
117 #24 := (+ #22 1::int) |
|
118 #25 := (uf_6 #24) |
|
119 #26 := (= #21 #25) |
|
120 #27 := (forall (vars (?x5 T2)) #26) |
|
121 #89 := (iff #27 #88) |
|
122 #86 := (iff #26 #85) |
|
123 #83 := (= #25 #82) |
|
124 #80 := (= #24 #78) |
|
125 #81 := [rewrite]: #80 |
|
126 #84 := [monotonicity #81]: #83 |
|
127 #87 := [monotonicity #84]: #86 |
|
128 #90 := [quant-intro #87]: #89 |
|
129 #77 := [asserted]: #27 |
|
130 #93 := [mp #77 #90]: #88 |
|
131 #203 := [mp~ #93 #182]: #88 |
|
132 #704 := [mp #203 #703]: #699 |
|
133 #607 := (not #699) |
|
134 #600 := (or #607 #605) |
|
135 #601 := [quant-inst]: #600 |
|
136 #269 := [unit-resolution #601 #704]: #605 |
|
137 #749 := [symm #269]: #748 |
|
138 #750 := (= #49 #597) |
|
139 #499 := (uf_7 #597) |
|
140 #337 := (uf_6 #499) |
|
141 #318 := (= #337 #597) |
|
142 #28 := (uf_6 #22) |
|
143 #92 := (= #20 #28) |
|
144 #705 := (forall (vars (?x6 T2)) (:pat #698) #92) |
|
145 #96 := (forall (vars (?x6 T2)) #92) |
|
146 #706 := (iff #96 #705) |
|
147 #708 := (iff #705 #705) |
|
148 #709 := [rewrite]: #708 |
|
149 #707 := [rewrite]: #706 |
|
150 #710 := [trans #707 #709]: #706 |
|
151 #183 := (~ #96 #96) |
|
152 #204 := (~ #92 #92) |
|
153 #205 := [refl]: #204 |
|
154 #184 := [nnf-pos #205]: #183 |
|
155 #29 := (= #28 #20) |
|
156 #30 := (forall (vars (?x6 T2)) #29) |
|
157 #97 := (iff #30 #96) |
|
158 #94 := (iff #29 #92) |
|
159 #95 := [rewrite]: #94 |
|
160 #98 := [quant-intro #95]: #97 |
|
161 #91 := [asserted]: #30 |
|
162 #101 := [mp #91 #98]: #96 |
|
163 #206 := [mp~ #101 #184]: #96 |
|
164 #711 := [mp #206 #710]: #705 |
|
165 #376 := (not #705) |
|
166 #325 := (or #376 #318) |
|
167 #316 := (= #597 #337) |
|
168 #326 := (or #376 #316) |
|
169 #328 := (iff #326 #325) |
|
170 #329 := (iff #325 #325) |
|
171 #310 := [rewrite]: #329 |
|
172 #323 := (iff #316 #318) |
|
173 #324 := [rewrite]: #323 |
|
174 #317 := [monotonicity #324]: #328 |
|
175 #312 := [trans #317 #310]: #328 |
|
176 #327 := [quant-inst]: #326 |
|
177 #313 := [mp #327 #312]: #325 |
|
178 #271 := [unit-resolution #313 #711]: #318 |
|
179 #746 := (= #49 #337) |
|
180 #744 := (= 2::int #499) |
|
181 #742 := (= #499 2::int) |
|
182 #578 := -1::int |
|
183 #513 := (* -1::int #666) |
|
184 #514 := (+ #499 #513) |
|
185 #474 := (<= #514 1::int) |
|
186 #512 := (= #514 1::int) |
|
187 #504 := (>= #666 -1::int) |
|
188 #586 := (>= #666 1::int) |
|
189 #378 := (= #666 1::int) |
|
190 #32 := (:var 0 int) |
|
191 #34 := (uf_6 #32) |
|
192 #712 := (pattern #34) |
|
193 #118 := (>= #32 0::int) |
|
194 #119 := (not #118) |
|
195 #35 := (uf_7 #34) |
|
196 #100 := (= #32 #35) |
|
197 #125 := (or #100 #119) |
|
198 #713 := (forall (vars (?x7 int)) (:pat #712) #125) |
|
199 #130 := (forall (vars (?x7 int)) #125) |
|
200 #716 := (iff #130 #713) |
|
201 #714 := (iff #125 #125) |
|
202 #715 := [refl]: #714 |
|
203 #717 := [quant-intro #715]: #716 |
|
204 #185 := (~ #130 #130) |
|
205 #207 := (~ #125 #125) |
|
206 #208 := [refl]: #207 |
|
207 #186 := [nnf-pos #208]: #185 |
|
208 #36 := (= #35 #32) |
|
209 #33 := (<= 0::int #32) |
|
210 #37 := (implies #33 #36) |
|
211 #38 := (forall (vars (?x7 int)) #37) |
|
212 #133 := (iff #38 #130) |
|
213 #107 := (not #33) |
|
214 #108 := (or #107 #100) |
|
215 #113 := (forall (vars (?x7 int)) #108) |
|
216 #131 := (iff #113 #130) |
|
217 #128 := (iff #108 #125) |
|
218 #122 := (or #119 #100) |
|
219 #126 := (iff #122 #125) |
|
220 #127 := [rewrite]: #126 |
|
221 #123 := (iff #108 #122) |
|
222 #120 := (iff #107 #119) |
|
223 #116 := (iff #33 #118) |
|
224 #117 := [rewrite]: #116 |
|
225 #121 := [monotonicity #117]: #120 |
|
226 #124 := [monotonicity #121]: #123 |
|
227 #129 := [trans #124 #127]: #128 |
|
228 #132 := [quant-intro #129]: #131 |
|
229 #114 := (iff #38 #113) |
|
230 #111 := (iff #37 #108) |
|
231 #104 := (implies #33 #100) |
|
232 #109 := (iff #104 #108) |
|
233 #110 := [rewrite]: #109 |
|
234 #105 := (iff #37 #104) |
|
235 #102 := (iff #36 #100) |
|
236 #103 := [rewrite]: #102 |
|
237 #106 := [monotonicity #103]: #105 |
|
238 #112 := [trans #106 #110]: #111 |
|
239 #115 := [quant-intro #112]: #114 |
|
240 #134 := [trans #115 #132]: #133 |
|
241 #99 := [asserted]: #38 |
|
242 #135 := [mp #99 #134]: #130 |
|
243 #209 := [mp~ #135 #186]: #130 |
|
244 #718 := [mp #209 #717]: #713 |
|
245 #673 := (not #713) |
|
246 #365 := (or #673 #378) |
|
247 #307 := (>= 1::int 0::int) |
|
248 #668 := (not #307) |
|
249 #669 := (= 1::int #666) |
|
250 #655 := (or #669 #668) |
|
251 #366 := (or #673 #655) |
|
252 #645 := (iff #366 #365) |
|
253 #360 := (iff #365 #365) |
|
254 #643 := [rewrite]: #360 |
|
255 #654 := (iff #655 #378) |
|
256 #374 := (or #378 false) |
|
257 #653 := (iff #374 #378) |
|
258 #650 := [rewrite]: #653 |
|
259 #375 := (iff #655 #374) |
|
260 #651 := (iff #668 false) |
|
261 #1 := true |
|
262 #670 := (not true) |
|
263 #677 := (iff #670 false) |
|
264 #678 := [rewrite]: #677 |
|
265 #381 := (iff #668 #670) |
|
266 #379 := (iff #307 true) |
|
267 #380 := [rewrite]: #379 |
|
268 #274 := [monotonicity #380]: #381 |
|
269 #652 := [trans #274 #678]: #651 |
|
270 #656 := (iff #669 #378) |
|
271 #363 := [rewrite]: #656 |
|
272 #649 := [monotonicity #363 #652]: #375 |
|
273 #364 := [trans #649 #650]: #654 |
|
274 #646 := [monotonicity #364]: #645 |
|
275 #647 := [trans #646 #643]: #645 |
|
276 #367 := [quant-inst]: #366 |
|
277 #644 := [mp #367 #647]: #365 |
|
278 #272 := [unit-resolution #644 #718]: #378 |
|
279 #270 := (not #378) |
|
280 #273 := (or #270 #586) |
|
281 #725 := [th-lemma]: #273 |
|
282 #726 := [unit-resolution #725 #272]: #586 |
|
283 #727 := (not #586) |
|
284 #728 := (or #727 #504) |
|
285 #729 := [th-lemma]: #728 |
|
286 #730 := [unit-resolution #729 #726]: #504 |
|
287 #481 := (not #504) |
|
288 #496 := (or #673 #481 #512) |
|
289 #509 := (>= #595 0::int) |
|
290 #468 := (not #509) |
|
291 #501 := (= #595 #499) |
|
292 #503 := (or #501 #468) |
|
293 #497 := (or #673 #503) |
|
294 #470 := (iff #497 #496) |
|
295 #491 := (or #481 #512) |
|
296 #498 := (or #673 #491) |
|
297 #467 := (iff #498 #496) |
|
298 #469 := [rewrite]: #467 |
|
299 #459 := (iff #497 #498) |
|
300 #494 := (iff #503 #491) |
|
301 #488 := (or #512 #481) |
|
302 #492 := (iff #488 #491) |
|
303 #493 := [rewrite]: #492 |
|
304 #489 := (iff #503 #488) |
|
305 #486 := (iff #468 #481) |
|
306 #525 := (iff #509 #504) |
|
307 #480 := [rewrite]: #525 |
|
308 #487 := [monotonicity #480]: #486 |
|
309 #510 := (iff #501 #512) |
|
310 #524 := [rewrite]: #510 |
|
311 #490 := [monotonicity #524 #487]: #489 |
|
312 #495 := [trans #490 #493]: #494 |
|
313 #460 := [monotonicity #495]: #459 |
|
314 #471 := [trans #460 #469]: #470 |
|
315 #482 := [quant-inst]: #497 |
|
316 #473 := [mp #482 #471]: #496 |
|
317 #731 := [unit-resolution #473 #718 #730]: #512 |
|
318 #732 := (not #512) |
|
319 #733 := (or #732 #474) |
|
320 #734 := [th-lemma]: #733 |
|
321 #735 := [unit-resolution #734 #731]: #474 |
|
322 #475 := (>= #514 1::int) |
|
323 #736 := (or #732 #475) |
|
324 #737 := [th-lemma]: #736 |
|
325 #738 := [unit-resolution #737 #731]: #475 |
|
326 #582 := (<= #666 1::int) |
|
327 #739 := (or #270 #582) |
|
328 #740 := [th-lemma]: #739 |
|
329 #741 := [unit-resolution #740 #272]: #582 |
|
330 #743 := [th-lemma #726 #741 #738 #735]: #742 |
|
331 #745 := [symm #743]: #744 |
|
332 #747 := [monotonicity #745]: #746 |
|
333 #751 := [trans #747 #271]: #750 |
|
334 #753 := [trans #751 #749]: #752 |
|
335 #755 := [monotonicity #753 #282]: #754 |
|
336 #759 := [trans #755 #757]: #758 |
|
337 #792 := (= #44 #352) |
|
338 #358 := (uf_7 #43) |
|
339 #613 := (+ 1::int #358) |
|
340 #617 := (uf_6 #613) |
|
341 #788 := (= #617 #352) |
|
342 #598 := (= #352 #617) |
|
343 #608 := (or #607 #598) |
|
344 #609 := [quant-inst]: #608 |
|
345 #760 := [unit-resolution #609 #704]: #598 |
|
346 #789 := [symm #760]: #788 |
|
347 #790 := (= #44 #617) |
|
348 #575 := (uf_7 #617) |
|
349 #390 := (uf_6 #575) |
|
350 #382 := (= #390 #617) |
|
351 #385 := (or #376 #382) |
|
352 #392 := (= #617 #390) |
|
353 #386 := (or #376 #392) |
|
354 #387 := (iff #386 #385) |
|
355 #369 := (iff #385 #385) |
|
356 #370 := [rewrite]: #369 |
|
357 #383 := (iff #392 #382) |
|
358 #384 := [rewrite]: #383 |
|
359 #368 := [monotonicity #384]: #387 |
|
360 #361 := [trans #368 #370]: #387 |
|
361 #377 := [quant-inst]: #386 |
|
362 #371 := [mp #377 #361]: #385 |
|
363 #761 := [unit-resolution #371 #711]: #382 |
|
364 #786 := (= #44 #390) |
|
365 #784 := (= 1::int #575) |
|
366 #782 := (= #575 1::int) |
|
367 #568 := (* -1::int #575) |
|
368 #579 := (+ #358 #568) |
|
369 #535 := (<= #579 -1::int) |
|
370 #557 := (= #579 -1::int) |
|
371 #561 := (>= #358 -1::int) |
|
372 #585 := (>= #358 0::int) |
|
373 #676 := (= #358 0::int) |
|
374 #315 := (or #673 #676) |
|
375 #268 := (>= 0::int 0::int) |
|
376 #354 := (not #268) |
|
377 #355 := (= 0::int #358) |
|
378 #359 := (or #355 #354) |
|
379 #657 := (or #673 #359) |
|
380 #320 := (iff #657 #315) |
|
381 #322 := (iff #315 #315) |
|
382 #659 := [rewrite]: #322 |
|
383 #672 := (iff #359 #676) |
|
384 #675 := (or #676 false) |
|
385 #330 := (iff #675 #676) |
|
386 #335 := [rewrite]: #330 |
|
387 #681 := (iff #359 #675) |
|
388 #679 := (iff #354 false) |
|
389 #343 := (iff #354 #670) |
|
390 #332 := (iff #268 true) |
|
391 #463 := [rewrite]: #332 |
|
392 #344 := [monotonicity #463]: #343 |
|
393 #680 := [trans #344 #678]: #679 |
|
394 #338 := (iff #355 #676) |
|
395 #674 := [rewrite]: #338 |
|
396 #671 := [monotonicity #674 #680]: #681 |
|
397 #331 := [trans #671 #335]: #672 |
|
398 #321 := [monotonicity #331]: #320 |
|
399 #660 := [trans #321 #659]: #320 |
|
400 #319 := [quant-inst]: #657 |
|
401 #661 := [mp #319 #660]: #315 |
|
402 #762 := [unit-resolution #661 #718]: #676 |
|
403 #763 := (not #676) |
|
404 #764 := (or #763 #585) |
|
405 #765 := [th-lemma]: #764 |
|
406 #766 := [unit-resolution #765 #762]: #585 |
|
407 #767 := (not #585) |
|
408 #768 := (or #767 #561) |
|
409 #769 := [th-lemma]: #768 |
|
410 #770 := [unit-resolution #769 #766]: #561 |
|
411 #564 := (not #561) |
|
412 #549 := (or #673 #557 #564) |
|
413 #570 := (>= #613 0::int) |
|
414 #571 := (not #570) |
|
415 #576 := (= #613 #575) |
|
416 #577 := (or #576 #571) |
|
417 #552 := (or #673 #577) |
|
418 #530 := (iff #552 #549) |
|
419 #551 := (or #557 #564) |
|
420 #554 := (or #673 #551) |
|
421 #556 := (iff #554 #549) |
|
422 #529 := [rewrite]: #556 |
|
423 #555 := (iff #552 #554) |
|
424 #547 := (iff #577 #551) |
|
425 #559 := (iff #571 #564) |
|
426 #562 := (iff #570 #561) |
|
427 #563 := [rewrite]: #562 |
|
428 #565 := [monotonicity #563]: #559 |
|
429 #558 := (iff #576 #557) |
|
430 #560 := [rewrite]: #558 |
|
431 #548 := [monotonicity #560 #565]: #547 |
|
432 #550 := [monotonicity #548]: #555 |
|
433 #531 := [trans #550 #529]: #530 |
|
434 #553 := [quant-inst]: #552 |
|
435 #424 := [mp #553 #531]: #549 |
|
436 #771 := [unit-resolution #424 #718 #770]: #557 |
|
437 #772 := (not #557) |
|
438 #773 := (or #772 #535) |
|
439 #774 := [th-lemma]: #773 |
|
440 #775 := [unit-resolution #774 #771]: #535 |
|
441 #536 := (>= #579 -1::int) |
|
442 #776 := (or #772 #536) |
|
443 #777 := [th-lemma]: #776 |
|
444 #778 := [unit-resolution #777 #771]: #536 |
|
445 #584 := (<= #358 0::int) |
|
446 #779 := (or #763 #584) |
|
447 #780 := [th-lemma]: #779 |
|
448 #781 := [unit-resolution #780 #762]: #584 |
|
449 #783 := [th-lemma #766 #781 #778 #775]: #782 |
|
450 #785 := [symm #783]: #784 |
|
451 #787 := [monotonicity #785]: #786 |
|
452 #791 := [trans #787 #761]: #790 |
|
453 #793 := [trans #791 #789]: #792 |
|
454 #796 := [monotonicity #793 #759]: #795 |
|
455 #798 := [symm #796]: #797 |
|
456 #353 := (= #47 #267) |
|
457 #356 := (or #345 #353) |
|
458 #357 := [quant-inst]: #356 |
|
459 #794 := [unit-resolution #357 #689]: #353 |
|
460 #799 := [trans #794 #798]: #52 |
|
461 #53 := (not #52) |
|
462 #177 := [asserted]: #53 |
|
463 [unit-resolution #177 #799]: false |
|
464 unsat |
|