--- a/src/HOL/SMT_Examples/SMT_Examples.certs Fri Apr 08 19:04:08 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Fri Apr 08 19:04:08 2011 +0200
@@ -15079,3 +15079,158 @@
#142 := [unit-resolution #141 #78]: #63
[unit-resolution #142 #85]: false
unsat
+4d18c87aa576f201e48ea20e31f11fb8675b59d4 8 0
+#2 := false
+#1 := true
+#33 := (not true)
+#63 := (iff #33 false)
+#65 := [rewrite]: #63
+#62 := [asserted]: #33
+[mp #62 #65]: false
+unsat
+ad406fc43130e24f380abadc1fc8a246fab490af 145 0
+#2 := false
+decl f3 :: (-> S2 Int S1)
+#22 := 42::Int
+decl f4 :: (-> S3 Int S2)
+#20 := 3::Int
+decl f6 :: S3
+#18 := f6
+#21 := (f4 f6 3::Int)
+#23 := (f3 #21 42::Int)
+decl f1 :: S1
+#4 := f1
+#86 := (= f1 #23)
+decl f5 :: S3
+#8 := f5
+#255 := (f4 f5 3::Int)
+#246 := (f3 #255 42::Int)
+#568 := (= #246 #23)
+#207 := (= #23 #246)
+#202 := (= #21 #255)
+#558 := (= #255 #21)
+#83 := (= f5 f6)
+#92 := (not #83)
+#93 := (or #92 #86)
+#98 := (not #93)
+#24 := (= #23 f1)
+#19 := (= f6 f5)
+#25 := (implies #19 #24)
+#26 := (not #25)
+#99 := (iff #26 #98)
+#96 := (iff #25 #93)
+#89 := (implies #83 #86)
+#94 := (iff #89 #93)
+#95 := [rewrite]: #94
+#90 := (iff #25 #89)
+#87 := (iff #24 #86)
+#88 := [rewrite]: #87
+#84 := (iff #19 #83)
+#85 := [rewrite]: #84
+#91 := [monotonicity #85 #88]: #90
+#97 := [trans #91 #95]: #96
+#100 := [monotonicity #97]: #99
+#82 := [asserted]: #26
+#103 := [mp #82 #100]: #98
+#101 := [not-or-elim #103]: #83
+#564 := [monotonicity #101]: #558
+#565 := [symm #564]: #202
+#208 := [monotonicity #565]: #207
+#566 := [symm #208]: #568
+#257 := (= f1 #246)
+#11 := (:var 0 Int)
+#9 := (:var 1 Int)
+#10 := (f4 f5 #9)
+#12 := (f3 #10 #11)
+#13 := (pattern #12)
+#64 := 0::Int
+#61 := -1::Int
+#62 := (* -1::Int #11)
+#63 := (+ #9 #62)
+#65 := (<= #63 0::Int)
+#47 := (= f1 #12)
+#71 := (iff #47 #65)
+#76 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #13) #71)
+#116 := (~ #76 #76)
+#114 := (~ #71 #71)
+#115 := [refl]: #114
+#117 := [nnf-pos #115]: #116
+#15 := (<= #9 #11)
+#14 := (= #12 f1)
+#16 := (iff #14 #15)
+#17 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #13) #16)
+#79 := (iff #17 #76)
+#53 := (iff #15 #47)
+#58 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #13) #53)
+#77 := (iff #58 #76)
+#74 := (iff #53 #71)
+#68 := (iff #65 #47)
+#72 := (iff #68 #71)
+#73 := [rewrite]: #72
+#69 := (iff #53 #68)
+#66 := (iff #15 #65)
+#67 := [rewrite]: #66
+#70 := [monotonicity #67]: #69
+#75 := [trans #70 #73]: #74
+#78 := [quant-intro #75]: #77
+#59 := (iff #17 #58)
+#56 := (iff #16 #53)
+#50 := (iff #47 #15)
+#54 := (iff #50 #53)
+#55 := [rewrite]: #54
+#51 := (iff #16 #50)
+#48 := (iff #14 #47)
+#49 := [rewrite]: #48
+#52 := [monotonicity #49]: #51
+#57 := [trans #52 #55]: #56
+#60 := [quant-intro #57]: #59
+#80 := [trans #60 #78]: #79
+#46 := [asserted]: #17
+#81 := [mp #46 #80]: #76
+#106 := [mp~ #81 #117]: #76
+#557 := (not #76)
+#220 := (or #557 #257)
+#168 := (* -1::Int 42::Int)
+#253 := (+ 3::Int #168)
+#254 := (<= #253 0::Int)
+#258 := (iff #257 #254)
+#221 := (or #557 #258)
+#223 := (iff #221 #220)
+#560 := (iff #220 #220)
+#561 := [rewrite]: #560
+#573 := (iff #258 #257)
+#1 := true
+#571 := (iff #257 true)
+#572 := (iff #571 #257)
+#232 := [rewrite]: #572
+#231 := (iff #258 #571)
+#575 := (iff #254 true)
+#576 := -39::Int
+#245 := (<= -39::Int 0::Int)
+#579 := (iff #245 true)
+#580 := [rewrite]: #579
+#577 := (iff #254 #245)
+#570 := (= #253 -39::Int)
+#186 := -42::Int
+#260 := (+ 3::Int -42::Int)
+#233 := (= #260 -39::Int)
+#363 := [rewrite]: #233
+#239 := (= #253 #260)
+#259 := (= #168 -42::Int)
+#256 := [rewrite]: #259
+#574 := [monotonicity #256]: #239
+#244 := [trans #574 #363]: #570
+#578 := [monotonicity #244]: #577
+#581 := [trans #578 #580]: #575
+#236 := [monotonicity #581]: #231
+#216 := [trans #236 #232]: #573
+#559 := [monotonicity #216]: #223
+#562 := [trans #559 #561]: #223
+#222 := [quant-inst #20 #22]: #221
+#563 := [mp #222 #562]: #220
+#567 := [unit-resolution #563 #106]: #257
+#569 := [trans #567 #566]: #86
+#102 := (not #86)
+#104 := [not-or-elim #103]: #102
+[unit-resolution #104 #569]: false
+unsat