============================== prooftrans ============================ Prover9 (32) version Dec-2007, Dec 2007. Process 708 was started by alexei on ALEXEI-LT, Fri Mar 29 09:45:22 2013 The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace4/bin-win32/prover9". ============================== end of head =========================== ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 25.60 (+ 0.50) seconds. % Length of proof is 69. % Level of proof is 18. % Maximum clause weight is 35. % Given clauses 848. 1 f((((a * a) * b') * b') * b',((((a * b) * a) * b') * a') * b') = f(a,b) # label(non_clause) # label(goal). [goal]. 2 e * x = x. [assumption]. 3 x * e = x. [assumption]. 4 x' * x = e. [assumption]. 5 x * x' = e. [assumption]. 6 (x * y) * z = x * (y * z). [assumption]. 7 f(x,y) = f(x',y). [assumption]. 8 f(x',y) = f(x,y). [copy(7),flip(a)]. 9 f(x,y) = f(x,y'). [assumption]. 10 f(x,y') = f(x,y). [copy(9),flip(a)]. 11 f(x,y) = f(x,y * x). [assumption]. 12 f(x,y * x) = f(x,y). [copy(11),flip(a)]. 13 f(x,y) = f(x * y,y). [assumption]. 14 f(x * y,y) = f(x,y). [copy(13),flip(a)]. 15 f(x,y) = f((z * x) * z',y). [assumption]. 16 f(x * (y * x'),z) = f(y,z). [copy(15),rewrite([6(4)]),flip(a)]. 17 f(x,y) = f((z' * x) * z,y). [assumption]. 18 f(x' * (y * x),z) = f(y,z). [copy(17),rewrite([6(4)]),flip(a)]. 19 f((((a * a) * b') * b') * b',((((a * b) * a) * b') * a') * b') != f(a,b). [deny(1)]. 20 f(a * (a * (b' * (b' * b'))),a * (b * (a * (b' * (a' * b'))))) != f(a,b). [copy(19),rewrite([6(6),6(9),6(8),6(12),6(11),6(10),6(17),6(20),6(19),6(23),6(22),6(21),6(26),6(25),6(24),6(23)])]. 22 x' * (x * y) = y. [para(4(a,1),6(a,1,1)),rewrite([2(2)]),flip(a)]. 23 x * (y * (x * y)') = e. [para(6(a,1),5(a,1))]. 24 x * (x' * y) = y. [para(5(a,1),6(a,1,1)),rewrite([2(2)]),flip(a)]. 26 f(x,y * (z * x)) = f(x,y * z). [para(6(a,1),12(a,1,2))]. 27 f(x,y * x') = f(x,y). [para(12(a,1),8(a,1)),rewrite([8(2)]),flip(a)]. 31 f(x * (y * (z * x')),u) = f(y * z,u). [para(6(a,1),16(a,1,1,2))]. 39 f(x,x * y) = f(y,x). [para(18(a,1),14(a,1)),rewrite([8(5),12(4)])]. 49 x'' = x. [para(4(a,1),22(a,1,2)),rewrite([3(4)])]. 51 f(x * y,x) = f(x,y). [para(22(a,1),12(a,1,2)),rewrite([14(2),10(4)]),flip(a)]. 58 x * (y * x)' = y'. [para(23(a,1),22(a,1,2)),rewrite([3(3)]),flip(a)]. 61 f(x * y,x * (y * z)) = f(z,x * y). [para(6(a,1),39(a,1,2))]. 62 f(x,y * (x * (y' * z))) = f(z,y * (x * y')). [para(39(a,1),16(a,1)),rewrite([6(8),6(7)]),flip(a)]. 65 f(x,y) = f(y,x). [para(51(a,1),16(a,1)),rewrite([27(3)])]. 67 f(x,y * (z * y')) = f(z,x). [para(16(a,1),51(a,2)),rewrite([6(4),6(3),65(8),16(8),62(5)])]. 79 f(x * y,z * x') = f(x * y,z * y). [para(22(a,1),26(a,1,2,2)),flip(a)]. 85 (x * y)' = y' * x'. [para(58(a,1),22(a,1,2)),flip(a)]. 93 f(x * y,z) = f(y * x,z). [para(4(a,1),31(a,1,1,2,2)),rewrite([3(2),49(4)])]. 110 f(x * (y * z),u) = f(z * (x * y),u). [para(6(a,1),93(a,1,1))]. 111 f(x' * y',z) = f(x * y,z). [para(93(a,1),8(a,2)),rewrite([85(2)])]. 113 f(a * (b' * (b' * (b' * a))),a * (b * (a * (b' * (a' * b'))))) != f(a,b). [para(93(a,1),20(a,1)),rewrite([6(12),6(11),6(10)])]. 116 f(x * y,y * (x * z)) = f(z,y * x). [para(93(a,1),39(a,1)),rewrite([6(3)])]. 118 f(x * y,z) = f(z,y * x). [para(93(a,1),65(a,1))]. 125 f(x * (y * z),u) = f(u,y * (z * x)). [para(6(a,1),118(a,2,2))]. 127 f(x,y * z) = f(x,z * y). [para(118(a,2),16(a,1)),rewrite([67(5)])]. 130 f(x,y * (x * z)) = f(x,z * y). [para(118(a,2),26(a,1)),rewrite([6(2),65(3)])]. 131 f(x * y,z * u) = f(u * z,y * x). [para(118(a,2),93(a,1))]. 143 f(b' * (b' * (b' * (a * a))),a * (b * (a * (b' * (a' * b'))))) != f(a,b). [para(93(a,1),113(a,1)),rewrite([6(12),6(11),6(10)])]. 147 f(b' * (b' * (b' * (a * a))),b * (a * (b' * (a' * (b' * a))))) != f(a,b). [para(118(a,2),143(a,1)),rewrite([6(14),6(13),6(12),6(11),65(27)])]. 150 f(x,y' * z') = f(x,y * z). [para(127(a,1),10(a,2)),rewrite([85(2)])]. 163 f(x' * y,z) = f(x * y',z). [para(49(a,1),111(a,1,1,1)),flip(a)]. 166 f(b * (a' * (a' * (b * b))),b * (a * (b' * (a' * (b' * a))))) != f(a,b). [back_rewrite(147),rewrite([163(27),85(11),85(8),85(5),49(9),6(8),49(11),6(10),6(9)])]. 185 f(b * (a' * (a' * (b * b))),a * (b' * (a' * (b' * (a * b))))) != f(a,b). [para(118(a,2),166(a,1)),rewrite([6(14),6(13),6(12),6(11),65(26)])]. 187 f(b * (a' * (a' * (b * b))),b' * (a' * (b' * (a * (b * a))))) != f(a,b). [para(118(a,2),185(a,1)),rewrite([6(14),6(13),6(12),6(11),65(26)])]. 198 f(x,y' * z) = f(x,y * z'). [para(49(a,1),150(a,1,2,1)),flip(a)]. 201 f(b * (a' * (a' * (b * b))),b * (a' * (b' * (a' * (b * a))))) != f(a,b). [back_rewrite(187),rewrite([198(26),85(24),85(21),85(18),85(16),6(20),49(23),6(22),6(21),49(25),6(24),6(23),6(22)])]. 214 f(x * y',z * x) = f(z * x,z * y). [para(24(a,1),61(a,1,2,2)),rewrite([163(7)]),flip(a)]. 273 f(x * (y' * z'),u) = f(y * (x' * z),u). [para(110(a,1),163(a,1)),rewrite([85(6)]),flip(a)]. 376 f(x * y,z * y') = f(y * x,z * x). [para(79(a,1),8(a,2)),rewrite([85(2),163(6),49(2)])]. 443 f(x * y',z * x) = f(z * y,z * x). [para(214(a,2),65(a,1))]. 454 f(b * (a' * (a' * (b * b))),b * (a' * (b * (b * (a' * (b' * a)))))) != f(a,b). [para(214(a,2),201(a,1)),rewrite([85(22),85(19),85(16),85(13),49(17),6(16),49(19),6(18),6(17),49(21),6(20),6(19),6(18),6(21),6(20),6(19),65(33),198(33),85(31),85(28),85(26),85(24),85(21),85(18),85(16),6(20),49(23),6(22),6(21),49(25),6(24),6(23),6(22),6(27),6(26),6(25),6(24),6(30),6(29),6(28),6(27),6(26),49(33),6(32),6(31),6(30),6(29),6(28),6(27),24(33),198(29),85(27),85(24),85(22),85(20),85(17),49(17),49(19),6(18),6(21),6(20),6(24),6(23),6(22),49(27),6(26),6(25),6(24),6(23)])]. 496 f(b * (a' * (a' * (b * b))),b * (b * (a' * (b' * (a * (b * a')))))) != f(a,b). [para(125(a,2),454(a,1)),rewrite([6(16),6(15),6(14),6(13),65(28)])]. 500 f(b * (a' * (a' * (b * b))),b * (a' * (b' * (a * (b * (a' * b)))))) != f(a,b). [para(118(a,2),496(a,1)),rewrite([6(16),6(15),6(14),6(13),6(12),65(28)])]. 507 f(b * (a' * (a' * (b * b))),b * (a' * (b * (a * (b' * a'))))) != f(a,b). [para(214(a,2),500(a,1)),rewrite([85(24),85(21),85(18),85(16),85(14),49(14),6(16),6(19),6(18),49(22),6(21),6(20),6(19),49(24),6(23),6(22),6(21),6(20),6(24),6(23),6(22),24(21),65(31),198(31),85(29),85(26),85(24),85(22),85(19),85(16),49(20),6(19),49(22),6(21),6(20),6(24),6(23),6(22),6(27),6(26),6(25),6(24),49(30),6(29),6(28),6(27),6(26),6(25),24(30),198(26),85(24),85(22),85(20),85(17),49(17),49(19),6(18),6(21),6(20),6(24),6(23),6(22)])]. 511 f(b * (a' * (a' * (b * b))),b * (a * (b' * (a' * (b * a'))))) != f(a,b). [para(125(a,2),507(a,1)),rewrite([6(14),6(13),6(12),65(26)])]. 635 f(a * (b' * (b' * (b' * a))),a * (b' * (a' * (b * (a' * b))))) != f(a,b). [para(131(a,1),511(a,1)),rewrite([6(14),6(13),6(12),6(11),6(25),6(24),6(23),65(26),163(26),85(10),85(7),85(5),6(9),49(12),6(11),6(10)])]. 701 f(x * y,z * y') = f(x * z,x * y). [para(376(a,2),130(a,2)),rewrite([6(3),116(5)]),flip(a)]. 1462 f(a * (b' * (a' * (b * (a' * b)))),b * (a' * (b * (a' * (b * (a' * b)))))) != f(a,b). [para(443(a,2),635(a,1)),rewrite([85(23),85(20),85(17),49(17),49(19),6(18),49(21),6(20),6(19),6(21),6(20),6(19),6(18),65(36),198(36),85(34),85(31),85(29),85(26),85(24),85(21),85(19),6(23),49(26),6(25),6(24),6(28),6(27),6(26),49(31),6(30),6(29),6(28),6(27),6(33),6(32),6(31),6(30),6(29),49(36),6(35),6(34),6(33),6(32),6(31),6(30),24(36),198(32),85(30),85(27),85(25),85(22),85(20),49(20),6(22),49(25),6(24),6(23),6(27),6(26),6(25),49(30),6(29),6(28),6(27),6(26)])]. 4116 f(x * (y' * z),y * u) = f(y * u,x * (u * z)). [para(273(a,1),701(a,2)),rewrite([6(6),198(7),85(5),49(3),49(3)]),flip(a)]. 15406 $F. [para(4116(a,1),1462(a,1)),rewrite([6(41),6(40),6(39),6(38),6(37),24(42),26(38),65(21),61(21),65(16),61(16),65(11),61(11),39(6),65(4),10(4),65(3)]),xx(a)]. ============================== end of proof ==========================