# HG changeset patch # User boehmes # Date 1307533395 -7200 # Node ID 4de998188c1d7faf6e9459e0e4ea03e6254bd37c # Parent 878c0935a4a4e65c2e5fa0e28b1007f1cba9d269 updated SMT certificates diff -r 878c0935a4a4 -r 4de998188c1d src/HOL/Multivariate_Analysis/Integration.certs --- a/src/HOL/Multivariate_Analysis/Integration.certs Wed Jun 08 11:59:45 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.certs Wed Jun 08 13:43:15 2011 +0200 @@ -621,7 +621,7 @@ #427 := [unit-resolution #411 #426]: #395 [th-lemma arith farkas 2 1 2 3 1 1 #421 #319 #321 #414 #318 #427]: false unsat -02d40f3e43c6a17458cd5dc30adbe4da03d87a0c 57 0 +abf6187dd71c2713828c15119491112c5b865e88 57 0 #2 := false #41 := 0::Real decl f12 :: (-> S5 Real) @@ -660,10 +660,10 @@ #243 := (iff #137 #137) #244 := [refl]: #243 #246 := [quant-intro #244]: #245 -#146 := (~ #139 #139) -#148 := (~ #137 #137) -#145 := [refl]: #148 -#143 := [nnf-pos #145]: #146 +#155 := (~ #139 #139) +#143 := (~ #137 #137) +#144 := [refl]: #143 +#156 := [nnf-pos #144]: #155 #47 := (<= 0::Real #46) #48 := (forall (vars (?v0 S4) (?v1 S4)) #47) #140 := (iff #48 #139) @@ -672,8 +672,8 @@ #141 := [quant-intro #138]: #140 #133 := [asserted]: #48 #142 := [mp #133 #141]: #139 -#144 := [mp~ #142 #143]: #139 -#247 := [mp #144 #246]: #242 +#157 := [mp~ #142 #156]: #139 +#247 := [mp #157 #246]: #242 #251 := (not #242) #252 := (or #251 #248) #253 := [quant-inst #37 #38]: #252 diff -r 878c0935a4a4 -r 4de998188c1d src/HOL/SMT_Examples/SMT_Examples.certs --- a/src/HOL/SMT_Examples/SMT_Examples.certs Wed Jun 08 11:59:45 2011 +0200 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs Wed Jun 08 13:43:15 2011 +0200 @@ -15565,3 +15565,598 @@ #252 := [asserted]: #105 [unit-resolution #252 #617]: false unsat +5a76ac61ccccc3cf413dd2cf808cc3df750b1eab 61 0 +#2 := false +decl f7 :: S2 +#18 := f7 +decl f5 :: S2 +#14 := f5 +#20 := (= f5 f7) +decl f3 :: (-> S4 S2) +decl f4 :: (-> S2 S3 S4) +decl f6 :: S3 +#15 := f6 +#16 := (f4 f5 f6) +#17 := (f3 #16) +#19 := (= #17 f7) +#50 := (not #19) +#52 := (or #50 #20) +#55 := (not #52) +#21 := (implies #19 #20) +#22 := (not #21) +#56 := (iff #22 #55) +#53 := (iff #21 #52) +#54 := [rewrite]: #53 +#57 := [monotonicity #54]: #56 +#49 := [asserted]: #22 +#60 := [mp #49 #57]: #55 +#58 := [not-or-elim #60]: #19 +#125 := (= f5 #17) +#9 := (:var 0 S3) +#8 := (:var 1 S2) +#10 := (f4 #8 #9) +#543 := (pattern #10) +#11 := (f3 #10) +#43 := (= #8 #11) +#544 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #543) #43) +#46 := (forall (vars (?v0 S2) (?v1 S3)) #43) +#547 := (iff #46 #544) +#545 := (iff #43 #43) +#546 := [refl]: #545 +#548 := [quant-intro #546]: #547 +#73 := (~ #46 #46) +#71 := (~ #43 #43) +#72 := [refl]: #71 +#74 := [nnf-pos #72]: #73 +#12 := (= #11 #8) +#13 := (forall (vars (?v0 S2) (?v1 S3)) #12) +#47 := (iff #13 #46) +#44 := (iff #12 #43) +#45 := [rewrite]: #44 +#48 := [quant-intro #45]: #47 +#42 := [asserted]: #13 +#51 := [mp #42 #48]: #46 +#63 := [mp~ #51 #74]: #46 +#549 := [mp #63 #548]: #544 +#213 := (not #544) +#127 := (or #213 #125) +#214 := [quant-inst #14 #15]: #127 +#212 := [unit-resolution #214 #549]: #125 +#126 := [trans #212 #58]: #20 +#59 := (not #20) +#61 := [not-or-elim #60]: #59 +[unit-resolution #61 #126]: false +unsat +e37a715fae94dfacce2b81d39c657fd74713dfe9 116 0 +#2 := false +decl f8 :: (-> S4 S3) +decl f12 :: S4 +#31 := f12 +#36 := (f8 f12) +decl f5 :: (-> S5 S3) +decl f9 :: S5 +#26 := f9 +#35 := (f5 f9) +#37 := (= #35 #36) +decl f4 :: (-> S2 S3 S4) +decl f10 :: S3 +#27 := f10 +decl f11 :: S2 +#28 := f11 +#32 := (f4 f11 f10) +#184 := (f8 #32) +#248 := (= #184 #36) +#600 := (= #36 #184) +#33 := (= f12 #32) +decl f6 :: (-> S3 S2 S5) +#29 := (f6 f10 f11) +#30 := (= f9 #29) +#34 := (and #30 #33) +#91 := (not #34) +#93 := (or #91 #37) +#96 := (not #93) +#38 := (implies #34 #37) +#39 := (not #38) +#97 := (iff #39 #96) +#94 := (iff #38 #93) +#95 := [rewrite]: #94 +#98 := [monotonicity #95]: #97 +#90 := [asserted]: #39 +#101 := [mp #90 #98]: #96 +#99 := [not-or-elim #101]: #34 +#102 := [and-elim #99]: #33 +#590 := [monotonicity #102]: #600 +#253 := [symm #590]: #248 +#592 := (= #35 #184) +#271 := (= f10 #184) +#9 := (:var 0 S3) +#8 := (:var 1 S2) +#10 := (f4 #8 #9) +#601 := (pattern #10) +#23 := (f8 #10) +#83 := (= #9 #23) +#621 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #601) #83) +#87 := (forall (vars (?v0 S2) (?v1 S3)) #83) +#624 := (iff #87 #621) +#622 := (iff #83 #83) +#623 := [refl]: #622 +#625 := [quant-intro #623]: #624 +#112 := (~ #87 #87) +#131 := (~ #83 #83) +#132 := [refl]: #131 +#113 := [nnf-pos #132]: #112 +#24 := (= #23 #9) +#25 := (forall (vars (?v0 S2) (?v1 S3)) #24) +#88 := (iff #25 #87) +#85 := (iff #24 #83) +#86 := [rewrite]: #85 +#89 := [quant-intro #86]: #88 +#82 := [asserted]: #25 +#92 := [mp #82 #89]: #87 +#133 := [mp~ #92 #113]: #87 +#626 := [mp #133 #625]: #621 +#203 := (not #621) +#276 := (or #203 #271) +#273 := [quant-inst #28 #27]: #276 +#382 := [unit-resolution #273 #626]: #271 +#591 := (= #35 f10) +#274 := (f5 #29) +#599 := (= #274 f10) +#275 := (= f10 #274) +#15 := (:var 0 S2) +#14 := (:var 1 S3) +#16 := (f6 #14 #15) +#608 := (pattern #16) +#17 := (f5 #16) +#67 := (= #14 #17) +#609 := (forall (vars (?v0 S3) (?v1 S2)) (:pat #608) #67) +#71 := (forall (vars (?v0 S3) (?v1 S2)) #67) +#612 := (iff #71 #609) +#610 := (iff #67 #67) +#611 := [refl]: #610 +#613 := [quant-intro #611]: #612 +#108 := (~ #71 #71) +#107 := (~ #67 #67) +#126 := [refl]: #107 +#109 := [nnf-pos #126]: #108 +#18 := (= #17 #14) +#19 := (forall (vars (?v0 S3) (?v1 S2)) #18) +#72 := (iff #19 #71) +#69 := (iff #18 #67) +#70 := [rewrite]: #69 +#73 := [quant-intro #70]: #72 +#66 := [asserted]: #19 +#76 := [mp #66 #73]: #71 +#127 := [mp~ #76 #109]: #71 +#614 := [mp #127 #613]: #609 +#593 := (not #609) +#595 := (or #593 #275) +#250 := [quant-inst #27 #28]: #595 +#589 := [unit-resolution #250 #614]: #275 +#594 := [symm #589]: #599 +#597 := (= #35 #274) +#100 := [and-elim #99]: #30 +#598 := [monotonicity #100]: #597 +#249 := [trans #598 #594]: #591 +#233 := [trans #249 #382]: #592 +#576 := [trans #233 #253]: #37 +#103 := (not #37) +#104 := [not-or-elim #101]: #103 +[unit-resolution #104 #576]: false +unsat +0a51c265dbf4d3067e92be219272e95358c500c5 415 0 +#2 := false +decl f3 :: (-> S2 S3) +decl f4 :: (-> S1 S2) +decl f1 :: S1 +#4 := f1 +#102 := (f4 f1) +#103 := (f3 #102) +decl f8 :: (-> S5 S3) +decl f9 :: (-> Int S5) +#99 := 3::Int +#100 := (f9 3::Int) +#101 := (f8 #100) +#104 := (= #101 #103) +decl f5 :: (-> S4 S3) +decl f6 :: (-> S1 S4 S4) +decl f7 :: S4 +#11 := f7 +#462 := (f6 f1 f7) +#546 := (f5 #462) +#638 := (= #546 #103) +#547 := (= #103 #546) +#8 := (:var 0 S1) +#12 := (f6 #8 f7) +#877 := (pattern #12) +#9 := (f4 #8) +#876 := (pattern #9) +#13 := (f5 #12) +#10 := (f3 #9) +#14 := (= #10 #13) +#878 := (forall (vars (?v0 S1)) (:pat #876 #877) #14) +#15 := (forall (vars (?v0 S1)) #14) +#881 := (iff #15 #878) +#879 := (iff #14 #14) +#880 := [refl]: #879 +#882 := [quant-intro #880]: #881 +#384 := (~ #15 #15) +#382 := (~ #14 #14) +#383 := [refl]: #382 +#385 := [nnf-pos #383]: #384 +#140 := [asserted]: #15 +#340 := [mp~ #140 #385]: #15 +#883 := [mp #340 #882]: #878 +#550 := (not #878) +#551 := (or #550 #547) +#552 := [quant-inst #4]: #551 +#719 := [unit-resolution #552 #883]: #547 +#640 := [symm #719]: #638 +#637 := (= #101 #546) +decl f16 :: (-> S4 S3) +#569 := (f16 #462) +#631 := (= #569 #546) +#843 := (= #546 #569) +#39 := (:var 0 S4) +#41 := (f16 #39) +#901 := (pattern #41) +#40 := (f5 #39) +#900 := (pattern #40) +#42 := (= #40 #41) +#902 := (forall (vars (?v0 S4)) (:pat #900 #901) #42) +#43 := (forall (vars (?v0 S4)) #42) +#905 := (iff #43 #902) +#903 := (iff #42 #42) +#904 := [refl]: #903 +#906 := [quant-intro #904]: #905 +#354 := (~ #43 #43) +#353 := (~ #42 #42) +#350 := [refl]: #353 +#355 := [nnf-pos #350]: #354 +#154 := [asserted]: #43 +#351 := [mp~ #154 #355]: #43 +#907 := [mp #351 #906]: #902 +#872 := (not #902) +#848 := (or #872 #843) +#558 := [quant-inst #462]: #848 +#674 := [unit-resolution #558 #907]: #843 +#634 := [symm #674]: #631 +#636 := (= #101 #569) +decl f18 :: (-> S7 Int S3) +decl f21 :: (-> S3 Int) +#85 := (f16 f7) +#847 := (f21 #85) +#64 := 1::Int +#844 := (+ 1::Int #847) +decl f19 :: S7 +#46 := f19 +#559 := (f18 f19 #844) +#561 := (= #559 #569) +#71 := (:var 1 S1) +#72 := (f6 #71 #39) +#943 := (pattern #72) +#94 := (f21 #41) +#238 := (+ 1::Int #94) +#243 := (f18 f19 #238) +#93 := (f16 #72) +#246 := (= #93 #243) +#944 := (forall (vars (?v0 S1) (?v1 S4)) (:pat #943) #246) +#249 := (forall (vars (?v0 S1) (?v1 S4)) #246) +#947 := (iff #249 #944) +#945 := (iff #246 #246) +#946 := [refl]: #945 +#948 := [quant-intro #946]: #947 +#370 := (~ #249 #249) +#369 := (~ #246 #246) +#366 := [refl]: #369 +#371 := [nnf-pos #366]: #370 +#47 := 0::Int +#65 := (+ 0::Int 1::Int) +#95 := (+ #94 #65) +#96 := (f18 f19 #95) +#97 := (= #93 #96) +#98 := (forall (vars (?v0 S1) (?v1 S4)) #97) +#250 := (iff #98 #249) +#247 := (iff #97 #246) +#244 := (= #96 #243) +#241 := (= #95 #238) +#234 := (+ #94 1::Int) +#239 := (= #234 #238) +#240 := [rewrite]: #239 +#236 := (= #95 #234) +#165 := (= #65 1::Int) +#167 := [rewrite]: #165 +#237 := [monotonicity #167]: #236 +#242 := [trans #237 #240]: #241 +#245 := [monotonicity #242]: #244 +#248 := [monotonicity #245]: #247 +#251 := [quant-intro #248]: #250 +#233 := [asserted]: #98 +#254 := [mp #233 #251]: #249 +#367 := [mp~ #254 #371]: #249 +#949 := [mp #367 #948]: #944 +#554 := (not #944) +#837 := (or #554 #561) +#560 := (= #569 #559) +#841 := (or #554 #560) +#842 := (iff #841 #837) +#832 := (iff #837 #837) +#833 := [rewrite]: #832 +#839 := (iff #560 #561) +#840 := [rewrite]: #839 +#831 := [monotonicity #840]: #842 +#828 := [trans #831 #833]: #842 +#838 := [quant-inst #4 #11]: #841 +#829 := [mp #838 #828]: #837 +#681 := [unit-resolution #829 #949]: #561 +#633 := (= #101 #559) +decl f15 :: (-> S6 S3) +decl f12 :: S6 +#19 := f12 +#83 := (f15 f12) +#830 := (f21 #83) +#836 := (+ 1::Int #830) +#679 := (f18 f19 #836) +#647 := (= #679 #559) +#646 := (= #836 #844) +#644 := (= 1::Int #844) +#653 := (= #844 1::Int) +#815 := (<= #847 0::Int) +#813 := (= #847 0::Int) +#48 := (f18 f19 0::Int) +#869 := (f21 #48) +#866 := (= #869 0::Int) +#16 := (:var 0 Int) +#112 := (f18 f19 #16) +#957 := (pattern #112) +#280 := (>= #16 0::Int) +#281 := (not #280) +#113 := (f21 #112) +#262 := (= #16 #113) +#287 := (or #262 #281) +#958 := (forall (vars (?v0 Int)) (:pat #957) #287) +#292 := (forall (vars (?v0 Int)) #287) +#961 := (iff #292 #958) +#959 := (iff #287 #287) +#960 := [refl]: #959 +#962 := [quant-intro #960]: #961 +#376 := (~ #292 #292) +#375 := (~ #287 #287) +#402 := [refl]: #375 +#377 := [nnf-pos #402]: #376 +#114 := (= #113 #16) +#111 := (<= 0::Int #16) +#115 := (implies #111 #114) +#116 := (forall (vars (?v0 Int)) #115) +#295 := (iff #116 #292) +#269 := (not #111) +#270 := (or #269 #262) +#275 := (forall (vars (?v0 Int)) #270) +#293 := (iff #275 #292) +#290 := (iff #270 #287) +#284 := (or #281 #262) +#288 := (iff #284 #287) +#289 := [rewrite]: #288 +#285 := (iff #270 #284) +#282 := (iff #269 #281) +#278 := (iff #111 #280) +#279 := [rewrite]: #278 +#283 := [monotonicity #279]: #282 +#286 := [monotonicity #283]: #285 +#291 := [trans #286 #289]: #290 +#294 := [quant-intro #291]: #293 +#276 := (iff #116 #275) +#273 := (iff #115 #270) +#266 := (implies #111 #262) +#271 := (iff #266 #270) +#272 := [rewrite]: #271 +#267 := (iff #115 #266) +#264 := (iff #114 #262) +#265 := [rewrite]: #264 +#268 := [monotonicity #265]: #267 +#274 := [trans #268 #272]: #273 +#277 := [quant-intro #274]: #276 +#296 := [trans #277 #294]: #295 +#261 := [asserted]: #116 +#297 := [mp #261 #296]: #292 +#403 := [mp~ #297 #377]: #292 +#963 := [mp #403 #962]: #958 +#859 := (not #958) +#861 := (or #859 #866) +#657 := (>= 0::Int 0::Int) +#871 := (not #657) +#875 := (= 0::Int #869) +#865 := (or #875 #871) +#500 := (or #859 #865) +#862 := (iff #500 #861) +#863 := (iff #861 #861) +#849 := [rewrite]: #863 +#858 := (iff #865 #866) +#854 := (or #866 false) +#857 := (iff #854 #866) +#852 := [rewrite]: #857 +#855 := (iff #865 #854) +#516 := (iff #871 false) +#1 := true +#509 := (not true) +#514 := (iff #509 false) +#515 := [rewrite]: #514 +#851 := (iff #871 #509) +#525 := (iff #657 true) +#867 := [rewrite]: #525 +#513 := [monotonicity #867]: #851 +#853 := [trans #513 #515]: #516 +#524 := (iff #875 #866) +#529 := [rewrite]: #524 +#856 := [monotonicity #529 #853]: #855 +#495 := [trans #856 #852]: #858 +#860 := [monotonicity #495]: #862 +#850 := [trans #860 #849]: #862 +#501 := [quant-inst #47]: #500 +#557 := [mp #501 #850]: #861 +#682 := [unit-resolution #557 #963]: #866 +#684 := (= #847 #869) +#86 := (= #85 #48) +#210 := (= #48 #85) +#212 := (iff #86 #210) +#213 := [rewrite]: #212 +#209 := [asserted]: #86 +#216 := [mp #209 #213]: #210 +#683 := [symm #216]: #86 +#685 := [monotonicity #683]: #684 +#686 := [trans #685 #682]: #813 +#687 := (not #813) +#688 := (or #687 #815) +#689 := [th-lemma arith triangle-eq]: #688 +#690 := [unit-resolution #689 #686]: #815 +#816 := (>= #847 0::Int) +#691 := (or #687 #816) +#676 := [th-lemma arith triangle-eq]: #691 +#692 := [unit-resolution #676 #686]: #816 +#654 := [th-lemma arith eq-propagate -1 -1 #692 #690]: #653 +#645 := [symm #654]: #644 +#673 := (= #836 1::Int) +#817 := (<= #830 0::Int) +#814 := (= #830 0::Int) +#663 := (= #830 #869) +#84 := (= #83 #48) +#205 := (= #48 #83) +#207 := (iff #84 #205) +#208 := [rewrite]: #207 +#204 := [asserted]: #84 +#211 := [mp #204 #208]: #205 +#661 := [symm #211]: #84 +#664 := [monotonicity #661]: #663 +#665 := [trans #664 #682]: #814 +#667 := (not #814) +#668 := (or #667 #817) +#669 := [th-lemma arith triangle-eq]: #668 +#670 := [unit-resolution #669 #665]: #817 +#699 := (>= #830 0::Int) +#671 := (or #667 #699) +#672 := [th-lemma arith triangle-eq]: #671 +#655 := [unit-resolution #672 #665]: #699 +#643 := [th-lemma arith eq-propagate -1 -1 #655 #670]: #673 +#648 := [trans #643 #645]: #646 +#652 := [monotonicity #648]: #647 +#642 := (= #101 #679) +decl f11 :: (-> Int S6 S6) +#548 := (f11 3::Int f12) +#834 := (f15 #548) +#821 := (= #834 #679) +#822 := (= #679 #834) +#34 := (:var 0 S6) +#56 := (:var 1 Int) +#57 := (f11 #56 #34) +#936 := (pattern #57) +#36 := (f15 #34) +#88 := (f21 #36) +#219 := (+ 1::Int #88) +#224 := (f18 f19 #219) +#87 := (f15 #57) +#227 := (= #87 #224) +#937 := (forall (vars (?v0 Int) (?v1 S6)) (:pat #936) #227) +#230 := (forall (vars (?v0 Int) (?v1 S6)) #227) +#940 := (iff #230 #937) +#938 := (iff #227 #227) +#939 := [refl]: #938 +#941 := [quant-intro #939]: #940 +#364 := (~ #230 #230) +#398 := (~ #227 #227) +#399 := [refl]: #398 +#365 := [nnf-pos #399]: #364 +#89 := (+ #88 #65) +#90 := (f18 f19 #89) +#91 := (= #87 #90) +#92 := (forall (vars (?v0 Int) (?v1 S6)) #91) +#231 := (iff #92 #230) +#228 := (iff #91 #227) +#225 := (= #90 #224) +#222 := (= #89 #219) +#215 := (+ #88 1::Int) +#220 := (= #215 #219) +#221 := [rewrite]: #220 +#217 := (= #89 #215) +#218 := [monotonicity #167]: #217 +#223 := [trans #218 #221]: #222 +#226 := [monotonicity #223]: #225 +#229 := [monotonicity #226]: #228 +#232 := [quant-intro #229]: #231 +#214 := [asserted]: #92 +#235 := [mp #214 #232]: #230 +#368 := [mp~ #235 #365]: #230 +#942 := [mp #368 #941]: #937 +#818 := (not #937) +#819 := (or #818 #822) +#825 := (or #818 #821) +#820 := (iff #825 #819) +#656 := (iff #819 #819) +#658 := [rewrite]: #656 +#823 := (iff #821 #822) +#824 := [rewrite]: #823 +#827 := [monotonicity #824]: #820 +#659 := [trans #827 #658]: #820 +#826 := [quant-inst #99 #19]: #825 +#812 := [mp #826 #659]: #819 +#649 := [unit-resolution #812 #942]: #822 +#651 := [symm #649]: #821 +#641 := (= #101 #834) +decl f10 :: (-> S6 S3) +#539 := (f10 #548) +#835 := (= #539 #834) +#893 := (pattern #36) +#35 := (f10 #34) +#892 := (pattern #35) +#37 := (= #35 #36) +#894 := (forall (vars (?v0 S6)) (:pat #892 #893) #37) +#38 := (forall (vars (?v0 S6)) #37) +#897 := (iff #38 #894) +#895 := (iff #37 #37) +#896 := [refl]: #895 +#898 := [quant-intro #896]: #897 +#344 := (~ #38 #38) +#388 := (~ #37 #37) +#389 := [refl]: #388 +#345 := [nnf-pos #389]: #344 +#153 := [asserted]: #38 +#352 := [mp~ #153 #345]: #38 +#899 := [mp #352 #898]: #894 +#864 := (not #894) +#677 := (or #864 #835) +#678 := [quant-inst #548]: #677 +#650 := [unit-resolution #678 #899]: #835 +#549 := (= #101 #539) +#20 := (f11 #16 f12) +#885 := (pattern #20) +#17 := (f9 #16) +#884 := (pattern #17) +#21 := (f10 #20) +#18 := (f8 #17) +#22 := (= #18 #21) +#886 := (forall (vars (?v0 Int)) (:pat #884 #885) #22) +#23 := (forall (vars (?v0 Int)) #22) +#889 := (iff #23 #886) +#887 := (iff #22 #22) +#888 := [refl]: #887 +#890 := [quant-intro #888]: #889 +#342 := (~ #23 #23) +#341 := (~ #22 #22) +#386 := [refl]: #341 +#343 := [nnf-pos #386]: #342 +#141 := [asserted]: #23 +#387 := [mp~ #141 #343]: #23 +#891 := [mp #387 #890]: #886 +#868 := (not #886) +#870 := (or #868 #549) +#526 := [quant-inst #99]: #870 +#492 := [unit-resolution #526 #891]: #549 +#639 := [trans #492 #650]: #641 +#630 := [trans #639 #651]: #642 +#635 := [trans #630 #652]: #633 +#632 := [trans #635 #681]: #636 +#627 := [trans #632 #634]: #637 +#617 := [trans #627 #640]: #104 +#105 := (not #104) +#252 := [asserted]: #105 +[unit-resolution #252 #617]: false +unsat diff -r 878c0935a4a4 -r 4de998188c1d src/HOL/SMT_Examples/SMT_Tests.certs --- a/src/HOL/SMT_Examples/SMT_Tests.certs Wed Jun 08 11:59:45 2011 +0200 +++ b/src/HOL/SMT_Examples/SMT_Tests.certs Wed Jun 08 13:43:15 2011 +0200 @@ -50037,7 +50037,7 @@ #87 := [and-elim #86]: #46 [th-lemma arith farkas 1 1 1 #87 #88 #89]: false unsat -267c94908fa1cba1e9bb1ecaaa4c65058e972cc1 43 0 +df4ce8c591cd4d3dc5b57ede848dc6285f8d31c0 43 0 #2 := false decl f3 :: (-> S3 S2) decl f4 :: (-> S2 S2 S3) @@ -50062,10 +50062,10 @@ #566 := (iff #49 #49) #567 := [refl]: #566 #569 := [quant-intro #567]: #568 -#76 := (~ #52 #52) -#83 := (~ #49 #49) -#84 := [refl]: #83 -#77 := [nnf-pos #84]: #76 +#86 := (~ #52 #52) +#84 := (~ #49 #49) +#85 := [refl]: #84 +#87 := [nnf-pos #85]: #86 #12 := (= #11 #8) #13 := (forall (vars (?v0 S2) (?v1 S2)) #12) #53 := (iff #13 #52) @@ -50074,14 +50074,14 @@ #54 := [quant-intro #51]: #53 #48 := [asserted]: #13 #57 := [mp #48 #54]: #52 -#78 := [mp~ #57 #77]: #52 -#570 := [mp #78 #569]: #565 +#74 := [mp~ #57 #87]: #52 +#570 := [mp #74 #569]: #565 #147 := (not #565) #234 := (or #147 #27) #148 := [quant-inst #23 #24]: #234 [unit-resolution #148 #570 #71]: false unsat -eba38932115d0bb0963b99e993a7e1b0dfff5581 43 0 +7eae83a754ae3930b3797f3d00ee6d160a313dd5 43 0 #2 := false decl f5 :: (-> S3 S2) decl f4 :: (-> S2 S2 S3) @@ -50106,10 +50106,10 @@ #572 := (iff #56 #56) #573 := [refl]: #572 #575 := [quant-intro #573]: #574 -#85 := (~ #60 #60) -#81 := (~ #56 #56) -#82 := [refl]: #81 -#86 := [nnf-pos #82]: #85 +#76 := (~ #60 #60) +#75 := (~ #56 #56) +#88 := [refl]: #75 +#77 := [nnf-pos #88]: #76 #15 := (= #14 #9) #16 := (forall (vars (?v0 S2) (?v1 S2)) #15) #61 := (iff #16 #60) @@ -50118,8 +50118,8 @@ #62 := [quant-intro #59]: #61 #55 := [asserted]: #16 #65 := [mp #55 #62]: #60 -#87 := [mp~ #65 #86]: #60 -#576 := [mp #87 #575]: #571 +#89 := [mp~ #65 #77]: #60 +#576 := [mp #89 #575]: #571 #237 := (not #571) #238 := (or #237 #27) #166 := [quant-inst #24 #23]: #238 @@ -50367,68 +50367,68 @@ #266 := [def-axiom]: #179 [unit-resolution #266 #292 #218 #572]: false unsat -39134e03a4a206aeb5e8ee58e8edb86a602fc708 91 0 +f40f3c3663b225f69de5b154d25c78946af8135f 91 0 #2 := false decl f12 :: S2 #42 := f12 decl f9 :: S2 #36 := f9 #49 := (= f9 f12) -decl f3 :: (-> S4 S2) +decl f5 :: (-> S5 S2) +decl f6 :: (-> S2 S4 S5) decl f4 :: (-> S2 S3 S4) -decl f6 :: (-> S2 S5 S3) -decl f14 :: S5 +decl f14 :: S3 #44 := f14 decl f13 :: S2 #43 := f13 -#45 := (f6 f13 f14) -#46 := (f4 f12 #45) -#47 := (f3 #46) -decl f11 :: S5 +#45 := (f4 f13 f14) +#46 := (f6 f12 #45) +#47 := (f5 #46) +decl f11 :: S3 #38 := f11 decl f10 :: S2 #37 := f10 -#39 := (f6 f10 f11) -#40 := (f4 f9 #39) -#41 := (f3 #40) +#39 := (f4 f10 f11) +#40 := (f6 f9 #39) +#41 := (f5 #40) #48 := (= #41 #47) #50 := (iff #48 #49) #327 := (iff #49 #48) -#280 := (= f12 #47) -#9 := (:var 0 S3) +#606 := (= f12 #47) +#14 := (:var 0 S4) #8 := (:var 1 S2) -#10 := (f4 #8 #9) -#631 := (pattern #10) -#11 := (f3 #10) -#72 := (= #8 #11) -#632 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #631) #72) -#75 := (forall (vars (?v0 S2) (?v1 S3)) #72) -#635 := (iff #75 #632) -#633 := (iff #72 #72) -#634 := [refl]: #633 -#636 := [quant-intro #634]: #635 -#128 := (~ #75 #75) -#139 := (~ #72 #72) -#140 := [refl]: #139 -#129 := [nnf-pos #140]: #128 -#12 := (= #11 #8) -#13 := (forall (vars (?v0 S2) (?v1 S3)) #12) -#76 := (iff #13 #75) -#73 := (iff #12 #72) -#74 := [rewrite]: #73 -#77 := [quant-intro #74]: #76 -#71 := [asserted]: #13 -#80 := [mp #71 #77]: #75 -#132 := [mp~ #80 #129]: #75 -#637 := [mp #132 #636]: #632 -#286 := (not #632) -#627 := (or #286 #280) -#628 := [quant-inst #42 #45]: #627 -#605 := [unit-resolution #628 #637]: #280 -#306 := (= f9 #41) -#623 := (or #286 #306) -#625 := [quant-inst #36 #39]: #623 -#311 := [unit-resolution #625 #637]: #306 +#15 := (f6 #8 #14) +#638 := (pattern #15) +#16 := (f5 #15) +#79 := (= #8 #16) +#639 := (forall (vars (?v0 S2) (?v1 S4)) (:pat #638) #79) +#83 := (forall (vars (?v0 S2) (?v1 S4)) #79) +#642 := (iff #83 #639) +#640 := (iff #79 #79) +#641 := [refl]: #640 +#643 := [quant-intro #641]: #642 +#128 := (~ #83 #83) +#127 := (~ #79 #79) +#146 := [refl]: #127 +#129 := [nnf-pos #146]: #128 +#17 := (= #16 #8) +#18 := (forall (vars (?v0 S2) (?v1 S4)) #17) +#84 := (iff #18 #83) +#81 := (iff #17 #79) +#82 := [rewrite]: #81 +#85 := [quant-intro #82]: #84 +#78 := [asserted]: #18 +#88 := [mp #78 #85]: #83 +#147 := [mp~ #88 #129]: #83 +#644 := [mp #147 #643]: #639 +#279 := (not #639) +#609 := (or #279 #606) +#610 := [quant-inst #42 #45]: #609 +#605 := [unit-resolution #610 #644]: #606 +#630 := (= f9 #41) +#622 := (or #279 #630) +#263 := [quant-inst #36 #39]: #622 +#311 := [unit-resolution #263 #644]: #630 #328 := [monotonicity #311 #605]: #327 #329 := [symm #328]: #50 #302 := (not #49) @@ -50459,74 +50459,74 @@ #323 := [unit-resolution #233 #601]: #302 [unit-resolution #323 #324]: false unsat -f188cd132a2dfe3292e7656a282b6a08809558ea 210 0 +21be96a84939ebc40a46fc69c9c8174cc17510e4 210 0 #2 := false decl f14 :: S5 #44 := f14 decl f11 :: S5 #38 := f11 #50 := (= f11 f14) -#159 := (not #50) +#163 := (not #50) decl f13 :: S2 #43 := f13 decl f10 :: S2 #37 := f10 #49 := (= f10 f13) -#158 := (not #49) -#160 := (or #158 #159) -decl f7 :: (-> S4 S3) +#162 := (not #49) +#140 := (or #162 #163) +decl f8 :: (-> S4 S3) decl f4 :: (-> S2 S3 S4) decl f6 :: (-> S2 S5 S3) #45 := (f6 f13 f14) decl f12 :: S2 #42 := f12 #46 := (f4 f12 #45) -#47 := (f7 #46) +#47 := (f8 #46) #39 := (f6 f10 f11) decl f9 :: S2 #36 := f9 #40 := (f4 f9 #39) -#41 := (f7 #40) +#41 := (f8 #40) #48 := (= #41 #47) #652 := (= #45 #47) #9 := (:var 0 S3) #8 := (:var 1 S2) #10 := (f4 #8 #9) #653 := (pattern #10) -#19 := (f7 #10) -#89 := (= #9 #19) -#667 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #653) #89) -#93 := (forall (vars (?v0 S2) (?v1 S3)) #89) -#670 := (iff #93 #667) -#668 := (iff #89 #89) -#669 := [refl]: #668 -#671 := [quant-intro #669]: #670 -#152 := (~ #93 #93) -#150 := (~ #89 #89) -#151 := [refl]: #150 -#153 := [nnf-pos #151]: #152 -#20 := (= #19 #9) -#21 := (forall (vars (?v0 S2) (?v1 S3)) #20) -#94 := (iff #21 #93) -#91 := (iff #20 #89) -#92 := [rewrite]: #91 -#95 := [quant-intro #92]: #94 -#88 := [asserted]: #21 -#98 := [mp #88 #95]: #93 -#154 := [mp~ #98 #153]: #93 -#672 := [mp #154 #671]: #667 -#650 := (not #667) +#22 := (f8 #10) +#97 := (= #9 #22) +#673 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #653) #97) +#101 := (forall (vars (?v0 S2) (?v1 S3)) #97) +#676 := (iff #101 #673) +#674 := (iff #97 #97) +#675 := [refl]: #674 +#677 := [quant-intro #675]: #676 +#134 := (~ #101 #101) +#153 := (~ #97 #97) +#154 := [refl]: #153 +#135 := [nnf-pos #154]: #134 +#23 := (= #22 #9) +#24 := (forall (vars (?v0 S2) (?v1 S3)) #23) +#102 := (iff #24 #101) +#99 := (iff #23 #97) +#100 := [rewrite]: #99 +#103 := [quant-intro #100]: #102 +#96 := [asserted]: #24 +#106 := [mp #96 #103]: #101 +#155 := [mp~ #106 #135]: #101 +#678 := [mp #155 #677]: #673 +#650 := (not #673) #301 := (or #650 #652) #644 := [quant-inst #42 #45]: #301 -#337 := [unit-resolution #644 #672]: #652 +#337 := [unit-resolution #644 #678]: #652 #624 := (= #41 #45) #346 := (= #39 #45) -#161 := (not #160) -#333 := [hypothesis]: #161 -#236 := (or #160 #50) +#141 := (not #140) +#333 := [hypothesis]: #141 +#236 := (or #140 #50) #323 := [def-axiom]: #236 #352 := [unit-resolution #323 #333]: #50 -#235 := (or #160 #49) +#235 := (or #140 #49) #322 := [def-axiom]: #235 #243 := [unit-resolution #322 #333]: #49 #620 := [monotonicity #243 #352]: #346 @@ -50534,27 +50534,27 @@ #434 := (= #39 #41) #651 := (or #650 #434) #646 := [quant-inst #36 #39]: #651 -#622 := [unit-resolution #646 #672]: #434 +#622 := [unit-resolution #646 #678]: #434 #345 := [symm #622]: #623 #621 := [trans #345 #620]: #624 #625 := [trans #621 #337]: #48 #121 := (not #48) -#308 := (or #121 #160) -#172 := (iff #48 #160) +#308 := (or #121 #140) +#172 := (iff #48 #140) #51 := (and #49 #50) #123 := (iff #51 #121) #175 := (iff #123 #172) -#167 := (iff #160 #48) +#167 := (iff #140 #48) #173 := (iff #167 #172) #174 := [rewrite]: #173 #170 := (iff #123 #167) -#164 := (iff #161 #121) +#164 := (iff #141 #121) #168 := (iff #164 #167) #169 := [rewrite]: #168 #165 := (iff #123 #164) -#162 := (iff #51 #161) -#163 := [rewrite]: #162 -#166 := [monotonicity #163]: #165 +#142 := (iff #51 #141) +#143 := [rewrite]: #142 +#166 := [monotonicity #143]: #165 #171 := [trans #166 #169]: #170 #176 := [trans #171 #174]: #175 #52 := (iff #48 #51) @@ -50565,12 +50565,12 @@ #128 := [mp #120 #125]: #123 #177 := [mp #128 #176]: #172 #315 := (not #172) -#325 := (or #121 #160 #315) +#325 := (or #121 #140 #315) #329 := [def-axiom]: #325 #645 := [unit-resolution #329 #177]: #308 #349 := [unit-resolution #645 #333]: #121 #334 := [unit-resolution #349 #625]: false -#335 := [lemma #334]: #160 +#335 := [lemma #334]: #140 decl f5 :: (-> S3 S2) #292 := (f5 #45) #609 := (= #292 f13) @@ -50586,10 +50586,10 @@ #662 := (iff #81 #81) #663 := [refl]: #662 #665 := [quant-intro #663]: #664 -#145 := (~ #85 #85) -#139 := (~ #81 #81) -#140 := [refl]: #139 -#146 := [nnf-pos #140]: #145 +#130 := (~ #85 #85) +#129 := (~ #81 #81) +#148 := [refl]: #129 +#131 := [nnf-pos #148]: #130 #17 := (= #16 #8) #18 := (forall (vars (?v0 S2) (?v1 S5)) #17) #86 := (iff #18 #85) @@ -50598,8 +50598,8 @@ #87 := [quant-intro #84]: #86 #80 := [asserted]: #18 #90 := [mp #80 #87]: #85 -#147 := [mp~ #90 #146]: #85 -#666 := [mp #147 #665]: #661 +#149 := [mp~ #90 #131]: #85 +#666 := [mp #149 #665]: #661 #289 := (not #661) #635 := (or #289 #630) #271 := [quant-inst #43 #44]: #635 @@ -50611,8 +50611,8 @@ #616 := (= #47 #45) #617 := [symm #337]: #616 #330 := (= #39 #47) -#255 := (or #48 #161) -#326 := (or #48 #161 #315) +#255 := (or #48 #141) +#326 := (or #48 #141 #315) #327 := [def-axiom]: #326 #328 := [unit-resolution #327 #177]: #255 #338 := [unit-resolution #328 #335]: #48 @@ -50625,52 +50625,52 @@ #615 := [unit-resolution #291 #666]: #643 #606 := [trans #615 #608]: #605 #611 := [trans #606 #610]: #49 -decl f8 :: (-> S3 S5) -#634 := (f8 #45) +decl f7 :: (-> S3 S5) +#634 := (f7 #45) #455 := (= #634 f14) #629 := (= f14 #634) -#22 := (f8 #15) -#97 := (= #14 #22) -#673 := (forall (vars (?v0 S2) (?v1 S5)) (:pat #660) #97) -#101 := (forall (vars (?v0 S2) (?v1 S5)) #97) -#676 := (iff #101 #673) -#674 := (iff #97 #97) -#675 := [refl]: #674 -#677 := [quant-intro #675]: #676 -#143 := (~ #101 #101) -#148 := (~ #97 #97) -#149 := [refl]: #148 -#144 := [nnf-pos #149]: #143 -#23 := (= #22 #14) -#24 := (forall (vars (?v0 S2) (?v1 S5)) #23) -#102 := (iff #24 #101) -#99 := (iff #23 #97) -#100 := [rewrite]: #99 -#103 := [quant-intro #100]: #102 -#96 := [asserted]: #24 -#106 := [mp #96 #103]: #101 -#155 := [mp~ #106 #144]: #101 -#678 := [mp #155 #677]: #673 -#631 := (not #673) +#19 := (f7 #15) +#89 := (= #14 #19) +#667 := (forall (vars (?v0 S2) (?v1 S5)) (:pat #660) #89) +#93 := (forall (vars (?v0 S2) (?v1 S5)) #89) +#670 := (iff #93 #667) +#668 := (iff #89 #89) +#669 := [refl]: #668 +#671 := [quant-intro #669]: #670 +#132 := (~ #93 #93) +#150 := (~ #89 #89) +#151 := [refl]: #150 +#133 := [nnf-pos #151]: #132 +#20 := (= #19 #14) +#21 := (forall (vars (?v0 S2) (?v1 S5)) #20) +#94 := (iff #21 #93) +#91 := (iff #20 #89) +#92 := [rewrite]: #91 +#95 := [quant-intro #92]: #94 +#88 := [asserted]: #21 +#98 := [mp #88 #95]: #93 +#152 := [mp~ #98 #133]: #93 +#672 := [mp #152 #671]: #667 +#631 := (not #667) #276 := (or #631 #629) #277 := [quant-inst #43 #44]: #276 -#612 := [unit-resolution #277 #678]: #629 +#612 := [unit-resolution #277 #672]: #629 #456 := [symm #612]: #455 #598 := (= f11 #634) -#285 := (f8 #39) +#285 := (f7 #39) #613 := (= #285 #634) #454 := [monotonicity #618]: #613 #628 := (= f11 #285) #632 := (or #631 #628) #633 := [quant-inst #37 #38]: #632 -#607 := [unit-resolution #633 #678]: #628 +#607 := [unit-resolution #633 #672]: #628 #599 := [trans #607 #454]: #598 #600 := [trans #599 #456]: #50 -#237 := (or #161 #158 #159) +#237 := (or #141 #162 #163) #324 := [def-axiom]: #237 [unit-resolution #324 #600 #611 #335]: false unsat -bb6d90f8a24326b7dc1b50e80f594ff94486f0cc 144 0 +67dcdd8ec04ec052a954041c9287b8a81ea9bcac 144 0 #2 := false decl f13 :: S2 #44 := f13 @@ -50678,7 +50678,7 @@ #37 := f10 #51 := (= f10 f13) decl f5 :: (-> S3 S2) -decl f7 :: (-> S4 S3) +decl f8 :: (-> S4 S3) decl f4 :: (-> S2 S3 S4) decl f6 :: (-> S2 S5 S3) decl f14 :: S5 @@ -50687,7 +50687,7 @@ decl f12 :: S2 #43 := f12 #47 := (f4 f12 #46) -#48 := (f7 #47) +#48 := (f8 #47) #49 := (f5 #48) decl f11 :: S5 #38 := f11 @@ -50695,7 +50695,7 @@ decl f9 :: S2 #36 := f9 #40 := (f4 f9 #39) -#41 := (f7 #40) +#41 := (f8 #40) #42 := (f5 #41) #50 := (= #42 #49) #52 := (iff #50 #51) @@ -50715,10 +50715,10 @@ #642 := (iff #81 #81) #643 := [refl]: #642 #645 := [quant-intro #643]: #644 -#133 := (~ #85 #85) -#138 := (~ #81 #81) -#132 := [refl]: #138 -#134 := [nnf-pos #132]: #133 +#130 := (~ #85 #85) +#129 := (~ #81 #81) +#148 := [refl]: #129 +#131 := [nnf-pos #148]: #130 #17 := (= #16 #8) #18 := (forall (vars (?v0 S2) (?v1 S5)) #17) #86 := (iff #18 #85) @@ -50727,8 +50727,8 @@ #87 := [quant-intro #84]: #86 #80 := [asserted]: #18 #90 := [mp #80 #87]: #85 -#135 := [mp~ #90 #134]: #85 -#646 := [mp #135 #645]: #641 +#149 := [mp~ #90 #131]: #85 +#646 := [mp #149 #645]: #641 #623 := (not #641) #611 := (or #623 #608) #612 := [quant-inst #44 #45]: #611 @@ -50740,32 +50740,32 @@ #9 := (:var 0 S3) #10 := (f4 #8 #9) #633 := (pattern #10) -#19 := (f7 #10) -#89 := (= #9 #19) -#647 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #633) #89) -#93 := (forall (vars (?v0 S2) (?v1 S3)) #89) -#650 := (iff #93 #647) -#648 := (iff #89 #89) -#649 := [refl]: #648 -#651 := [quant-intro #649]: #650 -#142 := (~ #93 #93) -#136 := (~ #89 #89) -#141 := [refl]: #136 -#143 := [nnf-pos #141]: #142 -#20 := (= #19 #9) -#21 := (forall (vars (?v0 S2) (?v1 S3)) #20) -#94 := (iff #21 #93) -#91 := (iff #20 #89) -#92 := [rewrite]: #91 -#95 := [quant-intro #92]: #94 -#88 := [asserted]: #21 -#98 := [mp #88 #95]: #93 -#148 := [mp~ #98 #143]: #93 -#652 := [mp #148 #651]: #647 -#621 := (not #647) +#22 := (f8 #10) +#97 := (= #9 #22) +#653 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #633) #97) +#101 := (forall (vars (?v0 S2) (?v1 S3)) #97) +#656 := (iff #101 #653) +#654 := (iff #97 #97) +#655 := [refl]: #654 +#657 := [quant-intro #655]: #656 +#134 := (~ #101 #101) +#153 := (~ #97 #97) +#154 := [refl]: #153 +#135 := [nnf-pos #154]: #134 +#23 := (= #22 #9) +#24 := (forall (vars (?v0 S2) (?v1 S3)) #23) +#102 := (iff #24 #101) +#99 := (iff #23 #97) +#100 := [rewrite]: #99 +#103 := [quant-intro #100]: #102 +#96 := [asserted]: #24 +#106 := [mp #96 #103]: #101 +#155 := [mp~ #106 #135]: #101 +#658 := [mp #155 #657]: #653 +#621 := (not #653) #632 := (or #621 #628) #622 := [quant-inst #43 #46]: #632 -#600 := [unit-resolution #622 #652]: #628 +#600 := [unit-resolution #622 #658]: #628 #601 := [symm #600]: #604 #314 := [monotonicity #601]: #605 #596 := [trans #314 #316]: #318 @@ -50782,7 +50782,7 @@ #309 := (= #39 #41) #293 := (or #621 #309) #294 := [quant-inst #36 #39]: #293 -#310 := [unit-resolution #294 #652]: #309 +#310 := [unit-resolution #294 #658]: #309 #598 := [symm #310]: #594 #599 := [monotonicity #598]: #595 #585 := [trans #599 #589]: #590 @@ -50815,15 +50815,15 @@ #435 := [unit-resolution #235 #434]: #304 [unit-resolution #435 #436]: false unsat -ff464dff75d057630c9c6f2ae16d33617edf611b 144 0 +f039385411d77981082c23334b58503acb7a1eee 144 0 #2 := false decl f14 :: S5 #45 := f14 decl f11 :: S5 #38 := f11 #51 := (= f11 f14) -decl f8 :: (-> S3 S5) -decl f7 :: (-> S4 S3) +decl f7 :: (-> S3 S5) +decl f8 :: (-> S4 S3) decl f4 :: (-> S2 S3 S4) decl f6 :: (-> S2 S5 S3) decl f13 :: S2 @@ -50832,52 +50832,52 @@ decl f12 :: S2 #43 := f12 #47 := (f4 f12 #46) -#48 := (f7 #47) -#49 := (f8 #48) +#48 := (f8 #47) +#49 := (f7 #48) decl f10 :: S2 #37 := f10 #39 := (f6 f10 f11) decl f9 :: S2 #36 := f9 #40 := (f4 f9 #39) -#41 := (f7 #40) -#42 := (f8 #41) +#41 := (f8 #40) +#42 := (f7 #41) #50 := (= #42 #49) #52 := (iff #50 #51) #318 := (= #49 f14) -#272 := (f8 #46) +#272 := (f7 #46) #315 := (= #272 f14) #610 := (= f14 #272) #14 := (:var 0 S5) #8 := (:var 1 S2) #15 := (f6 #8 #14) #640 := (pattern #15) -#22 := (f8 #15) -#97 := (= #14 #22) -#653 := (forall (vars (?v0 S2) (?v1 S5)) (:pat #640) #97) -#101 := (forall (vars (?v0 S2) (?v1 S5)) #97) -#656 := (iff #101 #653) -#654 := (iff #97 #97) -#655 := [refl]: #654 -#657 := [quant-intro #655]: #656 -#151 := (~ #101 #101) -#149 := (~ #97 #97) -#150 := [refl]: #149 -#152 := [nnf-pos #150]: #151 -#23 := (= #22 #14) -#24 := (forall (vars (?v0 S2) (?v1 S5)) #23) -#102 := (iff #24 #101) -#99 := (iff #23 #97) -#100 := [rewrite]: #99 -#103 := [quant-intro #100]: #102 -#96 := [asserted]: #24 -#106 := [mp #96 #103]: #101 -#153 := [mp~ #106 #152]: #101 -#658 := [mp #153 #657]: #653 -#269 := (not #653) +#19 := (f7 #15) +#89 := (= #14 #19) +#647 := (forall (vars (?v0 S2) (?v1 S5)) (:pat #640) #89) +#93 := (forall (vars (?v0 S2) (?v1 S5)) #89) +#650 := (iff #93 #647) +#648 := (iff #89 #89) +#649 := [refl]: #648 +#651 := [quant-intro #649]: #650 +#132 := (~ #93 #93) +#150 := (~ #89 #89) +#151 := [refl]: #150 +#133 := [nnf-pos #151]: #132 +#20 := (= #19 #14) +#21 := (forall (vars (?v0 S2) (?v1 S5)) #20) +#94 := (iff #21 #93) +#91 := (iff #20 #89) +#92 := [rewrite]: #91 +#95 := [quant-intro #92]: #94 +#88 := [asserted]: #21 +#98 := [mp #88 #95]: #93 +#152 := [mp~ #98 #133]: #93 +#652 := [mp #152 #651]: #647 +#269 := (not #647) #609 := (or #269 #610) #615 := [quant-inst #44 #45]: #609 -#326 := [unit-resolution #615 #658]: #610 +#326 := [unit-resolution #615 #652]: #610 #316 := [symm #326]: #315 #605 := (= #49 #272) #604 := (= #48 #46) @@ -50885,49 +50885,49 @@ #9 := (:var 0 S3) #10 := (f4 #8 #9) #633 := (pattern #10) -#19 := (f7 #10) -#89 := (= #9 #19) -#647 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #633) #89) -#93 := (forall (vars (?v0 S2) (?v1 S3)) #89) -#650 := (iff #93 #647) -#648 := (iff #89 #89) -#649 := [refl]: #648 -#651 := [quant-intro #649]: #650 -#142 := (~ #93 #93) -#140 := (~ #89 #89) -#141 := [refl]: #140 -#143 := [nnf-pos #141]: #142 -#20 := (= #19 #9) -#21 := (forall (vars (?v0 S2) (?v1 S3)) #20) -#94 := (iff #21 #93) -#91 := (iff #20 #89) -#92 := [rewrite]: #91 -#95 := [quant-intro #92]: #94 -#88 := [asserted]: #21 -#98 := [mp #88 #95]: #93 -#148 := [mp~ #98 #143]: #93 -#652 := [mp #148 #651]: #647 -#621 := (not #647) +#22 := (f8 #10) +#97 := (= #9 #22) +#653 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #633) #97) +#101 := (forall (vars (?v0 S2) (?v1 S3)) #97) +#656 := (iff #101 #653) +#654 := (iff #97 #97) +#655 := [refl]: #654 +#657 := [quant-intro #655]: #656 +#134 := (~ #101 #101) +#153 := (~ #97 #97) +#154 := [refl]: #153 +#135 := [nnf-pos #154]: #134 +#23 := (= #22 #9) +#24 := (forall (vars (?v0 S2) (?v1 S3)) #23) +#102 := (iff #24 #101) +#99 := (iff #23 #97) +#100 := [rewrite]: #99 +#103 := [quant-intro #100]: #102 +#96 := [asserted]: #24 +#106 := [mp #96 #103]: #101 +#155 := [mp~ #106 #135]: #101 +#658 := [mp #155 #657]: #653 +#621 := (not #653) #632 := (or #621 #628) #622 := [quant-inst #43 #46]: #632 -#600 := [unit-resolution #622 #652]: #628 +#600 := [unit-resolution #622 #658]: #628 #601 := [symm #600]: #604 #314 := [monotonicity #601]: #605 #596 := [trans #314 #316]: #318 #590 := (= #42 f11) -#280 := (f8 #39) +#280 := (f7 #39) #588 := (= #280 f11) #285 := (= f11 #280) #270 := (or #269 #285) #271 := [quant-inst #37 #38]: #270 -#597 := [unit-resolution #271 #658]: #285 +#597 := [unit-resolution #271 #652]: #285 #589 := [symm #597]: #588 #595 := (= #42 #280) #594 := (= #41 #39) #309 := (= #39 #41) #293 := (or #621 #309) #294 := [quant-inst #36 #39]: #293 -#310 := [unit-resolution #294 #652]: #309 +#310 := [unit-resolution #294 #658]: #309 #598 := [symm #310]: #594 #599 := [monotonicity #598]: #595 #585 := [trans #599 #589]: #590 @@ -50960,7 +50960,7 @@ #435 := [unit-resolution #235 #434]: #304 [unit-resolution #435 #436]: false unsat -c3d12f254b9672d4ea71a3aff4f3729162212903 103 0 +20f57d480df22411665e8be01511bda0544a754c 103 0 #2 := false decl f7 :: S2 #24 := f7 @@ -50989,10 +50989,10 @@ #580 := (iff #59 #59) #581 := [refl]: #580 #583 := [quant-intro #581]: #582 -#87 := (~ #63 #63) -#85 := (~ #59 #59) -#86 := [refl]: #85 -#88 := [nnf-pos #86]: #87 +#84 := (~ #63 #63) +#83 := (~ #59 #59) +#96 := [refl]: #83 +#85 := [nnf-pos #96]: #84 #15 := (= #14 #9) #16 := (forall (vars (?v0 S2) (?v1 S2)) #15) #64 := (iff #16 #63) @@ -51001,8 +51001,8 @@ #65 := [quant-intro #62]: #64 #58 := [asserted]: #16 #68 := [mp #58 #65]: #63 -#91 := [mp~ #68 #88]: #63 -#584 := [mp #91 #583]: #579 +#97 := [mp~ #68 #85]: #63 +#584 := [mp #97 #583]: #579 #353 := (not #579) #560 := (or #353 #244) #232 := [quant-inst #23 #24]: #560 @@ -51016,10 +51016,10 @@ #574 := (iff #52 #52) #575 := [refl]: #574 #577 := [quant-intro #575]: #576 -#89 := (~ #55 #55) -#94 := (~ #52 #52) -#95 := [refl]: #94 -#90 := [nnf-pos #95]: #89 +#94 := (~ #55 #55) +#92 := (~ #52 #52) +#93 := [refl]: #92 +#95 := [nnf-pos #93]: #94 #12 := (= #11 #8) #13 := (forall (vars (?v0 S2) (?v1 S2)) #12) #56 := (iff #13 #55) @@ -51028,8 +51028,8 @@ #57 := [quant-intro #54]: #56 #51 := [asserted]: #13 #60 := [mp #51 #57]: #55 -#84 := [mp~ #60 #90]: #55 -#578 := [mp #84 #577]: #573 +#81 := [mp~ #60 #95]: #55 +#578 := [mp #81 #577]: #573 #227 := (not #573) #564 := (or #227 #247) #566 := [quant-inst #23 #24]: #564 @@ -51064,7 +51064,7 @@ #208 := [unit-resolution #174 #547]: #243 [unit-resolution #208 #209]: false unsat -df71e79ae4d3b6ca6b9e37bd4464bcbb19ac1ad4 111 0 +bf86a55d7b42d914595abb0b42ed4b6837aa227f 111 0 #2 := false decl f5 :: (-> S3 S2) decl f9 :: S3 @@ -51117,10 +51117,10 @@ #593 := (iff #64 #64) #594 := [refl]: #593 #596 := [quant-intro #594]: #595 -#100 := (~ #68 #68) -#98 := (~ #64 #64) -#99 := [refl]: #98 -#101 := [nnf-pos #99]: #100 +#97 := (~ #68 #68) +#96 := (~ #64 #64) +#113 := [refl]: #96 +#98 := [nnf-pos #113]: #97 #15 := (= #14 #9) #16 := (forall (vars (?v0 S2) (?v1 S2)) #15) #69 := (iff #16 #68) @@ -51129,8 +51129,8 @@ #70 := [quant-intro #67]: #69 #63 := [asserted]: #16 #73 := [mp #63 #70]: #68 -#104 := [mp~ #73 #101]: #68 -#597 := [mp #104 #596]: #592 +#114 := [mp~ #73 #98]: #68 +#597 := [mp #114 #596]: #592 #187 := (not #592) #573 := (or #187 #240) #245 := [quant-inst #25 #24]: #573 @@ -51147,10 +51147,10 @@ #587 := (iff #57 #57) #588 := [refl]: #587 #590 := [quant-intro #588]: #589 -#102 := (~ #60 #60) -#107 := (~ #57 #57) -#108 := [refl]: #107 -#103 := [nnf-pos #108]: #102 +#111 := (~ #60 #60) +#109 := (~ #57 #57) +#110 := [refl]: #109 +#112 := [nnf-pos #110]: #111 #12 := (= #11 #8) #13 := (forall (vars (?v0 S2) (?v1 S2)) #12) #61 := (iff #13 #60) @@ -51159,8 +51159,8 @@ #62 := [quant-intro #59]: #61 #56 := [asserted]: #13 #65 := [mp #56 #62]: #60 -#97 := [mp~ #65 #103]: #60 -#591 := [mp #97 #590]: #586 +#95 := [mp~ #65 #112]: #60 +#591 := [mp #95 #590]: #586 #169 := (not #586) #256 := (or #169 #254) #247 := [quant-inst #24 #25]: #256 @@ -51176,7 +51176,7 @@ #93 := [not-or-elim #90]: #92 [unit-resolution #93 #566]: false unsat -e078bb600df2bd0f41e49114d3117704e2a9b9b4 117 0 +bc5180d3ea9553f4ce1005fa76475b6a88104f2a 117 0 #2 := false decl f4 :: (-> S2 S2 S3) decl f3 :: (-> S3 S2) @@ -51206,10 +51206,10 @@ #573 := (iff #51 #51) #574 := [refl]: #573 #576 := [quant-intro #574]: #575 -#88 := (~ #54 #54) -#93 := (~ #51 #51) -#94 := [refl]: #93 -#89 := [nnf-pos #94]: #88 +#93 := (~ #54 #54) +#91 := (~ #51 #51) +#92 := [refl]: #91 +#94 := [nnf-pos #92]: #93 #12 := (= #11 #8) #13 := (forall (vars (?v0 S2) (?v1 S2)) #12) #55 := (iff #13 #54) @@ -51218,8 +51218,8 @@ #56 := [quant-intro #53]: #55 #50 := [asserted]: #13 #59 := [mp #50 #56]: #54 -#83 := [mp~ #59 #89]: #54 -#577 := [mp #83 #576]: #572 +#80 := [mp~ #59 #94]: #54 +#577 := [mp #80 #576]: #572 #563 := (not #572) #565 := (or #563 #243) #220 := [quant-inst #25 #24]: #565 @@ -51267,10 +51267,10 @@ #587 := (iff #66 #66) #588 := [refl]: #587 #590 := [quant-intro #588]: #589 -#95 := (~ #70 #70) -#91 := (~ #66 #66) -#92 := [refl]: #91 -#96 := [nnf-pos #92]: #95 +#85 := (~ #70 #70) +#97 := (~ #66 #66) +#98 := [refl]: #97 +#86 := [nnf-pos #98]: #85 #21 := (= #20 #17) #22 := (forall (vars (?v0 S3)) #21) #71 := (iff #22 #70) @@ -51279,8 +51279,8 @@ #72 := [quant-intro #69]: #71 #65 := [asserted]: #22 #75 := [mp #65 #72]: #70 -#97 := [mp~ #75 #96]: #70 -#591 := [mp #97 #590]: #586 +#99 := [mp~ #75 #86]: #70 +#591 := [mp #99 #590]: #586 #569 := (not #586) #564 := (or #569 #559) #570 := [quant-inst #23]: #564 @@ -51294,7 +51294,7 @@ #548 := [unit-resolution #173 #210]: #242 [unit-resolution #548 #554]: false unsat -e0d0d958c704cd740ed0ffb718fec05abf4295fd 82 0 +4f529fd4091f297cfc050e5da16cb9f0bd732f8b 82 0 #2 := false decl f4 :: (-> S2 S3 S3) decl f6 :: S3 @@ -51341,10 +51341,10 @@ #708 := (iff #31 #31) #709 := [refl]: #708 #711 := [quant-intro #709]: #710 -#194 := (~ #32 #32) -#192 := (~ #31 #31) -#193 := [refl]: #192 -#195 := [nnf-pos #193]: #194 +#167 := (~ #32 #32) +#172 := (~ #31 #31) +#166 := [refl]: #172 +#164 := [nnf-pos #166]: #167 #27 := (= f6 #10) #28 := (not #27) #29 := (forall (vars (?v0 S2) (?v1 S3)) #28) @@ -51356,8 +51356,8 @@ #123 := [quant-intro #121]: #122 #116 := [asserted]: #29 #126 := [mp #116 #123]: #32 -#196 := [mp~ #126 #195]: #32 -#712 := [mp #196 #711]: #707 +#165 := [mp~ #126 #164]: #32 +#712 := [mp #165 #711]: #707 #289 := (not #707) #362 := (or #289 #349) #356 := (= #269 f6) @@ -51377,7 +51377,7 @@ #686 := [unit-resolution #675 #712]: #349 [unit-resolution #686 #323]: false unsat -08e36b4206627321e9ef13c16c3c6ff1083524c9 69 0 +3d691bfff446966153e91c446604c6142068edd9 69 0 #2 := false decl f4 :: (-> S2 S3 S3) decl f6 :: S3 @@ -51418,10 +51418,10 @@ #710 := (iff #31 #31) #711 := [refl]: #710 #713 := [quant-intro #711]: #712 -#196 := (~ #32 #32) -#194 := (~ #31 #31) -#195 := [refl]: #194 -#197 := [nnf-pos #195]: #196 +#169 := (~ #32 #32) +#174 := (~ #31 #31) +#168 := [refl]: #174 +#166 := [nnf-pos #168]: #169 #27 := (= f6 #10) #28 := (not #27) #29 := (forall (vars (?v0 S2) (?v1 S3)) #28) @@ -51433,8 +51433,8 @@ #125 := [quant-intro #123]: #124 #118 := [asserted]: #29 #128 := [mp #118 #125]: #32 -#198 := [mp~ #128 #197]: #32 -#714 := [mp #198 #713]: #709 +#167 := [mp~ #128 #166]: #32 +#714 := [mp #167 #713]: #709 #364 := (not #709) #649 := (or #364 #150) #490 := (or #364 #62) @@ -51447,7 +51447,7 @@ #639 := [mp #635 #638]: #649 [unit-resolution #639 #714 #162]: false unsat -e3c83bfe7d36b6dbe01f810a411eecc94e2d0020 136 0 +4c1447056b8cb4c1d1990c18e936eb64adf50f7a 136 0 #2 := false decl f4 :: (-> S2 S3 S3) decl f6 :: S3 @@ -51487,13 +51487,13 @@ #10 := (f4 #8 #9) #700 := (pattern #10 #19) #109 := (= #9 #18) -#163 := (not #109) +#200 := (not #109) #106 := (= #8 #17) -#162 := (not #106) -#160 := (or #162 #163) -#161 := (not #160) +#199 := (not #106) +#201 := (or #199 #200) +#202 := (not #201) #102 := (= #10 #19) -#205 := (iff #102 #161) +#205 := (iff #102 #202) #701 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S2) (?v3 S3)) (:pat #700) #205) #208 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S2) (?v3 S3)) #205) #704 := (iff #208 #701) @@ -51505,14 +51505,14 @@ #118 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S2) (?v3 S3)) #115) #209 := (iff #118 #208) #206 := (iff #115 #205) -#203 := (iff #112 #161) +#203 := (iff #112 #202) #204 := [rewrite]: #203 #207 := [monotonicity #204]: #206 #210 := [quant-intro #207]: #209 -#191 := (~ #118 #118) +#175 := (~ #118 #118) #177 := (~ #115 #115) #178 := [refl]: #177 -#192 := [nnf-pos #178]: #191 +#176 := [nnf-pos #178]: #175 #22 := (= #18 #9) #21 := (= #17 #8) #23 := (and #21 #22) @@ -51533,8 +51533,8 @@ #120 := [quant-intro #117]: #119 #101 := [asserted]: #25 #123 := [mp #101 #120]: #118 -#193 := [mp~ #123 #192]: #118 -#211 := [mp #193 #210]: #208 +#173 := [mp~ #123 #176]: #118 +#211 := [mp #173 #210]: #208 #706 := [mp #211 #705]: #701 #660 := (not #701) #661 := (or #660 #310) @@ -51584,7 +51584,7 @@ #656 := [mp #383 #277]: #661 [unit-resolution #656 #706 #616]: false unsat -8500def9bd98753ab4a7655e9231b63171fa5f04 50 0 +2c91ac71f41255b8ebcce1fb25dd8a7435a5aefc 50 0 #2 := false decl f3 :: (-> S3 S2) decl f4 :: (-> S2 S3 S3) @@ -51616,10 +51616,10 @@ #683 := (iff #83 #83) #684 := [refl]: #683 #686 := [quant-intro #684]: #685 -#170 := (~ #86 #86) -#177 := (~ #83 #83) -#178 := [refl]: #177 -#171 := [nnf-pos #178]: #170 +#163 := (~ #86 #86) +#125 := (~ #83 #83) +#162 := [refl]: #125 +#164 := [nnf-pos #162]: #163 #12 := (= #11 #8) #13 := (forall (vars (?v0 S2) (?v1 S3)) #12) #87 := (iff #13 #86) @@ -51628,14 +51628,14 @@ #88 := [quant-intro #85]: #87 #82 := [asserted]: #13 #91 := [mp #82 #88]: #86 -#125 := [mp~ #91 #171]: #86 -#687 := [mp #125 #686]: #682 +#175 := [mp~ #91 #164]: #86 +#687 := [mp #175 #686]: #682 #342 := (not #682) #676 := (or #342 #146) #677 := [quant-inst #57 #58]: #676 [unit-resolution #677 #687 #154]: false unsat -a4455fa26a2bf5d21921399b4d6f0e721daff1a2 50 0 +3ac68e901beccda437cc98a0bd632fd658e36767 50 0 #2 := false decl f5 :: (-> S3 S3) decl f4 :: (-> S2 S3 S3) @@ -51667,10 +51667,10 @@ #689 := (iff #90 #90) #690 := [refl]: #689 #692 := [quant-intro #690]: #691 -#158 := (~ #94 #94) -#165 := (~ #90 #90) -#166 := [refl]: #165 -#159 := [nnf-pos #166]: #158 +#174 := (~ #94 #94) +#176 := (~ #90 #90) +#173 := [refl]: #176 +#171 := [nnf-pos #173]: #174 #15 := (= #14 #9) #16 := (forall (vars (?v0 S2) (?v1 S3)) #15) #95 := (iff #16 #94) @@ -51679,14 +51679,14 @@ #96 := [quant-intro #93]: #95 #89 := [asserted]: #16 #99 := [mp #89 #96]: #94 -#160 := [mp~ #99 #159]: #94 -#693 := [mp #160 #692]: #688 +#172 := [mp~ #99 #171]: #94 +#693 := [mp #172 #692]: #688 #674 := (not #688) #680 := (or #674 #146) #670 := [quant-inst #57 #58]: #680 [unit-resolution #670 #693 #154]: false unsat -65f5926fa55a56a20b93bf43ca8b606d7a725e83 56 0 +8142fde9b86379b43ddc5095b2fea794eefa6812 56 0 #2 := false decl f3 :: (-> S3 S2) decl f4 :: (-> S2 S3 S3) @@ -51724,10 +51724,10 @@ #686 := (iff #86 #86) #687 := [refl]: #686 #689 := [quant-intro #687]: #688 -#169 := (~ #89 #89) +#166 := (~ #89 #89) #128 := (~ #86 #86) -#168 := [refl]: #128 -#159 := [nnf-pos #168]: #169 +#165 := [refl]: #128 +#167 := [nnf-pos #165]: #166 #12 := (= #11 #8) #13 := (forall (vars (?v0 S2) (?v1 S3)) #12) #90 := (iff #13 #89) @@ -51736,14 +51736,14 @@ #91 := [quant-intro #88]: #90 #85 := [asserted]: #13 #94 := [mp #85 #91]: #89 -#160 := [mp~ #94 #159]: #89 -#690 := [mp #160 #689]: #685 +#178 := [mp~ #94 #167]: #89 +#690 := [mp #178 #689]: #685 #618 := (not #685) #436 := (or #618 #149) #429 := [quant-inst #57 #61]: #436 [unit-resolution #429 #690 #157]: false unsat -d48bb23843eefa7d190bfd37fdd1c5737b414ba9 56 0 +4c528c48e59636ae8904df7a63f06102514e82cf 56 0 #2 := false decl f5 :: (-> S3 S3) decl f4 :: (-> S2 S3 S3) @@ -51781,10 +51781,10 @@ #692 := (iff #93 #93) #693 := [refl]: #692 #695 := [quant-intro #693]: #694 -#165 := (~ #97 #97) -#163 := (~ #93 #93) -#164 := [refl]: #163 -#170 := [nnf-pos #164]: #165 +#177 := (~ #97 #97) +#179 := (~ #93 #93) +#176 := [refl]: #179 +#174 := [nnf-pos #176]: #177 #15 := (= #14 #9) #16 := (forall (vars (?v0 S2) (?v1 S3)) #15) #98 := (iff #16 #97) @@ -51793,14 +51793,14 @@ #99 := [quant-intro #96]: #98 #92 := [asserted]: #16 #102 := [mp #92 #99]: #97 -#171 := [mp~ #102 #170]: #97 -#696 := [mp #171 #695]: #691 +#175 := [mp~ #102 #174]: #97 +#696 := [mp #175 #695]: #691 #600 := (not #691) #433 := (or #600 #149) #434 := [quant-inst #57 #61]: #433 [unit-resolution #434 #696 #157]: false unsat -6b5ffaa8a4665068d38b31a11461bd89d95e477d 95 0 +d57de5e3a80dc81f7c8246af61305a83e94d9d64 95 0 #2 := false decl f3 :: (-> S3 S2) decl f5 :: (-> S3 S3) @@ -51836,10 +51836,10 @@ #693 := (iff #94 #94) #694 := [refl]: #693 #696 := [quant-intro #694]: #695 -#162 := (~ #98 #98) -#160 := (~ #94 #94) -#161 := [refl]: #160 -#163 := [nnf-pos #161]: #162 +#178 := (~ #98 #98) +#180 := (~ #94 #94) +#177 := [refl]: #180 +#175 := [nnf-pos #177]: #178 #15 := (= #14 #9) #16 := (forall (vars (?v0 S2) (?v1 S3)) #15) #99 := (iff #16 #98) @@ -51848,8 +51848,8 @@ #100 := [quant-intro #97]: #99 #93 := [asserted]: #16 #103 := [mp #93 #100]: #98 -#164 := [mp~ #103 #163]: #98 -#697 := [mp #164 #696]: #692 +#176 := [mp~ #103 #175]: #98 +#697 := [mp #176 #696]: #692 #601 := (not #692) #435 := (or #601 #437) #421 := [quant-inst #57 #61]: #435 @@ -51866,10 +51866,10 @@ #687 := (iff #87 #87) #688 := [refl]: #687 #690 := [quant-intro #688]: #689 -#173 := (~ #90 #90) +#167 := (~ #90 #90) #129 := (~ #87 #87) -#172 := [refl]: #129 -#165 := [nnf-pos #172]: #173 +#166 := [refl]: #129 +#168 := [nnf-pos #166]: #167 #12 := (= #11 #8) #13 := (forall (vars (?v0 S2) (?v1 S3)) #12) #91 := (iff #13 #90) @@ -51878,8 +51878,8 @@ #92 := [quant-intro #89]: #91 #86 := [asserted]: #13 #95 := [mp #86 #92]: #90 -#166 := [mp~ #95 #165]: #90 -#691 := [mp #166 #690]: #686 +#179 := [mp~ #95 #168]: #90 +#691 := [mp #179 #690]: #686 #619 := (not #686) #515 := (or #619 #504) #516 := [quant-inst #58 #60]: #515 @@ -51896,7 +51896,7 @@ #158 := [mp #148 #155]: #153 [unit-resolution #158 #410]: false unsat -3c9960275d5862cae6ae020dd19199bbe60db8f3 71 0 +2396070c784c90f1fb45b2c026662e0b8ae4811a 71 0 #2 := false decl f5 :: (-> S3 S3) decl f4 :: (-> S2 S3 S3) @@ -51931,10 +51931,10 @@ #693 := (iff #94 #94) #694 := [refl]: #693 #696 := [quant-intro #694]: #695 -#166 := (~ #98 #98) -#164 := (~ #94 #94) -#165 := [refl]: #164 -#171 := [nnf-pos #165]: #166 +#178 := (~ #98 #98) +#180 := (~ #94 #94) +#177 := [refl]: #180 +#175 := [nnf-pos #177]: #178 #15 := (= #14 #9) #16 := (forall (vars (?v0 S2) (?v1 S3)) #15) #99 := (iff #16 #98) @@ -51943,8 +51943,8 @@ #100 := [quant-intro #97]: #99 #93 := [asserted]: #16 #103 := [mp #93 #100]: #98 -#172 := [mp~ #103 #171]: #98 -#697 := [mp #172 #696]: #692 +#176 := [mp~ #103 #175]: #98 +#697 := [mp #176 #696]: #692 #601 := (not #692) #435 := (or #601 #437) #421 := [quant-inst #57 #61]: #435 @@ -51968,7 +51968,7 @@ #158 := [mp #148 #155]: #153 [unit-resolution #158 #410]: false unsat -d5569cbebc9c95b668e726d7b9e33fb967151908 97 0 +db423730ba0ca064d1048e6169dad21fed1e792c 97 0 #2 := false decl f3 :: (-> S4 S2) decl f6 :: (-> S5 S4) @@ -52002,10 +52002,10 @@ #760 := (iff #123 #123) #761 := [refl]: #760 #763 := [quant-intro #761]: #762 -#213 := (~ #127 #127) -#211 := (~ #123 #123) -#212 := [refl]: #211 -#220 := [nnf-pos #212]: #213 +#208 := (~ #127 #127) +#213 := (~ #123 #123) +#207 := [refl]: #213 +#205 := [nnf-pos #207]: #208 #27 := (= #26 #23) #28 := (forall (vars (?v0 S4) (?v1 S5)) #27) #128 := (iff #28 #127) @@ -52014,8 +52014,8 @@ #129 := [quant-intro #126]: #128 #122 := [asserted]: #28 #132 := [mp #122 #129]: #127 -#221 := [mp~ #132 #220]: #127 -#764 := [mp #221 #763]: #759 +#206 := [mp~ #132 #205]: #127 +#764 := [mp #206 #763]: #759 #375 := (not #759) #376 := (or #375 #712) #714 := [quant-inst #74 #41]: #376 @@ -52036,10 +52036,10 @@ #739 := (iff #100 #100) #740 := [refl]: #739 #742 := [quant-intro #740]: #741 -#219 := (~ #103 #103) +#210 := (~ #103 #103) #166 := (~ #100 #100) -#218 := [refl]: #166 -#209 := [nnf-pos #218]: #219 +#209 := [refl]: #166 +#211 := [nnf-pos #209]: #210 #12 := (= #11 #8) #13 := (forall (vars (?v0 S2) (?v1 S3)) #12) #104 := (iff #13 #103) @@ -52048,8 +52048,8 @@ #105 := [quant-intro #102]: #104 #99 := [asserted]: #13 #108 := [mp #99 #105]: #103 -#210 := [mp~ #108 #209]: #103 -#743 := [mp #210 #742]: #738 +#222 := [mp~ #108 #211]: #103 +#743 := [mp #222 #742]: #738 #321 := (not #738) #408 := (or #321 #406) #399 := [quant-inst #72 #73]: #408 @@ -52066,7 +52066,7 @@ #195 := [mp #185 #192]: #190 [unit-resolution #195 #723]: false unsat -4d4a4abaf885c3c42662c956779a33f9969b3641 97 0 +e89d19faaf82ed94357ec4677d8f827dcc26761d 97 0 #2 := false decl f5 :: (-> S4 S3) decl f6 :: (-> S5 S4) @@ -52100,10 +52100,10 @@ #760 := (iff #123 #123) #761 := [refl]: #760 #763 := [quant-intro #761]: #762 -#213 := (~ #127 #127) -#211 := (~ #123 #123) -#212 := [refl]: #211 -#220 := [nnf-pos #212]: #213 +#208 := (~ #127 #127) +#213 := (~ #123 #123) +#207 := [refl]: #213 +#205 := [nnf-pos #207]: #208 #27 := (= #26 #23) #28 := (forall (vars (?v0 S4) (?v1 S5)) #27) #128 := (iff #28 #127) @@ -52112,8 +52112,8 @@ #129 := [quant-intro #126]: #128 #122 := [asserted]: #28 #132 := [mp #122 #129]: #127 -#221 := [mp~ #132 #220]: #127 -#764 := [mp #221 #763]: #759 +#206 := [mp~ #132 #205]: #127 +#764 := [mp #206 #763]: #759 #375 := (not #759) #376 := (or #375 #712) #714 := [quant-inst #74 #41]: #376 @@ -52134,10 +52134,10 @@ #745 := (iff #107 #107) #746 := [refl]: #745 #748 := [quant-intro #746]: #747 -#199 := (~ #111 #111) -#204 := (~ #107 #107) -#205 := [refl]: #204 -#200 := [nnf-pos #205]: #199 +#221 := (~ #111 #111) +#223 := (~ #107 #107) +#220 := [refl]: #223 +#218 := [nnf-pos #220]: #221 #15 := (= #14 #9) #16 := (forall (vars (?v0 S2) (?v1 S3)) #15) #112 := (iff #16 #111) @@ -52146,8 +52146,8 @@ #113 := [quant-intro #110]: #112 #106 := [asserted]: #16 #116 := [mp #106 #113]: #111 -#201 := [mp~ #116 #200]: #111 -#749 := [mp #201 #748]: #744 +#219 := [mp~ #116 #218]: #111 +#749 := [mp #219 #748]: #744 #339 := (not #744) #412 := (or #339 #407) #409 := [quant-inst #72 #73]: #412 @@ -52276,7 +52276,7 @@ #101 := [not-or-elim #103]: #43 [unit-resolution #101 #277]: false unsat -9701cdd9448439fa34387c2ec3bdc4fe35ec7bdc 54 0 +0c2977c8c8618eef37974bd4a2fc3d59345d9965 54 0 #2 := false #38 := 3::Int decl f3 :: (-> S3 Int) @@ -52331,7 +52331,7 @@ #247 := [mp #241 #246]: #236 [unit-resolution #247 #196 #91]: false unsat -3a7987f9f2406e33255cc3f658f066dbd894644a 54 0 +d68134f72bff3c71be36dfe7e7a5d3d9aa42e109 54 0 #2 := false #39 := 4::Int decl f5 :: (-> S3 Int) @@ -52386,7 +52386,7 @@ #262 := [mp #256 #261]: #254 [unit-resolution #262 #202 #91]: false unsat -2a9b9fb7f75472ed7447a04c770c82842793429a 109 0 +df4cc6af0d8c7c1f4e2ce7f971d5bcdb24cc7842 109 0 #2 := false #39 := 4::Int #38 := 3::Int @@ -52496,7 +52496,7 @@ #270 := [trans #268 #261]: #269 [mp #270 #272]: false unsat -2e54a746615da0b9042b7a1c7abdcba21277b942 73 0 +c3ea340f2ca5088543fc4bdcf4ebe731f9a5f650 73 0 #2 := false decl f6 :: (-> Int Int S3 S4) decl f13 :: S3 @@ -52570,7 +52570,7 @@ #100 := [asserted]: #52 [unit-resolution #100 #345]: false unsat -a5cf3bd14553e66b05989b95f1712c3548d79c05 73 0 +68cdbe5843e8281a606da777ab86dc4c9c5028ae 73 0 #2 := false decl f6 :: (-> Int Int S3 S4) decl f13 :: S3 @@ -52644,7 +52644,7 @@ #100 := [asserted]: #52 [unit-resolution #100 #345]: false unsat -b59ea79b3381bb3b8446dda45524f635379fcd3e 211 0 +ff18e62b724360b80c3a974588e17e2bef964664 211 0 #2 := false decl f11 :: (-> S2 S4 S4) decl f10 :: (-> S2 S4 S4) @@ -52856,7 +52856,7 @@ #127 := [not-or-elim #126]: #125 [unit-resolution #127 #437]: false unsat -e55f9d76dda3b8c2c60cf7fba6ece493ac2093db 211 0 +d86a80a06ecde74cac9fcb7a0ce1d146b14bdff5 211 0 #2 := false decl f10 :: (-> S2 S4 S4) decl f11 :: (-> S2 S4 S4) @@ -53124,7 +53124,7 @@ #154 := [not-or-elim #153]: #152 [unit-resolution #154 #347]: false unsat -1a1dbb36df0b0fe92eb18b671d63ad44f5ac7c76 71 0 +3fc90649d66e9e3133ec6ffaaa72e92cae1906e4 71 0 #2 := false decl f12 :: (-> S3 S1) decl f20 :: S3 @@ -53169,30 +53169,30 @@ #693 := [monotonicity #167]: #691 #348 := [monotonicity #693]: #152 #372 := (not #149) -#205 := (not #146) -#480 := (iff #205 #372) +#196 := (not #146) +#480 := (iff #196 #372) #687 := [monotonicity #348]: #480 -#375 := [hypothesis]: #205 +#375 := [hypothesis]: #196 #359 := [mp #375 #687]: #372 #370 := (or #149 #146) -#206 := (iff #149 #205) +#197 := (iff #149 #196) #168 := (not #152) -#207 := (iff #168 #206) -#208 := [rewrite]: #207 +#198 := (iff #168 #197) +#199 := [rewrite]: #198 #170 := [not-or-elim #169]: #168 -#209 := [mp #170 #208]: #206 -#368 := (not #206) +#200 := [mp #170 #199]: #197 +#368 := (not #197) #369 := (or #149 #146 #368) #284 := [def-axiom]: #369 -#361 := [unit-resolution #284 #209]: #370 +#361 := [unit-resolution #284 #200]: #370 #354 := [unit-resolution #361 #375]: #149 #360 := [unit-resolution #354 #359]: false #694 := [lemma #360]: #146 #696 := [mp #694 #348]: #149 -#374 := (or #372 #205) -#373 := (or #372 #205 #368) +#374 := (or #372 #196) +#373 := (or #372 #196 #368) #301 := [def-axiom]: #373 -#371 := [unit-resolution #301 #209]: #374 +#371 := [unit-resolution #301 #200]: #374 #695 := [unit-resolution #371 #694]: #372 [unit-resolution #695 #696]: false unsat @@ -53252,7 +53252,7 @@ #152 := [not-or-elim #154]: #70 [unit-resolution #152 #347]: false unsat -3c5eeec3f72704eac255d0f1e9284d0d20ab0722 87 0 +5ac8b5530f88aae423bf81b2aa1ee58c0cb330b8 87 0 #2 := false decl f12 :: (-> S3 S1) decl f20 :: S3 @@ -53324,11 +53324,11 @@ #375 := [mp #391 #703]: #388 #386 := (or #151 #148) #189 := [not-or-elim #190]: #157 -#225 := [mp #189 #163]: #161 +#216 := [mp #189 #163]: #161 #384 := (not #161) #385 := (or #151 #148 #384) #300 := [def-axiom]: #385 -#377 := [unit-resolution #300 #225]: #386 +#377 := [unit-resolution #300 #216]: #386 #370 := [unit-resolution #377 #391]: #151 #376 := [unit-resolution #370 #375]: false #710 := [lemma #376]: #148 @@ -53336,11 +53336,11 @@ #390 := (or #388 #160) #389 := (or #388 #160 #384) #317 := [def-axiom]: #389 -#387 := [unit-resolution #317 #225]: #390 +#387 := [unit-resolution #317 #216]: #390 #711 := [unit-resolution #387 #710]: #388 [unit-resolution #711 #712]: false unsat -60180a7beca4718d4b909f1bb0ce2c0b84139dea 58 0 +da4bfd4a4625015f645fceb2c4dd17a2e385441a 58 0 #2 := false #65 := 3::Int decl f3 :: (-> S3 Int) @@ -53399,7 +53399,7 @@ #382 := [mp #376 #381]: #371 [unit-resolution #382 #269 #144]: false unsat -4e405ea4a814758902eec1be5c3ffd542fdce183 58 0 +74804e4af971e8af0af6d60bbc463cc104ca380a 58 0 #2 := false #66 := 4::Int decl f5 :: (-> S3 Int) @@ -53458,7 +53458,7 @@ #397 := [mp #391 #396]: #389 [unit-resolution #397 #275 #144]: false unsat -4ed86aa1fa601dd0a3ec30f70fe5685baa4f141b 105 0 +29db4bfc400e68d7454857ddd1753e5e2b87bacd 105 0 #2 := false decl f12 :: (-> S3 S1) decl f4 :: (-> Int Int S2 S3) @@ -53564,7 +53564,7 @@ #416 := [unit-resolution #364 #409]: #415 [unit-resolution #416 #414 #413]: false unsat -1106827b733d83eccb037f282dd3b096b2abf8d0 113 0 +66c763bb178c6b9cd687c2f7614b778b686167f0 113 0 #2 := false #66 := 4::Int #65 := 3::Int @@ -53678,7 +53678,7 @@ #405 := [trans #403 #396]: #404 [mp #405 #407]: false unsat -df574a4365f54e674a55945a532b21aa0b2dc1f4 77 0 +ddb9b0a02011f2cff7e6d056c403901bbad7783e 77 0 #2 := false decl f6 :: (-> Int Int S3 S4) decl f14 :: (-> S1 S6 S3) @@ -53756,7 +53756,7 @@ #153 := [asserted]: #81 [unit-resolution #153 #540]: false unsat -4e89c6fb18f25038439974fdc91cdb5ab18a8af0 77 0 +ff379bc11c0b6e1c82ab589c8fa86258b5520522 77 0 #2 := false decl f6 :: (-> Int Int S3 S4) decl f14 :: (-> S1 S6 S3) @@ -53834,7 +53834,7 @@ #153 := [asserted]: #81 [unit-resolution #153 #540]: false unsat -68e99be1e87e8d0678d49d93a4e91b40c95b96ee 409 0 +0b8858aa262cda85f2c91cda2489bcba0a45e777 409 0 #2 := false decl f19 :: (-> S3 S5 S5) decl f13 :: (-> S2 S5 S5) @@ -54244,7 +54244,7 @@ #202 := [not-or-elim #201]: #200 [unit-resolution #202 #799]: false unsat -b772603aaba9792fa294ee48d2ae093633041197 381 0 +c94a232e1e97412d949006cec91fe1baa089456e 381 0 #2 := false decl f12 :: (-> S2 S5 S5) decl f19 :: (-> S3 S5 S5) @@ -54626,7 +54626,7 @@ #202 := [not-or-elim #201]: #200 [unit-resolution #202 #800]: false unsat -4bea4bb3dde48b2c759327219b4fbf786808215a 371 0 +1ab1638cab30b8ac06816e79bcba1d425930e19f 371 0 #2 := false decl f13 :: (-> S2 S5 S5) decl f12 :: (-> S2 S5 S5) @@ -56028,27 +56028,27 @@ #157 := [mp #147 #154]: #152 [unit-resolution #157 #592]: false unsat -1e7ecf060cee9e61bb4405bc59df8efef823a76d 1 0 -unsat -ed7be74f50946d158793410899f40df6519543b4 1 0 +ce5c7dc705bde44a6d76052fa847da849e2a25e8 1 0 +unsat +38f8891a46367464bd66f6857c08f6855d01823e 1 0 unsat 4c4662b7eb4bf820d980581a2fc91e7581f1e6de 1 0 unsat 604fe1781a4518f475d867cbe05bb790967e29f4 1 0 unsat -6f6dde323bd21ef16ff088176bfa80c841d2a67b 1 0 -unsat -2d706ed8665b791195dfe7d8dde2163fe3e3d050 1 0 -unsat -5a9342008efdfdb5868bb4ac65d28f9a70022d8e 1 0 -unsat -1dce42cc11b180208dab2d5cc87ea493ae738340 1 0 -unsat -24790734475987e966a5f8cdaae6e4d6cf5db0c8 1 0 -unsat -af484a68410644745b3c7f43e2cb6a1551acf2b9 1 0 -unsat -ade3c87b7f2ac2ad5c1c06607a5d5f1178485104 1 0 +e130feb491d595cdd26b50ba606e05e82253e662 1 0 +unsat +c88f40069f119a5ef611e766b88fb27a33376469 1 0 +unsat +1ccf6da8e3379de961a4726c61dbce60d8a156a6 1 0 +unsat +08d35d263f3f330d899a684f508f9fb87a1c3c37 1 0 +unsat +e5d8720cfd335d72e9a747ea51260f137ff368d8 1 0 +unsat +3b9051c93ad8585444c4095c41043c5faac0a057 1 0 +unsat +ed62fdab40c4611ac5f753597d277d2ce675438e 1 0 unsat 1bb4f3696612274f0ada059e663e5df3e8c1753c 1 0 unsat @@ -56056,21 +56056,21 @@ unsat 99a4b89024a5ade20a17839e46c3c800a839dc73 1 0 unsat -25d7cafeec4877bd332c7a84d48d1e1bba149730 1 0 -unsat -46cecad9c27ddd660a32c43da02fbc077e4d2653 1 0 -unsat -9985536f3adcfa82b82611a2e3c65c48234903b7 1 0 -unsat -650e66124ceb469142418bdf9b727f4eb46000d3 1 0 -unsat -ad845af29980d8f1b8f9106555beea4a0787e50b 1 0 -unsat -1226a39ae26fb124fa2784c01feeda2fa8b7f164 1 0 -unsat -aeed0548e98a49111c97d9c505f2ddcc25a8f0a0 1 0 -unsat -6937351f88cbcd4ce38d156d36ca3f3b7400b010 1 0 +0cc8b3c4c079835098be13e075f80b6f8f429792 1 0 +unsat +bae675adb36d3ecf65e47295f7f3002cfca775bc 1 0 +unsat +fffdec69ce4b32df667e7e36f2aeb449eb96e502 1 0 +unsat +0f8130ffadb0ea5f83bcb9678a8a0a428f75ba11 1 0 +unsat +14c521dcb3c0dfca6046dd47445512db024842c8 1 0 +unsat +70449057ac865f7275970f313c73de2e2e0661aa 1 0 +unsat +e981571d927b81eda8506ab06352029e66ca215d 1 0 +unsat +47e9f293cb55e7b278a387a7b63c8dca7bb74490 1 0 unsat 660ffa7d21617f3d9be770c0a37b4fe52fc41f63 1 0 unsat @@ -56080,57 +56080,57 @@ unsat 990af511d3a0b46205abbd2ddd25c459f6e66c5a 1 0 unsat -cf85ae43503909529635475e22a3bb7409c56a5c 1 0 -unsat -fb00d7a0af114cd80f8efb9453ee0baf42d58298 1 0 -unsat -ea112adb690b675025a205ff95598c0e1bacd1b3 1 0 -unsat -cde5d9f95f561892bc84c1a943338cf0d427920f 1 0 -unsat -848677eef79eb7cb4fb3573c0d5c5fca34811251 1 0 -unsat -0e0faa00af41d5f14b5cb0a291dc7001b6276b81 1 0 -unsat -3ec23529e810aeac05c8d7c95856e437cc15481a 1 0 -unsat -991d721d9af19456ad333e832e6e1ff105598a2a 1 0 -unsat -c6d7a69a2fdeee85db63627aecd087b63d4f1c1c 1 0 -unsat -f67f5ba5a69d007092f7dd70dc2dbb1215926e11 1 0 +002f1c6e9a3a5a1ad6e0f4bf2560ee22d04cb4cb 1 0 +unsat +d744812ec0e9257421fb2e0a9820bfee04042dcc 1 0 +unsat +839f47953dc6c5ce7fe7d2130b5506e3817c2d88 1 0 +unsat +9524a9683d04ec02a17fa21f4043facff04c80fc 1 0 +unsat +756c9bc731ec5fb4e483e2dc1116d061c5c2f35f 1 0 +unsat +a92f055099a204d5b9347ef35e4b654dbde35134 1 0 +unsat +11baeb6d885300b41ed62e9fc3dbdf6f45620679 1 0 +unsat +0f60a11f2d707aedad80fb23ffcd23106c420369 1 0 +unsat +8f1cf6dbbd974f52bf4332e11e8e73c8154082e3 1 0 +unsat +4aa264ab45139cb17c9c3b017f0459151b0f481a 1 0 unsat 1839415a04580c458d9a54c09162d0c394cad86c 1 0 unsat 595084d6acf7cb9e727b2d71c11dcd5adfd678ca 1 0 unsat -ce8e551a982c6290b1be8781429cefd4f9165293 1 0 +da3f2f9dbdb7632f25c324bc059065293b4304af 1 0 unsat c271fe52291540adaf545c617359ed457de173b1 1 0 unsat d040cce0ec356b71ba4556c265407ab2f545e54c 1 0 unsat -674646d69af329d3589eeca7a6f731cbd7aabfb5 1 0 -unsat -789139e6d5722962adae903c7c6f741a024ed141 1 0 -unsat -1380018796c654e6dbfb3153a9601c28877a3114 1 0 -unsat -16408e8543328af45ac16df15c0d63f3fc509499 1 0 -unsat -0cbacef48453639efbd9117592087fa963979a9a 1 0 -unsat -4f76e31263dc24919943a2ac6835f5ab5cbb885d 1 0 -unsat -a76f56105de0da9e78f9f1ecf4de50bfa08478b8 1 0 -unsat -fb3320cb741f8a5fec9b3b50a2caeab3ab35af68 1 0 -unsat -4236ba058a6f6c1bacb0db47f2f621769329ff77 1 0 -unsat -fe15efedfaad3ad3884dcd453f022326a429c99f 1 0 -unsat -0adc18b99c93cda1aa22c7bd01d4133c76309534 1 0 +e84d0b7d00ab46d7f97ab3271f0a8f18ecad1e24 1 0 +unsat +ff0c89be3232fff2c8dff18a14f6e1f4a9ac4ae1 1 0 +unsat +0f8a977f38a5400888bac7277401dedadf78f509 1 0 +unsat +30ec8a1fe895a83c6ea00219963e48e3d67bd9ff 1 0 +unsat +d3a9054335fcb92f91170f4fd55fa45552749054 1 0 +unsat +cbb3b7fa6dd1f35f64da4884777bcb6ae345f930 1 0 +unsat +34a3d396bad33b535f04edd371ba357068e3fac7 1 0 +unsat +4ab52d9261a65d65d938eebf39a1245e87bddc05 1 0 +unsat +6aacde84f68949cd3f125396e017b084e6ee2625 1 0 +unsat +0747bde3f05b6cd6790fc2f582793f7b8bd560f9 1 0 +unsat +dc4bda1004c107889de0fd5c23e4a3df7f0c9a2a 1 0 unsat 49462927b92e2fe852e19ddabb722de885a6169e 1 0 unsat @@ -56781,2147 +56781,6 @@ #92 := [not-or-elim #91]: #90 [unit-resolution #92 #499]: false unsat -3ab56ce3ce9ea17007c9ef9659d24c1591a2f1dc 31 0 -#2 := false -decl f1 :: S1 -#4 := f1 -decl f8 :: (-> S4 S1) -decl f9 :: S4 -#32 := f9 -#33 := (f8 f9) -#34 := (= #33 f1) -#35 := (iff #34 #34) -#36 := (not #35) -#125 := (iff #36 false) -#1 := true -#120 := (not true) -#123 := (iff #120 false) -#124 := [rewrite]: #123 -#121 := (iff #36 #120) -#118 := (iff #35 true) -#109 := (= f1 #33) -#113 := (iff #109 #109) -#116 := (iff #113 true) -#117 := [rewrite]: #116 -#114 := (iff #35 #113) -#111 := (iff #34 #109) -#112 := [rewrite]: #111 -#115 := [monotonicity #112 #112]: #114 -#119 := [trans #115 #117]: #118 -#122 := [monotonicity #119]: #121 -#126 := [trans #122 #124]: #125 -#108 := [asserted]: #36 -[mp #108 #126]: false -unsat -99e99593c1b6e7784dba4d3a0aca41c7272cf4c1 58 0 -#2 := false -decl f3 :: (-> S2 S1) -decl f8 :: S2 -#33 := f8 -#34 := (f3 f8) -decl f1 :: S1 -#4 := f1 -#110 := (= f1 #34) -#35 := (= #34 f1) -#36 := (not #35) -#37 := (not #36) -#122 := (iff #37 #110) -#114 := (not #110) -#117 := (not #114) -#120 := (iff #117 #110) -#121 := [rewrite]: #120 -#118 := (iff #37 #117) -#115 := (iff #36 #114) -#112 := (iff #35 #110) -#113 := [rewrite]: #112 -#116 := [monotonicity #113]: #115 -#119 := [monotonicity #116]: #118 -#123 := [trans #119 #121]: #122 -#109 := [asserted]: #37 -#126 := [mp #109 #123]: #110 -#8 := (:var 0 S2) -#9 := (f3 #8) -#634 := (pattern #9) -#58 := (= f1 #9) -#61 := (not #58) -#635 := (forall (vars (?v0 S2)) (:pat #634) #61) -#64 := (forall (vars (?v0 S2)) #61) -#638 := (iff #64 #635) -#636 := (iff #61 #61) -#637 := [refl]: #636 -#639 := [quant-intro #637]: #638 -#140 := (~ #64 #64) -#138 := (~ #61 #61) -#139 := [refl]: #138 -#141 := [nnf-pos #139]: #140 -#10 := (= #9 f1) -#11 := (not #10) -#12 := (forall (vars (?v0 S2)) #11) -#65 := (iff #12 #64) -#62 := (iff #11 #61) -#59 := (iff #10 #58) -#60 := [rewrite]: #59 -#63 := [monotonicity #60]: #62 -#66 := [quant-intro #63]: #65 -#57 := [asserted]: #12 -#69 := [mp #57 #66]: #64 -#125 := [mp~ #69 #141]: #64 -#640 := [mp #125 #639]: #635 -#217 := (not #635) -#304 := (or #217 #114) -#218 := [quant-inst #33]: #304 -[unit-resolution #218 #640 #126]: false -unsat -d9322750c44c3fbc7422a30bcad6e401e2be0930 46 0 -#2 := false -decl f4 :: (-> S3 S1) -decl f8 :: S3 -#33 := f8 -#34 := (f4 f8) -decl f1 :: S1 -#4 := f1 -#109 := (= f1 #34) -#113 := (not #109) -#35 := (= #34 f1) -#36 := (not #35) -#114 := (iff #36 #113) -#111 := (iff #35 #109) -#112 := [rewrite]: #111 -#115 := [monotonicity #112]: #114 -#108 := [asserted]: #36 -#118 := [mp #108 #115]: #113 -#13 := (:var 0 S3) -#14 := (f4 #13) -#633 := (pattern #14) -#67 := (= f1 #14) -#634 := (forall (vars (?v0 S3)) (:pat #633) #67) -#71 := (forall (vars (?v0 S3)) #67) -#637 := (iff #71 #634) -#635 := (iff #67 #67) -#636 := [refl]: #635 -#638 := [quant-intro #636]: #637 -#120 := (~ #71 #71) -#119 := (~ #67 #67) -#134 := [refl]: #119 -#121 := [nnf-pos #134]: #120 -#15 := (= #14 f1) -#16 := (forall (vars (?v0 S3)) #15) -#72 := (iff #16 #71) -#69 := (iff #15 #67) -#70 := [rewrite]: #69 -#73 := [quant-intro #70]: #72 -#66 := [asserted]: #16 -#76 := [mp #66 #73]: #71 -#135 := [mp~ #76 #121]: #71 -#639 := [mp #135 #638]: #634 -#209 := (not #634) -#296 := (or #209 #109) -#210 := [quant-inst #33]: #296 -[unit-resolution #210 #639 #118]: false -unsat -b2f7b9c42d68e0ecab24c1bc7abe7e061806dd00 119 0 -#2 := false -decl f5 :: (-> S3 S3 S4 S1) -decl f11 :: S4 -#41 := f11 -decl f10 :: S3 -#40 := f10 -decl f9 :: S3 -#39 := f9 -#42 := (f5 f9 f10 f11) -decl f1 :: S1 -#4 := f1 -#129 := (= f1 #42) -#148 := (not #129) -#652 := [hypothesis]: #148 -decl f6 :: (-> S3 S4 S1) -#46 := (f6 f10 f11) -#136 := (= f1 #46) -#44 := (f6 f9 f11) -#133 := (= f1 #44) -#139 := (or #133 #136) -#340 := (or #139 #129) -#149 := (iff #139 #148) -#47 := (= #46 f1) -#45 := (= #44 f1) -#48 := (or #45 #47) -#43 := (= #42 f1) -#49 := (iff #43 #48) -#50 := (not #49) -#152 := (iff #50 #149) -#142 := (iff #129 #139) -#145 := (not #142) -#150 := (iff #145 #149) -#151 := [rewrite]: #150 -#146 := (iff #50 #145) -#143 := (iff #49 #142) -#140 := (iff #48 #139) -#137 := (iff #47 #136) -#138 := [rewrite]: #137 -#134 := (iff #45 #133) -#135 := [rewrite]: #134 -#141 := [monotonicity #135 #138]: #140 -#131 := (iff #43 #129) -#132 := [rewrite]: #131 -#144 := [monotonicity #132 #141]: #143 -#147 := [monotonicity #144]: #146 -#153 := [trans #147 #151]: #152 -#128 := [asserted]: #50 -#156 := [mp #128 #153]: #149 -#266 := (not #149) -#339 := (or #139 #129 #266) -#336 := [def-axiom]: #339 -#319 := [unit-resolution #336 #156]: #340 -#324 := [unit-resolution #319 #652]: #139 -#326 := (not #139) -#655 := (or #129 #326) -#18 := (:var 0 S4) -#17 := (:var 1 S3) -#16 := (:var 2 S3) -#19 := (f5 #16 #17 #18) -#678 := (pattern #19) -#23 := (f6 #17 #18) -#96 := (= f1 #23) -#21 := (f6 #16 #18) -#93 := (= f1 #21) -#99 := (or #93 #96) -#89 := (= f1 #19) -#102 := (iff #89 #99) -#679 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) (:pat #678) #102) -#105 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #102) -#682 := (iff #105 #679) -#680 := (iff #102 #102) -#681 := [refl]: #680 -#683 := [quant-intro #681]: #682 -#160 := (~ #105 #105) -#174 := (~ #102 #102) -#175 := [refl]: #174 -#161 := [nnf-pos #175]: #160 -#24 := (= #23 f1) -#22 := (= #21 f1) -#25 := (or #22 #24) -#20 := (= #19 f1) -#26 := (iff #20 #25) -#27 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #26) -#106 := (iff #27 #105) -#103 := (iff #26 #102) -#100 := (iff #25 #99) -#97 := (iff #24 #96) -#98 := [rewrite]: #97 -#94 := (iff #22 #93) -#95 := [rewrite]: #94 -#101 := [monotonicity #95 #98]: #100 -#91 := (iff #20 #89) -#92 := [rewrite]: #91 -#104 := [monotonicity #92 #101]: #103 -#107 := [quant-intro #104]: #106 -#88 := [asserted]: #27 -#110 := [mp #88 #107]: #105 -#176 := [mp~ #110 #161]: #105 -#684 := [mp #176 #683]: #679 -#325 := (not #679) -#659 := (or #325 #142) -#660 := [quant-inst #39 #40 #41]: #659 -#312 := [unit-resolution #660 #684]: #142 -#661 := (or #145 #129 #326) -#662 := [def-axiom]: #661 -#296 := [unit-resolution #662 #312]: #655 -#639 := [unit-resolution #296 #324 #652]: false -#300 := [lemma #639]: #129 -#313 := (or #326 #148) -#656 := (or #326 #148 #266) -#658 := [def-axiom]: #656 -#445 := [unit-resolution #658 #156]: #313 -#301 := [unit-resolution #445 #300]: #326 -#302 := (or #148 #139) -#657 := (or #145 #148 #139) -#663 := [def-axiom]: #657 -#303 := [unit-resolution #663 #312]: #302 -[unit-resolution #303 #301 #300]: false -unsat -b364582b466f46f7d7a33b311dc9888a3ab60e44 154 0 -#2 := false -decl f3 :: (-> S3 S2 S1) -decl f10 :: S2 -#41 := f10 -decl f4 :: S3 -#8 := f4 -#330 := (f3 f4 f10) -decl f1 :: S1 -#4 := f1 -#327 := (= f1 #330) -decl f9 :: S3 -#40 := f9 -#44 := (f3 f9 f10) -#130 := (= f1 #44) -#331 := (or #130 #327) -decl f6 :: (-> S3 S3 S2 S1) -#42 := (f6 f9 f4 f10) -#126 := (= f1 #42) -#139 := (not #126) -#647 := [hypothesis]: #139 -#325 := (or #130 #126) -#140 := (iff #130 #139) -#45 := (= #44 f1) -#43 := (= #42 f1) -#46 := (iff #43 #45) -#47 := (not #46) -#143 := (iff #47 #140) -#133 := (iff #126 #130) -#136 := (not #133) -#141 := (iff #136 #140) -#142 := [rewrite]: #141 -#137 := (iff #47 #136) -#134 := (iff #46 #133) -#131 := (iff #45 #130) -#132 := [rewrite]: #131 -#128 := (iff #43 #126) -#129 := [rewrite]: #128 -#135 := [monotonicity #129 #132]: #134 -#138 := [monotonicity #135]: #137 -#144 := [trans #138 #142]: #143 -#125 := [asserted]: #47 -#147 := [mp #125 #144]: #140 -#237 := (not #140) -#324 := (or #130 #126 #237) -#238 := [def-axiom]: #324 -#239 := [unit-resolution #238 #147]: #325 -#649 := [unit-resolution #239 #647]: #130 -#653 := (not #331) -#293 := (or #126 #653) -#310 := (iff #126 #331) -#9 := (:var 0 S2) -#19 := (:var 1 S3) -#18 := (:var 2 S3) -#20 := (f6 #18 #19 #9) -#669 := (pattern #20) -#24 := (f3 #19 #9) -#93 := (= f1 #24) -#22 := (f3 #18 #9) -#90 := (= f1 #22) -#96 := (or #90 #93) -#86 := (= f1 #20) -#99 := (iff #86 #96) -#670 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) (:pat #669) #99) -#102 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #99) -#673 := (iff #102 #670) -#671 := (iff #99 #99) -#672 := [refl]: #671 -#674 := [quant-intro #672]: #673 -#151 := (~ #102 #102) -#165 := (~ #99 #99) -#166 := [refl]: #165 -#152 := [nnf-pos #166]: #151 -#25 := (= #24 f1) -#23 := (= #22 f1) -#26 := (or #23 #25) -#21 := (= #20 f1) -#27 := (iff #21 #26) -#28 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #27) -#103 := (iff #28 #102) -#100 := (iff #27 #99) -#97 := (iff #26 #96) -#94 := (iff #25 #93) -#95 := [rewrite]: #94 -#91 := (iff #23 #90) -#92 := [rewrite]: #91 -#98 := [monotonicity #92 #95]: #97 -#88 := (iff #21 #86) -#89 := [rewrite]: #88 -#101 := [monotonicity #89 #98]: #100 -#104 := [quant-intro #101]: #103 -#85 := [asserted]: #28 -#107 := [mp #85 #104]: #102 -#167 := [mp~ #107 #152]: #102 -#675 := [mp #167 #674]: #670 -#304 := (not #670) -#436 := (or #304 #310) -#643 := [quant-inst #40 #8 #41]: #436 -#292 := [unit-resolution #643 #675]: #310 -#644 := (not #310) -#302 := (or #644 #126 #653) -#307 := [def-axiom]: #302 -#294 := [unit-resolution #307 #292]: #293 -#632 := [unit-resolution #294 #647]: #653 -#326 := (not #130) -#315 := (or #331 #326) -#316 := [def-axiom]: #315 -#633 := [unit-resolution #316 #632 #649]: false -#634 := [lemma #633]: #126 -#635 := (or #139 #331) -#645 := (or #644 #139 #331) -#303 := [def-axiom]: #645 -#636 := [unit-resolution #303 #292]: #635 -#638 := [unit-resolution #636 #634]: #331 -#329 := (or #326 #139) -#317 := (or #326 #139 #237) -#328 := [def-axiom]: #317 -#257 := [unit-resolution #328 #147]: #329 -#640 := [unit-resolution #257 #634]: #326 -#648 := (or #653 #130 #327) -#654 := [def-axiom]: #648 -#278 := [unit-resolution #654 #640 #638]: #327 -#10 := (f3 f4 #9) -#655 := (pattern #10) -#68 := (= f1 #10) -#71 := (not #68) -#656 := (forall (vars (?v0 S2)) (:pat #655) #71) -#74 := (forall (vars (?v0 S2)) #71) -#659 := (iff #74 #656) -#657 := (iff #71 #71) -#658 := [refl]: #657 -#660 := [quant-intro #658]: #659 -#161 := (~ #74 #74) -#159 := (~ #71 #71) -#160 := [refl]: #159 -#162 := [nnf-pos #160]: #161 -#11 := (= #10 f1) -#12 := (not #11) -#13 := (forall (vars (?v0 S2)) #12) -#75 := (iff #13 #74) -#72 := (iff #12 #71) -#69 := (iff #11 #68) -#70 := [rewrite]: #69 -#73 := [monotonicity #70]: #72 -#76 := [quant-intro #73]: #75 -#67 := [asserted]: #13 -#79 := [mp #67 #76]: #74 -#146 := [mp~ #79 #162]: #74 -#661 := [mp #146 #660]: #656 -#650 := (not #327) -#631 := (not #656) -#637 := (or #631 #650) -#273 := [quant-inst #41]: #637 -[unit-resolution #273 #661 #278]: false -unsat -7d907ff63da540f87f38f6be518dd4d79ce5f3db 128 0 -#2 := false -decl f4 :: (-> S4 S3 S1) -decl f10 :: S3 -#41 := f10 -decl f5 :: S4 -#13 := f5 -#222 := (f4 f5 f10) -decl f1 :: S1 -#4 := f1 -#309 := (= f1 #222) -#636 := (not #309) -decl f9 :: S4 -#40 := f9 -#223 := (f4 f9 f10) -#310 := (= f1 #223) -#302 := (or #309 #310) -#287 := (not #302) -decl f6 :: (-> S4 S4 S3 S1) -#42 := (f6 f9 f5 f10) -#123 := (= f1 #42) -#242 := (iff #123 #302) -#14 := (:var 0 S3) -#19 := (:var 1 S4) -#18 := (:var 2 S4) -#20 := (f6 #18 #19 #14) -#654 := (pattern #20) -#24 := (f4 #19 #14) -#90 := (= f1 #24) -#22 := (f4 #18 #14) -#87 := (= f1 #22) -#93 := (or #87 #90) -#83 := (= f1 #20) -#96 := (iff #83 #93) -#655 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) (:pat #654) #96) -#99 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) #96) -#658 := (iff #99 #655) -#656 := (iff #96 #96) -#657 := [refl]: #656 -#659 := [quant-intro #657]: #658 -#136 := (~ #99 #99) -#150 := (~ #96 #96) -#151 := [refl]: #150 -#137 := [nnf-pos #151]: #136 -#25 := (= #24 f1) -#23 := (= #22 f1) -#26 := (or #23 #25) -#21 := (= #20 f1) -#27 := (iff #21 #26) -#28 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) #27) -#100 := (iff #28 #99) -#97 := (iff #27 #96) -#94 := (iff #26 #93) -#91 := (iff #25 #90) -#92 := [rewrite]: #91 -#88 := (iff #23 #87) -#89 := [rewrite]: #88 -#95 := [monotonicity #89 #92]: #94 -#85 := (iff #21 #83) -#86 := [rewrite]: #85 -#98 := [monotonicity #86 #95]: #97 -#101 := [quant-intro #98]: #100 -#82 := [asserted]: #28 -#104 := [mp #82 #101]: #99 -#152 := [mp~ #104 #137]: #99 -#660 := [mp #152 #659]: #655 -#316 := (not #655) -#295 := (or #316 #242) -#224 := (or #310 #309) -#311 := (iff #123 #224) -#632 := (or #316 #311) -#289 := (iff #632 #295) -#628 := (iff #295 #295) -#300 := [rewrite]: #628 -#315 := (iff #311 #242) -#313 := (iff #224 #302) -#314 := [rewrite]: #313 -#312 := [monotonicity #314]: #315 -#421 := [monotonicity #312]: #289 -#301 := [trans #421 #300]: #289 -#634 := [quant-inst #40 #13 #41]: #632 -#635 := [mp #634 #301]: #295 -#618 := [unit-resolution #635 #660]: #242 -#288 := (not #242) -#619 := (or #288 #287) -#127 := (not #123) -#43 := (= #42 f1) -#44 := (not #43) -#128 := (iff #44 #127) -#125 := (iff #43 #123) -#126 := [rewrite]: #125 -#129 := [monotonicity #126]: #128 -#122 := [asserted]: #44 -#132 := [mp #122 #129]: #127 -#631 := (or #288 #123 #287) -#272 := [def-axiom]: #631 -#622 := [unit-resolution #272 #132]: #619 -#258 := [unit-resolution #622 #618]: #287 -#637 := (or #302 #636) -#638 := [def-axiom]: #637 -#623 := [unit-resolution #638 #258]: #636 -#15 := (f4 f5 #14) -#647 := (pattern #15) -#75 := (= f1 #15) -#648 := (forall (vars (?v0 S3)) (:pat #647) #75) -#79 := (forall (vars (?v0 S3)) #75) -#651 := (iff #79 #648) -#649 := (iff #75 #75) -#650 := [refl]: #649 -#652 := [quant-intro #650]: #651 -#134 := (~ #79 #79) -#133 := (~ #75 #75) -#148 := [refl]: #133 -#135 := [nnf-pos #148]: #134 -#16 := (= #15 f1) -#17 := (forall (vars (?v0 S3)) #16) -#80 := (iff #17 #79) -#77 := (iff #16 #75) -#78 := [rewrite]: #77 -#81 := [quant-intro #78]: #80 -#74 := [asserted]: #17 -#84 := [mp #74 #81]: #79 -#149 := [mp~ #84 #135]: #79 -#653 := [mp #149 #652]: #648 -#620 := (not #648) -#621 := (or #620 #309) -#616 := [quant-inst #41]: #621 -[unit-resolution #616 #653 #623]: false -unsat -5cdc991e87f691c3b3a175ff2ede8c62635b20a0 146 0 -#2 := false -decl f5 :: (-> S3 S3 S4 S1) -decl f11 :: S4 -#41 := f11 -decl f9 :: S3 -#39 := f9 -decl f10 :: S3 -#40 := f10 -#44 := (f5 f10 f9 f11) -decl f1 :: S1 -#4 := f1 -#130 := (= f1 #44) -#326 := (not #130) -#42 := (f5 f9 f10 f11) -#126 := (= f1 #42) -#139 := (not #126) -#245 := [hypothesis]: #139 -#325 := (or #130 #126) -#140 := (iff #130 #139) -#45 := (= #44 f1) -#43 := (= #42 f1) -#46 := (iff #43 #45) -#47 := (not #46) -#143 := (iff #47 #140) -#133 := (iff #126 #130) -#136 := (not #133) -#141 := (iff #136 #140) -#142 := [rewrite]: #141 -#137 := (iff #47 #136) -#134 := (iff #46 #133) -#131 := (iff #45 #130) -#132 := [rewrite]: #131 -#128 := (iff #43 #126) -#129 := [rewrite]: #128 -#135 := [monotonicity #129 #132]: #134 -#138 := [monotonicity #135]: #137 -#144 := [trans #138 #142]: #143 -#125 := [asserted]: #47 -#147 := [mp #125 #144]: #140 -#237 := (not #140) -#324 := (or #130 #126 #237) -#238 := [def-axiom]: #324 -#239 := [unit-resolution #238 #147]: #325 -#624 := [unit-resolution #239 #245]: #130 -decl f6 :: (-> S3 S4 S1) -#330 := (f6 f9 f11) -#327 := (= f1 #330) -#331 := (f6 f10 f11) -#310 := (= f1 #331) -#647 := (or #310 #327) -#644 := (not #647) -#347 := (or #126 #644) -#634 := (iff #126 #647) -#18 := (:var 0 S4) -#17 := (:var 1 S3) -#16 := (:var 2 S3) -#19 := (f5 #16 #17 #18) -#669 := (pattern #19) -#23 := (f6 #17 #18) -#93 := (= f1 #23) -#21 := (f6 #16 #18) -#90 := (= f1 #21) -#96 := (or #90 #93) -#86 := (= f1 #19) -#99 := (iff #86 #96) -#670 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) (:pat #669) #99) -#102 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #99) -#673 := (iff #102 #670) -#671 := (iff #99 #99) -#672 := [refl]: #671 -#674 := [quant-intro #672]: #673 -#151 := (~ #102 #102) -#165 := (~ #99 #99) -#166 := [refl]: #165 -#152 := [nnf-pos #166]: #151 -#24 := (= #23 f1) -#22 := (= #21 f1) -#25 := (or #22 #24) -#20 := (= #19 f1) -#26 := (iff #20 #25) -#27 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #26) -#103 := (iff #27 #102) -#100 := (iff #26 #99) -#97 := (iff #25 #96) -#94 := (iff #24 #93) -#95 := [rewrite]: #94 -#91 := (iff #22 #90) -#92 := [rewrite]: #91 -#98 := [monotonicity #92 #95]: #97 -#88 := (iff #20 #86) -#89 := [rewrite]: #88 -#101 := [monotonicity #89 #98]: #100 -#104 := [quant-intro #101]: #103 -#85 := [asserted]: #27 -#107 := [mp #85 #104]: #102 -#167 := [mp~ #107 #152]: #102 -#675 := [mp #167 #674]: #670 -#643 := (not #670) -#631 := (or #643 #634) -#304 := (or #327 #310) -#436 := (iff #126 #304) -#637 := (or #643 #436) -#638 := (iff #637 #631) -#278 := (iff #631 #631) -#279 := [rewrite]: #278 -#635 := (iff #436 #634) -#632 := (iff #304 #647) -#633 := [rewrite]: #632 -#636 := [monotonicity #633]: #635 -#640 := [monotonicity #636]: #638 -#641 := [trans #640 #279]: #638 -#273 := [quant-inst #39 #40 #41]: #637 -#639 := [mp #273 #641]: #631 -#625 := [unit-resolution #639 #675]: #634 -#642 := (not #634) -#628 := (or #642 #126 #644) -#629 := [def-axiom]: #628 -#348 := [unit-resolution #629 #625]: #347 -#622 := [unit-resolution #348 #245]: #644 -#623 := (or #326 #647) -#649 := (iff #130 #647) -#315 := (or #643 #649) -#316 := [quant-inst #40 #39 #41]: #315 -#626 := [unit-resolution #316 #675]: #649 -#645 := (not #649) -#287 := (or #645 #326 #647) -#630 := [def-axiom]: #287 -#627 := [unit-resolution #630 #626]: #623 -#336 := [unit-resolution #627 #622 #624]: false -#337 := [lemma #336]: #126 -#329 := (or #326 #139) -#317 := (or #326 #139 #237) -#328 := [def-axiom]: #317 -#257 := [unit-resolution #328 #147]: #329 -#338 := [unit-resolution #257 #337]: #326 -#340 := (or #139 #647) -#335 := (or #642 #139 #647) -#351 := [def-axiom]: #335 -#618 := [unit-resolution #351 #625]: #340 -#619 := [unit-resolution #618 #337]: #647 -#332 := (or #130 #644) -#303 := (or #645 #130 #644) -#646 := [def-axiom]: #303 -#616 := [unit-resolution #646 #626]: #332 -[unit-resolution #616 #619 #338]: false -unsat -fa2f9bd8c428cc56374865b6337a9b9b3979db13 121 0 -#2 := false -decl f5 :: (-> S3 S3 S4 S1) -decl f10 :: S4 -#40 := f10 -decl f9 :: S3 -#39 := f9 -#41 := (f5 f9 f9 f10) -decl f1 :: S1 -#4 := f1 -#125 := (= f1 #41) -#138 := (not #125) -#629 := [hypothesis]: #138 -decl f6 :: (-> S3 S4 S1) -#43 := (f6 f9 f10) -#129 := (= f1 #43) -#324 := (or #129 #125) -#139 := (iff #129 #138) -#44 := (= #43 f1) -#42 := (= #41 f1) -#45 := (iff #42 #44) -#46 := (not #45) -#142 := (iff #46 #139) -#132 := (iff #125 #129) -#135 := (not #132) -#140 := (iff #135 #139) -#141 := [rewrite]: #140 -#136 := (iff #46 #135) -#133 := (iff #45 #132) -#130 := (iff #44 #129) -#131 := [rewrite]: #130 -#127 := (iff #42 #125) -#128 := [rewrite]: #127 -#134 := [monotonicity #128 #131]: #133 -#137 := [monotonicity #134]: #136 -#143 := [trans #137 #141]: #142 -#124 := [asserted]: #46 -#146 := [mp #124 #143]: #139 -#236 := (not #139) -#323 := (or #129 #125 #236) -#237 := [def-axiom]: #323 -#238 := [unit-resolution #237 #146]: #324 -#290 := [unit-resolution #238 #629]: #129 -#325 := (not #129) -#292 := (or #125 #325) -#18 := (:var 0 S4) -#17 := (:var 1 S3) -#16 := (:var 2 S3) -#19 := (f5 #16 #17 #18) -#668 := (pattern #19) -#23 := (f6 #17 #18) -#92 := (= f1 #23) -#21 := (f6 #16 #18) -#89 := (= f1 #21) -#95 := (or #89 #92) -#85 := (= f1 #19) -#98 := (iff #85 #95) -#669 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) (:pat #668) #98) -#101 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #98) -#672 := (iff #101 #669) -#670 := (iff #98 #98) -#671 := [refl]: #670 -#673 := [quant-intro #671]: #672 -#150 := (~ #101 #101) -#164 := (~ #98 #98) -#165 := [refl]: #164 -#151 := [nnf-pos #165]: #150 -#24 := (= #23 f1) -#22 := (= #21 f1) -#25 := (or #22 #24) -#20 := (= #19 f1) -#26 := (iff #20 #25) -#27 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #26) -#102 := (iff #27 #101) -#99 := (iff #26 #98) -#96 := (iff #25 #95) -#93 := (iff #24 #92) -#94 := [rewrite]: #93 -#90 := (iff #22 #89) -#91 := [rewrite]: #90 -#97 := [monotonicity #91 #94]: #96 -#87 := (iff #20 #85) -#88 := [rewrite]: #87 -#100 := [monotonicity #88 #97]: #99 -#103 := [quant-intro #100]: #102 -#84 := [asserted]: #27 -#106 := [mp #84 #103]: #101 -#166 := [mp~ #106 #151]: #101 -#674 := [mp #166 #673]: #669 -#303 := (not #669) -#435 := (or #303 #132) -#329 := (or #129 #129) -#326 := (iff #125 #329) -#642 := (or #303 #326) -#315 := (iff #642 #435) -#650 := (iff #435 #435) -#651 := [rewrite]: #650 -#646 := (iff #326 #132) -#330 := (iff #329 #129) -#309 := [rewrite]: #330 -#648 := [monotonicity #309]: #646 -#649 := [monotonicity #648]: #315 -#652 := [trans #649 #651]: #315 -#314 := [quant-inst #39 #39 #40]: #642 -#647 := [mp #314 #652]: #435 -#291 := [unit-resolution #647 #674]: #132 -#653 := (or #135 #125 #325) -#643 := [def-axiom]: #653 -#293 := [unit-resolution #643 #291]: #292 -#631 := [unit-resolution #293 #290 #629]: false -#632 := [lemma #631]: #125 -#328 := (or #325 #138) -#316 := (or #325 #138 #236) -#327 := [def-axiom]: #316 -#256 := [unit-resolution #327 #146]: #328 -#633 := [unit-resolution #256 #632]: #325 -#634 := (or #138 #129) -#301 := (or #135 #138 #129) -#306 := [def-axiom]: #301 -#635 := [unit-resolution #306 #291]: #634 -[unit-resolution #635 #633 #632]: false -unsat -63dfbec334f0b24e14d14e8841f417fc16248602 259 0 -#2 := false -decl f5 :: (-> S3 S4 S1) -decl f12 :: S4 -#45 := f12 -decl f10 :: S3 -#41 := f10 -#625 := (f5 f10 f12) -decl f1 :: S1 -#4 := f1 -#338 := (= f1 #625) -decl f11 :: S3 -#42 := f11 -#336 := (f5 f11 f12) -#333 := (= f1 #336) -#623 := (or #333 #338) -decl f6 :: (-> S3 S3 S3) -#43 := (f6 f10 f11) -#310 := (f5 #43 f12) -#442 := (= f1 #310) -#617 := (iff #442 #623) -#583 := (not #617) -#595 := (not #623) -#607 := (not #338) -decl f9 :: S3 -#40 := f9 -#638 := (f5 f9 f12) -#639 := (= f1 #638) -#485 := (or #338 #639) -#610 := (not #485) -#48 := (f6 f9 f10) -#337 := (f5 #48 f12) -#316 := (= f1 #337) -#593 := (iff #316 #485) -#585 := (not #593) -#578 := [hypothesis]: #585 -#19 := (:var 0 S4) -#17 := (:var 1 S3) -#16 := (:var 2 S3) -#18 := (f6 #16 #17) -#20 := (f5 #18 #19) -#675 := (pattern #20) -#24 := (f5 #17 #19) -#99 := (= f1 #24) -#22 := (f5 #16 #19) -#96 := (= f1 #22) -#102 := (or #96 #99) -#92 := (= f1 #20) -#105 := (iff #92 #102) -#676 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) (:pat #675) #105) -#108 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #105) -#679 := (iff #108 #676) -#677 := (iff #105 #105) -#678 := [refl]: #677 -#680 := [quant-intro #678]: #679 -#157 := (~ #108 #108) -#171 := (~ #105 #105) -#172 := [refl]: #171 -#158 := [nnf-pos #172]: #157 -#25 := (= #24 f1) -#23 := (= #22 f1) -#26 := (or #23 #25) -#21 := (= #20 f1) -#27 := (iff #21 #26) -#28 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S4)) #27) -#109 := (iff #28 #108) -#106 := (iff #27 #105) -#103 := (iff #26 #102) -#100 := (iff #25 #99) -#101 := [rewrite]: #100 -#97 := (iff #23 #96) -#98 := [rewrite]: #97 -#104 := [monotonicity #98 #101]: #103 -#94 := (iff #21 #92) -#95 := [rewrite]: #94 -#107 := [monotonicity #95 #104]: #106 -#110 := [quant-intro #107]: #109 -#91 := [asserted]: #28 -#113 := [mp #91 #110]: #108 -#173 := [mp~ #113 #158]: #108 -#681 := [mp #173 #680]: #676 -#649 := (not #676) -#591 := (or #649 #593) -#602 := (or #639 #338) -#484 := (iff #316 #602) -#594 := (or #649 #484) -#494 := (iff #594 #591) -#497 := (iff #591 #591) -#490 := [rewrite]: #497 -#495 := (iff #484 #593) -#486 := (iff #602 #485) -#445 := [rewrite]: #486 -#590 := [monotonicity #445]: #495 -#496 := [monotonicity #590]: #494 -#498 := [trans #496 #490]: #494 -#479 := [quant-inst #40 #41 #45]: #594 -#499 := [mp #479 #498]: #591 -#579 := [unit-resolution #499 #681 #578]: false -#580 := [lemma #579]: #593 -#656 := (not #316) -#653 := (or #316 #333) -#650 := (not #653) -#49 := (f6 #48 f11) -#50 := (f5 #49 f12) -#136 := (= f1 #50) -#332 := (not #136) -#44 := (f6 f9 #43) -#46 := (f5 #44 f12) -#132 := (= f1 #46) -#145 := (not #132) -#581 := [hypothesis]: #145 -#331 := (or #136 #132) -#146 := (iff #136 #145) -#51 := (= #50 f1) -#47 := (= #46 f1) -#52 := (iff #47 #51) -#53 := (not #52) -#149 := (iff #53 #146) -#139 := (iff #132 #136) -#142 := (not #139) -#147 := (iff #142 #146) -#148 := [rewrite]: #147 -#143 := (iff #53 #142) -#140 := (iff #52 #139) -#137 := (iff #51 #136) -#138 := [rewrite]: #137 -#134 := (iff #47 #132) -#135 := [rewrite]: #134 -#141 := [monotonicity #135 #138]: #140 -#144 := [monotonicity #141]: #143 -#150 := [trans #144 #148]: #149 -#131 := [asserted]: #53 -#153 := [mp #131 #150]: #146 -#243 := (not #146) -#330 := (or #136 #132 #243) -#244 := [def-axiom]: #330 -#245 := [unit-resolution #244 #153]: #331 -#575 := [unit-resolution #245 #581]: #136 -#566 := (or #332 #653) -#655 := (iff #136 #653) -#321 := (or #649 #655) -#322 := [quant-inst #48 #42 #45]: #321 -#582 := [unit-resolution #322 #681]: #655 -#651 := (not #655) -#293 := (or #651 #332 #653) -#636 := [def-axiom]: #293 -#567 := [unit-resolution #636 #582]: #566 -#569 := [unit-resolution #567 #575]: #653 -#659 := (not #333) -#599 := (or #649 #617) -#622 := (or #338 #333) -#626 := (iff #442 #622) -#619 := (or #649 #626) -#614 := (iff #619 #599) -#621 := (iff #599 #599) -#462 := [rewrite]: #621 -#618 := (iff #626 #617) -#627 := (iff #622 #623) -#616 := [rewrite]: #627 -#613 := [monotonicity #616]: #618 -#615 := [monotonicity #613]: #614 -#463 := [trans #615 #462]: #614 -#620 := [quant-inst #41 #42 #45]: #619 -#464 := [mp #620 #463]: #599 -#570 := [unit-resolution #464 #681]: #617 -#560 := (or #583 #595) -#358 := (not #442) -#642 := (or #442 #639) -#631 := (not #642) -#572 := (or #132 #631) -#279 := (iff #132 #642) -#284 := (or #649 #279) -#640 := (or #639 #442) -#641 := (iff #132 #640) -#285 := (or #649 #641) -#645 := (iff #285 #284) -#634 := (iff #284 #284) -#635 := [rewrite]: #634 -#644 := (iff #641 #279) -#637 := (iff #640 #642) -#643 := [rewrite]: #637 -#646 := [monotonicity #643]: #644 -#648 := [monotonicity #646]: #645 -#341 := [trans #648 #635]: #645 -#647 := [quant-inst #40 #43 #45]: #285 -#357 := [mp #647 #341]: #284 -#571 := [unit-resolution #357 #681]: #279 -#628 := (not #279) -#632 := (or #628 #132 #631) -#629 := [def-axiom]: #632 -#568 := [unit-resolution #629 #571]: #572 -#573 := [unit-resolution #568 #581]: #631 -#359 := (or #642 #358) -#345 := [def-axiom]: #359 -#559 := [unit-resolution #345 #573]: #358 -#577 := (or #583 #442 #595) -#574 := [def-axiom]: #577 -#562 := [unit-resolution #574 #559]: #560 -#563 := [unit-resolution #562 #570]: #595 -#606 := (or #623 #659) -#500 := [def-axiom]: #606 -#564 := [unit-resolution #500 #563]: #659 -#308 := (or #650 #316 #333) -#313 := [def-axiom]: #308 -#561 := [unit-resolution #313 #564 #569]: #316 -#360 := (not #639) -#251 := (or #642 #360) -#630 := [def-axiom]: #251 -#565 := [unit-resolution #630 #573]: #360 -#501 := (or #623 #607) -#502 := [def-axiom]: #501 -#545 := [unit-resolution #502 #563]: #607 -#611 := (or #610 #338 #639) -#605 := [def-axiom]: #611 -#546 := [unit-resolution #605 #545 #565]: #610 -#443 := (or #585 #656 #485) -#444 := [def-axiom]: #443 -#548 := [unit-resolution #444 #546 #561 #580]: false -#549 := [lemma #548]: #132 -#335 := (or #332 #145) -#323 := (or #332 #145 #243) -#334 := [def-axiom]: #323 -#263 := [unit-resolution #334 #153]: #335 -#550 := [unit-resolution #263 #549]: #332 -#551 := (or #136 #650) -#309 := (or #651 #136 #650) -#652 := [def-axiom]: #309 -#552 := [unit-resolution #652 #582]: #551 -#553 := [unit-resolution #552 #550]: #650 -#657 := (or #653 #656) -#658 := [def-axiom]: #657 -#554 := [unit-resolution #658 #553]: #656 -#612 := (or #585 #316 #610) -#441 := [def-axiom]: #612 -#555 := [unit-resolution #441 #554 #580]: #610 -#608 := (or #485 #607) -#609 := [def-axiom]: #608 -#556 := [unit-resolution #609 #555]: #607 -#654 := (or #653 #659) -#660 := [def-axiom]: #654 -#557 := [unit-resolution #660 #553]: #659 -#592 := (or #595 #333 #338) -#596 := [def-axiom]: #592 -#547 := [unit-resolution #596 #557 #556]: #595 -#558 := (or #145 #642) -#633 := (or #628 #145 #642) -#342 := [def-axiom]: #633 -#536 := [unit-resolution #342 #571]: #558 -#537 := [unit-resolution #536 #549]: #642 -#603 := (or #485 #360) -#604 := [def-axiom]: #603 -#539 := [unit-resolution #604 #555]: #360 -#353 := (or #631 #442 #639) -#354 := [def-axiom]: #353 -#540 := [unit-resolution #354 #539 #537]: #442 -#576 := (or #583 #358 #623) -#586 := [def-axiom]: #576 -#541 := [unit-resolution #586 #540 #547]: #583 -[unit-resolution #464 #681 #541]: false -unsat -b9a56cfd9dd84219baf29a97bb74d87de1fcb3ba 153 0 -#2 := false -decl f8 :: (-> S4 S5 S1) -decl f11 :: S5 -#41 := f11 -decl f10 :: S4 -#40 := f10 -#46 := (f8 f10 f11) -decl f1 :: S1 -#4 := f1 -#136 := (= f1 #46) -#190 := (not #136) -decl f9 :: S4 -#39 := f9 -#44 := (f8 f9 f11) -#133 := (= f1 #44) -#189 := (not #133) -#191 := (or #189 #190) -#192 := (not #191) -#333 := [hypothesis]: #192 -decl f7 :: (-> S4 S4 S5 S1) -#42 := (f7 f9 f10 f11) -#129 := (= f1 #42) -#148 := (not #129) -#339 := (or #148 #191) -#203 := (iff #129 #191) -#139 := (and #133 #136) -#149 := (iff #139 #148) -#206 := (iff #149 #203) -#198 := (iff #191 #129) -#204 := (iff #198 #203) -#205 := [rewrite]: #204 -#201 := (iff #149 #198) -#195 := (iff #192 #148) -#199 := (iff #195 #198) -#200 := [rewrite]: #199 -#196 := (iff #149 #195) -#193 := (iff #139 #192) -#194 := [rewrite]: #193 -#197 := [monotonicity #194]: #196 -#202 := [trans #197 #200]: #201 -#207 := [trans #202 #205]: #206 -#47 := (= #46 f1) -#45 := (= #44 f1) -#48 := (and #45 #47) -#43 := (= #42 f1) -#49 := (iff #43 #48) -#50 := (not #49) -#152 := (iff #50 #149) -#142 := (iff #129 #139) -#145 := (not #142) -#150 := (iff #145 #149) -#151 := [rewrite]: #150 -#146 := (iff #50 #145) -#143 := (iff #49 #142) -#140 := (iff #48 #139) -#137 := (iff #47 #136) -#138 := [rewrite]: #137 -#134 := (iff #45 #133) -#135 := [rewrite]: #134 -#141 := [monotonicity #135 #138]: #140 -#131 := (iff #43 #129) -#132 := [rewrite]: #131 -#144 := [monotonicity #132 #141]: #143 -#147 := [monotonicity #144]: #146 -#153 := [trans #147 #151]: #152 -#128 := [asserted]: #50 -#156 := [mp #128 #153]: #149 -#208 := [mp #156 #207]: #203 -#346 := (not #203) -#356 := (or #148 #191 #346) -#360 := [def-axiom]: #356 -#676 := [unit-resolution #360 #208]: #339 -#465 := [unit-resolution #676 #333]: #148 -#332 := (or #129 #191) -#678 := (iff #129 #192) -#29 := (:var 0 S5) -#28 := (:var 1 S4) -#27 := (:var 2 S4) -#30 := (f7 #27 #28 #29) -#705 := (pattern #30) -#34 := (f8 #28 #29) -#116 := (= f1 #34) -#181 := (not #116) -#32 := (f8 #27 #29) -#113 := (= f1 #32) -#180 := (not #113) -#164 := (or #180 #181) -#165 := (not #164) -#109 := (= f1 #30) -#182 := (iff #109 #165) -#706 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) (:pat #705) #182) -#185 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #182) -#709 := (iff #185 #706) -#707 := (iff #182 #182) -#708 := [refl]: #707 -#710 := [quant-intro #708]: #709 -#119 := (and #113 #116) -#122 := (iff #109 #119) -#125 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #122) -#186 := (iff #125 #185) -#183 := (iff #122 #182) -#166 := (iff #119 #165) -#167 := [rewrite]: #166 -#184 := [monotonicity #167]: #183 -#187 := [quant-intro #184]: #186 -#162 := (~ #125 #125) -#177 := (~ #122 #122) -#178 := [refl]: #177 -#163 := [nnf-pos #178]: #162 -#35 := (= #34 f1) -#33 := (= #32 f1) -#36 := (and #33 #35) -#31 := (= #30 f1) -#37 := (iff #31 #36) -#38 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #37) -#126 := (iff #38 #125) -#123 := (iff #37 #122) -#120 := (iff #36 #119) -#117 := (iff #35 #116) -#118 := [rewrite]: #117 -#114 := (iff #33 #113) -#115 := [rewrite]: #114 -#121 := [monotonicity #115 #118]: #120 -#111 := (iff #31 #109) -#112 := [rewrite]: #111 -#124 := [monotonicity #112 #121]: #123 -#127 := [quant-intro #124]: #126 -#108 := [asserted]: #38 -#130 := [mp #108 #127]: #125 -#179 := [mp~ #130 #163]: #125 -#188 := [mp #179 #187]: #185 -#711 := [mp #188 #710]: #706 -#672 := (not #706) -#344 := (or #672 #678) -#345 := [quant-inst #39 #40 #41]: #344 -#674 := [unit-resolution #345 #711]: #678 -#679 := (not #678) -#680 := (or #679 #129 #191) -#681 := [def-axiom]: #680 -#675 := [unit-resolution #681 #674]: #332 -#316 := [unit-resolution #675 #465 #333]: false -#659 := [lemma #316]: #191 -#286 := (or #129 #192) -#357 := (or #129 #192 #346) -#358 := [def-axiom]: #357 -#359 := [unit-resolution #358 #208]: #286 -#320 := [unit-resolution #359 #659]: #129 -#321 := (or #148 #192) -#682 := (or #679 #148 #192) -#677 := [def-axiom]: #682 -#322 := [unit-resolution #677 #674]: #321 -[unit-resolution #322 #320 #659]: false -unsat -7f98a59af5916f5d5b5c30234aa00391b0645729 141 0 -#2 := false -decl f3 :: (-> S3 S2 S1) -decl f10 :: S2 -#41 := f10 -decl f4 :: S3 -#8 := f4 -#230 := (f3 f4 f10) -decl f1 :: S1 -#4 := f1 -#317 := (= f1 #230) -#231 := (not #317) -decl f9 :: S3 -#40 := f9 -#318 := (f3 f9 f10) -#232 := (= f1 #318) -#319 := (not #232) -#310 := (or #319 #231) -#321 := (not #310) -decl f8 :: (-> S3 S3 S2 S1) -#42 := (f8 f9 f4 f10) -#124 := (= f1 #42) -#322 := (iff #124 #321) -#9 := (:var 0 S2) -#30 := (:var 1 S3) -#29 := (:var 2 S3) -#31 := (f8 #29 #30 #9) -#669 := (pattern #31) -#35 := (f3 #30 #9) -#111 := (= f1 #35) -#165 := (not #111) -#33 := (f3 #29 #9) -#108 := (= f1 #33) -#164 := (not #108) -#148 := (or #164 #165) -#149 := (not #148) -#104 := (= f1 #31) -#166 := (iff #104 #149) -#670 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) (:pat #669) #166) -#169 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #166) -#673 := (iff #169 #670) -#671 := (iff #166 #166) -#672 := [refl]: #671 -#674 := [quant-intro #672]: #673 -#114 := (and #108 #111) -#117 := (iff #104 #114) -#120 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #117) -#170 := (iff #120 #169) -#167 := (iff #117 #166) -#150 := (iff #114 #149) -#151 := [rewrite]: #150 -#168 := [monotonicity #151]: #167 -#171 := [quant-intro #168]: #170 -#146 := (~ #120 #120) -#161 := (~ #117 #117) -#162 := [refl]: #161 -#147 := [nnf-pos #162]: #146 -#36 := (= #35 f1) -#34 := (= #33 f1) -#37 := (and #34 #36) -#32 := (= #31 f1) -#38 := (iff #32 #37) -#39 := (forall (vars (?v0 S3) (?v1 S3) (?v2 S2)) #38) -#121 := (iff #39 #120) -#118 := (iff #38 #117) -#115 := (iff #37 #114) -#112 := (iff #36 #111) -#113 := [rewrite]: #112 -#109 := (iff #34 #108) -#110 := [rewrite]: #109 -#116 := [monotonicity #110 #113]: #115 -#106 := (iff #32 #104) -#107 := [rewrite]: #106 -#119 := [monotonicity #107 #116]: #118 -#122 := [quant-intro #119]: #121 -#103 := [asserted]: #39 -#125 := [mp #103 #122]: #120 -#163 := [mp~ #125 #147]: #120 -#172 := [mp #163 #171]: #169 -#675 := [mp #172 #674]: #670 -#320 := (not #670) -#324 := (or #320 #322) -#303 := [quant-inst #40 #8 #41]: #324 -#250 := [unit-resolution #303 #675]: #322 -#309 := (not #322) -#323 := (or #309 #321) -#43 := (= #42 f1) -#44 := (not #43) -#45 := (not #44) -#136 := (iff #45 #124) -#128 := (not #124) -#131 := (not #128) -#134 := (iff #131 #124) -#135 := [rewrite]: #134 -#132 := (iff #45 #131) -#129 := (iff #44 #128) -#126 := (iff #43 #124) -#127 := [rewrite]: #126 -#130 := [monotonicity #127]: #129 -#133 := [monotonicity #130]: #132 -#137 := [trans #133 #135]: #136 -#123 := [asserted]: #45 -#140 := [mp #123 #137]: #124 -#645 := (or #309 #128 #321) -#646 := [def-axiom]: #645 -#639 := [unit-resolution #646 #140]: #323 -#280 := [unit-resolution #639 #250]: #321 -#297 := (or #310 #317) -#429 := [def-axiom]: #297 -#623 := [unit-resolution #429 #280]: #317 -#10 := (f3 f4 #9) -#648 := (pattern #10) -#66 := (= f1 #10) -#69 := (not #66) -#649 := (forall (vars (?v0 S2)) (:pat #648) #69) -#72 := (forall (vars (?v0 S2)) #69) -#652 := (iff #72 #649) -#650 := (iff #69 #69) -#651 := [refl]: #650 -#653 := [quant-intro #651]: #652 -#154 := (~ #72 #72) -#152 := (~ #69 #69) -#153 := [refl]: #152 -#155 := [nnf-pos #153]: #154 -#11 := (= #10 f1) -#12 := (not #11) -#13 := (forall (vars (?v0 S2)) #12) -#73 := (iff #13 #72) -#70 := (iff #12 #69) -#67 := (iff #11 #66) -#68 := [rewrite]: #67 -#71 := [monotonicity #68]: #70 -#74 := [quant-intro #71]: #73 -#65 := [asserted]: #13 -#77 := [mp #65 #74]: #72 -#139 := [mp~ #77 #155]: #72 -#654 := [mp #139 #653]: #649 -#300 := (not #649) -#638 := (or #300 #231) -#296 := [quant-inst #41]: #638 -[unit-resolution #296 #654 #623]: false -unsat -b75cfd5dcf910762f51953bce5714d91441e0375 165 0 -#2 := false -decl f4 :: (-> S4 S3 S1) -decl f10 :: S3 -#41 := f10 -decl f9 :: S4 -#40 := f9 -#44 := (f4 f9 f10) -decl f1 :: S1 -#4 := f1 -#130 := (= f1 #44) -#326 := (not #130) -decl f8 :: (-> S4 S4 S3 S1) -decl f5 :: S4 -#13 := f5 -#42 := (f8 f9 f5 f10) -#126 := (= f1 #42) -#330 := (f4 f5 f10) -#327 := (= f1 #330) -#331 := (not #327) -#304 := [hypothesis]: #331 -#14 := (:var 0 S3) -#15 := (f4 f5 #14) -#662 := (pattern #15) -#78 := (= f1 #15) -#663 := (forall (vars (?v0 S3)) (:pat #662) #78) -#82 := (forall (vars (?v0 S3)) #78) -#666 := (iff #82 #663) -#664 := (iff #78 #78) -#665 := [refl]: #664 -#667 := [quant-intro #665]: #666 -#149 := (~ #82 #82) -#148 := (~ #78 #78) -#163 := [refl]: #148 -#150 := [nnf-pos #163]: #149 -#16 := (= #15 f1) -#17 := (forall (vars (?v0 S3)) #16) -#83 := (iff #17 #82) -#80 := (iff #16 #78) -#81 := [rewrite]: #80 -#84 := [quant-intro #81]: #83 -#77 := [asserted]: #17 -#87 := [mp #77 #84]: #82 -#164 := [mp~ #87 #150]: #82 -#668 := [mp #164 #667]: #663 -#292 := (not #663) -#293 := (or #292 #327) -#294 := [quant-inst #41]: #293 -#436 := [unit-resolution #294 #668 #304]: false -#632 := [lemma #436]: #327 -#139 := (not #126) -#633 := [hypothesis]: #139 -#325 := (or #130 #126) -#140 := (iff #130 #139) -#45 := (= #44 f1) -#43 := (= #42 f1) -#46 := (iff #43 #45) -#47 := (not #46) -#143 := (iff #47 #140) -#133 := (iff #126 #130) -#136 := (not #133) -#141 := (iff #136 #140) -#142 := [rewrite]: #141 -#137 := (iff #47 #136) -#134 := (iff #46 #133) -#131 := (iff #45 #130) -#132 := [rewrite]: #131 -#128 := (iff #43 #126) -#129 := [rewrite]: #128 -#135 := [monotonicity #129 #132]: #134 -#138 := [monotonicity #135]: #137 -#144 := [trans #138 #142]: #143 -#125 := [asserted]: #47 -#147 := [mp #125 #144]: #140 -#237 := (not #140) -#324 := (or #130 #126 #237) -#238 := [def-axiom]: #324 -#239 := [unit-resolution #238 #147]: #325 -#634 := [unit-resolution #239 #633]: #130 -#310 := (or #326 #331) -#636 := (or #126 #310) -#647 := (not #310) -#649 := (iff #126 #647) -#30 := (:var 1 S4) -#29 := (:var 2 S4) -#31 := (f8 #29 #30 #14) -#676 := (pattern #31) -#35 := (f4 #30 #14) -#113 := (= f1 #35) -#172 := (not #113) -#33 := (f4 #29 #14) -#110 := (= f1 #33) -#171 := (not #110) -#155 := (or #171 #172) -#156 := (not #155) -#106 := (= f1 #31) -#173 := (iff #106 #156) -#677 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) (:pat #676) #173) -#176 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) #173) -#680 := (iff #176 #677) -#678 := (iff #173 #173) -#679 := [refl]: #678 -#681 := [quant-intro #679]: #680 -#116 := (and #110 #113) -#119 := (iff #106 #116) -#122 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) #119) -#177 := (iff #122 #176) -#174 := (iff #119 #173) -#157 := (iff #116 #156) -#158 := [rewrite]: #157 -#175 := [monotonicity #158]: #174 -#178 := [quant-intro #175]: #177 -#153 := (~ #122 #122) -#168 := (~ #119 #119) -#169 := [refl]: #168 -#154 := [nnf-pos #169]: #153 -#36 := (= #35 f1) -#34 := (= #33 f1) -#37 := (and #34 #36) -#32 := (= #31 f1) -#38 := (iff #32 #37) -#39 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S3)) #38) -#123 := (iff #39 #122) -#120 := (iff #38 #119) -#117 := (iff #37 #116) -#114 := (iff #36 #113) -#115 := [rewrite]: #114 -#111 := (iff #34 #110) -#112 := [rewrite]: #111 -#118 := [monotonicity #112 #115]: #117 -#108 := (iff #32 #106) -#109 := [rewrite]: #108 -#121 := [monotonicity #109 #118]: #120 -#124 := [quant-intro #121]: #123 -#105 := [asserted]: #39 -#127 := [mp #105 #124]: #122 -#170 := [mp~ #127 #154]: #122 -#179 := [mp #170 #178]: #176 -#682 := [mp #179 #681]: #677 -#643 := (not #677) -#315 := (or #643 #649) -#316 := [quant-inst #40 #13 #41]: #315 -#635 := [unit-resolution #316 #682]: #649 -#644 := (not #649) -#302 := (or #644 #126 #310) -#307 := [def-axiom]: #302 -#631 := [unit-resolution #307 #635]: #636 -#637 := [unit-resolution #631 #633]: #310 -#648 := (or #647 #326 #331) -#654 := [def-axiom]: #648 -#273 := [unit-resolution #654 #637 #634 #632]: false -#638 := [lemma #273]: #126 -#329 := (or #326 #139) -#317 := (or #326 #139 #237) -#328 := [def-axiom]: #317 -#257 := [unit-resolution #328 #147]: #329 -#640 := [unit-resolution #257 #638]: #326 -#278 := (or #139 #647) -#645 := (or #644 #139 #647) -#303 := [def-axiom]: #645 -#279 := [unit-resolution #303 #635]: #278 -#641 := [unit-resolution #279 #638]: #647 -#650 := (or #310 #130) -#651 := [def-axiom]: #650 -[unit-resolution #651 #641 #640]: false -unsat -600bc627f2a337ab9492b3414ff9a405597dcbc3 164 0 -#2 := false -decl f7 :: (-> S4 S4 S5 S1) -decl f11 :: S5 -#41 := f11 -decl f9 :: S4 -#39 := f9 -decl f10 :: S4 -#40 := f10 -#44 := (f7 f10 f9 f11) -decl f1 :: S1 -#4 := f1 -#130 := (= f1 #44) -#326 := (not #130) -#42 := (f7 f9 f10 f11) -#126 := (= f1 #42) -#139 := (not #126) -#628 := [hypothesis]: #139 -#325 := (or #130 #126) -#140 := (iff #130 #139) -#45 := (= #44 f1) -#43 := (= #42 f1) -#46 := (iff #43 #45) -#47 := (not #46) -#143 := (iff #47 #140) -#133 := (iff #126 #130) -#136 := (not #133) -#141 := (iff #136 #140) -#142 := [rewrite]: #141 -#137 := (iff #47 #136) -#134 := (iff #46 #133) -#131 := (iff #45 #130) -#132 := [rewrite]: #131 -#128 := (iff #43 #126) -#129 := [rewrite]: #128 -#135 := [monotonicity #129 #132]: #134 -#138 := [monotonicity #135]: #137 -#144 := [trans #138 #142]: #143 -#125 := [asserted]: #47 -#147 := [mp #125 #144]: #140 -#237 := (not #140) -#324 := (or #130 #126 #237) -#238 := [def-axiom]: #324 -#239 := [unit-resolution #238 #147]: #325 -#629 := [unit-resolution #239 #628]: #130 -decl f8 :: (-> S4 S5 S1) -#310 := (f8 f10 f11) -#647 := (= f1 #310) -#649 := (not #647) -#330 := (f8 f9 f11) -#327 := (= f1 #330) -#331 := (not #327) -#315 := (or #331 #649) -#626 := (or #126 #315) -#651 := (not #315) -#642 := (iff #126 #651) -#29 := (:var 0 S5) -#28 := (:var 1 S4) -#27 := (:var 2 S4) -#30 := (f7 #27 #28 #29) -#676 := (pattern #30) -#34 := (f8 #28 #29) -#113 := (= f1 #34) -#172 := (not #113) -#32 := (f8 #27 #29) -#110 := (= f1 #32) -#171 := (not #110) -#155 := (or #171 #172) -#156 := (not #155) -#106 := (= f1 #30) -#173 := (iff #106 #156) -#677 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) (:pat #676) #173) -#176 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #173) -#680 := (iff #176 #677) -#678 := (iff #173 #173) -#679 := [refl]: #678 -#681 := [quant-intro #679]: #680 -#116 := (and #110 #113) -#119 := (iff #106 #116) -#122 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #119) -#177 := (iff #122 #176) -#174 := (iff #119 #173) -#157 := (iff #116 #156) -#158 := [rewrite]: #157 -#175 := [monotonicity #158]: #174 -#178 := [quant-intro #175]: #177 -#153 := (~ #122 #122) -#168 := (~ #119 #119) -#169 := [refl]: #168 -#154 := [nnf-pos #169]: #153 -#35 := (= #34 f1) -#33 := (= #32 f1) -#36 := (and #33 #35) -#31 := (= #30 f1) -#37 := (iff #31 #36) -#38 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #37) -#123 := (iff #38 #122) -#120 := (iff #37 #119) -#117 := (iff #36 #116) -#114 := (iff #35 #113) -#115 := [rewrite]: #114 -#111 := (iff #33 #110) -#112 := [rewrite]: #111 -#118 := [monotonicity #112 #115]: #117 -#108 := (iff #31 #106) -#109 := [rewrite]: #108 -#121 := [monotonicity #109 #118]: #120 -#124 := [quant-intro #121]: #123 -#105 := [asserted]: #38 -#127 := [mp #105 #124]: #122 -#170 := [mp~ #127 #154]: #122 -#179 := [mp #170 #178]: #176 -#682 := [mp #179 #681]: #677 -#302 := (not #677) -#335 := (or #302 #642) -#351 := [quant-inst #39 #40 #41]: #335 -#622 := [unit-resolution #351 #682]: #642 -#352 := (not #642) -#353 := (or #352 #126 #315) -#339 := [def-axiom]: #353 -#623 := [unit-resolution #339 #622]: #626 -#627 := [unit-resolution #623 #628]: #315 -#337 := (or #326 #651) -#648 := (iff #130 #651) -#307 := (or #302 #648) -#304 := (or #649 #331) -#436 := (not #304) -#643 := (iff #130 #436) -#645 := (or #302 #643) -#646 := (iff #645 #307) -#630 := (iff #307 #307) -#291 := [rewrite]: #630 -#654 := (iff #643 #648) -#652 := (iff #436 #651) -#316 := (iff #304 #315) -#650 := [rewrite]: #316 -#653 := [monotonicity #650]: #652 -#644 := [monotonicity #653]: #654 -#287 := [monotonicity #644]: #646 -#292 := [trans #287 #291]: #646 -#303 := [quant-inst #40 #39 #41]: #645 -#293 := [mp #303 #292]: #307 -#336 := [unit-resolution #293 #682]: #648 -#631 := (not #648) -#638 := (or #631 #326 #651) -#640 := [def-axiom]: #638 -#338 := [unit-resolution #640 #336]: #337 -#340 := [unit-resolution #338 #627 #629]: false -#618 := [lemma #340]: #126 -#329 := (or #326 #139) -#317 := (or #326 #139 #237) -#328 := [def-axiom]: #317 -#257 := [unit-resolution #328 #147]: #329 -#619 := [unit-resolution #257 #618]: #326 -#332 := (or #139 #651) -#354 := (or #352 #139 #651) -#245 := [def-axiom]: #354 -#616 := [unit-resolution #245 #622]: #332 -#620 := [unit-resolution #616 #618]: #651 -#617 := (or #130 #315) -#637 := (or #631 #130 #315) -#273 := [def-axiom]: #637 -#621 := [unit-resolution #273 #336]: #617 -[unit-resolution #621 #620 #619]: false -unsat -b05e302d276675d4c2c21abbf217592e2a23efc3 142 0 -#2 := false -decl f7 :: (-> S4 S4 S5 S1) -decl f10 :: S5 -#40 := f10 -decl f9 :: S4 -#39 := f9 -#41 := (f7 f9 f9 f10) -decl f1 :: S1 -#4 := f1 -#125 := (= f1 #41) -#138 := (not #125) -#634 := [hypothesis]: #138 -decl f8 :: (-> S4 S5 S1) -#43 := (f8 f9 f10) -#129 := (= f1 #43) -#324 := (or #129 #125) -#139 := (iff #129 #138) -#44 := (= #43 f1) -#42 := (= #41 f1) -#45 := (iff #42 #44) -#46 := (not #45) -#142 := (iff #46 #139) -#132 := (iff #125 #129) -#135 := (not #132) -#140 := (iff #135 #139) -#141 := [rewrite]: #140 -#136 := (iff #46 #135) -#133 := (iff #45 #132) -#130 := (iff #44 #129) -#131 := [rewrite]: #130 -#127 := (iff #42 #125) -#128 := [rewrite]: #127 -#134 := [monotonicity #128 #131]: #133 -#137 := [monotonicity #134]: #136 -#143 := [trans #137 #141]: #142 -#124 := [asserted]: #46 -#146 := [mp #124 #143]: #139 -#236 := (not #139) -#323 := (or #129 #125 #236) -#237 := [def-axiom]: #323 -#238 := [unit-resolution #237 #146]: #324 -#635 := [unit-resolution #238 #634]: #129 -#325 := (not #129) -#636 := (or #125 #325) -#29 := (:var 0 S5) -#28 := (:var 1 S4) -#27 := (:var 2 S4) -#30 := (f7 #27 #28 #29) -#675 := (pattern #30) -#34 := (f8 #28 #29) -#112 := (= f1 #34) -#171 := (not #112) -#32 := (f8 #27 #29) -#109 := (= f1 #32) -#170 := (not #109) -#154 := (or #170 #171) -#155 := (not #154) -#105 := (= f1 #30) -#172 := (iff #105 #155) -#676 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) (:pat #675) #172) -#175 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #172) -#679 := (iff #175 #676) -#677 := (iff #172 #172) -#678 := [refl]: #677 -#680 := [quant-intro #678]: #679 -#115 := (and #109 #112) -#118 := (iff #105 #115) -#121 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #118) -#176 := (iff #121 #175) -#173 := (iff #118 #172) -#156 := (iff #115 #155) -#157 := [rewrite]: #156 -#174 := [monotonicity #157]: #173 -#177 := [quant-intro #174]: #176 -#152 := (~ #121 #121) -#167 := (~ #118 #118) -#168 := [refl]: #167 -#153 := [nnf-pos #168]: #152 -#35 := (= #34 f1) -#33 := (= #32 f1) -#36 := (and #33 #35) -#31 := (= #30 f1) -#37 := (iff #31 #36) -#38 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #37) -#122 := (iff #38 #121) -#119 := (iff #37 #118) -#116 := (iff #36 #115) -#113 := (iff #35 #112) -#114 := [rewrite]: #113 -#110 := (iff #33 #109) -#111 := [rewrite]: #110 -#117 := [monotonicity #111 #114]: #116 -#107 := (iff #31 #105) -#108 := [rewrite]: #107 -#120 := [monotonicity #108 #117]: #119 -#123 := [quant-intro #120]: #122 -#104 := [asserted]: #38 -#126 := [mp #104 #123]: #121 -#169 := [mp~ #126 #153]: #121 -#178 := [mp #169 #177]: #175 -#681 := [mp #178 #680]: #676 -#652 := (not #676) -#647 := (or #652 #132) -#329 := (or #325 #325) -#326 := (not #329) -#330 := (iff #125 #326) -#653 := (or #652 #330) -#301 := (iff #653 #647) -#644 := (iff #647 #647) -#302 := [rewrite]: #644 -#650 := (iff #330 #132) -#315 := (iff #326 #129) -#648 := (not #325) -#642 := (iff #648 #129) -#314 := [rewrite]: #642 -#303 := (iff #326 #648) -#309 := (iff #329 #325) -#646 := [rewrite]: #309 -#435 := [monotonicity #646]: #303 -#649 := [trans #435 #314]: #315 -#651 := [monotonicity #649]: #650 -#306 := [monotonicity #651]: #301 -#645 := [trans #306 #302]: #301 -#643 := [quant-inst #39 #39 #40]: #653 -#286 := [mp #643 #645]: #647 -#630 := [unit-resolution #286 #681]: #132 -#629 := (or #135 #125 #325) -#290 := [def-axiom]: #629 -#272 := [unit-resolution #290 #630]: #636 -#637 := [unit-resolution #272 #635 #634]: false -#639 := [lemma #637]: #125 -#328 := (or #325 #138) -#316 := (or #325 #138 #236) -#327 := [def-axiom]: #316 -#256 := [unit-resolution #327 #146]: #328 -#277 := [unit-resolution #256 #639]: #325 -#278 := (or #138 #129) -#291 := (or #135 #138 #129) -#292 := [def-axiom]: #291 -#640 := [unit-resolution #292 #630]: #278 -[unit-resolution #640 #277 #639]: false -unsat -d8e9744832a91810c03cbef21eb26edf5cd1eec0 280 0 -#2 := false -decl f7 :: (-> S4 S5 S1) -decl f12 :: S5 -#45 := f12 -decl f8 :: (-> S4 S4 S4) -decl f10 :: S4 -#41 := f10 -decl f9 :: S4 -#40 := f9 -#48 := (f8 f9 f10) -#316 := (f7 #48 f12) -decl f1 :: S1 -#4 := f1 -#653 := (= f1 #316) -#251 := (f7 f10 f12) -#630 := (= f1 #251) -#627 := (not #630) -#341 := (f7 f9 f12) -#357 := (= f1 #341) -#358 := (not #357) -#616 := (or #358 #627) -#617 := (not #616) -#613 := (iff #617 #653) -#584 := (not #613) -decl f11 :: S4 -#42 := f11 -#336 := (f7 f11 f12) -#333 := (= f1 #336) -#337 := (not #333) -#486 := (or #337 #627) -#495 := (not #486) -#43 := (f8 f10 f11) -#648 := (f7 #43 f12) -#634 := (= f1 #648) -#496 := (iff #495 #634) -#589 := (not #496) -#569 := [hypothesis]: #589 -#30 := (:var 0 S5) -#28 := (:var 1 S4) -#27 := (:var 2 S4) -#29 := (f8 #27 #28) -#31 := (f7 #29 #30) -#682 := (pattern #31) -#35 := (f7 #28 #30) -#119 := (= f1 #35) -#178 := (not #119) -#33 := (f7 #27 #30) -#116 := (= f1 #33) -#177 := (not #116) -#161 := (or #177 #178) -#162 := (not #161) -#112 := (= f1 #31) -#179 := (iff #112 #162) -#683 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) (:pat #682) #179) -#182 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #179) -#686 := (iff #182 #683) -#684 := (iff #179 #179) -#685 := [refl]: #684 -#687 := [quant-intro #685]: #686 -#122 := (and #116 #119) -#125 := (iff #112 #122) -#128 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #125) -#183 := (iff #128 #182) -#180 := (iff #125 #179) -#163 := (iff #122 #162) -#164 := [rewrite]: #163 -#181 := [monotonicity #164]: #180 -#184 := [quant-intro #181]: #183 -#159 := (~ #128 #128) -#174 := (~ #125 #125) -#175 := [refl]: #174 -#160 := [nnf-pos #175]: #159 -#36 := (= #35 f1) -#34 := (= #33 f1) -#37 := (and #34 #36) -#32 := (= #31 f1) -#38 := (iff #32 #37) -#39 := (forall (vars (?v0 S4) (?v1 S4) (?v2 S5)) #38) -#129 := (iff #39 #128) -#126 := (iff #38 #125) -#123 := (iff #37 #122) -#120 := (iff #36 #119) -#121 := [rewrite]: #120 -#117 := (iff #34 #116) -#118 := [rewrite]: #117 -#124 := [monotonicity #118 #121]: #123 -#114 := (iff #32 #112) -#115 := [rewrite]: #114 -#127 := [monotonicity #115 #124]: #126 -#130 := [quant-intro #127]: #129 -#111 := [asserted]: #39 -#133 := [mp #111 #130]: #128 -#176 := [mp~ #133 #160]: #128 -#185 := [mp #176 #184]: #182 -#688 := [mp #185 #687]: #683 -#308 := (not #683) -#500 := (or #308 #496) -#602 := (or #627 #337) -#484 := (not #602) -#485 := (iff #634 #484) -#501 := (or #308 #485) -#595 := (iff #501 #500) -#596 := (iff #500 #500) -#583 := [rewrite]: #596 -#498 := (iff #485 #496) -#594 := (iff #634 #495) -#497 := (iff #594 #496) -#490 := [rewrite]: #497 -#479 := (iff #485 #594) -#590 := (iff #484 #495) -#445 := (iff #602 #486) -#593 := [rewrite]: #445 -#591 := [monotonicity #593]: #590 -#494 := [monotonicity #591]: #479 -#499 := [trans #494 #490]: #498 -#592 := [monotonicity #499]: #595 -#585 := [trans #592 #583]: #595 -#502 := [quant-inst #41 #42 #45]: #501 -#577 := [mp #502 #585]: #500 -#570 := [unit-resolution #577 #688 #569]: false -#571 := [lemma #570]: #496 -#635 := (not #634) -#359 := (or #358 #635) -#345 := (not #359) -#44 := (f8 f9 #43) -#46 := (f7 #44 f12) -#132 := (= f1 #46) -#145 := (not #132) -#572 := [hypothesis]: #145 -#573 := (or #132 #359) -#360 := (iff #132 #345) -#631 := (or #308 #360) -#353 := [quant-inst #40 #43 #45]: #631 -#568 := [unit-resolution #353 #688]: #360 -#343 := (not #360) -#344 := (or #343 #132 #359) -#346 := [def-axiom]: #344 -#559 := [unit-resolution #346 #568]: #573 -#560 := [unit-resolution #559 #572]: #359 -#599 := (or #308 #613) -#618 := (iff #653 #617) -#615 := (or #308 #618) -#620 := (iff #615 #599) -#463 := (iff #599 #599) -#464 := [rewrite]: #463 -#614 := (iff #618 #613) -#619 := [rewrite]: #614 -#462 := [monotonicity #619]: #620 -#606 := [trans #462 #464]: #620 -#621 := [quant-inst #40 #41 #45]: #615 -#607 := [mp #621 #606]: #599 -#562 := [unit-resolution #607 #688]: #613 -#548 := (or #584 #617) -#655 := (not #653) -#321 := (or #337 #655) -#657 := (not #321) -#49 := (f8 #48 f11) -#50 := (f7 #49 f12) -#136 := (= f1 #50) -#331 := (or #136 #132) -#146 := (iff #136 #145) -#51 := (= #50 f1) -#47 := (= #46 f1) -#52 := (iff #47 #51) -#53 := (not #52) -#149 := (iff #53 #146) -#139 := (iff #132 #136) -#142 := (not #139) -#147 := (iff #142 #146) -#148 := [rewrite]: #147 -#143 := (iff #53 #142) -#140 := (iff #52 #139) -#137 := (iff #51 #136) -#138 := [rewrite]: #137 -#134 := (iff #47 #132) -#135 := [rewrite]: #134 -#141 := [monotonicity #135 #138]: #140 -#144 := [monotonicity #141]: #143 -#150 := [trans #144 #148]: #149 -#131 := [asserted]: #53 -#153 := [mp #131 #150]: #146 -#243 := (not #146) -#330 := (or #136 #132 #243) -#244 := [def-axiom]: #330 -#245 := [unit-resolution #244 #153]: #331 -#563 := [unit-resolution #245 #572]: #136 -#332 := (not #136) -#561 := (or #332 #657) -#654 := (iff #136 #657) -#313 := (or #308 #654) -#310 := (or #655 #337) -#442 := (not #310) -#649 := (iff #136 #442) -#651 := (or #308 #649) -#652 := (iff #651 #313) -#636 := (iff #313 #313) -#297 := [rewrite]: #636 -#660 := (iff #649 #654) -#658 := (iff #442 #657) -#322 := (iff #310 #321) -#656 := [rewrite]: #322 -#659 := [monotonicity #656]: #658 -#650 := [monotonicity #659]: #660 -#293 := [monotonicity #650]: #652 -#298 := [trans #293 #297]: #652 -#309 := [quant-inst #48 #42 #45]: #651 -#299 := [mp #309 #298]: #313 -#564 := [unit-resolution #299 #688]: #654 -#637 := (not #654) -#644 := (or #637 #332 #657) -#646 := [def-axiom]: #644 -#565 := [unit-resolution #646 #564]: #561 -#545 := [unit-resolution #565 #563]: #657 -#639 := (or #321 #653) -#640 := [def-axiom]: #639 -#546 := [unit-resolution #640 #545]: #653 -#578 := (or #584 #617 #655) -#579 := [def-axiom]: #578 -#549 := [unit-resolution #579 #546]: #548 -#550 := [unit-resolution #549 #562]: #617 -#608 := (or #616 #357) -#574 := [def-axiom]: #608 -#551 := [unit-resolution #574 #550]: #357 -#633 := (or #345 #358 #635) -#342 := [def-axiom]: #633 -#552 := [unit-resolution #342 #551 #560]: #635 -#300 := (or #321 #333) -#638 := [def-axiom]: #300 -#553 := [unit-resolution #638 #545]: #333 -#576 := (or #616 #630) -#586 := [def-axiom]: #576 -#554 := [unit-resolution #586 #550]: #630 -#611 := (or #495 #337 #627) -#605 := [def-axiom]: #611 -#555 := [unit-resolution #605 #554 #553]: #495 -#443 := (or #589 #486 #634) -#444 := [def-axiom]: #443 -#556 := [unit-resolution #444 #555 #552 #571]: false -#557 := [lemma #556]: #132 -#547 := (or #145 #345) -#624 := (or #343 #145 #345) -#625 := [def-axiom]: #624 -#558 := [unit-resolution #625 #568]: #547 -#536 := [unit-resolution #558 #557]: #345 -#632 := (or #359 #634) -#629 := [def-axiom]: #632 -#537 := [unit-resolution #629 #536]: #634 -#612 := (or #589 #495 #635) -#441 := [def-axiom]: #612 -#539 := [unit-resolution #441 #537 #571]: #495 -#604 := (or #486 #630) -#610 := [def-axiom]: #604 -#540 := [unit-resolution #610 #539]: #630 -#354 := (or #359 #357) -#628 := [def-axiom]: #354 -#541 := [unit-resolution #628 #536]: #357 -#587 := (or #617 #358 #627) -#588 := [def-axiom]: #587 -#542 := [unit-resolution #588 #541 #540]: #617 -#335 := (or #332 #145) -#323 := (or #332 #145 #243) -#334 := [def-axiom]: #323 -#263 := [unit-resolution #334 #153]: #335 -#543 := [unit-resolution #263 #557]: #332 -#538 := (or #136 #321) -#643 := (or #637 #136 #321) -#279 := [def-axiom]: #643 -#544 := [unit-resolution #279 #564]: #538 -#530 := [unit-resolution #544 #543]: #321 -#609 := (or #486 #333) -#603 := [def-axiom]: #609 -#526 := [unit-resolution #603 #539]: #333 -#641 := (or #657 #337 #655) -#642 := [def-axiom]: #641 -#527 := [unit-resolution #642 #526 #530]: #655 -#580 := (or #584 #616 #653) -#581 := [def-axiom]: #580 -#528 := [unit-resolution #581 #527 #542]: #584 -[unit-resolution #607 #688 #528]: false -unsat -cdbf11c9465d749cfd2e9563f8fc0294f62a631c 18 0 -#2 := false -decl f8 :: S4 -#32 := f8 -#33 := (= f8 f8) -#34 := (not #33) -#115 := (iff #34 false) -#1 := true -#110 := (not true) -#113 := (iff #110 false) -#114 := [rewrite]: #113 -#111 := (iff #34 #110) -#107 := (iff #33 true) -#109 := [rewrite]: #107 -#112 := [monotonicity #109]: #111 -#116 := [trans #112 #114]: #115 -#106 := [asserted]: #34 -[mp #106 #116]: false -unsat bd811011020855800543e0a16a4dcb354fda48ef 31 0 #2 := false decl f1 :: S1