============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 32388 was started by veroff on io, Mon Jan 21 11:14:45 2008 The command was "prover9 -f 3.3.in". ============================== end of head =========================== op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.32 (+ 0.01) seconds: "(BCK1')". % Length of proof is 95. % Level of proof is 24. % Maximum clause weight is 27. % Given clauses 106. 1 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')") # 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]. 6 x v (x ^ y) = x # label("(D5)"). [assumption]. 7 x ^ (x v y) = x # label("(D6)"). [assumption]. 11 x ^ 1 = x # label("(D10)"). [assumption]. 13 ~ x v ~ y = ~ (x ^ y) # label("(DM1)"). [assumption]. 14 ~ x ^ ~ y = ~ (x v y) # label("(DM2)"). [assumption]. 15 ~ ~ x = x # label("(DN)"). [assumption]. 18 x -> x = 1 # label("(N2)"). [assumption]. 21 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)"). [assumption]. 22 (x ^ y) -> z = x -> (y -> z) # label("(N6)"). [assumption]. 27 x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)"). [assumption]. 28 (x -> y) ^ (~ y -> ~ x) = x => y. [copy(27),flip(a)]. 29 x -> 1 = 1 # label("(3.1)"). [assumption]. 31 (x -> y) -> (x -> z) = x -> (y -> z) # label("(3.3)"). [assumption]. 32 x -> (y -> z) = y -> (x -> z) # label("(3.4)"). [assumption]. 33 x -> (x -> y) = x -> y # label("(3.5)"). [assumption]. 35 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 36 x -> ~ (x -> y) = x -> ~ y # label("(3.8)"). [assumption]. 37 ~ (x -> y) -> z = x -> (~ y -> z) # label("(3.9)"). [assumption]. 40 x => y != 1 | y => x != 1 | x = y # label("(BCK4)"). [assumption]. 41 (x ^ y) -> y = 1 # label("(3.10)"). [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]. 46 x => (x => y) = x -> y # label("(3.15)"). [assumption]. 47 (c1 => c2) => ((c3 => c1) => (c3 => c2)) != 1 # label("(BCK1')") # answer("(BCK1')"). [deny(1)]. 66 (x ^ y) v x = x. [para(6(a,1),4(a,1)),flip(a)]. 67 x v (y ^ x) = x. [para(5(a,1),6(a,1,2))]. 72 x ^ (y v x) = x. [para(4(a,1),7(a,1,2))]. 253 ~ x -> (~ y -> z) = ~ (x v y) -> z. [para(14(a,1),22(a,1,1)),flip(a)]. 310 (x -> (y -> z)) ^ (x -> (~ z -> ~ y)) = x -> (y => z). [para(28(a,1),21(a,2,2))]. 331 x -> (y -> y) = 1. [para(31(a,1),18(a,1))]. 369 (x -> (y -> z)) ^ (~ (x -> z) -> ~ y) = y => (x -> z). [para(32(a,1),28(a,1,1))]. 441 x ^ (((x => y) => y) ^ z) = x ^ z. [para(35(a,1),3(a,1,1)),flip(a)]. 574 (x ^ (y ^ z)) => z = 1. [para(3(a,1),42(a,1,1))]. 575 (x ^ y) => x = 1. [para(5(a,1),42(a,1,1))]. 602 x ^ (y => x) = x. [para(44(a,1),5(a,1)),flip(a)]. 656 x -> (x => y) = x => (x -> y). [para(46(a,1),46(a,1,2)),flip(a)]. 674 x v (y => x) = y => x. [para(44(a,1),66(a,1,1))]. 694 (x -> y) v (x -> (z ^ y)) = x -> y. [para(21(a,1),67(a,1,2))]. 714 x -> (y v x) = 1. [para(72(a,1),41(a,1,1))]. 729 x -> (y -> x) = 1. [para(331(a,1),31(a,1)),flip(a)]. 750 (x => y) => (x -> y) = 1. [para(28(a,1),575(a,1,1))]. 754 x => (y => x) = 1. [para(44(a,1),575(a,1,1))]. 773 ~ x -> ~ (y ^ x) = 1. [para(13(a,1),714(a,1,2))]. 844 (x ^ y) => (z v y) = 1. [para(72(a,1),574(a,1,1,2))]. 879 (x => (x -> y)) => (x -> y) = 1. [para(33(a,1),750(a,1,2))]. 919 ~ x -> (y -> ~ (z ^ x)) = y -> 1. [para(773(a,1),32(a,1,2)),flip(a)]. 1009 x => (x -> y) = x -> y. [hyper(40,a,754,a,b,879,a),flip(a)]. 1075 x -> (x => y) = x -> y. [para(1009(a,1),656(a,2))]. 1101 x -> ~ (x -> y) = x -> ~ (x => y). [para(1075(a,1),36(a,1,2,1))]. 1108 ~ x -> (y => x) = ~ x -> ~ y. [para(43(a,1),1075(a,1,2))]. 1151 ~ x -> (~ (y => x) -> z) = ~ (~ x -> ~ y) -> z. [para(1108(a,1),37(a,1,1,1)),flip(a)]. 1220 x ^ (y => ((x => z) => z)) = x ^ ((x => z) => z). [para(602(a,1),441(a,1,2)),flip(a)]. 1320 ~ x -> (y -> ~ (z ^ x)) = 1. [para(29(a,1),919(a,2))]. 1431 x -> ~ (x => y) = x -> ~ y. [para(1101(a,1),36(a,1))]. 1471 x -> ~ (x => ~ y) = x -> y. [para(15(a,1),1431(a,2,2))]. 1499 x -> (~ ~ (x => y) -> z) = ~ (x -> ~ y) -> z. [para(1431(a,1),37(a,1,1,1)),flip(a)]. 1565 ~ x -> ~ (y => x) = ~ x -> y. [para(43(a,1),1471(a,1,2,1))]. 1772 x ^ (y => ((x => z) => z)) = x. [para(35(a,1),1220(a,2))]. 1836 x ^ ((x => y) -> y) = x. [para(46(a,1),1772(a,1,2))]. 1882 x => (y v ((x => z) -> z)) = 1. [para(1836(a,1),844(a,1,1))]. 1921 x => ((x => (y ^ z)) -> z) = 1. [para(694(a,1),1882(a,1,2))]. 2016 x -> (~ ~ (x => y) -> z) = x -> (~ ~ y -> z). [para(37(a,1),1499(a,2))]. 2083 x -> (~ ~ (x => y) -> z) = x -> (y -> z). [para(15(a,1),2016(a,2,2,1))]. 2196 x -> ((x => y) -> z) = x -> (y -> z). [para(15(a,1),2083(a,1,2,1))]. 2481 ~ x -> (~ (y => x) -> z) = ~ x -> (~ ~ y -> z). [para(37(a,1),1151(a,2))]. 2568 ~ x -> (~ (y => x) -> z) = ~ x -> (y -> z). [para(15(a,1),2481(a,2,2,1))]. 2795 ~ (x v (y => x)) -> z = ~ x -> (y -> z). [para(2568(a,1),253(a,1)),flip(a)]. 2898 ~ (x => y) -> z = ~ y -> (x -> z). [para(674(a,1),2795(a,1,1,1))]. 3008 ~ (x => y) -> z = x -> (~ y -> z). [para(32(a,1),2898(a,2))]. 3466 (x -> (y -> z)) ^ (x -> (~ z -> ~ y)) = y => (x -> z). [para(37(a,1),369(a,1,2))]. 3724 x -> (y => z) = y => (x -> z). [para(3466(a,1),310(a,1)),flip(a)]. 3734 (x => (y -> z)) ^ (~ (x => z) -> ~ y) = y => (x => z). [para(3724(a,1),28(a,1,1))]. 3809 (x => (y ^ z)) -> (x => z) = 1. [para(1921(a,1),3724(a,2))]. 3860 1 ^ (~ (x => y) -> ~ (x => (z ^ y))) = (x => (z ^ y)) => (x => y). [para(3809(a,1),28(a,1,1))]. 4009 (x => (y -> z)) ^ (x -> (~ z -> ~ y)) = y => (x => z). [para(3008(a,1),3734(a,1,2))]. 4132 (x => (y => (z -> u))) ^ (x -> (~ (y => u) -> ~ z)) = z => (x => (y => u)). [para(3724(a,1),4009(a,1,1,2))]. 4227 1 ^ (~ x -> (y -> ~ (y => (z ^ x)))) = (y => (z ^ x)) => (y => x). [para(2898(a,1),3860(a,1,2))]. 4325 (x => (y ^ z)) => (x => z) = 1 ^ (~ z -> (x -> ~ (y ^ z))). [para(1431(a,1),4227(a,1,2,2)),flip(a)]. 4467 (x => (y ^ z)) => (x => z) = 1 ^ 1. [para(1320(a,1),4325(a,2,2))]. 4551 (x => (y ^ z)) => (x => z) = 1. [para(11(a,1),4467(a,2))]. 4681 (x => y) => (x => ((y => z) -> z)) = 1. [para(1836(a,1),4551(a,1,1,2))]. 4927 (x => (y => (z -> u))) ^ (x -> (y -> (~ u -> ~ z))) = z => (x => (y => u)). [para(3008(a,1),4132(a,1,2,2))]. 5132 1 ^ ((x => y) -> (x -> (~ z -> ~ (y => z)))) = (y => z) => ((x => y) => (x => z)). [para(4681(a,1),4927(a,1,1))]. 5230 (x => y) => ((z => x) => (z => y)) = 1 ^ ((z => x) -> (z -> (~ y -> x))). [para(1565(a,1),5132(a,1,2,2,2)),flip(a)]. 5305 (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> ((z => x) -> (~ y -> x))). [para(32(a,1),5230(a,2,2))]. 5667 (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> (x -> (~ y -> x))). [para(2196(a,1),5305(a,2,2))]. 5811 (x => y) => ((z => x) => (z => y)) = 1 ^ (z -> 1). [para(729(a,1),5667(a,2,2,2))]. 6009 1 ^ (x -> 1) = 1. [para(5811(a,1),754(a,1))]. 6163 (x => y) => ((z => x) => (z => y)) = 1. [para(6009(a,1),5811(a,2))]. 6164 $F # answer("(BCK1')"). [resolve(6163,a,47,a)]. ============================== end of proof ==========================