1 tB2Atlor9W4pSnrAz5nHpw 907 0 |
1 534d3afbd3505abffa6b03e3986bfa7aa3cff358 428 0 |
|
2 #2 := false |
|
3 decl uf_10 :: T1 |
|
4 #38 := uf_10 |
|
5 decl uf_3 :: T1 |
|
6 #21 := uf_3 |
|
7 #45 := (= uf_3 uf_10) |
|
8 decl uf_1 :: (-> int T1) |
|
9 decl uf_2 :: (-> T1 int) |
|
10 #39 := (uf_2 uf_10) |
|
11 #588 := (uf_1 #39) |
|
12 #686 := (= #588 uf_10) |
|
13 #589 := (= uf_10 #588) |
|
14 #4 := (:var 0 T1) |
|
15 #5 := (uf_2 #4) |
|
16 #541 := (pattern #5) |
|
17 #6 := (uf_1 #5) |
|
18 #93 := (= #4 #6) |
|
19 #542 := (forall (vars (?x1 T1)) (:pat #541) #93) |
|
20 #96 := (forall (vars (?x1 T1)) #93) |
|
21 #545 := (iff #96 #542) |
|
22 #543 := (iff #93 #93) |
|
23 #544 := [refl]: #543 |
|
24 #546 := [quant-intro #544]: #545 |
|
25 #454 := (~ #96 #96) |
|
26 #456 := (~ #93 #93) |
|
27 #457 := [refl]: #456 |
|
28 #455 := [nnf-pos #457]: #454 |
|
29 #7 := (= #6 #4) |
|
30 #8 := (forall (vars (?x1 T1)) #7) |
|
31 #97 := (iff #8 #96) |
|
32 #94 := (iff #7 #93) |
|
33 #95 := [rewrite]: #94 |
|
34 #98 := [quant-intro #95]: #97 |
|
35 #92 := [asserted]: #8 |
|
36 #101 := [mp #92 #98]: #96 |
|
37 #452 := [mp~ #101 #455]: #96 |
|
38 #547 := [mp #452 #546]: #542 |
|
39 #590 := (not #542) |
|
40 #595 := (or #590 #589) |
|
41 #596 := [quant-inst]: #595 |
|
42 #680 := [unit-resolution #596 #547]: #589 |
|
43 #687 := [symm #680]: #686 |
|
44 #688 := (= uf_3 #588) |
|
45 #22 := (uf_2 uf_3) |
|
46 #586 := (uf_1 #22) |
|
47 #684 := (= #586 #588) |
|
48 #682 := (= #588 #586) |
|
49 #678 := (= #39 #22) |
|
50 #676 := (= #22 #39) |
|
51 #9 := 0::int |
|
52 #227 := -1::int |
|
53 #230 := (* -1::int #39) |
|
54 #231 := (+ #22 #230) |
|
55 #296 := (<= #231 0::int) |
|
56 #70 := (<= #22 #39) |
|
57 #393 := (iff #70 #296) |
|
58 #394 := [rewrite]: #393 |
|
59 #347 := [asserted]: #70 |
|
60 #395 := [mp #347 #394]: #296 |
|
61 #229 := (>= #231 0::int) |
|
62 decl uf_4 :: (-> T2 T3 real) |
|
63 decl uf_6 :: (-> T1 T3) |
|
64 #25 := (uf_6 uf_3) |
|
65 decl uf_7 :: T2 |
|
66 #27 := uf_7 |
|
67 #28 := (uf_4 uf_7 #25) |
|
68 decl uf_9 :: T2 |
|
69 #33 := uf_9 |
|
70 #34 := (uf_4 uf_9 #25) |
|
71 #46 := (uf_6 uf_10) |
|
72 decl uf_5 :: T2 |
|
73 #24 := uf_5 |
|
74 #47 := (uf_4 uf_5 #46) |
|
75 #48 := (ite #45 #47 #34) |
|
76 #256 := (ite #229 #48 #28) |
|
77 #568 := (= #28 #256) |
|
78 #648 := (not #568) |
|
79 #194 := 0::real |
|
80 #192 := -1::real |
|
81 #265 := (* -1::real #256) |
|
82 #640 := (+ #28 #265) |
|
83 #642 := (>= #640 0::real) |
|
84 #645 := (not #642) |
|
85 #643 := [hypothesis]: #642 |
|
86 decl uf_8 :: T2 |
|
87 #30 := uf_8 |
|
88 #31 := (uf_4 uf_8 #25) |
|
89 #266 := (+ #31 #265) |
|
90 #264 := (>= #266 0::real) |
|
91 #267 := (not #264) |
|
92 #26 := (uf_4 uf_5 #25) |
|
93 decl uf_11 :: T2 |
|
94 #41 := uf_11 |
|
95 #42 := (uf_4 uf_11 #25) |
|
96 #237 := (ite #229 #42 #26) |
|
97 #245 := (* -1::real #237) |
|
98 #246 := (+ #31 #245) |
|
99 #247 := (<= #246 0::real) |
|
100 #248 := (not #247) |
|
101 #272 := (and #248 #267) |
|
102 #40 := (< #22 #39) |
|
103 #49 := (ite #40 #28 #48) |
|
104 #50 := (< #31 #49) |
|
105 #43 := (ite #40 #26 #42) |
|
106 #44 := (< #43 #31) |
|
107 #51 := (and #44 #50) |
|
108 #273 := (iff #51 #272) |
|
109 #270 := (iff #50 #267) |
|
110 #261 := (< #31 #256) |
|
111 #268 := (iff #261 #267) |
|
112 #269 := [rewrite]: #268 |
|
113 #262 := (iff #50 #261) |
|
114 #259 := (= #49 #256) |
|
115 #228 := (not #229) |
|
116 #253 := (ite #228 #28 #48) |
|
117 #257 := (= #253 #256) |
|
118 #258 := [rewrite]: #257 |
|
119 #254 := (= #49 #253) |
|
120 #232 := (iff #40 #228) |
|
121 #233 := [rewrite]: #232 |
|
122 #255 := [monotonicity #233]: #254 |
|
123 #260 := [trans #255 #258]: #259 |
|
124 #263 := [monotonicity #260]: #262 |
|
125 #271 := [trans #263 #269]: #270 |
|
126 #251 := (iff #44 #248) |
|
127 #242 := (< #237 #31) |
|
128 #249 := (iff #242 #248) |
|
129 #250 := [rewrite]: #249 |
|
130 #243 := (iff #44 #242) |
|
131 #240 := (= #43 #237) |
|
132 #234 := (ite #228 #26 #42) |
|
133 #238 := (= #234 #237) |
|
134 #239 := [rewrite]: #238 |
|
135 #235 := (= #43 #234) |
|
136 #236 := [monotonicity #233]: #235 |
|
137 #241 := [trans #236 #239]: #240 |
|
138 #244 := [monotonicity #241]: #243 |
|
139 #252 := [trans #244 #250]: #251 |
|
140 #274 := [monotonicity #252 #271]: #273 |
|
141 #178 := [asserted]: #51 |
|
142 #275 := [mp #178 #274]: #272 |
|
143 #277 := [and-elim #275]: #267 |
|
144 #196 := (* -1::real #31) |
|
145 #197 := (+ #28 #196) |
|
146 #195 := (>= #197 0::real) |
|
147 #193 := (not #195) |
|
148 #213 := (* -1::real #34) |
|
149 #214 := (+ #31 #213) |
|
150 #212 := (>= #214 0::real) |
|
151 #215 := (not #212) |
|
152 #220 := (and #193 #215) |
|
153 #23 := (< #22 #22) |
|
154 #35 := (ite #23 #28 #34) |
|
155 #36 := (< #31 #35) |
|
156 #29 := (ite #23 #26 #28) |
|
157 #32 := (< #29 #31) |
|
158 #37 := (and #32 #36) |
|
159 #221 := (iff #37 #220) |
|
160 #218 := (iff #36 #215) |
|
161 #209 := (< #31 #34) |
|
162 #216 := (iff #209 #215) |
|
163 #217 := [rewrite]: #216 |
|
164 #210 := (iff #36 #209) |
|
165 #207 := (= #35 #34) |
|
166 #202 := (ite false #28 #34) |
|
167 #205 := (= #202 #34) |
|
168 #206 := [rewrite]: #205 |
|
169 #203 := (= #35 #202) |
|
170 #180 := (iff #23 false) |
|
171 #181 := [rewrite]: #180 |
|
172 #204 := [monotonicity #181]: #203 |
|
173 #208 := [trans #204 #206]: #207 |
|
174 #211 := [monotonicity #208]: #210 |
|
175 #219 := [trans #211 #217]: #218 |
|
176 #200 := (iff #32 #193) |
|
177 #189 := (< #28 #31) |
|
178 #198 := (iff #189 #193) |
|
179 #199 := [rewrite]: #198 |
|
180 #190 := (iff #32 #189) |
|
181 #187 := (= #29 #28) |
|
182 #182 := (ite false #26 #28) |
|
183 #185 := (= #182 #28) |
|
184 #186 := [rewrite]: #185 |
|
185 #183 := (= #29 #182) |
|
186 #184 := [monotonicity #181]: #183 |
|
187 #188 := [trans #184 #186]: #187 |
|
188 #191 := [monotonicity #188]: #190 |
|
189 #201 := [trans #191 #199]: #200 |
|
190 #222 := [monotonicity #201 #219]: #221 |
|
191 #177 := [asserted]: #37 |
|
192 #223 := [mp #177 #222]: #220 |
|
193 #224 := [and-elim #223]: #193 |
|
194 #644 := [th-lemma #224 #277 #643]: false |
|
195 #646 := [lemma #644]: #645 |
|
196 #647 := [hypothesis]: #568 |
|
197 #649 := (or #648 #642) |
|
198 #650 := [th-lemma]: #649 |
|
199 #651 := [unit-resolution #650 #647 #646]: false |
|
200 #652 := [lemma #651]: #648 |
|
201 #578 := (or #229 #568) |
|
202 #579 := [def-axiom]: #578 |
|
203 #675 := [unit-resolution #579 #652]: #229 |
|
204 #677 := [th-lemma #675 #395]: #676 |
|
205 #679 := [symm #677]: #678 |
|
206 #683 := [monotonicity #679]: #682 |
|
207 #685 := [symm #683]: #684 |
|
208 #587 := (= uf_3 #586) |
|
209 #591 := (or #590 #587) |
|
210 #592 := [quant-inst]: #591 |
|
211 #681 := [unit-resolution #592 #547]: #587 |
|
212 #689 := [trans #681 #685]: #688 |
|
213 #690 := [trans #689 #687]: #45 |
|
214 #571 := (not #45) |
|
215 #54 := (uf_4 uf_11 #46) |
|
216 #279 := (ite #45 #28 #54) |
|
217 #465 := (* -1::real #279) |
|
218 #632 := (+ #28 #465) |
|
219 #633 := (<= #632 0::real) |
|
220 #580 := (= #28 #279) |
|
221 #656 := [hypothesis]: #45 |
|
222 #582 := (or #571 #580) |
|
223 #583 := [def-axiom]: #582 |
|
224 #657 := [unit-resolution #583 #656]: #580 |
|
225 #658 := (not #580) |
|
226 #659 := (or #658 #633) |
|
227 #660 := [th-lemma]: #659 |
|
228 #661 := [unit-resolution #660 #657]: #633 |
|
229 #57 := (uf_4 uf_8 #46) |
|
230 #363 := (* -1::real #57) |
|
231 #379 := (+ #47 #363) |
|
232 #380 := (<= #379 0::real) |
|
233 #381 := (not #380) |
|
234 #364 := (+ #54 #363) |
|
235 #362 := (>= #364 0::real) |
|
236 #361 := (not #362) |
|
237 #386 := (and #361 #381) |
|
238 #59 := (uf_4 uf_7 #46) |
|
239 #64 := (< #39 #39) |
|
240 #67 := (ite #64 #59 #47) |
|
241 #68 := (< #57 #67) |
|
242 #65 := (ite #64 #47 #54) |
|
243 #66 := (< #65 #57) |
|
244 #69 := (and #66 #68) |
|
245 #387 := (iff #69 #386) |
|
246 #384 := (iff #68 #381) |
|
247 #376 := (< #57 #47) |
|
248 #382 := (iff #376 #381) |
|
249 #383 := [rewrite]: #382 |
|
250 #377 := (iff #68 #376) |
|
251 #374 := (= #67 #47) |
|
252 #369 := (ite false #59 #47) |
|
253 #372 := (= #369 #47) |
|
254 #373 := [rewrite]: #372 |
|
255 #370 := (= #67 #369) |
|
256 #349 := (iff #64 false) |
|
257 #350 := [rewrite]: #349 |
|
258 #371 := [monotonicity #350]: #370 |
|
259 #375 := [trans #371 #373]: #374 |
|
260 #378 := [monotonicity #375]: #377 |
|
261 #385 := [trans #378 #383]: #384 |
|
262 #367 := (iff #66 #361) |
|
263 #358 := (< #54 #57) |
|
264 #365 := (iff #358 #361) |
|
265 #366 := [rewrite]: #365 |
|
266 #359 := (iff #66 #358) |
|
267 #356 := (= #65 #54) |
|
268 #351 := (ite false #47 #54) |
|
269 #354 := (= #351 #54) |
|
270 #355 := [rewrite]: #354 |
|
271 #352 := (= #65 #351) |
|
272 #353 := [monotonicity #350]: #352 |
|
273 #357 := [trans #353 #355]: #356 |
|
274 #360 := [monotonicity #357]: #359 |
|
275 #368 := [trans #360 #366]: #367 |
|
276 #388 := [monotonicity #368 #385]: #387 |
|
277 #346 := [asserted]: #69 |
|
278 #389 := [mp #346 #388]: #386 |
|
279 #391 := [and-elim #389]: #381 |
|
280 #397 := (* -1::real #59) |
|
281 #398 := (+ #47 #397) |
|
282 #399 := (<= #398 0::real) |
|
283 #409 := (* -1::real #54) |
|
284 #410 := (+ #47 #409) |
|
285 #408 := (>= #410 0::real) |
|
286 #60 := (uf_4 uf_9 #46) |
|
287 #402 := (* -1::real #60) |
|
288 #403 := (+ #59 #402) |
|
289 #404 := (<= #403 0::real) |
|
290 #418 := (and #399 #404 #408) |
|
291 #73 := (<= #59 #60) |
|
292 #72 := (<= #47 #59) |
|
293 #74 := (and #72 #73) |
|
294 #71 := (<= #54 #47) |
|
295 #75 := (and #71 #74) |
|
296 #421 := (iff #75 #418) |
|
297 #412 := (and #399 #404) |
|
298 #415 := (and #408 #412) |
|
299 #419 := (iff #415 #418) |
|
300 #420 := [rewrite]: #419 |
|
301 #416 := (iff #75 #415) |
|
302 #413 := (iff #74 #412) |
|
303 #405 := (iff #73 #404) |
|
304 #406 := [rewrite]: #405 |
|
305 #400 := (iff #72 #399) |
|
306 #401 := [rewrite]: #400 |
|
307 #414 := [monotonicity #401 #406]: #413 |
|
308 #407 := (iff #71 #408) |
|
309 #411 := [rewrite]: #407 |
|
310 #417 := [monotonicity #411 #414]: #416 |
|
311 #422 := [trans #417 #420]: #421 |
|
312 #348 := [asserted]: #75 |
|
313 #423 := [mp #348 #422]: #418 |
|
314 #424 := [and-elim #423]: #399 |
|
315 #637 := (+ #28 #397) |
|
316 #639 := (>= #637 0::real) |
|
317 #636 := (= #28 #59) |
|
318 #666 := (= #59 #28) |
|
319 #664 := (= #46 #25) |
|
320 #662 := (= #25 #46) |
|
321 #663 := [monotonicity #656]: #662 |
|
322 #665 := [symm #663]: #664 |
|
323 #667 := [monotonicity #665]: #666 |
|
324 #668 := [symm #667]: #636 |
|
325 #669 := (not #636) |
|
326 #670 := (or #669 #639) |
|
327 #671 := [th-lemma]: #670 |
|
328 #672 := [unit-resolution #671 #668]: #639 |
|
329 #468 := (+ #57 #465) |
|
330 #471 := (<= #468 0::real) |
|
331 #444 := (not #471) |
|
332 #322 := (ite #296 #279 #47) |
|
333 #330 := (* -1::real #322) |
|
334 #331 := (+ #57 #330) |
|
335 #332 := (<= #331 0::real) |
|
336 #333 := (not #332) |
|
337 #445 := (iff #333 #444) |
|
338 #472 := (iff #332 #471) |
|
339 #469 := (= #331 #468) |
|
340 #466 := (= #330 #465) |
|
341 #463 := (= #322 #279) |
|
342 #1 := true |
|
343 #458 := (ite true #279 #47) |
|
344 #461 := (= #458 #279) |
|
345 #462 := [rewrite]: #461 |
|
346 #459 := (= #322 #458) |
|
347 #450 := (iff #296 true) |
|
348 #451 := [iff-true #395]: #450 |
|
349 #460 := [monotonicity #451]: #459 |
|
350 #464 := [trans #460 #462]: #463 |
|
351 #467 := [monotonicity #464]: #466 |
|
352 #470 := [monotonicity #467]: #469 |
|
353 #473 := [monotonicity #470]: #472 |
|
354 #474 := [monotonicity #473]: #445 |
|
355 #303 := (ite #296 #60 #59) |
|
356 #313 := (* -1::real #303) |
|
357 #314 := (+ #57 #313) |
|
358 #312 := (>= #314 0::real) |
|
359 #311 := (not #312) |
|
360 #338 := (and #311 #333) |
|
361 #52 := (< #39 #22) |
|
362 #61 := (ite #52 #59 #60) |
|
363 #62 := (< #57 #61) |
|
364 #53 := (= uf_10 uf_3) |
|
365 #55 := (ite #53 #28 #54) |
|
366 #56 := (ite #52 #47 #55) |
|
367 #58 := (< #56 #57) |
|
368 #63 := (and #58 #62) |
|
369 #341 := (iff #63 #338) |
|
370 #282 := (ite #52 #47 #279) |
|
371 #285 := (< #282 #57) |
|
372 #291 := (and #62 #285) |
|
373 #339 := (iff #291 #338) |
|
374 #336 := (iff #285 #333) |
|
375 #327 := (< #322 #57) |
|
376 #334 := (iff #327 #333) |
|
377 #335 := [rewrite]: #334 |
|
378 #328 := (iff #285 #327) |
|
379 #325 := (= #282 #322) |
|
380 #297 := (not #296) |
|
381 #319 := (ite #297 #47 #279) |
|
382 #323 := (= #319 #322) |
|
383 #324 := [rewrite]: #323 |
|
384 #320 := (= #282 #319) |
|
385 #298 := (iff #52 #297) |
|
386 #299 := [rewrite]: #298 |
|
387 #321 := [monotonicity #299]: #320 |
|
388 #326 := [trans #321 #324]: #325 |
|
389 #329 := [monotonicity #326]: #328 |
|
390 #337 := [trans #329 #335]: #336 |
|
391 #317 := (iff #62 #311) |
|
392 #308 := (< #57 #303) |
|
393 #315 := (iff #308 #311) |
|
394 #316 := [rewrite]: #315 |
|
395 #309 := (iff #62 #308) |
|
396 #306 := (= #61 #303) |
|
397 #300 := (ite #297 #59 #60) |
|
398 #304 := (= #300 #303) |
|
399 #305 := [rewrite]: #304 |
|
400 #301 := (= #61 #300) |
|
401 #302 := [monotonicity #299]: #301 |
|
402 #307 := [trans #302 #305]: #306 |
|
403 #310 := [monotonicity #307]: #309 |
|
404 #318 := [trans #310 #316]: #317 |
|
405 #340 := [monotonicity #318 #337]: #339 |
|
406 #294 := (iff #63 #291) |
|
407 #288 := (and #285 #62) |
|
408 #292 := (iff #288 #291) |
|
409 #293 := [rewrite]: #292 |
|
410 #289 := (iff #63 #288) |
|
411 #286 := (iff #58 #285) |
|
412 #283 := (= #56 #282) |
|
413 #280 := (= #55 #279) |
|
414 #226 := (iff #53 #45) |
|
415 #278 := [rewrite]: #226 |
|
416 #281 := [monotonicity #278]: #280 |
|
417 #284 := [monotonicity #281]: #283 |
|
418 #287 := [monotonicity #284]: #286 |
|
419 #290 := [monotonicity #287]: #289 |
|
420 #295 := [trans #290 #293]: #294 |
|
421 #342 := [trans #295 #340]: #341 |
|
422 #179 := [asserted]: #63 |
|
423 #343 := [mp #179 #342]: #338 |
|
424 #345 := [and-elim #343]: #333 |
|
425 #475 := [mp #345 #474]: #444 |
|
426 #673 := [th-lemma #475 #672 #424 #391 #661]: false |
|
427 #674 := [lemma #673]: #571 |
|
428 [unit-resolution #674 #690]: false |
|
429 unsat |
|
430 985f86fd1ea01264c02b8076ffd658677bd4d29a 419 0 |
|
431 #2 := false |
|
432 #194 := 0::real |
|
433 decl uf_4 :: (-> T2 T3 real) |
|
434 decl uf_6 :: (-> T1 T3) |
|
435 decl uf_3 :: T1 |
|
436 #21 := uf_3 |
|
437 #25 := (uf_6 uf_3) |
|
438 decl uf_5 :: T2 |
|
439 #24 := uf_5 |
|
440 #26 := (uf_4 uf_5 #25) |
|
441 decl uf_7 :: T2 |
|
442 #27 := uf_7 |
|
443 #28 := (uf_4 uf_7 #25) |
|
444 decl uf_10 :: T1 |
|
445 #38 := uf_10 |
|
446 #42 := (uf_6 uf_10) |
|
447 decl uf_9 :: T2 |
|
448 #33 := uf_9 |
|
449 #43 := (uf_4 uf_9 #42) |
|
450 #41 := (= uf_3 uf_10) |
|
451 #44 := (ite #41 #43 #28) |
|
452 #9 := 0::int |
|
453 decl uf_2 :: (-> T1 int) |
|
454 #39 := (uf_2 uf_10) |
|
455 #226 := -1::int |
|
456 #229 := (* -1::int #39) |
|
457 #22 := (uf_2 uf_3) |
|
458 #230 := (+ #22 #229) |
|
459 #228 := (>= #230 0::int) |
|
460 #236 := (ite #228 #44 #26) |
|
461 #192 := -1::real |
|
462 #244 := (* -1::real #236) |
|
463 #642 := (+ #26 #244) |
|
464 #643 := (<= #642 0::real) |
|
465 #567 := (= #26 #236) |
|
466 #227 := (not #228) |
|
467 decl uf_1 :: (-> int T1) |
|
468 #593 := (uf_1 #39) |
|
469 #660 := (= #593 uf_10) |
|
470 #594 := (= uf_10 #593) |
|
471 #4 := (:var 0 T1) |
|
472 #5 := (uf_2 #4) |
|
473 #546 := (pattern #5) |
|
474 #6 := (uf_1 #5) |
|
475 #93 := (= #4 #6) |
|
476 #547 := (forall (vars (?x1 T1)) (:pat #546) #93) |
|
477 #96 := (forall (vars (?x1 T1)) #93) |
|
478 #550 := (iff #96 #547) |
|
479 #548 := (iff #93 #93) |
|
480 #549 := [refl]: #548 |
|
481 #551 := [quant-intro #549]: #550 |
|
482 #448 := (~ #96 #96) |
|
483 #450 := (~ #93 #93) |
|
484 #451 := [refl]: #450 |
|
485 #449 := [nnf-pos #451]: #448 |
|
486 #7 := (= #6 #4) |
|
487 #8 := (forall (vars (?x1 T1)) #7) |
|
488 #97 := (iff #8 #96) |
|
489 #94 := (iff #7 #93) |
|
490 #95 := [rewrite]: #94 |
|
491 #98 := [quant-intro #95]: #97 |
|
492 #92 := [asserted]: #8 |
|
493 #101 := [mp #92 #98]: #96 |
|
494 #446 := [mp~ #101 #449]: #96 |
|
495 #552 := [mp #446 #551]: #547 |
|
496 #595 := (not #547) |
|
497 #600 := (or #595 #594) |
|
498 #601 := [quant-inst]: #600 |
|
499 #654 := [unit-resolution #601 #552]: #594 |
|
500 #680 := [symm #654]: #660 |
|
501 #681 := (= uf_3 #593) |
|
502 #591 := (uf_1 #22) |
|
503 #658 := (= #591 #593) |
|
504 #656 := (= #593 #591) |
|
505 #652 := (= #39 #22) |
|
506 #647 := (= #22 #39) |
|
507 #290 := (<= #230 0::int) |
|
508 #70 := (<= #22 #39) |
|
509 #388 := (iff #70 #290) |
|
510 #389 := [rewrite]: #388 |
|
511 #341 := [asserted]: #70 |
|
512 #390 := [mp #341 #389]: #290 |
|
513 #646 := [hypothesis]: #228 |
|
514 #648 := [th-lemma #646 #390]: #647 |
|
515 #653 := [symm #648]: #652 |
|
516 #657 := [monotonicity #653]: #656 |
|
517 #659 := [symm #657]: #658 |
|
518 #592 := (= uf_3 #591) |
|
519 #596 := (or #595 #592) |
|
520 #597 := [quant-inst]: #596 |
|
521 #655 := [unit-resolution #597 #552]: #592 |
|
522 #682 := [trans #655 #659]: #681 |
|
523 #683 := [trans #682 #680]: #41 |
|
524 #570 := (not #41) |
|
525 decl uf_11 :: T2 |
|
526 #47 := uf_11 |
|
527 #59 := (uf_4 uf_11 #42) |
|
528 #278 := (ite #41 #26 #59) |
|
529 #459 := (* -1::real #278) |
|
530 #637 := (+ #26 #459) |
|
531 #639 := (>= #637 0::real) |
|
532 #585 := (= #26 #278) |
|
533 #661 := [hypothesis]: #41 |
|
534 #587 := (or #570 #585) |
|
535 #588 := [def-axiom]: #587 |
|
536 #662 := [unit-resolution #588 #661]: #585 |
|
537 #663 := (not #585) |
|
538 #664 := (or #663 #639) |
|
539 #665 := [th-lemma]: #664 |
|
540 #666 := [unit-resolution #665 #662]: #639 |
|
541 decl uf_8 :: T2 |
|
542 #30 := uf_8 |
|
543 #56 := (uf_4 uf_8 #42) |
|
544 #357 := (* -1::real #56) |
|
545 #358 := (+ #43 #357) |
|
546 #356 := (>= #358 0::real) |
|
547 #355 := (not #356) |
|
548 #374 := (* -1::real #59) |
|
549 #375 := (+ #56 #374) |
|
550 #373 := (>= #375 0::real) |
|
551 #376 := (not #373) |
|
552 #381 := (and #355 #376) |
|
553 #64 := (< #39 #39) |
|
554 #67 := (ite #64 #43 #59) |
|
555 #68 := (< #56 #67) |
|
556 #53 := (uf_4 uf_5 #42) |
|
557 #65 := (ite #64 #53 #43) |
|
558 #66 := (< #65 #56) |
|
559 #69 := (and #66 #68) |
|
560 #382 := (iff #69 #381) |
|
561 #379 := (iff #68 #376) |
|
562 #370 := (< #56 #59) |
|
563 #377 := (iff #370 #376) |
|
564 #378 := [rewrite]: #377 |
|
565 #371 := (iff #68 #370) |
|
566 #368 := (= #67 #59) |
|
567 #363 := (ite false #43 #59) |
|
568 #366 := (= #363 #59) |
|
569 #367 := [rewrite]: #366 |
|
570 #364 := (= #67 #363) |
|
571 #343 := (iff #64 false) |
|
572 #344 := [rewrite]: #343 |
|
573 #365 := [monotonicity #344]: #364 |
|
574 #369 := [trans #365 #367]: #368 |
|
575 #372 := [monotonicity #369]: #371 |
|
576 #380 := [trans #372 #378]: #379 |
|
577 #361 := (iff #66 #355) |
|
578 #352 := (< #43 #56) |
|
579 #359 := (iff #352 #355) |
|
580 #360 := [rewrite]: #359 |
|
581 #353 := (iff #66 #352) |
|
582 #350 := (= #65 #43) |
|
583 #345 := (ite false #53 #43) |
|
584 #348 := (= #345 #43) |
|
585 #349 := [rewrite]: #348 |
|
586 #346 := (= #65 #345) |
|
587 #347 := [monotonicity #344]: #346 |
|
588 #351 := [trans #347 #349]: #350 |
|
589 #354 := [monotonicity #351]: #353 |
|
590 #362 := [trans #354 #360]: #361 |
|
591 #383 := [monotonicity #362 #380]: #382 |
|
592 #340 := [asserted]: #69 |
|
593 #384 := [mp #340 #383]: #381 |
|
594 #385 := [and-elim #384]: #355 |
|
595 #394 := (* -1::real #53) |
|
596 #395 := (+ #43 #394) |
|
597 #393 := (>= #395 0::real) |
|
598 #54 := (uf_4 uf_7 #42) |
|
599 #402 := (* -1::real #54) |
|
600 #403 := (+ #53 #402) |
|
601 #401 := (>= #403 0::real) |
|
602 #397 := (+ #43 #374) |
|
603 #398 := (<= #397 0::real) |
|
604 #412 := (and #393 #398 #401) |
|
605 #73 := (<= #43 #59) |
|
606 #72 := (<= #53 #43) |
|
607 #74 := (and #72 #73) |
|
608 #71 := (<= #54 #53) |
|
609 #75 := (and #71 #74) |
|
610 #415 := (iff #75 #412) |
|
611 #406 := (and #393 #398) |
|
612 #409 := (and #401 #406) |
|
613 #413 := (iff #409 #412) |
|
614 #414 := [rewrite]: #413 |
|
615 #410 := (iff #75 #409) |
|
616 #407 := (iff #74 #406) |
|
617 #399 := (iff #73 #398) |
|
618 #400 := [rewrite]: #399 |
|
619 #392 := (iff #72 #393) |
|
620 #396 := [rewrite]: #392 |
|
621 #408 := [monotonicity #396 #400]: #407 |
|
622 #404 := (iff #71 #401) |
|
623 #405 := [rewrite]: #404 |
|
624 #411 := [monotonicity #405 #408]: #410 |
|
625 #416 := [trans #411 #414]: #415 |
|
626 #342 := [asserted]: #75 |
|
627 #417 := [mp #342 #416]: #412 |
|
628 #418 := [and-elim #417]: #393 |
|
629 #650 := (+ #26 #394) |
|
630 #651 := (<= #650 0::real) |
|
631 #649 := (= #26 #53) |
|
632 #671 := (= #53 #26) |
|
633 #669 := (= #42 #25) |
|
634 #667 := (= #25 #42) |
|
635 #668 := [monotonicity #661]: #667 |
|
636 #670 := [symm #668]: #669 |
|
637 #672 := [monotonicity #670]: #671 |
|
638 #673 := [symm #672]: #649 |
|
639 #674 := (not #649) |
|
640 #675 := (or #674 #651) |
|
641 #676 := [th-lemma]: #675 |
|
642 #677 := [unit-resolution #676 #673]: #651 |
|
643 #462 := (+ #56 #459) |
|
644 #465 := (>= #462 0::real) |
|
645 #438 := (not #465) |
|
646 #316 := (ite #290 #278 #43) |
|
647 #326 := (* -1::real #316) |
|
648 #327 := (+ #56 #326) |
|
649 #325 := (>= #327 0::real) |
|
650 #324 := (not #325) |
|
651 #439 := (iff #324 #438) |
|
652 #466 := (iff #325 #465) |
|
653 #463 := (= #327 #462) |
|
654 #460 := (= #326 #459) |
|
655 #457 := (= #316 #278) |
|
656 #1 := true |
|
657 #452 := (ite true #278 #43) |
|
658 #455 := (= #452 #278) |
|
659 #456 := [rewrite]: #455 |
|
660 #453 := (= #316 #452) |
|
661 #444 := (iff #290 true) |
|
662 #445 := [iff-true #390]: #444 |
|
663 #454 := [monotonicity #445]: #453 |
|
664 #458 := [trans #454 #456]: #457 |
|
665 #461 := [monotonicity #458]: #460 |
|
666 #464 := [monotonicity #461]: #463 |
|
667 #467 := [monotonicity #464]: #466 |
|
668 #468 := [monotonicity #467]: #439 |
|
669 #297 := (ite #290 #54 #53) |
|
670 #305 := (* -1::real #297) |
|
671 #306 := (+ #56 #305) |
|
672 #307 := (<= #306 0::real) |
|
673 #308 := (not #307) |
|
674 #332 := (and #308 #324) |
|
675 #58 := (= uf_10 uf_3) |
|
676 #60 := (ite #58 #26 #59) |
|
677 #52 := (< #39 #22) |
|
678 #61 := (ite #52 #43 #60) |
|
679 #62 := (< #56 #61) |
|
680 #55 := (ite #52 #53 #54) |
|
681 #57 := (< #55 #56) |
|
682 #63 := (and #57 #62) |
|
683 #335 := (iff #63 #332) |
|
684 #281 := (ite #52 #43 #278) |
|
685 #284 := (< #56 #281) |
|
686 #287 := (and #57 #284) |
|
687 #333 := (iff #287 #332) |
|
688 #330 := (iff #284 #324) |
|
689 #321 := (< #56 #316) |
|
690 #328 := (iff #321 #324) |
|
691 #329 := [rewrite]: #328 |
|
692 #322 := (iff #284 #321) |
|
693 #319 := (= #281 #316) |
|
694 #291 := (not #290) |
|
695 #313 := (ite #291 #43 #278) |
|
696 #317 := (= #313 #316) |
|
697 #318 := [rewrite]: #317 |
|
698 #314 := (= #281 #313) |
|
699 #292 := (iff #52 #291) |
|
700 #293 := [rewrite]: #292 |
|
701 #315 := [monotonicity #293]: #314 |
|
702 #320 := [trans #315 #318]: #319 |
|
703 #323 := [monotonicity #320]: #322 |
|
704 #331 := [trans #323 #329]: #330 |
|
705 #311 := (iff #57 #308) |
|
706 #302 := (< #297 #56) |
|
707 #309 := (iff #302 #308) |
|
708 #310 := [rewrite]: #309 |
|
709 #303 := (iff #57 #302) |
|
710 #300 := (= #55 #297) |
|
711 #294 := (ite #291 #53 #54) |
|
712 #298 := (= #294 #297) |
|
713 #299 := [rewrite]: #298 |
|
714 #295 := (= #55 #294) |
|
715 #296 := [monotonicity #293]: #295 |
|
716 #301 := [trans #296 #299]: #300 |
|
717 #304 := [monotonicity #301]: #303 |
|
718 #312 := [trans #304 #310]: #311 |
|
719 #334 := [monotonicity #312 #331]: #333 |
|
720 #288 := (iff #63 #287) |
|
721 #285 := (iff #62 #284) |
|
722 #282 := (= #61 #281) |
|
723 #279 := (= #60 #278) |
|
724 #225 := (iff #58 #41) |
|
725 #277 := [rewrite]: #225 |
|
726 #280 := [monotonicity #277]: #279 |
|
727 #283 := [monotonicity #280]: #282 |
|
728 #286 := [monotonicity #283]: #285 |
|
729 #289 := [monotonicity #286]: #288 |
|
730 #336 := [trans #289 #334]: #335 |
|
731 #179 := [asserted]: #63 |
|
732 #337 := [mp #179 #336]: #332 |
|
733 #339 := [and-elim #337]: #324 |
|
734 #469 := [mp #339 #468]: #438 |
|
735 #678 := [th-lemma #469 #677 #418 #385 #666]: false |
|
736 #679 := [lemma #678]: #570 |
|
737 #684 := [unit-resolution #679 #683]: false |
|
738 #685 := [lemma #684]: #227 |
|
739 #577 := (or #228 #567) |
|
740 #578 := [def-axiom]: #577 |
|
741 #645 := [unit-resolution #578 #685]: #567 |
|
742 #686 := (not #567) |
|
743 #687 := (or #686 #643) |
|
744 #688 := [th-lemma]: #687 |
|
745 #689 := [unit-resolution #688 #645]: #643 |
|
746 #31 := (uf_4 uf_8 #25) |
|
747 #245 := (+ #31 #244) |
|
748 #246 := (<= #245 0::real) |
|
749 #247 := (not #246) |
|
750 #34 := (uf_4 uf_9 #25) |
|
751 #48 := (uf_4 uf_11 #25) |
|
752 #255 := (ite #228 #48 #34) |
|
753 #264 := (* -1::real #255) |
|
754 #265 := (+ #31 #264) |
|
755 #263 := (>= #265 0::real) |
|
756 #266 := (not #263) |
|
757 #271 := (and #247 #266) |
|
758 #40 := (< #22 #39) |
|
759 #49 := (ite #40 #34 #48) |
|
760 #50 := (< #31 #49) |
|
761 #45 := (ite #40 #26 #44) |
|
762 #46 := (< #45 #31) |
|
763 #51 := (and #46 #50) |
|
764 #272 := (iff #51 #271) |
|
765 #269 := (iff #50 #266) |
|
766 #260 := (< #31 #255) |
|
767 #267 := (iff #260 #266) |
|
768 #268 := [rewrite]: #267 |
|
769 #261 := (iff #50 #260) |
|
770 #258 := (= #49 #255) |
|
771 #252 := (ite #227 #34 #48) |
|
772 #256 := (= #252 #255) |
|
773 #257 := [rewrite]: #256 |
|
774 #253 := (= #49 #252) |
|
775 #231 := (iff #40 #227) |
|
776 #232 := [rewrite]: #231 |
|
777 #254 := [monotonicity #232]: #253 |
|
778 #259 := [trans #254 #257]: #258 |
|
779 #262 := [monotonicity #259]: #261 |
|
780 #270 := [trans #262 #268]: #269 |
|
781 #250 := (iff #46 #247) |
|
782 #241 := (< #236 #31) |
|
783 #248 := (iff #241 #247) |
|
784 #249 := [rewrite]: #248 |
|
785 #242 := (iff #46 #241) |
|
786 #239 := (= #45 #236) |
|
787 #233 := (ite #227 #26 #44) |
|
788 #237 := (= #233 #236) |
|
789 #238 := [rewrite]: #237 |
|
790 #234 := (= #45 #233) |
|
791 #235 := [monotonicity #232]: #234 |
|
792 #240 := [trans #235 #238]: #239 |
|
793 #243 := [monotonicity #240]: #242 |
|
794 #251 := [trans #243 #249]: #250 |
|
795 #273 := [monotonicity #251 #270]: #272 |
|
796 #178 := [asserted]: #51 |
|
797 #274 := [mp #178 #273]: #271 |
|
798 #275 := [and-elim #274]: #247 |
|
799 #196 := (* -1::real #31) |
|
800 #212 := (+ #26 #196) |
|
801 #213 := (<= #212 0::real) |
|
802 #214 := (not #213) |
|
803 #197 := (+ #28 #196) |
|
804 #195 := (>= #197 0::real) |
|
805 #193 := (not #195) |
|
806 #219 := (and #193 #214) |
|
807 #23 := (< #22 #22) |
|
808 #35 := (ite #23 #34 #26) |
|
809 #36 := (< #31 #35) |
|
810 #29 := (ite #23 #26 #28) |
|
811 #32 := (< #29 #31) |
|
812 #37 := (and #32 #36) |
|
813 #220 := (iff #37 #219) |
|
814 #217 := (iff #36 #214) |
|
815 #209 := (< #31 #26) |
|
816 #215 := (iff #209 #214) |
|
817 #216 := [rewrite]: #215 |
|
818 #210 := (iff #36 #209) |
|
819 #207 := (= #35 #26) |
|
820 #202 := (ite false #34 #26) |
|
821 #205 := (= #202 #26) |
|
822 #206 := [rewrite]: #205 |
|
823 #203 := (= #35 #202) |
|
824 #180 := (iff #23 false) |
|
825 #181 := [rewrite]: #180 |
|
826 #204 := [monotonicity #181]: #203 |
|
827 #208 := [trans #204 #206]: #207 |
|
828 #211 := [monotonicity #208]: #210 |
|
829 #218 := [trans #211 #216]: #217 |
|
830 #200 := (iff #32 #193) |
|
831 #189 := (< #28 #31) |
|
832 #198 := (iff #189 #193) |
|
833 #199 := [rewrite]: #198 |
|
834 #190 := (iff #32 #189) |
|
835 #187 := (= #29 #28) |
|
836 #182 := (ite false #26 #28) |
|
837 #185 := (= #182 #28) |
|
838 #186 := [rewrite]: #185 |
|
839 #183 := (= #29 #182) |
|
840 #184 := [monotonicity #181]: #183 |
|
841 #188 := [trans #184 #186]: #187 |
|
842 #191 := [monotonicity #188]: #190 |
|
843 #201 := [trans #191 #199]: #200 |
|
844 #221 := [monotonicity #201 #218]: #220 |
|
845 #177 := [asserted]: #37 |
|
846 #222 := [mp #177 #221]: #219 |
|
847 #224 := [and-elim #222]: #214 |
|
848 [th-lemma #224 #275 #689]: false |
|
849 unsat |
|
850 00b949278548f13329cf92f11a0ad2161fa40793 907 0 |
2 #2 := false |
851 #2 := false |
3 #299 := 0::real |
852 #299 := 0::real |
4 decl uf_1 :: (-> T3 T2 real) |
853 decl uf_1 :: (-> T3 T2 real) |
5 decl uf_10 :: (-> T4 T2) |
854 decl uf_10 :: (-> T4 T2) |
6 decl uf_7 :: T4 |
855 decl uf_7 :: T4 |
904 #1232 := (or #1216 #1231) |
1753 #1232 := (or #1216 #1231) |
905 #1233 := [def-axiom]: #1232 |
1754 #1233 := [def-axiom]: #1232 |
906 #1366 := [unit-resolution #1233 #1365]: #1231 |
1755 #1366 := [unit-resolution #1233 #1365]: #1231 |
907 [th-lemma #1366 #1364 #1362]: false |
1756 [th-lemma #1366 #1364 #1362]: false |
908 unsat |
1757 unsat |
909 NQHwTeL311Tq3wf2s5BReA 419 0 |
1758 f5cf3017773c1cf700f533cb220ba6c9eb22de56 211 0 |
910 #2 := false |
|
911 #194 := 0::real |
|
912 decl uf_4 :: (-> T2 T3 real) |
|
913 decl uf_6 :: (-> T1 T3) |
|
914 decl uf_3 :: T1 |
|
915 #21 := uf_3 |
|
916 #25 := (uf_6 uf_3) |
|
917 decl uf_5 :: T2 |
|
918 #24 := uf_5 |
|
919 #26 := (uf_4 uf_5 #25) |
|
920 decl uf_7 :: T2 |
|
921 #27 := uf_7 |
|
922 #28 := (uf_4 uf_7 #25) |
|
923 decl uf_10 :: T1 |
|
924 #38 := uf_10 |
|
925 #42 := (uf_6 uf_10) |
|
926 decl uf_9 :: T2 |
|
927 #33 := uf_9 |
|
928 #43 := (uf_4 uf_9 #42) |
|
929 #41 := (= uf_3 uf_10) |
|
930 #44 := (ite #41 #43 #28) |
|
931 #9 := 0::int |
|
932 decl uf_2 :: (-> T1 int) |
|
933 #39 := (uf_2 uf_10) |
|
934 #226 := -1::int |
|
935 #229 := (* -1::int #39) |
|
936 #22 := (uf_2 uf_3) |
|
937 #230 := (+ #22 #229) |
|
938 #228 := (>= #230 0::int) |
|
939 #236 := (ite #228 #44 #26) |
|
940 #192 := -1::real |
|
941 #244 := (* -1::real #236) |
|
942 #642 := (+ #26 #244) |
|
943 #643 := (<= #642 0::real) |
|
944 #567 := (= #26 #236) |
|
945 #227 := (not #228) |
|
946 decl uf_1 :: (-> int T1) |
|
947 #593 := (uf_1 #39) |
|
948 #660 := (= #593 uf_10) |
|
949 #594 := (= uf_10 #593) |
|
950 #4 := (:var 0 T1) |
|
951 #5 := (uf_2 #4) |
|
952 #546 := (pattern #5) |
|
953 #6 := (uf_1 #5) |
|
954 #93 := (= #4 #6) |
|
955 #547 := (forall (vars (?x1 T1)) (:pat #546) #93) |
|
956 #96 := (forall (vars (?x1 T1)) #93) |
|
957 #550 := (iff #96 #547) |
|
958 #548 := (iff #93 #93) |
|
959 #549 := [refl]: #548 |
|
960 #551 := [quant-intro #549]: #550 |
|
961 #448 := (~ #96 #96) |
|
962 #450 := (~ #93 #93) |
|
963 #451 := [refl]: #450 |
|
964 #449 := [nnf-pos #451]: #448 |
|
965 #7 := (= #6 #4) |
|
966 #8 := (forall (vars (?x1 T1)) #7) |
|
967 #97 := (iff #8 #96) |
|
968 #94 := (iff #7 #93) |
|
969 #95 := [rewrite]: #94 |
|
970 #98 := [quant-intro #95]: #97 |
|
971 #92 := [asserted]: #8 |
|
972 #101 := [mp #92 #98]: #96 |
|
973 #446 := [mp~ #101 #449]: #96 |
|
974 #552 := [mp #446 #551]: #547 |
|
975 #595 := (not #547) |
|
976 #600 := (or #595 #594) |
|
977 #601 := [quant-inst]: #600 |
|
978 #654 := [unit-resolution #601 #552]: #594 |
|
979 #680 := [symm #654]: #660 |
|
980 #681 := (= uf_3 #593) |
|
981 #591 := (uf_1 #22) |
|
982 #658 := (= #591 #593) |
|
983 #656 := (= #593 #591) |
|
984 #652 := (= #39 #22) |
|
985 #647 := (= #22 #39) |
|
986 #290 := (<= #230 0::int) |
|
987 #70 := (<= #22 #39) |
|
988 #388 := (iff #70 #290) |
|
989 #389 := [rewrite]: #388 |
|
990 #341 := [asserted]: #70 |
|
991 #390 := [mp #341 #389]: #290 |
|
992 #646 := [hypothesis]: #228 |
|
993 #648 := [th-lemma #646 #390]: #647 |
|
994 #653 := [symm #648]: #652 |
|
995 #657 := [monotonicity #653]: #656 |
|
996 #659 := [symm #657]: #658 |
|
997 #592 := (= uf_3 #591) |
|
998 #596 := (or #595 #592) |
|
999 #597 := [quant-inst]: #596 |
|
1000 #655 := [unit-resolution #597 #552]: #592 |
|
1001 #682 := [trans #655 #659]: #681 |
|
1002 #683 := [trans #682 #680]: #41 |
|
1003 #570 := (not #41) |
|
1004 decl uf_11 :: T2 |
|
1005 #47 := uf_11 |
|
1006 #59 := (uf_4 uf_11 #42) |
|
1007 #278 := (ite #41 #26 #59) |
|
1008 #459 := (* -1::real #278) |
|
1009 #637 := (+ #26 #459) |
|
1010 #639 := (>= #637 0::real) |
|
1011 #585 := (= #26 #278) |
|
1012 #661 := [hypothesis]: #41 |
|
1013 #587 := (or #570 #585) |
|
1014 #588 := [def-axiom]: #587 |
|
1015 #662 := [unit-resolution #588 #661]: #585 |
|
1016 #663 := (not #585) |
|
1017 #664 := (or #663 #639) |
|
1018 #665 := [th-lemma]: #664 |
|
1019 #666 := [unit-resolution #665 #662]: #639 |
|
1020 decl uf_8 :: T2 |
|
1021 #30 := uf_8 |
|
1022 #56 := (uf_4 uf_8 #42) |
|
1023 #357 := (* -1::real #56) |
|
1024 #358 := (+ #43 #357) |
|
1025 #356 := (>= #358 0::real) |
|
1026 #355 := (not #356) |
|
1027 #374 := (* -1::real #59) |
|
1028 #375 := (+ #56 #374) |
|
1029 #373 := (>= #375 0::real) |
|
1030 #376 := (not #373) |
|
1031 #381 := (and #355 #376) |
|
1032 #64 := (< #39 #39) |
|
1033 #67 := (ite #64 #43 #59) |
|
1034 #68 := (< #56 #67) |
|
1035 #53 := (uf_4 uf_5 #42) |
|
1036 #65 := (ite #64 #53 #43) |
|
1037 #66 := (< #65 #56) |
|
1038 #69 := (and #66 #68) |
|
1039 #382 := (iff #69 #381) |
|
1040 #379 := (iff #68 #376) |
|
1041 #370 := (< #56 #59) |
|
1042 #377 := (iff #370 #376) |
|
1043 #378 := [rewrite]: #377 |
|
1044 #371 := (iff #68 #370) |
|
1045 #368 := (= #67 #59) |
|
1046 #363 := (ite false #43 #59) |
|
1047 #366 := (= #363 #59) |
|
1048 #367 := [rewrite]: #366 |
|
1049 #364 := (= #67 #363) |
|
1050 #343 := (iff #64 false) |
|
1051 #344 := [rewrite]: #343 |
|
1052 #365 := [monotonicity #344]: #364 |
|
1053 #369 := [trans #365 #367]: #368 |
|
1054 #372 := [monotonicity #369]: #371 |
|
1055 #380 := [trans #372 #378]: #379 |
|
1056 #361 := (iff #66 #355) |
|
1057 #352 := (< #43 #56) |
|
1058 #359 := (iff #352 #355) |
|
1059 #360 := [rewrite]: #359 |
|
1060 #353 := (iff #66 #352) |
|
1061 #350 := (= #65 #43) |
|
1062 #345 := (ite false #53 #43) |
|
1063 #348 := (= #345 #43) |
|
1064 #349 := [rewrite]: #348 |
|
1065 #346 := (= #65 #345) |
|
1066 #347 := [monotonicity #344]: #346 |
|
1067 #351 := [trans #347 #349]: #350 |
|
1068 #354 := [monotonicity #351]: #353 |
|
1069 #362 := [trans #354 #360]: #361 |
|
1070 #383 := [monotonicity #362 #380]: #382 |
|
1071 #340 := [asserted]: #69 |
|
1072 #384 := [mp #340 #383]: #381 |
|
1073 #385 := [and-elim #384]: #355 |
|
1074 #394 := (* -1::real #53) |
|
1075 #395 := (+ #43 #394) |
|
1076 #393 := (>= #395 0::real) |
|
1077 #54 := (uf_4 uf_7 #42) |
|
1078 #402 := (* -1::real #54) |
|
1079 #403 := (+ #53 #402) |
|
1080 #401 := (>= #403 0::real) |
|
1081 #397 := (+ #43 #374) |
|
1082 #398 := (<= #397 0::real) |
|
1083 #412 := (and #393 #398 #401) |
|
1084 #73 := (<= #43 #59) |
|
1085 #72 := (<= #53 #43) |
|
1086 #74 := (and #72 #73) |
|
1087 #71 := (<= #54 #53) |
|
1088 #75 := (and #71 #74) |
|
1089 #415 := (iff #75 #412) |
|
1090 #406 := (and #393 #398) |
|
1091 #409 := (and #401 #406) |
|
1092 #413 := (iff #409 #412) |
|
1093 #414 := [rewrite]: #413 |
|
1094 #410 := (iff #75 #409) |
|
1095 #407 := (iff #74 #406) |
|
1096 #399 := (iff #73 #398) |
|
1097 #400 := [rewrite]: #399 |
|
1098 #392 := (iff #72 #393) |
|
1099 #396 := [rewrite]: #392 |
|
1100 #408 := [monotonicity #396 #400]: #407 |
|
1101 #404 := (iff #71 #401) |
|
1102 #405 := [rewrite]: #404 |
|
1103 #411 := [monotonicity #405 #408]: #410 |
|
1104 #416 := [trans #411 #414]: #415 |
|
1105 #342 := [asserted]: #75 |
|
1106 #417 := [mp #342 #416]: #412 |
|
1107 #418 := [and-elim #417]: #393 |
|
1108 #650 := (+ #26 #394) |
|
1109 #651 := (<= #650 0::real) |
|
1110 #649 := (= #26 #53) |
|
1111 #671 := (= #53 #26) |
|
1112 #669 := (= #42 #25) |
|
1113 #667 := (= #25 #42) |
|
1114 #668 := [monotonicity #661]: #667 |
|
1115 #670 := [symm #668]: #669 |
|
1116 #672 := [monotonicity #670]: #671 |
|
1117 #673 := [symm #672]: #649 |
|
1118 #674 := (not #649) |
|
1119 #675 := (or #674 #651) |
|
1120 #676 := [th-lemma]: #675 |
|
1121 #677 := [unit-resolution #676 #673]: #651 |
|
1122 #462 := (+ #56 #459) |
|
1123 #465 := (>= #462 0::real) |
|
1124 #438 := (not #465) |
|
1125 #316 := (ite #290 #278 #43) |
|
1126 #326 := (* -1::real #316) |
|
1127 #327 := (+ #56 #326) |
|
1128 #325 := (>= #327 0::real) |
|
1129 #324 := (not #325) |
|
1130 #439 := (iff #324 #438) |
|
1131 #466 := (iff #325 #465) |
|
1132 #463 := (= #327 #462) |
|
1133 #460 := (= #326 #459) |
|
1134 #457 := (= #316 #278) |
|
1135 #1 := true |
|
1136 #452 := (ite true #278 #43) |
|
1137 #455 := (= #452 #278) |
|
1138 #456 := [rewrite]: #455 |
|
1139 #453 := (= #316 #452) |
|
1140 #444 := (iff #290 true) |
|
1141 #445 := [iff-true #390]: #444 |
|
1142 #454 := [monotonicity #445]: #453 |
|
1143 #458 := [trans #454 #456]: #457 |
|
1144 #461 := [monotonicity #458]: #460 |
|
1145 #464 := [monotonicity #461]: #463 |
|
1146 #467 := [monotonicity #464]: #466 |
|
1147 #468 := [monotonicity #467]: #439 |
|
1148 #297 := (ite #290 #54 #53) |
|
1149 #305 := (* -1::real #297) |
|
1150 #306 := (+ #56 #305) |
|
1151 #307 := (<= #306 0::real) |
|
1152 #308 := (not #307) |
|
1153 #332 := (and #308 #324) |
|
1154 #58 := (= uf_10 uf_3) |
|
1155 #60 := (ite #58 #26 #59) |
|
1156 #52 := (< #39 #22) |
|
1157 #61 := (ite #52 #43 #60) |
|
1158 #62 := (< #56 #61) |
|
1159 #55 := (ite #52 #53 #54) |
|
1160 #57 := (< #55 #56) |
|
1161 #63 := (and #57 #62) |
|
1162 #335 := (iff #63 #332) |
|
1163 #281 := (ite #52 #43 #278) |
|
1164 #284 := (< #56 #281) |
|
1165 #287 := (and #57 #284) |
|
1166 #333 := (iff #287 #332) |
|
1167 #330 := (iff #284 #324) |
|
1168 #321 := (< #56 #316) |
|
1169 #328 := (iff #321 #324) |
|
1170 #329 := [rewrite]: #328 |
|
1171 #322 := (iff #284 #321) |
|
1172 #319 := (= #281 #316) |
|
1173 #291 := (not #290) |
|
1174 #313 := (ite #291 #43 #278) |
|
1175 #317 := (= #313 #316) |
|
1176 #318 := [rewrite]: #317 |
|
1177 #314 := (= #281 #313) |
|
1178 #292 := (iff #52 #291) |
|
1179 #293 := [rewrite]: #292 |
|
1180 #315 := [monotonicity #293]: #314 |
|
1181 #320 := [trans #315 #318]: #319 |
|
1182 #323 := [monotonicity #320]: #322 |
|
1183 #331 := [trans #323 #329]: #330 |
|
1184 #311 := (iff #57 #308) |
|
1185 #302 := (< #297 #56) |
|
1186 #309 := (iff #302 #308) |
|
1187 #310 := [rewrite]: #309 |
|
1188 #303 := (iff #57 #302) |
|
1189 #300 := (= #55 #297) |
|
1190 #294 := (ite #291 #53 #54) |
|
1191 #298 := (= #294 #297) |
|
1192 #299 := [rewrite]: #298 |
|
1193 #295 := (= #55 #294) |
|
1194 #296 := [monotonicity #293]: #295 |
|
1195 #301 := [trans #296 #299]: #300 |
|
1196 #304 := [monotonicity #301]: #303 |
|
1197 #312 := [trans #304 #310]: #311 |
|
1198 #334 := [monotonicity #312 #331]: #333 |
|
1199 #288 := (iff #63 #287) |
|
1200 #285 := (iff #62 #284) |
|
1201 #282 := (= #61 #281) |
|
1202 #279 := (= #60 #278) |
|
1203 #225 := (iff #58 #41) |
|
1204 #277 := [rewrite]: #225 |
|
1205 #280 := [monotonicity #277]: #279 |
|
1206 #283 := [monotonicity #280]: #282 |
|
1207 #286 := [monotonicity #283]: #285 |
|
1208 #289 := [monotonicity #286]: #288 |
|
1209 #336 := [trans #289 #334]: #335 |
|
1210 #179 := [asserted]: #63 |
|
1211 #337 := [mp #179 #336]: #332 |
|
1212 #339 := [and-elim #337]: #324 |
|
1213 #469 := [mp #339 #468]: #438 |
|
1214 #678 := [th-lemma #469 #677 #418 #385 #666]: false |
|
1215 #679 := [lemma #678]: #570 |
|
1216 #684 := [unit-resolution #679 #683]: false |
|
1217 #685 := [lemma #684]: #227 |
|
1218 #577 := (or #228 #567) |
|
1219 #578 := [def-axiom]: #577 |
|
1220 #645 := [unit-resolution #578 #685]: #567 |
|
1221 #686 := (not #567) |
|
1222 #687 := (or #686 #643) |
|
1223 #688 := [th-lemma]: #687 |
|
1224 #689 := [unit-resolution #688 #645]: #643 |
|
1225 #31 := (uf_4 uf_8 #25) |
|
1226 #245 := (+ #31 #244) |
|
1227 #246 := (<= #245 0::real) |
|
1228 #247 := (not #246) |
|
1229 #34 := (uf_4 uf_9 #25) |
|
1230 #48 := (uf_4 uf_11 #25) |
|
1231 #255 := (ite #228 #48 #34) |
|
1232 #264 := (* -1::real #255) |
|
1233 #265 := (+ #31 #264) |
|
1234 #263 := (>= #265 0::real) |
|
1235 #266 := (not #263) |
|
1236 #271 := (and #247 #266) |
|
1237 #40 := (< #22 #39) |
|
1238 #49 := (ite #40 #34 #48) |
|
1239 #50 := (< #31 #49) |
|
1240 #45 := (ite #40 #26 #44) |
|
1241 #46 := (< #45 #31) |
|
1242 #51 := (and #46 #50) |
|
1243 #272 := (iff #51 #271) |
|
1244 #269 := (iff #50 #266) |
|
1245 #260 := (< #31 #255) |
|
1246 #267 := (iff #260 #266) |
|
1247 #268 := [rewrite]: #267 |
|
1248 #261 := (iff #50 #260) |
|
1249 #258 := (= #49 #255) |
|
1250 #252 := (ite #227 #34 #48) |
|
1251 #256 := (= #252 #255) |
|
1252 #257 := [rewrite]: #256 |
|
1253 #253 := (= #49 #252) |
|
1254 #231 := (iff #40 #227) |
|
1255 #232 := [rewrite]: #231 |
|
1256 #254 := [monotonicity #232]: #253 |
|
1257 #259 := [trans #254 #257]: #258 |
|
1258 #262 := [monotonicity #259]: #261 |
|
1259 #270 := [trans #262 #268]: #269 |
|
1260 #250 := (iff #46 #247) |
|
1261 #241 := (< #236 #31) |
|
1262 #248 := (iff #241 #247) |
|
1263 #249 := [rewrite]: #248 |
|
1264 #242 := (iff #46 #241) |
|
1265 #239 := (= #45 #236) |
|
1266 #233 := (ite #227 #26 #44) |
|
1267 #237 := (= #233 #236) |
|
1268 #238 := [rewrite]: #237 |
|
1269 #234 := (= #45 #233) |
|
1270 #235 := [monotonicity #232]: #234 |
|
1271 #240 := [trans #235 #238]: #239 |
|
1272 #243 := [monotonicity #240]: #242 |
|
1273 #251 := [trans #243 #249]: #250 |
|
1274 #273 := [monotonicity #251 #270]: #272 |
|
1275 #178 := [asserted]: #51 |
|
1276 #274 := [mp #178 #273]: #271 |
|
1277 #275 := [and-elim #274]: #247 |
|
1278 #196 := (* -1::real #31) |
|
1279 #212 := (+ #26 #196) |
|
1280 #213 := (<= #212 0::real) |
|
1281 #214 := (not #213) |
|
1282 #197 := (+ #28 #196) |
|
1283 #195 := (>= #197 0::real) |
|
1284 #193 := (not #195) |
|
1285 #219 := (and #193 #214) |
|
1286 #23 := (< #22 #22) |
|
1287 #35 := (ite #23 #34 #26) |
|
1288 #36 := (< #31 #35) |
|
1289 #29 := (ite #23 #26 #28) |
|
1290 #32 := (< #29 #31) |
|
1291 #37 := (and #32 #36) |
|
1292 #220 := (iff #37 #219) |
|
1293 #217 := (iff #36 #214) |
|
1294 #209 := (< #31 #26) |
|
1295 #215 := (iff #209 #214) |
|
1296 #216 := [rewrite]: #215 |
|
1297 #210 := (iff #36 #209) |
|
1298 #207 := (= #35 #26) |
|
1299 #202 := (ite false #34 #26) |
|
1300 #205 := (= #202 #26) |
|
1301 #206 := [rewrite]: #205 |
|
1302 #203 := (= #35 #202) |
|
1303 #180 := (iff #23 false) |
|
1304 #181 := [rewrite]: #180 |
|
1305 #204 := [monotonicity #181]: #203 |
|
1306 #208 := [trans #204 #206]: #207 |
|
1307 #211 := [monotonicity #208]: #210 |
|
1308 #218 := [trans #211 #216]: #217 |
|
1309 #200 := (iff #32 #193) |
|
1310 #189 := (< #28 #31) |
|
1311 #198 := (iff #189 #193) |
|
1312 #199 := [rewrite]: #198 |
|
1313 #190 := (iff #32 #189) |
|
1314 #187 := (= #29 #28) |
|
1315 #182 := (ite false #26 #28) |
|
1316 #185 := (= #182 #28) |
|
1317 #186 := [rewrite]: #185 |
|
1318 #183 := (= #29 #182) |
|
1319 #184 := [monotonicity #181]: #183 |
|
1320 #188 := [trans #184 #186]: #187 |
|
1321 #191 := [monotonicity #188]: #190 |
|
1322 #201 := [trans #191 #199]: #200 |
|
1323 #221 := [monotonicity #201 #218]: #220 |
|
1324 #177 := [asserted]: #37 |
|
1325 #222 := [mp #177 #221]: #219 |
|
1326 #224 := [and-elim #222]: #214 |
|
1327 [th-lemma #224 #275 #689]: false |
|
1328 unsat |
|
1329 NX/HT1QOfbspC2LtZNKpBA 428 0 |
|
1330 #2 := false |
|
1331 decl uf_10 :: T1 |
|
1332 #38 := uf_10 |
|
1333 decl uf_3 :: T1 |
|
1334 #21 := uf_3 |
|
1335 #45 := (= uf_3 uf_10) |
|
1336 decl uf_1 :: (-> int T1) |
|
1337 decl uf_2 :: (-> T1 int) |
|
1338 #39 := (uf_2 uf_10) |
|
1339 #588 := (uf_1 #39) |
|
1340 #686 := (= #588 uf_10) |
|
1341 #589 := (= uf_10 #588) |
|
1342 #4 := (:var 0 T1) |
|
1343 #5 := (uf_2 #4) |
|
1344 #541 := (pattern #5) |
|
1345 #6 := (uf_1 #5) |
|
1346 #93 := (= #4 #6) |
|
1347 #542 := (forall (vars (?x1 T1)) (:pat #541) #93) |
|
1348 #96 := (forall (vars (?x1 T1)) #93) |
|
1349 #545 := (iff #96 #542) |
|
1350 #543 := (iff #93 #93) |
|
1351 #544 := [refl]: #543 |
|
1352 #546 := [quant-intro #544]: #545 |
|
1353 #454 := (~ #96 #96) |
|
1354 #456 := (~ #93 #93) |
|
1355 #457 := [refl]: #456 |
|
1356 #455 := [nnf-pos #457]: #454 |
|
1357 #7 := (= #6 #4) |
|
1358 #8 := (forall (vars (?x1 T1)) #7) |
|
1359 #97 := (iff #8 #96) |
|
1360 #94 := (iff #7 #93) |
|
1361 #95 := [rewrite]: #94 |
|
1362 #98 := [quant-intro #95]: #97 |
|
1363 #92 := [asserted]: #8 |
|
1364 #101 := [mp #92 #98]: #96 |
|
1365 #452 := [mp~ #101 #455]: #96 |
|
1366 #547 := [mp #452 #546]: #542 |
|
1367 #590 := (not #542) |
|
1368 #595 := (or #590 #589) |
|
1369 #596 := [quant-inst]: #595 |
|
1370 #680 := [unit-resolution #596 #547]: #589 |
|
1371 #687 := [symm #680]: #686 |
|
1372 #688 := (= uf_3 #588) |
|
1373 #22 := (uf_2 uf_3) |
|
1374 #586 := (uf_1 #22) |
|
1375 #684 := (= #586 #588) |
|
1376 #682 := (= #588 #586) |
|
1377 #678 := (= #39 #22) |
|
1378 #676 := (= #22 #39) |
|
1379 #9 := 0::int |
|
1380 #227 := -1::int |
|
1381 #230 := (* -1::int #39) |
|
1382 #231 := (+ #22 #230) |
|
1383 #296 := (<= #231 0::int) |
|
1384 #70 := (<= #22 #39) |
|
1385 #393 := (iff #70 #296) |
|
1386 #394 := [rewrite]: #393 |
|
1387 #347 := [asserted]: #70 |
|
1388 #395 := [mp #347 #394]: #296 |
|
1389 #229 := (>= #231 0::int) |
|
1390 decl uf_4 :: (-> T2 T3 real) |
|
1391 decl uf_6 :: (-> T1 T3) |
|
1392 #25 := (uf_6 uf_3) |
|
1393 decl uf_7 :: T2 |
|
1394 #27 := uf_7 |
|
1395 #28 := (uf_4 uf_7 #25) |
|
1396 decl uf_9 :: T2 |
|
1397 #33 := uf_9 |
|
1398 #34 := (uf_4 uf_9 #25) |
|
1399 #46 := (uf_6 uf_10) |
|
1400 decl uf_5 :: T2 |
|
1401 #24 := uf_5 |
|
1402 #47 := (uf_4 uf_5 #46) |
|
1403 #48 := (ite #45 #47 #34) |
|
1404 #256 := (ite #229 #48 #28) |
|
1405 #568 := (= #28 #256) |
|
1406 #648 := (not #568) |
|
1407 #194 := 0::real |
|
1408 #192 := -1::real |
|
1409 #265 := (* -1::real #256) |
|
1410 #640 := (+ #28 #265) |
|
1411 #642 := (>= #640 0::real) |
|
1412 #645 := (not #642) |
|
1413 #643 := [hypothesis]: #642 |
|
1414 decl uf_8 :: T2 |
|
1415 #30 := uf_8 |
|
1416 #31 := (uf_4 uf_8 #25) |
|
1417 #266 := (+ #31 #265) |
|
1418 #264 := (>= #266 0::real) |
|
1419 #267 := (not #264) |
|
1420 #26 := (uf_4 uf_5 #25) |
|
1421 decl uf_11 :: T2 |
|
1422 #41 := uf_11 |
|
1423 #42 := (uf_4 uf_11 #25) |
|
1424 #237 := (ite #229 #42 #26) |
|
1425 #245 := (* -1::real #237) |
|
1426 #246 := (+ #31 #245) |
|
1427 #247 := (<= #246 0::real) |
|
1428 #248 := (not #247) |
|
1429 #272 := (and #248 #267) |
|
1430 #40 := (< #22 #39) |
|
1431 #49 := (ite #40 #28 #48) |
|
1432 #50 := (< #31 #49) |
|
1433 #43 := (ite #40 #26 #42) |
|
1434 #44 := (< #43 #31) |
|
1435 #51 := (and #44 #50) |
|
1436 #273 := (iff #51 #272) |
|
1437 #270 := (iff #50 #267) |
|
1438 #261 := (< #31 #256) |
|
1439 #268 := (iff #261 #267) |
|
1440 #269 := [rewrite]: #268 |
|
1441 #262 := (iff #50 #261) |
|
1442 #259 := (= #49 #256) |
|
1443 #228 := (not #229) |
|
1444 #253 := (ite #228 #28 #48) |
|
1445 #257 := (= #253 #256) |
|
1446 #258 := [rewrite]: #257 |
|
1447 #254 := (= #49 #253) |
|
1448 #232 := (iff #40 #228) |
|
1449 #233 := [rewrite]: #232 |
|
1450 #255 := [monotonicity #233]: #254 |
|
1451 #260 := [trans #255 #258]: #259 |
|
1452 #263 := [monotonicity #260]: #262 |
|
1453 #271 := [trans #263 #269]: #270 |
|
1454 #251 := (iff #44 #248) |
|
1455 #242 := (< #237 #31) |
|
1456 #249 := (iff #242 #248) |
|
1457 #250 := [rewrite]: #249 |
|
1458 #243 := (iff #44 #242) |
|
1459 #240 := (= #43 #237) |
|
1460 #234 := (ite #228 #26 #42) |
|
1461 #238 := (= #234 #237) |
|
1462 #239 := [rewrite]: #238 |
|
1463 #235 := (= #43 #234) |
|
1464 #236 := [monotonicity #233]: #235 |
|
1465 #241 := [trans #236 #239]: #240 |
|
1466 #244 := [monotonicity #241]: #243 |
|
1467 #252 := [trans #244 #250]: #251 |
|
1468 #274 := [monotonicity #252 #271]: #273 |
|
1469 #178 := [asserted]: #51 |
|
1470 #275 := [mp #178 #274]: #272 |
|
1471 #277 := [and-elim #275]: #267 |
|
1472 #196 := (* -1::real #31) |
|
1473 #197 := (+ #28 #196) |
|
1474 #195 := (>= #197 0::real) |
|
1475 #193 := (not #195) |
|
1476 #213 := (* -1::real #34) |
|
1477 #214 := (+ #31 #213) |
|
1478 #212 := (>= #214 0::real) |
|
1479 #215 := (not #212) |
|
1480 #220 := (and #193 #215) |
|
1481 #23 := (< #22 #22) |
|
1482 #35 := (ite #23 #28 #34) |
|
1483 #36 := (< #31 #35) |
|
1484 #29 := (ite #23 #26 #28) |
|
1485 #32 := (< #29 #31) |
|
1486 #37 := (and #32 #36) |
|
1487 #221 := (iff #37 #220) |
|
1488 #218 := (iff #36 #215) |
|
1489 #209 := (< #31 #34) |
|
1490 #216 := (iff #209 #215) |
|
1491 #217 := [rewrite]: #216 |
|
1492 #210 := (iff #36 #209) |
|
1493 #207 := (= #35 #34) |
|
1494 #202 := (ite false #28 #34) |
|
1495 #205 := (= #202 #34) |
|
1496 #206 := [rewrite]: #205 |
|
1497 #203 := (= #35 #202) |
|
1498 #180 := (iff #23 false) |
|
1499 #181 := [rewrite]: #180 |
|
1500 #204 := [monotonicity #181]: #203 |
|
1501 #208 := [trans #204 #206]: #207 |
|
1502 #211 := [monotonicity #208]: #210 |
|
1503 #219 := [trans #211 #217]: #218 |
|
1504 #200 := (iff #32 #193) |
|
1505 #189 := (< #28 #31) |
|
1506 #198 := (iff #189 #193) |
|
1507 #199 := [rewrite]: #198 |
|
1508 #190 := (iff #32 #189) |
|
1509 #187 := (= #29 #28) |
|
1510 #182 := (ite false #26 #28) |
|
1511 #185 := (= #182 #28) |
|
1512 #186 := [rewrite]: #185 |
|
1513 #183 := (= #29 #182) |
|
1514 #184 := [monotonicity #181]: #183 |
|
1515 #188 := [trans #184 #186]: #187 |
|
1516 #191 := [monotonicity #188]: #190 |
|
1517 #201 := [trans #191 #199]: #200 |
|
1518 #222 := [monotonicity #201 #219]: #221 |
|
1519 #177 := [asserted]: #37 |
|
1520 #223 := [mp #177 #222]: #220 |
|
1521 #224 := [and-elim #223]: #193 |
|
1522 #644 := [th-lemma #224 #277 #643]: false |
|
1523 #646 := [lemma #644]: #645 |
|
1524 #647 := [hypothesis]: #568 |
|
1525 #649 := (or #648 #642) |
|
1526 #650 := [th-lemma]: #649 |
|
1527 #651 := [unit-resolution #650 #647 #646]: false |
|
1528 #652 := [lemma #651]: #648 |
|
1529 #578 := (or #229 #568) |
|
1530 #579 := [def-axiom]: #578 |
|
1531 #675 := [unit-resolution #579 #652]: #229 |
|
1532 #677 := [th-lemma #675 #395]: #676 |
|
1533 #679 := [symm #677]: #678 |
|
1534 #683 := [monotonicity #679]: #682 |
|
1535 #685 := [symm #683]: #684 |
|
1536 #587 := (= uf_3 #586) |
|
1537 #591 := (or #590 #587) |
|
1538 #592 := [quant-inst]: #591 |
|
1539 #681 := [unit-resolution #592 #547]: #587 |
|
1540 #689 := [trans #681 #685]: #688 |
|
1541 #690 := [trans #689 #687]: #45 |
|
1542 #571 := (not #45) |
|
1543 #54 := (uf_4 uf_11 #46) |
|
1544 #279 := (ite #45 #28 #54) |
|
1545 #465 := (* -1::real #279) |
|
1546 #632 := (+ #28 #465) |
|
1547 #633 := (<= #632 0::real) |
|
1548 #580 := (= #28 #279) |
|
1549 #656 := [hypothesis]: #45 |
|
1550 #582 := (or #571 #580) |
|
1551 #583 := [def-axiom]: #582 |
|
1552 #657 := [unit-resolution #583 #656]: #580 |
|
1553 #658 := (not #580) |
|
1554 #659 := (or #658 #633) |
|
1555 #660 := [th-lemma]: #659 |
|
1556 #661 := [unit-resolution #660 #657]: #633 |
|
1557 #57 := (uf_4 uf_8 #46) |
|
1558 #363 := (* -1::real #57) |
|
1559 #379 := (+ #47 #363) |
|
1560 #380 := (<= #379 0::real) |
|
1561 #381 := (not #380) |
|
1562 #364 := (+ #54 #363) |
|
1563 #362 := (>= #364 0::real) |
|
1564 #361 := (not #362) |
|
1565 #386 := (and #361 #381) |
|
1566 #59 := (uf_4 uf_7 #46) |
|
1567 #64 := (< #39 #39) |
|
1568 #67 := (ite #64 #59 #47) |
|
1569 #68 := (< #57 #67) |
|
1570 #65 := (ite #64 #47 #54) |
|
1571 #66 := (< #65 #57) |
|
1572 #69 := (and #66 #68) |
|
1573 #387 := (iff #69 #386) |
|
1574 #384 := (iff #68 #381) |
|
1575 #376 := (< #57 #47) |
|
1576 #382 := (iff #376 #381) |
|
1577 #383 := [rewrite]: #382 |
|
1578 #377 := (iff #68 #376) |
|
1579 #374 := (= #67 #47) |
|
1580 #369 := (ite false #59 #47) |
|
1581 #372 := (= #369 #47) |
|
1582 #373 := [rewrite]: #372 |
|
1583 #370 := (= #67 #369) |
|
1584 #349 := (iff #64 false) |
|
1585 #350 := [rewrite]: #349 |
|
1586 #371 := [monotonicity #350]: #370 |
|
1587 #375 := [trans #371 #373]: #374 |
|
1588 #378 := [monotonicity #375]: #377 |
|
1589 #385 := [trans #378 #383]: #384 |
|
1590 #367 := (iff #66 #361) |
|
1591 #358 := (< #54 #57) |
|
1592 #365 := (iff #358 #361) |
|
1593 #366 := [rewrite]: #365 |
|
1594 #359 := (iff #66 #358) |
|
1595 #356 := (= #65 #54) |
|
1596 #351 := (ite false #47 #54) |
|
1597 #354 := (= #351 #54) |
|
1598 #355 := [rewrite]: #354 |
|
1599 #352 := (= #65 #351) |
|
1600 #353 := [monotonicity #350]: #352 |
|
1601 #357 := [trans #353 #355]: #356 |
|
1602 #360 := [monotonicity #357]: #359 |
|
1603 #368 := [trans #360 #366]: #367 |
|
1604 #388 := [monotonicity #368 #385]: #387 |
|
1605 #346 := [asserted]: #69 |
|
1606 #389 := [mp #346 #388]: #386 |
|
1607 #391 := [and-elim #389]: #381 |
|
1608 #397 := (* -1::real #59) |
|
1609 #398 := (+ #47 #397) |
|
1610 #399 := (<= #398 0::real) |
|
1611 #409 := (* -1::real #54) |
|
1612 #410 := (+ #47 #409) |
|
1613 #408 := (>= #410 0::real) |
|
1614 #60 := (uf_4 uf_9 #46) |
|
1615 #402 := (* -1::real #60) |
|
1616 #403 := (+ #59 #402) |
|
1617 #404 := (<= #403 0::real) |
|
1618 #418 := (and #399 #404 #408) |
|
1619 #73 := (<= #59 #60) |
|
1620 #72 := (<= #47 #59) |
|
1621 #74 := (and #72 #73) |
|
1622 #71 := (<= #54 #47) |
|
1623 #75 := (and #71 #74) |
|
1624 #421 := (iff #75 #418) |
|
1625 #412 := (and #399 #404) |
|
1626 #415 := (and #408 #412) |
|
1627 #419 := (iff #415 #418) |
|
1628 #420 := [rewrite]: #419 |
|
1629 #416 := (iff #75 #415) |
|
1630 #413 := (iff #74 #412) |
|
1631 #405 := (iff #73 #404) |
|
1632 #406 := [rewrite]: #405 |
|
1633 #400 := (iff #72 #399) |
|
1634 #401 := [rewrite]: #400 |
|
1635 #414 := [monotonicity #401 #406]: #413 |
|
1636 #407 := (iff #71 #408) |
|
1637 #411 := [rewrite]: #407 |
|
1638 #417 := [monotonicity #411 #414]: #416 |
|
1639 #422 := [trans #417 #420]: #421 |
|
1640 #348 := [asserted]: #75 |
|
1641 #423 := [mp #348 #422]: #418 |
|
1642 #424 := [and-elim #423]: #399 |
|
1643 #637 := (+ #28 #397) |
|
1644 #639 := (>= #637 0::real) |
|
1645 #636 := (= #28 #59) |
|
1646 #666 := (= #59 #28) |
|
1647 #664 := (= #46 #25) |
|
1648 #662 := (= #25 #46) |
|
1649 #663 := [monotonicity #656]: #662 |
|
1650 #665 := [symm #663]: #664 |
|
1651 #667 := [monotonicity #665]: #666 |
|
1652 #668 := [symm #667]: #636 |
|
1653 #669 := (not #636) |
|
1654 #670 := (or #669 #639) |
|
1655 #671 := [th-lemma]: #670 |
|
1656 #672 := [unit-resolution #671 #668]: #639 |
|
1657 #468 := (+ #57 #465) |
|
1658 #471 := (<= #468 0::real) |
|
1659 #444 := (not #471) |
|
1660 #322 := (ite #296 #279 #47) |
|
1661 #330 := (* -1::real #322) |
|
1662 #331 := (+ #57 #330) |
|
1663 #332 := (<= #331 0::real) |
|
1664 #333 := (not #332) |
|
1665 #445 := (iff #333 #444) |
|
1666 #472 := (iff #332 #471) |
|
1667 #469 := (= #331 #468) |
|
1668 #466 := (= #330 #465) |
|
1669 #463 := (= #322 #279) |
|
1670 #1 := true |
|
1671 #458 := (ite true #279 #47) |
|
1672 #461 := (= #458 #279) |
|
1673 #462 := [rewrite]: #461 |
|
1674 #459 := (= #322 #458) |
|
1675 #450 := (iff #296 true) |
|
1676 #451 := [iff-true #395]: #450 |
|
1677 #460 := [monotonicity #451]: #459 |
|
1678 #464 := [trans #460 #462]: #463 |
|
1679 #467 := [monotonicity #464]: #466 |
|
1680 #470 := [monotonicity #467]: #469 |
|
1681 #473 := [monotonicity #470]: #472 |
|
1682 #474 := [monotonicity #473]: #445 |
|
1683 #303 := (ite #296 #60 #59) |
|
1684 #313 := (* -1::real #303) |
|
1685 #314 := (+ #57 #313) |
|
1686 #312 := (>= #314 0::real) |
|
1687 #311 := (not #312) |
|
1688 #338 := (and #311 #333) |
|
1689 #52 := (< #39 #22) |
|
1690 #61 := (ite #52 #59 #60) |
|
1691 #62 := (< #57 #61) |
|
1692 #53 := (= uf_10 uf_3) |
|
1693 #55 := (ite #53 #28 #54) |
|
1694 #56 := (ite #52 #47 #55) |
|
1695 #58 := (< #56 #57) |
|
1696 #63 := (and #58 #62) |
|
1697 #341 := (iff #63 #338) |
|
1698 #282 := (ite #52 #47 #279) |
|
1699 #285 := (< #282 #57) |
|
1700 #291 := (and #62 #285) |
|
1701 #339 := (iff #291 #338) |
|
1702 #336 := (iff #285 #333) |
|
1703 #327 := (< #322 #57) |
|
1704 #334 := (iff #327 #333) |
|
1705 #335 := [rewrite]: #334 |
|
1706 #328 := (iff #285 #327) |
|
1707 #325 := (= #282 #322) |
|
1708 #297 := (not #296) |
|
1709 #319 := (ite #297 #47 #279) |
|
1710 #323 := (= #319 #322) |
|
1711 #324 := [rewrite]: #323 |
|
1712 #320 := (= #282 #319) |
|
1713 #298 := (iff #52 #297) |
|
1714 #299 := [rewrite]: #298 |
|
1715 #321 := [monotonicity #299]: #320 |
|
1716 #326 := [trans #321 #324]: #325 |
|
1717 #329 := [monotonicity #326]: #328 |
|
1718 #337 := [trans #329 #335]: #336 |
|
1719 #317 := (iff #62 #311) |
|
1720 #308 := (< #57 #303) |
|
1721 #315 := (iff #308 #311) |
|
1722 #316 := [rewrite]: #315 |
|
1723 #309 := (iff #62 #308) |
|
1724 #306 := (= #61 #303) |
|
1725 #300 := (ite #297 #59 #60) |
|
1726 #304 := (= #300 #303) |
|
1727 #305 := [rewrite]: #304 |
|
1728 #301 := (= #61 #300) |
|
1729 #302 := [monotonicity #299]: #301 |
|
1730 #307 := [trans #302 #305]: #306 |
|
1731 #310 := [monotonicity #307]: #309 |
|
1732 #318 := [trans #310 #316]: #317 |
|
1733 #340 := [monotonicity #318 #337]: #339 |
|
1734 #294 := (iff #63 #291) |
|
1735 #288 := (and #285 #62) |
|
1736 #292 := (iff #288 #291) |
|
1737 #293 := [rewrite]: #292 |
|
1738 #289 := (iff #63 #288) |
|
1739 #286 := (iff #58 #285) |
|
1740 #283 := (= #56 #282) |
|
1741 #280 := (= #55 #279) |
|
1742 #226 := (iff #53 #45) |
|
1743 #278 := [rewrite]: #226 |
|
1744 #281 := [monotonicity #278]: #280 |
|
1745 #284 := [monotonicity #281]: #283 |
|
1746 #287 := [monotonicity #284]: #286 |
|
1747 #290 := [monotonicity #287]: #289 |
|
1748 #295 := [trans #290 #293]: #294 |
|
1749 #342 := [trans #295 #340]: #341 |
|
1750 #179 := [asserted]: #63 |
|
1751 #343 := [mp #179 #342]: #338 |
|
1752 #345 := [and-elim #343]: #333 |
|
1753 #475 := [mp #345 #474]: #444 |
|
1754 #673 := [th-lemma #475 #672 #424 #391 #661]: false |
|
1755 #674 := [lemma #673]: #571 |
|
1756 [unit-resolution #674 #690]: false |
|
1757 unsat |
|
1758 IL2powemHjRpCJYwmXFxyw 211 0 |
|
1759 #2 := false |
1759 #2 := false |
1760 #33 := 0::real |
1760 #33 := 0::real |
1761 decl uf_11 :: (-> T5 T6 real) |
1761 decl uf_11 :: (-> T5 T6 real) |
1762 decl uf_15 :: T6 |
1762 decl uf_15 :: T6 |
1763 #28 := uf_15 |
1763 #28 := uf_15 |
3208 #152 := (not #142) |
3208 #152 := (not #142) |
3209 #154 := (or #45 #152 #153) |
3209 #154 := (or #45 #152 #153) |
3210 #155 := [th-lemma]: #154 |
3210 #155 := [th-lemma]: #154 |
3211 [unit-resolution #155 #60 #148 #144]: false |
3211 [unit-resolution #155 #60 #148 #144]: false |
3212 unsat |
3212 unsat |
3213 V+IAyBZU/6QjYs6JkXx8LQ 57 0 |
|
3214 #2 := false |
|
3215 #4 := 0::real |
|
3216 decl uf_1 :: (-> T2 real) |
|
3217 decl uf_2 :: (-> T1 T1 T2) |
|
3218 decl uf_12 :: (-> T4 T1) |
|
3219 decl uf_4 :: T4 |
|
3220 #11 := uf_4 |
|
3221 #39 := (uf_12 uf_4) |
|
3222 decl uf_10 :: T4 |
|
3223 #27 := uf_10 |
|
3224 #38 := (uf_12 uf_10) |
|
3225 #40 := (uf_2 #38 #39) |
|
3226 #41 := (uf_1 #40) |
|
3227 #264 := (>= #41 0::real) |
|
3228 #266 := (not #264) |
|
3229 #43 := (= #41 0::real) |
|
3230 #44 := (not #43) |
|
3231 #131 := [asserted]: #44 |
|
3232 #272 := (or #43 #266) |
|
3233 #42 := (<= #41 0::real) |
|
3234 #130 := [asserted]: #42 |
|
3235 #265 := (not #42) |
|
3236 #270 := (or #43 #265 #266) |
|
3237 #271 := [th-lemma]: #270 |
|
3238 #273 := [unit-resolution #271 #130]: #272 |
|
3239 #274 := [unit-resolution #273 #131]: #266 |
|
3240 #6 := (:var 0 T1) |
|
3241 #5 := (:var 1 T1) |
|
3242 #7 := (uf_2 #5 #6) |
|
3243 #241 := (pattern #7) |
|
3244 #8 := (uf_1 #7) |
|
3245 #65 := (>= #8 0::real) |
|
3246 #242 := (forall (vars (?x1 T1) (?x2 T1)) (:pat #241) #65) |
|
3247 #66 := (forall (vars (?x1 T1) (?x2 T1)) #65) |
|
3248 #245 := (iff #66 #242) |
|
3249 #243 := (iff #65 #65) |
|
3250 #244 := [refl]: #243 |
|
3251 #246 := [quant-intro #244]: #245 |
|
3252 #149 := (~ #66 #66) |
|
3253 #151 := (~ #65 #65) |
|
3254 #152 := [refl]: #151 |
|
3255 #150 := [nnf-pos #152]: #149 |
|
3256 #9 := (<= 0::real #8) |
|
3257 #10 := (forall (vars (?x1 T1) (?x2 T1)) #9) |
|
3258 #67 := (iff #10 #66) |
|
3259 #63 := (iff #9 #65) |
|
3260 #64 := [rewrite]: #63 |
|
3261 #68 := [quant-intro #64]: #67 |
|
3262 #60 := [asserted]: #10 |
|
3263 #69 := [mp #60 #68]: #66 |
|
3264 #147 := [mp~ #69 #150]: #66 |
|
3265 #247 := [mp #147 #246]: #242 |
|
3266 #267 := (not #242) |
|
3267 #268 := (or #267 #264) |
|
3268 #269 := [quant-inst]: #268 |
|
3269 [unit-resolution #269 #247 #274]: false |
|
3270 unsat |
|
3271 vqiyJ/qjGXZ3iOg6xftiug 15 0 |
|
3272 uf_1 -> val!0 |
|
3273 uf_2 -> val!1 |
|
3274 uf_3 -> val!2 |
|
3275 uf_5 -> val!15 |
|
3276 uf_6 -> val!26 |
|
3277 uf_4 -> { |
|
3278 val!0 -> val!12 |
|
3279 val!1 -> val!13 |
|
3280 else -> val!13 |
|
3281 } |
|
3282 uf_7 -> { |
|
3283 val!6 -> val!31 |
|
3284 else -> val!31 |
|
3285 } |
|
3286 sat |
|
3287 mrZPJZyTokErrN6SYupisw 9 0 |
|
3288 uf_4 -> val!1 |
|
3289 uf_2 -> val!3 |
|
3290 uf_3 -> val!4 |
|
3291 uf_1 -> { |
|
3292 val!5 -> val!6 |
|
3293 val!4 -> val!7 |
|
3294 else -> val!7 |
|
3295 } |
|
3296 sat |
|
3297 qkVrmXMcHAG5MLuJ9d8jXQ 211 0 |
|
3298 #2 := false |
|
3299 #33 := 0::real |
|
3300 decl uf_11 :: (-> T5 T6 real) |
|
3301 decl uf_15 :: T6 |
|
3302 #28 := uf_15 |
|
3303 decl uf_16 :: T5 |
|
3304 #30 := uf_16 |
|
3305 #31 := (uf_11 uf_16 uf_15) |
|
3306 decl uf_12 :: (-> T7 T8 T5) |
|
3307 decl uf_14 :: T8 |
|
3308 #26 := uf_14 |
|
3309 decl uf_13 :: (-> T1 T7) |
|
3310 decl uf_8 :: T1 |
|
3311 #16 := uf_8 |
|
3312 #25 := (uf_13 uf_8) |
|
3313 #27 := (uf_12 #25 uf_14) |
|
3314 #29 := (uf_11 #27 uf_15) |
|
3315 #73 := -1::real |
|
3316 #84 := (* -1::real #29) |
|
3317 #85 := (+ #84 #31) |
|
3318 #74 := (* -1::real #31) |
|
3319 #75 := (+ #29 #74) |
|
3320 #112 := (>= #75 0::real) |
|
3321 #119 := (ite #112 #75 #85) |
|
3322 #127 := (* -1::real #119) |
|
3323 decl uf_17 :: T5 |
|
3324 #37 := uf_17 |
|
3325 #38 := (uf_11 uf_17 uf_15) |
|
3326 #102 := -1/3::real |
|
3327 #103 := (* -1/3::real #38) |
|
3328 #128 := (+ #103 #127) |
|
3329 #100 := 1/3::real |
|
3330 #101 := (* 1/3::real #31) |
|
3331 #129 := (+ #101 #128) |
|
3332 #130 := (<= #129 0::real) |
|
3333 #131 := (not #130) |
|
3334 #40 := 3::real |
|
3335 #39 := (- #31 #38) |
|
3336 #41 := (/ #39 3::real) |
|
3337 #32 := (- #29 #31) |
|
3338 #35 := (- #32) |
|
3339 #34 := (< #32 0::real) |
|
3340 #36 := (ite #34 #35 #32) |
|
3341 #42 := (< #36 #41) |
|
3342 #136 := (iff #42 #131) |
|
3343 #104 := (+ #101 #103) |
|
3344 #78 := (< #75 0::real) |
|
3345 #90 := (ite #78 #85 #75) |
|
3346 #109 := (< #90 #104) |
|
3347 #134 := (iff #109 #131) |
|
3348 #124 := (< #119 #104) |
|
3349 #132 := (iff #124 #131) |
|
3350 #133 := [rewrite]: #132 |
|
3351 #125 := (iff #109 #124) |
|
3352 #122 := (= #90 #119) |
|
3353 #113 := (not #112) |
|
3354 #116 := (ite #113 #85 #75) |
|
3355 #120 := (= #116 #119) |
|
3356 #121 := [rewrite]: #120 |
|
3357 #117 := (= #90 #116) |
|
3358 #114 := (iff #78 #113) |
|
3359 #115 := [rewrite]: #114 |
|
3360 #118 := [monotonicity #115]: #117 |
|
3361 #123 := [trans #118 #121]: #122 |
|
3362 #126 := [monotonicity #123]: #125 |
|
3363 #135 := [trans #126 #133]: #134 |
|
3364 #110 := (iff #42 #109) |
|
3365 #107 := (= #41 #104) |
|
3366 #93 := (* -1::real #38) |
|
3367 #94 := (+ #31 #93) |
|
3368 #97 := (/ #94 3::real) |
|
3369 #105 := (= #97 #104) |
|
3370 #106 := [rewrite]: #105 |
|
3371 #98 := (= #41 #97) |
|
3372 #95 := (= #39 #94) |
|
3373 #96 := [rewrite]: #95 |
|
3374 #99 := [monotonicity #96]: #98 |
|
3375 #108 := [trans #99 #106]: #107 |
|
3376 #91 := (= #36 #90) |
|
3377 #76 := (= #32 #75) |
|
3378 #77 := [rewrite]: #76 |
|
3379 #88 := (= #35 #85) |
|
3380 #81 := (- #75) |
|
3381 #86 := (= #81 #85) |
|
3382 #87 := [rewrite]: #86 |
|
3383 #82 := (= #35 #81) |
|
3384 #83 := [monotonicity #77]: #82 |
|
3385 #89 := [trans #83 #87]: #88 |
|
3386 #79 := (iff #34 #78) |
|
3387 #80 := [monotonicity #77]: #79 |
|
3388 #92 := [monotonicity #80 #89 #77]: #91 |
|
3389 #111 := [monotonicity #92 #108]: #110 |
|
3390 #137 := [trans #111 #135]: #136 |
|
3391 #72 := [asserted]: #42 |
|
3392 #138 := [mp #72 #137]: #131 |
|
3393 decl uf_1 :: T1 |
|
3394 #4 := uf_1 |
|
3395 #43 := (uf_13 uf_1) |
|
3396 #44 := (uf_12 #43 uf_14) |
|
3397 #45 := (uf_11 #44 uf_15) |
|
3398 #149 := (* -1::real #45) |
|
3399 #150 := (+ #38 #149) |
|
3400 #140 := (+ #93 #45) |
|
3401 #161 := (<= #150 0::real) |
|
3402 #168 := (ite #161 #140 #150) |
|
3403 #176 := (* -1::real #168) |
|
3404 #177 := (+ #103 #176) |
|
3405 #178 := (+ #101 #177) |
|
3406 #179 := (<= #178 0::real) |
|
3407 #180 := (not #179) |
|
3408 #46 := (- #45 #38) |
|
3409 #48 := (- #46) |
|
3410 #47 := (< #46 0::real) |
|
3411 #49 := (ite #47 #48 #46) |
|
3412 #50 := (< #49 #41) |
|
3413 #185 := (iff #50 #180) |
|
3414 #143 := (< #140 0::real) |
|
3415 #155 := (ite #143 #150 #140) |
|
3416 #158 := (< #155 #104) |
|
3417 #183 := (iff #158 #180) |
|
3418 #173 := (< #168 #104) |
|
3419 #181 := (iff #173 #180) |
|
3420 #182 := [rewrite]: #181 |
|
3421 #174 := (iff #158 #173) |
|
3422 #171 := (= #155 #168) |
|
3423 #162 := (not #161) |
|
3424 #165 := (ite #162 #150 #140) |
|
3425 #169 := (= #165 #168) |
|
3426 #170 := [rewrite]: #169 |
|
3427 #166 := (= #155 #165) |
|
3428 #163 := (iff #143 #162) |
|
3429 #164 := [rewrite]: #163 |
|
3430 #167 := [monotonicity #164]: #166 |
|
3431 #172 := [trans #167 #170]: #171 |
|
3432 #175 := [monotonicity #172]: #174 |
|
3433 #184 := [trans #175 #182]: #183 |
|
3434 #159 := (iff #50 #158) |
|
3435 #156 := (= #49 #155) |
|
3436 #141 := (= #46 #140) |
|
3437 #142 := [rewrite]: #141 |
|
3438 #153 := (= #48 #150) |
|
3439 #146 := (- #140) |
|
3440 #151 := (= #146 #150) |
|
3441 #152 := [rewrite]: #151 |
|
3442 #147 := (= #48 #146) |
|
3443 #148 := [monotonicity #142]: #147 |
|
3444 #154 := [trans #148 #152]: #153 |
|
3445 #144 := (iff #47 #143) |
|
3446 #145 := [monotonicity #142]: #144 |
|
3447 #157 := [monotonicity #145 #154 #142]: #156 |
|
3448 #160 := [monotonicity #157 #108]: #159 |
|
3449 #186 := [trans #160 #184]: #185 |
|
3450 #139 := [asserted]: #50 |
|
3451 #187 := [mp #139 #186]: #180 |
|
3452 #299 := (+ #140 #176) |
|
3453 #300 := (<= #299 0::real) |
|
3454 #290 := (= #140 #168) |
|
3455 #329 := [hypothesis]: #162 |
|
3456 #191 := (+ #29 #149) |
|
3457 #192 := (<= #191 0::real) |
|
3458 #51 := (<= #29 #45) |
|
3459 #193 := (iff #51 #192) |
|
3460 #194 := [rewrite]: #193 |
|
3461 #188 := [asserted]: #51 |
|
3462 #195 := [mp #188 #194]: #192 |
|
3463 #298 := (+ #75 #127) |
|
3464 #301 := (<= #298 0::real) |
|
3465 #284 := (= #75 #119) |
|
3466 #302 := [hypothesis]: #113 |
|
3467 #296 := (+ #85 #127) |
|
3468 #297 := (<= #296 0::real) |
|
3469 #285 := (= #85 #119) |
|
3470 #288 := (or #112 #285) |
|
3471 #289 := [def-axiom]: #288 |
|
3472 #303 := [unit-resolution #289 #302]: #285 |
|
3473 #304 := (not #285) |
|
3474 #305 := (or #304 #297) |
|
3475 #306 := [th-lemma]: #305 |
|
3476 #307 := [unit-resolution #306 #303]: #297 |
|
3477 #315 := (not #290) |
|
3478 #310 := (not #300) |
|
3479 #311 := (or #310 #112) |
|
3480 #308 := [hypothesis]: #300 |
|
3481 #309 := [th-lemma #308 #307 #138 #302 #187 #195]: false |
|
3482 #312 := [lemma #309]: #311 |
|
3483 #322 := [unit-resolution #312 #302]: #310 |
|
3484 #316 := (or #315 #300) |
|
3485 #313 := [hypothesis]: #310 |
|
3486 #314 := [hypothesis]: #290 |
|
3487 #317 := [th-lemma]: #316 |
|
3488 #318 := [unit-resolution #317 #314 #313]: false |
|
3489 #319 := [lemma #318]: #316 |
|
3490 #323 := [unit-resolution #319 #322]: #315 |
|
3491 #292 := (or #162 #290) |
|
3492 #293 := [def-axiom]: #292 |
|
3493 #324 := [unit-resolution #293 #323]: #162 |
|
3494 #325 := [th-lemma #324 #307 #138 #302 #195]: false |
|
3495 #326 := [lemma #325]: #112 |
|
3496 #286 := (or #113 #284) |
|
3497 #287 := [def-axiom]: #286 |
|
3498 #330 := [unit-resolution #287 #326]: #284 |
|
3499 #331 := (not #284) |
|
3500 #332 := (or #331 #301) |
|
3501 #333 := [th-lemma]: #332 |
|
3502 #334 := [unit-resolution #333 #330]: #301 |
|
3503 #335 := [th-lemma #326 #334 #195 #329 #138]: false |
|
3504 #336 := [lemma #335]: #161 |
|
3505 #327 := [unit-resolution #293 #336]: #290 |
|
3506 #328 := [unit-resolution #319 #327]: #300 |
|
3507 [th-lemma #326 #334 #195 #328 #187 #138]: false |
|
3508 unsat |
|
3509 WrIjxhfF5EcRCmS6xKG3XQ 211 0 |
|
3510 #2 := false |
|
3511 #33 := 0::real |
|
3512 decl uf_11 :: (-> T5 T6 real) |
|
3513 decl uf_15 :: T6 |
|
3514 #28 := uf_15 |
|
3515 decl uf_16 :: T5 |
|
3516 #30 := uf_16 |
|
3517 #31 := (uf_11 uf_16 uf_15) |
|
3518 decl uf_12 :: (-> T7 T8 T5) |
|
3519 decl uf_14 :: T8 |
|
3520 #26 := uf_14 |
|
3521 decl uf_13 :: (-> T1 T7) |
|
3522 decl uf_8 :: T1 |
|
3523 #16 := uf_8 |
|
3524 #25 := (uf_13 uf_8) |
|
3525 #27 := (uf_12 #25 uf_14) |
|
3526 #29 := (uf_11 #27 uf_15) |
|
3527 #73 := -1::real |
|
3528 #84 := (* -1::real #29) |
|
3529 #85 := (+ #84 #31) |
|
3530 #74 := (* -1::real #31) |
|
3531 #75 := (+ #29 #74) |
|
3532 #112 := (>= #75 0::real) |
|
3533 #119 := (ite #112 #75 #85) |
|
3534 #127 := (* -1::real #119) |
|
3535 decl uf_17 :: T5 |
|
3536 #37 := uf_17 |
|
3537 #38 := (uf_11 uf_17 uf_15) |
|
3538 #102 := -1/3::real |
|
3539 #103 := (* -1/3::real #38) |
|
3540 #128 := (+ #103 #127) |
|
3541 #100 := 1/3::real |
|
3542 #101 := (* 1/3::real #31) |
|
3543 #129 := (+ #101 #128) |
|
3544 #130 := (<= #129 0::real) |
|
3545 #131 := (not #130) |
|
3546 #40 := 3::real |
|
3547 #39 := (- #31 #38) |
|
3548 #41 := (/ #39 3::real) |
|
3549 #32 := (- #29 #31) |
|
3550 #35 := (- #32) |
|
3551 #34 := (< #32 0::real) |
|
3552 #36 := (ite #34 #35 #32) |
|
3553 #42 := (< #36 #41) |
|
3554 #136 := (iff #42 #131) |
|
3555 #104 := (+ #101 #103) |
|
3556 #78 := (< #75 0::real) |
|
3557 #90 := (ite #78 #85 #75) |
|
3558 #109 := (< #90 #104) |
|
3559 #134 := (iff #109 #131) |
|
3560 #124 := (< #119 #104) |
|
3561 #132 := (iff #124 #131) |
|
3562 #133 := [rewrite]: #132 |
|
3563 #125 := (iff #109 #124) |
|
3564 #122 := (= #90 #119) |
|
3565 #113 := (not #112) |
|
3566 #116 := (ite #113 #85 #75) |
|
3567 #120 := (= #116 #119) |
|
3568 #121 := [rewrite]: #120 |
|
3569 #117 := (= #90 #116) |
|
3570 #114 := (iff #78 #113) |
|
3571 #115 := [rewrite]: #114 |
|
3572 #118 := [monotonicity #115]: #117 |
|
3573 #123 := [trans #118 #121]: #122 |
|
3574 #126 := [monotonicity #123]: #125 |
|
3575 #135 := [trans #126 #133]: #134 |
|
3576 #110 := (iff #42 #109) |
|
3577 #107 := (= #41 #104) |
|
3578 #93 := (* -1::real #38) |
|
3579 #94 := (+ #31 #93) |
|
3580 #97 := (/ #94 3::real) |
|
3581 #105 := (= #97 #104) |
|
3582 #106 := [rewrite]: #105 |
|
3583 #98 := (= #41 #97) |
|
3584 #95 := (= #39 #94) |
|
3585 #96 := [rewrite]: #95 |
|
3586 #99 := [monotonicity #96]: #98 |
|
3587 #108 := [trans #99 #106]: #107 |
|
3588 #91 := (= #36 #90) |
|
3589 #76 := (= #32 #75) |
|
3590 #77 := [rewrite]: #76 |
|
3591 #88 := (= #35 #85) |
|
3592 #81 := (- #75) |
|
3593 #86 := (= #81 #85) |
|
3594 #87 := [rewrite]: #86 |
|
3595 #82 := (= #35 #81) |
|
3596 #83 := [monotonicity #77]: #82 |
|
3597 #89 := [trans #83 #87]: #88 |
|
3598 #79 := (iff #34 #78) |
|
3599 #80 := [monotonicity #77]: #79 |
|
3600 #92 := [monotonicity #80 #89 #77]: #91 |
|
3601 #111 := [monotonicity #92 #108]: #110 |
|
3602 #137 := [trans #111 #135]: #136 |
|
3603 #72 := [asserted]: #42 |
|
3604 #138 := [mp #72 #137]: #131 |
|
3605 decl uf_1 :: T1 |
|
3606 #4 := uf_1 |
|
3607 #43 := (uf_13 uf_1) |
|
3608 #44 := (uf_12 #43 uf_14) |
|
3609 #45 := (uf_11 #44 uf_15) |
|
3610 #149 := (* -1::real #45) |
|
3611 #150 := (+ #38 #149) |
|
3612 #140 := (+ #93 #45) |
|
3613 #161 := (<= #150 0::real) |
|
3614 #168 := (ite #161 #140 #150) |
|
3615 #176 := (* -1::real #168) |
|
3616 #177 := (+ #103 #176) |
|
3617 #178 := (+ #101 #177) |
|
3618 #179 := (<= #178 0::real) |
|
3619 #180 := (not #179) |
|
3620 #46 := (- #45 #38) |
|
3621 #48 := (- #46) |
|
3622 #47 := (< #46 0::real) |
|
3623 #49 := (ite #47 #48 #46) |
|
3624 #50 := (< #49 #41) |
|
3625 #185 := (iff #50 #180) |
|
3626 #143 := (< #140 0::real) |
|
3627 #155 := (ite #143 #150 #140) |
|
3628 #158 := (< #155 #104) |
|
3629 #183 := (iff #158 #180) |
|
3630 #173 := (< #168 #104) |
|
3631 #181 := (iff #173 #180) |
|
3632 #182 := [rewrite]: #181 |
|
3633 #174 := (iff #158 #173) |
|
3634 #171 := (= #155 #168) |
|
3635 #162 := (not #161) |
|
3636 #165 := (ite #162 #150 #140) |
|
3637 #169 := (= #165 #168) |
|
3638 #170 := [rewrite]: #169 |
|
3639 #166 := (= #155 #165) |
|
3640 #163 := (iff #143 #162) |
|
3641 #164 := [rewrite]: #163 |
|
3642 #167 := [monotonicity #164]: #166 |
|
3643 #172 := [trans #167 #170]: #171 |
|
3644 #175 := [monotonicity #172]: #174 |
|
3645 #184 := [trans #175 #182]: #183 |
|
3646 #159 := (iff #50 #158) |
|
3647 #156 := (= #49 #155) |
|
3648 #141 := (= #46 #140) |
|
3649 #142 := [rewrite]: #141 |
|
3650 #153 := (= #48 #150) |
|
3651 #146 := (- #140) |
|
3652 #151 := (= #146 #150) |
|
3653 #152 := [rewrite]: #151 |
|
3654 #147 := (= #48 #146) |
|
3655 #148 := [monotonicity #142]: #147 |
|
3656 #154 := [trans #148 #152]: #153 |
|
3657 #144 := (iff #47 #143) |
|
3658 #145 := [monotonicity #142]: #144 |
|
3659 #157 := [monotonicity #145 #154 #142]: #156 |
|
3660 #160 := [monotonicity #157 #108]: #159 |
|
3661 #186 := [trans #160 #184]: #185 |
|
3662 #139 := [asserted]: #50 |
|
3663 #187 := [mp #139 #186]: #180 |
|
3664 #299 := (+ #140 #176) |
|
3665 #300 := (<= #299 0::real) |
|
3666 #290 := (= #140 #168) |
|
3667 #329 := [hypothesis]: #162 |
|
3668 #191 := (+ #29 #149) |
|
3669 #192 := (<= #191 0::real) |
|
3670 #51 := (<= #29 #45) |
|
3671 #193 := (iff #51 #192) |
|
3672 #194 := [rewrite]: #193 |
|
3673 #188 := [asserted]: #51 |
|
3674 #195 := [mp #188 #194]: #192 |
|
3675 #298 := (+ #75 #127) |
|
3676 #301 := (<= #298 0::real) |
|
3677 #284 := (= #75 #119) |
|
3678 #302 := [hypothesis]: #113 |
|
3679 #296 := (+ #85 #127) |
|
3680 #297 := (<= #296 0::real) |
|
3681 #285 := (= #85 #119) |
|
3682 #288 := (or #112 #285) |
|
3683 #289 := [def-axiom]: #288 |
|
3684 #303 := [unit-resolution #289 #302]: #285 |
|
3685 #304 := (not #285) |
|
3686 #305 := (or #304 #297) |
|
3687 #306 := [th-lemma]: #305 |
|
3688 #307 := [unit-resolution #306 #303]: #297 |
|
3689 #315 := (not #290) |
|
3690 #310 := (not #300) |
|
3691 #311 := (or #310 #112) |
|
3692 #308 := [hypothesis]: #300 |
|
3693 #309 := [th-lemma #308 #307 #138 #302 #187 #195]: false |
|
3694 #312 := [lemma #309]: #311 |
|
3695 #322 := [unit-resolution #312 #302]: #310 |
|
3696 #316 := (or #315 #300) |
|
3697 #313 := [hypothesis]: #310 |
|
3698 #314 := [hypothesis]: #290 |
|
3699 #317 := [th-lemma]: #316 |
|
3700 #318 := [unit-resolution #317 #314 #313]: false |
|
3701 #319 := [lemma #318]: #316 |
|
3702 #323 := [unit-resolution #319 #322]: #315 |
|
3703 #292 := (or #162 #290) |
|
3704 #293 := [def-axiom]: #292 |
|
3705 #324 := [unit-resolution #293 #323]: #162 |
|
3706 #325 := [th-lemma #324 #307 #138 #302 #195]: false |
|
3707 #326 := [lemma #325]: #112 |
|
3708 #286 := (or #113 #284) |
|
3709 #287 := [def-axiom]: #286 |
|
3710 #330 := [unit-resolution #287 #326]: #284 |
|
3711 #331 := (not #284) |
|
3712 #332 := (or #331 #301) |
|
3713 #333 := [th-lemma]: #332 |
|
3714 #334 := [unit-resolution #333 #330]: #301 |
|
3715 #335 := [th-lemma #326 #334 #195 #329 #138]: false |
|
3716 #336 := [lemma #335]: #161 |
|
3717 #327 := [unit-resolution #293 #336]: #290 |
|
3718 #328 := [unit-resolution #319 #327]: #300 |
|
3719 [th-lemma #326 #334 #195 #328 #187 #138]: false |
|
3720 unsat |
|