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 up_35 :: (-> int bool)
#112 := 1::int
#113 := (up_35 1::int)
#114 := (not #113)
#297 := [asserted]: #114
#103 := (:var 0 int)
#104 := (up_35 #103)
#911 := (pattern #104)
#912 := (forall (vars (?x12 int)) (:pat #911) #104)
#294 := (forall (vars (?x12 int)) #104)
#915 := (iff #294 #912)
#913 := (iff #104 #104)
#914 := [refl]: #913
#916 := [quant-intro #914]: #915
#320 := (~ #294 #294)
#361 := (~ #104 #104)
#362 := [refl]: #361
#321 := [nnf-pos #362]: #320
decl up_32 :: (-> T13 bool)
decl uf_36 :: (-> int T13 T13)
decl uf_37 :: T13
#105 := uf_37
#106 := (uf_36 #103 uf_37)
#107 := (up_32 #106)
#108 := (not #107)
#109 := (or #107 #108)
#110 := (and #104 #109)
#111 := (forall (vars (?x12 int)) #110)
#295 := (iff #111 #294)
#292 := (iff #110 #104)
#1 := true
#287 := (and #104 true)
#290 := (iff #287 #104)
#291 := [rewrite]: #290
#288 := (iff #110 #287)
#284 := (iff #109 true)
#286 := [rewrite]: #284
#289 := [monotonicity #286]: #288
#293 := [trans #289 #291]: #292
#296 := [quant-intro #293]: #295
#283 := [asserted]: #111
#299 := [mp #283 #296]: #294
#363 := [mp~ #299 #321]: #294
#917 := [mp #363 #916]: #912
#418 := (not #912)
#504 := (or #418 #113)
#419 := [quant-inst]: #504
[unit-resolution #419 #917 #297]: false
unsat