15077 #78 := [not-or-elim #77]: #68 |
15077 #78 := [not-or-elim #77]: #68 |
15078 #141 := [th-lemma arith farkas 1 1]: #64 |
15078 #141 := [th-lemma arith farkas 1 1]: #64 |
15079 #142 := [unit-resolution #141 #78]: #63 |
15079 #142 := [unit-resolution #141 #78]: #63 |
15080 [unit-resolution #142 #85]: false |
15080 [unit-resolution #142 #85]: false |
15081 unsat |
15081 unsat |
|
15082 4d18c87aa576f201e48ea20e31f11fb8675b59d4 8 0 |
|
15083 #2 := false |
|
15084 #1 := true |
|
15085 #33 := (not true) |
|
15086 #63 := (iff #33 false) |
|
15087 #65 := [rewrite]: #63 |
|
15088 #62 := [asserted]: #33 |
|
15089 [mp #62 #65]: false |
|
15090 unsat |
|
15091 ad406fc43130e24f380abadc1fc8a246fab490af 145 0 |
|
15092 #2 := false |
|
15093 decl f3 :: (-> S2 Int S1) |
|
15094 #22 := 42::Int |
|
15095 decl f4 :: (-> S3 Int S2) |
|
15096 #20 := 3::Int |
|
15097 decl f6 :: S3 |
|
15098 #18 := f6 |
|
15099 #21 := (f4 f6 3::Int) |
|
15100 #23 := (f3 #21 42::Int) |
|
15101 decl f1 :: S1 |
|
15102 #4 := f1 |
|
15103 #86 := (= f1 #23) |
|
15104 decl f5 :: S3 |
|
15105 #8 := f5 |
|
15106 #255 := (f4 f5 3::Int) |
|
15107 #246 := (f3 #255 42::Int) |
|
15108 #568 := (= #246 #23) |
|
15109 #207 := (= #23 #246) |
|
15110 #202 := (= #21 #255) |
|
15111 #558 := (= #255 #21) |
|
15112 #83 := (= f5 f6) |
|
15113 #92 := (not #83) |
|
15114 #93 := (or #92 #86) |
|
15115 #98 := (not #93) |
|
15116 #24 := (= #23 f1) |
|
15117 #19 := (= f6 f5) |
|
15118 #25 := (implies #19 #24) |
|
15119 #26 := (not #25) |
|
15120 #99 := (iff #26 #98) |
|
15121 #96 := (iff #25 #93) |
|
15122 #89 := (implies #83 #86) |
|
15123 #94 := (iff #89 #93) |
|
15124 #95 := [rewrite]: #94 |
|
15125 #90 := (iff #25 #89) |
|
15126 #87 := (iff #24 #86) |
|
15127 #88 := [rewrite]: #87 |
|
15128 #84 := (iff #19 #83) |
|
15129 #85 := [rewrite]: #84 |
|
15130 #91 := [monotonicity #85 #88]: #90 |
|
15131 #97 := [trans #91 #95]: #96 |
|
15132 #100 := [monotonicity #97]: #99 |
|
15133 #82 := [asserted]: #26 |
|
15134 #103 := [mp #82 #100]: #98 |
|
15135 #101 := [not-or-elim #103]: #83 |
|
15136 #564 := [monotonicity #101]: #558 |
|
15137 #565 := [symm #564]: #202 |
|
15138 #208 := [monotonicity #565]: #207 |
|
15139 #566 := [symm #208]: #568 |
|
15140 #257 := (= f1 #246) |
|
15141 #11 := (:var 0 Int) |
|
15142 #9 := (:var 1 Int) |
|
15143 #10 := (f4 f5 #9) |
|
15144 #12 := (f3 #10 #11) |
|
15145 #13 := (pattern #12) |
|
15146 #64 := 0::Int |
|
15147 #61 := -1::Int |
|
15148 #62 := (* -1::Int #11) |
|
15149 #63 := (+ #9 #62) |
|
15150 #65 := (<= #63 0::Int) |
|
15151 #47 := (= f1 #12) |
|
15152 #71 := (iff #47 #65) |
|
15153 #76 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #13) #71) |
|
15154 #116 := (~ #76 #76) |
|
15155 #114 := (~ #71 #71) |
|
15156 #115 := [refl]: #114 |
|
15157 #117 := [nnf-pos #115]: #116 |
|
15158 #15 := (<= #9 #11) |
|
15159 #14 := (= #12 f1) |
|
15160 #16 := (iff #14 #15) |
|
15161 #17 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #13) #16) |
|
15162 #79 := (iff #17 #76) |
|
15163 #53 := (iff #15 #47) |
|
15164 #58 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #13) #53) |
|
15165 #77 := (iff #58 #76) |
|
15166 #74 := (iff #53 #71) |
|
15167 #68 := (iff #65 #47) |
|
15168 #72 := (iff #68 #71) |
|
15169 #73 := [rewrite]: #72 |
|
15170 #69 := (iff #53 #68) |
|
15171 #66 := (iff #15 #65) |
|
15172 #67 := [rewrite]: #66 |
|
15173 #70 := [monotonicity #67]: #69 |
|
15174 #75 := [trans #70 #73]: #74 |
|
15175 #78 := [quant-intro #75]: #77 |
|
15176 #59 := (iff #17 #58) |
|
15177 #56 := (iff #16 #53) |
|
15178 #50 := (iff #47 #15) |
|
15179 #54 := (iff #50 #53) |
|
15180 #55 := [rewrite]: #54 |
|
15181 #51 := (iff #16 #50) |
|
15182 #48 := (iff #14 #47) |
|
15183 #49 := [rewrite]: #48 |
|
15184 #52 := [monotonicity #49]: #51 |
|
15185 #57 := [trans #52 #55]: #56 |
|
15186 #60 := [quant-intro #57]: #59 |
|
15187 #80 := [trans #60 #78]: #79 |
|
15188 #46 := [asserted]: #17 |
|
15189 #81 := [mp #46 #80]: #76 |
|
15190 #106 := [mp~ #81 #117]: #76 |
|
15191 #557 := (not #76) |
|
15192 #220 := (or #557 #257) |
|
15193 #168 := (* -1::Int 42::Int) |
|
15194 #253 := (+ 3::Int #168) |
|
15195 #254 := (<= #253 0::Int) |
|
15196 #258 := (iff #257 #254) |
|
15197 #221 := (or #557 #258) |
|
15198 #223 := (iff #221 #220) |
|
15199 #560 := (iff #220 #220) |
|
15200 #561 := [rewrite]: #560 |
|
15201 #573 := (iff #258 #257) |
|
15202 #1 := true |
|
15203 #571 := (iff #257 true) |
|
15204 #572 := (iff #571 #257) |
|
15205 #232 := [rewrite]: #572 |
|
15206 #231 := (iff #258 #571) |
|
15207 #575 := (iff #254 true) |
|
15208 #576 := -39::Int |
|
15209 #245 := (<= -39::Int 0::Int) |
|
15210 #579 := (iff #245 true) |
|
15211 #580 := [rewrite]: #579 |
|
15212 #577 := (iff #254 #245) |
|
15213 #570 := (= #253 -39::Int) |
|
15214 #186 := -42::Int |
|
15215 #260 := (+ 3::Int -42::Int) |
|
15216 #233 := (= #260 -39::Int) |
|
15217 #363 := [rewrite]: #233 |
|
15218 #239 := (= #253 #260) |
|
15219 #259 := (= #168 -42::Int) |
|
15220 #256 := [rewrite]: #259 |
|
15221 #574 := [monotonicity #256]: #239 |
|
15222 #244 := [trans #574 #363]: #570 |
|
15223 #578 := [monotonicity #244]: #577 |
|
15224 #581 := [trans #578 #580]: #575 |
|
15225 #236 := [monotonicity #581]: #231 |
|
15226 #216 := [trans #236 #232]: #573 |
|
15227 #559 := [monotonicity #216]: #223 |
|
15228 #562 := [trans #559 #561]: #223 |
|
15229 #222 := [quant-inst #20 #22]: #221 |
|
15230 #563 := [mp #222 #562]: #220 |
|
15231 #567 := [unit-resolution #563 #106]: #257 |
|
15232 #569 := [trans #567 #566]: #86 |
|
15233 #102 := (not #86) |
|
15234 #104 := [not-or-elim #103]: #102 |
|
15235 [unit-resolution #104 #569]: false |
|
15236 unsat |