67230 unsat |
67230 unsat |
67231 5c9a9ffe9941b81f90170c912034e8b681bc281f 1 0 |
67231 5c9a9ffe9941b81f90170c912034e8b681bc281f 1 0 |
67232 unsat |
67232 unsat |
67233 26a6ebeac1bb75693d61408e7c0984072dfbd2df 1 0 |
67233 26a6ebeac1bb75693d61408e7c0984072dfbd2df 1 0 |
67234 unsat |
67234 unsat |
|
67235 2f894a623075d62f46fa0487301d3cff02b03b4d 123 0 |
|
67236 #2 := false |
|
67237 decl f4 :: S2 |
|
67238 #8 := f4 |
|
67239 decl f3 :: S2 |
|
67240 #7 := f3 |
|
67241 #9 := (= f3 f4) |
|
67242 decl inj!0 :: (-> S3 S2) |
|
67243 decl f6 :: (-> S2 S3) |
|
67244 #28 := (f6 f4) |
|
67245 #179 := (inj!0 #28) |
|
67246 #265 := (= #179 f4) |
|
67247 #18 := (:var 0 S2) |
|
67248 #19 := (f6 #18) |
|
67249 #112 := (pattern #19) |
|
67250 #111 := (inj!0 #19) |
|
67251 #108 := (= #111 #18) |
|
67252 #594 := (forall (vars (k!0 S2)) (:pat #112) #108) |
|
67253 #113 := (forall (vars (k!0 S2)) (:pat #112) #108) |
|
67254 #595 := (iff #113 #594) |
|
67255 #597 := (iff #594 #594) |
|
67256 #598 := [rewrite]: #597 |
|
67257 #596 := [rewrite]: #595 |
|
67258 #599 := [trans #596 #598]: #595 |
|
67259 #16 := (:var 1 S2) |
|
67260 #21 := (= #18 #16) |
|
67261 #17 := (f6 #16) |
|
67262 #20 := (= #17 #19) |
|
67263 #54 := (not #20) |
|
67264 #55 := (or #54 #21) |
|
67265 #58 := (forall (vars (?v0 S2) (?v1 S2)) #55) |
|
67266 #114 := (iff #58 #113) |
|
67267 #115 := [rewrite]: #114 |
|
67268 #118 := (~ #58 #58) |
|
67269 #116 := (~ #55 #55) |
|
67270 #117 := [refl]: #116 |
|
67271 #119 := [nnf-pos #117]: #118 |
|
67272 decl f5 :: S2 |
|
67273 #11 := f5 |
|
67274 #14 := (= f4 f5) |
|
67275 #15 := (not #14) |
|
67276 #12 := (= f3 f5) |
|
67277 #13 := (not #12) |
|
67278 #10 := (not #9) |
|
67279 #82 := (and #10 #13 #15 #58) |
|
67280 #27 := (f6 f3) |
|
67281 #29 := (= #27 #28) |
|
67282 #30 := (not #29) |
|
67283 #85 := (not #82) |
|
67284 #88 := (or #85 #30) |
|
67285 #91 := (not #88) |
|
67286 #22 := (implies #20 #21) |
|
67287 #23 := (forall (vars (?v0 S2) (?v1 S2)) #22) |
|
67288 #24 := (and #15 #23) |
|
67289 #25 := (and #13 #24) |
|
67290 #26 := (and #10 #25) |
|
67291 #31 := (implies #26 #30) |
|
67292 #32 := (not #31) |
|
67293 #94 := (iff #32 #91) |
|
67294 #61 := (and #15 #58) |
|
67295 #64 := (and #13 #61) |
|
67296 #67 := (and #10 #64) |
|
67297 #73 := (not #67) |
|
67298 #74 := (or #73 #30) |
|
67299 #79 := (not #74) |
|
67300 #92 := (iff #79 #91) |
|
67301 #89 := (iff #74 #88) |
|
67302 #86 := (iff #73 #85) |
|
67303 #83 := (iff #67 #82) |
|
67304 #84 := [rewrite]: #83 |
|
67305 #87 := [monotonicity #84]: #86 |
|
67306 #90 := [monotonicity #87]: #89 |
|
67307 #93 := [monotonicity #90]: #92 |
|
67308 #80 := (iff #32 #79) |
|
67309 #77 := (iff #31 #74) |
|
67310 #70 := (implies #67 #30) |
|
67311 #75 := (iff #70 #74) |
|
67312 #76 := [rewrite]: #75 |
|
67313 #71 := (iff #31 #70) |
|
67314 #68 := (iff #26 #67) |
|
67315 #65 := (iff #25 #64) |
|
67316 #62 := (iff #24 #61) |
|
67317 #59 := (iff #23 #58) |
|
67318 #56 := (iff #22 #55) |
|
67319 #57 := [rewrite]: #56 |
|
67320 #60 := [quant-intro #57]: #59 |
|
67321 #63 := [monotonicity #60]: #62 |
|
67322 #66 := [monotonicity #63]: #65 |
|
67323 #69 := [monotonicity #66]: #68 |
|
67324 #72 := [monotonicity #69]: #71 |
|
67325 #78 := [trans #72 #76]: #77 |
|
67326 #81 := [monotonicity #78]: #80 |
|
67327 #95 := [trans #81 #93]: #94 |
|
67328 #53 := [asserted]: #32 |
|
67329 #96 := [mp #53 #95]: #91 |
|
67330 #97 := [not-or-elim #96]: #82 |
|
67331 #101 := [and-elim #97]: #58 |
|
67332 #110 := [mp~ #101 #119]: #58 |
|
67333 #109 := [mp #110 #115]: #113 |
|
67334 #600 := [mp #109 #599]: #594 |
|
67335 #180 := (not #594) |
|
67336 #270 := (or #180 #265) |
|
67337 #267 := [quant-inst #8]: #270 |
|
67338 #250 := [unit-resolution #267 #600]: #265 |
|
67339 #590 := (= f3 #179) |
|
67340 #178 := (inj!0 #27) |
|
67341 #256 := (= #178 #179) |
|
67342 #244 := (= #179 #178) |
|
67343 #269 := (= #28 #27) |
|
67344 #102 := [not-or-elim #96]: #29 |
|
67345 #271 := [symm #102]: #269 |
|
67346 #375 := [monotonicity #271]: #244 |
|
67347 #589 := [symm #375]: #256 |
|
67348 #582 := (= f3 #178) |
|
67349 #264 := (= #178 f3) |
|
67350 #266 := (or #180 #264) |
|
67351 #257 := [quant-inst #7]: #266 |
|
67352 #268 := [unit-resolution #257 #600]: #264 |
|
67353 #255 := [symm #268]: #582 |
|
67354 #591 := [trans #255 #589]: #590 |
|
67355 #592 := [trans #591 #250]: #9 |
|
67356 #98 := [and-elim #97]: #10 |
|
67357 [unit-resolution #98 #592]: false |
|
67358 unsat |
|
67359 dbb5533c26f60f0a5c965d87e1dfccfd73b06e07 152 0 |
|
67360 #2 := false |
|
67361 decl f3 :: (-> S2 S3 S4) |
|
67362 decl f10 :: S3 |
|
67363 #34 := f10 |
|
67364 decl f11 :: S2 |
|
67365 #41 := f11 |
|
67366 #51 := (f3 f11 f10) |
|
67367 decl f4 :: (-> S5 S4 S2) |
|
67368 decl f12 :: S4 |
|
67369 #44 := f12 |
|
67370 decl f5 :: (-> S6 S3 S5) |
|
67371 decl f8 :: S3 |
|
67372 #30 := f8 |
|
67373 decl f6 :: (-> S7 S2 S6) |
|
67374 decl f7 :: S7 |
|
67375 #7 := f7 |
|
67376 #42 := (f6 f7 f11) |
|
67377 #43 := (f5 #42 f8) |
|
67378 #45 := (f4 #43 f12) |
|
67379 #281 := (f3 #45 f10) |
|
67380 #282 := (= #281 #51) |
|
67381 #568 := (= #281 f12) |
|
67382 #567 := (= f10 f8) |
|
67383 #565 := (if #567 #568 #282) |
|
67384 #23 := (:var 0 S3) |
|
67385 #21 := (:var 1 S4) |
|
67386 #19 := (:var 2 S3) |
|
67387 #17 := (:var 3 S2) |
|
67388 #18 := (f6 f7 #17) |
|
67389 #20 := (f5 #18 #19) |
|
67390 #22 := (f4 #20 #21) |
|
67391 #24 := (f3 #22 #23) |
|
67392 #611 := (pattern #24) |
|
67393 #26 := (f3 #17 #23) |
|
67394 #128 := (= #24 #26) |
|
67395 #127 := (= #24 #21) |
|
67396 #25 := (= #23 #19) |
|
67397 #111 := (if #25 #127 #128) |
|
67398 #612 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S4) (?v3 S3)) (:pat #611) #111) |
|
67399 #120 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S4) (?v3 S3)) #111) |
|
67400 #615 := (iff #120 #612) |
|
67401 #613 := (iff #111 #111) |
|
67402 #614 := [refl]: #613 |
|
67403 #616 := [quant-intro #614]: #615 |
|
67404 #27 := (if #25 #21 #26) |
|
67405 #28 := (= #24 #27) |
|
67406 #29 := (forall (vars (?v0 S2) (?v1 S3) (?v2 S4) (?v3 S3)) #28) |
|
67407 #117 := (iff #29 #120) |
|
67408 #112 := (iff #28 #111) |
|
67409 #119 := [rewrite]: #112 |
|
67410 #118 := [quant-intro #119]: #117 |
|
67411 #109 := (~ #29 #29) |
|
67412 #108 := (~ #28 #28) |
|
67413 #125 := [refl]: #108 |
|
67414 #110 := [nnf-pos #125]: #109 |
|
67415 #76 := [asserted]: #29 |
|
67416 #126 := [mp~ #76 #110]: #29 |
|
67417 #115 := [mp #126 #118]: #120 |
|
67418 #617 := [mp #115 #616]: #612 |
|
67419 #385 := (not #612) |
|
67420 #570 := (or #385 #565) |
|
67421 #559 := [quant-inst #41 #30 #44 #34]: #570 |
|
67422 #569 := [unit-resolution #559 #617]: #565 |
|
67423 #561 := (not #567) |
|
67424 #35 := (= f8 f10) |
|
67425 #36 := (not #35) |
|
67426 #546 := (iff #36 #561) |
|
67427 #551 := (iff #35 #567) |
|
67428 #566 := (iff #567 #35) |
|
67429 #550 := [commutativity]: #566 |
|
67430 #552 := [symm #550]: #551 |
|
67431 #547 := [monotonicity #552]: #546 |
|
67432 decl f9 :: S3 |
|
67433 #31 := f9 |
|
67434 #37 := (= f9 f10) |
|
67435 #38 := (not #37) |
|
67436 #32 := (= f8 f9) |
|
67437 #33 := (not #32) |
|
67438 #85 := (and #33 #36 #38) |
|
67439 decl f13 :: S4 |
|
67440 #48 := f13 |
|
67441 #46 := (f6 f7 #45) |
|
67442 #47 := (f5 #46 f9) |
|
67443 #49 := (f4 #47 f13) |
|
67444 #50 := (f3 #49 f10) |
|
67445 #52 := (= #50 #51) |
|
67446 #88 := (not #85) |
|
67447 #91 := (or #88 #52) |
|
67448 #94 := (not #91) |
|
67449 #39 := (and #36 #38) |
|
67450 #40 := (and #33 #39) |
|
67451 #53 := (implies #40 #52) |
|
67452 #54 := (not #53) |
|
67453 #97 := (iff #54 #94) |
|
67454 #78 := (not #40) |
|
67455 #79 := (or #78 #52) |
|
67456 #82 := (not #79) |
|
67457 #95 := (iff #82 #94) |
|
67458 #92 := (iff #79 #91) |
|
67459 #89 := (iff #78 #88) |
|
67460 #86 := (iff #40 #85) |
|
67461 #87 := [rewrite]: #86 |
|
67462 #90 := [monotonicity #87]: #89 |
|
67463 #93 := [monotonicity #90]: #92 |
|
67464 #96 := [monotonicity #93]: #95 |
|
67465 #83 := (iff #54 #82) |
|
67466 #80 := (iff #53 #79) |
|
67467 #81 := [rewrite]: #80 |
|
67468 #84 := [monotonicity #81]: #83 |
|
67469 #98 := [trans #84 #96]: #97 |
|
67470 #77 := [asserted]: #54 |
|
67471 #99 := [mp #77 #98]: #94 |
|
67472 #100 := [not-or-elim #99]: #85 |
|
67473 #102 := [and-elim #100]: #36 |
|
67474 #553 := [mp #102 #547]: #561 |
|
67475 #406 := (not #282) |
|
67476 #104 := (not #52) |
|
67477 #388 := (iff #104 #406) |
|
67478 #428 := (iff #52 #282) |
|
67479 #545 := (iff #282 #52) |
|
67480 #544 := (= #281 #50) |
|
67481 #260 := (= #50 #281) |
|
67482 #279 := (= #50 f13) |
|
67483 #278 := (= f10 f9) |
|
67484 #596 := (if #278 #279 #260) |
|
67485 #592 := (or #385 #596) |
|
67486 #265 := [quant-inst #45 #31 #48 #34]: #592 |
|
67487 #554 := [unit-resolution #265 #617]: #596 |
|
67488 #599 := (not #278) |
|
67489 #387 := (iff #38 #599) |
|
67490 #384 := (iff #37 #278) |
|
67491 #548 := (iff #278 #37) |
|
67492 #555 := [commutativity]: #548 |
|
67493 #386 := [symm #555]: #384 |
|
67494 #540 := [monotonicity #386]: #387 |
|
67495 #103 := [and-elim #100]: #38 |
|
67496 #541 := [mp #103 #540]: #599 |
|
67497 #266 := (not #596) |
|
67498 #602 := (or #266 #278 #260) |
|
67499 #597 := [def-axiom]: #602 |
|
67500 #543 := [unit-resolution #597 #541 #554]: #260 |
|
67501 #542 := [symm #543]: #544 |
|
67502 #427 := [monotonicity #542]: #545 |
|
67503 #429 := [symm #427]: #428 |
|
67504 #536 := [monotonicity #429]: #388 |
|
67505 #105 := [not-or-elim #99]: #104 |
|
67506 #438 := [mp #105 #536]: #406 |
|
67507 #560 := (not #565) |
|
67508 #562 := (or #560 #567 #282) |
|
67509 #563 := [def-axiom]: #562 |
|
67510 [unit-resolution #563 #438 #553 #569]: false |
|
67511 unsat |