============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 32375 was started by veroff on io, Mon Jan 21 11:14:43 2008 The command was "prover9 -f 3.2.in". ============================== end of head =========================== op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.05 (+ 0.01) seconds: "(3.15)". % Length of proof is 39. % Level of proof is 8. % Maximum clause weight is 15. % Given clauses 62. 1 x => (x => y) = x -> y # label("(3.15)") # 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 = x # label("(DN)"). [assumption]. 20 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)"). [assumption]. 21 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 27 x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. 28 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(27),flip(a)]. 33 x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. 40 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. 42 (x ^ y) => y = 1 # label("(3.11)"). [assumption]. 43 ~ x => ~ y = y => x # label("(3.12)"). [assumption]. 44 (x => y) ^ y = y # label("(3.13)"). [assumption]. 45 x => (x ^ y) = x => y # label("(3.14)"). [assumption]. 46 c1 => (c1 => c2) != c1 -> c2 # label("(3.15)") # answer("(3.15)"). [deny(1)]. 66 x v (y ^ x) = x. [para(5(a,1),6(a,1,2))]. 380 x -> ((x -> y) ^ z) = (x -> y) ^ (x -> z). [para(33(a,1),21(a,1,1)),flip(a)]. 574 (x ^ y) => x = 1. [para(5(a,1),42(a,1,1))]. 589 ~ x => y = ~ y => x. [para(15(a,1),43(a,1,2))]. 601 x ^ (y => x) = x. [para(44(a,1),5(a,1)),flip(a)]. 619 x => (x ^ (x -> y)) = x => (~ x v y). [para(20(a,1),45(a,1,2))]. 638 (x ^ y) v y = y. [para(66(a,1),4(a,1)),flip(a)]. 666 (x => y) => (x -> y) = 1. [para(28(a,1),574(a,1,1))]. 670 x => (y => x) = 1. [para(44(a,1),574(a,1,1))]. 682 ~ x ^ (x => y) = ~ x. [para(43(a,1),601(a,1,2))]. 722 x ^ (~ x => y) = x. [para(589(a,1),601(a,1,2))]. 745 (x => (x -> y)) => (x -> y) = 1. [para(33(a,1),666(a,1,2))]. 776 ~ x v (x => y) = x => y. [para(682(a,1),638(a,1,1))]. 805 x => (x -> y) = x -> y. [hyper(40,a,670,a,b,745,a),flip(a)]. 857 x ^ (~ x -> y) = x. [para(805(a,1),722(a,1,2))]. 908 x => (~ x v y) = x => (x -> y). [para(619(a,1),45(a,1))]. 953 x => (~ x v y) = x -> y. [para(805(a,1),908(a,2))]. 982 x -> (x => y) = x => (x => y). [para(776(a,1),953(a,1,2)),flip(a)]. 1052 x -> ((x -> y) ^ z) = x -> (y ^ z). [para(21(a,1),380(a,2))]. 1149 x -> (y ^ (~ y -> ~ x)) = x -> (x => y). [para(28(a,1),1052(a,1,2)),flip(a)]. 1249 x -> (x => y) = x -> y. [para(857(a,1),1149(a,1,2)),flip(a)]. 1312 x => (x => y) = x -> y. [para(1249(a,1),982(a,1)),flip(a)]. 1313 $F # answer("(3.15)"). [resolve(1312,a,46,a)]. ============================== end of proof ==========================