src/HOL/SMT/Examples/cert/z3_arith_quant_13.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
#4 := 0::int
#5 := (:var 0 int)
#48 := (<= #5 0::int)
#49 := (not #48)
#45 := (>= #5 0::int)
#44 := (not #45)
#52 := (or #44 #49)
#55 := (forall (vars (?x1 int)) #52)
#86 := (not #55)
#604 := (<= 0::int 0::int)
#264 := (not #604)
#269 := (>= 0::int 0::int)
#605 := (not #269)
#265 := (or #605 #264)
#588 := (or #86 #265)
#584 := (iff #588 #86)
#311 := (or #86 false)
#314 := (iff #311 #86)
#208 := [rewrite]: #314
#312 := (iff #588 #311)
#599 := (iff #265 false)
#598 := (or false false)
#241 := (iff #598 false)
#601 := [rewrite]: #241
#600 := (iff #265 #598)
#597 := (iff #264 false)
#1 := true
#590 := (not true)
#255 := (iff #590 false)
#256 := [rewrite]: #255
#596 := (iff #264 #590)
#594 := (iff #604 true)
#595 := [rewrite]: #594
#591 := [monotonicity #595]: #596
#235 := [trans #591 #256]: #597
#592 := (iff #605 false)
#253 := (iff #605 #590)
#606 := (iff #269 true)
#249 := [rewrite]: #606
#254 := [monotonicity #249]: #253
#593 := [trans #254 #256]: #592
#240 := [monotonicity #593 #235]: #600
#602 := [trans #240 #601]: #599
#313 := [monotonicity #602]: #312
#585 := [trans #313 #208]: #584
#589 := [quant-inst]: #588
#307 := [mp #589 #585]: #86
decl z3name!0 :: bool
#83 := z3name!0
#12 := 3::int
#32 := -1::int
#92 := (ite z3name!0 -1::int 3::int)
#290 := (= #92 3::int)
#610 := (not #290)
#607 := (>= #92 3::int)
#609 := (not #607)
#95 := (<= #92 0::int)
#58 := (ite #55 -1::int 3::int)
#64 := (<= #58 0::int)
#96 := (~ #64 #95)
#93 := (= #58 #92)
#90 := (~ #55 z3name!0)
#87 := (or z3name!0 #86)
#84 := (not z3name!0)
#85 := (or #84 #55)
#88 := (and #85 #87)
#89 := [intro-def]: #88
#91 := [apply-def #89]: #90
#94 := [monotonicity #91]: #93
#97 := [monotonicity #94]: #96
#10 := 1::int
#11 := (- 1::int)
#7 := (< 0::int #5)
#6 := (< #5 0::int)
#8 := (or #6 #7)
#9 := (forall (vars (?x1 int)) #8)
#13 := (ite #9 #11 3::int)
#14 := (< 0::int #13)
#15 := (not #14)
#77 := (iff #15 #64)
#35 := (ite #9 -1::int 3::int)
#38 := (< 0::int #35)
#41 := (not #38)
#75 := (iff #41 #64)
#65 := (not #64)
#70 := (not #65)
#73 := (iff #70 #64)
#74 := [rewrite]: #73
#71 := (iff #41 #70)
#68 := (iff #38 #65)
#61 := (< 0::int #58)
#66 := (iff #61 #65)
#67 := [rewrite]: #66
#62 := (iff #38 #61)
#59 := (= #35 #58)
#56 := (iff #9 #55)
#53 := (iff #8 #52)
#50 := (iff #7 #49)
#51 := [rewrite]: #50
#46 := (iff #6 #44)
#47 := [rewrite]: #46
#54 := [monotonicity #47 #51]: #53
#57 := [quant-intro #54]: #56
#60 := [monotonicity #57]: #59
#63 := [monotonicity #60]: #62
#69 := [trans #63 #67]: #68
#72 := [monotonicity #69]: #71
#76 := [trans #72 #74]: #75
#42 := (iff #15 #41)
#39 := (iff #14 #38)
#36 := (= #13 #35)
#33 := (= #11 -1::int)
#34 := [rewrite]: #33
#37 := [monotonicity #34]: #36
#40 := [monotonicity #37]: #39
#43 := [monotonicity #40]: #42
#78 := [trans #43 #76]: #77
#31 := [asserted]: #15
#79 := [mp #31 #78]: #64
#126 := [mp~ #79 #97]: #95
#266 := (not #95)
#396 := (or #609 #266)
#603 := [th-lemma]: #396
#277 := [unit-resolution #603 #126]: #609
#278 := [hypothesis]: #290
#611 := (or #610 #607)
#612 := [th-lemma]: #611
#613 := [unit-resolution #612 #278 #277]: false
#608 := [lemma #613]: #610
#289 := (or z3name!0 #290)
#293 := [def-axiom]: #289
#308 := [unit-resolution #293 #608]: z3name!0
#129 := (or #55 #84)
decl ?x1!1 :: int
#108 := ?x1!1
#111 := (>= ?x1!1 0::int)
#112 := (not #111)
#109 := (<= ?x1!1 0::int)
#110 := (not #109)
#132 := (or #110 #112)
#135 := (not #132)
#138 := (or z3name!0 #135)
#141 := (and #129 #138)
#113 := (or #112 #110)
#114 := (not #113)
#119 := (or z3name!0 #114)
#122 := (and #85 #119)
#142 := (iff #122 #141)
#139 := (iff #119 #138)
#136 := (iff #114 #135)
#133 := (iff #113 #132)
#134 := [rewrite]: #133
#137 := [monotonicity #134]: #136
#140 := [monotonicity #137]: #139
#130 := (iff #85 #129)
#131 := [rewrite]: #130
#143 := [monotonicity #131 #140]: #142
#123 := (~ #88 #122)
#120 := (~ #87 #119)
#115 := (~ #86 #114)
#116 := [sk]: #115
#106 := (~ z3name!0 z3name!0)
#107 := [refl]: #106
#121 := [monotonicity #107 #116]: #120
#104 := (~ #85 #85)
#102 := (~ #55 #55)
#100 := (~ #52 #52)
#101 := [refl]: #100
#103 := [nnf-pos #101]: #102
#98 := (~ #84 #84)
#99 := [refl]: #98
#105 := [monotonicity #99 #103]: #104
#124 := [monotonicity #105 #121]: #123
#125 := [mp~ #89 #124]: #122
#127 := [mp #125 #143]: #141
#128 := [and-elim #127]: #129
#582 := [unit-resolution #128 #308]: #55
[unit-resolution #582 #307]: false
unsat