--- a/src/HOL/SMT_Examples/SMT_Tests.certs Thu Dec 20 15:51:27 2012 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.certs Fri Dec 21 13:33:54 2012 +0100
@@ -56557,3 +56557,1404 @@
#78 := [asserted]: #52
[mp #78 #87]: false
unsat
+f797db065a8c5b2969ce205bd43175da50729663 62 0
+#2 := false
+#22 := 0::Int
+decl f3 :: (-> S2 S3 Int)
+decl f6 :: S3
+#10 := f6
+decl f4 :: S2
+#7 := f4
+#11 := (f3 f4 f6)
+decl f5 :: S3
+#8 := f5
+#9 := (f3 f4 f5)
+#56 := -1::Int
+#57 := (* -1::Int #11)
+#58 := (+ #9 #57)
+#59 := (<= #58 0::Int)
+#62 := (if #59 #9 #11)
+#70 := (* -1::Int #62)
+#253 := (+ #11 #70)
+#602 := (>= #253 0::Int)
+#290 := (= #11 #62)
+#206 := (not #59)
+#205 := (= #9 #62)
+#598 := (not #205)
+#71 := (+ #9 #70)
+#69 := (>= #71 0::Int)
+#75 := (not #69)
+#12 := (<= #9 #11)
+#13 := (if #12 #9 #11)
+#14 := (<= #13 #9)
+#15 := (not #14)
+#76 := (iff #15 #75)
+#73 := (iff #14 #69)
+#65 := (<= #62 #9)
+#68 := (iff #65 #69)
+#72 := [rewrite]: #68
+#66 := (iff #14 #65)
+#63 := (= #13 #62)
+#60 := (iff #12 #59)
+#61 := [rewrite]: #60
+#64 := [monotonicity #61]: #63
+#67 := [monotonicity #64]: #66
+#74 := [trans #67 #72]: #73
+#77 := [monotonicity #74]: #76
+#53 := [asserted]: #15
+#78 := [mp #53 #77]: #75
+#594 := [hypothesis]: #205
+#599 := (or #598 #69)
+#600 := [th-lemma arith triangle-eq]: #599
+#595 := [unit-resolution #600 #594 #78]: false
+#601 := [lemma #595]: #598
+#291 := (or #206 #205)
+#292 := [def-axiom]: #291
+#604 := [unit-resolution #292 #601]: #206
+#283 := (or #59 #290)
+#294 := [def-axiom]: #283
+#244 := [unit-resolution #294 #604]: #290
+#245 := (not #290)
+#605 := (or #245 #602)
+#603 := [th-lemma arith triangle-eq]: #605
+#606 := [unit-resolution #603 #244]: #602
+[th-lemma arith farkas 1 1 1 #78 #604 #606]: false
+unsat
+31e82c3a0418f1a5035c07306f1bcb632442caaa 62 0
+#2 := false
+#22 := 0::Int
+decl f3 :: (-> S2 S3 Int)
+decl f6 :: S3
+#10 := f6
+decl f4 :: S2
+#7 := f4
+#11 := (f3 f4 f6)
+decl f5 :: S3
+#8 := f5
+#9 := (f3 f4 f5)
+#56 := -1::Int
+#57 := (* -1::Int #11)
+#58 := (+ #9 #57)
+#59 := (<= #58 0::Int)
+#62 := (if #59 #9 #11)
+#69 := (* -1::Int #62)
+#70 := (+ #11 #69)
+#68 := (>= #70 0::Int)
+#75 := (not #68)
+#12 := (<= #9 #11)
+#13 := (if #12 #9 #11)
+#14 := (<= #13 #11)
+#15 := (not #14)
+#76 := (iff #15 #75)
+#73 := (iff #14 #68)
+#65 := (<= #62 #11)
+#71 := (iff #65 #68)
+#72 := [rewrite]: #71
+#66 := (iff #14 #65)
+#63 := (= #13 #62)
+#60 := (iff #12 #59)
+#61 := [rewrite]: #60
+#64 := [monotonicity #61]: #63
+#67 := [monotonicity #64]: #66
+#74 := [trans #67 #72]: #73
+#77 := [monotonicity #74]: #76
+#53 := [asserted]: #15
+#78 := [mp #53 #77]: #75
+#290 := (= #11 #62)
+#206 := (not #59)
+#599 := [hypothesis]: #59
+#253 := (+ #9 #69)
+#598 := (>= #253 0::Int)
+#205 := (= #9 #62)
+#291 := (or #206 #205)
+#292 := [def-axiom]: #291
+#600 := [unit-resolution #292 #599]: #205
+#595 := (not #205)
+#601 := (or #595 #598)
+#239 := [th-lemma arith triangle-eq]: #601
+#602 := [unit-resolution #239 #600]: #598
+#604 := [th-lemma arith farkas -1 1 1 #602 #78 #599]: false
+#244 := [lemma #604]: #206
+#283 := (or #59 #290)
+#294 := [def-axiom]: #283
+#245 := [unit-resolution #294 #244]: #290
+#605 := (not #290)
+#603 := (or #605 #68)
+#606 := [th-lemma arith triangle-eq]: #603
+[unit-resolution #606 #245 #78]: false
+unsat
+255fa9c9d454506807f3975ef67899ee95170888 238 0
+#2 := false
+#23 := 0::Int
+decl f3 :: (-> S2 S3 Int)
+decl f6 :: S3
+#10 := f6
+decl f4 :: S2
+#7 := f4
+#11 := (f3 f4 f6)
+decl f5 :: S3
+#8 := f5
+#9 := (f3 f4 f5)
+#57 := -1::Int
+#58 := (* -1::Int #11)
+#59 := (+ #9 #58)
+#60 := (<= #59 0::Int)
+#63 := (if #60 #9 #11)
+#72 := (* -1::Int #63)
+#255 := (+ #9 #72)
+#600 := (>= #255 0::Int)
+#607 := (not #600)
+#617 := (>= #11 0::Int)
+#586 := (= #11 0::Int)
+decl f7 :: (-> S4 Int S3)
+decl f8 :: S4
+#17 := f8
+#295 := (f7 f8 #11)
+#618 := (f3 f4 #295)
+#271 := (= #618 0::Int)
+#592 := (not #617)
+#439 := [hypothesis]: #592
+#612 := (or #617 #271)
+#24 := (:var 0 Int)
+#26 := (f7 f8 #24)
+#628 := (pattern #26)
+#27 := (f3 f4 #26)
+#32 := (= #27 0::Int)
+#89 := (>= #24 0::Int)
+#120 := (or #89 #32)
+#635 := (forall (vars (?v0 Int)) (:pat #628) #120)
+#123 := (forall (vars (?v0 Int)) #120)
+#638 := (iff #123 #635)
+#636 := (iff #120 #120)
+#637 := [refl]: #636
+#639 := [quant-intro #637]: #638
+#136 := (~ #123 #123)
+#144 := (~ #120 #120)
+#145 := [refl]: #144
+#137 := [nnf-pos #145]: #136
+#31 := (< #24 0::Int)
+#33 := (implies #31 #32)
+#34 := (forall (vars (?v0 Int)) #33)
+#126 := (iff #34 #123)
+#104 := (not #31)
+#105 := (or #104 #32)
+#108 := (forall (vars (?v0 Int)) #105)
+#124 := (iff #108 #123)
+#121 := (iff #105 #120)
+#118 := (iff #104 #89)
+#91 := (not #89)
+#113 := (not #91)
+#116 := (iff #113 #89)
+#117 := [rewrite]: #116
+#114 := (iff #104 #113)
+#111 := (iff #31 #91)
+#112 := [rewrite]: #111
+#115 := [monotonicity #112]: #114
+#119 := [trans #115 #117]: #118
+#122 := [monotonicity #119]: #121
+#125 := [quant-intro #122]: #124
+#109 := (iff #34 #108)
+#106 := (iff #33 #105)
+#107 := [rewrite]: #106
+#110 := [quant-intro #107]: #109
+#127 := [trans #110 #125]: #126
+#103 := [asserted]: #34
+#128 := [mp #103 #127]: #123
+#146 := [mp~ #128 #137]: #123
+#640 := [mp #146 #639]: #635
+#619 := (not #635)
+#259 := (or #619 #617 #271)
+#260 := (or #619 #612)
+#262 := (iff #260 #259)
+#598 := [rewrite]: #262
+#261 := [quant-inst #11]: #260
+#599 := [mp #261 #598]: #259
+#304 := [unit-resolution #599 #640]: #612
+#454 := [unit-resolution #304 #439]: #271
+#300 := (= #11 #618)
+#584 := (= f6 #295)
+#299 := (= #295 f6)
+#18 := (:var 0 S3)
+#19 := (f3 f4 #18)
+#621 := (pattern #19)
+#20 := (f7 f8 #19)
+#21 := (= #20 #18)
+#622 := (forall (vars (?v0 S3)) (:pat #621) #21)
+#22 := (forall (vars (?v0 S3)) #21)
+#625 := (iff #22 #622)
+#623 := (iff #21 #21)
+#624 := [refl]: #623
+#626 := [quant-intro #624]: #625
+#142 := (~ #22 #22)
+#140 := (~ #21 #21)
+#141 := [refl]: #140
+#143 := [nnf-pos #141]: #142
+#55 := [asserted]: #22
+#132 := [mp~ #55 #143]: #22
+#627 := [mp #132 #626]: #622
+#278 := (not #622)
+#609 := (or #278 #299)
+#283 := [quant-inst #10]: #609
+#306 := [unit-resolution #283 #627]: #299
+#585 := [symm #306]: #584
+#582 := [monotonicity #585]: #300
+#456 := [trans #582 #454]: #586
+#457 := (not #586)
+#450 := (or #457 #617)
+#458 := [th-lemma arith triangle-eq]: #450
+#459 := [unit-resolution #458 #439 #456]: false
+#460 := [lemma #459]: #617
+#555 := (or #592 #607)
+#73 := (+ #11 #72)
+#74 := (+ #9 #73)
+#70 := (>= #74 0::Int)
+#77 := (not #70)
+#14 := (+ #9 #11)
+#12 := (<= #9 #11)
+#13 := (if #12 #9 #11)
+#15 := (<= #13 #14)
+#16 := (not #15)
+#78 := (iff #16 #77)
+#75 := (iff #15 #70)
+#66 := (<= #63 #14)
+#69 := (iff #66 #70)
+#71 := [rewrite]: #69
+#67 := (iff #15 #66)
+#64 := (= #13 #63)
+#61 := (iff #12 #60)
+#62 := [rewrite]: #61
+#65 := [monotonicity #62]: #64
+#68 := [monotonicity #65]: #67
+#76 := [trans #68 #71]: #75
+#79 := [monotonicity #76]: #78
+#54 := [asserted]: #16
+#80 := [mp #54 #79]: #77
+#589 := (or #592 #607 #70)
+#593 := [th-lemma arith assign-bounds 1 -1]: #589
+#552 := [unit-resolution #593 #80]: #555
+#556 := [unit-resolution #552 #460]: #607
+#207 := (= #9 #63)
+#297 := (f7 f8 #9)
+#402 := (f3 f4 #297)
+#284 := (= #402 0::Int)
+#405 := (iff #284 #207)
+#445 := (iff #207 #284)
+#562 := (= #63 0::Int)
+#424 := (>= #73 0::Int)
+#292 := (= #11 #63)
+#580 := (iff #284 #292)
+#574 := (iff #292 #284)
+#587 := (= 0::Int #402)
+#578 := (iff #587 #284)
+#573 := [commutativity]: #578
+#576 := (iff #292 #587)
+#314 := (= #63 #402)
+#591 := (= #9 #402)
+#319 := (= f5 #297)
+#298 := (= #297 f5)
+#613 := (or #278 #298)
+#615 := [quant-inst #8]: #613
+#318 := [unit-resolution #615 #627]: #298
+#320 := [symm #318]: #319
+#313 := [monotonicity #320]: #591
+#214 := (= #63 #9)
+#601 := (not #292)
+#602 := [hypothesis]: #601
+#285 := (or #60 #292)
+#296 := [def-axiom]: #285
+#597 := [unit-resolution #296 #602]: #60
+#208 := (not #60)
+#293 := (or #208 #207)
+#294 := [def-axiom]: #293
+#603 := [unit-resolution #294 #597]: #207
+#590 := [symm #603]: #214
+#588 := [trans #590 #313]: #314
+#241 := (not #207)
+#604 := (or #241 #600)
+#606 := [th-lemma arith triangle-eq]: #604
+#246 := [unit-resolution #606 #603]: #600
+#303 := [unit-resolution #593 #246 #80]: #592
+#305 := [unit-resolution #304 #303]: #271
+#583 := [trans #582 #305]: #586
+#577 := [monotonicity #583 #588]: #576
+#579 := [trans #577 #573]: #574
+#575 := [symm #579]: #580
+#272 := (>= #9 0::Int)
+#247 := (not #272)
+#605 := (or #247 #208 #607 #70)
+#608 := [th-lemma arith assign-bounds -1 1 -1]: #605
+#594 := [unit-resolution #608 #597 #80 #246]: #247
+#616 := (or #272 #284)
+#614 := (or #619 #272 #284)
+#620 := (or #619 #616)
+#270 := (iff #620 #614)
+#275 := [rewrite]: #270
+#610 := [quant-inst #9]: #620
+#611 := [mp #610 #275]: #614
+#595 := [unit-resolution #611 #640]: #616
+#317 := [unit-resolution #595 #594]: #284
+#581 := [mp #317 #575]: #292
+#422 := [unit-resolution #602 #581]: false
+#423 := [lemma #422]: #292
+#567 := (or #601 #424)
+#568 := [th-lemma arith triangle-eq]: #567
+#569 := [unit-resolution #568 #423]: #424
+#566 := [hypothesis]: #241
+#572 := [unit-resolution #294 #566]: #208
+#563 := (not #424)
+#401 := (or #592 #563 #60 #70)
+#403 := [th-lemma arith assign-bounds 1 1 1]: #401
+#404 := [unit-resolution #403 #572 #80 #569]: #592
+#557 := [unit-resolution #304 #404]: #271
+#561 := (= #63 #618)
+#558 := (= #63 #11)
+#560 := [symm #423]: #558
+#559 := [trans #560 #582]: #561
+#444 := [trans #559 #557]: #562
+#446 := [monotonicity #313 #444]: #445
+#553 := [symm #446]: #405
+#564 := (or #247 #563 #70)
+#570 := [th-lemma arith assign-bounds 1 -1]: #564
+#571 := [unit-resolution #570 #569 #80]: #247
+#565 := [unit-resolution #595 #571]: #284
+#455 := [mp #565 #553]: #207
+#550 := [unit-resolution #566 #455]: false
+#551 := [lemma #550]: #207
+[unit-resolution #606 #551 #556]: false
+unsat
+045d7d8d25dac55517e319701f444d30bf2a94d9 109 0
+#2 := false
+#28 := 0::Int
+decl f3 :: (-> S2 S3 Int)
+decl f7 :: S3
+#13 := f7
+decl f4 :: S2
+#7 := f4
+#14 := (f3 f4 f7)
+decl f6 :: S3
+#10 := f6
+#11 := (f3 f4 f6)
+#67 := -1::Int
+#76 := (* -1::Int #14)
+#86 := (+ #11 #76)
+#87 := (<= #86 0::Int)
+#90 := (if #87 #11 #14)
+#98 := (* -1::Int #90)
+decl f5 :: S3
+#8 := f5
+#9 := (f3 f4 f5)
+#99 := (+ #9 #98)
+#97 := (>= #99 0::Int)
+#96 := (not #97)
+#77 := (+ #9 #76)
+#75 := (>= #77 0::Int)
+#74 := (not #75)
+#70 := (* -1::Int #11)
+#71 := (+ #9 #70)
+#69 := (>= #71 0::Int)
+#68 := (not #69)
+#80 := (and #68 #74)
+#83 := (not #80)
+#104 := (or #83 #96)
+#107 := (not #104)
+#17 := (<= #11 #14)
+#18 := (if #17 #11 #14)
+#19 := (< #9 #18)
+#15 := (< #9 #14)
+#12 := (< #9 #11)
+#16 := (and #12 #15)
+#20 := (implies #16 #19)
+#21 := (not #20)
+#110 := (iff #21 #107)
+#60 := (not #16)
+#61 := (or #60 #19)
+#64 := (not #61)
+#108 := (iff #64 #107)
+#105 := (iff #61 #104)
+#102 := (iff #19 #96)
+#93 := (< #9 #90)
+#100 := (iff #93 #96)
+#101 := [rewrite]: #100
+#94 := (iff #19 #93)
+#91 := (= #18 #90)
+#88 := (iff #17 #87)
+#89 := [rewrite]: #88
+#92 := [monotonicity #89]: #91
+#95 := [monotonicity #92]: #94
+#103 := [trans #95 #101]: #102
+#84 := (iff #60 #83)
+#81 := (iff #16 #80)
+#78 := (iff #15 #74)
+#79 := [rewrite]: #78
+#72 := (iff #12 #68)
+#73 := [rewrite]: #72
+#82 := [monotonicity #73 #79]: #81
+#85 := [monotonicity #82]: #84
+#106 := [monotonicity #85 #103]: #105
+#109 := [monotonicity #106]: #108
+#65 := (iff #21 #64)
+#62 := (iff #20 #61)
+#63 := [rewrite]: #62
+#66 := [monotonicity #63]: #65
+#111 := [trans #66 #109]: #110
+#59 := [asserted]: #21
+#112 := [mp #59 #111]: #107
+#116 := [not-or-elim #112]: #97
+#113 := [not-or-elim #112]: #80
+#115 := [and-elim #113]: #74
+#633 := (+ #14 #98)
+#630 := (<= #633 0::Int)
+#330 := (= #14 #90)
+#246 := (not #87)
+#245 := (= #11 #90)
+#628 := (not #245)
+#642 := (+ #11 #98)
+#644 := (<= #642 0::Int)
+#357 := (not #644)
+#114 := [and-elim #113]: #68
+#355 := [hypothesis]: #644
+#356 := [th-lemma arith farkas -1 -1 1 #355 #114 #116]: false
+#358 := [lemma #356]: #357
+#252 := [hypothesis]: #245
+#629 := (or #628 #644)
+#351 := [th-lemma arith triangle-eq]: #629
+#352 := [unit-resolution #351 #252 #358]: false
+#626 := [lemma #352]: #628
+#331 := (or #246 #245)
+#332 := [def-axiom]: #331
+#631 := [unit-resolution #332 #626]: #246
+#323 := (or #87 #330)
+#334 := [def-axiom]: #323
+#341 := [unit-resolution #334 #631]: #330
+#342 := (not #330)
+#343 := (or #342 #630)
+#344 := [th-lemma arith triangle-eq]: #343
+#622 := [unit-resolution #344 #341]: #630
+[th-lemma arith farkas -1 -1 1 #622 #115 #116]: false
+unsat
+1962433f8497846ba06e564f4ca48d7e020eb6e0 141 0
+#2 := false
+#10 := 0::Int
+decl f3 :: (-> S2 S3 Int)
+decl f6 :: (-> S4 Int S3)
+decl f5 :: S3
+#8 := f5
+decl f4 :: S2
+#7 := f4
+#9 := (f3 f4 f5)
+decl f7 :: S4
+#12 := f7
+#272 := (f6 f7 #9)
+#570 := (f3 f4 #272)
+#277 := (= #570 0::Int)
+#543 := (= #9 0::Int)
+#11 := (<= #9 0::Int)
+#13 := (f6 f7 0::Int)
+#14 := (if #11 f5 #13)
+#266 := (= #13 #14)
+#567 := (not #266)
+#15 := (= #14 #13)
+#16 := (not #15)
+#564 := (iff #16 #567)
+#293 := (iff #15 #266)
+#294 := [commutativity]: #293
+#568 := [monotonicity #294]: #564
+#52 := [asserted]: #16
+#278 := [mp #52 #568]: #567
+#259 := (or #11 #266)
+#270 := [def-axiom]: #259
+#279 := [unit-resolution #270 #278]: #11
+#569 := (>= #9 0::Int)
+#541 := (not #277)
+#181 := (= f5 #14)
+#182 := (not #11)
+#267 := (or #182 #181)
+#268 := [def-axiom]: #267
+#280 := [unit-resolution #268 #279]: #181
+#556 := (= #13 f5)
+#269 := (= #272 f5)
+#17 := (:var 0 S3)
+#18 := (f3 f4 #17)
+#596 := (pattern #18)
+#19 := (f6 f7 #18)
+#20 := (= #19 #17)
+#597 := (forall (vars (?v0 S3)) (:pat #596) #20)
+#21 := (forall (vars (?v0 S3)) #20)
+#600 := (iff #21 #597)
+#598 := (iff #20 #20)
+#599 := [refl]: #598
+#601 := [quant-intro #599]: #600
+#116 := (~ #21 #21)
+#114 := (~ #20 #20)
+#115 := [refl]: #114
+#117 := [nnf-pos #115]: #116
+#53 := [asserted]: #21
+#106 := [mp~ #53 #117]: #21
+#602 := [mp #106 #601]: #597
+#588 := (not #597)
+#590 := (or #588 #269)
+#246 := [quant-inst #8]: #590
+#281 := [unit-resolution #246 #602]: #269
+#549 := (= #13 #272)
+#553 := (= 0::Int #9)
+#551 := (= #570 #9)
+#557 := (= #9 #570)
+#560 := (= f5 #272)
+#274 := [symm #281]: #560
+#561 := [monotonicity #274]: #557
+#552 := [symm #561]: #551
+#558 := (= 0::Int #570)
+#559 := [hypothesis]: #277
+#562 := [symm #559]: #558
+#548 := [trans #562 #552]: #553
+#554 := [monotonicity #548]: #549
+#397 := [trans #554 #281]: #556
+#398 := [trans #397 #280]: #266
+#399 := [unit-resolution #278 #398]: false
+#542 := [lemma #399]: #541
+#292 := (or #569 #277)
+#22 := (:var 0 Int)
+#24 := (f6 f7 #22)
+#603 := (pattern #24)
+#25 := (f3 f4 #24)
+#30 := (= #25 0::Int)
+#64 := (>= #22 0::Int)
+#94 := (or #64 #30)
+#610 := (forall (vars (?v0 Int)) (:pat #603) #94)
+#97 := (forall (vars (?v0 Int)) #94)
+#613 := (iff #97 #610)
+#611 := (iff #94 #94)
+#612 := [refl]: #611
+#614 := [quant-intro #612]: #613
+#110 := (~ #97 #97)
+#118 := (~ #94 #94)
+#119 := [refl]: #118
+#111 := [nnf-pos #119]: #110
+#29 := (< #22 0::Int)
+#31 := (implies #29 #30)
+#32 := (forall (vars (?v0 Int)) #31)
+#100 := (iff #32 #97)
+#78 := (not #29)
+#79 := (or #78 #30)
+#82 := (forall (vars (?v0 Int)) #79)
+#98 := (iff #82 #97)
+#95 := (iff #79 #94)
+#92 := (iff #78 #64)
+#65 := (not #64)
+#87 := (not #65)
+#90 := (iff #87 #64)
+#91 := [rewrite]: #90
+#88 := (iff #78 #87)
+#85 := (iff #29 #65)
+#86 := [rewrite]: #85
+#89 := [monotonicity #86]: #88
+#93 := [trans #89 #91]: #92
+#96 := [monotonicity #93]: #95
+#99 := [quant-intro #96]: #98
+#83 := (iff #32 #82)
+#80 := (iff #31 #79)
+#81 := [rewrite]: #80
+#84 := [quant-intro #81]: #83
+#101 := [trans #84 #99]: #100
+#77 := [asserted]: #32
+#102 := [mp #77 #101]: #97
+#120 := [mp~ #102 #111]: #97
+#615 := [mp #120 #614]: #610
+#295 := (not #610)
+#188 := (or #295 #569 #277)
+#565 := (or #295 #292)
+#288 := (iff #565 #188)
+#289 := [rewrite]: #288
+#566 := [quant-inst #9]: #565
+#563 := [mp #566 #289]: #188
+#555 := [unit-resolution #563 #615]: #292
+#550 := [unit-resolution #555 #542]: #569
+#544 := [th-lemma arith eq-propagate 0 0 #550 #279]: #543
+#538 := [monotonicity #281]: #551
+#539 := [trans #538 #544]: #277
+[unit-resolution #542 #539]: false
+unsat
+f80dc9916afc1b74e708843f9de068b19b70dd30 62 0
+#2 := false
+#22 := 0::Int
+decl f3 :: (-> S2 S3 Int)
+decl f5 :: S3
+#8 := f5
+decl f4 :: S2
+#7 := f4
+#9 := (f3 f4 f5)
+decl f6 :: S3
+#10 := f6
+#11 := (f3 f4 f6)
+#56 := -1::Int
+#57 := (* -1::Int #11)
+#58 := (+ #9 #57)
+#59 := (<= #58 0::Int)
+#62 := (if #59 #11 #9)
+#68 := (* -1::Int #62)
+#69 := (+ #9 #68)
+#70 := (<= #69 0::Int)
+#75 := (not #70)
+#12 := (<= #9 #11)
+#13 := (if #12 #11 #9)
+#14 := (<= #9 #13)
+#15 := (not #14)
+#76 := (iff #15 #75)
+#73 := (iff #14 #70)
+#65 := (<= #9 #62)
+#71 := (iff #65 #70)
+#72 := [rewrite]: #71
+#66 := (iff #14 #65)
+#63 := (= #13 #62)
+#60 := (iff #12 #59)
+#61 := [rewrite]: #60
+#64 := [monotonicity #61]: #63
+#67 := [monotonicity #64]: #66
+#74 := [trans #67 #72]: #73
+#77 := [monotonicity #74]: #76
+#53 := [asserted]: #15
+#78 := [mp #53 #77]: #75
+#290 := (= #9 #62)
+#206 := (not #59)
+#599 := [hypothesis]: #59
+#253 := (+ #11 #68)
+#594 := (<= #253 0::Int)
+#205 := (= #11 #62)
+#291 := (or #206 #205)
+#292 := [def-axiom]: #291
+#600 := [unit-resolution #292 #599]: #205
+#595 := (not #205)
+#601 := (or #595 #594)
+#239 := [th-lemma arith triangle-eq]: #601
+#602 := [unit-resolution #239 #600]: #594
+#604 := [th-lemma arith farkas 1 -1 1 #602 #78 #599]: false
+#244 := [lemma #604]: #206
+#283 := (or #59 #290)
+#294 := [def-axiom]: #283
+#245 := [unit-resolution #294 #244]: #290
+#605 := (not #290)
+#603 := (or #605 #70)
+#606 := [th-lemma arith triangle-eq]: #603
+[unit-resolution #606 #245 #78]: false
+unsat
+863d026b871fd01ad877b22fe75d3d9947adc4c3 62 0
+#2 := false
+#22 := 0::Int
+decl f3 :: (-> S2 S3 Int)
+decl f6 :: S3
+#10 := f6
+decl f4 :: S2
+#7 := f4
+#11 := (f3 f4 f6)
+decl f5 :: S3
+#8 := f5
+#9 := (f3 f4 f5)
+#56 := -1::Int
+#59 := (* -1::Int #11)
+#60 := (+ #9 #59)
+#58 := (>= #60 0::Int)
+#62 := (if #58 #9 #11)
+#68 := (* -1::Int #62)
+#253 := (+ #11 #68)
+#239 := (<= #253 0::Int)
+#290 := (= #11 #62)
+#206 := (not #58)
+#205 := (= #9 #62)
+#598 := (not #205)
+#69 := (+ #9 #68)
+#70 := (<= #69 0::Int)
+#75 := (not #70)
+#12 := (<= #11 #9)
+#13 := (if #12 #9 #11)
+#14 := (<= #9 #13)
+#15 := (not #14)
+#76 := (iff #15 #75)
+#73 := (iff #14 #70)
+#65 := (<= #9 #62)
+#71 := (iff #65 #70)
+#72 := [rewrite]: #71
+#66 := (iff #14 #65)
+#63 := (= #13 #62)
+#57 := (iff #12 #58)
+#61 := [rewrite]: #57
+#64 := [monotonicity #61]: #63
+#67 := [monotonicity #64]: #66
+#74 := [trans #67 #72]: #73
+#77 := [monotonicity #74]: #76
+#53 := [asserted]: #15
+#78 := [mp #53 #77]: #75
+#594 := [hypothesis]: #205
+#599 := (or #598 #70)
+#600 := [th-lemma arith triangle-eq]: #599
+#595 := [unit-resolution #600 #594 #78]: false
+#601 := [lemma #595]: #598
+#291 := (or #206 #205)
+#292 := [def-axiom]: #291
+#604 := [unit-resolution #292 #601]: #206
+#283 := (or #58 #290)
+#294 := [def-axiom]: #283
+#244 := [unit-resolution #294 #604]: #290
+#245 := (not #290)
+#605 := (or #245 #239)
+#603 := [th-lemma arith triangle-eq]: #605
+#606 := [unit-resolution #603 #244]: #239
+[th-lemma arith farkas 1 1 1 #78 #604 #606]: false
+unsat
+54dc3056c3d64c5f00f83943070ff19ad35f8f48 409 0
+#2 := false
+#29 := 0::Int
+decl f3 :: (-> S2 S3 Int)
+decl f5 :: (-> S4 Int S3)
+decl f8 :: S3
+#11 := f8
+decl f4 :: S2
+#7 := f4
+#12 := (f3 f4 f8)
+decl f7 :: S3
+#9 := f7
+#10 := (f3 f4 f7)
+#61 := -1::Int
+#72 := (* -1::Int #10)
+#73 := (+ #72 #12)
+decl f6 :: S4
+#8 := f6
+#76 := (f5 f6 #73)
+#79 := (f3 f4 #76)
+#62 := (* -1::Int #12)
+#341 := (+ #62 #79)
+#619 := (+ #10 #341)
+#459 := (<= #619 0::Int)
+#620 := (= #619 0::Int)
+#63 := (+ #10 #62)
+#91 := (<= #63 0::Int)
+#94 := (if #91 #12 #10)
+#100 := (* -1::Int #94)
+#564 := (+ #10 #100)
+#540 := (<= #564 0::Int)
+#521 := (not #540)
+#594 := (<= #79 0::Int)
+#602 := (= #79 0::Int)
+#243 := (not #91)
+#487 := [hypothesis]: #243
+#604 := (or #91 #602)
+#30 := (:var 0 Int)
+#32 := (f5 f6 #30)
+#663 := (pattern #32)
+#33 := (f3 f4 #32)
+#38 := (= #33 0::Int)
+#124 := (>= #30 0::Int)
+#155 := (or #124 #38)
+#670 := (forall (vars (?v0 Int)) (:pat #663) #155)
+#158 := (forall (vars (?v0 Int)) #155)
+#673 := (iff #158 #670)
+#671 := (iff #155 #155)
+#672 := [refl]: #671
+#674 := [quant-intro #672]: #673
+#171 := (~ #158 #158)
+#179 := (~ #155 #155)
+#180 := [refl]: #179
+#172 := [nnf-pos #180]: #171
+#37 := (< #30 0::Int)
+#39 := (implies #37 #38)
+#40 := (forall (vars (?v0 Int)) #39)
+#161 := (iff #40 #158)
+#139 := (not #37)
+#140 := (or #139 #38)
+#143 := (forall (vars (?v0 Int)) #140)
+#159 := (iff #143 #158)
+#156 := (iff #140 #155)
+#153 := (iff #139 #124)
+#126 := (not #124)
+#148 := (not #126)
+#151 := (iff #148 #124)
+#152 := [rewrite]: #151
+#149 := (iff #139 #148)
+#146 := (iff #37 #126)
+#147 := [rewrite]: #146
+#150 := [monotonicity #147]: #149
+#154 := [trans #150 #152]: #153
+#157 := [monotonicity #154]: #156
+#160 := [quant-intro #157]: #159
+#144 := (iff #40 #143)
+#141 := (iff #39 #140)
+#142 := [rewrite]: #141
+#145 := [quant-intro #142]: #144
+#162 := [trans #145 #160]: #161
+#138 := [asserted]: #40
+#163 := [mp #138 #162]: #158
+#181 := [mp~ #163 #172]: #158
+#675 := [mp #181 #674]: #670
+#353 := (not #670)
+#605 := (or #353 #91 #602)
+#630 := (>= #73 0::Int)
+#603 := (or #630 #602)
+#606 := (or #353 #603)
+#593 := (iff #606 #605)
+#607 := (or #353 #604)
+#439 := (iff #607 #605)
+#592 := [rewrite]: #439
+#436 := (iff #606 #607)
+#598 := (iff #603 #604)
+#628 := (iff #630 #91)
+#338 := [rewrite]: #628
+#599 := [monotonicity #338]: #598
+#438 := [monotonicity #599]: #436
+#595 := [trans #438 #592]: #593
+#600 := [quant-inst #73]: #606
+#596 := [mp #600 #595]: #605
+#488 := [unit-resolution #596 #675]: #604
+#498 := [unit-resolution #488 #487]: #602
+#478 := (not #602)
+#499 := (or #478 #594)
+#454 := [th-lemma arith triangle-eq]: #499
+#455 := [unit-resolution #454 #498]: #594
+#539 := (not #594)
+#466 := (or #539 #521)
+#66 := (f5 f6 #63)
+#69 := (f3 f4 #66)
+#647 := (* -1::Int #69)
+#290 := (+ #62 #647)
+#631 := (+ #10 #290)
+#640 := (>= #631 0::Int)
+#646 := (= #631 0::Int)
+#654 := (>= #63 0::Int)
+#573 := (+ #12 #100)
+#574 := (<= #573 0::Int)
+#558 := (not #574)
+#349 := (<= #69 0::Int)
+#643 := (= #69 0::Int)
+#649 := (not #654)
+#527 := [hypothesis]: #649
+#629 := (or #654 #643)
+#354 := (or #353 #654 #643)
+#355 := (or #353 #629)
+#625 := (iff #355 #354)
+#626 := [rewrite]: #625
+#249 := [quant-inst #63]: #355
+#348 := [mp #249 #626]: #354
+#514 := [unit-resolution #348 #675]: #629
+#517 := [unit-resolution #514 #527]: #643
+#518 := (not #643)
+#519 := (or #518 #349)
+#515 := [th-lemma arith triangle-eq]: #519
+#520 := [unit-resolution #515 #517]: #349
+#479 := (>= #10 0::Int)
+#560 := (= #10 0::Int)
+#332 := (f5 f6 #10)
+#480 := (f3 f4 #332)
+#481 := (= #480 0::Int)
+#554 := (not #479)
+#541 := [hypothesis]: #554
+#440 := (or #479 #481)
+#585 := (or #353 #479 #481)
+#586 := (or #353 #440)
+#474 := (iff #586 #585)
+#489 := [rewrite]: #474
+#589 := [quant-inst #10]: #586
+#491 := [mp #589 #489]: #585
+#543 := [unit-resolution #491 #675]: #440
+#544 := [unit-resolution #543 #541]: #481
+#548 := (= #10 #480)
+#546 := (= f7 #332)
+#333 := (= #332 f7)
+#24 := (:var 0 S3)
+#25 := (f3 f4 #24)
+#656 := (pattern #25)
+#26 := (f5 f6 #25)
+#27 := (= #26 #24)
+#657 := (forall (vars (?v0 S3)) (:pat #656) #27)
+#28 := (forall (vars (?v0 S3)) #27)
+#660 := (iff #28 #657)
+#658 := (iff #27 #27)
+#659 := [refl]: #658
+#661 := [quant-intro #659]: #660
+#177 := (~ #28 #28)
+#175 := (~ #27 #27)
+#176 := [refl]: #175
+#178 := [nnf-pos #176]: #177
+#114 := [asserted]: #28
+#167 := [mp~ #114 #178]: #28
+#662 := [mp #167 #661]: #657
+#313 := (not #657)
+#648 := (or #313 #333)
+#650 := [quant-inst #9]: #648
+#545 := [unit-resolution #650 #662]: #333
+#547 := [symm #545]: #546
+#549 := [monotonicity #547]: #548
+#550 := [trans #549 #544]: #560
+#551 := (not #560)
+#552 := (or #551 #479)
+#542 := [th-lemma arith triangle-eq]: #552
+#553 := [unit-resolution #542 #541 #550]: false
+#531 := [lemma #553]: #479
+#500 := (or #654 #91)
+#446 := [th-lemma arith farkas 1 1]: #500
+#501 := [unit-resolution #446 #527]: #91
+#621 := (or #243 #620)
+#34 := (= #33 #30)
+#129 := (or #126 #34)
+#664 := (forall (vars (?v0 Int)) (:pat #663) #129)
+#132 := (forall (vars (?v0 Int)) #129)
+#667 := (iff #132 #664)
+#665 := (iff #129 #129)
+#666 := [refl]: #665
+#668 := [quant-intro #666]: #667
+#169 := (~ #132 #132)
+#168 := (~ #129 #129)
+#165 := [refl]: #168
+#170 := [nnf-pos #165]: #169
+#31 := (<= 0::Int #30)
+#35 := (implies #31 #34)
+#36 := (forall (vars (?v0 Int)) #35)
+#135 := (iff #36 #132)
+#116 := (not #31)
+#117 := (or #116 #34)
+#120 := (forall (vars (?v0 Int)) #117)
+#133 := (iff #120 #132)
+#130 := (iff #117 #129)
+#127 := (iff #116 #126)
+#123 := (iff #31 #124)
+#125 := [rewrite]: #123
+#128 := [monotonicity #125]: #127
+#131 := [monotonicity #128]: #130
+#134 := [quant-intro #131]: #133
+#121 := (iff #36 #120)
+#118 := (iff #35 #117)
+#119 := [rewrite]: #118
+#122 := [quant-intro #119]: #121
+#136 := [trans #122 #134]: #135
+#115 := [asserted]: #36
+#137 := [mp #115 #136]: #132
+#166 := [mp~ #137 #170]: #132
+#669 := [mp #166 #668]: #664
+#633 := (not #664)
+#611 := (or #633 #243 #620)
+#627 := (= #79 #73)
+#352 := (not #630)
+#624 := (or #352 #627)
+#612 := (or #633 #624)
+#616 := (iff #612 #611)
+#608 := (or #633 #621)
+#615 := (iff #608 #611)
+#610 := [rewrite]: #615
+#609 := (iff #612 #608)
+#618 := (iff #624 #621)
+#335 := (iff #627 #620)
+#617 := [rewrite]: #335
+#339 := (iff #352 #243)
+#340 := [monotonicity #338]: #339
+#622 := [monotonicity #340 #617]: #618
+#614 := [monotonicity #622]: #609
+#457 := [trans #614 #610]: #616
+#613 := [quant-inst #73]: #612
+#458 := [mp #613 #457]: #611
+#482 := [unit-resolution #458 #669]: #621
+#506 := [unit-resolution #482 #501]: #620
+#507 := (not #620)
+#502 := (or #507 #459)
+#508 := [th-lemma arith triangle-eq]: #502
+#476 := [unit-resolution #508 #506]: #459
+#557 := (not #459)
+#555 := (not #349)
+#559 := (or #554 #555 #557 #558)
+#565 := [hypothesis]: #574
+#566 := [hypothesis]: #479
+#567 := [hypothesis]: #459
+#101 := (+ #79 #100)
+#102 := (+ #69 #101)
+#103 := (<= #102 0::Int)
+#108 := (not #103)
+#20 := (<= #10 #12)
+#21 := (if #20 #12 #10)
+#16 := (- #12 #10)
+#17 := (f5 f6 #16)
+#18 := (f3 f4 #17)
+#13 := (- #10 #12)
+#14 := (f5 f6 #13)
+#15 := (f3 f4 #14)
+#19 := (+ #15 #18)
+#22 := (<= #19 #21)
+#23 := (not #22)
+#111 := (iff #23 #108)
+#82 := (+ #69 #79)
+#85 := (<= #82 #21)
+#88 := (not #85)
+#109 := (iff #88 #108)
+#106 := (iff #85 #103)
+#97 := (<= #82 #94)
+#104 := (iff #97 #103)
+#105 := [rewrite]: #104
+#98 := (iff #85 #97)
+#95 := (= #21 #94)
+#92 := (iff #20 #91)
+#93 := [rewrite]: #92
+#96 := [monotonicity #93]: #95
+#99 := [monotonicity #96]: #98
+#107 := [trans #99 #105]: #106
+#110 := [monotonicity #107]: #109
+#89 := (iff #23 #88)
+#86 := (iff #22 #85)
+#83 := (= #19 #82)
+#80 := (= #18 #79)
+#77 := (= #17 #76)
+#74 := (= #16 #73)
+#75 := [rewrite]: #74
+#78 := [monotonicity #75]: #77
+#81 := [monotonicity #78]: #80
+#70 := (= #15 #69)
+#67 := (= #14 #66)
+#64 := (= #13 #63)
+#65 := [rewrite]: #64
+#68 := [monotonicity #65]: #67
+#71 := [monotonicity #68]: #70
+#84 := [monotonicity #71 #81]: #83
+#87 := [monotonicity #84]: #86
+#90 := [monotonicity #87]: #89
+#112 := [trans #90 #110]: #111
+#60 := [asserted]: #23
+#113 := [mp #60 #112]: #108
+#563 := [hypothesis]: #349
+#568 := [th-lemma arith farkas 1 -1 1 -1 1 #563 #113 #567 #566 #565]: false
+#556 := [lemma #568]: #559
+#483 := [unit-resolution #556 #476 #531 #520]: #558
+#242 := (= #12 #94)
+#328 := (or #243 #242)
+#329 := [def-axiom]: #328
+#442 := [unit-resolution #329 #501]: #242
+#473 := (not #242)
+#475 := (or #473 #574)
+#477 := [th-lemma arith triangle-eq]: #475
+#484 := [unit-resolution #477 #442 #483]: false
+#486 := [lemma #484]: #654
+#295 := (or #649 #646)
+#634 := (or #633 #649 #646)
+#305 := (= #69 #63)
+#310 := (or #649 #305)
+#635 := (or #633 #310)
+#641 := (iff #635 #634)
+#637 := (or #633 #295)
+#276 := (iff #637 #634)
+#639 := [rewrite]: #276
+#632 := (iff #635 #637)
+#296 := (iff #310 #295)
+#306 := (iff #305 #646)
+#294 := [rewrite]: #306
+#297 := [monotonicity #294]: #296
+#638 := [monotonicity #297]: #632
+#281 := [trans #638 #639]: #641
+#636 := [quant-inst #63]: #635
+#282 := [mp #636 #281]: #634
+#460 := [unit-resolution #282 #669]: #295
+#461 := [unit-resolution #460 #486]: #646
+#462 := (not #646)
+#463 := (or #462 #640)
+#464 := [th-lemma arith triangle-eq]: #463
+#465 := [unit-resolution #464 #461]: #640
+#588 := (>= #12 0::Int)
+#526 := (= #12 0::Int)
+#330 := (f5 f6 #12)
+#490 := (f3 f4 #330)
+#492 := (= #490 0::Int)
+#533 := (not #588)
+#528 := [hypothesis]: #533
+#485 := (or #588 #492)
+#495 := (or #353 #588 #492)
+#496 := (or #353 #485)
+#590 := (iff #496 #495)
+#587 := [rewrite]: #590
+#497 := [quant-inst #12]: #496
+#591 := [mp #497 #587]: #495
+#529 := [unit-resolution #591 #675]: #485
+#524 := [unit-resolution #529 #528]: #492
+#505 := (= #12 #490)
+#503 := (= f8 #330)
+#334 := (= #330 f8)
+#644 := (or #313 #334)
+#318 := [quant-inst #11]: #644
+#530 := [unit-resolution #318 #662]: #334
+#504 := [symm #530]: #503
+#398 := [monotonicity #504]: #505
+#509 := [trans #398 #524]: #526
+#510 := (not #526)
+#511 := (or #510 #588)
+#516 := [th-lemma arith triangle-eq]: #511
+#512 := [unit-resolution #516 #528 #509]: false
+#513 := [lemma #512]: #588
+#525 := (not #640)
+#522 := (or #533 #539 #525 #521)
+#534 := [hypothesis]: #540
+#535 := [hypothesis]: #588
+#536 := [hypothesis]: #640
+#537 := [hypothesis]: #594
+#538 := [th-lemma arith farkas -1 1 -1 -1 1 #113 #537 #536 #535 #534]: false
+#523 := [lemma #538]: #522
+#467 := [unit-resolution #523 #513 #465]: #466
+#468 := [unit-resolution #467 #455]: #521
+#327 := (= #10 #94)
+#320 := (or #91 #327)
+#331 := [def-axiom]: #320
+#469 := [unit-resolution #331 #487]: #327
+#470 := (not #327)
+#471 := (or #470 #540)
+#456 := [th-lemma arith triangle-eq]: #471
+#472 := [unit-resolution #456 #469 #468]: false
+#433 := [lemma #472]: #91
+#434 := [unit-resolution #482 #433]: #620
+#441 := [unit-resolution #508 #434]: #459
+#443 := [unit-resolution #329 #433]: #242
+#444 := [unit-resolution #477 #443]: #574
+#445 := (or #349 #525 #243)
+#447 := [th-lemma arith assign-bounds 1 -1]: #445
+#448 := [unit-resolution #447 #465 #433]: #349
+#449 := (or #555 #557 #558)
+#450 := [unit-resolution #556 #531]: #449
+[unit-resolution #450 #448 #444 #441]: false
+unsat
+a792a04eb456fe8e05c404760a48764de177c4d7 109 0
+#2 := false
+#28 := 0::Int
+decl f3 :: (-> S2 S3 Int)
+decl f5 :: S3
+#8 := f5
+decl f4 :: S2
+#7 := f4
+#9 := (f3 f4 f5)
+decl f7 :: S3
+#13 := f7
+#14 := (f3 f4 f7)
+#67 := -1::Int
+#74 := (* -1::Int #14)
+#86 := (+ #9 #74)
+#87 := (<= #86 0::Int)
+#90 := (if #87 #14 #9)
+#96 := (* -1::Int #90)
+decl f6 :: S3
+#10 := f6
+#11 := (f3 f4 f6)
+#97 := (+ #11 #96)
+#98 := (<= #97 0::Int)
+#99 := (not #98)
+#75 := (+ #11 #74)
+#76 := (<= #75 0::Int)
+#77 := (not #76)
+#70 := (* -1::Int #11)
+#71 := (+ #9 #70)
+#69 := (>= #71 0::Int)
+#68 := (not #69)
+#80 := (and #68 #77)
+#83 := (not #80)
+#104 := (or #83 #99)
+#107 := (not #104)
+#17 := (<= #9 #14)
+#18 := (if #17 #14 #9)
+#19 := (< #18 #11)
+#15 := (< #14 #11)
+#12 := (< #9 #11)
+#16 := (and #12 #15)
+#20 := (implies #16 #19)
+#21 := (not #20)
+#110 := (iff #21 #107)
+#60 := (not #16)
+#61 := (or #60 #19)
+#64 := (not #61)
+#108 := (iff #64 #107)
+#105 := (iff #61 #104)
+#102 := (iff #19 #99)
+#93 := (< #90 #11)
+#100 := (iff #93 #99)
+#101 := [rewrite]: #100
+#94 := (iff #19 #93)
+#91 := (= #18 #90)
+#88 := (iff #17 #87)
+#89 := [rewrite]: #88
+#92 := [monotonicity #89]: #91
+#95 := [monotonicity #92]: #94
+#103 := [trans #95 #101]: #102
+#84 := (iff #60 #83)
+#81 := (iff #16 #80)
+#78 := (iff #15 #77)
+#79 := [rewrite]: #78
+#72 := (iff #12 #68)
+#73 := [rewrite]: #72
+#82 := [monotonicity #73 #79]: #81
+#85 := [monotonicity #82]: #84
+#106 := [monotonicity #85 #103]: #105
+#109 := [monotonicity #106]: #108
+#65 := (iff #21 #64)
+#62 := (iff #20 #61)
+#63 := [rewrite]: #62
+#66 := [monotonicity #63]: #65
+#111 := [trans #66 #109]: #110
+#59 := [asserted]: #21
+#112 := [mp #59 #111]: #107
+#116 := [not-or-elim #112]: #98
+#113 := [not-or-elim #112]: #80
+#114 := [and-elim #113]: #68
+#644 := (+ #9 #96)
+#627 := (>= #644 0::Int)
+#330 := (= #9 #90)
+#246 := (not #87)
+#245 := (= #14 #90)
+#628 := (not #245)
+#642 := (+ #14 #96)
+#633 := (>= #642 0::Int)
+#357 := (not #633)
+#115 := [and-elim #113]: #77
+#355 := [hypothesis]: #633
+#356 := [th-lemma arith farkas -1 -1 1 #355 #115 #116]: false
+#358 := [lemma #356]: #357
+#252 := [hypothesis]: #245
+#629 := (or #628 #633)
+#351 := [th-lemma arith triangle-eq]: #629
+#352 := [unit-resolution #351 #252 #358]: false
+#626 := [lemma #352]: #628
+#331 := (or #246 #245)
+#332 := [def-axiom]: #331
+#631 := [unit-resolution #332 #626]: #246
+#323 := (or #87 #330)
+#334 := [def-axiom]: #323
+#341 := [unit-resolution #334 #631]: #330
+#342 := (not #330)
+#343 := (or #342 #627)
+#344 := [th-lemma arith triangle-eq]: #343
+#622 := [unit-resolution #344 #341]: #627
+[th-lemma arith farkas -1 1 1 #622 #114 #116]: false
+unsat
+06ea32eecccdf6605c3b038ea8337a1d74e482b8 137 0
+#2 := false
+decl f5 :: S3
+#8 := f5
+decl f6 :: (-> S4 Int S3)
+#10 := 0::Int
+decl f7 :: S4
+#12 := f7
+#13 := (f6 f7 0::Int)
+decl f3 :: (-> S2 S3 Int)
+decl f4 :: S2
+#7 := f4
+#9 := (f3 f4 f5)
+#11 := (<= #9 0::Int)
+#14 := (if #11 #13 f5)
+#266 := (= f5 #14)
+#181 := (= #13 #14)
+#568 := (not #266)
+#15 := (= #14 f5)
+#16 := (not #15)
+#278 := (iff #16 #568)
+#567 := (iff #15 #266)
+#564 := [commutativity]: #567
+#279 := [monotonicity #564]: #278
+#52 := [asserted]: #16
+#280 := [mp #52 #279]: #568
+#259 := (or #11 #266)
+#270 := [def-axiom]: #259
+#281 := [unit-resolution #270 #280]: #11
+#182 := (not #11)
+#267 := (or #182 #181)
+#268 := [def-axiom]: #267
+#548 := [unit-resolution #268 #281]: #181
+#399 := (= f5 #13)
+#272 := (f6 f7 #9)
+#397 := (= #272 #13)
+#274 := (= #9 0::Int)
+#252 := (f3 f4 #272)
+#377 := (= #252 0::Int)
+#273 := (>= #9 0::Int)
+#289 := (not #377)
+#563 := [hypothesis]: #289
+#584 := (or #273 #377)
+#22 := (:var 0 Int)
+#24 := (f6 f7 #22)
+#603 := (pattern #24)
+#25 := (f3 f4 #24)
+#30 := (= #25 0::Int)
+#64 := (>= #22 0::Int)
+#94 := (or #64 #30)
+#610 := (forall (vars (?v0 Int)) (:pat #603) #94)
+#97 := (forall (vars (?v0 Int)) #94)
+#613 := (iff #97 #610)
+#611 := (iff #94 #94)
+#612 := [refl]: #611
+#614 := [quant-intro #612]: #613
+#110 := (~ #97 #97)
+#118 := (~ #94 #94)
+#119 := [refl]: #118
+#111 := [nnf-pos #119]: #110
+#29 := (< #22 0::Int)
+#31 := (implies #29 #30)
+#32 := (forall (vars (?v0 Int)) #31)
+#100 := (iff #32 #97)
+#78 := (not #29)
+#79 := (or #78 #30)
+#82 := (forall (vars (?v0 Int)) #79)
+#98 := (iff #82 #97)
+#95 := (iff #79 #94)
+#92 := (iff #78 #64)
+#65 := (not #64)
+#87 := (not #65)
+#90 := (iff #87 #64)
+#91 := [rewrite]: #90
+#88 := (iff #78 #87)
+#85 := (iff #29 #65)
+#86 := [rewrite]: #85
+#89 := [monotonicity #86]: #88
+#93 := [trans #89 #91]: #92
+#96 := [monotonicity #93]: #95
+#99 := [quant-intro #96]: #98
+#83 := (iff #32 #82)
+#80 := (iff #31 #79)
+#81 := [rewrite]: #80
+#84 := [quant-intro #81]: #83
+#101 := [trans #84 #99]: #100
+#77 := [asserted]: #32
+#102 := [mp #77 #101]: #97
+#120 := [mp~ #102 #111]: #97
+#615 := [mp #120 #614]: #610
+#591 := (not #610)
+#592 := (or #591 #273 #377)
+#593 := (or #591 #584)
+#589 := (iff #593 #592)
+#595 := [rewrite]: #589
+#594 := [quant-inst #9]: #593
+#585 := [mp #594 #595]: #592
+#559 := [unit-resolution #585 #615]: #584
+#560 := [unit-resolution #559 #563]: #273
+#557 := [th-lemma arith eq-propagate 0 0 #560 #281]: #274
+#558 := (= #252 #9)
+#269 := (= #272 f5)
+#17 := (:var 0 S3)
+#18 := (f3 f4 #17)
+#596 := (pattern #18)
+#19 := (f6 f7 #18)
+#20 := (= #19 #17)
+#597 := (forall (vars (?v0 S3)) (:pat #596) #20)
+#21 := (forall (vars (?v0 S3)) #20)
+#600 := (iff #21 #597)
+#598 := (iff #20 #20)
+#599 := [refl]: #598
+#601 := [quant-intro #599]: #600
+#116 := (~ #21 #21)
+#114 := (~ #20 #20)
+#115 := [refl]: #114
+#117 := [nnf-pos #115]: #116
+#53 := [asserted]: #21
+#106 := [mp~ #53 #117]: #21
+#602 := [mp #106 #601]: #597
+#588 := (not #597)
+#590 := (or #588 #269)
+#246 := [quant-inst #8]: #590
+#561 := [unit-resolution #246 #602]: #269
+#562 := [monotonicity #561]: #558
+#551 := [trans #562 #557]: #377
+#552 := [unit-resolution #563 #551]: false
+#553 := [lemma #552]: #377
+#555 := (= #9 #252)
+#549 := (= f5 #272)
+#554 := [symm #561]: #549
+#550 := [monotonicity #554]: #555
+#556 := [trans #550 #553]: #274
+#398 := [monotonicity #556]: #397
+#541 := [trans #554 #398]: #399
+#542 := [trans #541 #548]: #266
+[unit-resolution #280 #542]: false
+unsat
--- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Dec 20 15:51:27 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Dec 21 13:33:54 2012 +0100
@@ -346,6 +346,14 @@
(* unfolding of definitions and theory-specific rewritings *)
+fun expand_head_conv cv ct =
+ (case Thm.term_of ct of
+ _ $ _ =>
+ Conv.fun_conv (expand_head_conv cv) then_conv
+ Conv.try_conv (Thm.beta_conversion false)
+ | _ => cv) ct
+
+
(** rewrite bool case expressions as if expressions **)
local
@@ -355,7 +363,9 @@
val thm = mk_meta_eq @{lemma
"bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
- fun unfold_conv _ = SMT_Utils.if_true_conv is_bool_case (Conv.rewr_conv thm)
+ fun unfold_conv _ =
+ SMT_Utils.if_true_conv (is_bool_case o Term.head_of)
+ (expand_head_conv (Conv.rewr_conv thm))
in
fun rewrite_bool_case_conv ctxt =
@@ -393,8 +403,8 @@
| abs_min_max _ _ = NONE
fun unfold_amm_conv ctxt ct =
- (case abs_min_max ctxt (Thm.term_of ct) of
- SOME thm => Conv.rewr_conv thm
+ (case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of
+ SOME thm => expand_head_conv (Conv.rewr_conv thm)
| NONE => Conv.all_conv) ct
in
@@ -460,8 +470,11 @@
"int (n * m) = int n * int m"
"int (n div m) = int n div int m"
"int (n mod m) = int n mod int m"
+ by (auto simp add: int_mult zdiv_int zmod_int)}
+
+ val int_if = mk_meta_eq @{lemma
"int (if P then n else m) = (if P then int n else int m)"
- by (auto simp add: int_mult zdiv_int zmod_int)}
+ by simp}
fun mk_number_eq ctxt i lhs =
let
@@ -471,12 +484,8 @@
fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1
in Goal.norm_result (Goal.prove_internal [] eq tac) end
- fun expand_head_conv cv ct =
- (case Thm.term_of ct of
- _ $ _ =>
- Conv.fun_conv (expand_head_conv cv) then_conv
- Thm.beta_conversion false
- | _ => cv) ct
+ fun ite_conv cv1 cv2 =
+ Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
fun int_conv ctxt ct =
(case Thm.term_of ct of
@@ -484,7 +493,9 @@
Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
| @{const of_nat (int)} $ _ =>
(Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
- Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt
+ (Conv.rewr_conv int_if then_conv
+ ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv
+ Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt
| _ => Conv.no_conv) ct
and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt