--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_prop_07.proof Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,57 @@
+#2 := false
+decl up_1 :: bool
+#4 := up_1
+#5 := (iff up_1 up_1)
+#6 := (iff #5 up_1)
+#7 := (iff #6 up_1)
+#8 := (iff #7 up_1)
+#9 := (iff #8 up_1)
+#10 := (iff #9 up_1)
+#11 := (iff #10 up_1)
+#12 := (iff #11 up_1)
+#13 := (iff #12 up_1)
+#14 := (not #13)
+#69 := (iff #14 false)
+#1 := true
+#64 := (not true)
+#67 := (iff #64 false)
+#68 := [rewrite]: #67
+#65 := (iff #14 #64)
+#62 := (iff #13 true)
+#31 := (iff #5 true)
+#32 := [rewrite]: #31
+#60 := (iff #13 #5)
+#33 := (iff true up_1)
+#36 := (iff #33 up_1)
+#37 := [rewrite]: #36
+#57 := (iff #12 #33)
+#55 := (iff #11 true)
+#53 := (iff #11 #5)
+#50 := (iff #10 #33)
+#48 := (iff #9 true)
+#46 := (iff #9 #5)
+#43 := (iff #8 #33)
+#41 := (iff #7 true)
+#39 := (iff #7 #5)
+#34 := (iff #6 #33)
+#35 := [monotonicity #32]: #34
+#38 := [trans #35 #37]: #7
+#40 := [monotonicity #38]: #39
+#42 := [trans #40 #32]: #41
+#44 := [monotonicity #42]: #43
+#45 := [trans #44 #37]: #9
+#47 := [monotonicity #45]: #46
+#49 := [trans #47 #32]: #48
+#51 := [monotonicity #49]: #50
+#52 := [trans #51 #37]: #11
+#54 := [monotonicity #52]: #53
+#56 := [trans #54 #32]: #55
+#58 := [monotonicity #56]: #57
+#59 := [trans #58 #37]: #13
+#61 := [monotonicity #59]: #60
+#63 := [trans #61 #32]: #62
+#66 := [monotonicity #63]: #65
+#70 := [trans #66 #68]: #69
+#30 := [asserted]: #14
+[mp #30 #70]: false
+unsat