|
|
|
|
Quelle SMT_Examples.certs
Sprache: unbekannt
|
|
|
f4ff5c44833ca360a0e6110670545870e993732e 6 0
unsat
((set-logic AUFLIA)
(proof
(let ((@x30 (rewrite (= (not true) false))))
(mp (asserted (not true)) @x30 false))))
44c9e70361e406cdaa5515db0484a14de1f3823e 7 0
unsat
((set-logic AUFLIA)
(proof
(let ((@x36 (monotonicity (rewrite (= (or p$ (not p$)) true)) (= (not (or p$ (not p$))) (not true)))))
(let ((@x40 (trans @x36 (rewrite (= (not true) false)) (= (not (or p$ (not p$))) false))))
(mp (asserted (not (or p$ (not p$)))) @x40 false)))))
642064746d4dfc4babb357dafe234a81ef017f2c 9 0
unsat
((set-logic AUFLIA)
(proof
(let ((@x36 (monotonicity (rewrite (= (and p$ true) p$)) (= (= (and p$ true) p$) (= p$ p$)))))
(let ((@x40 (trans @x36 (rewrite (= (= p$ p$) true)) (= (= (and p$ true) p$) true))))
(let ((@x43 (monotonicity @x40 (= (not (= (and p$ true) p$)) (not true)))))
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= (and p$ true) p$)) false))))
(mp (asserted (not (= (and p$ true) p$))) @x47 false)))))))
0a1454d805d51972201b1f0614ae4d2b1ee0c238 13 0
unsat
((set-logic AUFLIA)
(proof
(let (($x33 (not (=> (and (or p$ q$) (not p$)) q$))))
(let (($x37 (= (=> (and (or p$ q$) (not p$)) q$) (or (not (and (or p$ q$) (not p$))) q$))))
(let ((@x41 (monotonicity (rewrite $x37) (= $x33 (not (or (not (and (or p$ q$) (not p$))) q$))))))
(let ((@x44 (mp (asserted $x33) @x41 (not (or (not (and (or p$ q$) (not p$))) q$)))))
(let ((@x45 (and-elim (not-or-elim @x44 (and (or p$ q$) (not p$))) (not p$))))
(let ((@x54 (monotonicity (iff-false @x45 (= p$ false)) (iff-false (not-or-elim @x44 (not q$)) (= q$ false)) (= (or p$ q$) (or false false)))))
(let ((@x58 (trans @x54 (rewrite (= (or false false) false)) (= (or p$ q$) false))))
(let (($x29 (or p$ q$)))
(mp (and-elim (not-or-elim @x44 (and $x29 (not p$))) $x29) @x58 false)))))))))))
34112335b57502835b641cecdefffafb46f85d80 11 0
unsat
((set-logic AUFLIA)
(proof
(let (($x32 (and c$ d$)))
(let (($x29 (and a$ b$)))
(let (($x33 (or $x29 $x32)))
(let (($x34 (=> $x33 $x33)))
(let (($x35 (not $x34)))
(let ((@x45 (trans (monotonicity (rewrite (= $x34 true)) (= $x35 (not true))) (rewrite (= (not true) false)) (= $x35 false))))
(mp (asserted $x35) @x45 false)))))))))
20bc477eba70622207284dac695d9d5d493c254c 23 0
unsat
((set-logic AUFLIA)
(proof
(let (($x33 (and p1$ p3$)))
(let (($x32 (and p3$ p2$)))
(let (($x34 (or $x32 $x33)))
(let (($x35 (=> p1$ $x34)))
(let (($x36 (or $x35 p1$)))
(let (($x29 (and p1$ p2$)))
(let (($x31 (or $x29 p3$)))
(let (($x37 (=> $x31 $x36)))
(let (($x38 (not $x37)))
(let (($x40 (not p1$)))
(let (($x41 (or $x40 $x34)))
(let (($x44 (or $x41 p1$)))
(let (($x50 (not $x31)))
(let (($x51 (or $x50 $x44)))
(let (($x56 (not $x51)))
(let ((@x67 (trans (monotonicity (rewrite (= $x51 true)) (= $x56 (not true))) (rewrite (= (not true) false)) (= $x56 false))))
(let ((@x49 (monotonicity (monotonicity (rewrite (= $x35 $x41)) (= $x36 $x44)) (= $x37 (=> $x31 $x44)))))
(let ((@x58 (monotonicity (trans @x49 (rewrite (= (=> $x31 $x44) $x51)) (= $x37 $x51)) (= $x38 $x56))))
(mp (asserted $x38) (trans @x58 @x67 (= $x38 false)) false)))))))))))))))))))))
31d9c9d3ff37ebd83ab46c7b87647ef17b2c57d5 24 0
unsat
((set-logic AUFLIA)
(proof
(let (($x28 (= p$ p$)))
(let (($x29 (= $x28 p$)))
(let (($x30 (= $x29 p$)))
(let (($x31 (= $x30 p$)))
(let (($x32 (= $x31 p$)))
(let (($x33 (= $x32 p$)))
(let (($x34 (= $x33 p$)))
(let (($x35 (= $x34 p$)))
(let (($x36 (= $x35 p$)))
(let (($x37 (not $x36)))
(let ((@x40 (rewrite (= $x28 true))))
(let ((@x45 (rewrite (= (= true p$) p$))))
(let ((@x47 (trans (monotonicity @x40 (= $x29 (= true p$))) @x45 (= $x29 p$))))
(let ((@x53 (monotonicity (trans (monotonicity @x47 (= $x30 $x28)) @x40 (= $x30 true)) (= $x31 (= true p$)))))
(let ((@x59 (trans (monotonicity (trans @x53 @x45 (= $x31 p$)) (= $x32 $x28)) @x40 (= $x32 true))))
(let ((@x63 (trans (monotonicity @x59 (= $x33 (= true p$))) @x45 (= $x33 p$))))
(let ((@x69 (monotonicity (trans (monotonicity @x63 (= $x34 $x28)) @x40 (= $x34 true)) (= $x35 (= true p$)))))
(let ((@x75 (trans (monotonicity (trans @x69 @x45 (= $x35 p$)) (= $x36 $x28)) @x40 (= $x36 true))))
(let ((@x82 (trans (monotonicity @x75 (= $x37 (not true))) (rewrite (= (not true) false)) (= $x37 false))))
(mp (asserted $x37) @x82 false))))))))))))))))))))))
330b2c9cc52cf5f35a134a2209b0d4127652f7c0 39 0
unsat
((set-logic AUFLIA)
(proof
(let (($x100 (not d$)))
(let (($x45 (not c$)))
(let (($x112 (or p$ (and q$ (not q$)))))
(let (($x113 (and (not p$) $x112)))
(let (($x114 (or c$ $x113)))
(let (($x115 (not $x114)))
(let ((@x121 (monotonicity (rewrite (= (and q$ (not q$)) false)) (= $x112 (or p$ false)))))
(let ((@x128 (monotonicity (trans @x121 (rewrite (= (or p$ false) p$)) (= $x112 p$)) (= $x113 (and (not p$) p$)))))
(let ((@x132 (trans @x128 (rewrite (= (and (not p$) p$) false)) (= $x113 false))))
(let ((@x139 (trans (monotonicity @x132 (= $x114 (or c$ false))) (rewrite (= (or c$ false) c$)) (= $x114 c$))))
(let ((@x153 (iff-false (mp (asserted $x115) (monotonicity @x139 (= $x115 $x45)) $x45) (= c$ false))))
(let ((@x147 (trans (monotonicity @x153 (= (or $x100 c$) (or $x100 false))) (rewrite (= (or $x100 false) $x100)) (= (or $x100 c$) $x100))))
(let (($x103 (or $x100 c$)))
(let ((@x102 (monotonicity (rewrite (= (or d$ false) d$)) (= (not (or d$ false)) $x100))))
(let ((@x108 (mp (asserted (or (not (or d$ false)) c$)) (monotonicity @x102 (= (or (not (or d$ false)) c$) $x103)) $x103)))
(let (($x87 (not b$)))
(let ((@x164 (trans (monotonicity @x153 (= (or $x87 c$) (or $x87 false))) (rewrite (= (or $x87 false) $x87)) (= (or $x87 c$) $x87))))
(let (($x90 (or $x87 c$)))
(let ((@x82 (monotonicity (rewrite (= (or x$ (not x$)) true)) (= (and b$ (or x$ (not x$))) (and b$ true)))))
(let ((@x86 (trans @x82 (rewrite (= (and b$ true) b$)) (= (and b$ (or x$ (not x$))) b$))))
(let ((@x92 (monotonicity (monotonicity @x86 (= (not (and b$ (or x$ (not x$)))) $x87)) (= (or (not (and b$ (or x$ (not x$)))) c$) $x90))))
(let ((@x95 (mp (asserted (or (not (and b$ (or x$ (not x$)))) c$)) @x92 $x90)))
(let (($x64 (not a$)))
(let ((@x170 (monotonicity (iff-false (mp @x95 @x164 $x87) (= b$ false)) (= (or $x64 b$) (or $x64 false)))))
(let ((@x174 (trans @x170 (rewrite (= (or $x64 false) $x64)) (= (or $x64 b$) $x64))))
(let (($x67 (or $x64 b$)))
(let ((@x59 (monotonicity (rewrite (= (and c$ $x45) false)) (= (or a$ (and c$ $x45)) (or a$ false)))))
(let ((@x63 (trans @x59 (rewrite (= (or a$ false) a$)) (= (or a$ (and c$ $x45)) a$))))
(let ((@x69 (monotonicity (monotonicity @x63 (= (not (or a$ (and c$ $x45))) $x64)) (= (or (not (or a$ (and c$ $x45))) b$) $x67))))
(let ((@x175 (mp (mp (asserted (or (not (or a$ (and c$ $x45))) b$)) @x69 $x67) @x174 $x64)))
(let ((@x198 (monotonicity (iff-false @x175 (= a$ false)) (iff-false (mp @x95 @x164 $x87) (= b$ false)) @x153 (iff-false (mp @x108 @x147 $x100) (= d$ false)) (= (or a$ b$ c$ d$) (or false false false false)))))
(let ((@x202 (trans @x198 (rewrite (= (or false false false false) false)) (= (or a$ b$ c$ d$) false))))
(let (($x37 (or a$ b$ c$ d$)))
(let ((@x40 (mp (asserted (or a$ (or b$ (or c$ d$)))) (rewrite (= (or a$ (or b$ (or c$ d$))) $x37)) $x37)))
(mp @x40 @x202 false)))))))))))))))))))))))))))))))))))))
ad87d7e797bdb9354f6592e3ce911c29af823c87 27 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x38 (symm_f$ b$ a$)))
(let ((?x37 (symm_f$ a$ b$)))
(let (($x39 (= ?x37 ?x38)))
(let (($x52 (not $x39)))
(let ((@x47 (monotonicity (rewrite (= (= a$ a$) true)) (= (and (= a$ a$) $x39) (and true $x39)))))
(let ((@x51 (trans @x47 (rewrite (= (and true $x39) $x39)) (= (and (= a$ a$) $x39) $x39))))
(let ((@x57 (mp (asserted (not (and (= a$ a$) $x39))) (monotonicity @x51 (= (not (and (= a$ a$) $x39)) $x52)) $x52)))
(let (($x480 (forall ((?v0 A$) (?v1 A$) )(! (let ((?x30 (symm_f$ ?v1 ?v0)))
(let ((?x29 (symm_f$ ?v0 ?v1)))
(= ?x29 ?x30))) :pattern ( (symm_f$ ?v0 ?v1) ) :pattern ( (symm_f$ ?v1 ?v0) ) :qid k!8))
))
(let (($x32 (forall ((?v0 A$) (?v1 A$) )(! (let ((?x30 (symm_f$ ?v1 ?v0)))
(let ((?x29 (symm_f$ ?v0 ?v1)))
(= ?x29 ?x30))) :qid k!8))
))
(let ((?x30 (symm_f$ ?0 ?1)))
(let ((?x29 (symm_f$ ?1 ?0)))
(let (($x31 (= ?x29 ?x30)))
(let ((@x60 (mp~ (asserted $x32) (nnf-pos (refl (~ $x31 $x31)) (~ $x32 $x32)) $x32)))
(let ((@x485 (mp @x60 (quant-intro (refl (= $x31 $x31)) (= $x32 $x480)) $x480)))
(let (($x149 (or (not $x480) $x39)))
(let ((@x61 ((_ quant-inst a$ b$) $x149)))
(unit-resolution @x61 @x485 @x57 false)))))))))))))))))))
475916706487c818c9d90b517b53e98cbd0b98a4 637 0
unsat
((set-logic AUFLIA)
(proof
(let (($x397 (not x38$)))
(let (($x553 (not x51$)))
(let (($x657 (not x25$)))
(let (($x610 (not x56$)))
(let (($x538 (not x17$)))
(let ((@x897 (hypothesis $x538)))
(let (($x482 (not x45$)))
(let (($x609 (not x22$)))
(let (($x453 (not x11$)))
(let ((@x815 (hypothesis $x453)))
(let (($x667 (not x27$)))
(let (($x638 (not x58$)))
(let (($x567 (not x52$)))
(let ((@x756 (hypothesis $x567)))
(let (($x509 (not x47$)))
(let (($x637 (not x24$)))
(let (($x566 (not x19$)))
(let (($x294 (or x24$ x53$)))
(let ((@x774 (monotonicity (iff-false (asserted (not x59$)) (= x59$ false)) (= (or x59$ x24$ x53$) (or false x24$ x53$)))))
(let ((@x778 (trans @x774 (rewrite (= (or false x24$ x53$) $x294)) (= (or x59$ x24$ x53$) $x294))))
(let (($x303 (or x59$ x24$ x53$)))
(let ((@x306 (mp (asserted (or x59$ $x294)) (rewrite (= (or x59$ $x294) $x303)) $x303)))
(let ((@x779 (mp @x306 @x778 $x294)))
(let ((@x1181 (unit-resolution @x779 (unit-resolution (asserted (or $x637 $x638)) (hypothesis x58$) $x637) x53$)))
(let (($x580 (not x53$)))
(let (($x581 (or $x580 $x566)))
(let ((@x582 (asserted $x581)))
(let ((@x1182 (unit-resolution @x582 @x1181 $x566)))
(let (($x496 (not x46$)))
(let (($x583 (or $x580 $x509)))
(let ((@x584 (asserted $x583)))
(let ((@x1183 (unit-resolution @x584 @x1181 $x509)))
(let (($x438 (not x41$)))
(let (($x363 (not x4$)))
(let (($x347 (not x2$)))
(let (($x336 (not x31$)))
(let (($x623 (not x23$)))
(let (($x645 (or $x638 $x623)))
(let ((@x646 (asserted $x645)))
(let ((@x974 (hypothesis $x509)))
(let ((@x757 (hypothesis $x566)))
(let ((@x853 (hypothesis $x397)))
(let (($x410 (not x8$)))
(let (($x355 (not x3$)))
(let (($x467 (not x12$)))
(let ((@x882 (hypothesis $x467)))
(let ((@x845 (hypothesis $x347)))
(let (($x356 (not x33$)))
(let (($x481 (not x13$)))
(let (($x424 (not x9$)))
(let ((@x728 (hypothesis x41$)))
(let (($x439 (or $x438 $x424)))
(let ((@x440 (asserted $x439)))
(let ((@x922 (unit-resolution @x440 @x728 $x424)))
(let (($x364 (not x34$)))
(let (($x72 (or x35$ x4$)))
(let ((@x77 (asserted $x72)))
(let ((@x994 (unit-resolution @x77 (unit-resolution (asserted (or $x438 (not x35$))) @x728 (not x35$)) x4$)))
(let (($x365 (or $x363 $x364)))
(let ((@x366 (asserted $x365)))
(let ((@x999 (unit-resolution @x366 @x994 $x364)))
(let (($x396 (not x7$)))
(let (($x414 (or $x410 $x396)))
(let ((@x415 (asserted $x414)))
(let (($x348 (not x32$)))
(let ((@x942 (hypothesis $x355)))
(let (($x64 (or x3$ x33$ x2$)))
(let ((@x67 (mp (asserted (or x3$ (or x33$ x2$))) (rewrite (= (or x3$ (or x33$ x2$)) $x64)) $x64)))
(let ((@x1048 (unit-resolution @x67 (unit-resolution (asserted (or $x410 $x356)) (hypothesis x8$) $x356) @x942 x2$)))
(let (($x349 (or $x347 $x348)))
(let ((@x350 (asserted $x349)))
(let (($x105 (or x7$ x38$ x6$ x32$)))
(let ((@x108 (mp (asserted (or x7$ (or x38$ (or x6$ x32$)))) (rewrite (= (or x7$ (or x38$ (or x6$ x32$))) $x105)) $x105)))
(let ((@x842 (unit-resolution @x108 (unit-resolution @x350 @x1048 $x348) (unit-resolution @x415 (hypothesis x8$) $x396) @x853 x6$)))
(let (($x701 (or x1$ x31$)))
(let ((@x700 (monotonicity (iff-false (asserted (not x0$)) (= x0$ false)) (= (or x1$ x31$ x0$) (or x1$ x31$ false)))))
(let ((@x705 (trans @x700 (rewrite (= (or x1$ x31$ false) $x701)) (= (or x1$ x31$ x0$) $x701))))
(let (($x46 (or x1$ x31$ x0$)))
(let ((@x49 (mp (asserted (or x1$ (or x31$ x0$))) (rewrite (= (or x1$ (or x31$ x0$)) $x46)) $x46)))
(let ((@x706 (mp @x49 @x705 $x701)))
(let ((@x1002 (unit-resolution @x706 (unit-resolution (asserted (or $x347 (not x1$))) @x1048 (not x1$)) x31$)))
(let (($x382 (not x6$)))
(let (($x388 (or $x382 $x336)))
(let ((@x389 (asserted $x388)))
(let ((@x1011 (lemma (unit-resolution @x389 @x1002 @x842 false) (or $x410 x38$ x3$))))
(let ((@x952 (unit-resolution @x1011 (unit-resolution (asserted (or $x363 $x355)) @x994 $x355) @x853 $x410)))
(let (($x125 (or x9$ x40$ x8$ x34$)))
(let ((@x128 (mp (asserted (or x9$ (or x40$ (or x8$ x34$)))) (rewrite (= (or x9$ (or x40$ (or x8$ x34$))) $x125)) $x125)))
(let (($x425 (not x40$)))
(let (($x505 (or $x496 $x425)))
(let ((@x506 (asserted $x505)))
(let ((@x868 (unit-resolution @x506 (unit-resolution @x128 @x952 @x999 @x922 x40$) $x496)))
(let (($x239 (or x19$ x52$ x18$ x46$)))
(let ((@x242 (mp (asserted (or x19$ (or x52$ (or x18$ x46$)))) (rewrite (= (or x19$ (or x52$ (or x18$ x46$))) $x239)) $x239)))
(let (($x411 (not x39$)))
(let ((@x992 (unit-resolution @x67 (unit-resolution (asserted (or $x363 $x355)) @x994 $x355) @x845 x33$)))
(let (($x420 (or $x411 $x356)))
(let ((@x421 (asserted $x420)))
(let (($x507 (or $x481 $x425)))
(let ((@x508 (asserted $x507)))
(let ((@x1036 (unit-resolution @x508 (unit-resolution @x128 @x952 @x999 @x922 x40$) $x481)))
(let (($x172 (or x13$ x45$ x12$ x39$)))
(let ((@x175 (mp (asserted (or x13$ (or x45$ (or x12$ x39$)))) (rewrite (= (or x13$ (or x45$ (or x12$ x39$))) $x172)) $x172)))
(let ((@x1037 (unit-resolution @x175 @x1036 @x882 (unit-resolution @x421 @x992 $x411) x45$)))
(let (($x552 (not x18$)))
(let (($x558 (or $x552 $x482)))
(let ((@x559 (asserted $x558)))
(let ((@x1080 (unit-resolution @x559 @x1037 (unit-resolution @x242 @x868 @x757 @x756 x18$) false)))
(let ((@x1051 (unit-resolution (lemma @x1080 (or $x438 x12$ x19$ x52$ x2$ x38$)) @x845 @x757 @x756 @x882 @x853 $x438)))
(let (($x190 (or x47$ x14$ x41$)))
(let ((@x193 (mp (asserted (or x47$ (or x14$ x41$))) (rewrite (= (or x47$ (or x14$ x41$)) $x190)) $x190)))
(let ((@x732 (unit-resolution @x193 @x1051 @x974 x14$)))
(let (($x495 (not x14$)))
(let (($x499 (or $x495 $x481)))
(let ((@x500 (asserted $x499)))
(let ((@x941 (unit-resolution @x242 (unit-resolution (asserted (or $x495 $x496)) @x732 $x496) @x757 @x756 x18$)))
(let ((@x991 (unit-resolution @x175 (unit-resolution @x559 @x941 $x482) @x882 (unit-resolution @x500 @x732 $x481) x39$)))
(let (($x367 (or $x363 $x355)))
(let ((@x368 (asserted $x367)))
(let ((@x980 (unit-resolution @x368 (unit-resolution @x67 (unit-resolution @x421 @x991 $x356) @x845 x3$) $x363)))
(let (($x369 (or $x364 $x355)))
(let ((@x370 (asserted $x369)))
(let ((@x878 (unit-resolution @x370 (unit-resolution @x67 (unit-resolution @x421 @x991 $x356) @x845 x3$) $x364)))
(let ((@x879 (unit-resolution @x128 @x878 (unit-resolution (asserted (or $x495 $x425)) @x732 $x425) (unit-resolution (asserted (or $x410 $x411)) @x991 $x410) x9$)))
(let (($x371 (not x35$)))
(let (($x443 (or $x424 $x371)))
(let ((@x444 (asserted $x443)))
(let ((@x912 (lemma (unit-resolution @x444 @x879 (unit-resolution @x77 @x980 x35$) false) (or x2$ x12$ x19$ x52$ x47$ x38$))))
(let ((@x1091 (unit-resolution @x912 @x882 @x757 @x756 @x974 @x853 x2$)))
(let (($x359 (or $x355 $x347)))
(let ((@x360 (asserted $x359)))
(let ((@x784 (unit-resolution @x706 (unit-resolution (asserted (or $x347 (not x1$))) @x1091 (not x1$)) x31$)))
(let ((@x808 (unit-resolution @x108 (unit-resolution @x389 @x784 $x382) (unit-resolution @x350 @x1091 $x348) @x853 x7$)))
(let (($x418 (or $x411 $x396)))
(let ((@x419 (asserted $x418)))
(let ((@x913 (hypothesis $x410)))
(let ((@x931 (unit-resolution @x193 (unit-resolution @x500 (hypothesis x13$) $x495) @x974 x41$)))
(let ((@x867 (unit-resolution @x128 (unit-resolution @x440 @x931 $x424) (unit-resolution @x508 (hypothesis x13$) $x425) @x913 x34$)))
(let ((@x917 (unit-resolution @x77 (unit-resolution (asserted (or $x438 $x371)) @x931 $x371) x4$)))
(let ((@x1090 (lemma (unit-resolution @x366 @x917 @x867 false) (or $x481 x8$ x47$))))
(let ((@x1056 (unit-resolution @x1090 (unit-resolution @x1011 (unit-resolution @x360 @x1091 $x355) @x853 $x410) @x974 $x481)))
(let ((@x1057 (unit-resolution @x175 @x1056 @x882 (unit-resolution @x419 @x808 $x411) x45$)))
(let ((@x937 (unit-resolution @x242 (unit-resolution @x559 @x1057 $x552) @x757 @x756 x46$)))
(let ((@x884 (unit-resolution @x193 (unit-resolution (asserted (or $x495 $x496)) @x937 $x495) @x974 x41$)))
(let ((@x800 (unit-resolution @x128 (unit-resolution @x440 @x884 $x424) (unit-resolution @x506 @x937 $x425) (unit-resolution @x1011 (unit-resolution @x360 @x1091 $x355) @x853 $x410) x34$)))
(let ((@x864 (unit-resolution @x77 (unit-resolution (asserted (or $x438 $x371)) @x884 $x371) x4$)))
(let ((@x1089 (lemma (unit-resolution @x366 @x864 @x800 false) (or x12$ x47$ x19$ x52$ x38$))))
(let ((@x1116 (unit-resolution @x1089 @x853 @x757 @x756 @x974 x12$)))
(let (($x489 (or $x482 $x467)))
(let ((@x490 (asserted $x489)))
(let (($x539 (not x50$)))
(let (($x619 (or $x610 $x539)))
(let ((@x620 (asserted $x619)))
(let ((@x1058 (unit-resolution @x620 (hypothesis x56$) $x539)))
(let (($x524 (not x16$)))
(let (($x587 (not x20$)))
(let ((@x896 (hypothesis $x539)))
(let (($x517 (not x48$)))
(let ((@x841 (hypothesis $x517)))
(let ((@x989 (unit-resolution @x193 (unit-resolution (asserted (or $x495 $x496)) (hypothesis x46$) $x495) @x974 x41$)))
(let (($x441 (or $x438 $x371)))
(let ((@x442 (asserted $x441)))
(let ((@x838 (unit-resolution @x368 (unit-resolution @x77 (unit-resolution @x442 @x989 $x371) x4$) $x355)))
(let ((@x1053 (unit-resolution @x366 (unit-resolution @x77 (unit-resolution @x442 @x989 $x371) x4$) $x364)))
(let ((@x862 (unit-resolution @x128 @x1053 (unit-resolution @x440 @x989 $x424) (unit-resolution @x506 (hypothesis x46$) $x425) x8$)))
(let (($x416 (or $x410 $x356)))
(let ((@x417 (asserted $x416)))
(let ((@x987 (unit-resolution @x350 (unit-resolution @x67 (unit-resolution @x417 @x862 $x356) @x838 x2$) $x348)))
(let (($x335 (not x1$)))
(let (($x351 (or $x347 $x335)))
(let ((@x352 (asserted $x351)))
(let ((@x935 (unit-resolution @x352 (unit-resolution @x67 (unit-resolution @x417 @x862 $x356) @x838 x2$) $x335)))
(let ((@x746 (unit-resolution @x706 @x935 x31$)))
(let ((@x1060 (unit-resolution @x108 (unit-resolution @x389 @x746 $x382) (unit-resolution @x415 @x862 $x396) @x987 x38$)))
(let (($x479 (or $x453 $x397)))
(let ((@x480 (asserted $x479)))
(let (($x445 (not x10$)))
(let (($x720 (or x5$ x36$)))
(let ((@x719 (monotonicity (iff-false (asserted (not x30$)) (= x30$ false)) (= (or x5$ x36$ x30$) (or x5$ x36$ false)))))
(let ((@x724 (trans @x719 (rewrite (= (or x5$ x36$ false) $x720)) (= (or x5$ x36$ x30$) $x720))))
(let (($x85 (or x5$ x36$ x30$)))
(let ((@x88 (mp (asserted (or x5$ (or x36$ x30$))) (rewrite (= (or x5$ (or x36$ x30$)) $x85)) $x85)))
(let ((@x725 (mp @x88 @x724 $x720)))
(let ((@x810 (unit-resolution @x725 (unit-resolution (asserted (or (not x5$) $x336)) @x746 (not x5$)) x36$)))
(let (($x375 (not x36$)))
(let (($x449 (or $x445 $x375)))
(let ((@x450 (asserted $x449)))
(let (($x152 (or x11$ x43$ x10$ x37$)))
(let ((@x155 (mp (asserted (or x11$ (or x43$ (or x10$ x37$)))) (rewrite (= (or x11$ (or x43$ (or x10$ x37$))) $x152)) $x152)))
(let ((@x840 (unit-resolution @x155 (unit-resolution @x450 @x810 $x445) (unit-resolution (asserted (or (not x37$) $x336)) @x746 (not x37$)) (unit-resolution @x480 @x1060 $x453) x43$)))
(let (($x199 (or x15$ x48$ x42$)))
(let ((@x202 (mp (asserted (or x15$ (or x48$ x42$))) (rewrite (= (or x15$ (or x48$ x42$)) $x199)) $x199)))
(let ((@x712 (unit-resolution @x202 (unit-resolution (asserted (or (not x42$) $x375)) @x810 (not x42$)) @x841 x15$)))
(let (($x454 (not x43$)))
(let (($x516 (not x15$)))
(let (($x536 (or $x516 $x454)))
(let ((@x537 (asserted $x536)))
(let ((@x844 (lemma (unit-resolution @x537 @x712 @x840 false) (or $x496 x48$ x47$))))
(let ((@x893 (unit-resolution @x242 (unit-resolution @x844 @x841 @x974 $x496) @x757 @x756 x18$)))
(let (($x556 (or $x552 $x538)))
(let ((@x557 (asserted $x556)))
(let (($x446 (not x42$)))
(let ((@x1023 (unit-resolution @x559 @x893 $x482)))
(let (($x468 (not x44$)))
(let ((@x738 (unit-resolution @x725 (unit-resolution (asserted (or $x446 $x375)) (hypothesis x42$) $x375) x5$)))
(let (($x374 (not x5$)))
(let (($x394 (or $x374 $x336)))
(let ((@x395 (asserted $x394)))
(let (($x353 (or $x348 $x335)))
(let ((@x354 (asserted $x353)))
(let ((@x1005 (unit-resolution @x354 (unit-resolution @x706 (unit-resolution @x395 @x738 $x336) x1$) $x348)))
(let ((@x983 (unit-resolution @x352 (unit-resolution @x706 (unit-resolution @x395 @x738 $x336) x1$) $x347)))
(let ((@x998 (hypothesis $x482)))
(let ((@x932 (unit-resolution @x128 (unit-resolution @x417 @x992 $x410) @x922 @x999 x40$)))
(let ((@x1030 (hypothesis $x348)))
(let ((@x1031 (hypothesis $x382)))
(let ((@x1039 (unit-resolution @x108 (unit-resolution (asserted (or $x396 $x356)) @x992 $x396) @x1031 @x1030 x38$)))
(let (($x473 (or $x467 $x397)))
(let ((@x474 (asserted $x473)))
(let ((@x971 (unit-resolution @x175 (unit-resolution @x474 @x1039 $x467) (unit-resolution @x508 @x932 $x481) @x998 (unit-resolution @x421 @x992 $x411) false)))
(let ((@x1013 (lemma @x971 (or $x438 x45$ x6$ x32$ x2$))))
(let ((@x1040 (unit-resolution @x1013 (unit-resolution (asserted (or $x382 $x374)) @x738 $x382) @x998 @x1005 @x983 $x438)))
(let (($x447 (or $x445 $x446)))
(let ((@x448 (asserted $x447)))
(let ((@x830 (unit-resolution @x448 (hypothesis x42$) $x445)))
(let ((@x1020 (hypothesis x12$)))
(let (($x469 (or $x467 $x468)))
(let ((@x470 (asserted $x469)))
(let ((@x1021 (unit-resolution @x470 @x1020 $x468)))
(let (($x219 (or x17$ x50$ x16$ x44$)))
(let ((@x222 (mp (asserted (or x17$ (or x50$ (or x16$ x44$)))) (rewrite (= (or x17$ (or x50$ (or x16$ x44$))) $x219)) $x219)))
(let (($x471 (or $x467 $x453)))
(let ((@x472 (asserted $x471)))
(let ((@x889 (unit-resolution @x472 @x1020 $x453)))
(let ((@x924 (unit-resolution @x155 @x889 (hypothesis $x445) (hypothesis (not x37$)) x43$)))
(let (($x530 (or $x524 $x454)))
(let ((@x531 (asserted $x530)))
(let ((@x925 (unit-resolution @x531 @x924 (unit-resolution @x222 @x1021 @x897 @x896 x16$) false)))
(let ((@x1075 (lemma @x925 (or $x467 x10$ x37$ x17$ x50$))))
(let ((@x831 (unit-resolution @x1075 @x830 (unit-resolution (asserted (or (not x37$) $x374)) @x738 (not x37$)) @x897 @x896 $x467)))
(let ((@x856 (unit-resolution @x175 @x831 @x998 (unit-resolution @x500 (unit-resolution @x193 @x1040 @x974 x14$) $x481) x39$)))
(let ((@x715 (unit-resolution @x108 (unit-resolution @x419 @x856 $x396) (unit-resolution (asserted (or $x382 $x374)) @x738 $x382) @x1005 x38$)))
(let (($x477 (or $x468 $x397)))
(let ((@x478 (asserted $x477)))
(let ((@x850 (unit-resolution @x222 (unit-resolution @x478 @x715 $x468) @x897 @x896 x16$)))
(let ((@x828 (unit-resolution @x155 (unit-resolution @x480 @x715 $x453) @x830 (unit-resolution (asserted (or (not x37$) $x374)) @x738 (not x37$)) x43$)))
(let ((@x1001 (lemma (unit-resolution @x531 @x828 @x850 false) (or $x446 x17$ x50$ x45$ x47$))))
(let ((@x762 (unit-resolution @x1001 (unit-resolution @x557 @x893 $x538) @x896 @x1023 @x974 $x446)))
(let (($x528 (or $x524 $x516)))
(let ((@x529 (asserted $x528)))
(let ((@x1017 (unit-resolution @x222 (unit-resolution @x529 (unit-resolution @x202 @x762 @x841 x15$) $x524) (unit-resolution @x557 @x893 $x538) @x896 x44$)))
(let ((@x901 (unit-resolution @x706 (unit-resolution @x395 (hypothesis x5$) $x336) x1$)))
(let ((@x823 (unit-resolution @x108 (unit-resolution @x354 @x901 $x348) @x853 (unit-resolution (asserted (or $x382 $x374)) (hypothesis x5$) $x382) x7$)))
(let ((@x740 (unit-resolution @x1013 (unit-resolution @x354 @x901 $x348) @x998 (unit-resolution (asserted (or $x382 $x374)) (hypothesis x5$) $x382) (unit-resolution @x352 @x901 $x347) $x438)))
(let ((@x835 (unit-resolution @x175 (unit-resolution @x500 (unit-resolution @x193 @x740 @x974 x14$) $x481) (unit-resolution @x419 @x823 $x411) @x998 @x882 false)))
(let ((@x769 (lemma @x835 (or $x374 x45$ x12$ x47$ x38$))))
(let ((@x898 (unit-resolution @x769 @x1023 (unit-resolution @x470 @x1017 $x467) @x974 (unit-resolution @x478 @x1017 $x397) $x374)))
(let ((@x735 (unit-resolution @x155 (unit-resolution @x450 (unit-resolution @x725 @x898 x36$) $x445) (unit-resolution @x537 (unit-resolution @x202 @x762 @x841 x15$) $x454) (unit-resolution (asserted (or $x468 $x453)) @x1017 $x453) x37$)))
(let (($x383 (not x37$)))
(let (($x384 (or $x382 $x383)))
(let ((@x385 (asserted $x384)))
(let ((@x946 (unit-resolution @x706 (unit-resolution (asserted (or $x383 $x336)) @x735 $x336) x1$)))
(let ((@x836 (unit-resolution @x108 (unit-resolution @x354 @x946 $x348) (unit-resolution @x478 @x1017 $x397) (unit-resolution @x385 @x735 $x382) x7$)))
(let ((@x1025 (unit-resolution @x1013 (unit-resolution @x354 @x946 $x348) @x1023 (unit-resolution @x385 @x735 $x382) (unit-resolution @x352 @x946 $x347) $x438)))
(let ((@x886 (unit-resolution @x175 (unit-resolution @x500 (unit-resolution @x193 @x1025 @x974 x14$) $x481) (unit-resolution @x419 @x836 $x411) @x1023 (unit-resolution @x470 @x1017 $x467) false)))
(let ((@x1059 (unit-resolution (lemma @x886 (or x48$ x47$ x50$ x19$ x52$)) @x1058 @x974 @x757 @x756 x48$)))
(let (($x591 (or $x587 $x517)))
(let ((@x592 (asserted $x591)))
(let (($x595 (not x21$)))
(let (($x617 (or $x610 $x595)))
(let ((@x618 (asserted $x617)))
(let (($x596 (not x55$)))
(let (($x302 (or x25$ x54$)))
(let ((@x307 (asserted $x302)))
(let ((@x855 (unit-resolution @x307 (unit-resolution (asserted (or (not x54$) $x517)) @x1059 (not x54$)) x25$)))
(let (($x665 (or $x657 $x596)))
(let ((@x666 (asserted $x665)))
(let (($x266 (or x21$ x55$ x20$ x49$)))
(let ((@x269 (mp (asserted (or x21$ (or x55$ (or x20$ x49$)))) (rewrite (= (or x21$ (or x55$ (or x20$ x49$))) $x266)) $x266)))
(let ((@x911 (unit-resolution @x269 (unit-resolution @x666 @x855 $x596) (unit-resolution @x618 (hypothesis x56$) $x595) (unit-resolution @x592 @x1059 $x587) x49$)))
(let (($x525 (not x49$)))
(let (($x526 (or $x524 $x525)))
(let ((@x527 (asserted $x526)))
(let ((@x1006 (unit-resolution @x242 (unit-resolution @x557 (hypothesis x17$) $x552) @x757 @x756 x46$)))
(let (($x503 (or $x496 $x481)))
(let ((@x504 (asserted $x503)))
(let ((@x752 (unit-resolution @x175 (unit-resolution @x504 @x1006 $x481) (unit-resolution (asserted (or $x538 $x482)) (hypothesis x17$) $x482) @x882 x39$)))
(let (($x412 (or $x410 $x411)))
(let ((@x413 (asserted $x412)))
(let ((@x806 (unit-resolution @x193 (unit-resolution (asserted (or $x495 $x496)) @x1006 $x495) @x974 x41$)))
(let ((@x954 (unit-resolution @x128 (unit-resolution @x440 @x806 $x424) (unit-resolution @x506 @x1006 $x425) (unit-resolution @x413 @x752 $x410) x34$)))
(let ((@x745 (unit-resolution @x366 (unit-resolution @x77 (unit-resolution @x442 @x806 $x371) x4$) @x954 false)))
(let ((@x771 (lemma @x745 (or $x538 x12$ x47$ x19$ x52$))))
(let ((@x928 (unit-resolution @x222 (unit-resolution @x771 @x882 @x974 @x757 @x756 $x538) (hypothesis $x524) @x896 x44$)))
(let ((@x929 (unit-resolution @x478 @x928 $x397)))
(let ((@x832 (hypothesis $x454)))
(let ((@x859 (unit-resolution @x242 (unit-resolution (asserted (or $x495 $x496)) (hypothesis x14$) $x496) @x757 @x756 x18$)))
(let ((@x951 (unit-resolution @x175 (unit-resolution @x559 @x859 $x482) (unit-resolution @x500 (hypothesis x14$) $x481) @x882 x39$)))
(let ((@x833 (unit-resolution @x769 (unit-resolution @x559 @x859 $x482) @x882 @x974 @x853 $x374)))
(let ((@x1076 (unit-resolution @x155 (unit-resolution @x450 (unit-resolution @x725 @x833 x36$) $x445) @x832 @x815 x37$)))
(let ((@x872 (unit-resolution @x108 (unit-resolution @x385 @x1076 $x382) (unit-resolution @x419 @x951 $x396) @x853 x32$)))
(let ((@x962 (unit-resolution @x706 (unit-resolution (asserted (or $x383 $x336)) @x1076 $x336) x1$)))
(let ((@x861 (lemma (unit-resolution @x354 @x962 @x872 false) (or $x495 x38$ x43$ x11$ x12$ x47$ x19$ x52$))))
(let ((@x1079 (unit-resolution @x861 @x929 @x832 (unit-resolution (asserted (or $x468 $x453)) @x928 $x453) @x882 @x974 @x757 @x756 $x495)))
(let ((@x709 (unit-resolution @x77 (unit-resolution @x442 (unit-resolution @x193 @x1079 @x974 x41$) $x371) x4$)))
(let ((@x939 (unit-resolution @x128 (unit-resolution @x1011 @x929 (unit-resolution @x368 @x709 $x355) $x410) (unit-resolution @x440 (unit-resolution @x193 @x1079 @x974 x41$) $x424) (unit-resolution @x366 @x709 $x364) x40$)))
(let ((@x754 (unit-resolution @x242 (unit-resolution @x506 @x939 $x496) @x757 @x756 x18$)))
(let ((@x904 (unit-resolution @x175 (unit-resolution @x559 @x754 $x482) (unit-resolution @x508 @x939 $x481) @x882 x39$)))
(let ((@x877 (unit-resolution @x67 (unit-resolution @x421 @x904 $x356) (unit-resolution @x368 @x709 $x355) x2$)))
(let ((@x927 (unit-resolution @x769 (unit-resolution @x559 @x754 $x482) @x882 @x974 @x929 $x374)))
(let ((@x880 (unit-resolution @x155 (unit-resolution @x450 (unit-resolution @x725 @x927 x36$) $x445) @x832 (unit-resolution (asserted (or $x468 $x453)) @x928 $x453) x37$)))
(let ((@x812 (unit-resolution @x108 (unit-resolution @x385 @x880 $x382) (unit-resolution @x350 @x877 $x348) (unit-resolution @x419 @x904 $x396) @x929 false)))
(let ((@x713 (unit-resolution (lemma @x812 (or x12$ x43$ x47$ x19$ x52$ x16$ x50$)) (unit-resolution (asserted (or $x525 $x454)) @x911 $x454) @x974 @x757 @x756 (unit-resolution @x527 @x911 $x524) @x1058 x12$)))
(let ((@x817 (unit-resolution @x222 (unit-resolution @x470 @x713 $x468) (unit-resolution @x527 @x911 $x524) @x1058 x17$)))
(let ((@x903 (unit-resolution @x242 (unit-resolution @x557 @x817 $x552) @x757 @x756 x46$)))
(let (($x497 (or $x495 $x496)))
(let ((@x498 (asserted $x497)))
(let ((@x748 (unit-resolution @x442 (unit-resolution @x193 (unit-resolution @x498 @x903 $x495) @x974 x41$) $x371)))
(let ((@x1027 (unit-resolution @x440 (unit-resolution @x193 (unit-resolution @x498 @x903 $x495) @x974 x41$) $x424)))
(let ((@x890 (unit-resolution @x128 (unit-resolution @x366 (unit-resolution @x77 @x748 x4$) $x364) (unit-resolution @x506 @x903 $x425) @x1027 x8$)))
(let ((@x891 (unit-resolution @x1011 @x890 (unit-resolution @x368 (unit-resolution @x77 @x748 x4$) $x355) (unit-resolution @x474 @x713 $x397) false)))
(let ((@x1118 (unit-resolution (lemma @x891 (or $x610 x47$ x19$ x52$)) @x974 @x757 @x756 $x610)))
(let ((@x802 (hypothesis $x623)))
(let ((@x914 (hypothesis $x610)))
(let (($x392 (or $x383 $x336)))
(let ((@x393 (asserted $x392)))
(let ((@x969 (unit-resolution @x393 (hypothesis x31$) $x383)))
(let ((@x1047 (unit-resolution @x725 (unit-resolution @x395 (hypothesis x31$) $x374) x36$)))
(let ((@x966 (unit-resolution @x450 @x1047 $x445)))
(let (($x615 (or $x609 $x539)))
(let ((@x616 (asserted $x615)))
(let ((@x730 (unit-resolution @x616 (unit-resolution @x1075 @x966 @x1020 @x897 @x969 x50$) $x609)))
(let (($x286 (or x23$ x57$ x22$ x51$)))
(let ((@x289 (mp (asserted (or x23$ (or x57$ (or x22$ x51$)))) (rewrite (= (or x23$ (or x57$ (or x22$ x51$))) $x286)) $x286)))
(let (($x624 (not x57$)))
(let (($x679 (or $x667 $x624)))
(let ((@x680 (asserted $x679)))
(let ((@x948 (unit-resolution @x680 (unit-resolution @x289 @x730 @x802 (hypothesis $x553) x57$) $x667)))
(let (($x322 (or x27$ x26$ x56$)))
(let ((@x325 (mp (asserted (or x27$ (or x26$ x56$))) (rewrite (= (or x27$ (or x26$ x56$)) $x322)) $x322)))
(let (($x588 (not x54$)))
(let ((@x798 (unit-resolution @x537 (unit-resolution @x155 @x966 @x889 @x969 x43$) $x516)))
(let ((@x799 (unit-resolution @x202 @x798 (unit-resolution (asserted (or $x446 $x375)) @x1047 $x446) x48$)))
(let (($x593 (or $x588 $x517)))
(let ((@x594 (asserted $x593)))
(let (($x660 (not x26$)))
(let (($x661 (or $x660 $x657)))
(let ((@x662 (asserted $x661)))
(let ((@x1094 (unit-resolution @x662 (unit-resolution @x307 (unit-resolution @x594 @x799 $x588) x25$) (unit-resolution @x325 @x948 @x914 x26$) false)))
(let ((@x1096 (lemma @x1094 (or $x336 x56$ x23$ x51$ $x467 x17$))))
(let ((@x1099 (unit-resolution @x1096 (unit-resolution (asserted (or $x552 $x553)) @x859 $x553) @x802 @x914 @x1020 (unit-resolution @x557 @x859 $x538) $x336)))
(let ((@x804 (unit-resolution @x725 (unit-resolution (asserted (or $x382 $x374)) (hypothesis x6$) $x374) x36$)))
(let ((@x1008 (unit-resolution @x1075 (unit-resolution @x450 @x804 $x445) @x1020 @x897 (unit-resolution @x385 (hypothesis x6$) $x383) x50$)))
(let ((@x874 (unit-resolution @x289 (unit-resolution @x616 @x1008 $x609) @x802 (hypothesis $x553) x57$)))
(let ((@x766 (unit-resolution @x155 (unit-resolution @x450 @x804 $x445) @x889 (unit-resolution @x385 (hypothesis x6$) $x383) x43$)))
(let ((@x818 (unit-resolution @x202 (unit-resolution @x537 @x766 $x516) (unit-resolution (asserted (or $x446 $x375)) @x804 $x446) x48$)))
(let ((@x783 (unit-resolution @x662 (unit-resolution @x307 (unit-resolution @x594 @x818 $x588) x25$) (unit-resolution @x325 (unit-resolution @x680 @x874 $x667) @x914 x26$) false)))
(let ((@x737 (lemma @x783 (or $x382 x56$ x23$ x51$ $x467 x17$))))
(let ((@x1102 (unit-resolution @x737 (unit-resolution (asserted (or $x552 $x553)) @x859 $x553) @x802 @x914 @x1020 (unit-resolution @x557 @x859 $x538) $x382)))
(let ((@x1104 (unit-resolution @x108 (unit-resolution @x354 (unit-resolution @x706 @x1099 x1$) $x348) @x1102 @x853 x7$)))
(let (($x422 (or $x396 $x356)))
(let ((@x423 (asserted $x422)))
(let ((@x1106 (unit-resolution @x67 (unit-resolution @x423 @x1104 $x356) (unit-resolution @x352 (unit-resolution @x706 @x1099 x1$) $x347) x3$)))
(let ((@x1112 (unit-resolution @x128 (unit-resolution @x370 @x1106 $x364) (unit-resolution (asserted (or $x495 $x425)) (hypothesis x14$) $x425) (unit-resolution @x415 @x1104 $x410) x9$)))
(let ((@x1113 (unit-resolution @x444 @x1112 (unit-resolution @x77 (unit-resolution @x368 @x1106 $x363) x35$) false)))
(let ((@x1119 (unit-resolution (lemma @x1113 (or $x495 x38$ x23$ x56$ $x467 x19$ x52$)) @x853 @x802 @x1118 @x1116 @x757 @x756 $x495)))
(let ((@x1120 (unit-resolution @x193 @x1119 @x974 x41$)))
(let ((@x1123 (unit-resolution @x366 (unit-resolution @x77 (unit-resolution @x442 @x1120 $x371) x4$) $x364)))
(let ((@x1125 (unit-resolution @x368 (unit-resolution @x77 (unit-resolution @x442 @x1120 $x371) x4$) $x355)))
(let ((@x1127 (unit-resolution @x128 (unit-resolution @x1011 @x1125 @x853 $x410) (unit-resolution @x440 @x1120 $x424) @x1123 x40$)))
(let ((@x1129 (unit-resolution @x242 (unit-resolution @x506 @x1127 $x496) @x757 @x756 x18$)))
(let ((@x1132 (unit-resolution @x737 (unit-resolution (asserted (or $x552 $x553)) @x1129 $x553) @x802 @x1118 @x1116 (unit-resolution @x557 @x1129 $x538) $x382)))
(let ((@x1133 (unit-resolution @x1096 (unit-resolution (asserted (or $x552 $x553)) @x1129 $x553) @x802 @x1118 @x1116 (unit-resolution @x557 @x1129 $x538) $x336)))
(let ((@x1137 (unit-resolution @x1013 (unit-resolution @x354 (unit-resolution @x706 @x1133 x1$) $x348) (unit-resolution @x352 (unit-resolution @x706 @x1133 x1$) $x347) @x1120 @x1132 (unit-resolution @x490 @x1116 $x482) false)))
(let ((@x1185 (unit-resolution (lemma @x1137 (or x38$ x23$ x19$ x52$ x47$)) (unit-resolution @x646 (hypothesis x58$) $x623) @x1182 @x756 @x1183 x38$)))
(let ((@x1188 (unit-resolution @x474 @x1185 $x467)))
(let ((@x1140 (unit-resolution @x155 @x966 @x815 @x969 x43$)))
(let (($x534 (or $x525 $x454)))
(let ((@x535 (asserted $x534)))
(let ((@x1142 (hypothesis $x468)))
(let ((@x1144 (unit-resolution @x222 (unit-resolution @x531 @x1140 $x524) @x897 @x1142 x50$)))
(let (($x621 (or $x595 $x539)))
(let ((@x622 (asserted $x621)))
(let ((@x1147 (unit-resolution @x202 (unit-resolution @x537 @x1140 $x516) (unit-resolution (asserted (or $x446 $x375)) @x1047 $x446) x48$)))
(let ((@x1149 (unit-resolution @x269 (unit-resolution @x592 @x1147 $x587) (unit-resolution @x622 @x1144 $x595) (unit-resolution @x535 @x1140 $x525) x55$)))
(let ((@x1152 (unit-resolution @x666 (unit-resolution @x307 (unit-resolution @x594 @x1147 $x588) x25$) @x1149 false)))
(let ((@x1154 (lemma @x1152 (or $x336 x17$ x44$ x11$))))
(let ((@x1190 (unit-resolution @x1154 (unit-resolution @x771 @x1188 @x1183 @x1182 @x756 $x538) (unit-resolution @x478 @x1185 $x468) (unit-resolution @x480 @x1185 $x453) $x336)))
(let ((@x1156 (unit-resolution @x559 (unit-resolution @x1013 @x728 @x1030 @x1031 @x845 x45$) $x552)))
(let ((@x1159 (unit-resolution @x506 (unit-resolution @x128 @x999 @x913 @x922 x40$) (unit-resolution @x242 @x1156 @x757 @x756 x46$) false)))
(let ((@x1163 (unit-resolution (lemma @x1159 (or $x438 x8$ x19$ x52$ x32$ x6$ x2$)) @x913 @x757 @x756 @x1030 @x1031 @x845 $x438)))
(let ((@x1166 (unit-resolution @x242 (unit-resolution @x498 (unit-resolution @x193 @x1163 @x974 x14$) $x496) @x757 @x756 x18$)))
(let ((@x1168 (unit-resolution @x175 (unit-resolution @x559 @x1166 $x482) @x882 (unit-resolution @x1090 @x913 @x974 $x481) x39$)))
(let ((@x1171 (unit-resolution @x368 (unit-resolution @x67 (unit-resolution @x421 @x1168 $x356) @x845 x3$) $x363)))
(let (($x501 (or $x495 $x425)))
(let ((@x502 (asserted $x501)))
(let ((@x1174 (unit-resolution @x370 (unit-resolution @x67 (unit-resolution @x421 @x1168 $x356) @x845 x3$) $x364)))
(let ((@x1175 (unit-resolution @x128 @x1174 @x913 (unit-resolution @x502 (unit-resolution @x193 @x1163 @x974 x14$) $x425) x9$)))
(let ((@x1178 (lemma (unit-resolution @x444 @x1175 (unit-resolution @x77 @x1171 x35$) false) (or x8$ x2$ x12$ x19$ x52$ x47$ x32$ x6$))))
(let ((@x1195 (unit-resolution @x1178 (unit-resolution @x352 (unit-resolution @x706 @x1190 x1$) $x347) @x1188 @x1182 @x756 @x1183 (unit-resolution (asserted (or $x397 $x348)) @x1185 $x348) (unit-resolution (asserted (or $x397 $x382)) @x1185 $x382) x8$)))
(let ((@x1197 (unit-resolution @x67 (unit-resolution @x417 @x1195 $x356) (unit-resolution @x352 (unit-resolution @x706 @x1190 x1$) $x347) x3$)))
(let ((@x1200 (unit-resolution @x442 (unit-resolution @x77 (unit-resolution @x368 @x1197 $x363) x35$) $x438)))
(let ((@x1203 (unit-resolution @x242 (unit-resolution @x498 (unit-resolution @x193 @x1200 @x1183 x14$) $x496) @x1182 @x756 x18$)))
(let ((@x1206 (unit-resolution @x175 (unit-resolution @x500 (unit-resolution @x193 @x1200 @x1183 x14$) $x481) @x1188 (unit-resolution @x413 @x1195 $x411) x45$)))
(let ((@x1215 (unit-resolution (lemma (unit-resolution @x559 @x1206 @x1203 false) (or $x638 x52$)) @x756 $x638)))
(let (($x328 (or x28$ x58$)))
(let ((@x792 (monotonicity (iff-false (asserted (not x29$)) (= x29$ false)) (= (or x29$ x28$ x58$) (or false x28$ x58$)))))
(let ((@x796 (trans @x792 (rewrite (= (or false x28$ x58$) $x328)) (= (or x29$ x28$ x58$) $x328))))
(let (($x337 (or x29$ x28$ x58$)))
(let ((@x340 (mp (asserted (or x29$ $x328)) (rewrite (= (or x29$ $x328) $x337)) $x337)))
(let ((@x797 (mp @x340 @x796 $x328)))
(let (($x674 (not x28$)))
(let (($x675 (or $x674 $x667)))
(let ((@x676 (asserted $x675)))
(let ((@x1224 (unit-resolution @x676 (unit-resolution @x797 @x1215 x28$) $x667)))
(let ((@x1285 (hypothesis $x438)))
(let ((@x708 (hypothesis $x411)))
(let ((@x1210 (hypothesis $x496)))
(let ((@x1213 (unit-resolution @x242 (unit-resolution (asserted (or $x566 $x509)) (hypothesis x47$) $x566) @x1210 @x756 x18$)))
(let (($x554 (or $x552 $x553)))
(let ((@x555 (asserted $x554)))
(let (($x677 (or $x674 $x624)))
(let ((@x678 (asserted $x677)))
(let ((@x1217 (unit-resolution @x678 (unit-resolution @x797 @x1215 x28$) $x624)))
(let ((@x1219 (unit-resolution @x779 (unit-resolution @x584 (hypothesis x47$) $x580) x24$)))
(let (($x641 (or $x637 $x623)))
(let ((@x642 (asserted $x641)))
(let ((@x1221 (unit-resolution @x289 (unit-resolution @x642 @x1219 $x623) @x1217 (unit-resolution @x555 @x1213 $x553) x22$)))
(let ((@x1226 (unit-resolution @x325 (unit-resolution (asserted (or $x609 $x610)) @x1221 $x610) @x1224 x26$)))
(let (($x663 (or $x660 $x596)))
(let ((@x664 (asserted $x663)))
(let (($x589 (or $x587 $x588)))
(let ((@x590 (asserted $x589)))
(let ((@x1231 (unit-resolution @x590 (unit-resolution @x307 (unit-resolution @x662 @x1226 $x657) x54$) $x587)))
(let ((@x1232 (unit-resolution @x269 @x1231 (unit-resolution (asserted (or $x609 $x595)) @x1221 $x595) (unit-resolution @x664 @x1226 $x596) x49$)))
(let ((@x1234 (unit-resolution @x222 (unit-resolution @x527 @x1232 $x524) (unit-resolution @x557 @x1213 $x538) (unit-resolution @x616 @x1221 $x539) x44$)))
(let (($x475 (or $x468 $x453)))
(let ((@x476 (asserted $x475)))
(let ((@x1237 (unit-resolution @x594 (unit-resolution @x307 (unit-resolution @x662 @x1226 $x657) x54$) $x517)))
(let ((@x1239 (unit-resolution @x202 (unit-resolution (asserted (or $x525 $x516)) @x1232 $x516) @x1237 x42$)))
(let ((@x1241 (unit-resolution @x155 (unit-resolution @x448 @x1239 $x445) (unit-resolution @x535 @x1232 $x454) (unit-resolution @x476 @x1234 $x453) x37$)))
(let ((@x1243 (unit-resolution @x725 (unit-resolution (asserted (or $x446 $x375)) @x1239 $x375) x5$)))
(let (($x390 (or $x383 $x374)))
(let ((@x391 (asserted $x390)))
(let ((@x1246 (lemma (unit-resolution @x391 @x1243 @x1241 false) (or $x509 x46$ x52$))))
(let ((@x1247 (unit-resolution @x1246 @x1210 @x756 $x509)))
(let ((@x1249 (unit-resolution @x175 (unit-resolution @x1090 @x1247 @x913 $x481) @x882 @x708 x45$)))
(let (($x562 (or $x553 $x482)))
(let ((@x563 (asserted $x562)))
(let ((@x1252 (unit-resolution @x242 (unit-resolution @x559 @x1249 $x552) @x1210 @x756 x19$)))
(let ((@x1255 (unit-resolution @x642 (unit-resolution @x779 (unit-resolution @x582 @x1252 $x580) x24$) $x623)))
(let ((@x1256 (unit-resolution @x289 @x1255 @x1217 (unit-resolution @x563 @x1249 $x553) x22$)))
(let ((@x1260 (unit-resolution @x325 (unit-resolution (asserted (or $x609 $x610)) @x1256 $x610) @x1224 x26$)))
(let ((@x1265 (unit-resolution @x590 (unit-resolution @x307 (unit-resolution @x662 @x1260 $x657) x54$) $x587)))
(let ((@x1266 (unit-resolution @x269 @x1265 (unit-resolution (asserted (or $x609 $x595)) @x1256 $x595) (unit-resolution @x664 @x1260 $x596) x49$)))
(let ((@x1268 (unit-resolution @x222 (unit-resolution @x527 @x1266 $x524) (unit-resolution (asserted (or $x538 $x482)) @x1249 $x538) (unit-resolution @x616 @x1256 $x539) x44$)))
(let ((@x1271 (unit-resolution @x594 (unit-resolution @x307 (unit-resolution @x662 @x1260 $x657) x54$) $x517)))
(let ((@x1273 (unit-resolution @x202 (unit-resolution (asserted (or $x525 $x516)) @x1266 $x516) @x1271 x42$)))
(let ((@x1275 (unit-resolution @x155 (unit-resolution @x448 @x1273 $x445) (unit-resolution @x535 @x1266 $x454) (unit-resolution @x476 @x1268 $x453) x37$)))
(let ((@x1277 (unit-resolution @x725 (unit-resolution (asserted (or $x446 $x375)) @x1273 $x375) x5$)))
(let ((@x1280 (lemma (unit-resolution @x391 @x1277 @x1275 false) (or x46$ x52$ x12$ x39$ x8$))))
(let ((@x1282 (unit-resolution @x504 (unit-resolution @x1280 @x708 @x882 @x756 @x913 x46$) $x481)))
(let ((@x1284 (unit-resolution @x563 (unit-resolution @x175 @x1282 @x882 @x708 x45$) $x553)))
(let ((@x1286 (unit-resolution @x498 (unit-resolution @x1280 @x708 @x882 @x756 @x913 x46$) $x495)))
(let ((@x1289 (unit-resolution @x779 (unit-resolution @x584 (unit-resolution @x193 @x1286 @x1285 x47$) $x580) x24$)))
(let ((@x1291 (unit-resolution @x289 (unit-resolution @x642 @x1289 $x623) @x1217 @x1284 x22$)))
(let (($x564 (or $x538 $x482)))
(let ((@x565 (asserted $x564)))
(let ((@x1293 (unit-resolution @x565 (unit-resolution @x175 @x1282 @x882 @x708 x45$) $x538)))
(let ((@x1295 (unit-resolution @x325 (unit-resolution (asserted (or $x609 $x610)) @x1291 $x610) @x1224 x26$)))
(let ((@x1300 (unit-resolution @x590 (unit-resolution @x307 (unit-resolution @x662 @x1295 $x657) x54$) $x587))) | | |
