diff -r b0ff69f0a248 -r 39f73a59e855 src/HOL/SMT/Examples/cert/z3_fol_04.proof
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_fol_04.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,56 @@
+#2 := false
+decl up_1 :: (-> T1 bool)
+decl uf_2 :: T1
+#4 := uf_2
+#5 := (up_1 uf_2)
+decl uf_3 :: T1
+#13 := uf_3
+#14 := (up_1 uf_3)
+#34 := (not #5)
+#35 := (or #34 #14)
+#38 := (not #35)
+#15 := (implies #5 #14)
+#16 := (not #15)
+#39 := (iff #16 #38)
+#36 := (iff #15 #35)
+#37 := [rewrite]: #36
+#40 := [monotonicity #37]: #39
+#33 := [asserted]: #16
+#43 := [mp #33 #40]: #38
+#41 := [not-or-elim #43]: #5
+#6 := (:var 0 T1)
+#7 := (up_1 #6)
+#536 := (pattern #7)
+#10 := (not #7)
+#537 := (forall (vars (?x2 T1)) (:pat #536) #10)
+#11 := (forall (vars (?x2 T1)) #10)
+#540 := (iff #11 #537)
+#538 := (iff #10 #10)
+#539 := [refl]: #538
+#541 := [quant-intro #539]: #540
+#8 := (exists (vars (?x1 T1)) #7)
+#9 := (not #8)
+#45 := (~ #9 #11)
+#50 := (~ #10 #10)
+#51 := [refl]: #50
+#59 := [nnf-neg #51]: #45
+#12 := (ite #5 #9 #11)
+#57 := (iff #12 #9)
+#1 := true
+#52 := (ite true #9 #11)
+#55 := (iff #52 #9)
+#56 := [rewrite]: #55
+#53 := (iff #12 #52)
+#48 := (iff #5 true)
+#49 := [iff-true #41]: #48
+#54 := [monotonicity #49]: #53
+#58 := [trans #54 #56]: #57
+#32 := [asserted]: #12
+#47 := [mp #32 #58]: #9
+#60 := [mp~ #47 #59]: #11
+#542 := [mp #60 #541]: #537
+#119 := (not #537)
+#206 := (or #119 #34)
+#120 := [quant-inst]: #206
+[unit-resolution #120 #542 #41]: false
+unsat