1.1 --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Wed Mar 24 14:03:52 2010 +0100
1.2 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Wed Mar 24 14:08:07 2010 +0100
1.3 @@ -1,4 +1,4 @@
1.4 -JinTdmjIiorL0/vvOyf3+w 6542 0
1.5 +6164a2366a9e57e212b8ac4aa01e3c8bcc1ea8e0 6542 0
1.6 #2 := false
1.7 decl up_6 :: (-> T4 T2 bool)
1.8 decl ?x47!7 :: (-> T2 T2)
2.1 --- a/src/HOL/Boogie/Examples/Boogie_Max.certs Wed Mar 24 14:03:52 2010 +0100
2.2 +++ b/src/HOL/Boogie/Examples/Boogie_Max.certs Wed Mar 24 14:08:07 2010 +0100
2.3 @@ -1,4 +1,4 @@
2.4 -iks4GfP7O/NgNFyGZ4ynjQ 2224 0
2.5 +cdfef9f27f2a4ba9648f86890c8563d0a1cfe888 2224 0
2.6 #2 := false
2.7 #4 := 0::int
2.8 decl uf_3 :: (-> int int)
3.1 --- a/src/HOL/Boogie/Examples/VCC_Max.certs Wed Mar 24 14:03:52 2010 +0100
3.2 +++ b/src/HOL/Boogie/Examples/VCC_Max.certs Wed Mar 24 14:08:07 2010 +0100
3.3 @@ -1,4 +1,4 @@
3.4 -6Q8QWdFv463DpfVfkr0XnA 7790 0
3.5 +b95bf7adc1e2b959cf13db317b64554768249b2e 7790 0
3.6 #2 := false
3.7 decl uf_110 :: (-> T4 T5 int)
3.8 decl uf_66 :: (-> T5 int T3 T5)
4.1 --- a/src/HOL/Multivariate_Analysis/Integration.cert Wed Mar 24 14:03:52 2010 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.cert Wed Mar 24 14:08:07 2010 +0100
4.3 @@ -1,4 +1,853 @@
4.4 -tB2Atlor9W4pSnrAz5nHpw 907 0
4.5 +534d3afbd3505abffa6b03e3986bfa7aa3cff358 428 0
4.6 +#2 := false
4.7 +decl uf_10 :: T1
4.8 +#38 := uf_10
4.9 +decl uf_3 :: T1
4.10 +#21 := uf_3
4.11 +#45 := (= uf_3 uf_10)
4.12 +decl uf_1 :: (-> int T1)
4.13 +decl uf_2 :: (-> T1 int)
4.14 +#39 := (uf_2 uf_10)
4.15 +#588 := (uf_1 #39)
4.16 +#686 := (= #588 uf_10)
4.17 +#589 := (= uf_10 #588)
4.18 +#4 := (:var 0 T1)
4.19 +#5 := (uf_2 #4)
4.20 +#541 := (pattern #5)
4.21 +#6 := (uf_1 #5)
4.22 +#93 := (= #4 #6)
4.23 +#542 := (forall (vars (?x1 T1)) (:pat #541) #93)
4.24 +#96 := (forall (vars (?x1 T1)) #93)
4.25 +#545 := (iff #96 #542)
4.26 +#543 := (iff #93 #93)
4.27 +#544 := [refl]: #543
4.28 +#546 := [quant-intro #544]: #545
4.29 +#454 := (~ #96 #96)
4.30 +#456 := (~ #93 #93)
4.31 +#457 := [refl]: #456
4.32 +#455 := [nnf-pos #457]: #454
4.33 +#7 := (= #6 #4)
4.34 +#8 := (forall (vars (?x1 T1)) #7)
4.35 +#97 := (iff #8 #96)
4.36 +#94 := (iff #7 #93)
4.37 +#95 := [rewrite]: #94
4.38 +#98 := [quant-intro #95]: #97
4.39 +#92 := [asserted]: #8
4.40 +#101 := [mp #92 #98]: #96
4.41 +#452 := [mp~ #101 #455]: #96
4.42 +#547 := [mp #452 #546]: #542
4.43 +#590 := (not #542)
4.44 +#595 := (or #590 #589)
4.45 +#596 := [quant-inst]: #595
4.46 +#680 := [unit-resolution #596 #547]: #589
4.47 +#687 := [symm #680]: #686
4.48 +#688 := (= uf_3 #588)
4.49 +#22 := (uf_2 uf_3)
4.50 +#586 := (uf_1 #22)
4.51 +#684 := (= #586 #588)
4.52 +#682 := (= #588 #586)
4.53 +#678 := (= #39 #22)
4.54 +#676 := (= #22 #39)
4.55 +#9 := 0::int
4.56 +#227 := -1::int
4.57 +#230 := (* -1::int #39)
4.58 +#231 := (+ #22 #230)
4.59 +#296 := (<= #231 0::int)
4.60 +#70 := (<= #22 #39)
4.61 +#393 := (iff #70 #296)
4.62 +#394 := [rewrite]: #393
4.63 +#347 := [asserted]: #70
4.64 +#395 := [mp #347 #394]: #296
4.65 +#229 := (>= #231 0::int)
4.66 +decl uf_4 :: (-> T2 T3 real)
4.67 +decl uf_6 :: (-> T1 T3)
4.68 +#25 := (uf_6 uf_3)
4.69 +decl uf_7 :: T2
4.70 +#27 := uf_7
4.71 +#28 := (uf_4 uf_7 #25)
4.72 +decl uf_9 :: T2
4.73 +#33 := uf_9
4.74 +#34 := (uf_4 uf_9 #25)
4.75 +#46 := (uf_6 uf_10)
4.76 +decl uf_5 :: T2
4.77 +#24 := uf_5
4.78 +#47 := (uf_4 uf_5 #46)
4.79 +#48 := (ite #45 #47 #34)
4.80 +#256 := (ite #229 #48 #28)
4.81 +#568 := (= #28 #256)
4.82 +#648 := (not #568)
4.83 +#194 := 0::real
4.84 +#192 := -1::real
4.85 +#265 := (* -1::real #256)
4.86 +#640 := (+ #28 #265)
4.87 +#642 := (>= #640 0::real)
4.88 +#645 := (not #642)
4.89 +#643 := [hypothesis]: #642
4.90 +decl uf_8 :: T2
4.91 +#30 := uf_8
4.92 +#31 := (uf_4 uf_8 #25)
4.93 +#266 := (+ #31 #265)
4.94 +#264 := (>= #266 0::real)
4.95 +#267 := (not #264)
4.96 +#26 := (uf_4 uf_5 #25)
4.97 +decl uf_11 :: T2
4.98 +#41 := uf_11
4.99 +#42 := (uf_4 uf_11 #25)
4.100 +#237 := (ite #229 #42 #26)
4.101 +#245 := (* -1::real #237)
4.102 +#246 := (+ #31 #245)
4.103 +#247 := (<= #246 0::real)
4.104 +#248 := (not #247)
4.105 +#272 := (and #248 #267)
4.106 +#40 := (< #22 #39)
4.107 +#49 := (ite #40 #28 #48)
4.108 +#50 := (< #31 #49)
4.109 +#43 := (ite #40 #26 #42)
4.110 +#44 := (< #43 #31)
4.111 +#51 := (and #44 #50)
4.112 +#273 := (iff #51 #272)
4.113 +#270 := (iff #50 #267)
4.114 +#261 := (< #31 #256)
4.115 +#268 := (iff #261 #267)
4.116 +#269 := [rewrite]: #268
4.117 +#262 := (iff #50 #261)
4.118 +#259 := (= #49 #256)
4.119 +#228 := (not #229)
4.120 +#253 := (ite #228 #28 #48)
4.121 +#257 := (= #253 #256)
4.122 +#258 := [rewrite]: #257
4.123 +#254 := (= #49 #253)
4.124 +#232 := (iff #40 #228)
4.125 +#233 := [rewrite]: #232
4.126 +#255 := [monotonicity #233]: #254
4.127 +#260 := [trans #255 #258]: #259
4.128 +#263 := [monotonicity #260]: #262
4.129 +#271 := [trans #263 #269]: #270
4.130 +#251 := (iff #44 #248)
4.131 +#242 := (< #237 #31)
4.132 +#249 := (iff #242 #248)
4.133 +#250 := [rewrite]: #249
4.134 +#243 := (iff #44 #242)
4.135 +#240 := (= #43 #237)
4.136 +#234 := (ite #228 #26 #42)
4.137 +#238 := (= #234 #237)
4.138 +#239 := [rewrite]: #238
4.139 +#235 := (= #43 #234)
4.140 +#236 := [monotonicity #233]: #235
4.141 +#241 := [trans #236 #239]: #240
4.142 +#244 := [monotonicity #241]: #243
4.143 +#252 := [trans #244 #250]: #251
4.144 +#274 := [monotonicity #252 #271]: #273
4.145 +#178 := [asserted]: #51
4.146 +#275 := [mp #178 #274]: #272
4.147 +#277 := [and-elim #275]: #267
4.148 +#196 := (* -1::real #31)
4.149 +#197 := (+ #28 #196)
4.150 +#195 := (>= #197 0::real)
4.151 +#193 := (not #195)
4.152 +#213 := (* -1::real #34)
4.153 +#214 := (+ #31 #213)
4.154 +#212 := (>= #214 0::real)
4.155 +#215 := (not #212)
4.156 +#220 := (and #193 #215)
4.157 +#23 := (< #22 #22)
4.158 +#35 := (ite #23 #28 #34)
4.159 +#36 := (< #31 #35)
4.160 +#29 := (ite #23 #26 #28)
4.161 +#32 := (< #29 #31)
4.162 +#37 := (and #32 #36)
4.163 +#221 := (iff #37 #220)
4.164 +#218 := (iff #36 #215)
4.165 +#209 := (< #31 #34)
4.166 +#216 := (iff #209 #215)
4.167 +#217 := [rewrite]: #216
4.168 +#210 := (iff #36 #209)
4.169 +#207 := (= #35 #34)
4.170 +#202 := (ite false #28 #34)
4.171 +#205 := (= #202 #34)
4.172 +#206 := [rewrite]: #205
4.173 +#203 := (= #35 #202)
4.174 +#180 := (iff #23 false)
4.175 +#181 := [rewrite]: #180
4.176 +#204 := [monotonicity #181]: #203
4.177 +#208 := [trans #204 #206]: #207
4.178 +#211 := [monotonicity #208]: #210
4.179 +#219 := [trans #211 #217]: #218
4.180 +#200 := (iff #32 #193)
4.181 +#189 := (< #28 #31)
4.182 +#198 := (iff #189 #193)
4.183 +#199 := [rewrite]: #198
4.184 +#190 := (iff #32 #189)
4.185 +#187 := (= #29 #28)
4.186 +#182 := (ite false #26 #28)
4.187 +#185 := (= #182 #28)
4.188 +#186 := [rewrite]: #185
4.189 +#183 := (= #29 #182)
4.190 +#184 := [monotonicity #181]: #183
4.191 +#188 := [trans #184 #186]: #187
4.192 +#191 := [monotonicity #188]: #190
4.193 +#201 := [trans #191 #199]: #200
4.194 +#222 := [monotonicity #201 #219]: #221
4.195 +#177 := [asserted]: #37
4.196 +#223 := [mp #177 #222]: #220
4.197 +#224 := [and-elim #223]: #193
4.198 +#644 := [th-lemma #224 #277 #643]: false
4.199 +#646 := [lemma #644]: #645
4.200 +#647 := [hypothesis]: #568
4.201 +#649 := (or #648 #642)
4.202 +#650 := [th-lemma]: #649
4.203 +#651 := [unit-resolution #650 #647 #646]: false
4.204 +#652 := [lemma #651]: #648
4.205 +#578 := (or #229 #568)
4.206 +#579 := [def-axiom]: #578
4.207 +#675 := [unit-resolution #579 #652]: #229
4.208 +#677 := [th-lemma #675 #395]: #676
4.209 +#679 := [symm #677]: #678
4.210 +#683 := [monotonicity #679]: #682
4.211 +#685 := [symm #683]: #684
4.212 +#587 := (= uf_3 #586)
4.213 +#591 := (or #590 #587)
4.214 +#592 := [quant-inst]: #591
4.215 +#681 := [unit-resolution #592 #547]: #587
4.216 +#689 := [trans #681 #685]: #688
4.217 +#690 := [trans #689 #687]: #45
4.218 +#571 := (not #45)
4.219 +#54 := (uf_4 uf_11 #46)
4.220 +#279 := (ite #45 #28 #54)
4.221 +#465 := (* -1::real #279)
4.222 +#632 := (+ #28 #465)
4.223 +#633 := (<= #632 0::real)
4.224 +#580 := (= #28 #279)
4.225 +#656 := [hypothesis]: #45
4.226 +#582 := (or #571 #580)
4.227 +#583 := [def-axiom]: #582
4.228 +#657 := [unit-resolution #583 #656]: #580
4.229 +#658 := (not #580)
4.230 +#659 := (or #658 #633)
4.231 +#660 := [th-lemma]: #659
4.232 +#661 := [unit-resolution #660 #657]: #633
4.233 +#57 := (uf_4 uf_8 #46)
4.234 +#363 := (* -1::real #57)
4.235 +#379 := (+ #47 #363)
4.236 +#380 := (<= #379 0::real)
4.237 +#381 := (not #380)
4.238 +#364 := (+ #54 #363)
4.239 +#362 := (>= #364 0::real)
4.240 +#361 := (not #362)
4.241 +#386 := (and #361 #381)
4.242 +#59 := (uf_4 uf_7 #46)
4.243 +#64 := (< #39 #39)
4.244 +#67 := (ite #64 #59 #47)
4.245 +#68 := (< #57 #67)
4.246 +#65 := (ite #64 #47 #54)
4.247 +#66 := (< #65 #57)
4.248 +#69 := (and #66 #68)
4.249 +#387 := (iff #69 #386)
4.250 +#384 := (iff #68 #381)
4.251 +#376 := (< #57 #47)
4.252 +#382 := (iff #376 #381)
4.253 +#383 := [rewrite]: #382
4.254 +#377 := (iff #68 #376)
4.255 +#374 := (= #67 #47)
4.256 +#369 := (ite false #59 #47)
4.257 +#372 := (= #369 #47)
4.258 +#373 := [rewrite]: #372
4.259 +#370 := (= #67 #369)
4.260 +#349 := (iff #64 false)
4.261 +#350 := [rewrite]: #349
4.262 +#371 := [monotonicity #350]: #370
4.263 +#375 := [trans #371 #373]: #374
4.264 +#378 := [monotonicity #375]: #377
4.265 +#385 := [trans #378 #383]: #384
4.266 +#367 := (iff #66 #361)
4.267 +#358 := (< #54 #57)
4.268 +#365 := (iff #358 #361)
4.269 +#366 := [rewrite]: #365
4.270 +#359 := (iff #66 #358)
4.271 +#356 := (= #65 #54)
4.272 +#351 := (ite false #47 #54)
4.273 +#354 := (= #351 #54)
4.274 +#355 := [rewrite]: #354
4.275 +#352 := (= #65 #351)
4.276 +#353 := [monotonicity #350]: #352
4.277 +#357 := [trans #353 #355]: #356
4.278 +#360 := [monotonicity #357]: #359
4.279 +#368 := [trans #360 #366]: #367
4.280 +#388 := [monotonicity #368 #385]: #387
4.281 +#346 := [asserted]: #69
4.282 +#389 := [mp #346 #388]: #386
4.283 +#391 := [and-elim #389]: #381
4.284 +#397 := (* -1::real #59)
4.285 +#398 := (+ #47 #397)
4.286 +#399 := (<= #398 0::real)
4.287 +#409 := (* -1::real #54)
4.288 +#410 := (+ #47 #409)
4.289 +#408 := (>= #410 0::real)
4.290 +#60 := (uf_4 uf_9 #46)
4.291 +#402 := (* -1::real #60)
4.292 +#403 := (+ #59 #402)
4.293 +#404 := (<= #403 0::real)
4.294 +#418 := (and #399 #404 #408)
4.295 +#73 := (<= #59 #60)
4.296 +#72 := (<= #47 #59)
4.297 +#74 := (and #72 #73)
4.298 +#71 := (<= #54 #47)
4.299 +#75 := (and #71 #74)
4.300 +#421 := (iff #75 #418)
4.301 +#412 := (and #399 #404)
4.302 +#415 := (and #408 #412)
4.303 +#419 := (iff #415 #418)
4.304 +#420 := [rewrite]: #419
4.305 +#416 := (iff #75 #415)
4.306 +#413 := (iff #74 #412)
4.307 +#405 := (iff #73 #404)
4.308 +#406 := [rewrite]: #405
4.309 +#400 := (iff #72 #399)
4.310 +#401 := [rewrite]: #400
4.311 +#414 := [monotonicity #401 #406]: #413
4.312 +#407 := (iff #71 #408)
4.313 +#411 := [rewrite]: #407
4.314 +#417 := [monotonicity #411 #414]: #416
4.315 +#422 := [trans #417 #420]: #421
4.316 +#348 := [asserted]: #75
4.317 +#423 := [mp #348 #422]: #418
4.318 +#424 := [and-elim #423]: #399
4.319 +#637 := (+ #28 #397)
4.320 +#639 := (>= #637 0::real)
4.321 +#636 := (= #28 #59)
4.322 +#666 := (= #59 #28)
4.323 +#664 := (= #46 #25)
4.324 +#662 := (= #25 #46)
4.325 +#663 := [monotonicity #656]: #662
4.326 +#665 := [symm #663]: #664
4.327 +#667 := [monotonicity #665]: #666
4.328 +#668 := [symm #667]: #636
4.329 +#669 := (not #636)
4.330 +#670 := (or #669 #639)
4.331 +#671 := [th-lemma]: #670
4.332 +#672 := [unit-resolution #671 #668]: #639
4.333 +#468 := (+ #57 #465)
4.334 +#471 := (<= #468 0::real)
4.335 +#444 := (not #471)
4.336 +#322 := (ite #296 #279 #47)
4.337 +#330 := (* -1::real #322)
4.338 +#331 := (+ #57 #330)
4.339 +#332 := (<= #331 0::real)
4.340 +#333 := (not #332)
4.341 +#445 := (iff #333 #444)
4.342 +#472 := (iff #332 #471)
4.343 +#469 := (= #331 #468)
4.344 +#466 := (= #330 #465)
4.345 +#463 := (= #322 #279)
4.346 +#1 := true
4.347 +#458 := (ite true #279 #47)
4.348 +#461 := (= #458 #279)
4.349 +#462 := [rewrite]: #461
4.350 +#459 := (= #322 #458)
4.351 +#450 := (iff #296 true)
4.352 +#451 := [iff-true #395]: #450
4.353 +#460 := [monotonicity #451]: #459
4.354 +#464 := [trans #460 #462]: #463
4.355 +#467 := [monotonicity #464]: #466
4.356 +#470 := [monotonicity #467]: #469
4.357 +#473 := [monotonicity #470]: #472
4.358 +#474 := [monotonicity #473]: #445
4.359 +#303 := (ite #296 #60 #59)
4.360 +#313 := (* -1::real #303)
4.361 +#314 := (+ #57 #313)
4.362 +#312 := (>= #314 0::real)
4.363 +#311 := (not #312)
4.364 +#338 := (and #311 #333)
4.365 +#52 := (< #39 #22)
4.366 +#61 := (ite #52 #59 #60)
4.367 +#62 := (< #57 #61)
4.368 +#53 := (= uf_10 uf_3)
4.369 +#55 := (ite #53 #28 #54)
4.370 +#56 := (ite #52 #47 #55)
4.371 +#58 := (< #56 #57)
4.372 +#63 := (and #58 #62)
4.373 +#341 := (iff #63 #338)
4.374 +#282 := (ite #52 #47 #279)
4.375 +#285 := (< #282 #57)
4.376 +#291 := (and #62 #285)
4.377 +#339 := (iff #291 #338)
4.378 +#336 := (iff #285 #333)
4.379 +#327 := (< #322 #57)
4.380 +#334 := (iff #327 #333)
4.381 +#335 := [rewrite]: #334
4.382 +#328 := (iff #285 #327)
4.383 +#325 := (= #282 #322)
4.384 +#297 := (not #296)
4.385 +#319 := (ite #297 #47 #279)
4.386 +#323 := (= #319 #322)
4.387 +#324 := [rewrite]: #323
4.388 +#320 := (= #282 #319)
4.389 +#298 := (iff #52 #297)
4.390 +#299 := [rewrite]: #298
4.391 +#321 := [monotonicity #299]: #320
4.392 +#326 := [trans #321 #324]: #325
4.393 +#329 := [monotonicity #326]: #328
4.394 +#337 := [trans #329 #335]: #336
4.395 +#317 := (iff #62 #311)
4.396 +#308 := (< #57 #303)
4.397 +#315 := (iff #308 #311)
4.398 +#316 := [rewrite]: #315
4.399 +#309 := (iff #62 #308)
4.400 +#306 := (= #61 #303)
4.401 +#300 := (ite #297 #59 #60)
4.402 +#304 := (= #300 #303)
4.403 +#305 := [rewrite]: #304
4.404 +#301 := (= #61 #300)
4.405 +#302 := [monotonicity #299]: #301
4.406 +#307 := [trans #302 #305]: #306
4.407 +#310 := [monotonicity #307]: #309
4.408 +#318 := [trans #310 #316]: #317
4.409 +#340 := [monotonicity #318 #337]: #339
4.410 +#294 := (iff #63 #291)
4.411 +#288 := (and #285 #62)
4.412 +#292 := (iff #288 #291)
4.413 +#293 := [rewrite]: #292
4.414 +#289 := (iff #63 #288)
4.415 +#286 := (iff #58 #285)
4.416 +#283 := (= #56 #282)
4.417 +#280 := (= #55 #279)
4.418 +#226 := (iff #53 #45)
4.419 +#278 := [rewrite]: #226
4.420 +#281 := [monotonicity #278]: #280
4.421 +#284 := [monotonicity #281]: #283
4.422 +#287 := [monotonicity #284]: #286
4.423 +#290 := [monotonicity #287]: #289
4.424 +#295 := [trans #290 #293]: #294
4.425 +#342 := [trans #295 #340]: #341
4.426 +#179 := [asserted]: #63
4.427 +#343 := [mp #179 #342]: #338
4.428 +#345 := [and-elim #343]: #333
4.429 +#475 := [mp #345 #474]: #444
4.430 +#673 := [th-lemma #475 #672 #424 #391 #661]: false
4.431 +#674 := [lemma #673]: #571
4.432 +[unit-resolution #674 #690]: false
4.433 +unsat
4.434 +985f86fd1ea01264c02b8076ffd658677bd4d29a 419 0
4.435 +#2 := false
4.436 +#194 := 0::real
4.437 +decl uf_4 :: (-> T2 T3 real)
4.438 +decl uf_6 :: (-> T1 T3)
4.439 +decl uf_3 :: T1
4.440 +#21 := uf_3
4.441 +#25 := (uf_6 uf_3)
4.442 +decl uf_5 :: T2
4.443 +#24 := uf_5
4.444 +#26 := (uf_4 uf_5 #25)
4.445 +decl uf_7 :: T2
4.446 +#27 := uf_7
4.447 +#28 := (uf_4 uf_7 #25)
4.448 +decl uf_10 :: T1
4.449 +#38 := uf_10
4.450 +#42 := (uf_6 uf_10)
4.451 +decl uf_9 :: T2
4.452 +#33 := uf_9
4.453 +#43 := (uf_4 uf_9 #42)
4.454 +#41 := (= uf_3 uf_10)
4.455 +#44 := (ite #41 #43 #28)
4.456 +#9 := 0::int
4.457 +decl uf_2 :: (-> T1 int)
4.458 +#39 := (uf_2 uf_10)
4.459 +#226 := -1::int
4.460 +#229 := (* -1::int #39)
4.461 +#22 := (uf_2 uf_3)
4.462 +#230 := (+ #22 #229)
4.463 +#228 := (>= #230 0::int)
4.464 +#236 := (ite #228 #44 #26)
4.465 +#192 := -1::real
4.466 +#244 := (* -1::real #236)
4.467 +#642 := (+ #26 #244)
4.468 +#643 := (<= #642 0::real)
4.469 +#567 := (= #26 #236)
4.470 +#227 := (not #228)
4.471 +decl uf_1 :: (-> int T1)
4.472 +#593 := (uf_1 #39)
4.473 +#660 := (= #593 uf_10)
4.474 +#594 := (= uf_10 #593)
4.475 +#4 := (:var 0 T1)
4.476 +#5 := (uf_2 #4)
4.477 +#546 := (pattern #5)
4.478 +#6 := (uf_1 #5)
4.479 +#93 := (= #4 #6)
4.480 +#547 := (forall (vars (?x1 T1)) (:pat #546) #93)
4.481 +#96 := (forall (vars (?x1 T1)) #93)
4.482 +#550 := (iff #96 #547)
4.483 +#548 := (iff #93 #93)
4.484 +#549 := [refl]: #548
4.485 +#551 := [quant-intro #549]: #550
4.486 +#448 := (~ #96 #96)
4.487 +#450 := (~ #93 #93)
4.488 +#451 := [refl]: #450
4.489 +#449 := [nnf-pos #451]: #448
4.490 +#7 := (= #6 #4)
4.491 +#8 := (forall (vars (?x1 T1)) #7)
4.492 +#97 := (iff #8 #96)
4.493 +#94 := (iff #7 #93)
4.494 +#95 := [rewrite]: #94
4.495 +#98 := [quant-intro #95]: #97
4.496 +#92 := [asserted]: #8
4.497 +#101 := [mp #92 #98]: #96
4.498 +#446 := [mp~ #101 #449]: #96
4.499 +#552 := [mp #446 #551]: #547
4.500 +#595 := (not #547)
4.501 +#600 := (or #595 #594)
4.502 +#601 := [quant-inst]: #600
4.503 +#654 := [unit-resolution #601 #552]: #594
4.504 +#680 := [symm #654]: #660
4.505 +#681 := (= uf_3 #593)
4.506 +#591 := (uf_1 #22)
4.507 +#658 := (= #591 #593)
4.508 +#656 := (= #593 #591)
4.509 +#652 := (= #39 #22)
4.510 +#647 := (= #22 #39)
4.511 +#290 := (<= #230 0::int)
4.512 +#70 := (<= #22 #39)
4.513 +#388 := (iff #70 #290)
4.514 +#389 := [rewrite]: #388
4.515 +#341 := [asserted]: #70
4.516 +#390 := [mp #341 #389]: #290
4.517 +#646 := [hypothesis]: #228
4.518 +#648 := [th-lemma #646 #390]: #647
4.519 +#653 := [symm #648]: #652
4.520 +#657 := [monotonicity #653]: #656
4.521 +#659 := [symm #657]: #658
4.522 +#592 := (= uf_3 #591)
4.523 +#596 := (or #595 #592)
4.524 +#597 := [quant-inst]: #596
4.525 +#655 := [unit-resolution #597 #552]: #592
4.526 +#682 := [trans #655 #659]: #681
4.527 +#683 := [trans #682 #680]: #41
4.528 +#570 := (not #41)
4.529 +decl uf_11 :: T2
4.530 +#47 := uf_11
4.531 +#59 := (uf_4 uf_11 #42)
4.532 +#278 := (ite #41 #26 #59)
4.533 +#459 := (* -1::real #278)
4.534 +#637 := (+ #26 #459)
4.535 +#639 := (>= #637 0::real)
4.536 +#585 := (= #26 #278)
4.537 +#661 := [hypothesis]: #41
4.538 +#587 := (or #570 #585)
4.539 +#588 := [def-axiom]: #587
4.540 +#662 := [unit-resolution #588 #661]: #585
4.541 +#663 := (not #585)
4.542 +#664 := (or #663 #639)
4.543 +#665 := [th-lemma]: #664
4.544 +#666 := [unit-resolution #665 #662]: #639
4.545 +decl uf_8 :: T2
4.546 +#30 := uf_8
4.547 +#56 := (uf_4 uf_8 #42)
4.548 +#357 := (* -1::real #56)
4.549 +#358 := (+ #43 #357)
4.550 +#356 := (>= #358 0::real)
4.551 +#355 := (not #356)
4.552 +#374 := (* -1::real #59)
4.553 +#375 := (+ #56 #374)
4.554 +#373 := (>= #375 0::real)
4.555 +#376 := (not #373)
4.556 +#381 := (and #355 #376)
4.557 +#64 := (< #39 #39)
4.558 +#67 := (ite #64 #43 #59)
4.559 +#68 := (< #56 #67)
4.560 +#53 := (uf_4 uf_5 #42)
4.561 +#65 := (ite #64 #53 #43)
4.562 +#66 := (< #65 #56)
4.563 +#69 := (and #66 #68)
4.564 +#382 := (iff #69 #381)
4.565 +#379 := (iff #68 #376)
4.566 +#370 := (< #56 #59)
4.567 +#377 := (iff #370 #376)
4.568 +#378 := [rewrite]: #377
4.569 +#371 := (iff #68 #370)
4.570 +#368 := (= #67 #59)
4.571 +#363 := (ite false #43 #59)
4.572 +#366 := (= #363 #59)
4.573 +#367 := [rewrite]: #366
4.574 +#364 := (= #67 #363)
4.575 +#343 := (iff #64 false)
4.576 +#344 := [rewrite]: #343
4.577 +#365 := [monotonicity #344]: #364
4.578 +#369 := [trans #365 #367]: #368
4.579 +#372 := [monotonicity #369]: #371
4.580 +#380 := [trans #372 #378]: #379
4.581 +#361 := (iff #66 #355)
4.582 +#352 := (< #43 #56)
4.583 +#359 := (iff #352 #355)
4.584 +#360 := [rewrite]: #359
4.585 +#353 := (iff #66 #352)
4.586 +#350 := (= #65 #43)
4.587 +#345 := (ite false #53 #43)
4.588 +#348 := (= #345 #43)
4.589 +#349 := [rewrite]: #348
4.590 +#346 := (= #65 #345)
4.591 +#347 := [monotonicity #344]: #346
4.592 +#351 := [trans #347 #349]: #350
4.593 +#354 := [monotonicity #351]: #353
4.594 +#362 := [trans #354 #360]: #361
4.595 +#383 := [monotonicity #362 #380]: #382
4.596 +#340 := [asserted]: #69
4.597 +#384 := [mp #340 #383]: #381
4.598 +#385 := [and-elim #384]: #355
4.599 +#394 := (* -1::real #53)
4.600 +#395 := (+ #43 #394)
4.601 +#393 := (>= #395 0::real)
4.602 +#54 := (uf_4 uf_7 #42)
4.603 +#402 := (* -1::real #54)
4.604 +#403 := (+ #53 #402)
4.605 +#401 := (>= #403 0::real)
4.606 +#397 := (+ #43 #374)
4.607 +#398 := (<= #397 0::real)
4.608 +#412 := (and #393 #398 #401)
4.609 +#73 := (<= #43 #59)
4.610 +#72 := (<= #53 #43)
4.611 +#74 := (and #72 #73)
4.612 +#71 := (<= #54 #53)
4.613 +#75 := (and #71 #74)
4.614 +#415 := (iff #75 #412)
4.615 +#406 := (and #393 #398)
4.616 +#409 := (and #401 #406)
4.617 +#413 := (iff #409 #412)
4.618 +#414 := [rewrite]: #413
4.619 +#410 := (iff #75 #409)
4.620 +#407 := (iff #74 #406)
4.621 +#399 := (iff #73 #398)
4.622 +#400 := [rewrite]: #399
4.623 +#392 := (iff #72 #393)
4.624 +#396 := [rewrite]: #392
4.625 +#408 := [monotonicity #396 #400]: #407
4.626 +#404 := (iff #71 #401)
4.627 +#405 := [rewrite]: #404
4.628 +#411 := [monotonicity #405 #408]: #410
4.629 +#416 := [trans #411 #414]: #415
4.630 +#342 := [asserted]: #75
4.631 +#417 := [mp #342 #416]: #412
4.632 +#418 := [and-elim #417]: #393
4.633 +#650 := (+ #26 #394)
4.634 +#651 := (<= #650 0::real)
4.635 +#649 := (= #26 #53)
4.636 +#671 := (= #53 #26)
4.637 +#669 := (= #42 #25)
4.638 +#667 := (= #25 #42)
4.639 +#668 := [monotonicity #661]: #667
4.640 +#670 := [symm #668]: #669
4.641 +#672 := [monotonicity #670]: #671
4.642 +#673 := [symm #672]: #649
4.643 +#674 := (not #649)
4.644 +#675 := (or #674 #651)
4.645 +#676 := [th-lemma]: #675
4.646 +#677 := [unit-resolution #676 #673]: #651
4.647 +#462 := (+ #56 #459)
4.648 +#465 := (>= #462 0::real)
4.649 +#438 := (not #465)
4.650 +#316 := (ite #290 #278 #43)
4.651 +#326 := (* -1::real #316)
4.652 +#327 := (+ #56 #326)
4.653 +#325 := (>= #327 0::real)
4.654 +#324 := (not #325)
4.655 +#439 := (iff #324 #438)
4.656 +#466 := (iff #325 #465)
4.657 +#463 := (= #327 #462)
4.658 +#460 := (= #326 #459)
4.659 +#457 := (= #316 #278)
4.660 +#1 := true
4.661 +#452 := (ite true #278 #43)
4.662 +#455 := (= #452 #278)
4.663 +#456 := [rewrite]: #455
4.664 +#453 := (= #316 #452)
4.665 +#444 := (iff #290 true)
4.666 +#445 := [iff-true #390]: #444
4.667 +#454 := [monotonicity #445]: #453
4.668 +#458 := [trans #454 #456]: #457
4.669 +#461 := [monotonicity #458]: #460
4.670 +#464 := [monotonicity #461]: #463
4.671 +#467 := [monotonicity #464]: #466
4.672 +#468 := [monotonicity #467]: #439
4.673 +#297 := (ite #290 #54 #53)
4.674 +#305 := (* -1::real #297)
4.675 +#306 := (+ #56 #305)
4.676 +#307 := (<= #306 0::real)
4.677 +#308 := (not #307)
4.678 +#332 := (and #308 #324)
4.679 +#58 := (= uf_10 uf_3)
4.680 +#60 := (ite #58 #26 #59)
4.681 +#52 := (< #39 #22)
4.682 +#61 := (ite #52 #43 #60)
4.683 +#62 := (< #56 #61)
4.684 +#55 := (ite #52 #53 #54)
4.685 +#57 := (< #55 #56)
4.686 +#63 := (and #57 #62)
4.687 +#335 := (iff #63 #332)
4.688 +#281 := (ite #52 #43 #278)
4.689 +#284 := (< #56 #281)
4.690 +#287 := (and #57 #284)
4.691 +#333 := (iff #287 #332)
4.692 +#330 := (iff #284 #324)
4.693 +#321 := (< #56 #316)
4.694 +#328 := (iff #321 #324)
4.695 +#329 := [rewrite]: #328
4.696 +#322 := (iff #284 #321)
4.697 +#319 := (= #281 #316)
4.698 +#291 := (not #290)
4.699 +#313 := (ite #291 #43 #278)
4.700 +#317 := (= #313 #316)
4.701 +#318 := [rewrite]: #317
4.702 +#314 := (= #281 #313)
4.703 +#292 := (iff #52 #291)
4.704 +#293 := [rewrite]: #292
4.705 +#315 := [monotonicity #293]: #314
4.706 +#320 := [trans #315 #318]: #319
4.707 +#323 := [monotonicity #320]: #322
4.708 +#331 := [trans #323 #329]: #330
4.709 +#311 := (iff #57 #308)
4.710 +#302 := (< #297 #56)
4.711 +#309 := (iff #302 #308)
4.712 +#310 := [rewrite]: #309
4.713 +#303 := (iff #57 #302)
4.714 +#300 := (= #55 #297)
4.715 +#294 := (ite #291 #53 #54)
4.716 +#298 := (= #294 #297)
4.717 +#299 := [rewrite]: #298
4.718 +#295 := (= #55 #294)
4.719 +#296 := [monotonicity #293]: #295
4.720 +#301 := [trans #296 #299]: #300
4.721 +#304 := [monotonicity #301]: #303
4.722 +#312 := [trans #304 #310]: #311
4.723 +#334 := [monotonicity #312 #331]: #333
4.724 +#288 := (iff #63 #287)
4.725 +#285 := (iff #62 #284)
4.726 +#282 := (= #61 #281)
4.727 +#279 := (= #60 #278)
4.728 +#225 := (iff #58 #41)
4.729 +#277 := [rewrite]: #225
4.730 +#280 := [monotonicity #277]: #279
4.731 +#283 := [monotonicity #280]: #282
4.732 +#286 := [monotonicity #283]: #285
4.733 +#289 := [monotonicity #286]: #288
4.734 +#336 := [trans #289 #334]: #335
4.735 +#179 := [asserted]: #63
4.736 +#337 := [mp #179 #336]: #332
4.737 +#339 := [and-elim #337]: #324
4.738 +#469 := [mp #339 #468]: #438
4.739 +#678 := [th-lemma #469 #677 #418 #385 #666]: false
4.740 +#679 := [lemma #678]: #570
4.741 +#684 := [unit-resolution #679 #683]: false
4.742 +#685 := [lemma #684]: #227
4.743 +#577 := (or #228 #567)
4.744 +#578 := [def-axiom]: #577
4.745 +#645 := [unit-resolution #578 #685]: #567
4.746 +#686 := (not #567)
4.747 +#687 := (or #686 #643)
4.748 +#688 := [th-lemma]: #687
4.749 +#689 := [unit-resolution #688 #645]: #643
4.750 +#31 := (uf_4 uf_8 #25)
4.751 +#245 := (+ #31 #244)
4.752 +#246 := (<= #245 0::real)
4.753 +#247 := (not #246)
4.754 +#34 := (uf_4 uf_9 #25)
4.755 +#48 := (uf_4 uf_11 #25)
4.756 +#255 := (ite #228 #48 #34)
4.757 +#264 := (* -1::real #255)
4.758 +#265 := (+ #31 #264)
4.759 +#263 := (>= #265 0::real)
4.760 +#266 := (not #263)
4.761 +#271 := (and #247 #266)
4.762 +#40 := (< #22 #39)
4.763 +#49 := (ite #40 #34 #48)
4.764 +#50 := (< #31 #49)
4.765 +#45 := (ite #40 #26 #44)
4.766 +#46 := (< #45 #31)
4.767 +#51 := (and #46 #50)
4.768 +#272 := (iff #51 #271)
4.769 +#269 := (iff #50 #266)
4.770 +#260 := (< #31 #255)
4.771 +#267 := (iff #260 #266)
4.772 +#268 := [rewrite]: #267
4.773 +#261 := (iff #50 #260)
4.774 +#258 := (= #49 #255)
4.775 +#252 := (ite #227 #34 #48)
4.776 +#256 := (= #252 #255)
4.777 +#257 := [rewrite]: #256
4.778 +#253 := (= #49 #252)
4.779 +#231 := (iff #40 #227)
4.780 +#232 := [rewrite]: #231
4.781 +#254 := [monotonicity #232]: #253
4.782 +#259 := [trans #254 #257]: #258
4.783 +#262 := [monotonicity #259]: #261
4.784 +#270 := [trans #262 #268]: #269
4.785 +#250 := (iff #46 #247)
4.786 +#241 := (< #236 #31)
4.787 +#248 := (iff #241 #247)
4.788 +#249 := [rewrite]: #248
4.789 +#242 := (iff #46 #241)
4.790 +#239 := (= #45 #236)
4.791 +#233 := (ite #227 #26 #44)
4.792 +#237 := (= #233 #236)
4.793 +#238 := [rewrite]: #237
4.794 +#234 := (= #45 #233)
4.795 +#235 := [monotonicity #232]: #234
4.796 +#240 := [trans #235 #238]: #239
4.797 +#243 := [monotonicity #240]: #242
4.798 +#251 := [trans #243 #249]: #250
4.799 +#273 := [monotonicity #251 #270]: #272
4.800 +#178 := [asserted]: #51
4.801 +#274 := [mp #178 #273]: #271
4.802 +#275 := [and-elim #274]: #247
4.803 +#196 := (* -1::real #31)
4.804 +#212 := (+ #26 #196)
4.805 +#213 := (<= #212 0::real)
4.806 +#214 := (not #213)
4.807 +#197 := (+ #28 #196)
4.808 +#195 := (>= #197 0::real)
4.809 +#193 := (not #195)
4.810 +#219 := (and #193 #214)
4.811 +#23 := (< #22 #22)
4.812 +#35 := (ite #23 #34 #26)
4.813 +#36 := (< #31 #35)
4.814 +#29 := (ite #23 #26 #28)
4.815 +#32 := (< #29 #31)
4.816 +#37 := (and #32 #36)
4.817 +#220 := (iff #37 #219)
4.818 +#217 := (iff #36 #214)
4.819 +#209 := (< #31 #26)
4.820 +#215 := (iff #209 #214)
4.821 +#216 := [rewrite]: #215
4.822 +#210 := (iff #36 #209)
4.823 +#207 := (= #35 #26)
4.824 +#202 := (ite false #34 #26)
4.825 +#205 := (= #202 #26)
4.826 +#206 := [rewrite]: #205
4.827 +#203 := (= #35 #202)
4.828 +#180 := (iff #23 false)
4.829 +#181 := [rewrite]: #180
4.830 +#204 := [monotonicity #181]: #203
4.831 +#208 := [trans #204 #206]: #207
4.832 +#211 := [monotonicity #208]: #210
4.833 +#218 := [trans #211 #216]: #217
4.834 +#200 := (iff #32 #193)
4.835 +#189 := (< #28 #31)
4.836 +#198 := (iff #189 #193)
4.837 +#199 := [rewrite]: #198
4.838 +#190 := (iff #32 #189)
4.839 +#187 := (= #29 #28)
4.840 +#182 := (ite false #26 #28)
4.841 +#185 := (= #182 #28)
4.842 +#186 := [rewrite]: #185
4.843 +#183 := (= #29 #182)
4.844 +#184 := [monotonicity #181]: #183
4.845 +#188 := [trans #184 #186]: #187
4.846 +#191 := [monotonicity #188]: #190
4.847 +#201 := [trans #191 #199]: #200
4.848 +#221 := [monotonicity #201 #218]: #220
4.849 +#177 := [asserted]: #37
4.850 +#222 := [mp #177 #221]: #219
4.851 +#224 := [and-elim #222]: #214
4.852 +[th-lemma #224 #275 #689]: false
4.853 +unsat
4.854 +00b949278548f13329cf92f11a0ad2161fa40793 907 0
4.855 #2 := false
4.856 #299 := 0::real
4.857 decl uf_1 :: (-> T3 T2 real)
4.858 @@ -906,856 +1755,7 @@
4.859 #1366 := [unit-resolution #1233 #1365]: #1231
4.860 [th-lemma #1366 #1364 #1362]: false
4.861 unsat
4.862 -NQHwTeL311Tq3wf2s5BReA 419 0
4.863 -#2 := false
4.864 -#194 := 0::real
4.865 -decl uf_4 :: (-> T2 T3 real)
4.866 -decl uf_6 :: (-> T1 T3)
4.867 -decl uf_3 :: T1
4.868 -#21 := uf_3
4.869 -#25 := (uf_6 uf_3)
4.870 -decl uf_5 :: T2
4.871 -#24 := uf_5
4.872 -#26 := (uf_4 uf_5 #25)
4.873 -decl uf_7 :: T2
4.874 -#27 := uf_7
4.875 -#28 := (uf_4 uf_7 #25)
4.876 -decl uf_10 :: T1
4.877 -#38 := uf_10
4.878 -#42 := (uf_6 uf_10)
4.879 -decl uf_9 :: T2
4.880 -#33 := uf_9
4.881 -#43 := (uf_4 uf_9 #42)
4.882 -#41 := (= uf_3 uf_10)
4.883 -#44 := (ite #41 #43 #28)
4.884 -#9 := 0::int
4.885 -decl uf_2 :: (-> T1 int)
4.886 -#39 := (uf_2 uf_10)
4.887 -#226 := -1::int
4.888 -#229 := (* -1::int #39)
4.889 -#22 := (uf_2 uf_3)
4.890 -#230 := (+ #22 #229)
4.891 -#228 := (>= #230 0::int)
4.892 -#236 := (ite #228 #44 #26)
4.893 -#192 := -1::real
4.894 -#244 := (* -1::real #236)
4.895 -#642 := (+ #26 #244)
4.896 -#643 := (<= #642 0::real)
4.897 -#567 := (= #26 #236)
4.898 -#227 := (not #228)
4.899 -decl uf_1 :: (-> int T1)
4.900 -#593 := (uf_1 #39)
4.901 -#660 := (= #593 uf_10)
4.902 -#594 := (= uf_10 #593)
4.903 -#4 := (:var 0 T1)
4.904 -#5 := (uf_2 #4)
4.905 -#546 := (pattern #5)
4.906 -#6 := (uf_1 #5)
4.907 -#93 := (= #4 #6)
4.908 -#547 := (forall (vars (?x1 T1)) (:pat #546) #93)
4.909 -#96 := (forall (vars (?x1 T1)) #93)
4.910 -#550 := (iff #96 #547)
4.911 -#548 := (iff #93 #93)
4.912 -#549 := [refl]: #548
4.913 -#551 := [quant-intro #549]: #550
4.914 -#448 := (~ #96 #96)
4.915 -#450 := (~ #93 #93)
4.916 -#451 := [refl]: #450
4.917 -#449 := [nnf-pos #451]: #448
4.918 -#7 := (= #6 #4)
4.919 -#8 := (forall (vars (?x1 T1)) #7)
4.920 -#97 := (iff #8 #96)
4.921 -#94 := (iff #7 #93)
4.922 -#95 := [rewrite]: #94
4.923 -#98 := [quant-intro #95]: #97
4.924 -#92 := [asserted]: #8
4.925 -#101 := [mp #92 #98]: #96
4.926 -#446 := [mp~ #101 #449]: #96
4.927 -#552 := [mp #446 #551]: #547
4.928 -#595 := (not #547)
4.929 -#600 := (or #595 #594)
4.930 -#601 := [quant-inst]: #600
4.931 -#654 := [unit-resolution #601 #552]: #594
4.932 -#680 := [symm #654]: #660
4.933 -#681 := (= uf_3 #593)
4.934 -#591 := (uf_1 #22)
4.935 -#658 := (= #591 #593)
4.936 -#656 := (= #593 #591)
4.937 -#652 := (= #39 #22)
4.938 -#647 := (= #22 #39)
4.939 -#290 := (<= #230 0::int)
4.940 -#70 := (<= #22 #39)
4.941 -#388 := (iff #70 #290)
4.942 -#389 := [rewrite]: #388
4.943 -#341 := [asserted]: #70
4.944 -#390 := [mp #341 #389]: #290
4.945 -#646 := [hypothesis]: #228
4.946 -#648 := [th-lemma #646 #390]: #647
4.947 -#653 := [symm #648]: #652
4.948 -#657 := [monotonicity #653]: #656
4.949 -#659 := [symm #657]: #658
4.950 -#592 := (= uf_3 #591)
4.951 -#596 := (or #595 #592)
4.952 -#597 := [quant-inst]: #596
4.953 -#655 := [unit-resolution #597 #552]: #592
4.954 -#682 := [trans #655 #659]: #681
4.955 -#683 := [trans #682 #680]: #41
4.956 -#570 := (not #41)
4.957 -decl uf_11 :: T2
4.958 -#47 := uf_11
4.959 -#59 := (uf_4 uf_11 #42)
4.960 -#278 := (ite #41 #26 #59)
4.961 -#459 := (* -1::real #278)
4.962 -#637 := (+ #26 #459)
4.963 -#639 := (>= #637 0::real)
4.964 -#585 := (= #26 #278)
4.965 -#661 := [hypothesis]: #41
4.966 -#587 := (or #570 #585)
4.967 -#588 := [def-axiom]: #587
4.968 -#662 := [unit-resolution #588 #661]: #585
4.969 -#663 := (not #585)
4.970 -#664 := (or #663 #639)
4.971 -#665 := [th-lemma]: #664
4.972 -#666 := [unit-resolution #665 #662]: #639
4.973 -decl uf_8 :: T2
4.974 -#30 := uf_8
4.975 -#56 := (uf_4 uf_8 #42)
4.976 -#357 := (* -1::real #56)
4.977 -#358 := (+ #43 #357)
4.978 -#356 := (>= #358 0::real)
4.979 -#355 := (not #356)
4.980 -#374 := (* -1::real #59)
4.981 -#375 := (+ #56 #374)
4.982 -#373 := (>= #375 0::real)
4.983 -#376 := (not #373)
4.984 -#381 := (and #355 #376)
4.985 -#64 := (< #39 #39)
4.986 -#67 := (ite #64 #43 #59)
4.987 -#68 := (< #56 #67)
4.988 -#53 := (uf_4 uf_5 #42)
4.989 -#65 := (ite #64 #53 #43)
4.990 -#66 := (< #65 #56)
4.991 -#69 := (and #66 #68)
4.992 -#382 := (iff #69 #381)
4.993 -#379 := (iff #68 #376)
4.994 -#370 := (< #56 #59)
4.995 -#377 := (iff #370 #376)
4.996 -#378 := [rewrite]: #377
4.997 -#371 := (iff #68 #370)
4.998 -#368 := (= #67 #59)
4.999 -#363 := (ite false #43 #59)
4.1000 -#366 := (= #363 #59)
4.1001 -#367 := [rewrite]: #366
4.1002 -#364 := (= #67 #363)
4.1003 -#343 := (iff #64 false)
4.1004 -#344 := [rewrite]: #343
4.1005 -#365 := [monotonicity #344]: #364
4.1006 -#369 := [trans #365 #367]: #368
4.1007 -#372 := [monotonicity #369]: #371
4.1008 -#380 := [trans #372 #378]: #379
4.1009 -#361 := (iff #66 #355)
4.1010 -#352 := (< #43 #56)
4.1011 -#359 := (iff #352 #355)
4.1012 -#360 := [rewrite]: #359
4.1013 -#353 := (iff #66 #352)
4.1014 -#350 := (= #65 #43)
4.1015 -#345 := (ite false #53 #43)
4.1016 -#348 := (= #345 #43)
4.1017 -#349 := [rewrite]: #348
4.1018 -#346 := (= #65 #345)
4.1019 -#347 := [monotonicity #344]: #346
4.1020 -#351 := [trans #347 #349]: #350
4.1021 -#354 := [monotonicity #351]: #353
4.1022 -#362 := [trans #354 #360]: #361
4.1023 -#383 := [monotonicity #362 #380]: #382
4.1024 -#340 := [asserted]: #69
4.1025 -#384 := [mp #340 #383]: #381
4.1026 -#385 := [and-elim #384]: #355
4.1027 -#394 := (* -1::real #53)
4.1028 -#395 := (+ #43 #394)
4.1029 -#393 := (>= #395 0::real)
4.1030 -#54 := (uf_4 uf_7 #42)
4.1031 -#402 := (* -1::real #54)
4.1032 -#403 := (+ #53 #402)
4.1033 -#401 := (>= #403 0::real)
4.1034 -#397 := (+ #43 #374)
4.1035 -#398 := (<= #397 0::real)
4.1036 -#412 := (and #393 #398 #401)
4.1037 -#73 := (<= #43 #59)
4.1038 -#72 := (<= #53 #43)
4.1039 -#74 := (and #72 #73)
4.1040 -#71 := (<= #54 #53)
4.1041 -#75 := (and #71 #74)
4.1042 -#415 := (iff #75 #412)
4.1043 -#406 := (and #393 #398)
4.1044 -#409 := (and #401 #406)
4.1045 -#413 := (iff #409 #412)
4.1046 -#414 := [rewrite]: #413
4.1047 -#410 := (iff #75 #409)
4.1048 -#407 := (iff #74 #406)
4.1049 -#399 := (iff #73 #398)
4.1050 -#400 := [rewrite]: #399
4.1051 -#392 := (iff #72 #393)
4.1052 -#396 := [rewrite]: #392
4.1053 -#408 := [monotonicity #396 #400]: #407
4.1054 -#404 := (iff #71 #401)
4.1055 -#405 := [rewrite]: #404
4.1056 -#411 := [monotonicity #405 #408]: #410
4.1057 -#416 := [trans #411 #414]: #415
4.1058 -#342 := [asserted]: #75
4.1059 -#417 := [mp #342 #416]: #412
4.1060 -#418 := [and-elim #417]: #393
4.1061 -#650 := (+ #26 #394)
4.1062 -#651 := (<= #650 0::real)
4.1063 -#649 := (= #26 #53)
4.1064 -#671 := (= #53 #26)
4.1065 -#669 := (= #42 #25)
4.1066 -#667 := (= #25 #42)
4.1067 -#668 := [monotonicity #661]: #667
4.1068 -#670 := [symm #668]: #669
4.1069 -#672 := [monotonicity #670]: #671
4.1070 -#673 := [symm #672]: #649
4.1071 -#674 := (not #649)
4.1072 -#675 := (or #674 #651)
4.1073 -#676 := [th-lemma]: #675
4.1074 -#677 := [unit-resolution #676 #673]: #651
4.1075 -#462 := (+ #56 #459)
4.1076 -#465 := (>= #462 0::real)
4.1077 -#438 := (not #465)
4.1078 -#316 := (ite #290 #278 #43)
4.1079 -#326 := (* -1::real #316)
4.1080 -#327 := (+ #56 #326)
4.1081 -#325 := (>= #327 0::real)
4.1082 -#324 := (not #325)
4.1083 -#439 := (iff #324 #438)
4.1084 -#466 := (iff #325 #465)
4.1085 -#463 := (= #327 #462)
4.1086 -#460 := (= #326 #459)
4.1087 -#457 := (= #316 #278)
4.1088 -#1 := true
4.1089 -#452 := (ite true #278 #43)
4.1090 -#455 := (= #452 #278)
4.1091 -#456 := [rewrite]: #455
4.1092 -#453 := (= #316 #452)
4.1093 -#444 := (iff #290 true)
4.1094 -#445 := [iff-true #390]: #444
4.1095 -#454 := [monotonicity #445]: #453
4.1096 -#458 := [trans #454 #456]: #457
4.1097 -#461 := [monotonicity #458]: #460
4.1098 -#464 := [monotonicity #461]: #463
4.1099 -#467 := [monotonicity #464]: #466
4.1100 -#468 := [monotonicity #467]: #439
4.1101 -#297 := (ite #290 #54 #53)
4.1102 -#305 := (* -1::real #297)
4.1103 -#306 := (+ #56 #305)
4.1104 -#307 := (<= #306 0::real)
4.1105 -#308 := (not #307)
4.1106 -#332 := (and #308 #324)
4.1107 -#58 := (= uf_10 uf_3)
4.1108 -#60 := (ite #58 #26 #59)
4.1109 -#52 := (< #39 #22)
4.1110 -#61 := (ite #52 #43 #60)
4.1111 -#62 := (< #56 #61)
4.1112 -#55 := (ite #52 #53 #54)
4.1113 -#57 := (< #55 #56)
4.1114 -#63 := (and #57 #62)
4.1115 -#335 := (iff #63 #332)
4.1116 -#281 := (ite #52 #43 #278)
4.1117 -#284 := (< #56 #281)
4.1118 -#287 := (and #57 #284)
4.1119 -#333 := (iff #287 #332)
4.1120 -#330 := (iff #284 #324)
4.1121 -#321 := (< #56 #316)
4.1122 -#328 := (iff #321 #324)
4.1123 -#329 := [rewrite]: #328
4.1124 -#322 := (iff #284 #321)
4.1125 -#319 := (= #281 #316)
4.1126 -#291 := (not #290)
4.1127 -#313 := (ite #291 #43 #278)
4.1128 -#317 := (= #313 #316)
4.1129 -#318 := [rewrite]: #317
4.1130 -#314 := (= #281 #313)
4.1131 -#292 := (iff #52 #291)
4.1132 -#293 := [rewrite]: #292
4.1133 -#315 := [monotonicity #293]: #314
4.1134 -#320 := [trans #315 #318]: #319
4.1135 -#323 := [monotonicity #320]: #322
4.1136 -#331 := [trans #323 #329]: #330
4.1137 -#311 := (iff #57 #308)
4.1138 -#302 := (< #297 #56)
4.1139 -#309 := (iff #302 #308)
4.1140 -#310 := [rewrite]: #309
4.1141 -#303 := (iff #57 #302)
4.1142 -#300 := (= #55 #297)
4.1143 -#294 := (ite #291 #53 #54)
4.1144 -#298 := (= #294 #297)
4.1145 -#299 := [rewrite]: #298
4.1146 -#295 := (= #55 #294)
4.1147 -#296 := [monotonicity #293]: #295
4.1148 -#301 := [trans #296 #299]: #300
4.1149 -#304 := [monotonicity #301]: #303
4.1150 -#312 := [trans #304 #310]: #311
4.1151 -#334 := [monotonicity #312 #331]: #333
4.1152 -#288 := (iff #63 #287)
4.1153 -#285 := (iff #62 #284)
4.1154 -#282 := (= #61 #281)
4.1155 -#279 := (= #60 #278)
4.1156 -#225 := (iff #58 #41)
4.1157 -#277 := [rewrite]: #225
4.1158 -#280 := [monotonicity #277]: #279
4.1159 -#283 := [monotonicity #280]: #282
4.1160 -#286 := [monotonicity #283]: #285
4.1161 -#289 := [monotonicity #286]: #288
4.1162 -#336 := [trans #289 #334]: #335
4.1163 -#179 := [asserted]: #63
4.1164 -#337 := [mp #179 #336]: #332
4.1165 -#339 := [and-elim #337]: #324
4.1166 -#469 := [mp #339 #468]: #438
4.1167 -#678 := [th-lemma #469 #677 #418 #385 #666]: false
4.1168 -#679 := [lemma #678]: #570
4.1169 -#684 := [unit-resolution #679 #683]: false
4.1170 -#685 := [lemma #684]: #227
4.1171 -#577 := (or #228 #567)
4.1172 -#578 := [def-axiom]: #577
4.1173 -#645 := [unit-resolution #578 #685]: #567
4.1174 -#686 := (not #567)
4.1175 -#687 := (or #686 #643)
4.1176 -#688 := [th-lemma]: #687
4.1177 -#689 := [unit-resolution #688 #645]: #643
4.1178 -#31 := (uf_4 uf_8 #25)
4.1179 -#245 := (+ #31 #244)
4.1180 -#246 := (<= #245 0::real)
4.1181 -#247 := (not #246)
4.1182 -#34 := (uf_4 uf_9 #25)
4.1183 -#48 := (uf_4 uf_11 #25)
4.1184 -#255 := (ite #228 #48 #34)
4.1185 -#264 := (* -1::real #255)
4.1186 -#265 := (+ #31 #264)
4.1187 -#263 := (>= #265 0::real)
4.1188 -#266 := (not #263)
4.1189 -#271 := (and #247 #266)
4.1190 -#40 := (< #22 #39)
4.1191 -#49 := (ite #40 #34 #48)
4.1192 -#50 := (< #31 #49)
4.1193 -#45 := (ite #40 #26 #44)
4.1194 -#46 := (< #45 #31)
4.1195 -#51 := (and #46 #50)
4.1196 -#272 := (iff #51 #271)
4.1197 -#269 := (iff #50 #266)
4.1198 -#260 := (< #31 #255)
4.1199 -#267 := (iff #260 #266)
4.1200 -#268 := [rewrite]: #267
4.1201 -#261 := (iff #50 #260)
4.1202 -#258 := (= #49 #255)
4.1203 -#252 := (ite #227 #34 #48)
4.1204 -#256 := (= #252 #255)
4.1205 -#257 := [rewrite]: #256
4.1206 -#253 := (= #49 #252)
4.1207 -#231 := (iff #40 #227)
4.1208 -#232 := [rewrite]: #231
4.1209 -#254 := [monotonicity #232]: #253
4.1210 -#259 := [trans #254 #257]: #258
4.1211 -#262 := [monotonicity #259]: #261
4.1212 -#270 := [trans #262 #268]: #269
4.1213 -#250 := (iff #46 #247)
4.1214 -#241 := (< #236 #31)
4.1215 -#248 := (iff #241 #247)
4.1216 -#249 := [rewrite]: #248
4.1217 -#242 := (iff #46 #241)
4.1218 -#239 := (= #45 #236)
4.1219 -#233 := (ite #227 #26 #44)
4.1220 -#237 := (= #233 #236)
4.1221 -#238 := [rewrite]: #237
4.1222 -#234 := (= #45 #233)
4.1223 -#235 := [monotonicity #232]: #234
4.1224 -#240 := [trans #235 #238]: #239
4.1225 -#243 := [monotonicity #240]: #242
4.1226 -#251 := [trans #243 #249]: #250
4.1227 -#273 := [monotonicity #251 #270]: #272
4.1228 -#178 := [asserted]: #51
4.1229 -#274 := [mp #178 #273]: #271
4.1230 -#275 := [and-elim #274]: #247
4.1231 -#196 := (* -1::real #31)
4.1232 -#212 := (+ #26 #196)
4.1233 -#213 := (<= #212 0::real)
4.1234 -#214 := (not #213)
4.1235 -#197 := (+ #28 #196)
4.1236 -#195 := (>= #197 0::real)
4.1237 -#193 := (not #195)
4.1238 -#219 := (and #193 #214)
4.1239 -#23 := (< #22 #22)
4.1240 -#35 := (ite #23 #34 #26)
4.1241 -#36 := (< #31 #35)
4.1242 -#29 := (ite #23 #26 #28)
4.1243 -#32 := (< #29 #31)
4.1244 -#37 := (and #32 #36)
4.1245 -#220 := (iff #37 #219)
4.1246 -#217 := (iff #36 #214)
4.1247 -#209 := (< #31 #26)
4.1248 -#215 := (iff #209 #214)
4.1249 -#216 := [rewrite]: #215
4.1250 -#210 := (iff #36 #209)
4.1251 -#207 := (= #35 #26)
4.1252 -#202 := (ite false #34 #26)
4.1253 -#205 := (= #202 #26)
4.1254 -#206 := [rewrite]: #205
4.1255 -#203 := (= #35 #202)
4.1256 -#180 := (iff #23 false)
4.1257 -#181 := [rewrite]: #180
4.1258 -#204 := [monotonicity #181]: #203
4.1259 -#208 := [trans #204 #206]: #207
4.1260 -#211 := [monotonicity #208]: #210
4.1261 -#218 := [trans #211 #216]: #217
4.1262 -#200 := (iff #32 #193)
4.1263 -#189 := (< #28 #31)
4.1264 -#198 := (iff #189 #193)
4.1265 -#199 := [rewrite]: #198
4.1266 -#190 := (iff #32 #189)
4.1267 -#187 := (= #29 #28)
4.1268 -#182 := (ite false #26 #28)
4.1269 -#185 := (= #182 #28)
4.1270 -#186 := [rewrite]: #185
4.1271 -#183 := (= #29 #182)
4.1272 -#184 := [monotonicity #181]: #183
4.1273 -#188 := [trans #184 #186]: #187
4.1274 -#191 := [monotonicity #188]: #190
4.1275 -#201 := [trans #191 #199]: #200
4.1276 -#221 := [monotonicity #201 #218]: #220
4.1277 -#177 := [asserted]: #37
4.1278 -#222 := [mp #177 #221]: #219
4.1279 -#224 := [and-elim #222]: #214
4.1280 -[th-lemma #224 #275 #689]: false
4.1281 -unsat
4.1282 -NX/HT1QOfbspC2LtZNKpBA 428 0
4.1283 -#2 := false
4.1284 -decl uf_10 :: T1
4.1285 -#38 := uf_10
4.1286 -decl uf_3 :: T1
4.1287 -#21 := uf_3
4.1288 -#45 := (= uf_3 uf_10)
4.1289 -decl uf_1 :: (-> int T1)
4.1290 -decl uf_2 :: (-> T1 int)
4.1291 -#39 := (uf_2 uf_10)
4.1292 -#588 := (uf_1 #39)
4.1293 -#686 := (= #588 uf_10)
4.1294 -#589 := (= uf_10 #588)
4.1295 -#4 := (:var 0 T1)
4.1296 -#5 := (uf_2 #4)
4.1297 -#541 := (pattern #5)
4.1298 -#6 := (uf_1 #5)
4.1299 -#93 := (= #4 #6)
4.1300 -#542 := (forall (vars (?x1 T1)) (:pat #541) #93)
4.1301 -#96 := (forall (vars (?x1 T1)) #93)
4.1302 -#545 := (iff #96 #542)
4.1303 -#543 := (iff #93 #93)
4.1304 -#544 := [refl]: #543
4.1305 -#546 := [quant-intro #544]: #545
4.1306 -#454 := (~ #96 #96)
4.1307 -#456 := (~ #93 #93)
4.1308 -#457 := [refl]: #456
4.1309 -#455 := [nnf-pos #457]: #454
4.1310 -#7 := (= #6 #4)
4.1311 -#8 := (forall (vars (?x1 T1)) #7)
4.1312 -#97 := (iff #8 #96)
4.1313 -#94 := (iff #7 #93)
4.1314 -#95 := [rewrite]: #94
4.1315 -#98 := [quant-intro #95]: #97
4.1316 -#92 := [asserted]: #8
4.1317 -#101 := [mp #92 #98]: #96
4.1318 -#452 := [mp~ #101 #455]: #96
4.1319 -#547 := [mp #452 #546]: #542
4.1320 -#590 := (not #542)
4.1321 -#595 := (or #590 #589)
4.1322 -#596 := [quant-inst]: #595
4.1323 -#680 := [unit-resolution #596 #547]: #589
4.1324 -#687 := [symm #680]: #686
4.1325 -#688 := (= uf_3 #588)
4.1326 -#22 := (uf_2 uf_3)
4.1327 -#586 := (uf_1 #22)
4.1328 -#684 := (= #586 #588)
4.1329 -#682 := (= #588 #586)
4.1330 -#678 := (= #39 #22)
4.1331 -#676 := (= #22 #39)
4.1332 -#9 := 0::int
4.1333 -#227 := -1::int
4.1334 -#230 := (* -1::int #39)
4.1335 -#231 := (+ #22 #230)
4.1336 -#296 := (<= #231 0::int)
4.1337 -#70 := (<= #22 #39)
4.1338 -#393 := (iff #70 #296)
4.1339 -#394 := [rewrite]: #393
4.1340 -#347 := [asserted]: #70
4.1341 -#395 := [mp #347 #394]: #296
4.1342 -#229 := (>= #231 0::int)
4.1343 -decl uf_4 :: (-> T2 T3 real)
4.1344 -decl uf_6 :: (-> T1 T3)
4.1345 -#25 := (uf_6 uf_3)
4.1346 -decl uf_7 :: T2
4.1347 -#27 := uf_7
4.1348 -#28 := (uf_4 uf_7 #25)
4.1349 -decl uf_9 :: T2
4.1350 -#33 := uf_9
4.1351 -#34 := (uf_4 uf_9 #25)
4.1352 -#46 := (uf_6 uf_10)
4.1353 -decl uf_5 :: T2
4.1354 -#24 := uf_5
4.1355 -#47 := (uf_4 uf_5 #46)
4.1356 -#48 := (ite #45 #47 #34)
4.1357 -#256 := (ite #229 #48 #28)
4.1358 -#568 := (= #28 #256)
4.1359 -#648 := (not #568)
4.1360 -#194 := 0::real
4.1361 -#192 := -1::real
4.1362 -#265 := (* -1::real #256)
4.1363 -#640 := (+ #28 #265)
4.1364 -#642 := (>= #640 0::real)
4.1365 -#645 := (not #642)
4.1366 -#643 := [hypothesis]: #642
4.1367 -decl uf_8 :: T2
4.1368 -#30 := uf_8
4.1369 -#31 := (uf_4 uf_8 #25)
4.1370 -#266 := (+ #31 #265)
4.1371 -#264 := (>= #266 0::real)
4.1372 -#267 := (not #264)
4.1373 -#26 := (uf_4 uf_5 #25)
4.1374 -decl uf_11 :: T2
4.1375 -#41 := uf_11
4.1376 -#42 := (uf_4 uf_11 #25)
4.1377 -#237 := (ite #229 #42 #26)
4.1378 -#245 := (* -1::real #237)
4.1379 -#246 := (+ #31 #245)
4.1380 -#247 := (<= #246 0::real)
4.1381 -#248 := (not #247)
4.1382 -#272 := (and #248 #267)
4.1383 -#40 := (< #22 #39)
4.1384 -#49 := (ite #40 #28 #48)
4.1385 -#50 := (< #31 #49)
4.1386 -#43 := (ite #40 #26 #42)
4.1387 -#44 := (< #43 #31)
4.1388 -#51 := (and #44 #50)
4.1389 -#273 := (iff #51 #272)
4.1390 -#270 := (iff #50 #267)
4.1391 -#261 := (< #31 #256)
4.1392 -#268 := (iff #261 #267)
4.1393 -#269 := [rewrite]: #268
4.1394 -#262 := (iff #50 #261)
4.1395 -#259 := (= #49 #256)
4.1396 -#228 := (not #229)
4.1397 -#253 := (ite #228 #28 #48)
4.1398 -#257 := (= #253 #256)
4.1399 -#258 := [rewrite]: #257
4.1400 -#254 := (= #49 #253)
4.1401 -#232 := (iff #40 #228)
4.1402 -#233 := [rewrite]: #232
4.1403 -#255 := [monotonicity #233]: #254
4.1404 -#260 := [trans #255 #258]: #259
4.1405 -#263 := [monotonicity #260]: #262
4.1406 -#271 := [trans #263 #269]: #270
4.1407 -#251 := (iff #44 #248)
4.1408 -#242 := (< #237 #31)
4.1409 -#249 := (iff #242 #248)
4.1410 -#250 := [rewrite]: #249
4.1411 -#243 := (iff #44 #242)
4.1412 -#240 := (= #43 #237)
4.1413 -#234 := (ite #228 #26 #42)
4.1414 -#238 := (= #234 #237)
4.1415 -#239 := [rewrite]: #238
4.1416 -#235 := (= #43 #234)
4.1417 -#236 := [monotonicity #233]: #235
4.1418 -#241 := [trans #236 #239]: #240
4.1419 -#244 := [monotonicity #241]: #243
4.1420 -#252 := [trans #244 #250]: #251
4.1421 -#274 := [monotonicity #252 #271]: #273
4.1422 -#178 := [asserted]: #51
4.1423 -#275 := [mp #178 #274]: #272
4.1424 -#277 := [and-elim #275]: #267
4.1425 -#196 := (* -1::real #31)
4.1426 -#197 := (+ #28 #196)
4.1427 -#195 := (>= #197 0::real)
4.1428 -#193 := (not #195)
4.1429 -#213 := (* -1::real #34)
4.1430 -#214 := (+ #31 #213)
4.1431 -#212 := (>= #214 0::real)
4.1432 -#215 := (not #212)
4.1433 -#220 := (and #193 #215)
4.1434 -#23 := (< #22 #22)
4.1435 -#35 := (ite #23 #28 #34)
4.1436 -#36 := (< #31 #35)
4.1437 -#29 := (ite #23 #26 #28)
4.1438 -#32 := (< #29 #31)
4.1439 -#37 := (and #32 #36)
4.1440 -#221 := (iff #37 #220)
4.1441 -#218 := (iff #36 #215)
4.1442 -#209 := (< #31 #34)
4.1443 -#216 := (iff #209 #215)
4.1444 -#217 := [rewrite]: #216
4.1445 -#210 := (iff #36 #209)
4.1446 -#207 := (= #35 #34)
4.1447 -#202 := (ite false #28 #34)
4.1448 -#205 := (= #202 #34)
4.1449 -#206 := [rewrite]: #205
4.1450 -#203 := (= #35 #202)
4.1451 -#180 := (iff #23 false)
4.1452 -#181 := [rewrite]: #180
4.1453 -#204 := [monotonicity #181]: #203
4.1454 -#208 := [trans #204 #206]: #207
4.1455 -#211 := [monotonicity #208]: #210
4.1456 -#219 := [trans #211 #217]: #218
4.1457 -#200 := (iff #32 #193)
4.1458 -#189 := (< #28 #31)
4.1459 -#198 := (iff #189 #193)
4.1460 -#199 := [rewrite]: #198
4.1461 -#190 := (iff #32 #189)
4.1462 -#187 := (= #29 #28)
4.1463 -#182 := (ite false #26 #28)
4.1464 -#185 := (= #182 #28)
4.1465 -#186 := [rewrite]: #185
4.1466 -#183 := (= #29 #182)
4.1467 -#184 := [monotonicity #181]: #183
4.1468 -#188 := [trans #184 #186]: #187
4.1469 -#191 := [monotonicity #188]: #190
4.1470 -#201 := [trans #191 #199]: #200
4.1471 -#222 := [monotonicity #201 #219]: #221
4.1472 -#177 := [asserted]: #37
4.1473 -#223 := [mp #177 #222]: #220
4.1474 -#224 := [and-elim #223]: #193
4.1475 -#644 := [th-lemma #224 #277 #643]: false
4.1476 -#646 := [lemma #644]: #645
4.1477 -#647 := [hypothesis]: #568
4.1478 -#649 := (or #648 #642)
4.1479 -#650 := [th-lemma]: #649
4.1480 -#651 := [unit-resolution #650 #647 #646]: false
4.1481 -#652 := [lemma #651]: #648
4.1482 -#578 := (or #229 #568)
4.1483 -#579 := [def-axiom]: #578
4.1484 -#675 := [unit-resolution #579 #652]: #229
4.1485 -#677 := [th-lemma #675 #395]: #676
4.1486 -#679 := [symm #677]: #678
4.1487 -#683 := [monotonicity #679]: #682
4.1488 -#685 := [symm #683]: #684
4.1489 -#587 := (= uf_3 #586)
4.1490 -#591 := (or #590 #587)
4.1491 -#592 := [quant-inst]: #591
4.1492 -#681 := [unit-resolution #592 #547]: #587
4.1493 -#689 := [trans #681 #685]: #688
4.1494 -#690 := [trans #689 #687]: #45
4.1495 -#571 := (not #45)
4.1496 -#54 := (uf_4 uf_11 #46)
4.1497 -#279 := (ite #45 #28 #54)
4.1498 -#465 := (* -1::real #279)
4.1499 -#632 := (+ #28 #465)
4.1500 -#633 := (<= #632 0::real)
4.1501 -#580 := (= #28 #279)
4.1502 -#656 := [hypothesis]: #45
4.1503 -#582 := (or #571 #580)
4.1504 -#583 := [def-axiom]: #582
4.1505 -#657 := [unit-resolution #583 #656]: #580
4.1506 -#658 := (not #580)
4.1507 -#659 := (or #658 #633)
4.1508 -#660 := [th-lemma]: #659
4.1509 -#661 := [unit-resolution #660 #657]: #633
4.1510 -#57 := (uf_4 uf_8 #46)
4.1511 -#363 := (* -1::real #57)
4.1512 -#379 := (+ #47 #363)
4.1513 -#380 := (<= #379 0::real)
4.1514 -#381 := (not #380)
4.1515 -#364 := (+ #54 #363)
4.1516 -#362 := (>= #364 0::real)
4.1517 -#361 := (not #362)
4.1518 -#386 := (and #361 #381)
4.1519 -#59 := (uf_4 uf_7 #46)
4.1520 -#64 := (< #39 #39)
4.1521 -#67 := (ite #64 #59 #47)
4.1522 -#68 := (< #57 #67)
4.1523 -#65 := (ite #64 #47 #54)
4.1524 -#66 := (< #65 #57)
4.1525 -#69 := (and #66 #68)
4.1526 -#387 := (iff #69 #386)
4.1527 -#384 := (iff #68 #381)
4.1528 -#376 := (< #57 #47)
4.1529 -#382 := (iff #376 #381)
4.1530 -#383 := [rewrite]: #382
4.1531 -#377 := (iff #68 #376)
4.1532 -#374 := (= #67 #47)
4.1533 -#369 := (ite false #59 #47)
4.1534 -#372 := (= #369 #47)
4.1535 -#373 := [rewrite]: #372
4.1536 -#370 := (= #67 #369)
4.1537 -#349 := (iff #64 false)
4.1538 -#350 := [rewrite]: #349
4.1539 -#371 := [monotonicity #350]: #370
4.1540 -#375 := [trans #371 #373]: #374
4.1541 -#378 := [monotonicity #375]: #377
4.1542 -#385 := [trans #378 #383]: #384
4.1543 -#367 := (iff #66 #361)
4.1544 -#358 := (< #54 #57)
4.1545 -#365 := (iff #358 #361)
4.1546 -#366 := [rewrite]: #365
4.1547 -#359 := (iff #66 #358)
4.1548 -#356 := (= #65 #54)
4.1549 -#351 := (ite false #47 #54)
4.1550 -#354 := (= #351 #54)
4.1551 -#355 := [rewrite]: #354
4.1552 -#352 := (= #65 #351)
4.1553 -#353 := [monotonicity #350]: #352
4.1554 -#357 := [trans #353 #355]: #356
4.1555 -#360 := [monotonicity #357]: #359
4.1556 -#368 := [trans #360 #366]: #367
4.1557 -#388 := [monotonicity #368 #385]: #387
4.1558 -#346 := [asserted]: #69
4.1559 -#389 := [mp #346 #388]: #386
4.1560 -#391 := [and-elim #389]: #381
4.1561 -#397 := (* -1::real #59)
4.1562 -#398 := (+ #47 #397)
4.1563 -#399 := (<= #398 0::real)
4.1564 -#409 := (* -1::real #54)
4.1565 -#410 := (+ #47 #409)
4.1566 -#408 := (>= #410 0::real)
4.1567 -#60 := (uf_4 uf_9 #46)
4.1568 -#402 := (* -1::real #60)
4.1569 -#403 := (+ #59 #402)
4.1570 -#404 := (<= #403 0::real)
4.1571 -#418 := (and #399 #404 #408)
4.1572 -#73 := (<= #59 #60)
4.1573 -#72 := (<= #47 #59)
4.1574 -#74 := (and #72 #73)
4.1575 -#71 := (<= #54 #47)
4.1576 -#75 := (and #71 #74)
4.1577 -#421 := (iff #75 #418)
4.1578 -#412 := (and #399 #404)
4.1579 -#415 := (and #408 #412)
4.1580 -#419 := (iff #415 #418)
4.1581 -#420 := [rewrite]: #419
4.1582 -#416 := (iff #75 #415)
4.1583 -#413 := (iff #74 #412)
4.1584 -#405 := (iff #73 #404)
4.1585 -#406 := [rewrite]: #405
4.1586 -#400 := (iff #72 #399)
4.1587 -#401 := [rewrite]: #400
4.1588 -#414 := [monotonicity #401 #406]: #413
4.1589 -#407 := (iff #71 #408)
4.1590 -#411 := [rewrite]: #407
4.1591 -#417 := [monotonicity #411 #414]: #416
4.1592 -#422 := [trans #417 #420]: #421
4.1593 -#348 := [asserted]: #75
4.1594 -#423 := [mp #348 #422]: #418
4.1595 -#424 := [and-elim #423]: #399
4.1596 -#637 := (+ #28 #397)
4.1597 -#639 := (>= #637 0::real)
4.1598 -#636 := (= #28 #59)
4.1599 -#666 := (= #59 #28)
4.1600 -#664 := (= #46 #25)
4.1601 -#662 := (= #25 #46)
4.1602 -#663 := [monotonicity #656]: #662
4.1603 -#665 := [symm #663]: #664
4.1604 -#667 := [monotonicity #665]: #666
4.1605 -#668 := [symm #667]: #636
4.1606 -#669 := (not #636)
4.1607 -#670 := (or #669 #639)
4.1608 -#671 := [th-lemma]: #670
4.1609 -#672 := [unit-resolution #671 #668]: #639
4.1610 -#468 := (+ #57 #465)
4.1611 -#471 := (<= #468 0::real)
4.1612 -#444 := (not #471)
4.1613 -#322 := (ite #296 #279 #47)
4.1614 -#330 := (* -1::real #322)
4.1615 -#331 := (+ #57 #330)
4.1616 -#332 := (<= #331 0::real)
4.1617 -#333 := (not #332)
4.1618 -#445 := (iff #333 #444)
4.1619 -#472 := (iff #332 #471)
4.1620 -#469 := (= #331 #468)
4.1621 -#466 := (= #330 #465)
4.1622 -#463 := (= #322 #279)
4.1623 -#1 := true
4.1624 -#458 := (ite true #279 #47)
4.1625 -#461 := (= #458 #279)
4.1626 -#462 := [rewrite]: #461
4.1627 -#459 := (= #322 #458)
4.1628 -#450 := (iff #296 true)
4.1629 -#451 := [iff-true #395]: #450
4.1630 -#460 := [monotonicity #451]: #459
4.1631 -#464 := [trans #460 #462]: #463
4.1632 -#467 := [monotonicity #464]: #466
4.1633 -#470 := [monotonicity #467]: #469
4.1634 -#473 := [monotonicity #470]: #472
4.1635 -#474 := [monotonicity #473]: #445
4.1636 -#303 := (ite #296 #60 #59)
4.1637 -#313 := (* -1::real #303)
4.1638 -#314 := (+ #57 #313)
4.1639 -#312 := (>= #314 0::real)
4.1640 -#311 := (not #312)
4.1641 -#338 := (and #311 #333)
4.1642 -#52 := (< #39 #22)
4.1643 -#61 := (ite #52 #59 #60)
4.1644 -#62 := (< #57 #61)
4.1645 -#53 := (= uf_10 uf_3)
4.1646 -#55 := (ite #53 #28 #54)
4.1647 -#56 := (ite #52 #47 #55)
4.1648 -#58 := (< #56 #57)
4.1649 -#63 := (and #58 #62)
4.1650 -#341 := (iff #63 #338)
4.1651 -#282 := (ite #52 #47 #279)
4.1652 -#285 := (< #282 #57)
4.1653 -#291 := (and #62 #285)
4.1654 -#339 := (iff #291 #338)
4.1655 -#336 := (iff #285 #333)
4.1656 -#327 := (< #322 #57)
4.1657 -#334 := (iff #327 #333)
4.1658 -#335 := [rewrite]: #334
4.1659 -#328 := (iff #285 #327)
4.1660 -#325 := (= #282 #322)
4.1661 -#297 := (not #296)
4.1662 -#319 := (ite #297 #47 #279)
4.1663 -#323 := (= #319 #322)
4.1664 -#324 := [rewrite]: #323
4.1665 -#320 := (= #282 #319)
4.1666 -#298 := (iff #52 #297)
4.1667 -#299 := [rewrite]: #298
4.1668 -#321 := [monotonicity #299]: #320
4.1669 -#326 := [trans #321 #324]: #325
4.1670 -#329 := [monotonicity #326]: #328
4.1671 -#337 := [trans #329 #335]: #336
4.1672 -#317 := (iff #62 #311)
4.1673 -#308 := (< #57 #303)
4.1674 -#315 := (iff #308 #311)
4.1675 -#316 := [rewrite]: #315
4.1676 -#309 := (iff #62 #308)
4.1677 -#306 := (= #61 #303)
4.1678 -#300 := (ite #297 #59 #60)
4.1679 -#304 := (= #300 #303)
4.1680 -#305 := [rewrite]: #304
4.1681 -#301 := (= #61 #300)
4.1682 -#302 := [monotonicity #299]: #301
4.1683 -#307 := [trans #302 #305]: #306
4.1684 -#310 := [monotonicity #307]: #309
4.1685 -#318 := [trans #310 #316]: #317
4.1686 -#340 := [monotonicity #318 #337]: #339
4.1687 -#294 := (iff #63 #291)
4.1688 -#288 := (and #285 #62)
4.1689 -#292 := (iff #288 #291)
4.1690 -#293 := [rewrite]: #292
4.1691 -#289 := (iff #63 #288)
4.1692 -#286 := (iff #58 #285)
4.1693 -#283 := (= #56 #282)
4.1694 -#280 := (= #55 #279)
4.1695 -#226 := (iff #53 #45)
4.1696 -#278 := [rewrite]: #226
4.1697 -#281 := [monotonicity #278]: #280
4.1698 -#284 := [monotonicity #281]: #283
4.1699 -#287 := [monotonicity #284]: #286
4.1700 -#290 := [monotonicity #287]: #289
4.1701 -#295 := [trans #290 #293]: #294
4.1702 -#342 := [trans #295 #340]: #341
4.1703 -#179 := [asserted]: #63
4.1704 -#343 := [mp #179 #342]: #338
4.1705 -#345 := [and-elim #343]: #333
4.1706 -#475 := [mp #345 #474]: #444
4.1707 -#673 := [th-lemma #475 #672 #424 #391 #661]: false
4.1708 -#674 := [lemma #673]: #571
4.1709 -[unit-resolution #674 #690]: false
4.1710 -unsat
4.1711 -IL2powemHjRpCJYwmXFxyw 211 0
4.1712 +f5cf3017773c1cf700f533cb220ba6c9eb22de56 211 0
4.1713 #2 := false
4.1714 #33 := 0::real
4.1715 decl uf_11 :: (-> T5 T6 real)
4.1716 @@ -1967,7 +1967,7 @@
4.1717 #328 := [unit-resolution #319 #327]: #300
4.1718 [th-lemma #326 #334 #195 #328 #187 #138]: false
4.1719 unsat
4.1720 -GX51o3DUO/UBS3eNP2P9kA 285 0
4.1721 +ad41c2d9b185dd9b4fd0abefcdc55357d2105ed8 285 0
4.1722 #2 := false
4.1723 #7 := 0::real
4.1724 decl uf_4 :: real
4.1725 @@ -2253,7 +2253,7 @@
4.1726 #286 := [lemma #284]: #285
4.1727 [unit-resolution #286 #308 #305]: false
4.1728 unsat
4.1729 -cebG074uorSr8ODzgTmcKg 97 0
4.1730 +076d8565ad4c4370b16a3b0c139e8c8e8fb58224 97 0
4.1731 #2 := false
4.1732 #18 := 0::real
4.1733 decl uf_1 :: (-> T2 T1 real)
4.1734 @@ -2351,7 +2351,7 @@
4.1735 #173 := [mp #167 #172]: #165
4.1736 [unit-resolution #173 #147 #76]: false
4.1737 unsat
4.1738 -DKRtrJ2XceCkITuNwNViRw 57 0
4.1739 +8e6ea05b53a9ffb5a6dec689eb004bdb0c2a755b 57 0
4.1740 #2 := false
4.1741 #4 := 0::real
4.1742 decl uf_1 :: (-> T2 real)
4.1743 @@ -2409,7 +2409,7 @@
4.1744 #269 := [quant-inst]: #268
4.1745 [unit-resolution #269 #247 #274]: false
4.1746 unsat
4.1747 -97KJAJfUio+nGchEHWvgAw 91 0
4.1748 +d278c38176edc1fb6492d54817f0a9092db653e6 91 0
4.1749 #2 := false
4.1750 #38 := 0::real
4.1751 decl uf_1 :: (-> T1 T2 real)
4.1752 @@ -2501,157 +2501,7 @@
4.1753 #153 := [mp #147 #152]: #145
4.1754 [unit-resolution #153 #129 #160]: false
4.1755 unsat
4.1756 -flJYbeWfe+t2l/zsRqdujA 149 0
4.1757 -#2 := false
4.1758 -#19 := 0::real
4.1759 -decl uf_1 :: (-> T1 T2 real)
4.1760 -decl uf_3 :: T2
4.1761 -#5 := uf_3
4.1762 -decl uf_4 :: T1
4.1763 -#7 := uf_4
4.1764 -#8 := (uf_1 uf_4 uf_3)
4.1765 -#44 := -1::real
4.1766 -#156 := (* -1::real #8)
4.1767 -decl uf_2 :: T1
4.1768 -#4 := uf_2
4.1769 -#6 := (uf_1 uf_2 uf_3)
4.1770 -#203 := (+ #6 #156)
4.1771 -#205 := (>= #203 0::real)
4.1772 -#9 := (= #6 #8)
4.1773 -#40 := [asserted]: #9
4.1774 -#208 := (not #9)
4.1775 -#209 := (or #208 #205)
4.1776 -#210 := [th-lemma]: #209
4.1777 -#211 := [unit-resolution #210 #40]: #205
4.1778 -decl uf_5 :: T1
4.1779 -#12 := uf_5
4.1780 -#22 := (uf_1 uf_5 uf_3)
4.1781 -#160 := (* -1::real #22)
4.1782 -#161 := (+ #6 #160)
4.1783 -#207 := (>= #161 0::real)
4.1784 -#222 := (not #207)
4.1785 -#206 := (= #6 #22)
4.1786 -#216 := (not #206)
4.1787 -#62 := (= #8 #22)
4.1788 -#70 := (not #62)
4.1789 -#217 := (iff #70 #216)
4.1790 -#214 := (iff #62 #206)
4.1791 -#212 := (iff #206 #62)
4.1792 -#213 := [monotonicity #40]: #212
4.1793 -#215 := [symm #213]: #214
4.1794 -#218 := [monotonicity #215]: #217
4.1795 -#23 := (= #22 #8)
4.1796 -#24 := (not #23)
4.1797 -#71 := (iff #24 #70)
4.1798 -#68 := (iff #23 #62)
4.1799 -#69 := [rewrite]: #68
4.1800 -#72 := [monotonicity #69]: #71
4.1801 -#43 := [asserted]: #24
4.1802 -#75 := [mp #43 #72]: #70
4.1803 -#219 := [mp #75 #218]: #216
4.1804 -#225 := (or #206 #222)
4.1805 -#162 := (<= #161 0::real)
4.1806 -#172 := (+ #8 #160)
4.1807 -#173 := (>= #172 0::real)
4.1808 -#178 := (not #173)
4.1809 -#163 := (not #162)
4.1810 -#181 := (or #163 #178)
4.1811 -#184 := (not #181)
4.1812 -#10 := (:var 0 T2)
4.1813 -#15 := (uf_1 uf_4 #10)
4.1814 -#149 := (pattern #15)
4.1815 -#13 := (uf_1 uf_5 #10)
4.1816 -#148 := (pattern #13)
4.1817 -#11 := (uf_1 uf_2 #10)
4.1818 -#147 := (pattern #11)
4.1819 -#50 := (* -1::real #15)
4.1820 -#51 := (+ #13 #50)
4.1821 -#52 := (<= #51 0::real)
4.1822 -#76 := (not #52)
4.1823 -#45 := (* -1::real #13)
4.1824 -#46 := (+ #11 #45)
4.1825 -#47 := (<= #46 0::real)
4.1826 -#78 := (not #47)
4.1827 -#73 := (or #78 #76)
4.1828 -#83 := (not #73)
4.1829 -#150 := (forall (vars (?x1 T2)) (:pat #147 #148 #149) #83)
4.1830 -#86 := (forall (vars (?x1 T2)) #83)
4.1831 -#153 := (iff #86 #150)
4.1832 -#151 := (iff #83 #83)
4.1833 -#152 := [refl]: #151
4.1834 -#154 := [quant-intro #152]: #153
4.1835 -#55 := (and #47 #52)
4.1836 -#58 := (forall (vars (?x1 T2)) #55)
4.1837 -#87 := (iff #58 #86)
4.1838 -#84 := (iff #55 #83)
4.1839 -#85 := [rewrite]: #84
4.1840 -#88 := [quant-intro #85]: #87
4.1841 -#79 := (~ #58 #58)
4.1842 -#81 := (~ #55 #55)
4.1843 -#82 := [refl]: #81
4.1844 -#80 := [nnf-pos #82]: #79
4.1845 -#16 := (<= #13 #15)
4.1846 -#14 := (<= #11 #13)
4.1847 -#17 := (and #14 #16)
4.1848 -#18 := (forall (vars (?x1 T2)) #17)
4.1849 -#59 := (iff #18 #58)
4.1850 -#56 := (iff #17 #55)
4.1851 -#53 := (iff #16 #52)
4.1852 -#54 := [rewrite]: #53
4.1853 -#48 := (iff #14 #47)
4.1854 -#49 := [rewrite]: #48
4.1855 -#57 := [monotonicity #49 #54]: #56
4.1856 -#60 := [quant-intro #57]: #59
4.1857 -#41 := [asserted]: #18
4.1858 -#61 := [mp #41 #60]: #58
4.1859 -#77 := [mp~ #61 #80]: #58
4.1860 -#89 := [mp #77 #88]: #86
4.1861 -#155 := [mp #89 #154]: #150
4.1862 -#187 := (not #150)
4.1863 -#188 := (or #187 #184)
4.1864 -#157 := (+ #22 #156)
4.1865 -#158 := (<= #157 0::real)
4.1866 -#159 := (not #158)
4.1867 -#164 := (or #163 #159)
4.1868 -#165 := (not #164)
4.1869 -#189 := (or #187 #165)
4.1870 -#191 := (iff #189 #188)
4.1871 -#193 := (iff #188 #188)
4.1872 -#194 := [rewrite]: #193
4.1873 -#185 := (iff #165 #184)
4.1874 -#182 := (iff #164 #181)
4.1875 -#179 := (iff #159 #178)
4.1876 -#176 := (iff #158 #173)
4.1877 -#166 := (+ #156 #22)
4.1878 -#169 := (<= #166 0::real)
4.1879 -#174 := (iff #169 #173)
4.1880 -#175 := [rewrite]: #174
4.1881 -#170 := (iff #158 #169)
4.1882 -#167 := (= #157 #166)
4.1883 -#168 := [rewrite]: #167
4.1884 -#171 := [monotonicity #168]: #170
4.1885 -#177 := [trans #171 #175]: #176
4.1886 -#180 := [monotonicity #177]: #179
4.1887 -#183 := [monotonicity #180]: #182
4.1888 -#186 := [monotonicity #183]: #185
4.1889 -#192 := [monotonicity #186]: #191
4.1890 -#195 := [trans #192 #194]: #191
4.1891 -#190 := [quant-inst]: #189
4.1892 -#196 := [mp #190 #195]: #188
4.1893 -#220 := [unit-resolution #196 #155]: #184
4.1894 -#197 := (or #181 #162)
4.1895 -#198 := [def-axiom]: #197
4.1896 -#221 := [unit-resolution #198 #220]: #162
4.1897 -#223 := (or #206 #163 #222)
4.1898 -#224 := [th-lemma]: #223
4.1899 -#226 := [unit-resolution #224 #221]: #225
4.1900 -#227 := [unit-resolution #226 #219]: #222
4.1901 -#199 := (or #181 #173)
4.1902 -#200 := [def-axiom]: #199
4.1903 -#228 := [unit-resolution #200 #220]: #173
4.1904 -[th-lemma #228 #227 #211]: false
4.1905 -unsat
4.1906 -rbrrQuQfaijtLkQizgEXnQ 222 0
4.1907 +38b5e95092f91070fab780891ebf7b83d5f95757 222 0
4.1908 #2 := false
4.1909 #4 := 0::real
4.1910 decl uf_2 :: (-> T2 T1 real)
4.1911 @@ -2874,7 +2724,7 @@
4.1912 #308 := [th-lemma]: #307
4.1913 [unit-resolution #308 #305 #290]: false
4.1914 unsat
4.1915 -hwh3oeLAWt56hnKIa8Wuow 248 0
4.1916 +4968b0a0840255d92fbecd59ed4dac302603b2bd 248 0
4.1917 #2 := false
4.1918 #4 := 0::real
4.1919 decl uf_2 :: (-> T2 T1 real)
4.1920 @@ -3123,7 +2973,157 @@
4.1921 #380 := [th-lemma]: #379
4.1922 [unit-resolution #380 #377 #363]: false
4.1923 unsat
4.1924 -WdMJH3tkMv/rps8y9Ukq5Q 86 0
4.1925 +a3b02dd75d8b2261f1b7ef7215268d84fd25e972 149 0
4.1926 +#2 := false
4.1927 +#19 := 0::real
4.1928 +decl uf_1 :: (-> T1 T2 real)
4.1929 +decl uf_3 :: T2
4.1930 +#5 := uf_3
4.1931 +decl uf_4 :: T1
4.1932 +#7 := uf_4
4.1933 +#8 := (uf_1 uf_4 uf_3)
4.1934 +#44 := -1::real
4.1935 +#156 := (* -1::real #8)
4.1936 +decl uf_2 :: T1
4.1937 +#4 := uf_2
4.1938 +#6 := (uf_1 uf_2 uf_3)
4.1939 +#203 := (+ #6 #156)
4.1940 +#205 := (>= #203 0::real)
4.1941 +#9 := (= #6 #8)
4.1942 +#40 := [asserted]: #9
4.1943 +#208 := (not #9)
4.1944 +#209 := (or #208 #205)
4.1945 +#210 := [th-lemma]: #209
4.1946 +#211 := [unit-resolution #210 #40]: #205
4.1947 +decl uf_5 :: T1
4.1948 +#12 := uf_5
4.1949 +#22 := (uf_1 uf_5 uf_3)
4.1950 +#160 := (* -1::real #22)
4.1951 +#161 := (+ #6 #160)
4.1952 +#207 := (>= #161 0::real)
4.1953 +#222 := (not #207)
4.1954 +#206 := (= #6 #22)
4.1955 +#216 := (not #206)
4.1956 +#62 := (= #8 #22)
4.1957 +#70 := (not #62)
4.1958 +#217 := (iff #70 #216)
4.1959 +#214 := (iff #62 #206)
4.1960 +#212 := (iff #206 #62)
4.1961 +#213 := [monotonicity #40]: #212
4.1962 +#215 := [symm #213]: #214
4.1963 +#218 := [monotonicity #215]: #217
4.1964 +#23 := (= #22 #8)
4.1965 +#24 := (not #23)
4.1966 +#71 := (iff #24 #70)
4.1967 +#68 := (iff #23 #62)
4.1968 +#69 := [rewrite]: #68
4.1969 +#72 := [monotonicity #69]: #71
4.1970 +#43 := [asserted]: #24
4.1971 +#75 := [mp #43 #72]: #70
4.1972 +#219 := [mp #75 #218]: #216
4.1973 +#225 := (or #206 #222)
4.1974 +#162 := (<= #161 0::real)
4.1975 +#172 := (+ #8 #160)
4.1976 +#173 := (>= #172 0::real)
4.1977 +#178 := (not #173)
4.1978 +#163 := (not #162)
4.1979 +#181 := (or #163 #178)
4.1980 +#184 := (not #181)
4.1981 +#10 := (:var 0 T2)
4.1982 +#15 := (uf_1 uf_4 #10)
4.1983 +#149 := (pattern #15)
4.1984 +#13 := (uf_1 uf_5 #10)
4.1985 +#148 := (pattern #13)
4.1986 +#11 := (uf_1 uf_2 #10)
4.1987 +#147 := (pattern #11)
4.1988 +#50 := (* -1::real #15)
4.1989 +#51 := (+ #13 #50)
4.1990 +#52 := (<= #51 0::real)
4.1991 +#76 := (not #52)
4.1992 +#45 := (* -1::real #13)
4.1993 +#46 := (+ #11 #45)
4.1994 +#47 := (<= #46 0::real)
4.1995 +#78 := (not #47)
4.1996 +#73 := (or #78 #76)
4.1997 +#83 := (not #73)
4.1998 +#150 := (forall (vars (?x1 T2)) (:pat #147 #148 #149) #83)
4.1999 +#86 := (forall (vars (?x1 T2)) #83)
4.2000 +#153 := (iff #86 #150)
4.2001 +#151 := (iff #83 #83)
4.2002 +#152 := [refl]: #151
4.2003 +#154 := [quant-intro #152]: #153
4.2004 +#55 := (and #47 #52)
4.2005 +#58 := (forall (vars (?x1 T2)) #55)
4.2006 +#87 := (iff #58 #86)
4.2007 +#84 := (iff #55 #83)
4.2008 +#85 := [rewrite]: #84
4.2009 +#88 := [quant-intro #85]: #87
4.2010 +#79 := (~ #58 #58)
4.2011 +#81 := (~ #55 #55)
4.2012 +#82 := [refl]: #81
4.2013 +#80 := [nnf-pos #82]: #79
4.2014 +#16 := (<= #13 #15)
4.2015 +#14 := (<= #11 #13)
4.2016 +#17 := (and #14 #16)
4.2017 +#18 := (forall (vars (?x1 T2)) #17)
4.2018 +#59 := (iff #18 #58)
4.2019 +#56 := (iff #17 #55)
4.2020 +#53 := (iff #16 #52)
4.2021 +#54 := [rewrite]: #53
4.2022 +#48 := (iff #14 #47)
4.2023 +#49 := [rewrite]: #48
4.2024 +#57 := [monotonicity #49 #54]: #56
4.2025 +#60 := [quant-intro #57]: #59
4.2026 +#41 := [asserted]: #18
4.2027 +#61 := [mp #41 #60]: #58
4.2028 +#77 := [mp~ #61 #80]: #58
4.2029 +#89 := [mp #77 #88]: #86
4.2030 +#155 := [mp #89 #154]: #150
4.2031 +#187 := (not #150)
4.2032 +#188 := (or #187 #184)
4.2033 +#157 := (+ #22 #156)
4.2034 +#158 := (<= #157 0::real)
4.2035 +#159 := (not #158)
4.2036 +#164 := (or #163 #159)
4.2037 +#165 := (not #164)
4.2038 +#189 := (or #187 #165)
4.2039 +#191 := (iff #189 #188)
4.2040 +#193 := (iff #188 #188)
4.2041 +#194 := [rewrite]: #193
4.2042 +#185 := (iff #165 #184)
4.2043 +#182 := (iff #164 #181)
4.2044 +#179 := (iff #159 #178)
4.2045 +#176 := (iff #158 #173)
4.2046 +#166 := (+ #156 #22)
4.2047 +#169 := (<= #166 0::real)
4.2048 +#174 := (iff #169 #173)
4.2049 +#175 := [rewrite]: #174
4.2050 +#170 := (iff #158 #169)
4.2051 +#167 := (= #157 #166)
4.2052 +#168 := [rewrite]: #167
4.2053 +#171 := [monotonicity #168]: #170
4.2054 +#177 := [trans #171 #175]: #176
4.2055 +#180 := [monotonicity #177]: #179
4.2056 +#183 := [monotonicity #180]: #182
4.2057 +#186 := [monotonicity #183]: #185
4.2058 +#192 := [monotonicity #186]: #191
4.2059 +#195 := [trans #192 #194]: #191
4.2060 +#190 := [quant-inst]: #189
4.2061 +#196 := [mp #190 #195]: #188
4.2062 +#220 := [unit-resolution #196 #155]: #184
4.2063 +#197 := (or #181 #162)
4.2064 +#198 := [def-axiom]: #197
4.2065 +#221 := [unit-resolution #198 #220]: #162
4.2066 +#223 := (or #206 #163 #222)
4.2067 +#224 := [th-lemma]: #223
4.2068 +#226 := [unit-resolution #224 #221]: #225
4.2069 +#227 := [unit-resolution #226 #219]: #222
4.2070 +#199 := (or #181 #173)
4.2071 +#200 := [def-axiom]: #199
4.2072 +#228 := [unit-resolution #200 #220]: #173
4.2073 +[th-lemma #228 #227 #211]: false
4.2074 +unsat
4.2075 +06d4133eb0950a5f12d22480aa2707e31af2b064 86 0
4.2076 #2 := false
4.2077 #37 := 0::real
4.2078 decl uf_2 :: (-> T2 T1 real)
4.2079 @@ -3210,511 +3210,3 @@
4.2080 #155 := [th-lemma]: #154
4.2081 [unit-resolution #155 #60 #148 #144]: false
4.2082 unsat
4.2083 -V+IAyBZU/6QjYs6JkXx8LQ 57 0
4.2084 -#2 := false
4.2085 -#4 := 0::real
4.2086 -decl uf_1 :: (-> T2 real)
4.2087 -decl uf_2 :: (-> T1 T1 T2)
4.2088 -decl uf_12 :: (-> T4 T1)
4.2089 -decl uf_4 :: T4
4.2090 -#11 := uf_4
4.2091 -#39 := (uf_12 uf_4)
4.2092 -decl uf_10 :: T4
4.2093 -#27 := uf_10
4.2094 -#38 := (uf_12 uf_10)
4.2095 -#40 := (uf_2 #38 #39)
4.2096 -#41 := (uf_1 #40)
4.2097 -#264 := (>= #41 0::real)
4.2098 -#266 := (not #264)
4.2099 -#43 := (= #41 0::real)
4.2100 -#44 := (not #43)
4.2101 -#131 := [asserted]: #44
4.2102 -#272 := (or #43 #266)
4.2103 -#42 := (<= #41 0::real)
4.2104 -#130 := [asserted]: #42
4.2105 -#265 := (not #42)
4.2106 -#270 := (or #43 #265 #266)
4.2107 -#271 := [th-lemma]: #270
4.2108 -#273 := [unit-resolution #271 #130]: #272
4.2109 -#274 := [unit-resolution #273 #131]: #266
4.2110 -#6 := (:var 0 T1)
4.2111 -#5 := (:var 1 T1)
4.2112 -#7 := (uf_2 #5 #6)
4.2113 -#241 := (pattern #7)
4.2114 -#8 := (uf_1 #7)
4.2115 -#65 := (>= #8 0::real)
4.2116 -#242 := (forall (vars (?x1 T1) (?x2 T1)) (:pat #241) #65)
4.2117 -#66 := (forall (vars (?x1 T1) (?x2 T1)) #65)
4.2118 -#245 := (iff #66 #242)
4.2119 -#243 := (iff #65 #65)
4.2120 -#244 := [refl]: #243
4.2121 -#246 := [quant-intro #244]: #245
4.2122 -#149 := (~ #66 #66)
4.2123 -#151 := (~ #65 #65)
4.2124 -#152 := [refl]: #151
4.2125 -#150 := [nnf-pos #152]: #149
4.2126 -#9 := (<= 0::real #8)
4.2127 -#10 := (forall (vars (?x1 T1) (?x2 T1)) #9)
4.2128 -#67 := (iff #10 #66)
4.2129 -#63 := (iff #9 #65)
4.2130 -#64 := [rewrite]: #63
4.2131 -#68 := [quant-intro #64]: #67
4.2132 -#60 := [asserted]: #10
4.2133 -#69 := [mp #60 #68]: #66
4.2134 -#147 := [mp~ #69 #150]: #66
4.2135 -#247 := [mp #147 #246]: #242
4.2136 -#267 := (not #242)
4.2137 -#268 := (or #267 #264)
4.2138 -#269 := [quant-inst]: #268
4.2139 -[unit-resolution #269 #247 #274]: false
4.2140 -unsat
4.2141 -vqiyJ/qjGXZ3iOg6xftiug 15 0
4.2142 -uf_1 -> val!0
4.2143 -uf_2 -> val!1
4.2144 -uf_3 -> val!2
4.2145 -uf_5 -> val!15
4.2146 -uf_6 -> val!26
4.2147 -uf_4 -> {
4.2148 - val!0 -> val!12
4.2149 - val!1 -> val!13
4.2150 - else -> val!13
4.2151 -}
4.2152 -uf_7 -> {
4.2153 - val!6 -> val!31
4.2154 - else -> val!31
4.2155 -}
4.2156 -sat
4.2157 -mrZPJZyTokErrN6SYupisw 9 0
4.2158 -uf_4 -> val!1
4.2159 -uf_2 -> val!3
4.2160 -uf_3 -> val!4
4.2161 -uf_1 -> {
4.2162 - val!5 -> val!6
4.2163 - val!4 -> val!7
4.2164 - else -> val!7
4.2165 -}
4.2166 -sat
4.2167 -qkVrmXMcHAG5MLuJ9d8jXQ 211 0
4.2168 -#2 := false
4.2169 -#33 := 0::real
4.2170 -decl uf_11 :: (-> T5 T6 real)
4.2171 -decl uf_15 :: T6
4.2172 -#28 := uf_15
4.2173 -decl uf_16 :: T5
4.2174 -#30 := uf_16
4.2175 -#31 := (uf_11 uf_16 uf_15)
4.2176 -decl uf_12 :: (-> T7 T8 T5)
4.2177 -decl uf_14 :: T8
4.2178 -#26 := uf_14
4.2179 -decl uf_13 :: (-> T1 T7)
4.2180 -decl uf_8 :: T1
4.2181 -#16 := uf_8
4.2182 -#25 := (uf_13 uf_8)
4.2183 -#27 := (uf_12 #25 uf_14)
4.2184 -#29 := (uf_11 #27 uf_15)
4.2185 -#73 := -1::real
4.2186 -#84 := (* -1::real #29)
4.2187 -#85 := (+ #84 #31)
4.2188 -#74 := (* -1::real #31)
4.2189 -#75 := (+ #29 #74)
4.2190 -#112 := (>= #75 0::real)
4.2191 -#119 := (ite #112 #75 #85)
4.2192 -#127 := (* -1::real #119)
4.2193 -decl uf_17 :: T5
4.2194 -#37 := uf_17
4.2195 -#38 := (uf_11 uf_17 uf_15)
4.2196 -#102 := -1/3::real
4.2197 -#103 := (* -1/3::real #38)
4.2198 -#128 := (+ #103 #127)
4.2199 -#100 := 1/3::real
4.2200 -#101 := (* 1/3::real #31)
4.2201 -#129 := (+ #101 #128)
4.2202 -#130 := (<= #129 0::real)
4.2203 -#131 := (not #130)
4.2204 -#40 := 3::real
4.2205 -#39 := (- #31 #38)
4.2206 -#41 := (/ #39 3::real)
4.2207 -#32 := (- #29 #31)
4.2208 -#35 := (- #32)
4.2209 -#34 := (< #32 0::real)
4.2210 -#36 := (ite #34 #35 #32)
4.2211 -#42 := (< #36 #41)
4.2212 -#136 := (iff #42 #131)
4.2213 -#104 := (+ #101 #103)
4.2214 -#78 := (< #75 0::real)
4.2215 -#90 := (ite #78 #85 #75)
4.2216 -#109 := (< #90 #104)
4.2217 -#134 := (iff #109 #131)
4.2218 -#124 := (< #119 #104)
4.2219 -#132 := (iff #124 #131)
4.2220 -#133 := [rewrite]: #132
4.2221 -#125 := (iff #109 #124)
4.2222 -#122 := (= #90 #119)
4.2223 -#113 := (not #112)
4.2224 -#116 := (ite #113 #85 #75)
4.2225 -#120 := (= #116 #119)
4.2226 -#121 := [rewrite]: #120
4.2227 -#117 := (= #90 #116)
4.2228 -#114 := (iff #78 #113)
4.2229 -#115 := [rewrite]: #114
4.2230 -#118 := [monotonicity #115]: #117
4.2231 -#123 := [trans #118 #121]: #122
4.2232 -#126 := [monotonicity #123]: #125
4.2233 -#135 := [trans #126 #133]: #134
4.2234 -#110 := (iff #42 #109)
4.2235 -#107 := (= #41 #104)
4.2236 -#93 := (* -1::real #38)
4.2237 -#94 := (+ #31 #93)
4.2238 -#97 := (/ #94 3::real)
4.2239 -#105 := (= #97 #104)
4.2240 -#106 := [rewrite]: #105
4.2241 -#98 := (= #41 #97)
4.2242 -#95 := (= #39 #94)
4.2243 -#96 := [rewrite]: #95
4.2244 -#99 := [monotonicity #96]: #98
4.2245 -#108 := [trans #99 #106]: #107
4.2246 -#91 := (= #36 #90)
4.2247 -#76 := (= #32 #75)
4.2248 -#77 := [rewrite]: #76
4.2249 -#88 := (= #35 #85)
4.2250 -#81 := (- #75)
4.2251 -#86 := (= #81 #85)
4.2252 -#87 := [rewrite]: #86
4.2253 -#82 := (= #35 #81)
4.2254 -#83 := [monotonicity #77]: #82
4.2255 -#89 := [trans #83 #87]: #88
4.2256 -#79 := (iff #34 #78)
4.2257 -#80 := [monotonicity #77]: #79
4.2258 -#92 := [monotonicity #80 #89 #77]: #91
4.2259 -#111 := [monotonicity #92 #108]: #110
4.2260 -#137 := [trans #111 #135]: #136
4.2261 -#72 := [asserted]: #42
4.2262 -#138 := [mp #72 #137]: #131
4.2263 -decl uf_1 :: T1
4.2264 -#4 := uf_1
4.2265 -#43 := (uf_13 uf_1)
4.2266 -#44 := (uf_12 #43 uf_14)
4.2267 -#45 := (uf_11 #44 uf_15)
4.2268 -#149 := (* -1::real #45)
4.2269 -#150 := (+ #38 #149)
4.2270 -#140 := (+ #93 #45)
4.2271 -#161 := (<= #150 0::real)
4.2272 -#168 := (ite #161 #140 #150)
4.2273 -#176 := (* -1::real #168)
4.2274 -#177 := (+ #103 #176)
4.2275 -#178 := (+ #101 #177)
4.2276 -#179 := (<= #178 0::real)
4.2277 -#180 := (not #179)
4.2278 -#46 := (- #45 #38)
4.2279 -#48 := (- #46)
4.2280 -#47 := (< #46 0::real)
4.2281 -#49 := (ite #47 #48 #46)
4.2282 -#50 := (< #49 #41)
4.2283 -#185 := (iff #50 #180)
4.2284 -#143 := (< #140 0::real)
4.2285 -#155 := (ite #143 #150 #140)
4.2286 -#158 := (< #155 #104)
4.2287 -#183 := (iff #158 #180)
4.2288 -#173 := (< #168 #104)
4.2289 -#181 := (iff #173 #180)
4.2290 -#182 := [rewrite]: #181
4.2291 -#174 := (iff #158 #173)
4.2292 -#171 := (= #155 #168)
4.2293 -#162 := (not #161)
4.2294 -#165 := (ite #162 #150 #140)
4.2295 -#169 := (= #165 #168)
4.2296 -#170 := [rewrite]: #169
4.2297 -#166 := (= #155 #165)
4.2298 -#163 := (iff #143 #162)
4.2299 -#164 := [rewrite]: #163
4.2300 -#167 := [monotonicity #164]: #166
4.2301 -#172 := [trans #167 #170]: #171
4.2302 -#175 := [monotonicity #172]: #174
4.2303 -#184 := [trans #175 #182]: #183
4.2304 -#159 := (iff #50 #158)
4.2305 -#156 := (= #49 #155)
4.2306 -#141 := (= #46 #140)
4.2307 -#142 := [rewrite]: #141
4.2308 -#153 := (= #48 #150)
4.2309 -#146 := (- #140)
4.2310 -#151 := (= #146 #150)
4.2311 -#152 := [rewrite]: #151
4.2312 -#147 := (= #48 #146)
4.2313 -#148 := [monotonicity #142]: #147
4.2314 -#154 := [trans #148 #152]: #153
4.2315 -#144 := (iff #47 #143)
4.2316 -#145 := [monotonicity #142]: #144
4.2317 -#157 := [monotonicity #145 #154 #142]: #156
4.2318 -#160 := [monotonicity #157 #108]: #159
4.2319 -#186 := [trans #160 #184]: #185
4.2320 -#139 := [asserted]: #50
4.2321 -#187 := [mp #139 #186]: #180
4.2322 -#299 := (+ #140 #176)
4.2323 -#300 := (<= #299 0::real)
4.2324 -#290 := (= #140 #168)
4.2325 -#329 := [hypothesis]: #162
4.2326 -#191 := (+ #29 #149)
4.2327 -#192 := (<= #191 0::real)
4.2328 -#51 := (<= #29 #45)
4.2329 -#193 := (iff #51 #192)
4.2330 -#194 := [rewrite]: #193
4.2331 -#188 := [asserted]: #51
4.2332 -#195 := [mp #188 #194]: #192
4.2333 -#298 := (+ #75 #127)
4.2334 -#301 := (<= #298 0::real)
4.2335 -#284 := (= #75 #119)
4.2336 -#302 := [hypothesis]: #113
4.2337 -#296 := (+ #85 #127)
4.2338 -#297 := (<= #296 0::real)
4.2339 -#285 := (= #85 #119)
4.2340 -#288 := (or #112 #285)
4.2341 -#289 := [def-axiom]: #288
4.2342 -#303 := [unit-resolution #289 #302]: #285
4.2343 -#304 := (not #285)
4.2344 -#305 := (or #304 #297)
4.2345 -#306 := [th-lemma]: #305
4.2346 -#307 := [unit-resolution #306 #303]: #297
4.2347 -#315 := (not #290)
4.2348 -#310 := (not #300)
4.2349 -#311 := (or #310 #112)
4.2350 -#308 := [hypothesis]: #300
4.2351 -#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false
4.2352 -#312 := [lemma #309]: #311
4.2353 -#322 := [unit-resolution #312 #302]: #310
4.2354 -#316 := (or #315 #300)
4.2355 -#313 := [hypothesis]: #310
4.2356 -#314 := [hypothesis]: #290
4.2357 -#317 := [th-lemma]: #316
4.2358 -#318 := [unit-resolution #317 #314 #313]: false
4.2359 -#319 := [lemma #318]: #316
4.2360 -#323 := [unit-resolution #319 #322]: #315
4.2361 -#292 := (or #162 #290)
4.2362 -#293 := [def-axiom]: #292
4.2363 -#324 := [unit-resolution #293 #323]: #162
4.2364 -#325 := [th-lemma #324 #307 #138 #302 #195]: false
4.2365 -#326 := [lemma #325]: #112
4.2366 -#286 := (or #113 #284)
4.2367 -#287 := [def-axiom]: #286
4.2368 -#330 := [unit-resolution #287 #326]: #284
4.2369 -#331 := (not #284)
4.2370 -#332 := (or #331 #301)
4.2371 -#333 := [th-lemma]: #332
4.2372 -#334 := [unit-resolution #333 #330]: #301
4.2373 -#335 := [th-lemma #326 #334 #195 #329 #138]: false
4.2374 -#336 := [lemma #335]: #161
4.2375 -#327 := [unit-resolution #293 #336]: #290
4.2376 -#328 := [unit-resolution #319 #327]: #300
4.2377 -[th-lemma #326 #334 #195 #328 #187 #138]: false
4.2378 -unsat
4.2379 -WrIjxhfF5EcRCmS6xKG3XQ 211 0
4.2380 -#2 := false
4.2381 -#33 := 0::real
4.2382 -decl uf_11 :: (-> T5 T6 real)
4.2383 -decl uf_15 :: T6
4.2384 -#28 := uf_15
4.2385 -decl uf_16 :: T5
4.2386 -#30 := uf_16
4.2387 -#31 := (uf_11 uf_16 uf_15)
4.2388 -decl uf_12 :: (-> T7 T8 T5)
4.2389 -decl uf_14 :: T8
4.2390 -#26 := uf_14
4.2391 -decl uf_13 :: (-> T1 T7)
4.2392 -decl uf_8 :: T1
4.2393 -#16 := uf_8
4.2394 -#25 := (uf_13 uf_8)
4.2395 -#27 := (uf_12 #25 uf_14)
4.2396 -#29 := (uf_11 #27 uf_15)
4.2397 -#73 := -1::real
4.2398 -#84 := (* -1::real #29)
4.2399 -#85 := (+ #84 #31)
4.2400 -#74 := (* -1::real #31)
4.2401 -#75 := (+ #29 #74)
4.2402 -#112 := (>= #75 0::real)
4.2403 -#119 := (ite #112 #75 #85)
4.2404 -#127 := (* -1::real #119)
4.2405 -decl uf_17 :: T5
4.2406 -#37 := uf_17
4.2407 -#38 := (uf_11 uf_17 uf_15)
4.2408 -#102 := -1/3::real
4.2409 -#103 := (* -1/3::real #38)
4.2410 -#128 := (+ #103 #127)
4.2411 -#100 := 1/3::real
4.2412 -#101 := (* 1/3::real #31)
4.2413 -#129 := (+ #101 #128)
4.2414 -#130 := (<= #129 0::real)
4.2415 -#131 := (not #130)
4.2416 -#40 := 3::real
4.2417 -#39 := (- #31 #38)
4.2418 -#41 := (/ #39 3::real)
4.2419 -#32 := (- #29 #31)
4.2420 -#35 := (- #32)
4.2421 -#34 := (< #32 0::real)
4.2422 -#36 := (ite #34 #35 #32)
4.2423 -#42 := (< #36 #41)
4.2424 -#136 := (iff #42 #131)
4.2425 -#104 := (+ #101 #103)
4.2426 -#78 := (< #75 0::real)
4.2427 -#90 := (ite #78 #85 #75)
4.2428 -#109 := (< #90 #104)
4.2429 -#134 := (iff #109 #131)
4.2430 -#124 := (< #119 #104)
4.2431 -#132 := (iff #124 #131)
4.2432 -#133 := [rewrite]: #132
4.2433 -#125 := (iff #109 #124)
4.2434 -#122 := (= #90 #119)
4.2435 -#113 := (not #112)
4.2436 -#116 := (ite #113 #85 #75)
4.2437 -#120 := (= #116 #119)
4.2438 -#121 := [rewrite]: #120
4.2439 -#117 := (= #90 #116)
4.2440 -#114 := (iff #78 #113)
4.2441 -#115 := [rewrite]: #114
4.2442 -#118 := [monotonicity #115]: #117
4.2443 -#123 := [trans #118 #121]: #122
4.2444 -#126 := [monotonicity #123]: #125
4.2445 -#135 := [trans #126 #133]: #134
4.2446 -#110 := (iff #42 #109)
4.2447 -#107 := (= #41 #104)
4.2448 -#93 := (* -1::real #38)
4.2449 -#94 := (+ #31 #93)
4.2450 -#97 := (/ #94 3::real)
4.2451 -#105 := (= #97 #104)
4.2452 -#106 := [rewrite]: #105
4.2453 -#98 := (= #41 #97)
4.2454 -#95 := (= #39 #94)
4.2455 -#96 := [rewrite]: #95
4.2456 -#99 := [monotonicity #96]: #98
4.2457 -#108 := [trans #99 #106]: #107
4.2458 -#91 := (= #36 #90)
4.2459 -#76 := (= #32 #75)
4.2460 -#77 := [rewrite]: #76
4.2461 -#88 := (= #35 #85)
4.2462 -#81 := (- #75)
4.2463 -#86 := (= #81 #85)
4.2464 -#87 := [rewrite]: #86
4.2465 -#82 := (= #35 #81)
4.2466 -#83 := [monotonicity #77]: #82
4.2467 -#89 := [trans #83 #87]: #88
4.2468 -#79 := (iff #34 #78)
4.2469 -#80 := [monotonicity #77]: #79
4.2470 -#92 := [monotonicity #80 #89 #77]: #91
4.2471 -#111 := [monotonicity #92 #108]: #110
4.2472 -#137 := [trans #111 #135]: #136
4.2473 -#72 := [asserted]: #42
4.2474 -#138 := [mp #72 #137]: #131
4.2475 -decl uf_1 :: T1
4.2476 -#4 := uf_1
4.2477 -#43 := (uf_13 uf_1)
4.2478 -#44 := (uf_12 #43 uf_14)
4.2479 -#45 := (uf_11 #44 uf_15)
4.2480 -#149 := (* -1::real #45)
4.2481 -#150 := (+ #38 #149)
4.2482 -#140 := (+ #93 #45)
4.2483 -#161 := (<= #150 0::real)
4.2484 -#168 := (ite #161 #140 #150)
4.2485 -#176 := (* -1::real #168)
4.2486 -#177 := (+ #103 #176)
4.2487 -#178 := (+ #101 #177)
4.2488 -#179 := (<= #178 0::real)
4.2489 -#180 := (not #179)
4.2490 -#46 := (- #45 #38)
4.2491 -#48 := (- #46)
4.2492 -#47 := (< #46 0::real)
4.2493 -#49 := (ite #47 #48 #46)
4.2494 -#50 := (< #49 #41)
4.2495 -#185 := (iff #50 #180)
4.2496 -#143 := (< #140 0::real)
4.2497 -#155 := (ite #143 #150 #140)
4.2498 -#158 := (< #155 #104)
4.2499 -#183 := (iff #158 #180)
4.2500 -#173 := (< #168 #104)
4.2501 -#181 := (iff #173 #180)
4.2502 -#182 := [rewrite]: #181
4.2503 -#174 := (iff #158 #173)
4.2504 -#171 := (= #155 #168)
4.2505 -#162 := (not #161)
4.2506 -#165 := (ite #162 #150 #140)
4.2507 -#169 := (= #165 #168)
4.2508 -#170 := [rewrite]: #169
4.2509 -#166 := (= #155 #165)
4.2510 -#163 := (iff #143 #162)
4.2511 -#164 := [rewrite]: #163
4.2512 -#167 := [monotonicity #164]: #166
4.2513 -#172 := [trans #167 #170]: #171
4.2514 -#175 := [monotonicity #172]: #174
4.2515 -#184 := [trans #175 #182]: #183
4.2516 -#159 := (iff #50 #158)
4.2517 -#156 := (= #49 #155)
4.2518 -#141 := (= #46 #140)
4.2519 -#142 := [rewrite]: #141
4.2520 -#153 := (= #48 #150)
4.2521 -#146 := (- #140)
4.2522 -#151 := (= #146 #150)
4.2523 -#152 := [rewrite]: #151
4.2524 -#147 := (= #48 #146)
4.2525 -#148 := [monotonicity #142]: #147
4.2526 -#154 := [trans #148 #152]: #153
4.2527 -#144 := (iff #47 #143)
4.2528 -#145 := [monotonicity #142]: #144
4.2529 -#157 := [monotonicity #145 #154 #142]: #156
4.2530 -#160 := [monotonicity #157 #108]: #159
4.2531 -#186 := [trans #160 #184]: #185
4.2532 -#139 := [asserted]: #50
4.2533 -#187 := [mp #139 #186]: #180
4.2534 -#299 := (+ #140 #176)
4.2535 -#300 := (<= #299 0::real)
4.2536 -#290 := (= #140 #168)
4.2537 -#329 := [hypothesis]: #162
4.2538 -#191 := (+ #29 #149)
4.2539 -#192 := (<= #191 0::real)
4.2540 -#51 := (<= #29 #45)
4.2541 -#193 := (iff #51 #192)
4.2542 -#194 := [rewrite]: #193
4.2543 -#188 := [asserted]: #51
4.2544 -#195 := [mp #188 #194]: #192
4.2545 -#298 := (+ #75 #127)
4.2546 -#301 := (<= #298 0::real)
4.2547 -#284 := (= #75 #119)
4.2548 -#302 := [hypothesis]: #113
4.2549 -#296 := (+ #85 #127)
4.2550 -#297 := (<= #296 0::real)
4.2551 -#285 := (= #85 #119)
4.2552 -#288 := (or #112 #285)
4.2553 -#289 := [def-axiom]: #288
4.2554 -#303 := [unit-resolution #289 #302]: #285
4.2555 -#304 := (not #285)
4.2556 -#305 := (or #304 #297)
4.2557 -#306 := [th-lemma]: #305
4.2558 -#307 := [unit-resolution #306 #303]: #297
4.2559 -#315 := (not #290)
4.2560 -#310 := (not #300)
4.2561 -#311 := (or #310 #112)
4.2562 -#308 := [hypothesis]: #300
4.2563 -#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false
4.2564 -#312 := [lemma #309]: #311
4.2565 -#322 := [unit-resolution #312 #302]: #310
4.2566 -#316 := (or #315 #300)
4.2567 -#313 := [hypothesis]: #310
4.2568 -#314 := [hypothesis]: #290
4.2569 -#317 := [th-lemma]: #316
4.2570 -#318 := [unit-resolution #317 #314 #313]: false
4.2571 -#319 := [lemma #318]: #316
4.2572 -#323 := [unit-resolution #319 #322]: #315
4.2573 -#292 := (or #162 #290)
4.2574 -#293 := [def-axiom]: #292
4.2575 -#324 := [unit-resolution #293 #323]: #162
4.2576 -#325 := [th-lemma #324 #307 #138 #302 #195]: false
4.2577 -#326 := [lemma #325]: #112
4.2578 -#286 := (or #113 #284)
4.2579 -#287 := [def-axiom]: #286
4.2580 -#330 := [unit-resolution #287 #326]: #284
4.2581 -#331 := (not #284)
4.2582 -#332 := (or #331 #301)
4.2583 -#333 := [th-lemma]: #332
4.2584 -#334 := [unit-resolution #333 #330]: #301
4.2585 -#335 := [th-lemma #326 #334 #195 #329 #138]: false
4.2586 -#336 := [lemma #335]: #161
4.2587 -#327 := [unit-resolution #293 #336]: #290
4.2588 -#328 := [unit-resolution #319 #327]: #300
4.2589 -[th-lemma #326 #334 #195 #328 #187 #138]: false
4.2590 -unsat
5.1 --- a/src/HOL/SMT/Examples/SMT_Examples.certs Wed Mar 24 14:03:52 2010 +0100
5.2 +++ b/src/HOL/SMT/Examples/SMT_Examples.certs Wed Mar 24 14:08:07 2010 +0100
5.3 @@ -1,4 +1,4 @@
5.4 -Fg1W6egjwo9zhhAmUXOW+w 8 0
5.5 +bb06851c317eb8b672e27364b0ae34a4e39eb880 8 0
5.6 #2 := false
5.7 #1 := true
5.8 #4 := (not true)
5.9 @@ -7,7 +7,7 @@
5.10 #20 := [asserted]: #4
5.11 [mp #20 #22]: false
5.12 unsat
5.13 -2+cndY9nzS72l7VvBCGRAw 19 0
5.14 +70d1f77bec207467bc0306af0d98a71fa8328274 19 0
5.15 #2 := false
5.16 decl up_1 :: bool
5.17 #4 := up_1
5.18 @@ -27,7 +27,7 @@
5.19 #23 := [asserted]: #7
5.20 [mp #23 #32]: false
5.21 unsat
5.22 -0vJQrobUDcQ9PkGJO8aM8g 25 0
5.23 +148012a9e9d44fe30a0c79e3344bdb805124f661 25 0
5.24 #2 := false
5.25 decl up_1 :: bool
5.26 #4 := up_1
5.27 @@ -53,7 +53,7 @@
5.28 #23 := [asserted]: #7
5.29 [mp #23 #38]: false
5.30 unsat
5.31 -AGGnpwEv208Vqxly7wTWHA 38 0
5.32 +bc9a25b7f6dc3ac2431ee71b6e71c5a7b25e89d1 38 0
5.33 #2 := false
5.34 decl up_2 :: bool
5.35 #5 := up_2
5.36 @@ -92,9 +92,9 @@
5.37 #30 := [and-elim #31]: #6
5.38 [mp #30 #52]: false
5.39 unsat
5.40 -wakXeIy1uoPgglzOQGFhJQ 1 0
5.41 -unsat
5.42 -cpSlDe0l7plVktRNxGU5dA 71 0
5.43 +9b3db6ce34c8a1806160f1349b898b6c5ca40ba0 1 0
5.44 +unsat
5.45 +912e9b7fb52f4a71d232354b3bb53c11e5a41ccd 71 0
5.46 #2 := false
5.47 decl up_1 :: bool
5.48 #4 := up_1
5.49 @@ -166,7 +166,7 @@
5.50 #31 := [asserted]: #15
5.51 [mp #31 #82]: false
5.52 unsat
5.53 -pg19mjJfV75T2QDrgWd4JA 57 0
5.54 +4d063d3cdf6657ddb4258379f900ef18e9042978 57 0
5.55 #2 := false
5.56 decl up_1 :: bool
5.57 #4 := up_1
5.58 @@ -224,7 +224,7 @@
5.59 #30 := [asserted]: #14
5.60 [mp #30 #70]: false
5.61 unsat
5.62 -Mj1B8X1MaN7xU/W4Kz3FoQ 194 0
5.63 +c6eb111aa830c9669a030c2e58b4e827706981da 194 0
5.64 #2 := false
5.65 decl up_1 :: bool
5.66 #4 := up_1
5.67 @@ -419,7 +419,7 @@
5.68 #237 := [mp #83 #236]: #75
5.69 [mp #237 #247]: false
5.70 unsat
5.71 -JkhYJB8FDavTZkizO1/9IA 52 0
5.72 +42890f9fa7c18237798ca55d0cf9dfff6f2f868a 52 0
5.73 #2 := false
5.74 decl uf_1 :: (-> T1 T1 T1)
5.75 decl uf_2 :: T1
5.76 @@ -472,7 +472,7 @@
5.77 #113 := [quant-inst]: #199
5.78 [unit-resolution #113 #536 #49]: false
5.79 unsat
5.80 -0ZdSZH2DbtjHNTyrDkZmXg 1667 0
5.81 +94169ba151f7a720e818287ce490015dde764bad 1667 0
5.82 #2 := false
5.83 decl up_54 :: bool
5.84 #126 := up_54
5.85 @@ -2140,7 +2140,7 @@
5.86 #2371 := [unit-resolution #891 #2369]: #166
5.87 [unit-resolution #2159 #2371 #2370 #2358 #2357]: false
5.88 unsat
5.89 -R3pmBDBlU9XdUrxJXhj7nA 78 0
5.90 +d8841d120b7cf772be783d793f759fb6353b9fcd 78 0
5.91 #2 := false
5.92 decl up_1 :: (-> int bool)
5.93 decl ?x1!0 :: int
5.94 @@ -2219,7 +2219,7 @@
5.95 #82 := [and-elim #81]: #55
5.96 [unit-resolution #82 #95]: false
5.97 unsat
5.98 -IBRj/loev6P6r0J+HOit6A 135 0
5.99 +18bde40beb0dd1fc2613a67805e24d767dd9a3bf 135 0
5.100 #2 := false
5.101 decl up_1 :: (-> T1 T2 bool)
5.102 #5 := (:var 0 T2)
5.103 @@ -2355,7 +2355,7 @@
5.104 #176 := [quant-inst]: #538
5.105 [unit-resolution #176 #252 #535]: false
5.106 unsat
5.107 -72504KVBixGB/87pOYiU/A 135 2
5.108 +013861f683c286a3ef38681266913846a3a39b9a 135 2
5.109 #2 := false
5.110 decl up_1 :: (-> T1 T2 bool)
5.111 #5 := (:var 0 T2)
5.112 @@ -2493,7 +2493,7 @@
5.113 unsat
5.114 WARNING: failed to find a pattern for quantifier (quantifier id: k!12)
5.115
5.116 -RaQLz4GxtUICnOD5WoYnzQ 56 0
5.117 +0e958e27514643bb596851e6dbb61a23f6b348b0 56 0
5.118 #2 := false
5.119 decl up_1 :: (-> T1 bool)
5.120 decl uf_2 :: T1
5.121 @@ -2550,7 +2550,7 @@
5.122 #120 := [quant-inst]: #206
5.123 [unit-resolution #120 #542 #41]: false
5.124 unsat
5.125 -NPQIgVPhSpgSLeS+u/EatQ 17 0
5.126 +6ecefa4023d224e6c51226d5bee17e2a19cc4333 17 0
5.127 #2 := false
5.128 #4 := 3::int
5.129 #5 := (= 3::int 3::int)
5.130 @@ -2568,7 +2568,7 @@
5.131 #22 := [asserted]: #6
5.132 [mp #22 #31]: false
5.133 unsat
5.134 -Lc9NwVtwY2Wo0G7UbFD1oA 17 0
5.135 +5e0256133fc82f0e2fea6597b863483e4e61d3c6 17 0
5.136 #2 := false
5.137 #4 := 3::real
5.138 #5 := (= 3::real 3::real)
5.139 @@ -2586,7 +2586,7 @@
5.140 #22 := [asserted]: #6
5.141 [mp #22 #31]: false
5.142 unsat
5.143 -pYVrUflpYrrZEWALJDnvPw 26 0
5.144 +55cf32b061b843ac5bcaefb74005a7dd3a24386f 26 0
5.145 #2 := false
5.146 #7 := 4::int
5.147 #5 := 1::int
5.148 @@ -2613,7 +2613,7 @@
5.149 #25 := [asserted]: #9
5.150 [mp #25 #40]: false
5.151 unsat
5.152 -FIqzVlbN8RT0iWarmBEpjw 41 0
5.153 +e81d17ec85af9db5ec6ba5bf4ced62daaa719ef3 41 0
5.154 #2 := false
5.155 decl uf_1 :: int
5.156 #4 := uf_1
5.157 @@ -2655,7 +2655,7 @@
5.158 #28 := [asserted]: #12
5.159 [mp #28 #52]: false
5.160 unsat
5.161 -HWVNtxMa8xktQsg8pHG+1w 35 0
5.162 +448f188ebf9d7fbd2920c0a51a8f105192e6af1a 35 0
5.163 #2 := false
5.164 #5 := 3::int
5.165 #6 := 8::int
5.166 @@ -2691,7 +2691,7 @@
5.167 #26 := [asserted]: #10
5.168 [mp #26 #51]: false
5.169 unsat
5.170 -M71YYpEc8u/aEIH3MOQrcg 250 0
5.171 +c3751ecae7701923f4ba6a90c6c6eee35ee1b13d 250 0
5.172 #2 := false
5.173 #7 := 0::real
5.174 decl uf_2 :: real
5.175 @@ -2942,7 +2942,7 @@
5.176 #294 := [unit-resolution #190 #293]: #188
5.177 [th-lemma #280 #294]: false
5.178 unsat
5.179 -G00bTqBjtW66EmwIZbXbOg 124 0
5.180 +8e6af261ea9f94b967813d4e2f2abcb94463d612 124 0
5.181 #2 := false
5.182 decl uf_1 :: (-> T1 T2)
5.183 decl uf_3 :: T1
5.184 @@ -3067,7 +3067,7 @@
5.185 #34 := [asserted]: #11
5.186 [unit-resolution #34 #536]: false
5.187 unsat
5.188 -6QdzkSy/RtEjUu+wUKIKqA 54 0
5.189 +243524c591f6dcfe16a79ddd249c64a337ff3612 54 0
5.190 #2 := false
5.191 #9 := 1::int
5.192 decl uf_1 :: int
5.193 @@ -3122,7 +3122,7 @@
5.194 #28 := [asserted]: #12
5.195 [mp #28 #67]: false
5.196 unsat
5.197 -xoSwaSeELbR0PHe0zb/BSg 63 0
5.198 +adfe7d6c2da6653191952bd9673c1274f94c2ab2 63 0
5.199 #2 := false
5.200 #11 := 0::int
5.201 decl uf_2 :: int
5.202 @@ -3186,7 +3186,7 @@
5.203 #76 := [mp #52 #75]: #63
5.204 [mp #76 #84]: false
5.205 unsat
5.206 -ciHqmDSmPpA15rO932dhvA 35 0
5.207 +3440e29713ba625633b10a2c4fdc186cb6e0cf3e 35 0
5.208 #2 := false
5.209 #6 := 5::int
5.210 #4 := 2::int
5.211 @@ -3222,7 +3222,7 @@
5.212 #25 := [asserted]: #9
5.213 [mp #25 #49]: false
5.214 unsat
5.215 -HzwFy7SRHqpspkYnzyeF4w 45 0
5.216 +5f3503ae4a43341932052006638f286bea551e87 45 0
5.217 #2 := false
5.218 #11 := 4::real
5.219 decl uf_2 :: real
5.220 @@ -3268,7 +3268,7 @@
5.221 #60 := [mp #36 #59]: #51
5.222 [th-lemma #60 #47 #38]: false
5.223 unsat
5.224 -XW7QIWmzYjfQXaHHPc98eA 59 0
5.225 +347776ce17d7d3f6d1252ead05795e4eee6f4b20 59 0
5.226 #2 := false
5.227 #16 := (not false)
5.228 decl uf_2 :: int
5.229 @@ -3328,94 +3328,7 @@
5.230 #34 := [asserted]: #18
5.231 [mp #34 #71]: false
5.232 unsat
5.233 -ZGL00TLLioiLlWFiXUnbxg 86 0
5.234 -#2 := false
5.235 -decl uf_1 :: int
5.236 -#5 := uf_1
5.237 -#7 := 2::int
5.238 -#29 := (* 2::int uf_1)
5.239 -#4 := 0::int
5.240 -#54 := (= 0::int #29)
5.241 -#55 := (not #54)
5.242 -#61 := (= #29 0::int)
5.243 -#104 := (not #61)
5.244 -#110 := (iff #104 #55)
5.245 -#108 := (iff #61 #54)
5.246 -#109 := [commutativity]: #108
5.247 -#111 := [monotonicity #109]: #110
5.248 -#62 := (<= #29 0::int)
5.249 -#100 := (not #62)
5.250 -#30 := (<= uf_1 0::int)
5.251 -#31 := (not #30)
5.252 -#6 := (< 0::int uf_1)
5.253 -#32 := (iff #6 #31)
5.254 -#33 := [rewrite]: #32
5.255 -#27 := [asserted]: #6
5.256 -#34 := [mp #27 #33]: #31
5.257 -#101 := (or #100 #30)
5.258 -#102 := [th-lemma]: #101
5.259 -#103 := [unit-resolution #102 #34]: #100
5.260 -#105 := (or #104 #62)
5.261 -#106 := [th-lemma]: #105
5.262 -#107 := [unit-resolution #106 #103]: #104
5.263 -#112 := [mp #107 #111]: #55
5.264 -#56 := (= uf_1 #29)
5.265 -#57 := (not #56)
5.266 -#53 := (= 0::int uf_1)
5.267 -#50 := (not #53)
5.268 -#58 := (and #50 #55 #57)
5.269 -#69 := (not #58)
5.270 -#42 := (distinct 0::int uf_1 #29)
5.271 -#47 := (not #42)
5.272 -#9 := (- uf_1 uf_1)
5.273 -#8 := (* uf_1 2::int)
5.274 -#10 := (distinct uf_1 #8 #9)
5.275 -#11 := (not #10)
5.276 -#48 := (iff #11 #47)
5.277 -#45 := (iff #10 #42)
5.278 -#39 := (distinct uf_1 #29 0::int)
5.279 -#43 := (iff #39 #42)
5.280 -#44 := [rewrite]: #43
5.281 -#40 := (iff #10 #39)
5.282 -#37 := (= #9 0::int)
5.283 -#38 := [rewrite]: #37
5.284 -#35 := (= #8 #29)
5.285 -#36 := [rewrite]: #35
5.286 -#41 := [monotonicity #36 #38]: #40
5.287 -#46 := [trans #41 #44]: #45
5.288 -#49 := [monotonicity #46]: #48
5.289 -#28 := [asserted]: #11
5.290 -#52 := [mp #28 #49]: #47
5.291 -#80 := (or #42 #69)
5.292 -#81 := [def-axiom]: #80
5.293 -#82 := [unit-resolution #81 #52]: #69
5.294 -#59 := (= uf_1 0::int)
5.295 -#83 := (not #59)
5.296 -#89 := (iff #83 #50)
5.297 -#87 := (iff #59 #53)
5.298 -#88 := [commutativity]: #87
5.299 -#90 := [monotonicity #88]: #89
5.300 -#84 := (or #83 #30)
5.301 -#85 := [th-lemma]: #84
5.302 -#86 := [unit-resolution #85 #34]: #83
5.303 -#91 := [mp #86 #90]: #50
5.304 -#64 := -1::int
5.305 -#65 := (* -1::int #29)
5.306 -#66 := (+ uf_1 #65)
5.307 -#68 := (>= #66 0::int)
5.308 -#92 := (not #68)
5.309 -#93 := (or #92 #30)
5.310 -#94 := [th-lemma]: #93
5.311 -#95 := [unit-resolution #94 #34]: #92
5.312 -#96 := (or #57 #68)
5.313 -#97 := [th-lemma]: #96
5.314 -#98 := [unit-resolution #97 #95]: #57
5.315 -#76 := (or #58 #53 #54 #56)
5.316 -#77 := [def-axiom]: #76
5.317 -#99 := [unit-resolution #77 #98 #91 #82]: #54
5.318 -[unit-resolution #99 #112]: false
5.319 -unsat
5.320 -DWt5rIK6NWlI4vrw+691Zg 212 0
5.321 +f7b1b99e3470f713e48aaae1336ace10223be6f0 212 0
5.322 #2 := false
5.323 decl uf_4 :: T1
5.324 #13 := uf_4
5.325 @@ -3628,7 +3541,94 @@
5.326 #519 := [unit-resolution #521 #518]: #547
5.327 [unit-resolution #519 #522]: false
5.328 unsat
5.329 -PaSeDRf7Set5ywlblDOoTg 673 0
5.330 +bf36938883aa38907d4d00c1860a1d18e7b620d0 86 0
5.331 +#2 := false
5.332 +decl uf_1 :: int
5.333 +#5 := uf_1
5.334 +#7 := 2::int
5.335 +#29 := (* 2::int uf_1)
5.336 +#4 := 0::int
5.337 +#54 := (= 0::int #29)
5.338 +#55 := (not #54)
5.339 +#61 := (= #29 0::int)
5.340 +#104 := (not #61)
5.341 +#110 := (iff #104 #55)
5.342 +#108 := (iff #61 #54)
5.343 +#109 := [commutativity]: #108
5.344 +#111 := [monotonicity #109]: #110
5.345 +#62 := (<= #29 0::int)
5.346 +#100 := (not #62)
5.347 +#30 := (<= uf_1 0::int)
5.348 +#31 := (not #30)
5.349 +#6 := (< 0::int uf_1)
5.350 +#32 := (iff #6 #31)
5.351 +#33 := [rewrite]: #32
5.352 +#27 := [asserted]: #6
5.353 +#34 := [mp #27 #33]: #31
5.354 +#101 := (or #100 #30)
5.355 +#102 := [th-lemma]: #101
5.356 +#103 := [unit-resolution #102 #34]: #100
5.357 +#105 := (or #104 #62)
5.358 +#106 := [th-lemma]: #105
5.359 +#107 := [unit-resolution #106 #103]: #104
5.360 +#112 := [mp #107 #111]: #55
5.361 +#56 := (= uf_1 #29)
5.362 +#57 := (not #56)
5.363 +#53 := (= 0::int uf_1)
5.364 +#50 := (not #53)
5.365 +#58 := (and #50 #55 #57)
5.366 +#69 := (not #58)
5.367 +#42 := (distinct 0::int uf_1 #29)
5.368 +#47 := (not #42)
5.369 +#9 := (- uf_1 uf_1)
5.370 +#8 := (* uf_1 2::int)
5.371 +#10 := (distinct uf_1 #8 #9)
5.372 +#11 := (not #10)
5.373 +#48 := (iff #11 #47)
5.374 +#45 := (iff #10 #42)
5.375 +#39 := (distinct uf_1 #29 0::int)
5.376 +#43 := (iff #39 #42)
5.377 +#44 := [rewrite]: #43
5.378 +#40 := (iff #10 #39)
5.379 +#37 := (= #9 0::int)
5.380 +#38 := [rewrite]: #37
5.381 +#35 := (= #8 #29)
5.382 +#36 := [rewrite]: #35
5.383 +#41 := [monotonicity #36 #38]: #40
5.384 +#46 := [trans #41 #44]: #45
5.385 +#49 := [monotonicity #46]: #48
5.386 +#28 := [asserted]: #11
5.387 +#52 := [mp #28 #49]: #47
5.388 +#80 := (or #42 #69)
5.389 +#81 := [def-axiom]: #80
5.390 +#82 := [unit-resolution #81 #52]: #69
5.391 +#59 := (= uf_1 0::int)
5.392 +#83 := (not #59)
5.393 +#89 := (iff #83 #50)
5.394 +#87 := (iff #59 #53)
5.395 +#88 := [commutativity]: #87
5.396 +#90 := [monotonicity #88]: #89
5.397 +#84 := (or #83 #30)
5.398 +#85 := [th-lemma]: #84
5.399 +#86 := [unit-resolution #85 #34]: #83
5.400 +#91 := [mp #86 #90]: #50
5.401 +#64 := -1::int
5.402 +#65 := (* -1::int #29)
5.403 +#66 := (+ uf_1 #65)
5.404 +#68 := (>= #66 0::int)
5.405 +#92 := (not #68)
5.406 +#93 := (or #92 #30)
5.407 +#94 := [th-lemma]: #93
5.408 +#95 := [unit-resolution #94 #34]: #92
5.409 +#96 := (or #57 #68)
5.410 +#97 := [th-lemma]: #96
5.411 +#98 := [unit-resolution #97 #95]: #57
5.412 +#76 := (or #58 #53 #54 #56)
5.413 +#77 := [def-axiom]: #76
5.414 +#99 := [unit-resolution #77 #98 #91 #82]: #54
5.415 +[unit-resolution #99 #112]: false
5.416 +unsat
5.417 +9791139ea2cfda88ae799477fc61e411aab42b18 673 0
5.418 #2 := false
5.419 #169 := 0::int
5.420 decl uf_2 :: int
5.421 @@ -4302,7 +4302,7 @@
5.422 #410 := [mp #349 #409]: #405
5.423 [unit-resolution #410 #710 #709 #697 #706]: false
5.424 unsat
5.425 -U7jSPEM53XYq3qs03aUczw 2291 0
5.426 +0d07e457c5602ba4a5dc70af32b6dc53a80a858c 2291 0
5.427 #2 := false
5.428 #6 := 0::int
5.429 decl z3name!0 :: int
5.430 @@ -6594,7 +6594,7 @@
5.431 #2323 := [unit-resolution #918 #2322]: #100
5.432 [unit-resolution #917 #2323 #2318]: false
5.433 unsat
5.434 -eqE7IAqFr0UIBuUsVDgHvw 52 0
5.435 +258b6cd4609a61b7800235c7f356739cfb8996c5 52 0
5.436 #2 := false
5.437 #8 := 1::real
5.438 decl uf_1 :: real
5.439 @@ -6647,7 +6647,7 @@
5.440 #29 := [asserted]: #13
5.441 [mp #29 #65]: false
5.442 unsat
5.443 -ADs4ZPiuUr7Xu7tk71NnEw 59 0
5.444 +3d1d0473f97c11d6c4d10f6e0313b2e2f4aac879 59 0
5.445 #2 := false
5.446 #55 := 0::int
5.447 #7 := 2::int
5.448 @@ -6707,7 +6707,7 @@
5.449 #144 := [unit-resolution #143 #28]: #58
5.450 [unit-resolution #144 #68]: false
5.451 unsat
5.452 -x2NmsblNl28xPXP2EG22rA 54 0
5.453 +f768cbe713eb8031e45b1a78d0f49a07f5398eb8 54 0
5.454 #2 := false
5.455 #5 := 2::int
5.456 decl uf_1 :: int
5.457 @@ -6762,7 +6762,7 @@
5.458 #139 := [unit-resolution #138 #27]: #127
5.459 [unit-resolution #139 #62]: false
5.460 unsat
5.461 -kfLiOGBz3RZx9wt+FS+hfg 118 0
5.462 +2c2bcacfbe018175dd39ce04dd5cbe02c800a0dd 118 0
5.463 #2 := false
5.464 #5 := 0::real
5.465 decl uf_1 :: real
5.466 @@ -6881,7 +6881,7 @@
5.467 #126 := [mp #101 #125]: #115
5.468 [unit-resolution #126 #132 #129]: false
5.469 unsat
5.470 -FPTJq9aN3ES4iIrHgaTv+A 208 0
5.471 +c8ed8eae868ac61c8f3a616f1b0b1df4032f4eac 208 0
5.472 #2 := false
5.473 #9 := 0::int
5.474 #11 := 4::int
5.475 @@ -7090,7 +7090,7 @@
5.476 #418 := [unit-resolution #417 #36]: #298
5.477 [th-lemma #418 #415 #412 #411 #99 #400 #397 #396]: false
5.478 unsat
5.479 -yN0aj3KferzvOSp2KlyNwg 24 0
5.480 +7beaddc803d2c23197634dc63d56d564292d85fe 24 0
5.481 #2 := false
5.482 #4 := (exists (vars (?x1 int)) false)
5.483 #5 := (not #4)
5.484 @@ -7115,7 +7115,7 @@
5.485 #22 := [asserted]: #6
5.486 [mp #22 #38]: false
5.487 unsat
5.488 -7iMPasu6AIeHm45slLCByA 24 0
5.489 +723fcd1ecb9fa59a7e0fede642f23063fb499818 24 0
5.490 #2 := false
5.491 #4 := (exists (vars (?x1 real)) false)
5.492 #5 := (not #4)
5.493 @@ -7140,13 +7140,13 @@
5.494 #22 := [asserted]: #6
5.495 [mp #22 #38]: false
5.496 unsat
5.497 -cv2pC2I0gIUYtVwtXngvXg 1 0
5.498 -unsat
5.499 -4r8/IxBBDH1ZqF0YfzLLTg 1 0
5.500 -unsat
5.501 -uj7n+C4nG462DNJy9Divrg 1 0
5.502 -unsat
5.503 -dn/LVwy1BXEOmtqdUBNhLw 73 0
5.504 +a72d0e977596e1fac0cccee600f0bf9d29ed71aa 1 0
5.505 +unsat
5.506 +70141a690f46561f859d3deed80b9611816f9f81 1 0
5.507 +unsat
5.508 +41b6ddffa2c7efc9285d0e0a65d74c4325ef6ddb 1 0
5.509 +unsat
5.510 +a08fcdd29520930b0a940df57c3d8266dbefd10f 73 0
5.511 #2 := false
5.512 #5 := 0::int
5.513 #8 := 1::int
5.514 @@ -7220,7 +7220,7 @@
5.515 #144 := [trans #142 #82]: #143
5.516 [mp #144 #146]: false
5.517 unsat
5.518 -VzZ1W5SEEis1AJp1qZz86g 82 0
5.519 +470993954e986ab72716000fd7da9fa600b05225 82 0
5.520 #2 := false
5.521 #5 := (:var 0 int)
5.522 #7 := 0::int
5.523 @@ -7303,7 +7303,7 @@
5.524 #30 := [asserted]: #14
5.525 [mp #30 #96]: false
5.526 unsat
5.527 -UoXgZh5LkmyNCmQEfEtnig 78 0
5.528 +40c93af1a084932780f95bda03b3df7712e01201 78 0
5.529 #2 := false
5.530 #5 := (:var 0 int)
5.531 #7 := 2::int
5.532 @@ -7382,7 +7382,7 @@
5.533 #31 := [asserted]: #15
5.534 [mp #31 #92]: false
5.535 unsat
5.536 -Qv4gVhCmOzC39uufV9ZpDA 61 0
5.537 +26b175ea54cef59293a917c6fb083751b00d312a 61 0
5.538 #2 := false
5.539 #9 := (:var 0 int)
5.540 #4 := 2::int
5.541 @@ -7444,7 +7444,7 @@
5.542 #30 := [asserted]: #14
5.543 [mp #30 #75]: false
5.544 unsat
5.545 -+j+tSj7aUImWej2XcTL9dw 111 0
5.546 +74037c10b4f126275ba21e7140b7f1e159b39ed9 111 0
5.547 #2 := false
5.548 #4 := 2::int
5.549 decl ?x1!1 :: int
5.550 @@ -7556,7 +7556,7 @@
5.551 #184 := [th-lemma]: #183
5.552 [unit-resolution #184 #127 #125 #126]: false
5.553 unsat
5.554 -kQRsBd9oowc7exsvsEgTUg 89 0
5.555 +628c1b88ca8fb09c896ae05059a52dc2f8e25db2 89 0
5.556 #2 := false
5.557 #4 := 0::int
5.558 decl ?x1!0 :: int
5.559 @@ -7646,7 +7646,7 @@
5.560 #167 := [unit-resolution #154 #90]: #166
5.561 [unit-resolution #167 #165 #162]: false
5.562 unsat
5.563 -VPjD8BtzPcTZKIRT4SA3Nw 83 2
5.564 +b7c4f9440c4594c46eee14ce57f17610bb7e2536 83 2
5.565 #2 := false
5.566 #5 := 0::int
5.567 #4 := (:var 0 int)
5.568 @@ -7732,7 +7732,7 @@
5.569 unsat
5.570 WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
5.571
5.572 -DCV5zpDW3cC2A61VghqFkA 180 2
5.573 +7a9cc3ee85422788d981af84d181bd61d65f774c 180 2
5.574 #2 := false
5.575 #4 := 0::int
5.576 #5 := (:var 0 int)
5.577 @@ -7915,7 +7915,7 @@
5.578 unsat
5.579 WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
5.580
5.581 -lYXJpXHB9nLXJbOsr9VH1w 68 0
5.582 +5201b12abd6b3d0f247a34c1fd9f443fc951c55f 68 0
5.583 #2 := false
5.584 #12 := 1::int
5.585 #9 := (:var 1 int)
5.586 @@ -7984,7 +7984,7 @@
5.587 #32 := [asserted]: #16
5.588 [mp #32 #83]: false
5.589 unsat
5.590 -jNvpOd8qnh73F8B6mQDrRw 107 0
5.591 +0f9091dc6853772b5280c29fc11ae1382022f24d 107 0
5.592 #2 := false
5.593 #4 := 0::int
5.594 decl ?x2!1 :: int
5.595 @@ -8092,7 +8092,7 @@
5.596 #123 := [and-elim #101]: #88
5.597 [th-lemma #123 #124 #125]: false
5.598 unsat
5.599 -QWWPBUGjgvTCpxqJ9oPGdQ 117 0
5.600 +a19e2cec45cb985989328595a0e06836a1e0fbc3 117 0
5.601 #2 := false
5.602 #4 := 0::int
5.603 decl ?x2!1 :: int
5.604 @@ -8210,7 +8210,7 @@
5.605 #188 := [unit-resolution #187 #110]: #98
5.606 [unit-resolution #188 #130]: false
5.607 unsat
5.608 -3r4MsKEvDJc1RWnNRxu/3Q 148 0
5.609 +34bf666106f50c4ee2e8834de4912d59c6e7d9d9 148 0
5.610 #2 := false
5.611 #144 := (not false)
5.612 #7 := 0::int
5.613 @@ -8359,7 +8359,7 @@
5.614 #158 := [mp #126 #157]: #153
5.615 [mp #158 #181]: false
5.616 unsat
5.617 -Q+cnHyqIFLGWsSlQkp3fEg 67 0
5.618 +1d6946d9384f22b76e98f04aff657c54e4fe51ad 67 0
5.619 #2 := false
5.620 #4 := (:var 0 int)
5.621 #5 := (pattern #4)
5.622 @@ -8427,9 +8427,9 @@
5.623 #30 := [asserted]: #14
5.624 [mp #30 #80]: false
5.625 unsat
5.626 -Q7HDzu4ER2dw+lHHM6YgFg 1 0
5.627 -unsat
5.628 -saejIG5KeeVxOolEIo3gtw 75 0
5.629 +d938f8b556e86b20a82e4661e3a61bad7d95357d 1 0
5.630 +unsat
5.631 +dfca84a72c9a54145743ea34eaa7c75e8665fd45 75 0
5.632 #2 := false
5.633 #6 := 1::int
5.634 decl uf_3 :: int
5.635 @@ -8505,7 +8505,7 @@
5.636 #32 := [asserted]: #16
5.637 [mp #32 #86]: false
5.638 unsat
5.639 -PPaoU5CzQFYr3LRpOsGPhQ 62 0
5.640 +2662a556257bfe403cd3fda75e9fe55964bc9dcd 62 0
5.641 #2 := false
5.642 decl uf_2 :: real
5.643 #6 := uf_2
5.644 @@ -8568,7 +8568,7 @@
5.645 #32 := [asserted]: #16
5.646 [mp #32 #74]: false
5.647 unsat
5.648 -hXKzem5+KYZMOj+GKxjszQ 141 0
5.649 +99d65e323e3d85dbdc2d8c52c169db4d46ead198 141 0
5.650 #2 := false
5.651 decl uf_4 :: int
5.652 #9 := uf_4
5.653 @@ -8710,7 +8710,7 @@
5.654 #45 := [asserted]: #29
5.655 [mp #45 #150]: false
5.656 unsat
5.657 -3D8WhjZTO7T824d7mwXcCA 252 0
5.658 +2e721ab2035f9845f1e87e78db6dfc67c28f6d40 252 0
5.659 #2 := false
5.660 #9 := 0::int
5.661 decl uf_2 :: (-> T1 int)
5.662 @@ -8963,7 +8963,7 @@
5.663 #539 := [unit-resolution #532 #451]: #557
5.664 [th-lemma #455 #539 #537 #546]: false
5.665 unsat
5.666 -kyphS4o71h68g2YhvYbQQQ 223 0
5.667 +5d4787d5f6bf7b62bda1a48bdd01dc6863801852 223 0
5.668 #2 := false
5.669 #23 := 3::int
5.670 decl uf_2 :: (-> T1 int)
5.671 @@ -9187,7 +9187,7 @@
5.672 #598 := [unit-resolution #593 #596]: #623
5.673 [th-lemma #152 #598 #139]: false
5.674 unsat
5.675 -M8P5WxpiY5AWxaJDBtXoLQ 367 0
5.676 +60689c41168db239dbf5f3a98d5f2bce0fef9e02 367 0
5.677 #2 := false
5.678 #9 := 0::int
5.679 decl uf_2 :: (-> T1 int)
5.680 @@ -9555,7 +9555,7 @@
5.681 #456 := [th-lemma]: #455
5.682 [unit-resolution #456 #464 #452]: false
5.683 unsat
5.684 -Xs4JZCKb5egkcPabsrodXg 302 0
5.685 +94b7ba760bb9dd467688fc28632e0ae8f6f51951 302 0
5.686 #2 := false
5.687 #9 := 0::int
5.688 decl uf_2 :: (-> T1 int)
5.689 @@ -9858,7 +9858,7 @@
5.690 #601 := [unit-resolution #615 #613]: #683
5.691 [th-lemma #623 #188 #601 #628]: false
5.692 unsat
5.693 -clMAi2WqMi360EjFURRGLg 458 0
5.694 +8d2fca14b1477934a0c7f4f6528bd3be029bba7b 458 0
5.695 #2 := false
5.696 #9 := 0::int
5.697 decl uf_2 :: (-> T1 int)
5.698 @@ -10317,7 +10317,7 @@
5.699 #350 := [unit-resolution #369 #367]: #368
5.700 [unit-resolution #350 #323]: false
5.701 unsat
5.702 -mu7O1os0t3tPqWZhwizjxw 161 0
5.703 +720080123967f7b12d5ac9ba2a5e5203400a16cd 161 0
5.704 #2 := false
5.705 #9 := 0::int
5.706 decl uf_3 :: int
5.707 @@ -10479,7 +10479,7 @@
5.708 #361 := [unit-resolution #639 #655]: #647
5.709 [th-lemma #656 #361 #261]: false
5.710 unsat
5.711 -08cmOtIT4NYs2PG/F3zeZw 557 0
5.712 +980ba021fe0853c3aa46377383e3f0f6fa9e2888 557 0
5.713 #2 := false
5.714 #9 := 0::int
5.715 decl uf_2 :: (-> T1 int)
5.716 @@ -11037,57 +11037,57 @@
5.717 #990 := [unit-resolution #501 #807]: #511
5.718 [unit-resolution #990 #989 #979]: false
5.719 unsat
5.720 -8HdmSMHHP2B8XMFzjNuw5Q 1 0
5.721 -unsat
5.722 -O4aM0+/isn2q5CrIefZjzg 1 0
5.723 -unsat
5.724 -t/ni9djl2DqxH0iKupZSwg 1 0
5.725 -unsat
5.726 -RumBGekdxZQaBF1HNa3x9w 1 0
5.727 -unsat
5.728 -Q9d+IbQ8chjKld71X6/zqw 1 0
5.729 -unsat
5.730 -PhC8zQV8hnJ6E2YYjZPGjQ 1 0
5.731 -unsat
5.732 -mieI2RhSp3bYaojlWH1A4A 1 0
5.733 -unsat
5.734 -pRSV6nBLconzrQz2zUrJ6g 1 0
5.735 -unsat
5.736 -Js0JfdwDoKq3YuilPPgeZw 1 0
5.737 -unsat
5.738 -GRIqjLUJiqXbo+pXhAeKIw 1 0
5.739 -unsat
5.740 -Bg5scsmPFp82+7Y2ScL6Wg 1 0
5.741 -unsat
5.742 -XD6zX6850dLxyfZSfNv30A 1 0
5.743 -unsat
5.744 -BG/HwJYnumvDICXxtBu/tA 1 0
5.745 -unsat
5.746 -YMc4t19sUMWbUkx3woxCmQ 1 0
5.747 -unsat
5.748 -YyD9IF72pKXGGKZTO7FY5Q 1 0
5.749 -unsat
5.750 -zRPsIUi+TEoz5fPWP0H9bQ 1 0
5.751 -unsat
5.752 -8ipTE8BOXpvSo/U6D4p3lA 1 0
5.753 -unsat
5.754 -MSzQywedZPsOE0CDxrrO0g 1 0
5.755 -unsat
5.756 -SryZuXv48ItET8NPIv07pA 1 0
5.757 -unsat
5.758 -qOMUQN18hYFl/wWt54lvbA 1 0
5.759 -unsat
5.760 -+njWXdn6fETK3/AjtiHjcA 1 0
5.761 -unsat
5.762 -5cQ7gJ33gzYTIIPA3hbBmQ 1 0
5.763 -unsat
5.764 -ZznT34cvumrP00mXZ3gcjw 1 0
5.765 -unsat
5.766 -//LQca1Et5RfhQJZA+CGCA 1 0
5.767 -unsat
5.768 -3ntxKz+kaQNfTrLzY9sVXw 1 0
5.769 -unsat
5.770 -4lL2Qo8ngE1EH1UdeN1Qng 43 0
5.771 +22877b17eafaba69b1f8a961a616fea28ae70d56 1 0
5.772 +unsat
5.773 +b5839159097bbd4e601a5681d1ca3493ec994a7c 1 0
5.774 +unsat
5.775 +90e1074350b5dcaae149781bcaa5d643b2ca9f48 1 0
5.776 +unsat
5.777 +08c7117fe974f5767051ed5aa61a27ce3084eb1d 1 0
5.778 +unsat
5.779 +858012417c9d327d8997f2a5dcb3da095ec65d34 1 0
5.780 +unsat
5.781 +84b2eee4890eaadb3638c7e522fb3237b3d476b0 1 0
5.782 +unsat
5.783 +8867717d9736308a2c27df0665a6e391b0562076 1 0
5.784 +unsat
5.785 +cd79c9a0488ab597d08dd9a0d6ac0f3647003bd6 1 0
5.786 +unsat
5.787 +395dd6c10b2a432137f9e3401cba8ec4dd64911b 1 0
5.788 +unsat
5.789 +17e3cc9534e04d86f095ec1a92c77d46d7dbb8e5 1 0
5.790 +unsat
5.791 +e046ea79beacf4bc3567b3b7f755232369d0c185 1 0
5.792 +unsat
5.793 +8ce4235464829d4be72e682f0c72bc5e3c6902d0 1 0
5.794 +unsat
5.795 +656a40b977d7716264443900d6bdb4d3d117d52f 1 0
5.796 +unsat
5.797 +ec27a57e58719625ff71dd4d68ed53a3851efb5c 1 0
5.798 +unsat
5.799 +2c3c366b8488ca0991cc767c94cdb78b18db9d5f 1 0
5.800 +unsat
5.801 +5894f6f19250b12885e38f54eae81f143b58fa01 1 0
5.802 +unsat
5.803 +e150815d9eb1ec168805b5501d7f4b2e378dd883 1 0
5.804 +unsat
5.805 +396d6254e993f414335de9378150e486d3cfcd4e 1 0
5.806 +unsat
5.807 +96014c61f582a811aff25ad7fa62b575b830fa8b 1 0
5.808 +unsat
5.809 +10580b87c0d062c9854e79d16047a53d045ccfac 1 0
5.810 +unsat
5.811 +87b5f388df1f43cc02ac0fa0d6944eb8cd8f8f50 1 0
5.812 +unsat
5.813 +92a5e2bb68f74b9e7dd3a9ef79ea641e9700d563 1 0
5.814 +unsat
5.815 +152e0f0f0a04b399b057beae92ae0455408b224f 1 0
5.816 +unsat
5.817 +41925af4711748a6e411453f2465920a1c6ffb8e 1 0
5.818 +unsat
5.819 +757462716f4a2619a1410bdca3faa2d058042c10 1 0
5.820 +unsat
5.821 +abdeeb4668a63f19473d6da94232379344d99fea 43 0
5.822 #2 := false
5.823 #6 := 0::int
5.824 decl uf_1 :: (-> bv[2] int)
5.825 @@ -11131,9 +11131,9 @@
5.826 #287 := [th-lemma]: #627
5.827 [unit-resolution #287 #47 #635]: false
5.828 unsat
5.829 -+xe3O927LrflFUE6NDqRlA 1 0
5.830 -unsat
5.831 -JPoL7fPYhqhAkjUiVF+THQ 50 0
5.832 +2e4bd6e1ab7bfedbefd3ada8caf5332ba5651065 1 0
5.833 +unsat
5.834 +96d2e1aad559535e781a07ee5e55bb19caef769c 50 0
5.835 #2 := false
5.836 decl uf_6 :: T2
5.837 #23 := uf_6
5.838 @@ -11184,7 +11184,7 @@
5.839 #66 := [asserted]: #26
5.840 [unit-resolution #66 #235]: false
5.841 unsat
5.842 -l23ZDmd0VbO/Q+uO5EtabA 105 0
5.843 +008ad82b0a62ff600e66e8f2cc72b5795c7c5032 105 0
5.844 #2 := false
5.845 decl uf_6 :: (-> T4 T2)
5.846 decl uf_10 :: T4
5.847 @@ -11290,7 +11290,7 @@
5.848 #110 := [asserted]: #46
5.849 [unit-resolution #110 #238]: false
5.850 unsat
5.851 -GZjffeZPQnL3OyLCvxdCpg 181 0
5.852 +0a15a60660bc0c3f06688ad5de50ed50a24d0df0 181 0
5.853 #2 := false
5.854 decl uf_1 :: (-> T1 T2 T3)
5.855 decl uf_3 :: T2
5.856 @@ -11472,7 +11472,7 @@
5.857 #76 := [asserted]: #38
5.858 [unit-resolution #76 #489]: false
5.859 unsat
5.860 -i6jCzzRosHYE0w7sF1Nraw 62 0
5.861 +dde2364f13fc9ce8af00c7a02bfea9a6c979a805 62 0
5.862 #2 := false
5.863 decl up_4 :: (-> T1 T2 bool)
5.864 decl uf_3 :: T2
5.865 @@ -11535,7 +11535,7 @@
5.866 #73 := [unit-resolution #71 #68]: #72
5.867 [unit-resolution #73 #59 #61]: false
5.868 unsat
5.869 -YZHSyhN2TGlpe+vpkzWrgQ 115 0
5.870 +3cb6787c7063b0a04bff9e2bfa4203b73903dabe 115 0
5.871 #2 := false
5.872 decl up_2 :: (-> T2 bool)
5.873 decl uf_3 :: T2
5.874 @@ -11651,7 +11651,7 @@
5.875 #560 := [mp #344 #559]: #557
5.876 [unit-resolution #560 #576 #561]: false
5.877 unsat
5.878 -TibRlXkU+X+1+zGPYTiT0g 464 0
5.879 +dcb635ada6f2482ea11de30713fe962bcb57c9ad 464 0
5.880 #2 := false
5.881 decl uf_2 :: (-> T2 T3 T3)
5.882 decl uf_4 :: T3
5.883 @@ -12116,7 +12116,7 @@
5.884 #177 := [asserted]: #53
5.885 [unit-resolution #177 #793]: false
5.886 unsat
5.887 -DJPKxi9AO25zGBcs5kxUrw 21 0
5.888 +ca467a37d809de06757809cab1cd30e08586674f 21 0
5.889 #2 := false
5.890 decl up_1 :: (-> T1 bool)
5.891 #4 := (:var 0 T1)
5.892 @@ -12138,7 +12138,7 @@
5.893 #25 := [asserted]: #9
5.894 [mp #25 #34]: false
5.895 unsat
5.896 -i5PnMbuM9mWv5LnVszz9+g 366 0
5.897 +f6e9645ebbb8739d12b8e96bc83ddef33c7d53bc 366 0
5.898 #2 := false
5.899 decl uf_1 :: (-> int T1)
5.900 #37 := 6::int
5.901 @@ -12505,7 +12505,7 @@
5.902 #182 := [asserted]: #40
5.903 [unit-resolution #182 #399]: false
5.904 unsat
5.905 -K2SXMHU6QCZJ8TRs6zjKRg 408 0
5.906 +b15b527236338a437e355afcde07dd3c6dfc451f 408 0
5.907 #2 := false
5.908 #22 := 0::int
5.909 #8 := 2::int
5.910 @@ -12914,7 +12914,7 @@
5.911 #375 := [unit-resolution #374 #407]: #708
5.912 [th-lemma #375 #370 #465]: false
5.913 unsat
5.914 -1DhSL9G2fGRGmuI8IaMNOA 50 0
5.915 +71b79533f46a8514b2fc189fc382867d50f52a9a 50 0
5.916 #2 := false
5.917 decl up_35 :: (-> int bool)
5.918 #112 := 1::int
5.919 @@ -12965,7 +12965,7 @@
5.920 #504 := [quant-inst]: #503
5.921 [unit-resolution #504 #916 #297]: false
5.922 unsat
5.923 -dyXROdcPFSd36N3K7dpmDw 506 0
5.924 +e40ba7aed8ae5409337a331038da0587c03354d6 506 0
5.925 #2 := false
5.926 decl uf_17 :: (-> T8 T3)
5.927 decl uf_18 :: (-> T1 T8)