============================== prooftrans ============================ Prover9 (32) version Dec-2007, Dec 2007. Process 5488 was started by alexei on ALEXEI-LT, Fri Mar 14 21:54:10 2014 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.61 (+ 0.08) seconds. % Length of proof is 307. % Level of proof is 36. % Maximum clause weight is 93. % Given clauses 285. 1 a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 & a10 = a11 & a11 = a12 & a12 = a13 & a13 = a14 & a14 = a15 & a15 = a16 & a16 = a17 & a17 = a18 & a18 = a19 & a19 = a20 & a20 = a21 & a21 = a22 & a22 = a23 & a23 = a24 & a24 = a25 & a25 = a26 & a26 = a27 & a27 = a28 & a28 = a29 & a29 = a30 & a30 = a31 & a31 = a32 # 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 * a31 = a2. [assumption]. 7 a2 * a25 = a3. [assumption]. 8 a3 * a29 = a4. [assumption]. 9 a4 * a11 = a5. [assumption]. 10 a5 * a15 = a6. [assumption]. 12 a7 * a19 = a8. [assumption]. 13 a8 * a5 = a9. [assumption]. 14 a9 * a17 = a10. [assumption]. 15 a10 * a7 = a11. [assumption]. 16 a11 * a5 = a12. [assumption]. 17 a12 * a19 = a13. [assumption]. 18 a13 * a7 = a14. [assumption]. 19 a14 * a17 = a15. [assumption]. 20 a15 * a5 = a16. [assumption]. 21 a16 * a19 = a17. [assumption]. 22 a17 * a9 = a18. [assumption]. 23 a18 * a15 = a19. [assumption]. 24 a19 * a11 = a20. [assumption]. 25 a20 * a29 = a21. [assumption]. 26 a21 * a25 = a22. [assumption]. 27 a22 * a31 = a23. [assumption]. 28 a23 * a21 = a24. [assumption]. 29 a24 * a3 = a25. [assumption]. 30 a25 * a23 = a26. [assumption]. 31 a26 * a1 = a27. [assumption]. 32 a27 * a21 = a28. [assumption]. 33 a28 * a3 = a29. [assumption]. 34 a29 * a1 = a30. [assumption]. 35 a30 * a23 = a31. [assumption]. 36 a31 * a3 = a32. [assumption]. 37 a32 * a21 = a1. [assumption]. 38 a2 != a1 | a3 != a2 | a4 != a3 | a5 != a4 | a6 != a5 | a7 != a6 | a8 != a7 | a8 != a9 | a10 != a9 | a10 != a11 | a12 != a11 | a13 != a12 | a14 != a13 | a14 != a15 | a16 != a15 | a16 != a17 | a18 != a17 | a18 != a19 | a20 != a19 | a21 != a20 | a22 != a21 | a23 != a22 | a24 != a23 | a24 != a25 | a26 != a25 | a27 != a26 | a28 != a27 | a28 != a29 | a30 != a29 | a30 != a31 | a32 != a31. [deny(1)]. 39 a2 != a1 | a2 != a3 | a4 != a3 | a4 != a5 | a6 != a5 | a6 != a7 | a8 != a7 | a8 != a9 | a10 != a9 | a10 != a11 | a12 != a11 | a13 != a12 | a14 != a13 | a14 != a15 | a16 != a15 | a16 != a17 | a18 != a17 | a18 != a19 | a20 != a19 | a20 != a21 | a22 != a21 | a22 != a23 | a24 != a23 | a24 != a25 | a26 != a25 | a27 != a26 | a28 != a27 | a28 != a29 | a30 != a29 | a30 != a31 | a32 != a31. [copy(38),flip(b),flip(d),flip(f),flip(t),flip(v)]. 41 (x * y) * x = x * (y * x). [para(3(a,1),5(a,1,1)),flip(a)]. 42 ((x * y) * z) * y = x * (z * y). [para(4(a,1),5(a,1,1)),flip(a)]. 43 (x * (y * z)) * z = (x * z) * y. [para(4(a,1),5(a,1,2)),flip(a)]. 44 ((x * y) * z) * (u * (y * z)) = ((x * z) * u) * (y * z). [para(5(a,1),5(a,1,1))]. 45 (x * (y * z)) * ((u * y) * z) = (x * (u * z)) * (y * z). [para(5(a,1),5(a,1,2))]. 46 a2 * a31 = a1. [para(6(a,1),4(a,1,1))]. 47 (a1 * x) * a31 = a2 * (x * a31). [para(6(a,1),5(a,1,1)),flip(a)]. 48 (x * a31) * a2 = (x * a1) * a31. [para(6(a,1),5(a,1,2))]. 49 a3 * a25 = a2. [para(7(a,1),4(a,1,1))]. 50 (a2 * x) * a25 = a3 * (x * a25). [para(7(a,1),5(a,1,1)),flip(a)]. 51 (x * a2) * a25 = (x * a25) * a3. [para(7(a,1),5(a,1,2)),flip(a)]. 52 a4 * a29 = a3. [para(8(a,1),4(a,1,1))]. 64 a8 * a19 = a7. [para(12(a,1),4(a,1,1))]. 65 (a7 * x) * a19 = a8 * (x * a19). [para(12(a,1),5(a,1,1)),flip(a)]. 66 (x * a7) * a19 = (x * a19) * a8. [para(12(a,1),5(a,1,2)),flip(a)]. 68 (a8 * x) * a5 = a9 * (x * a5). [para(13(a,1),5(a,1,1)),flip(a)]. 69 (x * a8) * a5 = (x * a5) * a9. [para(13(a,1),5(a,1,2)),flip(a)]. 70 a10 * a17 = a9. [para(14(a,1),4(a,1,1))]. 71 (a9 * x) * a17 = a10 * (x * a17). [para(14(a,1),5(a,1,1)),flip(a)]. 73 a11 * a7 = a10. [para(15(a,1),4(a,1,1))]. 76 a12 * a5 = a11. [para(16(a,1),4(a,1,1))]. 77 (a11 * x) * a5 = a12 * (x * a5). [para(16(a,1),5(a,1,1)),flip(a)]. 78 (x * a11) * a5 = (x * a5) * a12. [para(16(a,1),5(a,1,2)),flip(a)]. 80 a13 * a19 = a12. [para(17(a,1),4(a,1,1))]. 81 (a12 * x) * a19 = a13 * (x * a19). [para(17(a,1),5(a,1,1)),flip(a)]. 82 (x * a12) * a19 = (x * a19) * a13. [para(17(a,1),5(a,1,2)),flip(a)]. 86 a15 * a17 = a14. [para(19(a,1),4(a,1,1))]. 89 a16 * a5 = a15. [para(20(a,1),4(a,1,1))]. 90 (a15 * x) * a5 = a16 * (x * a5). [para(20(a,1),5(a,1,1)),flip(a)]. 91 (x * a15) * a5 = (x * a5) * a16. [para(20(a,1),5(a,1,2)),flip(a)]. 92 a17 * a19 = a16. [para(21(a,1),4(a,1,1))]. 93 (a16 * x) * a19 = a17 * (x * a19). [para(21(a,1),5(a,1,1)),flip(a)]. 94 (x * a16) * a19 = (x * a19) * a17. [para(21(a,1),5(a,1,2)),flip(a)]. 95 a18 * a9 = a17. [para(22(a,1),4(a,1,1))]. 98 a19 * a15 = a18. [para(23(a,1),4(a,1,1))]. 99 (a18 * x) * a15 = a19 * (x * a15). [para(23(a,1),5(a,1,1)),flip(a)]. 101 a20 * a11 = a19. [para(24(a,1),4(a,1,1))]. 104 a21 * a29 = a20. [para(25(a,1),4(a,1,1))]. 105 (a20 * x) * a29 = a21 * (x * a29). [para(25(a,1),5(a,1,1)),flip(a)]. 107 a22 * a25 = a21. [para(26(a,1),4(a,1,1))]. 108 (a21 * x) * a25 = a22 * (x * a25). [para(26(a,1),5(a,1,1)),flip(a)]. 110 a23 * a31 = a22. [para(27(a,1),4(a,1,1))]. 111 (a22 * x) * a31 = a23 * (x * a31). [para(27(a,1),5(a,1,1)),flip(a)]. 112 (x * a22) * a31 = (x * a31) * a23. [para(27(a,1),5(a,1,2)),flip(a)]. 113 a24 * a21 = a23. [para(28(a,1),4(a,1,1))]. 114 (a23 * x) * a21 = a24 * (x * a21). [para(28(a,1),5(a,1,1)),flip(a)]. 115 (x * a23) * a21 = (x * a21) * a24. [para(28(a,1),5(a,1,2)),flip(a)]. 116 a25 * a3 = a24. [para(29(a,1),4(a,1,1))]. 118 (x * a24) * a3 = (x * a3) * a25. [para(29(a,1),5(a,1,2)),flip(a)]. 119 a26 * a23 = a25. [para(30(a,1),4(a,1,1))]. 122 a27 * a1 = a26. [para(31(a,1),4(a,1,1))]. 125 a28 * a21 = a27. [para(32(a,1),4(a,1,1))]. 126 (a27 * x) * a21 = a28 * (x * a21). [para(32(a,1),5(a,1,1)),flip(a)]. 128 a29 * a3 = a28. [para(33(a,1),4(a,1,1))]. 129 (a28 * x) * a3 = a29 * (x * a3). [para(33(a,1),5(a,1,1)),flip(a)]. 132 (a29 * x) * a1 = a30 * (x * a1). [para(34(a,1),5(a,1,1)),flip(a)]. 133 (x * a29) * a1 = (x * a1) * a30. [para(34(a,1),5(a,1,2)),flip(a)]. 134 a31 * a23 = a30. [para(35(a,1),4(a,1,1))]. 135 (a30 * x) * a23 = a31 * (x * a23). [para(35(a,1),5(a,1,1)),flip(a)]. 136 (x * a30) * a23 = (x * a23) * a31. [para(35(a,1),5(a,1,2)),flip(a)]. 137 a32 * a3 = a31. [para(36(a,1),4(a,1,1))]. 138 (a31 * x) * a3 = a32 * (x * a3). [para(36(a,1),5(a,1,1)),flip(a)]. 139 (x * a31) * a3 = (x * a3) * a32. [para(36(a,1),5(a,1,2)),flip(a)]. 140 a1 * a21 = a32. [para(37(a,1),4(a,1,1))]. 142 (x * a32) * a21 = (x * a21) * a1. [para(37(a,1),5(a,1,2)),flip(a)]. 143 (x * y) * (y * (x * y)) = x * (x * y). [para(4(a,1),41(a,1,1)),flip(a)]. 144 (x * (y * x)) * (z * x) = ((x * y) * z) * x. [para(41(a,1),5(a,1,1))]. 146 (x * (y * x)) * y = x * (x * y). [para(41(a,1),5(a,1)),rewrite([143(4),41(4)]),flip(a)]. 147 a1 * (a31 * a1) = a2 * a1. [para(6(a,1),41(a,1,1)),flip(a)]. 148 a2 * (a25 * a2) = a3 * a2. [para(7(a,1),41(a,1,1)),flip(a)]. 157 a10 * a9 = a9 * a18. [para(14(a,1),41(a,1,1)),rewrite([22(7)])]. 158 a18 * a17 = a17 * a10. [para(14(a,1),41(a,2,2)),rewrite([22(3)])]. 167 a19 * (a11 * a19) = a20 * a19. [para(24(a,1),41(a,1,1)),flip(a)]. 170 a22 * (a31 * a22) = a23 * a22. [para(27(a,1),41(a,1,1)),flip(a)]. 177 a29 * (a1 * a29) = a30 * a29. [para(34(a,1),41(a,1,1)),flip(a)]. 179 a31 * (a3 * a31) = a32 * a31. [para(36(a,1),41(a,1,1)),flip(a)]. 182 (a2 * x) * a31 = a1 * (x * a31). [para(46(a,1),5(a,1,1)),flip(a)]. 183 (x * a2) * a31 = (x * a31) * a1. [para(46(a,1),5(a,1,2)),flip(a)]. 185 (a3 * x) * a25 = a2 * (x * a25). [para(49(a,1),5(a,1,1)),flip(a)]. 187 a2 * a3 = a3 * a24. [para(49(a,1),41(a,1,1)),rewrite([116(7)])]. 203 (a10 * x) * a17 = a9 * (x * a17). [para(14(a,1),42(a,1,1,1))]. 210 (a17 * x) * a19 = a16 * (x * a19). [para(21(a,1),42(a,1,1,1))]. 219 (a25 * x) * a3 = a24 * (x * a3). [para(29(a,1),42(a,1,1,1))]. 221 (a27 * x) * a1 = a26 * (x * a1). [para(31(a,1),42(a,1,1,1))]. 227 (a1 * x) * a21 = a32 * (x * a21). [para(37(a,1),42(a,1,1,1))]. 238 (x * a8) * a19 = (x * a19) * a7. [para(64(a,1),5(a,1,2)),flip(a)]. 256 (x * a22) * a25 = (x * a25) * a21. [para(26(a,1),43(a,1,1,2))]. 257 (x * a31) * a22 = (x * a23) * a31. [para(27(a,1),43(a,1,1,2)),flip(a)]. 258 (x * a24) * a21 = (x * a21) * a23. [para(28(a,1),43(a,1,1,2))]. 259 (x * a25) * a3 = (x * a3) * a24. [para(29(a,1),43(a,1,1,2))]. 260 (x * a26) * a23 = (x * a23) * a25. [para(30(a,1),43(a,1,1,2))]. 263 (x * a29) * a3 = (x * a3) * a28. [para(33(a,1),43(a,1,1,2))]. 265 (x * a31) * a23 = (x * a23) * a30. [para(35(a,1),43(a,1,1,2))]. 269 (x * a2) * a25 = (x * a3) * a24. [back_rewrite(51),rewrite([259(8)])]. 271 (x * a22) * a31 = (x * a23) * a30. [back_rewrite(112),rewrite([265(8)])]. 272 a10 * (a17 * a10) = a9 * a10. [para(70(a,1),41(a,1,1)),flip(a)]. 361 (x * a3) * ((y * a3) * a24) = (x * (y * a25)) * a3. [para(7(a,1),45(a,1,1,2)),rewrite([269(6),7(13)])]. 442 a18 * (a9 * a18) = a17 * a18. [para(95(a,1),41(a,1,1)),flip(a)]. 447 a19 * (a15 * a19) = a18 * a19. [para(98(a,1),41(a,1,1)),flip(a)]. 462 (a1 * a23) * a30 = a2 * a23. [para(27(a,1),47(a,2,2)),rewrite([271(5)])]. 469 a22 * (a25 * a22) = a21 * a22. [para(107(a,1),41(a,1,1)),flip(a)]. 472 a22 * a23 = a23 * a30. [para(110(a,1),41(a,1,1)),rewrite([134(7)])]. 473 a30 * a31 = a31 * a22. [para(110(a,1),41(a,2,2)),rewrite([134(3)])]. 476 ((x * a23) * a31) * (y * a22) = ((x * a31) * y) * a22. [para(110(a,1),44(a,1,2,2)),rewrite([110(13)])]. 497 (x * (a26 * y)) * (a23 * y) = (x * (a23 * y)) * (a25 * y). [para(119(a,1),45(a,1,2,1)),flip(a)]. 526 a1 * (a21 * a1) = a32 * a1. [para(140(a,1),41(a,1,1)),flip(a)]. 529 a2 * (a21 * a31) = a32 * a31. [para(140(a,1),47(a,1,1)),flip(a)]. 588 (a9 * a18) * a10 = a10 * (a9 * a10). [para(157(a,1),41(a,1,1))]. 652 (a23 * a30) * a22 = a22 * (a23 * a22). [para(472(a,1),41(a,1,1))]. 663 (x * (a31 * a22)) * a31 = (x * a31) * a30. [para(473(a,1),43(a,1,1,2))]. 678 (a31 * a2) * a1 = a31 * (a31 * a1). [para(147(a,1),41(a,2,2)),rewrite([4(5),5(12)]),flip(a)]. 681 (x * (y * (a31 * a1))) * (a2 * a1) = (x * (a2 * a1)) * ((y * a31) * a1). [para(147(a,1),45(a,1,1,2)),rewrite([5(10),147(19)]),flip(a)]. 843 a31 * (a31 * a22) = a30 * a22. [para(170(a,1),41(a,2,2)),rewrite([4(5),5(12),134(8)])]. 844 ((x * a23) * a30) * (a31 * a22) = x * (a23 * a22). [para(170(a,1),42(a,2,2)),rewrite([43(6),271(4)])]. 845 (x * (a23 * a22)) * (a31 * a22) = (x * a23) * a30. [para(170(a,1),43(a,1,1,2)),rewrite([43(14),271(12)])]. 898 (a10 * a19) * a8 = a11 * a19. [para(15(a,1),66(a,1,1)),flip(a)]. 899 a14 * a19 = a12 * a8. [para(18(a,1),66(a,1,1)),rewrite([80(6)])]. 938 (a1 * a30) * a29 = a1 * (a1 * a29). [para(177(a,1),41(a,2,2)),rewrite([4(5),5(12)]),flip(a)]. 942 ((x * a1) * a30) * a29 = x * (a1 * a29). [para(177(a,1),44(a,1,2)),rewrite([5(8),4(10)])]. 949 a9 * (a19 * a5) = a7 * a5. [para(64(a,1),68(a,1,1)),flip(a)]. 965 (a3 * a32) * a31 = a3 * (a3 * a31). [para(179(a,1),41(a,2,2)),rewrite([4(5),5(12)]),flip(a)]. 969 ((x * a3) * a32) * a31 = x * (a3 * a31). [para(179(a,1),44(a,1,2)),rewrite([5(8),4(10)])]. 1149 a9 * (a9 * a18) = a10 * a18. [para(442(a,1),41(a,2,2)),rewrite([4(5),5(12),14(8)])]. 1194 (x * (a2 * a23)) * a30 = (x * a30) * (a1 * a23). [para(462(a,1),43(a,1,1,2))]. 1203 (x * (a21 * a22)) * (a25 * a22) = (x * a25) * a21. [para(469(a,1),43(a,1,1,2)),rewrite([43(14),256(12)])]. 1222 a12 * (a7 * a5) = a10 * a5. [para(73(a,1),77(a,1,1)),flip(a)]. 1265 (a19 * a5) * a12 = a20 * a5. [para(24(a,1),78(a,1,1)),flip(a)]. 1307 (a21 * a32) * a1 = a21 * (a21 * a1). [para(526(a,1),41(a,2,2)),rewrite([4(5),5(12)]),flip(a)]. 1311 ((x * a21) * a32) * a1 = x * (a21 * a1). [para(526(a,1),44(a,1,2)),rewrite([5(8),4(10)])]. 1333 a3 * (a22 * (a31 * a25)) = (a32 * a31) * a25. [para(529(a,1),50(a,1,1)),rewrite([108(11)]),flip(a)]. 1360 a13 * (a5 * a19) = a11 * a19. [para(76(a,1),81(a,1,1)),flip(a)]. 1421 (a31 * a30) * a22 = a30 * (a31 * a22). [para(843(a,1),41(a,2,2)),rewrite([41(5),27(4),134(3),5(12)]),flip(a)]. 1424 (x * (a30 * a22)) * (a31 * a22) = (x * a31) * a30. [para(843(a,1),43(a,1,1,2)),rewrite([663(14)])]. 1427 ((x * a31) * a30) * a22 = x * (a23 * a22). [para(843(a,1),44(a,1,2)),rewrite([257(4),476(8),271(10),844(14)])]. 1458 ((a10 * a19) * a5) * a9 = a12 * (a19 * a5). [para(898(a,1),69(a,1,1)),rewrite([77(5)]),flip(a)]. 1632 a10 * (a9 * a10) = a9 * (a17 * a10). [para(1149(a,1),71(a,1,1)),rewrite([203(5),158(4),71(11),158(10),272(11)]),flip(a)]. 1633 (a9 * a18) * a10 = a9 * (a17 * a10). [back_rewrite(588),rewrite([1632(10)])]. 1644 a13 * (a8 * (a5 * a19)) = (a10 * a5) * a19. [para(1222(a,1),81(a,1,1)),rewrite([65(11)]),flip(a)]. 1653 (a19 * (a5 * a19)) * a13 = (a20 * a5) * a19. [para(1265(a,1),82(a,1,1)),rewrite([41(10)]),flip(a)]. 1660 a16 * (a17 * a5) = a14 * a5. [para(86(a,1),90(a,1,1)),flip(a)]. 1692 (a18 * a5) * a16 = a19 * a5. [para(23(a,1),91(a,1,1)),flip(a)]. 1730 a17 * (a16 * (a5 * a19)) = (a14 * a5) * a19. [para(1660(a,1),93(a,1,1)),rewrite([210(11)]),flip(a)]. 1740 ((a18 * a5) * a19) * a17 = a19 * (a5 * a19). [para(1692(a,1),94(a,1,1)),rewrite([41(5)]),flip(a)]. 1788 (a17 * a10) * a15 = a19 * (a17 * a15). [para(158(a,1),99(a,1,1))]. 1862 a21 * (a11 * a29) = a19 * a29. [para(101(a,1),105(a,1,1)),flip(a)]. 1903 (a21 * a3) * a24 = a22 * a3. [para(7(a,1),108(a,2,2)),rewrite([269(5)])]. 1912 a22 * ((a11 * a29) * a25) = (a19 * a29) * a25. [para(1862(a,1),108(a,1,1)),flip(a)]. 1963 a23 * (a25 * a31) = a21 * a31. [para(107(a,1),111(a,1,1)),flip(a)]. 1969 (a26 * a30) * (a25 * a31) = (a25 * a21) * a31. [para(1963(a,1),41(a,2,2)),rewrite([265(5),30(3),5(14)])]. 1997 (a25 * a21) * a24 = a26 * a21. [para(30(a,1),115(a,1,1)),flip(a)]. 2060 (a24 * (a21 * a3)) * a25 = (a26 * a21) * a3. [para(1997(a,1),118(a,1,1)),rewrite([219(10)]),flip(a)]. 2165 a28 * a32 = a26 * a21. [para(122(a,1),126(a,1,1)),rewrite([140(7)]),flip(a)]. 2199 a29 * (a21 * a3) = a27 * a3. [para(125(a,1),129(a,1,1)),flip(a)]. 2200 (a26 * a21) * a3 = a29 * a31. [para(137(a,1),129(a,2,2)),rewrite([2165(3)])]. 2203 (a24 * (a21 * a3)) * a25 = a29 * a31. [back_rewrite(2060),rewrite([2200(12)])]. 2238 a30 * (a3 * a1) = a28 * a1. [para(128(a,1),132(a,1,1)),flip(a)]. 2240 a30 * ((a21 * a3) * a1) = a26 * (a3 * a1). [para(2199(a,1),132(a,1,1)),rewrite([221(5)]),flip(a)]. 2242 (x * (a3 * a1)) * (a28 * a1) = (x * a30) * (a3 * a1). [para(2238(a,1),5(a,1,2))]. 2250 (x * a1) * ((y * a1) * a30) = (x * (y * a29)) * a1. [para(133(a,1),5(a,1,2))]. 2293 (a31 * (x * a23)) * x = a30 * (a23 * x). [para(135(a,1),42(a,1,1))]. 2318 ((x * a30) * a21) * a24 = ((x * a23) * a31) * a21. [para(136(a,1),115(a,1,1)),flip(a)]. 2331 a32 * (a23 * a3) = a30 * a3. [para(134(a,1),138(a,1,1)),flip(a)]. 2347 (a3 * a24) * a32 = a1 * a3. [para(46(a,1),139(a,1,1)),rewrite([187(6)]),flip(a)]. 2355 (a23 * a3) * a32 = a22 * a3. [para(110(a,1),139(a,1,1)),flip(a)]. 2378 (x * (a24 * a32)) * (a1 * a3) = (x * (a3 * a32)) * (a24 * a32). [para(2347(a,1),45(a,1,2))]. 2403 (x * a21) * ((y * a21) * a1) = (x * (y * a32)) * a21. [para(142(a,1),5(a,1,2))]. 2405 (((x * a32) * y) * a21) * a1 = (x * (y * a32)) * a21. [para(42(a,1),142(a,1,1)),flip(a)]. 2406 ((x * (y * a32)) * a21) * a1 = ((x * a32) * y) * a21. [para(43(a,1),142(a,1,1)),flip(a)]. 2413 ((a3 * a21) * a23) * a1 = a32 * (a3 * a21). [para(2347(a,1),142(a,1,1)),rewrite([227(5),258(10)]),flip(a)]. 2414 (a24 * (a3 * a21)) * a1 = (a22 * a3) * a21. [para(2355(a,1),142(a,1,1)),rewrite([114(10)]),flip(a)]. 2417 a1 * (a25 * a31) = a3 * a31. [para(7(a,1),182(a,1,1)),flip(a)]. 2426 a1 * ((a25 * a31) * a1) = (a3 * a31) * a1. [para(148(a,1),182(a,1,1)),rewrite([183(5),183(11)]),flip(a)]. 2430 (x * (a3 * a31)) * (a25 * a31) = (x * (a25 * a31)) * a1. [para(2417(a,1),43(a,1,1,2))]. 2459 (a24 * (x * a3)) * a25 = (a25 * (x * a25)) * a2. [para(49(a,1),144(a,1,2)),rewrite([219(10)]),flip(a)]. 2692 (a21 * (a3 * a21)) * a23 = (a22 * a3) * a21. [para(1903(a,1),144(a,2,1)),rewrite([113(8)])]. 2790 (a25 * a22) * a2 = a29 * a31. [back_rewrite(2203),rewrite([2459(7),26(4)])]. 2791 a31 * a22 = a25 * a22. [para(2790(a,1),4(a,1,1)),rewrite([48(5),34(3),473(3)])]. 2807 (x * (a30 * a22)) * (a25 * a22) = (x * a31) * a30. [back_rewrite(1424),rewrite([2791(7)])]. 2810 (a31 * a30) * a22 = a30 * (a25 * a22). [back_rewrite(1421),rewrite([2791(9)])]. 2821 (x * (a23 * a22)) * (a25 * a22) = (x * a23) * a30. [back_rewrite(845),rewrite([2791(7)])]. 2835 a23 * a22 = a21 * a22. [back_rewrite(170),rewrite([2791(4),469(5)]),flip(a)]. 2841 (x * a25) * a21 = (x * a23) * a30. [back_rewrite(2821),rewrite([2835(3),1203(8)])]. 2848 ((x * a31) * a30) * a22 = x * (a21 * a22). [back_rewrite(1427),rewrite([2835(9)])]. 2850 (a23 * a30) * a22 = a22 * (a21 * a22). [back_rewrite(652),rewrite([2835(9)])]. 2860 a31 = a25. [para(2791(a,1),4(a,1,1)),rewrite([4(5)]),flip(a)]. 2864 ((x * a25) * a30) * a22 = x * (a21 * a22). [back_rewrite(2848),rewrite([2860(1)])]. 2887 (a25 * a30) * a22 = a30 * (a25 * a22). [back_rewrite(2810),rewrite([2860(1)])]. 2890 (x * (a30 * a22)) * (a25 * a22) = (x * a25) * a30. [back_rewrite(2807),rewrite([2860(9)])]. 2946 (x * a25) * a1 = (x * a3) * a24. [back_rewrite(2430),rewrite([2860(2),49(3),2860(4),3(5),269(4),2860(6),3(7)]),flip(a)]. 2950 a1 * (a25 * a1) = a2 * a1. [back_rewrite(2426),rewrite([2860(3),3(4),2860(7),49(8)])]. 2959 a1 * a25 = a2. [back_rewrite(2417),rewrite([2860(3),3(4),2860(5),49(6)])]. 2994 ((x * a30) * a21) * a24 = x * a30. [back_rewrite(2318),rewrite([2860(9),2841(12),4(10)])]. 3017 (a25 * (x * a23)) * x = a30 * (a23 * x). [back_rewrite(2293),rewrite([2860(1)])]. 3055 (a26 * a30) * a25 = a25 * a22. [back_rewrite(1969),rewrite([2860(5),3(6),2860(9),41(10),26(9)])]. 3070 a3 * a21 = a32. [back_rewrite(1333),rewrite([2860(3),3(5),107(4),2860(5),4(8)])]. 3091 ((x * a3) * a32) * a25 = x * a2. [back_rewrite(969),rewrite([2860(5),2860(8),49(9)])]. 3095 a2 * (a32 * a25) = a3 * a2. [back_rewrite(965),rewrite([2860(4),185(5),2860(8),49(9)])]. 3106 (x * (y * (a25 * a1))) * (a2 * a1) = (x * (a2 * a1)) * ((y * a3) * a24). [back_rewrite(681),rewrite([2860(1),2860(14),2946(17)])]. 3109 (a25 * a2) * a1 = a25 * (a25 * a1). [back_rewrite(678),rewrite([2860(1),2860(6),2860(7)])]. 3149 a32 * a3 = a25. [back_rewrite(137),rewrite([2860(4)])]. 3152 a30 = a26. [back_rewrite(134),rewrite([2860(1),30(3)]),flip(a)]. 3154 a1 = a3. [back_rewrite(46),rewrite([2860(2),7(3)]),flip(a)]. 3155 a2 != a3 | a4 != a3 | a4 != a5 | a6 != a5 | a6 != a7 | a8 != a7 | a8 != a9 | a10 != a9 | a10 != a11 | a12 != a11 | a13 != a12 | a14 != a13 | a14 != a15 | a16 != a15 | a16 != a17 | a18 != a17 | a18 != a19 | a20 != a19 | a20 != a21 | a22 != a21 | a22 != a23 | a24 != a23 | a24 != a25 | a26 != a25 | a27 != a26 | a28 != a27 | a28 != a29 | a26 != a29 | a32 != a25. [back_rewrite(39),rewrite([3154(2),3152(85),3152(88),2860(89),2860(92)]),merge(b),merge(D)]. 3156 a32 = a24. [back_rewrite(36),rewrite([2860(1),116(3)]),flip(a)]. 3157 a23 = a21. [back_rewrite(27),rewrite([2860(2),107(3)]),flip(a)]. 3165 (x * (a26 * y)) * (a21 * y) = (x * (a21 * y)) * (a25 * y). [back_rewrite(497),rewrite([3157(4),3157(7)])]. 3222 (x * a26) * a21 = (x * a21) * a25. [back_rewrite(260),rewrite([3157(3),3157(5)])]. 3246 (a22 * a3) * a21 = a21. [back_rewrite(2692),rewrite([3070(4),3156(2),3157(4),41(5),113(4),3157(2),3(3)]),flip(a)]. 3248 a25 = a21. [back_rewrite(2414),rewrite([3070(4),3156(2),3(3),3154(2),29(3),3246(6)])]. 3249 a21 * a3 = a24. [back_rewrite(2413),rewrite([3070(3),3156(1),3157(2),113(3),3157(1),3154(2),3156(4),3070(7),3156(5),3(6)])]. 3253 a2 * a21 = a3 * a2. [back_rewrite(3095),rewrite([3156(2),3248(3),113(4),3157(2)])]. 3294 x * a2 = x * a3. [back_rewrite(3091),rewrite([3156(3),3248(5),258(6),3157(5),4(6)]),flip(a)]. 3322 a26 * a3 = a24. [back_rewrite(2331),rewrite([3156(1),3157(2),3249(4),3(3),3152(2)]),flip(a)]. 3333 a26 * a21 = a21 * a22. [back_rewrite(3055),rewrite([3152(2),3(3),3248(2),3248(4)])]. 3339 a26 * (a21 * x) = a21 * (a21 * x). [back_rewrite(3017),rewrite([3248(1),3157(2),146(5),3152(5),3157(6)]),flip(a)]. 3343 x * a26 = x * a24. [back_rewrite(2994),rewrite([3152(1),3222(4),3248(3),4(4),3152(3)]),flip(a)]. 3355 (x * a21) * a24 = x. [back_rewrite(2890),rewrite([3152(1),3248(5),3165(8),3248(5),4(8),3248(1),3152(3),3343(4)]),flip(a)]. 3358 (a21 * a24) * a22 = a21 * (a21 * a22). [back_rewrite(2887),rewrite([3248(1),3152(2),3343(3),3152(6),3248(7),3339(10)])]. 3371 x * (a21 * a22) = x * a22. [back_rewrite(2864),rewrite([3248(1),3152(3),3343(4),3355(4)]),flip(a)]. 3372 a21 * a22 = a22. [back_rewrite(2850),rewrite([3157(1),3152(2),3343(3),3358(5),3371(5),3371(8),3(6)])]. 3428 (x * (y * a29)) * a3 = (x * (y * a21)) * a3. [back_rewrite(2250),rewrite([3154(1),3154(3),3152(5),3343(6),361(7),3248(1),3154(9)]),flip(a)]. 3434 (x * a3) * a29 = (x * a3) * a21. [back_rewrite(2242),rewrite([3154(2),3(3),3154(4),33(5),3152(5),3343(6),3154(8),3(9),118(8),3248(7)])]. 3436 a24 = a22. [back_rewrite(2240),rewrite([3152(1),3249(4),3154(3),29(4),3248(2),3333(3),3372(3),3154(4),3(5),3322(4)]),flip(a)]. 3438 a22 = a29. [back_rewrite(2238),rewrite([3152(1),3154(3),3(4),3322(3),3436(1),3154(3),33(4)])]. 3473 (x * a3) * a21 = x. [back_rewrite(1194),rewrite([3157(2),3253(3),3294(3),3(3),3152(3),3343(4),3436(3),3438(3),3434(4),3152(5),3343(6),3436(5),3438(5),3154(7),3157(8),3070(9),3156(7),3436(7),3438(7),4(8)])]. 3479 x * a4 = x * a29. [back_rewrite(942),rewrite([3154(1),3152(3),3343(4),3436(3),3438(3),3434(4),3473(4),3154(3),8(5)]),flip(a)]. 3483 a4 = a3. [back_rewrite(938),rewrite([3154(1),3152(2),3343(3),3436(2),3438(2),8(3),52(3),3154(2),3154(3),8(5),3479(4),8(4)]),flip(a)]. 3497 a28 = a26. [back_rewrite(34),rewrite([3154(2),128(3),3152(2)])]. 3516 a26 = a20. [back_rewrite(3109),rewrite([3248(1),3294(3),3249(3),3436(1),3438(1),3154(2),128(3),3497(1),3248(2),3248(3),3154(4),3249(5),3436(3),3438(3),104(4)])]. 3518 (x * (y * a21)) * a3 = (x * a3) * y. [back_rewrite(3106),rewrite([3248(1),3154(2),3249(3),3436(1),3438(1),3154(5),187(6),3436(5),3438(5),8(6),3483(4),3428(5),3154(7),187(8),3436(7),3438(7),8(8),3483(6),3436(10),3438(10),3434(11),3473(11)])]. 3519 a2 = a29. [back_rewrite(2959),rewrite([3154(1),3248(2),3070(3),3156(1),3436(1),3438(1)]),flip(a)]. 3520 a20 = a3. [back_rewrite(2950),rewrite([3154(1),3248(2),3154(3),3249(4),3436(2),3438(2),8(3),3483(1),3519(2),3154(3),128(4),3497(2),3516(2)]),flip(a)]. 3522 (x * a21) * a3 = x. [back_rewrite(2946),rewrite([3248(1),3154(3),3436(7),3438(7),3434(8),3473(8)])]. 3539 ((x * a29) * y) * a21 = x * (y * a29). [back_rewrite(2406),rewrite([3156(1),3436(1),3438(1),3154(6),3522(7),3156(4),3436(4),3438(4)]),flip(a)]. 3540 (x * (y * a29)) * a21 = (x * a3) * y. [back_rewrite(2405),rewrite([3156(1),3436(1),3438(1),3539(5),3154(4),3428(5),3518(5),3156(4),3436(4),3438(4)]),flip(a)]. 3542 (x * a3) * y = (x * a21) * y. [back_rewrite(2403),rewrite([3154(5),3522(6),3156(4),3436(4),3438(4),3540(8)]),flip(a)]. 3547 (x * a21) * a29 = x. [back_rewrite(2378),rewrite([3436(1),3438(1),3156(2),3436(2),3438(2),3(3),3154(3),3(5),263(4),3497(3),3516(3),3520(3),4(4),3156(2),3436(2),3438(2),8(3),3483(1),3436(3),3438(3),3156(4),3436(4),3438(4),3(5),3542(4)]),flip(a)]. 3575 x * a29 = x * a3. [back_rewrite(1311),rewrite([3156(3),3436(3),3438(3),3547(4),3154(1),3154(4),3249(5),3436(3),3438(3)]),flip(a)]. 3576 a29 = a3. [back_rewrite(1307),rewrite([3156(2),3436(2),3438(2),3575(3),3249(3),3436(1),3438(1),3154(2),128(3),3497(1),3516(1),3520(1),3154(4),3249(5),3436(3),3438(3),3575(4),3249(4),3436(2),3438(2)]),flip(a)]. 3586 a27 = a3. [back_rewrite(31),rewrite([3516(1),3520(1),3154(2),3(3)]),flip(a)]. 3587 a5 != a3 | a6 != a5 | a6 != a7 | a8 != a7 | a8 != a9 | a10 != a9 | a10 != a11 | a12 != a11 | a13 != a12 | a14 != a13 | a14 != a15 | a16 != a15 | a16 != a17 | a18 != a17 | a18 != a19 | a3 != a19 | a3 != a21. [back_rewrite(3155),rewrite([3519(1),3576(1),3483(4),3483(7),3520(52),3520(55),3438(58),3576(58),3438(61),3576(61),3157(62),3436(64),3438(64),3576(64),3157(65),3436(67),3438(67),3576(67),3248(68),3516(70),3520(70),3248(71),3586(73),3516(74),3520(74),3497(76),3516(76),3520(76),3586(77),3497(79),3516(79),3520(79),3576(80),3516(82),3520(82),3576(83),3156(85),3436(85),3438(85),3576(85),3248(86)]),flip(c),xx(a),xx(b),xx(y),xx(z),xx(A),xx(B),merge(r),merge(s),merge(t),merge(u),merge(v),merge(w)]. 3588 a3 = a21. [back_rewrite(3149),rewrite([3156(1),3436(1),3438(1),3576(1),3(3),3248(2)])]. 3590 a21 * a11 = a19. [back_rewrite(1912),rewrite([3438(1),3576(1),3588(1),3576(3),3588(3),3248(5),4(6),3576(5),3588(5),3248(7),4(8)])]. 3715 a5 = a19. [back_rewrite(9),rewrite([3483(1),3588(1),3590(3)]),flip(a)]. 3762 a19 * a13 = a21. [back_rewrite(1653),rewrite([3715(2),3(4),3(3),3520(4),3588(4),3715(5),4(8)])]. 3772 a21 * a19 = a19 * a12. [back_rewrite(1265),rewrite([3715(2),3(3),3520(4),3588(4),3715(5)]),flip(a)]. 3794 a19 * (a11 * a19) = a19 * a12. [back_rewrite(167),rewrite([3520(6),3588(6),3772(8)])]. 3800 a21 != a19 | a6 != a19 | a6 != a7 | a8 != a7 | a8 != a9 | a10 != a9 | a10 != a11 | a12 != a11 | a13 != a12 | a14 != a13 | a14 != a15 | a16 != a15 | a16 != a17 | a18 != a17 | a18 != a19. [back_rewrite(3587),rewrite([3715(1),3588(2),3715(5),3588(46),3588(49)]),flip(a),xx(q),merge(p)]. 3816 a17 * a10 = a19. [back_rewrite(1740),rewrite([3715(2),4(5),158(3),3715(5),3(7),3(6)])]. 3817 a14 = a17. [back_rewrite(1730),rewrite([3715(3),3(5),21(4),3(3),3715(3),899(4),238(6),17(4),18(4)]),flip(a)]. 3826 a10 = a17. [back_rewrite(1644),rewrite([3715(3),3(5),64(4),18(3),3817(1),3715(3),4(6)]),flip(a)]. 3828 a11 * a19 = a12. [back_rewrite(1360),rewrite([3715(2),3(4),80(3)]),flip(a)]. 4011 a18 = a13. [back_rewrite(1458),rewrite([3826(1),92(3),3715(2),21(3),22(3),3715(4),3(5),17(4)])]. 4025 a12 * a8 = a16. [back_rewrite(1222),rewrite([3715(3),12(4),3826(4),3715(5),92(6)])]. 4072 a9 * a19 = a8. [back_rewrite(949),rewrite([3715(3),3(4),3715(5),12(6)])]. 4140 a17 = a15. [back_rewrite(89),rewrite([3715(2),21(3)])]. 4141 a13 = a11. [back_rewrite(76),rewrite([3715(2),17(3)])]. 4147 a9 = a7. [back_rewrite(13),rewrite([3715(2),64(3)]),flip(a)]. 4148 a6 = a11. [back_rewrite(10),rewrite([3715(1),98(3),4011(1),4141(1)]),flip(a)]. 4187 a15 = a11. [back_rewrite(1788),rewrite([4140(1),3826(2),4140(2),3(3),3(3),4140(3),3(5),98(4),4011(2),4141(2)])]. 4188 a7 * a11 = a7. [back_rewrite(1633),rewrite([4147(1),4011(2),4141(2),3826(4),4140(4),4187(4),4(5),4147(2),4140(3),4187(3),3826(4),4140(4),4187(4),3(5)]),flip(a)]. 4189 a7 = a11. [back_rewrite(1632),rewrite([3826(1),4140(1),4187(1),4147(2),3826(3),4140(3),4187(3),4188(4),73(3),3826(1),4140(1),4187(1),4147(2),4140(3),4187(3),3826(4),4140(4),4187(4),3(5),4188(4)]),flip(a)]. 4190 a21 != a19 | a11 != a19 | a8 != a11 | a12 != a11 | a16 != a11. [back_rewrite(3800),rewrite([4148(4),4148(7),4189(8),4189(11),4147(14),4189(14),3826(16),4140(16),4187(16),4147(17),4189(17),3826(19),4140(19),4187(19),4141(25),3817(28),4140(28),4187(28),4141(29),3817(31),4140(31),4187(31),4187(32),4187(35),4140(38),4187(38),4011(40),4141(40),4140(41),4187(41),4011(43),4141(43)]),flip(i),xx(c),xx(f),xx(g),xx(j),xx(k),xx(n),merge(d),merge(f),merge(h),merge(i)]. 4202 a16 = a12. [back_rewrite(899),rewrite([3817(1),4140(1),4187(1),3828(3),4025(4)]),flip(a)]. 4210 a19 * a12 = a12. [back_rewrite(447),rewrite([4187(2),3828(4),4011(4),4141(4),3828(6)])]. 4215 a11 = a19. [back_rewrite(3816),rewrite([4140(1),4187(1),3826(2),4140(2),4187(2),3(3)])]. 4223 a12 = a19. [back_rewrite(3794),rewrite([4215(2),3(4),3(3),4210(4)]),flip(a)]. 4234 a21 = a19. [back_rewrite(3762),rewrite([4141(2),4215(2),3(3)]),flip(a)]. 4243 a8 = a19. [back_rewrite(4072),rewrite([4147(1),4189(1),4215(1),3(3)]),flip(a)]. 4246 $F. [back_rewrite(4190),rewrite([4234(1),4215(4),4243(7),4215(8),4223(10),4215(11),4202(13),4223(13),4215(14)]),xx(a),xx(b),xx(c),xx(d),xx(e)]. ============================== end of proof ==========================