--- a/src/HOL/SMT/Examples/cert/z3_hol_03.proof Tue Feb 02 18:11:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,115 +0,0 @@
-#2 := false
-decl up_2 :: (-> T2 bool)
-decl uf_3 :: T2
-#10 := uf_3
-#17 := (up_2 uf_3)
-#78 := (not #17)
-decl uf_1 :: (-> T1 T1)
-decl uf_4 :: T1
-#14 := uf_4
-#15 := (uf_1 uf_4)
-#46 := (= uf_4 #15)
-#79 := (not #46)
-#145 := [hypothesis]: #79
-#4 := (:var 0 T1)
-#5 := (uf_1 #4)
-#563 := (pattern #5)
-#37 := (= #4 #5)
-#564 := (forall (vars (?x1 T1)) (:pat #563) #37)
-#40 := (forall (vars (?x1 T1)) #37)
-#567 := (iff #40 #564)
-#565 := (iff #37 #37)
-#566 := [refl]: #565
-#568 := [quant-intro #566]: #567
-#72 := (~ #40 #40)
-#70 := (~ #37 #37)
-#71 := [refl]: #70
-#73 := [nnf-pos #71]: #72
-#6 := (= #5 #4)
-#7 := (forall (vars (?x1 T1)) #6)
-#41 := (iff #7 #40)
-#38 := (iff #6 #37)
-#39 := [rewrite]: #38
-#42 := [quant-intro #39]: #41
-#36 := [asserted]: #7
-#45 := [mp #36 #42]: #40
-#74 := [mp~ #45 #73]: #40
-#569 := [mp #74 #568]: #564
-#146 := (not #564)
-#233 := (or #146 #46)
-#147 := [quant-inst]: #233
-#232 := [unit-resolution #147 #569 #145]: false
-#234 := [lemma #232]: #46
-#66 := (or #78 #79)
-#54 := (and #17 #46)
-#59 := (not #54)
-#85 := (iff #59 #66)
-#67 := (not #66)
-#80 := (not #67)
-#83 := (iff #80 #66)
-#84 := [rewrite]: #83
-#81 := (iff #59 #80)
-#68 := (iff #54 #67)
-#69 := [rewrite]: #68
-#82 := [monotonicity #69]: #81
-#86 := [trans #82 #84]: #85
-#1 := true
-#18 := (iff #17 true)
-#16 := (= #15 uf_4)
-#19 := (and #16 #18)
-#20 := (not #19)
-#60 := (iff #20 #59)
-#57 := (iff #19 #54)
-#51 := (and #46 #17)
-#55 := (iff #51 #54)
-#56 := [rewrite]: #55
-#52 := (iff #19 #51)
-#49 := (iff #18 #17)
-#50 := [rewrite]: #49
-#47 := (iff #16 #46)
-#48 := [rewrite]: #47
-#53 := [monotonicity #48 #50]: #52
-#58 := [trans #53 #56]: #57
-#61 := [monotonicity #58]: #60
-#44 := [asserted]: #20
-#64 := [mp #44 #61]: #59
-#87 := [mp #64 #86]: #66
-#561 := [unit-resolution #87 #234]: #78
-#8 := (:var 0 T2)
-#9 := (up_2 #8)
-#570 := (pattern #9)
-#11 := (= #8 uf_3)
-#12 := (iff #9 #11)
-#571 := (forall (vars (?x2 T2)) (:pat #570) #12)
-#13 := (forall (vars (?x2 T2)) #12)
-#574 := (iff #13 #571)
-#572 := (iff #12 #12)
-#573 := [refl]: #572
-#575 := [quant-intro #573]: #574
-#65 := (~ #13 #13)
-#75 := (~ #12 #12)
-#76 := [refl]: #75
-#62 := [nnf-pos #76]: #65
-#43 := [asserted]: #13
-#77 := [mp~ #43 #62]: #13
-#576 := [mp #77 #575]: #571
-#555 := (not #571)
-#557 := (or #555 #17)
-#225 := (= uf_3 uf_3)
-#236 := (iff #17 #225)
-#212 := (or #555 #236)
-#551 := (iff #212 #557)
-#224 := (iff #557 #557)
-#558 := [rewrite]: #224
-#239 := (iff #236 #17)
-#238 := (iff #236 #18)
-#237 := (iff #225 true)
-#165 := [rewrite]: #237
-#235 := [monotonicity #165]: #238
-#218 := [trans #235 #50]: #239
-#223 := [monotonicity #218]: #551
-#559 := [trans #223 #558]: #551
-#344 := [quant-inst]: #212
-#560 := [mp #344 #559]: #557
-[unit-resolution #560 #576 #561]: false
-unsat