============================== prooftrans ============================ Prover9 (32) version Dec-2007, Dec 2007. Process 2448 was started by Alexei on Alexei-PC, Sun Jun 9 13:41:59 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 0.03 (+ 0.03) seconds. % Length of proof is 145. % Level of proof is 22. % Maximum clause weight is 27. % Given clauses 56. 1 a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 # label(non_clause) # label(goal). [goal]. 3 x * x = x. [assumption]. 4 (x * y) * y = x. [assumption]. 5 (x * y) * (z * y) = (x * z) * y. [assumption]. 6 a1 = a9 * a7. [assumption]. 7 a9 * a7 = a1. [copy(6),flip(a)]. 8 a3 = a1 * a2. [assumption]. 9 a1 * a2 = a3. [copy(8),flip(a)]. 10 a2 = a3 * a4. [assumption]. 11 a3 * a4 = a2. [copy(10),flip(a)]. 12 a5 = a2 * a10. [assumption]. 13 a2 * a10 = a5. [copy(12),flip(a)]. 14 a6 = a5 * a4. [assumption]. 15 a5 * a4 = a6. [copy(14),flip(a)]. 16 a7 = a6 * a1. [assumption]. 17 a6 * a1 = a7. [copy(16),flip(a)]. 18 a8 = a7 * a4. [assumption]. 19 a7 * a4 = a8. [copy(18),flip(a)]. 20 a10 = a8 * a9. [assumption]. 21 a8 * a9 = a10. [copy(20),flip(a)]. 22 a4 = a10 * a3. [assumption]. 23 a10 * a3 = a4. [copy(22),flip(a)]. 24 a9 = a4 * a8. [assumption]. 25 a4 * a8 = a9. [copy(24),flip(a)]. 26 a2 != a1 | a2 != a3 | a4 != a3 | a5 != a4 | a6 != a5 | a6 != a7 | a8 != a7 | a8 != a9 | a10 != a9. [deny(1)]. 27 a2 != a1 | a3 != a2 | a3 != a4 | a5 != a4 | a6 != a5 | a6 != a7 | a8 != a7 | a9 != a8 | a9 != a10. [copy(26),flip(b),flip(c),flip(h),flip(i)]. 29 (x * y) * x = x * (y * x). [para(3(a,1),5(a,1,1)),flip(a)]. 30 ((x * y) * z) * y = x * (z * y). [para(4(a,1),5(a,1,1)),flip(a)]. 31 (x * (y * z)) * z = (x * z) * y. [para(4(a,1),5(a,1,2)),flip(a)]. 32 ((x * y) * z) * (u * (y * z)) = ((x * z) * u) * (y * z). [para(5(a,1),5(a,1,1))]. 33 (x * (y * z)) * ((u * y) * z) = (x * (u * z)) * (y * z). [para(5(a,1),5(a,1,2))]. 34 a1 * a7 = a9. [para(7(a,1),4(a,1,1))]. 35 (a9 * x) * a7 = a1 * (x * a7). [para(7(a,1),5(a,1,1)),flip(a)]. 36 (x * a9) * a7 = (x * a7) * a1. [para(7(a,1),5(a,1,2)),flip(a)]. 37 a3 * a2 = a1. [para(9(a,1),4(a,1,1))]. 39 (x * a2) * a3 = (x * a1) * a2. [para(9(a,1),5(a,1,2))]. 40 a2 * a4 = a3. [para(11(a,1),4(a,1,1))]. 41 (a3 * x) * a4 = a2 * (x * a4). [para(11(a,1),5(a,1,1)),flip(a)]. 42 (x * a3) * a4 = (x * a4) * a2. [para(11(a,1),5(a,1,2)),flip(a)]. 46 a6 * a4 = a5. [para(15(a,1),4(a,1,1))]. 48 (x * a5) * a4 = (x * a4) * a6. [para(15(a,1),5(a,1,2)),flip(a)]. 49 a7 * a1 = a6. [para(17(a,1),4(a,1,1))]. 52 a8 * a4 = a7. [para(19(a,1),4(a,1,1))]. 55 a10 * a9 = a8. [para(21(a,1),4(a,1,1))]. 57 (x * a9) * a10 = (x * a8) * a9. [para(21(a,1),5(a,1,2))]. 58 a4 * a3 = a10. [para(23(a,1),4(a,1,1))]. 60 (x * a10) * a3 = (x * a4) * a2. [para(23(a,1),5(a,1,2)),rewrite([42(4)]),flip(a)]. 61 a9 * a8 = a4. [para(25(a,1),4(a,1,1))]. 63 (x * a8) * a9 = (x * a4) * a8. [para(25(a,1),5(a,1,2))]. 64 (x * a9) * a10 = (x * a4) * a8. [back_rewrite(57),rewrite([63(8)])]. 69 a9 * (a7 * a9) = a1 * a9. [para(7(a,1),29(a,1,1)),flip(a)]. 71 a3 * a10 = a2 * a3. [para(11(a,1),29(a,1,1)),rewrite([58(7)]),flip(a)]. 72 a10 * a4 = a4 * a2. [para(11(a,1),29(a,2,2)),rewrite([58(3)])]. 73 a2 * (a10 * a2) = a5 * a2. [para(13(a,1),29(a,1,1)),flip(a)]. 77 a10 * a8 = a7. [para(21(a,1),29(a,1,1)),rewrite([61(7),52(6)])]. 78 a9 * a10 = a4 * a9. [para(21(a,1),29(a,2,2)),rewrite([61(3)]),flip(a)]. 79 a10 * (a2 * a3) = a4 * a10. [para(23(a,1),29(a,1,1)),rewrite([71(7)]),flip(a)]. 80 a9 * a4 = a4 * a7. [para(25(a,1),29(a,1,1)),rewrite([52(7)])]. 84 (x * a7) * a9 = (x * a1) * a7. [para(34(a,1),5(a,1,2))]. 89 a3 * (a2 * a3) = a1 * a3. [para(37(a,1),29(a,1,1)),flip(a)]. 92 a2 * (a4 * a2) = a1. [para(40(a,1),29(a,1,1)),rewrite([37(3)]),flip(a)]. 104 ((x * a9) * a4) * a8 = x * a10. [para(21(a,1),30(a,2,2)),rewrite([63(6)])]. 114 (x * a7) * a1 = (x * a1) * a6. [para(49(a,1),5(a,1,2)),flip(a)]. 115 (x * a9) * a7 = (x * a1) * a6. [back_rewrite(36),rewrite([114(8)])]. 116 (x * a8) * a4 = (x * a4) * a7. [para(52(a,1),5(a,1,2)),flip(a)]. 117 (x * a9) * a8 = (x * a10) * a9. [para(55(a,1),5(a,1,2))]. 118 a10 * (a4 * a9) = a8 * a10. [para(55(a,1),29(a,1,1)),rewrite([78(7)]),flip(a)]. 121 (x * a3) * a10 = (x * a4) * a3. [para(23(a,1),31(a,1,1,2)),flip(a)]. 122 (x * a10) * a9 = (x * a4) * a7. [para(25(a,1),31(a,1,1,2)),rewrite([117(4),116(8)])]. 128 a10 * (a8 * a10) = a7 * a10. [para(77(a,1),29(a,1,1)),flip(a)]. 146 ((x * a4) * a8) * (y * a10) = ((x * a9) * y) * a10. [para(21(a,1),32(a,1,2,2)),rewrite([63(4),21(13)])]. 155 ((x * a1) * a7) * (y * a9) = ((x * a7) * y) * a9. [para(34(a,1),32(a,1,2,2)),rewrite([34(13)])]. 167 ((x * a4) * a3) * (y * a10) = ((x * a3) * y) * a10. [para(58(a,1),32(a,1,2,2)),rewrite([58(13)])]. 176 (a2 * a3) * (x * a10) = (a3 * x) * a10. [para(71(a,1),5(a,1,1))]. 177 (x * a10) * (a2 * a3) = (x * a4) * a3. [para(71(a,1),5(a,1,2)),rewrite([121(10)])]. 178 ((a2 * a3) * x) * a10 = a3 * (x * a10). [para(71(a,1),30(a,1,1,1))]. 180 (x * (a2 * a3)) * a10 = (x * a4) * a2. [para(71(a,1),31(a,1,1,2)),rewrite([60(10)])]. 191 (x * a10) * (a4 * a9) = (x * a4) * a8. [para(78(a,1),5(a,1,2)),rewrite([64(10)])]. 192 ((a4 * a9) * x) * a10 = a9 * (x * a10). [para(78(a,1),30(a,1,1,1))]. 194 (x * (a4 * a9)) * a10 = (x * a4) * a7. [para(78(a,1),31(a,1,1,2)),rewrite([122(10)])]. 217 (x * a10) * ((y * a4) * a8) = (x * (y * a9)) * a10. [para(21(a,1),33(a,1,1,2)),rewrite([63(6),21(13)])]. 241 (x * a10) * ((y * a4) * a3) = (x * (y * a3)) * a10. [para(58(a,1),33(a,1,1,2)),rewrite([58(13)])]. 288 a1 * (a4 * a2) = a2. [para(92(a,1),4(a,1,1))]. 291 (a4 * a2) * a1 = a4 * (a4 * a2). [para(92(a,1),29(a,2,2)),rewrite([4(5)]),flip(a)]. 297 ((x * a4) * a2) * a1 = x * (a4 * a2). [para(92(a,1),32(a,1,2)),rewrite([4(10)])]. 300 a1 * (a4 * (a4 * a2)) = a2 * a1. [para(288(a,1),29(a,1,1)),rewrite([291(9)]),flip(a)]. 310 (a4 * a1) * a6 = a1 * (a10 * a7). [para(78(a,1),35(a,1,1)),rewrite([115(5)])]. 311 a1 * (a4 * a7) = a4. [para(80(a,1),35(a,1,1)),rewrite([4(5)]),flip(a)]. 314 a4 * (a4 * a7) = a1. [para(311(a,1),4(a,1,1))]. 315 (a1 * x) * (a4 * a7) = a4 * (x * (a4 * a7)). [para(311(a,1),5(a,1,1)),flip(a)]. 318 a4 * ((a4 * a2) * a7) = a9. [para(311(a,1),29(a,2,2)),rewrite([114(5),310(5),315(9),5(8),72(4),29(12),19(11),25(10)])]. 326 a1 * a4 = a4 * a9. [para(314(a,1),29(a,1,1)),rewrite([29(9),19(8),25(7)])]. 336 (a4 * a9) * a1 = a1 * (a4 * a1). [para(326(a,1),29(a,1,1))]. 338 (x * (a4 * a9)) * a4 = (x * a4) * a1. [para(326(a,1),31(a,1,1,2))]. 345 a7 * (a7 * a9) = a6 * a9. [para(69(a,1),29(a,2,2)),rewrite([4(5),5(12),49(8)])]. 350 ((x * a1) * a6) * a9 = x * (a7 * a9). [para(69(a,1),32(a,1,2)),rewrite([84(4),155(8),114(4),4(10)])]. 372 (a10 * a5) * a2 = a10 * (a10 * a2). [para(73(a,1),29(a,2,2)),rewrite([4(5),5(12)]),flip(a)]. 376 ((x * a10) * a5) * a2 = x * (a10 * a2). [para(73(a,1),32(a,1,2)),rewrite([5(8),4(10)])]. 417 (x * (a2 * a3)) * (a4 * a10) = (x * a4) * a3. [para(79(a,1),5(a,1,2)),rewrite([177(14)])]. 418 a1 * a3 = a5. [para(79(a,1),29(a,2,2)),rewrite([121(5),40(3),3(3),89(5),176(10),11(6),13(6)])]. 420 ((x * a4) * a2) * (a2 * a3) = x * (a4 * a10). [para(79(a,1),30(a,2,2)),rewrite([180(6)])]. 421 (a4 * a1) * a2 = a4 * a10. [para(79(a,1),30(a,2)),rewrite([23(3),39(5)])]. 429 a3 * (a2 * a3) = a5. [back_rewrite(89),rewrite([418(8)])]. 455 a2 * a3 = a4 * a9. [para(37(a,1),41(a,1,1)),rewrite([326(3),40(7)]),flip(a)]. 461 a3 * (a4 * a9) = a5. [back_rewrite(429),rewrite([455(4)])]. 468 ((x * a4) * a2) * (a4 * a9) = x * (a4 * a10). [back_rewrite(420),rewrite([455(7)])]. 470 (x * (a4 * a9)) * (a4 * a10) = (x * a4) * a3. [back_rewrite(417),rewrite([455(3)])]. 480 (x * a4) * a7 = (x * a4) * a2. [back_rewrite(180),rewrite([455(3),194(6)])]. 482 a9 * (x * a10) = a3 * (x * a10). [back_rewrite(178),rewrite([455(3),192(6)])]. 483 (x * a4) * a8 = (x * a4) * a3. [back_rewrite(177),rewrite([455(5),191(6)])]. 485 a8 * a10 = a4 * a10. [back_rewrite(79),rewrite([455(4),118(5)])]. 497 (x * (a4 * a9)) * a10 = (x * a4) * a2. [back_rewrite(194),rewrite([480(10)])]. 503 ((a4 * a9) * x) * a10 = a3 * (x * a10). [back_rewrite(192),rewrite([482(10)])]. 506 (x * (y * a9)) * a10 = (x * (y * a3)) * a10. [back_rewrite(217),rewrite([483(6),241(7)]),flip(a)]. 507 (x * a10) * (a4 * a9) = (x * a4) * a3. [back_rewrite(191),rewrite([483(10)])]. 509 ((x * a9) * y) * a10 = ((x * a3) * y) * a10. [back_rewrite(146),rewrite([483(4),167(7)]),flip(a)]. 510 ((x * a9) * a4) * a3 = x * a10. [back_rewrite(104),rewrite([483(6)])]. 515 a10 * (a4 * a10) = a7 * a10. [back_rewrite(128),rewrite([485(4)])]. 516 a10 * (a4 * a9) = a4 * a10. [back_rewrite(118),rewrite([485(8)])]. 517 (x * a4) * a2 = x. [back_rewrite(497),rewrite([506(6),58(3),4(4)]),flip(a)]. 518 a3 * (x * a10) = a10 * (x * a10). [back_rewrite(503),rewrite([509(6),58(3),29(4)]),flip(a)]. 529 x * (a4 * a9) = x * (a4 * a10). [back_rewrite(468),rewrite([517(4)])]. 531 x * (a4 * a2) = x * a1. [back_rewrite(297),rewrite([517(4)]),flip(a)]. 537 a7 * a10 = a4 * a10. [back_rewrite(516),rewrite([529(5),515(5)])]. 538 (x * a4) * a3 = (x * a4) * a10. [back_rewrite(507),rewrite([529(6),5(6)]),flip(a)]. 544 (x * a4) * a10 = x. [back_rewrite(470),rewrite([529(4),4(8),538(4)]),flip(a)]. 547 a4 * a10 = a5. [back_rewrite(461),rewrite([529(5),518(5),515(5),537(3)])]. 550 (x * a4) * a6 = (x * a4) * a1. [back_rewrite(338),rewrite([529(4),547(3),48(4)])]. 554 a1 * (a4 * a1) = a2 * a1. [back_rewrite(300),rewrite([531(6)])]. 558 a2 = a1. [back_rewrite(288),rewrite([531(5),3(3)]),flip(a)]. 569 x * a9 = x * a10. [back_rewrite(510),rewrite([538(6),544(6)])]. 591 a5 = a4. [back_rewrite(421),rewrite([558(4),4(5),547(4)]),flip(a)]. 592 (x * a4) * a1 = x. [back_rewrite(48),rewrite([591(1),4(4),550(4)]),flip(a)]. 593 a4 * a1 = a1. [back_rewrite(336),rewrite([569(3),547(3),591(1),554(8),558(4),3(6)])]. 617 x * (a10 * a1) = x * a10. [back_rewrite(376),rewrite([591(3),558(5),592(6),558(4)]),flip(a)]. 618 a10 = a1. [back_rewrite(372),rewrite([591(2),72(3),558(2),593(3),558(2),3(3),558(4),617(6),3(4)]),flip(a)]. 629 a9 = a1. [back_rewrite(318),rewrite([558(3),593(4),34(4),569(3),618(2),593(3)]),flip(a)]. 648 a3 = a1. [back_rewrite(40),rewrite([558(1),326(3),629(2),593(3)]),flip(a)]. 649 a1 != a4 | a6 != a4 | a6 != a7 | a8 != a7 | a8 != a1. [back_rewrite(27),rewrite([558(1),648(4),558(5),648(7),591(10),591(14),629(22),629(25),618(26)]),flip(h),xx(a),xx(b),xx(d),xx(i)]. 650 a1 = a4. [back_rewrite(13),rewrite([558(1),618(2),3(3),591(2)])]. 653 x * a8 = x * a4. [back_rewrite(350),rewrite([650(1),550(4),650(3),4(4),629(1),650(1),629(4),650(4),19(5)]),flip(a)]. 654 a8 = a4. [back_rewrite(345),rewrite([629(3),650(3),19(4),653(3),19(3),629(3),650(3),46(4),591(2)])]. 681 a6 = a4. [back_rewrite(15),rewrite([591(1),3(3)]),flip(a)]. 687 a7 = a4. [back_rewrite(77),rewrite([618(1),650(1),654(2),3(3)]),flip(a)]. 688 \$F. [back_rewrite(649),rewrite([650(1),681(4),681(7),687(8),654(10),687(11),654(13),650(14)]),xx(a),xx(b),xx(c),xx(d),xx(e)]. ============================== end of proof ==========================