============================== prooftrans (BV) ======================= Prover9 (64) version Aug-2007, Aug 2007. Process 26266 was started by veroff on titan, Sat Jan 19 14:18:54 2008 The command was "prover9 -f 4.4_alt.in". ============================== end of head =========================== op(400,infix,[^,v,"->","=>",*]). op(200,prefix,[~,-]). ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.12 (+ 0.00) seconds: "(4.9)". % Length of proof is 23. % Level of proof is 10. % Maximum clause weight is 17. % Given clauses 86. 1 x -> ((y v x) -> z) = x -> z # label("(4.9)") # label(non_clause) # label(goal). [goal]. 5 x v y = y v x # label("(D3)"). [assumption]. 6 x ^ y = y ^ x # label("(D4)"). [assumption]. 21 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 22 x => (x => y) = x -> y. [copy(21),flip(a)]. 27 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 40 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 42 (x => y) ^ y = y # label("(3.13)"). [assumption]. 44 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. 46 c1 -> ((c2 v c1) -> c3) != c1 -> c3 # label("(4.9)") # answer("(4.9)"). [deny(1)]. 190 x => (x -> y) = x => (x => y). [para(22(a,1),27(a,1,2))]. 579 x ^ (y => x) = x. [para(42(a,1),6(a,1)),flip(a)]. 646 x => (y -> (x => z)) = y -> (x -> z). [para(22(a,1),44(a,1,2)),flip(a)]. 844 x => (x -> y) = x -> y. [para(22(a,1),190(a,2))]. 898 (x -> y) ^ (z => (x -> y)) = (x v z) => (x -> y). [para(844(a,1),40(a,1,1))]. 1330 x => (x => (y -> z)) = y -> (x -> z). [para(44(a,1),646(a,1,2))]. 1559 x -> (y -> z) = y -> (x -> z). [para(1330(a,1),22(a,1))]. 2694 (x v y) => (x -> z) = x -> z. [para(898(a,1),579(a,1))]. 2721 (x v y) -> (x -> z) = (x v y) => (x -> z). [para(2694(a,1),22(a,1,2)),flip(a)]. 2819 (x v y) -> (x -> z) = x -> z. [para(2694(a,1),2721(a,2))]. 2823 (x v y) -> (y -> z) = y -> z. [para(5(a,1),2819(a,1,1))]. 2892 x -> ((y v x) -> z) = x -> z # label("(4.9)"). [para(2823(a,1),1559(a,1)),flip(a)]. 2893 $F # answer("(4.9)"). [resolve(2892,a,46,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 2 at 0.15 (+ 0.00) seconds: "(4.10)". % Length of proof is 70. % Level of proof is 18. % Maximum clause weight is 17. % Given clauses 95. 2 x -> (~ x v y) = x -> y # label("(4.10)") # label(non_clause) # label(goal). [goal]. 5 x v y = y v x # label("(D3)"). [assumption]. 6 x ^ y = y ^ x # label("(D4)"). [assumption]. 7 x v (x ^ y) = x # label("(D5)"). [assumption]. 10 1 => x = x # label("(BCK2)"). [assumption]. 14 x * y = y * x # label("(M2)"). [assumption]. 16 (x * y) => z = x => (y => z) # label("(P)"). [assumption]. 18 x ^ ((x => y) => y) = x # label("(3.7)"). [assumption]. 21 x -> y = x => (x => y) # label("(-> def)"). [assumption]. 22 x => (x => y) = x -> y. [copy(21),flip(a)]. 23 ~ x = x => 0 # label("(~ def)"). [assumption]. 24 x => 0 = ~ x. [copy(23),flip(a)]. 27 x => (x => (x => y)) = x => (x => y) # label("(E_2)"). [assumption]. 30 ~ ~ x = x # label("(DN)"). [assumption]. 32 (x => y) => ((z => x) => (z => y)) = 1 # label("(BCK1')"). [assumption]. 36 x => (y => z) = y => (x => z) # label("(3.18)"). [assumption]. 38 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)"). [assumption]. 40 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)"). [assumption]. 41 ((x => y) * z) => (x => (y * z)) = 1 # label("(4.5)"). [assumption]. 42 (x => y) ^ y = y # label("(3.13)"). [assumption]. 43 (x v y) => y = x => y # label("(4.6)"). [assumption]. 44 x -> (y => z) = y => (x -> z) # label("(4.7)"). [assumption]. 47 c4 -> (~ c4 v c5) != c4 -> c5 # label("(4.10)") # answer("(4.10)"). [deny(2)]. 66 (x ^ y) v x = x. [para(7(a,1),5(a,1)),flip(a)]. 149 x => (y => 0) = ~ (x * y). [para(24(a,1),16(a,1)),flip(a)]. 190 x => (x -> y) = x => (x => y). [para(22(a,1),27(a,1,2))]. 379 (x => y) => (z => ((z => x) => y)) = 1. [para(36(a,1),32(a,1,2))]. 431 x => ((x => y) ^ z) = (x -> y) ^ (x => z). [para(22(a,1),38(a,1,1)),flip(a)]. 507 ~ x ^ (y => 0) = (x v y) => 0. [para(24(a,1),40(a,1,1))]. 543 (x * (y => z)) => (y => (z * x)) = 1. [para(14(a,1),41(a,1,1))]. 692 x v (y => x) = y => x. [para(42(a,1),66(a,1,1))]. 763 ~ (x * y) = x => ~ y. [para(24(a,1),149(a,1,2)),flip(a)]. 804 ~ (x => ~ y) = x * y. [para(763(a,1),30(a,1,1))]. 824 (x v ~ y) * y = ~ (x => ~ y). [para(43(a,1),804(a,1,1)),flip(a)]. 844 x => (x -> y) = x -> y. [para(22(a,1),190(a,2))]. 894 x => (y => (x -> z)) = y => (x -> z). [para(844(a,1),36(a,1,2)),flip(a)]. 921 (x v y) => 0 = ~ x ^ ~ y. [para(24(a,1),507(a,1,2)),flip(a)]. 949 ~ x ^ ~ y = ~ (x v y). [para(921(a,1),24(a,1))]. 999 ~ (~ x v y) = x ^ ~ y. [para(30(a,1),949(a,1,1)),flip(a)]. 1012 ~ (x v ~ y) = y ^ ~ x. [para(5(a,1),999(a,1,1))]. 1047 ~ (x v (y => ~ z)) = (y * z) ^ ~ x. [para(763(a,1),1012(a,1,1,2))]. 1094 (x v ~ y) * y = x * y. [para(804(a,1),824(a,2))]. 1103 x * (y v ~ x) = y * x. [para(1094(a,1),14(a,1)),flip(a)]. 1193 x => ((y => z) => ((x => y) => z)) = 1. [para(379(a,1),36(a,1)),flip(a)]. 1258 x => ((y * (x => z)) => (z * y)) = 1. [para(543(a,1),36(a,1)),flip(a)]. 1409 x => (((x => y) => z) => ((x -> y) => z)) = 1. [para(22(a,1),1193(a,1,2,2,1))]. 1493 x => (y => ((x => z) => (z * y))) = 1. [para(16(a,1),1258(a,1,2))]. 1628 x -> ((x => y) => (y * x)) = 1. [para(1493(a,1),22(a,1)),flip(a)]. 1690 x -> ((x => y) => (x * y)) = 1. [para(14(a,1),1628(a,1,2,2))]. 1748 (x => y) => (x -> (x * y)) = 1. [para(1690(a,1),44(a,1)),flip(a)]. 1860 (x * y) ^ ~ ~ y = ~ (x => ~ y). [para(692(a,1),1047(a,1,1)),flip(a)]. 1916 (x * y) ^ ~ ~ y = x * y. [para(804(a,1),1860(a,2))]. 1943 (x * y) ^ y = x * y. [para(30(a,1),1916(a,1,2))]. 1983 x => (y ^ (x => z)) = (x -> z) ^ (x => y). [para(6(a,1),431(a,1,2))]. 2146 x => ((x -> y) => (((x => y) => z) => z)) = 1. [para(36(a,1),1409(a,1,2))]. 2233 x => ((x => y) ^ (x => z)) = (x -> z) ^ (x -> y). [para(22(a,1),1983(a,2,2))]. 2435 x => ((x -> y) => (1 => (x -> (x * y)))) = 1. [para(1748(a,1),2146(a,1,2,2,1))]. 2453 x => ((x -> y) => (x -> (x * y))) = 1. [para(10(a,1),2435(a,1,2,2))]. 2547 (x -> y) => (x -> (x * y)) = 1. [para(2453(a,1),894(a,1)),flip(a)]. 2572 (x -> y) ^ (1 => (x -> (x * y))) = x -> y. [para(2547(a,1),18(a,1,2,1))]. 2622 (x -> y) ^ (x -> (x * y)) = x -> y. [para(10(a,1),2572(a,1,2))]. 3028 x => (x => (y ^ z)) = (x -> z) ^ (x -> y). [para(38(a,1),2233(a,1,2))]. 3149 (x -> y) ^ (x -> z) = x -> (z ^ y). [para(3028(a,1),22(a,1))]. 3275 x -> ((x * y) ^ y) = x -> y. [para(3149(a,1),2622(a,1))]. 3312 x -> (x * y) = x -> y. [para(1943(a,1),3275(a,1,2))]. 3360 x -> (y v ~ x) = x -> (y * x). [para(1103(a,1),3312(a,1,2)),flip(a)]. 3411 x -> (y v ~ x) = x -> (x * y). [para(14(a,1),3360(a,2,2))]. 3526 x -> (y v ~ x) = x -> y. [para(3312(a,1),3411(a,2))]. 3528 x -> (~ x v y) = x -> y # label("(4.10)"). [para(5(a,1),3526(a,1,2))]. 3529 $F # answer("(4.10)"). [resolve(3528,a,47,a)]. ============================== end of proof ==========================