src/HOL/SMT/Examples/cert/z3_linarith_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 uf_1 :: (-> T1 T2)
decl uf_3 :: T1
#8 := uf_3
#9 := (uf_1 uf_3)
decl uf_2 :: (-> int int T1)
#5 := 3::int
#4 := 2::int
#6 := (uf_2 2::int 3::int)
#7 := (uf_1 #6)
#10 := (= #7 #9)
#225 := (= #6 uf_3)
#13 := (:var 0 int)
#12 := (:var 1 int)
#14 := (uf_2 #12 #13)
#549 := (pattern #14)
#52 := 0::int
#50 := -1::int
#54 := (* -1::int #13)
#55 := (+ #12 #54)
#53 := (>= #55 0::int)
#51 := (not #53)
#36 := (= uf_3 #14)
#61 := (iff #36 #51)
#550 := (forall (vars (?x1 int) (?x2 int)) (:pat #549) #61)
#66 := (forall (vars (?x1 int) (?x2 int)) #61)
#553 := (iff #66 #550)
#551 := (iff #61 #61)
#552 := [refl]: #551
#554 := [quant-intro #552]: #553
#79 := (~ #66 #66)
#77 := (~ #61 #61)
#78 := [refl]: #77
#80 := [nnf-pos #78]: #79
#16 := (< #12 #13)
#15 := (= #14 uf_3)
#17 := (iff #15 #16)
#18 := (forall (vars (?x1 int) (?x2 int)) #17)
#69 := (iff #18 #66)
#42 := (iff #16 #36)
#47 := (forall (vars (?x1 int) (?x2 int)) #42)
#67 := (iff #47 #66)
#64 := (iff #42 #61)
#58 := (iff #51 #36)
#62 := (iff #58 #61)
#63 := [rewrite]: #62
#59 := (iff #42 #58)
#56 := (iff #16 #51)
#57 := [rewrite]: #56
#60 := [monotonicity #57]: #59
#65 := [trans #60 #63]: #64
#68 := [quant-intro #65]: #67
#48 := (iff #18 #47)
#45 := (iff #17 #42)
#39 := (iff #36 #16)
#43 := (iff #39 #42)
#44 := [rewrite]: #43
#40 := (iff #17 #39)
#37 := (iff #15 #36)
#38 := [rewrite]: #37
#41 := [monotonicity #38]: #40
#46 := [trans #41 #44]: #45
#49 := [quant-intro #46]: #48
#70 := [trans #49 #68]: #69
#35 := [asserted]: #18
#71 := [mp #35 #70]: #66
#74 := [mp~ #71 #80]: #66
#555 := [mp #74 #554]: #550
#529 := (not #550)
#530 := (or #529 #225)
#220 := (* -1::int 3::int)
#221 := (+ 2::int #220)
#222 := (>= #221 0::int)
#213 := (not #222)
#135 := (= uf_3 #6)
#224 := (iff #135 #213)
#525 := (or #529 #224)
#169 := (iff #525 #530)
#534 := (iff #530 #530)
#174 := [rewrite]: #534
#527 := (iff #224 #225)
#1 := true
#187 := (iff #225 true)
#190 := (iff #187 #225)
#526 := [rewrite]: #190
#188 := (iff #224 #187)
#183 := (iff #213 true)
#198 := (not false)
#199 := (iff #198 true)
#540 := [rewrite]: #199
#203 := (iff #213 #198)
#548 := (iff #222 false)
#544 := (>= -1::int 0::int)
#547 := (iff #544 false)
#542 := [rewrite]: #547
#545 := (iff #222 #544)
#211 := (= #221 -1::int)
#223 := -3::int
#541 := (+ 2::int -3::int)
#330 := (= #541 -1::int)
#537 := [rewrite]: #330
#543 := (= #221 #541)
#227 := (= #220 -3::int)
#206 := [rewrite]: #227
#200 := [monotonicity #206]: #543
#212 := [trans #200 #537]: #211
#546 := [monotonicity #212]: #545
#538 := [trans #546 #542]: #548
#539 := [monotonicity #538]: #203
#524 := [trans #539 #540]: #183
#153 := (iff #135 #225)
#226 := [rewrite]: #153
#189 := [monotonicity #226 #524]: #188
#528 := [trans #189 #526]: #527
#532 := [monotonicity #528]: #169
#175 := [trans #532 #174]: #169
#531 := [quant-inst]: #525
#535 := [mp #531 #175]: #530
#533 := [unit-resolution #535 #555]: #225
#536 := [monotonicity #533]: #10
#11 := (not #10)
#34 := [asserted]: #11
[unit-resolution #34 #536]: false
unsat