--- a/src/HOL/SMT_Examples/SMT_Examples.certs Mon Feb 14 10:40:43 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Mon Feb 14 12:25:26 2011 +0100
@@ -14831,3 +14831,80 @@
#269 := [asserted]: #104
[unit-resolution #269 #614]: false
unsat
+b5935b8a85a2e047200d1ea44e320dc9dcfbbbbc 76 0
+#2 := false
+decl f3 :: (-> Int S1)
+#118 := 1::Int
+#119 := (f3 1::Int)
+decl f1 :: S1
+#4 := f1
+#421 := (= f1 #119)
+#425 := (not #421)
+#120 := (= #119 f1)
+#121 := (not #120)
+#426 := (iff #121 #425)
+#423 := (iff #120 #421)
+#424 := [rewrite]: #423
+#427 := [monotonicity #424]: #426
+#420 := [asserted]: #121
+#430 := [mp #420 #427]: #425
+#8 := (:var 0 Int)
+#9 := (f3 #8)
+#953 := (pattern #9)
+#142 := (= f1 #9)
+#954 := (forall (vars (?v0 Int)) (:pat #953) #142)
+#165 := (forall (vars (?v0 Int)) #142)
+#957 := (iff #165 #954)
+#955 := (iff #142 #142)
+#956 := [refl]: #955
+#958 := [quant-intro #956]: #957
+#456 := (~ #165 #165)
+#454 := (~ #142 #142)
+#455 := [refl]: #454
+#457 := [nnf-pos #455]: #456
+decl f4 :: (-> S2 S1)
+decl f5 :: (-> Int S2 S2)
+decl f6 :: S2
+#11 := f6
+#12 := (f5 #8 f6)
+#13 := (f4 #12)
+#14 := (= #13 f1)
+#15 := (not #14)
+#16 := (or #14 #15)
+#10 := (= #9 f1)
+#17 := (and #10 #16)
+#18 := (forall (vars (?v0 Int)) #17)
+#166 := (iff #18 #165)
+#163 := (iff #17 #142)
+#1 := true
+#158 := (and #142 true)
+#161 := (iff #158 #142)
+#162 := [rewrite]: #161
+#159 := (iff #17 #158)
+#156 := (iff #16 true)
+#145 := (= f1 #13)
+#148 := (not #145)
+#151 := (or #145 #148)
+#154 := (iff #151 true)
+#155 := [rewrite]: #154
+#152 := (iff #16 #151)
+#149 := (iff #15 #148)
+#146 := (iff #14 #145)
+#147 := [rewrite]: #146
+#150 := [monotonicity #147]: #149
+#153 := [monotonicity #147 #150]: #152
+#157 := [trans #153 #155]: #156
+#143 := (iff #10 #142)
+#144 := [rewrite]: #143
+#160 := [monotonicity #144 #157]: #159
+#164 := [trans #160 #162]: #163
+#167 := [quant-intro #164]: #166
+#141 := [asserted]: #18
+#170 := [mp #141 #167]: #165
+#429 := [mp~ #170 #457]: #165
+#959 := [mp #429 #958]: #954
+#538 := (not #954)
+#623 := (or #538 #421)
+#624 := [quant-inst #118]: #623
+[unit-resolution #624 #959 #430]: false
+unsat