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

faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
custom-made (top-down) atomize_conv,
store predicate and function symbols in a table instead of a list for faster lookup,
updated certificates

#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