============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 26314 was started by veroff on titan, Sat Jan 19 14:19:06 2008 The command was "prover9 -f 4.8.in". ============================== end of head =========================== op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.09 (+ 0.00) seconds: "(N6)". % Length of proof is 43. % Level of proof is 14. % Maximum clause weight is 17. % Given clauses 70. 1 (x ^ y) -> z = x -> (y -> z) # label("(N6)") # label(non_clause) # label(goal). [goal]. 4 x v y = y v x # label("(D3)"). [assumption]. 5 x ^ y = y ^ x # label("(D4)"). [assumption]. 6 x v (x ^ y) = x # label("(D5)"). [assumption]. 15 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 16 x ^ 1 = x # label("(D10)"). [assumption]. 20 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 21 x => (x => y) = x -> y. [copy(20),flip(a)]. 33 x => x = 1 # label("(3.16)"). [assumption]. 35 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 37 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 38 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. 41 (x => y) ^ y = y # label("(3.13)"). [assumption]. 43 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. 45 x -> ((y v x) -> z) = x -> z # label("(4.9)"). [assumption]. 50 (c1 ^ c2) -> c3 != c1 -> (c2 -> c3) # label("(N6)") # answer("(N6)"). [deny(1)]. 69 (x ^ y) v x = x. [para(6(a,1),4(a,1)),flip(a)]. 114 1 ^ x = x. [para(16(a,1),5(a,1)),flip(a)]. 144 (x * y) => (x => (y => z)) = (x * y) -> z. [para(15(a,1),21(a,1,2))]. 370 x => (y => (x => z)) = y => (x -> z). [para(21(a,1),35(a,1,2)),flip(a)]. 449 x => (x ^ y) = 1 ^ (x => y). [para(33(a,1),37(a,1,1)),flip(a)]. 647 x => (y -> (x => z)) = y -> (x -> z). [para(21(a,1),43(a,1,2)),flip(a)]. 678 x -> ((x v y) -> z) = x -> z. [para(4(a,1),45(a,1,2,1))]. 787 x v (y => x) = y => x. [para(41(a,1),69(a,1,1))]. 897 x => (x ^ y) = x => y. [para(449(a,2),114(a,1))]. 983 x -> ((y => x) -> z) = x -> z. [para(787(a,1),678(a,1,2,1))]. 1138 x => (x => (y -> z)) = y -> (x -> z). [para(43(a,1),647(a,1,2))]. 1172 x -> (y -> z) = y -> (x -> z). [para(1138(a,1),21(a,1))]. 1225 (x v y) -> (y -> z) = y -> z. [para(1172(a,1),45(a,1))]. 1235 (x v y) -> (x -> z) = x -> z. [para(1172(a,1),678(a,1))]. 1247 x -> ((x ^ y) -> z) = (x ^ y) -> z. [para(6(a,1),1225(a,1,1))]. 1286 x -> ((y * (y => x)) -> z) = (y * (y => x)) -> z. [para(38(a,1),1235(a,1,1))]. 1402 x => (y => (x => (y => z))) = (x * y) -> z. [para(144(a,1),15(a,1)),flip(a)]. 1560 x => (x => (y -> z)) = (x * y) -> z. [para(370(a,1),1402(a,1,2))]. 1587 (x * y) -> z = x -> (y -> z). [para(1560(a,1),21(a,1))]. 1794 x -> (y -> ((y => x) -> z)) = (y * (y => x)) -> z. [para(1587(a,1),1286(a,1,2))]. 1878 x -> (y -> ((x => y) -> z)) = (x * (x => y)) -> z. [para(1794(a,1),1172(a,1)),flip(a)]. 1971 (x * (x => y)) -> z = x -> (y -> z). [para(983(a,1),1878(a,1,2)),flip(a)]. 2100 x -> ((x => y) -> z) = x -> (y -> z). [para(1971(a,1),1587(a,1)),flip(a)]. 2153 x -> ((x => y) -> z) = x -> ((x ^ y) -> z). [para(897(a,1),2100(a,1,2,1))]. 2337 x -> ((x ^ y) -> z) = x -> (y -> z). [para(2153(a,1),2100(a,1))]. 2403 (x ^ y) -> z = x -> (y -> z). [para(2337(a,1),1247(a,1)),flip(a)]. 2404 $F # answer("(N6)"). [resolve(2403,a,50,a)]. ============================== end of proof ==========================