--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_prop_04.proof Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,38 @@
+#2 := false
+decl up_2 :: bool
+#5 := up_2
+decl up_1 :: bool
+#4 := up_1
+#6 := (or up_1 up_2)
+#51 := (iff #6 false)
+#46 := (or false false)
+#49 := (iff #46 false)
+#50 := [rewrite]: #49
+#47 := (iff #6 #46)
+#40 := (iff up_2 false)
+#9 := (not up_2)
+#43 := (iff #9 #40)
+#41 := (iff #40 #9)
+#42 := [rewrite]: #41
+#44 := [symm #42]: #43
+#32 := [asserted]: #9
+#45 := [mp #32 #44]: #40
+#35 := (iff up_1 false)
+#7 := (not up_1)
+#37 := (iff #7 #35)
+#33 := (iff #35 #7)
+#36 := [rewrite]: #33
+#38 := [symm #36]: #37
+#26 := (and #7 #6)
+#8 := (and #6 #7)
+#27 := (iff #8 #26)
+#28 := [rewrite]: #27
+#25 := [asserted]: #8
+#31 := [mp #25 #28]: #26
+#29 := [and-elim #31]: #7
+#39 := [mp #29 #38]: #35
+#48 := [monotonicity #39 #45]: #47
+#52 := [trans #48 #50]: #51
+#30 := [and-elim #31]: #6
+[mp #30 #52]: false
+unsat