Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/SMT_Examples/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 300 kB

Impressum SMT_Examples.certs Sprache: Lisp

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)))
(let ((@x1301 (unit-resolution @x269 @x1300 (unit-resolution (asserted (or $x609 $x595)) @x1291 $x595) (unit-resolution @x664 @x1295 $x596) x49$)))
(let ((@x1303 (unit-resolution @x222 (unit-resolution @x527 @x1301 $x524) @x1293 (unit-resolution @x616 @x1291 $x539) x44$)))
(let ((@x1306 (unit-resolution @x594 (unit-resolution @x307 (unit-resolution @x662 @x1295 $x657) x54$) $x517)))
(let ((@x1308 (unit-resolution @x202 (unit-resolution (asserted (or $x525 $x516)) @x1301 $x516) @x1306 x42$)))
(let ((@x1310 (unit-resolution @x155 (unit-resolution @x448 @x1308 $x445) (unit-resolution @x535 @x1301 $x454) (unit-resolution @x476 @x1303 $x453) x37$)))
(let ((@x1312 (unit-resolution @x725 (unit-resolution (asserted (or $x446 $x375)) @x1308 $x375) x5$)))
(let ((@x1315 (lemma (unit-resolution @x391 @x1312 @x1310 false) (or x39$ x12$ x41$ x52$ x8$))))
(let ((@x1317 (unit-resolution @x421 (unit-resolution @x1315 @x1285 @x882 @x756 @x913 x39$) $x356)))
(let ((@x1321 (unit-resolution @x77 (unit-resolution @x368 (unit-resolution @x67 @x1317 @x845 x3$) $x363) x35$)))
(let ((@x1323 (unit-resolution @x128 (unit-resolution @x444 @x1321 $x424) @x913 (unit-resolution @x370 (unit-resolution @x67 @x1317 @x845 x3$) $x364) x40$)))
(let ((@x1327 (unit-resolution @x1246 (unit-resolution @x193 (unit-resolution @x502 @x1323 $x495) @x1285 x47$) (unit-resolution @x506 @x1323 $x496) @x756 false)))
(let ((@x1330 (unit-resolution (lemma @x1327 (or x41$ x52$ x8$ x2$ x12$)) @x845 @x913 @x756 @x882 x41$)))
(let ((@x1334 (unit-resolution @x366 (unit-resolution @x77 (unit-resolution @x442 @x1330 $x371) x4$) $x364)))
(let ((@x1335 (unit-resolution @x128 @x1334 @x913 (unit-resolution @x440 @x1330 $x424) x40$)))
(let ((@x1337 (unit-resolution @x368 (unit-resolution @x77 (unit-resolution @x442 @x1330 $x371) x4$) $x355)))
(let ((@x1340 (unit-resolution @x1280 (unit-resolution @x421 (unit-resolution @x67 @x1337 @x845 x33$) $x411) (unit-resolution @x506 @x1335 $x496) @x882 @x756 @x913 false)))
(let ((@x1343 (unit-resolution (lemma @x1340 (or x2$ x12$ x52$ x8$)) @x913 @x756 @x882 x2$)))
(let ((@x1345 (unit-resolution @x706 (unit-resolution @x352 @x1343 $x335) x31$)))
(let (($x451 (or $x446 $x375)))
(let ((@x452 (asserted $x451)))
(let ((@x1348 (unit-resolution @x452 (unit-resolution @x725 (unit-resolution @x395 @x1345 $x374) x36$) $x446)))
(let ((@x1349 (unit-resolution @x450 (unit-resolution @x725 (unit-resolution @x395 @x1345 $x374) x36$) $x445)))
(let ((@x1354 (unit-resolution @x419 (unit-resolution @x1280 @x1210 @x882 @x756 @x913 x39$) $x396)))
(let ((@x1355 (unit-resolution @x108 @x1354 (unit-resolution @x350 @x1343 $x348) (unit-resolution @x389 @x1345 $x382) x38$)))
(let ((@x1357 (unit-resolution @x155 (unit-resolution @x480 @x1355 $x453) (unit-resolution @x393 @x1345 $x383) @x1349 x43$)))
(let ((@x1360 (unit-resolution @x594 (unit-resolution @x202 (unit-resolution @x537 @x1357 $x516) @x1348 x48$) $x588)))
(let ((@x1364 (unit-resolution @x1154 (unit-resolution @x478 @x1355 $x468) @x1345 (unit-resolution @x480 @x1355 $x453) x17$)))
(let (($x560 (or $x553 $x538)))
(let ((@x561 (asserted $x560)))
(let ((@x1367 (unit-resolution @x582 (unit-resolution @x771 @x1364 @x882 @x1247 @x756 x19$) $x580)))
(let ((@x1370 (unit-resolution @x289 (unit-resolution @x642 (unit-resolution @x779 @x1367 x24$) $x623) @x1217 (unit-resolution @x561 @x1364 $x553) x22$)))
(let (($x611 (or $x609 $x610)))
(let ((@x612 (asserted $x611)))
(let ((@x1372 (unit-resolution @x325 (unit-resolution @x612 @x1370 $x610) (unit-resolution @x662 (unit-resolution @x307 @x1360 x25$) $x660) @x1224 false)))
(let ((@x1384 (unit-resolution (lemma @x1372 (or x46$ x12$ x52$ x8$)) @x913 @x756 @x882 x46$)))
(let ((@x1376 (unit-resolution (lemma @x891 (or $x610 x47$ x19$ x52$)) @x974 (unit-resolution (asserted (or $x566 $x496)) (hypothesis x46$) $x566) @x756 $x610)))
(let ((@x1379 (unit-resolution @x594 (unit-resolution @x844 @x974 (hypothesis x46$) x48$) $x588)))
(let ((@x1381 (unit-resolution @x662 (unit-resolution @x307 @x1379 x25$) (unit-resolution @x325 @x1376 @x1224 x26$) false)))
(let ((@x1383 (lemma @x1381 (or x47$ x52$ $x496))))
(let (($x512 (or $x509 $x438)))
(let ((@x513 (asserted $x512)))
(let ((@x1387 (unit-resolution @x1315 (unit-resolution @x513 (unit-resolution @x1383 @x1384 @x756 x47$) $x438) @x882 @x756 @x913 x39$)))
(let ((@x1389 (unit-resolution @x108 (unit-resolution @x419 @x1387 $x396) (unit-resolution @x350 @x1343 $x348) (unit-resolution @x389 @x1345 $x382) x38$)))
(let ((@x1391 (unit-resolution @x155 (unit-resolution @x480 @x1389 $x453) (unit-resolution @x393 @x1345 $x383) @x1349 x43$)))
(let ((@x1394 (unit-resolution @x594 (unit-resolution @x202 (unit-resolution @x537 @x1391 $x516) @x1348 x48$) $x588)))
(let ((@x1397 (unit-resolution @x779 (unit-resolution @x584 (unit-resolution @x1383 @x1384 @x756 x47$) $x580) x24$)))
(let ((@x1400 (unit-resolution @x1154 (unit-resolution @x480 @x1389 $x453) @x1345 (unit-resolution @x478 @x1389 $x468) x17$)))
(let ((@x1402 (unit-resolution @x289 (unit-resolution @x561 @x1400 $x553) @x1217 (unit-resolution @x642 @x1397 $x623) x22$)))
(let ((@x1405 (unit-resolution @x662 (unit-resolution @x325 (unit-resolution @x612 @x1402 $x610) @x1224 x26$) (unit-resolution @x307 @x1394 x25$) false)))
(let ((@x1440 (unit-resolution (lemma @x1405 (or x8$ x12$ x52$)) @x882 @x756 x8$)))
(let ((@x1411 (unit-resolution @x242 (unit-resolution @x559 (hypothesis x45$) $x552) @x1210 @x756 x19$)))
(let ((@x1414 (unit-resolution @x642 (unit-resolution @x779 (unit-resolution @x582 @x1411 $x580) x24$) $x623)))
(let ((@x1415 (unit-resolution @x289 @x1414 @x1217 (unit-resolution @x563 (hypothesis x45$) $x553) x22$)))
(let ((@x1418 (unit-resolution @x662 (unit-resolution @x325 (unit-resolution @x612 @x1415 $x610) @x1224 x26$) $x657)))
(let ((@x1421 (unit-resolution @x664 (unit-resolution @x325 (unit-resolution @x612 @x1415 $x610) @x1224 x26$) $x596)))
(let ((@x1424 (unit-resolution @x269 (unit-resolution @x590 (unit-resolution @x307 @x1418 x54$) $x587) (unit-resolution (asserted (or $x609 $x595)) @x1415 $x595) @x1421 x49$)))
(let (($x532 (or $x525 $x516)))
(let ((@x533 (asserted $x532)))
(let ((@x1426 (unit-resolution @x202 (unit-resolution @x533 @x1424 $x516) (unit-resolution @x594 (unit-resolution @x307 @x1418 x54$) $x517) x42$)))
(let ((@x1432 (unit-resolution @x222 (unit-resolution @x527 @x1424 $x524) (unit-resolution @x565 (hypothesis x45$) $x538) (unit-resolution @x616 @x1415 $x539) x44$)))
(let ((@x1434 (unit-resolution @x155 (unit-resolution @x476 @x1432 $x453) (unit-resolution @x535 @x1424 $x454) (unit-resolution @x448 @x1426 $x445) x37$)))
(let ((@x1437 (unit-resolution @x391 (unit-resolution @x725 (unit-resolution @x452 @x1426 $x375) x5$) @x1434 false)))
(let ((@x1444 (unit-resolution @x175 (unit-resolution (lemma @x1437 (or $x482 x46$ x52$)) @x1210 @x756 $x482) @x882 (unit-resolution @x413 @x1440 $x411) x13$)))
(let ((@x1447 (unit-resolution @x442 (unit-resolution @x193 (unit-resolution @x500 @x1444 $x495) @x1247 x41$) $x371)))
(let ((@x1450 (unit-resolution @x67 (unit-resolution @x368 (unit-resolution @x77 @x1447 x4$) $x355) (unit-resolution @x417 @x1440 $x356) x2$)))
(let ((@x1452 (unit-resolution @x706 (unit-resolution @x352 @x1450 $x335) x31$)))
(let ((@x1455 (unit-resolution @x452 (unit-resolution @x725 (unit-resolution @x395 @x1452 $x374) x36$) $x446)))
(let ((@x1457 (unit-resolution @x1011 (unit-resolution @x368 (unit-resolution @x77 @x1447 x4$) $x355) @x1440 x38$)))
(let ((@x1459 (unit-resolution @x450 (unit-resolution @x725 (unit-resolution @x395 @x1452 $x374) x36$) $x445)))
(let ((@x1460 (unit-resolution @x155 @x1459 (unit-resolution @x480 @x1457 $x453) (unit-resolution @x393 @x1452 $x383) x43$)))
(let ((@x1463 (unit-resolution @x594 (unit-resolution @x202 (unit-resolution @x537 @x1460 $x516) @x1455 x48$) $x588)))
(let ((@x1466 (unit-resolution @x1154 @x1452 (unit-resolution @x478 @x1457 $x468) (unit-resolution @x480 @x1457 $x453) x17$)))
(let ((@x1469 (unit-resolution @x582 (unit-resolution @x771 @x1466 @x882 @x1247 @x756 x19$) $x580)))
(let ((@x1472 (unit-resolution @x289 (unit-resolution @x642 (unit-resolution @x779 @x1469 x24$) $x623) @x1217 (unit-resolution @x561 @x1466 $x553) x22$)))
(let ((@x1475 (unit-resolution @x662 (unit-resolution @x325 (unit-resolution @x612 @x1472 $x610) @x1224 x26$) (unit-resolution @x307 @x1463 x25$) false)))
(let ((@x1478 (unit-resolution (lemma @x1475 (or x46$ x12$ x52$)) @x882 @x756 x46$)))
(let ((@x1480 (unit-resolution @x175 (unit-resolution @x504 @x1478 $x481) @x882 (unit-resolution @x413 @x1440 $x411) x45$)))
(let ((@x1484 (unit-resolution @x779 (unit-resolution @x584 (unit-resolution @x1383 @x1478 @x756 x47$) $x580) x24$)))
(let ((@x1486 (unit-resolution @x289 (unit-resolution @x642 @x1484 $x623) @x1217 (unit-resolution @x563 @x1480 $x553) x22$)))
(let ((@x1491 (unit-resolution @x664 (unit-resolution @x325 (unit-resolution @x612 @x1486 $x610) @x1224 x26$) $x596)))
(let ((@x1493 (unit-resolution @x662 (unit-resolution @x325 (unit-resolution @x612 @x1486 $x610) @x1224 x26$) $x657)))
(let ((@x1496 (unit-resolution @x269 (unit-resolution @x590 (unit-resolution @x307 @x1493 x54$) $x587) (unit-resolution (asserted (or $x609 $x595)) @x1486 $x595) @x1491 x49$)))
(let ((@x1498 (unit-resolution @x222 (unit-resolution @x527 @x1496 $x524) (unit-resolution @x565 @x1480 $x538) (unit-resolution @x616 @x1486 $x539) x44$)))
(let ((@x1503 (unit-resolution @x202 (unit-resolution @x533 @x1496 $x516) (unit-resolution @x594 (unit-resolution @x307 @x1493 x54$) $x517) x42$)))
(let ((@x1505 (unit-resolution @x155 (unit-resolution @x448 @x1503 $x445) (unit-resolution @x535 @x1496 $x454) (unit-resolution @x476 @x1498 $x453) x37$)))
(let ((@x1508 (unit-resolution @x391 (unit-resolution @x725 (unit-resolution @x452 @x1503 $x375) x5$) @x1505 false)))
(let ((@x1576 (unit-resolution @x472 (unit-resolution (lemma @x1508 (or x12$ x52$)) @x756 x12$) $x453)))
(let ((@x1547 (hypothesis $x667)))
(let ((@x1557 (unit-resolution @x325 (unit-resolution @x612 (hypothesis x22$) $x610) @x1547 x26$)))
(let ((@x1561 (unit-resolution @x590 (unit-resolution @x307 (unit-resolution @x662 @x1557 $x657) x54$) $x587)))
(let ((@x1562 (unit-resolution @x269 @x1561 (unit-resolution @x664 @x1557 $x596) (unit-resolution (asserted (or $x609 $x595)) (hypothesis x22$) $x595) x49$)))
(let ((@x1564 (unit-resolution @x594 (unit-resolution @x307 (unit-resolution @x662 @x1557 $x657) x54$) $x517)))
(let ((@x1512 (unit-resolution @x391 @x738 (unit-resolution @x155 @x830 @x832 @x815 x37$) false)))
(let ((@x1514 (lemma @x1512 (or $x446 x43$ x11$))))
(let ((@x1567 (unit-resolution @x1514 (unit-resolution @x202 (unit-resolution @x533 @x1562 $x516) @x1564 x42$) (unit-resolution @x535 @x1562 $x454) @x815 false)))
(let ((@x1569 (lemma @x1567 (or $x609 x11$ x27$))))
(let ((@x1584 (hypothesis $x446)))
(let ((@x1587 (unit-resolution @x307 (unit-resolution @x662 (hypothesis x26$) $x657) x54$)))
(let ((@x1590 (unit-resolution @x529 (unit-resolution @x202 (unit-resolution @x594 @x1587 $x517) @x1584 x15$) $x524)))
(let ((@x1594 (unit-resolution @x533 (unit-resolution @x202 (unit-resolution @x594 @x1587 $x517) @x1584 x15$) $x525)))
(let ((@x1595 (unit-resolution @x269 @x1594 (unit-resolution @x664 (hypothesis x26$) $x596) (unit-resolution @x590 @x1587 $x587) x21$)))
(let ((@x1596 (unit-resolution @x622 @x1595 (unit-resolution @x222 @x1590 @x1142 @x897 x50$) false)))
(let ((@x1599 (unit-resolution (lemma @x1596 (or $x660 x44$ x17$ x42$)) @x1584 @x897 @x1142 $x660)))
(let ((@x1602 (unit-resolution @x222 (unit-resolution @x620 (unit-resolution @x325 @x1599 @x1547 x56$) $x539) @x1142 @x897 x16$)))
(let ((@x1607 (unit-resolution @x592 (unit-resolution @x202 (unit-resolution @x529 @x1602 $x516) @x1584 x48$) $x587)))
(let ((@x1608 (unit-resolution @x269 @x1607 (unit-resolution @x618 (unit-resolution @x325 @x1599 @x1547 x56$) $x595) (unit-resolution @x527 @x1602 $x525) x55$)))
(let ((@x1609 (unit-resolution @x594 (unit-resolution @x202 (unit-resolution @x529 @x1602 $x516) @x1584 x48$) $x588)))
(let ((@x1613 (lemma (unit-resolution @x666 (unit-resolution @x307 @x1609 x25$) @x1608 false) (or x42$ x44$ x17$ x27$))))
(let ((@x1615 (unit-resolution @x448 (unit-resolution @x1613 @x897 @x1021 @x1547 x42$) $x445)))
(let ((@x1616 (unit-resolution @x1514 (unit-resolution @x1613 @x897 @x1021 @x1547 x42$) @x889 x43$)))
(let (($x463 (or $x454 $x383)))
(let ((@x464 (asserted $x463)))
(let ((@x1618 (unit-resolution @x1075 (unit-resolution @x464 @x1616 $x383) @x1020 @x897 @x1615 x50$)))
(let ((@x1621 (unit-resolution @x662 (unit-resolution @x325 (unit-resolution @x620 @x1618 $x610) @x1547 x26$) $x657)))
(let ((@x1625 (unit-resolution @x664 (unit-resolution @x325 (unit-resolution @x620 @x1618 $x610) @x1547 x26$) $x596)))
(let ((@x1626 (unit-resolution @x269 @x1625 (unit-resolution @x622 @x1618 $x595) (unit-resolution @x535 @x1616 $x525) x20$)))
(let ((@x1629 (lemma (unit-resolution @x590 @x1626 (unit-resolution @x307 @x1621 x54$) false) (or x17$ x27$ $x467))))
(let ((@x1630 (unit-resolution @x1629 @x1224 (unit-resolution (lemma @x1508 (or x12$ x52$)) @x756 x12$) x17$)))
(let ((@x1632 (unit-resolution @x289 (unit-resolution @x561 @x1630 $x553) @x1217 (unit-resolution @x1569 @x1576 @x1224 $x609) x23$)))
(let ((@x1635 (unit-resolution @x584 (unit-resolution @x779 (unit-resolution @x642 @x1632 $x637) x53$) $x509)))
(let ((@x1637 (unit-resolution @x582 (unit-resolution @x779 (unit-resolution @x642 @x1632 $x637) x53$) $x566)))
(let ((@x1638 (unit-resolution @x242 @x1637 (unit-resolution @x557 @x1630 $x552) @x756 x46$)))
(let ((@x1640 (lemma (unit-resolution @x1383 @x1638 @x1635 @x756 false) x52$)))
(let (($x647 (or $x638 $x567)))
(let ((@x648 (asserted $x647)))
(let ((@x1665 (unit-resolution @x676 (unit-resolution @x797 (unit-resolution @x648 @x1640 $x638) x28$) $x667)))
(let ((@x1668 (unit-resolution (unit-resolution @x1569 @x1665 (or $x609 x11$)) @x815 $x609)))
(let ((@x1669 (unit-resolution @x678 (unit-resolution @x797 (unit-resolution @x648 @x1640 $x638) x28$) $x624)))
(let ((@x1671 (unit-resolution @x289 (unit-resolution (asserted (or $x623 $x567)) @x1640 $x623) @x1669 (or x22$ x51$))))
(let ((@x1673 (unit-resolution @x563 (unit-resolution @x1671 @x1668 x51$) $x482)))
(let ((@x1676 (unit-resolution (unit-resolution @x1629 @x1665 (or x17$ $x467)) @x897 $x467)))
(let ((@x1650 (unit-resolution @x77 (unit-resolution @x368 (hypothesis x3$) $x363) x35$)))
(let ((@x1579 (unit-resolution @x779 (unit-resolution (asserted (or $x637 $x567)) @x1640 $x637) x53$)))
(let ((@x1580 (unit-resolution @x584 @x1579 $x509)))
(let ((@x1653 (unit-resolution (unit-resolution @x193 @x1580 (or x14$ x41$)) (unit-resolution @x442 @x1650 $x438) x14$)))
(let ((@x1655 (unit-resolution @x175 (unit-resolution @x500 @x1653 $x481) @x882 @x998 x39$)))
(let ((@x1659 (unit-resolution @x128 (unit-resolution @x502 @x1653 $x425) (unit-resolution @x444 @x1650 $x424) (unit-resolution @x370 (hypothesis x3$) $x364) x8$)))
(let ((@x1662 (lemma (unit-resolution @x413 @x1659 @x1655 false) (or $x355 x12$ x45$))))
(let ((@x1574 (unit-resolution (unit-resolution @x1090 @x1580 (or $x481 x8$)) (unit-resolution @x1011 @x942 @x853 $x410) $x481)))
(let ((@x1581 (unit-resolution @x419 (unit-resolution @x175 @x1574 @x882 @x998 x39$) $x396)))
(let ((@x1582 (unit-resolution @x421 (unit-resolution @x175 @x1574 @x882 @x998 x39$) $x356)))
(let ((@x1642 (unit-resolution @x108 (unit-resolution @x350 (unit-resolution @x67 @x1582 @x942 x2$) $x348) @x1581 @x853 x6$)))
(let ((@x1644 (unit-resolution @x706 (unit-resolution @x352 (unit-resolution @x67 @x1582 @x942 x2$) $x335) x31$)))
(let ((@x1647 (lemma (unit-resolution @x389 @x1644 @x1642 false) (or x3$ x38$ x12$ x45$))))
(let ((@x1678 (unit-resolution @x1647 (unit-resolution @x1662 @x1673 @x1676 $x355) @x1676 @x1673 x38$)))
(let ((@x1681 (unit-resolution @x706 (unit-resolution @x1154 (unit-resolution @x478 @x1678 $x468) @x897 @x815 $x336) x1$)))
(let ((@x1683 (unit-resolution @x67 (unit-resolution @x352 @x1681 $x347) (unit-resolution @x1662 @x1673 @x1676 $x355) x33$)))
(let ((@x1686 (unit-resolution (unit-resolution @x1090 @x1580 (or $x481 x8$)) (unit-resolution @x417 @x1683 $x410) $x481)))
(let ((@x1687 (unit-resolution @x175 @x1686 (unit-resolution @x421 @x1683 $x411) @x1676 @x1673 false)))
(let ((@x1691 (unit-resolution @x480 (unit-resolution (lemma @x1687 (or x11$ x17$)) @x897 x11$) $x397)))
(let ((@x1692 (unit-resolution @x476 (unit-resolution (lemma @x1687 (or x11$ x17$)) @x897 x11$) $x468)))
(let ((@x1695 (unit-resolution (unit-resolution @x1613 @x1665 (or x42$ x44$ x17$)) @x1692 @x897 x42$)))
(let ((@x1700 (unit-resolution (unit-resolution @x769 @x1580 (or $x374 x45$ x12$ x38$)) (unit-resolution @x725 (unit-resolution @x452 @x1695 $x375) x5$) @x1676 @x1691 x45$)))
(let ((@x1702 (unit-resolution @x1671 (unit-resolution @x563 @x1700 $x553) x22$)))
(let ((@x1705 (unit-resolution (unit-resolution @x325 @x1665 (or x26$ x56$)) (unit-resolution @x612 @x1702 $x610) x26$)))
(let ((@x1709 (unit-resolution @x222 (unit-resolution @x616 @x1702 $x539) @x897 @x1692 x16$)))
(let ((@x1713 (unit-resolution @x269 (unit-resolution @x664 @x1705 $x596) (unit-resolution (asserted (or $x609 $x595)) @x1702 $x595) (unit-resolution @x527 @x1709 $x525) x20$)))
(let ((@x1714 (unit-resolution @x590 @x1713 (unit-resolution @x307 (unit-resolution @x662 @x1705 $x657) x54$) false)))
(let ((@x1715 (lemma @x1714 x17$)))
(let ((@x1718 (unit-resolution (unit-resolution @x1569 @x1665 (or $x609 x11$)) (unit-resolution @x1671 (unit-resolution @x561 @x1715 $x553) x22$) x11$)))
(let ((@x1722 (unit-resolution @x1662 (unit-resolution @x472 @x1718 $x467) (unit-resolution @x565 @x1715 $x482) $x355)))
(unit-resolution @x1647 @x1722 (unit-resolution @x472 @x1718 $x467) (unit-resolution @x565 @x1715 $x482) (unit-resolution @x480 @x1718 $x397) false)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

53d98ae38981e94d40d6d86fc0074ee3a2e0fb7e 38 0
unsat
((set-logic AUFLIA)
(declare-fun ?v0!0 () Int)
(declare-fun ?v1!1 () Int)
(proof
(let (($x48 (p$ ?v0!0)))
(let (($x50 (not $x48)))
(let (($x63 (not (or $x48 (p$ ?v1!1)))))
(let ((@x77 (monotonicity (rewrite (= (not $x50) $x48)) (= (and (not $x50) $x63) (and $x48 $x63)))))
(let (($x57 (not $x50)))
(let (($x67 (and $x57 $x63)))
(let (($x41 (forall ((?v0 Int) )(! (let (($x32 (forall ((?v1 Int) )(! (let (($x28 (p$ ?v1)))
(or (p$ ?v0) $x28)) :qid k!5))
))
(or (not (p$ ?v0)) $x32)) :qid k!5))
))
(let (($x44 (not $x41)))
(let (($x52 (forall ((?v1 Int) )(! (let (($x28 (p$ ?v1)))
(let (($x48 (p$ ?v0!0)))
(or $x48 $x28))) :qid k!5))
))
(let ((@x69 (nnf-neg (refl (~ $x57 $x57)) (sk (~ (not $x52) $x63)) (~ (not (or $x50 $x52)) $x67))))
(let (($x34 (forall ((?v0 Int) )(! (let (($x32 (forall ((?v1 Int) )(! (let (($x28 (p$ ?v1)))
(or (p$ ?v0) $x28)) :qid k!5))
))
(let (($x28 (p$ ?v0)))
(=> $x28 $x32))) :qid k!5))
))
(let (($x35 (not $x34)))
(let (($x32 (forall ((?v1 Int) )(! (let (($x28 (p$ ?v1)))
(or (p$ ?0) $x28)) :qid k!5))
))
(let ((@x43 (quant-intro (rewrite (= (=> (p$ ?0) $x32) (or (not (p$ ?0)) $x32))) (= $x34 $x41))))
(let ((@x72 (mp~ (mp (asserted $x35) (monotonicity @x43 (= $x35 $x44)) $x44) (trans (sk (~ $x44 (not (or $x50 $x52)))) @x69 (~ $x44 $x67)) $x67)))
(let ((@x81 (not-or-elim (and-elim (mp @x72 @x77 (and $x48 $x63)) $x63) $x50)))
(let ((@x79 (and-elim (mp @x72 @x77 (and $x48 $x63)) $x48)))
(unit-resolution @x79 @x81 false))))))))))))))))))))

e22c0f9d8d283fe65facdddeef75c43b520c8702 53 0
unsat
((set-logic AUFLIA)
(declare-fun ?v0!0 () A$)
(proof
(let (($x517 (forall ((?v0 A$) )(! (let (($x40 (p$ x$ ?v0)))
(not $x40)) :pattern ( (p$ x$ ?v0) ) :qid k!9))
))
(let (($x44 (p$ x$ c$)))
(let (($x91 (= $x44 x$)))
(let (($x510 (forall ((?v0 Bool) (?v1 A$) )(! (let (($x29 (p$ ?v0 ?v1)))
(= $x29 ?v0)) :pattern ( (p$ ?v0 ?v1) ) :qid k!8))
))
(let (($x36 (forall ((?v0 Bool) (?v1 A$) )(! (let (($x29 (p$ ?v0 ?v1)))
(= $x29 ?v0)) :qid k!8))
))
(let ((@x514 (quant-intro (refl (= (= (p$ ?1 ?0) ?1) (= (p$ ?1 ?0) ?1))) (= $x36 $x510))))
(let ((@x64 (nnf-pos (refl (~ (= (p$ ?1 ?0) ?1) (= (p$ ?1 ?0) ?1))) (~ $x36 $x36))))
(let (($x31 (forall ((?v0 Bool) (?v1 A$) )(! (let (($x29 (p$ ?v0 ?v1)))
(= $x29 ?v0)) :qid k!8))
))
(let ((@x38 (quant-intro (rewrite (= (= (p$ ?1 ?0) ?1) (= (p$ ?1 ?0) ?1))) (= $x31 $x36))))
(let ((@x515 (mp (mp~ (mp (asserted $x31) @x38 $x36) @x64 $x36) @x514 $x510)))
(let (($x170 (or (not $x510) $x91)))
(let ((@x503 ((_ quant-inst x$ c$) $x170)))
(let (($x73 (p$ x$ ?v0!0)))
(let (($x179 (= $x73 x$)))
(let (($x85 (or $x73 $x44)))
(let (($x81 (not $x44)))
(let (($x69 (forall ((?v0 A$) )(! (let (($x40 (p$ x$ ?v0)))
(not $x40)) :qid k!9))
))
(let (($x84 (or $x69 $x81)))
(let (($x42 (exists ((?v0 A$) )(! (p$ x$ ?v0) :qid k!9))
))
(let (($x54 (not $x42)))
(let (($x55 (= $x54 $x44)))
(let ((@x71 (nnf-neg (refl (~ (not (p$ x$ ?0)) (not (p$ x$ ?0)))) (~ $x54 $x69))))
(let ((@x88 (nnf-pos @x71 (nnf-neg (sk (~ $x42 $x73)) (~ (not $x54) $x73)) (refl (~ $x44 $x44)) (refl (~ $x81 $x81)) (~ $x55 (and $x85 $x84)))))
(let ((@x53 (monotonicity (rewrite (= (= $x42 $x44) (= $x42 $x44))) (= (not (= $x42 $x44)) (not (= $x42 $x44))))))
(let ((@x59 (trans @x53 (rewrite (= (not (= $x42 $x44)) $x55)) (= (not (= $x42 $x44)) $x55))))
(let ((@x89 (mp~ (mp (asserted (not (= $x42 $x44))) @x59 $x55) @x88 (and $x85 $x84))))
(let ((@x92 (and-elim @x89 $x85)))
(let ((@x484 (unit-resolution (def-axiom (or (not $x179) (not $x73) x$)) (unit-resolution @x92 (hypothesis $x81) $x73) (or (not $x179) x$))))
(let ((@x145 (unit-resolution @x484 (unit-resolution ((_ quant-inst x$ ?v0!0) (or (not $x510) $x179)) @x515 $x179) x$)))
--> --------------------

--> maximum size reached

--> --------------------

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.17Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.