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_4 :: T1
#13 := uf_4
decl uf_1 :: (-> int int T1)
#5 := 3::int
decl uf_2 :: int
#4 := uf_2
#6 := (uf_1 uf_2 3::int)
#559 := (= #6 uf_4)
decl uf_3 :: (-> int int T1)
#7 := (uf_3 3::int uf_2)
#254 := (= #7 uf_4)
#524 := (iff #254 #559)
#529 := (iff #559 #254)
#39 := (= #6 #7)
#8 := (distinct #6 #7)
#9 := (not #8)
#48 := (iff #9 #39)
#40 := (not #39)
#43 := (not #40)
#46 := (iff #43 #39)
#47 := [rewrite]: #46
#44 := (iff #9 #43)
#41 := (iff #8 #40)
#42 := [rewrite]: #41
#45 := [monotonicity #42]: #44
#49 := [trans #45 #47]: #48
#38 := [asserted]: #9
#52 := [mp #38 #49]: #39
#523 := [monotonicity #52]: #529
#530 := [symm #523]: #524
#547 := (not #559)
#570 := (not #254)
#531 := (iff #570 #547)
#525 := [monotonicity #530]: #531
#540 := [hypothesis]: #570
#532 := [mp #540 #525]: #547
#256 := (>= uf_2 3::int)
#579 := (not #256)
#541 := (or #254 #579)
#258 := (iff #254 #256)
#11 := (:var 0 int)
#10 := (:var 1 int)
#12 := (uf_3 #10 #11)
#581 := (pattern #12)
#57 := 0::int
#54 := -1::int
#55 := (* -1::int #11)
#56 := (+ #10 #55)
#58 := (<= #56 0::int)
#14 := (= #12 uf_4)
#61 := (iff #14 #58)
#582 := (forall (vars (?x1 int) (?x2 int)) (:pat #581) #61)
#64 := (forall (vars (?x1 int) (?x2 int)) #61)
#585 := (iff #64 #582)
#583 := (iff #61 #61)
#584 := [refl]: #583
#586 := [quant-intro #584]: #585
#108 := (~ #64 #64)
#106 := (~ #61 #61)
#107 := [refl]: #106
#109 := [nnf-pos #107]: #108
#15 := (<= #10 #11)
#16 := (iff #14 #15)
#17 := (forall (vars (?x1 int) (?x2 int)) #16)
#65 := (iff #17 #64)
#62 := (iff #16 #61)
#59 := (iff #15 #58)
#60 := [rewrite]: #59
#63 := [monotonicity #60]: #62
#66 := [quant-intro #63]: #65
#50 := [asserted]: #17
#67 := [mp #50 #66]: #64
#101 := [mp~ #67 #109]: #64
#587 := [mp #101 #586]: #582
#238 := (not #582)
#573 := (or #238 #258)
#167 := (* -1::int uf_2)
#252 := (+ 3::int #167)
#253 := (<= #252 0::int)
#245 := (iff #254 #253)
#575 := (or #238 #245)
#362 := (iff #575 #573)
#243 := (iff #573 #573)
#244 := [rewrite]: #243
#255 := (iff #245 #258)
#257 := (iff #253 #256)
#185 := [rewrite]: #257
#259 := [monotonicity #185]: #255
#569 := [monotonicity #259]: #362
#576 := [trans #569 #244]: #362
#232 := [quant-inst]: #575
#577 := [mp #232 #576]: #573
#535 := [unit-resolution #577 #587]: #258
#578 := (not #258)
#574 := (or #578 #254 #579)
#580 := [def-axiom]: #574
#382 := [unit-resolution #580 #535]: #541
#383 := [unit-resolution #382 #540]: #579
#526 := (or #559 #256)
#273 := (iff #559 #579)
#18 := (uf_1 #10 #11)
#588 := (pattern #18)
#82 := (>= #56 0::int)
#81 := (not #82)
#53 := (= uf_4 #18)
#88 := (iff #53 #81)
#589 := (forall (vars (?x3 int) (?x4 int)) (:pat #588) #88)
#93 := (forall (vars (?x3 int) (?x4 int)) #88)
#592 := (iff #93 #589)
#590 := (iff #88 #88)
#591 := [refl]: #590
#593 := [quant-intro #591]: #592
#102 := (~ #93 #93)
#99 := (~ #88 #88)
#110 := [refl]: #99
#103 := [nnf-pos #110]: #102
#20 := (< #10 #11)
#19 := (= #18 uf_4)
#21 := (iff #19 #20)
#22 := (forall (vars (?x3 int) (?x4 int)) #21)
#96 := (iff #22 #93)
#73 := (iff #20 #53)
#78 := (forall (vars (?x3 int) (?x4 int)) #73)
#94 := (iff #78 #93)
#91 := (iff #73 #88)
#85 := (iff #81 #53)
#89 := (iff #85 #88)
#90 := [rewrite]: #89
#86 := (iff #73 #85)
#83 := (iff #20 #81)
#84 := [rewrite]: #83
#87 := [monotonicity #84]: #86
#92 := [trans #87 #90]: #91
#95 := [quant-intro #92]: #94
#79 := (iff #22 #78)
#76 := (iff #21 #73)
#70 := (iff #53 #20)
#74 := (iff #70 #73)
#75 := [rewrite]: #74
#71 := (iff #21 #70)
#68 := (iff #19 #53)
#69 := [rewrite]: #68
#72 := [monotonicity #69]: #71
#77 := [trans #72 #75]: #76
#80 := [quant-intro #77]: #79
#97 := [trans #80 #95]: #96
#51 := [asserted]: #22
#98 := [mp #51 #97]: #93
#111 := [mp~ #98 #103]: #93
#594 := [mp #111 #593]: #589
#552 := (not #589)
#549 := (or #552 #273)
#219 := (* -1::int 3::int)
#220 := (+ uf_2 #219)
#221 := (>= #220 0::int)
#222 := (not #221)
#556 := (= uf_4 #6)
#558 := (iff #556 #222)
#553 := (or #552 #558)
#264 := (iff #553 #549)
#266 := (iff #549 #549)
#544 := [rewrite]: #266
#274 := (iff #558 #273)
#550 := (iff #222 #579)
#280 := (iff #221 #256)
#562 := -3::int
#206 := (+ -3::int uf_2)
#554 := (>= #206 0::int)
#278 := (iff #554 #256)
#279 := [rewrite]: #278
#555 := (iff #221 #554)
#565 := (= #220 #206)
#201 := (+ uf_2 -3::int)
#207 := (= #201 #206)
#567 := [rewrite]: #207
#564 := (= #220 #201)
#557 := (= #219 -3::int)
#563 := [rewrite]: #557
#566 := [monotonicity #563]: #564
#568 := [trans #566 #567]: #565
#277 := [monotonicity #568]: #555
#173 := [trans #277 #279]: #280
#551 := [monotonicity #173]: #550
#560 := (iff #556 #559)
#561 := [rewrite]: #560
#548 := [monotonicity #561 #551]: #274
#265 := [monotonicity #548]: #264
#545 := [trans #265 #544]: #264
#263 := [quant-inst]: #553
#260 := [mp #263 #545]: #549
#384 := [unit-resolution #260 #594]: #273
#542 := (not #273)
#546 := (or #542 #559 #256)
#543 := [def-axiom]: #546
#527 := [unit-resolution #543 #384]: #526
#528 := [unit-resolution #527 #383]: #559
#361 := [unit-resolution #528 #532]: false
#363 := [lemma #361]: #254
#522 := [mp #363 #530]: #559
#364 := (or #570 #256)
#230 := (or #578 #570 #256)
#235 := [def-axiom]: #230
#517 := [unit-resolution #235 #535]: #364
#518 := [unit-resolution #517 #363]: #256
#520 := (or #547 #579)
#536 := (or #542 #547 #579)
#537 := [def-axiom]: #536
#521 := [unit-resolution #537 #384]: #520
#519 := [unit-resolution #521 #518]: #547
[unit-resolution #519 #522]: false
unsat