67153 #145 := [monotonicity #142]: #144 |
67153 #145 := [monotonicity #142]: #144 |
67154 #149 := [trans #145 #147]: #148 |
67154 #149 := [trans #145 #147]: #148 |
67155 #139 := [asserted]: #53 |
67155 #139 := [asserted]: #53 |
67156 [mp #139 #149]: false |
67156 [mp #139 #149]: false |
67157 unsat |
67157 unsat |
|
67158 f09576464eb9a729afbe3fe966b57e4354456502 30 0 |
|
67159 #2 := false |
|
67160 decl f4 :: (-> S3 S4) |
|
67161 decl f6 :: S3 |
|
67162 #16 := f6 |
|
67163 #17 := (f4 f6) |
|
67164 decl f3 :: (-> S2 S4) |
|
67165 decl f5 :: S2 |
|
67166 #14 := f5 |
|
67167 #15 := (f3 f5) |
|
67168 #18 := (= #15 #17) |
|
67169 #19 := (not #18) |
|
67170 #41 := [asserted]: #19 |
|
67171 #9 := (:var 0 S3) |
|
67172 #10 := (f4 #9) |
|
67173 #7 := (:var 1 S2) |
|
67174 #8 := (f3 #7) |
|
67175 #11 := (pattern #8 #10) |
|
67176 #12 := (= #8 #10) |
|
67177 #13 := (forall (vars (?v0 S2) (?v1 S3)) (:pat #11) #12) |
|
67178 #51 := (~ #13 #13) |
|
67179 #49 := (~ #12 #12) |
|
67180 #50 := [refl]: #49 |
|
67181 #52 := [nnf-pos #50]: #51 |
|
67182 #40 := [asserted]: #13 |
|
67183 #43 := [mp~ #40 #52]: #13 |
|
67184 #111 := (not #13) |
|
67185 #197 := (or #111 #18) |
|
67186 #112 := [quant-inst #14 #16]: #197 |
|
67187 [unit-resolution #112 #43 #41]: false |
|
67188 unsat |
|
67189 5a4509215da405eb20d4081e74524f90aaca407d 1 0 |
|
67190 unsat |
|
67191 ec561a73aaf24cad28c298d64ff90ab9419e03b9 1 0 |
|
67192 unsat |
|
67193 99895ba337908a50454cc51cd8d58f8c9973a5d8 1 0 |
|
67194 unsat |
|
67195 f66af12ea27f7d59df586df568e3d48733d0c2ad 1 0 |
|
67196 unsat |
|
67197 98a1d35ce489ce400102751e60b482d34ba4c100 1 0 |
|
67198 unsat |
|
67199 997d0c877f7a6af3978a25e9a11fe86be44aa3d7 1 0 |
|
67200 unsat |
|
67201 dec47d92e2bc6704596ff538272e4aa7dad033f8 1 0 |
|
67202 unsat |
|
67203 79ff64606be9eaf1430551196cf6a56b904cd2f0 1 0 |
|
67204 unsat |
|
67205 9ddb2d0aa5571f810dbdcf99f2a9c0dd91892822 1 0 |
|
67206 unsat |
|
67207 383af2a9be136c8b9da304961ed7781d6d8b67da 1 0 |
|
67208 unsat |
|
67209 8a45fca8152b4b73650f0bdadc7b4837d03b0e4f 1 0 |
|
67210 unsat |
|
67211 028cbfc14838b1039241d56404b98b994249bd70 1 0 |
|
67212 unsat |
|
67213 0c3c93869b86cd3cceaa64f6505c6b53e5a0d5f5 1 0 |
|
67214 unsat |
|
67215 da5a18ce51a6fcaf95a5da1f3cf6ec44d50d2911 1 0 |
|
67216 unsat |
|
67217 b326e9b62ea312d34250c299905421b42e169a3d 1 0 |
|
67218 unsat |
|
67219 2df9f9573f4c3d690e8e9d39a01fbee0d0dabfca 1 0 |
|
67220 unsat |
|
67221 64fe45c879d2ce11b605b7ccbadec44b7474cdb3 1 0 |
|
67222 unsat |
|
67223 27388d866d376a195719342119d2c39bddbbda5e 1 0 |
|
67224 unsat |
|
67225 4fdb33415d645476800f24bc2645077ed20fbcc7 1 0 |
|
67226 unsat |
|
67227 34954aeef00ac521d8d6983ea46bbdde741af613 1 0 |
|
67228 unsat |
|
67229 c975ecb6377964929f32ae1b30fbd693a2969c6a 1 0 |
|
67230 unsat |
|
67231 5c9a9ffe9941b81f90170c912034e8b681bc281f 1 0 |
|
67232 unsat |
|
67233 26a6ebeac1bb75693d61408e7c0984072dfbd2df 1 0 |
|
67234 unsat |