============================== Prover9 =============================== Prover9 (32) version Dec-2007, Dec 2007. Process 1328 was started by alexei on ALEXEI-LT, Tue Jan 14 14:39:45 2014 The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace4/bin-win32/prover9". ============================== end of head =========================== ============================== INPUT ================================= assign(report_stderr,2). set(ignore_option_dependencies). if(Prover9). % Conditional input included. assign(eq_defs,pass). assign(max_megs,520). assign(max_weight,4000). assign(demod_step_limit,1660). assign(demod_size_limit,1620). assign(max_seconds,60). end_if. if(Mace4). % Conditional input omitted. end_if. if(Prover9). % Conditional input included. assign(max_seconds,-1). assign(max_seconds,-1). assign(max_seconds,-1). assign(max_seconds,-1). end_if. if(Mace4). % Conditional input omitted. end_if. formulas(assumptions). x * x = x. (x * y) * y = x. (x * z) * (y * z) = (x * y) * z. a1 * a6 = a2. a2 * a7 = a3. a3 * a1 = a4. a4 * a10 = a5. a5 * a9 = a6. a6 * a2 = a7. a7 * a3 = a8. a8 * a6 = a9. a9 * a4 = a10. a10 * a5 = a11. a11 * a4 = a1. end_of_list. formulas(goals). a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 & a10 = a11. X * (x * y) = y. end_of_list. ============================== end of input ========================== % Enabling option dependencies (ignore applies only on input). ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 & a10 = a11 # label(non_clause) # label(goal). [goal]. 2 X * (x * y) = y # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x * x = x. [assumption]. (x * y) * y = x. [assumption]. (x * y) * (z * y) = (x * z) * y. [assumption]. a1 * a6 = a2. [assumption]. a2 * a7 = a3. [assumption]. a3 * a1 = a4. [assumption]. a4 * a10 = a5. [assumption]. a5 * a9 = a6. [assumption]. a6 * a2 = a7. [assumption]. a7 * a3 = a8. [assumption]. a8 * a6 = a9. [assumption]. a9 * a4 = a10. [assumption]. a10 * a5 = a11. [assumption]. a11 * a4 = a1. [assumption]. a2 != a1 | a3 != a2 | a4 != a3 | a5 != a4 | a5 != a6 | a7 != a6 | a8 != a7 | a8 != a9 | a9 != a10 | a11 != a10. [deny(1)]. X * (c1 * c2) != c2. [deny(2)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 2). % (Horn set with more than one neg. clause) Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ a4, a6, a1, a10, a2, a3, a5, a7, a9, a11, a8, X, c1, c2, * ]). After inverse_order: (no changes). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 10). % (nonunit Horn with equality) Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 3 x * x = x. [assumption]. 4 (x * y) * y = x. [assumption]. 5 (x * y) * (z * y) = (x * z) * y. [assumption]. 6 a1 * a6 = a2. [assumption]. 7 a2 * a7 = a3. [assumption]. 8 a3 * a1 = a4. [assumption]. 9 a4 * a10 = a5. [assumption]. 10 a5 * a9 = a6. [assumption]. 11 a6 * a2 = a7. [assumption]. 12 a7 * a3 = a8. [assumption]. 13 a8 * a6 = a9. [assumption]. 14 a9 * a4 = a10. [assumption]. 15 a10 * a5 = a11. [assumption]. 16 a11 * a4 = a1. [assumption]. 18 a2 != a1 | a3 != a2 | a3 != a4 | a5 != a4 | a5 != a6 | a7 != a6 | a8 != a7 | a8 != a9 | a9 != a10 | a11 != a10. [copy(17),flip(c)]. 19 X * (c1 * c2) != c2. [deny(2)]. end_of_list. formulas(demodulators). 3 x * x = x. [assumption]. 4 (x * y) * y = x. [assumption]. 6 a1 * a6 = a2. [assumption]. 7 a2 * a7 = a3. [assumption]. 8 a3 * a1 = a4. [assumption]. 9 a4 * a10 = a5. [assumption]. 10 a5 * a9 = a6. [assumption]. 11 a6 * a2 = a7. [assumption]. 12 a7 * a3 = a8. [assumption]. 13 a8 * a6 = a9. [assumption]. 14 a9 * a4 = a10. [assumption]. 15 a10 * a5 = a11. [assumption]. 16 a11 * a4 = a1. [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=5): 3 x * x = x. [assumption]. given #2 (I,wt=7): 4 (x * y) * y = x. [assumption]. given #3 (I,wt=13): 5 (x * y) * (z * y) = (x * z) * y. [assumption]. given #4 (I,wt=5): 6 a1 * a6 = a2. [assumption]. given #5 (I,wt=5): 7 a2 * a7 = a3. [assumption]. given #6 (I,wt=5): 8 a3 * a1 = a4. [assumption]. given #7 (I,wt=5): 9 a4 * a10 = a5. [assumption]. given #8 (I,wt=5): 10 a5 * a9 = a6. [assumption]. given #9 (I,wt=5): 11 a6 * a2 = a7. [assumption]. given #10 (I,wt=5): 12 a7 * a3 = a8. [assumption]. given #11 (I,wt=5): 13 a8 * a6 = a9. [assumption]. given #12 (I,wt=5): 14 a9 * a4 = a10. [assumption]. given #13 (I,wt=5): 15 a10 * a5 = a11. [assumption]. given #14 (I,wt=5): 16 a11 * a4 = a1. [assumption]. given #15 (I,wt=30): 18 a2 != a1 | a3 != a2 | a3 != a4 | a5 != a4 | a5 != a6 | a7 != a6 | a8 != a7 | a8 != a9 | a9 != a10 | a11 != a10. [copy(17),flip(c)]. given #16 (I,wt=7): 19 X * (c1 * c2) != c2. [deny(2)]. given #17 (A,wt=11): 21 (x * y) * x = x * (y * x). [para(3(a,1),5(a,1,1)),flip(a)]. given #18 (T,wt=5): 33 a2 * a6 = a1. [para(6(a,1),4(a,1,1))]. given #19 (T,wt=5): 37 a3 * a7 = a2. [para(7(a,1),4(a,1,1))]. given #20 (T,wt=5): 41 a4 * a1 = a3. [para(8(a,1),4(a,1,1))]. given #21 (T,wt=5): 45 a5 * a10 = a4. [para(9(a,1),4(a,1,1))]. given #22 (A,wt=13): 22 ((x * y) * z) * (y * z) = x * z. [para(5(a,1),4(a,1,1))]. given #23 (T,wt=5): 49 a6 * a9 = a5. [para(10(a,1),4(a,1,1))]. given #24 (T,wt=5): 53 a7 * a2 = a6. [para(11(a,1),4(a,1,1))]. given #25 (T,wt=5): 58 a8 * a3 = a7. [para(12(a,1),4(a,1,1))]. given #26 (T,wt=5): 62 a9 * a6 = a8. [para(13(a,1),4(a,1,1))]. given #27 (A,wt=13): 24 ((x * y) * z) * y = x * (z * y). [para(4(a,1),5(a,1,1)),flip(a)]. given #28 (T,wt=5): 66 a10 * a4 = a9. [para(14(a,1),4(a,1,1))]. given #29 (T,wt=5): 70 a11 * a5 = a10. [para(15(a,1),4(a,1,1))]. given #30 (T,wt=5): 74 a1 * a4 = a11. [para(16(a,1),4(a,1,1))]. given #31 (T,wt=5): 86 a3 * a2 = a1. [para(7(a,1),21(a,1,1)),rewrite([53(7),33(6)])]. given #32 (A,wt=13): 25 (x * (y * z)) * z = (x * z) * y. [para(4(a,1),5(a,1,2)),flip(a)]. given #33 (T,wt=5): 87 a6 * a7 = a8. [para(7(a,1),21(a,2,2)),rewrite([53(3),12(6)])]. given #34 (T,wt=5): 90 a9 * a10 = a11. [para(9(a,1),21(a,2,2)),rewrite([66(3),15(6)])]. given #35 (T,wt=5): 93 a1 * a2 = a3. [para(11(a,1),21(a,2,2)),rewrite([33(3),7(6)])]. given #36 (T,wt=5): 94 a8 * a7 = a6. [para(12(a,1),21(a,1,1)),rewrite([37(7),53(6)])]. given #37 (A,wt=21): 26 ((x * y) * z) * (u * (y * z)) = ((x * z) * u) * (y * z). [para(5(a,1),5(a,1,1))]. given #38 (T,wt=5): 98 a11 * a10 = a9. [para(15(a,1),21(a,1,1)),rewrite([45(7),66(6)])]. given #39 (T,wt=7): 89 a5 * a4 = a4 * a9. [para(9(a,1),21(a,1,1)),rewrite([66(7)])]. given #40 (T,wt=7): 92 a7 * a6 = a6 * a1. [para(11(a,1),21(a,1,1)),rewrite([33(7)])]. given #41 (T,wt=7): 95 a3 * a8 = a2 * a3. [para(12(a,1),21(a,2,2)),rewrite([37(3)]),flip(a)]. given #42 (A,wt=21): 27 (x * (y * z)) * ((u * y) * z) = (x * (u * z)) * (y * z). [para(5(a,1),5(a,1,2))]. given #43 (T,wt=7): 99 a5 * a11 = a4 * a5. [para(15(a,1),21(a,2,2)),rewrite([45(3)]),flip(a)]. given #44 (T,wt=7): 111 a3 * a4 = a4 * a11. [para(41(a,1),21(a,1,1)),rewrite([74(7)])]. given #45 (T,wt=7): 112 a11 * a1 = a1 * a3. [para(41(a,1),21(a,2,2)),rewrite([74(3)])]. given #46 (T,wt=7): 137 a5 * a6 = a6 * a8. [para(49(a,1),21(a,1,1)),rewrite([62(7)])]. given #47 (A,wt=19): 28 ((x * y) * z) * ((u * y) * z) = ((x * u) * y) * z. [para(5(a,1),5(a,2,1))]. given #48 (T,wt=7): 138 a8 * a9 = a9 * a5. [para(49(a,1),21(a,2,2)),rewrite([62(3)])]. given #49 (T,wt=7): 186 a6 * (a6 * a1) = a9. [para(87(a,1),21(a,1,1)),rewrite([13(3),92(5)]),flip(a)]. given #50 (T,wt=5): 665 a7 * a1 = a9. [para(186(a,1),24(a,2)),rewrite([21(5),6(4),11(3)])]. given #51 (T,wt=5): 667 a9 * a1 = a7. [para(186(a,1),25(a,1,1)),rewrite([21(8),6(7),11(6)])]. given #52 (A,wt=17): 29 (x * (y * z)) * (z * (y * z)) = (x * y) * z. [para(5(a,1),5(a,2))]. given #53 (T,wt=7): 657 a9 * (a6 * a1) = a6. [para(186(a,1),4(a,1,1))]. given #54 (T,wt=9): 85 a2 * a1 = a1 * (a6 * a1). [para(6(a,1),21(a,1,1))]. given #55 (T,wt=9): 88 a3 * (a1 * a3) = a4 * a3. [para(8(a,1),21(a,1,1)),flip(a)]. given #56 (T,wt=9): 91 a5 * (a9 * a5) = a6 * a5. [para(10(a,1),21(a,1,1)),flip(a)]. given #57 (A,wt=19): 30 ((x * y) * (z * y)) * (u * y) = ((x * z) * u) * y. [para(5(a,2),5(a,1,1))]. given #58 (T,wt=9): 96 a8 * (a6 * a8) = a9 * a8. [para(13(a,1),21(a,1,1)),flip(a)]. given #59 (T,wt=9): 97 a9 * (a4 * a9) = a10 * a9. [para(14(a,1),21(a,1,1)),flip(a)]. given #60 (T,wt=7): 1001 a4 * (a4 * a9) = a6. [para(97(a,1),21(a,2,2)),rewrite([4(5),48(12),10(8)])]. given #61 (T,wt=7): 1013 a6 * (a4 * a9) = a4. [para(1001(a,1),4(a,1,1))]. given #62 (A,wt=19): 31 (x * (y * z)) * u = (x * u) * ((y * u) * (z * u)). [para(5(a,2),5(a,1,2)),flip(a)]. given #63 (T,wt=7): 1017 a6 * a4 = a4 * a5. [para(1001(a,1),21(a,1,1)),rewrite([21(9),14(8),9(7)])]. given #64 (T,wt=9): 100 a11 * (a4 * a11) = a1 * a11. [para(16(a,1),21(a,1,1)),flip(a)]. given #65 (T,wt=9): 144 a8 * (a2 * a3) = a7 * a8. [para(58(a,1),21(a,1,1)),rewrite([95(7)]),flip(a)]. given #66 (T,wt=7): 1336 a7 * a8 = a6 * a3. [para(144(a,1),24(a,2)),rewrite([58(3),53(3)]),flip(a)]. given #67 (A,wt=19): 32 ((x * y) * (z * y)) * u = ((x * z) * u) * (y * u). [para(5(a,2),5(a,2,1)),flip(a)]. given #68 (T,wt=9): 168 a11 * (a4 * a5) = a10 * a11. [para(70(a,1),21(a,1,1)),rewrite([99(7)]),flip(a)]. given #69 (T,wt=7): 1602 a9 * a5 = a10 * a11. [para(168(a,1),24(a,2)),rewrite([70(3),66(3)])]. given #70 (T,wt=7): 1652 a8 * a9 = a10 * a11. [back_rewrite(138),rewrite([1602(6)])]. given #71 (T,wt=7): 1656 (a10 * a11) * a9 = a8. [para(1602(a,1),21(a,1,1)),rewrite([10(9),62(8)])]. given #72 (A,wt=11): 34 (a1 * x) * a6 = a2 * (x * a6). [para(6(a,1),5(a,1,1)),flip(a)]. given #73 (T,wt=7): 1669 a10 * (a10 * a9) = a8. [para(1656(a,1),5(a,2)),rewrite([194(6),78(9)])]. given #74 (T,wt=7): 1706 a8 * (a10 * a9) = a10. [para(1669(a,1),4(a,1,1))]. given #75 (T,wt=9): 175 a3 * (a2 * a3) = a1 * a3. [para(86(a,1),21(a,1,1)),flip(a)]. given #76 (T,wt=9): 194 a11 * a9 = a9 * (a10 * a9). [para(90(a,1),21(a,1,1))]. given #77 (A,wt=11): 35 (x * a1) * a6 = (x * a6) * a2. [para(6(a,1),5(a,1,2)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.28 (+ 0.06) seconds. % Length of proof is 134. % Level of proof is 18. % Maximum clause weight is 30. % Given clauses 77. 1 a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 & a10 = a11 # 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 * a6 = a2. [assumption]. 7 a2 * a7 = a3. [assumption]. 8 a3 * a1 = a4. [assumption]. 9 a4 * a10 = a5. [assumption]. 10 a5 * a9 = a6. [assumption]. 11 a6 * a2 = a7. [assumption]. 12 a7 * a3 = a8. [assumption]. 13 a8 * a6 = a9. [assumption]. 14 a9 * a4 = a10. [assumption]. 15 a10 * a5 = a11. [assumption]. 16 a11 * a4 = a1. [assumption]. 17 a2 != a1 | a3 != a2 | a4 != a3 | a5 != a4 | a5 != a6 | a7 != a6 | a8 != a7 | a8 != a9 | a9 != a10 | a11 != a10. [deny(1)]. 18 a2 != a1 | a3 != a2 | a3 != a4 | a5 != a4 | a5 != a6 | a7 != a6 | a8 != a7 | a8 != a9 | a9 != a10 | a11 != a10. [copy(17),flip(c)]. 21 (x * y) * x = x * (y * x). [para(3(a,1),5(a,1,1)),flip(a)]. 22 ((x * y) * z) * (y * z) = x * z. [para(5(a,1),4(a,1,1))]. 24 ((x * y) * z) * y = x * (z * y). [para(4(a,1),5(a,1,1)),flip(a)]. 25 (x * (y * z)) * z = (x * z) * y. [para(4(a,1),5(a,1,2)),flip(a)]. 26 ((x * y) * z) * (u * (y * z)) = ((x * z) * u) * (y * z). [para(5(a,1),5(a,1,1))]. 27 (x * (y * z)) * ((u * y) * z) = (x * (u * z)) * (y * z). [para(5(a,1),5(a,1,2))]. 29 (x * (y * z)) * (z * (y * z)) = (x * y) * z. [para(5(a,1),5(a,2))]. 31 (x * (y * z)) * u = (x * u) * ((y * u) * (z * u)). [para(5(a,2),5(a,1,2)),flip(a)]. 33 a2 * a6 = a1. [para(6(a,1),4(a,1,1))]. 34 (a1 * x) * a6 = a2 * (x * a6). [para(6(a,1),5(a,1,1)),flip(a)]. 35 (x * a1) * a6 = (x * a6) * a2. [para(6(a,1),5(a,1,2)),flip(a)]. 37 a3 * a7 = a2. [para(7(a,1),4(a,1,1))]. 41 a4 * a1 = a3. [para(8(a,1),4(a,1,1))]. 45 a5 * a10 = a4. [para(9(a,1),4(a,1,1))]. 47 (x * a10) * a5 = (x * a4) * a10. [para(9(a,1),5(a,1,2))]. 48 (a4 * x) * (a10 * x) = a5 * x. [para(9(a,1),5(a,2,1))]. 49 a6 * a9 = a5. [para(10(a,1),4(a,1,1))]. 51 (x * a9) * a6 = (x * a5) * a9. [para(10(a,1),5(a,1,2))]. 53 a7 * a2 = a6. [para(11(a,1),4(a,1,1))]. 58 a8 * a3 = a7. [para(12(a,1),4(a,1,1))]. 62 a9 * a6 = a8. [para(13(a,1),4(a,1,1))]. 66 a10 * a4 = a9. [para(14(a,1),4(a,1,1))]. 68 (x * a9) * a4 = (x * a4) * a10. [para(14(a,1),5(a,1,2)),flip(a)]. 70 a11 * a5 = a10. [para(15(a,1),4(a,1,1))]. 72 (x * a5) * a11 = (x * a4) * a10. [para(15(a,1),5(a,1,2)),rewrite([47(8)])]. 74 a1 * a4 = a11. [para(16(a,1),4(a,1,1))]. 78 (x * y) * (y * (x * y)) = x * (x * y). [para(4(a,1),21(a,1,1)),flip(a)]. 85 a2 * a1 = a1 * (a6 * a1). [para(6(a,1),21(a,1,1))]. 86 a3 * a2 = a1. [para(7(a,1),21(a,1,1)),rewrite([53(7),33(6)])]. 87 a6 * a7 = a8. [para(7(a,1),21(a,2,2)),rewrite([53(3),12(6)])]. 89 a5 * a4 = a4 * a9. [para(9(a,1),21(a,1,1)),rewrite([66(7)])]. 90 a9 * a10 = a11. [para(9(a,1),21(a,2,2)),rewrite([66(3),15(6)])]. 92 a7 * a6 = a6 * a1. [para(11(a,1),21(a,1,1)),rewrite([33(7)])]. 93 a1 * a2 = a3. [para(11(a,1),21(a,2,2)),rewrite([33(3),7(6)])]. 94 a8 * a7 = a6. [para(12(a,1),21(a,1,1)),rewrite([37(7),53(6)])]. 95 a3 * a8 = a2 * a3. [para(12(a,1),21(a,2,2)),rewrite([37(3)]),flip(a)]. 97 a9 * (a4 * a9) = a10 * a9. [para(14(a,1),21(a,1,1)),flip(a)]. 99 a5 * a11 = a4 * a5. [para(15(a,1),21(a,2,2)),rewrite([45(3)]),flip(a)]. 114 (x * a5) * a10 = (x * a10) * a4. [para(45(a,1),5(a,1,2)),flip(a)]. 135 (a6 * x) * a9 = a5 * (x * a9). [para(49(a,1),5(a,1,1)),flip(a)]. 136 (x * a9) * a5 = (x * a6) * a9. [para(49(a,1),5(a,1,2))]. 144 a8 * (a2 * a3) = a7 * a8. [para(58(a,1),21(a,1,1)),rewrite([95(7)]),flip(a)]. 147 (x * a5) * a9 = (x * a6) * a8. [para(62(a,1),5(a,1,2)),rewrite([51(8)]),flip(a)]. 148 (x * a9) * a6 = (x * a6) * a8. [back_rewrite(51),rewrite([147(8)])]. 158 ((x * a10) * a4) * a5 = x * a11. [para(15(a,1),24(a,2,2)),rewrite([114(4)])]. 164 (x * a10) * a4 = (x * a4) * a9. [para(66(a,1),5(a,1,2)),flip(a)]. 165 ((x * a4) * a6) * a9 = x * a11. [back_rewrite(158),rewrite([164(4),136(6)])]. 166 (x * a5) * a10 = (x * a4) * a9. [back_rewrite(114),rewrite([164(8)])]. 167 (x * a11) * a5 = (x * a4) * a9. [para(70(a,1),5(a,1,2)),rewrite([166(4)]),flip(a)]. 168 a11 * (a4 * a5) = a10 * a11. [para(70(a,1),21(a,1,1)),rewrite([99(7)]),flip(a)]. 170 (x * a1) * a4 = (x * a4) * a11. [para(74(a,1),5(a,1,2)),flip(a)]. 173 (x * a3) * a2 = (x * a2) * a1. [para(86(a,1),5(a,1,2)),flip(a)]. 186 a6 * (a6 * a1) = a9. [para(87(a,1),21(a,1,1)),rewrite([13(3),92(5)]),flip(a)]. 194 a11 * a9 = a9 * (a10 * a9). [para(90(a,1),21(a,1,1))]. 198 a1 * (a1 * (a6 * a1)) = a4. [para(93(a,1),21(a,1,1)),rewrite([8(3),85(5)]),flip(a)]. 199 a8 * (a7 * a8) = a6 * a8. [para(94(a,1),21(a,1,1)),flip(a)]. 392 (x * (y * a5)) * a10 = (x * a10) * ((y * a4) * a9). [para(70(a,1),27(a,1,1,2)),rewrite([167(6),70(13)]),flip(a)]. 657 a9 * (a6 * a1) = a6. [para(186(a,1),4(a,1,1))]. 710 (x * a2) * a1 = (x * a1) * (a1 * (a6 * a1)). [para(86(a,1),29(a,1,1,2)),rewrite([86(6),85(5),173(12)]),flip(a)]. 751 a9 * (a5 * (a1 * a9)) = a5. [para(657(a,1),21(a,1,1)),rewrite([49(3),135(7)]),flip(a)]. 760 a8 * a1 = a6 * (a1 * (a6 * a1)). [para(657(a,1),29(a,1,1)),rewrite([62(10)]),flip(a)]. 766 (x * (a1 * (a6 * a1))) * a4 = (x * a1) * (a1 * (a6 * a1)). [para(85(a,1),29(a,1,1,2)),rewrite([85(10),198(13),710(12)])]. 1001 a4 * (a4 * a9) = a6. [para(97(a,1),21(a,2,2)),rewrite([4(5),48(12),10(8)])]. 1002 ((x * a4) * a10) * (a4 * a9) = x * (a10 * a9). [para(97(a,1),24(a,2,2)),rewrite([25(6),68(4)])]. 1005 ((x * a4) * a9) * (a10 * a9) = x * (a4 * a9). [para(97(a,1),26(a,1,2)),rewrite([4(12)])]. 1013 a6 * (a4 * a9) = a4. [para(1001(a,1),4(a,1,1))]. 1017 a6 * a4 = a4 * a5. [para(1001(a,1),21(a,1,1)),rewrite([21(9),14(8),9(7)])]. 1018 (a4 * a6) * a8 = a5 * (a4 * a9). [para(1001(a,1),21(a,2,2)),rewrite([21(5),14(4),9(3),148(10)]),flip(a)]. 1026 ((x * a4) * a6) * a8 = x * (a10 * a9). [para(1001(a,1),26(a,1,2)),rewrite([148(6),68(10),1002(14)])]. 1033 a6 * (a10 * a9) = a4 * a9. [para(1001(a,1),29(a,1,1)),rewrite([97(6),3(8)])]. 1035 a6 * (a5 * (a4 * a9)) = a4 * a6. [para(1013(a,1),21(a,1,1)),rewrite([148(9),1018(9)]),flip(a)]. 1043 a5 * (a4 * a9) = a4 * (a10 * a9). [para(1013(a,1),29(a,1,1)),rewrite([97(6),1017(8),147(10),1018(10)]),flip(a)]. 1046 a6 * (a4 * (a10 * a9)) = a4 * a6. [back_rewrite(1035),rewrite([1043(6)])]. 1071 (x * (a6 * y)) * a2 = (x * a2) * (a7 * (y * a2)). [para(11(a,1),31(a,2,2,1))]. 1121 (x * (a1 * y)) * a4 = (x * a4) * (a11 * (y * a4)). [para(74(a,1),31(a,2,2,1))]. 1294 (x * a1) * (a1 * (a6 * a1)) = (x * a4) * a10. [back_rewrite(766),rewrite([1121(8),170(8),1017(6),72(8),3(6),9(6),70(5)]),flip(a)]. 1301 (x * a2) * a1 = (x * a4) * a10. [back_rewrite(710),rewrite([1294(12)])]. 1303 (x * a6) * a4 = (x * a4) * (a4 * a5). [para(1017(a,1),5(a,1,2)),flip(a)]. 1336 a7 * a8 = a6 * a3. [para(144(a,1),24(a,2)),rewrite([58(3),53(3)]),flip(a)]. 1356 a8 * (a6 * a3) = a6 * a8. [back_rewrite(199),rewrite([1336(4)])]. 1358 a8 * (a2 * a3) = a6 * a3. [back_rewrite(144),rewrite([1336(8)])]. 1602 a9 * a5 = a10 * a11. [para(168(a,1),24(a,2)),rewrite([70(3),66(3)])]. 1613 (a10 * a11) * (a5 * (a4 * a5)) = a1 * a5. [para(168(a,1),29(a,1,1)),rewrite([16(12)])]. 1656 (a10 * a11) * a9 = a8. [para(1602(a,1),21(a,1,1)),rewrite([10(9),62(8)])]. 1657 ((x * a6) * a8) * a5 = x * (a10 * a11). [para(1602(a,1),24(a,2,2)),rewrite([147(4)])]. 1669 a10 * (a10 * a9) = a8. [para(1656(a,1),5(a,2)),rewrite([194(6),78(9)])]. 1671 a8 * (a9 * (a10 * a9)) = a10 * a9. [para(1656(a,1),22(a,1,1)),rewrite([194(4)])]. 1692 a3 * a6 = a1 * (a6 * a1). [para(33(a,1),34(a,2,2)),rewrite([93(3),85(6)])]. 1706 a8 * (a10 * a9) = a10. [para(1669(a,1),4(a,1,1))]. 1769 (x * a11) * a9 = (x * a9) * (a9 * (a10 * a9)). [para(194(a,1),5(a,1,2)),flip(a)]. 1784 a2 * a3 = a4 * a6. [para(8(a,1),35(a,1,1)),rewrite([1692(6),1071(10),93(6),93(8),12(7),95(6)]),flip(a)]. 1789 x * (a10 * a9) = x * (a6 * a1). [para(35(a,1),24(a,1,1)),rewrite([1301(6),1303(4),392(8),3(7),1002(8)])]. 1822 a8 * (a4 * a6) = a6 * a3. [back_rewrite(1358),rewrite([1784(4)])]. 1867 (x * a11) * a9 = (x * a6) * a8. [back_rewrite(1769),rewrite([1789(11),657(11),148(8)])]. 1891 a8 * (a6 * a1) = a10. [back_rewrite(1706),rewrite([1789(5)])]. 1893 a10 * a9 = a9. [back_rewrite(1671),rewrite([1789(6),657(6),13(3)]),flip(a)]. 1894 a8 = a9. [back_rewrite(1669),rewrite([1893(4),1893(3)]),flip(a)]. 1897 a4 * a6 = a4. [back_rewrite(1046),rewrite([1893(5),1013(5)]),flip(a)]. 1899 a4 * a9 = a5. [back_rewrite(1033),rewrite([1893(4),49(3)]),flip(a)]. 1900 x * a11 = x * a9. [back_rewrite(1026),rewrite([1894(5),165(6),1893(5)])]. 1901 x * a5 = x * a4. [back_rewrite(1005),rewrite([1893(7),4(6),1899(5)]),flip(a)]. 1910 x * (a6 * a1) = x * a9. [back_rewrite(1789),rewrite([1893(3)]),flip(a)]. 1919 a9 = a10. [back_rewrite(1891),rewrite([1894(1),1910(5),3(3)])]. 1920 (x * a6) * a10 = x. [back_rewrite(1867),rewrite([1900(2),1919(1),1919(3),4(4),1894(3),1919(3)]),flip(a)]. 1938 a6 * a3 = a10. [back_rewrite(1822),rewrite([1894(1),1919(1),1897(4),66(3),1919(1)]),flip(a)]. 1941 x * a10 = x * a4. [back_rewrite(1657),rewrite([1894(3),1919(3),1920(4),1901(2),1900(5),1919(4),3(5)]),flip(a)]. 1962 a10 = a4. [back_rewrite(1356),rewrite([1894(1),1919(1),1938(4),3(3),1894(3),1919(3),1941(4),1017(4),1901(4),3(4)])]. 1986 a3 = a4. [back_rewrite(760),rewrite([1894(1),1919(1),1962(1),41(3),1910(7),1919(4),1962(4),74(5),1900(4),1919(3),1962(3),1017(4),1901(4),3(4)])]. 2021 a7 = a4. [back_rewrite(58),rewrite([1894(1),1919(1),1962(1),1986(2),3(3)]),flip(a)]. 2022 a2 != a1 | a2 != a4 | a5 != a4 | a5 != a6 | a6 != a4 | a11 != a4. [back_rewrite(18),rewrite([1986(4),1986(7),2021(16),1894(19),1919(19),1962(19),2021(20),1894(22),1919(22),1962(22),1919(23),1962(23),1919(25),1962(25),1962(26),1962(29)]),flip(b),flip(f),xx(c),xx(g),xx(h),xx(i)]. 2023 a11 = a4. [back_rewrite(1613),rewrite([1962(1),1900(3),1919(2),1962(2),3(3),1901(5),3(5),89(4),1919(3),1962(3),3(4),3(3),1901(4),74(4)]),flip(a)]. 2036 a6 = a4. [back_rewrite(1001),rewrite([1919(3),1962(3),3(4),3(3)]),flip(a)]. 2043 a5 * a4 = a4. [back_rewrite(89),rewrite([1919(5),1962(5),3(6)])]. 2072 a5 = a4. [back_rewrite(751),rewrite([1919(1),1962(1),1919(4),1962(4),74(5),2023(3),2043(4),3(3)]),flip(a)]. 2083 a1 = a4. [back_rewrite(16),rewrite([2023(1),3(3)]),flip(a)]. 2111 a2 = a4. [back_rewrite(37),rewrite([1986(1),2021(2),3(3)]),flip(a)]. 2112 \$F. [back_rewrite(2022),rewrite([2111(1),2083(2),2111(4),2072(7),2072(10),2036(11),2036(13),2023(16)]),xx(a),xx(b),xx(c),xx(d),xx(e),xx(f)]. ============================== end of proof ========================== % Disable descendants (x means already disabled): 17x 18x 2022x given #78 (T,wt=3): 1962 a10 = a4. [back_rewrite(1356),rewrite([1894(1),1919(1),1938(4),3(3),1894(3),1919(3),1941(4),1017(4),1901(4),3(4)])]. given #79 (T,wt=3): 1986 a3 = a4. [back_rewrite(760),rewrite([1894(1),1919(1),1962(1),41(3),1910(7),1919(4),1962(4),74(5),1900(4),1919(3),1962(3),1017(4),1901(4),3(4)])]. given #80 (T,wt=3): 2021 a7 = a4. [back_rewrite(58),rewrite([1894(1),1919(1),1962(1),1986(2),3(3)]),flip(a)]. given #81 (T,wt=3): 2023 a11 = a4. [back_rewrite(1613),rewrite([1962(1),1900(3),1919(2),1962(2),3(3),1901(5),3(5),89(4),1919(3),1962(3),3(4),3(3),1901(4),74(4)]),flip(a)]. given #82 (A,wt=15): 78 (x * y) * (y * (x * y)) = x * (x * y). [para(4(a,1),21(a,1,1)),flip(a)]. given #83 (T,wt=3): 2036 a6 = a4. [back_rewrite(1001),rewrite([1919(3),1962(3),3(4),3(3)]),flip(a)]. given #84 (T,wt=3): 2072 a5 = a4. [back_rewrite(751),rewrite([1919(1),1962(1),1919(4),1962(4),74(5),2023(3),2043(4),3(3)]),flip(a)]. given #85 (T,wt=3): 2083 a1 = a4. [back_rewrite(16),rewrite([2023(1),3(3)]),flip(a)]. given #86 (T,wt=3): 2084 a8 = a4. [back_rewrite(1894),rewrite([1919(2),1962(2)])]. given #87 (A,wt=17): 79 ((x * y) * z) * x = (x * (y * x)) * (z * x). [para(21(a,1),5(a,1,1)),flip(a)]. given #88 (T,wt=3): 2094 a9 = a4. [back_rewrite(1919),rewrite([1962(2)])]. given #89 (T,wt=3): 2111 a2 = a4. [back_rewrite(37),rewrite([1986(1),2021(2),3(3)]),flip(a)]. given #90 (T,wt=13): 1062 (x * a4) * y = (x * y) * (a4 * y). [para(8(a,1),31(a,1,1,2)),rewrite([44(9)])]. given #91 (T,wt=17): 80 (x * (y * z)) * y = (x * y) * (y * (z * y)). [para(21(a,1),5(a,1,2)),flip(a)]. given #92 (A,wt=17): 81 ((x * y) * z) * (x * z) = (x * (y * x)) * z. [para(21(a,1),5(a,2,1))]. given #93 (T,wt=17): 84 x * ((y * z) * x) = x * ((y * x) * (z * x)). [para(5(a,2),21(a,2,2)),rewrite([21(3)])]. given #94 (T,wt=17): 119 ((x * y) * z) * (z * (y * z)) = x * (y * z). [para(5(a,1),22(a,1,1))]. given #95 (T,wt=17): 134 (x * y) * (y * (z * y)) = (x * z) * (z * y). [para(22(a,1),22(a,1,1))]. given #96 (T,wt=15): 2648 (x * y) * (y * x) = x * (x * (y * x)). [para(3(a,1),134(a,1,1)),flip(a)]. given #97 (A,wt=21): 83 ((x * y) * (z * y)) * (x * z) = (x * z) * (y * (x * z)). [para(5(a,2),21(a,1,1))]. given #98 (T,wt=17): 153 x * ((y * z) * (u * z)) = x * ((y * u) * z). [para(5(a,1),24(a,2,2)),rewrite([24(6)])]. given #99 (T,wt=17): 179 ((x * y) * (z * y)) * u = ((x * z) * y) * u. [para(5(a,1),25(a,2,1)),rewrite([25(6)])]. given #100 (T,wt=17): 181 ((x * y) * z) * (z * y) = x * (y * (z * y)). [para(25(a,1),24(a,1,1))]. given #101 (T,wt=17): 264 (x * (y * z)) * u = (x * u) * ((y * z) * u). [para(26(a,1),24(a,1,1)),rewrite([25(5),24(3),25(7)])]. given #102 (A,wt=21): 116 (((x * y) * z) * u) * (y * z) = (x * z) * (u * (y * z)). [para(22(a,1),5(a,1,1)),flip(a)]. given #103 (T,wt=17): 2179 (x * y) * (x * (x * y)) = x * (y * (x * y)). [para(78(a,1),78(a,1,1)),rewrite([78(8),700(7),2122(6),78(8)]),flip(a)]. given #104 (T,wt=17): 2181 (x * y) * (x * (y * x)) = x * (y * (y * x)). [back_rewrite(2121),rewrite([2179(6),78(4)]),flip(a)]. given #105 (T,wt=17): 2258 x * ((y * a4) * z) = x * ((y * z) * (a4 * z)). [para(1062(a,1),24(a,2,2)),rewrite([24(5)])]. given #106 (T,wt=17): 2259 ((x * a4) * y) * z = ((x * y) * (a4 * y)) * z. [para(1062(a,1),25(a,2,1)),rewrite([25(5)])]. given #107 (A,wt=21): 117 (x * ((y * z) * u)) * (z * u) = (x * (z * u)) * (y * u). [para(22(a,1),5(a,1,2)),flip(a)]. given #108 (T,wt=17): 3099 (x * ((y * z) * u)) * ((y * u) * (z * u)) = x. [para(153(a,1),4(a,1,1))]. given #109 (T,wt=17): 3100 (x * ((y * z) * (u * z))) * ((y * u) * z) = x. [para(153(a,1),4(a,1))]. given #110 (T,wt=19): 118 (((x * y) * z) * u) * ((y * z) * u) = (x * z) * u. [para(22(a,1),5(a,2,1))]. given #111 (T,wt=19): 122 ((x * (y * z)) * u) * ((y * u) * (z * u)) = x * u. [para(5(a,2),22(a,1,2))]. given #112 (A,wt=21): 120 ((x * (y * z)) * (u * z)) * ((y * u) * z) = x * (u * z). [para(5(a,1),22(a,1,2))]. given #113 (T,wt=19): 149 (((x * y) * z) * u) * y = (x * (z * y)) * (u * y). [para(24(a,1),5(a,1,1)),flip(a)]. given #114 (T,wt=19): 150 (x * ((y * z) * u)) * z = (x * z) * (y * (u * z)). [para(24(a,1),5(a,1,2)),flip(a)]. given #115 (T,wt=19): 152 (((x * y) * z) * u) * (y * u) = (x * (z * y)) * u. [para(24(a,1),5(a,2,1))]. given #116 (T,wt=19): 161 ((x * (y * z)) * u) * (z * u) = ((x * z) * y) * u. [para(24(a,1),22(a,1,1,1))]. given #117 (A,wt=25): 133 ((x * y) * z) * ((y * z) * ((x * y) * z)) = (x * z) * ((x * y) * z). [para(22(a,1),21(a,1,1)),flip(a)]. given #118 (T,wt=19): 163 ((x * (y * z)) * u) * z = ((x * z) * y) * (u * z). [para(24(a,1),24(a,1,1,1))]. given #119 (T,wt=19): 178 (x * (y * (z * u))) * u = (x * u) * ((y * u) * z). [para(25(a,1),5(a,1,2)),flip(a)]. given #120 (T,wt=19): 318 (x * (y * (y * z))) * (z * (y * z)) = (x * z) * y. [para(3(a,1),27(a,1,2)),rewrite([25(5),25(3)]),flip(a)]. given #121 (T,wt=19): 693 (x * (y * (z * y))) * (z * (z * y)) = (x * z) * y. [para(29(a,1),5(a,2)),rewrite([78(7)])]. given #122 (A,wt=25): 160 ((x * y) * z) * (y * ((x * y) * z)) = (x * (z * y)) * ((x * y) * z). [para(24(a,1),21(a,1,1)),flip(a)]. given #123 (T,wt=19): 704 ((x * y) * z) * (y * (y * z)) = x * (z * (y * z)). [para(29(a,1),22(a,1,1)),rewrite([78(6)])]. given #124 (T,wt=19): 2123 ((x * y) * z) * (y * (z * y)) = x * (z * (z * y)). [para(78(a,1),24(a,2,2)),rewrite([25(5),25(3)])]. given #125 (T,wt=17): 6442 (x * a4) * (a4 * y) = (x * y) * (y * (a4 * y)). [para(1062(a,2),2123(a,2)),rewrite([25(4),4(5)]),flip(a)]. given #126 (T,wt=19): 2254 ((x * a4) * y) * z = ((x * z) * (a4 * z)) * (y * z). [para(1062(a,1),5(a,1,1)),flip(a)]. given #127 (A,wt=25): 180 ((x * y) * z) * (x * (z * y)) = (x * (z * y)) * (y * (x * (z * y))). [para(25(a,1),21(a,1,1))]. given #128 (T,wt=19): 2255 ((x * a4) * y) * (z * y) = ((x * z) * (a4 * z)) * y. [para(1062(a,1),5(a,2,1))]. given #129 (T,wt=19): 2256 ((x * a4) * y) * z = ((x * y) * z) * ((a4 * y) * z). [para(1062(a,2),5(a,2,1)),flip(a)]. given #130 (T,wt=19): 2576 (x * y) * (z * (z * y)) = (x * z) * (y * (z * y)). [para(22(a,1),119(a,1,1)),rewrite([78(5)])]. given #131 (T,wt=19): 2881 (x * (y * z)) * (z * y) = (x * z) * (y * (z * y)). [para(2648(a,1),5(a,1,2)),rewrite([2573(6)]),flip(a)]. given #132 (A,wt=21): 201 ((x * y) * z) * ((x * z) * (y * z)) = (x * z) * (y * z). [para(3(a,1),26(a,2,1))]. given #133 (T,wt=19): 3744 (x * y) * (y * (y * (x * y))) = x * (x * (x * y)). [para(2179(a,1),21(a,2,2)),rewrite([4(4),3720(9)]),flip(a)]. given #134 (T,wt=19): 6626 (x * a4) * (y * (a4 * y)) = (x * y) * (a4 * (a4 * y)). [para(6442(a,1),116(a,1)),rewrite([4(4)])]. given #135 (T,wt=19): 7358 (x * y) * (y * (y * x)) = x * (x * (x * (y * x))). [para(2576(a,2),21(a,1)),rewrite([21(3),4(2),3720(10),3(5)])]. given #136 (T,wt=21): 244 ((x * y) * z) * (x * (y * z)) = (x * (z * x)) * (y * z). [para(21(a,1),26(a,2,1))].