| author | boehmes |
| Mon, 03 Jan 2011 16:49:28 +0100 | |
| changeset 41427 | 5fbad0390649 |
| parent 41426 | 09615ed31f04 |
| child 41428 | 44511bf5dcc6 |
| src/HOL/SMT_Examples/SMT_Tests.certs | file | annotate | diff | comparison | revisions | |
| src/HOL/SMT_Examples/SMT_Tests.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/SMT_Examples/SMT_Tests.certs Mon Jan 03 16:22:08 2011 +0100 +++ b/src/HOL/SMT_Examples/SMT_Tests.certs Mon Jan 03 16:49:28 2011 +0100 @@ -50919,6 +50919,4834 @@ #207 := [unit-resolution #173 #546]: #242 [unit-resolution #207 #552]: false unsat +49afcc0d7e8a703cc498df193e407add0e832e10 72 0 +#2 := false +decl f4 :: (-> S4 S5 S5) +decl f9 :: S5 +#22 := f9 +decl f16 :: S4 +#59 := f16 +#60 := (f4 f16 f9) +#270 := (f4 f16 #60) +#343 := (= f9 #270) +#320 := (= #60 #270) +#336 := (= #270 #60) +#61 := (= #60 f9) +#146 := (= f9 #60) +#62 := (not #61) +#63 := (not #62) +#158 := (iff #63 #146) +#150 := (not #146) +#153 := (not #150) +#156 := (iff #153 #146) +#157 := [rewrite]: #156 +#154 := (iff #63 #153) +#151 := (iff #62 #150) +#148 := (iff #61 #146) +#149 := [rewrite]: #148 +#152 := [monotonicity #149]: #151 +#155 := [monotonicity #152]: #154 +#159 := [trans #155 #157]: #158 +#145 := [asserted]: #63 +#162 := [mp #145 #159]: #146 +#678 := [symm #162]: #61 +#679 := [monotonicity #678]: #336 +#663 := [symm #679]: #320 +#324 := [trans #162 #663]: #343 +#337 := (not #343) +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#717 := (pattern #12) +#38 := (= #12 f9) +#39 := (not #38) +#718 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #717) #39) +#40 := (forall (vars (?v0 S4) (?v1 S5)) #39) +#721 := (iff #40 #718) +#719 := (iff #39 #39) +#720 := [refl]: #719 +#722 := [quant-intro #720]: #721 +#165 := (~ #40 #40) +#167 := (~ #39 #39) +#164 := [refl]: #167 +#161 := [nnf-pos #164]: #165 +#100 := [asserted]: #40 +#163 := [mp~ #100 #161]: #40 +#723 := [mp #163 #722]: #718 +#348 := (not #718) +#349 := (or #348 #337) +#362 := (= #270 f9) +#290 := (not #362) +#683 := (or #348 #290) +#685 := (iff #683 #349) +#681 := (iff #349 #349) +#687 := [rewrite]: #681 +#469 := (iff #290 #337) +#680 := (iff #362 #343) +#682 := [rewrite]: #680 +#676 := [monotonicity #682]: #469 +#686 := [monotonicity #676]: #685 +#677 := [trans #686 #687]: #685 +#684 := [quant-inst #59 #60]: #683 +#335 := [mp #684 #677]: #349 +#340 := [unit-resolution #335 #723]: #337 +[unit-resolution #340 #324]: false +unsat +04befb37cbbc5695f38171536eac721870f8c5ee 59 0 +#2 := false +decl f4 :: (-> S4 S5 S5) +decl f9 :: S5 +#22 := f9 +decl f17 :: S4 +#60 := f17 +#61 := (f4 f17 f9) +decl f16 :: S4 +#59 := f16 +#62 := (f4 f16 #61) +#148 := (= f9 #62) +#63 := (= #62 f9) +#64 := (not #63) +#65 := (not #64) +#160 := (iff #65 #148) +#152 := (not #148) +#155 := (not #152) +#158 := (iff #155 #148) +#159 := [rewrite]: #158 +#156 := (iff #65 #155) +#153 := (iff #64 #152) +#150 := (iff #63 #148) +#151 := [rewrite]: #150 +#154 := [monotonicity #151]: #153 +#157 := [monotonicity #154]: #156 +#161 := [trans #157 #159]: #160 +#147 := [asserted]: #65 +#164 := [mp #147 #161]: #148 +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#719 := (pattern #12) +#38 := (= #12 f9) +#39 := (not #38) +#720 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #719) #39) +#40 := (forall (vars (?v0 S4) (?v1 S5)) #39) +#723 := (iff #40 #720) +#721 := (iff #39 #39) +#722 := [refl]: #721 +#724 := [quant-intro #722]: #723 +#167 := (~ #40 #40) +#169 := (~ #39 #39) +#166 := [refl]: #169 +#163 := [nnf-pos #166]: #167 +#102 := [asserted]: #40 +#165 := [mp~ #102 #163]: #40 +#725 := [mp #165 #724]: #720 +#351 := (not #720) +#635 := (or #351 #152) +#636 := (or #351 #64) +#633 := (iff #636 #635) +#640 := (iff #635 #635) +#634 := [rewrite]: #640 +#639 := [monotonicity #154]: #633 +#641 := [trans #639 #634]: #633 +#632 := [quant-inst #59 #61]: #636 +#470 := [mp #632 #641]: #635 +[unit-resolution #470 #725 #164]: false +unsat +b0341ff23e5abb796f1191ac954b55a496b57644 136 0 +#2 := false +decl f4 :: (-> S4 S5 S5) +decl f9 :: S5 +#22 := f9 +decl f17 :: S4 +#60 := f17 +#64 := (f4 f17 f9) +decl f16 :: S4 +#59 := f16 +#63 := (f4 f16 f9) +#65 := (= #63 #64) +#61 := (= f16 f17) +#386 := (iff #61 #65) +#373 := (not #386) +#66 := (not #65) +#151 := (or #61 #66) +#155 := (not #151) +#62 := (not #61) +#67 := (implies #62 #66) +#68 := (not #67) +#156 := (iff #68 #155) +#153 := (iff #67 #151) +#154 := [rewrite]: #153 +#157 := [monotonicity #154]: #156 +#150 := [asserted]: #68 +#160 := [mp #150 #157]: #155 +#159 := [not-or-elim #160]: #65 +#158 := [not-or-elim #160]: #62 +#651 := (or #373 #61 #66) +#652 := [def-axiom]: #651 +#621 := [unit-resolution #652 #158 #159]: #373 +#45 := (:var 2 S5) +#44 := (:var 3 S4) +#46 := (f4 #44 #45) +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#724 := (pattern #12 #46) +#122 := (= #11 #45) +#201 := (not #122) +#119 := (= #10 #44) +#200 := (not #119) +#202 := (or #200 #201) +#203 := (not #202) +#115 := (= #12 #46) +#206 := (iff #115 #203) +#725 := (forall (vars (?v0 S4) (?v1 S5) (?v2 S4) (?v3 S5)) (:pat #724) #206) +#209 := (forall (vars (?v0 S4) (?v1 S5) (?v2 S4) (?v3 S5)) #206) +#728 := (iff #209 #725) +#726 := (iff #206 #206) +#727 := [refl]: #726 +#729 := [quant-intro #727]: #728 +#125 := (and #119 #122) +#128 := (iff #115 #125) +#131 := (forall (vars (?v0 S4) (?v1 S5) (?v2 S4) (?v3 S5)) #128) +#210 := (iff #131 #209) +#207 := (iff #128 #206) +#204 := (iff #125 #203) +#205 := [rewrite]: #204 +#208 := [monotonicity #205]: #207 +#211 := [quant-intro #208]: #210 +#187 := (~ #131 #131) +#162 := (~ #128 #128) +#163 := [refl]: #162 +#188 := [nnf-pos #163]: #187 +#49 := (= #45 #11) +#48 := (= #44 #10) +#50 := (and #48 #49) +#47 := (= #46 #12) +#51 := (iff #47 #50) +#52 := (forall (vars (?v0 S4) (?v1 S5) (?v2 S4) (?v3 S5)) #51) +#132 := (iff #52 #131) +#129 := (iff #51 #128) +#126 := (iff #50 #125) +#123 := (iff #49 #122) +#124 := [rewrite]: #123 +#120 := (iff #48 #119) +#121 := [rewrite]: #120 +#127 := [monotonicity #121 #124]: #126 +#117 := (iff #47 #115) +#118 := [rewrite]: #117 +#130 := [monotonicity #118 #127]: #129 +#133 := [quant-intro #130]: #132 +#114 := [asserted]: #52 +#136 := [mp #114 #133]: #131 +#189 := [mp~ #136 #188]: #131 +#212 := [mp #189 #211]: #209 +#730 := [mp #212 #729]: #725 +#658 := (not #725) +#380 := (or #658 #386) +#335 := (= f9 f9) +#340 := (not #335) +#678 := (or #62 #340) +#336 := (not #678) +#679 := (iff #65 #336) +#381 := (or #658 #679) +#659 := (iff #381 #380) +#660 := (iff #380 #380) +#369 := [rewrite]: #660 +#278 := (iff #679 #386) +#368 := (iff #65 #61) +#372 := (iff #368 #386) +#387 := [rewrite]: #372 +#384 := (iff #679 #368) +#661 := (iff #336 #61) +#311 := (not #62) +#672 := (iff #311 #61) +#675 := [rewrite]: #672 +#312 := (iff #336 #311) +#671 := (iff #678 #62) +#668 := (or #62 false) +#670 := (iff #668 #62) +#306 := [rewrite]: #670 +#669 := (iff #678 #668) +#666 := (iff #340 false) +#1 := true +#324 := (not true) +#327 := (iff #324 false) +#665 := [rewrite]: #327 +#325 := (iff #340 #324) +#320 := (iff #335 true) +#663 := [rewrite]: #320 +#326 := [monotonicity #663]: #325 +#667 := [trans #326 #665]: #666 +#664 := [monotonicity #667]: #669 +#673 := [trans #664 #306]: #671 +#674 := [monotonicity #673]: #312 +#662 := [trans #674 #675]: #661 +#385 := [monotonicity #662]: #384 +#657 := [trans #385 #387]: #278 +#656 := [monotonicity #657]: #659 +#370 := [trans #656 #369]: #659 +#655 := [quant-inst #60 #22 #59 #22]: #381 +#371 := [mp #655 #370]: #380 +[unit-resolution #371 #730 #621]: false +unsat +fff2cbf089f9102929d14127f6531c5541969006 50 0 +#2 := false +decl f15 :: (-> S5 S4) +decl f4 :: (-> S4 S5 S5) +decl f17 :: S5 +#60 := f17 +decl f16 :: S4 +#59 := f16 +#61 := (f4 f16 f17) +#62 := (f15 #61) +#147 := (= f16 #62) +#151 := (not #147) +#63 := (= #62 f16) +#64 := (not #63) +#152 := (iff #64 #151) +#149 := (iff #63 #147) +#150 := [rewrite]: #149 +#153 := [monotonicity #150]: #152 +#146 := [asserted]: #64 +#156 := [mp #146 #153]: #151 +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#711 := (pattern #12) +#56 := (f15 #12) +#139 := (= #10 #56) +#731 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #711) #139) +#143 := (forall (vars (?v0 S4) (?v1 S5)) #139) +#734 := (iff #143 #731) +#732 := (iff #139 #139) +#733 := [refl]: #732 +#735 := [quant-intro #733]: #734 +#191 := (~ #143 #143) +#189 := (~ #139 #139) +#190 := [refl]: #189 +#192 := [nnf-pos #190]: #191 +#57 := (= #56 #10) +#58 := (forall (vars (?v0 S4) (?v1 S5)) #57) +#144 := (iff #58 #143) +#141 := (iff #57 #139) +#142 := [rewrite]: #141 +#145 := [quant-intro #142]: #144 +#138 := [asserted]: #58 +#148 := [mp #138 #145]: #143 +#193 := [mp~ #148 #192]: #143 +#736 := [mp #193 #735]: #731 +#265 := (not #731) +#352 := (or #265 #147) +#266 := [quant-inst #59 #60]: #352 +[unit-resolution #266 #736 #156]: false +unsat +affee22ddd78a2e982940d231a35763dd8db5ff1 50 0 +#2 := false +decl f14 :: (-> S5 S5) +decl f4 :: (-> S4 S5 S5) +decl f17 :: S5 +#60 := f17 +decl f16 :: S4 +#59 := f16 +#61 := (f4 f16 f17) +#62 := (f14 #61) +#147 := (= f17 #62) +#151 := (not #147) +#63 := (= #62 f17) +#64 := (not #63) +#152 := (iff #64 #151) +#149 := (iff #63 #147) +#150 := [rewrite]: #149 +#153 := [monotonicity #150]: #152 +#146 := [asserted]: #64 +#156 := [mp #146 #153]: #151 +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#711 := (pattern #12) +#53 := (f14 #12) +#131 := (= #11 #53) +#725 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #711) #131) +#135 := (forall (vars (?v0 S4) (?v1 S5)) #131) +#728 := (iff #135 #725) +#726 := (iff #131 #131) +#727 := [refl]: #726 +#729 := [quant-intro #727]: #728 +#186 := (~ #135 #135) +#184 := (~ #131 #131) +#185 := [refl]: #184 +#187 := [nnf-pos #185]: #186 +#54 := (= #53 #11) +#55 := (forall (vars (?v0 S4) (?v1 S5)) #54) +#136 := (iff #55 #135) +#133 := (iff #54 #131) +#134 := [rewrite]: #133 +#137 := [quant-intro #134]: #136 +#130 := [asserted]: #55 +#140 := [mp #130 #137]: #135 +#188 := [mp~ #140 #187]: #135 +#730 := [mp #188 #729]: #725 +#355 := (not #725) +#356 := (or #355 #147) +#284 := [quant-inst #59 #60]: #356 +[unit-resolution #284 #730 #156]: false +unsat +9aafa835b8aaa001d18bcde9a4c11eddfa9c9649 56 0 +#2 := false +decl f15 :: (-> S5 S4) +decl f4 :: (-> S4 S5 S5) +decl f9 :: S5 +#22 := f9 +decl f18 :: S4 +#61 := f18 +#62 := (f4 f18 f9) +decl f17 :: S4 +#60 := f17 +#63 := (f4 f17 #62) +decl f16 :: S4 +#59 := f16 +#64 := (f4 f16 #63) +#65 := (f15 #64) +#150 := (= f16 #65) +#154 := (not #150) +#66 := (= #65 f16) +#67 := (not #66) +#155 := (iff #67 #154) +#152 := (iff #66 #150) +#153 := [rewrite]: #152 +#156 := [monotonicity #153]: #155 +#149 := [asserted]: #67 +#159 := [mp #149 #156]: #154 +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#714 := (pattern #12) +#56 := (f15 #12) +#142 := (= #10 #56) +#734 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #714) #142) +#146 := (forall (vars (?v0 S4) (?v1 S5)) #142) +#737 := (iff #146 #734) +#735 := (iff #142 #142) +#736 := [refl]: #735 +#738 := [quant-intro #736]: #737 +#194 := (~ #146 #146) +#192 := (~ #142 #142) +#193 := [refl]: #192 +#195 := [nnf-pos #193]: #194 +#57 := (= #56 #10) +#58 := (forall (vars (?v0 S4) (?v1 S5)) #57) +#147 := (iff #58 #146) +#144 := (iff #57 #142) +#145 := [rewrite]: #144 +#148 := [quant-intro #145]: #147 +#141 := [asserted]: #58 +#151 := [mp #141 #148]: #146 +#196 := [mp~ #151 #195]: #146 +#739 := [mp #196 #738]: #734 +#269 := (not #734) +#516 := (or #269 #150) +#517 := [quant-inst #59 #63]: #516 +[unit-resolution #517 #739 #159]: false +unsat +5f1277eca9b4949514eac16a5c81e154e20379e5 56 0 +#2 := false +decl f14 :: (-> S5 S5) +decl f4 :: (-> S4 S5 S5) +decl f9 :: S5 +#22 := f9 +decl f18 :: S4 +#61 := f18 +#62 := (f4 f18 f9) +decl f17 :: S4 +#60 := f17 +#63 := (f4 f17 #62) +decl f16 :: S4 +#59 := f16 +#64 := (f4 f16 #63) +#65 := (f14 #64) +#150 := (= #63 #65) +#154 := (not #150) +#66 := (= #65 #63) +#67 := (not #66) +#155 := (iff #67 #154) +#152 := (iff #66 #150) +#153 := [rewrite]: #152 +#156 := [monotonicity #153]: #155 +#149 := [asserted]: #67 +#159 := [mp #149 #156]: #154 +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#714 := (pattern #12) +#53 := (f14 #12) +#134 := (= #11 #53) +#728 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #714) #134) +#138 := (forall (vars (?v0 S4) (?v1 S5)) #134) +#731 := (iff #138 #728) +#729 := (iff #134 #134) +#730 := [refl]: #729 +#732 := [quant-intro #730]: #731 +#189 := (~ #138 #138) +#187 := (~ #134 #134) +#188 := [refl]: #187 +#190 := [nnf-pos #188]: #189 +#54 := (= #53 #11) +#55 := (forall (vars (?v0 S4) (?v1 S5)) #54) +#139 := (iff #55 #138) +#136 := (iff #54 #134) +#137 := [rewrite]: #136 +#140 := [quant-intro #137]: #139 +#133 := [asserted]: #55 +#143 := [mp #133 #140]: #138 +#191 := [mp~ #143 #190]: #138 +#733 := [mp #191 #732]: #728 +#287 := (not #728) +#528 := (or #287 #150) +#483 := [quant-inst #59 #63]: #528 +[unit-resolution #483 #733 #159]: false +unsat +3d958afb574f2b777d342f1a937e466d602feddd 95 0 +#2 := false +decl f15 :: (-> S5 S4) +decl f14 :: (-> S5 S5) +decl f4 :: (-> S4 S5 S5) +decl f9 :: S5 +#22 := f9 +decl f18 :: S4 +#61 := f18 +#62 := (f4 f18 f9) +decl f17 :: S4 +#60 := f17 +#63 := (f4 f17 #62) +decl f16 :: S4 +#59 := f16 +#64 := (f4 f16 #63) +#65 := (f14 #64) +#66 := (f15 #65) +#151 := (= f17 #66) +#617 := (f15 #63) +#435 := (= #617 #66) +#439 := (= #66 #617) +#434 := (= #65 #63) +#517 := (= #63 #65) +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#715 := (pattern #12) +#53 := (f14 #12) +#135 := (= #11 #53) +#729 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #715) #135) +#139 := (forall (vars (?v0 S4) (?v1 S5)) #135) +#732 := (iff #139 #729) +#730 := (iff #135 #135) +#731 := [refl]: #730 +#733 := [quant-intro #731]: #732 +#190 := (~ #139 #139) +#188 := (~ #135 #135) +#189 := [refl]: #188 +#191 := [nnf-pos #189]: #190 +#54 := (= #53 #11) +#55 := (forall (vars (?v0 S4) (?v1 S5)) #54) +#140 := (iff #55 #139) +#137 := (iff #54 #135) +#138 := [rewrite]: #137 +#141 := [quant-intro #138]: #140 +#134 := [asserted]: #55 +#144 := [mp #134 #141]: #139 +#192 := [mp~ #144 #191]: #139 +#734 := [mp #192 #733]: #729 +#288 := (not #729) +#484 := (or #288 #517) +#485 := [quant-inst #59 #63]: #484 +#433 := [unit-resolution #485 #734]: #517 +#438 := [symm #433]: #434 +#432 := [monotonicity #438]: #439 +#436 := [symm #432]: #435 +#621 := (= f17 #617) +#56 := (f15 #12) +#143 := (= #10 #56) +#735 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #715) #143) +#147 := (forall (vars (?v0 S4) (?v1 S5)) #143) +#738 := (iff #147 #735) +#736 := (iff #143 #143) +#737 := [refl]: #736 +#739 := [quant-intro #737]: #738 +#195 := (~ #147 #147) +#193 := (~ #143 #143) +#194 := [refl]: #193 +#196 := [nnf-pos #194]: #195 +#57 := (= #56 #10) +#58 := (forall (vars (?v0 S4) (?v1 S5)) #57) +#148 := (iff #58 #147) +#145 := (iff #57 #143) +#146 := [rewrite]: #145 +#149 := [quant-intro #146]: #148 +#142 := [asserted]: #58 +#152 := [mp #142 #149]: #147 +#197 := [mp~ #152 #196]: #147 +#740 := [mp #197 #739]: #735 +#270 := (not #735) +#602 := (or #270 #621) +#599 := [quant-inst #60 #62]: #602 +#431 := [unit-resolution #599 #740]: #621 +#422 := [trans #431 #436]: #151 +#155 := (not #151) +#67 := (= #66 f17) +#68 := (not #67) +#156 := (iff #68 #155) +#153 := (iff #67 #151) +#154 := [rewrite]: #153 +#157 := [monotonicity #154]: #156 +#150 := [asserted]: #68 +#160 := [mp #150 #157]: #155 +[unit-resolution #160 #422]: false +unsat +27c15c60b6aaec6351efe83812dce879a8ad44d1 71 0 +#2 := false +decl f14 :: (-> S5 S5) +decl f4 :: (-> S4 S5 S5) +decl f9 :: S5 +#22 := f9 +decl f18 :: S4 +#61 := f18 +#62 := (f4 f18 f9) +decl f17 :: S4 +#60 := f17 +#63 := (f4 f17 #62) +decl f16 :: S4 +#59 := f16 +#64 := (f4 f16 #63) +#65 := (f14 #64) +#66 := (f14 #65) +#151 := (= #62 #66) +#608 := (f14 #63) +#435 := (= #608 #66) +#439 := (= #66 #608) +#434 := (= #65 #63) +#517 := (= #63 #65) +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#715 := (pattern #12) +#53 := (f14 #12) +#135 := (= #11 #53) +#729 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #715) #135) +#139 := (forall (vars (?v0 S4) (?v1 S5)) #135) +#732 := (iff #139 #729) +#730 := (iff #135 #135) +#731 := [refl]: #730 +#733 := [quant-intro #731]: #732 +#190 := (~ #139 #139) +#188 := (~ #135 #135) +#189 := [refl]: #188 +#191 := [nnf-pos #189]: #190 +#54 := (= #53 #11) +#55 := (forall (vars (?v0 S4) (?v1 S5)) #54) +#140 := (iff #55 #139) +#137 := (iff #54 #135) +#138 := [rewrite]: #137 +#141 := [quant-intro #138]: #140 +#134 := [asserted]: #55 +#144 := [mp #134 #141]: #139 +#192 := [mp~ #144 #191]: #139 +#734 := [mp #192 #733]: #729 +#288 := (not #729) +#484 := (or #288 #517) +#485 := [quant-inst #59 #63]: #484 +#433 := [unit-resolution #485 #734]: #517 +#438 := [symm #433]: #434 +#432 := [monotonicity #438]: #439 +#436 := [symm #432]: #435 +#610 := (= #62 #608) +#612 := (or #288 #610) +#613 := [quant-inst #60 #62]: #612 +#431 := [unit-resolution #613 #734]: #610 +#422 := [trans #431 #436]: #151 +#155 := (not #151) +#67 := (= #66 #62) +#68 := (not #67) +#156 := (iff #68 #155) +#153 := (iff #67 #151) +#154 := [rewrite]: #153 +#157 := [monotonicity #154]: #156 +#150 := [asserted]: #68 +#160 := [mp #150 #157]: #155 +[unit-resolution #160 #422]: false +unsat +a98c8f96e82461af4b3fef055b4043eba1bf782f 97 0 +#2 := false +decl f17 :: (-> S4 S15) +decl f15 :: (-> S5 S4) +decl f4 :: (-> S4 S5 S5) +decl f9 :: S5 +#22 := f9 +decl f16 :: (-> S15 S16 S4) +decl f20 :: S16 +#75 := f20 +decl f19 :: S15 +#74 := f19 +#76 := (f16 f19 f20) +#77 := (f4 #76 f9) +#78 := (f15 #77) +#79 := (f17 #78) +#188 := (= f19 #79) +#374 := (f17 #76) +#361 := (= #374 #79) +#721 := (= #79 #374) +#717 := (= #78 #76) +#320 := (= #76 #78) +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#767 := (pattern #12) +#56 := (f15 #12) +#156 := (= #10 #56) +#787 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #767) #156) +#160 := (forall (vars (?v0 S4) (?v1 S5)) #156) +#790 := (iff #160 #787) +#788 := (iff #156 #156) +#789 := [refl]: #788 +#791 := [quant-intro #789]: #790 +#232 := (~ #160 #160) +#230 := (~ #156 #156) +#231 := [refl]: #230 +#233 := [nnf-pos #231]: #232 +#57 := (= #56 #10) +#58 := (forall (vars (?v0 S4) (?v1 S5)) #57) +#161 := (iff #58 #160) +#158 := (iff #57 #156) +#159 := [rewrite]: #158 +#162 := [quant-intro #159]: #161 +#155 := [asserted]: #58 +#165 := [mp #155 #162]: #160 +#234 := [mp~ #165 #233]: #160 +#792 := [mp #234 #791]: #787 +#408 := (not #787) +#322 := (or #408 #320) +#409 := [quant-inst #76 #22]: #322 +#716 := [unit-resolution #409 #792]: #320 +#720 := [symm #716]: #717 +#723 := [monotonicity #720]: #721 +#362 := [symm #723]: #361 +#375 := (= f19 #374) +#66 := (:var 0 S16) +#65 := (:var 1 S15) +#67 := (f16 #65 #66) +#801 := (pattern #67) +#71 := (f17 #67) +#180 := (= #65 #71) +#808 := (forall (vars (?v0 S15) (?v1 S16)) (:pat #801) #180) +#184 := (forall (vars (?v0 S15) (?v1 S16)) #180) +#811 := (iff #184 #808) +#809 := (iff #180 #180) +#810 := [refl]: #809 +#812 := [quant-intro #810]: #811 +#247 := (~ #184 #184) +#245 := (~ #180 #180) +#246 := [refl]: #245 +#248 := [nnf-pos #246]: #247 +#72 := (= #71 #65) +#73 := (forall (vars (?v0 S15) (?v1 S16)) #72) +#185 := (iff #73 #184) +#182 := (iff #72 #180) +#183 := [rewrite]: #182 +#186 := [quant-intro #183]: #185 +#179 := [asserted]: #73 +#189 := [mp #179 #186]: #184 +#249 := [mp~ #189 #248]: #184 +#813 := [mp #249 #812]: #808 +#718 := (not #808) +#719 := (or #718 #375) +#714 := [quant-inst #74 #75]: #719 +#356 := [unit-resolution #714 #813]: #375 +#724 := [trans #356 #362]: #188 +#192 := (not #188) +#80 := (= #79 f19) +#81 := (not #80) +#193 := (iff #81 #192) +#190 := (iff #80 #188) +#191 := [rewrite]: #190 +#194 := [monotonicity #191]: #193 +#187 := [asserted]: #81 +#197 := [mp #187 #194]: #192 +[unit-resolution #197 #724]: false +unsat +81664cdfae8156255b7987f37aef4ab63fd862c1 97 0 +#2 := false +decl f18 :: (-> S4 S16) +decl f15 :: (-> S5 S4) +decl f4 :: (-> S4 S5 S5) +decl f9 :: S5 +#22 := f9 +decl f16 :: (-> S15 S16 S4) +decl f20 :: S16 +#75 := f20 +decl f19 :: S15 +#74 := f19 +#76 := (f16 f19 f20) +#77 := (f4 #76 f9) +#78 := (f15 #77) +#79 := (f18 #78) +#188 := (= f20 #79) +#728 := (f18 #76) +#361 := (= #728 #79) +#721 := (= #79 #728) +#717 := (= #78 #76) +#320 := (= #76 #78) +#11 := (:var 0 S5) +#10 := (:var 1 S4) +#12 := (f4 #10 #11) +#767 := (pattern #12) +#56 := (f15 #12) +#156 := (= #10 #56) +#787 := (forall (vars (?v0 S4) (?v1 S5)) (:pat #767) #156) +#160 := (forall (vars (?v0 S4) (?v1 S5)) #156) +#790 := (iff #160 #787) +#788 := (iff #156 #156) +#789 := [refl]: #788 +#791 := [quant-intro #789]: #790 +#232 := (~ #160 #160) +#230 := (~ #156 #156) +#231 := [refl]: #230 +#233 := [nnf-pos #231]: #232 +#57 := (= #56 #10) +#58 := (forall (vars (?v0 S4) (?v1 S5)) #57) +#161 := (iff #58 #160) +#158 := (iff #57 #156) +#159 := [rewrite]: #158 +#162 := [quant-intro #159]: #161 +#155 := [asserted]: #58 +#165 := [mp #155 #162]: #160 +#234 := [mp~ #165 #233]: #160 +#792 := [mp #234 #791]: #787 +#408 := (not #787) +#322 := (or #408 #320) +#409 := [quant-inst #76 #22]: #322 +#716 := [unit-resolution #409 #792]: #320 +#720 := [symm #716]: #717 +#723 := [monotonicity #720]: #721 +#362 := [symm #723]: #361 +#386 := (= f20 #728) +#66 := (:var 0 S16) +#65 := (:var 1 S15) +#67 := (f16 #65 #66) +#801 := (pattern #67) +#68 := (f18 #67) +#172 := (= #66 #68) +#802 := (forall (vars (?v0 S15) (?v1 S16)) (:pat #801) #172) +#176 := (forall (vars (?v0 S15) (?v1 S16)) #172) +#805 := (iff #176 #802) +#803 := (iff #172 #172) +#804 := [refl]: #803 +#806 := [quant-intro #804]: #805 +#242 := (~ #176 #176) +#240 := (~ #172 #172) +#241 := [refl]: #240 +#243 := [nnf-pos #241]: #242 +#69 := (= #68 #66) +#70 := (forall (vars (?v0 S15) (?v1 S16)) #69) +#177 := (iff #70 #176) +#174 := (iff #69 #172) +#175 := [rewrite]: #174 +#178 := [quant-intro #175]: #177 +#171 := [asserted]: #70 +#181 := [mp #171 #178]: #176 +#244 := [mp~ #181 #243]: #176 +#807 := [mp #244 #806]: #802 +#376 := (not #802) +#377 := (or #376 #386) +#715 := [quant-inst #74 #75]: #377 +#356 := [unit-resolution #715 #807]: #386 +#724 := [trans #356 #362]: #188 +#192 := (not #188) +#80 := (= #79 f20) +#81 := (not #80) +#193 := (iff #81 #192) +#190 := (iff #80 #188) +#191 := [rewrite]: #190 +#194 := [monotonicity #191]: #193 +#187 := [asserted]: #81 +#197 := [mp #187 #194]: #192 +[unit-resolution #197 #724]: false +unsat +cf613377475a54ad92f6fa8003d09874c4dd987e 27 0 +#2 := false +decl f11 :: (-> S4 Int) +decl f13 :: S4 +#39 := f13 +#42 := (f11 f13) +decl f12 :: S4 +#38 := f12 +#41 := (f11 f12) +#43 := (= #41 #42) +#40 := (= f12 f13) +#92 := (not #40) +#94 := (or #92 #43) +#97 := (not #94) +#44 := (implies #40 #43) +#45 := (not #44) +#98 := (iff #45 #97) +#95 := (iff #44 #94) +#96 := [rewrite]: #95 +#99 := [monotonicity #96]: #98 +#91 := [asserted]: #45 +#102 := [mp #91 #99]: #97 +#100 := [not-or-elim #102]: #40 +#277 := [monotonicity #100]: #43 +#101 := (not #43) +#103 := [not-or-elim #102]: #101 +[unit-resolution #103 #277]: false +unsat +6d6860bfe81ec3edbe1c99a18aabbf9ae1253e74 27 0 +#2 := false +decl f10 :: (-> S4 Int) +decl f13 :: S4 +#39 := f13 +#42 := (f10 f13) +decl f12 :: S4 +#38 := f12 +#41 := (f10 f12) +#43 := (= #41 #42) +#40 := (= f12 f13) +#92 := (not #40) +#94 := (or #92 #43) +#97 := (not #94) +#44 := (implies #40 #43) +#45 := (not #44) +#98 := (iff #45 #97) +#95 := (iff #44 #94) +#96 := [rewrite]: #95 +#99 := [monotonicity #96]: #98 +#91 := [asserted]: #45 +#102 := [mp #91 #99]: #97 +#100 := [not-or-elim #102]: #40 +#277 := [monotonicity #100]: #43 +#101 := (not #43) +#103 := [not-or-elim #102]: #101 +[unit-resolution #103 #277]: false +unsat +ef081363dddbf9a4a6afa336a6060e79996228d7 27 0 +#2 := false +decl f11 :: (-> S4 Int) +decl f13 :: S4 +#40 := f13 +#41 := (f11 f13) +decl f12 :: S4 +#38 := f12 +#39 := (f11 f12) +#42 := (= #39 #41) +#44 := (= f12 f13) +#45 := (not #44) +#94 := (or #42 #45) +#98 := (not #94) +#43 := (not #42) +#46 := (implies #43 #45) +#47 := (not #46) +#99 := (iff #47 #98) +#96 := (iff #46 #94) +#97 := [rewrite]: #96 +#100 := [monotonicity #97]: #99 +#93 := [asserted]: #47 +#103 := [mp #93 #100]: #98 +#102 := [not-or-elim #103]: #44 +#277 := [monotonicity #102]: #42 +#101 := [not-or-elim #103]: #43 +[unit-resolution #101 #277]: false +unsat +903c4f7ca1d07607d314979b3f7a41a8fc46e4c9 27 0 +#2 := false +decl f10 :: (-> S4 Int) +decl f13 :: S4 +#40 := f13 +#41 := (f10 f13) +decl f12 :: S4 +#38 := f12 +#39 := (f10 f12) +#42 := (= #39 #41) +#44 := (= f12 f13) +#45 := (not #44) +#94 := (or #42 #45) +#98 := (not #94) +#43 := (not #42) +#46 := (implies #43 #45) +#47 := (not #46) +#99 := (iff #47 #98) +#96 := (iff #46 #94) +#97 := [rewrite]: #96 +#100 := [monotonicity #97]: #99 +#93 := [asserted]: #47 +#103 := [mp #93 #100]: #98 +#102 := [not-or-elim #103]: #44 +#277 := [monotonicity #102]: #42 +#101 := [not-or-elim #103]: #43 +[unit-resolution #101 #277]: false +unsat +c2ddf97e343f0f179028b651e27488b381d9b232 54 0 +#2 := false +#38 := 3::Int +decl f11 :: (-> S4 Int) +decl f4 :: (-> Int Int S3 S4) +decl f12 :: S3 +#40 := f12 +#39 := 4::Int +#41 := (f4 3::Int 4::Int f12) +#42 := (f11 #41) +#43 := (= #42 3::Int) +#44 := (not #43) +#90 := [asserted]: #44 +#11 := (:var 0 S3) +#10 := (:var 1 Int) +#9 := (:var 2 Int) +#12 := (f4 #9 #10 #11) +#214 := (pattern #12) +#35 := (f11 #12) +#83 := (= #9 #35) +#227 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) (:pat #214) #83) +#87 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) #83) +#230 := (iff #87 #227) +#228 := (iff #83 #83) +#229 := [refl]: #228 +#231 := [quant-intro #229]: #230 +#130 := (~ #87 #87) +#128 := (~ #83 #83) +#129 := [refl]: #128 +#131 := [nnf-pos #129]: #130 +#36 := (= #35 #9) +#37 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) #36) +#88 := (iff #37 #87) +#85 := (iff #36 #83) +#86 := [rewrite]: #85 +#89 := [quant-intro #86]: #88 +#82 := [asserted]: #37 +#92 := [mp #82 #89]: #87 +#132 := [mp~ #92 #131]: #87 +#232 := [mp #132 #231]: #227 +#233 := (not #227) +#234 := (or #233 #43) +#91 := (= 3::Int #42) +#235 := (or #233 #91) +#237 := (iff #235 #234) +#239 := (iff #234 #234) +#240 := [rewrite]: #239 +#98 := (iff #91 #43) +#99 := [rewrite]: #98 +#238 := [monotonicity #99]: #237 +#241 := [trans #238 #240]: #237 +#236 := [quant-inst #38 #39 #40]: #235 +#242 := [mp #236 #241]: #234 +[unit-resolution #242 #232 #90]: false +unsat +57a3abfe79abd00a70bcda611ae3d757ad63951c 54 0 +#2 := false +#39 := 4::Int +decl f10 :: (-> S4 Int) +decl f4 :: (-> Int Int S3 S4) +decl f12 :: S3 +#40 := f12 +#38 := 3::Int +#41 := (f4 3::Int 4::Int f12) +#42 := (f10 #41) +#43 := (= #42 4::Int) +#44 := (not #43) +#90 := [asserted]: #44 +#11 := (:var 0 S3) +#10 := (:var 1 Int) +#9 := (:var 2 Int) +#12 := (f4 #9 #10 #11) +#214 := (pattern #12) +#32 := (f10 #12) +#75 := (= #10 #32) +#221 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) (:pat #214) #75) +#79 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) #75) +#224 := (iff #79 #221) +#222 := (iff #75 #75) +#223 := [refl]: #222 +#225 := [quant-intro #223]: #224 +#125 := (~ #79 #79) +#123 := (~ #75 #75) +#124 := [refl]: #123 +#126 := [nnf-pos #124]: #125 +#33 := (= #32 #10) +#34 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) #33) +#80 := (iff #34 #79) +#77 := (iff #33 #75) +#78 := [rewrite]: #77 +#81 := [quant-intro #78]: #80 +#74 := [asserted]: #34 +#84 := [mp #74 #81]: #79 +#127 := [mp~ #84 #126]: #79 +#226 := [mp #127 #225]: #221 +#248 := (not #221) +#249 := (or #248 #43) +#91 := (= 4::Int #42) +#250 := (or #248 #91) +#252 := (iff #250 #249) +#254 := (iff #249 #249) +#255 := [rewrite]: #254 +#98 := (iff #91 #43) +#99 := [rewrite]: #98 +#253 := [monotonicity #99]: #252 +#256 := [trans #253 #255]: #252 +#251 := [quant-inst #38 #39 #40]: #250 +#257 := [mp #251 #256]: #249 +[unit-resolution #257 #226 #90]: false +unsat +1627078085337168675bc7c62614c7f389cf7cb9 109 0 +#2 := false +#39 := 4::Int +#38 := 3::Int +#269 := (= 3::Int 4::Int) +#271 := (iff #269 false) +#272 := [rewrite]: #271 +decl f10 :: (-> S4 Int) +decl f4 :: (-> Int Int S3 S4) +decl f12 :: S3 +#40 := f12 +#41 := (f4 3::Int 4::Int f12) +#43 := (f10 #41) +#245 := (= #43 4::Int) +#11 := (:var 0 S3) +#10 := (:var 1 Int) +#9 := (:var 2 Int) +#12 := (f4 #9 #10 #11) +#209 := (pattern #12) +#32 := (f10 #12) +#77 := (= #10 #32) +#216 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) (:pat #209) #77) +#81 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) #77) +#219 := (iff #81 #216) +#217 := (iff #77 #77) +#218 := [refl]: #217 +#220 := [quant-intro #218]: #219 +#120 := (~ #81 #81) +#118 := (~ #77 #77) +#119 := [refl]: #118 +#121 := [nnf-pos #119]: #120 +#33 := (= #32 #10) +#34 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) #33) +#82 := (iff #34 #81) +#79 := (iff #33 #77) +#80 := [rewrite]: #79 +#83 := [quant-intro #80]: #82 +#76 := [asserted]: #34 +#86 := [mp #76 #83]: #81 +#122 := [mp~ #86 #121]: #81 +#221 := [mp #122 #220]: #216 +#246 := (not #216) +#247 := (or #246 #245) +#242 := (= 4::Int #43) +#248 := (or #246 #242) +#250 := (iff #248 #247) +#252 := (iff #247 #247) +#253 := [rewrite]: #252 +#243 := (iff #242 #245) +#244 := [rewrite]: #243 +#251 := [monotonicity #244]: #250 +#254 := [trans #251 #253]: #250 +#249 := [quant-inst #38 #39 #40]: #248 +#255 := [mp #249 #254]: #247 +#258 := [unit-resolution #255 #221]: #245 +#267 := (= 3::Int #43) +#265 := (= #43 3::Int) +decl f11 :: (-> S4 Int) +#42 := (f11 #41) +#231 := (= #42 3::Int) +#35 := (f11 #12) +#85 := (= #9 #35) +#222 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) (:pat #209) #85) +#89 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) #85) +#225 := (iff #89 #222) +#223 := (iff #85 #85) +#224 := [refl]: #223 +#226 := [quant-intro #224]: #225 +#125 := (~ #89 #89) +#123 := (~ #85 #85) +#124 := [refl]: #123 +#126 := [nnf-pos #124]: #125 +#36 := (= #35 #9) +#37 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S3)) #36) +#90 := (iff #37 #89) +#87 := (iff #36 #85) +#88 := [rewrite]: #87 +#91 := [quant-intro #88]: #90 +#84 := [asserted]: #37 +#94 := [mp #84 #91]: #89 +#127 := [mp~ #94 #126]: #89 +#227 := [mp #127 #226]: #222 +#232 := (not #222) +#233 := (or #232 #231) +#228 := (= 3::Int #42) +#234 := (or #232 #228) +#236 := (iff #234 #233) +#238 := (iff #233 #233) +#239 := [rewrite]: #238 +#229 := (iff #228 #231) +#230 := [rewrite]: #229 +#237 := [monotonicity #230]: #236 +#240 := [trans #237 #239]: #236 +#235 := [quant-inst #38 #39 #40]: #234 +#241 := [mp #235 #240]: #233 +#259 := [unit-resolution #241 #227]: #231 +#263 := (= #43 #42) +#44 := (= #42 #43) +#45 := (not #44) +#46 := (not #45) +#93 := (iff #46 #44) +#95 := [rewrite]: #93 +#92 := [asserted]: #46 +#98 := [mp #92 #95]: #44 +#264 := [symm #98]: #263 +#266 := [trans #264 #259]: #265 +#268 := [symm #266]: #267 +#270 := [trans #268 #258]: #269 +[mp #270 #272]: false +unsat +5633d72176578081af78ab5b81311524f1bf4c82 73 0 +#2 := false +decl f6 :: (-> Int Int S4 S5) +decl f13 :: S4 +#47 := f13 +#46 := 4::Int +#12 := 5::Int +#50 := (f6 5::Int 4::Int f13) +decl f9 :: (-> S2 S5 S5) +#45 := 3::Int +#48 := (f6 3::Int 4::Int f13) +decl f4 :: S2 +#8 := f4 +#49 := (f9 f4 #48) +#51 := (= #49 #50) +decl f3 :: (-> S2 Int Int) +#302 := (f3 f4 3::Int) +#303 := (f6 #302 4::Int f13) +#343 := (= #303 #50) +#341 := (= #50 #303) +#335 := (= 5::Int #302) +#331 := (= #302 5::Int) +#9 := (:var 0 Int) +#10 := (f3 f4 #9) +#11 := (pattern #10) +#13 := (= #10 5::Int) +#14 := (forall (vars (?v0 Int)) (:pat #11) #13) +#104 := (~ #14 #14) +#102 := (~ #13 #13) +#103 := [refl]: #102 +#105 := [nnf-pos #103]: #104 +#72 := [asserted]: #14 +#106 := [mp~ #72 #105]: #14 +#336 := (not #14) +#337 := (or #336 #331) +#338 := [quant-inst #45]: #337 +#332 := [unit-resolution #338 #106]: #331 +#339 := [symm #332]: #335 +#342 := [monotonicity #339]: #341 +#344 := [symm #342]: #343 +#306 := (= #49 #303) +#18 := (:var 0 S4) +#17 := (:var 1 Int) +#16 := (:var 2 Int) +#25 := (:var 3 S2) +#32 := (f3 #25 #16) +#33 := (f6 #32 #17 #18) +#211 := (pattern #33) +#19 := (f6 #16 #17 #18) +#31 := (f9 #25 #19) +#210 := (pattern #31) +#34 := (= #31 #33) +#212 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) (:pat #210 #211) #34) +#35 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) #34) +#215 := (iff #35 #212) +#213 := (iff #34 #34) +#214 := [refl]: #213 +#216 := [quant-intro #214]: #215 +#119 := (~ #35 #35) +#117 := (~ #34 #34) +#118 := [refl]: #117 +#120 := [nnf-pos #118]: #119 +#75 := [asserted]: #35 +#121 := [mp~ #75 #120]: #35 +#217 := [mp #121 #216]: #212 +#309 := (not #212) +#310 := (or #309 #306) +#311 := [quant-inst #8 #45 #46 #47]: #310 +#340 := [unit-resolution #311 #217]: #306 +#345 := [trans #340 #344]: #51 +#52 := (not #51) +#99 := [asserted]: #52 +[unit-resolution #99 #345]: false +unsat +5ea02bfc9534897f0d6e70c9e3473bb7ef10a30a 73 0 +#2 := false +decl f6 :: (-> Int Int S4 S5) +decl f13 :: S4 +#47 := f13 +#12 := 6::Int +#45 := 3::Int +#50 := (f6 3::Int 6::Int f13) +decl f8 :: (-> S2 S5 S5) +#46 := 4::Int +#48 := (f6 3::Int 4::Int f13) +decl f4 :: S2 +#8 := f4 +#49 := (f8 f4 #48) +#51 := (= #49 #50) +decl f3 :: (-> S2 Int Int) +#302 := (f3 f4 4::Int) +#303 := (f6 3::Int #302 f13) +#343 := (= #303 #50) +#341 := (= #50 #303) +#335 := (= 6::Int #302) +#331 := (= #302 6::Int) +#9 := (:var 0 Int) +#10 := (f3 f4 #9) +#11 := (pattern #10) +#13 := (= #10 6::Int) +#14 := (forall (vars (?v0 Int)) (:pat #11) #13) +#104 := (~ #14 #14) +#102 := (~ #13 #13) +#103 := [refl]: #102 +#105 := [nnf-pos #103]: #104 +#72 := [asserted]: #14 +#106 := [mp~ #72 #105]: #14 +#336 := (not #14) +#337 := (or #336 #331) +#338 := [quant-inst #46]: #337 +#332 := [unit-resolution #338 #106]: #331 +#339 := [symm #332]: #335 +#342 := [monotonicity #339]: #341 +#344 := [symm #342]: #343 +#306 := (= #49 #303) +#18 := (:var 0 S4) +#17 := (:var 1 Int) +#25 := (:var 3 S2) +#27 := (f3 #25 #17) +#16 := (:var 2 Int) +#28 := (f6 #16 #27 #18) +#203 := (pattern #28) +#19 := (f6 #16 #17 #18) +#26 := (f8 #25 #19) +#202 := (pattern #26) +#29 := (= #26 #28) +#204 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) (:pat #202 #203) #29) +#30 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) #29) +#207 := (iff #30 #204) +#205 := (iff #29 #29) +#206 := [refl]: #205 +#208 := [quant-intro #206]: #207 +#114 := (~ #30 #30) +#112 := (~ #29 #29) +#113 := [refl]: #112 +#115 := [nnf-pos #113]: #114 +#74 := [asserted]: #30 +#116 := [mp~ #74 #115]: #30 +#209 := [mp #116 #208]: #204 +#309 := (not #204) +#310 := (or #309 #306) +#311 := [quant-inst #8 #45 #46 #47]: #310 +#340 := [unit-resolution #311 #209]: #306 +#345 := [trans #340 #344]: #51 +#52 := (not #51) +#99 := [asserted]: #52 +[unit-resolution #99 #345]: false +unsat +0ea4cdefb3e3290c8d99d636ae708d57bfa0c66f 211 0 +#2 := false +decl f9 :: (-> S2 S5 S5) +decl f10 :: (-> S2 S5 S5) +decl f14 :: S5 +#51 := f14 +decl f5 :: S2 +#15 := f5 +#55 := (f10 f5 f14) +decl f4 :: S2 +#8 := f4 +#56 := (f9 f4 #55) +#108 := (= f14 #56) +decl f7 :: (-> Int Int S4 S5) +decl f11 :: (-> S5 S4) +decl f15 :: S4 +#52 := f15 +#12 := 4::Int +#18 := 3::Int +#53 := (f7 3::Int 4::Int f15) +#316 := (f11 #53) +decl f3 :: (-> S2 Int Int) +#269 := (f3 f5 3::Int) +#318 := (f7 #269 4::Int #316) +#350 := (f9 f4 #318) +#431 := (= #350 #56) +#424 := (= #56 #350) +#422 := (= #55 #318) +#270 := (f7 #269 4::Int f15) +#418 := (= #270 #318) +#415 := (= #318 #270) +#404 := (= #316 f15) +#317 := (= f15 #316) +#24 := (:var 0 S4) +#23 := (:var 1 Int) +#22 := (:var 2 Int) +#25 := (f7 #22 #23 #24) +#250 := (pattern #25) +#42 := (f11 #25) +#85 := (= #24 #42) +#251 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S4)) (:pat #250) #85) +#88 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S4)) #85) +#254 := (iff #88 #251) +#252 := (iff #85 #85) +#253 := [refl]: #252 +#255 := [quant-intro #253]: #254 +#156 := (~ #88 #88) +#154 := (~ #85 #85) +#155 := [refl]: #154 +#157 := [nnf-pos #155]: #156 +#43 := (= #42 #24) +#44 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S4)) #43) +#89 := (iff #44 #88) +#86 := (iff #43 #85) +#87 := [rewrite]: #86 +#90 := [quant-intro #87]: #89 +#84 := [asserted]: #44 +#93 := [mp #84 #90]: #88 +#158 := [mp~ #93 #157]: #88 +#256 := [mp #158 #255]: #251 +#320 := (not #251) +#321 := (or #320 #317) +#322 := [quant-inst #18 #12 #52]: #321 +#403 := [unit-resolution #322 #256]: #317 +#408 := [symm #403]: #404 +#416 := [monotonicity #408]: #415 +#419 := [symm #416]: #418 +#420 := (= #55 #270) +#271 := (f10 f5 #53) +#272 := (= #271 #270) +#273 := (= #270 #271) +#31 := (:var 3 S2) +#38 := (f3 #31 #22) +#39 := (f7 #38 #23 #24) +#243 := (pattern #39) +#37 := (f10 #31 #25) +#242 := (pattern #37) +#40 := (= #37 #39) +#244 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) (:pat #242 #243) #40) +#41 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) #40) +#247 := (iff #41 #244) +#245 := (iff #40 #40) +#246 := [refl]: #245 +#248 := [quant-intro #246]: #247 +#151 := (~ #41 #41) +#149 := (~ #40 #40) +#150 := [refl]: #149 +#152 := [nnf-pos #150]: #151 +#83 := [asserted]: #41 +#153 := [mp~ #83 #152]: #41 +#249 := [mp #153 #248]: #244 +#276 := (not #244) +#277 := (or #276 #273) +#278 := (or #276 #272) +#280 := (iff #278 #277) +#282 := (iff #277 #277) +#283 := [rewrite]: #282 +#274 := (iff #272 #273) +#275 := [rewrite]: #274 +#281 := [monotonicity #275]: #280 +#284 := [trans #281 #283]: #280 +#279 := [quant-inst #15 #18 #12 #52]: #278 +#285 := [mp #279 #284]: #277 +#412 := [unit-resolution #285 #249]: #273 +#417 := [symm #412]: #272 +#413 := (= #55 #271) +#54 := (= f14 #53) +#115 := (not #54) +#116 := (or #115 #108) +#121 := (not #116) +#57 := (= #56 f14) +#58 := (implies #54 #57) +#59 := (not #58) +#122 := (iff #59 #121) +#119 := (iff #58 #116) +#112 := (implies #54 #108) +#117 := (iff #112 #116) +#118 := [rewrite]: #117 +#113 := (iff #58 #112) +#110 := (iff #57 #108) +#111 := [rewrite]: #110 +#114 := [monotonicity #111]: #113 +#120 := [trans #114 #118]: #119 +#123 := [monotonicity #120]: #122 +#107 := [asserted]: #59 +#126 := [mp #107 #123]: #121 +#124 := [not-or-elim #126]: #54 +#414 := [monotonicity #124]: #413 +#421 := [trans #414 #417]: #420 +#423 := [trans #421 #419]: #422 +#425 := [monotonicity #423]: #424 +#432 := [symm #425]: #431 +#435 := (= f14 #350) +#343 := (f3 f4 4::Int) +#346 := (f7 #269 #343 #316) +#352 := (= #346 #350) +#33 := (f3 #31 #23) +#34 := (f7 #22 #33 #24) +#235 := (pattern #34) +#32 := (f9 #31 #25) +#234 := (pattern #32) +#35 := (= #32 #34) +#236 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) (:pat #234 #235) #35) +#36 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) #35) +#239 := (iff #36 #236) +#237 := (iff #35 #35) +#238 := [refl]: #237 +#240 := [quant-intro #238]: #239 +#146 := (~ #36 #36) +#144 := (~ #35 #35) +#145 := [refl]: #144 +#147 := [nnf-pos #145]: #146 +#82 := [asserted]: #36 +#148 := [mp~ #82 #147]: #36 +#241 := [mp #148 #240]: #236 +#355 := (not #236) +#356 := (or #355 #352) +#351 := (= #350 #346) +#357 := (or #355 #351) +#359 := (iff #357 #356) +#361 := (iff #356 #356) +#362 := [rewrite]: #361 +#353 := (iff #351 #352) +#354 := [rewrite]: #353 +#360 := [monotonicity #354]: #359 +#363 := [trans #360 #362]: #359 +#358 := [quant-inst #8 #269 #12 #316]: #357 +#364 := [mp #358 #363]: #356 +#411 := [unit-resolution #364 #241]: #352 +#433 := (= f14 #346) +#429 := (= #53 #346) +#427 := (= #346 #53) +#402 := (= #343 4::Int) +#9 := (:var 0 Int) +#10 := (f3 f4 #9) +#11 := (pattern #10) +#13 := (= #10 4::Int) +#14 := (forall (vars (?v0 Int)) (:pat #11) #13) +#131 := (~ #14 #14) +#129 := (~ #13 #13) +#130 := [refl]: #129 +#132 := [nnf-pos #130]: #131 +#79 := [asserted]: #14 +#133 := [mp~ #79 #132]: #14 +#405 := (not #14) +#406 := (or #405 #402) +#407 := [quant-inst #12]: #406 +#409 := [unit-resolution #407 #133]: #402 +#342 := (= #269 3::Int) +#16 := (f3 f5 #9) +#17 := (pattern #16) +#19 := (= #16 3::Int) +#20 := (forall (vars (?v0 Int)) (:pat #17) #19) +#136 := (~ #20 #20) +#134 := (~ #19 #19) +#135 := [refl]: #134 +#137 := [nnf-pos #135]: #136 +#80 := [asserted]: #20 +#138 := [mp~ #80 #137]: #20 +#347 := (not #20) +#348 := (or #347 #342) +#349 := [quant-inst #18]: #348 +#410 := [unit-resolution #349 #138]: #342 +#428 := [monotonicity #410 #409 #408]: #427 +#430 := [symm #428]: #429 +#434 := [trans #124 #430]: #433 +#436 := [trans #434 #411]: #435 +#437 := [trans #436 #432]: #108 +#125 := (not #108) +#127 := [not-or-elim #126]: #125 +[unit-resolution #127 #437]: false +unsat +18733e050cdd31352b0648b5596d94a4afc48033 211 0 +#2 := false +decl f10 :: (-> S2 S5 S5) +decl f9 :: (-> S2 S5 S5) +decl f14 :: S5 +#51 := f14 +decl f4 :: S2 +#8 := f4 +#55 := (f9 f4 f14) +decl f5 :: S2 +#15 := f5 +#56 := (f10 f5 #55) +#108 := (= f14 #56) +decl f7 :: (-> Int Int S4 S5) +decl f11 :: (-> S5 S4) +decl f15 :: S4 +#52 := f15 +#12 := 4::Int +#18 := 3::Int +#53 := (f7 3::Int 4::Int f15) +#316 := (f11 #53) +decl f3 :: (-> S2 Int Int) +#269 := (f3 f4 4::Int) +#318 := (f7 3::Int #269 #316) +#350 := (f10 f5 #318) +#431 := (= #350 #56) +#424 := (= #56 #350) +#422 := (= #55 #318) +#270 := (f7 3::Int #269 f15) +#418 := (= #270 #318) +#415 := (= #318 #270) +#404 := (= #316 f15) +#317 := (= f15 #316) +#24 := (:var 0 S4) +#23 := (:var 1 Int) +#22 := (:var 2 Int) +#25 := (f7 #22 #23 #24) +#250 := (pattern #25) +#42 := (f11 #25) +#85 := (= #24 #42) +#251 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S4)) (:pat #250) #85) +#88 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S4)) #85) +#254 := (iff #88 #251) +#252 := (iff #85 #85) +#253 := [refl]: #252 +#255 := [quant-intro #253]: #254 +#156 := (~ #88 #88) +#154 := (~ #85 #85) +#155 := [refl]: #154 +#157 := [nnf-pos #155]: #156 +#43 := (= #42 #24) +#44 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S4)) #43) +#89 := (iff #44 #88) +#86 := (iff #43 #85) +#87 := [rewrite]: #86 +#90 := [quant-intro #87]: #89 +#84 := [asserted]: #44 +#93 := [mp #84 #90]: #88 +#158 := [mp~ #93 #157]: #88 +#256 := [mp #158 #255]: #251 +#320 := (not #251) +#321 := (or #320 #317) +#322 := [quant-inst #18 #12 #52]: #321 +#403 := [unit-resolution #322 #256]: #317 +#408 := [symm #403]: #404 +#416 := [monotonicity #408]: #415 +#419 := [symm #416]: #418 +#420 := (= #55 #270) +#271 := (f9 f4 #53) +#272 := (= #271 #270) +#273 := (= #270 #271) +#31 := (:var 3 S2) +#33 := (f3 #31 #23) +#34 := (f7 #22 #33 #24) +#235 := (pattern #34) +#32 := (f9 #31 #25) +#234 := (pattern #32) +#35 := (= #32 #34) +#236 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) (:pat #234 #235) #35) +#36 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) #35) +#239 := (iff #36 #236) +#237 := (iff #35 #35) +#238 := [refl]: #237 +#240 := [quant-intro #238]: #239 +#146 := (~ #36 #36) +#144 := (~ #35 #35) +#145 := [refl]: #144 +#147 := [nnf-pos #145]: #146 +#82 := [asserted]: #36 +#148 := [mp~ #82 #147]: #36 +#241 := [mp #148 #240]: #236 +#276 := (not #236) +#277 := (or #276 #273) +#278 := (or #276 #272) +#280 := (iff #278 #277) +#282 := (iff #277 #277) +#283 := [rewrite]: #282 +#274 := (iff #272 #273) +#275 := [rewrite]: #274 +#281 := [monotonicity #275]: #280 +#284 := [trans #281 #283]: #280 +#279 := [quant-inst #8 #18 #12 #52]: #278 +#285 := [mp #279 #284]: #277 +#412 := [unit-resolution #285 #241]: #273 +#417 := [symm #412]: #272 +#413 := (= #55 #271) +#54 := (= f14 #53) +#115 := (not #54) +#116 := (or #115 #108) +#121 := (not #116) +#57 := (= #56 f14) +#58 := (implies #54 #57) +#59 := (not #58) +#122 := (iff #59 #121) +#119 := (iff #58 #116) +#112 := (implies #54 #108) +#117 := (iff #112 #116) +#118 := [rewrite]: #117 +#113 := (iff #58 #112) +#110 := (iff #57 #108) +#111 := [rewrite]: #110 +#114 := [monotonicity #111]: #113 +#120 := [trans #114 #118]: #119 +#123 := [monotonicity #120]: #122 +#107 := [asserted]: #59 +#126 := [mp #107 #123]: #121 +#124 := [not-or-elim #126]: #54 +#414 := [monotonicity #124]: #413 +#421 := [trans #414 #417]: #420 +#423 := [trans #421 #419]: #422 +#425 := [monotonicity #423]: #424 +#432 := [symm #425]: #431 +#435 := (= f14 #350) +#343 := (f3 f5 3::Int) +#346 := (f7 #343 #269 #316) +#352 := (= #346 #350) +#38 := (f3 #31 #22) +#39 := (f7 #38 #23 #24) +#243 := (pattern #39) +#37 := (f10 #31 #25) +#242 := (pattern #37) +#40 := (= #37 #39) +#244 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) (:pat #242 #243) #40) +#41 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S4)) #40) +#247 := (iff #41 #244) +#245 := (iff #40 #40) +#246 := [refl]: #245 +#248 := [quant-intro #246]: #247 +#151 := (~ #41 #41) +#149 := (~ #40 #40) +#150 := [refl]: #149 +#152 := [nnf-pos #150]: #151 +#83 := [asserted]: #41 +#153 := [mp~ #83 #152]: #41 +#249 := [mp #153 #248]: #244 +#355 := (not #244) +#356 := (or #355 #352) +#351 := (= #350 #346) +#357 := (or #355 #351) +#359 := (iff #357 #356) +#361 := (iff #356 #356) +#362 := [rewrite]: #361 +#353 := (iff #351 #352) +#354 := [rewrite]: #353 +#360 := [monotonicity #354]: #359 +#363 := [trans #360 #362]: #359 +#358 := [quant-inst #15 #18 #269 #316]: #357 +#364 := [mp #358 #363]: #356 +#411 := [unit-resolution #364 #249]: #352 +#433 := (= f14 #346) +#429 := (= #53 #346) +#427 := (= #346 #53) +#342 := (= #269 4::Int) +#9 := (:var 0 Int) +#10 := (f3 f4 #9) +#11 := (pattern #10) +#13 := (= #10 4::Int) +#14 := (forall (vars (?v0 Int)) (:pat #11) #13) +#131 := (~ #14 #14) +#129 := (~ #13 #13) +#130 := [refl]: #129 +#132 := [nnf-pos #130]: #131 +#79 := [asserted]: #14 +#133 := [mp~ #79 #132]: #14 +#347 := (not #14) +#348 := (or #347 #342) +#349 := [quant-inst #12]: #348 +#409 := [unit-resolution #349 #133]: #342 +#402 := (= #343 3::Int) +#16 := (f3 f5 #9) +#17 := (pattern #16) +#19 := (= #16 3::Int) +#20 := (forall (vars (?v0 Int)) (:pat #17) #19) +#136 := (~ #20 #20) +#134 := (~ #19 #19) +#135 := [refl]: #134 +#137 := [nnf-pos #135]: #136 +#80 := [asserted]: #20 +#138 := [mp~ #80 #137]: #20 +#405 := (not #20) +#406 := (or #405 #402) +#407 := [quant-inst #18]: #406 +#410 := [unit-resolution #407 #138]: #402 +#428 := [monotonicity #410 #409 #408]: #427 +#430 := [symm #428]: #429 +#434 := [trans #124 #430]: #433 +#436 := [trans #434 #411]: #435 +#437 := [trans #436 #432]: #108 +#125 := (not #108) +#127 := [not-or-elim #126]: #125 +[unit-resolution #127 #437]: false +unsat +034f1b430cea4d797df825ad65ed44ba0879f423 27 0 +#2 := false +decl f18 :: (-> S4 Int) +decl f20 :: S4 +#66 := f20 +#69 := (f18 f20) +decl f19 :: S4 +#65 := f19 +#68 := (f18 f19) +#70 := (= #68 #69) +#67 := (= f19 f20) +#143 := (not #67) +#145 := (or #143 #70) +#148 := (not #145) +#71 := (implies #67 #70) +#72 := (not #71) +#149 := (iff #72 #148) +#146 := (iff #71 #145) +#147 := [rewrite]: #146 +#150 := [monotonicity #147]: #149 +#142 := [asserted]: #72 +#153 := [mp #142 #150]: #148 +#151 := [not-or-elim #153]: #67 +#347 := [monotonicity #151]: #70 +#152 := (not #70) +#154 := [not-or-elim #153]: #152 +[unit-resolution #154 #347]: false +unsat +abd2ff3a1f4279c6df17226a8ab8bfa529a1ad2f 27 0 +#2 := false +decl f17 :: (-> S4 Int) +decl f20 :: S4 +#66 := f20 +#69 := (f17 f20) +decl f19 :: S4 +#65 := f19 +#68 := (f17 f19) +#70 := (= #68 #69) +#67 := (= f19 f20) +#143 := (not #67) +#145 := (or #143 #70) +#148 := (not #145) +#71 := (implies #67 #70) +#72 := (not #71) +#149 := (iff #72 #148) +#146 := (iff #71 #145) +#147 := [rewrite]: #146 +#150 := [monotonicity #147]: #149 +#142 := [asserted]: #72 +#153 := [mp #142 #150]: #148 +#151 := [not-or-elim #153]: #67 +#347 := [monotonicity #151]: #70 +#152 := (not #70) +#154 := [not-or-elim #153]: #152 +[unit-resolution #154 #347]: false +unsat +bcb488b65c53b04f7a912c4badcb5fcbbb811c48 71 0 +#2 := false +decl f10 :: (-> S4 S1) +decl f20 :: S4 +#66 := f20 +#70 := (f10 f20) +decl f1 :: S1 +#4 := f1 +#149 := (= f1 #70) +decl f19 :: S4 +#65 := f19 +#68 := (f10 f19) +#145 := (= f1 #68) +#152 := (iff #145 #149) +#691 := (= #68 #70) +#67 := (= f19 f20) +#158 := (not #67) +#159 := (or #158 #152) +#164 := (not #159) +#71 := (= #70 f1) +#69 := (= #68 f1) +#72 := (iff #69 #71) +#73 := (implies #67 #72) +#74 := (not #73) +#165 := (iff #74 #164) +#162 := (iff #73 #159) +#155 := (implies #67 #152) +#160 := (iff #155 #159) +#161 := [rewrite]: #160 +#156 := (iff #73 #155) +#153 := (iff #72 #152) +#150 := (iff #71 #149) +#151 := [rewrite]: #150 +#147 := (iff #69 #145) +#148 := [rewrite]: #147 +#154 := [monotonicity #148 #151]: #153 +#157 := [monotonicity #154]: #156 +#163 := [trans #157 #161]: #162 +#166 := [monotonicity #163]: #165 +#144 := [asserted]: #74 +#169 := [mp #144 #166]: #164 +#167 := [not-or-elim #169]: #67 +#693 := [monotonicity #167]: #691 +#348 := [monotonicity #693]: #152 +#372 := (not #149) +#196 := (not #145) +#480 := (iff #196 #372) +#687 := [monotonicity #348]: #480 +#375 := [hypothesis]: #196 +#359 := [mp #375 #687]: #372 +#370 := (or #149 #145) +#197 := (iff #149 #196) +#168 := (not #152) +#198 := (iff #168 #197) +#199 := [rewrite]: #198 +#170 := [not-or-elim #169]: #168 +#200 := [mp #170 #199]: #197 +#368 := (not #197) +#369 := (or #149 #145 #368) +#284 := [def-axiom]: #369 +#361 := [unit-resolution #284 #200]: #370 +#354 := [unit-resolution #361 #375]: #149 +#360 := [unit-resolution #354 #359]: false +#694 := [lemma #360]: #145 +#696 := [mp #694 #348]: #149 +#374 := (or #372 #196) +#373 := (or #372 #196 #368) +#301 := [def-axiom]: #373 +#371 := [unit-resolution #301 #200]: #374 +#695 := [unit-resolution #371 #694]: #372 +[unit-resolution #695 #696]: false +unsat +692be396fb86f21c3efb4c10b7720c21916ee57c 27 0 +#2 := false +decl f18 :: (-> S4 Int) +decl f20 :: S4 +#67 := f20 +#68 := (f18 f20) +decl f19 :: S4 +#65 := f19 +#66 := (f18 f19) +#69 := (= #66 #68) +#71 := (= f19 f20) +#72 := (not #71) +#145 := (or #69 #72) +#149 := (not #145) +#70 := (not #69) +#73 := (implies #70 #72) +#74 := (not #73) +#150 := (iff #74 #149) +#147 := (iff #73 #145) +#148 := [rewrite]: #147 +#151 := [monotonicity #148]: #150 +#144 := [asserted]: #74 +#154 := [mp #144 #151]: #149 +#153 := [not-or-elim #154]: #71 +#347 := [monotonicity #153]: #69 +#152 := [not-or-elim #154]: #70 +[unit-resolution #152 #347]: false +unsat +8c59e0b3bbed886482ee7c694f7985c4332c80bd 27 0 +#2 := false +decl f17 :: (-> S4 Int) +decl f20 :: S4 +#67 := f20 +#68 := (f17 f20) +decl f19 :: S4 +#65 := f19 +#66 := (f17 f19) +#69 := (= #66 #68) +#71 := (= f19 f20) +#72 := (not #71) +#145 := (or #69 #72) +#149 := (not #145) +#70 := (not #69) +#73 := (implies #70 #72) +#74 := (not #73) +#150 := (iff #74 #149) +#147 := (iff #73 #145) +#148 := [rewrite]: #147 +#151 := [monotonicity #148]: #150 +#144 := [asserted]: #74 +#154 := [mp #144 #151]: #149 +#153 := [not-or-elim #154]: #71 +#347 := [monotonicity #153]: #69 +#152 := [not-or-elim #154]: #70 +[unit-resolution #152 #347]: false +unsat +ec34ee7bf3443acccceee16793505089997d4233 87 0 +#2 := false +decl f10 :: (-> S4 S1) +decl f20 :: S4 +#68 := f20 +#69 := (f10 f20) +decl f1 :: S1 +#4 := f1 +#151 := (= f1 #69) +decl f19 :: S4 +#65 := f19 +#66 := (f10 f19) +#147 := (= f1 #66) +#154 := (iff #147 #151) +#707 := (= #66 #69) +#73 := (= f19 f20) +#74 := (not #73) +#180 := (or #74 #154) +#183 := (not #180) +#70 := (= #69 f1) +#67 := (= #66 f1) +#71 := (iff #67 #70) +#72 := (not #71) +#75 := (implies #72 #74) +#76 := (not #75) +#186 := (iff #76 #183) +#170 := (iff #151 #147) +#169 := (or #74 #170) +#175 := (not #169) +#184 := (iff #175 #183) +#181 := (iff #169 #180) +#178 := (iff #170 #154) +#179 := [rewrite]: #178 +#182 := [monotonicity #179]: #181 +#185 := [monotonicity #182]: #184 +#176 := (iff #76 #175) +#173 := (iff #75 #169) +#160 := (not #147) +#161 := (iff #151 #160) +#166 := (implies #161 #74) +#171 := (iff #166 #169) +#172 := [rewrite]: #171 +#167 := (iff #75 #166) +#164 := (iff #72 #161) +#157 := (not #154) +#162 := (iff #157 #161) +#163 := [rewrite]: #162 +#158 := (iff #72 #157) +#155 := (iff #71 #154) +#152 := (iff #70 #151) +#153 := [rewrite]: #152 +#149 := (iff #67 #147) +#150 := [rewrite]: #149 +#156 := [monotonicity #150 #153]: #155 +#159 := [monotonicity #156]: #158 +#165 := [trans #159 #163]: #164 +#168 := [monotonicity #165]: #167 +#174 := [trans #168 #172]: #173 +#177 := [monotonicity #174]: #176 +#187 := [trans #177 #185]: #186 +#146 := [asserted]: #76 +#190 := [mp #146 #187]: #183 +#188 := [not-or-elim #190]: #73 +#709 := [monotonicity #188]: #707 +#364 := [monotonicity #709]: #154 +#388 := (not #151) +#496 := (iff #160 #388) +#703 := [monotonicity #364]: #496 +#391 := [hypothesis]: #160 +#375 := [mp #391 #703]: #388 +#386 := (or #151 #147) +#189 := [not-or-elim #190]: #157 +#216 := [mp #189 #163]: #161 +#384 := (not #161) +#385 := (or #151 #147 #384) +#300 := [def-axiom]: #385 +#377 := [unit-resolution #300 #216]: #386 +#370 := [unit-resolution #377 #391]: #151 +#376 := [unit-resolution #370 #375]: false +#710 := [lemma #376]: #147 +#712 := [mp #710 #364]: #151 +#390 := (or #388 #160) +#389 := (or #388 #160 #384) +#317 := [def-axiom]: #389 +#387 := [unit-resolution #317 #216]: #390 +#711 := [unit-resolution #387 #710]: #388 +[unit-resolution #711 #712]: false +unsat +c2545d9068e0d6accd875f4379ed4317f0c0b477 58 0 +#2 := false +#65 := 3::Int +decl f18 :: (-> S4 Int) +decl f4 :: (-> Int Int S5 S4) +decl f5 :: (-> S1 S3 S5) +decl f20 :: S3 +#68 := f20 +decl f19 :: S1 +#67 := f19 +#69 := (f5 f19 f20) +#66 := 4::Int +#70 := (f4 3::Int 4::Int #69) +#71 := (f18 #70) +#72 := (= #71 3::Int) +#73 := (not #72) +#143 := [asserted]: #73 +#38 := (:var 0 S5) +#37 := (:var 1 Int) +#10 := (:var 2 Int) +#39 := (f4 #10 #37 #38) +#316 := (pattern #39) +#62 := (f18 #39) +#136 := (= #10 #62) +#329 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) (:pat #316) #136) +#140 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) #136) +#332 := (iff #140 #329) +#330 := (iff #136 #136) +#331 := [refl]: #330 +#333 := [quant-intro #331]: #332 +#203 := (~ #140 #140) +#201 := (~ #136 #136) +#202 := [refl]: #201 +#204 := [nnf-pos #202]: #203 +#63 := (= #62 #10) +#64 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) #63) +#141 := (iff #64 #140) +#138 := (iff #63 #136) +#139 := [rewrite]: #138 +#142 := [quant-intro #139]: #141 +#135 := [asserted]: #64 +#145 := [mp #135 #142]: #140 +#205 := [mp~ #145 #204]: #140 +#334 := [mp #205 #333]: #329 +#335 := (not #329) +#336 := (or #335 #72) +#144 := (= 3::Int #71) +#337 := (or #335 #144) +#339 := (iff #337 #336) +#341 := (iff #336 #336) +#342 := [rewrite]: #341 +#151 := (iff #144 #72) +#152 := [rewrite]: #151 +#340 := [monotonicity #152]: #339 +#343 := [trans #340 #342]: #339 +#338 := [quant-inst #65 #66 #69]: #337 +#344 := [mp #338 #343]: #336 +[unit-resolution #344 #334 #143]: false +unsat +e3bb9ab1eb53aa14b85baa6b04545cdb6811e412 58 0 +#2 := false +#66 := 4::Int +decl f17 :: (-> S4 Int) +decl f4 :: (-> Int Int S5 S4) +decl f5 :: (-> S1 S3 S5) +decl f20 :: S3 +#68 := f20 +decl f19 :: S1 +#67 := f19 +#69 := (f5 f19 f20) +#65 := 3::Int +#70 := (f4 3::Int 4::Int #69) +#71 := (f17 #70) +#72 := (= #71 4::Int) +#73 := (not #72) +#143 := [asserted]: #73 +#38 := (:var 0 S5) +#37 := (:var 1 Int) +#10 := (:var 2 Int) +#39 := (f4 #10 #37 #38) +#316 := (pattern #39) +#59 := (f17 #39) +#128 := (= #37 #59) +#323 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) (:pat #316) #128) +#132 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) #128) +#326 := (iff #132 #323) +#324 := (iff #128 #128) +#325 := [refl]: #324 +#327 := [quant-intro #325]: #326 +#198 := (~ #132 #132) +#196 := (~ #128 #128) +#197 := [refl]: #196 +#199 := [nnf-pos #197]: #198 +#60 := (= #59 #37) +#61 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) #60) +#133 := (iff #61 #132) +#130 := (iff #60 #128) +#131 := [rewrite]: #130 +#134 := [quant-intro #131]: #133 +#127 := [asserted]: #61 +#137 := [mp #127 #134]: #132 +#200 := [mp~ #137 #199]: #132 +#328 := [mp #200 #327]: #323 +#350 := (not #323) +#351 := (or #350 #72) +#144 := (= 4::Int #71) +#352 := (or #350 #144) +#354 := (iff #352 #351) +#356 := (iff #351 #351) +#357 := [rewrite]: #356 +#151 := (iff #144 #72) +#152 := [rewrite]: #151 +#355 := [monotonicity #152]: #354 +#358 := [trans #355 #357]: #354 +#353 := [quant-inst #65 #66 #69]: #352 +#359 := [mp #353 #358]: #351 +[unit-resolution #359 #328 #143]: false +unsat +6296fe8461e452d749fb761ed56ebcfb1fc552d0 105 0 +#2 := false +decl f10 :: (-> S4 S1) +decl f4 :: (-> Int Int S5 S4) +decl f5 :: (-> S1 S3 S5) +decl f20 :: S3 +#68 := f20 +decl f19 :: S1 +#67 := f19 +#69 := (f5 f19 f20) +#66 := 4::Int +#65 := 3::Int +#70 := (f4 3::Int 4::Int #69) +#71 := (f10 #70) +decl f1 :: S1 +#4 := f1 +#146 := (= f1 #71) +#159 := (not #146) +#404 := [hypothesis]: #159 +#150 := (= f1 f19) +#349 := (or #150 #146) +#160 := (iff #150 #159) +#73 := (= f19 f1) +#72 := (= #71 f1) +#74 := (iff #72 #73) +#75 := (not #74) +#163 := (iff #75 #160) +#153 := (iff #146 #150) +#156 := (not #153) +#161 := (iff #156 #160) +#162 := [rewrite]: #161 +#157 := (iff #75 #156) +#154 := (iff #74 #153) +#151 := (iff #73 #150) +#152 := [rewrite]: #151 +#148 := (iff #72 #146) +#149 := [rewrite]: #148 +#155 := [monotonicity #149 #152]: #154 +#158 := [monotonicity #155]: #157 +#164 := [trans #158 #162]: #163 +#145 := [asserted]: #75 +#167 := [mp #145 #164]: #160 +#346 := (not #160) +#347 := (or #150 #146 #346) +#348 := [def-axiom]: #347 +#350 := [unit-resolution #348 #167]: #349 +#405 := [unit-resolution #350 #404]: #150 +#351 := (not #150) +#410 := (or #146 #351) +#12 := (:var 0 S3) +#11 := (:var 1 S1) +#13 := (f5 #11 #12) +#10 := (:var 2 Int) +#9 := (:var 3 Int) +#14 := (f4 #9 #10 #13) +#290 := (pattern #14) +#109 := (= f1 #11) +#31 := (f10 #14) +#105 := (= f1 #31) +#112 := (iff #105 #109) +#297 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S3)) (:pat #290) #112) +#115 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S3)) #112) +#300 := (iff #115 #297) +#298 := (iff #112 #112) +#299 := [refl]: #298 +#301 := [quant-intro #299]: #300 +#184 := (~ #115 #115) +#182 := (~ #112 #112) +#183 := [refl]: #182 +#185 := [nnf-pos #183]: #184 +#33 := (= #11 f1) +#32 := (= #31 f1) +#34 := (iff #32 #33) +#35 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S3)) #34) +#116 := (iff #35 #115) +#113 := (iff #34 #112) +#110 := (iff #33 #109) +#111 := [rewrite]: #110 +#107 := (iff #32 #105) +#108 := [rewrite]: #107 +#114 := [monotonicity #108 #111]: #113 +#117 := [quant-intro #114]: #116 +#104 := [asserted]: #35 +#120 := [mp #104 #117]: #115 +#186 := [mp~ #120 #185]: #115 +#302 := [mp #186 #301]: #297 +#393 := (not #297) +#394 := (or #393 #153) +#395 := [quant-inst #65 #66 #67 #68]: #394 +#409 := [unit-resolution #395 #302]: #153 +#396 := (or #156 #146 #351) +#397 := [def-axiom]: #396 +#411 := [unit-resolution #397 #409]: #410 +#412 := [unit-resolution #411 #405 #404]: false +#413 := [lemma #412]: #146 +#354 := (or #351 #159) +#352 := (or #351 #159 #346) +#353 := [def-axiom]: #352 +#355 := [unit-resolution #353 #167]: #354 +#414 := [unit-resolution #355 #413]: #351 +#415 := (or #159 #150) +#398 := (or #156 #159 #150) +#399 := [def-axiom]: #398 +#416 := [unit-resolution #399 #409]: #415 +[unit-resolution #416 #414 #413]: false +unsat +da58db0437f12c2e8d1330c20990ed8cbae3b7f4 113 0 +#2 := false +#66 := 4::Int +#65 := 3::Int +#404 := (= 3::Int 4::Int) +#406 := (iff #404 false) +#407 := [rewrite]: #406 +decl f17 :: (-> S4 Int) +decl f4 :: (-> Int Int S5 S4) +decl f5 :: (-> S1 S3 S5) +decl f20 :: S3 +#68 := f20 +decl f19 :: S1 +#67 := f19 +#69 := (f5 f19 f20) +#70 := (f4 3::Int 4::Int #69) +#72 := (f17 #70) +#347 := (= #72 4::Int) +#38 := (:var 0 S5) +#37 := (:var 1 Int) +#10 := (:var 2 Int) +#39 := (f4 #10 #37 #38) +#311 := (pattern #39) +#59 := (f17 #39) +#130 := (= #37 #59) +#318 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) (:pat #311) #130) +#134 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) #130) +#321 := (iff #134 #318) +#319 := (iff #130 #130) +#320 := [refl]: #319 +#322 := [quant-intro #320]: #321 +#193 := (~ #134 #134) +#191 := (~ #130 #130) +#192 := [refl]: #191 +#194 := [nnf-pos #192]: #193 +#60 := (= #59 #37) +#61 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) #60) +#135 := (iff #61 #134) +#132 := (iff #60 #130) +#133 := [rewrite]: #132 +#136 := [quant-intro #133]: #135 +#129 := [asserted]: #61 +#139 := [mp #129 #136]: #134 +#195 := [mp~ #139 #194]: #134 +#323 := [mp #195 #322]: #318 +#348 := (not #318) +#349 := (or #348 #347) +#344 := (= 4::Int #72) +#350 := (or #348 #344) +#352 := (iff #350 #349) +#354 := (iff #349 #349) +#355 := [rewrite]: #354 +#345 := (iff #344 #347) +#346 := [rewrite]: #345 +#353 := [monotonicity #346]: #352 +#356 := [trans #353 #355]: #352 +#351 := [quant-inst #65 #66 #69]: #350 +#357 := [mp #351 #356]: #349 +#393 := [unit-resolution #357 #323]: #347 +#402 := (= 3::Int #72) +#400 := (= #72 3::Int) +decl f18 :: (-> S4 Int) +#71 := (f18 #70) +#333 := (= #71 3::Int) +#62 := (f18 #39) +#138 := (= #10 #62) +#324 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) (:pat #311) #138) +#142 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) #138) +#327 := (iff #142 #324) +#325 := (iff #138 #138) +#326 := [refl]: #325 +#328 := [quant-intro #326]: #327 +#198 := (~ #142 #142) +#196 := (~ #138 #138) +#197 := [refl]: #196 +#199 := [nnf-pos #197]: #198 +#63 := (= #62 #10) +#64 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S5)) #63) +#143 := (iff #64 #142) +#140 := (iff #63 #138) +#141 := [rewrite]: #140 +#144 := [quant-intro #141]: #143 +#137 := [asserted]: #64 +#147 := [mp #137 #144]: #142 +#200 := [mp~ #147 #199]: #142 +#329 := [mp #200 #328]: #324 +#334 := (not #324) +#335 := (or #334 #333) +#330 := (= 3::Int #71) +#336 := (or #334 #330) +#338 := (iff #336 #335) +#340 := (iff #335 #335) +#341 := [rewrite]: #340 +#331 := (iff #330 #333) +#332 := [rewrite]: #331 +#339 := [monotonicity #332]: #338 +#342 := [trans #339 #341]: #338 +#337 := [quant-inst #65 #66 #69]: #336 +#343 := [mp #337 #342]: #335 +#394 := [unit-resolution #343 #329]: #333 +#398 := (= #72 #71) +#73 := (= #71 #72) +#74 := (not #73) +#75 := (not #74) +#146 := (iff #75 #73) +#148 := [rewrite]: #146 +#145 := [asserted]: #75 +#151 := [mp #145 #148]: #73 +#399 := [symm #151]: #398 +#401 := [trans #399 #394]: #400 +#403 := [symm #401]: #402 +#405 := [trans #403 #393]: #404 +[mp #405 #407]: false +unsat +b782d188626a2e0381f5b576a0374250a8df82c5 77 0 +#2 := false +decl f6 :: (-> Int Int S6 S5) +decl f7 :: (-> S1 S4 S6) +decl f21 :: S4 +#75 := f21 +decl f20 :: S1 +#74 := f20 +#76 := (f7 f20 f21) +#73 := 4::Int +#12 := 5::Int +#79 := (f6 5::Int 4::Int #76) +decl f16 :: (-> S2 S5 S5) +#72 := 3::Int +#77 := (f6 3::Int 4::Int #76) +decl f4 :: S2 +#8 := f4 +#78 := (f16 f4 #77) +#80 := (= #78 #79) +decl f3 :: (-> S2 Int Int) +#466 := (f3 f4 3::Int) +#467 := (f6 #466 4::Int #76) +#538 := (= #467 #79) +#536 := (= #79 #467) +#530 := (= 5::Int #466) +#526 := (= #466 5::Int) +#9 := (:var 0 Int) +#10 := (f3 f4 #9) +#11 := (pattern #10) +#13 := (= #10 5::Int) +#14 := (forall (vars (?v0 Int)) (:pat #11) #13) +#157 := (~ #14 #14) +#155 := (~ #13 #13) +#156 := [refl]: #155 +#158 := [nnf-pos #156]: #157 +#101 := [asserted]: #14 +#159 := [mp~ #101 #158]: #14 +#531 := (not #14) +#532 := (or #531 #526) +#533 := [quant-inst #72]: #532 +#527 := [unit-resolution #533 #159]: #526 +#534 := [symm #527]: #530 +#537 := [monotonicity #534]: #536 +#539 := [symm #537]: #538 +#470 := (= #78 #467) +#45 := (:var 0 S6) +#44 := (:var 1 Int) +#17 := (:var 2 Int) +#52 := (:var 3 S2) +#59 := (f3 #52 #17) +#60 := (f6 #59 #44 #45) +#313 := (pattern #60) +#46 := (f6 #17 #44 #45) +#58 := (f16 #52 #46) +#312 := (pattern #58) +#61 := (= #58 #60) +#314 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S6)) (:pat #312 #313) #61) +#62 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S6)) #61) +#317 := (iff #62 #314) +#315 := (iff #61 #61) +#316 := [refl]: #315 +#318 := [quant-intro #316]: #317 +#192 := (~ #62 #62) +#190 := (~ #61 #61) +#191 := [refl]: #190 +#193 := [nnf-pos #191]: #192 +#128 := [asserted]: #62 +#194 := [mp~ #128 #193]: #62 +#319 := [mp #194 #318]: #314 +#473 := (not #314) +#474 := (or #473 #470) +#475 := [quant-inst #8 #72 #73 #76]: #474 +#535 := [unit-resolution #475 #319]: #470 +#540 := [trans #535 #539]: #80 +#81 := (not #80) +#152 := [asserted]: #81 +[unit-resolution #152 #540]: false +unsat +a4d93eb089616c7c0d14a8c862a8b98919dd97bb 77 0 +#2 := false +decl f6 :: (-> Int Int S6 S5) +decl f7 :: (-> S1 S4 S6) +decl f21 :: S4 +#75 := f21 +decl f20 :: S1 +#74 := f20 +#76 := (f7 f20 f21) +#12 := 6::Int +#72 := 3::Int +#79 := (f6 3::Int 6::Int #76) +decl f15 :: (-> S2 S5 S5) +#73 := 4::Int +#77 := (f6 3::Int 4::Int #76) +decl f4 :: S2 +#8 := f4 +#78 := (f15 f4 #77) +#80 := (= #78 #79) +decl f3 :: (-> S2 Int Int) +#466 := (f3 f4 4::Int) +#467 := (f6 3::Int #466 #76) +#538 := (= #467 #79) +#536 := (= #79 #467) +#530 := (= 6::Int #466) +#526 := (= #466 6::Int) +#9 := (:var 0 Int) +#10 := (f3 f4 #9) +#11 := (pattern #10) +#13 := (= #10 6::Int) +#14 := (forall (vars (?v0 Int)) (:pat #11) #13) +#157 := (~ #14 #14) +#155 := (~ #13 #13) +#156 := [refl]: #155 +#158 := [nnf-pos #156]: #157 +#101 := [asserted]: #14 +#159 := [mp~ #101 #158]: #14 +#531 := (not #14) +#532 := (or #531 #526) +#533 := [quant-inst #73]: #532 +#527 := [unit-resolution #533 #159]: #526 +#534 := [symm #527]: #530 +#537 := [monotonicity #534]: #536 +#539 := [symm #537]: #538 +#470 := (= #78 #467) +#45 := (:var 0 S6) +#44 := (:var 1 Int) +#52 := (:var 3 S2) +#54 := (f3 #52 #44) +#17 := (:var 2 Int) +#55 := (f6 #17 #54 #45) +#305 := (pattern #55) +#46 := (f6 #17 #44 #45) +#53 := (f15 #52 #46) +#304 := (pattern #53) +#56 := (= #53 #55) +#306 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S6)) (:pat #304 #305) #56) +#57 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S6)) #56) +#309 := (iff #57 #306) +#307 := (iff #56 #56) +#308 := [refl]: #307 +#310 := [quant-intro #308]: #309 +#187 := (~ #57 #57) +#185 := (~ #56 #56) +#186 := [refl]: #185 +#188 := [nnf-pos #186]: #187 +#126 := [asserted]: #57 +#189 := [mp~ #126 #188]: #57 +#311 := [mp #189 #310]: #306 +#473 := (not #306) +#474 := (or #473 #470) +#475 := [quant-inst #8 #72 #73 #76]: #474 +#535 := [unit-resolution #475 #311]: #470 +#540 := [trans #535 #539]: #80 +#81 := (not #80) +#152 := [asserted]: #81 +[unit-resolution #152 #540]: false +unsat +9b928998cfefb8ac92745f24b207e3b96bdec398 409 0 +#2 := false +decl f12 :: (-> S3 S6 S6) +decl f17 :: (-> S2 S6 S6) +decl f18 :: (-> S2 S6 S6) +decl f22 :: S6 +#85 := f22 +decl f5 :: S2 +#15 := f5 +#90 := (f18 f5 f22) +decl f4 :: S2 +#8 := f4 +#91 := (f17 f4 #90) +decl f7 :: S3 +#21 := f7 +#92 := (f12 f7 #91) +#183 := (= f22 #92) +decl f9 :: (-> Int Int S7 S6) +decl f10 :: (-> S1 S5 S7) +decl f13 :: (-> S6 S5) +decl f23 :: S5 +#86 := f23 +decl f1 :: S1 +#4 := f1 +#87 := (f10 f1 f23) +#12 := 4::Int +#18 := 3::Int +#88 := (f9 3::Int 4::Int #87) +#473 := (f13 #88) +decl f14 :: (-> S6 S1) +#448 := (f14 #88) +#499 := (f10 #448 #473) +decl f3 :: (-> S2 Int Int) +#532 := (f3 f4 4::Int) +#591 := (f9 3::Int #532 #499) +#628 := (f12 f7 #591) +#793 := (= #628 #92) +#786 := (= #92 #628) +#784 := (= #91 #591) +decl f19 :: (-> S6 S7) +#445 := (f19 #88) +#398 := (f3 f5 3::Int) +#535 := (f9 #398 #532 #445) +#780 := (= #535 #591) +#778 := (= #591 #535) +#755 := (= #499 #445) +#446 := (= #87 #445) +#58 := (:var 0 S7) +#57 := (:var 1 Int) +#30 := (:var 2 Int) +#59 := (f9 #30 #57 #58) +#379 := (pattern #59) +#76 := (f19 #59) +#160 := (= #58 #76) +#380 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S7)) (:pat #379) #160) +#163 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S7)) #160) +#383 := (iff #163 #380) +#381 := (iff #160 #160) +#382 := [refl]: #381 +#384 := [quant-intro #382]: #383 +#256 := (~ #163 #163) +#254 := (~ #160 #160) +#255 := [refl]: #254 +#257 := [nnf-pos #255]: #256 +#77 := (= #76 #58) +#78 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S7)) #77) +#164 := (iff #78 #163) +#161 := (iff #77 #160) +#162 := [rewrite]: #161 +#165 := [quant-intro #162]: #164 +#159 := [asserted]: #78 +#168 := [mp #159 #165]: #163 +#258 := [mp~ #168 #257]: #163 +#385 := [mp #258 #384]: #380 +#449 := (not #380) +#450 := (or #449 #446) +#451 := [quant-inst #18 #12 #87]: #450 +#749 := [unit-resolution #451 #385]: #446 +#753 := (= #499 #87) +#737 := (= #473 f23) +#474 := (= f23 #473) +#32 := (:var 0 S5) +#31 := (:var 1 S1) +#33 := (f10 #31 #32) +#29 := (:var 3 Int) +#34 := (f9 #29 #30 #33) +#342 := (pattern #34) +#48 := (f13 #34) +#135 := (= #32 #48) +#343 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) (:pat #342) #135) +#138 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #135) +#346 := (iff #138 #343) +#344 := (iff #135 #135) +#345 := [refl]: #344 +#347 := [quant-intro #345]: #346 +#231 := (~ #138 #138) +#229 := (~ #135 #135) +#230 := [refl]: #229 +#232 := [nnf-pos #230]: #231 +#49 := (= #48 #32) +#50 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #49) +#139 := (iff #50 #138) +#136 := (iff #49 #135) +#137 := [rewrite]: #136 +#140 := [quant-intro #137]: #139 +#134 := [asserted]: #50 +#143 := [mp #134 #140]: #138 +#233 := [mp~ #143 #232]: #138 +#348 := [mp #233 #347]: #343 +#477 := (not #343) +#478 := (or #477 #474) +#479 := [quant-inst #18 #12 #4 #86]: #478 +#736 := [unit-resolution #479 #348]: #474 +#741 := [symm #736]: #737 +#751 := (= #448 f1) +#452 := (= f1 #448) +#146 := (= f1 #31) +#51 := (f14 #34) +#142 := (= f1 #51) +#149 := (iff #142 #146) +#349 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) (:pat #342) #149) +#152 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #149) +#352 := (iff #152 #349) +#350 := (iff #149 #149) +#351 := [refl]: #350 +#353 := [quant-intro #351]: #352 +#236 := (~ #152 #152) +#234 := (~ #149 #149) +#235 := [refl]: #234 +#237 := [nnf-pos #235]: #236 +#53 := (= #31 f1) +#52 := (= #51 f1) +#54 := (iff #52 #53) +#55 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #54) +#153 := (iff #55 #152) +#150 := (iff #54 #149) +#147 := (iff #53 #146) +#148 := [rewrite]: #147 +#144 := (iff #52 #142) +#145 := [rewrite]: #144 +#151 := [monotonicity #145 #148]: #150 +#154 := [quant-intro #151]: #153 +#141 := [asserted]: #55 +#157 := [mp #141 #154]: #152 +#238 := [mp~ #157 #237]: #152 +#354 := [mp #238 #353]: #349 +#463 := (not #349) +#464 := (or #463 #452) +#447 := (= f1 f1) +#453 := (iff #452 #447) +#465 := (or #463 #453) +#467 := (iff #465 #464) +#469 := (iff #464 #464) +#470 := [rewrite]: #469 +#461 := (iff #453 #452) +#1 := true +#456 := (iff #452 true) +#459 := (iff #456 #452) +#460 := [rewrite]: #459 +#457 := (iff #453 #456) +#454 := (iff #447 true) +#455 := [rewrite]: #454 +#458 := [monotonicity #455]: #457 +#462 := [trans #458 #460]: #461 +#468 := [monotonicity #462]: #467 +#471 := [trans #468 #470]: #467 +#466 := [quant-inst #18 #12 #4 #86]: #465 +#472 := [mp #466 #471]: #464 +#750 := [unit-resolution #472 #354]: #452 +#752 := [symm #750]: #751 +#754 := [monotonicity #752 #741]: #753 +#756 := [trans #754 #749]: #755 +#758 := (= 3::Int #398) +#531 := (= #398 3::Int) +#9 := (:var 0 Int) +#16 := (f3 f5 #9) +#17 := (pattern #16) +#19 := (= #16 3::Int) +#20 := (forall (vars (?v0 Int)) (:pat #17) #19) +#211 := (~ #20 #20) +#209 := (~ #19 #19) +#210 := [refl]: #209 +#212 := [nnf-pos #210]: #211 +#116 := [asserted]: #20 +#213 := [mp~ #116 #212]: #20 +#536 := (not #20) +#537 := (or #536 #531) +#538 := [quant-inst #18]: #537 +#757 := [unit-resolution #538 #213]: #531 +#759 := [symm #757]: #758 +#779 := [monotonicity #759 #756]: #778 +#781 := [symm #779]: #780 +#782 := (= #91 #535) +#475 := (f9 #398 4::Int #445) +#539 := (f17 f4 #475) +#540 := (= #539 #535) +#541 := (= #535 #539) +#65 := (:var 3 S2) +#67 := (f3 #65 #57) +#68 := (f9 #30 #67 #58) +#364 := (pattern #68) +#66 := (f17 #65 #59) +#363 := (pattern #66) +#69 := (= #66 #68) +#365 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) (:pat #363 #364) #69) +#70 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) #69) +#368 := (iff #70 #365) +#366 := (iff #69 #69) +#367 := [refl]: #366 +#369 := [quant-intro #367]: #368 +#246 := (~ #70 #70) +#244 := (~ #69 #69) +#245 := [refl]: #244 +#247 := [nnf-pos #245]: #246 +#156 := [asserted]: #70 +#248 := [mp~ #156 #247]: #70 +#370 := [mp #248 #369]: #365 +#544 := (not #365) +#545 := (or #544 #541) +#546 := (or #544 #540) +#548 := (iff #546 #545) +#550 := (iff #545 #545) +#551 := [rewrite]: #550 +#542 := (iff #540 #541) +#543 := [rewrite]: #542 +#549 := [monotonicity #543]: #548 +#552 := [trans #549 #551]: #548 +#547 := [quant-inst #8 #398 #12 #445]: #546 +#553 := [mp #547 #552]: #545 +#760 := [unit-resolution #553 #370]: #541 +#777 := [symm #760]: #540 +#775 := (= #91 #539) +#773 := (= #90 #475) +#399 := (f9 #398 4::Int #87) +#769 := (= #399 #475) +#766 := (= #475 #399) +#762 := (= #445 #87) +#763 := [symm #749]: #762 +#767 := [monotonicity #763]: #766 +#770 := [symm #767]: #769 +#771 := (= #90 #399) +#400 := (f18 f5 #88) +#401 := (= #400 #399) +#402 := (= #399 #400) +#72 := (f3 #65 #30) +#73 := (f9 #72 #57 #58) +#372 := (pattern #73) +#71 := (f18 #65 #59) +#371 := (pattern #71) +#74 := (= #71 #73) +#373 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) (:pat #371 #372) #74) +#75 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) #74) +#376 := (iff #75 #373) +#374 := (iff #74 #74) +#375 := [refl]: #374 +#377 := [quant-intro #375]: #376 +#251 := (~ #75 #75) +#249 := (~ #74 #74) +#250 := [refl]: #249 +#252 := [nnf-pos #250]: #251 +#158 := [asserted]: #75 +#253 := [mp~ #158 #252]: #75 +#378 := [mp #253 #377]: #373 +#405 := (not #373) +#406 := (or #405 #402) +#407 := (or #405 #401) +#409 := (iff #407 #406) +#411 := (iff #406 #406) +#412 := [rewrite]: #411 +#403 := (iff #401 #402) +#404 := [rewrite]: #403 +#410 := [monotonicity #404]: #409 +#413 := [trans #410 #412]: #409 +#408 := [quant-inst #15 #18 #12 #87]: #407 +#414 := [mp #408 #413]: #406 +#761 := [unit-resolution #414 #378]: #402 +#768 := [symm #761]: #401 +#764 := (= #90 #400) +#89 := (= f22 #88) +#190 := (not #89) +#191 := (or #190 #183) +#196 := (not #191) +#93 := (= #92 f22) +#94 := (implies #89 #93) +#95 := (not #94) +#197 := (iff #95 #196) +#194 := (iff #94 #191) +#187 := (implies #89 #183) +#192 := (iff #187 #191) +#193 := [rewrite]: #192 +#188 := (iff #94 #187) +#185 := (iff #93 #183) +#186 := [rewrite]: #185 +#189 := [monotonicity #186]: #188 +#195 := [trans #189 #193]: #194 +#198 := [monotonicity #195]: #197 +#182 := [asserted]: #95 +#201 := [mp #182 #198]: #196 +#199 := [not-or-elim #201]: #89 +#765 := [monotonicity #199]: #764 +#772 := [trans #765 #768]: #771 +#774 := [trans #772 #770]: #773 +#776 := [monotonicity #774]: #775 +#783 := [trans #776 #777]: #782 +#785 := [trans #783 #781]: #784 +#787 := [monotonicity #785]: #786 +#794 := [symm #787]: #793 +#797 := (= f22 #628) +decl f6 :: (-> S3 S1 S1) +#620 := (f6 f7 #448) +#623 := (f10 #620 #473) +#627 := (f9 3::Int #532 #623) +#630 := (= #627 #628) +#41 := (:var 4 S3) +#43 := (f6 #41 #31) +#44 := (f10 #43 #32) +#45 := (f9 #29 #30 #44) +#335 := (pattern #45) +#42 := (f12 #41 #34) +#334 := (pattern #42) +#46 := (= #42 #45) +#336 := (forall (vars (?v0 S3) (?v1 Int) (?v2 Int) (?v3 S1) (?v4 S5)) (:pat #334 #335) #46) +#47 := (forall (vars (?v0 S3) (?v1 Int) (?v2 Int) (?v3 S1) (?v4 S5)) #46) +#339 := (iff #47 #336) +#337 := (iff #46 #46) +#338 := [refl]: #337 +#340 := [quant-intro #338]: #339 +#226 := (~ #47 #47) +#224 := (~ #46 #46) +#225 := [refl]: #224 +#227 := [nnf-pos #225]: #226 +#132 := [asserted]: #47 +#228 := [mp~ #132 #227]: #47 +#341 := [mp #228 #340]: #336 +#633 := (not #336) +#634 := (or #633 #630) +#629 := (= #628 #627) +#635 := (or #633 #629) +#637 := (iff #635 #634) +#639 := (iff #634 #634) +#640 := [rewrite]: #639 +#631 := (iff #629 #630) +#632 := [rewrite]: #631 +#638 := [monotonicity #632]: #637 +#641 := [trans #638 #640]: #637 +#636 := [quant-inst #21 #18 #532 #448 #473]: #635 +#642 := [mp #636 #641]: #634 +#748 := [unit-resolution #642 #341]: #630 +#795 := (= f22 #627) +#791 := (= #88 #627) +#789 := (= #627 #88) +#745 := (= #623 #87) +#743 := (= #620 f1) +#691 := (= f1 #620) +#22 := (:var 0 S1) +#23 := (f6 f7 #22) +#24 := (pattern #23) +#118 := (= f1 #23) +#128 := (forall (vars (?v0 S1)) (:pat #24) #118) +#216 := (~ #128 #128) +#214 := (~ #118 #118) +#215 := [refl]: #214 +#217 := [nnf-pos #215]: #216 +#25 := (= #23 f1) +#26 := (iff #25 true) +#27 := (forall (vars (?v0 S1)) (:pat #24) #26) +#129 := (iff #27 #128) +#126 := (iff #26 #118) +#121 := (iff #118 true) +#124 := (iff #121 #118) +#125 := [rewrite]: #124 +#122 := (iff #26 #121) +#119 := (iff #25 #118) +#120 := [rewrite]: #119 +#123 := [monotonicity #120]: #122 +#127 := [trans #123 #125]: #126 +#130 := [quant-intro #127]: #129 +#117 := [asserted]: #27 +#133 := [mp #117 #130]: #128 +#218 := [mp~ #133 #217]: #128 +#738 := (not #128) +#739 := (or #738 #691) +#740 := [quant-inst #448]: #739 +#742 := [unit-resolution #740 #218]: #691 +#744 := [symm #742]: #743 +#746 := [monotonicity #744 #741]: #745 +#619 := (= #532 4::Int) +#10 := (f3 f4 #9) +#11 := (pattern #10) +#13 := (= #10 4::Int) +#14 := (forall (vars (?v0 Int)) (:pat #11) #13) +#206 := (~ #14 #14) +#204 := (~ #13 #13) +#205 := [refl]: #204 +#207 := [nnf-pos #205]: #206 +#115 := [asserted]: #14 +#208 := [mp~ #115 #207]: #14 +#624 := (not #14) +#625 := (or #624 #619) +#626 := [quant-inst #12]: #625 +#747 := [unit-resolution #626 #208]: #619 +#790 := [monotonicity #747 #746]: #789 +#792 := [symm #790]: #791 +#796 := [trans #199 #792]: #795 +#798 := [trans #796 #748]: #797 +#799 := [trans #798 #794]: #183 +#200 := (not #183) +#202 := [not-or-elim #201]: #200 +[unit-resolution #202 #799]: false +unsat +4e5bdb146605ddee0e865e055a144749744ef3dd 381 0 +#2 := false +decl f18 :: (-> S2 S6 S6) +decl f12 :: (-> S3 S6 S6) +decl f17 :: (-> S2 S6 S6) +decl f22 :: S6 +#85 := f22 +decl f4 :: S2 +#8 := f4 +#90 := (f17 f4 f22) +decl f7 :: S3 +#21 := f7 +#91 := (f12 f7 #90) +decl f5 :: S2 +#15 := f5 +#92 := (f18 f5 #91) +#183 := (= f22 #92) +decl f9 :: (-> Int Int S7 S6) +decl f10 :: (-> S1 S5 S7) +decl f13 :: (-> S6 S5) +decl f23 :: S5 +#86 := f23 +decl f1 :: S1 +#4 := f1 +#87 := (f10 f1 f23) +#12 := 4::Int +#18 := 3::Int +#88 := (f9 3::Int 4::Int #87) +#473 := (f13 #88) +decl f6 :: (-> S3 S1 S1) +decl f14 :: (-> S6 S1) +#448 := (f14 #88) +#532 := (f6 f7 #448) +#535 := (f10 #532 #473) +#555 := (f9 3::Int 4::Int #535) +#638 := (f18 f5 #555) +#794 := (= #638 #92) +#787 := (= #92 #638) +#785 := (= #91 #555) +decl f3 :: (-> S2 Int Int) +#398 := (f3 f4 4::Int) +#539 := (f9 3::Int #398 #535) +#781 := (= #539 #555) +#779 := (= #555 #539) +#750 := (= 4::Int #398) +#531 := (= #398 4::Int) +#9 := (:var 0 Int) +#10 := (f3 f4 #9) +#11 := (pattern #10) +#13 := (= #10 4::Int) +#14 := (forall (vars (?v0 Int)) (:pat #11) #13) +#206 := (~ #14 #14) +#204 := (~ #13 #13) +#205 := [refl]: #204 +#207 := [nnf-pos #205]: #206 +#115 := [asserted]: #14 +#208 := [mp~ #115 #207]: #14 +#536 := (not #14) +#537 := (or #536 #531) +#538 := [quant-inst #12]: #537 +#749 := [unit-resolution #538 #208]: #531 +#751 := [symm #749]: #750 +#780 := [monotonicity #751]: #779 +#782 := [symm #780]: #781 +#783 := (= #91 #539) +#499 := (f10 #448 #473) +#500 := (f9 3::Int #398 #499) +#540 := (f12 f7 #500) +#541 := (= #540 #539) +#542 := (= #539 #540) +#32 := (:var 0 S5) +#31 := (:var 1 S1) +#41 := (:var 4 S3) +#43 := (f6 #41 #31) +#44 := (f10 #43 #32) +#30 := (:var 2 Int) +#29 := (:var 3 Int) +#45 := (f9 #29 #30 #44) +#335 := (pattern #45) +#33 := (f10 #31 #32) +#34 := (f9 #29 #30 #33) +#42 := (f12 #41 #34) +#334 := (pattern #42) +#46 := (= #42 #45) +#336 := (forall (vars (?v0 S3) (?v1 Int) (?v2 Int) (?v3 S1) (?v4 S5)) (:pat #334 #335) #46) +#47 := (forall (vars (?v0 S3) (?v1 Int) (?v2 Int) (?v3 S1) (?v4 S5)) #46) +#339 := (iff #47 #336) +#337 := (iff #46 #46) +#338 := [refl]: #337 +#340 := [quant-intro #338]: #339 +#226 := (~ #47 #47) +#224 := (~ #46 #46) +#225 := [refl]: #224 +#227 := [nnf-pos #225]: #226 +#132 := [asserted]: #47 +#228 := [mp~ #132 #227]: #47 +#341 := [mp #228 #340]: #336 +#545 := (not #336) +#546 := (or #545 #542) +#547 := (or #545 #541) +#549 := (iff #547 #546) +#551 := (iff #546 #546) +#552 := [rewrite]: #551 +#543 := (iff #541 #542) +#544 := [rewrite]: #543 +#550 := [monotonicity #544]: #549 +#553 := [trans #550 #552]: #549 +#548 := [quant-inst #21 #18 #398 #448 #473]: #547 +#554 := [mp #548 #553]: #546 +#752 := [unit-resolution #554 #341]: #542 +#778 := [symm #752]: #541 +#776 := (= #91 #540) +#774 := (= #90 #500) +#768 := (= #88 #500) +#761 := (= #500 #88) +#757 := (= #499 #87) +#737 := (= #473 f23) +#474 := (= f23 #473) +#342 := (pattern #34) +#48 := (f13 #34) +#135 := (= #32 #48) +#343 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) (:pat #342) #135) +#138 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #135) +#346 := (iff #138 #343) +#344 := (iff #135 #135) +#345 := [refl]: #344 +#347 := [quant-intro #345]: #346 +#231 := (~ #138 #138) +#229 := (~ #135 #135) +#230 := [refl]: #229 +#232 := [nnf-pos #230]: #231 +#49 := (= #48 #32) +#50 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #49) +#139 := (iff #50 #138) +#136 := (iff #49 #135) +#137 := [rewrite]: #136 +#140 := [quant-intro #137]: #139 +#134 := [asserted]: #50 +#143 := [mp #134 #140]: #138 +#233 := [mp~ #143 #232]: #138 +#348 := [mp #233 #347]: #343 +#477 := (not #343) +#478 := (or #477 #474) +#479 := [quant-inst #18 #12 #4 #86]: #478 +#736 := [unit-resolution #479 #348]: #474 +#741 := [symm #736]: #737 +#755 := (= #448 f1) +#452 := (= f1 #448) +#146 := (= f1 #31) +#51 := (f14 #34) +#142 := (= f1 #51) +#149 := (iff #142 #146) +#349 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) (:pat #342) #149) +#152 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #149) +#352 := (iff #152 #349) +#350 := (iff #149 #149) +#351 := [refl]: #350 +#353 := [quant-intro #351]: #352 +#236 := (~ #152 #152) +#234 := (~ #149 #149) +#235 := [refl]: #234 +#237 := [nnf-pos #235]: #236 +#53 := (= #31 f1) +#52 := (= #51 f1) +#54 := (iff #52 #53) +#55 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #54) +#153 := (iff #55 #152) +#150 := (iff #54 #149) +#147 := (iff #53 #146) +#148 := [rewrite]: #147 +#144 := (iff #52 #142) +#145 := [rewrite]: #144 +#151 := [monotonicity #145 #148]: #150 +#154 := [quant-intro #151]: #153 +#141 := [asserted]: #55 +#157 := [mp #141 #154]: #152 +#238 := [mp~ #157 #237]: #152 +#354 := [mp #238 #353]: #349 +#463 := (not #349) +#464 := (or #463 #452) +#447 := (= f1 f1) +#453 := (iff #452 #447) +#465 := (or #463 #453) +#467 := (iff #465 #464) +#469 := (iff #464 #464) +#470 := [rewrite]: #469 +#461 := (iff #453 #452) +#1 := true +#456 := (iff #452 true) +#459 := (iff #456 #452) +#460 := [rewrite]: #459 +#457 := (iff #453 #456) +#454 := (iff #447 true) +#455 := [rewrite]: #454 +#458 := [monotonicity #455]: #457 +#462 := [trans #458 #460]: #461 +#468 := [monotonicity #462]: #467 +#471 := [trans #468 #470]: #467 +#466 := [quant-inst #18 #12 #4 #86]: #465 +#472 := [mp #466 #471]: #464 +#754 := [unit-resolution #472 #354]: #452 +#756 := [symm #754]: #755 +#758 := [monotonicity #756 #741]: #757 +#762 := [monotonicity #749 #758]: #761 +#769 := [symm #762]: #768 +#772 := (= #90 #88) +#399 := (f9 3::Int #398 #87) +#766 := (= #399 #88) +#763 := (= #88 #399) +#764 := [monotonicity #751]: #763 +#767 := [symm #764]: #766 +#770 := (= #90 #399) +#400 := (f17 f4 #88) +#401 := (= #400 #399) +#402 := (= #399 #400) +#58 := (:var 0 S7) +#57 := (:var 1 Int) +#65 := (:var 3 S2) +#67 := (f3 #65 #57) +#68 := (f9 #30 #67 #58) +#364 := (pattern #68) +#59 := (f9 #30 #57 #58) +#66 := (f17 #65 #59) +#363 := (pattern #66) +#69 := (= #66 #68) +#365 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) (:pat #363 #364) #69) +#70 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) #69) +#368 := (iff #70 #365) +#366 := (iff #69 #69) +#367 := [refl]: #366 +#369 := [quant-intro #367]: #368 +#246 := (~ #70 #70) +#244 := (~ #69 #69) +#245 := [refl]: #244 +#247 := [nnf-pos #245]: #246 +#156 := [asserted]: #70 +#248 := [mp~ #156 #247]: #70 +#370 := [mp #248 #369]: #365 +#405 := (not #365) +#406 := (or #405 #402) +#407 := (or #405 #401) +#409 := (iff #407 #406) +#411 := (iff #406 #406) +#412 := [rewrite]: #411 +#403 := (iff #401 #402) +#404 := [rewrite]: #403 +#410 := [monotonicity #404]: #409 +#413 := [trans #410 #412]: #409 +#408 := [quant-inst #8 #18 #12 #87]: #407 +#414 := [mp #408 #413]: #406 +#753 := [unit-resolution #414 #370]: #402 +#765 := [symm #753]: #401 +#759 := (= #90 #400) +#89 := (= f22 #88) +#190 := (not #89) +#191 := (or #190 #183) +#196 := (not #191) +#93 := (= #92 f22) +#94 := (implies #89 #93) +#95 := (not #94) +#197 := (iff #95 #196) +#194 := (iff #94 #191) +#187 := (implies #89 #183) +#192 := (iff #187 #191) +#193 := [rewrite]: #192 +#188 := (iff #94 #187) +#185 := (iff #93 #183) +#186 := [rewrite]: #185 +#189 := [monotonicity #186]: #188 +#195 := [trans #189 #193]: #194 +#198 := [monotonicity #195]: #197 +#182 := [asserted]: #95 +#201 := [mp #182 #198]: #196 +#199 := [not-or-elim #201]: #89 +#760 := [monotonicity #199]: #759 +#771 := [trans #760 #765]: #770 +#773 := [trans #771 #767]: #772 +#775 := [trans #773 #769]: #774 +#777 := [monotonicity #775]: #776 +#784 := [trans #777 #778]: #783 +#786 := [trans #784 #782]: #785 +#788 := [monotonicity #786]: #787 +#795 := [symm #788]: #794 +#798 := (= f22 #638) +#633 := (f3 f5 3::Int) +#634 := (f9 #633 4::Int #535) +#640 := (= #634 #638) +#72 := (f3 #65 #30) +#73 := (f9 #72 #57 #58) +#372 := (pattern #73) +#71 := (f18 #65 #59) +#371 := (pattern #71) +#74 := (= #71 #73) +#373 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) (:pat #371 #372) #74) +#75 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) #74) +#376 := (iff #75 #373) +#374 := (iff #74 #74) +#375 := [refl]: #374 +#377 := [quant-intro #375]: #376 +#251 := (~ #75 #75) +#249 := (~ #74 #74) +#250 := [refl]: #249 +#252 := [nnf-pos #250]: #251 +#158 := [asserted]: #75 +#253 := [mp~ #158 #252]: #75 +#378 := [mp #253 #377]: #373 +#643 := (not #373) +#644 := (or #643 #640) +#639 := (= #638 #634) +#645 := (or #643 #639) +#647 := (iff #645 #644) +#649 := (iff #644 #644) +#650 := [rewrite]: #649 +#641 := (iff #639 #640) +#642 := [rewrite]: #641 +#648 := [monotonicity #642]: #647 +#651 := [trans #648 #650]: #647 +#646 := [quant-inst #15 #18 #12 #535]: #645 +#652 := [mp #646 #651]: #644 +#748 := [unit-resolution #652 #378]: #640 +#796 := (= f22 #634) +#792 := (= #88 #634) +#790 := (= #634 #88) +#745 := (= #535 #87) +#743 := (= #532 f1) +#586 := (= f1 #532) +#22 := (:var 0 S1) +#23 := (f6 f7 #22) +#24 := (pattern #23) +#118 := (= f1 #23) +#128 := (forall (vars (?v0 S1)) (:pat #24) #118) +#216 := (~ #128 #128) +#214 := (~ #118 #118) +#215 := [refl]: #214 +#217 := [nnf-pos #215]: #216 +#25 := (= #23 f1) +#26 := (iff #25 true) +#27 := (forall (vars (?v0 S1)) (:pat #24) #26) +#129 := (iff #27 #128) +#126 := (iff #26 #118) +#121 := (iff #118 true) +#124 := (iff #121 #118) +#125 := [rewrite]: #124 +#122 := (iff #26 #121) +#119 := (iff #25 #118) +#120 := [rewrite]: #119 +#123 := [monotonicity #120]: #122 +#127 := [trans #123 #125]: #126 +#130 := [quant-intro #127]: #129 +#117 := [asserted]: #27 +#133 := [mp #117 #130]: #128 +#218 := [mp~ #133 #217]: #128 +#635 := (not #128) +#636 := (or #635 #586) +#637 := [quant-inst #448]: #636 +#742 := [unit-resolution #637 #218]: #586 +#744 := [symm #742]: #743 +#746 := [monotonicity #744 #741]: #745 +#735 := (= #633 3::Int) +#16 := (f3 f5 #9) +#17 := (pattern #16) +#19 := (= #16 3::Int) +#20 := (forall (vars (?v0 Int)) (:pat #17) #19) +#211 := (~ #20 #20) +#209 := (~ #19 #19) +#210 := [refl]: #209 +#212 := [nnf-pos #210]: #211 +#116 := [asserted]: #20 +#213 := [mp~ #116 #212]: #20 +#738 := (not #20) +#739 := (or #738 #735) +#740 := [quant-inst #18]: #739 +#747 := [unit-resolution #740 #213]: #735 +#791 := [monotonicity #747 #746]: #790 +#793 := [symm #791]: #792 +#797 := [trans #199 #793]: #796 +#799 := [trans #797 #748]: #798 +#800 := [trans #799 #795]: #183 +#200 := (not #183) +#202 := [not-or-elim #201]: #200 +[unit-resolution #202 #800]: false +unsat +28647514baf56d812f754250e53a79198fbce4ff 371 0 +#2 := false +decl f17 :: (-> S2 S6 S6) +decl f18 :: (-> S2 S6 S6) +decl f12 :: (-> S3 S6 S6) +decl f22 :: S6 +#85 := f22 +decl f7 :: S3 +#21 := f7 +#90 := (f12 f7 f22) +decl f5 :: S2 +#15 := f5 +#91 := (f18 f5 #90) +decl f4 :: S2 +#8 := f4 +#92 := (f17 f4 #91) +#183 := (= f22 #92) +decl f9 :: (-> Int Int S7 S6) +decl f19 :: (-> S6 S7) +decl f10 :: (-> S1 S5 S7) +decl f23 :: S5 +#86 := f23 +decl f6 :: (-> S3 S1 S1) +decl f1 :: S1 +#4 := f1 +#398 := (f6 f7 f1) +#399 := (f10 #398 f23) +#12 := 4::Int +#18 := 3::Int +#400 := (f9 3::Int 4::Int #399) +#507 := (f19 #400) +decl f3 :: (-> S2 Int Int) +#546 := (f3 f5 3::Int) +#566 := (f9 #546 4::Int #507) +#643 := (f17 f4 #566) +#788 := (= #643 #92) +#781 := (= #92 #643) +#766 := (= #91 #566) +#547 := (f9 #546 4::Int #399) +#762 := (= #547 #566) +#760 := (= #566 #547) +#742 := (= #507 #399) +#508 := (= #399 #507) +#58 := (:var 0 S7) +#57 := (:var 1 Int) +#30 := (:var 2 Int) +#59 := (f9 #30 #57 #58) +#379 := (pattern #59) +#76 := (f19 #59) +#160 := (= #58 #76) +#380 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S7)) (:pat #379) #160) +#163 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S7)) #160) +#383 := (iff #163 #380) +#381 := (iff #160 #160) +#382 := [refl]: #381 +#384 := [quant-intro #382]: #383 +#256 := (~ #163 #163) +#254 := (~ #160 #160) +#255 := [refl]: #254 +#257 := [nnf-pos #255]: #256 +#77 := (= #76 #58) +#78 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S7)) #77) +#164 := (iff #78 #163) +#161 := (iff #77 #160) +#162 := [rewrite]: #161 +#165 := [quant-intro #162]: #164 +#159 := [asserted]: #78 +#168 := [mp #159 #165]: #163 +#258 := [mp~ #168 #257]: #163 +#385 := [mp #258 #384]: #380 +#450 := (not #380) +#511 := (or #450 #508) +#512 := [quant-inst #18 #12 #399]: #511 +#741 := [unit-resolution #512 #385]: #508 +#746 := [symm #741]: #742 +#761 := [monotonicity #746]: #760 +#763 := [symm #761]: #762 +#764 := (= #91 #547) +#551 := (f18 f5 #400) +#552 := (= #551 #547) +#553 := (= #547 #551) +#65 := (:var 3 S2) +#72 := (f3 #65 #30) +#73 := (f9 #72 #57 #58) +#372 := (pattern #73) +#71 := (f18 #65 #59) +#371 := (pattern #71) +#74 := (= #71 #73) +#373 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) (:pat #371 #372) #74) +#75 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) #74) +#376 := (iff #75 #373) +#374 := (iff #74 #74) +#375 := [refl]: #374 +#377 := [quant-intro #375]: #376 +#251 := (~ #75 #75) +#249 := (~ #74 #74) +#250 := [refl]: #249 +#252 := [nnf-pos #250]: #251 +#158 := [asserted]: #75 +#253 := [mp~ #158 #252]: #75 +#378 := [mp #253 #377]: #373 +#556 := (not #373) +#557 := (or #556 #553) +#558 := (or #556 #552) +#560 := (iff #558 #557) +#562 := (iff #557 #557) +#563 := [rewrite]: #562 +#554 := (iff #552 #553) +#555 := [rewrite]: #554 +#561 := [monotonicity #555]: #560 +#564 := [trans #561 #563]: #560 +#559 := [quant-inst #15 #18 #12 #399]: #558 +#565 := [mp #559 #564]: #557 +#750 := [unit-resolution #565 #378]: #553 +#759 := [symm #750]: #552 +#757 := (= #91 #551) +#755 := (= #90 #400) +#87 := (f10 f1 f23) +#88 := (f9 3::Int 4::Int #87) +#401 := (f12 f7 #88) +#402 := (= #401 #400) +#403 := (= #400 #401) +#32 := (:var 0 S5) +#31 := (:var 1 S1) +#41 := (:var 4 S3) +#43 := (f6 #41 #31) +#44 := (f10 #43 #32) +#29 := (:var 3 Int) +#45 := (f9 #29 #30 #44) +#335 := (pattern #45) +#33 := (f10 #31 #32) +#34 := (f9 #29 #30 #33) +#42 := (f12 #41 #34) +#334 := (pattern #42) +#46 := (= #42 #45) +#336 := (forall (vars (?v0 S3) (?v1 Int) (?v2 Int) (?v3 S1) (?v4 S5)) (:pat #334 #335) #46) +#47 := (forall (vars (?v0 S3) (?v1 Int) (?v2 Int) (?v3 S1) (?v4 S5)) #46) +#339 := (iff #47 #336) +#337 := (iff #46 #46) +#338 := [refl]: #337 +#340 := [quant-intro #338]: #339 +#226 := (~ #47 #47) +#224 := (~ #46 #46) +#225 := [refl]: #224 +#227 := [nnf-pos #225]: #226 +#132 := [asserted]: #47 +#228 := [mp~ #132 #227]: #47 +#341 := [mp #228 #340]: #336 +#406 := (not #336) +#407 := (or #406 #403) +#408 := (or #406 #402) +#410 := (iff #408 #407) +#412 := (iff #407 #407) +#413 := [rewrite]: #412 +#404 := (iff #402 #403) +#405 := [rewrite]: #404 +#411 := [monotonicity #405]: #410 +#414 := [trans #411 #413]: #410 +#409 := [quant-inst #21 #18 #12 #4 #86]: #408 +#415 := [mp #409 #414]: #407 +#751 := [unit-resolution #415 #341]: #403 +#754 := [symm #751]: #402 +#752 := (= #90 #401) +#89 := (= f22 #88) +#190 := (not #89) +#191 := (or #190 #183) +#196 := (not #191) +#93 := (= #92 f22) +#94 := (implies #89 #93) +#95 := (not #94) +#197 := (iff #95 #196) +#194 := (iff #94 #191) +#187 := (implies #89 #183) +#192 := (iff #187 #191) +#193 := [rewrite]: #192 +#188 := (iff #94 #187) +#185 := (iff #93 #183) +#186 := [rewrite]: #185 +#189 := [monotonicity #186]: #188 +#195 := [trans #189 #193]: #194 +#198 := [monotonicity #195]: #197 +#182 := [asserted]: #95 +#201 := [mp #182 #198]: #196 +#199 := [not-or-elim #201]: #89 +#753 := [monotonicity #199]: #752 +#756 := [trans #753 #754]: #755 +#758 := [monotonicity #756]: #757 +#765 := [trans #758 #759]: #764 +#767 := [trans #765 #763]: #766 +#782 := [monotonicity #767]: #781 +#789 := [symm #782]: #788 +#794 := (= f22 #643) +#638 := (f3 f4 4::Int) +#639 := (f9 #546 #638 #507) +#645 := (= #639 #643) +#67 := (f3 #65 #57) +#68 := (f9 #30 #67 #58) +#364 := (pattern #68) +#66 := (f17 #65 #59) +#363 := (pattern #66) +#69 := (= #66 #68) +#365 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) (:pat #363 #364) #69) +#70 := (forall (vars (?v0 S2) (?v1 Int) (?v2 Int) (?v3 S7)) #69) +#368 := (iff #70 #365) +#366 := (iff #69 #69) +#367 := [refl]: #366 +#369 := [quant-intro #367]: #368 +#246 := (~ #70 #70) +#244 := (~ #69 #69) +#245 := [refl]: #244 +#247 := [nnf-pos #245]: #246 +#156 := [asserted]: #70 +#248 := [mp~ #156 #247]: #70 +#370 := [mp #248 #369]: #365 +#648 := (not #365) +#649 := (or #648 #645) +#644 := (= #643 #639) +#650 := (or #648 #644) +#652 := (iff #650 #649) +#654 := (iff #649 #649) +#655 := [rewrite]: #654 +#646 := (iff #644 #645) +#647 := [rewrite]: #646 +#653 := [monotonicity #647]: #652 +#656 := [trans #653 #655]: #652 +#651 := [quant-inst #8 #546 #12 #507]: #650 +#657 := [mp #651 #656]: #649 +#749 := [unit-resolution #657 #370]: #645 +#792 := (= f22 #639) +#786 := (= #400 #639) +#784 := (= #639 #400) +#740 := (= #638 4::Int) +#9 := (:var 0 Int) +#10 := (f3 f4 #9) +#11 := (pattern #10) +#13 := (= #10 4::Int) +#14 := (forall (vars (?v0 Int)) (:pat #11) #13) +#206 := (~ #14 #14) +#204 := (~ #13 #13) +#205 := [refl]: #204 +#207 := [nnf-pos #205]: #206 +#115 := [asserted]: #14 +#208 := [mp~ #115 #207]: #14 +#743 := (not #14) +#744 := (or #743 #740) +#745 := [quant-inst #12]: #744 +#747 := [unit-resolution #745 #208]: #740 +#637 := (= #546 3::Int) +#16 := (f3 f5 #9) +#17 := (pattern #16) +#19 := (= #16 3::Int) +#20 := (forall (vars (?v0 Int)) (:pat #17) #19) +#211 := (~ #20 #20) +#209 := (~ #19 #19) +#210 := [refl]: #209 +#212 := [nnf-pos #210]: #211 +#116 := [asserted]: #20 +#213 := [mp~ #116 #212]: #20 +#640 := (not #20) +#641 := (or #640 #637) +#642 := [quant-inst #18]: #641 +#748 := [unit-resolution #642 #213]: #637 +#785 := [monotonicity #748 #747 #746]: #784 +#787 := [symm #785]: #786 +#790 := (= f22 #400) +#779 := (= #88 #400) +#777 := (= #87 #399) +#509 := (= f1 #398) +decl f14 :: (-> S6 S1) +#449 := (f14 #88) +#542 := (f6 f7 #449) +#774 := (= #542 #398) +#770 := (= #398 #542) +#453 := (= f1 #449) +#342 := (pattern #34) +#146 := (= f1 #31) +#51 := (f14 #34) +#142 := (= f1 #51) +#149 := (iff #142 #146) +#349 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) (:pat #342) #149) +#152 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #149) +#352 := (iff #152 #349) +#350 := (iff #149 #149) +#351 := [refl]: #350 +#353 := [quant-intro #351]: #352 +#236 := (~ #152 #152) +#234 := (~ #149 #149) +#235 := [refl]: #234 +#237 := [nnf-pos #235]: #236 +#53 := (= #31 f1) +#52 := (= #51 f1) +#54 := (iff #52 #53) +#55 := (forall (vars (?v0 Int) (?v1 Int) (?v2 S1) (?v3 S5)) #54) +#153 := (iff #55 #152) +#150 := (iff #54 #149) +#147 := (iff #53 #146) +#148 := [rewrite]: #147 +#144 := (iff #52 #142) +#145 := [rewrite]: #144 +#151 := [monotonicity #145 #148]: #150 +#154 := [quant-intro #151]: #153 +#141 := [asserted]: #55 +#157 := [mp #141 #154]: #152 +#238 := [mp~ #157 #237]: #152 +#354 := [mp #238 #353]: #349 +#464 := (not #349) +#465 := (or #464 #453) +#448 := (= f1 f1) +#454 := (iff #453 #448) +#466 := (or #464 #454) +#468 := (iff #466 #465) +#470 := (iff #465 #465) +#471 := [rewrite]: #470 +#462 := (iff #454 #453) +#1 := true +#457 := (iff #453 true) +#460 := (iff #457 #453) +#461 := [rewrite]: #460 +#458 := (iff #454 #457) +#455 := (iff #448 true) +#456 := [rewrite]: #455 +#459 := [monotonicity #456]: #458 +#463 := [trans #459 #461]: #462 +#469 := [monotonicity #463]: #468 +#472 := [trans #469 #471]: #468 +#467 := [quant-inst #18 #12 #4 #86]: #466 +#473 := [mp #467 #472]: #465 +#769 := [unit-resolution #473 #354]: #453 +#771 := [monotonicity #769]: #770 +#775 := [symm #771]: #774 +#543 := (= f1 #542) +#22 := (:var 0 S1) +#23 := (f6 f7 #22) +#24 := (pattern #23) +#118 := (= f1 #23) +#128 := (forall (vars (?v0 S1)) (:pat #24) #118) +#216 := (~ #128 #128) +#214 := (~ #118 #118) +#215 := [refl]: #214 +#217 := [nnf-pos #215]: #216 +#25 := (= #23 f1) +#26 := (iff #25 true) +#27 := (forall (vars (?v0 S1)) (:pat #24) #26) +#129 := (iff #27 #128) +#126 := (iff #26 #118) +#121 := (iff #118 true) +#124 := (iff #121 #118) +#125 := [rewrite]: #124 +#122 := (iff #26 #121) +#119 := (iff #25 #118) +#120 := [rewrite]: #119 +#123 := [monotonicity #120]: #122 +#127 := [trans #123 #125]: #126 +#130 := [quant-intro #127]: #129 +#117 := [asserted]: #27 +#133 := [mp #117 #130]: #128 +#218 := [mp~ #133 #217]: #128 +#548 := (not #128) +#549 := (or #548 #543) +#550 := [quant-inst #449]: #549 +#768 := [unit-resolution #550 #218]: #543 +#776 := [trans #768 #775]: #509 +#778 := [monotonicity #776]: #777 +#780 := [monotonicity #778]: #779 +#791 := [trans #199 #780]: #790 +#793 := [trans #791 #787]: #792 +#795 := [trans #793 #749]: #794 +#796 := [trans #795 #789]: #183 +#200 := (not #183) +#202 := [not-or-elim #201]: #200 +[unit-resolution #202 #796]: false +unsat +32bed77391f2e5bd3429d275156eab0436b0859c 18 0 +#2 := false +decl f3 :: S2 +#8 := f3 +#48 := (= f3 f3) +#49 := (not #48) +#155 := (iff #49 false) +#1 := true +#150 := (not true) +#153 := (iff #150 false) +#154 := [rewrite]: #153 +#151 := (iff #49 #150) +#147 := (iff #48 true) +#149 := [rewrite]: #147 +#152 := [monotonicity #149]: #151 +#156 := [trans #152 #154]: #155 +#146 := [asserted]: #49 +[mp #146 #156]: false +unsat +3c1ec477ccf1b2909c916c4e5bde25988097c01d 18 0 +#2 := false +decl f5 :: S2 +#12 := f5 +#48 := (= f5 f5) +#49 := (not #48) +#155 := (iff #49 false) +#1 := true +#150 := (not true) +#153 := (iff #150 false) +#154 := [rewrite]: #153 +#151 := (iff #49 #150) +#147 := (iff #48 true) +#149 := [rewrite]: #147 +#152 := [monotonicity #149]: #151 +#156 := [trans #152 #154]: #155 +#146 := [asserted]: #49 +[mp #146 #156]: false +unsat +fc393122d71ac475e5b68121edf0d1d7e9737e48 277 0 +#2 := false +#13 := 2::Int +#9 := 1::Int +#330 := (= 1::Int 2::Int) +#335 := (iff #330 false) +#336 := [rewrite]: #335 +decl f8 :: (-> S2 Int) +decl f4 :: (-> Int S2) +#14 := (f4 2::Int) +#282 := (f8 #14) +#290 := (= #282 2::Int) +decl f9 :: (-> Int S3 S1) +decl f10 :: S3 +#30 := f10 +#284 := (f9 2::Int f10) +decl f1 :: S1 +#4 := f1 +#285 := (= f1 #284) +#286 := (not #285) +#446 := [hypothesis]: #286 +#29 := (:var 0 Int) +#31 := (f9 #29 f10) +#237 := (pattern #31) +#17 := 3::Int +#35 := (= #29 3::Int) +#34 := (= #29 2::Int) +#33 := (= #29 1::Int) +#109 := (or #33 #34 #35) +#75 := (= f1 #31) +#114 := (iff #75 #109) +#238 := (forall (vars (?v0 Int)) (:pat #237) #114) +#117 := (forall (vars (?v0 Int)) #114) +#241 := (iff #117 #238) +#239 := (iff #114 #114) +#240 := [refl]: #239 +#242 := [quant-intro #240]: #241 +#160 := (~ #117 #117) +#158 := (~ #114 #114) +#159 := [refl]: #158 +#161 := [nnf-pos #159]: #160 +#36 := (or #34 #35) +#37 := (or #33 #36) +#32 := (= #31 f1) +#38 := (iff #32 #37) +#39 := (forall (vars (?v0 Int)) #38) +#120 := (iff #39 #117) +#84 := (= 3::Int #29) +#81 := (= 2::Int #29) +#87 := (or #81 #84) +#78 := (= 1::Int #29) +#90 := (or #78 #87) +#93 := (iff #75 #90) +#96 := (forall (vars (?v0 Int)) #93) +#118 := (iff #96 #117) +#115 := (iff #93 #114) +#112 := (iff #90 #109) +#110 := (iff #37 #109) +#111 := [rewrite]: #110 +#107 := (iff #90 #37) +#105 := (iff #87 #36) +#101 := (iff #84 #35) +#102 := [rewrite]: #101 +#99 := (iff #81 #34) +#100 := [rewrite]: #99 +#106 := [monotonicity #100 #102]: #105 +#103 := (iff #78 #33) +#104 := [rewrite]: #103 +#108 := [monotonicity #104 #106]: #107 +#113 := [trans #108 #111]: #112 +#116 := [monotonicity #113]: #115 +#119 := [quant-intro #116]: #118 +#97 := (iff #39 #96) +#94 := (iff #38 #93) +#91 := (iff #37 #90) +#88 := (iff #36 #87) +#85 := (iff #35 #84) +#86 := [rewrite]: #85 +#82 := (iff #34 #81) +#83 := [rewrite]: #82 +#89 := [monotonicity #83 #86]: #88 +#79 := (iff #33 #78) +#80 := [rewrite]: #79 +#92 := [monotonicity #80 #89]: #91 +#76 := (iff #32 #75) +#77 := [rewrite]: #76 +#95 := [monotonicity #77 #92]: #94 +#98 := [quant-intro #95]: #97 +#121 := [trans #98 #119]: #120 +#74 := [asserted]: #39 +#122 := [mp #74 #121]: #117 +#162 := [mp~ #122 #161]: #117 +#243 := [mp #162 #242]: #238 +#353 := (not #238) +#437 := (or #353 #285) +#411 := (= 2::Int 3::Int) +#414 := (= 2::Int 2::Int) +#410 := (= 2::Int 1::Int) +#415 := (or #410 #414 #411) +#416 := (iff #285 #415) +#438 := (or #353 #416) +#440 := (iff #438 #437) +#442 := (iff #437 #437) +#443 := [rewrite]: #442 +#435 := (iff #416 #285) +#1 := true +#430 := (iff #285 true) +#433 := (iff #430 #285) +#434 := [rewrite]: #433 +#431 := (iff #416 #430) +#428 := (iff #415 true) +#423 := (or false true false) +#426 := (iff #423 true) +#427 := [rewrite]: #426 +#424 := (iff #415 #423) +#421 := (iff #411 false) +#422 := [rewrite]: #421 +#419 := (iff #414 true) +#420 := [rewrite]: #419 +#417 := (iff #410 false) +#418 := [rewrite]: #417 +#425 := [monotonicity #418 #420 #422]: #424 +#429 := [trans #425 #427]: #428 +#432 := [monotonicity #429]: #431 +#436 := [trans #432 #434]: #435 +#441 := [monotonicity #436]: #440 +#444 := [trans #441 #443]: #440 +#439 := [quant-inst #13]: #438 +#445 := [mp #439 #444]: #437 +#447 := [unit-resolution #445 #243 #446]: false +#448 := [lemma #447]: #285 +#291 := (or #286 #290) +#43 := (f4 #29) +#251 := (pattern #43) +#44 := (f8 #43) +#131 := (= #29 #44) +#138 := (not #75) +#139 := (or #138 #131) +#252 := (forall (vars (?v0 Int)) (:pat #237 #251) #139) +#144 := (forall (vars (?v0 Int)) #139) +#255 := (iff #144 #252) +#253 := (iff #139 #139) +#254 := [refl]: #253 +#256 := [quant-intro #254]: #255 +#170 := (~ #144 #144) +#168 := (~ #139 #139) +#169 := [refl]: #168 +#171 := [nnf-pos #169]: #170 +#45 := (= #44 #29) +#46 := (implies #32 #45) +#47 := (forall (vars (?v0 Int)) #46) +#145 := (iff #47 #144) +#142 := (iff #46 #139) +#135 := (implies #75 #131) +#140 := (iff #135 #139) +#141 := [rewrite]: #140 +#136 := (iff #46 #135) +#133 := (iff #45 #131) +#134 := [rewrite]: #133 +#137 := [monotonicity #77 #134]: #136 +#143 := [trans #137 #141]: #142 +#146 := [quant-intro #143]: #145 +#130 := [asserted]: #47 +#149 := [mp #130 #146]: #144 +#172 := [mp~ #149 #171]: #144 +#257 := [mp #172 #256]: #252 +#270 := (not #252) +#294 := (or #270 #286 #290) +#283 := (= 2::Int #282) +#287 := (or #286 #283) +#295 := (or #270 #287) +#302 := (iff #295 #294) +#297 := (or #270 #291) +#300 := (iff #297 #294) +#301 := [rewrite]: #300 +#298 := (iff #295 #297) +#292 := (iff #287 #291) +#288 := (iff #283 #290) +#289 := [rewrite]: #288 +#293 := [monotonicity #289]: #292 +#299 := [monotonicity #293]: #298 +#303 := [trans #299 #301]: #302 +#296 := [quant-inst #13]: #295 +#304 := [mp #296 #303]: #294 +#449 := [unit-resolution #304 #257]: #291 +#450 := [unit-resolution #449 #448]: #290 +#467 := (= 1::Int #282) +#465 := (= #282 1::Int) +#10 := (f4 1::Int) +#258 := (f8 #10) +#266 := (= #258 1::Int) +#260 := (f9 1::Int f10) +#261 := (= f1 #260) +#262 := (not #261) +#363 := [hypothesis]: #262 +#354 := (or #353 #261) +#329 := (= 1::Int 3::Int) +#328 := (= 1::Int 1::Int) +#331 := (or #328 #330 #329) +#332 := (iff #261 #331) +#355 := (or #353 #332) +#357 := (iff #355 #354) +#359 := (iff #354 #354) +#360 := [rewrite]: #359 +#351 := (iff #332 #261) +#346 := (iff #261 true) +#349 := (iff #346 #261) +#350 := [rewrite]: #349 +#347 := (iff #332 #346) +#344 := (iff #331 true) +#339 := (or true false false) +#342 := (iff #339 true) +#343 := [rewrite]: #342 +#340 := (iff #331 #339) +#337 := (iff #329 false) +#338 := [rewrite]: #337 +#333 := (iff #328 true) +#334 := [rewrite]: #333 +#341 := [monotonicity #334 #336 #338]: #340 +#345 := [trans #341 #343]: #344 +#348 := [monotonicity #345]: #347 +#352 := [trans #348 #350]: #351 +#358 := [monotonicity #352]: #357 +#361 := [trans #358 #360]: #357 +#356 := [quant-inst #9]: #355 +#362 := [mp #356 #361]: #354 +#364 := [unit-resolution #362 #243 #363]: false +#365 := [lemma #364]: #261 +#267 := (or #262 #266) +#271 := (or #270 #262 #266) +#259 := (= 1::Int #258) +#263 := (or #262 #259) +#272 := (or #270 #263) +#279 := (iff #272 #271) +#274 := (or #270 #267) +#277 := (iff #274 #271) +#278 := [rewrite]: #277 +#275 := (iff #272 #274) +#268 := (iff #263 #267) +#264 := (iff #259 #266) +#265 := [rewrite]: #264 +#269 := [monotonicity #265]: #268 +#276 := [monotonicity #269]: #275 +#280 := [trans #276 #278]: #279 +#273 := [quant-inst #9]: #272 +#281 := [mp #273 #280]: #271 +#451 := [unit-resolution #281 #257]: #267 +#452 := [unit-resolution #451 #365]: #266 +#463 := (= #282 #258) +#461 := (= #14 #10) +decl f3 :: S2 +#8 := f3 +#11 := (= f3 #10) +#70 := [asserted]: #11 +#459 := (= #14 f3) +decl f5 :: S2 +#12 := f5 +#457 := (= f5 f3) +#48 := (= f3 f5) +#49 := (not #48) +#50 := (not #49) +#148 := (iff #50 #48) +#150 := [rewrite]: #148 +#147 := [asserted]: #50 +#153 := [mp #147 #150]: #48 +#458 := [symm #153]: #457 +#455 := (= #14 f5) +#15 := (= f5 #14) +#71 := [asserted]: #15 +#456 := [symm #71]: #455 +#460 := [trans #456 #458]: #459 +#462 := [trans #460 #70]: #461 +#464 := [monotonicity #462]: #463 +#466 := [trans #464 #452]: #465 +#468 := [symm #466]: #467 +#469 := [trans #468 #450]: #330 +[mp #469 #336]: false +unsat +3eced97a83aec74943eda175c04a4dc551f95874 277 0 +#2 := false +decl f7 :: (-> S2 S2 S2) +decl f3 :: S2 +#8 := f3 +#48 := (f7 f3 f3) +decl f5 :: S2 +#12 := f5 +#148 := (= f5 #48) +decl f4 :: (-> Int S2) +#9 := 1::Int +#10 := (f4 1::Int) +#265 := (f7 #10 #10) +#503 := (= #265 #48) +#499 := (= #48 #265) +#11 := (= f3 #10) +#70 := [asserted]: #11 +#500 := [monotonicity #70 #70]: #499 +#504 := [symm #500]: #503 +#507 := (= f5 #265) +decl f8 :: (-> S2 Int) +#262 := (f8 #10) +#13 := 2::Int +#267 := (* 2::Int #262) +#270 := (f4 #267) +#501 := (= #270 #265) +#273 := (= #265 #270) +#21 := (:var 0 S2) +#20 := (:var 1 S2) +#22 := (f7 #20 #21) +#234 := (pattern #22) +#24 := (f8 #21) +#23 := (f8 #20) +#25 := (+ #23 #24) +#26 := (f4 #25) +#27 := (= #22 #26) +#235 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #234) #27) +#28 := (forall (vars (?v0 S2) (?v1 S2)) #27) +#238 := (iff #28 #235) +#236 := (iff #27 #27) +#237 := [refl]: #236 +#239 := [quant-intro #237]: #238 +#159 := (~ #28 #28) +#156 := (~ #27 #27) +#158 := [refl]: #156 +#160 := [nnf-pos #158]: #159 +#73 := [asserted]: #28 +#161 := [mp~ #73 #160]: #28 +#240 := [mp #161 #239]: #235 +#276 := (not #235) +#277 := (or #276 #273) +#263 := (+ #262 #262) +#264 := (f4 #263) +#266 := (= #265 #264) +#278 := (or #276 #266) +#280 := (iff #278 #277) +#282 := (iff #277 #277) +#283 := [rewrite]: #282 +#274 := (iff #266 #273) +#271 := (= #264 #270) +#268 := (= #263 #267) +#269 := [rewrite]: #268 +#272 := [monotonicity #269]: #271 +#275 := [monotonicity #272]: #274 +#281 := [monotonicity #275]: #280 +#284 := [trans #281 #283]: #280 +#279 := [quant-inst #10 #10]: #278 +#285 := [mp #279 #284]: #277 +#484 := [unit-resolution #285 #240]: #273 +#502 := [symm #484]: #501 +#505 := (= f5 #270) +#14 := (f4 2::Int) +#497 := (= #14 #270) +#495 := (= 2::Int #267) +#493 := (= #267 2::Int) +#309 := (<= #262 1::Int) +#293 := (= #262 1::Int) +decl f9 :: (-> Int S3 S1) +decl f10 :: S3 +#30 := f10 +#287 := (f9 1::Int f10) +decl f1 :: S1 +#4 := f1 +#288 := (= f1 #287) +#289 := (not #288) +#481 := [hypothesis]: #289 +#29 := (:var 0 Int) +#31 := (f9 #29 f10) +#241 := (pattern #31) +#17 := 3::Int +#35 := (= #29 3::Int) +#34 := (= #29 2::Int) +#33 := (= #29 1::Int) +#109 := (or #33 #34 #35) +#75 := (= f1 #31) +#114 := (iff #75 #109) +#242 := (forall (vars (?v0 Int)) (:pat #241) #114) +#117 := (forall (vars (?v0 Int)) #114) +#245 := (iff #117 #242) +#243 := (iff #114 #114) +#244 := [refl]: #243 +#246 := [quant-intro #244]: #245 +#164 := (~ #117 #117) +#162 := (~ #114 #114) +#163 := [refl]: #162 +#165 := [nnf-pos #163]: #164 +#36 := (or #34 #35) +#37 := (or #33 #36) +#32 := (= #31 f1) +#38 := (iff #32 #37) +#39 := (forall (vars (?v0 Int)) #38) +#120 := (iff #39 #117) +#84 := (= 3::Int #29) +#81 := (= 2::Int #29) +#87 := (or #81 #84) +#78 := (= 1::Int #29) +#90 := (or #78 #87) +#93 := (iff #75 #90) +#96 := (forall (vars (?v0 Int)) #93) +#118 := (iff #96 #117) +#115 := (iff #93 #114) +#112 := (iff #90 #109) +#110 := (iff #37 #109) +#111 := [rewrite]: #110 +#107 := (iff #90 #37) +#105 := (iff #87 #36) +#101 := (iff #84 #35) +#102 := [rewrite]: #101 +#99 := (iff #81 #34) +#100 := [rewrite]: #99 +#106 := [monotonicity #100 #102]: #105 +#103 := (iff #78 #33) +#104 := [rewrite]: #103 +#108 := [monotonicity #104 #106]: #107 +#113 := [trans #108 #111]: #112 +#116 := [monotonicity #113]: #115 +#119 := [quant-intro #116]: #118 +#97 := (iff #39 #96) +#94 := (iff #38 #93) +#91 := (iff #37 #90) +#88 := (iff #36 #87) +#85 := (iff #35 #84) +#86 := [rewrite]: #85 +#82 := (iff #34 #81) +#83 := [rewrite]: #82 +#89 := [monotonicity #83 #86]: #88 +#79 := (iff #33 #78) +#80 := [rewrite]: #79 +#92 := [monotonicity #80 #89]: #91 +#76 := (iff #32 #75) +#77 := [rewrite]: #76 +#95 := [monotonicity #77 #92]: #94 +#98 := [quant-intro #95]: #97 +#121 := [trans #98 #119]: #120 +#74 := [asserted]: #39 +#122 := [mp #74 #121]: #117 +#166 := [mp~ #122 #165]: #117 +#247 := [mp #166 #246]: #242 +#401 := (not #242) +#472 := (or #401 #288) +#442 := (= 1::Int 3::Int) +#449 := (= 1::Int 2::Int) +#441 := (= 1::Int 1::Int) +#450 := (or #441 #449 #442) +#451 := (iff #288 #450) +#473 := (or #401 #451) +#475 := (iff #473 #472) +#477 := (iff #472 #472) +#478 := [rewrite]: #477 +#470 := (iff #451 #288) +#1 := true +#465 := (iff #288 true) +#468 := (iff #465 #288) +#469 := [rewrite]: #468 +#466 := (iff #451 #465) +#463 := (iff #450 true) +#458 := (or true false false) +#461 := (iff #458 true) +#462 := [rewrite]: #461 +#459 := (iff #450 #458) +#456 := (iff #442 false) +#457 := [rewrite]: #456 +#454 := (iff #449 false) +#455 := [rewrite]: #454 +#452 := (iff #441 true) +#453 := [rewrite]: #452 +#460 := [monotonicity #453 #455 #457]: #459 +#464 := [trans #460 #462]: #463 +#467 := [monotonicity #464]: #466 +#471 := [trans #467 #469]: #470 +#476 := [monotonicity #471]: #475 +#479 := [trans #476 #478]: #475 +#474 := [quant-inst #9]: #473 +#480 := [mp #474 #479]: #472 +#482 := [unit-resolution #480 #247 #481]: false +#483 := [lemma #482]: #288 +#294 := (or #289 #293) +#43 := (f4 #29) +#255 := (pattern #43) +#44 := (f8 #43) +#131 := (= #29 #44) +#138 := (not #75) +#139 := (or #138 #131) +#256 := (forall (vars (?v0 Int)) (:pat #241 #255) #139) +#144 := (forall (vars (?v0 Int)) #139) +#259 := (iff #144 #256) +#257 := (iff #139 #139) +#258 := [refl]: #257 +#260 := [quant-intro #258]: #259 +#174 := (~ #144 #144) +#172 := (~ #139 #139) +#173 := [refl]: #172 +#175 := [nnf-pos #173]: #174 +#45 := (= #44 #29) +#46 := (implies #32 #45) +#47 := (forall (vars (?v0 Int)) #46) +#145 := (iff #47 #144) +#142 := (iff #46 #139) +#135 := (implies #75 #131) +#140 := (iff #135 #139) +#141 := [rewrite]: #140 +#136 := (iff #46 #135) +#133 := (iff #45 #131) +#134 := [rewrite]: #133 +#137 := [monotonicity #77 #134]: #136 +#143 := [trans #137 #141]: #142 +#146 := [quant-intro #143]: #145 +#130 := [asserted]: #47 +#149 := [mp #130 #146]: #144 +#176 := [mp~ #149 #175]: #144 +#261 := [mp #176 #260]: #256 +#297 := (not #256) +#298 := (or #297 #289 #293) +#286 := (= 1::Int #262) +#290 := (or #289 #286) +#299 := (or #297 #290) +#306 := (iff #299 #298) +#301 := (or #297 #294) +#304 := (iff #301 #298) +#305 := [rewrite]: #304 +#302 := (iff #299 #301) +#295 := (iff #290 #294) +#291 := (iff #286 #293) +#292 := [rewrite]: #291 +#296 := [monotonicity #292]: #295 +#303 := [monotonicity #296]: #302 +#307 := [trans #303 #305]: #306 +#300 := [quant-inst #9]: #299 +#308 := [mp #300 #307]: #298 +#485 := [unit-resolution #308 #261]: #294 +#486 := [unit-resolution #485 #483]: #293 +#415 := (not #293) +#487 := (or #415 #309) +#488 := [th-lemma arith triangle-eq]: #487 +#489 := [unit-resolution #488 #486]: #309 +#310 := (>= #262 1::Int) +#490 := (or #415 #310) +#491 := [th-lemma arith triangle-eq]: #490 +#492 := [unit-resolution #491 #486]: #310 +#494 := [th-lemma arith eq-propagate -2 -2 #492 #489]: #493 +#496 := [symm #494]: #495 +#498 := [monotonicity #496]: #497 +#15 := (= f5 #14) +#71 := [asserted]: #15 +#506 := [trans #71 #498]: #505 +#508 := [trans #506 #502]: #507 +#509 := [trans #508 #504]: #148 +#152 := (not #148) +#49 := (= #48 f5) +#50 := (not #49) +#153 := (iff #50 #152) +#150 := (iff #49 #148) +#151 := [rewrite]: #150 +#154 := [monotonicity #151]: #153 +#147 := [asserted]: #50 +#157 := [mp #147 #154]: #152 +[unit-resolution #157 #509]: false +unsat +430c03c5c26128e8a75bc59c68cc6da929b262eb 435 0 +#2 := false +decl f7 :: (-> S2 S2 S2) +decl f5 :: S2 +#12 := f5 +decl f3 :: S2 +#8 := f3 +#48 := (f7 f3 f5) +decl f6 :: S2 +#16 := f6 +#148 := (= f6 #48) +decl f4 :: (-> Int S2) +#13 := 2::Int +#14 := (f4 2::Int) +#9 := 1::Int +#10 := (f4 1::Int) +#266 := (f7 #10 #14) +#584 := (= #266 #48) +#618 := (= #48 #266) +#15 := (= f5 #14) +#71 := [asserted]: #15 +#11 := (= f3 #10) +#70 := [asserted]: #11 +#619 := [monotonicity #70 #71]: #618 +#587 := [symm #619]: #584 +#590 := (= f6 #266) +decl f8 :: (-> S2 Int) +#263 := (f8 #10) +#262 := (f8 #14) +#268 := (+ #262 #263) +#271 := (f4 #268) +#585 := (= #271 #266) +#274 := (= #266 #271) +#21 := (:var 0 S2) +#20 := (:var 1 S2) +#22 := (f7 #20 #21) +#234 := (pattern #22) +#24 := (f8 #21) +#23 := (f8 #20) +#25 := (+ #23 #24) +#26 := (f4 #25) +#27 := (= #22 #26) +#235 := (forall (vars (?v0 S2) (?v1 S2)) (:pat #234) #27) +#28 := (forall (vars (?v0 S2) (?v1 S2)) #27) +#238 := (iff #28 #235) +#236 := (iff #27 #27) +#237 := [refl]: #236 +#239 := [quant-intro #237]: #238 +#159 := (~ #28 #28) +#156 := (~ #27 #27) +#158 := [refl]: #156 +#160 := [nnf-pos #158]: #159 +#73 := [asserted]: #28 +#161 := [mp~ #73 #160]: #28 +#240 := [mp #161 #239]: #235 +#277 := (not #235) +#278 := (or #277 #274) +#264 := (+ #263 #262) +#265 := (f4 #264) +#267 := (= #266 #265) +#279 := (or #277 #267) +#281 := (iff #279 #278) +#283 := (iff #278 #278) +#284 := [rewrite]: #283 +#275 := (iff #267 #274) +#272 := (= #265 #271) +#269 := (= #264 #268) +#270 := [rewrite]: #269 +#273 := [monotonicity #270]: #272 +#276 := [monotonicity #273]: #275 +#282 := [monotonicity #276]: #281 +#285 := [trans #282 #284]: #281 +#280 := [quant-inst #10 #14]: #279 +#286 := [mp #280 #285]: #278 +#599 := [unit-resolution #286 #240]: #274 +#586 := [symm #599]: #585 +#588 := (= f6 #271) +#17 := 3::Int +#18 := (f4 3::Int) +#616 := (= #18 #271) +#614 := (= 3::Int #268) +#504 := (= #268 3::Int) +#310 := (<= #263 1::Int) +#294 := (= #263 1::Int) +decl f9 :: (-> Int S3 S1) +decl f10 :: S3 +#30 := f10 +#288 := (f9 1::Int f10) +decl f1 :: S1 +#4 := f1 +#289 := (= f1 #288) +#290 := (not #289) +#533 := [hypothesis]: #290 +#29 := (:var 0 Int) +#31 := (f9 #29 f10) +#241 := (pattern #31) +#35 := (= #29 3::Int) +#34 := (= #29 2::Int) +#33 := (= #29 1::Int) +#109 := (or #33 #34 #35) +#75 := (= f1 #31) +#114 := (iff #75 #109) +#242 := (forall (vars (?v0 Int)) (:pat #241) #114) +#117 := (forall (vars (?v0 Int)) #114) +#245 := (iff #117 #242) +#243 := (iff #114 #114) +#244 := [refl]: #243 +#246 := [quant-intro #244]: #245 +#164 := (~ #117 #117) +#162 := (~ #114 #114) +#163 := [refl]: #162 +#165 := [nnf-pos #163]: #164 +#36 := (or #34 #35) +#37 := (or #33 #36) +#32 := (= #31 f1) +#38 := (iff #32 #37) +#39 := (forall (vars (?v0 Int)) #38) +#120 := (iff #39 #117) +#84 := (= 3::Int #29) +#81 := (= 2::Int #29) +#87 := (or #81 #84) +#78 := (= 1::Int #29) +#90 := (or #78 #87) +#93 := (iff #75 #90) +#96 := (forall (vars (?v0 Int)) #93) +#118 := (iff #96 #117) +#115 := (iff #93 #114) +#112 := (iff #90 #109) +#110 := (iff #37 #109) +#111 := [rewrite]: #110 +#107 := (iff #90 #37) +#105 := (iff #87 #36) +#101 := (iff #84 #35) +#102 := [rewrite]: #101 +#99 := (iff #81 #34) +#100 := [rewrite]: #99 +#106 := [monotonicity #100 #102]: #105 +#103 := (iff #78 #33) +#104 := [rewrite]: #103 +#108 := [monotonicity #104 #106]: #107 +#113 := [trans #108 #111]: #112 +#116 := [monotonicity #113]: #115 +#119 := [quant-intro #116]: #118 +#97 := (iff #39 #96) +#94 := (iff #38 #93) +#91 := (iff #37 #90) +#88 := (iff #36 #87) +#85 := (iff #35 #84) +#86 := [rewrite]: #85 +#82 := (iff #34 #81) +#83 := [rewrite]: #82 +#89 := [monotonicity #83 #86]: #88 +#79 := (iff #33 #78) +#80 := [rewrite]: #79 +#92 := [monotonicity #80 #89]: #91 +#76 := (iff #32 #75) +#77 := [rewrite]: #76 +#95 := [monotonicity #77 #92]: #94 +#98 := [quant-intro #95]: #97 +#121 := [trans #98 #119]: #120 +#74 := [asserted]: #39 +#122 := [mp #74 #121]: #117 +#166 := [mp~ #122 #165]: #117 +#247 := [mp #166 #246]: #242 +#408 := (not #242) +#524 := (or #408 #289) +#536 := (= 1::Int 3::Int) +#537 := (= 1::Int 2::Int) +#535 := (= 1::Int 1::Int) +#538 := (or #535 #537 #536) +#539 := (iff #289 #538) +#525 := (or #408 #539) +#527 := (iff #525 #524) +#529 := (iff #524 #524) +#530 := [rewrite]: #529 +#520 := (iff #539 #289) +#1 := true +#553 := (iff #289 true) +#521 := (iff #553 #289) +#522 := [rewrite]: #521 +#554 := (iff #539 #553) +#551 := (iff #538 true) +#546 := (or true false false) +#549 := (iff #546 true) +#550 := [rewrite]: #549 +#547 := (iff #538 #546) +#544 := (iff #536 false) +#545 := [rewrite]: #544 +#542 := (iff #537 false) +#543 := [rewrite]: #542 +#540 := (iff #535 true) +#541 := [rewrite]: #540 +#548 := [monotonicity #541 #543 #545]: #547 +#552 := [trans #548 #550]: #551 +#555 := [monotonicity #552]: #554 +#523 := [trans #555 #522]: #520 +#528 := [monotonicity #523]: #527 +#531 := [trans #528 #530]: #527 +#526 := [quant-inst #9]: #525 +#532 := [mp #526 #531]: #524 +#534 := [unit-resolution #532 #247 #533]: false +#583 := [lemma #534]: #289 +#295 := (or #290 #294) +#43 := (f4 #29) +#255 := (pattern #43) +#44 := (f8 #43) +#131 := (= #29 #44) +#138 := (not #75) +#139 := (or #138 #131) +#256 := (forall (vars (?v0 Int)) (:pat #241 #255) #139) +#144 := (forall (vars (?v0 Int)) #139) +#259 := (iff #144 #256) +#257 := (iff #139 #139) +#258 := [refl]: #257 +#260 := [quant-intro #258]: #259 +#174 := (~ #144 #144) +#172 := (~ #139 #139) +#173 := [refl]: #172 +#175 := [nnf-pos #173]: #174 +#45 := (= #44 #29) +#46 := (implies #32 #45) +#47 := (forall (vars (?v0 Int)) #46) +#145 := (iff #47 #144) +#142 := (iff #46 #139) +#135 := (implies #75 #131) +#140 := (iff #135 #139) +#141 := [rewrite]: #140 +#136 := (iff #46 #135) +#133 := (iff #45 #131) +#134 := [rewrite]: #133 +#137 := [monotonicity #77 #134]: #136 +#143 := [trans #137 #141]: #142 +#146 := [quant-intro #143]: #145 +#130 := [asserted]: #47 +#149 := [mp #130 #146]: #144 +#176 := [mp~ #149 #175]: #144 +#261 := [mp #176 #260]: #256 +#298 := (not #256) +#299 := (or #298 #290 #294) +#287 := (= 1::Int #263) +#291 := (or #290 #287) +#300 := (or #298 #291) +#307 := (iff #300 #299) +#302 := (or #298 #295) +#305 := (iff #302 #299) +#306 := [rewrite]: #305 +#303 := (iff #300 #302) +#296 := (iff #291 #295) +#292 := (iff #287 #294) +#293 := [rewrite]: #292 +#297 := [monotonicity #293]: #296 +#304 := [monotonicity #297]: #303 +#308 := [trans #304 #306]: #307 +#301 := [quant-inst #9]: #300 +#309 := [mp #301 #308]: #299 +#600 := [unit-resolution #309 #261]: #295 +#601 := [unit-resolution #600 #583]: #294 +#422 := (not #294) +#602 := (or #422 #310) +#603 := [th-lemma arith triangle-eq]: #602 +#604 := [unit-resolution #603 #601]: #310 +#311 := (>= #263 1::Int) +#556 := (not #311) +#557 := [hypothesis]: #556 +#558 := (or #422 #311) +#559 := [th-lemma arith triangle-eq]: #558 +#560 := [unit-resolution #559 #557]: #422 +#396 := (= #263 3::Int) +#425 := (not #396) +#419 := (>= #263 3::Int) +#561 := (not #419) +#562 := (or #561 #311) +#563 := [th-lemma arith farkas 1 1]: #562 +#564 := [unit-resolution #563 #557]: #561 +#565 := (or #425 #419) +#566 := [th-lemma arith triangle-eq]: #565 +#567 := [unit-resolution #566 #564]: #425 +#397 := (= #263 2::Int) +#428 := (not #397) +#421 := (>= #263 2::Int) +#568 := (not #421) +#569 := (or #568 #311) +#570 := [th-lemma arith farkas 1 1]: #569 +#571 := [unit-resolution #570 #557]: #568 +#572 := (or #428 #421) +#573 := [th-lemma arith triangle-eq]: #572 +#574 := [unit-resolution #573 #571]: #428 +#402 := (or #294 #396 #397) +#389 := (f9 #263 f10) +#390 := (= f1 #389) +#405 := (iff #390 #402) +#409 := (or #408 #405) +#400 := (or #294 #397 #396) +#401 := (iff #390 #400) +#410 := (or #408 #401) +#412 := (iff #410 #409) +#414 := (iff #409 #409) +#415 := [rewrite]: #414 +#406 := (iff #401 #405) +#403 := (iff #400 #402) +#404 := [rewrite]: #403 +#407 := [monotonicity #404]: #406 +#413 := [monotonicity #407]: #412 +#416 := [trans #413 #415]: #412 +#411 := [quant-inst #263]: #410 +#417 := [mp #411 #416]: #409 +#575 := [unit-resolution #417 #247]: #405 +#434 := (not #405) +#577 := (or #434 #402) +#248 := (pattern #24) +#40 := (f9 #24 f10) +#124 := (= f1 #40) +#249 := (forall (vars (?v0 S2)) (:pat #248) #124) +#127 := (forall (vars (?v0 S2)) #124) +#252 := (iff #127 #249) +#250 := (iff #124 #124) +#251 := [refl]: #250 +#253 := [quant-intro #251]: #252 +#169 := (~ #127 #127) +#167 := (~ #124 #124) +#168 := [refl]: #167 +#170 := [nnf-pos #168]: #169 +#41 := (= #40 f1) +#42 := (forall (vars (?v0 S2)) #41) +#128 := (iff #42 #127) +#125 := (iff #41 #124) +#126 := [rewrite]: #125 +#129 := [quant-intro #126]: #128 +#123 := [asserted]: #42 +#132 := [mp #123 #129]: #127 +#171 := [mp~ #132 #170]: #127 +#254 := [mp #171 #253]: #249 +#393 := (not #249) +#394 := (or #393 #390) +#395 := [quant-inst #10]: #394 +#576 := [unit-resolution #395 #254]: #390 +#437 := (not #390) +#438 := (or #434 #437 #402) +#439 := [def-axiom]: #438 +#578 := [unit-resolution #439 #576]: #577 +#579 := [unit-resolution #578 #575]: #402 +#431 := (not #402) +#432 := (or #431 #294 #396 #397) +#433 := [def-axiom]: #432 +#580 := [unit-resolution #433 #579]: #402 +#581 := [unit-resolution #580 #574 #567 #560]: false +#582 := [lemma #581]: #311 +#334 := (<= #262 2::Int) +#319 := (= #262 2::Int) +#313 := (f9 2::Int f10) +#314 := (= f1 #313) +#315 := (not #314) +#654 := [hypothesis]: #315 +#645 := (or #408 #314) +#621 := (= 2::Int 3::Int) +#622 := (= 2::Int 2::Int) +#620 := (= 2::Int 1::Int) +#623 := (or #620 #622 #621) +#624 := (iff #314 #623) +#646 := (or #408 #624) +#648 := (iff #646 #645) +#650 := (iff #645 #645) +#651 := [rewrite]: #650 +#643 := (iff #624 #314) +#638 := (iff #314 true) +#641 := (iff #638 #314) +#642 := [rewrite]: #641 +#639 := (iff #624 #638) +#636 := (iff #623 true) +#631 := (or false true false) +#634 := (iff #631 true) +#635 := [rewrite]: #634 +#632 := (iff #623 #631) +#629 := (iff #621 false) +#630 := [rewrite]: #629 +#627 := (iff #622 true) +#628 := [rewrite]: #627 +#625 := (iff #620 false) +#626 := [rewrite]: #625 +#633 := [monotonicity #626 #628 #630]: #632 +#637 := [trans #633 #635]: #636 +#640 := [monotonicity #637]: #639 +#644 := [trans #640 #642]: #643 +#649 := [monotonicity #644]: #648 +#652 := [trans #649 #651]: #648 +#647 := [quant-inst #13]: #646 +#653 := [mp #647 #652]: #645 +#655 := [unit-resolution #653 #247 #654]: false +#656 := [lemma #655]: #314 +#320 := (or #315 #319) +#323 := (or #298 #315 #319) +#312 := (= 2::Int #262) +#316 := (or #315 #312) +#324 := (or #298 #316) +#331 := (iff #324 #323) +#326 := (or #298 #320) +#329 := (iff #326 #323) +#330 := [rewrite]: #329 +#327 := (iff #324 #326) +#321 := (iff #316 #320) +#317 := (iff #312 #319) +#318 := [rewrite]: #317 +#322 := [monotonicity #318]: #321 +#328 := [monotonicity #322]: #327 +#332 := [trans #328 #330]: #331 +#325 := [quant-inst #13]: #324 +#333 := [mp #325 #332]: #323 +#605 := [unit-resolution #333 #261]: #320 +#606 := [unit-resolution #605 #656]: #319 +#477 := (not #319) +#607 := (or #477 #334) +#608 := [th-lemma arith triangle-eq]: #607 +#609 := [unit-resolution #608 #606]: #334 +#335 := (>= #262 2::Int) +#610 := (or #477 #335) +#611 := [th-lemma arith triangle-eq]: #610 +#612 := [unit-resolution #611 #606]: #335 +#613 := [th-lemma arith eq-propagate -1 -1 -1 -1 #612 #609 #582 #604]: #504 +#615 := [symm #613]: #614 +#617 := [monotonicity #615]: #616 +#19 := (= f6 #18) +#72 := [asserted]: #19 +#589 := [trans #72 #617]: #588 +#591 := [trans #589 #586]: #590 +#592 := [trans #591 #587]: #148 +#152 := (not #148) +#49 := (= #48 f6) +#50 := (not #49) +#153 := (iff #50 #152) +#150 := (iff #49 #148) +#151 := [rewrite]: #150 +#154 := [monotonicity #151]: #153 +#147 := [asserted]: #50 +#157 := [mp #147 #154]: #152 +[unit-resolution #157 #592]: false +unsat +e90da59d7c0ef5b4100b7b5941ef59b730edfa8b 1 0 +unsat +b8fa35f9ffb93b572016b3a7093d90ff2dc40803 1 0 +unsat +67a18ee4a41e7117d729538d363dd01cbfa4400f 1 0 +unsat +29980cc57d37b1e6a91568b59eb645177c64332b 1 0 +unsat +dd72068dbc111520c8cda49beba061234668dba7 1 0 +unsat +bb1b1bf771dfd4a69322f6b2c9c31e57298bea9e 1 0 +unsat +f591b022c531a1890a327600010c782c78467eea 1 0 +unsat +09e7a23356dd5244a2517b62d3c6c28d99ae59e0 1 0 +unsat +7e5bac87b0ad340d97ecc55bcd3e3e6d37b536c9 1 0 +unsat +353f7e426c920cff9e100b30ce094cb37c8e66ef 1 0 +unsat +f963333a6744a2101618437d210242d060c0ac5f 1 0 +unsat +d01b3542d6a35de6bfb4aabf081dc52de8396d03 1 0 +unsat +e4b3e00cd29c16e895ffff3cac3d892b78dd9d59 1 0 +unsat +92350fc2dc39b61c7b65a45e3abab78db9321ed5 1 0 +unsat +d1a2878c51a9f44dc2f50ee9dd016f837f75dee3 1 0 +unsat +4b51e5348b328fdbe195bfc6dbb2d5f6e8e086af 1 0 +unsat +9960e2fa518de05dd4c22ebef61695106b67bab7 1 0 +unsat +d76cad4f4fe52cdb217d0d7a4c83030e5fa9bc16 1 0 +unsat +7701f25b2b2e492d6188369ec45f452bde984707 1 0 +unsat +9a74b65514398a03fd5460e9b464fc4f5bb5b307 1 0 +unsat +f80447a4f9b0f86fa11f2153b5158216a61f7a84 1 0 +unsat +458218ced7c9e0f75f06741e621b45de73ff0cd1 1 0 +unsat +14345cc17c0b30096f6adb793fe85b488a534926 1 0 +unsat +aef4860d2ed0c8d87f72946dc202dcd55f3ca531 1 0 +unsat +8257b3938dcc8cb19f272f67be8d362ad144f382 1 0 +unsat +60a21c8506be79a307d9799d9dfff80c0c772737 1 0 +unsat +83d73aee1e57b6bce6f0ec35dfd1ee35d30d33a1 1 0 +unsat +553daa4feeb8e9fdfd2f7bcfa581d9f0c1549602 1 0 +unsat +d403b2341400efa6e1957a6278e319822955eb05 1 0 +unsat +33032b5811c88e9f094d892b2a819fd19687b4da 1 0 +unsat +af7864ebe2c19275b1474fcca68f68b40df07ee6 1 0 +unsat +f0be9c3035095639c56feef5476f5ff5d0ee0300 1 0 +unsat +be181562b775b67e969c16b78a52a45719fecfc8 1 0 +unsat +e4212f39c43f0c68b93f2fa581abc8dc5b04f3dc 1 0 +unsat +45a80c71e5479b14c918c2ca636ce6a9093c7d91 1 0 +unsat +5c358740eab4a6d03dfdc04d4f4ace62d00a397c 1 0 +unsat +0cb2094ef75f1257300f2250bf51922ba0fc3eb4 1 0 +unsat +ee7744e271c9a6a2fec104da7e0da7381f74a42b 1 0 +unsat +509b9e96fe074cbcbee283f62b2e6df84f698cac 1 0 +unsat +817280eb269b77adcbb4245ba3f6e9840888526e 1 0 +unsat +9f0e8a08f3bda5c750992a9feaa96f513f7e38ad 1 0 +unsat +93dac8884c5cd6ad5574a943f98c41bd92476bb2 1 0 +unsat +46f948909b4f895c551d3cd1088294f8741c9b04 1 0 +unsat +199918281288b75f2e2685c34a7c9417c1a0fe8f 1 0 +unsat +182c59ee9cff8516467bee4139ec0b725d34bea4 1 0 +unsat +82ca1ca20ab4808c4ae7a1caec7420902013622a 1 0 +unsat +6e3dbdb2dcf0542a229dae87275558c052685051 1 0 +unsat +a55f212df57bb2f04fc56139adb1e6560632f9d3 1 0 +unsat +1a8fb5088e7f67909ddfef3f916ce9a46f24aa6e 1 0 +unsat +0d6c154e2af0c7b5235b4452bd2ff759befe4467 1 0 +unsat +782376c8bcd4bfd5ff0740cfd50cd7d65b48e694 1 0 +unsat +2fa5afe46742045fc9ae2c785161c40cd3eca8b0 1 0 +unsat +49462927b92e2fe852e19ddabb722de885a6169e 1 0 +unsat +4f884cc648fe339fa52f195bb2ef09de0043846d 1 0 +unsat +11d8c5d16e3dccca0ac06212a5289df04eac0cf0 1 0 +unsat +030f4a4becd7bcd4096d97c72b2c9fcdad6c8545 1 0 +unsat +67cb8659b90bbf301d02aab19df117412048c996 1 0 +unsat f647fab40fc301b72eb10ef98660c1294aab2896 91 0 #2 := false decl f3 :: (-> S2 S3 S4 S3 S4)
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Mon Jan 03 16:22:08 2011 +0100 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Mon Jan 03 16:49:28 2011 +0100 @@ -652,71 +652,71 @@ subsubsection {* Records *} record point = - x :: int - y :: int + cx :: int + cy :: int record bw_point = point + black :: bool lemma - "p1 = p2 \<longrightarrow> x p1 = x p2" - "p1 = p2 \<longrightarrow> y p1 = y p2" - "x p1 \<noteq> x p2 \<longrightarrow> p1 \<noteq> p2" - "y p1 \<noteq> y p2 \<longrightarrow> p1 \<noteq> p2" + "p1 = p2 \<longrightarrow> cx p1 = cx p2" + "p1 = p2 \<longrightarrow> cy p1 = cy p2" + "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2" + "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2" using point.simps by smt+ lemma - "x \<lparr> x = 3, y = 4 \<rparr> = 3" - "y \<lparr> x = 3, y = 4 \<rparr> = 4" - "x \<lparr> x = 3, y = 4 \<rparr> \<noteq> y \<lparr> x = 3, y = 4 \<rparr>" - "\<lparr> x = 3, y = 4 \<rparr> \<lparr> x := 5 \<rparr> = \<lparr> x = 5, y = 4 \<rparr>" - "\<lparr> x = 3, y = 4 \<rparr> \<lparr> y := 6 \<rparr> = \<lparr> x = 3, y = 6 \<rparr>" - "p = \<lparr> x = 3, y = 4 \<rparr> \<longrightarrow> p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p" - "p = \<lparr> x = 3, y = 4 \<rparr> \<longrightarrow> p \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr> = p" + "cx \<lparr> cx = 3, cy = 4 \<rparr> = 3" + "cy \<lparr> cx = 3, cy = 4 \<rparr> = 4" + "cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>" + "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>" + "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>" + "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" + "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p" using point.simps using [[z3_options="AUTO_CONFIG=false"]] by smt+ lemma - "y (p \<lparr> x := a \<rparr>) = y p" - "x (p \<lparr> y := a \<rparr>) = x p" - "p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr>" + "cy (p \<lparr> cx := a \<rparr>) = cy p" + "cx (p \<lparr> cy := a \<rparr>) = cx p" + "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" sorry lemma - "p1 = p2 \<longrightarrow> x p1 = x p2" - "p1 = p2 \<longrightarrow> y p1 = y p2" + "p1 = p2 \<longrightarrow> cx p1 = cx p2" + "p1 = p2 \<longrightarrow> cy p1 = cy p2" "p1 = p2 \<longrightarrow> black p1 = black p2" - "x p1 \<noteq> x p2 \<longrightarrow> p1 \<noteq> p2" - "y p1 \<noteq> y p2 \<longrightarrow> p1 \<noteq> p2" + "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2" + "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2" "black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2" using point.simps bw_point.simps by smt+ lemma - "x \<lparr> x = 3, y = 4, black = b \<rparr> = 3" - "y \<lparr> x = 3, y = 4, black = b \<rparr> = 4" - "black \<lparr> x = 3, y = 4, black = b \<rparr> = b" - "x \<lparr> x = 3, y = 4, black = b \<rparr> \<noteq> y \<lparr> x = 3, y = 4, black = b \<rparr>" - "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> x := 5 \<rparr> = \<lparr> x = 5, y = 4, black = b \<rparr>" - "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> y := 6 \<rparr> = \<lparr> x = 3, y = 6, black = b \<rparr>" - "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> x = 3, y = 4, black = w \<rparr>" - "\<lparr> x = 3, y = 4, black = True \<rparr> \<lparr> black := False \<rparr> = - \<lparr> x = 3, y = 4, black = False \<rparr>" - "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow> - p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> = p" - "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow> - p \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> x := 3 \<rparr> = p" - "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow> - p \<lparr> black := True \<rparr> \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p" + "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" + "cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" + "black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" + "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" + "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" + "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" + "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> + p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" + "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> + p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" + "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> + p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" using point.simps bw_point.simps using [[z3_options="AUTO_CONFIG=false"]] by smt+ lemma - "p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> = - p \<lparr> black := True \<rparr> \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr>" + "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" + "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = + \<lparr> cx = 3, cy = 4, black = False \<rparr>" + "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = + p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" sorry @@ -729,7 +729,7 @@ definition n3 where "n3 = Abs_three 3" definition nplus where "nplus n m = Abs_three (Rep_three n + Rep_three m)" -lemma three_def': "(x \<in> three) = (x = 1 \<or> x = 2 \<or> x = 3)" +lemma three_def': "(n \<in> three) = (n = 1 \<or> n = 2 \<or> n = 3)" by (auto simp add: three_def) lemma @@ -790,72 +790,75 @@ subsubsection {* Records *} lemma - "p1 = p2 \<longrightarrow> x p1 = x p2" - "p1 = p2 \<longrightarrow> y p1 = y p2" - "x p1 \<noteq> x p2 \<longrightarrow> p1 \<noteq> p2" - "y p1 \<noteq> y p2 \<longrightarrow> p1 \<noteq> p2" + "p1 = p2 \<longrightarrow> cx p1 = cx p2" + "p1 = p2 \<longrightarrow> cy p1 = cy p2" + "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2" + "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2" using point.simps using [[smt_datatypes, smt_oracle]] using [[z3_options="AUTO_CONFIG=false"]] by smt+ lemma - "x \<lparr> x = 3, y = 4 \<rparr> = 3" - "y \<lparr> x = 3, y = 4 \<rparr> = 4" - "x \<lparr> x = 3, y = 4 \<rparr> \<noteq> y \<lparr> x = 3, y = 4 \<rparr>" - "\<lparr> x = 3, y = 4 \<rparr> \<lparr> x := 5 \<rparr> = \<lparr> x = 5, y = 4 \<rparr>" - "\<lparr> x = 3, y = 4 \<rparr> \<lparr> y := 6 \<rparr> = \<lparr> x = 3, y = 6 \<rparr>" - "p = \<lparr> x = 3, y = 4 \<rparr> \<longrightarrow> p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p" - "p = \<lparr> x = 3, y = 4 \<rparr> \<longrightarrow> p \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr> = p" + "cx \<lparr> cx = 3, cy = 4 \<rparr> = 3" + "cy \<lparr> cx = 3, cy = 4 \<rparr> = 4" + "cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>" + "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>" + "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>" + "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" + "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p" using point.simps using [[smt_datatypes, smt_oracle]] using [[z3_options="AUTO_CONFIG=false"]] by smt+ lemma - "y (p \<lparr> x := a \<rparr>) = y p" - "x (p \<lparr> y := a \<rparr>) = x p" - "p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr>" + "cy (p \<lparr> cx := a \<rparr>) = cy p" + "cx (p \<lparr> cy := a \<rparr>) = cx p" + "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" using point.simps using [[smt_datatypes, smt_oracle]] using [[z3_options="AUTO_CONFIG=false"]] by smt+ lemma - "p1 = p2 \<longrightarrow> x p1 = x p2" - "p1 = p2 \<longrightarrow> y p1 = y p2" + "p1 = p2 \<longrightarrow> cx p1 = cx p2" + "p1 = p2 \<longrightarrow> cy p1 = cy p2" "p1 = p2 \<longrightarrow> black p1 = black p2" - "x p1 \<noteq> x p2 \<longrightarrow> p1 \<noteq> p2" - "y p1 \<noteq> y p2 \<longrightarrow> p1 \<noteq> p2" + "cx p1 \<noteq> cx p2 \<longrightarrow> p1 \<noteq> p2" + "cy p1 \<noteq> cy p2 \<longrightarrow> p1 \<noteq> p2" "black p1 \<noteq> black p2 \<longrightarrow> p1 \<noteq> p2" using point.simps bw_point.simps using [[smt_datatypes, smt_oracle]] by smt+ lemma - "x \<lparr> x = 3, y = 4, black = b \<rparr> = 3" - "y \<lparr> x = 3, y = 4, black = b \<rparr> = 4" - "black \<lparr> x = 3, y = 4, black = b \<rparr> = b" - "x \<lparr> x = 3, y = 4, black = b \<rparr> \<noteq> y \<lparr> x = 3, y = 4, black = b \<rparr>" - "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> x := 5 \<rparr> = \<lparr> x = 5, y = 4, black = b \<rparr>" - "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> y := 6 \<rparr> = \<lparr> x = 3, y = 6, black = b \<rparr>" - "\<lparr> x = 3, y = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> x = 3, y = 4, black = w \<rparr>" - "\<lparr> x = 3, y = 4, black = True \<rparr> \<lparr> black := False \<rparr> = - \<lparr> x = 3, y = 4, black = False \<rparr>" - "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow> - p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> = p" - "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow> - p \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> x := 3 \<rparr> = p" - "p = \<lparr> x = 3, y = 4, black = True \<rparr> \<longrightarrow> - p \<lparr> black := True \<rparr> \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> = p" + "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3" + "cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4" + "black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b" + "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>" + "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>" + "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>" + "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> + p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p" + "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> + p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" + "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> + p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" using point.simps bw_point.simps using [[smt_datatypes, smt_oracle]] using [[z3_options="AUTO_CONFIG=false"]] by smt+ lemma - "p \<lparr> x := 3 \<rparr> \<lparr> y := 4 \<rparr> \<lparr> black := True \<rparr> = - p \<lparr> black := True \<rparr> \<lparr> y := 4 \<rparr> \<lparr> x := 3 \<rparr>" + "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" + "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = + \<lparr> cx = 3, cy = 4, black = False \<rparr>" + sorry + +lemma + "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = + p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>" using point.simps bw_point.simps using [[smt_datatypes, smt_oracle]] using [[z3_options="AUTO_CONFIG=false"]]