============================== prooftrans ============================ Prover9 (32) version Dec-2007, Dec 2007. Process 3592 was started by alexei on ALEXEI-LT, Wed Mar 12 09:56:06 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.51 (+ 0.08) seconds. % Length of proof is 179. % Level of proof is 28. % Maximum clause weight is 42. % Given clauses 111. 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 # 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 * a2 = a3. [assumption]. 7 a3 * a4 = a5. [assumption]. 8 a5 * a6 = a7. [assumption]. 9 a7 * a3 = a8. [assumption]. 10 a8 * a2 = a9. [assumption]. 11 a9 * a1 = a10. [assumption]. 12 a10 * a11 = a12. [assumption]. 13 a12 * a3 = a13. [assumption]. 14 a13 * a8 = a6. [assumption]. 15 a6 * a7 = a2. [assumption]. 16 a2 * a12 = a14. [assumption]. 17 a14 * a3 = a15. [assumption]. 18 a15 * a8 = a4. [assumption]. 19 a4 * a7 = a11. [assumption]. 20 a11 * a10 = a1. [assumption]. 21 a2 != a1 | a3 != a2 | a4 != a3 | a5 != a4 | a6 != a5 | a7 != a6 | a8 != a7 | a9 != a8 | a10 != a9 | a11 != a10 | a12 != a11 | a13 != a12 | a14 != a13 | a15 != a14. [deny(1)]. 22 a1 != a2 | a2 != a3 | a4 != a3 | a5 != a4 | a5 != a6 | a6 != a7 | a8 != a7 | a9 != a8 | a9 != a10 | a11 != a10 | a12 != a11 | a13 != a12 | a14 != a13 | a15 != a14. [copy(21),flip(a),flip(b),flip(e),flip(f),flip(i)]. 25 (x * y) * x = x * (y * x). [para(3(a,1),5(a,1,1)),flip(a)]. 26 ((x * y) * z) * (y * z) = x * z. [para(5(a,1),4(a,1,1))]. 28 ((x * y) * z) * y = x * (z * y). [para(4(a,1),5(a,1,1)),flip(a)]. 29 (x * (y * z)) * z = (x * z) * y. [para(4(a,1),5(a,1,2)),flip(a)]. 30 ((x * y) * z) * (u * (y * z)) = ((x * z) * u) * (y * z). [para(5(a,1),5(a,1,1))]. 31 (x * (y * z)) * ((u * y) * z) = (x * (u * z)) * (y * z). [para(5(a,1),5(a,1,2))]. 32 ((x * y) * z) * ((u * y) * z) = ((x * u) * y) * z. [para(5(a,1),5(a,2,1))]. 33 (x * (y * z)) * (z * (y * z)) = (x * y) * z. [para(5(a,1),5(a,2))]. 35 (x * (y * z)) * u = (x * u) * ((y * u) * (z * u)). [para(5(a,2),5(a,1,2)),flip(a)]. 37 a3 * a2 = a1. [para(6(a,1),4(a,1,1))]. 38 (a1 * x) * a2 = a3 * (x * a2). [para(6(a,1),5(a,1,1)),flip(a)]. 41 a5 * a4 = a3. [para(7(a,1),4(a,1,1))]. 44 (a3 * x) * (a4 * x) = a5 * x. [para(7(a,1),5(a,2,1))]. 45 a7 * a6 = a5. [para(8(a,1),4(a,1,1))]. 46 (a5 * x) * a6 = a7 * (x * a6). [para(8(a,1),5(a,1,1)),flip(a)]. 47 (x * a5) * a6 = (x * a6) * a7. [para(8(a,1),5(a,1,2)),flip(a)]. 49 a8 * a3 = a7. [para(9(a,1),4(a,1,1))]. 50 (a7 * x) * a3 = a8 * (x * a3). [para(9(a,1),5(a,1,1)),flip(a)]. 51 (x * a7) * a3 = (x * a3) * a8. [para(9(a,1),5(a,1,2)),flip(a)]. 53 a9 * a2 = a8. [para(10(a,1),4(a,1,1))]. 54 (a8 * x) * a2 = a9 * (x * a2). [para(10(a,1),5(a,1,1)),flip(a)]. 57 a10 * a1 = a9. [para(11(a,1),4(a,1,1))]. 61 a12 * a11 = a10. [para(12(a,1),4(a,1,1))]. 63 (x * a11) * a12 = (x * a10) * a11. [para(12(a,1),5(a,1,2))]. 65 a13 * a3 = a12. [para(13(a,1),4(a,1,1))]. 69 a6 * a8 = a13. [para(14(a,1),4(a,1,1))]. 73 a2 * a7 = a6. [para(15(a,1),4(a,1,1))]. 75 (x * a6) * a7 = (x * a7) * a2. [para(15(a,1),5(a,1,2)),flip(a)]. 77 (x * a5) * a6 = (x * a7) * a2. [back_rewrite(47),rewrite([75(8)])]. 86 a4 * a8 = a15. [para(18(a,1),4(a,1,1))]. 94 a1 * a10 = a11. [para(20(a,1),4(a,1,1))]. 96 (x * a11) * a10 = (x * a10) * a1. [para(20(a,1),5(a,1,2)),flip(a)]. 100 (x * (y * z)) * y = (x * y) * (y * (z * y)). [para(25(a,1),5(a,1,2)),flip(a)]. 106 a5 * a3 = a3 * (a4 * a3). [para(7(a,1),25(a,1,1))]. 107 a5 * (a6 * a5) = a7 * a5. [para(8(a,1),25(a,1,1)),flip(a)]. 111 a12 * a10 = a9. [para(12(a,1),25(a,1,1)),rewrite([20(7),57(6)])]. 112 a11 * a12 = a1 * a11. [para(12(a,1),25(a,2,2)),rewrite([20(3)]),flip(a)]. 115 a6 * a5 = a2 * a6. [para(15(a,1),25(a,1,1)),rewrite([45(7)]),flip(a)]. 116 a5 * a7 = a7 * a2. [para(15(a,1),25(a,2,2)),rewrite([45(3)])]. 122 a5 * (a2 * a6) = a7 * a5. [back_rewrite(107),rewrite([115(4)])]. 123 (a3 * x) * a2 = a1 * (x * a2). [para(37(a,1),5(a,1,1)),flip(a)]. 124 (x * a2) * a1 = (x * a3) * a2. [para(37(a,1),5(a,1,2))]. 128 (x * a5) * a4 = (x * a4) * a3. [para(41(a,1),5(a,1,2)),flip(a)]. 132 (x * a6) * a5 = (x * a7) * a6. [para(45(a,1),5(a,1,2))]. 162 (x * a10) * a1 = (x * a1) * a9. [para(57(a,1),5(a,1,2)),flip(a)]. 165 (x * a11) * a10 = (x * a1) * a9. [back_rewrite(96),rewrite([162(8)])]. 167 (x * a12) * a11 = (x * a1) * a9. [para(61(a,1),5(a,1,2)),rewrite([165(4)]),flip(a)]. 168 a12 * (a1 * a11) = a10 * a12. [para(61(a,1),25(a,1,1)),rewrite([112(7)]),flip(a)]. 169 ((x * a1) * a9) * a10 = x * a11. [para(61(a,1),26(a,1,2)),rewrite([167(4)])]. 179 (a6 * x) * a8 = a13 * (x * a8). [para(14(a,1),28(a,1,1,1))]. 183 (a4 * x) * a8 = a15 * (x * a8). [para(18(a,1),28(a,1,1,1))]. 192 (x * a7) * a6 = (x * a2) * a7. [para(73(a,1),5(a,1,2))]. 194 (x * a6) * a5 = (x * a2) * a7. [back_rewrite(132),rewrite([192(8)])]. 203 (x * a10) * a11 = (x * a1) * a10. [para(20(a,1),29(a,1,1,2)),flip(a)]. 206 (x * a11) * a12 = (x * a1) * a10. [back_rewrite(63),rewrite([203(8)])]. 207 a15 * a4 = a4 * (a8 * a4). [para(86(a,1),25(a,1,1))]. 212 a9 * a12 = a12 * (a10 * a12). [para(111(a,1),25(a,1,1))]. 215 (x * a9) * a10 = (x * a10) * a12. [para(111(a,1),29(a,1,1,2))]. 216 ((x * a1) * a10) * a12 = x * a11. [back_rewrite(169),rewrite([215(6)])]. 316 (x * a12) * (a1 * a11) = (x * a1) * a10. [para(112(a,1),5(a,1,2)),rewrite([206(10)])]. 319 ((x * a1) * a10) * (a1 * a11) = x * a12. [para(112(a,1),26(a,1,2)),rewrite([206(4)])]. 328 ((x * a7) * a2) * a5 = x * (a2 * a6). [para(115(a,1),28(a,2,2)),rewrite([77(4)])]. 499 (x * a5) * a3 = (x * a3) * (a3 * (a4 * a3)). [para(106(a,1),5(a,1,2)),flip(a)]. 503 (x * (a5 * y)) * (a3 * y) = (x * (a3 * y)) * ((a3 * (a4 * a3)) * y). [para(106(a,1),31(a,1,2,1)),flip(a)]. 561 ((x * a4) * a3) * y = ((x * a4) * y) * (a3 * y). [para(41(a,1),32(a,1,2,1)),rewrite([128(10)]),flip(a)]. 726 (x * a7) * a2 = (x * a2) * (a7 * a2). [para(15(a,1),33(a,1,1,2)),rewrite([15(6),75(10)]),flip(a)]. 732 (x * a4) * a3 = (x * a3) * (a4 * a3). [para(41(a,1),33(a,1,1,2)),rewrite([41(6),128(10)]),flip(a)]. 751 (x * (a1 * a11)) * (a10 * a12) = (x * a1) * a10. [para(112(a,1),33(a,1,1,2)),rewrite([112(8),168(9),206(12)])]. 783 ((x * a2) * (a7 * a2)) * a5 = x * (a2 * a6). [back_rewrite(328),rewrite([726(4)])]. 786 (x * a6) * a7 = (x * a2) * (a7 * a2). [back_rewrite(75),rewrite([726(8)])]. 791 ((x * a4) * y) * (a3 * y) = ((x * a3) * (a4 * a3)) * y. [back_rewrite(561),rewrite([732(4)]),flip(a)]. 1035 (a2 * a6) * (a7 * a5) = a6 * (a2 * a6). [para(122(a,1),25(a,2,2)),rewrite([194(5),3(3),73(3)]),flip(a)]. 1146 (x * (a3 * y)) * a2 = (x * a2) * (a1 * (y * a2)). [para(37(a,1),35(a,2,2,1))]. 1188 (x * (a4 * y)) * a8 = (x * a8) * (a15 * (y * a8)). [para(86(a,1),35(a,2,2,1))]. 1370 (a12 * x) * ((a1 * a11) * x) = (a10 * a12) * x. [para(168(a,1),5(a,2,1))]. 1371 (a1 * a11) * (a10 * a12) = a11 * (a1 * a11). [para(168(a,1),25(a,2,2)),rewrite([206(5),3(3),94(3)]),flip(a)]. 1372 ((x * a1) * a10) * (a10 * a12) = x * (a1 * a11). [para(168(a,1),26(a,1,2)),rewrite([316(6)])]. 1382 ((x * (a1 * a11)) * y) * ((a10 * a12) * y) = ((x * a1) * a10) * y. [para(168(a,1),32(a,1,2,1)),rewrite([316(16)])]. 1728 a11 * a2 = a3 * (a10 * a2). [para(94(a,1),38(a,1,1))]. 1742 (a4 * (a8 * a4)) * a15 = a15 * (a4 * a15). [para(207(a,1),25(a,1,1))]. 1904 (a3 * a7) * a11 = a7 * a2. [para(19(a,1),44(a,1,2)),rewrite([116(8)])]. 1906 (a3 * a8) * a15 = a5 * a8. [para(86(a,1),44(a,1,2))]. 1923 (a7 * a2) * a11 = a3 * a7. [para(1904(a,1),4(a,1,1))]. 1964 a7 * (a4 * a6) = a3 * a6. [para(41(a,1),46(a,1,1)),flip(a)]. 1981 (a5 * a8) * a15 = a3 * a8. [para(1906(a,1),4(a,1,1))]. 1983 (x * (a3 * a8)) * a15 = (x * a15) * (a5 * a8). [para(1906(a,1),5(a,1,2)),flip(a)]. 2015 ((a7 * x) * a2) * a11 = (a3 * a7) * ((x * a2) * a11). [para(1923(a,1),32(a,1,1)),flip(a)]. 2034 ((x * a2) * (a7 * a2)) * (a4 * a6) = ((x * a3) * (a4 * a3)) * a6. [para(1964(a,1),30(a,1,2)),rewrite([791(8),786(12)]),flip(a)]. 2048 (a3 * a8) * (a8 * a15) = a5 * a15. [para(1981(a,1),26(a,1,1))]. 2055 ((x * a5) * a8) * a15 = ((x * a8) * a15) * (a3 * a8). [para(1981(a,1),32(a,1,2)),flip(a)]. 2156 a8 * (a6 * a3) = a3 * (a4 * a3). [para(45(a,1),50(a,1,1)),rewrite([106(3)]),flip(a)]. 2170 a13 * (a3 * a8) = a2 * a3. [para(15(a,1),51(a,1,1)),rewrite([179(8)]),flip(a)]. 2171 a15 * (a3 * a8) = a11 * a3. [para(19(a,1),51(a,1,1)),rewrite([183(8)]),flip(a)]. 2177 (a3 * a8) * (a11 * a3) = a8 * (a2 * a3). [para(116(a,1),51(a,1,1)),rewrite([50(5),106(8),1188(12),2171(13)]),flip(a)]. 2188 (a2 * a3) * (a3 * a8) = a13. [para(2170(a,1),4(a,1,1))]. 2214 (a11 * a3) * a15 = a15 * (a5 * a8). [para(2171(a,1),25(a,1,1)),rewrite([1906(11)])]. 2217 ((x * a15) * (a3 * a8)) * (a8 * (a2 * a3)) = x * (a11 * a3). [para(2171(a,1),28(a,2,2)),rewrite([1983(6),503(10),1188(13),2171(14),2177(13)])]. 2221 ((x * a8) * a15) * (a3 * a8) = ((x * a3) * a8) * (a11 * a3). [para(2171(a,1),30(a,1,2)),flip(a)]. 2233 ((x * a5) * a8) * a15 = ((x * a3) * a8) * (a11 * a3). [back_rewrite(2055),rewrite([2221(14)])]. 2298 a2 * (a3 * a7) = a12. [para(2188(a,1),28(a,1,1)),rewrite([65(3),25(7),49(6)]),flip(a)]. 2319 a12 * (a3 * a7) = a2. [para(2298(a,1),4(a,1,1))]. 2324 (a1 * (a7 * a2)) * (a3 * a7) = (a3 * a7) * a12. [para(2298(a,1),25(a,2,2)),rewrite([123(5)])]. 2327 ((x * a2) * (a1 * (a7 * a2))) * (a3 * a7) = x * a12. [para(2298(a,1),28(a,2,2)),rewrite([1146(6)])]. 2328 (x * a12) * (a3 * a7) = (x * a2) * (a1 * (a7 * a2)). [para(2298(a,1),29(a,1,1,2)),rewrite([1146(12)])]. 2329 a6 * a3 = a12 * a7. [para(2298(a,1),29(a,1,1)),rewrite([73(6)]),flip(a)]. 2389 a3 * (a4 * a3) = a8 * (a12 * a7). [back_rewrite(2156),rewrite([2329(4)]),flip(a)]. 2403 (x * a5) * a3 = (x * a3) * (a8 * (a12 * a7)). [back_rewrite(499),rewrite([2389(11)])]. 2405 a5 * a3 = a8 * (a12 * a7). [back_rewrite(106),rewrite([2389(8)])]. 2406 a12 * ((a3 * a7) * a12) = a14. [para(2319(a,1),25(a,1,1)),rewrite([16(3)]),flip(a)]. 2435 (a12 * a7) * a8 = a2 * a3. [para(2329(a,1),51(a,2,1)),rewrite([15(3)]),flip(a)]. 2441 a7 * a2 = a10. [para(37(a,1),54(a,2,2)),rewrite([49(3),11(6)])]. 2481 (x * a12) * (a3 * a7) = (x * a2) * a11. [back_rewrite(2328),rewrite([2441(12),94(11)])]. 2482 ((x * a2) * a11) * (a3 * a7) = x * a12. [back_rewrite(2327),rewrite([2441(6),94(5)])]. 2483 (a3 * a7) * a12 = a11 * (a3 * a7). [back_rewrite(2324),rewrite([2441(4),94(3)]),flip(a)]. 2488 ((x * a2) * a10) * (a4 * a6) = ((x * a3) * (a4 * a3)) * a6. [back_rewrite(2034),rewrite([2441(5)])]. 2518 a3 * a7 = a12. [back_rewrite(1923),rewrite([2441(3),12(3)]),flip(a)]. 2546 ((x * a2) * a10) * a5 = x * (a2 * a6). [back_rewrite(783),rewrite([2441(5)])]. 2559 a14 = a12. [back_rewrite(2406),rewrite([2518(4),3(4),3(3)]),flip(a)]. 2562 ((x * a3) * a2) * a10 = x * a12. [back_rewrite(2482),rewrite([2518(7),206(6),124(4)])]. 2564 ((a7 * x) * a2) * a11 = a12 * ((x * a2) * a11). [back_rewrite(2015),rewrite([2518(9)])]. 2566 a1 * a11 = a12. [back_rewrite(2483),rewrite([2518(3),3(3),2518(5),112(4)]),flip(a)]. 2577 (x * a2) * a11 = x. [back_rewrite(2481),rewrite([2518(5),4(4)]),flip(a)]. 2584 a12 = a2. [back_rewrite(2319),rewrite([2518(4),3(3)])]. 2671 a1 != a2 | a2 != a3 | a4 != a3 | a5 != a4 | a5 != a6 | a6 != a7 | a8 != a7 | a9 != a8 | a9 != a10 | a11 != a10 | a11 != a2 | a13 != a2 | a15 != a2. [back_rewrite(22),rewrite([2584(31),2584(35),2559(37),2584(37),2559(41),2584(41)]),flip(k),flip(m),merge(m)]. 2672 a2 * a3 = a15. [back_rewrite(17),rewrite([2559(1),2584(1)])]. 2675 a15 = a13. [back_rewrite(2435),rewrite([2584(1),73(3),69(3),2672(4)]),flip(a)]. 2723 (a10 * a2) * x = a2 * x. [back_rewrite(1370),rewrite([2584(1),2566(5),2584(3),3(5),2584(4)]),flip(a)]. 2757 ((x * a1) * a10) * y = x * y. [back_rewrite(1382),rewrite([2566(3),2584(1),2584(5),2723(7),26(6)]),flip(a)]. 2762 x * (a10 * a2) = x * a2. [back_rewrite(1372),rewrite([2584(6),2757(8),2566(7),2584(5)])]. 2763 a1 = a2. [back_rewrite(1371),rewrite([2566(3),2584(1),2584(3),2762(5),3(3),2566(5),2584(3),1728(4),2762(6),37(4)]),flip(a)]. 2766 (x * a2) * a10 = x. [back_rewrite(751),rewrite([2763(1),2584(6),2762(8),100(6),1728(6),2762(8),37(6),2763(4),3(5),4(4),2763(1)]),flip(a)]. 2772 x * (a2 * a11) = x * a2. [back_rewrite(319),rewrite([2763(1),2766(4),2763(1),2584(5)])]. 2774 a10 * a2 = a2. [back_rewrite(168),rewrite([2584(1),2763(2),2772(5),3(3),2584(3)]),flip(a)]. 2775 a2 * a11 = a2. [back_rewrite(112),rewrite([2584(2),1728(3),2774(4),37(3),2763(1),2763(2)]),flip(a)]. 2777 a7 * x = a2 * x. [back_rewrite(2564),rewrite([2577(6),2584(3),2577(7)])]. 2784 a5 * a3 = a8 * a6. [back_rewrite(2405),rewrite([2584(5),73(7)])]. 2786 (x * a5) * a3 = (x * a3) * (a8 * a6). [back_rewrite(2403),rewrite([2584(8),73(10)])]. 2798 a3 * (a4 * a3) = a8 * a6. [back_rewrite(2389),rewrite([2584(7),73(9)])]. 2800 a6 * a3 = a6. [back_rewrite(2329),rewrite([2584(4),73(6)])]. 2836 a8 = a2. [back_rewrite(212),rewrite([2584(2),53(3),2584(2),2584(4),2774(5),3(4)])]. 2844 a10 = a2. [back_rewrite(61),rewrite([2584(1),2775(3)]),flip(a)]. 2862 x * a2 = x * a3. [back_rewrite(2562),rewrite([2844(5),4(6),2584(3)]),flip(a)]. 2880 x * a11 = x * a3. [back_rewrite(216),rewrite([2763(1),2862(2),2844(3),2862(4),4(4),2584(1),2862(2)]),flip(a)]. 2887 a13 = a2. [back_rewrite(12),rewrite([2844(1),2880(3),2672(3),2675(1),2584(2)])]. 2894 x * (a11 * a3) = x * a3. [back_rewrite(2217),rewrite([2675(1),2887(1),2862(2),2836(4),2862(5),3(5),4(4),2836(1),2672(4),2675(2),2887(2),3(3),2862(2)]),flip(a)]. 2895 a2 = a3. [back_rewrite(2177),rewrite([2836(2),2862(3),3(3),2894(5),3(3),2836(2),2672(5),2675(3),2887(3),3(4)]),flip(a)]. 2896 a4 != a3 | a5 != a4 | a5 != a6 | a6 != a7 | a7 != a3 | a9 != a3 | a11 != a3. [back_rewrite(2671),rewrite([2763(1),2895(1),2895(2),2895(4),2836(19),2895(19),2836(23),2895(23),2844(26),2895(26),2844(29),2895(29),2895(32),2887(34),2895(34),2895(35),2675(37),2887(37),2895(37),2895(38)]),flip(g),xx(a),xx(b),xx(l),xx(m),merge(g),merge(i)]. 2897 x * (a3 * a6) = x * a3. [back_rewrite(2233),rewrite([2836(3),2895(3),2786(4),2836(3),2895(3),2675(7),2887(7),2895(7),100(8),4(4),2800(4),2836(7),2895(7),4(8),2894(8)])]. 2901 a11 = a3. [back_rewrite(2214),rewrite([2675(4),2887(4),2895(4),4(5),2675(2),2887(2),2895(2),2836(4),2895(4),2784(5),2836(3),2895(3),2897(6),3(4)])]. 2904 a3 * a6 = a3. [back_rewrite(2048),rewrite([2836(2),2895(2),3(3),2836(2),2895(2),2675(3),2887(3),2895(3),3(4),3(3),2675(3),2887(3),2895(3),2784(4),2836(2),2895(2)]),flip(a)]. 2912 a4 = a3. [back_rewrite(1742),rewrite([2836(2),2895(2),7(4),2675(4),2887(4),2895(4),2786(5),2836(4),2895(4),2904(6),4(5),2675(2),2887(2),2895(2),2675(4),2887(4),2895(4),2798(6),2836(2),2895(2),2904(4)])]. 2937 a9 = a3. [back_rewrite(57),rewrite([2844(1),2895(1),2763(2),2895(2),3(3)]),flip(a)]. 2940 x * a5 = x * a3. [back_rewrite(2546),rewrite([2895(1),2844(3),2895(3),4(4),2895(3),2904(5)])]. 2948 x * a6 = x * a3. [back_rewrite(2488),rewrite([2895(1),2844(3),2895(3),4(4),2912(1),2904(3),2912(5),3(7),4(6)]),flip(a)]. 2989 a6 = a3. [back_rewrite(1035),rewrite([2895(1),2948(3),3(3),2940(4),2777(4),2895(2),3(4),3(3),2895(3),2948(5),3(5),2800(4)]),flip(a)]. 2993 a5 = a3. [back_rewrite(45),rewrite([2989(2),2777(3),2895(1),3(3)]),flip(a)]. 3014 a7 = a3. [back_rewrite(49),rewrite([2836(1),2895(1),3(3)]),flip(a)]. 3022 \$F. [back_rewrite(2896),rewrite([2912(1),2993(4),2912(5),2993(7),2989(8),2989(10),3014(11),3014(13),2937(16),2901(19)]),xx(a),xx(b),xx(c),xx(d),xx(e),xx(f),xx(g)]. ============================== end of proof ==========================