37156
|
1 |
5ee060971856d2def7cc6d40549073dace7efe45 428 0
|
36900
|
2 |
#2 := false
|
|
3 |
decl f12 :: S2
|
|
4 |
#42 := f12
|
|
5 |
decl f5 :: S2
|
|
6 |
#25 := f5
|
|
7 |
#49 := (= f5 f12)
|
|
8 |
decl f3 :: (-> int S2)
|
|
9 |
decl f4 :: (-> S2 int)
|
|
10 |
#43 := (f4 f12)
|
|
11 |
#593 := (f3 #43)
|
|
12 |
#691 := (= #593 f12)
|
|
13 |
#594 := (= f12 #593)
|
|
14 |
#8 := (:var 0 S2)
|
|
15 |
#9 := (f4 #8)
|
|
16 |
#546 := (pattern #9)
|
|
17 |
#10 := (f3 #9)
|
|
18 |
#98 := (= #8 #10)
|
|
19 |
#547 := (forall (vars (?v0 S2)) (:pat #546) #98)
|
|
20 |
#101 := (forall (vars (?v0 S2)) #98)
|
|
21 |
#550 := (iff #101 #547)
|
|
22 |
#548 := (iff #98 #98)
|
|
23 |
#549 := [refl]: #548
|
|
24 |
#551 := [quant-intro #549]: #550
|
|
25 |
#461 := (~ #101 #101)
|
|
26 |
#463 := (~ #98 #98)
|
|
27 |
#464 := [refl]: #463
|
|
28 |
#462 := [nnf-pos #464]: #461
|
|
29 |
#11 := (= #10 #8)
|
|
30 |
#12 := (forall (vars (?v0 S2)) #11)
|
|
31 |
#102 := (iff #12 #101)
|
|
32 |
#99 := (iff #11 #98)
|
|
33 |
#100 := [rewrite]: #99
|
|
34 |
#103 := [quant-intro #100]: #102
|
|
35 |
#97 := [asserted]: #12
|
|
36 |
#106 := [mp #97 #103]: #101
|
|
37 |
#459 := [mp~ #106 #462]: #101
|
|
38 |
#552 := [mp #459 #551]: #547
|
|
39 |
#595 := (not #547)
|
|
40 |
#600 := (or #595 #594)
|
|
41 |
#601 := [quant-inst]: #600
|
|
42 |
#685 := [unit-resolution #601 #552]: #594
|
|
43 |
#692 := [symm #685]: #691
|
|
44 |
#693 := (= f5 #593)
|
|
45 |
#26 := (f4 f5)
|
|
46 |
#591 := (f3 #26)
|
|
47 |
#689 := (= #591 #593)
|
|
48 |
#687 := (= #593 #591)
|
|
49 |
#683 := (= #43 #26)
|
|
50 |
#681 := (= #26 #43)
|
|
51 |
#13 := 0::int
|
|
52 |
#232 := -1::int
|
|
53 |
#235 := (* -1::int #43)
|
|
54 |
#236 := (+ #26 #235)
|
|
55 |
#301 := (<= #236 0::int)
|
|
56 |
#74 := (<= #26 #43)
|
|
57 |
#398 := (iff #74 #301)
|
|
58 |
#399 := [rewrite]: #398
|
|
59 |
#352 := [asserted]: #74
|
|
60 |
#400 := [mp #352 #399]: #301
|
|
61 |
#234 := (>= #236 0::int)
|
|
62 |
decl f6 :: (-> S3 S4 real)
|
|
63 |
decl f8 :: (-> S2 S4)
|
|
64 |
#29 := (f8 f5)
|
|
65 |
decl f9 :: S3
|
|
66 |
#31 := f9
|
|
67 |
#32 := (f6 f9 #29)
|
|
68 |
decl f11 :: S3
|
|
69 |
#37 := f11
|
|
70 |
#38 := (f6 f11 #29)
|
|
71 |
#50 := (f8 f12)
|
|
72 |
decl f7 :: S3
|
|
73 |
#28 := f7
|
|
74 |
#51 := (f6 f7 #50)
|
|
75 |
#52 := (ite #49 #51 #38)
|
|
76 |
#261 := (ite #234 #52 #32)
|
|
77 |
#573 := (= #32 #261)
|
|
78 |
#653 := (not #573)
|
|
79 |
#199 := 0::real
|
|
80 |
#197 := -1::real
|
|
81 |
#270 := (* -1::real #261)
|
|
82 |
#645 := (+ #32 #270)
|
|
83 |
#647 := (>= #645 0::real)
|
|
84 |
#650 := (not #647)
|
|
85 |
#648 := [hypothesis]: #647
|
|
86 |
decl f10 :: S3
|
|
87 |
#34 := f10
|
|
88 |
#35 := (f6 f10 #29)
|
|
89 |
#271 := (+ #35 #270)
|
|
90 |
#269 := (>= #271 0::real)
|
|
91 |
#272 := (not #269)
|
|
92 |
#30 := (f6 f7 #29)
|
|
93 |
decl f13 :: S3
|
|
94 |
#45 := f13
|
|
95 |
#46 := (f6 f13 #29)
|
|
96 |
#242 := (ite #234 #46 #30)
|
|
97 |
#250 := (* -1::real #242)
|
|
98 |
#251 := (+ #35 #250)
|
|
99 |
#252 := (<= #251 0::real)
|
|
100 |
#253 := (not #252)
|
|
101 |
#277 := (and #253 #272)
|
|
102 |
#44 := (< #26 #43)
|
|
103 |
#53 := (ite #44 #32 #52)
|
|
104 |
#54 := (< #35 #53)
|
|
105 |
#47 := (ite #44 #30 #46)
|
|
106 |
#48 := (< #47 #35)
|
|
107 |
#55 := (and #48 #54)
|
|
108 |
#278 := (iff #55 #277)
|
|
109 |
#275 := (iff #54 #272)
|
|
110 |
#266 := (< #35 #261)
|
|
111 |
#273 := (iff #266 #272)
|
|
112 |
#274 := [rewrite]: #273
|
|
113 |
#267 := (iff #54 #266)
|
|
114 |
#264 := (= #53 #261)
|
|
115 |
#233 := (not #234)
|
|
116 |
#258 := (ite #233 #32 #52)
|
|
117 |
#262 := (= #258 #261)
|
|
118 |
#263 := [rewrite]: #262
|
|
119 |
#259 := (= #53 #258)
|
|
120 |
#237 := (iff #44 #233)
|
|
121 |
#238 := [rewrite]: #237
|
|
122 |
#260 := [monotonicity #238]: #259
|
|
123 |
#265 := [trans #260 #263]: #264
|
|
124 |
#268 := [monotonicity #265]: #267
|
|
125 |
#276 := [trans #268 #274]: #275
|
|
126 |
#256 := (iff #48 #253)
|
|
127 |
#247 := (< #242 #35)
|
|
128 |
#254 := (iff #247 #253)
|
|
129 |
#255 := [rewrite]: #254
|
|
130 |
#248 := (iff #48 #247)
|
|
131 |
#245 := (= #47 #242)
|
|
132 |
#239 := (ite #233 #30 #46)
|
|
133 |
#243 := (= #239 #242)
|
|
134 |
#244 := [rewrite]: #243
|
|
135 |
#240 := (= #47 #239)
|
|
136 |
#241 := [monotonicity #238]: #240
|
|
137 |
#246 := [trans #241 #244]: #245
|
|
138 |
#249 := [monotonicity #246]: #248
|
|
139 |
#257 := [trans #249 #255]: #256
|
|
140 |
#279 := [monotonicity #257 #276]: #278
|
|
141 |
#183 := [asserted]: #55
|
|
142 |
#280 := [mp #183 #279]: #277
|
|
143 |
#282 := [and-elim #280]: #272
|
|
144 |
#201 := (* -1::real #35)
|
|
145 |
#202 := (+ #32 #201)
|
|
146 |
#200 := (>= #202 0::real)
|
|
147 |
#198 := (not #200)
|
|
148 |
#218 := (* -1::real #38)
|
|
149 |
#219 := (+ #35 #218)
|
|
150 |
#217 := (>= #219 0::real)
|
|
151 |
#220 := (not #217)
|
|
152 |
#225 := (and #198 #220)
|
|
153 |
#27 := (< #26 #26)
|
|
154 |
#39 := (ite #27 #32 #38)
|
|
155 |
#40 := (< #35 #39)
|
|
156 |
#33 := (ite #27 #30 #32)
|
|
157 |
#36 := (< #33 #35)
|
|
158 |
#41 := (and #36 #40)
|
|
159 |
#226 := (iff #41 #225)
|
|
160 |
#223 := (iff #40 #220)
|
|
161 |
#214 := (< #35 #38)
|
|
162 |
#221 := (iff #214 #220)
|
|
163 |
#222 := [rewrite]: #221
|
|
164 |
#215 := (iff #40 #214)
|
|
165 |
#212 := (= #39 #38)
|
|
166 |
#207 := (ite false #32 #38)
|
|
167 |
#210 := (= #207 #38)
|
|
168 |
#211 := [rewrite]: #210
|
|
169 |
#208 := (= #39 #207)
|
|
170 |
#185 := (iff #27 false)
|
|
171 |
#186 := [rewrite]: #185
|
|
172 |
#209 := [monotonicity #186]: #208
|
|
173 |
#213 := [trans #209 #211]: #212
|
|
174 |
#216 := [monotonicity #213]: #215
|
|
175 |
#224 := [trans #216 #222]: #223
|
|
176 |
#205 := (iff #36 #198)
|
|
177 |
#194 := (< #32 #35)
|
|
178 |
#203 := (iff #194 #198)
|
|
179 |
#204 := [rewrite]: #203
|
|
180 |
#195 := (iff #36 #194)
|
|
181 |
#192 := (= #33 #32)
|
|
182 |
#187 := (ite false #30 #32)
|
|
183 |
#190 := (= #187 #32)
|
|
184 |
#191 := [rewrite]: #190
|
|
185 |
#188 := (= #33 #187)
|
|
186 |
#189 := [monotonicity #186]: #188
|
|
187 |
#193 := [trans #189 #191]: #192
|
|
188 |
#196 := [monotonicity #193]: #195
|
|
189 |
#206 := [trans #196 #204]: #205
|
|
190 |
#227 := [monotonicity #206 #224]: #226
|
|
191 |
#182 := [asserted]: #41
|
|
192 |
#228 := [mp #182 #227]: #225
|
|
193 |
#229 := [and-elim #228]: #198
|
|
194 |
#649 := [th-lemma #229 #282 #648]: false
|
|
195 |
#651 := [lemma #649]: #650
|
|
196 |
#652 := [hypothesis]: #573
|
|
197 |
#654 := (or #653 #647)
|
|
198 |
#655 := [th-lemma]: #654
|
|
199 |
#656 := [unit-resolution #655 #652 #651]: false
|
|
200 |
#657 := [lemma #656]: #653
|
|
201 |
#583 := (or #234 #573)
|
|
202 |
#584 := [def-axiom]: #583
|
|
203 |
#680 := [unit-resolution #584 #657]: #234
|
|
204 |
#682 := [th-lemma #680 #400]: #681
|
|
205 |
#684 := [symm #682]: #683
|
|
206 |
#688 := [monotonicity #684]: #687
|
|
207 |
#690 := [symm #688]: #689
|
|
208 |
#592 := (= f5 #591)
|
|
209 |
#596 := (or #595 #592)
|
|
210 |
#597 := [quant-inst]: #596
|
|
211 |
#686 := [unit-resolution #597 #552]: #592
|
|
212 |
#694 := [trans #686 #690]: #693
|
|
213 |
#695 := [trans #694 #692]: #49
|
|
214 |
#576 := (not #49)
|
|
215 |
#58 := (f6 f13 #50)
|
|
216 |
#284 := (ite #49 #32 #58)
|
|
217 |
#472 := (* -1::real #284)
|
|
218 |
#637 := (+ #32 #472)
|
|
219 |
#638 := (<= #637 0::real)
|
|
220 |
#585 := (= #32 #284)
|
|
221 |
#661 := [hypothesis]: #49
|
|
222 |
#587 := (or #576 #585)
|
|
223 |
#588 := [def-axiom]: #587
|
|
224 |
#662 := [unit-resolution #588 #661]: #585
|
|
225 |
#663 := (not #585)
|
|
226 |
#664 := (or #663 #638)
|
|
227 |
#665 := [th-lemma]: #664
|
|
228 |
#666 := [unit-resolution #665 #662]: #638
|
|
229 |
#61 := (f6 f10 #50)
|
|
230 |
#368 := (* -1::real #61)
|
|
231 |
#384 := (+ #51 #368)
|
|
232 |
#385 := (<= #384 0::real)
|
|
233 |
#386 := (not #385)
|
|
234 |
#369 := (+ #58 #368)
|
|
235 |
#367 := (>= #369 0::real)
|
|
236 |
#366 := (not #367)
|
|
237 |
#391 := (and #366 #386)
|
|
238 |
#63 := (f6 f9 #50)
|
|
239 |
#68 := (< #43 #43)
|
|
240 |
#71 := (ite #68 #63 #51)
|
|
241 |
#72 := (< #61 #71)
|
|
242 |
#69 := (ite #68 #51 #58)
|
|
243 |
#70 := (< #69 #61)
|
|
244 |
#73 := (and #70 #72)
|
|
245 |
#392 := (iff #73 #391)
|
|
246 |
#389 := (iff #72 #386)
|
|
247 |
#381 := (< #61 #51)
|
|
248 |
#387 := (iff #381 #386)
|
|
249 |
#388 := [rewrite]: #387
|
|
250 |
#382 := (iff #72 #381)
|
|
251 |
#379 := (= #71 #51)
|
|
252 |
#374 := (ite false #63 #51)
|
|
253 |
#377 := (= #374 #51)
|
|
254 |
#378 := [rewrite]: #377
|
|
255 |
#375 := (= #71 #374)
|
|
256 |
#354 := (iff #68 false)
|
|
257 |
#355 := [rewrite]: #354
|
|
258 |
#376 := [monotonicity #355]: #375
|
|
259 |
#380 := [trans #376 #378]: #379
|
|
260 |
#383 := [monotonicity #380]: #382
|
|
261 |
#390 := [trans #383 #388]: #389
|
|
262 |
#372 := (iff #70 #366)
|
|
263 |
#363 := (< #58 #61)
|
|
264 |
#370 := (iff #363 #366)
|
|
265 |
#371 := [rewrite]: #370
|
|
266 |
#364 := (iff #70 #363)
|
|
267 |
#361 := (= #69 #58)
|
|
268 |
#356 := (ite false #51 #58)
|
|
269 |
#359 := (= #356 #58)
|
|
270 |
#360 := [rewrite]: #359
|
|
271 |
#357 := (= #69 #356)
|
|
272 |
#358 := [monotonicity #355]: #357
|
|
273 |
#362 := [trans #358 #360]: #361
|
|
274 |
#365 := [monotonicity #362]: #364
|
|
275 |
#373 := [trans #365 #371]: #372
|
|
276 |
#393 := [monotonicity #373 #390]: #392
|
|
277 |
#351 := [asserted]: #73
|
|
278 |
#394 := [mp #351 #393]: #391
|
|
279 |
#396 := [and-elim #394]: #386
|
|
280 |
#402 := (* -1::real #63)
|
|
281 |
#403 := (+ #51 #402)
|
|
282 |
#404 := (<= #403 0::real)
|
|
283 |
#414 := (* -1::real #58)
|
|
284 |
#415 := (+ #51 #414)
|
|
285 |
#413 := (>= #415 0::real)
|
|
286 |
#64 := (f6 f11 #50)
|
|
287 |
#407 := (* -1::real #64)
|
|
288 |
#408 := (+ #63 #407)
|
|
289 |
#409 := (<= #408 0::real)
|
|
290 |
#423 := (and #404 #409 #413)
|
|
291 |
#77 := (<= #63 #64)
|
|
292 |
#76 := (<= #51 #63)
|
|
293 |
#78 := (and #76 #77)
|
|
294 |
#75 := (<= #58 #51)
|
|
295 |
#79 := (and #75 #78)
|
|
296 |
#426 := (iff #79 #423)
|
|
297 |
#417 := (and #404 #409)
|
|
298 |
#420 := (and #413 #417)
|
|
299 |
#424 := (iff #420 #423)
|
|
300 |
#425 := [rewrite]: #424
|
|
301 |
#421 := (iff #79 #420)
|
|
302 |
#418 := (iff #78 #417)
|
|
303 |
#410 := (iff #77 #409)
|
|
304 |
#411 := [rewrite]: #410
|
|
305 |
#405 := (iff #76 #404)
|
|
306 |
#406 := [rewrite]: #405
|
|
307 |
#419 := [monotonicity #406 #411]: #418
|
|
308 |
#412 := (iff #75 #413)
|
|
309 |
#416 := [rewrite]: #412
|
|
310 |
#422 := [monotonicity #416 #419]: #421
|
|
311 |
#427 := [trans #422 #425]: #426
|
|
312 |
#353 := [asserted]: #79
|
|
313 |
#428 := [mp #353 #427]: #423
|
|
314 |
#429 := [and-elim #428]: #404
|
|
315 |
#642 := (+ #32 #402)
|
|
316 |
#644 := (>= #642 0::real)
|
|
317 |
#641 := (= #32 #63)
|
|
318 |
#671 := (= #63 #32)
|
|
319 |
#669 := (= #50 #29)
|
|
320 |
#667 := (= #29 #50)
|
|
321 |
#668 := [monotonicity #661]: #667
|
|
322 |
#670 := [symm #668]: #669
|
|
323 |
#672 := [monotonicity #670]: #671
|
|
324 |
#673 := [symm #672]: #641
|
|
325 |
#674 := (not #641)
|
|
326 |
#675 := (or #674 #644)
|
|
327 |
#676 := [th-lemma]: #675
|
|
328 |
#677 := [unit-resolution #676 #673]: #644
|
|
329 |
#475 := (+ #61 #472)
|
|
330 |
#478 := (<= #475 0::real)
|
|
331 |
#451 := (not #478)
|
|
332 |
#327 := (ite #301 #284 #51)
|
|
333 |
#335 := (* -1::real #327)
|
|
334 |
#336 := (+ #61 #335)
|
|
335 |
#337 := (<= #336 0::real)
|
|
336 |
#338 := (not #337)
|
|
337 |
#452 := (iff #338 #451)
|
|
338 |
#479 := (iff #337 #478)
|
|
339 |
#476 := (= #336 #475)
|
|
340 |
#473 := (= #335 #472)
|
|
341 |
#470 := (= #327 #284)
|
|
342 |
#1 := true
|
|
343 |
#465 := (ite true #284 #51)
|
|
344 |
#468 := (= #465 #284)
|
|
345 |
#469 := [rewrite]: #468
|
|
346 |
#466 := (= #327 #465)
|
|
347 |
#457 := (iff #301 true)
|
|
348 |
#458 := [iff-true #400]: #457
|
|
349 |
#467 := [monotonicity #458]: #466
|
|
350 |
#471 := [trans #467 #469]: #470
|
|
351 |
#474 := [monotonicity #471]: #473
|
|
352 |
#477 := [monotonicity #474]: #476
|
|
353 |
#480 := [monotonicity #477]: #479
|
|
354 |
#481 := [monotonicity #480]: #452
|
|
355 |
#308 := (ite #301 #64 #63)
|
|
356 |
#318 := (* -1::real #308)
|
|
357 |
#319 := (+ #61 #318)
|
|
358 |
#317 := (>= #319 0::real)
|
|
359 |
#316 := (not #317)
|
|
360 |
#343 := (and #316 #338)
|
|
361 |
#56 := (< #43 #26)
|
|
362 |
#65 := (ite #56 #63 #64)
|
|
363 |
#66 := (< #61 #65)
|
|
364 |
#57 := (= f12 f5)
|
|
365 |
#59 := (ite #57 #32 #58)
|
|
366 |
#60 := (ite #56 #51 #59)
|
|
367 |
#62 := (< #60 #61)
|
|
368 |
#67 := (and #62 #66)
|
|
369 |
#346 := (iff #67 #343)
|
|
370 |
#287 := (ite #56 #51 #284)
|
|
371 |
#290 := (< #287 #61)
|
|
372 |
#296 := (and #66 #290)
|
|
373 |
#344 := (iff #296 #343)
|
|
374 |
#341 := (iff #290 #338)
|
|
375 |
#332 := (< #327 #61)
|
|
376 |
#339 := (iff #332 #338)
|
|
377 |
#340 := [rewrite]: #339
|
|
378 |
#333 := (iff #290 #332)
|
|
379 |
#330 := (= #287 #327)
|
|
380 |
#302 := (not #301)
|
|
381 |
#324 := (ite #302 #51 #284)
|
|
382 |
#328 := (= #324 #327)
|
|
383 |
#329 := [rewrite]: #328
|
|
384 |
#325 := (= #287 #324)
|
|
385 |
#303 := (iff #56 #302)
|
|
386 |
#304 := [rewrite]: #303
|
|
387 |
#326 := [monotonicity #304]: #325
|
|
388 |
#331 := [trans #326 #329]: #330
|
|
389 |
#334 := [monotonicity #331]: #333
|
|
390 |
#342 := [trans #334 #340]: #341
|
|
391 |
#322 := (iff #66 #316)
|
|
392 |
#313 := (< #61 #308)
|
|
393 |
#320 := (iff #313 #316)
|
|
394 |
#321 := [rewrite]: #320
|
|
395 |
#314 := (iff #66 #313)
|
|
396 |
#311 := (= #65 #308)
|
|
397 |
#305 := (ite #302 #63 #64)
|
|
398 |
#309 := (= #305 #308)
|
|
399 |
#310 := [rewrite]: #309
|
|
400 |
#306 := (= #65 #305)
|
|
401 |
#307 := [monotonicity #304]: #306
|
|
402 |
#312 := [trans #307 #310]: #311
|
|
403 |
#315 := [monotonicity #312]: #314
|
|
404 |
#323 := [trans #315 #321]: #322
|
|
405 |
#345 := [monotonicity #323 #342]: #344
|
|
406 |
#299 := (iff #67 #296)
|
|
407 |
#293 := (and #290 #66)
|
|
408 |
#297 := (iff #293 #296)
|
|
409 |
#298 := [rewrite]: #297
|
|
410 |
#294 := (iff #67 #293)
|
|
411 |
#291 := (iff #62 #290)
|
|
412 |
#288 := (= #60 #287)
|
|
413 |
#285 := (= #59 #284)
|
|
414 |
#231 := (iff #57 #49)
|
|
415 |
#283 := [rewrite]: #231
|
|
416 |
#286 := [monotonicity #283]: #285
|
|
417 |
#289 := [monotonicity #286]: #288
|
|
418 |
#292 := [monotonicity #289]: #291
|
|
419 |
#295 := [monotonicity #292]: #294
|
|
420 |
#300 := [trans #295 #298]: #299
|
|
421 |
#347 := [trans #300 #345]: #346
|
|
422 |
#184 := [asserted]: #67
|
|
423 |
#348 := [mp #184 #347]: #343
|
|
424 |
#350 := [and-elim #348]: #338
|
|
425 |
#482 := [mp #350 #481]: #451
|
|
426 |
#678 := [th-lemma #482 #677 #429 #396 #666]: false
|
|
427 |
#679 := [lemma #678]: #576
|
|
428 |
[unit-resolution #679 #695]: false
|
|
429 |
unsat
|
37156
|
430 |
6c73093b27236ef09bc4a53162dee78b6dc31895 422 0
|
36900
|
431 |
#2 := false
|
|
432 |
decl f12 :: S2
|
|
433 |
#42 := f12
|
|
434 |
decl f5 :: S2
|
|
435 |
#25 := f5
|
|
436 |
#45 := (= f5 f12)
|
|
437 |
decl f3 :: (-> int S2)
|
|
438 |
decl f4 :: (-> S2 int)
|
|
439 |
#43 := (f4 f12)
|
|
440 |
#598 := (f3 #43)
|
|
441 |
#696 := (= #598 f12)
|
|
442 |
#599 := (= f12 #598)
|
|
443 |
#8 := (:var 0 S2)
|
|
444 |
#9 := (f4 #8)
|
|
445 |
#551 := (pattern #9)
|
|
446 |
#10 := (f3 #9)
|
|
447 |
#98 := (= #8 #10)
|
|
448 |
#552 := (forall (vars (?v0 S2)) (:pat #551) #98)
|
|
449 |
#101 := (forall (vars (?v0 S2)) #98)
|
|
450 |
#555 := (iff #101 #552)
|
|
451 |
#553 := (iff #98 #98)
|
|
452 |
#554 := [refl]: #553
|
|
453 |
#556 := [quant-intro #554]: #555
|
|
454 |
#455 := (~ #101 #101)
|
|
455 |
#457 := (~ #98 #98)
|
|
456 |
#458 := [refl]: #457
|
|
457 |
#456 := [nnf-pos #458]: #455
|
|
458 |
#11 := (= #10 #8)
|
|
459 |
#12 := (forall (vars (?v0 S2)) #11)
|
|
460 |
#102 := (iff #12 #101)
|
|
461 |
#99 := (iff #11 #98)
|
|
462 |
#100 := [rewrite]: #99
|
|
463 |
#103 := [quant-intro #100]: #102
|
|
464 |
#97 := [asserted]: #12
|
|
465 |
#106 := [mp #97 #103]: #101
|
|
466 |
#453 := [mp~ #106 #456]: #101
|
|
467 |
#557 := [mp #453 #556]: #552
|
|
468 |
#600 := (not #552)
|
|
469 |
#605 := (or #600 #599)
|
|
470 |
#606 := [quant-inst]: #605
|
|
471 |
#690 := [unit-resolution #606 #557]: #599
|
|
472 |
#697 := [symm #690]: #696
|
|
473 |
#698 := (= f5 #598)
|
|
474 |
#26 := (f4 f5)
|
|
475 |
#596 := (f3 #26)
|
|
476 |
#694 := (= #596 #598)
|
|
477 |
#692 := (= #598 #596)
|
|
478 |
#688 := (= #43 #26)
|
|
479 |
#686 := (= #26 #43)
|
|
480 |
#13 := 0::int
|
|
481 |
#231 := -1::int
|
|
482 |
#234 := (* -1::int #43)
|
|
483 |
#235 := (+ #26 #234)
|
|
484 |
#295 := (<= #235 0::int)
|
|
485 |
#74 := (<= #26 #43)
|
|
486 |
#393 := (iff #74 #295)
|
|
487 |
#394 := [rewrite]: #393
|
|
488 |
#346 := [asserted]: #74
|
|
489 |
#395 := [mp #346 #394]: #295
|
|
490 |
#233 := (>= #235 0::int)
|
|
491 |
decl f6 :: (-> S3 S4 real)
|
|
492 |
decl f8 :: (-> S2 S4)
|
|
493 |
#29 := (f8 f5)
|
|
494 |
decl f7 :: S3
|
|
495 |
#28 := f7
|
|
496 |
#30 := (f6 f7 #29)
|
|
497 |
decl f9 :: S3
|
|
498 |
#31 := f9
|
|
499 |
#32 := (f6 f9 #29)
|
|
500 |
#46 := (f8 f12)
|
|
501 |
decl f11 :: S3
|
|
502 |
#37 := f11
|
|
503 |
#47 := (f6 f11 #46)
|
|
504 |
#48 := (ite #45 #47 #32)
|
|
505 |
#241 := (ite #233 #48 #30)
|
|
506 |
#572 := (= #30 #241)
|
|
507 |
#658 := (not #572)
|
|
508 |
#199 := 0::real
|
|
509 |
#197 := -1::real
|
|
510 |
#249 := (* -1::real #241)
|
|
511 |
#647 := (+ #30 #249)
|
|
512 |
#648 := (<= #647 0::real)
|
|
513 |
#652 := (not #648)
|
|
514 |
#650 := [hypothesis]: #648
|
|
515 |
decl f10 :: S3
|
|
516 |
#34 := f10
|
|
517 |
#35 := (f6 f10 #29)
|
|
518 |
#250 := (+ #35 #249)
|
|
519 |
#251 := (<= #250 0::real)
|
|
520 |
#252 := (not #251)
|
|
521 |
#38 := (f6 f11 #29)
|
|
522 |
decl f13 :: S3
|
|
523 |
#51 := f13
|
|
524 |
#52 := (f6 f13 #29)
|
|
525 |
#260 := (ite #233 #52 #38)
|
|
526 |
#269 := (* -1::real #260)
|
|
527 |
#270 := (+ #35 #269)
|
|
528 |
#268 := (>= #270 0::real)
|
|
529 |
#271 := (not #268)
|
|
530 |
#276 := (and #252 #271)
|
|
531 |
#44 := (< #26 #43)
|
|
532 |
#53 := (ite #44 #38 #52)
|
|
533 |
#54 := (< #35 #53)
|
|
534 |
#49 := (ite #44 #30 #48)
|
|
535 |
#50 := (< #49 #35)
|
|
536 |
#55 := (and #50 #54)
|
|
537 |
#277 := (iff #55 #276)
|
|
538 |
#274 := (iff #54 #271)
|
|
539 |
#265 := (< #35 #260)
|
|
540 |
#272 := (iff #265 #271)
|
|
541 |
#273 := [rewrite]: #272
|
|
542 |
#266 := (iff #54 #265)
|
|
543 |
#263 := (= #53 #260)
|
|
544 |
#232 := (not #233)
|
|
545 |
#257 := (ite #232 #38 #52)
|
|
546 |
#261 := (= #257 #260)
|
|
547 |
#262 := [rewrite]: #261
|
|
548 |
#258 := (= #53 #257)
|
|
549 |
#236 := (iff #44 #232)
|
|
550 |
#237 := [rewrite]: #236
|
|
551 |
#259 := [monotonicity #237]: #258
|
|
552 |
#264 := [trans #259 #262]: #263
|
|
553 |
#267 := [monotonicity #264]: #266
|
|
554 |
#275 := [trans #267 #273]: #274
|
|
555 |
#255 := (iff #50 #252)
|
|
556 |
#246 := (< #241 #35)
|
|
557 |
#253 := (iff #246 #252)
|
|
558 |
#254 := [rewrite]: #253
|
|
559 |
#247 := (iff #50 #246)
|
|
560 |
#244 := (= #49 #241)
|
|
561 |
#238 := (ite #232 #30 #48)
|
|
562 |
#242 := (= #238 #241)
|
|
563 |
#243 := [rewrite]: #242
|
|
564 |
#239 := (= #49 #238)
|
|
565 |
#240 := [monotonicity #237]: #239
|
|
566 |
#245 := [trans #240 #243]: #244
|
|
567 |
#248 := [monotonicity #245]: #247
|
|
568 |
#256 := [trans #248 #254]: #255
|
|
569 |
#278 := [monotonicity #256 #275]: #277
|
|
570 |
#183 := [asserted]: #55
|
|
571 |
#279 := [mp #183 #278]: #276
|
|
572 |
#280 := [and-elim #279]: #252
|
|
573 |
#201 := (* -1::real #35)
|
|
574 |
#217 := (+ #30 #201)
|
|
575 |
#218 := (<= #217 0::real)
|
|
576 |
#219 := (not #218)
|
|
577 |
#202 := (+ #32 #201)
|
|
578 |
#200 := (>= #202 0::real)
|
|
579 |
#198 := (not #200)
|
|
580 |
#224 := (and #198 #219)
|
|
581 |
#27 := (< #26 #26)
|
|
582 |
#39 := (ite #27 #38 #30)
|
|
583 |
#40 := (< #35 #39)
|
|
584 |
#33 := (ite #27 #30 #32)
|
|
585 |
#36 := (< #33 #35)
|
|
586 |
#41 := (and #36 #40)
|
|
587 |
#225 := (iff #41 #224)
|
|
588 |
#222 := (iff #40 #219)
|
|
589 |
#214 := (< #35 #30)
|
|
590 |
#220 := (iff #214 #219)
|
|
591 |
#221 := [rewrite]: #220
|
|
592 |
#215 := (iff #40 #214)
|
|
593 |
#212 := (= #39 #30)
|
|
594 |
#207 := (ite false #38 #30)
|
|
595 |
#210 := (= #207 #30)
|
|
596 |
#211 := [rewrite]: #210
|
|
597 |
#208 := (= #39 #207)
|
|
598 |
#185 := (iff #27 false)
|
|
599 |
#186 := [rewrite]: #185
|
|
600 |
#209 := [monotonicity #186]: #208
|
|
601 |
#213 := [trans #209 #211]: #212
|
|
602 |
#216 := [monotonicity #213]: #215
|
|
603 |
#223 := [trans #216 #221]: #222
|
|
604 |
#205 := (iff #36 #198)
|
|
605 |
#194 := (< #32 #35)
|
|
606 |
#203 := (iff #194 #198)
|
|
607 |
#204 := [rewrite]: #203
|
|
608 |
#195 := (iff #36 #194)
|
|
609 |
#192 := (= #33 #32)
|
|
610 |
#187 := (ite false #30 #32)
|
|
611 |
#190 := (= #187 #32)
|
|
612 |
#191 := [rewrite]: #190
|
|
613 |
#188 := (= #33 #187)
|
|
614 |
#189 := [monotonicity #186]: #188
|
|
615 |
#193 := [trans #189 #191]: #192
|
|
616 |
#196 := [monotonicity #193]: #195
|
|
617 |
#206 := [trans #196 #204]: #205
|
|
618 |
#226 := [monotonicity #206 #223]: #225
|
|
619 |
#182 := [asserted]: #41
|
|
620 |
#227 := [mp #182 #226]: #224
|
|
621 |
#229 := [and-elim #227]: #219
|
|
622 |
#651 := [th-lemma #229 #280 #650]: false
|
|
623 |
#653 := [lemma #651]: #652
|
|
624 |
#657 := [hypothesis]: #572
|
|
625 |
#659 := (or #658 #648)
|
|
626 |
#660 := [th-lemma]: #659
|
|
627 |
#661 := [unit-resolution #660 #657 #653]: false
|
|
628 |
#662 := [lemma #661]: #658
|
|
629 |
#582 := (or #233 #572)
|
|
630 |
#583 := [def-axiom]: #582
|
|
631 |
#685 := [unit-resolution #583 #662]: #233
|
|
632 |
#687 := [th-lemma #685 #395]: #686
|
|
633 |
#689 := [symm #687]: #688
|
|
634 |
#693 := [monotonicity #689]: #692
|
|
635 |
#695 := [symm #693]: #694
|
|
636 |
#597 := (= f5 #596)
|
|
637 |
#601 := (or #600 #597)
|
|
638 |
#602 := [quant-inst]: #601
|
|
639 |
#691 := [unit-resolution #602 #557]: #597
|
|
640 |
#699 := [trans #691 #695]: #698
|
|
641 |
#700 := [trans #699 #697]: #45
|
|
642 |
#575 := (not #45)
|
|
643 |
#63 := (f6 f13 #46)
|
|
644 |
#283 := (ite #45 #30 #63)
|
|
645 |
#466 := (* -1::real #283)
|
|
646 |
#642 := (+ #30 #466)
|
|
647 |
#644 := (>= #642 0::real)
|
|
648 |
#590 := (= #30 #283)
|
|
649 |
#666 := [hypothesis]: #45
|
|
650 |
#592 := (or #575 #590)
|
|
651 |
#593 := [def-axiom]: #592
|
|
652 |
#667 := [unit-resolution #593 #666]: #590
|
|
653 |
#668 := (not #590)
|
|
654 |
#669 := (or #668 #644)
|
|
655 |
#670 := [th-lemma]: #669
|
|
656 |
#671 := [unit-resolution #670 #667]: #644
|
|
657 |
#60 := (f6 f10 #46)
|
|
658 |
#362 := (* -1::real #60)
|
|
659 |
#363 := (+ #47 #362)
|
|
660 |
#361 := (>= #363 0::real)
|
|
661 |
#360 := (not #361)
|
|
662 |
#379 := (* -1::real #63)
|
|
663 |
#380 := (+ #60 #379)
|
|
664 |
#378 := (>= #380 0::real)
|
|
665 |
#381 := (not #378)
|
|
666 |
#386 := (and #360 #381)
|
|
667 |
#68 := (< #43 #43)
|
|
668 |
#71 := (ite #68 #47 #63)
|
|
669 |
#72 := (< #60 #71)
|
|
670 |
#57 := (f6 f7 #46)
|
|
671 |
#69 := (ite #68 #57 #47)
|
|
672 |
#70 := (< #69 #60)
|
|
673 |
#73 := (and #70 #72)
|
|
674 |
#387 := (iff #73 #386)
|
|
675 |
#384 := (iff #72 #381)
|
|
676 |
#375 := (< #60 #63)
|
|
677 |
#382 := (iff #375 #381)
|
|
678 |
#383 := [rewrite]: #382
|
|
679 |
#376 := (iff #72 #375)
|
|
680 |
#373 := (= #71 #63)
|
|
681 |
#368 := (ite false #47 #63)
|
|
682 |
#371 := (= #368 #63)
|
|
683 |
#372 := [rewrite]: #371
|
|
684 |
#369 := (= #71 #368)
|
|
685 |
#348 := (iff #68 false)
|
|
686 |
#349 := [rewrite]: #348
|
|
687 |
#370 := [monotonicity #349]: #369
|
|
688 |
#374 := [trans #370 #372]: #373
|
|
689 |
#377 := [monotonicity #374]: #376
|
|
690 |
#385 := [trans #377 #383]: #384
|
|
691 |
#366 := (iff #70 #360)
|
|
692 |
#357 := (< #47 #60)
|
|
693 |
#364 := (iff #357 #360)
|
|
694 |
#365 := [rewrite]: #364
|
|
695 |
#358 := (iff #70 #357)
|
|
696 |
#355 := (= #69 #47)
|
|
697 |
#350 := (ite false #57 #47)
|
|
698 |
#353 := (= #350 #47)
|
|
699 |
#354 := [rewrite]: #353
|
|
700 |
#351 := (= #69 #350)
|
|
701 |
#352 := [monotonicity #349]: #351
|
|
702 |
#356 := [trans #352 #354]: #355
|
|
703 |
#359 := [monotonicity #356]: #358
|
|
704 |
#367 := [trans #359 #365]: #366
|
|
705 |
#388 := [monotonicity #367 #385]: #387
|
|
706 |
#345 := [asserted]: #73
|
|
707 |
#389 := [mp #345 #388]: #386
|
|
708 |
#390 := [and-elim #389]: #360
|
|
709 |
#399 := (* -1::real #57)
|
|
710 |
#400 := (+ #47 #399)
|
|
711 |
#398 := (>= #400 0::real)
|
|
712 |
#58 := (f6 f9 #46)
|
|
713 |
#407 := (* -1::real #58)
|
|
714 |
#408 := (+ #57 #407)
|
|
715 |
#406 := (>= #408 0::real)
|
|
716 |
#402 := (+ #47 #379)
|
|
717 |
#403 := (<= #402 0::real)
|
|
718 |
#417 := (and #398 #403 #406)
|
|
719 |
#77 := (<= #47 #63)
|
|
720 |
#76 := (<= #57 #47)
|
|
721 |
#78 := (and #76 #77)
|
|
722 |
#75 := (<= #58 #57)
|
|
723 |
#79 := (and #75 #78)
|
|
724 |
#420 := (iff #79 #417)
|
|
725 |
#411 := (and #398 #403)
|
|
726 |
#414 := (and #406 #411)
|
|
727 |
#418 := (iff #414 #417)
|
|
728 |
#419 := [rewrite]: #418
|
|
729 |
#415 := (iff #79 #414)
|
|
730 |
#412 := (iff #78 #411)
|
|
731 |
#404 := (iff #77 #403)
|
|
732 |
#405 := [rewrite]: #404
|
|
733 |
#397 := (iff #76 #398)
|
|
734 |
#401 := [rewrite]: #397
|
|
735 |
#413 := [monotonicity #401 #405]: #412
|
|
736 |
#409 := (iff #75 #406)
|
|
737 |
#410 := [rewrite]: #409
|
|
738 |
#416 := [monotonicity #410 #413]: #415
|
|
739 |
#421 := [trans #416 #419]: #420
|
|
740 |
#347 := [asserted]: #79
|
|
741 |
#422 := [mp #347 #421]: #417
|
|
742 |
#423 := [and-elim #422]: #398
|
|
743 |
#655 := (+ #30 #399)
|
|
744 |
#656 := (<= #655 0::real)
|
|
745 |
#654 := (= #30 #57)
|
|
746 |
#676 := (= #57 #30)
|
|
747 |
#674 := (= #46 #29)
|
|
748 |
#672 := (= #29 #46)
|
|
749 |
#673 := [monotonicity #666]: #672
|
|
750 |
#675 := [symm #673]: #674
|
|
751 |
#677 := [monotonicity #675]: #676
|
|
752 |
#678 := [symm #677]: #654
|
|
753 |
#679 := (not #654)
|
|
754 |
#680 := (or #679 #656)
|
|
755 |
#681 := [th-lemma]: #680
|
|
756 |
#682 := [unit-resolution #681 #678]: #656
|
|
757 |
#469 := (+ #60 #466)
|
|
758 |
#472 := (>= #469 0::real)
|
|
759 |
#445 := (not #472)
|
|
760 |
#321 := (ite #295 #283 #47)
|
|
761 |
#331 := (* -1::real #321)
|
|
762 |
#332 := (+ #60 #331)
|
|
763 |
#330 := (>= #332 0::real)
|
|
764 |
#329 := (not #330)
|
|
765 |
#446 := (iff #329 #445)
|
|
766 |
#473 := (iff #330 #472)
|
|
767 |
#470 := (= #332 #469)
|
|
768 |
#467 := (= #331 #466)
|
|
769 |
#464 := (= #321 #283)
|
|
770 |
#1 := true
|
|
771 |
#459 := (ite true #283 #47)
|
|
772 |
#462 := (= #459 #283)
|
|
773 |
#463 := [rewrite]: #462
|
|
774 |
#460 := (= #321 #459)
|
|
775 |
#451 := (iff #295 true)
|
|
776 |
#452 := [iff-true #395]: #451
|
|
777 |
#461 := [monotonicity #452]: #460
|
|
778 |
#465 := [trans #461 #463]: #464
|
|
779 |
#468 := [monotonicity #465]: #467
|
|
780 |
#471 := [monotonicity #468]: #470
|
|
781 |
#474 := [monotonicity #471]: #473
|
|
782 |
#475 := [monotonicity #474]: #446
|
|
783 |
#302 := (ite #295 #58 #57)
|
|
784 |
#310 := (* -1::real #302)
|
|
785 |
#311 := (+ #60 #310)
|
|
786 |
#312 := (<= #311 0::real)
|
|
787 |
#313 := (not #312)
|
|
788 |
#337 := (and #313 #329)
|
|
789 |
#62 := (= f12 f5)
|
|
790 |
#64 := (ite #62 #30 #63)
|
|
791 |
#56 := (< #43 #26)
|
|
792 |
#65 := (ite #56 #47 #64)
|
|
793 |
#66 := (< #60 #65)
|
|
794 |
#59 := (ite #56 #57 #58)
|
|
795 |
#61 := (< #59 #60)
|
|
796 |
#67 := (and #61 #66)
|
|
797 |
#340 := (iff #67 #337)
|
|
798 |
#286 := (ite #56 #47 #283)
|
|
799 |
#289 := (< #60 #286)
|
|
800 |
#292 := (and #61 #289)
|
|
801 |
#338 := (iff #292 #337)
|
|
802 |
#335 := (iff #289 #329)
|
|
803 |
#326 := (< #60 #321)
|
|
804 |
#333 := (iff #326 #329)
|
|
805 |
#334 := [rewrite]: #333
|
|
806 |
#327 := (iff #289 #326)
|
|
807 |
#324 := (= #286 #321)
|
|
808 |
#296 := (not #295)
|
|
809 |
#318 := (ite #296 #47 #283)
|
|
810 |
#322 := (= #318 #321)
|
|
811 |
#323 := [rewrite]: #322
|
|
812 |
#319 := (= #286 #318)
|
|
813 |
#297 := (iff #56 #296)
|
|
814 |
#298 := [rewrite]: #297
|
|
815 |
#320 := [monotonicity #298]: #319
|
|
816 |
#325 := [trans #320 #323]: #324
|
|
817 |
#328 := [monotonicity #325]: #327
|
|
818 |
#336 := [trans #328 #334]: #335
|
|
819 |
#316 := (iff #61 #313)
|
|
820 |
#307 := (< #302 #60)
|
|
821 |
#314 := (iff #307 #313)
|
|
822 |
#315 := [rewrite]: #314
|
|
823 |
#308 := (iff #61 #307)
|
|
824 |
#305 := (= #59 #302)
|
|
825 |
#299 := (ite #296 #57 #58)
|
|
826 |
#303 := (= #299 #302)
|
|
827 |
#304 := [rewrite]: #303
|
|
828 |
#300 := (= #59 #299)
|
|
829 |
#301 := [monotonicity #298]: #300
|
|
830 |
#306 := [trans #301 #304]: #305
|
|
831 |
#309 := [monotonicity #306]: #308
|
|
832 |
#317 := [trans #309 #315]: #316
|
|
833 |
#339 := [monotonicity #317 #336]: #338
|
|
834 |
#293 := (iff #67 #292)
|
|
835 |
#290 := (iff #66 #289)
|
|
836 |
#287 := (= #65 #286)
|
|
837 |
#284 := (= #64 #283)
|
|
838 |
#230 := (iff #62 #45)
|
|
839 |
#282 := [rewrite]: #230
|
|
840 |
#285 := [monotonicity #282]: #284
|
|
841 |
#288 := [monotonicity #285]: #287
|
|
842 |
#291 := [monotonicity #288]: #290
|
|
843 |
#294 := [monotonicity #291]: #293
|
|
844 |
#341 := [trans #294 #339]: #340
|
|
845 |
#184 := [asserted]: #67
|
|
846 |
#342 := [mp #184 #341]: #337
|
|
847 |
#344 := [and-elim #342]: #329
|
|
848 |
#476 := [mp #344 #475]: #445
|
|
849 |
#683 := [th-lemma #476 #682 #423 #390 #671]: false
|
|
850 |
#684 := [lemma #683]: #575
|
|
851 |
[unit-resolution #684 #700]: false
|
|
852 |
unsat
|
37156
|
853 |
c220892677421b557c184d2f3de28c1bae1b8341 921 0
|
36900
|
854 |
#2 := false
|
|
855 |
#58 := 0::int
|
|
856 |
decl f5 :: (-> S4 int)
|
|
857 |
decl f6 :: (-> S2 S4)
|
|
858 |
decl f11 :: (-> S4 S2)
|
|
859 |
decl f14 :: S4
|
|
860 |
#30 := f14
|
|
861 |
#34 := (f11 f14)
|
|
862 |
#70 := (f6 #34)
|
|
863 |
#605 := (f5 #70)
|
|
864 |
#121 := -1::int
|
|
865 |
#615 := (* -1::int #605)
|
|
866 |
decl f7 :: S4
|
|
867 |
#13 := f7
|
|
868 |
#14 := (f5 f7)
|
|
869 |
#662 := (+ #14 #615)
|
|
870 |
#663 := (<= #662 0::int)
|
|
871 |
decl f8 :: (-> S5 S2 real)
|
|
872 |
decl f19 :: (-> S3 S5)
|
|
873 |
decl f15 :: S3
|
|
874 |
#40 := f15
|
|
875 |
#86 := (f19 f15)
|
|
876 |
#650 := (f8 #86 #34)
|
|
877 |
decl f10 :: S5
|
|
878 |
#19 := f10
|
|
879 |
#35 := (f8 f10 #34)
|
|
880 |
#651 := (= #35 #650)
|
|
881 |
#690 := (not #651)
|
|
882 |
decl f13 :: S3
|
|
883 |
#28 := f13
|
|
884 |
#81 := (f19 f13)
|
|
885 |
#749 := (f8 #81 #34)
|
|
886 |
#1233 := (= #650 #749)
|
|
887 |
#1246 := (not #1233)
|
|
888 |
#1335 := (iff #1246 #690)
|
|
889 |
#1333 := (iff #1233 #651)
|
|
890 |
#1328 := (= #650 #35)
|
|
891 |
#1331 := (iff #1328 #651)
|
|
892 |
#1332 := [commutativity]: #1331
|
|
893 |
#1329 := (iff #1233 #1328)
|
|
894 |
#1326 := (= #749 #35)
|
|
895 |
#752 := (= #35 #749)
|
|
896 |
decl f12 :: S5
|
|
897 |
#22 := f12
|
|
898 |
#696 := (f8 f12 #34)
|
|
899 |
#751 := (= #696 #749)
|
|
900 |
#281 := (= f14 #70)
|
|
901 |
#755 := (ite #281 #752 #751)
|
|
902 |
decl f9 :: S5
|
|
903 |
#16 := f9
|
|
904 |
#694 := (f8 f9 #34)
|
|
905 |
#750 := (= #694 #749)
|
|
906 |
#31 := (f5 f14)
|
|
907 |
#616 := (+ #31 #615)
|
|
908 |
#617 := (<= #616 0::int)
|
|
909 |
#758 := (ite #617 #755 #750)
|
|
910 |
#9 := (:var 0 S2)
|
|
911 |
#17 := (f8 f9 #9)
|
|
912 |
#538 := (pattern #17)
|
|
913 |
#23 := (f8 f12 #9)
|
|
914 |
#537 := (pattern #23)
|
|
915 |
#82 := (f8 #81 #9)
|
|
916 |
#545 := (pattern #82)
|
|
917 |
#11 := (f6 #9)
|
|
918 |
#535 := (pattern #11)
|
|
919 |
#452 := (= #17 #82)
|
|
920 |
#450 := (= #23 #82)
|
|
921 |
#449 := (= #35 #82)
|
|
922 |
#33 := (= #11 f14)
|
|
923 |
#451 := (ite #33 #449 #450)
|
|
924 |
#146 := (* -1::int #31)
|
|
925 |
#12 := (f5 #11)
|
|
926 |
#147 := (+ #12 #146)
|
|
927 |
#145 := (>= #147 0::int)
|
|
928 |
#453 := (ite #145 #451 #452)
|
|
929 |
#546 := (forall (vars (?v0 S2)) (:pat #535 #545 #537 #538) #453)
|
|
930 |
#456 := (forall (vars (?v0 S2)) #453)
|
|
931 |
#549 := (iff #456 #546)
|
|
932 |
#547 := (iff #453 #453)
|
|
933 |
#548 := [refl]: #547
|
|
934 |
#550 := [quant-intro #548]: #549
|
|
935 |
#36 := (ite #33 #35 #23)
|
|
936 |
#153 := (ite #145 #36 #17)
|
|
937 |
#380 := (= #82 #153)
|
|
938 |
#381 := (forall (vars (?v0 S2)) #380)
|
|
939 |
#457 := (iff #381 #456)
|
|
940 |
#454 := (iff #380 #453)
|
|
941 |
#455 := [rewrite]: #454
|
|
942 |
#458 := [quant-intro #455]: #457
|
|
943 |
#366 := (~ #381 #381)
|
|
944 |
#368 := (~ #380 #380)
|
|
945 |
#365 := [refl]: #368
|
|
946 |
#363 := [nnf-pos #365]: #366
|
|
947 |
decl f3 :: (-> S3 S2 real)
|
|
948 |
#29 := (f3 f13 #9)
|
|
949 |
#158 := (= #29 #153)
|
|
950 |
#161 := (forall (vars (?v0 S2)) #158)
|
|
951 |
#382 := (iff #161 #381)
|
|
952 |
#96 := (:var 1 S3)
|
|
953 |
#99 := (f3 #96 #9)
|
|
954 |
#97 := (f19 #96)
|
|
955 |
#98 := (f8 #97 #9)
|
|
956 |
#100 := (= #98 #99)
|
|
957 |
#101 := (forall (vars (?v0 S3) (?v1 S2)) #100)
|
|
958 |
#298 := [asserted]: #101
|
|
959 |
#383 := [rewrite* #298]: #382
|
|
960 |
#32 := (< #12 #31)
|
|
961 |
#37 := (ite #32 #17 #36)
|
|
962 |
#38 := (= #29 #37)
|
|
963 |
#39 := (forall (vars (?v0 S2)) #38)
|
|
964 |
#162 := (iff #39 #161)
|
|
965 |
#159 := (iff #38 #158)
|
|
966 |
#156 := (= #37 #153)
|
|
967 |
#144 := (not #145)
|
|
968 |
#150 := (ite #144 #17 #36)
|
|
969 |
#154 := (= #150 #153)
|
|
970 |
#155 := [rewrite]: #154
|
|
971 |
#151 := (= #37 #150)
|
|
972 |
#148 := (iff #32 #144)
|
|
973 |
#149 := [rewrite]: #148
|
|
974 |
#152 := [monotonicity #149]: #151
|
|
975 |
#157 := [trans #152 #155]: #156
|
|
976 |
#160 := [monotonicity #157]: #159
|
|
977 |
#163 := [quant-intro #160]: #162
|
|
978 |
#119 := [asserted]: #39
|
|
979 |
#164 := [mp #119 #163]: #161
|
|
980 |
#384 := [mp #164 #383]: #381
|
|
981 |
#364 := [mp~ #384 #363]: #381
|
|
982 |
#459 := [mp #364 #458]: #456
|
|
983 |
#551 := [mp #459 #550]: #546
|
|
984 |
#761 := (not #546)
|
|
985 |
#762 := (or #761 #758)
|
|
986 |
#71 := (= #70 f14)
|
|
987 |
#753 := (ite #71 #752 #751)
|
|
988 |
#606 := (+ #605 #146)
|
|
989 |
#607 := (>= #606 0::int)
|
|
990 |
#754 := (ite #607 #753 #750)
|
|
991 |
#763 := (or #761 #754)
|
|
992 |
#765 := (iff #763 #762)
|
|
993 |
#767 := (iff #762 #762)
|
|
994 |
#768 := [rewrite]: #767
|
|
995 |
#759 := (iff #754 #758)
|
|
996 |
#756 := (iff #753 #755)
|
|
997 |
#282 := (iff #71 #281)
|
|
998 |
#283 := [rewrite]: #282
|
|
999 |
#757 := [monotonicity #283]: #756
|
|
1000 |
#620 := (iff #607 #617)
|
|
1001 |
#609 := (+ #146 #605)
|
|
1002 |
#612 := (>= #609 0::int)
|
|
1003 |
#618 := (iff #612 #617)
|
|
1004 |
#619 := [rewrite]: #618
|
|
1005 |
#613 := (iff #607 #612)
|
|
1006 |
#610 := (= #606 #609)
|
|
1007 |
#611 := [rewrite]: #610
|
|
1008 |
#614 := [monotonicity #611]: #613
|
|
1009 |
#621 := [trans #614 #619]: #620
|
|
1010 |
#760 := [monotonicity #621 #757]: #759
|
|
1011 |
#766 := [monotonicity #760]: #765
|
|
1012 |
#769 := [trans #766 #768]: #765
|
|
1013 |
#764 := [quant-inst]: #763
|
|
1014 |
#770 := [mp #764 #769]: #762
|
|
1015 |
#1317 := [unit-resolution #770 #551]: #758
|
|
1016 |
#981 := (= #31 #605)
|
|
1017 |
#1295 := (= #605 #31)
|
|
1018 |
#280 := [asserted]: #71
|
|
1019 |
#286 := [mp #280 #283]: #281
|
|
1020 |
#1290 := [symm #286]: #71
|
|
1021 |
#1296 := [monotonicity #1290]: #1295
|
|
1022 |
#1297 := [symm #1296]: #981
|
|
1023 |
#1318 := (not #981)
|
|
1024 |
#1319 := (or #1318 #617)
|
|
1025 |
#1320 := [th-lemma]: #1319
|
|
1026 |
#1321 := [unit-resolution #1320 #1297]: #617
|
|
1027 |
#639 := (not #617)
|
|
1028 |
#783 := (not #758)
|
|
1029 |
#784 := (or #783 #639 #755)
|
|
1030 |
#785 := [def-axiom]: #784
|
|
1031 |
#1322 := [unit-resolution #785 #1321 #1317]: #755
|
|
1032 |
#771 := (not #755)
|
|
1033 |
#1323 := (or #771 #752)
|
|
1034 |
#772 := (not #281)
|
|
1035 |
#773 := (or #771 #772 #752)
|
|
1036 |
#774 := [def-axiom]: #773
|
|
1037 |
#1324 := [unit-resolution #774 #286]: #1323
|
|
1038 |
#1325 := [unit-resolution #1324 #1322]: #752
|
|
1039 |
#1327 := [symm #1325]: #1326
|
|
1040 |
#1330 := [monotonicity #1327]: #1329
|
|
1041 |
#1334 := [trans #1330 #1332]: #1333
|
|
1042 |
#1336 := [monotonicity #1334]: #1335
|
|
1043 |
#303 := 0::real
|
|
1044 |
#301 := -1::real
|
|
1045 |
#1033 := (* -1::real #749)
|
|
1046 |
#1234 := (+ #650 #1033)
|
|
1047 |
#1236 := (>= #1234 0::real)
|
|
1048 |
#1243 := (not #1236)
|
|
1049 |
#1237 := [hypothesis]: #1236
|
|
1050 |
decl f20 :: S5
|
|
1051 |
#78 := f20
|
|
1052 |
#1034 := (f8 f20 #34)
|
|
1053 |
#1037 := (* -1::real #1034)
|
|
1054 |
#1048 := (+ #749 #1037)
|
|
1055 |
#1049 := (<= #1048 0::real)
|
|
1056 |
#1073 := (not #1049)
|
|
1057 |
decl f17 :: S3
|
|
1058 |
#48 := f17
|
|
1059 |
#76 := (f19 f17)
|
|
1060 |
#601 := (f8 #76 #34)
|
|
1061 |
#1038 := (+ #601 #1037)
|
|
1062 |
#1039 := (>= #1038 0::real)
|
|
1063 |
#1054 := (or #1039 #1049)
|
|
1064 |
#1057 := (not #1054)
|
|
1065 |
#79 := (f8 f20 #9)
|
|
1066 |
#588 := (pattern #79)
|
|
1067 |
#77 := (f8 #76 #9)
|
|
1068 |
#561 := (pattern #77)
|
|
1069 |
#310 := (* -1::real #82)
|
|
1070 |
#311 := (+ #79 #310)
|
|
1071 |
#309 := (>= #311 0::real)
|
|
1072 |
#305 := (* -1::real #79)
|
|
1073 |
#306 := (+ #77 #305)
|
|
1074 |
#304 := (>= #306 0::real)
|
|
1075 |
#422 := (or #304 #309)
|
|
1076 |
#423 := (not #422)
|
|
1077 |
#589 := (forall (vars (?v0 S2)) (:pat #561 #588 #545) #423)
|
|
1078 |
#426 := (forall (vars (?v0 S2)) #423)
|
|
1079 |
#592 := (iff #426 #589)
|
|
1080 |
#590 := (iff #423 #423)
|
|
1081 |
#591 := [refl]: #590
|
|
1082 |
#593 := [quant-intro #591]: #592
|
|
1083 |
#312 := (not #309)
|
|
1084 |
#302 := (not #304)
|
|
1085 |
#315 := (and #302 #312)
|
|
1086 |
#318 := (forall (vars (?v0 S2)) #315)
|
|
1087 |
#427 := (iff #318 #426)
|
|
1088 |
#424 := (iff #315 #423)
|
|
1089 |
#425 := [rewrite]: #424
|
|
1090 |
#428 := [quant-intro #425]: #427
|
|
1091 |
#414 := (~ #318 #318)
|
|
1092 |
#412 := (~ #315 #315)
|
|
1093 |
#413 := [refl]: #412
|
|
1094 |
#415 := [nnf-pos #413]: #414
|
|
1095 |
decl f4 :: S3
|
|
1096 |
#8 := f4
|
|
1097 |
#89 := (f19 f4)
|
|
1098 |
#90 := (f8 #89 #9)
|
|
1099 |
#328 := (* -1::real #90)
|
|
1100 |
#329 := (+ #79 #328)
|
|
1101 |
#327 := (>= #329 0::real)
|
|
1102 |
#330 := (not #327)
|
|
1103 |
#87 := (f8 #86 #9)
|
|
1104 |
#321 := (* -1::real #87)
|
|
1105 |
#322 := (+ #79 #321)
|
|
1106 |
#323 := (<= #322 0::real)
|
|
1107 |
#324 := (not #323)
|
|
1108 |
#333 := (and #324 #330)
|
|
1109 |
#336 := (forall (vars (?v0 S2)) #333)
|
|
1110 |
#339 := (and #318 #336)
|
|
1111 |
#91 := (< #79 #90)
|
|
1112 |
#88 := (< #87 #79)
|
|
1113 |
#92 := (and #88 #91)
|
|
1114 |
#93 := (forall (vars (?v0 S2)) #92)
|
|
1115 |
#83 := (< #79 #82)
|
|
1116 |
#80 := (< #77 #79)
|
|
1117 |
#84 := (and #80 #83)
|
|
1118 |
#85 := (forall (vars (?v0 S2)) #84)
|
|
1119 |
#94 := (and #85 #93)
|
|
1120 |
#340 := (iff #94 #339)
|
|
1121 |
#337 := (iff #93 #336)
|
|
1122 |
#334 := (iff #92 #333)
|
|
1123 |
#331 := (iff #91 #330)
|
|
1124 |
#332 := [rewrite]: #331
|
|
1125 |
#325 := (iff #88 #324)
|
|
1126 |
#326 := [rewrite]: #325
|
|
1127 |
#335 := [monotonicity #326 #332]: #334
|
|
1128 |
#338 := [quant-intro #335]: #337
|
|
1129 |
#319 := (iff #85 #318)
|
|
1130 |
#316 := (iff #84 #315)
|
|
1131 |
#313 := (iff #83 #312)
|
|
1132 |
#314 := [rewrite]: #313
|
|
1133 |
#307 := (iff #80 #302)
|
|
1134 |
#308 := [rewrite]: #307
|
|
1135 |
#317 := [monotonicity #308 #314]: #316
|
|
1136 |
#320 := [quant-intro #317]: #319
|
|
1137 |
#341 := [monotonicity #320 #338]: #340
|
|
1138 |
#297 := [asserted]: #94
|
|
1139 |
#342 := [mp #297 #341]: #339
|
|
1140 |
#343 := [and-elim #342]: #318
|
|
1141 |
#416 := [mp~ #343 #415]: #318
|
|
1142 |
#429 := [mp #416 #428]: #426
|
|
1143 |
#594 := [mp #429 #593]: #589
|
|
1144 |
#1060 := (not #589)
|
|
1145 |
#1061 := (or #1060 #1057)
|
|
1146 |
#1035 := (+ #1034 #1033)
|
|
1147 |
#1036 := (>= #1035 0::real)
|
|
1148 |
#1040 := (or #1039 #1036)
|
|
1149 |
#1041 := (not #1040)
|
|
1150 |
#1062 := (or #1060 #1041)
|
|
1151 |
#1064 := (iff #1062 #1061)
|
|
1152 |
#1066 := (iff #1061 #1061)
|
|
1153 |
#1067 := [rewrite]: #1066
|
|
1154 |
#1058 := (iff #1041 #1057)
|
|
1155 |
#1055 := (iff #1040 #1054)
|
|
1156 |
#1052 := (iff #1036 #1049)
|
|
1157 |
#1042 := (+ #1033 #1034)
|
|
1158 |
#1045 := (>= #1042 0::real)
|
|
1159 |
#1050 := (iff #1045 #1049)
|
|
1160 |
#1051 := [rewrite]: #1050
|
|
1161 |
#1046 := (iff #1036 #1045)
|
|
1162 |
#1043 := (= #1035 #1042)
|
|
1163 |
#1044 := [rewrite]: #1043
|
|
1164 |
#1047 := [monotonicity #1044]: #1046
|
|
1165 |
#1053 := [trans #1047 #1051]: #1052
|
|
1166 |
#1056 := [monotonicity #1053]: #1055
|
|
1167 |
#1059 := [monotonicity #1056]: #1058
|
|
1168 |
#1065 := [monotonicity #1059]: #1064
|
|
1169 |
#1068 := [trans #1065 #1067]: #1064
|
|
1170 |
#1063 := [quant-inst]: #1062
|
|
1171 |
#1069 := [mp #1063 #1068]: #1061
|
|
1172 |
#1238 := [unit-resolution #1069 #594]: #1057
|
|
1173 |
#1074 := (or #1054 #1073)
|
|
1174 |
#1075 := [def-axiom]: #1074
|
|
1175 |
#1239 := [unit-resolution #1075 #1238]: #1073
|
|
1176 |
#1150 := (+ #650 #1037)
|
|
1177 |
#1151 := (>= #1150 0::real)
|
|
1178 |
#1183 := (not #1151)
|
|
1179 |
#693 := (f8 #89 #34)
|
|
1180 |
#1162 := (+ #693 #1037)
|
|
1181 |
#1163 := (<= #1162 0::real)
|
|
1182 |
#1168 := (or #1151 #1163)
|
|
1183 |
#1171 := (not #1168)
|
|
1184 |
#536 := (pattern #90)
|
|
1185 |
#553 := (pattern #87)
|
|
1186 |
#430 := (or #323 #327)
|
|
1187 |
#431 := (not #430)
|
|
1188 |
#595 := (forall (vars (?v0 S2)) (:pat #588 #553 #536) #431)
|
|
1189 |
#434 := (forall (vars (?v0 S2)) #431)
|
|
1190 |
#598 := (iff #434 #595)
|
|
1191 |
#596 := (iff #431 #431)
|
|
1192 |
#597 := [refl]: #596
|
|
1193 |
#599 := [quant-intro #597]: #598
|
|
1194 |
#435 := (iff #336 #434)
|
|
1195 |
#432 := (iff #333 #431)
|
|
1196 |
#433 := [rewrite]: #432
|
|
1197 |
#436 := [quant-intro #433]: #435
|
|
1198 |
#419 := (~ #336 #336)
|
|
1199 |
#417 := (~ #333 #333)
|
|
1200 |
#418 := [refl]: #417
|
|
1201 |
#420 := [nnf-pos #418]: #419
|
|
1202 |
#344 := [and-elim #342]: #336
|
|
1203 |
#421 := [mp~ #344 #420]: #336
|
|
1204 |
#437 := [mp #421 #436]: #434
|
|
1205 |
#600 := [mp #437 #599]: #595
|
|
1206 |
#1118 := (not #595)
|
|
1207 |
#1174 := (or #1118 #1171)
|
|
1208 |
#1136 := (* -1::real #693)
|
|
1209 |
#1137 := (+ #1034 #1136)
|
|
1210 |
#1138 := (>= #1137 0::real)
|
|
1211 |
#1139 := (* -1::real #650)
|
|
1212 |
#1140 := (+ #1034 #1139)
|
|
1213 |
#1141 := (<= #1140 0::real)
|
|
1214 |
#1142 := (or #1141 #1138)
|
|
1215 |
#1143 := (not #1142)
|
|
1216 |
#1175 := (or #1118 #1143)
|
|
1217 |
#1177 := (iff #1175 #1174)
|
|
1218 |
#1179 := (iff #1174 #1174)
|
|
1219 |
#1180 := [rewrite]: #1179
|
|
1220 |
#1172 := (iff #1143 #1171)
|
|
1221 |
#1169 := (iff #1142 #1168)
|
|
1222 |
#1166 := (iff #1138 #1163)
|
|
1223 |
#1156 := (+ #1136 #1034)
|
|
1224 |
#1159 := (>= #1156 0::real)
|
|
1225 |
#1164 := (iff #1159 #1163)
|
|
1226 |
#1165 := [rewrite]: #1164
|
|
1227 |
#1160 := (iff #1138 #1159)
|
|
1228 |
#1157 := (= #1137 #1156)
|
|
1229 |
#1158 := [rewrite]: #1157
|
|
1230 |
#1161 := [monotonicity #1158]: #1160
|
|
1231 |
#1167 := [trans #1161 #1165]: #1166
|
|
1232 |
#1154 := (iff #1141 #1151)
|
|
1233 |
#1144 := (+ #1139 #1034)
|
|
1234 |
#1147 := (<= #1144 0::real)
|
|
1235 |
#1152 := (iff #1147 #1151)
|
|
1236 |
#1153 := [rewrite]: #1152
|
|
1237 |
#1148 := (iff #1141 #1147)
|
|
1238 |
#1145 := (= #1140 #1144)
|
|
1239 |
#1146 := [rewrite]: #1145
|
|
1240 |
#1149 := [monotonicity #1146]: #1148
|
|
1241 |
#1155 := [trans #1149 #1153]: #1154
|
|
1242 |
#1170 := [monotonicity #1155 #1167]: #1169
|
|
1243 |
#1173 := [monotonicity #1170]: #1172
|
|
1244 |
#1178 := [monotonicity #1173]: #1177
|
|
1245 |
#1181 := [trans #1178 #1180]: #1177
|
|
1246 |
#1176 := [quant-inst]: #1175
|
|
1247 |
#1182 := [mp #1176 #1181]: #1174
|
|
1248 |
#1240 := [unit-resolution #1182 #600]: #1171
|
|
1249 |
#1184 := (or #1168 #1183)
|
|
1250 |
#1185 := [def-axiom]: #1184
|
|
1251 |
#1241 := [unit-resolution #1185 #1240]: #1183
|
|
1252 |
#1242 := [th-lemma #1241 #1239 #1237]: false
|
|
1253 |
#1244 := [lemma #1242]: #1243
|
|
1254 |
#1247 := (or #1246 #1236)
|
|
1255 |
#1248 := [th-lemma]: #1247
|
|
1256 |
#1316 := [unit-resolution #1248 #1244]: #1246
|
|
1257 |
#1337 := [mp #1316 #1336]: #690
|
|
1258 |
#1339 := (or #663 #651)
|
|
1259 |
decl f16 :: S5
|
|
1260 |
#43 := f16
|
|
1261 |
#603 := (f8 f16 #34)
|
|
1262 |
#652 := (= #603 #650)
|
|
1263 |
#668 := (ite #663 #652 #651)
|
|
1264 |
#42 := (f8 f10 #9)
|
|
1265 |
#554 := (pattern #42)
|
|
1266 |
#44 := (f8 f16 #9)
|
|
1267 |
#552 := (pattern #44)
|
|
1268 |
#461 := (= #42 #87)
|
|
1269 |
#460 := (= #44 #87)
|
|
1270 |
#124 := (* -1::int #14)
|
|
1271 |
#125 := (+ #12 #124)
|
|
1272 |
#123 := (>= #125 0::int)
|
|
1273 |
#462 := (ite #123 #460 #461)
|
|
1274 |
#555 := (forall (vars (?v0 S2)) (:pat #535 #552 #553 #554) #462)
|
|
1275 |
#465 := (forall (vars (?v0 S2)) #462)
|
|
1276 |
#558 := (iff #465 #555)
|
|
1277 |
#556 := (iff #462 #462)
|
|
1278 |
#557 := [refl]: #556
|
|
1279 |
#559 := [quant-intro #557]: #558
|
|
1280 |
#169 := (ite #123 #44 #42)
|
|
1281 |
#385 := (= #87 #169)
|
|
1282 |
#386 := (forall (vars (?v0 S2)) #385)
|
|
1283 |
#466 := (iff #386 #465)
|
|
1284 |
#463 := (iff #385 #462)
|
|
1285 |
#464 := [rewrite]: #463
|
|
1286 |
#467 := [quant-intro #464]: #466
|
|
1287 |
#359 := (~ #386 #386)
|
|
1288 |
#361 := (~ #385 #385)
|
|
1289 |
#362 := [refl]: #361
|
|
1290 |
#360 := [nnf-pos #362]: #359
|
|
1291 |
#41 := (f3 f15 #9)
|
|
1292 |
#174 := (= #41 #169)
|
|
1293 |
#177 := (forall (vars (?v0 S2)) #174)
|
|
1294 |
#387 := (iff #177 #386)
|
|
1295 |
#388 := [rewrite* #298]: #387
|
|
1296 |
#15 := (< #12 #14)
|
|
1297 |
#45 := (ite #15 #42 #44)
|
|
1298 |
#46 := (= #41 #45)
|
|
1299 |
#47 := (forall (vars (?v0 S2)) #46)
|
|
1300 |
#178 := (iff #47 #177)
|
|
1301 |
#175 := (iff #46 #174)
|
|
1302 |
#172 := (= #45 #169)
|
|
1303 |
#122 := (not #123)
|
|
1304 |
#166 := (ite #122 #42 #44)
|
|
1305 |
#170 := (= #166 #169)
|
|
1306 |
#171 := [rewrite]: #170
|
|
1307 |
#167 := (= #45 #166)
|
|
1308 |
#126 := (iff #15 #122)
|
|
1309 |
#127 := [rewrite]: #126
|
|
1310 |
#168 := [monotonicity #127]: #167
|
|
1311 |
#173 := [trans #168 #171]: #172
|
|
1312 |
#176 := [monotonicity #173]: #175
|
|
1313 |
#179 := [quant-intro #176]: #178
|
|
1314 |
#120 := [asserted]: #47
|
|
1315 |
#180 := [mp #120 #179]: #177
|
|
1316 |
#389 := [mp #180 #388]: #386
|
|
1317 |
#357 := [mp~ #389 #360]: #386
|
|
1318 |
#468 := [mp #357 #467]: #465
|
|
1319 |
#560 := [mp #468 #559]: #555
|
|
1320 |
#671 := (not #555)
|
|
1321 |
#672 := (or #671 #668)
|
|
1322 |
#653 := (+ #605 #124)
|
|
1323 |
#654 := (>= #653 0::int)
|
|
1324 |
#655 := (ite #654 #652 #651)
|
|
1325 |
#673 := (or #671 #655)
|
|
1326 |
#675 := (iff #673 #672)
|
|
1327 |
#677 := (iff #672 #672)
|
|
1328 |
#678 := [rewrite]: #677
|
|
1329 |
#669 := (iff #655 #668)
|
|
1330 |
#666 := (iff #654 #663)
|
|
1331 |
#656 := (+ #124 #605)
|
|
1332 |
#659 := (>= #656 0::int)
|
|
1333 |
#664 := (iff #659 #663)
|
|
1334 |
#665 := [rewrite]: #664
|
|
1335 |
#660 := (iff #654 #659)
|
|
1336 |
#657 := (= #653 #656)
|
|
1337 |
#658 := [rewrite]: #657
|
|
1338 |
#661 := [monotonicity #658]: #660
|
|
1339 |
#667 := [trans #661 #665]: #666
|
|
1340 |
#670 := [monotonicity #667]: #669
|
|
1341 |
#676 := [monotonicity #670]: #675
|
|
1342 |
#679 := [trans #676 #678]: #675
|
|
1343 |
#674 := [quant-inst]: #673
|
|
1344 |
#680 := [mp #674 #679]: #672
|
|
1345 |
#1338 := [unit-resolution #680 #560]: #668
|
|
1346 |
#681 := (not #668)
|
|
1347 |
#685 := (or #681 #663 #651)
|
|
1348 |
#686 := [def-axiom]: #685
|
|
1349 |
#1340 := [unit-resolution #686 #1338]: #1339
|
|
1350 |
#1341 := [unit-resolution #1340 #1337]: #663
|
|
1351 |
#1286 := (+ #14 #146)
|
|
1352 |
#1287 := (<= #1286 0::int)
|
|
1353 |
#1376 := (not #1287)
|
|
1354 |
#1285 := (= #14 #31)
|
|
1355 |
#1314 := (not #1285)
|
|
1356 |
#290 := (= f7 f14)
|
|
1357 |
#702 := (= f7 #70)
|
|
1358 |
decl f18 :: (-> int S4)
|
|
1359 |
#985 := (f18 #605)
|
|
1360 |
#1305 := (= #985 #70)
|
|
1361 |
#986 := (= #70 #985)
|
|
1362 |
#53 := (:var 0 S4)
|
|
1363 |
#54 := (f5 #53)
|
|
1364 |
#568 := (pattern #54)
|
|
1365 |
#55 := (f18 #54)
|
|
1366 |
#181 := (= #53 #55)
|
|
1367 |
#569 := (forall (vars (?v0 S4)) (:pat #568) #181)
|
|
1368 |
#199 := (forall (vars (?v0 S4)) #181)
|
|
1369 |
#572 := (iff #199 #569)
|
|
1370 |
#570 := (iff #181 #181)
|
|
1371 |
#571 := [refl]: #570
|
|
1372 |
#573 := [quant-intro #571]: #572
|
|
1373 |
#399 := (~ #199 #199)
|
|
1374 |
#397 := (~ #181 #181)
|
|
1375 |
#398 := [refl]: #397
|
|
1376 |
#400 := [nnf-pos #398]: #399
|
|
1377 |
#56 := (= #55 #53)
|
|
1378 |
#57 := (forall (vars (?v0 S4)) #56)
|
|
1379 |
#200 := (iff #57 #199)
|
|
1380 |
#197 := (iff #56 #181)
|
|
1381 |
#198 := [rewrite]: #197
|
|
1382 |
#201 := [quant-intro #198]: #200
|
|
1383 |
#165 := [asserted]: #57
|
|
1384 |
#204 := [mp #165 #201]: #199
|
|
1385 |
#401 := [mp~ #204 #400]: #199
|
|
1386 |
#574 := [mp #401 #573]: #569
|
|
1387 |
#989 := (not #569)
|
|
1388 |
#990 := (or #989 #986)
|
|
1389 |
#991 := [quant-inst]: #990
|
|
1390 |
#1289 := [unit-resolution #991 #574]: #986
|
|
1391 |
#1306 := [symm #1289]: #1305
|
|
1392 |
#1309 := (= f7 #985)
|
|
1393 |
#20 := (f11 f7)
|
|
1394 |
#72 := (f6 #20)
|
|
1395 |
#797 := (f5 #72)
|
|
1396 |
#987 := (f18 #797)
|
|
1397 |
#1303 := (= #987 #985)
|
|
1398 |
#1300 := (= #797 #605)
|
|
1399 |
#1298 := (= #797 #31)
|
|
1400 |
#1291 := [hypothesis]: #1285
|
|
1401 |
#1293 := (= #797 #14)
|
|
1402 |
#73 := (= #72 f7)
|
|
1403 |
#285 := (= f7 #72)
|
|
1404 |
#287 := (iff #73 #285)
|
|
1405 |
#288 := [rewrite]: #287
|
|
1406 |
#284 := [asserted]: #73
|
|
1407 |
#291 := [mp #284 #288]: #285
|
|
1408 |
#1292 := [symm #291]: #73
|
|
1409 |
#1294 := [monotonicity #1292]: #1293
|
|
1410 |
#1299 := [trans #1294 #1291]: #1298
|
|
1411 |
#1301 := [trans #1299 #1297]: #1300
|
|
1412 |
#1304 := [monotonicity #1301]: #1303
|
|
1413 |
#1307 := (= f7 #987)
|
|
1414 |
#988 := (= #72 #987)
|
|
1415 |
#994 := (or #989 #988)
|
|
1416 |
#995 := [quant-inst]: #994
|
|
1417 |
#1302 := [unit-resolution #995 #574]: #988
|
|
1418 |
#1308 := [trans #291 #1302]: #1307
|
|
1419 |
#1310 := [trans #1308 #1304]: #1309
|
|
1420 |
#1311 := [trans #1310 #1306]: #702
|
|
1421 |
#1312 := [trans #1311 #1290]: #290
|
|
1422 |
#294 := (not #290)
|
|
1423 |
#74 := (= f14 f7)
|
|
1424 |
#75 := (not #74)
|
|
1425 |
#295 := (iff #75 #294)
|
|
1426 |
#292 := (iff #74 #290)
|
|
1427 |
#293 := [rewrite]: #292
|
|
1428 |
#296 := [monotonicity #293]: #295
|
|
1429 |
#289 := [asserted]: #75
|
|
1430 |
#299 := [mp #289 #296]: #294
|
|
1431 |
#1313 := [unit-resolution #299 #1312]: false
|
|
1432 |
#1315 := [lemma #1313]: #1314
|
|
1433 |
#1380 := (or #1285 #1376)
|
|
1434 |
#1288 := (>= #1286 0::int)
|
|
1435 |
#807 := (* -1::int #797)
|
|
1436 |
#808 := (+ #31 #807)
|
|
1437 |
#809 := (<= #808 0::int)
|
|
1438 |
#793 := (f8 #76 #20)
|
|
1439 |
#21 := (f8 f10 #20)
|
|
1440 |
#794 := (= #21 #793)
|
|
1441 |
#838 := (not #794)
|
|
1442 |
#883 := (f8 #89 #20)
|
|
1443 |
#1259 := (= #793 #883)
|
|
1444 |
#1272 := (not #1259)
|
|
1445 |
#1362 := (iff #1272 #838)
|
|
1446 |
#1360 := (iff #1259 #794)
|
|
1447 |
#1355 := (= #793 #21)
|
|
1448 |
#1358 := (iff #1355 #794)
|
|
1449 |
#1359 := [commutativity]: #1358
|
|
1450 |
#1356 := (iff #1259 #1355)
|
|
1451 |
#1353 := (= #883 #21)
|
|
1452 |
#888 := (= #21 #883)
|
|
1453 |
#886 := (f8 f12 #20)
|
|
1454 |
#891 := (= #883 #886)
|
|
1455 |
#894 := (ite #285 #888 #891)
|
|
1456 |
#884 := (f8 f9 #20)
|
|
1457 |
#897 := (= #883 #884)
|
|
1458 |
#853 := (+ #14 #807)
|
|
1459 |
#854 := (<= #853 0::int)
|
|
1460 |
#900 := (ite #854 #894 #897)
|
|
1461 |
#441 := (= #17 #90)
|
|
1462 |
#439 := (= #23 #90)
|
|
1463 |
#438 := (= #21 #90)
|
|
1464 |
#18 := (= #11 f7)
|
|
1465 |
#440 := (ite #18 #438 #439)
|
|
1466 |
#442 := (ite #123 #440 #441)
|
|
1467 |
#539 := (forall (vars (?v0 S2)) (:pat #535 #536 #537 #538) #442)
|
|
1468 |
#445 := (forall (vars (?v0 S2)) #442)
|
|
1469 |
#542 := (iff #445 #539)
|
|
1470 |
#540 := (iff #442 #442)
|
|
1471 |
#541 := [refl]: #540
|
|
1472 |
#543 := [quant-intro #541]: #542
|
|
1473 |
#24 := (ite #18 #21 #23)
|
|
1474 |
#131 := (ite #123 #24 #17)
|
|
1475 |
#375 := (= #90 #131)
|
|
1476 |
#376 := (forall (vars (?v0 S2)) #375)
|
|
1477 |
#446 := (iff #376 #445)
|
|
1478 |
#443 := (iff #375 #442)
|
|
1479 |
#444 := [rewrite]: #443
|
|
1480 |
#447 := [quant-intro #444]: #446
|
|
1481 |
#369 := (~ #376 #376)
|
|
1482 |
#371 := (~ #375 #375)
|
|
1483 |
#372 := [refl]: #371
|
|
1484 |
#370 := [nnf-pos #372]: #369
|
|
1485 |
#10 := (f3 f4 #9)
|
|
1486 |
#136 := (= #10 #131)
|
|
1487 |
#139 := (forall (vars (?v0 S2)) #136)
|
|
1488 |
#377 := (iff #139 #376)
|
|
1489 |
#378 := [rewrite* #298]: #377
|
|
1490 |
#25 := (ite #15 #17 #24)
|
|
1491 |
#26 := (= #10 #25)
|
|
1492 |
#27 := (forall (vars (?v0 S2)) #26)
|
|
1493 |
#140 := (iff #27 #139)
|
|
1494 |
#137 := (iff #26 #136)
|
|
1495 |
#134 := (= #25 #131)
|
|
1496 |
#128 := (ite #122 #17 #24)
|
|
1497 |
#132 := (= #128 #131)
|
|
1498 |
#133 := [rewrite]: #132
|
|
1499 |
#129 := (= #25 #128)
|
|
1500 |
#130 := [monotonicity #127]: #129
|
|
1501 |
#135 := [trans #130 #133]: #134
|
|
1502 |
#138 := [monotonicity #135]: #137
|
|
1503 |
#141 := [quant-intro #138]: #140
|
|
1504 |
#118 := [asserted]: #27
|
|
1505 |
#142 := [mp #118 #141]: #139
|
|
1506 |
#379 := [mp #142 #378]: #376
|
|
1507 |
#367 := [mp~ #379 #370]: #376
|
|
1508 |
#448 := [mp #367 #447]: #445
|
|
1509 |
#544 := [mp #448 #543]: #539
|
|
1510 |
#717 := (not #539)
|
|
1511 |
#903 := (or #717 #900)
|
|
1512 |
#885 := (= #884 #883)
|
|
1513 |
#887 := (= #886 #883)
|
|
1514 |
#889 := (ite #73 #888 #887)
|
|
1515 |
#844 := (+ #797 #124)
|
|
1516 |
#845 := (>= #844 0::int)
|
|
1517 |
#890 := (ite #845 #889 #885)
|
|
1518 |
#904 := (or #717 #890)
|
|
1519 |
#906 := (iff #904 #903)
|
|
1520 |
#908 := (iff #903 #903)
|
|
1521 |
#909 := [rewrite]: #908
|
|
1522 |
#901 := (iff #890 #900)
|
|
1523 |
#898 := (iff #885 #897)
|
|
1524 |
#899 := [rewrite]: #898
|
|
1525 |
#895 := (iff #889 #894)
|
|
1526 |
#892 := (iff #887 #891)
|
|
1527 |
#893 := [rewrite]: #892
|
|
1528 |
#896 := [monotonicity #288 #893]: #895
|
|
1529 |
#857 := (iff #845 #854)
|
|
1530 |
#847 := (+ #124 #797)
|
|
1531 |
#850 := (>= #847 0::int)
|
|
1532 |
#855 := (iff #850 #854)
|
|
1533 |
#856 := [rewrite]: #855
|
|
1534 |
#851 := (iff #845 #850)
|
|
1535 |
#848 := (= #844 #847)
|
|
1536 |
#849 := [rewrite]: #848
|
|
1537 |
#852 := [monotonicity #849]: #851
|
|
1538 |
#858 := [trans #852 #856]: #857
|
|
1539 |
#902 := [monotonicity #858 #896 #899]: #901
|
|
1540 |
#907 := [monotonicity #902]: #906
|
|
1541 |
#910 := [trans #907 #909]: #906
|
|
1542 |
#905 := [quant-inst]: #904
|
|
1543 |
#911 := [mp #905 #910]: #903
|
|
1544 |
#1343 := [unit-resolution #911 #544]: #900
|
|
1545 |
#983 := (= #14 #797)
|
|
1546 |
#1344 := [symm #1294]: #983
|
|
1547 |
#1345 := (not #983)
|
|
1548 |
#1346 := (or #1345 #854)
|
|
1549 |
#1347 := [th-lemma]: #1346
|
|
1550 |
#1348 := [unit-resolution #1347 #1344]: #854
|
|
1551 |
#872 := (not #854)
|
|
1552 |
#924 := (not #900)
|
|
1553 |
#925 := (or #924 #872 #894)
|
|
1554 |
#926 := [def-axiom]: #925
|
|
1555 |
#1349 := [unit-resolution #926 #1348 #1343]: #894
|
|
1556 |
#912 := (not #894)
|
|
1557 |
#1350 := (or #912 #888)
|
|
1558 |
#913 := (not #285)
|
|
1559 |
#914 := (or #912 #913 #888)
|
|
1560 |
#915 := [def-axiom]: #914
|
|
1561 |
#1351 := [unit-resolution #915 #291]: #1350
|
|
1562 |
#1352 := [unit-resolution #1351 #1349]: #888
|
|
1563 |
#1354 := [symm #1352]: #1353
|
|
1564 |
#1357 := [monotonicity #1354]: #1356
|
|
1565 |
#1361 := [trans #1357 #1359]: #1360
|
|
1566 |
#1363 := [monotonicity #1361]: #1362
|
|
1567 |
#1078 := (* -1::real #883)
|
|
1568 |
#1260 := (+ #793 #1078)
|
|
1569 |
#1262 := (>= #1260 0::real)
|
|
1570 |
#1269 := (not #1262)
|
|
1571 |
#1263 := [hypothesis]: #1262
|
|
1572 |
#1079 := (f8 f20 #20)
|
|
1573 |
#1093 := (* -1::real #1079)
|
|
1574 |
#1106 := (+ #883 #1093)
|
|
1575 |
#1107 := (<= #1106 0::real)
|
|
1576 |
#1131 := (not #1107)
|
|
1577 |
#841 := (f8 #86 #20)
|
|
1578 |
#1094 := (+ #841 #1093)
|
|
1579 |
#1095 := (>= #1094 0::real)
|
|
1580 |
#1112 := (or #1095 #1107)
|
|
1581 |
#1115 := (not #1112)
|
|
1582 |
#1119 := (or #1118 #1115)
|
|
1583 |
#1080 := (+ #1079 #1078)
|
|
1584 |
#1081 := (>= #1080 0::real)
|
|
1585 |
#1082 := (* -1::real #841)
|
|
1586 |
#1083 := (+ #1079 #1082)
|
|
1587 |
#1084 := (<= #1083 0::real)
|
|
1588 |
#1085 := (or #1084 #1081)
|
|
1589 |
#1086 := (not #1085)
|
|
1590 |
#1120 := (or #1118 #1086)
|
|
1591 |
#1122 := (iff #1120 #1119)
|
|
1592 |
#1124 := (iff #1119 #1119)
|
|
1593 |
#1125 := [rewrite]: #1124
|
|
1594 |
#1116 := (iff #1086 #1115)
|
|
1595 |
#1113 := (iff #1085 #1112)
|
|
1596 |
#1110 := (iff #1081 #1107)
|
|
1597 |
#1100 := (+ #1078 #1079)
|
|
1598 |
#1103 := (>= #1100 0::real)
|
|
1599 |
#1108 := (iff #1103 #1107)
|
|
1600 |
#1109 := [rewrite]: #1108
|
|
1601 |
#1104 := (iff #1081 #1103)
|
|
1602 |
#1101 := (= #1080 #1100)
|
|
1603 |
#1102 := [rewrite]: #1101
|
|
1604 |
#1105 := [monotonicity #1102]: #1104
|
|
1605 |
#1111 := [trans #1105 #1109]: #1110
|
|
1606 |
#1098 := (iff #1084 #1095)
|
|
1607 |
#1087 := (+ #1082 #1079)
|
|
1608 |
#1090 := (<= #1087 0::real)
|
|
1609 |
#1096 := (iff #1090 #1095)
|
|
1610 |
#1097 := [rewrite]: #1096
|
|
1611 |
#1091 := (iff #1084 #1090)
|
|
1612 |
#1088 := (= #1083 #1087)
|
|
1613 |
#1089 := [rewrite]: #1088
|
|
1614 |
#1092 := [monotonicity #1089]: #1091
|
|
1615 |
#1099 := [trans #1092 #1097]: #1098
|
|
1616 |
#1114 := [monotonicity #1099 #1111]: #1113
|
|
1617 |
#1117 := [monotonicity #1114]: #1116
|
|
1618 |
#1123 := [monotonicity #1117]: #1122
|
|
1619 |
#1126 := [trans #1123 #1125]: #1122
|
|
1620 |
#1121 := [quant-inst]: #1120
|
|
1621 |
#1127 := [mp #1121 #1126]: #1119
|
|
1622 |
#1264 := [unit-resolution #1127 #600]: #1115
|
|
1623 |
#1132 := (or #1112 #1131)
|
|
1624 |
#1133 := [def-axiom]: #1132
|
|
1625 |
#1265 := [unit-resolution #1133 #1264]: #1131
|
|
1626 |
#1194 := (+ #793 #1093)
|
|
1627 |
#1195 := (>= #1194 0::real)
|
|
1628 |
#1225 := (not #1195)
|
|
1629 |
#934 := (f8 #81 #20)
|
|
1630 |
#1204 := (+ #934 #1093)
|
|
1631 |
#1205 := (<= #1204 0::real)
|
|
1632 |
#1210 := (or #1195 #1205)
|
|
1633 |
#1213 := (not #1210)
|
|
1634 |
#1216 := (or #1060 #1213)
|
|
1635 |
#1191 := (* -1::real #934)
|
|
1636 |
#1192 := (+ #1079 #1191)
|
|
1637 |
#1193 := (>= #1192 0::real)
|
|
1638 |
#1196 := (or #1195 #1193)
|
|
1639 |
#1197 := (not #1196)
|
|
1640 |
#1217 := (or #1060 #1197)
|
|
1641 |
#1219 := (iff #1217 #1216)
|
|
1642 |
#1221 := (iff #1216 #1216)
|
|
1643 |
#1222 := [rewrite]: #1221
|
|
1644 |
#1214 := (iff #1197 #1213)
|
|
1645 |
#1211 := (iff #1196 #1210)
|
|
1646 |
#1208 := (iff #1193 #1205)
|
|
1647 |
#1198 := (+ #1191 #1079)
|
|
1648 |
#1201 := (>= #1198 0::real)
|
|
1649 |
#1206 := (iff #1201 #1205)
|
|
1650 |
#1207 := [rewrite]: #1206
|
|
1651 |
#1202 := (iff #1193 #1201)
|
|
1652 |
#1199 := (= #1192 #1198)
|
|
1653 |
#1200 := [rewrite]: #1199
|
|
1654 |
#1203 := [monotonicity #1200]: #1202
|
|
1655 |
#1209 := [trans #1203 #1207]: #1208
|
|
1656 |
#1212 := [monotonicity #1209]: #1211
|
|
1657 |
#1215 := [monotonicity #1212]: #1214
|
|
1658 |
#1220 := [monotonicity #1215]: #1219
|
|
1659 |
#1223 := [trans #1220 #1222]: #1219
|
|
1660 |
#1218 := [quant-inst]: #1217
|
|
1661 |
#1224 := [mp #1218 #1223]: #1216
|
|
1662 |
#1266 := [unit-resolution #1224 #594]: #1213
|
|
1663 |
#1226 := (or #1210 #1225)
|
|
1664 |
#1227 := [def-axiom]: #1226
|
|
1665 |
#1267 := [unit-resolution #1227 #1266]: #1225
|
|
1666 |
#1268 := [th-lemma #1267 #1265 #1263]: false
|
|
1667 |
#1270 := [lemma #1268]: #1269
|
|
1668 |
#1273 := (or #1272 #1262)
|
|
1669 |
#1274 := [th-lemma]: #1273
|
|
1670 |
#1342 := [unit-resolution #1274 #1270]: #1272
|
|
1671 |
#1364 := [mp #1342 #1363]: #838
|
|
1672 |
#1366 := (or #809 #794)
|
|
1673 |
#795 := (f8 f16 #20)
|
|
1674 |
#814 := (= #793 #795)
|
|
1675 |
#817 := (ite #809 #814 #794)
|
|
1676 |
#470 := (= #42 #77)
|
|
1677 |
#469 := (= #44 #77)
|
|
1678 |
#471 := (ite #145 #469 #470)
|
|
1679 |
#562 := (forall (vars (?v0 S2)) (:pat #535 #552 #561 #554) #471)
|
|
1680 |
#474 := (forall (vars (?v0 S2)) #471)
|
|
1681 |
#565 := (iff #474 #562)
|
|
1682 |
#563 := (iff #471 #471)
|
|
1683 |
#564 := [refl]: #563
|
|
1684 |
#566 := [quant-intro #564]: #565
|
|
1685 |
#185 := (ite #145 #44 #42)
|
|
1686 |
#390 := (= #77 #185)
|
|
1687 |
#391 := (forall (vars (?v0 S2)) #390)
|
|
1688 |
#475 := (iff #391 #474)
|
|
1689 |
#472 := (iff #390 #471)
|
|
1690 |
#473 := [rewrite]: #472
|
|
1691 |
#476 := [quant-intro #473]: #475
|
|
1692 |
#348 := (~ #391 #391)
|
|
1693 |
#358 := (~ #390 #390)
|
|
1694 |
#347 := [refl]: #358
|
|
1695 |
#395 := [nnf-pos #347]: #348
|
|
1696 |
#49 := (f3 f17 #9)
|
|
1697 |
#190 := (= #49 #185)
|
|
1698 |
#193 := (forall (vars (?v0 S2)) #190)
|
|
1699 |
#392 := (iff #193 #391)
|
|
1700 |
#393 := [rewrite* #298]: #392
|
|
1701 |
#50 := (ite #32 #42 #44)
|
|
1702 |
#51 := (= #49 #50)
|
|
1703 |
#52 := (forall (vars (?v0 S2)) #51)
|
|
1704 |
#194 := (iff #52 #193)
|
|
1705 |
#191 := (iff #51 #190)
|
|
1706 |
#188 := (= #50 #185)
|
|
1707 |
#182 := (ite #144 #42 #44)
|
|
1708 |
#186 := (= #182 #185)
|
|
1709 |
#187 := [rewrite]: #186
|
|
1710 |
#183 := (= #50 #182)
|
|
1711 |
#184 := [monotonicity #149]: #183
|
|
1712 |
#189 := [trans #184 #187]: #188
|
|
1713 |
#192 := [monotonicity #189]: #191
|
|
1714 |
#195 := [quant-intro #192]: #194
|
|
1715 |
#143 := [asserted]: #52
|
|
1716 |
#196 := [mp #143 #195]: #193
|
|
1717 |
#394 := [mp #196 #393]: #391
|
|
1718 |
#396 := [mp~ #394 #395]: #391
|
|
1719 |
#477 := [mp #396 #476]: #474
|
|
1720 |
#567 := [mp #477 #566]: #562
|
|
1721 |
#628 := (not #562)
|
|
1722 |
#820 := (or #628 #817)
|
|
1723 |
#796 := (= #795 #793)
|
|
1724 |
#798 := (+ #797 #146)
|
|
1725 |
#799 := (>= #798 0::int)
|
|
1726 |
#800 := (ite #799 #796 #794)
|
|
1727 |
#821 := (or #628 #800)
|
|
1728 |
#823 := (iff #821 #820)
|
|
1729 |
#825 := (iff #820 #820)
|
|
1730 |
#826 := [rewrite]: #825
|
|
1731 |
#818 := (iff #800 #817)
|
|
1732 |
#815 := (iff #796 #814)
|
|
1733 |
#816 := [rewrite]: #815
|
|
1734 |
#812 := (iff #799 #809)
|
|
1735 |
#801 := (+ #146 #797)
|
|
1736 |
#804 := (>= #801 0::int)
|
|
1737 |
#810 := (iff #804 #809)
|
|
1738 |
#811 := [rewrite]: #810
|
|
1739 |
#805 := (iff #799 #804)
|
|
1740 |
#802 := (= #798 #801)
|
|
1741 |
#803 := [rewrite]: #802
|
|
1742 |
#806 := [monotonicity #803]: #805
|
|
1743 |
#813 := [trans #806 #811]: #812
|
|
1744 |
#819 := [monotonicity #813 #816]: #818
|
|
1745 |
#824 := [monotonicity #819]: #823
|
|
1746 |
#827 := [trans #824 #826]: #823
|
|
1747 |
#822 := [quant-inst]: #821
|
|
1748 |
#828 := [mp #822 #827]: #820
|
|
1749 |
#1365 := [unit-resolution #828 #567]: #817
|
|
1750 |
#829 := (not #817)
|
|
1751 |
#833 := (or #829 #809 #794)
|
|
1752 |
#834 := [def-axiom]: #833
|
|
1753 |
#1367 := [unit-resolution #834 #1365]: #1366
|
|
1754 |
#1368 := [unit-resolution #1367 #1364]: #809
|
|
1755 |
#984 := (>= #853 0::int)
|
|
1756 |
#1369 := (or #1345 #984)
|
|
1757 |
#1370 := [th-lemma]: #1369
|
|
1758 |
#1371 := [unit-resolution #1370 #1344]: #984
|
|
1759 |
#830 := (not #809)
|
|
1760 |
#1372 := (not #984)
|
|
1761 |
#1373 := (or #1288 #1372 #830)
|
|
1762 |
#1374 := [th-lemma]: #1373
|
|
1763 |
#1375 := [unit-resolution #1374 #1371 #1368]: #1288
|
|
1764 |
#1377 := (not #1288)
|
|
1765 |
#1378 := (or #1285 #1376 #1377)
|
|
1766 |
#1379 := [th-lemma]: #1378
|
|
1767 |
#1381 := [unit-resolution #1379 #1375]: #1380
|
|
1768 |
#1382 := [unit-resolution #1381 #1315]: #1376
|
|
1769 |
#982 := (>= #616 0::int)
|
|
1770 |
#1383 := (or #1318 #982)
|
|
1771 |
#1384 := [th-lemma]: #1383
|
|
1772 |
#1385 := [unit-resolution #1384 #1297]: #982
|
|
1773 |
[th-lemma #1385 #1382 #1341]: false
|
|
1774 |
unsat
|
37156
|
1775 |
ca942f6174c1f53254d5ef1b69b0e75f0d4027d4 208 0
|
36900
|
1776 |
#2 := false
|
|
1777 |
#37 := 0::real
|
|
1778 |
decl f13 :: (-> S6 S7 real)
|
|
1779 |
decl f17 :: S7
|
|
1780 |
#32 := f17
|
|
1781 |
decl f18 :: S6
|
|
1782 |
#34 := f18
|
|
1783 |
#35 := (f13 f18 f17)
|
|
1784 |
decl f14 :: (-> S8 S9 S6)
|
|
1785 |
decl f16 :: S9
|
|
1786 |
#30 := f16
|
|
1787 |
decl f15 :: (-> S2 S8)
|
|
1788 |
decl f5 :: S2
|
|
1789 |
#11 := f5
|
|
1790 |
#29 := (f15 f5)
|
|
1791 |
#31 := (f14 #29 f16)
|
|
1792 |
#33 := (f13 #31 f17)
|
|
1793 |
#96 := -1::real
|
|
1794 |
#107 := (* -1::real #33)
|
|
1795 |
#108 := (+ #107 #35)
|
|
1796 |
#97 := (* -1::real #35)
|
|
1797 |
#98 := (+ #33 #97)
|
|
1798 |
#135 := (>= #98 0::real)
|
|
1799 |
#142 := (ite #135 #98 #108)
|
|
1800 |
#150 := (* -1::real #142)
|
|
1801 |
#383 := (+ #108 #150)
|
|
1802 |
#384 := (<= #383 0::real)
|
|
1803 |
#369 := (= #108 #142)
|
|
1804 |
#136 := (not #135)
|
|
1805 |
decl f3 :: S2
|
|
1806 |
#8 := f3
|
|
1807 |
#47 := (f15 f3)
|
|
1808 |
#48 := (f14 #47 f16)
|
|
1809 |
#49 := (f13 #48 f17)
|
|
1810 |
#172 := (* -1::real #49)
|
|
1811 |
decl f19 :: S6
|
|
1812 |
#41 := f19
|
|
1813 |
#42 := (f13 f19 f17)
|
|
1814 |
#173 := (+ #42 #172)
|
|
1815 |
#116 := (* -1::real #42)
|
|
1816 |
#163 := (+ #116 #49)
|
|
1817 |
#184 := (<= #173 0::real)
|
|
1818 |
#191 := (ite #184 #163 #173)
|
|
1819 |
#199 := (* -1::real #191)
|
|
1820 |
#382 := (+ #173 #199)
|
|
1821 |
#385 := (<= #382 0::real)
|
|
1822 |
#375 := (= #173 #191)
|
|
1823 |
#185 := (not #184)
|
|
1824 |
#386 := [hypothesis]: #184
|
|
1825 |
#394 := (or #136 #185)
|
|
1826 |
#125 := -1/3::real
|
|
1827 |
#126 := (* -1/3::real #42)
|
|
1828 |
#200 := (+ #126 #199)
|
|
1829 |
#123 := 1/3::real
|
|
1830 |
#124 := (* 1/3::real #35)
|
|
1831 |
#201 := (+ #124 #200)
|
|
1832 |
#202 := (<= #201 0::real)
|
|
1833 |
#203 := (not #202)
|
|
1834 |
#44 := 3::real
|
|
1835 |
#43 := (- #35 #42)
|
|
1836 |
#45 := (/ #43 3::real)
|
|
1837 |
#50 := (- #49 #42)
|
|
1838 |
#52 := (- #50)
|
|
1839 |
#51 := (< #50 0::real)
|
|
1840 |
#53 := (ite #51 #52 #50)
|
|
1841 |
#54 := (< #53 #45)
|
|
1842 |
#208 := (iff #54 #203)
|
|
1843 |
#127 := (+ #124 #126)
|
|
1844 |
#166 := (< #163 0::real)
|
|
1845 |
#178 := (ite #166 #173 #163)
|
|
1846 |
#181 := (< #178 #127)
|
|
1847 |
#206 := (iff #181 #203)
|
|
1848 |
#196 := (< #191 #127)
|
|
1849 |
#204 := (iff #196 #203)
|
|
1850 |
#205 := [rewrite]: #204
|
|
1851 |
#197 := (iff #181 #196)
|
|
1852 |
#194 := (= #178 #191)
|
|
1853 |
#188 := (ite #185 #173 #163)
|
|
1854 |
#192 := (= #188 #191)
|
|
1855 |
#193 := [rewrite]: #192
|
|
1856 |
#189 := (= #178 #188)
|
|
1857 |
#186 := (iff #166 #185)
|
|
1858 |
#187 := [rewrite]: #186
|
|
1859 |
#190 := [monotonicity #187]: #189
|
|
1860 |
#195 := [trans #190 #193]: #194
|
|
1861 |
#198 := [monotonicity #195]: #197
|
|
1862 |
#207 := [trans #198 #205]: #206
|
|
1863 |
#182 := (iff #54 #181)
|
|
1864 |
#130 := (= #45 #127)
|
|
1865 |
#117 := (+ #35 #116)
|
|
1866 |
#120 := (/ #117 3::real)
|
|
1867 |
#128 := (= #120 #127)
|
|
1868 |
#129 := [rewrite]: #128
|
|
1869 |
#121 := (= #45 #120)
|
|
1870 |
#118 := (= #43 #117)
|
|
1871 |
#119 := [rewrite]: #118
|
|
1872 |
#122 := [monotonicity #119]: #121
|
|
1873 |
#131 := [trans #122 #129]: #130
|
|
1874 |
#179 := (= #53 #178)
|
|
1875 |
#164 := (= #50 #163)
|
|
1876 |
#165 := [rewrite]: #164
|
|
1877 |
#176 := (= #52 #173)
|
|
1878 |
#169 := (- #163)
|
|
1879 |
#174 := (= #169 #173)
|
|
1880 |
#175 := [rewrite]: #174
|
|
1881 |
#170 := (= #52 #169)
|
|
1882 |
#171 := [monotonicity #165]: #170
|
|
1883 |
#177 := [trans #171 #175]: #176
|
|
1884 |
#167 := (iff #51 #166)
|
|
1885 |
#168 := [monotonicity #165]: #167
|
|
1886 |
#180 := [monotonicity #168 #177 #165]: #179
|
|
1887 |
#183 := [monotonicity #180 #131]: #182
|
|
1888 |
#209 := [trans #183 #207]: #208
|
|
1889 |
#162 := [asserted]: #54
|
|
1890 |
#210 := [mp #162 #209]: #203
|
|
1891 |
#380 := (+ #163 #199)
|
|
1892 |
#381 := (<= #380 0::real)
|
|
1893 |
#374 := (= #163 #191)
|
|
1894 |
#376 := (or #185 #374)
|
|
1895 |
#377 := [def-axiom]: #376
|
|
1896 |
#387 := [unit-resolution #377 #386]: #374
|
|
1897 |
#388 := (not #374)
|
|
1898 |
#389 := (or #388 #381)
|
|
1899 |
#390 := [th-lemma]: #389
|
|
1900 |
#391 := [unit-resolution #390 #387]: #381
|
|
1901 |
#392 := [hypothesis]: #135
|
|
1902 |
#214 := (+ #33 #172)
|
|
1903 |
#215 := (<= #214 0::real)
|
|
1904 |
#55 := (<= #33 #49)
|
|
1905 |
#216 := (iff #55 #215)
|
|
1906 |
#217 := [rewrite]: #216
|
|
1907 |
#211 := [asserted]: #55
|
|
1908 |
#218 := [mp #211 #217]: #215
|
|
1909 |
#393 := [th-lemma #218 #392 #391 #210 #386]: false
|
|
1910 |
#395 := [lemma #393]: #394
|
|
1911 |
#396 := [unit-resolution #395 #386]: #136
|
|
1912 |
#151 := (+ #126 #150)
|
|
1913 |
#152 := (+ #124 #151)
|
|
1914 |
#153 := (<= #152 0::real)
|
|
1915 |
#154 := (not #153)
|
|
1916 |
#36 := (- #33 #35)
|
|
1917 |
#39 := (- #36)
|
|
1918 |
#38 := (< #36 0::real)
|
|
1919 |
#40 := (ite #38 #39 #36)
|
|
1920 |
#46 := (< #40 #45)
|
|
1921 |
#159 := (iff #46 #154)
|
|
1922 |
#101 := (< #98 0::real)
|
|
1923 |
#113 := (ite #101 #108 #98)
|
|
1924 |
#132 := (< #113 #127)
|
|
1925 |
#157 := (iff #132 #154)
|
|
1926 |
#147 := (< #142 #127)
|
|
1927 |
#155 := (iff #147 #154)
|
|
1928 |
#156 := [rewrite]: #155
|
|
1929 |
#148 := (iff #132 #147)
|
|
1930 |
#145 := (= #113 #142)
|
|
1931 |
#139 := (ite #136 #108 #98)
|
|
1932 |
#143 := (= #139 #142)
|
|
1933 |
#144 := [rewrite]: #143
|
|
1934 |
#140 := (= #113 #139)
|
|
1935 |
#137 := (iff #101 #136)
|
|
1936 |
#138 := [rewrite]: #137
|
|
1937 |
#141 := [monotonicity #138]: #140
|
|
1938 |
#146 := [trans #141 #144]: #145
|
|
1939 |
#149 := [monotonicity #146]: #148
|
|
1940 |
#158 := [trans #149 #156]: #157
|
|
1941 |
#133 := (iff #46 #132)
|
|
1942 |
#114 := (= #40 #113)
|
|
1943 |
#99 := (= #36 #98)
|
|
1944 |
#100 := [rewrite]: #99
|
|
1945 |
#111 := (= #39 #108)
|
|
1946 |
#104 := (- #98)
|
|
1947 |
#109 := (= #104 #108)
|
|
1948 |
#110 := [rewrite]: #109
|
|
1949 |
#105 := (= #39 #104)
|
|
1950 |
#106 := [monotonicity #100]: #105
|
|
1951 |
#112 := [trans #106 #110]: #111
|
|
1952 |
#102 := (iff #38 #101)
|
|
1953 |
#103 := [monotonicity #100]: #102
|
|
1954 |
#115 := [monotonicity #103 #112 #100]: #114
|
|
1955 |
#134 := [monotonicity #115 #131]: #133
|
|
1956 |
#160 := [trans #134 #158]: #159
|
|
1957 |
#95 := [asserted]: #46
|
|
1958 |
#161 := [mp #95 #160]: #154
|
|
1959 |
#372 := (or #135 #369)
|
|
1960 |
#373 := [def-axiom]: #372
|
|
1961 |
#397 := [unit-resolution #373 #396]: #369
|
|
1962 |
#398 := (not #369)
|
|
1963 |
#399 := (or #398 #384)
|
|
1964 |
#400 := [th-lemma]: #399
|
|
1965 |
#401 := [unit-resolution #400 #397]: #384
|
|
1966 |
#402 := [th-lemma #401 #161 #391 #210 #218 #396]: false
|
|
1967 |
#403 := [lemma #402]: #185
|
|
1968 |
#378 := (or #184 #375)
|
|
1969 |
#379 := [def-axiom]: #378
|
|
1970 |
#406 := [unit-resolution #379 #403]: #375
|
|
1971 |
#407 := (not #375)
|
|
1972 |
#408 := (or #407 #385)
|
|
1973 |
#409 := [th-lemma]: #408
|
|
1974 |
#410 := [unit-resolution #409 #406]: #385
|
|
1975 |
#412 := (not #215)
|
|
1976 |
#411 := (not #385)
|
|
1977 |
#413 := (or #136 #411 #412 #202 #184)
|
|
1978 |
#414 := [th-lemma]: #413
|
|
1979 |
#415 := [unit-resolution #414 #403 #210 #218 #410]: #136
|
|
1980 |
#416 := [unit-resolution #373 #415]: #369
|
|
1981 |
#417 := [unit-resolution #400 #416]: #384
|
|
1982 |
[th-lemma #410 #218 #210 #403 #161 #417]: false
|
|
1983 |
unsat
|
37156
|
1984 |
504ce5f4f6961a0f59840c0aa303f063d46936a5 333 0
|
36900
|
1985 |
#2 := false
|
|
1986 |
#11 := 0::real
|
|
1987 |
decl ?v2!1 :: real
|
|
1988 |
#225 := ?v2!1
|
|
1989 |
decl ?v1!2 :: real
|
|
1990 |
#223 := ?v1!2
|
|
1991 |
#45 := -1::real
|
|
1992 |
#238 := (* -1::real ?v1!2)
|
|
1993 |
#260 := (+ #238 ?v2!1)
|
|
1994 |
#240 := (* -1::real ?v2!1)
|
|
1995 |
#266 := (+ ?v1!2 #240)
|
|
1996 |
#267 := (>= #266 0::real)
|
|
1997 |
#274 := (ite #267 #266 #260)
|
|
1998 |
#277 := (* -1::real #274)
|
|
1999 |
#74 := -1/3::real
|
|
2000 |
#233 := (* -1/3::real ?v2!1)
|
|
2001 |
#280 := (+ #233 #277)
|
|
2002 |
decl ?v3!0 :: real
|
|
2003 |
#224 := ?v3!0
|
|
2004 |
#72 := 1/3::real
|
|
2005 |
#235 := (* 1/3::real ?v3!0)
|
|
2006 |
#283 := (+ #235 #280)
|
|
2007 |
#286 := (<= #283 0::real)
|
|
2008 |
#302 := (not #286)
|
|
2009 |
decl ?v0!3 :: real
|
|
2010 |
#221 := ?v0!3
|
|
2011 |
#248 := (+ ?v0!3 #238)
|
|
2012 |
#249 := (<= #248 0::real)
|
|
2013 |
#250 := (not #249)
|
|
2014 |
#226 := (* -1::real ?v0!3)
|
|
2015 |
#227 := (+ #226 ?v3!0)
|
|
2016 |
#228 := (* -1::real ?v3!0)
|
|
2017 |
#229 := (+ ?v0!3 #228)
|
|
2018 |
#230 := (>= #229 0::real)
|
|
2019 |
#231 := (ite #230 #229 #227)
|
|
2020 |
#232 := (* -1::real #231)
|
|
2021 |
#234 := (+ #233 #232)
|
|
2022 |
#236 := (+ #235 #234)
|
|
2023 |
#237 := (<= #236 0::real)
|
|
2024 |
#292 := (or #237 #250 #286)
|
|
2025 |
#297 := (not #292)
|
|
2026 |
#239 := (+ ?v2!1 #238)
|
|
2027 |
#241 := (+ #240 ?v1!2)
|
|
2028 |
#242 := (<= #239 0::real)
|
|
2029 |
#243 := (ite #242 #241 #239)
|
|
2030 |
#244 := (* -1::real #243)
|
|
2031 |
#245 := (+ #233 #244)
|
|
2032 |
#246 := (+ #235 #245)
|
|
2033 |
#247 := (<= #246 0::real)
|
|
2034 |
#251 := (or #250 #247 #237)
|
|
2035 |
#252 := (not #251)
|
|
2036 |
#298 := (iff #252 #297)
|
|
2037 |
#295 := (iff #251 #292)
|
|
2038 |
#289 := (or #250 #286 #237)
|
|
2039 |
#293 := (iff #289 #292)
|
|
2040 |
#294 := [rewrite]: #293
|
|
2041 |
#290 := (iff #251 #289)
|
|
2042 |
#287 := (iff #247 #286)
|
|
2043 |
#284 := (= #246 #283)
|
|
2044 |
#281 := (= #245 #280)
|
|
2045 |
#278 := (= #244 #277)
|
|
2046 |
#275 := (= #243 #274)
|
|
2047 |
#261 := (= #239 #260)
|
|
2048 |
#262 := [rewrite]: #261
|
|
2049 |
#272 := (= #241 #266)
|
|
2050 |
#273 := [rewrite]: #272
|
|
2051 |
#270 := (iff #242 #267)
|
|
2052 |
#263 := (<= #260 0::real)
|
|
2053 |
#268 := (iff #263 #267)
|
|
2054 |
#269 := [rewrite]: #268
|
|
2055 |
#264 := (iff #242 #263)
|
|
2056 |
#265 := [monotonicity #262]: #264
|
|
2057 |
#271 := [trans #265 #269]: #270
|
|
2058 |
#276 := [monotonicity #271 #273 #262]: #275
|
|
2059 |
#279 := [monotonicity #276]: #278
|
|
2060 |
#282 := [monotonicity #279]: #281
|
|
2061 |
#285 := [monotonicity #282]: #284
|
|
2062 |
#288 := [monotonicity #285]: #287
|
|
2063 |
#291 := [monotonicity #288]: #290
|
|
2064 |
#296 := [trans #291 #294]: #295
|
|
2065 |
#299 := [monotonicity #296]: #298
|
|
2066 |
#9 := (:var 0 real)
|
|
2067 |
#8 := (:var 3 real)
|
|
2068 |
#56 := (* -1::real #8)
|
|
2069 |
#57 := (+ #56 #9)
|
|
2070 |
#46 := (* -1::real #9)
|
|
2071 |
#47 := (+ #8 #46)
|
|
2072 |
#170 := (>= #47 0::real)
|
|
2073 |
#177 := (ite #170 #47 #57)
|
|
2074 |
#185 := (* -1::real #177)
|
|
2075 |
#15 := (:var 1 real)
|
|
2076 |
#75 := (* -1/3::real #15)
|
|
2077 |
#186 := (+ #75 #185)
|
|
2078 |
#73 := (* 1/3::real #9)
|
|
2079 |
#187 := (+ #73 #186)
|
|
2080 |
#188 := (<= #187 0::real)
|
|
2081 |
#20 := (:var 2 real)
|
|
2082 |
#93 := (* -1::real #20)
|
|
2083 |
#94 := (+ #15 #93)
|
|
2084 |
#65 := (* -1::real #15)
|
|
2085 |
#84 := (+ #65 #20)
|
|
2086 |
#139 := (<= #94 0::real)
|
|
2087 |
#146 := (ite #139 #84 #94)
|
|
2088 |
#154 := (* -1::real #146)
|
|
2089 |
#155 := (+ #75 #154)
|
|
2090 |
#156 := (+ #73 #155)
|
|
2091 |
#157 := (<= #156 0::real)
|
|
2092 |
#132 := (+ #8 #93)
|
|
2093 |
#133 := (<= #132 0::real)
|
|
2094 |
#136 := (not #133)
|
|
2095 |
#207 := (or #136 #157 #188)
|
|
2096 |
#212 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #207)
|
|
2097 |
#215 := (not #212)
|
|
2098 |
#253 := (~ #215 #252)
|
|
2099 |
#254 := [sk]: #253
|
|
2100 |
#26 := (<= #8 #20)
|
|
2101 |
#27 := (implies #26 false)
|
|
2102 |
#17 := 3::real
|
|
2103 |
#16 := (- #9 #15)
|
|
2104 |
#18 := (/ #16 3::real)
|
|
2105 |
#21 := (- #20 #15)
|
|
2106 |
#23 := (- #21)
|
|
2107 |
#22 := (< #21 0::real)
|
|
2108 |
#24 := (ite #22 #23 #21)
|
|
2109 |
#25 := (< #24 #18)
|
|
2110 |
#28 := (implies #25 #27)
|
|
2111 |
#10 := (- #8 #9)
|
|
2112 |
#13 := (- #10)
|
|
2113 |
#12 := (< #10 0::real)
|
|
2114 |
#14 := (ite #12 #13 #10)
|
|
2115 |
#19 := (< #14 #18)
|
|
2116 |
#29 := (implies #19 #28)
|
|
2117 |
#30 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #29)
|
|
2118 |
#31 := (not #30)
|
|
2119 |
#218 := (iff #31 #215)
|
|
2120 |
#76 := (+ #73 #75)
|
|
2121 |
#87 := (< #84 0::real)
|
|
2122 |
#99 := (ite #87 #94 #84)
|
|
2123 |
#102 := (< #99 #76)
|
|
2124 |
#111 := (not #102)
|
|
2125 |
#105 := (not #26)
|
|
2126 |
#112 := (or #105 #111)
|
|
2127 |
#50 := (< #47 0::real)
|
|
2128 |
#62 := (ite #50 #57 #47)
|
|
2129 |
#81 := (< #62 #76)
|
|
2130 |
#120 := (not #81)
|
|
2131 |
#121 := (or #120 #112)
|
|
2132 |
#126 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real)) #121)
|
|
2133 |
#129 := (not #126)
|
|
2134 |
#216 := (iff #129 #215)
|
|
2135 |
#213 := (iff #126 #212)
|
|
2136 |
#210 := (iff #121 #207)
|
|
2137 |
#201 := (or #136 #157)
|
|
2138 |
#204 := (or #188 #201)
|
|
2139 |
#208 := (iff #204 #207)
|
|
2140 |
#209 := [rewrite]: #208
|
|
2141 |
#205 := (iff #121 #204)
|
|
2142 |
#202 := (iff #112 #201)
|
|
2143 |
#168 := (iff #111 #157)
|
|
2144 |
#158 := (not #157)
|
|
2145 |
#163 := (not #158)
|
|
2146 |
#166 := (iff #163 #157)
|
|
2147 |
#167 := [rewrite]: #166
|
|
2148 |
#164 := (iff #111 #163)
|
|
2149 |
#161 := (iff #102 #158)
|
|
2150 |
#151 := (< #146 #76)
|
|
2151 |
#159 := (iff #151 #158)
|
|
2152 |
#160 := [rewrite]: #159
|
|
2153 |
#152 := (iff #102 #151)
|
|
2154 |
#149 := (= #99 #146)
|
|
2155 |
#140 := (not #139)
|
|
2156 |
#143 := (ite #140 #94 #84)
|
|
2157 |
#147 := (= #143 #146)
|
|
2158 |
#148 := [rewrite]: #147
|
|
2159 |
#144 := (= #99 #143)
|
|
2160 |
#141 := (iff #87 #140)
|
|
2161 |
#142 := [rewrite]: #141
|
|
2162 |
#145 := [monotonicity #142]: #144
|
|
2163 |
#150 := [trans #145 #148]: #149
|
|
2164 |
#153 := [monotonicity #150]: #152
|
|
2165 |
#162 := [trans #153 #160]: #161
|
|
2166 |
#165 := [monotonicity #162]: #164
|
|
2167 |
#169 := [trans #165 #167]: #168
|
|
2168 |
#137 := (iff #105 #136)
|
|
2169 |
#134 := (iff #26 #133)
|
|
2170 |
#135 := [rewrite]: #134
|
|
2171 |
#138 := [monotonicity #135]: #137
|
|
2172 |
#203 := [monotonicity #138 #169]: #202
|
|
2173 |
#199 := (iff #120 #188)
|
|
2174 |
#189 := (not #188)
|
|
2175 |
#194 := (not #189)
|
|
2176 |
#197 := (iff #194 #188)
|
|
2177 |
#198 := [rewrite]: #197
|
|
2178 |
#195 := (iff #120 #194)
|
|
2179 |
#192 := (iff #81 #189)
|
|
2180 |
#182 := (< #177 #76)
|
|
2181 |
#190 := (iff #182 #189)
|
|
2182 |
#191 := [rewrite]: #190
|
|
2183 |
#183 := (iff #81 #182)
|
|
2184 |
#180 := (= #62 #177)
|
|
2185 |
#171 := (not #170)
|
|
2186 |
#174 := (ite #171 #57 #47)
|
|
2187 |
#178 := (= #174 #177)
|
|
2188 |
#179 := [rewrite]: #178
|
|
2189 |
#175 := (= #62 #174)
|
|
2190 |
#172 := (iff #50 #171)
|
|
2191 |
#173 := [rewrite]: #172
|
|
2192 |
#176 := [monotonicity #173]: #175
|
|
2193 |
#181 := [trans #176 #179]: #180
|
|
2194 |
#184 := [monotonicity #181]: #183
|
|
2195 |
#193 := [trans #184 #191]: #192
|
|
2196 |
#196 := [monotonicity #193]: #195
|
|
2197 |
#200 := [trans #196 #198]: #199
|
|
2198 |
#206 := [monotonicity #200 #203]: #205
|
|
2199 |
#211 := [trans #206 #209]: #210
|
|
2200 |
#214 := [quant-intro #211]: #213
|
|
2201 |
#217 := [monotonicity #214]: #216
|
|
2202 |
#130 := (iff #31 #129)
|
|
2203 |
#127 := (iff #30 #126)
|
|
2204 |
#124 := (iff #29 #121)
|
|
2205 |
#117 := (implies #81 #112)
|
|
2206 |
#122 := (iff #117 #121)
|
|
2207 |
#123 := [rewrite]: #122
|
|
2208 |
#118 := (iff #29 #117)
|
|
2209 |
#115 := (iff #28 #112)
|
|
2210 |
#108 := (implies #102 #105)
|
|
2211 |
#113 := (iff #108 #112)
|
|
2212 |
#114 := [rewrite]: #113
|
|
2213 |
#109 := (iff #28 #108)
|
|
2214 |
#106 := (iff #27 #105)
|
|
2215 |
#107 := [rewrite]: #106
|
|
2216 |
#103 := (iff #25 #102)
|
|
2217 |
#79 := (= #18 #76)
|
|
2218 |
#66 := (+ #9 #65)
|
|
2219 |
#69 := (/ #66 3::real)
|
|
2220 |
#77 := (= #69 #76)
|
|
2221 |
#78 := [rewrite]: #77
|
|
2222 |
#70 := (= #18 #69)
|
|
2223 |
#67 := (= #16 #66)
|
|
2224 |
#68 := [rewrite]: #67
|
|
2225 |
#71 := [monotonicity #68]: #70
|
|
2226 |
#80 := [trans #71 #78]: #79
|
|
2227 |
#100 := (= #24 #99)
|
|
2228 |
#85 := (= #21 #84)
|
|
2229 |
#86 := [rewrite]: #85
|
|
2230 |
#97 := (= #23 #94)
|
|
2231 |
#90 := (- #84)
|
|
2232 |
#95 := (= #90 #94)
|
|
2233 |
#96 := [rewrite]: #95
|
|
2234 |
#91 := (= #23 #90)
|
|
2235 |
#92 := [monotonicity #86]: #91
|
|
2236 |
#98 := [trans #92 #96]: #97
|
|
2237 |
#88 := (iff #22 #87)
|
|
2238 |
#89 := [monotonicity #86]: #88
|
|
2239 |
#101 := [monotonicity #89 #98 #86]: #100
|
|
2240 |
#104 := [monotonicity #101 #80]: #103
|
|
2241 |
#110 := [monotonicity #104 #107]: #109
|
|
2242 |
#116 := [trans #110 #114]: #115
|
|
2243 |
#82 := (iff #19 #81)
|
|
2244 |
#63 := (= #14 #62)
|
|
2245 |
#48 := (= #10 #47)
|
|
2246 |
#49 := [rewrite]: #48
|
|
2247 |
#60 := (= #13 #57)
|
|
2248 |
#53 := (- #47)
|
|
2249 |
#58 := (= #53 #57)
|
|
2250 |
#59 := [rewrite]: #58
|
|
2251 |
#54 := (= #13 #53)
|
|
2252 |
#55 := [monotonicity #49]: #54
|
|
2253 |
#61 := [trans #55 #59]: #60
|
|
2254 |
#51 := (iff #12 #50)
|
|
2255 |
#52 := [monotonicity #49]: #51
|
|
2256 |
#64 := [monotonicity #52 #61 #49]: #63
|
|
2257 |
#83 := [monotonicity #64 #80]: #82
|
|
2258 |
#119 := [monotonicity #83 #116]: #118
|
|
2259 |
#125 := [trans #119 #123]: #124
|
|
2260 |
#128 := [quant-intro #125]: #127
|
|
2261 |
#131 := [monotonicity #128]: #130
|
|
2262 |
#219 := [trans #131 #217]: #218
|
|
2263 |
#44 := [asserted]: #31
|
|
2264 |
#220 := [mp #44 #219]: #215
|
|
2265 |
#257 := [mp~ #220 #254]: #252
|
|
2266 |
#258 := [mp #257 #299]: #297
|
|
2267 |
#303 := [not-or-elim #258]: #302
|
|
2268 |
#301 := [not-or-elim #258]: #249
|
|
2269 |
#259 := (not #237)
|
|
2270 |
#300 := [not-or-elim #258]: #259
|
|
2271 |
#376 := (+ #227 #232)
|
|
2272 |
#377 := (<= #376 0::real)
|
|
2273 |
#360 := (= #227 #231)
|
|
2274 |
#361 := (not #230)
|
|
2275 |
#368 := (not #267)
|
|
2276 |
#379 := [hypothesis]: #368
|
|
2277 |
#387 := (or #361 #267)
|
|
2278 |
#373 := (+ #260 #277)
|
|
2279 |
#374 := (<= #373 0::real)
|
|
2280 |
#367 := (= #260 #274)
|
|
2281 |
#371 := (or #267 #367)
|
|
2282 |
#372 := [def-axiom]: #371
|
|
2283 |
#380 := [unit-resolution #372 #379]: #367
|
|
2284 |
#381 := (not #367)
|
|
2285 |
#382 := (or #381 #374)
|
|
2286 |
#383 := [th-lemma]: #382
|
|
2287 |
#384 := [unit-resolution #383 #380]: #374
|
|
2288 |
#385 := [hypothesis]: #230
|
|
2289 |
#386 := [th-lemma #385 #384 #303 #379 #301]: false
|
|
2290 |
#388 := [lemma #386]: #387
|
|
2291 |
#389 := [unit-resolution #388 #379]: #361
|
|
2292 |
#364 := (or #230 #360)
|
|
2293 |
#365 := [def-axiom]: #364
|
|
2294 |
#390 := [unit-resolution #365 #389]: #360
|
|
2295 |
#391 := (not #360)
|
|
2296 |
#392 := (or #391 #377)
|
|
2297 |
#393 := [th-lemma]: #392
|
|
2298 |
#394 := [unit-resolution #393 #390]: #377
|
|
2299 |
#395 := [th-lemma #384 #303 #379 #394 #300 #301]: false
|
|
2300 |
#396 := [lemma #395]: #267
|
|
2301 |
#399 := [hypothesis]: #361
|
|
2302 |
#400 := [unit-resolution #365 #399]: #360
|
|
2303 |
#401 := [unit-resolution #393 #400]: #377
|
|
2304 |
#375 := (+ #266 #277)
|
|
2305 |
#378 := (<= #375 0::real)
|
|
2306 |
#366 := (= #266 #274)
|
|
2307 |
#369 := (or #368 #366)
|
|
2308 |
#370 := [def-axiom]: #369
|
|
2309 |
#402 := [unit-resolution #370 #396]: #366
|
|
2310 |
#403 := (not #366)
|
|
2311 |
#404 := (or #403 #378)
|
|
2312 |
#405 := [th-lemma]: #404
|
|
2313 |
#406 := [unit-resolution #405 #402]: #378
|
|
2314 |
#407 := [th-lemma #406 #301 #401 #300 #399 #303]: false
|
|
2315 |
#408 := [lemma #407]: #230
|
|
2316 |
[th-lemma #406 #301 #408 #396 #303]: false
|
|
2317 |
unsat
|
37156
|
2318 |
024080ea9e6de105c72225d6d55cc8b136a93933 165 0
|
36900
|
2319 |
#2 := false
|
|
2320 |
#22 := 0::real
|
|
2321 |
decl f3 :: (-> S3 S2 real)
|
|
2322 |
decl ?v0!0 :: S2
|
|
2323 |
#118 := ?v0!0
|
|
2324 |
decl f5 :: S3
|
|
2325 |
#11 := f5
|
|
2326 |
#119 := (f3 f5 ?v0!0)
|
|
2327 |
#49 := -1::real
|
|
2328 |
#117 := (* -1::real #119)
|
|
2329 |
decl f4 :: S3
|
|
2330 |
#8 := f4
|
|
2331 |
#115 := (f3 f4 ?v0!0)
|
|
2332 |
#120 := (+ #115 #117)
|
|
2333 |
#121 := (>= #120 0::real)
|
|
2334 |
decl f6 :: (-> S2 S4 S1)
|
|
2335 |
decl f7 :: (-> S4 S4 S4)
|
|
2336 |
decl f9 :: (-> S2 S4 S4)
|
|
2337 |
decl f11 :: S4
|
|
2338 |
#17 := f11
|
|
2339 |
decl f10 :: S2
|
|
2340 |
#16 := f10
|
|
2341 |
#18 := (f9 f10 f11)
|
|
2342 |
decl f8 :: S4
|
|
2343 |
#15 := f8
|
|
2344 |
#19 := (f7 f8 #18)
|
|
2345 |
#123 := (f6 ?v0!0 #19)
|
|
2346 |
decl f1 :: S1
|
|
2347 |
#4 := f1
|
|
2348 |
#124 := (= f1 #123)
|
|
2349 |
#9 := (:var 0 S2)
|
|
2350 |
#12 := (f3 f5 #9)
|
|
2351 |
#81 := (* -1::real #12)
|
|
2352 |
#10 := (f3 f4 #9)
|
|
2353 |
#82 := (+ #10 #81)
|
|
2354 |
#83 := (>= #82 0::real)
|
|
2355 |
#84 := (not #83)
|
|
2356 |
#89 := (forall (vars (?v1 S2)) #84)
|
|
2357 |
#158 := (and #89 #121 #124)
|
|
2358 |
#122 := (not #121)
|
|
2359 |
#133 := (not #122)
|
|
2360 |
#125 := (not #124)
|
|
2361 |
#130 := (not #125)
|
|
2362 |
#143 := (and #130 #133 #89)
|
|
2363 |
#161 := (iff #143 #158)
|
|
2364 |
#155 := (and #124 #121 #89)
|
|
2365 |
#159 := (iff #155 #158)
|
|
2366 |
#160 := [rewrite]: #159
|
|
2367 |
#156 := (iff #143 #155)
|
|
2368 |
#153 := (iff #133 #121)
|
|
2369 |
#154 := [rewrite]: #153
|
|
2370 |
#151 := (iff #130 #124)
|
|
2371 |
#152 := [rewrite]: #151
|
|
2372 |
#157 := [monotonicity #152 #154]: #156
|
|
2373 |
#162 := [trans #157 #160]: #161
|
|
2374 |
#92 := (not #89)
|
|
2375 |
#20 := (f6 #9 #19)
|
|
2376 |
#46 := (= f1 #20)
|
|
2377 |
#60 := (not #46)
|
|
2378 |
#101 := (or #60 #84 #92)
|
|
2379 |
#106 := (forall (vars (?v0 S2)) #101)
|
|
2380 |
#109 := (not #106)
|
|
2381 |
#146 := (~ #109 #143)
|
|
2382 |
#126 := (or #125 #122 #92)
|
|
2383 |
#127 := (not #126)
|
|
2384 |
#144 := (~ #127 #143)
|
|
2385 |
#140 := (not #92)
|
|
2386 |
#141 := (~ #140 #89)
|
|
2387 |
#138 := (~ #89 #89)
|
|
2388 |
#136 := (~ #84 #84)
|
|
2389 |
#137 := [refl]: #136
|
|
2390 |
#139 := [nnf-pos #137]: #138
|
|
2391 |
#142 := [nnf-neg #139]: #141
|
|
2392 |
#134 := (~ #133 #133)
|
|
2393 |
#135 := [refl]: #134
|
|
2394 |
#131 := (~ #130 #130)
|
|
2395 |
#132 := [refl]: #131
|
|
2396 |
#145 := [nnf-neg #132 #135 #142]: #144
|
|
2397 |
#128 := (~ #109 #127)
|
|
2398 |
#129 := [sk]: #128
|
|
2399 |
#147 := [trans #129 #145]: #146
|
|
2400 |
#23 := (- #12 #10)
|
|
2401 |
#24 := (< 0::real #23)
|
|
2402 |
#21 := (= #20 f1)
|
|
2403 |
#25 := (implies #21 #24)
|
|
2404 |
#13 := (< #10 #12)
|
|
2405 |
#14 := (forall (vars (?v1 S2)) #13)
|
|
2406 |
#26 := (implies #14 #25)
|
|
2407 |
#27 := (forall (vars (?v0 S2)) #26)
|
|
2408 |
#28 := (not #27)
|
|
2409 |
#112 := (iff #28 #109)
|
|
2410 |
#50 := (* -1::real #10)
|
|
2411 |
#51 := (+ #50 #12)
|
|
2412 |
#54 := (< 0::real #51)
|
|
2413 |
#61 := (or #60 #54)
|
|
2414 |
#69 := (not #14)
|
|
2415 |
#70 := (or #69 #61)
|
|
2416 |
#75 := (forall (vars (?v0 S2)) #70)
|
|
2417 |
#78 := (not #75)
|
|
2418 |
#110 := (iff #78 #109)
|
|
2419 |
#107 := (iff #75 #106)
|
|
2420 |
#104 := (iff #70 #101)
|
|
2421 |
#95 := (or #60 #84)
|
|
2422 |
#98 := (or #92 #95)
|
|
2423 |
#102 := (iff #98 #101)
|
|
2424 |
#103 := [rewrite]: #102
|
|
2425 |
#99 := (iff #70 #98)
|
|
2426 |
#96 := (iff #61 #95)
|
|
2427 |
#85 := (iff #54 #84)
|
|
2428 |
#86 := [rewrite]: #85
|
|
2429 |
#97 := [monotonicity #86]: #96
|
|
2430 |
#93 := (iff #69 #92)
|
|
2431 |
#90 := (iff #14 #89)
|
|
2432 |
#87 := (iff #13 #84)
|
|
2433 |
#88 := [rewrite]: #87
|
|
2434 |
#91 := [quant-intro #88]: #90
|
|
2435 |
#94 := [monotonicity #91]: #93
|
|
2436 |
#100 := [monotonicity #94 #97]: #99
|
|
2437 |
#105 := [trans #100 #103]: #104
|
|
2438 |
#108 := [quant-intro #105]: #107
|
|
2439 |
#111 := [monotonicity #108]: #110
|
|
2440 |
#79 := (iff #28 #78)
|
|
2441 |
#76 := (iff #27 #75)
|
|
2442 |
#73 := (iff #26 #70)
|
|
2443 |
#66 := (implies #14 #61)
|
|
2444 |
#71 := (iff #66 #70)
|
|
2445 |
#72 := [rewrite]: #71
|
|
2446 |
#67 := (iff #26 #66)
|
|
2447 |
#64 := (iff #25 #61)
|
|
2448 |
#57 := (implies #46 #54)
|
|
2449 |
#62 := (iff #57 #61)
|
|
2450 |
#63 := [rewrite]: #62
|
|
2451 |
#58 := (iff #25 #57)
|
|
2452 |
#55 := (iff #24 #54)
|
|
2453 |
#52 := (= #23 #51)
|
|
2454 |
#53 := [rewrite]: #52
|
|
2455 |
#56 := [monotonicity #53]: #55
|
|
2456 |
#47 := (iff #21 #46)
|
|
2457 |
#48 := [rewrite]: #47
|
|
2458 |
#59 := [monotonicity #48 #56]: #58
|
|
2459 |
#65 := [trans #59 #63]: #64
|
|
2460 |
#68 := [monotonicity #65]: #67
|
|
2461 |
#74 := [trans #68 #72]: #73
|
|
2462 |
#77 := [quant-intro #74]: #76
|
|
2463 |
#80 := [monotonicity #77]: #79
|
|
2464 |
#113 := [trans #80 #111]: #112
|
|
2465 |
#45 := [asserted]: #28
|
|
2466 |
#114 := [mp #45 #113]: #109
|
|
2467 |
#148 := [mp~ #114 #147]: #143
|
|
2468 |
#149 := [mp #148 #162]: #158
|
|
2469 |
#163 := [and-elim #149]: #121
|
|
2470 |
#223 := (pattern #12)
|
|
2471 |
#222 := (pattern #10)
|
|
2472 |
#224 := (forall (vars (?v1 S2)) (:pat #222 #223) #84)
|
|
2473 |
#227 := (iff #89 #224)
|
|
2474 |
#225 := (iff #84 #84)
|
|
2475 |
#226 := [refl]: #225
|
|
2476 |
#228 := [quant-intro #226]: #227
|
|
2477 |
#150 := [and-elim #149]: #89
|
|
2478 |
#229 := [mp #150 #228]: #224
|
|
2479 |
#232 := (not #224)
|
|
2480 |
#233 := (or #232 #122)
|
|
2481 |
#234 := [quant-inst]: #233
|
|
2482 |
[unit-resolution #234 #229 #163]: false
|
|
2483 |
unsat
|
37156
|
2484 |
116b1dd4c85396a326f34f6c1266b1ad85116049 57 0
|
36900
|
2485 |
#2 := false
|
|
2486 |
decl f13 :: (-> S4 S4 S5)
|
|
2487 |
#44 := (:var 0 S4)
|
|
2488 |
#43 := (:var 1 S4)
|
|
2489 |
#45 := (f13 #43 #44)
|
|
2490 |
#252 := (pattern #45)
|
|
2491 |
#39 := 0::real
|
|
2492 |
decl f12 :: (-> S5 real)
|
|
2493 |
#46 := (f12 #45)
|
|
2494 |
#133 := (>= #46 0::real)
|
|
2495 |
#253 := (forall (vars (?v0 S4) (?v1 S4)) (:pat #252) #133)
|
|
2496 |
#135 := (forall (vars (?v0 S4) (?v1 S4)) #133)
|
|
2497 |
#256 := (iff #135 #253)
|
|
2498 |
#254 := (iff #133 #133)
|
|
2499 |
#255 := [refl]: #254
|
|
2500 |
#257 := [quant-intro #255]: #256
|
|
2501 |
#150 := (~ #135 #135)
|
|
2502 |
#139 := (~ #133 #133)
|
|
2503 |
#130 := [refl]: #139
|
|
2504 |
#151 := [nnf-pos #130]: #150
|
|
2505 |
#47 := (<= 0::real #46)
|
|
2506 |
#48 := (forall (vars (?v0 S4) (?v1 S4)) #47)
|
|
2507 |
#136 := (iff #48 #135)
|
|
2508 |
#132 := (iff #47 #133)
|
|
2509 |
#134 := [rewrite]: #132
|
|
2510 |
#137 := [quant-intro #134]: #136
|
|
2511 |
#129 := [asserted]: #48
|
|
2512 |
#138 := [mp #129 #137]: #135
|
|
2513 |
#152 := [mp~ #138 #151]: #135
|
|
2514 |
#258 := [mp #152 #257]: #253
|
|
2515 |
decl f14 :: (-> S3 S4)
|
|
2516 |
decl f4 :: S3
|
|
2517 |
#8 := f4
|
|
2518 |
#36 := (f14 f4)
|
|
2519 |
decl f10 :: S3
|
|
2520 |
#24 := f10
|
|
2521 |
#35 := (f14 f10)
|
|
2522 |
#37 := (f13 #35 #36)
|
|
2523 |
#38 := (f12 #37)
|
|
2524 |
#259 := (>= #38 0::real)
|
|
2525 |
#261 := (not #259)
|
|
2526 |
#41 := (= #38 0::real)
|
|
2527 |
#42 := (not #41)
|
|
2528 |
#128 := [asserted]: #42
|
|
2529 |
#267 := (or #41 #261)
|
|
2530 |
#40 := (<= #38 0::real)
|
|
2531 |
#127 := [asserted]: #40
|
|
2532 |
#260 := (not #40)
|
|
2533 |
#265 := (or #41 #260 #261)
|
|
2534 |
#266 := [th-lemma]: #265
|
|
2535 |
#268 := [unit-resolution #266 #127]: #267
|
|
2536 |
#269 := [unit-resolution #268 #128]: #261
|
|
2537 |
#262 := (not #253)
|
|
2538 |
#263 := (or #262 #259)
|
|
2539 |
#264 := [quant-inst]: #263
|
|
2540 |
[unit-resolution #264 #269 #258]: false
|
|
2541 |
unsat
|
37156
|
2542 |
74073317ccefcdf35878e5154f8155d12c8475cf 91 0
|
36900
|
2543 |
#2 := false
|
|
2544 |
#43 := 0::real
|
|
2545 |
decl f3 :: (-> S2 S3 real)
|
|
2546 |
decl f5 :: S3
|
|
2547 |
#9 := f5
|
|
2548 |
decl f6 :: S2
|
|
2549 |
#11 := f6
|
|
2550 |
#12 := (f3 f6 f5)
|
|
2551 |
#40 := -1::real
|
|
2552 |
#41 := (* -1::real #12)
|
|
2553 |
decl f4 :: S2
|
|
2554 |
#8 := f4
|
|
2555 |
#10 := (f3 f4 f5)
|
|
2556 |
#42 := (+ #10 #41)
|
|
2557 |
#135 := (>= #42 0::real)
|
|
2558 |
#160 := (not #135)
|
|
2559 |
#48 := (= #10 #12)
|
|
2560 |
#60 := (not #48)
|
|
2561 |
#19 := (= #12 #10)
|
|
2562 |
#20 := (not #19)
|
|
2563 |
#61 := (iff #20 #60)
|
|
2564 |
#58 := (iff #19 #48)
|
|
2565 |
#59 := [rewrite]: #58
|
|
2566 |
#62 := [monotonicity #59]: #61
|
|
2567 |
#39 := [asserted]: #20
|
|
2568 |
#65 := [mp #39 #62]: #60
|
|
2569 |
#163 := (or #48 #160)
|
|
2570 |
#44 := (<= #42 0::real)
|
|
2571 |
#13 := (<= #10 #12)
|
|
2572 |
#45 := (iff #13 #44)
|
|
2573 |
#46 := [rewrite]: #45
|
|
2574 |
#37 := [asserted]: #13
|
|
2575 |
#47 := [mp #37 #46]: #44
|
|
2576 |
#159 := (not #44)
|
|
2577 |
#161 := (or #48 #159 #160)
|
|
2578 |
#162 := [th-lemma]: #161
|
|
2579 |
#164 := [unit-resolution #162 #47]: #163
|
|
2580 |
#165 := [unit-resolution #164 #65]: #160
|
|
2581 |
#14 := (:var 0 S3)
|
|
2582 |
#16 := (f3 f4 #14)
|
|
2583 |
#128 := (pattern #16)
|
|
2584 |
#15 := (f3 f6 #14)
|
|
2585 |
#127 := (pattern #15)
|
|
2586 |
#49 := (* -1::real #16)
|
|
2587 |
#50 := (+ #15 #49)
|
|
2588 |
#51 := (<= #50 0::real)
|
|
2589 |
#129 := (forall (vars (?v0 S3)) (:pat #127 #128) #51)
|
|
2590 |
#54 := (forall (vars (?v0 S3)) #51)
|
|
2591 |
#132 := (iff #54 #129)
|
|
2592 |
#130 := (iff #51 #51)
|
|
2593 |
#131 := [refl]: #130
|
|
2594 |
#133 := [quant-intro #131]: #132
|
|
2595 |
#69 := (~ #54 #54)
|
|
2596 |
#71 := (~ #51 #51)
|
|
2597 |
#72 := [refl]: #71
|
|
2598 |
#70 := [nnf-pos #72]: #69
|
|
2599 |
#17 := (<= #15 #16)
|
|
2600 |
#18 := (forall (vars (?v0 S3)) #17)
|
|
2601 |
#55 := (iff #18 #54)
|
|
2602 |
#52 := (iff #17 #51)
|
|
2603 |
#53 := [rewrite]: #52
|
|
2604 |
#56 := [quant-intro #53]: #55
|
|
2605 |
#38 := [asserted]: #18
|
|
2606 |
#57 := [mp #38 #56]: #54
|
|
2607 |
#67 := [mp~ #57 #70]: #54
|
|
2608 |
#134 := [mp #67 #133]: #129
|
|
2609 |
#149 := (not #129)
|
|
2610 |
#150 := (or #149 #135)
|
|
2611 |
#136 := (* -1::real #10)
|
|
2612 |
#137 := (+ #12 #136)
|
|
2613 |
#138 := (<= #137 0::real)
|
|
2614 |
#151 := (or #149 #138)
|
|
2615 |
#153 := (iff #151 #150)
|
|
2616 |
#155 := (iff #150 #150)
|
|
2617 |
#156 := [rewrite]: #155
|
|
2618 |
#147 := (iff #138 #135)
|
|
2619 |
#139 := (+ #136 #12)
|
|
2620 |
#142 := (<= #139 0::real)
|
|
2621 |
#145 := (iff #142 #135)
|
|
2622 |
#146 := [rewrite]: #145
|
|
2623 |
#143 := (iff #138 #142)
|
|
2624 |
#140 := (= #137 #139)
|
|
2625 |
#141 := [rewrite]: #140
|
|
2626 |
#144 := [monotonicity #141]: #143
|
|
2627 |
#148 := [trans #144 #146]: #147
|
|
2628 |
#154 := [monotonicity #148]: #153
|
|
2629 |
#157 := [trans #154 #156]: #153
|
|
2630 |
#152 := [quant-inst]: #151
|
|
2631 |
#158 := [mp #152 #157]: #150
|
|
2632 |
[unit-resolution #158 #134 #165]: false
|
|
2633 |
unsat
|
37156
|
2634 |
ada412db5ba79d588ff49226c319d0dae76f5f87 271 0
|
36900
|
2635 |
#2 := false
|
|
2636 |
#8 := 0::real
|
|
2637 |
decl f4 :: (-> S3 S2 real)
|
|
2638 |
decl f7 :: S2
|
|
2639 |
#19 := f7
|
|
2640 |
decl f5 :: S3
|
|
2641 |
#11 := f5
|
|
2642 |
#24 := (f4 f5 f7)
|
|
2643 |
decl f8 :: S3
|
|
2644 |
#21 := f8
|
|
2645 |
#22 := (f4 f8 f7)
|
|
2646 |
#66 := -1::real
|
|
2647 |
#87 := (* -1::real #22)
|
|
2648 |
#88 := (+ #87 #24)
|
|
2649 |
decl f3 :: real
|
|
2650 |
#9 := f3
|
|
2651 |
#148 := (* -1::real #24)
|
|
2652 |
#149 := (+ #22 #148)
|
|
2653 |
#150 := (+ f3 #149)
|
|
2654 |
#151 := (<= #150 0::real)
|
|
2655 |
#154 := (ite #151 f3 #88)
|
|
2656 |
#320 := (* -1::real #154)
|
|
2657 |
#321 := (+ f3 #320)
|
|
2658 |
#322 := (<= #321 0::real)
|
|
2659 |
#329 := (not #322)
|
|
2660 |
#65 := 1/2::real
|
|
2661 |
#157 := (* 1/2::real #154)
|
|
2662 |
#289 := (<= #157 0::real)
|
|
2663 |
#168 := (= #157 0::real)
|
|
2664 |
#178 := (<= #149 0::real)
|
|
2665 |
decl f6 :: S3
|
|
2666 |
#14 := f6
|
|
2667 |
#20 := (f4 f6 f7)
|
|
2668 |
#174 := (+ #20 #87)
|
|
2669 |
#175 := (<= #174 0::real)
|
|
2670 |
#181 := (and #175 #178)
|
|
2671 |
#184 := (not #181)
|
|
2672 |
#171 := (not #168)
|
|
2673 |
#80 := (* 1/2::real #24)
|
|
2674 |
#145 := (+ #87 #80)
|
|
2675 |
#79 := (* 1/2::real #20)
|
|
2676 |
#146 := (+ #79 #145)
|
|
2677 |
#143 := (>= #146 0::real)
|
|
2678 |
#141 := (not #143)
|
|
2679 |
#193 := (or #141 #171 #184)
|
|
2680 |
#198 := (not #193)
|
|
2681 |
#28 := 2::real
|
|
2682 |
#31 := (- #24 #22)
|
|
2683 |
#32 := (<= f3 #31)
|
|
2684 |
#33 := (ite #32 f3 #31)
|
|
2685 |
#34 := (/ #33 2::real)
|
|
2686 |
#35 := (+ #22 #34)
|
|
2687 |
#36 := (= #35 #22)
|
|
2688 |
#37 := (not #36)
|
|
2689 |
#27 := (+ #20 #24)
|
|
2690 |
#29 := (/ #27 2::real)
|
|
2691 |
#30 := (<= #22 #29)
|
|
2692 |
#38 := (implies #30 #37)
|
|
2693 |
#25 := (<= #22 #24)
|
|
2694 |
#23 := (<= #20 #22)
|
|
2695 |
#26 := (and #23 #25)
|
|
2696 |
#39 := (implies #26 #38)
|
|
2697 |
#40 := (not #39)
|
|
2698 |
#201 := (iff #40 #198)
|
|
2699 |
#91 := (<= f3 #88)
|
|
2700 |
#94 := (ite #91 f3 #88)
|
|
2701 |
#100 := (* 1/2::real #94)
|
|
2702 |
#105 := (+ #22 #100)
|
|
2703 |
#111 := (= #22 #105)
|
|
2704 |
#116 := (not #111)
|
|
2705 |
#81 := (+ #79 #80)
|
|
2706 |
#84 := (<= #22 #81)
|
|
2707 |
#122 := (not #84)
|
|
2708 |
#123 := (or #122 #116)
|
|
2709 |
#131 := (not #26)
|
|
2710 |
#132 := (or #131 #123)
|
|
2711 |
#137 := (not #132)
|
|
2712 |
#199 := (iff #137 #198)
|
|
2713 |
#196 := (iff #132 #193)
|
|
2714 |
#187 := (or #141 #171)
|
|
2715 |
#190 := (or #184 #187)
|
|
2716 |
#194 := (iff #190 #193)
|
|
2717 |
#195 := [rewrite]: #194
|
|
2718 |
#191 := (iff #132 #190)
|
|
2719 |
#188 := (iff #123 #187)
|
|
2720 |
#172 := (iff #116 #171)
|
|
2721 |
#169 := (iff #111 #168)
|
|
2722 |
#160 := (+ #22 #157)
|
|
2723 |
#163 := (= #22 #160)
|
|
2724 |
#166 := (iff #163 #168)
|
|
2725 |
#167 := [rewrite]: #166
|
|
2726 |
#164 := (iff #111 #163)
|
|
2727 |
#161 := (= #105 #160)
|
|
2728 |
#158 := (= #100 #157)
|
|
2729 |
#155 := (= #94 #154)
|
|
2730 |
#152 := (iff #91 #151)
|
|
2731 |
#153 := [rewrite]: #152
|
|
2732 |
#156 := [monotonicity #153]: #155
|
|
2733 |
#159 := [monotonicity #156]: #158
|
|
2734 |
#162 := [monotonicity #159]: #161
|
|
2735 |
#165 := [monotonicity #162]: #164
|
|
2736 |
#170 := [trans #165 #167]: #169
|
|
2737 |
#173 := [monotonicity #170]: #172
|
|
2738 |
#144 := (iff #122 #141)
|
|
2739 |
#140 := (iff #84 #143)
|
|
2740 |
#142 := [rewrite]: #140
|
|
2741 |
#147 := [monotonicity #142]: #144
|
|
2742 |
#189 := [monotonicity #147 #173]: #188
|
|
2743 |
#185 := (iff #131 #184)
|
|
2744 |
#182 := (iff #26 #181)
|
|
2745 |
#179 := (iff #25 #178)
|
|
2746 |
#180 := [rewrite]: #179
|
|
2747 |
#176 := (iff #23 #175)
|
|
2748 |
#177 := [rewrite]: #176
|
|
2749 |
#183 := [monotonicity #177 #180]: #182
|
|
2750 |
#186 := [monotonicity #183]: #185
|
|
2751 |
#192 := [monotonicity #186 #189]: #191
|
|
2752 |
#197 := [trans #192 #195]: #196
|
|
2753 |
#200 := [monotonicity #197]: #199
|
|
2754 |
#138 := (iff #40 #137)
|
|
2755 |
#135 := (iff #39 #132)
|
|
2756 |
#128 := (implies #26 #123)
|
|
2757 |
#133 := (iff #128 #132)
|
|
2758 |
#134 := [rewrite]: #133
|
|
2759 |
#129 := (iff #39 #128)
|
|
2760 |
#126 := (iff #38 #123)
|
|
2761 |
#119 := (implies #84 #116)
|
|
2762 |
#124 := (iff #119 #123)
|
|
2763 |
#125 := [rewrite]: #124
|
|
2764 |
#120 := (iff #38 #119)
|
|
2765 |
#117 := (iff #37 #116)
|
|
2766 |
#114 := (iff #36 #111)
|
|
2767 |
#108 := (= #105 #22)
|
|
2768 |
#112 := (iff #108 #111)
|
|
2769 |
#113 := [rewrite]: #112
|
|
2770 |
#109 := (iff #36 #108)
|
|
2771 |
#106 := (= #35 #105)
|
|
2772 |
#103 := (= #34 #100)
|
|
2773 |
#97 := (/ #94 2::real)
|
|
2774 |
#101 := (= #97 #100)
|
|
2775 |
#102 := [rewrite]: #101
|
|
2776 |
#98 := (= #34 #97)
|
|
2777 |
#95 := (= #33 #94)
|
|
2778 |
#89 := (= #31 #88)
|
|
2779 |
#90 := [rewrite]: #89
|
|
2780 |
#92 := (iff #32 #91)
|
|
2781 |
#93 := [monotonicity #90]: #92
|
|
2782 |
#96 := [monotonicity #93 #90]: #95
|
|
2783 |
#99 := [monotonicity #96]: #98
|
|
2784 |
#104 := [trans #99 #102]: #103
|
|
2785 |
#107 := [monotonicity #104]: #106
|
|
2786 |
#110 := [monotonicity #107]: #109
|
|
2787 |
#115 := [trans #110 #113]: #114
|
|
2788 |
#118 := [monotonicity #115]: #117
|
|
2789 |
#85 := (iff #30 #84)
|
|
2790 |
#82 := (= #29 #81)
|
|
2791 |
#83 := [rewrite]: #82
|
|
2792 |
#86 := [monotonicity #83]: #85
|
|
2793 |
#121 := [monotonicity #86 #118]: #120
|
|
2794 |
#127 := [trans #121 #125]: #126
|
|
2795 |
#130 := [monotonicity #127]: #129
|
|
2796 |
#136 := [trans #130 #134]: #135
|
|
2797 |
#139 := [monotonicity #136]: #138
|
|
2798 |
#202 := [trans #139 #200]: #201
|
|
2799 |
#59 := [asserted]: #40
|
|
2800 |
#203 := [mp #59 #202]: #198
|
|
2801 |
#205 := [not-or-elim #203]: #168
|
|
2802 |
#324 := (or #171 #289)
|
|
2803 |
#325 := [th-lemma]: #324
|
|
2804 |
#326 := [unit-resolution #325 #205]: #289
|
|
2805 |
#327 := [hypothesis]: #322
|
|
2806 |
#60 := (<= f3 0::real)
|
|
2807 |
#61 := (not #60)
|
|
2808 |
#10 := (< 0::real f3)
|
|
2809 |
#62 := (iff #10 #61)
|
|
2810 |
#63 := [rewrite]: #62
|
|
2811 |
#57 := [asserted]: #10
|
|
2812 |
#64 := [mp #57 #63]: #61
|
|
2813 |
#328 := [th-lemma #64 #327 #326]: false
|
|
2814 |
#330 := [lemma #328]: #329
|
|
2815 |
#282 := (= f3 #154)
|
|
2816 |
#283 := (= #88 #154)
|
|
2817 |
#339 := (not #283)
|
|
2818 |
#323 := (+ #88 #320)
|
|
2819 |
#331 := (<= #323 0::real)
|
|
2820 |
#336 := (not #331)
|
|
2821 |
#301 := (+ #20 #148)
|
|
2822 |
#302 := (>= #301 0::real)
|
|
2823 |
#307 := (not #302)
|
|
2824 |
#12 := (:var 0 S2)
|
|
2825 |
#15 := (f4 f6 #12)
|
|
2826 |
#275 := (pattern #15)
|
|
2827 |
#13 := (f4 f5 #12)
|
|
2828 |
#274 := (pattern #13)
|
|
2829 |
#67 := (* -1::real #15)
|
|
2830 |
#68 := (+ #13 #67)
|
|
2831 |
#69 := (<= #68 0::real)
|
|
2832 |
#218 := (not #69)
|
|
2833 |
#276 := (forall (vars (?v0 S2)) (:pat #274 #275) #218)
|
|
2834 |
#223 := (forall (vars (?v0 S2)) #218)
|
|
2835 |
#279 := (iff #223 #276)
|
|
2836 |
#277 := (iff #218 #218)
|
|
2837 |
#278 := [refl]: #277
|
|
2838 |
#280 := [quant-intro #278]: #279
|
|
2839 |
#72 := (exists (vars (?v0 S2)) #69)
|
|
2840 |
#75 := (not #72)
|
|
2841 |
#220 := (~ #75 #223)
|
|
2842 |
#219 := (~ #218 #218)
|
|
2843 |
#222 := [refl]: #219
|
|
2844 |
#221 := [nnf-neg #222]: #220
|
|
2845 |
#16 := (<= #13 #15)
|
|
2846 |
#17 := (exists (vars (?v0 S2)) #16)
|
|
2847 |
#18 := (not #17)
|
|
2848 |
#76 := (iff #18 #75)
|
|
2849 |
#73 := (iff #17 #72)
|
|
2850 |
#70 := (iff #16 #69)
|
|
2851 |
#71 := [rewrite]: #70
|
|
2852 |
#74 := [quant-intro #71]: #73
|
|
2853 |
#77 := [monotonicity #74]: #76
|
|
2854 |
#58 := [asserted]: #18
|
|
2855 |
#78 := [mp #58 #77]: #75
|
|
2856 |
#216 := [mp~ #78 #221]: #223
|
|
2857 |
#281 := [mp #216 #280]: #276
|
|
2858 |
#310 := (not #276)
|
|
2859 |
#311 := (or #310 #307)
|
|
2860 |
#291 := (* -1::real #20)
|
|
2861 |
#292 := (+ #24 #291)
|
|
2862 |
#293 := (<= #292 0::real)
|
|
2863 |
#294 := (not #293)
|
|
2864 |
#312 := (or #310 #294)
|
|
2865 |
#314 := (iff #312 #311)
|
|
2866 |
#316 := (iff #311 #311)
|
|
2867 |
#317 := [rewrite]: #316
|
|
2868 |
#308 := (iff #294 #307)
|
|
2869 |
#305 := (iff #293 #302)
|
|
2870 |
#295 := (+ #291 #24)
|
|
2871 |
#298 := (<= #295 0::real)
|
|
2872 |
#303 := (iff #298 #302)
|
|
2873 |
#304 := [rewrite]: #303
|
|
2874 |
#299 := (iff #293 #298)
|
|
2875 |
#296 := (= #292 #295)
|
|
2876 |
#297 := [rewrite]: #296
|
|
2877 |
#300 := [monotonicity #297]: #299
|
|
2878 |
#306 := [trans #300 #304]: #305
|
|
2879 |
#309 := [monotonicity #306]: #308
|
|
2880 |
#315 := [monotonicity #309]: #314
|
|
2881 |
#318 := [trans #315 #317]: #314
|
|
2882 |
#313 := [quant-inst]: #312
|
|
2883 |
#319 := [mp #313 #318]: #311
|
|
2884 |
#333 := [unit-resolution #319 #281]: #307
|
|
2885 |
#204 := [not-or-elim #203]: #143
|
|
2886 |
#334 := [hypothesis]: #331
|
|
2887 |
#335 := [th-lemma #334 #204 #333 #326]: false
|
|
2888 |
#337 := [lemma #335]: #336
|
|
2889 |
#338 := [hypothesis]: #283
|
|
2890 |
#340 := (or #339 #331)
|
|
2891 |
#341 := [th-lemma]: #340
|
|
2892 |
#342 := [unit-resolution #341 #338 #337]: false
|
|
2893 |
#343 := [lemma #342]: #339
|
|
2894 |
#287 := (or #151 #283)
|
|
2895 |
#288 := [def-axiom]: #287
|
|
2896 |
#344 := [unit-resolution #288 #343]: #151
|
|
2897 |
#284 := (not #151)
|
|
2898 |
#285 := (or #284 #282)
|
|
2899 |
#286 := [def-axiom]: #285
|
|
2900 |
#345 := [unit-resolution #286 #344]: #282
|
|
2901 |
#346 := (not #282)
|
|
2902 |
#347 := (or #346 #322)
|
|
2903 |
#348 := [th-lemma]: #347
|
|
2904 |
[unit-resolution #348 #345 #330]: false
|
|
2905 |
unsat
|
37156
|
2906 |
3f6125a99a8cb462db3a2586a1eae0021b892091 288 0
|
36900
|
2907 |
#2 := false
|
|
2908 |
#8 := 0::real
|
|
2909 |
decl f4 :: (-> S3 S2 real)
|
|
2910 |
decl f7 :: S2
|
|
2911 |
#19 := f7
|
|
2912 |
decl f8 :: S3
|
|
2913 |
#21 := f8
|
|
2914 |
#22 := (f4 f8 f7)
|
|
2915 |
decl f6 :: S3
|
|
2916 |
#14 := f6
|
|
2917 |
#20 := (f4 f6 f7)
|
|
2918 |
#73 := -1::real
|
|
2919 |
#118 := (* -1::real #20)
|
|
2920 |
#119 := (+ #118 #22)
|
|
2921 |
decl f3 :: real
|
|
2922 |
#9 := f3
|
|
2923 |
#97 := (* -1::real #22)
|
|
2924 |
#211 := (+ #20 #97)
|
|
2925 |
#212 := (+ f3 #211)
|
|
2926 |
#213 := (<= #212 0::real)
|
|
2927 |
#216 := (ite #213 f3 #119)
|
|
2928 |
#397 := (* -1::real #216)
|
|
2929 |
#398 := (+ f3 #397)
|
|
2930 |
#399 := (<= #398 0::real)
|
|
2931 |
#407 := (not #399)
|
|
2932 |
#72 := 1/2::real
|
|
2933 |
#287 := (* 1/2::real #216)
|
|
2934 |
#367 := (<= #287 0::real)
|
|
2935 |
#288 := (= #287 0::real)
|
|
2936 |
#139 := -1/2::real
|
|
2937 |
#219 := (* -1/2::real #216)
|
|
2938 |
#222 := (+ #22 #219)
|
|
2939 |
decl f5 :: S3
|
|
2940 |
#11 := f5
|
|
2941 |
#24 := (f4 f5 f7)
|
|
2942 |
#98 := (+ #97 #24)
|
|
2943 |
#196 := (* -1::real #24)
|
|
2944 |
#197 := (+ #22 #196)
|
|
2945 |
#198 := (+ f3 #197)
|
|
2946 |
#199 := (<= #198 0::real)
|
|
2947 |
#202 := (ite #199 f3 #98)
|
|
2948 |
#205 := (* 1/2::real #202)
|
|
2949 |
#208 := (+ #22 #205)
|
|
2950 |
#87 := (* 1/2::real #24)
|
|
2951 |
#185 := (+ #97 #87)
|
|
2952 |
#86 := (* 1/2::real #20)
|
|
2953 |
#186 := (+ #86 #185)
|
|
2954 |
#183 := (>= #186 0::real)
|
|
2955 |
#225 := (ite #183 #208 #222)
|
|
2956 |
#228 := (= #22 #225)
|
|
2957 |
#291 := (iff #228 #288)
|
|
2958 |
#284 := (= #22 #222)
|
|
2959 |
#289 := (iff #284 #288)
|
|
2960 |
#290 := [rewrite]: #289
|
|
2961 |
#285 := (iff #228 #284)
|
|
2962 |
#282 := (= #225 #222)
|
|
2963 |
#277 := (ite false #208 #222)
|
|
2964 |
#280 := (= #277 #222)
|
|
2965 |
#281 := [rewrite]: #280
|
|
2966 |
#278 := (= #225 #277)
|
|
2967 |
#275 := (iff #183 false)
|
|
2968 |
#182 := (not #183)
|
|
2969 |
#237 := (<= #197 0::real)
|
|
2970 |
#234 := (<= #211 0::real)
|
|
2971 |
#240 := (and #234 #237)
|
|
2972 |
#243 := (not #240)
|
|
2973 |
#231 := (not #228)
|
|
2974 |
#252 := (or #183 #231 #243)
|
|
2975 |
#257 := (not #252)
|
|
2976 |
#28 := 2::real
|
|
2977 |
#37 := (- #22 #20)
|
|
2978 |
#38 := (<= f3 #37)
|
|
2979 |
#39 := (ite #38 f3 #37)
|
|
2980 |
#40 := (/ #39 2::real)
|
|
2981 |
#41 := (- #22 #40)
|
|
2982 |
#32 := (- #24 #22)
|
|
2983 |
#33 := (<= f3 #32)
|
|
2984 |
#34 := (ite #33 f3 #32)
|
|
2985 |
#35 := (/ #34 2::real)
|
|
2986 |
#36 := (+ #22 #35)
|
|
2987 |
#27 := (+ #20 #24)
|
|
2988 |
#29 := (/ #27 2::real)
|
|
2989 |
#31 := (<= #22 #29)
|
|
2990 |
#42 := (ite #31 #36 #41)
|
|
2991 |
#43 := (= #42 #22)
|
|
2992 |
#44 := (not #43)
|
|
2993 |
#30 := (< #29 #22)
|
|
2994 |
#45 := (implies #30 #44)
|
|
2995 |
#25 := (<= #22 #24)
|
|
2996 |
#23 := (<= #20 #22)
|
|
2997 |
#26 := (and #23 #25)
|
|
2998 |
#46 := (implies #26 #45)
|
|
2999 |
#47 := (not #46)
|
|
3000 |
#260 := (iff #47 #257)
|
|
3001 |
#122 := (<= f3 #119)
|
|
3002 |
#125 := (ite #122 f3 #119)
|
|
3003 |
#140 := (* -1/2::real #125)
|
|
3004 |
#141 := (+ #22 #140)
|
|
3005 |
#101 := (<= f3 #98)
|
|
3006 |
#104 := (ite #101 f3 #98)
|
|
3007 |
#110 := (* 1/2::real #104)
|
|
3008 |
#115 := (+ #22 #110)
|
|
3009 |
#88 := (+ #86 #87)
|
|
3010 |
#94 := (<= #22 #88)
|
|
3011 |
#146 := (ite #94 #115 #141)
|
|
3012 |
#152 := (= #22 #146)
|
|
3013 |
#157 := (not #152)
|
|
3014 |
#91 := (< #88 #22)
|
|
3015 |
#163 := (not #91)
|
|
3016 |
#164 := (or #163 #157)
|
|
3017 |
#172 := (not #26)
|
|
3018 |
#173 := (or #172 #164)
|
|
3019 |
#178 := (not #173)
|
|
3020 |
#258 := (iff #178 #257)
|
|
3021 |
#255 := (iff #173 #252)
|
|
3022 |
#246 := (or #183 #231)
|
|
3023 |
#249 := (or #243 #246)
|
|
3024 |
#253 := (iff #249 #252)
|
|
3025 |
#254 := [rewrite]: #253
|
|
3026 |
#250 := (iff #173 #249)
|
|
3027 |
#247 := (iff #164 #246)
|
|
3028 |
#232 := (iff #157 #231)
|
|
3029 |
#229 := (iff #152 #228)
|
|
3030 |
#226 := (= #146 #225)
|
|
3031 |
#223 := (= #141 #222)
|
|
3032 |
#220 := (= #140 #219)
|
|
3033 |
#217 := (= #125 #216)
|
|
3034 |
#214 := (iff #122 #213)
|
|
3035 |
#215 := [rewrite]: #214
|
|
3036 |
#218 := [monotonicity #215]: #217
|
|
3037 |
#221 := [monotonicity #218]: #220
|
|
3038 |
#224 := [monotonicity #221]: #223
|
|
3039 |
#209 := (= #115 #208)
|
|
3040 |
#206 := (= #110 #205)
|
|
3041 |
#203 := (= #104 #202)
|
|
3042 |
#200 := (iff #101 #199)
|
|
3043 |
#201 := [rewrite]: #200
|
|
3044 |
#204 := [monotonicity #201]: #203
|
|
3045 |
#207 := [monotonicity #204]: #206
|
|
3046 |
#210 := [monotonicity #207]: #209
|
|
3047 |
#195 := (iff #94 #183)
|
|
3048 |
#194 := [rewrite]: #195
|
|
3049 |
#227 := [monotonicity #194 #210 #224]: #226
|
|
3050 |
#230 := [monotonicity #227]: #229
|
|
3051 |
#233 := [monotonicity #230]: #232
|
|
3052 |
#192 := (iff #163 #183)
|
|
3053 |
#187 := (not #182)
|
|
3054 |
#190 := (iff #187 #183)
|
|
3055 |
#191 := [rewrite]: #190
|
|
3056 |
#188 := (iff #163 #187)
|
|
3057 |
#181 := (iff #91 #182)
|
|
3058 |
#184 := [rewrite]: #181
|
|
3059 |
#189 := [monotonicity #184]: #188
|
|
3060 |
#193 := [trans #189 #191]: #192
|
|
3061 |
#248 := [monotonicity #193 #233]: #247
|
|
3062 |
#244 := (iff #172 #243)
|
|
3063 |
#241 := (iff #26 #240)
|
|
3064 |
#238 := (iff #25 #237)
|
|
3065 |
#239 := [rewrite]: #238
|
|
3066 |
#235 := (iff #23 #234)
|
|
3067 |
#236 := [rewrite]: #235
|
|
3068 |
#242 := [monotonicity #236 #239]: #241
|
|
3069 |
#245 := [monotonicity #242]: #244
|
|
3070 |
#251 := [monotonicity #245 #248]: #250
|
|
3071 |
#256 := [trans #251 #254]: #255
|
|
3072 |
#259 := [monotonicity #256]: #258
|
|
3073 |
#179 := (iff #47 #178)
|
|
3074 |
#176 := (iff #46 #173)
|
|
3075 |
#169 := (implies #26 #164)
|
|
3076 |
#174 := (iff #169 #173)
|
|
3077 |
#175 := [rewrite]: #174
|
|
3078 |
#170 := (iff #46 #169)
|
|
3079 |
#167 := (iff #45 #164)
|
|
3080 |
#160 := (implies #91 #157)
|
|
3081 |
#165 := (iff #160 #164)
|
|
3082 |
#166 := [rewrite]: #165
|
|
3083 |
#161 := (iff #45 #160)
|
|
3084 |
#158 := (iff #44 #157)
|
|
3085 |
#155 := (iff #43 #152)
|
|
3086 |
#149 := (= #146 #22)
|
|
3087 |
#153 := (iff #149 #152)
|
|
3088 |
#154 := [rewrite]: #153
|
|
3089 |
#150 := (iff #43 #149)
|
|
3090 |
#147 := (= #42 #146)
|
|
3091 |
#144 := (= #41 #141)
|
|
3092 |
#131 := (* 1/2::real #125)
|
|
3093 |
#136 := (- #22 #131)
|
|
3094 |
#142 := (= #136 #141)
|
|
3095 |
#143 := [rewrite]: #142
|
|
3096 |
#137 := (= #41 #136)
|
|
3097 |
#134 := (= #40 #131)
|
|
3098 |
#128 := (/ #125 2::real)
|
|
3099 |
#132 := (= #128 #131)
|
|
3100 |
#133 := [rewrite]: #132
|
|
3101 |
#129 := (= #40 #128)
|
|
3102 |
#126 := (= #39 #125)
|
|
3103 |
#120 := (= #37 #119)
|
|
3104 |
#121 := [rewrite]: #120
|
|
3105 |
#123 := (iff #38 #122)
|
|
3106 |
#124 := [monotonicity #121]: #123
|
|
3107 |
#127 := [monotonicity #124 #121]: #126
|
|
3108 |
#130 := [monotonicity #127]: #129
|
|
3109 |
#135 := [trans #130 #133]: #134
|
|
3110 |
#138 := [monotonicity #135]: #137
|
|
3111 |
#145 := [trans #138 #143]: #144
|
|
3112 |
#116 := (= #36 #115)
|
|
3113 |
#113 := (= #35 #110)
|
|
3114 |
#107 := (/ #104 2::real)
|
|
3115 |
#111 := (= #107 #110)
|
|
3116 |
#112 := [rewrite]: #111
|
|
3117 |
#108 := (= #35 #107)
|
|
3118 |
#105 := (= #34 #104)
|
|
3119 |
#99 := (= #32 #98)
|
|
3120 |
#100 := [rewrite]: #99
|
|
3121 |
#102 := (iff #33 #101)
|
|
3122 |
#103 := [monotonicity #100]: #102
|
|
3123 |
#106 := [monotonicity #103 #100]: #105
|
|
3124 |
#109 := [monotonicity #106]: #108
|
|
3125 |
#114 := [trans #109 #112]: #113
|
|
3126 |
#117 := [monotonicity #114]: #116
|
|
3127 |
#95 := (iff #31 #94)
|
|
3128 |
#89 := (= #29 #88)
|
|
3129 |
#90 := [rewrite]: #89
|
|
3130 |
#96 := [monotonicity #90]: #95
|
|
3131 |
#148 := [monotonicity #96 #117 #145]: #147
|
|
3132 |
#151 := [monotonicity #148]: #150
|
|
3133 |
#156 := [trans #151 #154]: #155
|
|
3134 |
#159 := [monotonicity #156]: #158
|
|
3135 |
#92 := (iff #30 #91)
|
|
3136 |
#93 := [monotonicity #90]: #92
|
|
3137 |
#162 := [monotonicity #93 #159]: #161
|
|
3138 |
#168 := [trans #162 #166]: #167
|
|
3139 |
#171 := [monotonicity #168]: #170
|
|
3140 |
#177 := [trans #171 #175]: #176
|
|
3141 |
#180 := [monotonicity #177]: #179
|
|
3142 |
#261 := [trans #180 #259]: #260
|
|
3143 |
#66 := [asserted]: #47
|
|
3144 |
#262 := [mp #66 #261]: #257
|
|
3145 |
#263 := [not-or-elim #262]: #182
|
|
3146 |
#276 := [iff-false #263]: #275
|
|
3147 |
#279 := [monotonicity #276]: #278
|
|
3148 |
#283 := [trans #279 #281]: #282
|
|
3149 |
#286 := [monotonicity #283]: #285
|
|
3150 |
#292 := [trans #286 #290]: #291
|
|
3151 |
#264 := [not-or-elim #262]: #228
|
|
3152 |
#293 := [mp #264 #292]: #288
|
|
3153 |
#401 := (not #288)
|
|
3154 |
#402 := (or #401 #367)
|
|
3155 |
#403 := [th-lemma]: #402
|
|
3156 |
#404 := [unit-resolution #403 #293]: #367
|
|
3157 |
#405 := [hypothesis]: #399
|
|
3158 |
#67 := (<= f3 0::real)
|
|
3159 |
#68 := (not #67)
|
|
3160 |
#10 := (< 0::real f3)
|
|
3161 |
#69 := (iff #10 #68)
|
|
3162 |
#70 := [rewrite]: #69
|
|
3163 |
#64 := [asserted]: #10
|
|
3164 |
#71 := [mp #64 #70]: #68
|
|
3165 |
#406 := [th-lemma #71 #405 #404]: false
|
|
3166 |
#408 := [lemma #406]: #407
|
|
3167 |
#360 := (= f3 #216)
|
|
3168 |
#361 := (= #119 #216)
|
|
3169 |
#416 := (not #361)
|
|
3170 |
#400 := (+ #119 #397)
|
|
3171 |
#409 := (<= #400 0::real)
|
|
3172 |
#413 := (not #409)
|
|
3173 |
#265 := [not-or-elim #262]: #240
|
|
3174 |
#267 := [and-elim #265]: #237
|
|
3175 |
#411 := [hypothesis]: #409
|
|
3176 |
#412 := [th-lemma #411 #267 #263 #404]: false
|
|
3177 |
#414 := [lemma #412]: #413
|
|
3178 |
#415 := [hypothesis]: #361
|
|
3179 |
#417 := (or #416 #409)
|
|
3180 |
#418 := [th-lemma]: #417
|
|
3181 |
#419 := [unit-resolution #418 #415 #414]: false
|
|
3182 |
#420 := [lemma #419]: #416
|
|
3183 |
#365 := (or #213 #361)
|
|
3184 |
#366 := [def-axiom]: #365
|
|
3185 |
#421 := [unit-resolution #366 #420]: #213
|
|
3186 |
#362 := (not #213)
|
|
3187 |
#363 := (or #362 #360)
|
|
3188 |
#364 := [def-axiom]: #363
|
|
3189 |
#422 := [unit-resolution #364 #421]: #360
|
|
3190 |
#423 := (not #360)
|
|
3191 |
#424 := (or #423 #399)
|
|
3192 |
#425 := [th-lemma]: #424
|
|
3193 |
[unit-resolution #425 #422 #408]: false
|
|
3194 |
unsat
|
37156
|
3195 |
9ecd5f8eb0c8f78bd68a366175093e04632f1f73 149 0
|
36900
|
3196 |
#2 := false
|
|
3197 |
#23 := 0::real
|
|
3198 |
decl f3 :: (-> S2 S3 real)
|
|
3199 |
decl f5 :: S3
|
|
3200 |
#9 := f5
|
|
3201 |
decl f6 :: S2
|
|
3202 |
#11 := f6
|
|
3203 |
#12 := (f3 f6 f5)
|
|
3204 |
#49 := -1::real
|
|
3205 |
#161 := (* -1::real #12)
|
|
3206 |
decl f4 :: S2
|
|
3207 |
#8 := f4
|
|
3208 |
#10 := (f3 f4 f5)
|
|
3209 |
#208 := (+ #10 #161)
|
|
3210 |
#210 := (>= #208 0::real)
|
|
3211 |
#13 := (= #10 #12)
|
|
3212 |
#45 := [asserted]: #13
|
|
3213 |
#213 := (not #13)
|
|
3214 |
#214 := (or #213 #210)
|
|
3215 |
#215 := [th-lemma]: #214
|
|
3216 |
#216 := [unit-resolution #215 #45]: #210
|
|
3217 |
decl f7 :: S2
|
|
3218 |
#16 := f7
|
|
3219 |
#26 := (f3 f7 f5)
|
|
3220 |
#165 := (* -1::real #26)
|
|
3221 |
#166 := (+ #10 #165)
|
|
3222 |
#212 := (>= #166 0::real)
|
|
3223 |
#227 := (not #212)
|
|
3224 |
#211 := (= #10 #26)
|
|
3225 |
#221 := (not #211)
|
|
3226 |
#67 := (= #12 #26)
|
|
3227 |
#75 := (not #67)
|
|
3228 |
#222 := (iff #75 #221)
|
|
3229 |
#219 := (iff #67 #211)
|
|
3230 |
#217 := (iff #211 #67)
|
|
3231 |
#218 := [monotonicity #45]: #217
|
|
3232 |
#220 := [symm #218]: #219
|
|
3233 |
#223 := [monotonicity #220]: #222
|
|
3234 |
#27 := (= #26 #12)
|
|
3235 |
#28 := (not #27)
|
|
3236 |
#76 := (iff #28 #75)
|
|
3237 |
#73 := (iff #27 #67)
|
|
3238 |
#74 := [rewrite]: #73
|
|
3239 |
#77 := [monotonicity #74]: #76
|
|
3240 |
#48 := [asserted]: #28
|
|
3241 |
#80 := [mp #48 #77]: #75
|
|
3242 |
#224 := [mp #80 #223]: #221
|
|
3243 |
#230 := (or #211 #227)
|
|
3244 |
#167 := (<= #166 0::real)
|
|
3245 |
#177 := (+ #12 #165)
|
|
3246 |
#178 := (>= #177 0::real)
|
|
3247 |
#183 := (not #178)
|
|
3248 |
#168 := (not #167)
|
|
3249 |
#186 := (or #168 #183)
|
|
3250 |
#189 := (not #186)
|
|
3251 |
#14 := (:var 0 S3)
|
|
3252 |
#19 := (f3 f6 #14)
|
|
3253 |
#154 := (pattern #19)
|
|
3254 |
#17 := (f3 f7 #14)
|
|
3255 |
#153 := (pattern #17)
|
|
3256 |
#15 := (f3 f4 #14)
|
|
3257 |
#152 := (pattern #15)
|
|
3258 |
#55 := (* -1::real #19)
|
|
3259 |
#56 := (+ #17 #55)
|
|
3260 |
#57 := (<= #56 0::real)
|
|
3261 |
#82 := (not #57)
|
|
3262 |
#50 := (* -1::real #17)
|
|
3263 |
#51 := (+ #15 #50)
|
|
3264 |
#52 := (<= #51 0::real)
|
|
3265 |
#85 := (not #52)
|
|
3266 |
#83 := (or #85 #82)
|
|
3267 |
#81 := (not #83)
|
|
3268 |
#155 := (forall (vars (?v0 S3)) (:pat #152 #153 #154) #81)
|
|
3269 |
#91 := (forall (vars (?v0 S3)) #81)
|
|
3270 |
#158 := (iff #91 #155)
|
|
3271 |
#156 := (iff #81 #81)
|
|
3272 |
#157 := [refl]: #156
|
|
3273 |
#159 := [quant-intro #157]: #158
|
|
3274 |
#60 := (and #52 #57)
|
|
3275 |
#63 := (forall (vars (?v0 S3)) #60)
|
|
3276 |
#92 := (iff #63 #91)
|
|
3277 |
#78 := (iff #60 #81)
|
|
3278 |
#90 := [rewrite]: #78
|
|
3279 |
#93 := [quant-intro #90]: #92
|
|
3280 |
#86 := (~ #63 #63)
|
|
3281 |
#88 := (~ #60 #60)
|
|
3282 |
#89 := [refl]: #88
|
|
3283 |
#87 := [nnf-pos #89]: #86
|
|
3284 |
#20 := (<= #17 #19)
|
|
3285 |
#18 := (<= #15 #17)
|
|
3286 |
#21 := (and #18 #20)
|
|
3287 |
#22 := (forall (vars (?v0 S3)) #21)
|
|
3288 |
#64 := (iff #22 #63)
|
|
3289 |
#61 := (iff #21 #60)
|
|
3290 |
#58 := (iff #20 #57)
|
|
3291 |
#59 := [rewrite]: #58
|
|
3292 |
#53 := (iff #18 #52)
|
|
3293 |
#54 := [rewrite]: #53
|
|
3294 |
#62 := [monotonicity #54 #59]: #61
|
|
3295 |
#65 := [quant-intro #62]: #64
|
|
3296 |
#46 := [asserted]: #22
|
|
3297 |
#66 := [mp #46 #65]: #63
|
|
3298 |
#84 := [mp~ #66 #87]: #63
|
|
3299 |
#94 := [mp #84 #93]: #91
|
|
3300 |
#160 := [mp #94 #159]: #155
|
|
3301 |
#192 := (not #155)
|
|
3302 |
#193 := (or #192 #189)
|
|
3303 |
#162 := (+ #26 #161)
|
|
3304 |
#163 := (<= #162 0::real)
|
|
3305 |
#164 := (not #163)
|
|
3306 |
#169 := (or #168 #164)
|
|
3307 |
#170 := (not #169)
|
|
3308 |
#194 := (or #192 #170)
|
|
3309 |
#196 := (iff #194 #193)
|
|
3310 |
#198 := (iff #193 #193)
|
|
3311 |
#199 := [rewrite]: #198
|
|
3312 |
#190 := (iff #170 #189)
|
|
3313 |
#187 := (iff #169 #186)
|
|
3314 |
#184 := (iff #164 #183)
|
|
3315 |
#181 := (iff #163 #178)
|
|
3316 |
#171 := (+ #161 #26)
|
|
3317 |
#174 := (<= #171 0::real)
|
|
3318 |
#179 := (iff #174 #178)
|
|
3319 |
#180 := [rewrite]: #179
|
|
3320 |
#175 := (iff #163 #174)
|
|
3321 |
#172 := (= #162 #171)
|
|
3322 |
#173 := [rewrite]: #172
|
|
3323 |
#176 := [monotonicity #173]: #175
|
|
3324 |
#182 := [trans #176 #180]: #181
|
|
3325 |
#185 := [monotonicity #182]: #184
|
|
3326 |
#188 := [monotonicity #185]: #187
|
|
3327 |
#191 := [monotonicity #188]: #190
|
|
3328 |
#197 := [monotonicity #191]: #196
|
|
3329 |
#200 := [trans #197 #199]: #196
|
|
3330 |
#195 := [quant-inst]: #194
|
|
3331 |
#201 := [mp #195 #200]: #193
|
|
3332 |
#225 := [unit-resolution #201 #160]: #189
|
|
3333 |
#202 := (or #186 #167)
|
|
3334 |
#203 := [def-axiom]: #202
|
|
3335 |
#226 := [unit-resolution #203 #225]: #167
|
|
3336 |
#228 := (or #211 #168 #227)
|
|
3337 |
#229 := [th-lemma]: #228
|
|
3338 |
#231 := [unit-resolution #229 #226]: #230
|
|
3339 |
#232 := [unit-resolution #231 #224]: #227
|
|
3340 |
#204 := (or #186 #178)
|
|
3341 |
#205 := [def-axiom]: #204
|
|
3342 |
#233 := [unit-resolution #205 #225]: #178
|
|
3343 |
[th-lemma #233 #232 #216]: false
|
|
3344 |
unsat
|
37156
|
3345 |
2dea73fd0603d00ddaec5e14116c465addb0b89e 870 0
|
36900
|
3346 |
#2 := false
|
|
3347 |
#11 := 0::real
|
|
3348 |
decl f5 :: real
|
|
3349 |
#26 := f5
|
|
3350 |
decl f3 :: real
|
|
3351 |
#9 := f3
|
|
3352 |
#76 := -1::real
|
|
3353 |
#77 := (* -1::real f3)
|
|
3354 |
#176 := (+ #77 f5)
|
|
3355 |
#124 := (* -1::real f5)
|
|
3356 |
#167 := (+ f3 #124)
|
|
3357 |
#260 := (>= #167 0::real)
|
|
3358 |
#267 := (ite #260 #167 #176)
|
|
3359 |
#275 := (* -1::real #267)
|
|
3360 |
decl f4 :: real
|
|
3361 |
#15 := f4
|
|
3362 |
#96 := 1/3::real
|
|
3363 |
#97 := (* 1/3::real f4)
|
|
3364 |
#276 := (+ #97 #275)
|
|
3365 |
#277 := (<= #276 0::real)
|
|
3366 |
#278 := (not #277)
|
|
3367 |
decl ?v0!5 :: real
|
|
3368 |
#448 := ?v0!5
|
|
3369 |
#459 := (* -1::real ?v0!5)
|
|
3370 |
#573 := (+ f3 #459)
|
|
3371 |
#567 := (+ #77 ?v0!5)
|
|
3372 |
#574 := (<= #573 0::real)
|
|
3373 |
#581 := (ite #574 #567 #573)
|
|
3374 |
#584 := (* -1::real #581)
|
|
3375 |
#587 := (+ #97 #584)
|
|
3376 |
#590 := (<= #587 0::real)
|
|
3377 |
#593 := (not #590)
|
|
3378 |
decl ?v2!3 :: real
|
|
3379 |
#442 := ?v2!3
|
|
3380 |
#477 := (* -1::real ?v2!3)
|
|
3381 |
#544 := (+ f5 #477)
|
|
3382 |
#538 := (+ #124 ?v2!3)
|
|
3383 |
#545 := (<= #544 0::real)
|
|
3384 |
#552 := (ite #545 #538 #544)
|
|
3385 |
#555 := (* -1::real #552)
|
|
3386 |
#558 := (+ #97 #555)
|
|
3387 |
#561 := (<= #558 0::real)
|
|
3388 |
#564 := (not #561)
|
|
3389 |
decl ?v4!1 :: real
|
|
3390 |
#446 := ?v4!1
|
|
3391 |
#532 := (+ ?v4!1 #459)
|
|
3392 |
#533 := (>= #532 0::real)
|
|
3393 |
decl ?v1!4 :: real
|
|
3394 |
#447 := ?v1!4
|
|
3395 |
#468 := (* -1::real ?v1!4)
|
|
3396 |
decl ?v5!0 :: real
|
|
3397 |
#445 := ?v5!0
|
|
3398 |
#520 := (+ ?v5!0 #468)
|
|
3399 |
#521 := (>= #520 0::real)
|
|
3400 |
#451 := (* -1::real ?v5!0)
|
|
3401 |
decl ?v3!2 :: real
|
|
3402 |
#444 := ?v3!2
|
|
3403 |
#499 := (+ ?v3!2 #451)
|
|
3404 |
#500 := (>= #499 0::real)
|
|
3405 |
#449 := (* -1::real ?v4!1)
|
|
3406 |
#497 := (+ ?v2!3 #449)
|
|
3407 |
#498 := (>= #497 0::real)
|
|
3408 |
#486 := (* -1::real ?v3!2)
|
|
3409 |
#487 := (+ f5 #486)
|
|
3410 |
#488 := (+ #124 ?v3!2)
|
|
3411 |
#489 := (<= #487 0::real)
|
|
3412 |
#490 := (ite #489 #488 #487)
|
|
3413 |
#491 := (* -1::real #490)
|
|
3414 |
#492 := (+ #97 #491)
|
|
3415 |
#493 := (<= #492 0::real)
|
|
3416 |
#494 := (not #493)
|
|
3417 |
#469 := (+ f3 #468)
|
|
3418 |
#470 := (+ #77 ?v1!4)
|
|
3419 |
#471 := (<= #469 0::real)
|
|
3420 |
#472 := (ite #471 #470 #469)
|
|
3421 |
#473 := (* -1::real #472)
|
|
3422 |
#474 := (+ #97 #473)
|
|
3423 |
#475 := (<= #474 0::real)
|
|
3424 |
#476 := (not #475)
|
|
3425 |
#599 := (and #278 #476 #494 #498 #500 #521 #533 #564 #593)
|
|
3426 |
#613 := (+ ?v5!0 #449)
|
|
3427 |
#607 := (+ #451 ?v4!1)
|
|
3428 |
#614 := (<= #613 0::real)
|
|
3429 |
#621 := (ite #614 #607 #613)
|
|
3430 |
#624 := (* -1::real #621)
|
|
3431 |
#627 := (+ f4 #624)
|
|
3432 |
#630 := (<= #627 0::real)
|
|
3433 |
#633 := (not #630)
|
|
3434 |
#604 := (not #599)
|
|
3435 |
#636 := (or #604 #633)
|
|
3436 |
#639 := (not #636)
|
|
3437 |
#450 := (+ #449 ?v5!0)
|
|
3438 |
#452 := (+ ?v4!1 #451)
|
|
3439 |
#453 := (>= #452 0::real)
|
|
3440 |
#454 := (ite #453 #452 #450)
|
|
3441 |
#455 := (* -1::real #454)
|
|
3442 |
#456 := (+ f4 #455)
|
|
3443 |
#457 := (<= #456 0::real)
|
|
3444 |
#458 := (not #457)
|
|
3445 |
#460 := (+ #459 f3)
|
|
3446 |
#461 := (+ ?v0!5 #77)
|
|
3447 |
#462 := (>= #461 0::real)
|
|
3448 |
#463 := (ite #462 #461 #460)
|
|
3449 |
#464 := (* -1::real #463)
|
|
3450 |
#465 := (+ #97 #464)
|
|
3451 |
#466 := (<= #465 0::real)
|
|
3452 |
#467 := (not #466)
|
|
3453 |
#478 := (+ #477 f5)
|
|
3454 |
#479 := (+ ?v2!3 #124)
|
|
3455 |
#480 := (>= #479 0::real)
|
|
3456 |
#481 := (ite #480 #479 #478)
|
|
3457 |
#482 := (* -1::real #481)
|
|
3458 |
#483 := (+ #97 #482)
|
|
3459 |
#484 := (<= #483 0::real)
|
|
3460 |
#485 := (not #484)
|
|
3461 |
#495 := (+ ?v0!5 #449)
|
|
3462 |
#496 := (<= #495 0::real)
|
|
3463 |
#501 := (+ ?v1!4 #451)
|
|
3464 |
#502 := (<= #501 0::real)
|
|
3465 |
#503 := (and #502 #500 #498 #496 #278 #494 #485 #476 #467)
|
|
3466 |
#504 := (not #503)
|
|
3467 |
#505 := (or #504 #458)
|
|
3468 |
#506 := (not #505)
|
|
3469 |
#640 := (iff #506 #639)
|
|
3470 |
#637 := (iff #505 #636)
|
|
3471 |
#634 := (iff #458 #633)
|
|
3472 |
#631 := (iff #457 #630)
|
|
3473 |
#628 := (= #456 #627)
|
|
3474 |
#625 := (= #455 #624)
|
|
3475 |
#622 := (= #454 #621)
|
|
3476 |
#619 := (= #450 #613)
|
|
3477 |
#620 := [rewrite]: #619
|
|
3478 |
#608 := (= #452 #607)
|
|
3479 |
#609 := [rewrite]: #608
|
|
3480 |
#617 := (iff #453 #614)
|
|
3481 |
#610 := (>= #607 0::real)
|
|
3482 |
#615 := (iff #610 #614)
|
|
3483 |
#616 := [rewrite]: #615
|
|
3484 |
#611 := (iff #453 #610)
|
|
3485 |
#612 := [monotonicity #609]: #611
|
|
3486 |
#618 := [trans #612 #616]: #617
|
|
3487 |
#623 := [monotonicity #618 #609 #620]: #622
|
|
3488 |
#626 := [monotonicity #623]: #625
|
|
3489 |
#629 := [monotonicity #626]: #628
|
|
3490 |
#632 := [monotonicity #629]: #631
|
|
3491 |
#635 := [monotonicity #632]: #634
|
|
3492 |
#605 := (iff #504 #604)
|
|
3493 |
#602 := (iff #503 #599)
|
|
3494 |
#596 := (and #521 #500 #498 #533 #278 #494 #564 #476 #593)
|
|
3495 |
#600 := (iff #596 #599)
|
|
3496 |
#601 := [rewrite]: #600
|
|
3497 |
#597 := (iff #503 #596)
|
|
3498 |
#594 := (iff #467 #593)
|
|
3499 |
#591 := (iff #466 #590)
|
|
3500 |
#588 := (= #465 #587)
|
|
3501 |
#585 := (= #464 #584)
|
|
3502 |
#582 := (= #463 #581)
|
|
3503 |
#579 := (= #460 #573)
|
|
3504 |
#580 := [rewrite]: #579
|
|
3505 |
#568 := (= #461 #567)
|
|
3506 |
#569 := [rewrite]: #568
|
|
3507 |
#577 := (iff #462 #574)
|
|
3508 |
#570 := (>= #567 0::real)
|
|
3509 |
#575 := (iff #570 #574)
|
|
3510 |
#576 := [rewrite]: #575
|
|
3511 |
#571 := (iff #462 #570)
|
|
3512 |
#572 := [monotonicity #569]: #571
|
|
3513 |
#578 := [trans #572 #576]: #577
|
|
3514 |
#583 := [monotonicity #578 #569 #580]: #582
|
|
3515 |
#586 := [monotonicity #583]: #585
|
|
3516 |
#589 := [monotonicity #586]: #588
|
|
3517 |
#592 := [monotonicity #589]: #591
|
|
3518 |
#595 := [monotonicity #592]: #594
|
|
3519 |
#565 := (iff #485 #564)
|
|
3520 |
#562 := (iff #484 #561)
|
|
3521 |
#559 := (= #483 #558)
|
|
3522 |
#556 := (= #482 #555)
|
|
3523 |
#553 := (= #481 #552)
|
|
3524 |
#550 := (= #478 #544)
|
|
3525 |
#551 := [rewrite]: #550
|
|
3526 |
#539 := (= #479 #538)
|
|
3527 |
#540 := [rewrite]: #539
|
|
3528 |
#548 := (iff #480 #545)
|
|
3529 |
#541 := (>= #538 0::real)
|
|
3530 |
#546 := (iff #541 #545)
|
|
3531 |
#547 := [rewrite]: #546
|
|
3532 |
#542 := (iff #480 #541)
|
|
3533 |
#543 := [monotonicity #540]: #542
|
|
3534 |
#549 := [trans #543 #547]: #548
|
|
3535 |
#554 := [monotonicity #549 #540 #551]: #553
|
|
3536 |
#557 := [monotonicity #554]: #556
|
|
3537 |
#560 := [monotonicity #557]: #559
|
|
3538 |
#563 := [monotonicity #560]: #562
|
|
3539 |
#566 := [monotonicity #563]: #565
|
|
3540 |
#536 := (iff #496 #533)
|
|
3541 |
#526 := (+ #449 ?v0!5)
|
|
3542 |
#529 := (<= #526 0::real)
|
|
3543 |
#534 := (iff #529 #533)
|
|
3544 |
#535 := [rewrite]: #534
|
|
3545 |
#530 := (iff #496 #529)
|
|
3546 |
#527 := (= #495 #526)
|
|
3547 |
#528 := [rewrite]: #527
|
|
3548 |
#531 := [monotonicity #528]: #530
|
|
3549 |
#537 := [trans #531 #535]: #536
|
|
3550 |
#524 := (iff #502 #521)
|
|
3551 |
#514 := (+ #451 ?v1!4)
|
|
3552 |
#517 := (<= #514 0::real)
|
|
3553 |
#522 := (iff #517 #521)
|
|
3554 |
#523 := [rewrite]: #522
|
|
3555 |
#518 := (iff #502 #517)
|
|
3556 |
#515 := (= #501 #514)
|
|
3557 |
#516 := [rewrite]: #515
|
|
3558 |
#519 := [monotonicity #516]: #518
|
|
3559 |
#525 := [trans #519 #523]: #524
|
|
3560 |
#598 := [monotonicity #525 #537 #566 #595]: #597
|
|
3561 |
#603 := [trans #598 #601]: #602
|
|
3562 |
#606 := [monotonicity #603]: #605
|
|
3563 |
#638 := [monotonicity #606 #635]: #637
|
|
3564 |
#641 := [monotonicity #638]: #640
|
|
3565 |
#46 := (:var 0 real)
|
|
3566 |
#43 := (:var 1 real)
|
|
3567 |
#217 := (* -1::real #43)
|
|
3568 |
#218 := (+ #217 #46)
|
|
3569 |
#207 := (* -1::real #46)
|
|
3570 |
#208 := (+ #43 #207)
|
|
3571 |
#407 := (>= #208 0::real)
|
|
3572 |
#414 := (ite #407 #208 #218)
|
|
3573 |
#422 := (* -1::real #414)
|
|
3574 |
#423 := (+ f4 #422)
|
|
3575 |
#424 := (<= #423 0::real)
|
|
3576 |
#425 := (not #424)
|
|
3577 |
#8 := (:var 5 real)
|
|
3578 |
#87 := (* -1::real #8)
|
|
3579 |
#88 := (+ #87 f3)
|
|
3580 |
#78 := (+ #8 #77)
|
|
3581 |
#352 := (>= #78 0::real)
|
|
3582 |
#359 := (ite #352 #78 #88)
|
|
3583 |
#367 := (* -1::real #359)
|
|
3584 |
#368 := (+ #97 #367)
|
|
3585 |
#369 := (<= #368 0::real)
|
|
3586 |
#370 := (not #369)
|
|
3587 |
#19 := (:var 4 real)
|
|
3588 |
#112 := (* -1::real #19)
|
|
3589 |
#113 := (+ f3 #112)
|
|
3590 |
#103 := (+ #77 #19)
|
|
3591 |
#329 := (<= #113 0::real)
|
|
3592 |
#336 := (ite #329 #103 #113)
|
|
3593 |
#344 := (* -1::real #336)
|
|
3594 |
#345 := (+ #97 #344)
|
|
3595 |
#346 := (<= #345 0::real)
|
|
3596 |
#347 := (not #346)
|
|
3597 |
#25 := (:var 3 real)
|
|
3598 |
#134 := (* -1::real #25)
|
|
3599 |
#135 := (+ #134 f5)
|
|
3600 |
#125 := (+ #25 #124)
|
|
3601 |
#306 := (>= #125 0::real)
|
|
3602 |
#313 := (ite #306 #125 #135)
|
|
3603 |
#321 := (* -1::real #313)
|
|
3604 |
#322 := (+ #97 #321)
|
|
3605 |
#323 := (<= #322 0::real)
|
|
3606 |
#324 := (not #323)
|
|
3607 |
#32 := (:var 2 real)
|
|
3608 |
#155 := (* -1::real #32)
|
|
3609 |
#156 := (+ f5 #155)
|
|
3610 |
#146 := (+ #124 #32)
|
|
3611 |
#283 := (<= #156 0::real)
|
|
3612 |
#290 := (ite #283 #146 #156)
|
|
3613 |
#298 := (* -1::real #290)
|
|
3614 |
#299 := (+ #97 #298)
|
|
3615 |
#300 := (<= #299 0::real)
|
|
3616 |
#301 := (not #300)
|
|
3617 |
#256 := (+ #8 #217)
|
|
3618 |
#257 := (<= #256 0::real)
|
|
3619 |
#253 := (+ #25 #217)
|
|
3620 |
#252 := (>= #253 0::real)
|
|
3621 |
#249 := (+ #32 #207)
|
|
3622 |
#248 := (>= #249 0::real)
|
|
3623 |
#244 := (+ #19 #207)
|
|
3624 |
#245 := (<= #244 0::real)
|
|
3625 |
#399 := (and #245 #248 #252 #257 #278 #301 #324 #347 #370)
|
|
3626 |
#404 := (not #399)
|
|
3627 |
#430 := (or #404 #425)
|
|
3628 |
#433 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #430)
|
|
3629 |
#436 := (not #433)
|
|
3630 |
#507 := (~ #436 #506)
|
|
3631 |
#508 := [sk]: #507
|
|
3632 |
#57 := (- #43 #46)
|
|
3633 |
#59 := (- #57)
|
|
3634 |
#58 := (< #57 0::real)
|
|
3635 |
#60 := (ite #58 #59 #57)
|
|
3636 |
#61 := (< #60 f4)
|
|
3637 |
#48 := (<= #46 #32)
|
|
3638 |
#47 := (<= #19 #46)
|
|
3639 |
#49 := (and #47 #48)
|
|
3640 |
#45 := (<= #43 #25)
|
|
3641 |
#50 := (and #45 #49)
|
|
3642 |
#44 := (<= #8 #43)
|
|
3643 |
#51 := (and #44 #50)
|
|
3644 |
#16 := 3::real
|
|
3645 |
#17 := (/ f4 3::real)
|
|
3646 |
#38 := (- f3 f5)
|
|
3647 |
#40 := (- #38)
|
|
3648 |
#39 := (< #38 0::real)
|
|
3649 |
#41 := (ite #39 #40 #38)
|
|
3650 |
#42 := (< #41 #17)
|
|
3651 |
#52 := (and #42 #51)
|
|
3652 |
#33 := (- #32 f5)
|
|
3653 |
#35 := (- #33)
|
|
3654 |
#34 := (< #33 0::real)
|
|
3655 |
#36 := (ite #34 #35 #33)
|
|
3656 |
#37 := (< #36 #17)
|
|
3657 |
#53 := (and #37 #52)
|
|
3658 |
#27 := (- #25 f5)
|
|
3659 |
#29 := (- #27)
|
|
3660 |
#28 := (< #27 0::real)
|
|
3661 |
#30 := (ite #28 #29 #27)
|
|
3662 |
#31 := (< #30 #17)
|
|
3663 |
#54 := (and #31 #53)
|
|
3664 |
#20 := (- #19 f3)
|
|
3665 |
#22 := (- #20)
|
|
3666 |
#21 := (< #20 0::real)
|
|
3667 |
#23 := (ite #21 #22 #20)
|
|
3668 |
#24 := (< #23 #17)
|
|
3669 |
#55 := (and #24 #54)
|
|
3670 |
#10 := (- #8 f3)
|
|
3671 |
#13 := (- #10)
|
|
3672 |
#12 := (< #10 0::real)
|
|
3673 |
#14 := (ite #12 #13 #10)
|
|
3674 |
#18 := (< #14 #17)
|
|
3675 |
#56 := (and #18 #55)
|
|
3676 |
#62 := (implies #56 #61)
|
|
3677 |
#63 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #62)
|
|
3678 |
#64 := (not #63)
|
|
3679 |
#439 := (iff #64 #436)
|
|
3680 |
#211 := (< #208 0::real)
|
|
3681 |
#223 := (ite #211 #218 #208)
|
|
3682 |
#226 := (< #223 f4)
|
|
3683 |
#170 := (< #167 0::real)
|
|
3684 |
#181 := (ite #170 #176 #167)
|
|
3685 |
#184 := (< #181 #97)
|
|
3686 |
#190 := (and #51 #184)
|
|
3687 |
#149 := (< #146 0::real)
|
|
3688 |
#161 := (ite #149 #156 #146)
|
|
3689 |
#164 := (< #161 #97)
|
|
3690 |
#195 := (and #164 #190)
|
|
3691 |
#128 := (< #125 0::real)
|
|
3692 |
#140 := (ite #128 #135 #125)
|
|
3693 |
#143 := (< #140 #97)
|
|
3694 |
#198 := (and #143 #195)
|
|
3695 |
#106 := (< #103 0::real)
|
|
3696 |
#118 := (ite #106 #113 #103)
|
|
3697 |
#121 := (< #118 #97)
|
|
3698 |
#201 := (and #121 #198)
|
|
3699 |
#81 := (< #78 0::real)
|
|
3700 |
#93 := (ite #81 #88 #78)
|
|
3701 |
#100 := (< #93 #97)
|
|
3702 |
#204 := (and #100 #201)
|
|
3703 |
#232 := (not #204)
|
|
3704 |
#233 := (or #232 #226)
|
|
3705 |
#238 := (forall (vars (?v0 real) (?v1 real) (?v2 real) (?v3 real) (?v4 real) (?v5 real)) #233)
|
|
3706 |
#241 := (not #238)
|
|
3707 |
#437 := (iff #241 #436)
|
|
3708 |
#434 := (iff #238 #433)
|
|
3709 |
#431 := (iff #233 #430)
|
|
3710 |
#428 := (iff #226 #425)
|
|
3711 |
#419 := (< #414 f4)
|
|
3712 |
#426 := (iff #419 #425)
|
|
3713 |
#427 := [rewrite]: #426
|
|
3714 |
#420 := (iff #226 #419)
|
|
3715 |
#417 := (= #223 #414)
|
|
3716 |
#408 := (not #407)
|
|
3717 |
#411 := (ite #408 #218 #208)
|
|
3718 |
#415 := (= #411 #414)
|
|
3719 |
#416 := [rewrite]: #415
|
|
3720 |
#412 := (= #223 #411)
|
|
3721 |
#409 := (iff #211 #408)
|
|
3722 |
#410 := [rewrite]: #409
|
|
3723 |
#413 := [monotonicity #410]: #412
|
|
3724 |
#418 := [trans #413 #416]: #417
|
|
3725 |
#421 := [monotonicity #418]: #420
|
|
3726 |
#429 := [trans #421 #427]: #428
|
|
3727 |
#405 := (iff #232 #404)
|
|
3728 |
#402 := (iff #204 #399)
|
|
3729 |
#375 := (and #245 #248)
|
|
3730 |
#378 := (and #252 #375)
|
|
3731 |
#381 := (and #257 #378)
|
|
3732 |
#384 := (and #381 #278)
|
|
3733 |
#387 := (and #301 #384)
|
|
3734 |
#390 := (and #324 #387)
|
|
3735 |
#393 := (and #347 #390)
|
|
3736 |
#396 := (and #370 #393)
|
|
3737 |
#400 := (iff #396 #399)
|
|
3738 |
#401 := [rewrite]: #400
|
|
3739 |
#397 := (iff #204 #396)
|
|
3740 |
#394 := (iff #201 #393)
|
|
3741 |
#391 := (iff #198 #390)
|
|
3742 |
#388 := (iff #195 #387)
|
|
3743 |
#385 := (iff #190 #384)
|
|
3744 |
#281 := (iff #184 #278)
|
|
3745 |
#272 := (< #267 #97)
|
|
3746 |
#279 := (iff #272 #278)
|
|
3747 |
#280 := [rewrite]: #279
|
|
3748 |
#273 := (iff #184 #272)
|
|
3749 |
#270 := (= #181 #267)
|
|
3750 |
#261 := (not #260)
|
|
3751 |
#264 := (ite #261 #176 #167)
|
|
3752 |
#268 := (= #264 #267)
|
|
3753 |
#269 := [rewrite]: #268
|
|
3754 |
#265 := (= #181 #264)
|
|
3755 |
#262 := (iff #170 #261)
|
|
3756 |
#263 := [rewrite]: #262
|
|
3757 |
#266 := [monotonicity #263]: #265
|
|
3758 |
#271 := [trans #266 #269]: #270
|
|
3759 |
#274 := [monotonicity #271]: #273
|
|
3760 |
#282 := [trans #274 #280]: #281
|
|
3761 |
#382 := (iff #51 #381)
|
|
3762 |
#379 := (iff #50 #378)
|
|
3763 |
#376 := (iff #49 #375)
|
|
3764 |
#250 := (iff #48 #248)
|
|
3765 |
#251 := [rewrite]: #250
|
|
3766 |
#246 := (iff #47 #245)
|
|
3767 |
#247 := [rewrite]: #246
|
|
3768 |
#377 := [monotonicity #247 #251]: #376
|
|
3769 |
#254 := (iff #45 #252)
|
|
3770 |
#255 := [rewrite]: #254
|
|
3771 |
#380 := [monotonicity #255 #377]: #379
|
|
3772 |
#258 := (iff #44 #257)
|
|
3773 |
#259 := [rewrite]: #258
|
|
3774 |
#383 := [monotonicity #259 #380]: #382
|
|
3775 |
#386 := [monotonicity #383 #282]: #385
|
|
3776 |
#304 := (iff #164 #301)
|
|
3777 |
#295 := (< #290 #97)
|
|
3778 |
#302 := (iff #295 #301)
|
|
3779 |
#303 := [rewrite]: #302
|
|
3780 |
#296 := (iff #164 #295)
|
|
3781 |
#293 := (= #161 #290)
|
|
3782 |
#284 := (not #283)
|
|
3783 |
#287 := (ite #284 #156 #146)
|
|
3784 |
#291 := (= #287 #290)
|
|
3785 |
#292 := [rewrite]: #291
|
|
3786 |
#288 := (= #161 #287)
|
|
3787 |
#285 := (iff #149 #284)
|
|
3788 |
#286 := [rewrite]: #285
|
|
3789 |
#289 := [monotonicity #286]: #288
|
|
3790 |
#294 := [trans #289 #292]: #293
|
|
3791 |
#297 := [monotonicity #294]: #296
|
|
3792 |
#305 := [trans #297 #303]: #304
|
|
3793 |
#389 := [monotonicity #305 #386]: #388
|
|
3794 |
#327 := (iff #143 #324)
|
|
3795 |
#318 := (< #313 #97)
|
|
3796 |
#325 := (iff #318 #324)
|
|
3797 |
#326 := [rewrite]: #325
|
|
3798 |
#319 := (iff #143 #318)
|
|
3799 |
#316 := (= #140 #313)
|
|
3800 |
#307 := (not #306)
|
|
3801 |
#310 := (ite #307 #135 #125)
|
|
3802 |
#314 := (= #310 #313)
|
|
3803 |
#315 := [rewrite]: #314
|
|
3804 |
#311 := (= #140 #310)
|
|
3805 |
#308 := (iff #128 #307)
|
|
3806 |
#309 := [rewrite]: #308
|
|
3807 |
#312 := [monotonicity #309]: #311
|
|
3808 |
#317 := [trans #312 #315]: #316
|
|
3809 |
#320 := [monotonicity #317]: #319
|
|
3810 |
#328 := [trans #320 #326]: #327
|
|
3811 |
#392 := [monotonicity #328 #389]: #391
|
|
3812 |
#350 := (iff #121 #347)
|
|
3813 |
#341 := (< #336 #97)
|
|
3814 |
#348 := (iff #341 #347)
|
|
3815 |
#349 := [rewrite]: #348
|
|
3816 |
#342 := (iff #121 #341)
|
|
3817 |
#339 := (= #118 #336)
|
|
3818 |
#330 := (not #329)
|
|
3819 |
#333 := (ite #330 #113 #103)
|
|
3820 |
#337 := (= #333 #336)
|
|
3821 |
#338 := [rewrite]: #337
|
|
3822 |
#334 := (= #118 #333)
|
|
3823 |
#331 := (iff #106 #330)
|
|
3824 |
#332 := [rewrite]: #331
|
|
3825 |
#335 := [monotonicity #332]: #334
|
|
3826 |
#340 := [trans #335 #338]: #339
|
|
3827 |
#343 := [monotonicity #340]: #342
|
|
3828 |
#351 := [trans #343 #349]: #350
|
|
3829 |
#395 := [monotonicity #351 #392]: #394
|
|
3830 |
#373 := (iff #100 #370)
|
|
3831 |
#364 := (< #359 #97)
|
|
3832 |
#371 := (iff #364 #370)
|
|
3833 |
#372 := [rewrite]: #371
|
|
3834 |
#365 := (iff #100 #364)
|
|
3835 |
#362 := (= #93 #359)
|
|
3836 |
#353 := (not #352)
|
|
3837 |
#356 := (ite #353 #88 #78)
|
|
3838 |
#360 := (= #356 #359)
|
|
3839 |
#361 := [rewrite]: #360
|
|
3840 |
#357 := (= #93 #356)
|
|
3841 |
#354 := (iff #81 #353)
|
|
3842 |
#355 := [rewrite]: #354
|
|
3843 |
#358 := [monotonicity #355]: #357
|
|
3844 |
#363 := [trans #358 #361]: #362
|
|
3845 |
#366 := [monotonicity #363]: #365
|
|
3846 |
#374 := [trans #366 #372]: #373
|
|
3847 |
#398 := [monotonicity #374 #395]: #397
|
|
3848 |
#403 := [trans #398 #401]: #402
|
|
3849 |
#406 := [monotonicity #403]: #405
|
|
3850 |
#432 := [monotonicity #406 #429]: #431
|
|
3851 |
#435 := [quant-intro #432]: #434
|
|
3852 |
#438 := [monotonicity #435]: #437
|
|
3853 |
#242 := (iff #64 #241)
|
|
3854 |
#239 := (iff #63 #238)
|
|
3855 |
#236 := (iff #62 #233)
|
|
3856 |
#229 := (implies #204 #226)
|
|
3857 |
#234 := (iff #229 #233)
|
|
3858 |
#235 := [rewrite]: #234
|
|
3859 |
#230 := (iff #62 #229)
|
|
3860 |
#227 := (iff #61 #226)
|
|
3861 |
#224 := (= #60 #223)
|
|
3862 |
#209 := (= #57 #208)
|
|
3863 |
#210 := [rewrite]: #209
|
|
3864 |
#221 := (= #59 #218)
|
|
3865 |
#214 := (- #208)
|
|
3866 |
#219 := (= #214 #218)
|
|
3867 |
#220 := [rewrite]: #219
|
|
3868 |
#215 := (= #59 #214)
|
|
3869 |
#216 := [monotonicity #210]: #215
|
|
3870 |
#222 := [trans #216 #220]: #221
|
|
3871 |
#212 := (iff #58 #211)
|
|
3872 |
#213 := [monotonicity #210]: #212
|
|
3873 |
#225 := [monotonicity #213 #222 #210]: #224
|
|
3874 |
#228 := [monotonicity #225]: #227
|
|
3875 |
#205 := (iff #56 #204)
|
|
3876 |
#202 := (iff #55 #201)
|
|
3877 |
#199 := (iff #54 #198)
|
|
3878 |
#196 := (iff #53 #195)
|
|
3879 |
#193 := (iff #52 #190)
|
|
3880 |
#187 := (and #184 #51)
|
|
3881 |
#191 := (iff #187 #190)
|
|
3882 |
#192 := [rewrite]: #191
|
|
3883 |
#188 := (iff #52 #187)
|
|
3884 |
#185 := (iff #42 #184)
|
|
3885 |
#98 := (= #17 #97)
|
|
3886 |
#99 := [rewrite]: #98
|
|
3887 |
#182 := (= #41 #181)
|
|
3888 |
#168 := (= #38 #167)
|
|
3889 |
#169 := [rewrite]: #168
|
|
3890 |
#179 := (= #40 #176)
|
|
3891 |
#173 := (- #167)
|
|
3892 |
#177 := (= #173 #176)
|
|
3893 |
#178 := [rewrite]: #177
|
|
3894 |
#174 := (= #40 #173)
|
|
3895 |
#175 := [monotonicity #169]: #174
|
|
3896 |
#180 := [trans #175 #178]: #179
|
|
3897 |
#171 := (iff #39 #170)
|
|
3898 |
#172 := [monotonicity #169]: #171
|
|
3899 |
#183 := [monotonicity #172 #180 #169]: #182
|
|
3900 |
#186 := [monotonicity #183 #99]: #185
|
|
3901 |
#189 := [monotonicity #186]: #188
|
|
3902 |
#194 := [trans #189 #192]: #193
|
|
3903 |
#165 := (iff #37 #164)
|
|
3904 |
#162 := (= #36 #161)
|
|
3905 |
#147 := (= #33 #146)
|
|
3906 |
#148 := [rewrite]: #147
|
|
3907 |
#159 := (= #35 #156)
|
|
3908 |
#152 := (- #146)
|
|
3909 |
#157 := (= #152 #156)
|
|
3910 |
#158 := [rewrite]: #157
|
|
3911 |
#153 := (= #35 #152)
|
|
3912 |
#154 := [monotonicity #148]: #153
|
|
3913 |
#160 := [trans #154 #158]: #159
|
|
3914 |
#150 := (iff #34 #149)
|
|
3915 |
#151 := [monotonicity #148]: #150
|
|
3916 |
#163 := [monotonicity #151 #160 #148]: #162
|
|
3917 |
#166 := [monotonicity #163 #99]: #165
|
|
3918 |
#197 := [monotonicity #166 #194]: #196
|
|
3919 |
#144 := (iff #31 #143)
|
|
3920 |
#141 := (= #30 #140)
|
|
3921 |
#126 := (= #27 #125)
|
|
3922 |
#127 := [rewrite]: #126
|
|
3923 |
#138 := (= #29 #135)
|
|
3924 |
#131 := (- #125)
|
|
3925 |
#136 := (= #131 #135)
|
|
3926 |
#137 := [rewrite]: #136
|
|
3927 |
#132 := (= #29 #131)
|
|
3928 |
#133 := [monotonicity #127]: #132
|
|
3929 |
#139 := [trans #133 #137]: #138
|
|
3930 |
#129 := (iff #28 #128)
|
|
3931 |
#130 := [monotonicity #127]: #129
|
|
3932 |
#142 := [monotonicity #130 #139 #127]: #141
|
|
3933 |
#145 := [monotonicity #142 #99]: #144
|
|
3934 |
#200 := [monotonicity #145 #197]: #199
|
|
3935 |
#122 := (iff #24 #121)
|
|
3936 |
#119 := (= #23 #118)
|
|
3937 |
#104 := (= #20 #103)
|
|
3938 |
#105 := [rewrite]: #104
|
|
3939 |
#116 := (= #22 #113)
|
|
3940 |
#109 := (- #103)
|
|
3941 |
#114 := (= #109 #113)
|
|
3942 |
#115 := [rewrite]: #114
|
|
3943 |
#110 := (= #22 #109)
|
|
3944 |
#111 := [monotonicity #105]: #110
|
|
3945 |
#117 := [trans #111 #115]: #116
|
|
3946 |
#107 := (iff #21 #106)
|
|
3947 |
#108 := [monotonicity #105]: #107
|
|
3948 |
#120 := [monotonicity #108 #117 #105]: #119
|
|
3949 |
#123 := [monotonicity #120 #99]: #122
|
|
3950 |
#203 := [monotonicity #123 #200]: #202
|
|
3951 |
#101 := (iff #18 #100)
|
|
3952 |
#94 := (= #14 #93)
|
|
3953 |
#79 := (= #10 #78)
|
|
3954 |
#80 := [rewrite]: #79
|
|
3955 |
#91 := (= #13 #88)
|
|
3956 |
#84 := (- #78)
|
|
3957 |
#89 := (= #84 #88)
|
|
3958 |
#90 := [rewrite]: #89
|
|
3959 |
#85 := (= #13 #84)
|
|
3960 |
#86 := [monotonicity #80]: #85
|
|
3961 |
#92 := [trans #86 #90]: #91
|
|
3962 |
#82 := (iff #12 #81)
|
|
3963 |
#83 := [monotonicity #80]: #82
|
|
3964 |
#95 := [monotonicity #83 #92 #80]: #94
|
|
3965 |
#102 := [monotonicity #95 #99]: #101
|
|
3966 |
#206 := [monotonicity #102 #203]: #205
|
|
3967 |
#231 := [monotonicity #206 #228]: #230
|
|
3968 |
#237 := [trans #231 #235]: #236
|
|
3969 |
#240 := [quant-intro #237]: #239
|
|
3970 |
#243 := [monotonicity #240]: #242
|
|
3971 |
#440 := [trans #243 #438]: #439
|
|
3972 |
#75 := [asserted]: #64
|
|
3973 |
#441 := [mp #75 #440]: #436
|
|
3974 |
#511 := [mp~ #441 #508]: #506
|
|
3975 |
#512 := [mp #511 #641]: #639
|
|
3976 |
#513 := [not-or-elim #512]: #599
|
|
3977 |
#642 := [and-elim #513]: #278
|
|
3978 |
#644 := [and-elim #513]: #494
|
|
3979 |
#891 := (+ #488 #491)
|
|
3980 |
#892 := (<= #891 0::real)
|
|
3981 |
#720 := (= #488 #490)
|
|
3982 |
#743 := (not #614)
|
|
3983 |
#741 := (= #607 #621)
|
|
3984 |
#884 := (not #741)
|
|
3985 |
#748 := (+ #607 #624)
|
|
3986 |
#750 := (>= #748 0::real)
|
|
3987 |
#778 := (not #750)
|
|
3988 |
#754 := (+ #538 #555)
|
|
3989 |
#755 := (<= #754 0::real)
|
|
3990 |
#777 := (not #755)
|
|
3991 |
#753 := (+ #573 #584)
|
|
3992 |
#756 := (<= #753 0::real)
|
|
3993 |
#735 := (= #573 #581)
|
|
3994 |
#736 := (not #574)
|
|
3995 |
#773 := [hypothesis]: #750
|
|
3996 |
#837 := (or #736 #778)
|
|
3997 |
#648 := [and-elim #513]: #533
|
|
3998 |
#645 := [and-elim #513]: #498
|
|
3999 |
#729 := (not #545)
|
|
4000 |
#727 := (= #538 #552)
|
|
4001 |
#814 := (not #727)
|
|
4002 |
#767 := [hypothesis]: #574
|
|
4003 |
#802 := (or #777 #778 #736)
|
|
4004 |
#763 := (+ #176 #275)
|
|
4005 |
#764 := (<= #763 0::real)
|
|
4006 |
#708 := (= #176 #267)
|
|
4007 |
#757 := (+ #469 #473)
|
|
4008 |
#758 := (<= #757 0::real)
|
|
4009 |
#714 := (= #469 #472)
|
|
4010 |
#715 := (not #471)
|
|
4011 |
#774 := [hypothesis]: #755
|
|
4012 |
#788 := (or #715 #777 #778 #736)
|
|
4013 |
#766 := [hypothesis]: #471
|
|
4014 |
#779 := (or #261 #736 #777 #778 #715)
|
|
4015 |
#649 := [and-elim #513]: #564
|
|
4016 |
#650 := [and-elim #513]: #593
|
|
4017 |
#751 := (+ #567 #584)
|
|
4018 |
#752 := (<= #751 0::real)
|
|
4019 |
#734 := (= #567 #581)
|
|
4020 |
#737 := (or #736 #734)
|
|
4021 |
#738 := [def-axiom]: #737
|
|
4022 |
#768 := [unit-resolution #738 #767]: #734
|
|
4023 |
#769 := (not #734)
|
|
4024 |
#770 := (or #769 #752)
|
|
4025 |
#771 := [th-lemma]: #770
|
|
4026 |
#772 := [unit-resolution #771 #768]: #752
|
|
4027 |
#651 := [not-or-elim #512]: #630
|
|
4028 |
#775 := [hypothesis]: #260
|
|
4029 |
#647 := [and-elim #513]: #521
|
|
4030 |
#776 := [th-lemma #767 #647 #775 #774 #645 #773 #651 #772 #650 #649 #766]: false
|
|
4031 |
#780 := [lemma #776]: #779
|
|
4032 |
#781 := [unit-resolution #780 #766 #774 #773 #767]: #261
|
|
4033 |
#711 := (or #260 #708)
|
|
4034 |
#712 := [def-axiom]: #711
|
|
4035 |
#782 := [unit-resolution #712 #781]: #708
|
|
4036 |
#783 := (not #708)
|
|
4037 |
#784 := (or #783 #764)
|
|
4038 |
#785 := [th-lemma]: #784
|
|
4039 |
#786 := [unit-resolution #785 #782]: #764
|
|
4040 |
#787 := [th-lemma #647 #774 #645 #773 #651 #649 #786 #642 #781 #766]: false
|
|
4041 |
#789 := [lemma #787]: #788
|
|
4042 |
#761 := [unit-resolution #789 #774 #773 #767]: #715
|
|
4043 |
#718 := (or #471 #714)
|
|
4044 |
#719 := [def-axiom]: #718
|
|
4045 |
#762 := [unit-resolution #719 #761]: #714
|
|
4046 |
#765 := (not #714)
|
|
4047 |
#790 := (or #765 #758)
|
|
4048 |
#791 := [th-lemma]: #790
|
|
4049 |
#792 := [unit-resolution #791 #762]: #758
|
|
4050 |
#643 := [and-elim #513]: #476
|
|
4051 |
#795 := (not #758)
|
|
4052 |
#794 := (not #498)
|
|
4053 |
#793 := (not #521)
|
|
4054 |
#796 := (or #261 #471 #793 #777 #794 #778 #633 #561 #795 #475)
|
|
4055 |
#797 := [th-lemma]: #796
|
|
4056 |
#798 := [unit-resolution #797 #761 #643 #645 #647 #649 #651 #773 #774 #792]: #261
|
|
4057 |
#799 := [unit-resolution #712 #798]: #708
|
|
4058 |
#800 := [unit-resolution #785 #799]: #764
|
|
4059 |
#801 := [th-lemma #647 #774 #645 #773 #651 #649 #792 #643 #642 #800]: false
|
|
4060 |
#803 := [lemma #801]: #802
|
|
4061 |
#826 := [unit-resolution #803 #767 #773]: #777
|
|
4062 |
#815 := (or #814 #755)
|
|
4063 |
#804 := [hypothesis]: #777
|
|
4064 |
#805 := [hypothesis]: #727
|
|
4065 |
#816 := [th-lemma]: #815
|
|
4066 |
#817 := [unit-resolution #816 #805 #804]: false
|
|
4067 |
#818 := [lemma #817]: #815
|
|
4068 |
#833 := [unit-resolution #818 #826]: #814
|
|
4069 |
#730 := (or #729 #727)
|
|
4070 |
#731 := [def-axiom]: #730
|
|
4071 |
#834 := [unit-resolution #731 #833]: #729
|
|
4072 |
#831 := (or #260 #545 #778)
|
|
4073 |
#806 := [hypothesis]: #261
|
|
4074 |
#810 := [hypothesis]: #729
|
|
4075 |
#812 := (or #545 #795 #778 #260)
|
|
4076 |
#807 := [unit-resolution #712 #806]: #708
|
|
4077 |
#808 := [unit-resolution #785 #807]: #764
|
|
4078 |
#809 := [hypothesis]: #758
|
|
4079 |
#811 := [th-lemma #810 #645 #809 #643 #647 #773 #651 #808 #642 #806]: false
|
|
4080 |
#813 := [lemma #811]: #812
|
|
4081 |
#827 := [unit-resolution #813 #806 #773 #810]: #795
|
|
4082 |
#821 := [hypothesis]: #795
|
|
4083 |
#822 := [hypothesis]: #714
|
|
4084 |
#823 := [unit-resolution #791 #822 #821]: false
|
|
4085 |
#824 := [lemma #823]: #790
|
|
4086 |
#828 := [unit-resolution #824 #827]: #765
|
|
4087 |
#829 := [unit-resolution #719 #828]: #471
|
|
4088 |
#830 := [th-lemma #808 #642 #829 #810 #645 #647 #773 #651 #806]: false
|
|
4089 |
#832 := [lemma #830]: #831
|
|
4090 |
#835 := [unit-resolution #832 #834 #773]: #260
|
|
4091 |
#836 := [th-lemma #767 #835 #834 #645 #648]: false
|
|
4092 |
#838 := [lemma #836]: #837
|
|
4093 |
#863 := [unit-resolution #838 #773]: #736
|
|
4094 |
#739 := (or #574 #735)
|
|
4095 |
#740 := [def-axiom]: #739
|
|
4096 |
#864 := [unit-resolution #740 #863]: #735
|
|
4097 |
#865 := (not #735)
|
|
4098 |
#866 := (or #865 #756)
|
|
4099 |
#867 := [th-lemma]: #866
|
|
4100 |
#868 := [unit-resolution #867 #864]: #756
|
|
4101 |
#852 := (or #260 #778)
|
|
4102 |
#845 := [unit-resolution #832 #806 #773]: #545
|
|
4103 |
#846 := [unit-resolution #731 #845]: #727
|
|
4104 |
#847 := [unit-resolution #818 #846]: #755
|
|
4105 |
#840 := (not #764)
|
|
4106 |
#841 := (or #795 #777 #778 #840)
|
|
4107 |
#825 := [hypothesis]: #764
|
|
4108 |
#839 := [th-lemma #774 #645 #647 #773 #651 #809 #643 #825 #642 #649]: false
|
|
4109 |
#842 := [lemma #839]: #841
|
|
4110 |
#848 := [unit-resolution #842 #847 #773 #808]: #795
|
|
4111 |
#849 := [unit-resolution #824 #848]: #765
|
|
4112 |
#850 := [unit-resolution #719 #849]: #471
|
|
4113 |
#851 := [th-lemma #847 #649 #645 #647 #773 #651 #808 #850 #806 #642]: false
|
|
4114 |
#853 := [lemma #851]: #852
|
|
4115 |
#859 := [unit-resolution #853 #773]: #260
|
|
4116 |
#870 := (or #471 #778)
|
|
4117 |
#856 := [hypothesis]: #715
|
|
4118 |
#857 := [unit-resolution #719 #856]: #714
|
|
4119 |
#858 := [unit-resolution #824 #857]: #758
|
|
4120 |
#860 := [unit-resolution #797 #858 #643 #645 #647 #649 #651 #773 #859 #856]: #777
|
|
4121 |
#861 := [unit-resolution #818 #860]: #814
|
|
4122 |
#862 := [unit-resolution #731 #861]: #729
|
|
4123 |
#869 := [th-lemma #643 #650 #863 #868 #859 #862 #645 #647 #773 #651 #858]: false
|
|
4124 |
#871 := [lemma #869]: #870
|
|
4125 |
#855 := [unit-resolution #871 #773]: #471
|
|
4126 |
#872 := (not #756)
|
|
4127 |
#873 := (or #777 #590 #574 #872 #561 #261 #794 #793 #778 #633 #715)
|
|
4128 |
#874 := [th-lemma]: #873
|
|
4129 |
#875 := [unit-resolution #874 #855 #645 #647 #649 #863 #650 #651 #773 #859 #868]: #777
|
|
4130 |
#876 := (or #545 #261 #794 #793 #778 #633 #715 #590 #574 #872)
|
|
4131 |
#877 := [th-lemma]: #876
|
|
4132 |
#878 := [unit-resolution #877 #855 #645 #647 #859 #863 #650 #651 #773 #868]: #545
|
|
4133 |
#879 := [unit-resolution #731 #878]: #727
|
|
4134 |
#880 := [unit-resolution #818 #879 #875]: false
|
|
4135 |
#881 := [lemma #880]: #778
|
|
4136 |
#883 := [hypothesis]: #741
|
|
4137 |
#885 := (or #884 #750)
|
|
4138 |
#886 := [th-lemma]: #885
|
|
4139 |
#887 := [unit-resolution #886 #883 #881]: false
|
|
4140 |
#888 := [lemma #887]: #884
|
|
4141 |
#744 := (or #743 #741)
|
|
4142 |
#745 := [def-axiom]: #744
|
|
4143 |
#894 := [unit-resolution #745 #888]: #743
|
|
4144 |
#930 := [hypothesis]: #736
|
|
4145 |
#935 := (or #489 #574)
|
|
4146 |
#931 := [unit-resolution #740 #930]: #735
|
|
4147 |
#893 := [hypothesis]: #872
|
|
4148 |
#915 := [hypothesis]: #735
|
|
4149 |
#916 := [unit-resolution #867 #915 #893]: false
|
|
4150 |
#917 := [lemma #916]: #866
|
|
4151 |
#932 := [unit-resolution #917 #931]: #756
|
|
4152 |
#749 := (+ #613 #624)
|
|
4153 |
#844 := (>= #749 0::real)
|
|
4154 |
#742 := (= #613 #621)
|
|
4155 |
#746 := (or #614 #742)
|
|
4156 |
#747 := [def-axiom]: #746
|
|
4157 |
#895 := [unit-resolution #747 #894]: #742
|
|
4158 |
#896 := (not #742)
|
|
4159 |
#897 := (or #896 #844)
|
|
4160 |
#898 := [th-lemma]: #897
|
|
4161 |
#899 := [unit-resolution #898 #895]: #844
|
|
4162 |
#913 := (or #872 #260)
|
|
4163 |
#900 := [hypothesis]: #756
|
|
4164 |
#646 := [and-elim #513]: #500
|
|
4165 |
#903 := (not #844)
|
|
4166 |
#902 := (not #533)
|
|
4167 |
#901 := (not #500)
|
|
4168 |
#904 := (or #489 #901 #260 #872 #840 #277 #590 #902 #903 #633)
|
|
4169 |
#905 := [th-lemma]: #904
|
|
4170 |
#906 := [unit-resolution #905 #900 #806 #646 #648 #650 #651 #808 #642 #899]: #489
|
|
4171 |
#722 := (not #489)
|
|
4172 |
#723 := (or #722 #720)
|
|
4173 |
#724 := [def-axiom]: #723
|
|
4174 |
#907 := [unit-resolution #724 #906]: #720
|
|
4175 |
#908 := (not #720)
|
|
4176 |
#909 := (or #908 #892)
|
|
4177 |
#910 := [th-lemma]: #909
|
|
4178 |
#911 := [unit-resolution #910 #907]: #892
|
|
4179 |
#912 := [th-lemma #911 #646 #900 #808 #650 #648 #899 #651 #644 #642]: false
|
|
4180 |
#914 := [lemma #912]: #913
|
|
4181 |
#890 := [unit-resolution #914 #806]: #872
|
|
4182 |
#918 := [unit-resolution #917 #890]: #865
|
|
4183 |
#919 := [unit-resolution #740 #918]: #574
|
|
4184 |
#920 := (or #489 #901 #260 #902 #903 #633 #840 #277 #736)
|
|
4185 |
#921 := [th-lemma]: #920
|
|
4186 |
#922 := [unit-resolution #921 #806 #642 #646 #648 #919 #651 #808 #899]: #489
|
|
4187 |
#923 := [unit-resolution #724 #922]: #720
|
|
4188 |
#924 := [unit-resolution #910 #923]: #892
|
|
4189 |
#925 := [th-lemma #924 #646 #806 #648 #899 #651 #808 #919 #644 #642]: false
|
|
4190 |
#926 := [lemma #925]: #260
|
|
4191 |
#933 := [hypothesis]: #722
|
|
4192 |
#934 := [th-lemma #646 #933 #926 #648 #899 #651 #932 #650 #930]: false
|
|
4193 |
#936 := [lemma #934]: #935
|
|
4194 |
#927 := [unit-resolution #936 #930]: #489
|
|
4195 |
#928 := [unit-resolution #724 #927]: #720
|
|
4196 |
#929 := [unit-resolution #910 #928]: #892
|
|
4197 |
#937 := [th-lemma #929 #644 #926 #932 #650 #646 #648 #899 #651 #927]: false
|
|
4198 |
#938 := [lemma #937]: #574
|
|
4199 |
#940 := (or #489 #261 #614 #901 #902 #736)
|
|
4200 |
#941 := [th-lemma]: #940
|
|
4201 |
#942 := [unit-resolution #941 #926 #646 #648 #938 #894]: #489
|
|
4202 |
#943 := [unit-resolution #724 #942]: #720
|
|
4203 |
#944 := [unit-resolution #910 #943]: #892
|
|
4204 |
#760 := (+ #167 #275)
|
|
4205 |
#819 := (<= #760 0::real)
|
|
4206 |
#707 := (= #167 #267)
|
|
4207 |
#709 := (or #261 #707)
|
|
4208 |
#710 := [def-axiom]: #709
|
|
4209 |
#945 := [unit-resolution #710 #926]: #707
|
|
4210 |
#946 := (not #707)
|
|
4211 |
#947 := (or #946 #819)
|
|
4212 |
#948 := [th-lemma]: #947
|
|
4213 |
#949 := [unit-resolution #948 #945]: #819
|
|
4214 |
[th-lemma #926 #949 #646 #648 #899 #651 #938 #944 #644 #642]: false
|
|
4215 |
unsat
|