# HG changeset patch # User boehmes # Date 1269436087 -3600 # Node ID 7a86d7706106026782e31473a98372d9e22be627 # Parent fcd02244e63d018b8584635cf5957dc511dd1719 updated SMT certificates diff -r fcd02244e63d -r 7a86d7706106 src/HOL/Boogie/Examples/Boogie_Dijkstra.certs --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Wed Mar 24 14:03:52 2010 +0100 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Wed Mar 24 14:08:07 2010 +0100 @@ -1,4 +1,4 @@ -JinTdmjIiorL0/vvOyf3+w 6542 0 +6164a2366a9e57e212b8ac4aa01e3c8bcc1ea8e0 6542 0 #2 := false decl up_6 :: (-> T4 T2 bool) decl ?x47!7 :: (-> T2 T2) diff -r fcd02244e63d -r 7a86d7706106 src/HOL/Boogie/Examples/Boogie_Max.certs --- a/src/HOL/Boogie/Examples/Boogie_Max.certs Wed Mar 24 14:03:52 2010 +0100 +++ b/src/HOL/Boogie/Examples/Boogie_Max.certs Wed Mar 24 14:08:07 2010 +0100 @@ -1,4 +1,4 @@ -iks4GfP7O/NgNFyGZ4ynjQ 2224 0 +cdfef9f27f2a4ba9648f86890c8563d0a1cfe888 2224 0 #2 := false #4 := 0::int decl uf_3 :: (-> int int) diff -r fcd02244e63d -r 7a86d7706106 src/HOL/Boogie/Examples/VCC_Max.certs --- a/src/HOL/Boogie/Examples/VCC_Max.certs Wed Mar 24 14:03:52 2010 +0100 +++ b/src/HOL/Boogie/Examples/VCC_Max.certs Wed Mar 24 14:08:07 2010 +0100 @@ -1,4 +1,4 @@ -6Q8QWdFv463DpfVfkr0XnA 7790 0 +b95bf7adc1e2b959cf13db317b64554768249b2e 7790 0 #2 := false decl uf_110 :: (-> T4 T5 int) decl uf_66 :: (-> T5 int T3 T5) diff -r fcd02244e63d -r 7a86d7706106 src/HOL/Multivariate_Analysis/Integration.cert --- a/src/HOL/Multivariate_Analysis/Integration.cert Wed Mar 24 14:03:52 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.cert Wed Mar 24 14:08:07 2010 +0100 @@ -1,4 +1,853 @@ -tB2Atlor9W4pSnrAz5nHpw 907 0 +534d3afbd3505abffa6b03e3986bfa7aa3cff358 428 0 +#2 := false +decl uf_10 :: T1 +#38 := uf_10 +decl uf_3 :: T1 +#21 := uf_3 +#45 := (= uf_3 uf_10) +decl uf_1 :: (-> int T1) +decl uf_2 :: (-> T1 int) +#39 := (uf_2 uf_10) +#588 := (uf_1 #39) +#686 := (= #588 uf_10) +#589 := (= uf_10 #588) +#4 := (:var 0 T1) +#5 := (uf_2 #4) +#541 := (pattern #5) +#6 := (uf_1 #5) +#93 := (= #4 #6) +#542 := (forall (vars (?x1 T1)) (:pat #541) #93) +#96 := (forall (vars (?x1 T1)) #93) +#545 := (iff #96 #542) +#543 := (iff #93 #93) +#544 := [refl]: #543 +#546 := [quant-intro #544]: #545 +#454 := (~ #96 #96) +#456 := (~ #93 #93) +#457 := [refl]: #456 +#455 := [nnf-pos #457]: #454 +#7 := (= #6 #4) +#8 := (forall (vars (?x1 T1)) #7) +#97 := (iff #8 #96) +#94 := (iff #7 #93) +#95 := [rewrite]: #94 +#98 := [quant-intro #95]: #97 +#92 := [asserted]: #8 +#101 := [mp #92 #98]: #96 +#452 := [mp~ #101 #455]: #96 +#547 := [mp #452 #546]: #542 +#590 := (not #542) +#595 := (or #590 #589) +#596 := [quant-inst]: #595 +#680 := [unit-resolution #596 #547]: #589 +#687 := [symm #680]: #686 +#688 := (= uf_3 #588) +#22 := (uf_2 uf_3) +#586 := (uf_1 #22) +#684 := (= #586 #588) +#682 := (= #588 #586) +#678 := (= #39 #22) +#676 := (= #22 #39) +#9 := 0::int +#227 := -1::int +#230 := (* -1::int #39) +#231 := (+ #22 #230) +#296 := (<= #231 0::int) +#70 := (<= #22 #39) +#393 := (iff #70 #296) +#394 := [rewrite]: #393 +#347 := [asserted]: #70 +#395 := [mp #347 #394]: #296 +#229 := (>= #231 0::int) +decl uf_4 :: (-> T2 T3 real) +decl uf_6 :: (-> T1 T3) +#25 := (uf_6 uf_3) +decl uf_7 :: T2 +#27 := uf_7 +#28 := (uf_4 uf_7 #25) +decl uf_9 :: T2 +#33 := uf_9 +#34 := (uf_4 uf_9 #25) +#46 := (uf_6 uf_10) +decl uf_5 :: T2 +#24 := uf_5 +#47 := (uf_4 uf_5 #46) +#48 := (ite #45 #47 #34) +#256 := (ite #229 #48 #28) +#568 := (= #28 #256) +#648 := (not #568) +#194 := 0::real +#192 := -1::real +#265 := (* -1::real #256) +#640 := (+ #28 #265) +#642 := (>= #640 0::real) +#645 := (not #642) +#643 := [hypothesis]: #642 +decl uf_8 :: T2 +#30 := uf_8 +#31 := (uf_4 uf_8 #25) +#266 := (+ #31 #265) +#264 := (>= #266 0::real) +#267 := (not #264) +#26 := (uf_4 uf_5 #25) +decl uf_11 :: T2 +#41 := uf_11 +#42 := (uf_4 uf_11 #25) +#237 := (ite #229 #42 #26) +#245 := (* -1::real #237) +#246 := (+ #31 #245) +#247 := (<= #246 0::real) +#248 := (not #247) +#272 := (and #248 #267) +#40 := (< #22 #39) +#49 := (ite #40 #28 #48) +#50 := (< #31 #49) +#43 := (ite #40 #26 #42) +#44 := (< #43 #31) +#51 := (and #44 #50) +#273 := (iff #51 #272) +#270 := (iff #50 #267) +#261 := (< #31 #256) +#268 := (iff #261 #267) +#269 := [rewrite]: #268 +#262 := (iff #50 #261) +#259 := (= #49 #256) +#228 := (not #229) +#253 := (ite #228 #28 #48) +#257 := (= #253 #256) +#258 := [rewrite]: #257 +#254 := (= #49 #253) +#232 := (iff #40 #228) +#233 := [rewrite]: #232 +#255 := [monotonicity #233]: #254 +#260 := [trans #255 #258]: #259 +#263 := [monotonicity #260]: #262 +#271 := [trans #263 #269]: #270 +#251 := (iff #44 #248) +#242 := (< #237 #31) +#249 := (iff #242 #248) +#250 := [rewrite]: #249 +#243 := (iff #44 #242) +#240 := (= #43 #237) +#234 := (ite #228 #26 #42) +#238 := (= #234 #237) +#239 := [rewrite]: #238 +#235 := (= #43 #234) +#236 := [monotonicity #233]: #235 +#241 := [trans #236 #239]: #240 +#244 := [monotonicity #241]: #243 +#252 := [trans #244 #250]: #251 +#274 := [monotonicity #252 #271]: #273 +#178 := [asserted]: #51 +#275 := [mp #178 #274]: #272 +#277 := [and-elim #275]: #267 +#196 := (* -1::real #31) +#197 := (+ #28 #196) +#195 := (>= #197 0::real) +#193 := (not #195) +#213 := (* -1::real #34) +#214 := (+ #31 #213) +#212 := (>= #214 0::real) +#215 := (not #212) +#220 := (and #193 #215) +#23 := (< #22 #22) +#35 := (ite #23 #28 #34) +#36 := (< #31 #35) +#29 := (ite #23 #26 #28) +#32 := (< #29 #31) +#37 := (and #32 #36) +#221 := (iff #37 #220) +#218 := (iff #36 #215) +#209 := (< #31 #34) +#216 := (iff #209 #215) +#217 := [rewrite]: #216 +#210 := (iff #36 #209) +#207 := (= #35 #34) +#202 := (ite false #28 #34) +#205 := (= #202 #34) +#206 := [rewrite]: #205 +#203 := (= #35 #202) +#180 := (iff #23 false) +#181 := [rewrite]: #180 +#204 := [monotonicity #181]: #203 +#208 := [trans #204 #206]: #207 +#211 := [monotonicity #208]: #210 +#219 := [trans #211 #217]: #218 +#200 := (iff #32 #193) +#189 := (< #28 #31) +#198 := (iff #189 #193) +#199 := [rewrite]: #198 +#190 := (iff #32 #189) +#187 := (= #29 #28) +#182 := (ite false #26 #28) +#185 := (= #182 #28) +#186 := [rewrite]: #185 +#183 := (= #29 #182) +#184 := [monotonicity #181]: #183 +#188 := [trans #184 #186]: #187 +#191 := [monotonicity #188]: #190 +#201 := [trans #191 #199]: #200 +#222 := [monotonicity #201 #219]: #221 +#177 := [asserted]: #37 +#223 := [mp #177 #222]: #220 +#224 := [and-elim #223]: #193 +#644 := [th-lemma #224 #277 #643]: false +#646 := [lemma #644]: #645 +#647 := [hypothesis]: #568 +#649 := (or #648 #642) +#650 := [th-lemma]: #649 +#651 := [unit-resolution #650 #647 #646]: false +#652 := [lemma #651]: #648 +#578 := (or #229 #568) +#579 := [def-axiom]: #578 +#675 := [unit-resolution #579 #652]: #229 +#677 := [th-lemma #675 #395]: #676 +#679 := [symm #677]: #678 +#683 := [monotonicity #679]: #682 +#685 := [symm #683]: #684 +#587 := (= uf_3 #586) +#591 := (or #590 #587) +#592 := [quant-inst]: #591 +#681 := [unit-resolution #592 #547]: #587 +#689 := [trans #681 #685]: #688 +#690 := [trans #689 #687]: #45 +#571 := (not #45) +#54 := (uf_4 uf_11 #46) +#279 := (ite #45 #28 #54) +#465 := (* -1::real #279) +#632 := (+ #28 #465) +#633 := (<= #632 0::real) +#580 := (= #28 #279) +#656 := [hypothesis]: #45 +#582 := (or #571 #580) +#583 := [def-axiom]: #582 +#657 := [unit-resolution #583 #656]: #580 +#658 := (not #580) +#659 := (or #658 #633) +#660 := [th-lemma]: #659 +#661 := [unit-resolution #660 #657]: #633 +#57 := (uf_4 uf_8 #46) +#363 := (* -1::real #57) +#379 := (+ #47 #363) +#380 := (<= #379 0::real) +#381 := (not #380) +#364 := (+ #54 #363) +#362 := (>= #364 0::real) +#361 := (not #362) +#386 := (and #361 #381) +#59 := (uf_4 uf_7 #46) +#64 := (< #39 #39) +#67 := (ite #64 #59 #47) +#68 := (< #57 #67) +#65 := (ite #64 #47 #54) +#66 := (< #65 #57) +#69 := (and #66 #68) +#387 := (iff #69 #386) +#384 := (iff #68 #381) +#376 := (< #57 #47) +#382 := (iff #376 #381) +#383 := [rewrite]: #382 +#377 := (iff #68 #376) +#374 := (= #67 #47) +#369 := (ite false #59 #47) +#372 := (= #369 #47) +#373 := [rewrite]: #372 +#370 := (= #67 #369) +#349 := (iff #64 false) +#350 := [rewrite]: #349 +#371 := [monotonicity #350]: #370 +#375 := [trans #371 #373]: #374 +#378 := [monotonicity #375]: #377 +#385 := [trans #378 #383]: #384 +#367 := (iff #66 #361) +#358 := (< #54 #57) +#365 := (iff #358 #361) +#366 := [rewrite]: #365 +#359 := (iff #66 #358) +#356 := (= #65 #54) +#351 := (ite false #47 #54) +#354 := (= #351 #54) +#355 := [rewrite]: #354 +#352 := (= #65 #351) +#353 := [monotonicity #350]: #352 +#357 := [trans #353 #355]: #356 +#360 := [monotonicity #357]: #359 +#368 := [trans #360 #366]: #367 +#388 := [monotonicity #368 #385]: #387 +#346 := [asserted]: #69 +#389 := [mp #346 #388]: #386 +#391 := [and-elim #389]: #381 +#397 := (* -1::real #59) +#398 := (+ #47 #397) +#399 := (<= #398 0::real) +#409 := (* -1::real #54) +#410 := (+ #47 #409) +#408 := (>= #410 0::real) +#60 := (uf_4 uf_9 #46) +#402 := (* -1::real #60) +#403 := (+ #59 #402) +#404 := (<= #403 0::real) +#418 := (and #399 #404 #408) +#73 := (<= #59 #60) +#72 := (<= #47 #59) +#74 := (and #72 #73) +#71 := (<= #54 #47) +#75 := (and #71 #74) +#421 := (iff #75 #418) +#412 := (and #399 #404) +#415 := (and #408 #412) +#419 := (iff #415 #418) +#420 := [rewrite]: #419 +#416 := (iff #75 #415) +#413 := (iff #74 #412) +#405 := (iff #73 #404) +#406 := [rewrite]: #405 +#400 := (iff #72 #399) +#401 := [rewrite]: #400 +#414 := [monotonicity #401 #406]: #413 +#407 := (iff #71 #408) +#411 := [rewrite]: #407 +#417 := [monotonicity #411 #414]: #416 +#422 := [trans #417 #420]: #421 +#348 := [asserted]: #75 +#423 := [mp #348 #422]: #418 +#424 := [and-elim #423]: #399 +#637 := (+ #28 #397) +#639 := (>= #637 0::real) +#636 := (= #28 #59) +#666 := (= #59 #28) +#664 := (= #46 #25) +#662 := (= #25 #46) +#663 := [monotonicity #656]: #662 +#665 := [symm #663]: #664 +#667 := [monotonicity #665]: #666 +#668 := [symm #667]: #636 +#669 := (not #636) +#670 := (or #669 #639) +#671 := [th-lemma]: #670 +#672 := [unit-resolution #671 #668]: #639 +#468 := (+ #57 #465) +#471 := (<= #468 0::real) +#444 := (not #471) +#322 := (ite #296 #279 #47) +#330 := (* -1::real #322) +#331 := (+ #57 #330) +#332 := (<= #331 0::real) +#333 := (not #332) +#445 := (iff #333 #444) +#472 := (iff #332 #471) +#469 := (= #331 #468) +#466 := (= #330 #465) +#463 := (= #322 #279) +#1 := true +#458 := (ite true #279 #47) +#461 := (= #458 #279) +#462 := [rewrite]: #461 +#459 := (= #322 #458) +#450 := (iff #296 true) +#451 := [iff-true #395]: #450 +#460 := [monotonicity #451]: #459 +#464 := [trans #460 #462]: #463 +#467 := [monotonicity #464]: #466 +#470 := [monotonicity #467]: #469 +#473 := [monotonicity #470]: #472 +#474 := [monotonicity #473]: #445 +#303 := (ite #296 #60 #59) +#313 := (* -1::real #303) +#314 := (+ #57 #313) +#312 := (>= #314 0::real) +#311 := (not #312) +#338 := (and #311 #333) +#52 := (< #39 #22) +#61 := (ite #52 #59 #60) +#62 := (< #57 #61) +#53 := (= uf_10 uf_3) +#55 := (ite #53 #28 #54) +#56 := (ite #52 #47 #55) +#58 := (< #56 #57) +#63 := (and #58 #62) +#341 := (iff #63 #338) +#282 := (ite #52 #47 #279) +#285 := (< #282 #57) +#291 := (and #62 #285) +#339 := (iff #291 #338) +#336 := (iff #285 #333) +#327 := (< #322 #57) +#334 := (iff #327 #333) +#335 := [rewrite]: #334 +#328 := (iff #285 #327) +#325 := (= #282 #322) +#297 := (not #296) +#319 := (ite #297 #47 #279) +#323 := (= #319 #322) +#324 := [rewrite]: #323 +#320 := (= #282 #319) +#298 := (iff #52 #297) +#299 := [rewrite]: #298 +#321 := [monotonicity #299]: #320 +#326 := [trans #321 #324]: #325 +#329 := [monotonicity #326]: #328 +#337 := [trans #329 #335]: #336 +#317 := (iff #62 #311) +#308 := (< #57 #303) +#315 := (iff #308 #311) +#316 := [rewrite]: #315 +#309 := (iff #62 #308) +#306 := (= #61 #303) +#300 := (ite #297 #59 #60) +#304 := (= #300 #303) +#305 := [rewrite]: #304 +#301 := (= #61 #300) +#302 := [monotonicity #299]: #301 +#307 := [trans #302 #305]: #306 +#310 := [monotonicity #307]: #309 +#318 := [trans #310 #316]: #317 +#340 := [monotonicity #318 #337]: #339 +#294 := (iff #63 #291) +#288 := (and #285 #62) +#292 := (iff #288 #291) +#293 := [rewrite]: #292 +#289 := (iff #63 #288) +#286 := (iff #58 #285) +#283 := (= #56 #282) +#280 := (= #55 #279) +#226 := (iff #53 #45) +#278 := [rewrite]: #226 +#281 := [monotonicity #278]: #280 +#284 := [monotonicity #281]: #283 +#287 := [monotonicity #284]: #286 +#290 := [monotonicity #287]: #289 +#295 := [trans #290 #293]: #294 +#342 := [trans #295 #340]: #341 +#179 := [asserted]: #63 +#343 := [mp #179 #342]: #338 +#345 := [and-elim #343]: #333 +#475 := [mp #345 #474]: #444 +#673 := [th-lemma #475 #672 #424 #391 #661]: false +#674 := [lemma #673]: #571 +[unit-resolution #674 #690]: false +unsat +985f86fd1ea01264c02b8076ffd658677bd4d29a 419 0 +#2 := false +#194 := 0::real +decl uf_4 :: (-> T2 T3 real) +decl uf_6 :: (-> T1 T3) +decl uf_3 :: T1 +#21 := uf_3 +#25 := (uf_6 uf_3) +decl uf_5 :: T2 +#24 := uf_5 +#26 := (uf_4 uf_5 #25) +decl uf_7 :: T2 +#27 := uf_7 +#28 := (uf_4 uf_7 #25) +decl uf_10 :: T1 +#38 := uf_10 +#42 := (uf_6 uf_10) +decl uf_9 :: T2 +#33 := uf_9 +#43 := (uf_4 uf_9 #42) +#41 := (= uf_3 uf_10) +#44 := (ite #41 #43 #28) +#9 := 0::int +decl uf_2 :: (-> T1 int) +#39 := (uf_2 uf_10) +#226 := -1::int +#229 := (* -1::int #39) +#22 := (uf_2 uf_3) +#230 := (+ #22 #229) +#228 := (>= #230 0::int) +#236 := (ite #228 #44 #26) +#192 := -1::real +#244 := (* -1::real #236) +#642 := (+ #26 #244) +#643 := (<= #642 0::real) +#567 := (= #26 #236) +#227 := (not #228) +decl uf_1 :: (-> int T1) +#593 := (uf_1 #39) +#660 := (= #593 uf_10) +#594 := (= uf_10 #593) +#4 := (:var 0 T1) +#5 := (uf_2 #4) +#546 := (pattern #5) +#6 := (uf_1 #5) +#93 := (= #4 #6) +#547 := (forall (vars (?x1 T1)) (:pat #546) #93) +#96 := (forall (vars (?x1 T1)) #93) +#550 := (iff #96 #547) +#548 := (iff #93 #93) +#549 := [refl]: #548 +#551 := [quant-intro #549]: #550 +#448 := (~ #96 #96) +#450 := (~ #93 #93) +#451 := [refl]: #450 +#449 := [nnf-pos #451]: #448 +#7 := (= #6 #4) +#8 := (forall (vars (?x1 T1)) #7) +#97 := (iff #8 #96) +#94 := (iff #7 #93) +#95 := [rewrite]: #94 +#98 := [quant-intro #95]: #97 +#92 := [asserted]: #8 +#101 := [mp #92 #98]: #96 +#446 := [mp~ #101 #449]: #96 +#552 := [mp #446 #551]: #547 +#595 := (not #547) +#600 := (or #595 #594) +#601 := [quant-inst]: #600 +#654 := [unit-resolution #601 #552]: #594 +#680 := [symm #654]: #660 +#681 := (= uf_3 #593) +#591 := (uf_1 #22) +#658 := (= #591 #593) +#656 := (= #593 #591) +#652 := (= #39 #22) +#647 := (= #22 #39) +#290 := (<= #230 0::int) +#70 := (<= #22 #39) +#388 := (iff #70 #290) +#389 := [rewrite]: #388 +#341 := [asserted]: #70 +#390 := [mp #341 #389]: #290 +#646 := [hypothesis]: #228 +#648 := [th-lemma #646 #390]: #647 +#653 := [symm #648]: #652 +#657 := [monotonicity #653]: #656 +#659 := [symm #657]: #658 +#592 := (= uf_3 #591) +#596 := (or #595 #592) +#597 := [quant-inst]: #596 +#655 := [unit-resolution #597 #552]: #592 +#682 := [trans #655 #659]: #681 +#683 := [trans #682 #680]: #41 +#570 := (not #41) +decl uf_11 :: T2 +#47 := uf_11 +#59 := (uf_4 uf_11 #42) +#278 := (ite #41 #26 #59) +#459 := (* -1::real #278) +#637 := (+ #26 #459) +#639 := (>= #637 0::real) +#585 := (= #26 #278) +#661 := [hypothesis]: #41 +#587 := (or #570 #585) +#588 := [def-axiom]: #587 +#662 := [unit-resolution #588 #661]: #585 +#663 := (not #585) +#664 := (or #663 #639) +#665 := [th-lemma]: #664 +#666 := [unit-resolution #665 #662]: #639 +decl uf_8 :: T2 +#30 := uf_8 +#56 := (uf_4 uf_8 #42) +#357 := (* -1::real #56) +#358 := (+ #43 #357) +#356 := (>= #358 0::real) +#355 := (not #356) +#374 := (* -1::real #59) +#375 := (+ #56 #374) +#373 := (>= #375 0::real) +#376 := (not #373) +#381 := (and #355 #376) +#64 := (< #39 #39) +#67 := (ite #64 #43 #59) +#68 := (< #56 #67) +#53 := (uf_4 uf_5 #42) +#65 := (ite #64 #53 #43) +#66 := (< #65 #56) +#69 := (and #66 #68) +#382 := (iff #69 #381) +#379 := (iff #68 #376) +#370 := (< #56 #59) +#377 := (iff #370 #376) +#378 := [rewrite]: #377 +#371 := (iff #68 #370) +#368 := (= #67 #59) +#363 := (ite false #43 #59) +#366 := (= #363 #59) +#367 := [rewrite]: #366 +#364 := (= #67 #363) +#343 := (iff #64 false) +#344 := [rewrite]: #343 +#365 := [monotonicity #344]: #364 +#369 := [trans #365 #367]: #368 +#372 := [monotonicity #369]: #371 +#380 := [trans #372 #378]: #379 +#361 := (iff #66 #355) +#352 := (< #43 #56) +#359 := (iff #352 #355) +#360 := [rewrite]: #359 +#353 := (iff #66 #352) +#350 := (= #65 #43) +#345 := (ite false #53 #43) +#348 := (= #345 #43) +#349 := [rewrite]: #348 +#346 := (= #65 #345) +#347 := [monotonicity #344]: #346 +#351 := [trans #347 #349]: #350 +#354 := [monotonicity #351]: #353 +#362 := [trans #354 #360]: #361 +#383 := [monotonicity #362 #380]: #382 +#340 := [asserted]: #69 +#384 := [mp #340 #383]: #381 +#385 := [and-elim #384]: #355 +#394 := (* -1::real #53) +#395 := (+ #43 #394) +#393 := (>= #395 0::real) +#54 := (uf_4 uf_7 #42) +#402 := (* -1::real #54) +#403 := (+ #53 #402) +#401 := (>= #403 0::real) +#397 := (+ #43 #374) +#398 := (<= #397 0::real) +#412 := (and #393 #398 #401) +#73 := (<= #43 #59) +#72 := (<= #53 #43) +#74 := (and #72 #73) +#71 := (<= #54 #53) +#75 := (and #71 #74) +#415 := (iff #75 #412) +#406 := (and #393 #398) +#409 := (and #401 #406) +#413 := (iff #409 #412) +#414 := [rewrite]: #413 +#410 := (iff #75 #409) +#407 := (iff #74 #406) +#399 := (iff #73 #398) +#400 := [rewrite]: #399 +#392 := (iff #72 #393) +#396 := [rewrite]: #392 +#408 := [monotonicity #396 #400]: #407 +#404 := (iff #71 #401) +#405 := [rewrite]: #404 +#411 := [monotonicity #405 #408]: #410 +#416 := [trans #411 #414]: #415 +#342 := [asserted]: #75 +#417 := [mp #342 #416]: #412 +#418 := [and-elim #417]: #393 +#650 := (+ #26 #394) +#651 := (<= #650 0::real) +#649 := (= #26 #53) +#671 := (= #53 #26) +#669 := (= #42 #25) +#667 := (= #25 #42) +#668 := [monotonicity #661]: #667 +#670 := [symm #668]: #669 +#672 := [monotonicity #670]: #671 +#673 := [symm #672]: #649 +#674 := (not #649) +#675 := (or #674 #651) +#676 := [th-lemma]: #675 +#677 := [unit-resolution #676 #673]: #651 +#462 := (+ #56 #459) +#465 := (>= #462 0::real) +#438 := (not #465) +#316 := (ite #290 #278 #43) +#326 := (* -1::real #316) +#327 := (+ #56 #326) +#325 := (>= #327 0::real) +#324 := (not #325) +#439 := (iff #324 #438) +#466 := (iff #325 #465) +#463 := (= #327 #462) +#460 := (= #326 #459) +#457 := (= #316 #278) +#1 := true +#452 := (ite true #278 #43) +#455 := (= #452 #278) +#456 := [rewrite]: #455 +#453 := (= #316 #452) +#444 := (iff #290 true) +#445 := [iff-true #390]: #444 +#454 := [monotonicity #445]: #453 +#458 := [trans #454 #456]: #457 +#461 := [monotonicity #458]: #460 +#464 := [monotonicity #461]: #463 +#467 := [monotonicity #464]: #466 +#468 := [monotonicity #467]: #439 +#297 := (ite #290 #54 #53) +#305 := (* -1::real #297) +#306 := (+ #56 #305) +#307 := (<= #306 0::real) +#308 := (not #307) +#332 := (and #308 #324) +#58 := (= uf_10 uf_3) +#60 := (ite #58 #26 #59) +#52 := (< #39 #22) +#61 := (ite #52 #43 #60) +#62 := (< #56 #61) +#55 := (ite #52 #53 #54) +#57 := (< #55 #56) +#63 := (and #57 #62) +#335 := (iff #63 #332) +#281 := (ite #52 #43 #278) +#284 := (< #56 #281) +#287 := (and #57 #284) +#333 := (iff #287 #332) +#330 := (iff #284 #324) +#321 := (< #56 #316) +#328 := (iff #321 #324) +#329 := [rewrite]: #328 +#322 := (iff #284 #321) +#319 := (= #281 #316) +#291 := (not #290) +#313 := (ite #291 #43 #278) +#317 := (= #313 #316) +#318 := [rewrite]: #317 +#314 := (= #281 #313) +#292 := (iff #52 #291) +#293 := [rewrite]: #292 +#315 := [monotonicity #293]: #314 +#320 := [trans #315 #318]: #319 +#323 := [monotonicity #320]: #322 +#331 := [trans #323 #329]: #330 +#311 := (iff #57 #308) +#302 := (< #297 #56) +#309 := (iff #302 #308) +#310 := [rewrite]: #309 +#303 := (iff #57 #302) +#300 := (= #55 #297) +#294 := (ite #291 #53 #54) +#298 := (= #294 #297) +#299 := [rewrite]: #298 +#295 := (= #55 #294) +#296 := [monotonicity #293]: #295 +#301 := [trans #296 #299]: #300 +#304 := [monotonicity #301]: #303 +#312 := [trans #304 #310]: #311 +#334 := [monotonicity #312 #331]: #333 +#288 := (iff #63 #287) +#285 := (iff #62 #284) +#282 := (= #61 #281) +#279 := (= #60 #278) +#225 := (iff #58 #41) +#277 := [rewrite]: #225 +#280 := [monotonicity #277]: #279 +#283 := [monotonicity #280]: #282 +#286 := [monotonicity #283]: #285 +#289 := [monotonicity #286]: #288 +#336 := [trans #289 #334]: #335 +#179 := [asserted]: #63 +#337 := [mp #179 #336]: #332 +#339 := [and-elim #337]: #324 +#469 := [mp #339 #468]: #438 +#678 := [th-lemma #469 #677 #418 #385 #666]: false +#679 := [lemma #678]: #570 +#684 := [unit-resolution #679 #683]: false +#685 := [lemma #684]: #227 +#577 := (or #228 #567) +#578 := [def-axiom]: #577 +#645 := [unit-resolution #578 #685]: #567 +#686 := (not #567) +#687 := (or #686 #643) +#688 := [th-lemma]: #687 +#689 := [unit-resolution #688 #645]: #643 +#31 := (uf_4 uf_8 #25) +#245 := (+ #31 #244) +#246 := (<= #245 0::real) +#247 := (not #246) +#34 := (uf_4 uf_9 #25) +#48 := (uf_4 uf_11 #25) +#255 := (ite #228 #48 #34) +#264 := (* -1::real #255) +#265 := (+ #31 #264) +#263 := (>= #265 0::real) +#266 := (not #263) +#271 := (and #247 #266) +#40 := (< #22 #39) +#49 := (ite #40 #34 #48) +#50 := (< #31 #49) +#45 := (ite #40 #26 #44) +#46 := (< #45 #31) +#51 := (and #46 #50) +#272 := (iff #51 #271) +#269 := (iff #50 #266) +#260 := (< #31 #255) +#267 := (iff #260 #266) +#268 := [rewrite]: #267 +#261 := (iff #50 #260) +#258 := (= #49 #255) +#252 := (ite #227 #34 #48) +#256 := (= #252 #255) +#257 := [rewrite]: #256 +#253 := (= #49 #252) +#231 := (iff #40 #227) +#232 := [rewrite]: #231 +#254 := [monotonicity #232]: #253 +#259 := [trans #254 #257]: #258 +#262 := [monotonicity #259]: #261 +#270 := [trans #262 #268]: #269 +#250 := (iff #46 #247) +#241 := (< #236 #31) +#248 := (iff #241 #247) +#249 := [rewrite]: #248 +#242 := (iff #46 #241) +#239 := (= #45 #236) +#233 := (ite #227 #26 #44) +#237 := (= #233 #236) +#238 := [rewrite]: #237 +#234 := (= #45 #233) +#235 := [monotonicity #232]: #234 +#240 := [trans #235 #238]: #239 +#243 := [monotonicity #240]: #242 +#251 := [trans #243 #249]: #250 +#273 := [monotonicity #251 #270]: #272 +#178 := [asserted]: #51 +#274 := [mp #178 #273]: #271 +#275 := [and-elim #274]: #247 +#196 := (* -1::real #31) +#212 := (+ #26 #196) +#213 := (<= #212 0::real) +#214 := (not #213) +#197 := (+ #28 #196) +#195 := (>= #197 0::real) +#193 := (not #195) +#219 := (and #193 #214) +#23 := (< #22 #22) +#35 := (ite #23 #34 #26) +#36 := (< #31 #35) +#29 := (ite #23 #26 #28) +#32 := (< #29 #31) +#37 := (and #32 #36) +#220 := (iff #37 #219) +#217 := (iff #36 #214) +#209 := (< #31 #26) +#215 := (iff #209 #214) +#216 := [rewrite]: #215 +#210 := (iff #36 #209) +#207 := (= #35 #26) +#202 := (ite false #34 #26) +#205 := (= #202 #26) +#206 := [rewrite]: #205 +#203 := (= #35 #202) +#180 := (iff #23 false) +#181 := [rewrite]: #180 +#204 := [monotonicity #181]: #203 +#208 := [trans #204 #206]: #207 +#211 := [monotonicity #208]: #210 +#218 := [trans #211 #216]: #217 +#200 := (iff #32 #193) +#189 := (< #28 #31) +#198 := (iff #189 #193) +#199 := [rewrite]: #198 +#190 := (iff #32 #189) +#187 := (= #29 #28) +#182 := (ite false #26 #28) +#185 := (= #182 #28) +#186 := [rewrite]: #185 +#183 := (= #29 #182) +#184 := [monotonicity #181]: #183 +#188 := [trans #184 #186]: #187 +#191 := [monotonicity #188]: #190 +#201 := [trans #191 #199]: #200 +#221 := [monotonicity #201 #218]: #220 +#177 := [asserted]: #37 +#222 := [mp #177 #221]: #219 +#224 := [and-elim #222]: #214 +[th-lemma #224 #275 #689]: false +unsat +00b949278548f13329cf92f11a0ad2161fa40793 907 0 #2 := false #299 := 0::real decl uf_1 :: (-> T3 T2 real) @@ -906,856 +1755,7 @@ #1366 := [unit-resolution #1233 #1365]: #1231 [th-lemma #1366 #1364 #1362]: false unsat -NQHwTeL311Tq3wf2s5BReA 419 0 -#2 := false -#194 := 0::real -decl uf_4 :: (-> T2 T3 real) -decl uf_6 :: (-> T1 T3) -decl uf_3 :: T1 -#21 := uf_3 -#25 := (uf_6 uf_3) -decl uf_5 :: T2 -#24 := uf_5 -#26 := (uf_4 uf_5 #25) -decl uf_7 :: T2 -#27 := uf_7 -#28 := (uf_4 uf_7 #25) -decl uf_10 :: T1 -#38 := uf_10 -#42 := (uf_6 uf_10) -decl uf_9 :: T2 -#33 := uf_9 -#43 := (uf_4 uf_9 #42) -#41 := (= uf_3 uf_10) -#44 := (ite #41 #43 #28) -#9 := 0::int -decl uf_2 :: (-> T1 int) -#39 := (uf_2 uf_10) -#226 := -1::int -#229 := (* -1::int #39) -#22 := (uf_2 uf_3) -#230 := (+ #22 #229) -#228 := (>= #230 0::int) -#236 := (ite #228 #44 #26) -#192 := -1::real -#244 := (* -1::real #236) -#642 := (+ #26 #244) -#643 := (<= #642 0::real) -#567 := (= #26 #236) -#227 := (not #228) -decl uf_1 :: (-> int T1) -#593 := (uf_1 #39) -#660 := (= #593 uf_10) -#594 := (= uf_10 #593) -#4 := (:var 0 T1) -#5 := (uf_2 #4) -#546 := (pattern #5) -#6 := (uf_1 #5) -#93 := (= #4 #6) -#547 := (forall (vars (?x1 T1)) (:pat #546) #93) -#96 := (forall (vars (?x1 T1)) #93) -#550 := (iff #96 #547) -#548 := (iff #93 #93) -#549 := [refl]: #548 -#551 := [quant-intro #549]: #550 -#448 := (~ #96 #96) -#450 := (~ #93 #93) -#451 := [refl]: #450 -#449 := [nnf-pos #451]: #448 -#7 := (= #6 #4) -#8 := (forall (vars (?x1 T1)) #7) -#97 := (iff #8 #96) -#94 := (iff #7 #93) -#95 := [rewrite]: #94 -#98 := [quant-intro #95]: #97 -#92 := [asserted]: #8 -#101 := [mp #92 #98]: #96 -#446 := [mp~ #101 #449]: #96 -#552 := [mp #446 #551]: #547 -#595 := (not #547) -#600 := (or #595 #594) -#601 := [quant-inst]: #600 -#654 := [unit-resolution #601 #552]: #594 -#680 := [symm #654]: #660 -#681 := (= uf_3 #593) -#591 := (uf_1 #22) -#658 := (= #591 #593) -#656 := (= #593 #591) -#652 := (= #39 #22) -#647 := (= #22 #39) -#290 := (<= #230 0::int) -#70 := (<= #22 #39) -#388 := (iff #70 #290) -#389 := [rewrite]: #388 -#341 := [asserted]: #70 -#390 := [mp #341 #389]: #290 -#646 := [hypothesis]: #228 -#648 := [th-lemma #646 #390]: #647 -#653 := [symm #648]: #652 -#657 := [monotonicity #653]: #656 -#659 := [symm #657]: #658 -#592 := (= uf_3 #591) -#596 := (or #595 #592) -#597 := [quant-inst]: #596 -#655 := [unit-resolution #597 #552]: #592 -#682 := [trans #655 #659]: #681 -#683 := [trans #682 #680]: #41 -#570 := (not #41) -decl uf_11 :: T2 -#47 := uf_11 -#59 := (uf_4 uf_11 #42) -#278 := (ite #41 #26 #59) -#459 := (* -1::real #278) -#637 := (+ #26 #459) -#639 := (>= #637 0::real) -#585 := (= #26 #278) -#661 := [hypothesis]: #41 -#587 := (or #570 #585) -#588 := [def-axiom]: #587 -#662 := [unit-resolution #588 #661]: #585 -#663 := (not #585) -#664 := (or #663 #639) -#665 := [th-lemma]: #664 -#666 := [unit-resolution #665 #662]: #639 -decl uf_8 :: T2 -#30 := uf_8 -#56 := (uf_4 uf_8 #42) -#357 := (* -1::real #56) -#358 := (+ #43 #357) -#356 := (>= #358 0::real) -#355 := (not #356) -#374 := (* -1::real #59) -#375 := (+ #56 #374) -#373 := (>= #375 0::real) -#376 := (not #373) -#381 := (and #355 #376) -#64 := (< #39 #39) -#67 := (ite #64 #43 #59) -#68 := (< #56 #67) -#53 := (uf_4 uf_5 #42) -#65 := (ite #64 #53 #43) -#66 := (< #65 #56) -#69 := (and #66 #68) -#382 := (iff #69 #381) -#379 := (iff #68 #376) -#370 := (< #56 #59) -#377 := (iff #370 #376) -#378 := [rewrite]: #377 -#371 := (iff #68 #370) -#368 := (= #67 #59) -#363 := (ite false #43 #59) -#366 := (= #363 #59) -#367 := [rewrite]: #366 -#364 := (= #67 #363) -#343 := (iff #64 false) -#344 := [rewrite]: #343 -#365 := [monotonicity #344]: #364 -#369 := [trans #365 #367]: #368 -#372 := [monotonicity #369]: #371 -#380 := [trans #372 #378]: #379 -#361 := (iff #66 #355) -#352 := (< #43 #56) -#359 := (iff #352 #355) -#360 := [rewrite]: #359 -#353 := (iff #66 #352) -#350 := (= #65 #43) -#345 := (ite false #53 #43) -#348 := (= #345 #43) -#349 := [rewrite]: #348 -#346 := (= #65 #345) -#347 := [monotonicity #344]: #346 -#351 := [trans #347 #349]: #350 -#354 := [monotonicity #351]: #353 -#362 := [trans #354 #360]: #361 -#383 := [monotonicity #362 #380]: #382 -#340 := [asserted]: #69 -#384 := [mp #340 #383]: #381 -#385 := [and-elim #384]: #355 -#394 := (* -1::real #53) -#395 := (+ #43 #394) -#393 := (>= #395 0::real) -#54 := (uf_4 uf_7 #42) -#402 := (* -1::real #54) -#403 := (+ #53 #402) -#401 := (>= #403 0::real) -#397 := (+ #43 #374) -#398 := (<= #397 0::real) -#412 := (and #393 #398 #401) -#73 := (<= #43 #59) -#72 := (<= #53 #43) -#74 := (and #72 #73) -#71 := (<= #54 #53) -#75 := (and #71 #74) -#415 := (iff #75 #412) -#406 := (and #393 #398) -#409 := (and #401 #406) -#413 := (iff #409 #412) -#414 := [rewrite]: #413 -#410 := (iff #75 #409) -#407 := (iff #74 #406) -#399 := (iff #73 #398) -#400 := [rewrite]: #399 -#392 := (iff #72 #393) -#396 := [rewrite]: #392 -#408 := [monotonicity #396 #400]: #407 -#404 := (iff #71 #401) -#405 := [rewrite]: #404 -#411 := [monotonicity #405 #408]: #410 -#416 := [trans #411 #414]: #415 -#342 := [asserted]: #75 -#417 := [mp #342 #416]: #412 -#418 := [and-elim #417]: #393 -#650 := (+ #26 #394) -#651 := (<= #650 0::real) -#649 := (= #26 #53) -#671 := (= #53 #26) -#669 := (= #42 #25) -#667 := (= #25 #42) -#668 := [monotonicity #661]: #667 -#670 := [symm #668]: #669 -#672 := [monotonicity #670]: #671 -#673 := [symm #672]: #649 -#674 := (not #649) -#675 := (or #674 #651) -#676 := [th-lemma]: #675 -#677 := [unit-resolution #676 #673]: #651 -#462 := (+ #56 #459) -#465 := (>= #462 0::real) -#438 := (not #465) -#316 := (ite #290 #278 #43) -#326 := (* -1::real #316) -#327 := (+ #56 #326) -#325 := (>= #327 0::real) -#324 := (not #325) -#439 := (iff #324 #438) -#466 := (iff #325 #465) -#463 := (= #327 #462) -#460 := (= #326 #459) -#457 := (= #316 #278) -#1 := true -#452 := (ite true #278 #43) -#455 := (= #452 #278) -#456 := [rewrite]: #455 -#453 := (= #316 #452) -#444 := (iff #290 true) -#445 := [iff-true #390]: #444 -#454 := [monotonicity #445]: #453 -#458 := [trans #454 #456]: #457 -#461 := [monotonicity #458]: #460 -#464 := [monotonicity #461]: #463 -#467 := [monotonicity #464]: #466 -#468 := [monotonicity #467]: #439 -#297 := (ite #290 #54 #53) -#305 := (* -1::real #297) -#306 := (+ #56 #305) -#307 := (<= #306 0::real) -#308 := (not #307) -#332 := (and #308 #324) -#58 := (= uf_10 uf_3) -#60 := (ite #58 #26 #59) -#52 := (< #39 #22) -#61 := (ite #52 #43 #60) -#62 := (< #56 #61) -#55 := (ite #52 #53 #54) -#57 := (< #55 #56) -#63 := (and #57 #62) -#335 := (iff #63 #332) -#281 := (ite #52 #43 #278) -#284 := (< #56 #281) -#287 := (and #57 #284) -#333 := (iff #287 #332) -#330 := (iff #284 #324) -#321 := (< #56 #316) -#328 := (iff #321 #324) -#329 := [rewrite]: #328 -#322 := (iff #284 #321) -#319 := (= #281 #316) -#291 := (not #290) -#313 := (ite #291 #43 #278) -#317 := (= #313 #316) -#318 := [rewrite]: #317 -#314 := (= #281 #313) -#292 := (iff #52 #291) -#293 := [rewrite]: #292 -#315 := [monotonicity #293]: #314 -#320 := [trans #315 #318]: #319 -#323 := [monotonicity #320]: #322 -#331 := [trans #323 #329]: #330 -#311 := (iff #57 #308) -#302 := (< #297 #56) -#309 := (iff #302 #308) -#310 := [rewrite]: #309 -#303 := (iff #57 #302) -#300 := (= #55 #297) -#294 := (ite #291 #53 #54) -#298 := (= #294 #297) -#299 := [rewrite]: #298 -#295 := (= #55 #294) -#296 := [monotonicity #293]: #295 -#301 := [trans #296 #299]: #300 -#304 := [monotonicity #301]: #303 -#312 := [trans #304 #310]: #311 -#334 := [monotonicity #312 #331]: #333 -#288 := (iff #63 #287) -#285 := (iff #62 #284) -#282 := (= #61 #281) -#279 := (= #60 #278) -#225 := (iff #58 #41) -#277 := [rewrite]: #225 -#280 := [monotonicity #277]: #279 -#283 := [monotonicity #280]: #282 -#286 := [monotonicity #283]: #285 -#289 := [monotonicity #286]: #288 -#336 := [trans #289 #334]: #335 -#179 := [asserted]: #63 -#337 := [mp #179 #336]: #332 -#339 := [and-elim #337]: #324 -#469 := [mp #339 #468]: #438 -#678 := [th-lemma #469 #677 #418 #385 #666]: false -#679 := [lemma #678]: #570 -#684 := [unit-resolution #679 #683]: false -#685 := [lemma #684]: #227 -#577 := (or #228 #567) -#578 := [def-axiom]: #577 -#645 := [unit-resolution #578 #685]: #567 -#686 := (not #567) -#687 := (or #686 #643) -#688 := [th-lemma]: #687 -#689 := [unit-resolution #688 #645]: #643 -#31 := (uf_4 uf_8 #25) -#245 := (+ #31 #244) -#246 := (<= #245 0::real) -#247 := (not #246) -#34 := (uf_4 uf_9 #25) -#48 := (uf_4 uf_11 #25) -#255 := (ite #228 #48 #34) -#264 := (* -1::real #255) -#265 := (+ #31 #264) -#263 := (>= #265 0::real) -#266 := (not #263) -#271 := (and #247 #266) -#40 := (< #22 #39) -#49 := (ite #40 #34 #48) -#50 := (< #31 #49) -#45 := (ite #40 #26 #44) -#46 := (< #45 #31) -#51 := (and #46 #50) -#272 := (iff #51 #271) -#269 := (iff #50 #266) -#260 := (< #31 #255) -#267 := (iff #260 #266) -#268 := [rewrite]: #267 -#261 := (iff #50 #260) -#258 := (= #49 #255) -#252 := (ite #227 #34 #48) -#256 := (= #252 #255) -#257 := [rewrite]: #256 -#253 := (= #49 #252) -#231 := (iff #40 #227) -#232 := [rewrite]: #231 -#254 := [monotonicity #232]: #253 -#259 := [trans #254 #257]: #258 -#262 := [monotonicity #259]: #261 -#270 := [trans #262 #268]: #269 -#250 := (iff #46 #247) -#241 := (< #236 #31) -#248 := (iff #241 #247) -#249 := [rewrite]: #248 -#242 := (iff #46 #241) -#239 := (= #45 #236) -#233 := (ite #227 #26 #44) -#237 := (= #233 #236) -#238 := [rewrite]: #237 -#234 := (= #45 #233) -#235 := [monotonicity #232]: #234 -#240 := [trans #235 #238]: #239 -#243 := [monotonicity #240]: #242 -#251 := [trans #243 #249]: #250 -#273 := [monotonicity #251 #270]: #272 -#178 := [asserted]: #51 -#274 := [mp #178 #273]: #271 -#275 := [and-elim #274]: #247 -#196 := (* -1::real #31) -#212 := (+ #26 #196) -#213 := (<= #212 0::real) -#214 := (not #213) -#197 := (+ #28 #196) -#195 := (>= #197 0::real) -#193 := (not #195) -#219 := (and #193 #214) -#23 := (< #22 #22) -#35 := (ite #23 #34 #26) -#36 := (< #31 #35) -#29 := (ite #23 #26 #28) -#32 := (< #29 #31) -#37 := (and #32 #36) -#220 := (iff #37 #219) -#217 := (iff #36 #214) -#209 := (< #31 #26) -#215 := (iff #209 #214) -#216 := [rewrite]: #215 -#210 := (iff #36 #209) -#207 := (= #35 #26) -#202 := (ite false #34 #26) -#205 := (= #202 #26) -#206 := [rewrite]: #205 -#203 := (= #35 #202) -#180 := (iff #23 false) -#181 := [rewrite]: #180 -#204 := [monotonicity #181]: #203 -#208 := [trans #204 #206]: #207 -#211 := [monotonicity #208]: #210 -#218 := [trans #211 #216]: #217 -#200 := (iff #32 #193) -#189 := (< #28 #31) -#198 := (iff #189 #193) -#199 := [rewrite]: #198 -#190 := (iff #32 #189) -#187 := (= #29 #28) -#182 := (ite false #26 #28) -#185 := (= #182 #28) -#186 := [rewrite]: #185 -#183 := (= #29 #182) -#184 := [monotonicity #181]: #183 -#188 := [trans #184 #186]: #187 -#191 := [monotonicity #188]: #190 -#201 := [trans #191 #199]: #200 -#221 := [monotonicity #201 #218]: #220 -#177 := [asserted]: #37 -#222 := [mp #177 #221]: #219 -#224 := [and-elim #222]: #214 -[th-lemma #224 #275 #689]: false -unsat -NX/HT1QOfbspC2LtZNKpBA 428 0 -#2 := false -decl uf_10 :: T1 -#38 := uf_10 -decl uf_3 :: T1 -#21 := uf_3 -#45 := (= uf_3 uf_10) -decl uf_1 :: (-> int T1) -decl uf_2 :: (-> T1 int) -#39 := (uf_2 uf_10) -#588 := (uf_1 #39) -#686 := (= #588 uf_10) -#589 := (= uf_10 #588) -#4 := (:var 0 T1) -#5 := (uf_2 #4) -#541 := (pattern #5) -#6 := (uf_1 #5) -#93 := (= #4 #6) -#542 := (forall (vars (?x1 T1)) (:pat #541) #93) -#96 := (forall (vars (?x1 T1)) #93) -#545 := (iff #96 #542) -#543 := (iff #93 #93) -#544 := [refl]: #543 -#546 := [quant-intro #544]: #545 -#454 := (~ #96 #96) -#456 := (~ #93 #93) -#457 := [refl]: #456 -#455 := [nnf-pos #457]: #454 -#7 := (= #6 #4) -#8 := (forall (vars (?x1 T1)) #7) -#97 := (iff #8 #96) -#94 := (iff #7 #93) -#95 := [rewrite]: #94 -#98 := [quant-intro #95]: #97 -#92 := [asserted]: #8 -#101 := [mp #92 #98]: #96 -#452 := [mp~ #101 #455]: #96 -#547 := [mp #452 #546]: #542 -#590 := (not #542) -#595 := (or #590 #589) -#596 := [quant-inst]: #595 -#680 := [unit-resolution #596 #547]: #589 -#687 := [symm #680]: #686 -#688 := (= uf_3 #588) -#22 := (uf_2 uf_3) -#586 := (uf_1 #22) -#684 := (= #586 #588) -#682 := (= #588 #586) -#678 := (= #39 #22) -#676 := (= #22 #39) -#9 := 0::int -#227 := -1::int -#230 := (* -1::int #39) -#231 := (+ #22 #230) -#296 := (<= #231 0::int) -#70 := (<= #22 #39) -#393 := (iff #70 #296) -#394 := [rewrite]: #393 -#347 := [asserted]: #70 -#395 := [mp #347 #394]: #296 -#229 := (>= #231 0::int) -decl uf_4 :: (-> T2 T3 real) -decl uf_6 :: (-> T1 T3) -#25 := (uf_6 uf_3) -decl uf_7 :: T2 -#27 := uf_7 -#28 := (uf_4 uf_7 #25) -decl uf_9 :: T2 -#33 := uf_9 -#34 := (uf_4 uf_9 #25) -#46 := (uf_6 uf_10) -decl uf_5 :: T2 -#24 := uf_5 -#47 := (uf_4 uf_5 #46) -#48 := (ite #45 #47 #34) -#256 := (ite #229 #48 #28) -#568 := (= #28 #256) -#648 := (not #568) -#194 := 0::real -#192 := -1::real -#265 := (* -1::real #256) -#640 := (+ #28 #265) -#642 := (>= #640 0::real) -#645 := (not #642) -#643 := [hypothesis]: #642 -decl uf_8 :: T2 -#30 := uf_8 -#31 := (uf_4 uf_8 #25) -#266 := (+ #31 #265) -#264 := (>= #266 0::real) -#267 := (not #264) -#26 := (uf_4 uf_5 #25) -decl uf_11 :: T2 -#41 := uf_11 -#42 := (uf_4 uf_11 #25) -#237 := (ite #229 #42 #26) -#245 := (* -1::real #237) -#246 := (+ #31 #245) -#247 := (<= #246 0::real) -#248 := (not #247) -#272 := (and #248 #267) -#40 := (< #22 #39) -#49 := (ite #40 #28 #48) -#50 := (< #31 #49) -#43 := (ite #40 #26 #42) -#44 := (< #43 #31) -#51 := (and #44 #50) -#273 := (iff #51 #272) -#270 := (iff #50 #267) -#261 := (< #31 #256) -#268 := (iff #261 #267) -#269 := [rewrite]: #268 -#262 := (iff #50 #261) -#259 := (= #49 #256) -#228 := (not #229) -#253 := (ite #228 #28 #48) -#257 := (= #253 #256) -#258 := [rewrite]: #257 -#254 := (= #49 #253) -#232 := (iff #40 #228) -#233 := [rewrite]: #232 -#255 := [monotonicity #233]: #254 -#260 := [trans #255 #258]: #259 -#263 := [monotonicity #260]: #262 -#271 := [trans #263 #269]: #270 -#251 := (iff #44 #248) -#242 := (< #237 #31) -#249 := (iff #242 #248) -#250 := [rewrite]: #249 -#243 := (iff #44 #242) -#240 := (= #43 #237) -#234 := (ite #228 #26 #42) -#238 := (= #234 #237) -#239 := [rewrite]: #238 -#235 := (= #43 #234) -#236 := [monotonicity #233]: #235 -#241 := [trans #236 #239]: #240 -#244 := [monotonicity #241]: #243 -#252 := [trans #244 #250]: #251 -#274 := [monotonicity #252 #271]: #273 -#178 := [asserted]: #51 -#275 := [mp #178 #274]: #272 -#277 := [and-elim #275]: #267 -#196 := (* -1::real #31) -#197 := (+ #28 #196) -#195 := (>= #197 0::real) -#193 := (not #195) -#213 := (* -1::real #34) -#214 := (+ #31 #213) -#212 := (>= #214 0::real) -#215 := (not #212) -#220 := (and #193 #215) -#23 := (< #22 #22) -#35 := (ite #23 #28 #34) -#36 := (< #31 #35) -#29 := (ite #23 #26 #28) -#32 := (< #29 #31) -#37 := (and #32 #36) -#221 := (iff #37 #220) -#218 := (iff #36 #215) -#209 := (< #31 #34) -#216 := (iff #209 #215) -#217 := [rewrite]: #216 -#210 := (iff #36 #209) -#207 := (= #35 #34) -#202 := (ite false #28 #34) -#205 := (= #202 #34) -#206 := [rewrite]: #205 -#203 := (= #35 #202) -#180 := (iff #23 false) -#181 := [rewrite]: #180 -#204 := [monotonicity #181]: #203 -#208 := [trans #204 #206]: #207 -#211 := [monotonicity #208]: #210 -#219 := [trans #211 #217]: #218 -#200 := (iff #32 #193) -#189 := (< #28 #31) -#198 := (iff #189 #193) -#199 := [rewrite]: #198 -#190 := (iff #32 #189) -#187 := (= #29 #28) -#182 := (ite false #26 #28) -#185 := (= #182 #28) -#186 := [rewrite]: #185 -#183 := (= #29 #182) -#184 := [monotonicity #181]: #183 -#188 := [trans #184 #186]: #187 -#191 := [monotonicity #188]: #190 -#201 := [trans #191 #199]: #200 -#222 := [monotonicity #201 #219]: #221 -#177 := [asserted]: #37 -#223 := [mp #177 #222]: #220 -#224 := [and-elim #223]: #193 -#644 := [th-lemma #224 #277 #643]: false -#646 := [lemma #644]: #645 -#647 := [hypothesis]: #568 -#649 := (or #648 #642) -#650 := [th-lemma]: #649 -#651 := [unit-resolution #650 #647 #646]: false -#652 := [lemma #651]: #648 -#578 := (or #229 #568) -#579 := [def-axiom]: #578 -#675 := [unit-resolution #579 #652]: #229 -#677 := [th-lemma #675 #395]: #676 -#679 := [symm #677]: #678 -#683 := [monotonicity #679]: #682 -#685 := [symm #683]: #684 -#587 := (= uf_3 #586) -#591 := (or #590 #587) -#592 := [quant-inst]: #591 -#681 := [unit-resolution #592 #547]: #587 -#689 := [trans #681 #685]: #688 -#690 := [trans #689 #687]: #45 -#571 := (not #45) -#54 := (uf_4 uf_11 #46) -#279 := (ite #45 #28 #54) -#465 := (* -1::real #279) -#632 := (+ #28 #465) -#633 := (<= #632 0::real) -#580 := (= #28 #279) -#656 := [hypothesis]: #45 -#582 := (or #571 #580) -#583 := [def-axiom]: #582 -#657 := [unit-resolution #583 #656]: #580 -#658 := (not #580) -#659 := (or #658 #633) -#660 := [th-lemma]: #659 -#661 := [unit-resolution #660 #657]: #633 -#57 := (uf_4 uf_8 #46) -#363 := (* -1::real #57) -#379 := (+ #47 #363) -#380 := (<= #379 0::real) -#381 := (not #380) -#364 := (+ #54 #363) -#362 := (>= #364 0::real) -#361 := (not #362) -#386 := (and #361 #381) -#59 := (uf_4 uf_7 #46) -#64 := (< #39 #39) -#67 := (ite #64 #59 #47) -#68 := (< #57 #67) -#65 := (ite #64 #47 #54) -#66 := (< #65 #57) -#69 := (and #66 #68) -#387 := (iff #69 #386) -#384 := (iff #68 #381) -#376 := (< #57 #47) -#382 := (iff #376 #381) -#383 := [rewrite]: #382 -#377 := (iff #68 #376) -#374 := (= #67 #47) -#369 := (ite false #59 #47) -#372 := (= #369 #47) -#373 := [rewrite]: #372 -#370 := (= #67 #369) -#349 := (iff #64 false) -#350 := [rewrite]: #349 -#371 := [monotonicity #350]: #370 -#375 := [trans #371 #373]: #374 -#378 := [monotonicity #375]: #377 -#385 := [trans #378 #383]: #384 -#367 := (iff #66 #361) -#358 := (< #54 #57) -#365 := (iff #358 #361) -#366 := [rewrite]: #365 -#359 := (iff #66 #358) -#356 := (= #65 #54) -#351 := (ite false #47 #54) -#354 := (= #351 #54) -#355 := [rewrite]: #354 -#352 := (= #65 #351) -#353 := [monotonicity #350]: #352 -#357 := [trans #353 #355]: #356 -#360 := [monotonicity #357]: #359 -#368 := [trans #360 #366]: #367 -#388 := [monotonicity #368 #385]: #387 -#346 := [asserted]: #69 -#389 := [mp #346 #388]: #386 -#391 := [and-elim #389]: #381 -#397 := (* -1::real #59) -#398 := (+ #47 #397) -#399 := (<= #398 0::real) -#409 := (* -1::real #54) -#410 := (+ #47 #409) -#408 := (>= #410 0::real) -#60 := (uf_4 uf_9 #46) -#402 := (* -1::real #60) -#403 := (+ #59 #402) -#404 := (<= #403 0::real) -#418 := (and #399 #404 #408) -#73 := (<= #59 #60) -#72 := (<= #47 #59) -#74 := (and #72 #73) -#71 := (<= #54 #47) -#75 := (and #71 #74) -#421 := (iff #75 #418) -#412 := (and #399 #404) -#415 := (and #408 #412) -#419 := (iff #415 #418) -#420 := [rewrite]: #419 -#416 := (iff #75 #415) -#413 := (iff #74 #412) -#405 := (iff #73 #404) -#406 := [rewrite]: #405 -#400 := (iff #72 #399) -#401 := [rewrite]: #400 -#414 := [monotonicity #401 #406]: #413 -#407 := (iff #71 #408) -#411 := [rewrite]: #407 -#417 := [monotonicity #411 #414]: #416 -#422 := [trans #417 #420]: #421 -#348 := [asserted]: #75 -#423 := [mp #348 #422]: #418 -#424 := [and-elim #423]: #399 -#637 := (+ #28 #397) -#639 := (>= #637 0::real) -#636 := (= #28 #59) -#666 := (= #59 #28) -#664 := (= #46 #25) -#662 := (= #25 #46) -#663 := [monotonicity #656]: #662 -#665 := [symm #663]: #664 -#667 := [monotonicity #665]: #666 -#668 := [symm #667]: #636 -#669 := (not #636) -#670 := (or #669 #639) -#671 := [th-lemma]: #670 -#672 := [unit-resolution #671 #668]: #639 -#468 := (+ #57 #465) -#471 := (<= #468 0::real) -#444 := (not #471) -#322 := (ite #296 #279 #47) -#330 := (* -1::real #322) -#331 := (+ #57 #330) -#332 := (<= #331 0::real) -#333 := (not #332) -#445 := (iff #333 #444) -#472 := (iff #332 #471) -#469 := (= #331 #468) -#466 := (= #330 #465) -#463 := (= #322 #279) -#1 := true -#458 := (ite true #279 #47) -#461 := (= #458 #279) -#462 := [rewrite]: #461 -#459 := (= #322 #458) -#450 := (iff #296 true) -#451 := [iff-true #395]: #450 -#460 := [monotonicity #451]: #459 -#464 := [trans #460 #462]: #463 -#467 := [monotonicity #464]: #466 -#470 := [monotonicity #467]: #469 -#473 := [monotonicity #470]: #472 -#474 := [monotonicity #473]: #445 -#303 := (ite #296 #60 #59) -#313 := (* -1::real #303) -#314 := (+ #57 #313) -#312 := (>= #314 0::real) -#311 := (not #312) -#338 := (and #311 #333) -#52 := (< #39 #22) -#61 := (ite #52 #59 #60) -#62 := (< #57 #61) -#53 := (= uf_10 uf_3) -#55 := (ite #53 #28 #54) -#56 := (ite #52 #47 #55) -#58 := (< #56 #57) -#63 := (and #58 #62) -#341 := (iff #63 #338) -#282 := (ite #52 #47 #279) -#285 := (< #282 #57) -#291 := (and #62 #285) -#339 := (iff #291 #338) -#336 := (iff #285 #333) -#327 := (< #322 #57) -#334 := (iff #327 #333) -#335 := [rewrite]: #334 -#328 := (iff #285 #327) -#325 := (= #282 #322) -#297 := (not #296) -#319 := (ite #297 #47 #279) -#323 := (= #319 #322) -#324 := [rewrite]: #323 -#320 := (= #282 #319) -#298 := (iff #52 #297) -#299 := [rewrite]: #298 -#321 := [monotonicity #299]: #320 -#326 := [trans #321 #324]: #325 -#329 := [monotonicity #326]: #328 -#337 := [trans #329 #335]: #336 -#317 := (iff #62 #311) -#308 := (< #57 #303) -#315 := (iff #308 #311) -#316 := [rewrite]: #315 -#309 := (iff #62 #308) -#306 := (= #61 #303) -#300 := (ite #297 #59 #60) -#304 := (= #300 #303) -#305 := [rewrite]: #304 -#301 := (= #61 #300) -#302 := [monotonicity #299]: #301 -#307 := [trans #302 #305]: #306 -#310 := [monotonicity #307]: #309 -#318 := [trans #310 #316]: #317 -#340 := [monotonicity #318 #337]: #339 -#294 := (iff #63 #291) -#288 := (and #285 #62) -#292 := (iff #288 #291) -#293 := [rewrite]: #292 -#289 := (iff #63 #288) -#286 := (iff #58 #285) -#283 := (= #56 #282) -#280 := (= #55 #279) -#226 := (iff #53 #45) -#278 := [rewrite]: #226 -#281 := [monotonicity #278]: #280 -#284 := [monotonicity #281]: #283 -#287 := [monotonicity #284]: #286 -#290 := [monotonicity #287]: #289 -#295 := [trans #290 #293]: #294 -#342 := [trans #295 #340]: #341 -#179 := [asserted]: #63 -#343 := [mp #179 #342]: #338 -#345 := [and-elim #343]: #333 -#475 := [mp #345 #474]: #444 -#673 := [th-lemma #475 #672 #424 #391 #661]: false -#674 := [lemma #673]: #571 -[unit-resolution #674 #690]: false -unsat -IL2powemHjRpCJYwmXFxyw 211 0 +f5cf3017773c1cf700f533cb220ba6c9eb22de56 211 0 #2 := false #33 := 0::real decl uf_11 :: (-> T5 T6 real) @@ -1967,7 +1967,7 @@ #328 := [unit-resolution #319 #327]: #300 [th-lemma #326 #334 #195 #328 #187 #138]: false unsat -GX51o3DUO/UBS3eNP2P9kA 285 0 +ad41c2d9b185dd9b4fd0abefcdc55357d2105ed8 285 0 #2 := false #7 := 0::real decl uf_4 :: real @@ -2253,7 +2253,7 @@ #286 := [lemma #284]: #285 [unit-resolution #286 #308 #305]: false unsat -cebG074uorSr8ODzgTmcKg 97 0 +076d8565ad4c4370b16a3b0c139e8c8e8fb58224 97 0 #2 := false #18 := 0::real decl uf_1 :: (-> T2 T1 real) @@ -2351,7 +2351,7 @@ #173 := [mp #167 #172]: #165 [unit-resolution #173 #147 #76]: false unsat -DKRtrJ2XceCkITuNwNViRw 57 0 +8e6ea05b53a9ffb5a6dec689eb004bdb0c2a755b 57 0 #2 := false #4 := 0::real decl uf_1 :: (-> T2 real) @@ -2409,7 +2409,7 @@ #269 := [quant-inst]: #268 [unit-resolution #269 #247 #274]: false unsat -97KJAJfUio+nGchEHWvgAw 91 0 +d278c38176edc1fb6492d54817f0a9092db653e6 91 0 #2 := false #38 := 0::real decl uf_1 :: (-> T1 T2 real) @@ -2501,157 +2501,7 @@ #153 := [mp #147 #152]: #145 [unit-resolution #153 #129 #160]: false unsat -flJYbeWfe+t2l/zsRqdujA 149 0 -#2 := false -#19 := 0::real -decl uf_1 :: (-> T1 T2 real) -decl uf_3 :: T2 -#5 := uf_3 -decl uf_4 :: T1 -#7 := uf_4 -#8 := (uf_1 uf_4 uf_3) -#44 := -1::real -#156 := (* -1::real #8) -decl uf_2 :: T1 -#4 := uf_2 -#6 := (uf_1 uf_2 uf_3) -#203 := (+ #6 #156) -#205 := (>= #203 0::real) -#9 := (= #6 #8) -#40 := [asserted]: #9 -#208 := (not #9) -#209 := (or #208 #205) -#210 := [th-lemma]: #209 -#211 := [unit-resolution #210 #40]: #205 -decl uf_5 :: T1 -#12 := uf_5 -#22 := (uf_1 uf_5 uf_3) -#160 := (* -1::real #22) -#161 := (+ #6 #160) -#207 := (>= #161 0::real) -#222 := (not #207) -#206 := (= #6 #22) -#216 := (not #206) -#62 := (= #8 #22) -#70 := (not #62) -#217 := (iff #70 #216) -#214 := (iff #62 #206) -#212 := (iff #206 #62) -#213 := [monotonicity #40]: #212 -#215 := [symm #213]: #214 -#218 := [monotonicity #215]: #217 -#23 := (= #22 #8) -#24 := (not #23) -#71 := (iff #24 #70) -#68 := (iff #23 #62) -#69 := [rewrite]: #68 -#72 := [monotonicity #69]: #71 -#43 := [asserted]: #24 -#75 := [mp #43 #72]: #70 -#219 := [mp #75 #218]: #216 -#225 := (or #206 #222) -#162 := (<= #161 0::real) -#172 := (+ #8 #160) -#173 := (>= #172 0::real) -#178 := (not #173) -#163 := (not #162) -#181 := (or #163 #178) -#184 := (not #181) -#10 := (:var 0 T2) -#15 := (uf_1 uf_4 #10) -#149 := (pattern #15) -#13 := (uf_1 uf_5 #10) -#148 := (pattern #13) -#11 := (uf_1 uf_2 #10) -#147 := (pattern #11) -#50 := (* -1::real #15) -#51 := (+ #13 #50) -#52 := (<= #51 0::real) -#76 := (not #52) -#45 := (* -1::real #13) -#46 := (+ #11 #45) -#47 := (<= #46 0::real) -#78 := (not #47) -#73 := (or #78 #76) -#83 := (not #73) -#150 := (forall (vars (?x1 T2)) (:pat #147 #148 #149) #83) -#86 := (forall (vars (?x1 T2)) #83) -#153 := (iff #86 #150) -#151 := (iff #83 #83) -#152 := [refl]: #151 -#154 := [quant-intro #152]: #153 -#55 := (and #47 #52) -#58 := (forall (vars (?x1 T2)) #55) -#87 := (iff #58 #86) -#84 := (iff #55 #83) -#85 := [rewrite]: #84 -#88 := [quant-intro #85]: #87 -#79 := (~ #58 #58) -#81 := (~ #55 #55) -#82 := [refl]: #81 -#80 := [nnf-pos #82]: #79 -#16 := (<= #13 #15) -#14 := (<= #11 #13) -#17 := (and #14 #16) -#18 := (forall (vars (?x1 T2)) #17) -#59 := (iff #18 #58) -#56 := (iff #17 #55) -#53 := (iff #16 #52) -#54 := [rewrite]: #53 -#48 := (iff #14 #47) -#49 := [rewrite]: #48 -#57 := [monotonicity #49 #54]: #56 -#60 := [quant-intro #57]: #59 -#41 := [asserted]: #18 -#61 := [mp #41 #60]: #58 -#77 := [mp~ #61 #80]: #58 -#89 := [mp #77 #88]: #86 -#155 := [mp #89 #154]: #150 -#187 := (not #150) -#188 := (or #187 #184) -#157 := (+ #22 #156) -#158 := (<= #157 0::real) -#159 := (not #158) -#164 := (or #163 #159) -#165 := (not #164) -#189 := (or #187 #165) -#191 := (iff #189 #188) -#193 := (iff #188 #188) -#194 := [rewrite]: #193 -#185 := (iff #165 #184) -#182 := (iff #164 #181) -#179 := (iff #159 #178) -#176 := (iff #158 #173) -#166 := (+ #156 #22) -#169 := (<= #166 0::real) -#174 := (iff #169 #173) -#175 := [rewrite]: #174 -#170 := (iff #158 #169) -#167 := (= #157 #166) -#168 := [rewrite]: #167 -#171 := [monotonicity #168]: #170 -#177 := [trans #171 #175]: #176 -#180 := [monotonicity #177]: #179 -#183 := [monotonicity #180]: #182 -#186 := [monotonicity #183]: #185 -#192 := [monotonicity #186]: #191 -#195 := [trans #192 #194]: #191 -#190 := [quant-inst]: #189 -#196 := [mp #190 #195]: #188 -#220 := [unit-resolution #196 #155]: #184 -#197 := (or #181 #162) -#198 := [def-axiom]: #197 -#221 := [unit-resolution #198 #220]: #162 -#223 := (or #206 #163 #222) -#224 := [th-lemma]: #223 -#226 := [unit-resolution #224 #221]: #225 -#227 := [unit-resolution #226 #219]: #222 -#199 := (or #181 #173) -#200 := [def-axiom]: #199 -#228 := [unit-resolution #200 #220]: #173 -[th-lemma #228 #227 #211]: false -unsat -rbrrQuQfaijtLkQizgEXnQ 222 0 +38b5e95092f91070fab780891ebf7b83d5f95757 222 0 #2 := false #4 := 0::real decl uf_2 :: (-> T2 T1 real) @@ -2874,7 +2724,7 @@ #308 := [th-lemma]: #307 [unit-resolution #308 #305 #290]: false unsat -hwh3oeLAWt56hnKIa8Wuow 248 0 +4968b0a0840255d92fbecd59ed4dac302603b2bd 248 0 #2 := false #4 := 0::real decl uf_2 :: (-> T2 T1 real) @@ -3123,7 +2973,157 @@ #380 := [th-lemma]: #379 [unit-resolution #380 #377 #363]: false unsat -WdMJH3tkMv/rps8y9Ukq5Q 86 0 +a3b02dd75d8b2261f1b7ef7215268d84fd25e972 149 0 +#2 := false +#19 := 0::real +decl uf_1 :: (-> T1 T2 real) +decl uf_3 :: T2 +#5 := uf_3 +decl uf_4 :: T1 +#7 := uf_4 +#8 := (uf_1 uf_4 uf_3) +#44 := -1::real +#156 := (* -1::real #8) +decl uf_2 :: T1 +#4 := uf_2 +#6 := (uf_1 uf_2 uf_3) +#203 := (+ #6 #156) +#205 := (>= #203 0::real) +#9 := (= #6 #8) +#40 := [asserted]: #9 +#208 := (not #9) +#209 := (or #208 #205) +#210 := [th-lemma]: #209 +#211 := [unit-resolution #210 #40]: #205 +decl uf_5 :: T1 +#12 := uf_5 +#22 := (uf_1 uf_5 uf_3) +#160 := (* -1::real #22) +#161 := (+ #6 #160) +#207 := (>= #161 0::real) +#222 := (not #207) +#206 := (= #6 #22) +#216 := (not #206) +#62 := (= #8 #22) +#70 := (not #62) +#217 := (iff #70 #216) +#214 := (iff #62 #206) +#212 := (iff #206 #62) +#213 := [monotonicity #40]: #212 +#215 := [symm #213]: #214 +#218 := [monotonicity #215]: #217 +#23 := (= #22 #8) +#24 := (not #23) +#71 := (iff #24 #70) +#68 := (iff #23 #62) +#69 := [rewrite]: #68 +#72 := [monotonicity #69]: #71 +#43 := [asserted]: #24 +#75 := [mp #43 #72]: #70 +#219 := [mp #75 #218]: #216 +#225 := (or #206 #222) +#162 := (<= #161 0::real) +#172 := (+ #8 #160) +#173 := (>= #172 0::real) +#178 := (not #173) +#163 := (not #162) +#181 := (or #163 #178) +#184 := (not #181) +#10 := (:var 0 T2) +#15 := (uf_1 uf_4 #10) +#149 := (pattern #15) +#13 := (uf_1 uf_5 #10) +#148 := (pattern #13) +#11 := (uf_1 uf_2 #10) +#147 := (pattern #11) +#50 := (* -1::real #15) +#51 := (+ #13 #50) +#52 := (<= #51 0::real) +#76 := (not #52) +#45 := (* -1::real #13) +#46 := (+ #11 #45) +#47 := (<= #46 0::real) +#78 := (not #47) +#73 := (or #78 #76) +#83 := (not #73) +#150 := (forall (vars (?x1 T2)) (:pat #147 #148 #149) #83) +#86 := (forall (vars (?x1 T2)) #83) +#153 := (iff #86 #150) +#151 := (iff #83 #83) +#152 := [refl]: #151 +#154 := [quant-intro #152]: #153 +#55 := (and #47 #52) +#58 := (forall (vars (?x1 T2)) #55) +#87 := (iff #58 #86) +#84 := (iff #55 #83) +#85 := [rewrite]: #84 +#88 := [quant-intro #85]: #87 +#79 := (~ #58 #58) +#81 := (~ #55 #55) +#82 := [refl]: #81 +#80 := [nnf-pos #82]: #79 +#16 := (<= #13 #15) +#14 := (<= #11 #13) +#17 := (and #14 #16) +#18 := (forall (vars (?x1 T2)) #17) +#59 := (iff #18 #58) +#56 := (iff #17 #55) +#53 := (iff #16 #52) +#54 := [rewrite]: #53 +#48 := (iff #14 #47) +#49 := [rewrite]: #48 +#57 := [monotonicity #49 #54]: #56 +#60 := [quant-intro #57]: #59 +#41 := [asserted]: #18 +#61 := [mp #41 #60]: #58 +#77 := [mp~ #61 #80]: #58 +#89 := [mp #77 #88]: #86 +#155 := [mp #89 #154]: #150 +#187 := (not #150) +#188 := (or #187 #184) +#157 := (+ #22 #156) +#158 := (<= #157 0::real) +#159 := (not #158) +#164 := (or #163 #159) +#165 := (not #164) +#189 := (or #187 #165) +#191 := (iff #189 #188) +#193 := (iff #188 #188) +#194 := [rewrite]: #193 +#185 := (iff #165 #184) +#182 := (iff #164 #181) +#179 := (iff #159 #178) +#176 := (iff #158 #173) +#166 := (+ #156 #22) +#169 := (<= #166 0::real) +#174 := (iff #169 #173) +#175 := [rewrite]: #174 +#170 := (iff #158 #169) +#167 := (= #157 #166) +#168 := [rewrite]: #167 +#171 := [monotonicity #168]: #170 +#177 := [trans #171 #175]: #176 +#180 := [monotonicity #177]: #179 +#183 := [monotonicity #180]: #182 +#186 := [monotonicity #183]: #185 +#192 := [monotonicity #186]: #191 +#195 := [trans #192 #194]: #191 +#190 := [quant-inst]: #189 +#196 := [mp #190 #195]: #188 +#220 := [unit-resolution #196 #155]: #184 +#197 := (or #181 #162) +#198 := [def-axiom]: #197 +#221 := [unit-resolution #198 #220]: #162 +#223 := (or #206 #163 #222) +#224 := [th-lemma]: #223 +#226 := [unit-resolution #224 #221]: #225 +#227 := [unit-resolution #226 #219]: #222 +#199 := (or #181 #173) +#200 := [def-axiom]: #199 +#228 := [unit-resolution #200 #220]: #173 +[th-lemma #228 #227 #211]: false +unsat +06d4133eb0950a5f12d22480aa2707e31af2b064 86 0 #2 := false #37 := 0::real decl uf_2 :: (-> T2 T1 real) @@ -3210,511 +3210,3 @@ #155 := [th-lemma]: #154 [unit-resolution #155 #60 #148 #144]: false unsat -V+IAyBZU/6QjYs6JkXx8LQ 57 0 -#2 := false -#4 := 0::real -decl uf_1 :: (-> T2 real) -decl uf_2 :: (-> T1 T1 T2) -decl uf_12 :: (-> T4 T1) -decl uf_4 :: T4 -#11 := uf_4 -#39 := (uf_12 uf_4) -decl uf_10 :: T4 -#27 := uf_10 -#38 := (uf_12 uf_10) -#40 := (uf_2 #38 #39) -#41 := (uf_1 #40) -#264 := (>= #41 0::real) -#266 := (not #264) -#43 := (= #41 0::real) -#44 := (not #43) -#131 := [asserted]: #44 -#272 := (or #43 #266) -#42 := (<= #41 0::real) -#130 := [asserted]: #42 -#265 := (not #42) -#270 := (or #43 #265 #266) -#271 := [th-lemma]: #270 -#273 := [unit-resolution #271 #130]: #272 -#274 := [unit-resolution #273 #131]: #266 -#6 := (:var 0 T1) -#5 := (:var 1 T1) -#7 := (uf_2 #5 #6) -#241 := (pattern #7) -#8 := (uf_1 #7) -#65 := (>= #8 0::real) -#242 := (forall (vars (?x1 T1) (?x2 T1)) (:pat #241) #65) -#66 := (forall (vars (?x1 T1) (?x2 T1)) #65) -#245 := (iff #66 #242) -#243 := (iff #65 #65) -#244 := [refl]: #243 -#246 := [quant-intro #244]: #245 -#149 := (~ #66 #66) -#151 := (~ #65 #65) -#152 := [refl]: #151 -#150 := [nnf-pos #152]: #149 -#9 := (<= 0::real #8) -#10 := (forall (vars (?x1 T1) (?x2 T1)) #9) -#67 := (iff #10 #66) -#63 := (iff #9 #65) -#64 := [rewrite]: #63 -#68 := [quant-intro #64]: #67 -#60 := [asserted]: #10 -#69 := [mp #60 #68]: #66 -#147 := [mp~ #69 #150]: #66 -#247 := [mp #147 #246]: #242 -#267 := (not #242) -#268 := (or #267 #264) -#269 := [quant-inst]: #268 -[unit-resolution #269 #247 #274]: false -unsat -vqiyJ/qjGXZ3iOg6xftiug 15 0 -uf_1 -> val!0 -uf_2 -> val!1 -uf_3 -> val!2 -uf_5 -> val!15 -uf_6 -> val!26 -uf_4 -> { - val!0 -> val!12 - val!1 -> val!13 - else -> val!13 -} -uf_7 -> { - val!6 -> val!31 - else -> val!31 -} -sat -mrZPJZyTokErrN6SYupisw 9 0 -uf_4 -> val!1 -uf_2 -> val!3 -uf_3 -> val!4 -uf_1 -> { - val!5 -> val!6 - val!4 -> val!7 - else -> val!7 -} -sat -qkVrmXMcHAG5MLuJ9d8jXQ 211 0 -#2 := false -#33 := 0::real -decl uf_11 :: (-> T5 T6 real) -decl uf_15 :: T6 -#28 := uf_15 -decl uf_16 :: T5 -#30 := uf_16 -#31 := (uf_11 uf_16 uf_15) -decl uf_12 :: (-> T7 T8 T5) -decl uf_14 :: T8 -#26 := uf_14 -decl uf_13 :: (-> T1 T7) -decl uf_8 :: T1 -#16 := uf_8 -#25 := (uf_13 uf_8) -#27 := (uf_12 #25 uf_14) -#29 := (uf_11 #27 uf_15) -#73 := -1::real -#84 := (* -1::real #29) -#85 := (+ #84 #31) -#74 := (* -1::real #31) -#75 := (+ #29 #74) -#112 := (>= #75 0::real) -#119 := (ite #112 #75 #85) -#127 := (* -1::real #119) -decl uf_17 :: T5 -#37 := uf_17 -#38 := (uf_11 uf_17 uf_15) -#102 := -1/3::real -#103 := (* -1/3::real #38) -#128 := (+ #103 #127) -#100 := 1/3::real -#101 := (* 1/3::real #31) -#129 := (+ #101 #128) -#130 := (<= #129 0::real) -#131 := (not #130) -#40 := 3::real -#39 := (- #31 #38) -#41 := (/ #39 3::real) -#32 := (- #29 #31) -#35 := (- #32) -#34 := (< #32 0::real) -#36 := (ite #34 #35 #32) -#42 := (< #36 #41) -#136 := (iff #42 #131) -#104 := (+ #101 #103) -#78 := (< #75 0::real) -#90 := (ite #78 #85 #75) -#109 := (< #90 #104) -#134 := (iff #109 #131) -#124 := (< #119 #104) -#132 := (iff #124 #131) -#133 := [rewrite]: #132 -#125 := (iff #109 #124) -#122 := (= #90 #119) -#113 := (not #112) -#116 := (ite #113 #85 #75) -#120 := (= #116 #119) -#121 := [rewrite]: #120 -#117 := (= #90 #116) -#114 := (iff #78 #113) -#115 := [rewrite]: #114 -#118 := [monotonicity #115]: #117 -#123 := [trans #118 #121]: #122 -#126 := [monotonicity #123]: #125 -#135 := [trans #126 #133]: #134 -#110 := (iff #42 #109) -#107 := (= #41 #104) -#93 := (* -1::real #38) -#94 := (+ #31 #93) -#97 := (/ #94 3::real) -#105 := (= #97 #104) -#106 := [rewrite]: #105 -#98 := (= #41 #97) -#95 := (= #39 #94) -#96 := [rewrite]: #95 -#99 := [monotonicity #96]: #98 -#108 := [trans #99 #106]: #107 -#91 := (= #36 #90) -#76 := (= #32 #75) -#77 := [rewrite]: #76 -#88 := (= #35 #85) -#81 := (- #75) -#86 := (= #81 #85) -#87 := [rewrite]: #86 -#82 := (= #35 #81) -#83 := [monotonicity #77]: #82 -#89 := [trans #83 #87]: #88 -#79 := (iff #34 #78) -#80 := [monotonicity #77]: #79 -#92 := [monotonicity #80 #89 #77]: #91 -#111 := [monotonicity #92 #108]: #110 -#137 := [trans #111 #135]: #136 -#72 := [asserted]: #42 -#138 := [mp #72 #137]: #131 -decl uf_1 :: T1 -#4 := uf_1 -#43 := (uf_13 uf_1) -#44 := (uf_12 #43 uf_14) -#45 := (uf_11 #44 uf_15) -#149 := (* -1::real #45) -#150 := (+ #38 #149) -#140 := (+ #93 #45) -#161 := (<= #150 0::real) -#168 := (ite #161 #140 #150) -#176 := (* -1::real #168) -#177 := (+ #103 #176) -#178 := (+ #101 #177) -#179 := (<= #178 0::real) -#180 := (not #179) -#46 := (- #45 #38) -#48 := (- #46) -#47 := (< #46 0::real) -#49 := (ite #47 #48 #46) -#50 := (< #49 #41) -#185 := (iff #50 #180) -#143 := (< #140 0::real) -#155 := (ite #143 #150 #140) -#158 := (< #155 #104) -#183 := (iff #158 #180) -#173 := (< #168 #104) -#181 := (iff #173 #180) -#182 := [rewrite]: #181 -#174 := (iff #158 #173) -#171 := (= #155 #168) -#162 := (not #161) -#165 := (ite #162 #150 #140) -#169 := (= #165 #168) -#170 := [rewrite]: #169 -#166 := (= #155 #165) -#163 := (iff #143 #162) -#164 := [rewrite]: #163 -#167 := [monotonicity #164]: #166 -#172 := [trans #167 #170]: #171 -#175 := [monotonicity #172]: #174 -#184 := [trans #175 #182]: #183 -#159 := (iff #50 #158) -#156 := (= #49 #155) -#141 := (= #46 #140) -#142 := [rewrite]: #141 -#153 := (= #48 #150) -#146 := (- #140) -#151 := (= #146 #150) -#152 := [rewrite]: #151 -#147 := (= #48 #146) -#148 := [monotonicity #142]: #147 -#154 := [trans #148 #152]: #153 -#144 := (iff #47 #143) -#145 := [monotonicity #142]: #144 -#157 := [monotonicity #145 #154 #142]: #156 -#160 := [monotonicity #157 #108]: #159 -#186 := [trans #160 #184]: #185 -#139 := [asserted]: #50 -#187 := [mp #139 #186]: #180 -#299 := (+ #140 #176) -#300 := (<= #299 0::real) -#290 := (= #140 #168) -#329 := [hypothesis]: #162 -#191 := (+ #29 #149) -#192 := (<= #191 0::real) -#51 := (<= #29 #45) -#193 := (iff #51 #192) -#194 := [rewrite]: #193 -#188 := [asserted]: #51 -#195 := [mp #188 #194]: #192 -#298 := (+ #75 #127) -#301 := (<= #298 0::real) -#284 := (= #75 #119) -#302 := [hypothesis]: #113 -#296 := (+ #85 #127) -#297 := (<= #296 0::real) -#285 := (= #85 #119) -#288 := (or #112 #285) -#289 := [def-axiom]: #288 -#303 := [unit-resolution #289 #302]: #285 -#304 := (not #285) -#305 := (or #304 #297) -#306 := [th-lemma]: #305 -#307 := [unit-resolution #306 #303]: #297 -#315 := (not #290) -#310 := (not #300) -#311 := (or #310 #112) -#308 := [hypothesis]: #300 -#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false -#312 := [lemma #309]: #311 -#322 := [unit-resolution #312 #302]: #310 -#316 := (or #315 #300) -#313 := [hypothesis]: #310 -#314 := [hypothesis]: #290 -#317 := [th-lemma]: #316 -#318 := [unit-resolution #317 #314 #313]: false -#319 := [lemma #318]: #316 -#323 := [unit-resolution #319 #322]: #315 -#292 := (or #162 #290) -#293 := [def-axiom]: #292 -#324 := [unit-resolution #293 #323]: #162 -#325 := [th-lemma #324 #307 #138 #302 #195]: false -#326 := [lemma #325]: #112 -#286 := (or #113 #284) -#287 := [def-axiom]: #286 -#330 := [unit-resolution #287 #326]: #284 -#331 := (not #284) -#332 := (or #331 #301) -#333 := [th-lemma]: #332 -#334 := [unit-resolution #333 #330]: #301 -#335 := [th-lemma #326 #334 #195 #329 #138]: false -#336 := [lemma #335]: #161 -#327 := [unit-resolution #293 #336]: #290 -#328 := [unit-resolution #319 #327]: #300 -[th-lemma #326 #334 #195 #328 #187 #138]: false -unsat -WrIjxhfF5EcRCmS6xKG3XQ 211 0 -#2 := false -#33 := 0::real -decl uf_11 :: (-> T5 T6 real) -decl uf_15 :: T6 -#28 := uf_15 -decl uf_16 :: T5 -#30 := uf_16 -#31 := (uf_11 uf_16 uf_15) -decl uf_12 :: (-> T7 T8 T5) -decl uf_14 :: T8 -#26 := uf_14 -decl uf_13 :: (-> T1 T7) -decl uf_8 :: T1 -#16 := uf_8 -#25 := (uf_13 uf_8) -#27 := (uf_12 #25 uf_14) -#29 := (uf_11 #27 uf_15) -#73 := -1::real -#84 := (* -1::real #29) -#85 := (+ #84 #31) -#74 := (* -1::real #31) -#75 := (+ #29 #74) -#112 := (>= #75 0::real) -#119 := (ite #112 #75 #85) -#127 := (* -1::real #119) -decl uf_17 :: T5 -#37 := uf_17 -#38 := (uf_11 uf_17 uf_15) -#102 := -1/3::real -#103 := (* -1/3::real #38) -#128 := (+ #103 #127) -#100 := 1/3::real -#101 := (* 1/3::real #31) -#129 := (+ #101 #128) -#130 := (<= #129 0::real) -#131 := (not #130) -#40 := 3::real -#39 := (- #31 #38) -#41 := (/ #39 3::real) -#32 := (- #29 #31) -#35 := (- #32) -#34 := (< #32 0::real) -#36 := (ite #34 #35 #32) -#42 := (< #36 #41) -#136 := (iff #42 #131) -#104 := (+ #101 #103) -#78 := (< #75 0::real) -#90 := (ite #78 #85 #75) -#109 := (< #90 #104) -#134 := (iff #109 #131) -#124 := (< #119 #104) -#132 := (iff #124 #131) -#133 := [rewrite]: #132 -#125 := (iff #109 #124) -#122 := (= #90 #119) -#113 := (not #112) -#116 := (ite #113 #85 #75) -#120 := (= #116 #119) -#121 := [rewrite]: #120 -#117 := (= #90 #116) -#114 := (iff #78 #113) -#115 := [rewrite]: #114 -#118 := [monotonicity #115]: #117 -#123 := [trans #118 #121]: #122 -#126 := [monotonicity #123]: #125 -#135 := [trans #126 #133]: #134 -#110 := (iff #42 #109) -#107 := (= #41 #104) -#93 := (* -1::real #38) -#94 := (+ #31 #93) -#97 := (/ #94 3::real) -#105 := (= #97 #104) -#106 := [rewrite]: #105 -#98 := (= #41 #97) -#95 := (= #39 #94) -#96 := [rewrite]: #95 -#99 := [monotonicity #96]: #98 -#108 := [trans #99 #106]: #107 -#91 := (= #36 #90) -#76 := (= #32 #75) -#77 := [rewrite]: #76 -#88 := (= #35 #85) -#81 := (- #75) -#86 := (= #81 #85) -#87 := [rewrite]: #86 -#82 := (= #35 #81) -#83 := [monotonicity #77]: #82 -#89 := [trans #83 #87]: #88 -#79 := (iff #34 #78) -#80 := [monotonicity #77]: #79 -#92 := [monotonicity #80 #89 #77]: #91 -#111 := [monotonicity #92 #108]: #110 -#137 := [trans #111 #135]: #136 -#72 := [asserted]: #42 -#138 := [mp #72 #137]: #131 -decl uf_1 :: T1 -#4 := uf_1 -#43 := (uf_13 uf_1) -#44 := (uf_12 #43 uf_14) -#45 := (uf_11 #44 uf_15) -#149 := (* -1::real #45) -#150 := (+ #38 #149) -#140 := (+ #93 #45) -#161 := (<= #150 0::real) -#168 := (ite #161 #140 #150) -#176 := (* -1::real #168) -#177 := (+ #103 #176) -#178 := (+ #101 #177) -#179 := (<= #178 0::real) -#180 := (not #179) -#46 := (- #45 #38) -#48 := (- #46) -#47 := (< #46 0::real) -#49 := (ite #47 #48 #46) -#50 := (< #49 #41) -#185 := (iff #50 #180) -#143 := (< #140 0::real) -#155 := (ite #143 #150 #140) -#158 := (< #155 #104) -#183 := (iff #158 #180) -#173 := (< #168 #104) -#181 := (iff #173 #180) -#182 := [rewrite]: #181 -#174 := (iff #158 #173) -#171 := (= #155 #168) -#162 := (not #161) -#165 := (ite #162 #150 #140) -#169 := (= #165 #168) -#170 := [rewrite]: #169 -#166 := (= #155 #165) -#163 := (iff #143 #162) -#164 := [rewrite]: #163 -#167 := [monotonicity #164]: #166 -#172 := [trans #167 #170]: #171 -#175 := [monotonicity #172]: #174 -#184 := [trans #175 #182]: #183 -#159 := (iff #50 #158) -#156 := (= #49 #155) -#141 := (= #46 #140) -#142 := [rewrite]: #141 -#153 := (= #48 #150) -#146 := (- #140) -#151 := (= #146 #150) -#152 := [rewrite]: #151 -#147 := (= #48 #146) -#148 := [monotonicity #142]: #147 -#154 := [trans #148 #152]: #153 -#144 := (iff #47 #143) -#145 := [monotonicity #142]: #144 -#157 := [monotonicity #145 #154 #142]: #156 -#160 := [monotonicity #157 #108]: #159 -#186 := [trans #160 #184]: #185 -#139 := [asserted]: #50 -#187 := [mp #139 #186]: #180 -#299 := (+ #140 #176) -#300 := (<= #299 0::real) -#290 := (= #140 #168) -#329 := [hypothesis]: #162 -#191 := (+ #29 #149) -#192 := (<= #191 0::real) -#51 := (<= #29 #45) -#193 := (iff #51 #192) -#194 := [rewrite]: #193 -#188 := [asserted]: #51 -#195 := [mp #188 #194]: #192 -#298 := (+ #75 #127) -#301 := (<= #298 0::real) -#284 := (= #75 #119) -#302 := [hypothesis]: #113 -#296 := (+ #85 #127) -#297 := (<= #296 0::real) -#285 := (= #85 #119) -#288 := (or #112 #285) -#289 := [def-axiom]: #288 -#303 := [unit-resolution #289 #302]: #285 -#304 := (not #285) -#305 := (or #304 #297) -#306 := [th-lemma]: #305 -#307 := [unit-resolution #306 #303]: #297 -#315 := (not #290) -#310 := (not #300) -#311 := (or #310 #112) -#308 := [hypothesis]: #300 -#309 := [th-lemma #308 #307 #138 #302 #187 #195]: false -#312 := [lemma #309]: #311 -#322 := [unit-resolution #312 #302]: #310 -#316 := (or #315 #300) -#313 := [hypothesis]: #310 -#314 := [hypothesis]: #290 -#317 := [th-lemma]: #316 -#318 := [unit-resolution #317 #314 #313]: false -#319 := [lemma #318]: #316 -#323 := [unit-resolution #319 #322]: #315 -#292 := (or #162 #290) -#293 := [def-axiom]: #292 -#324 := [unit-resolution #293 #323]: #162 -#325 := [th-lemma #324 #307 #138 #302 #195]: false -#326 := [lemma #325]: #112 -#286 := (or #113 #284) -#287 := [def-axiom]: #286 -#330 := [unit-resolution #287 #326]: #284 -#331 := (not #284) -#332 := (or #331 #301) -#333 := [th-lemma]: #332 -#334 := [unit-resolution #333 #330]: #301 -#335 := [th-lemma #326 #334 #195 #329 #138]: false -#336 := [lemma #335]: #161 -#327 := [unit-resolution #293 #336]: #290 -#328 := [unit-resolution #319 #327]: #300 -[th-lemma #326 #334 #195 #328 #187 #138]: false -unsat diff -r fcd02244e63d -r 7a86d7706106 src/HOL/SMT/Examples/SMT_Examples.certs --- a/src/HOL/SMT/Examples/SMT_Examples.certs Wed Mar 24 14:03:52 2010 +0100 +++ b/src/HOL/SMT/Examples/SMT_Examples.certs Wed Mar 24 14:08:07 2010 +0100 @@ -1,4 +1,4 @@ -Fg1W6egjwo9zhhAmUXOW+w 8 0 +bb06851c317eb8b672e27364b0ae34a4e39eb880 8 0 #2 := false #1 := true #4 := (not true) @@ -7,7 +7,7 @@ #20 := [asserted]: #4 [mp #20 #22]: false unsat -2+cndY9nzS72l7VvBCGRAw 19 0 +70d1f77bec207467bc0306af0d98a71fa8328274 19 0 #2 := false decl up_1 :: bool #4 := up_1 @@ -27,7 +27,7 @@ #23 := [asserted]: #7 [mp #23 #32]: false unsat -0vJQrobUDcQ9PkGJO8aM8g 25 0 +148012a9e9d44fe30a0c79e3344bdb805124f661 25 0 #2 := false decl up_1 :: bool #4 := up_1 @@ -53,7 +53,7 @@ #23 := [asserted]: #7 [mp #23 #38]: false unsat -AGGnpwEv208Vqxly7wTWHA 38 0 +bc9a25b7f6dc3ac2431ee71b6e71c5a7b25e89d1 38 0 #2 := false decl up_2 :: bool #5 := up_2 @@ -92,9 +92,9 @@ #30 := [and-elim #31]: #6 [mp #30 #52]: false unsat -wakXeIy1uoPgglzOQGFhJQ 1 0 -unsat -cpSlDe0l7plVktRNxGU5dA 71 0 +9b3db6ce34c8a1806160f1349b898b6c5ca40ba0 1 0 +unsat +912e9b7fb52f4a71d232354b3bb53c11e5a41ccd 71 0 #2 := false decl up_1 :: bool #4 := up_1 @@ -166,7 +166,7 @@ #31 := [asserted]: #15 [mp #31 #82]: false unsat -pg19mjJfV75T2QDrgWd4JA 57 0 +4d063d3cdf6657ddb4258379f900ef18e9042978 57 0 #2 := false decl up_1 :: bool #4 := up_1 @@ -224,7 +224,7 @@ #30 := [asserted]: #14 [mp #30 #70]: false unsat -Mj1B8X1MaN7xU/W4Kz3FoQ 194 0 +c6eb111aa830c9669a030c2e58b4e827706981da 194 0 #2 := false decl up_1 :: bool #4 := up_1 @@ -419,7 +419,7 @@ #237 := [mp #83 #236]: #75 [mp #237 #247]: false unsat -JkhYJB8FDavTZkizO1/9IA 52 0 +42890f9fa7c18237798ca55d0cf9dfff6f2f868a 52 0 #2 := false decl uf_1 :: (-> T1 T1 T1) decl uf_2 :: T1 @@ -472,7 +472,7 @@ #113 := [quant-inst]: #199 [unit-resolution #113 #536 #49]: false unsat -0ZdSZH2DbtjHNTyrDkZmXg 1667 0 +94169ba151f7a720e818287ce490015dde764bad 1667 0 #2 := false decl up_54 :: bool #126 := up_54 @@ -2140,7 +2140,7 @@ #2371 := [unit-resolution #891 #2369]: #166 [unit-resolution #2159 #2371 #2370 #2358 #2357]: false unsat -R3pmBDBlU9XdUrxJXhj7nA 78 0 +d8841d120b7cf772be783d793f759fb6353b9fcd 78 0 #2 := false decl up_1 :: (-> int bool) decl ?x1!0 :: int @@ -2219,7 +2219,7 @@ #82 := [and-elim #81]: #55 [unit-resolution #82 #95]: false unsat -IBRj/loev6P6r0J+HOit6A 135 0 +18bde40beb0dd1fc2613a67805e24d767dd9a3bf 135 0 #2 := false decl up_1 :: (-> T1 T2 bool) #5 := (:var 0 T2) @@ -2355,7 +2355,7 @@ #176 := [quant-inst]: #538 [unit-resolution #176 #252 #535]: false unsat -72504KVBixGB/87pOYiU/A 135 2 +013861f683c286a3ef38681266913846a3a39b9a 135 2 #2 := false decl up_1 :: (-> T1 T2 bool) #5 := (:var 0 T2) @@ -2493,7 +2493,7 @@ unsat WARNING: failed to find a pattern for quantifier (quantifier id: k!12) -RaQLz4GxtUICnOD5WoYnzQ 56 0 +0e958e27514643bb596851e6dbb61a23f6b348b0 56 0 #2 := false decl up_1 :: (-> T1 bool) decl uf_2 :: T1 @@ -2550,7 +2550,7 @@ #120 := [quant-inst]: #206 [unit-resolution #120 #542 #41]: false unsat -NPQIgVPhSpgSLeS+u/EatQ 17 0 +6ecefa4023d224e6c51226d5bee17e2a19cc4333 17 0 #2 := false #4 := 3::int #5 := (= 3::int 3::int) @@ -2568,7 +2568,7 @@ #22 := [asserted]: #6 [mp #22 #31]: false unsat -Lc9NwVtwY2Wo0G7UbFD1oA 17 0 +5e0256133fc82f0e2fea6597b863483e4e61d3c6 17 0 #2 := false #4 := 3::real #5 := (= 3::real 3::real) @@ -2586,7 +2586,7 @@ #22 := [asserted]: #6 [mp #22 #31]: false unsat -pYVrUflpYrrZEWALJDnvPw 26 0 +55cf32b061b843ac5bcaefb74005a7dd3a24386f 26 0 #2 := false #7 := 4::int #5 := 1::int @@ -2613,7 +2613,7 @@ #25 := [asserted]: #9 [mp #25 #40]: false unsat -FIqzVlbN8RT0iWarmBEpjw 41 0 +e81d17ec85af9db5ec6ba5bf4ced62daaa719ef3 41 0 #2 := false decl uf_1 :: int #4 := uf_1 @@ -2655,7 +2655,7 @@ #28 := [asserted]: #12 [mp #28 #52]: false unsat -HWVNtxMa8xktQsg8pHG+1w 35 0 +448f188ebf9d7fbd2920c0a51a8f105192e6af1a 35 0 #2 := false #5 := 3::int #6 := 8::int @@ -2691,7 +2691,7 @@ #26 := [asserted]: #10 [mp #26 #51]: false unsat -M71YYpEc8u/aEIH3MOQrcg 250 0 +c3751ecae7701923f4ba6a90c6c6eee35ee1b13d 250 0 #2 := false #7 := 0::real decl uf_2 :: real @@ -2942,7 +2942,7 @@ #294 := [unit-resolution #190 #293]: #188 [th-lemma #280 #294]: false unsat -G00bTqBjtW66EmwIZbXbOg 124 0 +8e6af261ea9f94b967813d4e2f2abcb94463d612 124 0 #2 := false decl uf_1 :: (-> T1 T2) decl uf_3 :: T1 @@ -3067,7 +3067,7 @@ #34 := [asserted]: #11 [unit-resolution #34 #536]: false unsat -6QdzkSy/RtEjUu+wUKIKqA 54 0 +243524c591f6dcfe16a79ddd249c64a337ff3612 54 0 #2 := false #9 := 1::int decl uf_1 :: int @@ -3122,7 +3122,7 @@ #28 := [asserted]: #12 [mp #28 #67]: false unsat -xoSwaSeELbR0PHe0zb/BSg 63 0 +adfe7d6c2da6653191952bd9673c1274f94c2ab2 63 0 #2 := false #11 := 0::int decl uf_2 :: int @@ -3186,7 +3186,7 @@ #76 := [mp #52 #75]: #63 [mp #76 #84]: false unsat -ciHqmDSmPpA15rO932dhvA 35 0 +3440e29713ba625633b10a2c4fdc186cb6e0cf3e 35 0 #2 := false #6 := 5::int #4 := 2::int @@ -3222,7 +3222,7 @@ #25 := [asserted]: #9 [mp #25 #49]: false unsat -HzwFy7SRHqpspkYnzyeF4w 45 0 +5f3503ae4a43341932052006638f286bea551e87 45 0 #2 := false #11 := 4::real decl uf_2 :: real @@ -3268,7 +3268,7 @@ #60 := [mp #36 #59]: #51 [th-lemma #60 #47 #38]: false unsat -XW7QIWmzYjfQXaHHPc98eA 59 0 +347776ce17d7d3f6d1252ead05795e4eee6f4b20 59 0 #2 := false #16 := (not false) decl uf_2 :: int @@ -3328,94 +3328,7 @@ #34 := [asserted]: #18 [mp #34 #71]: false unsat -ZGL00TLLioiLlWFiXUnbxg 86 0 -#2 := false -decl uf_1 :: int -#5 := uf_1 -#7 := 2::int -#29 := (* 2::int uf_1) -#4 := 0::int -#54 := (= 0::int #29) -#55 := (not #54) -#61 := (= #29 0::int) -#104 := (not #61) -#110 := (iff #104 #55) -#108 := (iff #61 #54) -#109 := [commutativity]: #108 -#111 := [monotonicity #109]: #110 -#62 := (<= #29 0::int) -#100 := (not #62) -#30 := (<= uf_1 0::int) -#31 := (not #30) -#6 := (< 0::int uf_1) -#32 := (iff #6 #31) -#33 := [rewrite]: #32 -#27 := [asserted]: #6 -#34 := [mp #27 #33]: #31 -#101 := (or #100 #30) -#102 := [th-lemma]: #101 -#103 := [unit-resolution #102 #34]: #100 -#105 := (or #104 #62) -#106 := [th-lemma]: #105 -#107 := [unit-resolution #106 #103]: #104 -#112 := [mp #107 #111]: #55 -#56 := (= uf_1 #29) -#57 := (not #56) -#53 := (= 0::int uf_1) -#50 := (not #53) -#58 := (and #50 #55 #57) -#69 := (not #58) -#42 := (distinct 0::int uf_1 #29) -#47 := (not #42) -#9 := (- uf_1 uf_1) -#8 := (* uf_1 2::int) -#10 := (distinct uf_1 #8 #9) -#11 := (not #10) -#48 := (iff #11 #47) -#45 := (iff #10 #42) -#39 := (distinct uf_1 #29 0::int) -#43 := (iff #39 #42) -#44 := [rewrite]: #43 -#40 := (iff #10 #39) -#37 := (= #9 0::int) -#38 := [rewrite]: #37 -#35 := (= #8 #29) -#36 := [rewrite]: #35 -#41 := [monotonicity #36 #38]: #40 -#46 := [trans #41 #44]: #45 -#49 := [monotonicity #46]: #48 -#28 := [asserted]: #11 -#52 := [mp #28 #49]: #47 -#80 := (or #42 #69) -#81 := [def-axiom]: #80 -#82 := [unit-resolution #81 #52]: #69 -#59 := (= uf_1 0::int) -#83 := (not #59) -#89 := (iff #83 #50) -#87 := (iff #59 #53) -#88 := [commutativity]: #87 -#90 := [monotonicity #88]: #89 -#84 := (or #83 #30) -#85 := [th-lemma]: #84 -#86 := [unit-resolution #85 #34]: #83 -#91 := [mp #86 #90]: #50 -#64 := -1::int -#65 := (* -1::int #29) -#66 := (+ uf_1 #65) -#68 := (>= #66 0::int) -#92 := (not #68) -#93 := (or #92 #30) -#94 := [th-lemma]: #93 -#95 := [unit-resolution #94 #34]: #92 -#96 := (or #57 #68) -#97 := [th-lemma]: #96 -#98 := [unit-resolution #97 #95]: #57 -#76 := (or #58 #53 #54 #56) -#77 := [def-axiom]: #76 -#99 := [unit-resolution #77 #98 #91 #82]: #54 -[unit-resolution #99 #112]: false -unsat -DWt5rIK6NWlI4vrw+691Zg 212 0 +f7b1b99e3470f713e48aaae1336ace10223be6f0 212 0 #2 := false decl uf_4 :: T1 #13 := uf_4 @@ -3628,7 +3541,94 @@ #519 := [unit-resolution #521 #518]: #547 [unit-resolution #519 #522]: false unsat -PaSeDRf7Set5ywlblDOoTg 673 0 +bf36938883aa38907d4d00c1860a1d18e7b620d0 86 0 +#2 := false +decl uf_1 :: int +#5 := uf_1 +#7 := 2::int +#29 := (* 2::int uf_1) +#4 := 0::int +#54 := (= 0::int #29) +#55 := (not #54) +#61 := (= #29 0::int) +#104 := (not #61) +#110 := (iff #104 #55) +#108 := (iff #61 #54) +#109 := [commutativity]: #108 +#111 := [monotonicity #109]: #110 +#62 := (<= #29 0::int) +#100 := (not #62) +#30 := (<= uf_1 0::int) +#31 := (not #30) +#6 := (< 0::int uf_1) +#32 := (iff #6 #31) +#33 := [rewrite]: #32 +#27 := [asserted]: #6 +#34 := [mp #27 #33]: #31 +#101 := (or #100 #30) +#102 := [th-lemma]: #101 +#103 := [unit-resolution #102 #34]: #100 +#105 := (or #104 #62) +#106 := [th-lemma]: #105 +#107 := [unit-resolution #106 #103]: #104 +#112 := [mp #107 #111]: #55 +#56 := (= uf_1 #29) +#57 := (not #56) +#53 := (= 0::int uf_1) +#50 := (not #53) +#58 := (and #50 #55 #57) +#69 := (not #58) +#42 := (distinct 0::int uf_1 #29) +#47 := (not #42) +#9 := (- uf_1 uf_1) +#8 := (* uf_1 2::int) +#10 := (distinct uf_1 #8 #9) +#11 := (not #10) +#48 := (iff #11 #47) +#45 := (iff #10 #42) +#39 := (distinct uf_1 #29 0::int) +#43 := (iff #39 #42) +#44 := [rewrite]: #43 +#40 := (iff #10 #39) +#37 := (= #9 0::int) +#38 := [rewrite]: #37 +#35 := (= #8 #29) +#36 := [rewrite]: #35 +#41 := [monotonicity #36 #38]: #40 +#46 := [trans #41 #44]: #45 +#49 := [monotonicity #46]: #48 +#28 := [asserted]: #11 +#52 := [mp #28 #49]: #47 +#80 := (or #42 #69) +#81 := [def-axiom]: #80 +#82 := [unit-resolution #81 #52]: #69 +#59 := (= uf_1 0::int) +#83 := (not #59) +#89 := (iff #83 #50) +#87 := (iff #59 #53) +#88 := [commutativity]: #87 +#90 := [monotonicity #88]: #89 +#84 := (or #83 #30) +#85 := [th-lemma]: #84 +#86 := [unit-resolution #85 #34]: #83 +#91 := [mp #86 #90]: #50 +#64 := -1::int +#65 := (* -1::int #29) +#66 := (+ uf_1 #65) +#68 := (>= #66 0::int) +#92 := (not #68) +#93 := (or #92 #30) +#94 := [th-lemma]: #93 +#95 := [unit-resolution #94 #34]: #92 +#96 := (or #57 #68) +#97 := [th-lemma]: #96 +#98 := [unit-resolution #97 #95]: #57 +#76 := (or #58 #53 #54 #56) +#77 := [def-axiom]: #76 +#99 := [unit-resolution #77 #98 #91 #82]: #54 +[unit-resolution #99 #112]: false +unsat +9791139ea2cfda88ae799477fc61e411aab42b18 673 0 #2 := false #169 := 0::int decl uf_2 :: int @@ -4302,7 +4302,7 @@ #410 := [mp #349 #409]: #405 [unit-resolution #410 #710 #709 #697 #706]: false unsat -U7jSPEM53XYq3qs03aUczw 2291 0 +0d07e457c5602ba4a5dc70af32b6dc53a80a858c 2291 0 #2 := false #6 := 0::int decl z3name!0 :: int @@ -6594,7 +6594,7 @@ #2323 := [unit-resolution #918 #2322]: #100 [unit-resolution #917 #2323 #2318]: false unsat -eqE7IAqFr0UIBuUsVDgHvw 52 0 +258b6cd4609a61b7800235c7f356739cfb8996c5 52 0 #2 := false #8 := 1::real decl uf_1 :: real @@ -6647,7 +6647,7 @@ #29 := [asserted]: #13 [mp #29 #65]: false unsat -ADs4ZPiuUr7Xu7tk71NnEw 59 0 +3d1d0473f97c11d6c4d10f6e0313b2e2f4aac879 59 0 #2 := false #55 := 0::int #7 := 2::int @@ -6707,7 +6707,7 @@ #144 := [unit-resolution #143 #28]: #58 [unit-resolution #144 #68]: false unsat -x2NmsblNl28xPXP2EG22rA 54 0 +f768cbe713eb8031e45b1a78d0f49a07f5398eb8 54 0 #2 := false #5 := 2::int decl uf_1 :: int @@ -6762,7 +6762,7 @@ #139 := [unit-resolution #138 #27]: #127 [unit-resolution #139 #62]: false unsat -kfLiOGBz3RZx9wt+FS+hfg 118 0 +2c2bcacfbe018175dd39ce04dd5cbe02c800a0dd 118 0 #2 := false #5 := 0::real decl uf_1 :: real @@ -6881,7 +6881,7 @@ #126 := [mp #101 #125]: #115 [unit-resolution #126 #132 #129]: false unsat -FPTJq9aN3ES4iIrHgaTv+A 208 0 +c8ed8eae868ac61c8f3a616f1b0b1df4032f4eac 208 0 #2 := false #9 := 0::int #11 := 4::int @@ -7090,7 +7090,7 @@ #418 := [unit-resolution #417 #36]: #298 [th-lemma #418 #415 #412 #411 #99 #400 #397 #396]: false unsat -yN0aj3KferzvOSp2KlyNwg 24 0 +7beaddc803d2c23197634dc63d56d564292d85fe 24 0 #2 := false #4 := (exists (vars (?x1 int)) false) #5 := (not #4) @@ -7115,7 +7115,7 @@ #22 := [asserted]: #6 [mp #22 #38]: false unsat -7iMPasu6AIeHm45slLCByA 24 0 +723fcd1ecb9fa59a7e0fede642f23063fb499818 24 0 #2 := false #4 := (exists (vars (?x1 real)) false) #5 := (not #4) @@ -7140,13 +7140,13 @@ #22 := [asserted]: #6 [mp #22 #38]: false unsat -cv2pC2I0gIUYtVwtXngvXg 1 0 -unsat -4r8/IxBBDH1ZqF0YfzLLTg 1 0 -unsat -uj7n+C4nG462DNJy9Divrg 1 0 -unsat -dn/LVwy1BXEOmtqdUBNhLw 73 0 +a72d0e977596e1fac0cccee600f0bf9d29ed71aa 1 0 +unsat +70141a690f46561f859d3deed80b9611816f9f81 1 0 +unsat +41b6ddffa2c7efc9285d0e0a65d74c4325ef6ddb 1 0 +unsat +a08fcdd29520930b0a940df57c3d8266dbefd10f 73 0 #2 := false #5 := 0::int #8 := 1::int @@ -7220,7 +7220,7 @@ #144 := [trans #142 #82]: #143 [mp #144 #146]: false unsat -VzZ1W5SEEis1AJp1qZz86g 82 0 +470993954e986ab72716000fd7da9fa600b05225 82 0 #2 := false #5 := (:var 0 int) #7 := 0::int @@ -7303,7 +7303,7 @@ #30 := [asserted]: #14 [mp #30 #96]: false unsat -UoXgZh5LkmyNCmQEfEtnig 78 0 +40c93af1a084932780f95bda03b3df7712e01201 78 0 #2 := false #5 := (:var 0 int) #7 := 2::int @@ -7382,7 +7382,7 @@ #31 := [asserted]: #15 [mp #31 #92]: false unsat -Qv4gVhCmOzC39uufV9ZpDA 61 0 +26b175ea54cef59293a917c6fb083751b00d312a 61 0 #2 := false #9 := (:var 0 int) #4 := 2::int @@ -7444,7 +7444,7 @@ #30 := [asserted]: #14 [mp #30 #75]: false unsat -+j+tSj7aUImWej2XcTL9dw 111 0 +74037c10b4f126275ba21e7140b7f1e159b39ed9 111 0 #2 := false #4 := 2::int decl ?x1!1 :: int @@ -7556,7 +7556,7 @@ #184 := [th-lemma]: #183 [unit-resolution #184 #127 #125 #126]: false unsat -kQRsBd9oowc7exsvsEgTUg 89 0 +628c1b88ca8fb09c896ae05059a52dc2f8e25db2 89 0 #2 := false #4 := 0::int decl ?x1!0 :: int @@ -7646,7 +7646,7 @@ #167 := [unit-resolution #154 #90]: #166 [unit-resolution #167 #165 #162]: false unsat -VPjD8BtzPcTZKIRT4SA3Nw 83 2 +b7c4f9440c4594c46eee14ce57f17610bb7e2536 83 2 #2 := false #5 := 0::int #4 := (:var 0 int) @@ -7732,7 +7732,7 @@ unsat WARNING: failed to find a pattern for quantifier (quantifier id: k!2) -DCV5zpDW3cC2A61VghqFkA 180 2 +7a9cc3ee85422788d981af84d181bd61d65f774c 180 2 #2 := false #4 := 0::int #5 := (:var 0 int) @@ -7915,7 +7915,7 @@ unsat WARNING: failed to find a pattern for quantifier (quantifier id: k!2) -lYXJpXHB9nLXJbOsr9VH1w 68 0 +5201b12abd6b3d0f247a34c1fd9f443fc951c55f 68 0 #2 := false #12 := 1::int #9 := (:var 1 int) @@ -7984,7 +7984,7 @@ #32 := [asserted]: #16 [mp #32 #83]: false unsat -jNvpOd8qnh73F8B6mQDrRw 107 0 +0f9091dc6853772b5280c29fc11ae1382022f24d 107 0 #2 := false #4 := 0::int decl ?x2!1 :: int @@ -8092,7 +8092,7 @@ #123 := [and-elim #101]: #88 [th-lemma #123 #124 #125]: false unsat -QWWPBUGjgvTCpxqJ9oPGdQ 117 0 +a19e2cec45cb985989328595a0e06836a1e0fbc3 117 0 #2 := false #4 := 0::int decl ?x2!1 :: int @@ -8210,7 +8210,7 @@ #188 := [unit-resolution #187 #110]: #98 [unit-resolution #188 #130]: false unsat -3r4MsKEvDJc1RWnNRxu/3Q 148 0 +34bf666106f50c4ee2e8834de4912d59c6e7d9d9 148 0 #2 := false #144 := (not false) #7 := 0::int @@ -8359,7 +8359,7 @@ #158 := [mp #126 #157]: #153 [mp #158 #181]: false unsat -Q+cnHyqIFLGWsSlQkp3fEg 67 0 +1d6946d9384f22b76e98f04aff657c54e4fe51ad 67 0 #2 := false #4 := (:var 0 int) #5 := (pattern #4) @@ -8427,9 +8427,9 @@ #30 := [asserted]: #14 [mp #30 #80]: false unsat -Q7HDzu4ER2dw+lHHM6YgFg 1 0 -unsat -saejIG5KeeVxOolEIo3gtw 75 0 +d938f8b556e86b20a82e4661e3a61bad7d95357d 1 0 +unsat +dfca84a72c9a54145743ea34eaa7c75e8665fd45 75 0 #2 := false #6 := 1::int decl uf_3 :: int @@ -8505,7 +8505,7 @@ #32 := [asserted]: #16 [mp #32 #86]: false unsat -PPaoU5CzQFYr3LRpOsGPhQ 62 0 +2662a556257bfe403cd3fda75e9fe55964bc9dcd 62 0 #2 := false decl uf_2 :: real #6 := uf_2 @@ -8568,7 +8568,7 @@ #32 := [asserted]: #16 [mp #32 #74]: false unsat -hXKzem5+KYZMOj+GKxjszQ 141 0 +99d65e323e3d85dbdc2d8c52c169db4d46ead198 141 0 #2 := false decl uf_4 :: int #9 := uf_4 @@ -8710,7 +8710,7 @@ #45 := [asserted]: #29 [mp #45 #150]: false unsat -3D8WhjZTO7T824d7mwXcCA 252 0 +2e721ab2035f9845f1e87e78db6dfc67c28f6d40 252 0 #2 := false #9 := 0::int decl uf_2 :: (-> T1 int) @@ -8963,7 +8963,7 @@ #539 := [unit-resolution #532 #451]: #557 [th-lemma #455 #539 #537 #546]: false unsat -kyphS4o71h68g2YhvYbQQQ 223 0 +5d4787d5f6bf7b62bda1a48bdd01dc6863801852 223 0 #2 := false #23 := 3::int decl uf_2 :: (-> T1 int) @@ -9187,7 +9187,7 @@ #598 := [unit-resolution #593 #596]: #623 [th-lemma #152 #598 #139]: false unsat -M8P5WxpiY5AWxaJDBtXoLQ 367 0 +60689c41168db239dbf5f3a98d5f2bce0fef9e02 367 0 #2 := false #9 := 0::int decl uf_2 :: (-> T1 int) @@ -9555,7 +9555,7 @@ #456 := [th-lemma]: #455 [unit-resolution #456 #464 #452]: false unsat -Xs4JZCKb5egkcPabsrodXg 302 0 +94b7ba760bb9dd467688fc28632e0ae8f6f51951 302 0 #2 := false #9 := 0::int decl uf_2 :: (-> T1 int) @@ -9858,7 +9858,7 @@ #601 := [unit-resolution #615 #613]: #683 [th-lemma #623 #188 #601 #628]: false unsat -clMAi2WqMi360EjFURRGLg 458 0 +8d2fca14b1477934a0c7f4f6528bd3be029bba7b 458 0 #2 := false #9 := 0::int decl uf_2 :: (-> T1 int) @@ -10317,7 +10317,7 @@ #350 := [unit-resolution #369 #367]: #368 [unit-resolution #350 #323]: false unsat -mu7O1os0t3tPqWZhwizjxw 161 0 +720080123967f7b12d5ac9ba2a5e5203400a16cd 161 0 #2 := false #9 := 0::int decl uf_3 :: int @@ -10479,7 +10479,7 @@ #361 := [unit-resolution #639 #655]: #647 [th-lemma #656 #361 #261]: false unsat -08cmOtIT4NYs2PG/F3zeZw 557 0 +980ba021fe0853c3aa46377383e3f0f6fa9e2888 557 0 #2 := false #9 := 0::int decl uf_2 :: (-> T1 int) @@ -11037,57 +11037,57 @@ #990 := [unit-resolution #501 #807]: #511 [unit-resolution #990 #989 #979]: false unsat -8HdmSMHHP2B8XMFzjNuw5Q 1 0 -unsat -O4aM0+/isn2q5CrIefZjzg 1 0 -unsat -t/ni9djl2DqxH0iKupZSwg 1 0 -unsat -RumBGekdxZQaBF1HNa3x9w 1 0 -unsat -Q9d+IbQ8chjKld71X6/zqw 1 0 -unsat -PhC8zQV8hnJ6E2YYjZPGjQ 1 0 -unsat -mieI2RhSp3bYaojlWH1A4A 1 0 -unsat -pRSV6nBLconzrQz2zUrJ6g 1 0 -unsat -Js0JfdwDoKq3YuilPPgeZw 1 0 -unsat -GRIqjLUJiqXbo+pXhAeKIw 1 0 -unsat -Bg5scsmPFp82+7Y2ScL6Wg 1 0 -unsat -XD6zX6850dLxyfZSfNv30A 1 0 -unsat -BG/HwJYnumvDICXxtBu/tA 1 0 -unsat -YMc4t19sUMWbUkx3woxCmQ 1 0 -unsat -YyD9IF72pKXGGKZTO7FY5Q 1 0 -unsat -zRPsIUi+TEoz5fPWP0H9bQ 1 0 -unsat -8ipTE8BOXpvSo/U6D4p3lA 1 0 -unsat -MSzQywedZPsOE0CDxrrO0g 1 0 -unsat -SryZuXv48ItET8NPIv07pA 1 0 -unsat -qOMUQN18hYFl/wWt54lvbA 1 0 -unsat -+njWXdn6fETK3/AjtiHjcA 1 0 -unsat -5cQ7gJ33gzYTIIPA3hbBmQ 1 0 -unsat -ZznT34cvumrP00mXZ3gcjw 1 0 -unsat -//LQca1Et5RfhQJZA+CGCA 1 0 -unsat -3ntxKz+kaQNfTrLzY9sVXw 1 0 -unsat -4lL2Qo8ngE1EH1UdeN1Qng 43 0 +22877b17eafaba69b1f8a961a616fea28ae70d56 1 0 +unsat +b5839159097bbd4e601a5681d1ca3493ec994a7c 1 0 +unsat +90e1074350b5dcaae149781bcaa5d643b2ca9f48 1 0 +unsat +08c7117fe974f5767051ed5aa61a27ce3084eb1d 1 0 +unsat +858012417c9d327d8997f2a5dcb3da095ec65d34 1 0 +unsat +84b2eee4890eaadb3638c7e522fb3237b3d476b0 1 0 +unsat +8867717d9736308a2c27df0665a6e391b0562076 1 0 +unsat +cd79c9a0488ab597d08dd9a0d6ac0f3647003bd6 1 0 +unsat +395dd6c10b2a432137f9e3401cba8ec4dd64911b 1 0 +unsat +17e3cc9534e04d86f095ec1a92c77d46d7dbb8e5 1 0 +unsat +e046ea79beacf4bc3567b3b7f755232369d0c185 1 0 +unsat +8ce4235464829d4be72e682f0c72bc5e3c6902d0 1 0 +unsat +656a40b977d7716264443900d6bdb4d3d117d52f 1 0 +unsat +ec27a57e58719625ff71dd4d68ed53a3851efb5c 1 0 +unsat +2c3c366b8488ca0991cc767c94cdb78b18db9d5f 1 0 +unsat +5894f6f19250b12885e38f54eae81f143b58fa01 1 0 +unsat +e150815d9eb1ec168805b5501d7f4b2e378dd883 1 0 +unsat +396d6254e993f414335de9378150e486d3cfcd4e 1 0 +unsat +96014c61f582a811aff25ad7fa62b575b830fa8b 1 0 +unsat +10580b87c0d062c9854e79d16047a53d045ccfac 1 0 +unsat +87b5f388df1f43cc02ac0fa0d6944eb8cd8f8f50 1 0 +unsat +92a5e2bb68f74b9e7dd3a9ef79ea641e9700d563 1 0 +unsat +152e0f0f0a04b399b057beae92ae0455408b224f 1 0 +unsat +41925af4711748a6e411453f2465920a1c6ffb8e 1 0 +unsat +757462716f4a2619a1410bdca3faa2d058042c10 1 0 +unsat +abdeeb4668a63f19473d6da94232379344d99fea 43 0 #2 := false #6 := 0::int decl uf_1 :: (-> bv[2] int) @@ -11131,9 +11131,9 @@ #287 := [th-lemma]: #627 [unit-resolution #287 #47 #635]: false unsat -+xe3O927LrflFUE6NDqRlA 1 0 -unsat -JPoL7fPYhqhAkjUiVF+THQ 50 0 +2e4bd6e1ab7bfedbefd3ada8caf5332ba5651065 1 0 +unsat +96d2e1aad559535e781a07ee5e55bb19caef769c 50 0 #2 := false decl uf_6 :: T2 #23 := uf_6 @@ -11184,7 +11184,7 @@ #66 := [asserted]: #26 [unit-resolution #66 #235]: false unsat -l23ZDmd0VbO/Q+uO5EtabA 105 0 +008ad82b0a62ff600e66e8f2cc72b5795c7c5032 105 0 #2 := false decl uf_6 :: (-> T4 T2) decl uf_10 :: T4 @@ -11290,7 +11290,7 @@ #110 := [asserted]: #46 [unit-resolution #110 #238]: false unsat -GZjffeZPQnL3OyLCvxdCpg 181 0 +0a15a60660bc0c3f06688ad5de50ed50a24d0df0 181 0 #2 := false decl uf_1 :: (-> T1 T2 T3) decl uf_3 :: T2 @@ -11472,7 +11472,7 @@ #76 := [asserted]: #38 [unit-resolution #76 #489]: false unsat -i6jCzzRosHYE0w7sF1Nraw 62 0 +dde2364f13fc9ce8af00c7a02bfea9a6c979a805 62 0 #2 := false decl up_4 :: (-> T1 T2 bool) decl uf_3 :: T2 @@ -11535,7 +11535,7 @@ #73 := [unit-resolution #71 #68]: #72 [unit-resolution #73 #59 #61]: false unsat -YZHSyhN2TGlpe+vpkzWrgQ 115 0 +3cb6787c7063b0a04bff9e2bfa4203b73903dabe 115 0 #2 := false decl up_2 :: (-> T2 bool) decl uf_3 :: T2 @@ -11651,7 +11651,7 @@ #560 := [mp #344 #559]: #557 [unit-resolution #560 #576 #561]: false unsat -TibRlXkU+X+1+zGPYTiT0g 464 0 +dcb635ada6f2482ea11de30713fe962bcb57c9ad 464 0 #2 := false decl uf_2 :: (-> T2 T3 T3) decl uf_4 :: T3 @@ -12116,7 +12116,7 @@ #177 := [asserted]: #53 [unit-resolution #177 #793]: false unsat -DJPKxi9AO25zGBcs5kxUrw 21 0 +ca467a37d809de06757809cab1cd30e08586674f 21 0 #2 := false decl up_1 :: (-> T1 bool) #4 := (:var 0 T1) @@ -12138,7 +12138,7 @@ #25 := [asserted]: #9 [mp #25 #34]: false unsat -i5PnMbuM9mWv5LnVszz9+g 366 0 +f6e9645ebbb8739d12b8e96bc83ddef33c7d53bc 366 0 #2 := false decl uf_1 :: (-> int T1) #37 := 6::int @@ -12505,7 +12505,7 @@ #182 := [asserted]: #40 [unit-resolution #182 #399]: false unsat -K2SXMHU6QCZJ8TRs6zjKRg 408 0 +b15b527236338a437e355afcde07dd3c6dfc451f 408 0 #2 := false #22 := 0::int #8 := 2::int @@ -12914,7 +12914,7 @@ #375 := [unit-resolution #374 #407]: #708 [th-lemma #375 #370 #465]: false unsat -1DhSL9G2fGRGmuI8IaMNOA 50 0 +71b79533f46a8514b2fc189fc382867d50f52a9a 50 0 #2 := false decl up_35 :: (-> int bool) #112 := 1::int @@ -12965,7 +12965,7 @@ #504 := [quant-inst]: #503 [unit-resolution #504 #916 #297]: false unsat -dyXROdcPFSd36N3K7dpmDw 506 0 +e40ba7aed8ae5409337a331038da0587c03354d6 506 0 #2 := false decl uf_17 :: (-> T8 T3) decl uf_18 :: (-> T1 T8)