--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_prop_02.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,19 @@
+#2 := false
+decl up_1 :: bool
+#4 := up_1
+#5 := (not up_1)
+#6 := (or up_1 #5)
+#7 := (not #6)
+#31 := (iff #7 false)
+#1 := true
+#26 := (not true)
+#29 := (iff #26 false)
+#30 := [rewrite]: #29
+#27 := (iff #7 #26)
+#24 := (iff #6 true)
+#25 := [rewrite]: #24
+#28 := [monotonicity #25]: #27
+#32 := [trans #28 #30]: #31
+#23 := [asserted]: #7
+[mp #23 #32]: false
+unsat