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

removed fixme - quick-and-dirty flag is appropriate

#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