src/HOL/SMT/Examples/cert/z3_prop_06.proof

+#2 := false
+decl up_1 :: bool
+#4 := up_1
+decl up_3 :: bool
+#7 := up_3
+#10 := (and up_1 up_3)
+decl up_2 :: bool
+#5 := up_2
+#9 := (and up_3 up_2)
+#11 := (or #9 #10)
+#12 := (implies up_1 #11)
+#13 := (or #12 up_1)
+#6 := (and up_1 up_2)
+#8 := (or #6 up_3)
+#14 := (implies #8 #13)
+#15 := (not #14)
+#81 := (iff #15 false)
+#32 := (and up_2 up_3)
+#38 := (or #10 #32)
+#46 := (not up_1)
+#47 := (or #46 #38)
+#55 := (or up_1 #47)
+#63 := (not #8)
+#64 := (or #63 #55)
+#69 := (not #64)
+#79 := (iff #69 false)
+#1 := true
+#74 := (not true)
+#77 := (iff #74 false)
+#78 := [rewrite]: #77
+#75 := (iff #69 #74)
+#72 := (iff #64 true)
+#73 := [rewrite]: #72
+#76 := [monotonicity #73]: #75
+#80 := [trans #76 #78]: #79
+#70 := (iff #15 #69)
+#67 := (iff #14 #64)
+#60 := (implies #8 #55)
+#65 := (iff #60 #64)
+#66 := [rewrite]: #65
+#61 := (iff #14 #60)
+#58 := (iff #13 #55)
+#52 := (or #47 up_1)
+#56 := (iff #52 #55)
+#57 := [rewrite]: #56
+#53 := (iff #13 #52)
+#50 := (iff #12 #47)
+#43 := (implies up_1 #38)
+#48 := (iff #43 #47)
+#49 := [rewrite]: #48
+#44 := (iff #12 #43)
+#41 := (iff #11 #38)
+#35 := (or #32 #10)
+#39 := (iff #35 #38)
+#40 := [rewrite]: #39
+#36 := (iff #11 #35)
+#33 := (iff #9 #32)
+#34 := [rewrite]: #33
+#37 := [monotonicity #34]: #36
+#42 := [trans #37 #40]: #41
+#45 := [monotonicity #42]: #44
+#51 := [trans #45 #49]: #50
+#54 := [monotonicity #51]: #53
+#59 := [trans #54 #57]: #58
+#62 := [monotonicity #59]: #61
+#68 := [trans #62 #66]: #67
+#71 := [monotonicity #68]: #70
+#82 := [trans #71 #80]: #81
+#31 := [asserted]: #15
+[mp #31 #82]: false
+unsat