============================== prooftrans ============================ Prover9 (64) version 2008-06A, June 2008. Process 23416 was started by veroff on pengy, Tue Jul 8 08:19:41 2008 The command was "prover9 -f 5.1.in". ============================== end of head =========================== op(400,infix,[^,v,"=>",*]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.03 (+ 0.01) seconds. % Length of proof is 24. % Level of proof is 5. % Maximum clause weight is 16. % Given clauses 30. 1 -P(x => y) | -P(x) | P(y) # label("MP"). [assumption]. 2 P((x => y) => ((y => z) => (x => z))) # label("(A1)"). [assumption]. 7 P((x ^ y) => x) # label("(A6)"). [assumption]. 8 P((x ^ y) => y) # label("(A7)"). [assumption]. 9 P((x => y) => ((x => z) => (x => (y ^ z)))) # label("(A8)"). [assumption]. 10 P(x => (x v y)) # label("(A9)"). [assumption]. 11 P(x => (y v x)) # label("(A10)"). [assumption]. 12 P((x => y) => ((z => y) => ((x v z) => y))) # label("(A11)"). [assumption]. 15 P(A => B). [assumption]. 17 P(C => D). [assumption]. 19 -P((A ^ C) => (B ^ D)) | -P((A v C) => (B v D)). [assumption]. 49 P((x => y) => ((x ^ z) => y)). [hyper(1,a,2,a,b,7,a)]. 54 P((x => y) => ((z ^ x) => y)). [hyper(1,a,2,a,b,8,a)]. 132 P((B => x) => (A => x)). [hyper(1,a,2,a,b,15,a)]. 146 P((D => x) => (C => x)). [hyper(1,a,2,a,b,17,a)]. 165 P(A => (B v x)). [hyper(1,a,132,a,b,10,a)]. 168 P((x => (B v y)) => ((A v x) => (B v y))). [hyper(1,a,12,a,b,165,a)]. 185 P(C => (x v D)). [hyper(1,a,146,a,b,11,a)]. 213 P((A ^ x) => B). [hyper(1,a,49,a,b,15,a)]. 230 P(((A ^ x) => y) => ((A ^ x) => (B ^ y))). [hyper(1,a,9,a,b,213,a)]. 252 P((x ^ C) => D). [hyper(1,a,54,a,b,17,a)]. 287 P((A v C) => (B v D)). [hyper(1,a,168,a,b,185,a)]. 315 P((A ^ C) => (B ^ D)). [hyper(1,a,230,a,b,252,a)]. 323 $F. [hyper(19,a,315,a,b,287,a)]. ============================== end of proof ==========================