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 :: 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