src/HOL/SMT/Examples/cert/z3_nlarith_03.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 uf_2 :: real
#6 := uf_2
decl uf_1 :: real
#4 := uf_1
#12 := 2::real
#13 := (* 2::real uf_1)
#14 := (* #13 uf_2)
#5 := 1::real
#9 := (- 1::real uf_2)
#10 := (* uf_1 #9)
#7 := (+ 1::real uf_2)
#8 := (* uf_1 #7)
#11 := (- #8 #10)
#15 := (= #11 #14)
#16 := (not #15)
#73 := (iff #16 false)
#1 := true
#68 := (not true)
#71 := (iff #68 false)
#72 := [rewrite]: #71
#69 := (iff #16 #68)
#66 := (iff #15 true)
#33 := (* uf_1 uf_2)
#55 := (* 2::real #33)
#61 := (= #55 #55)
#64 := (iff #61 true)
#65 := [rewrite]: #64
#62 := (iff #15 #61)
#59 := (= #14 #55)
#60 := [rewrite]: #59
#57 := (= #11 #55)
#37 := -1::real
#45 := (* -1::real #33)
#46 := (+ uf_1 #45)
#34 := (+ uf_1 #33)
#51 := (- #34 #46)
#54 := (= #51 #55)
#56 := [rewrite]: #54
#52 := (= #11 #51)
#49 := (= #10 #46)
#38 := (* -1::real uf_2)
#39 := (+ 1::real #38)
#42 := (* uf_1 #39)
#47 := (= #42 #46)
#48 := [rewrite]: #47
#43 := (= #10 #42)
#40 := (= #9 #39)
#41 := [rewrite]: #40
#44 := [monotonicity #41]: #43
#50 := [trans #44 #48]: #49
#35 := (= #8 #34)
#36 := [rewrite]: #35
#53 := [monotonicity #36 #50]: #52
#58 := [trans #53 #56]: #57
#63 := [monotonicity #58 #60]: #62
#67 := [trans #63 #65]: #66
#70 := [monotonicity #67]: #69
#74 := [trans #70 #72]: #73
#32 := [asserted]: #16
[mp #32 #74]: false
unsat