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
decl uf_17 :: (-> T8 T3)
decl uf_18 :: (-> T1 T8)
decl uf_19 :: T1
#104 := uf_19
#105 := (uf_18 uf_19)
#106 := (uf_17 #105)
decl uf_15 :: (-> T7 T3)
decl uf_16 :: (-> int T7)
#101 := 3::int
#102 := (uf_16 3::int)
#103 := (uf_15 #102)
#107 := (= #103 #106)
decl uf_13 :: (-> T2 T3)
decl uf_2 :: (-> T1 T2 T2)
decl uf_7 :: T2
#29 := uf_7
#857 := (uf_2 uf_19 uf_7)
#859 := (uf_13 #857)
#599 := (= #859 #106)
#526 := (= #106 #859)
#79 := (:var 0 T1)
#82 := (uf_2 #79 uf_7)
#932 := (pattern #82)
#80 := (uf_18 #79)
#931 := (pattern #80)
#83 := (uf_13 #82)
#81 := (uf_17 #80)
#84 := (= #81 #83)
#933 := (forall (vars (?x16 T1)) (:pat #931 #932) #84)
#85 := (forall (vars (?x16 T1)) #84)
#936 := (iff #85 #933)
#934 := (iff #84 #84)
#935 := [refl]: #934
#937 := [quant-intro #935]: #936
#347 := (~ #85 #85)
#384 := (~ #84 #84)
#385 := [refl]: #384
#348 := [nnf-pos #385]: #347
#238 := [asserted]: #85
#386 := [mp~ #238 #348]: #85
#938 := [mp #386 #937]: #933
#861 := (not #933)
#862 := (or #861 #526)
#863 := [quant-inst]: #862
#601 := [unit-resolution #863 #938]: #526
#588 := [symm #601]: #599
#586 := (= #103 #859)
decl uf_1 :: (-> T2 T3)
#558 := (uf_1 #857)
#832 := (= #558 #859)
#5 := (:var 0 T2)
#66 := (uf_13 #5)
#908 := (pattern #66)
#8 := (uf_1 #5)
#907 := (pattern #8)
#222 := (= #8 #66)
#909 := (forall (vars (?x13 T2)) (:pat #907 #908) #222)
#226 := (forall (vars (?x13 T2)) #222)
#912 := (iff #226 #909)
#910 := (iff #222 #222)
#911 := [refl]: #910
#913 := [quant-intro #911]: #912
#341 := (~ #226 #226)
#375 := (~ #222 #222)
#376 := [refl]: #375
#342 := [nnf-pos #376]: #341
#67 := (= #66 #8)
#68 := (forall (vars (?x13 T2)) #67)
#227 := (iff #68 #226)
#224 := (iff #67 #222)
#225 := [rewrite]: #224
#228 := [quant-intro #225]: #227
#221 := [asserted]: #68
#231 := [mp #221 #228]: #226
#377 := [mp~ #231 #342]: #226
#914 := [mp #377 #913]: #909
#451 := (not #909)
#837 := (or #451 #832)
#547 := [quant-inst]: #837
#615 := [unit-resolution #547 #914]: #832
#585 := (= #103 #558)
decl uf_3 :: (-> int T3)
decl uf_4 :: (-> T3 int)
#30 := (uf_1 uf_7)
#806 := (uf_4 #30)
#11 := 1::int
#127 := (uf_3 1::int)
#130 := (uf_4 #127)
#649 := (+ #130 #806)
#794 := (uf_3 #649)
#597 := (= #794 #558)
#683 := (= #558 #794)
#4 := (:var 1 T1)
#6 := (uf_2 #4 #5)
#865 := (pattern #6)
#9 := (uf_4 #8)
#133 := (+ #9 #130)
#136 := (uf_3 #133)
#7 := (uf_1 #6)
#139 := (= #7 #136)
#866 := (forall (vars (?x1 T1) (?x2 T2)) (:pat #865) #139)
#142 := (forall (vars (?x1 T1) (?x2 T2)) #139)
#869 := (iff #142 #866)
#867 := (iff #139 #139)
#868 := [refl]: #867
#870 := [quant-intro #868]: #869
#361 := (~ #142 #142)
#359 := (~ #139 #139)
#360 := [refl]: #359
#362 := [nnf-pos #360]: #361
#10 := 0::int
#12 := (+ 0::int 1::int)
#13 := (uf_3 #12)
#14 := (uf_4 #13)
#15 := (+ #9 #14)
#16 := (uf_3 #15)
#17 := (= #7 #16)
#18 := (forall (vars (?x1 T1) (?x2 T2)) #17)
#143 := (iff #18 #142)
#140 := (iff #17 #139)
#137 := (= #16 #136)
#134 := (= #15 #133)
#131 := (= #14 #130)
#128 := (= #13 #127)
#125 := (= #12 1::int)
#126 := [rewrite]: #125
#129 := [monotonicity #126]: #128
#132 := [monotonicity #129]: #131
#135 := [monotonicity #132]: #134
#138 := [monotonicity #135]: #137
#141 := [monotonicity #138]: #140
#144 := [quant-intro #141]: #143
#124 := [asserted]: #18
#147 := [mp #124 #144]: #142
#363 := [mp~ #147 #362]: #142
#871 := [mp #363 #870]: #866
#701 := (not #866)
#694 := (or #701 #683)
#688 := (+ #806 #130)
#689 := (uf_3 #688)
#690 := (= #558 #689)
#702 := (or #701 #690)
#704 := (iff #702 #694)
#706 := (iff #694 #694)
#799 := [rewrite]: #706
#698 := (iff #690 #683)
#795 := (= #689 #794)
#797 := (= #688 #649)
#699 := [rewrite]: #797
#798 := [monotonicity #699]: #795
#700 := [monotonicity #798]: #698
#705 := [monotonicity #700]: #704
#796 := [trans #705 #799]: #704
#703 := [quant-inst]: #702
#800 := [mp #703 #796]: #694
#614 := [unit-resolution #800 #871]: #683
#598 := [symm #614]: #597
#583 := (= #103 #794)
#595 := (= #127 #794)
#605 := (= #794 #127)
#618 := (= #649 1::int)
#780 := (<= #806 0::int)
#778 := (= #806 0::int)
#31 := (uf_3 0::int)
#858 := (uf_4 #31)
#855 := (= #858 0::int)
#72 := (:var 0 int)
#92 := (uf_3 #72)
#947 := (pattern #92)
#266 := (>= #72 0::int)
#267 := (not #266)
#93 := (uf_4 #92)
#248 := (= #72 #93)
#273 := (or #248 #267)
#948 := (forall (vars (?x18 int)) (:pat #947) #273)
#278 := (forall (vars (?x18 int)) #273)
#951 := (iff #278 #948)
#949 := (iff #273 #273)
#950 := [refl]: #949
#952 := [quant-intro #950]: #951
#351 := (~ #278 #278)
#390 := (~ #273 #273)
#391 := [refl]: #390
#352 := [nnf-pos #391]: #351
#94 := (= #93 #72)
#91 := (<= 0::int #72)
#95 := (implies #91 #94)
#96 := (forall (vars (?x18 int)) #95)
#281 := (iff #96 #278)
#255 := (not #91)
#256 := (or #255 #248)
#261 := (forall (vars (?x18 int)) #256)
#279 := (iff #261 #278)
#276 := (iff #256 #273)
#270 := (or #267 #248)
#274 := (iff #270 #273)
#275 := [rewrite]: #274
#271 := (iff #256 #270)
#268 := (iff #255 #267)
#264 := (iff #91 #266)
#265 := [rewrite]: #264
#269 := [monotonicity #265]: #268
#272 := [monotonicity #269]: #271
#277 := [trans #272 #275]: #276
#280 := [quant-intro #277]: #279
#262 := (iff #96 #261)
#259 := (iff #95 #256)
#252 := (implies #91 #248)
#257 := (iff #252 #256)
#258 := [rewrite]: #257
#253 := (iff #95 #252)
#250 := (iff #94 #248)
#251 := [rewrite]: #250
#254 := [monotonicity #251]: #253
#260 := [trans #254 #258]: #259
#263 := [quant-intro #260]: #262
#282 := [trans #263 #280]: #281
#247 := [asserted]: #96
#283 := [mp #247 #282]: #278
#392 := [mp~ #283 #352]: #278
#953 := [mp #392 #952]: #948
#848 := (not #948)
#850 := (or #848 #855)
#527 := (>= 0::int 0::int)
#860 := (not #527)
#864 := (= 0::int #858)
#854 := (or #864 #860)
#489 := (or #848 #854)
#851 := (iff #489 #850)
#852 := (iff #850 #850)
#838 := [rewrite]: #852
#847 := (iff #854 #855)
#843 := (or #855 false)
#846 := (iff #843 #855)
#841 := [rewrite]: #846
#844 := (iff #854 #843)
#505 := (iff #860 false)
#1 := true
#498 := (not true)
#503 := (iff #498 false)
#504 := [rewrite]: #503
#840 := (iff #860 #498)
#514 := (iff #527 true)
#856 := [rewrite]: #514
#502 := [monotonicity #856]: #840
#842 := [trans #502 #504]: #505
#513 := (iff #864 #855)
#518 := [rewrite]: #513
#845 := [monotonicity #518 #842]: #844
#484 := [trans #845 #841]: #847
#849 := [monotonicity #484]: #851
#839 := [trans #849 #838]: #851
#490 := [quant-inst]: #489
#546 := [mp #490 #839]: #850
#644 := [unit-resolution #546 #953]: #855
#621 := (= #806 #858)
#32 := (= #30 #31)
#159 := [asserted]: #32
#626 := [monotonicity #159]: #621
#616 := [trans #626 #644]: #778
#606 := (not #778)
#608 := (or #606 #780)
#609 := [th-lemma]: #608
#612 := [unit-resolution #609 #616]: #780
#790 := (>= #806 0::int)
#613 := (or #606 #790)
#617 := [th-lemma]: #613
#610 := [unit-resolution #617 #616]: #790
#723 := (<= #130 1::int)
#746 := (= #130 1::int)
#713 := (or #848 #746)
#755 := (>= 1::int 0::int)
#756 := (not #755)
#743 := (= 1::int #130)
#744 := (or #743 #756)
#714 := (or #848 #744)
#718 := (iff #714 #713)
#720 := (iff #713 #713)
#725 := [rewrite]: #720
#739 := (iff #744 #746)
#735 := (or #746 false)
#738 := (iff #735 #746)
#733 := [rewrite]: #738
#736 := (iff #744 #735)
#731 := (iff #756 false)
#734 := (iff #756 #498)
#742 := (iff #755 true)
#748 := [rewrite]: #742
#730 := [monotonicity #748]: #734
#732 := [trans #730 #504]: #731
#745 := (iff #743 #746)
#747 := [rewrite]: #745
#737 := [monotonicity #747 #732]: #736
#712 := [trans #737 #733]: #739
#719 := [monotonicity #712]: #718
#721 := [trans #719 #725]: #718
#607 := [quant-inst]: #714
#722 := [mp #607 #721]: #713
#641 := [unit-resolution #722 #953]: #746
#620 := (not #746)
#623 := (or #620 #723)
#627 := [th-lemma]: #623
#629 := [unit-resolution #627 #641]: #723
#726 := (>= #130 1::int)
#630 := (or #620 #726)
#628 := [th-lemma]: #630
#631 := [unit-resolution #628 #641]: #726
#611 := [th-lemma #631 #629 #610 #612]: #618
#587 := [monotonicity #611]: #605
#596 := [symm #587]: #595
#581 := (= #103 #127)
decl uf_5 :: (-> T4 T3)
decl uf_8 :: T4
#33 := uf_8
#34 := (uf_5 uf_8)
#822 := (uf_4 #34)
#824 := (+ #130 #822)
#666 := (uf_3 #824)
#593 := (= #666 #127)
#589 := (= #127 #666)
#624 := (= 1::int #824)
#619 := (= #824 1::int)
#789 := (<= #822 0::int)
#787 := (= #822 0::int)
#632 := (= #822 #858)
#35 := (= #34 #31)
#162 := (= #31 #34)
#163 := (iff #35 #162)
#164 := [rewrite]: #163
#160 := [asserted]: #35
#167 := [mp #160 #164]: #162
#662 := [symm #167]: #35
#633 := [monotonicity #662]: #632
#634 := [trans #633 #644]: #787
#635 := (not #787)
#637 := (or #635 #789)
#638 := [th-lemma]: #637
#639 := [unit-resolution #638 #634]: #789
#781 := (>= #822 0::int)
#481 := (or #635 #781)
#640 := [th-lemma]: #481
#636 := [unit-resolution #640 #634]: #781
#622 := [th-lemma #631 #629 #636 #639]: #619
#625 := [symm #622]: #624
#590 := [monotonicity #625]: #589
#594 := [symm #590]: #593
#579 := (= #103 #666)
decl uf_6 :: (-> int T4 T4)
#539 := (uf_6 3::int uf_8)
#836 := (uf_5 #539)
#810 := (= #836 #666)
#813 := (= #666 #836)
#20 := (:var 0 T4)
#19 := (:var 1 int)
#21 := (uf_6 #19 #20)
#872 := (pattern #21)
#23 := (uf_5 #20)
#24 := (uf_4 #23)
#146 := (+ #24 #130)
#150 := (uf_3 #146)
#22 := (uf_5 #21)
#153 := (= #22 #150)
#873 := (forall (vars (?x3 int) (?x4 T4)) (:pat #872) #153)
#156 := (forall (vars (?x3 int) (?x4 T4)) #153)
#876 := (iff #156 #873)
#874 := (iff #153 #153)
#875 := [refl]: #874
#877 := [quant-intro #875]: #876
#328 := (~ #156 #156)
#364 := (~ #153 #153)
#365 := [refl]: #364
#326 := [nnf-pos #365]: #328
#25 := (+ #24 #14)
#26 := (uf_3 #25)
#27 := (= #22 #26)
#28 := (forall (vars (?x3 int) (?x4 T4)) #27)
#157 := (iff #28 #156)
#154 := (iff #27 #153)
#151 := (= #26 #150)
#148 := (= #25 #146)
#149 := [monotonicity #132]: #148
#152 := [monotonicity #149]: #151
#155 := [monotonicity #152]: #154
#158 := [quant-intro #155]: #157
#145 := [asserted]: #28
#161 := [mp #145 #158]: #156
#366 := [mp~ #161 #326]: #156
#878 := [mp #366 #877]: #873
#809 := (not #873)
#816 := (or #809 #813)
#817 := (+ #822 #130)
#818 := (uf_3 #817)
#823 := (= #836 #818)
#645 := (or #809 #823)
#648 := (iff #645 #816)
#802 := (iff #816 #816)
#804 := [rewrite]: #802
#814 := (iff #823 #813)
#807 := (iff #810 #813)
#808 := [rewrite]: #807
#811 := (iff #823 #810)
#667 := (= #818 #666)
#819 := (= #817 #824)
#825 := [rewrite]: #819
#668 := [monotonicity #825]: #667
#812 := [monotonicity #668]: #811
#815 := [trans #812 #808]: #814
#801 := [monotonicity #815]: #648
#805 := [trans #801 #804]: #648
#647 := [quant-inst]: #645
#803 := [mp #647 #805]: #816
#658 := [unit-resolution #803 #878]: #813
#592 := [symm #658]: #810
#600 := (= #103 #836)
decl uf_14 :: (-> T4 T3)
#540 := (uf_14 #539)
#548 := (= #540 #836)
#69 := (uf_14 #20)
#916 := (pattern #69)
#915 := (pattern #23)
#230 := (= #23 #69)
#917 := (forall (vars (?x14 T4)) (:pat #915 #916) #230)
#234 := (forall (vars (?x14 T4)) #230)
#920 := (iff #234 #917)
#918 := (iff #230 #230)
#919 := [refl]: #918
#921 := [quant-intro #919]: #920
#343 := (~ #234 #234)
#378 := (~ #230 #230)
#379 := [refl]: #378
#344 := [nnf-pos #379]: #343
#70 := (= #69 #23)
#71 := (forall (vars (?x14 T4)) #70)
#235 := (iff #71 #234)
#232 := (iff #70 #230)
#233 := [rewrite]: #232
#236 := [quant-intro #233]: #235
#229 := [asserted]: #71
#239 := [mp #229 #236]: #234
#380 := [mp~ #239 #344]: #234
#922 := [mp #380 #921]: #917
#541 := (not #917)
#828 := (or #541 #548)
#833 := (= #836 #540)
#829 := (or #541 #833)
#826 := (iff #829 #828)
#827 := (iff #828 #828)
#831 := [rewrite]: #827
#549 := (iff #833 #548)
#550 := [rewrite]: #549
#830 := [monotonicity #550]: #826
#820 := [trans #830 #831]: #826
#543 := [quant-inst]: #829
#821 := [mp #543 #820]: #828
#657 := [unit-resolution #821 #922]: #548
#521 := (= #103 #540)
#75 := (uf_6 #72 uf_8)
#924 := (pattern #75)
#73 := (uf_16 #72)
#923 := (pattern #73)
#76 := (uf_14 #75)
#74 := (uf_15 #73)
#77 := (= #74 #76)
#925 := (forall (vars (?x15 int)) (:pat #923 #924) #77)
#78 := (forall (vars (?x15 int)) #77)
#928 := (iff #78 #925)
#926 := (iff #77 #77)
#927 := [refl]: #926
#929 := [quant-intro #927]: #928
#345 := (~ #78 #78)
#381 := (~ #77 #77)
#382 := [refl]: #381
#346 := [nnf-pos #382]: #345
#237 := [asserted]: #78
#383 := [mp~ #237 #346]: #78
#930 := [mp #383 #929]: #925
#515 := (not #925)
#646 := (or #515 #521)
#853 := [quant-inst]: #646
#603 := [unit-resolution #853 #930]: #521
#577 := [trans #603 #657]: #600
#580 := [trans #577 #592]: #579
#582 := [trans #580 #594]: #581
#584 := [trans #582 #596]: #583
#578 := [trans #584 #598]: #585
#571 := [trans #578 #615]: #586
#572 := [trans #571 #588]: #107
#108 := (not #107)
#325 := [asserted]: #108
[unit-resolution #325 #572]: false
unsat