============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 26326 was started by veroff on titan, Sat Jan 19 14:19:09 2008 The command was "prover9 -f 4.9.in". ============================== end of head =========================== op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.17 (+ 0.00) seconds: "(N4)". % Length of proof is 76. % Level of proof is 22. % Maximum clause weight is 25. % Given clauses 97. 1 x ^ (~ x v y) = x ^ (x -> y) # label("(N4)") # label(non_clause) # label(goal). [goal]. 3 (x ^ y) ^ z = x ^ (y ^ z) # label("(D2)"). [assumption]. 4 x v y = y v x # label("(D3)"). [assumption]. 5 x ^ y = y ^ x # label("(D4)"). [assumption]. 9 1 => x = x # label("(BCK2)"). [assumption]. 15 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 17 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 20 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 21 x => (x => y) = x -> y. [copy(20),flip(a)]. 22 ~ x = x => 0 # label("(~ def)"). [assumption]. 23 x => 0 = ~ x. [copy(22),flip(a)]. 29 ~ ~ x = x # label("(DN)"). [assumption]. 30 (x -> y) ^ (~ y -> ~ x) = x => y # label("(N)"). [assumption]. 33 x => x = 1 # label("(3.16)"). [assumption]. 35 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 38 (x * (x => y)) v y = y # label("(4.3)"). [assumption]. 39 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [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]. 46 x -> (~ x v y) = x -> y # label("(4.10)"). [assumption]. 50 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. 51 c1 ^ (~ c1 v c2) != c1 ^ (c1 -> c2) # label("(N4)") # answer("(N4)"). [deny(1)]. 144 (x * x) => y = x -> y. [para(21(a,1),15(a,2))]. 145 (x * y) => (x => (y => z)) = (x * y) -> z. [para(15(a,1),21(a,1,2))]. 152 x => (y => 0) = ~ (x * y). [para(23(a,1),15(a,1)),flip(a)]. 250 ~ x => 0 = x. [para(29(a,1),23(a,2))]. 371 x => (y => (x => z)) = y => (x -> z). [para(21(a,1),35(a,1,2)),flip(a)]. 372 x => (y => 0) = y => ~ x. [para(23(a,1),35(a,1,2)),flip(a)]. 509 ~ x ^ (y => 0) = (x v y) => 0. [para(23(a,1),39(a,1,1))]. 686 x -> (x -> y) = x -> y. [para(38(a,1),45(a,1,2,1))]. 692 x -> (y v ~ x) = x -> y. [para(4(a,1),46(a,1,2))]. 768 (x -> (y -> z)) ^ (~ z -> ~ (x ^ y)) = (x ^ y) => z. [para(50(a,1),30(a,1,1))]. 857 (x -> y) ^ y = y. [para(144(a,1),41(a,1,1))]. 919 ~ (x * y) = x => ~ y. [para(23(a,1),152(a,1,2)),flip(a)]. 960 ~ (x => ~ y) = x * y. [para(919(a,1),29(a,1,1))]. 979 ~ (x => y) = x * ~ y. [para(29(a,1),960(a,1,1,2))]. 998 x * ~ (x => y) = ~ (x -> y). [para(21(a,1),979(a,1,1)),flip(a)]. 1068 ~ x => ~ y = y => x. [para(250(a,1),372(a,1,2)),flip(a)]. 1115 ~ x => (y -> ~ z) = y -> (z => x). [para(1068(a,1),43(a,1,2)),flip(a)]. 1150 (x -> y) ^ (y v ~ x) = y v ~ x. [para(692(a,1),857(a,1,1))]. 1196 x * (x * ~ y) = ~ (x -> y). [para(979(a,1),998(a,1,2))]. 1236 (x v y) => 0 = ~ x ^ ~ y. [para(23(a,1),509(a,1,2)),flip(a)]. 1265 ~ x ^ ~ y = ~ (x v y). [para(1236(a,1),23(a,1))]. 1313 ~ (~ x v y) = x ^ ~ y. [para(29(a,1),1265(a,1,1)),flip(a)]. 1319 ~ x -> (~ y -> z) = ~ (x v y) -> z. [para(1265(a,1),50(a,1,1)),flip(a)]. 1331 ~ (x ^ ~ y) = ~ x v y. [para(1313(a,1),29(a,1,1))]. 1368 ~ x v ~ y = ~ (x ^ y). [para(29(a,1),1331(a,1,1,2)),flip(a)]. 1420 x -> ~ (x ^ y) = x -> ~ y. [para(1368(a,1),46(a,1,2))]. 1610 ~ x => (y -> ~ z) = z => (y -> x). [para(43(a,1),1115(a,2))]. 1732 ~ x => (y -> ~ z) = (y ^ z) => (y -> x). [para(1420(a,1),1610(a,1,2))]. 1744 ~ (~ x v y) -> z = x -> (~ y -> z). [para(29(a,1),1319(a,1,1)),flip(a)]. 1796 ~ (x v ~ y) -> z = y -> (~ x -> z). [para(4(a,1),1744(a,1,1,1))]. 1939 x => (y => (x => (y => z))) = (x * y) -> z. [para(145(a,1),15(a,1)),flip(a)]. 2113 (x ^ y) => (x -> z) = y => (x -> z). [para(1732(a,1),1610(a,1))]. 2124 (x ^ y) => (y -> z) = x => (y -> z). [para(5(a,1),2113(a,1,1))]. 2371 x => (x => (y -> z)) = (x * y) -> z. [para(371(a,1),1939(a,1,2))]. 2399 (x * y) -> z = x -> (y -> z). [para(2371(a,1),21(a,1))]. 2498 x -> ((x * ~ y) -> z) = ~ (x -> y) -> z. [para(1196(a,1),2399(a,1,1)),flip(a)]. 2601 x -> (x -> (~ y -> z)) = ~ (x -> y) -> z. [para(2399(a,1),2498(a,1,2))]. 2637 ~ (x -> y) -> z = x -> (~ y -> z). [para(2601(a,1),686(a,1))]. 2858 (x -> (y -> z)) ^ (~ (y -> z) -> ~ (x ^ y)) = (x ^ y) => (y -> z). [para(686(a,1),768(a,1,1,2))]. 2865 (x -> (y -> z)) ^ (~ (z v ~ y) -> ~ (x ^ y)) = (x ^ y) => (z v ~ y). [para(692(a,1),768(a,1,1,2))]. 3017 (x -> (y -> z)) ^ (y -> (~ z -> ~ (x ^ y))) = (x ^ y) => (y -> z). [para(2637(a,1),2858(a,1,2))]. 3122 (x -> (y -> z)) ^ (y -> (~ z -> ~ (x ^ y))) = x => (y -> z). [para(2124(a,1),3017(a,2))]. 3348 (x -> (y -> z)) ^ (y -> (~ z -> ~ (x ^ y))) = (x ^ y) => (z v ~ y). [para(1796(a,1),2865(a,1,2))]. 3496 (x ^ y) => (z v ~ y) = x => (y -> z). [para(3348(a,1),3122(a,1))]. 3517 (x ^ y) ^ ((x => (y -> z)) => (z v ~ y)) = x ^ y. [para(3496(a,1),17(a,1,2,1))]. 3625 ((x -> y) ^ x) ^ (1 => (y v ~ x)) = (x -> y) ^ x. [para(33(a,1),3517(a,1,2,1))]. 3712 (x ^ (x -> y)) ^ (1 => (y v ~ x)) = (x -> y) ^ x. [para(5(a,1),3625(a,1,1))]. 3788 (x ^ (x -> y)) ^ (y v ~ x) = (x -> y) ^ x. [para(9(a,1),3712(a,1,2))]. 3855 x ^ ((x -> y) ^ (y v ~ x)) = (x -> y) ^ x. [para(3788(a,1),3(a,1)),flip(a)]. 3970 x ^ (y v ~ x) = (x -> y) ^ x. [para(1150(a,1),3855(a,1,2))]. 4006 x ^ (~ x v y) = (x -> y) ^ x. [para(4(a,1),3970(a,1,2))]. 4064 x ^ (~ x v y) = x ^ (x -> y). [para(5(a,1),4006(a,2))]. 4065 $F # answer("(N4)"). [resolve(4064,a,51,a)]. ============================== end of proof ==========================