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
#4 := 0::int
decl ?x1!0 :: int
#78 := ?x1!0
#83 := (<= ?x1!0 0::int)
#146 := (not #83)
#155 := [hypothesis]: #83
#7 := 1::int
#81 := (>= ?x1!0 1::int)
#82 := (not #81)
#156 := (or #82 #146)
#157 := [th-lemma]: #156
#158 := [unit-resolution #157 #155]: #82
#159 := (or #146 #81)
#49 := -1::int
#79 := (<= ?x1!0 -1::int)
#80 := (not #79)
#84 := (ite #83 #82 #80)
#85 := (not #84)
#5 := (:var 0 int)
#50 := (<= #5 -1::int)
#51 := (not #50)
#55 := (>= #5 1::int)
#54 := (not #55)
#45 := (<= #5 0::int)
#61 := (ite #45 #54 #51)
#66 := (forall (vars (?x1 int)) #61)
#69 := (not #66)
#86 := (~ #69 #85)
#87 := [sk]: #86
#10 := (< #5 1::int)
#8 := (+ #5 1::int)
#9 := (< 0::int #8)
#6 := (< 0::int #5)
#11 := (ite #6 #9 #10)
#12 := (forall (vars (?x1 int)) #11)
#13 := (not #12)
#72 := (iff #13 #69)
#30 := (+ 1::int #5)
#33 := (< 0::int #30)
#36 := (ite #6 #33 #10)
#39 := (forall (vars (?x1 int)) #36)
#42 := (not #39)
#70 := (iff #42 #69)
#67 := (iff #39 #66)
#64 := (iff #36 #61)
#46 := (not #45)
#58 := (ite #46 #51 #54)
#62 := (iff #58 #61)
#63 := [rewrite]: #62
#59 := (iff #36 #58)
#56 := (iff #10 #54)
#57 := [rewrite]: #56
#52 := (iff #33 #51)
#53 := [rewrite]: #52
#47 := (iff #6 #46)
#48 := [rewrite]: #47
#60 := [monotonicity #48 #53 #57]: #59
#65 := [trans #60 #63]: #64
#68 := [quant-intro #65]: #67
#71 := [monotonicity #68]: #70
#43 := (iff #13 #42)
#40 := (iff #12 #39)
#37 := (iff #11 #36)
#34 := (iff #9 #33)
#31 := (= #8 #30)
#32 := [rewrite]: #31
#35 := [monotonicity #32]: #34
#38 := [monotonicity #35]: #37
#41 := [quant-intro #38]: #40
#44 := [monotonicity #41]: #43
#73 := [trans #44 #71]: #72
#29 := [asserted]: #13
#74 := [mp #29 #73]: #69
#90 := [mp~ #74 #87]: #85
#151 := (or #84 #146 #81)
#152 := [def-axiom]: #151
#160 := [unit-resolution #152 #90]: #159
#161 := [unit-resolution #160 #158 #155]: false
#162 := [lemma #161]: #146
#163 := (or #80 #83)
#164 := [th-lemma]: #163
#165 := [unit-resolution #164 #162]: #80
#166 := (or #83 #79)
#153 := (or #84 #83 #79)
#154 := [def-axiom]: #153
#167 := [unit-resolution #154 #90]: #166
[unit-resolution #167 #165 #162]: false
unsat