--- a/src/HOL/SMT_Examples/SMT_Examples.certs Fri Dec 17 00:27:40 2010 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Fri Dec 17 08:37:35 2010 +0100
@@ -14816,3 +14816,80 @@
#287 := [mp #270 #284]: #282
[unit-resolution #287 #630]: false
unsat
+a7ba12fdd24a1cfe15f53475941aaf6855022b7f 76 0
+#2 := false
+decl f28 :: (-> Int S1)
+#107 := 1::Int
+#108 := (f28 1::Int)
+decl f1 :: S1
+#4 := f1
+#382 := (= f1 #108)
+#386 := (not #382)
+#109 := (= #108 f1)
+#110 := (not #109)
+#387 := (iff #110 #386)
+#384 := (iff #109 #382)
+#385 := [rewrite]: #384
+#388 := [monotonicity #385]: #387
+#381 := [asserted]: #110
+#391 := [mp #381 #388]: #386
+#96 := (:var 0 Int)
+#97 := (f28 #96)
+#965 := (pattern #97)
+#354 := (= f1 #97)
+#966 := (forall (vars (?v0 Int)) (:pat #965) #354)
+#378 := (forall (vars (?v0 Int)) #354)
+#969 := (iff #378 #966)
+#967 := (iff #354 #354)
+#968 := [refl]: #967
+#970 := [quant-intro #968]: #969
+#407 := (~ #378 #378)
+#437 := (~ #354 #354)
+#438 := [refl]: #437
+#408 := [nnf-pos #438]: #407
+decl f3 :: (-> S2 S1)
+decl f29 :: (-> Int S2 S2)
+decl f30 :: S2
+#99 := f30
+#100 := (f29 #96 f30)
+#101 := (f3 #100)
+#102 := (= #101 f1)
+#103 := (not #102)
+#104 := (or #102 #103)
+#98 := (= #97 f1)
+#105 := (and #98 #104)
+#106 := (forall (vars (?v0 Int)) #105)
+#379 := (iff #106 #378)
+#376 := (iff #105 #354)
+#1 := true
+#371 := (and #354 true)
+#374 := (iff #371 #354)
+#375 := [rewrite]: #374
+#372 := (iff #105 #371)
+#369 := (iff #104 true)
+#358 := (= f1 #101)
+#361 := (not #358)
+#364 := (or #358 #361)
+#367 := (iff #364 true)
+#368 := [rewrite]: #367
+#365 := (iff #104 #364)
+#362 := (iff #103 #361)
+#359 := (iff #102 #358)
+#360 := [rewrite]: #359
+#363 := [monotonicity #360]: #362
+#366 := [monotonicity #360 #363]: #365
+#370 := [trans #366 #368]: #369
+#356 := (iff #98 #354)
+#357 := [rewrite]: #356
+#373 := [monotonicity #357 #370]: #372
+#377 := [trans #373 #375]: #376
+#380 := [quant-intro #377]: #379
+#353 := [asserted]: #106
+#383 := [mp #353 #380]: #378
+#439 := [mp~ #383 #408]: #378
+#971 := [mp #439 #970]: #966
+#494 := (not #966)
+#579 := (or #494 #382)
+#580 := [quant-inst #107]: #579
+[unit-resolution #580 #971 #391]: false
+unsat