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_1 :: (-> T1 T2 T3)
decl uf_3 :: T2
#22 := uf_3
decl uf_6 :: T1
#30 := uf_6
#36 := (uf_1 uf_6 uf_3)
decl uf_2 :: (-> T1 T2 T3 T1)
decl uf_8 :: T3
#33 := uf_8
decl uf_5 :: T2
#26 := uf_5
decl uf_7 :: T3
#31 := uf_7
decl uf_4 :: T2
#23 := uf_4
#32 := (uf_2 uf_6 uf_4 uf_7)
#34 := (uf_2 #32 uf_5 uf_8)
#35 := (uf_1 #34 uf_3)
#37 := (= #35 #36)
#223 := (uf_1 #32 uf_4)
#214 := (uf_2 uf_6 uf_4 #223)
#552 := (uf_1 #214 uf_3)
#555 := (= #552 #36)
#560 := (= #36 #552)
#556 := (= #223 #552)
#24 := (= uf_3 uf_4)
#561 := (ite #24 #556 #560)
#8 := (:var 0 T2)
#6 := (:var 1 T3)
#5 := (:var 2 T2)
#4 := (:var 3 T1)
#7 := (uf_2 #4 #5 #6)
#9 := (uf_1 #7 #8)
#575 := (pattern #9)
#11 := (uf_1 #4 #8)
#100 := (= #9 #11)
#99 := (= #6 #9)
#55 := (= #5 #8)
#83 := (ite #55 #99 #100)
#576 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) (:pat #575) #83)
#90 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) #83)
#579 := (iff #90 #576)
#577 := (iff #83 #83)
#578 := [refl]: #577
#580 := [quant-intro #578]: #579
#58 := (ite #55 #6 #11)
#61 := (= #9 #58)
#64 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) #61)
#87 := (iff #64 #90)
#84 := (iff #61 #83)
#89 := [rewrite]: #84
#88 := [quant-intro #89]: #87
#93 := (~ #64 #64)
#91 := (~ #61 #61)
#92 := [refl]: #91
#94 := [nnf-pos #92]: #93
#10 := (= #8 #5)
#12 := (ite #10 #6 #11)
#13 := (= #9 #12)
#14 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) #13)
#65 := (iff #14 #64)
#62 := (iff #13 #61)
#59 := (= #12 #58)
#56 := (iff #10 #55)
#57 := [rewrite]: #56
#60 := [monotonicity #57]: #59
#63 := [monotonicity #60]: #62
#66 := [quant-intro #63]: #65
#54 := [asserted]: #14
#69 := [mp #54 #66]: #64
#95 := [mp~ #69 #94]: #64
#85 := [mp #95 #88]: #90
#581 := [mp #85 #580]: #576
#250 := (not #576)
#548 := (or #250 #561)
#551 := (= uf_4 uf_3)
#557 := (ite #551 #556 #555)
#549 := (or #250 #557)
#271 := (iff #549 #548)
#273 := (iff #548 #548)
#259 := [rewrite]: #273
#559 := (iff #557 #561)
#198 := (iff #555 #560)
#199 := [rewrite]: #198
#193 := (iff #551 #24)
#558 := [rewrite]: #193
#562 := [monotonicity #558 #199]: #559
#272 := [monotonicity #562]: #271
#274 := [trans #272 #259]: #271
#255 := [quant-inst]: #549
#165 := [mp #255 #274]: #548
#510 := [unit-resolution #165 #581]: #561
#544 := (not #561)
#497 := (or #544 #560)
#25 := (not #24)
#27 := (= uf_3 uf_5)
#28 := (not #27)
#29 := (and #25 #28)
#75 := [asserted]: #29
#79 := [and-elim #75]: #25
#268 := (or #544 #24 #560)
#542 := [def-axiom]: #268
#499 := [unit-resolution #542 #79]: #497
#491 := [unit-resolution #499 #510]: #560
#493 := [symm #491]: #555
#494 := (= #35 #552)
#157 := (uf_1 #32 uf_3)
#503 := (= #157 #552)
#502 := (= #552 #157)
#509 := (= #214 #32)
#415 := (= #223 uf_7)
#566 := (= uf_7 #223)
#17 := (:var 0 T3)
#16 := (:var 1 T2)
#15 := (:var 2 T1)
#18 := (uf_2 #15 #16 #17)
#582 := (pattern #18)
#19 := (uf_1 #18 #16)
#68 := (= #17 #19)
#584 := (forall (vars (?x5 T1) (?x6 T2) (?x7 T3)) (:pat #582) #68)
#72 := (forall (vars (?x5 T1) (?x6 T2) (?x7 T3)) #68)
#583 := (iff #72 #584)
#586 := (iff #584 #584)
#587 := [rewrite]: #586
#585 := [rewrite]: #583
#588 := [trans #585 #587]: #583
#82 := (~ #72 #72)
#96 := (~ #68 #68)
#97 := [refl]: #96
#78 := [nnf-pos #97]: #82
#20 := (= #19 #17)
#21 := (forall (vars (?x5 T1) (?x6 T2) (?x7 T3)) #20)
#73 := (iff #21 #72)
#70 := (iff #20 #68)
#71 := [rewrite]: #70
#74 := [quant-intro #71]: #73
#67 := [asserted]: #21
#77 := [mp #67 #74]: #72
#98 := [mp~ #77 #78]: #72
#589 := [mp #98 #588]: #584
#211 := (not #584)
#212 := (or #211 #566)
#213 := [quant-inst]: #212
#414 := [unit-resolution #213 #589]: #566
#416 := [symm #414]: #415
#506 := [monotonicity #416]: #509
#498 := [monotonicity #506]: #502
#492 := [symm #498]: #503
#244 := (= #35 #157)
#158 := (= uf_8 #35)
#248 := (ite #27 #158 #244)
#247 := (or #250 #248)
#245 := (= uf_5 uf_3)
#159 := (ite #245 #158 #244)
#251 := (or #250 #159)
#567 := (iff #251 #247)
#224 := (iff #247 #247)
#356 := [rewrite]: #224
#249 := (iff #159 #248)
#246 := (iff #245 #27)
#237 := [rewrite]: #246
#177 := [monotonicity #237]: #249
#569 := [monotonicity #177]: #567
#563 := [trans #569 #356]: #567
#230 := [quant-inst]: #251
#235 := [mp #230 #563]: #247
#488 := [unit-resolution #235 #581]: #248
#236 := (not #248)
#490 := (or #236 #244)
#80 := [and-elim #75]: #28
#572 := (or #236 #27 #244)
#573 := [def-axiom]: #572
#500 := [unit-resolution #573 #80]: #490
#501 := [unit-resolution #500 #488]: #244
#495 := [trans #501 #492]: #494
#489 := [trans #495 #493]: #37
#38 := (not #37)
#76 := [asserted]: #38
[unit-resolution #76 #489]: false
unsat