added proof reconstructon for Z3,
added certificates for simpler re-checking of proofs (no need to invoke external solvers),
added examples and certificates for all examples,
removed Unsynchronized.ref (in smt_normalize.ML)
#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
decl uf_3 :: T1
#22 := uf_3
#23 := (uf_2 uf_3)
#469 := (= #23 0::int)
decl uf_1 :: (-> int T1)
#251 := (uf_1 #23)
#557 := (uf_2 #251)
#558 := (= #557 0::int)
#556 := (>= #23 0::int)
#477 := (not #556)
#144 := -1::int
#348 := (>= #23 -1::int)
#628 := (not #348)
#21 := 1::int
#24 := (+ 1::int #23)
#25 := (uf_1 #24)
#26 := (uf_2 #25)
#632 := (* -1::int #26)
#636 := (+ #23 #632)
#633 := (= #636 -1::int)
#471 := (not #633)
#613 := (<= #636 -1::int)
#527 := (not #613)
#145 := (* -1::int #23)
#146 := (+ #145 #26)
#149 := (uf_1 #146)
#152 := (uf_2 #149)
#504 := (+ #632 #152)
#505 := (+ #23 #504)
#573 := (>= #505 0::int)
#502 := (= #505 0::int)
#599 := (<= #636 0::int)
#526 := [hypothesis]: #613
#491 := (or #527 #599)
#515 := [th-lemma]: #491
#516 := [unit-resolution #515 #526]: #599
#587 := (not #599)
#578 := (or #502 #587)
#10 := (:var 0 int)
#12 := (uf_1 #10)
#673 := (pattern #12)
#76 := (>= #10 0::int)
#77 := (not #76)
#13 := (uf_2 #12)
#58 := (= #10 #13)
#83 := (or #58 #77)
#674 := (forall (vars (?x2 int)) (:pat #673) #83)
#88 := (forall (vars (?x2 int)) #83)
#677 := (iff #88 #674)
#675 := (iff #83 #83)
#676 := [refl]: #675
#678 := [quant-intro #676]: #677
#179 := (~ #88 #88)
#191 := (~ #83 #83)
#192 := [refl]: #191
#177 := [nnf-pos #192]: #179
#14 := (= #13 #10)
#11 := (<= 0::int #10)
#15 := (implies #11 #14)
#16 := (forall (vars (?x2 int)) #15)
#91 := (iff #16 #88)
#65 := (not #11)
#66 := (or #65 #58)
#71 := (forall (vars (?x2 int)) #66)
#89 := (iff #71 #88)
#86 := (iff #66 #83)
#80 := (or #77 #58)
#84 := (iff #80 #83)
#85 := [rewrite]: #84
#81 := (iff #66 #80)
#78 := (iff #65 #77)
#74 := (iff #11 #76)
#75 := [rewrite]: #74
#79 := [monotonicity #75]: #78
#82 := [monotonicity #79]: #81
#87 := [trans #82 #85]: #86
#90 := [quant-intro #87]: #89
#72 := (iff #16 #71)
#69 := (iff #15 #66)
#62 := (implies #11 #58)
#67 := (iff #62 #66)
#68 := [rewrite]: #67
#63 := (iff #15 #62)
#60 := (iff #14 #58)
#61 := [rewrite]: #60
#64 := [monotonicity #61]: #63
#70 := [trans #64 #68]: #69
#73 := [quant-intro #70]: #72
#92 := [trans #73 #90]: #91
#57 := [asserted]: #16
#93 := [mp #57 #92]: #88
#193 := [mp~ #93 #177]: #88
#679 := [mp #193 #678]: #674
#644 := (not #674)
#591 := (or #644 #502 #587)
#498 := (>= #146 0::int)
#500 := (not #498)
#501 := (= #146 #152)
#494 := (or #501 #500)
#592 := (or #644 #494)
#579 := (iff #592 #591)
#593 := (or #644 #578)
#584 := (iff #593 #591)
#585 := [rewrite]: #584
#582 := (iff #592 #593)
#580 := (iff #494 #578)
#589 := (iff #500 #587)
#596 := (iff #498 #599)
#600 := [rewrite]: #596
#581 := [monotonicity #600]: #589
#503 := (iff #501 #502)
#506 := [rewrite]: #503
#590 := [monotonicity #506 #581]: #580
#583 := [monotonicity #590]: #582
#586 := [trans #583 #585]: #579
#588 := [quant-inst]: #592
#570 := [mp #588 #586]: #591
#511 := [unit-resolution #570 #679]: #578
#517 := [unit-resolution #511 #516]: #502
#485 := (not #502)
#492 := (or #485 #573)
#451 := [th-lemma]: #492
#482 := [unit-resolution #451 #517]: #573
#554 := (<= #152 0::int)
#163 := (* -1::int #152)
#138 := (uf_1 0::int)
#141 := (uf_2 #138)
#164 := (+ #141 #163)
#162 := (>= #164 0::int)
#30 := (- #26 #23)
#31 := (uf_1 #30)
#32 := (uf_2 #31)
#27 := (* 0::int #26)
#28 := (uf_1 #27)
#29 := (uf_2 #28)
#33 := (< #29 #32)
#34 := (not #33)
#174 := (iff #34 #162)
#155 := (< #141 #152)
#158 := (not #155)
#172 := (iff #158 #162)
#161 := (not #162)
#167 := (not #161)
#170 := (iff #167 #162)
#171 := [rewrite]: #170
#168 := (iff #158 #167)
#165 := (iff #155 #161)
#166 := [rewrite]: #165
#169 := [monotonicity #166]: #168
#173 := [trans #169 #171]: #172
#159 := (iff #34 #158)
#156 := (iff #33 #155)
#153 := (= #32 #152)
#150 := (= #31 #149)
#147 := (= #30 #146)
#148 := [rewrite]: #147
#151 := [monotonicity #148]: #150
#154 := [monotonicity #151]: #153
#142 := (= #29 #141)
#139 := (= #28 #138)
#136 := (= #27 0::int)
#137 := [rewrite]: #136
#140 := [monotonicity #137]: #139
#143 := [monotonicity #140]: #142
#157 := [monotonicity #143 #154]: #156
#160 := [monotonicity #157]: #159
#175 := [trans #160 #173]: #174
#135 := [asserted]: #34
#176 := [mp #135 #175]: #162
#651 := (<= #141 0::int)
#662 := (= #141 0::int)
#645 := (or #644 #662)
#316 := (>= 0::int 0::int)
#446 := (not #316)
#328 := (= 0::int #141)
#660 := (or #328 #446)
#646 := (or #644 #660)
#647 := (iff #646 #645)
#648 := (iff #645 #645)
#650 := [rewrite]: #648
#642 := (iff #660 #662)
#640 := (or #662 false)
#305 := (iff #640 #662)
#306 := [rewrite]: #305
#303 := (iff #660 #640)
#656 := (iff #446 false)
#1 := true
#654 := (not true)
#655 := (iff #654 false)
#315 := [rewrite]: #655
#314 := (iff #446 #654)
#658 := (iff #316 true)
#664 := [rewrite]: #658
#319 := [monotonicity #664]: #314
#299 := [trans #319 #315]: #656
#661 := (iff #328 #662)
#663 := [rewrite]: #661
#304 := [monotonicity #663 #299]: #303
#643 := [trans #304 #306]: #642
#285 := [monotonicity #643]: #647
#290 := [trans #285 #650]: #647
#641 := [quant-inst]: #646
#291 := [mp #641 #290]: #645
#484 := [unit-resolution #291 #679]: #662
#486 := (not #662)
#493 := (or #486 #651)
#495 := [th-lemma]: #493
#496 := [unit-resolution #495 #484]: #651
#497 := (not #651)
#507 := (or #554 #497 #161)
#487 := [th-lemma]: #507
#508 := [unit-resolution #487 #496 #176]: #554
#463 := [th-lemma #508 #526 #482]: false
#464 := [lemma #463]: #527
#472 := (or #471 #613)
#473 := [th-lemma]: #472
#474 := [unit-resolution #473 #464]: #471
#631 := (or #628 #633)
#618 := (or #644 #628 #633)
#634 := (>= #24 0::int)
#635 := (not #634)
#357 := (= #24 #26)
#358 := (or #357 #635)
#623 := (or #644 #358)
#610 := (iff #623 #618)
#619 := (or #644 #631)
#467 := (iff #619 #618)
#468 := [rewrite]: #467
#625 := (iff #623 #619)
#622 := (iff #358 #631)
#626 := (or #633 #628)
#620 := (iff #626 #631)
#621 := [rewrite]: #620
#630 := (iff #358 #626)
#629 := (iff #635 #628)
#349 := (iff #634 #348)
#350 := [rewrite]: #349
#344 := [monotonicity #350]: #629
#637 := (iff #357 #633)
#347 := [rewrite]: #637
#627 := [monotonicity #347 #344]: #630
#617 := [trans #627 #621]: #622
#466 := [monotonicity #617]: #625
#611 := [trans #466 #468]: #610
#624 := [quant-inst]: #623
#612 := [mp #624 #611]: #618
#475 := [unit-resolution #612 #679]: #631
#476 := [unit-resolution #475 #474]: #628
#478 := (or #477 #348)
#479 := [th-lemma]: #478
#480 := [unit-resolution #479 #476]: #477
#560 := (or #556 #558)
#18 := (= #13 0::int)
#124 := (or #18 #76)
#680 := (forall (vars (?x3 int)) (:pat #673) #124)
#129 := (forall (vars (?x3 int)) #124)
#683 := (iff #129 #680)
#681 := (iff #124 #124)
#682 := [refl]: #681
#684 := [quant-intro #682]: #683
#180 := (~ #129 #129)
#194 := (~ #124 #124)
#195 := [refl]: #194
#181 := [nnf-pos #195]: #180
#17 := (< #10 0::int)
#19 := (implies #17 #18)
#20 := (forall (vars (?x3 int)) #19)
#132 := (iff #20 #129)
#95 := (= 0::int #13)
#101 := (not #17)
#102 := (or #101 #95)
#107 := (forall (vars (?x3 int)) #102)
#130 := (iff #107 #129)
#127 := (iff #102 #124)
#121 := (or #76 #18)
#125 := (iff #121 #124)
#126 := [rewrite]: #125
#122 := (iff #102 #121)
#119 := (iff #95 #18)
#120 := [rewrite]: #119
#117 := (iff #101 #76)
#112 := (not #77)
#115 := (iff #112 #76)
#116 := [rewrite]: #115
#113 := (iff #101 #112)
#110 := (iff #17 #77)
#111 := [rewrite]: #110
#114 := [monotonicity #111]: #113
#118 := [trans #114 #116]: #117
#123 := [monotonicity #118 #120]: #122
#128 := [trans #123 #126]: #127
#131 := [quant-intro #128]: #130
#108 := (iff #20 #107)
#105 := (iff #19 #102)
#98 := (implies #17 #95)
#103 := (iff #98 #102)
#104 := [rewrite]: #103
#99 := (iff #19 #98)
#96 := (iff #18 #95)
#97 := [rewrite]: #96
#100 := [monotonicity #97]: #99
#106 := [trans #100 #104]: #105
#109 := [quant-intro #106]: #108
#133 := [trans #109 #131]: #132
#94 := [asserted]: #20
#134 := [mp #94 #133]: #129
#196 := [mp~ #134 #181]: #129
#685 := [mp #196 #684]: #680
#604 := (not #680)
#562 := (or #604 #556 #558)
#559 := (or #558 #556)
#540 := (or #604 #559)
#542 := (iff #540 #562)
#543 := (or #604 #560)
#546 := (iff #543 #562)
#547 := [rewrite]: #546
#544 := (iff #540 #543)
#561 := (iff #559 #560)
#551 := [rewrite]: #561
#545 := [monotonicity #551]: #544
#548 := [trans #545 #547]: #542
#541 := [quant-inst]: #540
#534 := [mp #541 #548]: #562
#465 := [unit-resolution #534 #685]: #560
#481 := [unit-resolution #465 #480]: #558
#443 := (= #23 #557)
#337 := (= uf_3 #251)
#4 := (:var 0 T1)
#5 := (uf_2 #4)
#665 := (pattern #5)
#6 := (uf_1 #5)
#51 := (= #4 #6)
#666 := (forall (vars (?x1 T1)) (:pat #665) #51)
#54 := (forall (vars (?x1 T1)) #51)
#667 := (iff #54 #666)
#669 := (iff #666 #666)
#670 := [rewrite]: #669
#668 := [rewrite]: #667
#671 := [trans #668 #670]: #667
#188 := (~ #54 #54)
#186 := (~ #51 #51)
#187 := [refl]: #186
#189 := [nnf-pos #187]: #188
#7 := (= #6 #4)
#8 := (forall (vars (?x1 T1)) #7)
#55 := (iff #8 #54)
#52 := (iff #7 #51)
#53 := [rewrite]: #52
#56 := [quant-intro #53]: #55
#50 := [asserted]: #8
#59 := [mp #50 #56]: #54
#190 := [mp~ #59 #189]: #54
#672 := [mp #190 #671]: #666
#252 := (not #666)
#342 := (or #252 #337)
#339 := [quant-inst]: #342
#442 := [unit-resolution #339 #672]: #337
#450 := [monotonicity #442]: #443
#452 := [trans #450 #481]: #469
#453 := (not #469)
#454 := (or #453 #556)
#456 := [th-lemma]: #454
[unit-resolution #456 #480 #452]: false
unsat