1.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Fri Dec 17 12:02:46 2010 +0100
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Fri Dec 17 12:02:57 2010 +0100
     1.3 @@ -14816,3 +14816,80 @@
     1.4  #287 := [mp #270 #284]: #282
     1.5  [unit-resolution #287 #630]: false
     1.6  unsat
     1.7 +a7ba12fdd24a1cfe15f53475941aaf6855022b7f 76 0
     1.8 +#2 := false
     1.9 +decl f28 :: (-> Int S1)
    1.10 +#107 := 1::Int
    1.11 +#108 := (f28 1::Int)
    1.12 +decl f1 :: S1
    1.13 +#4 := f1
    1.14 +#382 := (= f1 #108)
    1.15 +#386 := (not #382)
    1.16 +#109 := (= #108 f1)
    1.17 +#110 := (not #109)
    1.18 +#387 := (iff #110 #386)
    1.19 +#384 := (iff #109 #382)
    1.20 +#385 := [rewrite]: #384
    1.21 +#388 := [monotonicity #385]: #387
    1.22 +#381 := [asserted]: #110
    1.23 +#391 := [mp #381 #388]: #386
    1.24 +#96 := (:var 0 Int)
    1.25 +#97 := (f28 #96)
    1.26 +#965 := (pattern #97)
    1.27 +#354 := (= f1 #97)
    1.28 +#966 := (forall (vars (?v0 Int)) (:pat #965) #354)
    1.29 +#378 := (forall (vars (?v0 Int)) #354)
    1.30 +#969 := (iff #378 #966)
    1.31 +#967 := (iff #354 #354)
    1.32 +#968 := [refl]: #967
    1.33 +#970 := [quant-intro #968]: #969
    1.34 +#407 := (~ #378 #378)
    1.35 +#437 := (~ #354 #354)
    1.36 +#438 := [refl]: #437
    1.37 +#408 := [nnf-pos #438]: #407
    1.38 +decl f3 :: (-> S2 S1)
    1.39 +decl f29 :: (-> Int S2 S2)
    1.40 +decl f30 :: S2
    1.41 +#99 := f30
    1.42 +#100 := (f29 #96 f30)
    1.43 +#101 := (f3 #100)
    1.44 +#102 := (= #101 f1)
    1.45 +#103 := (not #102)
    1.46 +#104 := (or #102 #103)
    1.47 +#98 := (= #97 f1)
    1.48 +#105 := (and #98 #104)
    1.49 +#106 := (forall (vars (?v0 Int)) #105)
    1.50 +#379 := (iff #106 #378)
    1.51 +#376 := (iff #105 #354)
    1.52 +#1 := true
    1.53 +#371 := (and #354 true)
    1.54 +#374 := (iff #371 #354)
    1.55 +#375 := [rewrite]: #374
    1.56 +#372 := (iff #105 #371)
    1.57 +#369 := (iff #104 true)
    1.58 +#358 := (= f1 #101)
    1.59 +#361 := (not #358)
    1.60 +#364 := (or #358 #361)
    1.61 +#367 := (iff #364 true)
    1.62 +#368 := [rewrite]: #367
    1.63 +#365 := (iff #104 #364)
    1.64 +#362 := (iff #103 #361)
    1.65 +#359 := (iff #102 #358)
    1.66 +#360 := [rewrite]: #359
    1.67 +#363 := [monotonicity #360]: #362
    1.68 +#366 := [monotonicity #360 #363]: #365
    1.69 +#370 := [trans #366 #368]: #369
    1.70 +#356 := (iff #98 #354)
    1.71 +#357 := [rewrite]: #356
    1.72 +#373 := [monotonicity #357 #370]: #372
    1.73 +#377 := [trans #373 #375]: #376
    1.74 +#380 := [quant-intro #377]: #379
    1.75 +#353 := [asserted]: #106
    1.76 +#383 := [mp #353 #380]: #378
    1.77 +#439 := [mp~ #383 #408]: #378
    1.78 +#971 := [mp #439 #970]: #966
    1.79 +#494 := (not #966)
    1.80 +#579 := (or #494 #382)
    1.81 +#580 := [quant-inst #107]: #579
    1.82 +[unit-resolution #580 #971 #391]: false
    1.83 +unsat