============================== Prover9 =============================== Prover9 (64) version 2017-05A, May 2017. Process 17987 was started by veroff on theorem, Wed Jun 14 05:43:56 2017 The command was "prover9 -f p9header axioms.in Case1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file p9header clear(ordered_res). set(para_from_small). % Reading from file axioms.in formulas(assumptions). (x * y) * z = x * (y * z). x * y = x * z -> y = z. x * y = z * y -> x = z. x * y != x. x * y != y. x * y = u * v -> x = u | (exists w1 x * w1 = u) | (exists w2 w2 * y = v) # label("EQD"). Power(x,x). Power(x,y) & Power(y,z) -> Power(x,z). Power(y,x) & Power(z,x) -> Power(y * z,x). Power(y,x) & Power(z,x) -> y = z | (exists u (Power(u,x) & (y = z * u & y = u * z | z = y * u & z = u * y))). Power(y * z,x) -> Power(y,x) & Power(z,x) | (exists u exists v (u * v = x & (y = u | (exists y1 (y = y1 * u & Power(y1,x)))) & (z = v | (exists z1 (z = v * z1 & Power(z1,x)))))). Power(y,x) & Power(u * (y * v),x) -> (exists z (Power(y,z) & Power(u,z) & Power(v,z))). -Shorter(x,x). Shorter(x,y) -> -Shorter(y,x). Shorter(x,y) & Shorter(y,z) -> Shorter(x,z). Shorter(x,x * y). Shorter(x,y * x). Shorter(x,y) <-> Shorter(x * z,y * z). Shorter(x,y) <-> Shorter(z * x,z * y). Shorter(x,y) <-> Shorter(x * z,z * y). Shorter(x,y) <-> Shorter(z * x,y * z). Prefix(x,y) <-> (exists z x * z = y). Suffix(x,y) <-> (exists z z * x = y). Period(x,y) <-> (exists z (Power(z,x) & Prefix(y,z))). end_of_list. % Reading from file Case1.in formulas(goals). Power(u * u1,x) & Power(u * u2,y) & u = x * u3 & u = y * u4 & -Shorter(u,x * y) & u = x * y -> x * y = y * x # label("Case 1"). end_of_list. formulas(assumptions). x * y = u * v -> Prefix(x,u) | Prefix(u,x) | x = u # label("Lemma 1"). Prefix(x,y) -> Shorter(x,y) # label("Lemma 2"). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x * y = x * z -> y = z # label(non_clause). [assumption]. 2 x * y = z * y -> x = z # label(non_clause). [assumption]. 3 x * y = u * v -> x = u | (exists w1 x * w1 = u) | (exists w2 w2 * y = v) # label("EQD") # label(non_clause). [assumption]. 4 Power(x,y) & Power(y,z) -> Power(x,z) # label(non_clause). [assumption]. 5 Power(y,x) & Power(z,x) -> Power(y * z,x) # label(non_clause). [assumption]. 6 Power(y,x) & Power(z,x) -> y = z | (exists u (Power(u,x) & (y = z * u & y = u * z | z = y * u & z = u * y))) # label(non_clause). [assumption]. 7 Power(y * z,x) -> Power(y,x) & Power(z,x) | (exists u exists v (u * v = x & (y = u | (exists y1 (y = y1 * u & Power(y1,x)))) & (z = v | (exists z1 (z = v * z1 & Power(z1,x)))))) # label(non_clause). [assumption]. 8 Power(y,x) & Power(u * (y * v),x) -> (exists z (Power(y,z) & Power(u,z) & Power(v,z))) # label(non_clause). [assumption]. 9 Shorter(x,y) -> -Shorter(y,x) # label(non_clause). [assumption]. 10 Shorter(x,y) & Shorter(y,z) -> Shorter(x,z) # label(non_clause). [assumption]. 11 Shorter(x,y) <-> Shorter(x * z,y * z) # label(non_clause). [assumption]. 12 Shorter(x,y) <-> Shorter(z * x,z * y) # label(non_clause). [assumption]. 13 Shorter(x,y) <-> Shorter(x * z,z * y) # label(non_clause). [assumption]. 14 Shorter(x,y) <-> Shorter(z * x,y * z) # label(non_clause). [assumption]. 15 Prefix(x,y) <-> (exists z x * z = y) # label(non_clause). [assumption]. 16 Suffix(x,y) <-> (exists z z * x = y) # label(non_clause). [assumption]. 17 Period(x,y) <-> (exists z (Power(z,x) & Prefix(y,z))) # label(non_clause). [assumption]. 18 x * y = u * v -> Prefix(x,u) | Prefix(u,x) | x = u # label("Lemma 1") # label(non_clause). [assumption]. 19 Prefix(x,y) -> Shorter(x,y) # label("Lemma 2") # label(non_clause). [assumption]. 20 Power(u * u1,x) & Power(u * u2,y) & u = x * u3 & u = y * u4 & -Shorter(u,x * y) & u = x * y -> x * y = y * x # label("Case 1") # 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 * y) * z = x * (y * z). [assumption]. x * y != x * z | y = z. [clausify(1)]. x * y != z * y | x = z. [clausify(2)]. x * y != x. [assumption]. x * y != y. [assumption]. x * y != z * u | x = z | z * f1(z,x,u,y) = x | f2(z,x,u,y) * u = y # label("EQD"). [clausify(3)]. Power(x,x). [assumption]. -Power(x,y) | -Power(y,z) | Power(x,z). [clausify(4)]. -Power(x,y) | -Power(z,y) | Power(x * z,y). [clausify(5)]. -Power(x,y) | -Power(z,y) | z = x | Power(f3(y,x,z),y). [clausify(6)]. -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | x * f3(y,x,z) = z. [clausify(6)]. -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | f3(y,x,z) * x = z. [clausify(6)]. -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | x * f3(y,x,z) = z. [clausify(6)]. -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | f3(y,x,z) * x = z. [clausify(6)]. -Power(x * y,z) | Power(x,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. -Power(x * y,z) | Power(y,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. -Power(x,y) | -Power(z * (x * u),y) | Power(x,f8(y,x,z,u)). [clausify(8)]. -Power(x,y) | -Power(z * (x * u),y) | Power(z,f8(y,x,z,u)). [clausify(8)]. -Power(x,y) | -Power(z * (x * u),y) | Power(u,f8(y,x,z,u)). [clausify(8)]. -Shorter(x,x). [assumption]. -Shorter(x,y) | -Shorter(y,x). [clausify(9)]. -Shorter(x,y) | -Shorter(y,z) | Shorter(x,z). [clausify(10)]. Shorter(x,x * y). [assumption]. Shorter(x,y * x). [assumption]. -Shorter(x,y) | Shorter(x * z,y * z). [clausify(11)]. Shorter(x,y) | -Shorter(x * z,y * z). [clausify(11)]. -Shorter(x,y) | Shorter(z * x,z * y). [clausify(12)]. Shorter(x,y) | -Shorter(z * x,z * y). [clausify(12)]. -Shorter(x,y) | Shorter(x * z,z * y). [clausify(13)]. Shorter(x,y) | -Shorter(x * z,z * y). [clausify(13)]. -Shorter(x,y) | Shorter(z * x,y * z). [clausify(14)]. Shorter(x,y) | -Shorter(z * x,y * z). [clausify(14)]. -Prefix(x,y) | x * f9(x,y) = y. [clausify(15)]. Prefix(x,y) | x * z != y. [clausify(15)]. -Suffix(x,y) | f10(x,y) * x = y. [clausify(16)]. Suffix(x,y) | z * x != y. [clausify(16)]. -Period(x,y) | Power(f11(x,y),x). [clausify(17)]. -Period(x,y) | Prefix(y,f11(x,y)). [clausify(17)]. Period(x,y) | -Power(z,x) | -Prefix(y,z). [clausify(17)]. x * y != z * u | Prefix(z,x) | Prefix(x,z) | x = z # label("Lemma 1"). [clausify(18)]. -Prefix(x,y) | Shorter(x,y) # label("Lemma 2"). [clausify(19)]. Power(c1 * c2,c3) # label("Case 1"). [deny(20)]. Power(c1 * c4,c5) # label("Case 1"). [deny(20)]. c3 * c6 = c1 # label("Case 1"). [deny(20)]. c5 * c7 = c1 # label("Case 1"). [deny(20)]. -Shorter(c1,c3 * c5) # label("Case 1"). [deny(20)]. c3 * c5 = c1 # label("Case 1"). [deny(20)]. c5 * c3 != c3 * c5 # label("Case 1"). [deny(20)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating Suffix/2 21 Suffix(x,y) | z * x != y. [clausify(16)]. 22 -Suffix(x,y) | f10(x,y) * x = y. [clausify(16)]. Derived: x * y != z | f10(y,z) * y = z. [resolve(21,a,22,a)]. Eliminating Period/2 23 Period(x,y) | -Power(z,x) | -Prefix(y,z). [clausify(17)]. 24 -Period(x,y) | Power(f11(x,y),x). [clausify(17)]. 25 -Period(x,y) | Prefix(y,f11(x,y)). [clausify(17)]. Derived: -Power(x,y) | -Prefix(z,x) | Power(f11(y,z),y). [resolve(23,a,24,a)]. Derived: -Power(x,y) | -Prefix(z,x) | Prefix(z,f11(y,z)). [resolve(23,a,25,a)]. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, Power, Shorter, Prefix ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, c7, *, f9, f10, f11, f3, f4, f5, f6, f7, f1, f2, f8 ]). After inverse_order: (no changes). Unfolding symbols: c1/0. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (non-Horn, less than 100 clauses) Auto_process settings: % set(factor). % (non-Horn) % set(unit_deletion). % (non-Horn) kept: 26 (x * y) * z = x * (y * z). [assumption]. kept: 27 x * y != x * z | y = z. [clausify(1)]. kept: 28 x * y != z * y | x = z. [clausify(2)]. kept: 29 x * y != x. [assumption]. kept: 30 x * y != y. [assumption]. kept: 31 x * y != z * u | x = z | z * f1(z,x,u,y) = x | f2(z,x,u,y) * u = y # label("EQD"). [clausify(3)]. kept: 32 Power(x,x). [assumption]. kept: 33 -Power(x,y) | -Power(y,z) | Power(x,z). [clausify(4)]. kept: 34 -Power(x,y) | -Power(z,y) | Power(x * z,y). [clausify(5)]. kept: 35 -Power(x,y) | -Power(z,y) | z = x | Power(f3(y,x,z),y). [clausify(6)]. kept: 36 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | x * f3(y,x,z) = z. [clausify(6)]. kept: 37 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | f3(y,x,z) * x = z. [clausify(6)]. kept: 38 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | x * f3(y,x,z) = z. [clausify(6)]. kept: 39 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | f3(y,x,z) * x = z. [clausify(6)]. kept: 40 -Power(x * y,z) | Power(x,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. kept: 41 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. kept: 42 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. kept: 43 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. kept: 44 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. kept: 45 -Power(x * y,z) | Power(y,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. kept: 46 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. kept: 47 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. kept: 48 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. kept: 49 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. kept: 50 -Power(x,y) | -Power(z * (x * u),y) | Power(x,f8(y,x,z,u)). [clausify(8)]. kept: 51 -Power(x,y) | -Power(z * (x * u),y) | Power(z,f8(y,x,z,u)). [clausify(8)]. kept: 52 -Power(x,y) | -Power(z * (x * u),y) | Power(u,f8(y,x,z,u)). [clausify(8)]. kept: 53 -Shorter(x,x). [assumption]. kept: 54 -Shorter(x,y) | -Shorter(y,x). [clausify(9)]. kept: 55 -Shorter(x,y) | -Shorter(y,z) | Shorter(x,z). [clausify(10)]. kept: 56 Shorter(x,x * y). [assumption]. kept: 57 Shorter(x,y * x). [assumption]. kept: 58 -Shorter(x,y) | Shorter(x * z,y * z). [clausify(11)]. kept: 59 Shorter(x,y) | -Shorter(x * z,y * z). [clausify(11)]. kept: 60 -Shorter(x,y) | Shorter(z * x,z * y). [clausify(12)]. kept: 61 Shorter(x,y) | -Shorter(z * x,z * y). [clausify(12)]. kept: 62 -Shorter(x,y) | Shorter(x * z,z * y). [clausify(13)]. kept: 63 Shorter(x,y) | -Shorter(x * z,z * y). [clausify(13)]. kept: 64 -Shorter(x,y) | Shorter(z * x,y * z). [clausify(14)]. kept: 65 Shorter(x,y) | -Shorter(z * x,y * z). [clausify(14)]. kept: 66 -Prefix(x,y) | x * f9(x,y) = y. [clausify(15)]. kept: 67 Prefix(x,y) | x * z != y. [clausify(15)]. kept: 68 x * y != z * u | Prefix(z,x) | Prefix(x,z) | x = z # label("Lemma 1"). [clausify(18)]. kept: 69 -Prefix(x,y) | Shorter(x,y) # label("Lemma 2"). [clausify(19)]. kept: 70 Power(c1 * c2,c3) # label("Case 1"). [deny(20)]. kept: 71 Power(c1 * c4,c5) # label("Case 1"). [deny(20)]. 72 c3 * c6 = c1 # label("Case 1"). [deny(20)]. kept: 73 c1 = c3 * c6. [copy(72),flip(a)]. 74 c5 * c7 = c1 # label("Case 1"). [deny(20)]. kept: 75 c5 * c7 = c3 * c6. [copy(74),rewrite([73(4)])]. 76 -Shorter(c1,c3 * c5) # label("Case 1"). [deny(20)]. kept: 77 -Shorter(c3 * c6,c3 * c5). [copy(76),rewrite([73(1)])]. 78 c3 * c5 = c1 # label("Case 1"). [deny(20)]. kept: 79 c3 * c6 = c3 * c5. [copy(78),rewrite([73(4)]),flip(a)]. kept: 80 c5 * c3 != c3 * c5 # label("Case 1"). [deny(20)]. kept: 81 x * y != z | f10(y,z) * y = z. [resolve(21,a,22,a)]. kept: 82 -Power(x,y) | -Prefix(z,x) | Power(f11(y,z),y). [resolve(23,a,24,a)]. kept: 83 -Power(x,y) | -Prefix(z,x) | Prefix(z,f11(y,z)). [resolve(23,a,25,a)]. kept: 84 -Power(x,y) | Power(x * x,y). [factor(34,a,b)]. kept: 85 Power(c3 * (c5 * c4),c5). [back_rewrite(71),rewrite([73(1),79(3),26(5)])]. kept: 86 Power(c3 * (c5 * c2),c3). [back_rewrite(70),rewrite([73(1),79(3),26(5)])]. kept: 87 c5 * c7 = c3 * c5. [back_rewrite(75),rewrite([79(6)])]. kept: 88 c1 = c3 * c5. [back_rewrite(73),rewrite([79(4)])]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 26 (x * y) * z = x * (y * z). [assumption]. 27 x * y != x * z | y = z. [clausify(1)]. 28 x * y != z * y | x = z. [clausify(2)]. 29 x * y != x. [assumption]. 30 x * y != y. [assumption]. 31 x * y != z * u | x = z | z * f1(z,x,u,y) = x | f2(z,x,u,y) * u = y # label("EQD"). [clausify(3)]. 32 Power(x,x). [assumption]. 33 -Power(x,y) | -Power(y,z) | Power(x,z). [clausify(4)]. 34 -Power(x,y) | -Power(z,y) | Power(x * z,y). [clausify(5)]. 35 -Power(x,y) | -Power(z,y) | z = x | Power(f3(y,x,z),y). [clausify(6)]. 36 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | x * f3(y,x,z) = z. [clausify(6)]. 37 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | f3(y,x,z) * x = z. [clausify(6)]. 38 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | x * f3(y,x,z) = z. [clausify(6)]. 39 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | f3(y,x,z) * x = z. [clausify(6)]. 40 -Power(x * y,z) | Power(x,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. 41 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. 42 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. 43 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. 44 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. 45 -Power(x * y,z) | Power(y,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. 46 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. 47 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. 48 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. 49 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. 50 -Power(x,y) | -Power(z * (x * u),y) | Power(x,f8(y,x,z,u)). [clausify(8)]. 51 -Power(x,y) | -Power(z * (x * u),y) | Power(z,f8(y,x,z,u)). [clausify(8)]. 52 -Power(x,y) | -Power(z * (x * u),y) | Power(u,f8(y,x,z,u)). [clausify(8)]. 53 -Shorter(x,x). [assumption]. 54 -Shorter(x,y) | -Shorter(y,x). [clausify(9)]. 55 -Shorter(x,y) | -Shorter(y,z) | Shorter(x,z). [clausify(10)]. 56 Shorter(x,x * y). [assumption]. 57 Shorter(x,y * x). [assumption]. 58 -Shorter(x,y) | Shorter(x * z,y * z). [clausify(11)]. 59 Shorter(x,y) | -Shorter(x * z,y * z). [clausify(11)]. 60 -Shorter(x,y) | Shorter(z * x,z * y). [clausify(12)]. 61 Shorter(x,y) | -Shorter(z * x,z * y). [clausify(12)]. 62 -Shorter(x,y) | Shorter(x * z,z * y). [clausify(13)]. 63 Shorter(x,y) | -Shorter(x * z,z * y). [clausify(13)]. 64 -Shorter(x,y) | Shorter(z * x,y * z). [clausify(14)]. 65 Shorter(x,y) | -Shorter(z * x,y * z). [clausify(14)]. 66 -Prefix(x,y) | x * f9(x,y) = y. [clausify(15)]. 67 Prefix(x,y) | x * z != y. [clausify(15)]. 68 x * y != z * u | Prefix(z,x) | Prefix(x,z) | x = z # label("Lemma 1"). [clausify(18)]. 69 -Prefix(x,y) | Shorter(x,y) # label("Lemma 2"). [clausify(19)]. 79 c3 * c6 = c3 * c5. [copy(78),rewrite([73(4)]),flip(a)]. 80 c5 * c3 != c3 * c5 # label("Case 1"). [deny(20)]. 81 x * y != z | f10(y,z) * y = z. [resolve(21,a,22,a)]. 82 -Power(x,y) | -Prefix(z,x) | Power(f11(y,z),y). [resolve(23,a,24,a)]. 83 -Power(x,y) | -Prefix(z,x) | Prefix(z,f11(y,z)). [resolve(23,a,25,a)]. 84 -Power(x,y) | Power(x * x,y). [factor(34,a,b)]. 85 Power(c3 * (c5 * c4),c5). [back_rewrite(71),rewrite([73(1),79(3),26(5)])]. 86 Power(c3 * (c5 * c2),c3). [back_rewrite(70),rewrite([73(1),79(3),26(5)])]. 87 c5 * c7 = c3 * c5. [back_rewrite(75),rewrite([79(6)])]. 88 c1 = c3 * c5. [back_rewrite(73),rewrite([79(4)])]. end_of_list. formulas(demodulators). 26 (x * y) * z = x * (y * z). [assumption]. 79 c3 * c6 = c3 * c5. [copy(78),rewrite([73(4)]),flip(a)]. 87 c5 * c7 = c3 * c5. [back_rewrite(75),rewrite([79(6)])]. 88 c1 = c3 * c5. [back_rewrite(73),rewrite([79(4)])]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 26 (x * y) * z = x * (y * z). [assumption]. given #2 (I,wt=10): 27 x * y != x * z | y = z. [clausify(1)]. given #3 (I,wt=10): 28 x * y != z * y | x = z. [clausify(2)]. given #4 (I,wt=5): 29 x * y != x. [assumption]. given #5 (I,wt=5): 30 x * y != y. [assumption]. given #6 (I,wt=28): 31 x * y != z * u | x = z | z * f1(z,x,u,y) = x | f2(z,x,u,y) * u = y # label("EQD"). [clausify(3)]. given #7 (I,wt=3): 32 Power(x,x). [assumption]. given #8 (I,wt=9): 33 -Power(x,y) | -Power(y,z) | Power(x,z). [clausify(4)]. given #9 (I,wt=11): 34 -Power(x,y) | -Power(z,y) | Power(x * z,y). [clausify(5)]. given #10 (I,wt=15): 35 -Power(x,y) | -Power(z,y) | z = x | Power(f3(y,x,z),y). [clausify(6)]. given #11 (I,wt=25): 36 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | x * f3(y,x,z) = z. [clausify(6)]. given #12 (I,wt=25): 37 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | f3(y,x,z) * x = z. [clausify(6)]. given #13 (I,wt=25): 38 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | x * f3(y,x,z) = z. [clausify(6)]. given #14 (I,wt=25): 39 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | f3(y,x,z) * x = z. [clausify(6)]. given #15 (I,wt=19): 40 -Power(x * y,z) | Power(x,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. given #16 (I,wt=25): 41 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. given #17 (I,wt=20): 42 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. given #18 (I,wt=25): 43 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. given #19 (I,wt=20): 44 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. given #20 (I,wt=19): 45 -Power(x * y,z) | Power(y,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. given #21 (I,wt=25): 46 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. given #22 (I,wt=20): 47 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. given #23 (I,wt=25): 48 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. given #24 (I,wt=20): 49 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. given #25 (I,wt=17): 50 -Power(x,y) | -Power(z * (x * u),y) | Power(x,f8(y,x,z,u)). [clausify(8)]. given #26 (I,wt=17): 51 -Power(x,y) | -Power(z * (x * u),y) | Power(z,f8(y,x,z,u)). [clausify(8)]. given #27 (I,wt=17): 52 -Power(x,y) | -Power(z * (x * u),y) | Power(u,f8(y,x,z,u)). [clausify(8)]. given #28 (I,wt=3): 53 -Shorter(x,x). [assumption]. given #29 (I,wt=6): 54 -Shorter(x,y) | -Shorter(y,x). [clausify(9)]. given #30 (I,wt=9): 55 -Shorter(x,y) | -Shorter(y,z) | Shorter(x,z). [clausify(10)]. given #31 (I,wt=5): 56 Shorter(x,x * y). [assumption]. given #32 (I,wt=5): 57 Shorter(x,y * x). [assumption]. given #33 (I,wt=10): 58 -Shorter(x,y) | Shorter(x * z,y * z). [clausify(11)]. given #34 (I,wt=10): 59 Shorter(x,y) | -Shorter(x * z,y * z). [clausify(11)]. given #35 (I,wt=10): 60 -Shorter(x,y) | Shorter(z * x,z * y). [clausify(12)]. given #36 (I,wt=10): 61 Shorter(x,y) | -Shorter(z * x,z * y). [clausify(12)]. given #37 (I,wt=10): 62 -Shorter(x,y) | Shorter(x * z,z * y). [clausify(13)]. given #38 (I,wt=10): 63 Shorter(x,y) | -Shorter(x * z,z * y). [clausify(13)]. given #39 (I,wt=10): 64 -Shorter(x,y) | Shorter(z * x,y * z). [clausify(14)]. given #40 (I,wt=10): 65 Shorter(x,y) | -Shorter(z * x,y * z). [clausify(14)]. given #41 (I,wt=10): 66 -Prefix(x,y) | x * f9(x,y) = y. [clausify(15)]. given #42 (I,wt=8): 67 Prefix(x,y) | x * z != y. [clausify(15)]. given #43 (I,wt=16): 68 x * y != z * u | Prefix(z,x) | Prefix(x,z) | x = z # label("Lemma 1"). [clausify(18)]. given #44 (I,wt=6): 69 -Prefix(x,y) | Shorter(x,y) # label("Lemma 2"). [clausify(19)]. given #45 (I,wt=7): 79 c3 * c6 = c3 * c5. [copy(78),rewrite([73(4)]),flip(a)]. given #46 (I,wt=7): 80 c5 * c3 != c3 * c5 # label("Case 1"). [deny(20)]. given #47 (I,wt=12): 81 x * y != z | f10(y,z) * y = z. [resolve(21,a,22,a)]. given #48 (I,wt=11): 82 -Power(x,y) | -Prefix(z,x) | Power(f11(y,z),y). [resolve(23,a,24,a)]. given #49 (I,wt=11): 83 -Power(x,y) | -Prefix(z,x) | Prefix(z,f11(y,z)). [resolve(23,a,25,a)]. given #50 (I,wt=8): 84 -Power(x,y) | Power(x * x,y). [factor(34,a,b)]. given #51 (I,wt=7): 85 Power(c3 * (c5 * c4),c5). [back_rewrite(71),rewrite([73(1),79(3),26(5)])]. given #52 (I,wt=7): 86 Power(c3 * (c5 * c2),c3). [back_rewrite(70),rewrite([73(1),79(3),26(5)])]. given #53 (I,wt=7): 87 c5 * c7 = c3 * c5. [back_rewrite(75),rewrite([79(6)])]. given #54 (I,wt=5): 88 c1 = c3 * c5. [back_rewrite(73),rewrite([79(4)])]. given #55 (A,wt=14): 89 x * (y * z) != x * (y * u) | z = u. [para(26(a,1),27(a,1)),rewrite([26(4)])]. given #56 (F,wt=3): 160 -Prefix(x,x). [ur(66,b,29,a)]. given #57 (F,wt=5): 142 -Shorter(x * y,x). [resolve(56,a,54,b)]. given #58 (F,wt=5): 146 -Shorter(x * y,y). [resolve(57,a,54,b)]. given #59 (F,wt=5): 235 c3 * c5 != c7. [para(87(a,1),30(a,1))]. given #60 (T,wt=3): 167 c6 = c5. [resolve(79,a,27,a)]. given #61 (T,wt=5): 163 Prefix(x,x * y). [xx_res(67,b)]. given #62 (T,wt=5): 175 Power(x * x,x). [resolve(84,a,32,a)]. given #63 (T,wt=5): 229 Prefix(c5,c3 * c5). [resolve(87,a,67,b)]. given #64 (A,wt=14): 90 x * (y * z) != u * z | x * y = u. [para(26(a,1),28(a,1))]. given #65 (F,wt=5): 268 -Prefix(x * y,x). [ur(69,b,142,a)]. given #66 (F,wt=5): 274 -Prefix(x * y,y). [ur(69,b,146,a)]. given #67 (F,wt=5): 277 -Shorter(c3 * c5,c7). [para(87(a,1),146(a,1))]. given #68 (F,wt=5): 313 -Prefix(c3 * c5,c7). [para(87(a,1),274(a,1))]. given #69 (T,wt=5): 251 Shorter(c7,c3 * c5). [para(87(a,1),57(a,2))]. given #70 (T,wt=7): 147 Shorter(x,y * (z * x)). [para(26(a,1),57(a,2))]. given #71 (T,wt=7): 177 Power(c4,f8(c5,c5,c3,c4)). [resolve(85,a,52,b),unit_del(a,32)]. given #72 (T,wt=7): 178 Power(c3,f8(c5,c5,c3,c4)). [resolve(85,a,51,b),unit_del(a,32)]. given #73 (A,wt=9): 91 x * (y * z) != x * z. [ur(28,b,29,a),rewrite([26(2)])]. given #74 (F,wt=7): 93 x * (y * z) != z. [para(26(a,1),30(a,1))]. given #75 (F,wt=7): 154 -Shorter(x * y,y * x). [ur(63,a,53,a)]. given #76 (F,wt=5): 378 -Shorter(c5 * c3,c7). [ur(55,b,251,a,c,154,a)]. given #77 (F,wt=5): 384 -Prefix(c5 * c3,c7). [ur(69,b,378,a)]. given #78 (T,wt=7): 179 Power(c5,f8(c5,c5,c3,c4)). [resolve(85,a,50,b),unit_del(a,32)]. given #79 (T,wt=7): 328 Shorter(x,y * (x * z)). [resolve(147,a,63,b)]. given #80 (T,wt=7): 337 Shorter(c7,x * (c3 * c5)). [para(87(a,1),147(a,2,2))]. given #81 (T,wt=8): 99 -Power(x,y) | Power(y * x,y). [resolve(34,a,32,a)]. given #82 (A,wt=9): 92 x * (y * z) != x * y. [ur(27,b,29,a)]. given #83 (F,wt=7): 273 -Shorter(x * (y * z),y). [ur(55,b,57,a,c,142,a),rewrite([26(2)])]. given #84 (F,wt=7): 276 -Shorter(x * (y * z),z). [ur(55,b,57,a,c,146,a)]. given #85 (F,wt=7): 311 x * (y * z) != y. [ur(67,a,274,a),rewrite([26(2)])]. given #86 (F,wt=7): 312 -Prefix(x * (y * z),z). [para(26(a,1),274(a,1))]. given #87 (T,wt=7): 429 Power(x * (x * x),x). [resolve(99,a,175,a)]. given #88 (T,wt=7): 454 Power(x,f8(x,x,x,x)). [resolve(429,a,52,b),unit_del(a,32)]. given #89 (T,wt=8): 100 -Power(x,y) | Power(x * y,y). [resolve(34,b,32,a)]. given #90 (T,wt=8): 140 -Shorter(x,y) | Shorter(x,y * z). [resolve(56,a,55,b)]. given #91 (A,wt=15): 94 x * f1(x,x * y,y * z,z) = x * y. [resolve(31,a,26,a),unit_del(a,29),unit_del(c,93)]. given #92 (F,wt=7): 318 -Shorter(x * (c3 * c5),c7). [ur(55,a,57,a,c,277,a)]. given #93 (F,wt=7): 319 -Shorter(c3 * (c5 * x),c7). [ur(55,a,56,a,c,277,a),rewrite([26(4)])]. given #94 (F,wt=7): 320 c3 * (c5 * x) != c7. [ur(67,a,313,a),rewrite([26(4)])]. given #95 (F,wt=7): 373 x * (c3 * c5) != c7. [para(87(a,1),93(a,1,2))]. given #96 (T,wt=7): 506 Shorter(c7,c3 * (c5 * x)). [resolve(140,a,251,a),rewrite([26(5)])]. given #97 (T,wt=8): 141 -Shorter(x * y,z) | Shorter(x,z). [resolve(56,a,55,a)]. given #98 (T,wt=8): 144 -Shorter(x,y) | Shorter(x,z * y). [resolve(57,a,55,b)]. given #99 (T,wt=8): 145 -Shorter(x * y,z) | Shorter(y,z). [resolve(57,a,55,a)]. given #100 (A,wt=15): 95 f2(x * y,x,z,y * z) * z = y * z. [resolve(31,a,26,a(flip)),rewrite([26(7)]),flip(a),unit_del(a,29),unit_del(b,29)]. given #101 (F,wt=7): 374 -Prefix(x * y,y * x). [ur(69,b,154,a)]. given #102 (F,wt=7): 382 -Shorter(c3 * c5,c7 * c5). [para(87(a,1),154(a,1))]. given #103 (F,wt=3): 557 -Shorter(c3,c7). [ur(58,b,382,a)]. given #104 (F,wt=3): 562 -Prefix(c3,c7). [ur(69,b,557,a)]. given #105 (T,wt=8): 260 Prefix(c5,x) | c3 * c5 != x. [para(87(a,1),67(b,1))]. given #106 (T,wt=8): 300 -Power(x,y * y) | Power(x,y). [resolve(175,a,33,b)]. given #107 (T,wt=8): 325 -Shorter(x,c7) | Shorter(x,c3 * c5). [resolve(251,a,55,b)]. given #108 (T,wt=8): 326 -Shorter(c3 * c5,x) | Shorter(c7,x). [resolve(251,a,55,a)]. given #109 (A,wt=38): 96 x * (y * z) != u * w | x * y = u | u * f1(u,x * y,w,z) = x * y | f2(u,x * y,w,z) * w = z. [para(26(a,1),31(a,1))]. given #110 (F,wt=5): 560 -Shorter(x * c3,c7). [ur(145,b,557,a)]. given #111 (F,wt=5): 561 -Shorter(c3 * x,c7). [ur(141,b,557,a)]. given #112 (F,wt=5): 569 c3 * x != c7. [ur(67,a,562,a)]. given #113 (F,wt=5): 576 -Prefix(x * c3,c7). [ur(69,b,560,a)]. given #114 (T,wt=9): 143 Shorter(x * y,x * (y * z)). [para(26(a,1),56(a,2))]. given #115 (T,wt=9): 148 Shorter(x * y,x * (z * y)). [resolve(58,a,56,a),rewrite([26(3)])]. given #116 (T,wt=7): 599 Shorter(c7,c3 * (x * c5)). [resolve(148,a,326,a)]. given #117 (T,wt=9): 152 Shorter(x * y,y * (z * x)). [resolve(62,a,57,a)]. given #118 (A,wt=38): 97 x * (y * z) != u * w | x * y = u | x * (y * f1(x * y,u,z,w)) = u | f2(x * y,u,z,w) * z = w. [para(26(a,1),31(a,2)),rewrite([26(10)]),flip(a),flip(b)]. given #119 (F,wt=5): 583 -Prefix(c3 * x,c7). [ur(69,b,561,a)]. given #120 (F,wt=7): 383 -Shorter(c7 * c5,c3 * c5). [para(87(a,1),154(a,2))]. given #121 (F,wt=3): 650 -Shorter(c7,c3). [ur(58,b,383,a)]. given #122 (F,wt=3): 657 -Prefix(c7,c3). [ur(69,b,650,a)]. given #123 (T,wt=7): 616 Shorter(c7,c5 * (x * c3)). [resolve(152,a,326,a)]. given #124 (T,wt=9): 153 Shorter(x * y,y * (x * z)). [resolve(62,a,56,a)]. given #125 (T,wt=7): 676 Shorter(c7,c5 * (c3 * x)). [resolve(153,a,326,a)]. given #126 (T,wt=9): 157 Shorter(x * y,z * (y * x)). [resolve(64,a,57,a),rewrite([26(3)])]. given #127 (A,wt=36): 98 x * (y * z) != u * w | u = x | x * f1(x,u,y * z,w) = u | f2(x,u,y * z,w) * (y * z) = w. [para(26(a,2),31(a,2)),rewrite([26(3)]),flip(a)]. given #128 (F,wt=5): 655 -Shorter(x * c7,c3). [ur(145,b,650,a)]. given #129 (F,wt=5): 656 -Shorter(c7 * x,c3). [ur(141,b,650,a)]. given #130 (F,wt=5): 664 c7 * x != c3. [ur(67,a,657,a)]. given #131 (F,wt=5): 706 -Prefix(x * c7,c3). [ur(69,b,655,a)]. given #132 (T,wt=7): 694 Shorter(c7,x * (c5 * c3)). [resolve(157,a,326,a)]. given #133 (T,wt=9): 161 Prefix(x * y,x * (y * z)). [resolve(67,b,26,a)]. given #134 (T,wt=9): 228 Prefix(c3,c5) | Prefix(c5,c3) | c5 = c3. [resolve(87,a,68,a)]. given #135 (T,wt=9): 284 Power(x * (x * (x * x)),x). [resolve(175,a,84,a),rewrite([26(3)])]. given #136 (A,wt=12): 101 -Power(x,y) | x = y | Power(f3(y,y,x),y). [resolve(35,a,32,a)]. given #137 (F,wt=5): 713 -Prefix(c7 * x,c3). [ur(69,b,656,a)]. given #138 (F,wt=7): 433 -Prefix(x * (y * z),y). [ur(69,b,273,a)]. given #139 (F,wt=7): 452 -Prefix(x * (c3 * c5),c7). [para(87(a,1),312(a,1,2))]. given #140 (F,wt=7): 549 -Prefix(c3 * c5,c7 * c5). [para(87(a,1),374(a,1))]. given #141 (T,wt=8): 775 Power(f3(x,x,x * x),x). [resolve(101,a,175,a),unit_del(a,29)]. given #142 (T,wt=9): 321 Shorter(x * c7,c3 * (c5 * x)). [resolve(251,a,64,a),rewrite([26(6)])]. given #143 (T,wt=5): 805 Shorter(c7,c5 * c3). [resolve(321,a,61,b)]. given #144 (T,wt=8): 820 -Shorter(x,c7) | Shorter(x,c5 * c3). [resolve(805,a,55,b)]. given #145 (A,wt=12): 102 -Power(x,y) | y = x | Power(f3(y,x,y),y). [resolve(35,b,32,a)]. given #146 (F,wt=7): 550 -Prefix(c7 * c5,c3 * c5). [para(87(a,1),374(a,2))]. given #147 (F,wt=7): 563 -Shorter(x * c3,c7 * x). [ur(65,a,557,a)]. given #148 (F,wt=7): 564 -Shorter(c3 * x,x * c7). [ur(63,a,557,a)]. given #149 (F,wt=7): 565 -Shorter(x * c3,x * c7). [ur(61,a,557,a)]. given #150 (T,wt=8): 821 -Shorter(c5 * c3,x) | Shorter(c7,x). [resolve(805,a,55,a)]. given #151 (T,wt=8): 829 Power(f3(x,x * x,x),x). [resolve(102,a,175,a),flip(a),unit_del(a,29)]. given #152 (T,wt=9): 322 Shorter(c7 * x,x * (c3 * c5)). [resolve(251,a,62,a)]. given #153 (T,wt=9): 323 Shorter(x * c7,x * (c3 * c5)). [resolve(251,a,60,a)]. given #154 (A,wt=22): 103 -Power(x,y) | x = y | x * f3(y,y,x) = y | y * f3(y,y,x) = x. [resolve(36,a,32,a)]. given #155 (F,wt=7): 566 -Shorter(c3 * x,c7 * x). [ur(59,a,557,a)]. given #156 (F,wt=7): 567 -Shorter(x * (c3 * y),c7). [ur(55,a,328,a,c,557,a)]. given #157 (F,wt=7): 568 -Shorter(x * (y * c3),c7). [ur(55,a,147,a,c,557,a)]. given #158 (F,wt=7): 591 x * (c3 * y) != c7. [ur(67,a,576,a),rewrite([26(3)])]. given #159 (T,wt=9): 324 Shorter(c7 * x,c3 * (c5 * x)). [resolve(251,a,58,a),rewrite([26(6)])]. given #160 (T,wt=9): 336 Shorter(x,y * (z * (u * x))). [para(26(a,1),147(a,2,2))]. given #161 (T,wt=9): 338 Power(c4 * c4,f8(c5,c5,c3,c4)). [resolve(177,a,84,a)]. given #162 (T,wt=9): 353 Power(c3 * c3,f8(c5,c5,c3,c4)). [resolve(178,a,84,a)]. given #163 (A,wt=22): 104 -Power(x,y) | y = x | y * f3(y,x,y) = x | x * f3(y,x,y) = y. [resolve(36,b,32,a)]. given #164 (F,wt=7): 592 -Prefix(x * (y * c3),c7). [para(26(a,1),576(a,1))]. given #165 (F,wt=7): 658 -Shorter(x * c7,c3 * x). [ur(65,a,650,a)]. given #166 (F,wt=7): 659 -Shorter(c7 * x,x * c3). [ur(63,a,650,a)]. given #167 (F,wt=7): 660 -Shorter(x * c7,x * c3). [ur(61,a,650,a)]. given #168 (T,wt=9): 393 Power(c5 * c5,f8(c5,c5,c3,c4)). [resolve(179,a,84,a)]. given #169 (T,wt=9): 418 Shorter(x,y * (z * (x * u))). [para(26(a,1),328(a,2))]. given #170 (T,wt=9): 425 Shorter(c7,x * (y * (c3 * c5))). [para(26(a,1),337(a,2))]. given #171 (T,wt=9): 430 Power(c3 * (c3 * (c5 * c2)),c3). [resolve(99,a,86,a)]. given #172 (A,wt=22): 105 -Power(x,y) | x = y | x * f3(y,y,x) = y | f3(y,y,x) * y = x. [resolve(37,a,32,a)]. given #173 (F,wt=7): 661 -Shorter(c7 * x,c3 * x). [ur(59,a,650,a)]. given #174 (F,wt=7): 662 -Shorter(x * (c7 * y),c3). [ur(55,a,328,a,c,650,a)]. given #175 (F,wt=7): 663 -Shorter(x * (y * c7),c3). [ur(55,a,147,a,c,650,a)]. given #176 (F,wt=7): 727 x * (c7 * y) != c3. [ur(67,a,706,a),rewrite([26(3)])]. given #177 (T,wt=9): 431 Power(c5 * (c3 * (c5 * c4)),c5). [resolve(99,a,85,a)]. given #178 (T,wt=9): 471 Power(x * x,f8(x,x,x,x)). [resolve(454,a,84,a)]. given #179 (T,wt=9): 503 Power(c3 * (c5 * (c2 * c3)),c3). [resolve(100,a,86,a),rewrite([26(7),26(6)])]. given #180 (T,wt=9): 504 Power(c3 * (c5 * (c4 * c5)),c5). [resolve(100,a,85,a),rewrite([26(7),26(6)])]. given #181 (A,wt=22): 106 -Power(x,y) | y = x | y * f3(y,x,y) = x | f3(y,x,y) * x = y. [resolve(37,b,32,a)]. given #182 (F,wt=7): 728 -Prefix(x * (y * c7),c3). [para(26(a,1),706(a,1))]. given #183 (F,wt=7): 834 -Prefix(x * c3,c7 * x). [ur(69,b,563,a)]. given #184 (F,wt=7): 845 -Prefix(c3 * x,x * c7). [ur(69,b,564,a)]. given #185 (F,wt=7): 853 -Prefix(x * c3,x * c7). [ur(69,b,565,a)]. given #186 (T,wt=9): 505 Shorter(c7,x * (c3 * (c5 * y))). [resolve(140,a,337,a),rewrite([26(6),26(5)])]. given #187 (T,wt=9): 606 Shorter(c3 * c5,c5 * (x * c7)). [para(87(a,1),148(a,1))]. given #188 (T,wt=5): 1312 Shorter(c3,x * c7). [resolve(606,a,63,b)]. given #189 (T,wt=7): 1322 Shorter(c3,x * (y * c7)). [resolve(1312,a,144,a)]. given #190 (A,wt=22): 107 -Power(x,y) | x = y | f3(y,y,x) * x = y | y * f3(y,y,x) = x. [resolve(38,a,32,a)]. given #191 (F,wt=7): 909 -Prefix(c3 * x,c7 * x). [ur(69,b,566,a)]. given #192 (F,wt=7): 914 -Prefix(x * (c3 * y),c7). [ur(69,b,567,a)]. given #193 (F,wt=7): 1025 -Prefix(x * c7,c3 * x). [ur(69,b,658,a)]. given #194 (F,wt=7): 1037 -Prefix(c7 * x,x * c3). [ur(69,b,659,a)]. given #195 (T,wt=7): 1323 Shorter(c3,x * (c7 * y)). [resolve(1312,a,140,a),rewrite([26(4)])]. given #196 (T,wt=8): 1328 -Shorter(x,c3) | Shorter(x,y * c7). [resolve(1312,a,55,b)]. given #197 (T,wt=8): 1329 -Shorter(x * c7,y) | Shorter(c3,y). [resolve(1312,a,55,a)]. given #198 (T,wt=7): 1362 Shorter(c3,c7 * (x * y)). [resolve(1329,a,153,a)]. given #199 (A,wt=22): 108 -Power(x,y) | y = x | f3(y,x,y) * y = x | x * f3(y,x,y) = y. [resolve(38,b,32,a)]. given #200 (F,wt=7): 1045 -Prefix(x * c7,x * c3). [ur(69,b,660,a)]. given #201 (F,wt=7): 1134 -Prefix(c7 * x,c3 * x). [ur(69,b,661,a)]. given #202 (F,wt=7): 1141 -Prefix(x * (c7 * y),c3). [ur(69,b,662,a)]. given #203 (F,wt=9): 269 -Shorter(x * (y * z),y * x). [ur(65,a,142,a)]. given #204 (T,wt=9): 607 Shorter(c7,x * (c3 * (y * c5))). [resolve(599,a,144,a)]. given #205 (T,wt=9): 608 Shorter(c7,c3 * (x * (c5 * y))). [resolve(599,a,140,a),rewrite([26(6),26(5)])]. given #206 (T,wt=9): 615 Shorter(c7,c3 * (x * (y * c5))). [para(26(a,1),599(a,2,2))]. given #207 (T,wt=9): 626 Shorter(c3 * c5,c7 * (x * c5)). [para(87(a,1),152(a,1))]. given #208 (A,wt=22): 109 -Power(x,y) | x = y | f3(y,y,x) * x = y | f3(y,y,x) * y = x. [resolve(39,a,32,a)]. given #209 (F,wt=9): 270 -Shorter(x * (y * z),z * x). [ur(63,a,142,a),rewrite([26(2)])]. given #210 (F,wt=9): 271 -Shorter(x * (y * z),x * y). [ur(61,a,142,a)]. given #211 (F,wt=9): 272 -Shorter(x * (y * z),x * z). [ur(59,a,142,a),rewrite([26(2)])]. given #212 (F,wt=9): 275 -Shorter(x * (y * z),z * y). [ur(63,a,146,a),rewrite([26(2)])]. given #213 (T,wt=9): 665 Shorter(c7,x * (c5 * (y * c3))). [resolve(616,a,144,a)]. given #214 (T,wt=9): 666 Shorter(c7,c5 * (x * (c3 * y))). [resolve(616,a,140,a),rewrite([26(6),26(5)])]. given #215 (T,wt=9): 675 Shorter(c7,c5 * (x * (y * c3))). [para(26(a,1),616(a,2,2))]. given #216 (T,wt=9): 685 Shorter(c3 * c5,c7 * (c5 * x)). [para(87(a,1),153(a,1))]. given #217 (A,wt=22): 110 -Power(x,y) | y = x | f3(y,x,y) * y = x | f3(y,x,y) * x = y. [resolve(39,b,32,a)]. given #218 (F,wt=9): 310 -Prefix(x * (y * z),x * y). [para(26(a,1),268(a,1))]. given #219 (F,wt=9): 333 -Shorter(x * (y * (z * u)),u). [ur(55,b,147,a,c,146,a)]. given #220 (F,wt=9): 334 -Shorter(x * (y * (z * u)),z). [ur(55,b,147,a,c,142,a),rewrite([26(3),26(2)])]. given #221 (F,wt=9): 370 c5 * (x * c7) != c3 * c5. [para(87(a,1),91(a,2))]. given #222 (T,wt=9): 686 Shorter(c7,x * (c5 * (c3 * y))). [resolve(676,a,144,a)]. given #223 (T,wt=9): 704 Shorter(c7 * c5,x * (c3 * c5)). [para(87(a,1),157(a,2,2))]. given #224 (T,wt=9): 729 Shorter(c7,x * (y * (c5 * c3))). [resolve(694,a,144,a)]. given #225 (T,wt=9): 741 Prefix(x * c5,x * (c3 * c5)). [para(87(a,1),161(a,2,2))]. given #226 (A,wt=22): 111 Power(x,x * y) | f4(x,y,x * y) * f5(x,y,x * y) = x * y. [resolve(40,a,32,a)]. given #227 (F,wt=9): 372 x * (y * (z * u)) != u. [para(26(a,1),93(a,1,2))]. given #228 (F,wt=9): 450 x * (y * (z * u)) != z. [para(26(a,1),311(a,1))]. given #229 (F,wt=9): 451 -Prefix(x * (y * (z * u)),u). [para(26(a,1),312(a,1,2))]. given #230 (F,wt=9): 546 x * (y * z) != y * x. [ur(67,a,374,a),rewrite([26(2)])]. given #231 (T,wt=9): 744 Prefix(c5,c3) | c5 = c3 | Shorter(c3,c5). [resolve(228,a,69,a)]. given #232 (T,wt=9): 748 Prefix(c3,c5) | c5 = c3 | Shorter(c5,c3). [resolve(228,b,69,a)]. given #233 (T,wt=9): 753 Power(x,f8(x,x,x,x * x)). [resolve(284,a,51,b),unit_del(a,32)]. given #234 (T,wt=9): 815 Shorter(c7 * c7,c3 * (c3 * c5)). [para(87(a,1),321(a,2,2))]. given #235 (A,wt=27): 112 -Power(x * (y * z),u) | Power(x * y,u) | f4(x * y,z,u) * f5(x * y,z,u) = u. [para(26(a,1),40(a,1))]. given #236 (F,wt=9): 577 -Shorter(x * (y * c3),c7 * x). [ur(65,a,560,a)]. given #237 (F,wt=9): 578 -Shorter(x * (c3 * y),y * c7). [ur(63,a,560,a),rewrite([26(3)])]. given #238 (F,wt=9): 579 -Shorter(x * (y * c3),x * c7). [ur(61,a,560,a)]. given #239 (F,wt=9): 580 -Shorter(x * (c3 * y),c7 * y). [ur(59,a,560,a),rewrite([26(3)])]. given #240 (T,wt=9): 816 Shorter(x * c7,c5 * (c3 * x)). [resolve(805,a,64,a),rewrite([26(6)])]. given #241 (T,wt=9): 817 Shorter(c7 * x,x * (c5 * c3)). [resolve(805,a,62,a)]. given #242 (T,wt=9): 818 Shorter(x * c7,x * (c5 * c3)). [resolve(805,a,60,a)]. given #243 (T,wt=9): 819 Shorter(c7 * x,c5 * (c3 * x)). [resolve(805,a,58,a),rewrite([26(6)])]. given #244 (A,wt=28): 113 Power(x,x * y) | f4(x,y,x * y) = x | f6(x,y,x * y) * f4(x,y,x * y) = x. [resolve(41,a,32,a)]. given #245 (F,wt=9): 581 -Shorter(x * (y * (c3 * z)),c7). [ur(55,a,328,a,c,560,a),rewrite([26(3)])]. given #246 (F,wt=9): 582 -Shorter(x * (y * (z * c3)),c7). [ur(55,a,147,a,c,560,a)]. given #247 (F,wt=9): 584 -Shorter(x * (c3 * y),c7 * x). [ur(65,a,561,a)]. given #248 (F,wt=9): 585 -Shorter(c3 * (x * y),y * c7). [ur(63,a,561,a),rewrite([26(3)])]. given #249 (T,wt=9): 1104 Power(c3,f8(c3,c3,c3,c5 * c2)). [resolve(430,a,51,b),unit_del(a,32)]. given #250 (T,wt=9): 1260 Power(c3,f8(c5,c5,c3,c4 * c5)). [resolve(504,a,51,b),unit_del(a,32)]. given #251 (T,wt=9): 1261 Power(c5,f8(c5,c5,c3,c4 * c5)). [resolve(504,a,50,b),unit_del(a,32)]. given #252 (T,wt=9): 1324 Shorter(x * c3,y * (c7 * x)). [resolve(1312,a,64,a),rewrite([26(5)])]. given #253 (A,wt=39): 114 -Power(x * (y * z),u) | Power(x * y,u) | f4(x * y,z,u) = x * y | f6(x * y,z,u) * f4(x * y,z,u) = x * y. [para(26(a,1),41(a,1))]. given #254 (F,wt=9): 586 -Shorter(x * (c3 * y),x * c7). [ur(61,a,561,a)]. given #255 (F,wt=9): 587 -Shorter(c3 * (x * y),c7 * y). [ur(59,a,561,a),rewrite([26(3)])]. given #256 (F,wt=9): 588 c7 * x != c3 * (y * x). [ur(90,b,569,a),flip(a)]. given #257 (F,wt=9): 590 x * (c3 * y) != x * c7. [ur(27,b,569,a)]. given #258 (T,wt=5): 2017 Shorter(c3,c7 * x). [resolve(1324,a,61,b)]. given #259 (T,wt=8): 2060 -Shorter(x,c3) | Shorter(x,c7 * y). [resolve(2017,a,55,b)]. given #260 (T,wt=8): 2061 -Shorter(c7 * x,y) | Shorter(c3,y). [resolve(2017,a,55,a)]. given #261 (T,wt=9): 1325 Shorter(c3 * x,x * (y * c7)). [resolve(1312,a,62,a)]. given #262 (A,wt=23): 115 Power(x,x * y) | f4(x,y,x * y) = x | Power(f6(x,y,x * y),x * y). [resolve(42,a,32,a)]. given #263 (F,wt=9): 707 -Shorter(x * (y * c7),c3 * x). [ur(65,a,655,a)]. given #264 (F,wt=9): 708 -Shorter(x * (c7 * y),y * c3). [ur(63,a,655,a),rewrite([26(3)])]. given #265 (F,wt=9): 709 -Shorter(x * (y * c7),x * c3). [ur(61,a,655,a)]. given #266 (F,wt=9): 710 -Shorter(x * (c7 * y),c3 * y). [ur(59,a,655,a),rewrite([26(3)])]. given #267 (T,wt=9): 1326 Shorter(x * c3,x * (y * c7)). [resolve(1312,a,60,a)]. given #268 (T,wt=9): 1327 Shorter(c3 * x,y * (c7 * x)). [resolve(1312,a,58,a),rewrite([26(5)])]. given #269 (T,wt=9): 1330 Shorter(c3,x * (y * (z * c7))). [resolve(1322,a,144,a)]. given #270 (T,wt=9): 1331 Shorter(c3,x * (y * (c7 * z))). [resolve(1322,a,140,a),rewrite([26(5),26(4)])]. given #271 (A,wt=30): 116 -Power(x * (y * z),u) | Power(x * y,u) | f4(x * y,z,u) = x * y | Power(f6(x * y,z,u),u). [para(26(a,1),42(a,1))]. given #272 (F,wt=9): 711 -Shorter(x * (y * (c7 * z)),c3). [ur(55,a,328,a,c,655,a),rewrite([26(3)])]. given #273 (F,wt=9): 712 -Shorter(x * (y * (z * c7)),c3). [ur(55,a,147,a,c,655,a)]. given #274 (F,wt=9): 714 -Shorter(x * (c7 * y),c3 * x). [ur(65,a,656,a)]. given #275 (F,wt=9): 715 -Shorter(c7 * (x * y),y * c3). [ur(63,a,656,a),rewrite([26(3)])]. given #276 (T,wt=9): 1695 c5 = c3 | Shorter(c3,c5) | Shorter(c5,c3). [resolve(744,a,69,a)]. given #277 (T,wt=9): 1705 Prefix(c5,c3) | c5 = c3 | -Shorter(c5,c3). [resolve(744,c,54,b)]. given #278 (T,wt=9): 1718 Prefix(c3,c5) | c5 = c3 | -Shorter(c3,c5). [resolve(748,c,54,b)]. given #279 (T,wt=9): 2056 Shorter(x * c3,c7 * (y * x)). [resolve(2017,a,64,a),rewrite([26(5)])]. given #280 (A,wt=28): 117 Power(x,x * y) | f5(x,y,x * y) = y | f5(x,y,x * y) * f7(x,y,x * y) = y. [resolve(43,a,32,a)]. given #281 (F,wt=9): 716 -Shorter(x * (c7 * y),x * c3). [ur(61,a,656,a)]. given #282 (F,wt=9): 717 -Shorter(c7 * (x * y),c3 * y). [ur(59,a,656,a),rewrite([26(3)])]. given #283 (F,wt=9): 720 c7 * (x * y) != c3 * y. [ur(97,b,664,a,c,664,a,d,30,a)]. given #284 (F,wt=9): 726 x * (c7 * y) != x * c3. [ur(27,b,664,a)]. given #285 (T,wt=9): 2057 Shorter(c3 * x,x * (c7 * y)). [resolve(2017,a,62,a)]. given #286 (T,wt=9): 2058 Shorter(x * c3,x * (c7 * y)). [resolve(2017,a,60,a)]. given #287 (T,wt=9): 2059 Shorter(c3 * x,c7 * (y * x)). [resolve(2017,a,58,a),rewrite([26(5)])]. given #288 (T,wt=10): 202 -Power(x,c3 * (c5 * c4)) | Power(x,c5). [resolve(85,a,33,b)]. given #289 (A,wt=35): 118 -Power(x * (y * z),u) | Power(x * y,u) | f5(x * y,z,u) = z | f5(x * y,z,u) * f7(x * y,z,u) = z. [para(26(a,1),43(a,1))]. given #290 (F,wt=9): 779 -Prefix(x * (y * (z * u)),z). [para(26(a,1),433(a,1))]. given #291 (F,wt=9): 833 -Shorter(x * (y * c3),c7 * y). [ur(145,b,563,a)]. given #292 (F,wt=9): 839 -Shorter(x * (y * c3),y * c7). [ur(55,b,152,a,c,563,a),rewrite([26(3)])]. given #293 (F,wt=9): 841 -Shorter(c3 * (x * y),c7 * x). [ur(55,a,153,a,c,563,a)]. given #294 (T,wt=10): 203 -Power(c5,x) | Power(c3 * (c5 * c4),x). [resolve(85,a,33,a)]. given #295 (T,wt=10): 205 -Power(c5,c3) | Power(c2,f8(c3,c5,c3,c2)). [resolve(86,a,52,b)]. given #296 (T,wt=10): 206 -Power(c5,c3) | Power(c3,f8(c3,c5,c3,c2)). [resolve(86,a,51,b)]. given #297 (T,wt=10): 207 -Power(c5,c3) | Power(c5,f8(c3,c5,c3,c2)). [resolve(86,a,50,b)]. given #298 (A,wt=23): 119 Power(x,x * y) | f5(x,y,x * y) = y | Power(f7(x,y,x * y),x * y). [resolve(44,a,32,a)]. given #299 (F,wt=9): 844 -Shorter(c3 * (x * y),x * c7). [ur(141,b,564,a),rewrite([26(3)])]. given #300 (F,wt=9): 850 -Shorter(c3 * (c5 * c3),c7 * c7). [ur(55,a,321,a,c,564,a)]. given #301 (F,wt=9): 888 -Shorter(c3 * (c3 * c5),c7 * c7). [ur(55,a,322,a,c,565,a)]. given #302 (F,wt=9): 942 x * (y * (c3 * z)) != c7. [para(26(a,1),591(a,1))]. given #303 (T,wt=10): 225 -Power(x,c3 * (c5 * c2)) | Power(x,c3). [resolve(86,a,33,b)]. given #304 (T,wt=10): 226 -Power(c3,x) | Power(c3 * (c5 * c2),x). [resolve(86,a,33,a)]. given #305 (T,wt=10): 233 c5 * x != c3 * c5 | c7 = x. [para(87(a,1),27(a,1)),flip(a)]. given #306 (T,wt=10): 234 c3 * c5 != x * c7 | c5 = x. [para(87(a,1),28(a,1))]. given #307 (A,wt=28): 120 -Power(x * (y * z),u) | Power(x * y,u) | f5(x * y,z,u) = z | Power(f7(x * y,z,u),u). [para(26(a,1),44(a,1))]. given #308 (F,wt=9): 1023 -Prefix(x * (y * (z * c3)),c7). [para(26(a,1),592(a,1,2))]. given #309 (F,wt=9): 1024 -Shorter(x * (y * c7),c3 * y). [ur(145,b,658,a)]. given #310 (F,wt=9): 1030 -Shorter(x * (y * c7),y * c3). [ur(55,b,152,a,c,658,a),rewrite([26(3)])]. given #311 (F,wt=9): 1033 -Shorter(c7 * (x * y),c3 * x). [ur(55,a,153,a,c,658,a)]. given #312 (T,wt=10): 252 Shorter(c5,x) | -Shorter(c3 * c5,x * c7). [para(87(a,1),59(b,1))]. given #313 (T,wt=10): 253 Shorter(x,c5) | -Shorter(x * c7,c3 * c5). [para(87(a,1),59(b,2))]. given #314 (T,wt=10): 254 Shorter(c7,x) | -Shorter(c3 * c5,c5 * x). [para(87(a,1),61(b,1))]. given #315 (T,wt=5): 2609 Shorter(c7,c3 * x). [resolve(254,b,153,a)]. given #316 (A,wt=22): 121 Power(x,y * x) | f4(y,x,y * x) * f5(y,x,y * x) = y * x. [resolve(45,a,32,a)]. given #317 (F,wt=9): 1036 -Shorter(c7 * (x * y),x * c3). [ur(141,b,659,a),rewrite([26(3)])]. given #318 (F,wt=9): 1171 x * (y * (c7 * z)) != c3. [para(26(a,1),727(a,1))]. given #319 (F,wt=9): 1296 -Prefix(x * (y * (z * c7)),c3). [para(26(a,1),728(a,1,2))]. given #320 (F,wt=9): 1297 c7 * x != x * (c3 * y). [ur(67,a,834,a),rewrite([26(3)]),flip(a)]. given #321 (T,wt=5): 2610 Shorter(c7,x * c3). [resolve(254,b,152,a)]. given #322 (T,wt=7): 2611 Shorter(c7,x * (c3 * y)). [resolve(2609,a,144,a)]. given #323 (T,wt=7): 2710 Shorter(c7,x * (y * c3)). [resolve(2610,a,144,a)]. given #324 (T,wt=8): 2616 -Shorter(x,c7) | Shorter(x,c3 * y). [resolve(2609,a,55,b)]. given #325 (A,wt=25): 122 -Power(x * (y * z),u) | Power(z,u) | f4(x * y,z,u) * f5(x * y,z,u) = u. [para(26(a,1),45(a,1))]. given #326 (F,wt=9): 1299 c3 * (x * y) != x * c7. [ur(67,a,845,a),rewrite([26(3)])]. given #327 (F,wt=9): 1348 c7 * x != c3 * (x * y). [ur(67,a,909,a),rewrite([26(3)]),flip(a)]. given #328 (F,wt=9): 1349 -Prefix(x * (y * (c3 * z)),c7). [para(26(a,1),914(a,1))]. given #329 (F,wt=9): 1350 c3 * x != x * (c7 * y). [ur(67,a,1025,a),rewrite([26(3)]),flip(a)]. given #330 (T,wt=8): 2617 -Shorter(c3 * x,y) | Shorter(c7,y). [resolve(2609,a,55,a)]. given #331 (T,wt=8): 2715 -Shorter(x,c7) | Shorter(x,y * c3). [resolve(2610,a,55,b)]. given #332 (T,wt=8): 2716 -Shorter(x * c3,y) | Shorter(c7,y). [resolve(2610,a,55,a)]. given #333 (T,wt=9): 2612 Shorter(x * c7,c3 * (y * x)). [resolve(2609,a,64,a),rewrite([26(5)])]. given #334 (A,wt=28): 123 Power(x,y * x) | f4(y,x,y * x) = y | f6(y,x,y * x) * f4(y,x,y * x) = y. [resolve(46,a,32,a)]. given #335 (F,wt=9): 1352 c7 * (x * y) != x * c3. [ur(67,a,1037,a),rewrite([26(3)])]. given #336 (F,wt=9): 1389 c7 * (x * y) != c3 * x. [ur(67,a,1134,a),rewrite([26(3)])]. given #337 (F,wt=9): 1390 -Prefix(x * (y * (c7 * z)),c3). [para(26(a,1),1141(a,1))]. given #338 (F,wt=9): 1391 -Prefix(x * (y * z),y * x). [ur(69,b,269,a)]. given #339 (T,wt=9): 2613 Shorter(c7 * x,x * (c3 * y)). [resolve(2609,a,62,a)]. given #340 (T,wt=9): 2614 Shorter(x * c7,x * (c3 * y)). [resolve(2609,a,60,a)]. given #341 (T,wt=9): 2615 Shorter(c7 * x,c3 * (y * x)). [resolve(2609,a,58,a),rewrite([26(5)])]. given #342 (T,wt=9): 2711 Shorter(x * c7,y * (c3 * x)). [resolve(2610,a,64,a),rewrite([26(5)])]. given #343 (A,wt=37): 124 -Power(x * (y * z),u) | Power(z,u) | f4(x * y,z,u) = x * y | f6(x * y,z,u) * f4(x * y,z,u) = x * y. [para(26(a,1),46(a,1))]. given #344 (F,wt=9): 1442 -Prefix(x * (y * z),z * x). [ur(69,b,270,a)]. given #345 (F,wt=9): 1455 -Prefix(x * (y * z),x * z). [ur(69,b,272,a)]. given #346 (F,wt=9): 1463 -Prefix(x * (y * z),z * y). [ur(69,b,275,a)]. given #347 (F,wt=9): 1691 c5 * x != x * (c3 * c5). [para(87(a,1),546(a,1,2)),flip(a)]. given #348 (T,wt=9): 2712 Shorter(c7 * x,x * (y * c3)). [resolve(2610,a,62,a)]. given #349 (T,wt=9): 2713 Shorter(x * c7,x * (y * c3)). [resolve(2610,a,60,a)]. given #350 (T,wt=9): 2714 Shorter(c7 * x,y * (c3 * x)). [resolve(2610,a,58,a),rewrite([26(5)])]. given #351 (T,wt=9): 2717 Shorter(c7,x * (y * (c3 * z))). [resolve(2611,a,144,a)]. given #352 (A,wt=23): 125 Power(x,y * x) | f4(y,x,y * x) = y | Power(f6(y,x,y * x),y * x). [resolve(47,a,32,a)]. given #353 (F,wt=9): 1692 c3 * x != x * (c3 * c5). [para(87(a,2),546(a,1,2)),rewrite([87(3)]),flip(a)]. given #354 (F,wt=9): 1789 -Prefix(x * (y * c3),c7 * x). [ur(69,b,577,a)]. given #355 (F,wt=9): 1800 -Prefix(x * (c3 * y),y * c7). [ur(69,b,578,a)]. given #356 (F,wt=9): 1807 -Prefix(x * (y * c3),x * c7). [ur(69,b,579,a)]. given #357 (T,wt=9): 2724 Shorter(c7,x * (y * (z * c3))). [resolve(2710,a,144,a)]. given #358 (T,wt=10): 255 Shorter(x,c7) | -Shorter(c5 * x,c3 * c5). [para(87(a,1),61(b,2))]. given #359 (T,wt=10): 256 Shorter(c5,x) | -Shorter(c3 * c5,c7 * x). [para(87(a,1),63(b,1))]. given #360 (T,wt=10): 257 Shorter(x,c7) | -Shorter(x * c5,c3 * c5). [para(87(a,1),63(b,2))]. given #361 (A,wt=28): 126 -Power(x * (y * z),u) | Power(z,u) | f4(x * y,z,u) = x * y | Power(f6(x * y,z,u),u). [para(26(a,1),47(a,1))]. given #362 (F,wt=9): 1816 -Prefix(x * (c3 * y),c7 * y). [ur(69,b,580,a)]. given #363 (F,wt=9): 1912 -Prefix(x * (c3 * y),c7 * x). [ur(69,b,584,a)]. given #364 (F,wt=9): 1924 -Prefix(c3 * (x * y),y * c7). [ur(69,b,585,a)]. given #365 (F,wt=9): 2024 -Shorter(x * (c7 * c7),c3 * c3). [ur(55,a,1324,a,c,661,a)]. given #366 (T,wt=10): 258 Shorter(c7,x) | -Shorter(c3 * c5,x * c5). [para(87(a,1),65(b,1))]. given #367 (T,wt=10): 259 Shorter(x,c5) | -Shorter(c7 * x,c3 * c5). [para(87(a,1),65(b,2))]. given #368 (T,wt=10): 281 -Power(x * y,z) | Prefix(x,f11(z,x)). [resolve(163,a,83,b)]. given #369 (T,wt=5): 3080 Prefix(c3,f11(c5,c3)). [resolve(281,a,504,a)]. given #370 (A,wt=28): 127 Power(x,y * x) | f5(y,x,y * x) = x | f5(y,x,y * x) * f7(y,x,y * x) = x. [resolve(48,a,32,a)]. given #371 (F,wt=9): 2036 -Prefix(x * (c3 * y),x * c7). [ur(69,b,586,a)]. given #372 (F,wt=9): 2042 -Prefix(c3 * (x * y),c7 * y). [ur(69,b,587,a)]. given #373 (F,wt=9): 2054 c7 * c7 != c3 * (c3 * c5). [para(87(a,1),588(a,2,2))]. given #374 (F,wt=9): 2069 -Shorter(c7 * (x * c7),c3 * c3). [ur(55,b,1325,a,c,661,a)]. given #375 (T,wt=5): 3085 Prefix(x,f11(x,x)). [resolve(281,a,429,a)]. given #376 (T,wt=5): 3100 Shorter(c3,f11(c5,c3)). [resolve(3080,a,69,a)]. given #377 (T,wt=5): 3180 Shorter(x,f11(x,x)). [resolve(3085,a,69,a)]. given #378 (T,wt=7): 3097 Prefix(x,f11(x * y,x)). [resolve(281,a,32,a)]. given #379 (A,wt=33): 128 -Power(x * (y * z),u) | Power(z,u) | f5(x * y,z,u) = z | f5(x * y,z,u) * f7(x * y,z,u) = z. [para(26(a,1),48(a,1))]. given #380 (F,wt=5): 3190 -Shorter(f11(c5,c3),c3). [resolve(3100,a,54,b)]. given #381 (F,wt=5): 3197 -Shorter(f11(c5,c3),c7). [ur(55,a,3100,a,c,557,a)]. given #382 (F,wt=5): 3212 -Shorter(f11(x,x),x). [resolve(3180,a,54,b)]. given #383 (F,wt=5): 3247 -Shorter(f11(c7,c7),c3). [ur(55,a,3180,a,c,650,a)]. given #384 (T,wt=7): 3182 Shorter(c3,x * f11(c5,c3)). [resolve(3100,a,144,a)]. given #385 (T,wt=7): 3183 Shorter(c3,f11(c5,c3) * x). [resolve(3100,a,140,a)]. given #386 (T,wt=7): 3203 Shorter(x,y * f11(x,x)). [resolve(3180,a,144,a)]. given #387 (T,wt=7): 3205 Shorter(x,f11(x,x) * y). [resolve(3180,a,140,a)]. given #388 (A,wt=23): 129 Power(x,y * x) | f5(y,x,y * x) = x | Power(f7(y,x,y * x),y * x). [resolve(49,a,32,a)]. given #389 (F,wt=5): 3266 -Shorter(f11(c3,c3),c7). [ur(55,a,3180,a,c,557,a)]. given #390 (F,wt=5): 3302 -Prefix(f11(c5,c3),c3). [ur(69,b,3190,a)]. given #391 (F,wt=5): 3310 -Prefix(f11(c5,c3),c7). [ur(69,b,3197,a)]. given #392 (F,wt=5): 3324 -Prefix(f11(x,x),x). [ur(69,b,3212,a)]. given #393 (T,wt=7): 3281 Shorter(x,f11(x * y,x)). [resolve(3097,a,69,a)]. given #394 (T,wt=7): 3284 Prefix(c5,f11(c3 * c5,c5)). [para(87(a,1),3097(a,2,1))]. given #395 (T,wt=7): 3711 Shorter(c5,f11(c3 * c5,c5)). [para(87(a,1),3281(a,2,1))]. given #396 (T,wt=8): 3188 -Shorter(x,c3) | Shorter(x,f11(c5,c3)). [resolve(3100,a,55,b)]. given #397 (A,wt=26): 130 -Power(x * (y * z),u) | Power(z,u) | f5(x * y,z,u) = z | Power(f7(x * y,z,u),u). [para(26(a,1),49(a,1))]. given #398 (F,wt=5): 3333 -Prefix(f11(c7,c7),c3). [ur(69,b,3247,a)]. given #399 (F,wt=5): 3608 -Prefix(f11(c3,c3),c7). [ur(69,b,3266,a)]. given #400 (F,wt=7): 3195 -Shorter(x * f11(c5,c3),c3). [ur(55,b,3100,a,c,146,a)]. given #401 (F,wt=7): 3196 -Shorter(f11(c5,c3) * x,c3). [ur(55,b,3100,a,c,142,a)]. given #402 (T,wt=8): 3189 -Shorter(f11(c5,c3),x) | Shorter(c3,x). [resolve(3100,a,55,a)]. given #403 (T,wt=8): 3210 -Shorter(x,y) | Shorter(x,f11(y,y)). [resolve(3180,a,55,b)]. given #404 (T,wt=8): 3211 -Shorter(f11(x,x),y) | Shorter(x,y). [resolve(3180,a,55,a)]. given #405 (T,wt=9): 3082 Prefix(x,f11(f8(x,x,x,x),x)). [resolve(281,a,471,a)]. given #406 (A,wt=18): 131 -Power(x,y * (x * z)) | Power(x,f8(y * (x * z),x,y,z)). [resolve(50,b,32,a)]. given #407 (F,wt=7): 3217 -Shorter(x * f11(y,y),y). [ur(55,b,3180,a,c,146,a)]. given #408 (F,wt=7): 3218 -Shorter(f11(x,x) * y,x). [ur(55,b,3180,a,c,142,a)]. given #409 (F,wt=7): 3308 -Shorter(x * f11(c5,c3),c7). [ur(145,b,3197,a)]. given #410 (F,wt=7): 3309 -Shorter(f11(c5,c3) * x,c7). [ur(141,b,3197,a)]. given #411 (T,wt=9): 3086 Prefix(c5,f11(f8(c5,c5,c3,c4),c5)). [resolve(281,a,393,a)]. given #412 (T,wt=9): 3087 Prefix(c3,f11(f8(c5,c5,c3,c4),c3)). [resolve(281,a,353,a)]. given #413 (T,wt=9): 3088 Prefix(c4,f11(f8(c5,c5,c3,c4),c4)). [resolve(281,a,338,a)]. given #414 (T,wt=9): 3184 Shorter(x * c3,f11(c5,c3) * x). [resolve(3100,a,64,a)]. given #415 (A,wt=25): 132 -Power(x * y,z) | -Power(u * (x * (y * w)),z) | Power(x * y,f8(z,x * y,u,w)). [para(26(a,1),50(b,1,2))]. given #416 (F,wt=7): 3331 -Shorter(x * f11(c7,c7),c3). [ur(145,b,3247,a)]. given #417 (F,wt=7): 3332 -Shorter(f11(c7,c7) * x,c3). [ur(141,b,3247,a)]. given #418 (F,wt=7): 3428 -Shorter(x * f11(c3,c3),c7). [ur(55,a,3203,a,c,557,a)]. given #419 (F,wt=7): 3504 -Shorter(f11(c3,c3) * x,c7). [ur(55,a,3205,a,c,557,a)]. given #420 (T,wt=7): 3904 Shorter(c7,f11(c5,c3) * x). [resolve(3184,a,2716,a)]. given #421 (T,wt=9): 3185 Shorter(c3 * x,x * f11(c5,c3)). [resolve(3100,a,62,a)]. given #422 (T,wt=5): 4003 Shorter(c7,f11(c5,c3)). [resolve(3185,a,254,b)]. given #423 (T,wt=7): 4002 Shorter(c7,x * f11(c5,c3)). [resolve(3185,a,2617,a)]. given #424 (A,wt=21): 133 -Power(x,y) | -Power(z * (u * (x * w)),y) | Power(x,f8(y,x,z * u,w)). [para(26(a,1),50(b,1))]. given #425 (F,wt=7): 3620 f11(c5,c3) * x != c3. [ur(67,a,3302,a)]. given #426 (F,wt=7): 3621 f11(c5,c3) * x != c7. [ur(67,a,3310,a)]. given #427 (F,wt=7): 3622 f11(x,x) * y != x. [ur(67,a,3324,a)]. given #428 (F,wt=7): 3637 -Shorter(f11(x * y,x),x). [resolve(3281,a,54,b)]. given #429 (T,wt=8): 4029 -Shorter(x,c7) | Shorter(x,f11(c5,c3)). [resolve(4003,a,55,b)]. given #430 (T,wt=8): 4030 -Shorter(f11(c5,c3),x) | Shorter(c7,x). [resolve(4003,a,55,a)]. given #431 (T,wt=9): 3186 Shorter(x * c3,x * f11(c5,c3)). [resolve(3100,a,60,a)]. given #432 (T,wt=9): 3187 Shorter(c3 * x,f11(c5,c3) * x). [resolve(3100,a,58,a)]. given #433 (A,wt=18): 134 -Power(x,y * (x * z)) | Power(y,f8(y * (x * z),x,y,z)). [resolve(51,b,32,a)]. given #434 (F,wt=7): 3678 -Shorter(f11(c7 * x,c7),c3). [ur(55,a,3281,a,c,650,a)]. given #435 (F,wt=7): 3697 -Shorter(f11(c3 * x,c3),c7). [ur(55,a,3281,a,c,557,a)]. given #436 (F,wt=7): 3723 -Shorter(f11(c3 * c5,c5),c5). [resolve(3711,a,54,b)]. given #437 (F,wt=7): 3754 f11(c7,c7) * x != c3. [ur(67,a,3333,a)]. given #438 (T,wt=9): 3198 Shorter(c7,f11(x * c3,x * c3)). [resolve(3180,a,2716,a)]. given #439 (T,wt=9): 3199 Shorter(c7,f11(c3 * x,c3 * x)). [resolve(3180,a,2617,a)]. given #440 (T,wt=9): 3200 Shorter(c3,f11(c7 * x,c7 * x)). [resolve(3180,a,2061,a)]. given #441 (T,wt=9): 3201 Shorter(c3,f11(x * c7,x * c7)). [resolve(3180,a,1329,a)]. given #442 (A,wt=23): 135 -Power(x * y,z) | -Power(u * (x * (y * w)),z) | Power(u,f8(z,x * y,u,w)). [para(26(a,1),51(b,1,2))]. given #443 (F,wt=7): 3755 f11(c3,c3) * x != c7. [ur(67,a,3608,a)]. given #444 (F,wt=7): 3756 -Prefix(x * f11(c5,c3),c3). [ur(69,b,3195,a)]. given #445 (F,wt=7): 3764 -Prefix(f11(c5,c3) * x,c3). [ur(69,b,3196,a)]. given #446 (F,wt=7): 3845 -Prefix(x * f11(y,y),y). [ur(69,b,3217,a)]. given #447 (T,wt=9): 3202 Shorter(x,f11(y * x,y * x)). [resolve(3180,a,145,a)]. given #448 (T,wt=9): 3204 Shorter(x,f11(x * y,x * y)). [resolve(3180,a,141,a)]. given #449 (T,wt=9): 3206 Shorter(x * y,f11(y,y) * x). [resolve(3180,a,64,a)]. given #450 (T,wt=7): 4512 Shorter(c7,f11(c3,c3) * x). [resolve(3206,a,2716,a)]. given #451 (A,wt=23): 136 -Power(x,y) | -Power(z * (u * (x * w)),y) | Power(z * u,f8(y,x,z * u,w)). [para(26(a,1),51(b,1))]. given #452 (F,wt=7): 3861 -Prefix(f11(x,x) * y,x). [ur(69,b,3218,a)]. given #453 (F,wt=7): 3872 -Prefix(x * f11(c5,c3),c7). [ur(69,b,3308,a)]. given #454 (F,wt=7): 3883 -Prefix(f11(c5,c3) * x,c7). [ur(69,b,3309,a)]. given #455 (F,wt=7): 3954 -Prefix(x * f11(c7,c7),c3). [ur(69,b,3331,a)]. given #456 (T,wt=7): 4513 Shorter(c3,f11(c7,c7) * x). [resolve(3206,a,1329,a)]. given #457 (T,wt=9): 3207 Shorter(x * y,y * f11(x,x)). [resolve(3180,a,62,a)]. given #458 (T,wt=5): 4616 Shorter(c7,f11(c3,c3)). [resolve(3207,a,254,b)]. given #459 (T,wt=7): 4614 Shorter(c7,x * f11(c3,c3)). [resolve(3207,a,2617,a)]. given #460 (A,wt=18): 137 -Power(x,y * (x * z)) | Power(z,f8(y * (x * z),x,y,z)). [resolve(52,b,32,a)]. given #461 (F,wt=7): 3965 -Prefix(f11(c7,c7) * x,c3). [ur(69,b,3332,a)]. given #462 (F,wt=7): 3974 -Prefix(x * f11(c3,c3),c7). [ur(69,b,3428,a)]. given #463 (F,wt=7): 3985 -Prefix(f11(c3,c3) * x,c7). [ur(69,b,3504,a)]. given #464 (F,wt=7): 4178 -Prefix(f11(x * y,x),x). [ur(69,b,3637,a)]. given #465 (T,wt=7): 4615 Shorter(c3,x * f11(c7,c7)). [resolve(3207,a,2061,a)]. given #466 (T,wt=8): 4660 -Shorter(x,c7) | Shorter(x,f11(c3,c3)). [resolve(4616,a,55,b)]. given #467 (T,wt=8): 4661 -Shorter(f11(c3,c3),x) | Shorter(c7,x). [resolve(4616,a,55,a)]. given #468 (T,wt=9): 3208 Shorter(x * y,x * f11(y,y)). [resolve(3180,a,60,a)]. given #469 (A,wt=23): 138 -Power(x * y,z) | -Power(u * (x * (y * w)),z) | Power(w,f8(z,x * y,u,w)). [para(26(a,1),52(b,1,2))]. given #470 (F,wt=7): 4232 -Prefix(f11(c7 * x,c7),c3). [ur(69,b,3678,a)]. given #471 (F,wt=7): 4247 -Prefix(f11(c3 * x,c3),c7). [ur(69,b,3697,a)]. given #472 (F,wt=7): 4261 -Prefix(f11(c3 * c5,c5),c5). [ur(69,b,3723,a)]. given #473 (F,wt=9): 2155 -Prefix(x * (y * c7),c3 * x). [ur(69,b,707,a)]. given #474 (T,wt=9): 3209 Shorter(x * y,f11(x,x) * y). [resolve(3180,a,58,a)]. given #475 (T,wt=9): 3343 Shorter(c3,x * (y * f11(c5,c3))). [resolve(3182,a,144,a)]. given #476 (T,wt=9): 3344 Shorter(c3,x * (f11(c5,c3) * y)). [resolve(3182,a,140,a),rewrite([26(6)])]. given #477 (T,wt=9): 3366 Shorter(x,y * (z * f11(x,x))). [resolve(3203,a,144,a)]. given #478 (A,wt=21): 139 -Power(x,y) | -Power(z * (u * (x * w)),y) | Power(w,f8(y,x,z * u,w)). [para(26(a,1),52(b,1))]. given #479 (F,wt=9): 2162 -Prefix(x * (c7 * y),y * c3). [ur(69,b,708,a)]. given #480 (F,wt=9): 2167 -Prefix(x * (y * c7),x * c3). [ur(69,b,709,a)]. given #481 (F,wt=9): 2176 -Prefix(x * (c7 * y),c3 * y). [ur(69,b,710,a)]. given #482 (F,wt=9): 2224 -Prefix(x * (c7 * y),c3 * x). [ur(69,b,714,a)]. given #483 (T,wt=9): 3368 Shorter(x,y * (f11(x,x) * z)). [resolve(3203,a,140,a),rewrite([26(3)])]. given #484 (T,wt=9): 3628 Shorter(x,y * f11(x * z,x)). [resolve(3281,a,144,a)]. given #485 (T,wt=9): 3630 Shorter(x,f11(x * y,x) * z). [resolve(3281,a,140,a)]. given #486 (T,wt=9): 3715 Shorter(c5,x * f11(c3 * c5,c5)). [resolve(3711,a,144,a)]. given #487 (A,wt=14): 149 Shorter(x * y,z) | -Shorter(x * (y * u),z * u). [para(26(a,1),59(b,1))]. given #488 (F,wt=9): 2236 -Prefix(c7 * (x * y),y * c3). [ur(69,b,715,a)]. given #489 (F,wt=9): 2326 -Prefix(x * (c7 * y),x * c3). [ur(69,b,716,a)]. given #490 (F,wt=9): 2332 -Prefix(c7 * (x * y),c3 * y). [ur(69,b,717,a)]. given #491 (F,wt=9): 2352 -Shorter(c7 * (c7 * x),c3 * c3). [ur(55,b,2057,a,c,661,a)]. given #492 (T,wt=9): 3716 Shorter(c5,f11(c3 * c5,c5) * x). [resolve(3711,a,140,a)]. given #493 (T,wt=9): 3775 Shorter(c3,f11(f11(c5,c3),f11(c5,c3))). [resolve(3189,a,3180,a)]. given #494 (T,wt=9): 3784 Shorter(x,f11(f11(x,x),f11(x,x))). [resolve(3210,a,3180,a)]. given #495 (T,wt=9): 3831 Shorter(x,f11(f8(x,x,x,x),x)). [resolve(3082,a,69,a)]. given #496 (A,wt=14): 150 Shorter(x,y * z) | -Shorter(x * u,y * (z * u)). [para(26(a,1),59(b,2))]. given #497 (F,wt=9): 2389 -Prefix(x * (y * c3),c7 * y). [ur(69,b,833,a)]. given #498 (F,wt=9): 2397 -Prefix(x * (y * c3),y * c7). [ur(69,b,839,a)]. given #499 (F,wt=9): 2404 -Prefix(c3 * (x * y),c7 * x). [ur(69,b,841,a)]. given #500 (F,wt=9): 2501 -Prefix(c3 * (x * y),x * c7). [ur(69,b,844,a)]. given #501 (T,wt=9): 3893 Shorter(c5,f11(f8(c5,c5,c3,c4),c5)). [resolve(3086,a,69,a)]. given #502 (T,wt=9): 3897 Shorter(c3,f11(f8(c5,c5,c3,c4),c3)). [resolve(3087,a,69,a)]. given #503 (T,wt=9): 3901 Shorter(c4,f11(f8(c5,c5,c3,c4),c4)). [resolve(3088,a,69,a)]. given #504 (T,wt=9): 3994 Shorter(c7,x * (f11(c5,c3) * y)). [resolve(3904,a,144,a)]. given #505 (A,wt=14): 151 Shorter(x,y) | -Shorter(z * (u * x),z * (u * y)). [para(26(a,1),61(b,1)),rewrite([26(5)])]. given #506 (F,wt=9): 2507 -Prefix(c3 * (c5 * c3),c7 * c7). [ur(69,b,850,a)]. given #507 (F,wt=9): 2516 -Prefix(c3 * (c3 * c5),c7 * c7). [ur(69,b,888,a)]. given #508 (F,wt=9): 2586 -Prefix(x * (y * c7),c3 * y). [ur(69,b,1024,a)]. given #509 (F,wt=9): 2594 -Prefix(x * (y * c7),y * c3). [ur(69,b,1030,a)]. given #510 (T,wt=9): 4024 Shorter(c7,f11(f11(c5,c3),f11(c5,c3))). [resolve(4003,a,3210,a)]. given #511 (T,wt=9): 4025 Shorter(x * c7,f11(c5,c3) * x). [resolve(4003,a,64,a)]. given #512 (T,wt=9): 4026 Shorter(c7 * x,x * f11(c5,c3)). [resolve(4003,a,62,a)]. given #513 (T,wt=9): 4027 Shorter(x * c7,x * f11(c5,c3)). [resolve(4003,a,60,a)]. given #514 (A,wt=14): 155 Shorter(x * y,z) | -Shorter(x * (y * u),u * z). [para(26(a,1),63(b,1))]. given #515 (F,wt=9): 2601 -Prefix(c7 * (x * y),c3 * x). [ur(69,b,1033,a)]. given #516 (F,wt=9): 2673 -Prefix(c7 * (x * y),x * c3). [ur(69,b,1036,a)]. given #517 (F,wt=9): 2775 -Shorter(c3 * (x * c3),c7 * c7). [ur(55,a,2612,a,c,566,a)]. given #518 (F,wt=9): 2843 c7 * (c3 * c5) != c5 * c3. [para(87(a,1),1352(a,1,2))]. given #519 (T,wt=9): 4028 Shorter(c7 * x,f11(c5,c3) * x). [resolve(4003,a,58,a)]. given #520 (T,wt=9): 4032 Shorter(c7,x * (y * f11(c5,c3))). [resolve(4002,a,144,a)]. given #521 (T,wt=9): 4044 Power(c5,f8(c5,c5,c5 * c3,c4)). [resolve(133,b,431,a),unit_del(a,32)]. given #522 (T,wt=9): 4047 Power(x,f8(x,x,x * x,x)). [resolve(133,b,284,a),unit_del(a,32)]. given #523 (A,wt=14): 156 Shorter(x,y) | -Shorter(x * (z * u),z * (u * y)). [para(26(a,1),63(b,2))]. given #524 (F,wt=9): 2862 -Shorter(c3 * (c3 * x),c7 * c7). [ur(55,b,2613,a,c,566,a)]. given #525 (F,wt=9): 2884 -Shorter(x * (c3 * c3),c7 * c7). [ur(55,a,2711,a,c,566,a)]. given #526 (F,wt=9): 3067 -Prefix(x * (c7 * c7),c3 * c3). [ur(69,b,2024,a)]. given #527 (F,wt=9): 3169 -Prefix(c7 * (x * c7),c3 * c3). [ur(69,b,2069,a)]. given #528 (T,wt=9): 4365 Power(x,f8(x,x * x,x,x)). [resolve(135,b,284,a),unit_del(a,175)]. given #529 (T,wt=9): 4572 Shorter(c3 * c5,f11(c7,c7) * c5). [para(87(a,1),3206(a,1))]. given #530 (T,wt=5): 6031 Shorter(c3,f11(c7,c7)). [resolve(4572,a,59,b)]. given #531 (T,wt=8): 6048 -Shorter(x,c3) | Shorter(x,f11(c7,c7)). [resolve(6031,a,55,b)]. given #532 (A,wt=14): 158 Shorter(x,y) | -Shorter(z * (u * x),y * (z * u)). [para(26(a,1),65(b,1))]. given #533 (F,wt=9): 3193 -Shorter(x * (y * f11(c5,c3)),c3). [ur(55,b,3100,a,c,276,a)]. given #534 (F,wt=9): 3194 -Shorter(x * (f11(c5,c3) * y),c3). [ur(55,b,3100,a,c,273,a)]. given #535 (F,wt=9): 3215 -Shorter(x * (y * f11(z,z)),z). [ur(55,b,3180,a,c,276,a)]. given #536 (F,wt=9): 3216 -Shorter(x * (f11(y,y) * z),y). [ur(55,b,3180,a,c,273,a)]. given #537 (T,wt=8): 6049 -Shorter(f11(c7,c7),x) | Shorter(c3,x). [resolve(6031,a,55,a)]. given #538 (T,wt=9): 4574 Shorter(c7,x * (f11(c3,c3) * y)). [resolve(4512,a,144,a)]. given #539 (T,wt=9): 4606 Shorter(c3,x * (f11(c7,c7) * y)). [resolve(4513,a,144,a)]. given #540 (T,wt=9): 4654 Shorter(c3 * c5,c7 * f11(c5,c5)). [para(87(a,1),3207(a,1))]. given #541 (A,wt=14): 159 Shorter(x,y * z) | -Shorter(u * x,y * (z * u)). [para(26(a,1),65(b,2))]. given #542 (F,wt=9): 3245 -Shorter(f11(c7 * x,c7 * x),c3). [ur(55,a,3180,a,c,656,a)]. given #543 (F,wt=9): 3246 -Shorter(f11(x * c7,x * c7),c3). [ur(55,a,3180,a,c,655,a)]. given #544 (F,wt=9): 3264 -Shorter(f11(c3 * x,c3 * x),c7). [ur(55,a,3180,a,c,561,a)]. given #545 (F,wt=9): 3265 -Shorter(f11(x * c3,x * c3),c7). [ur(55,a,3180,a,c,560,a)]. given #546 (T,wt=9): 4655 Shorter(c7,f11(f11(c3,c3),f11(c3,c3))). [resolve(4616,a,3210,a)]. given #547 (T,wt=9): 4656 Shorter(x * c7,f11(c3,c3) * x). [resolve(4616,a,64,a)]. given #548 (T,wt=9): 4657 Shorter(c7 * x,x * f11(c3,c3)). [resolve(4616,a,62,a)]. given #549 (T,wt=9): 4658 Shorter(x * c7,x * f11(c3,c3)). [resolve(4616,a,60,a)]. given #550 (A,wt=12): 164 Prefix(x * y,z) | x * (y * u) != z. [para(26(a,1),67(b,1))]. given #551 (F,wt=9): 3277 -Shorter(f11(x * y,x * y),y). [ur(55,a,3180,a,c,146,a)]. given #552 (F,wt=9): 3278 -Shorter(f11(x * y,x * y),x). [ur(55,a,3180,a,c,142,a)]. given #553 (F,wt=9): 3303 -Shorter(x * f11(c5,c3),c3 * x). [ur(65,a,3190,a)]. given #554 (F,wt=9): 3304 -Shorter(f11(c5,c3) * x,x * c3). [ur(63,a,3190,a)]. given #555 (T,wt=9): 4659 Shorter(c7 * x,f11(c3,c3) * x). [resolve(4616,a,58,a)]. given #556 (T,wt=9): 4663 Shorter(c7,x * (y * f11(c3,c3))). [resolve(4614,a,144,a)]. given #557 (T,wt=9): 4683 Shorter(c3,x * (y * f11(c7,c7))). [resolve(4615,a,144,a)]. given #558 (T,wt=9): 4779 Shorter(c3 * c5,f11(c5,c5) * c7). [para(87(a,1),3209(a,1))]. given #559 (A,wt=24): 165 x * (y * z) != u * w | Prefix(u,x * y) | Prefix(x * y,u) | x * y = u. [para(26(a,1),68(a,1))]. given #560 (F,wt=9): 3305 -Shorter(x * f11(c5,c3),x * c3). [ur(61,a,3190,a)]. given #561 (F,wt=9): 3306 -Shorter(f11(c5,c3) * x,c3 * x). [ur(59,a,3190,a)]. given #562 (F,wt=9): 3307 -Shorter(f11(f11(c5,c3),f11(c5,c3)),c3). [ur(55,a,3180,a,c,3190,a)]. given #563 (F,wt=9): 3311 -Shorter(x * f11(c5,c3),c7 * x). [ur(65,a,3197,a)]. given #564 (T,wt=9): 4900 Power(c4,f8(c5,c5,c5 * c3,c4)). [resolve(139,b,431,a),unit_del(a,32)]. given #565 (T,wt=9): 5712 Shorter(c7 * x,c3 * (x * y)). [resolve(155,b,2714,a)]. given #566 (T,wt=9): 5713 Shorter(c7 * x,y * (x * c3)). [resolve(155,b,2615,a)]. given #567 (T,wt=9): 5714 Shorter(c3 * x,y * (x * c7)). [resolve(155,b,2059,a)]. given #568 (A,wt=18): 166 x * (y * z) != u * w | Prefix(x,u) | Prefix(u,x) | u = x. [para(26(a,2),68(a,2)),rewrite([26(3)]),flip(a)]. given #569 (F,wt=9): 3312 -Shorter(f11(c5,c3) * x,x * c7). [ur(63,a,3197,a)]. given #570 (F,wt=9): 3313 -Shorter(x * f11(c5,c3),x * c7). [ur(61,a,3197,a)]. given #571 (F,wt=9): 3314 -Shorter(f11(c5,c3) * x,c7 * x). [ur(59,a,3197,a)]. given #572 (F,wt=9): 3315 -Shorter(f11(f11(c5,c3),f11(c5,c3)),c7). [ur(55,a,3180,a,c,3197,a)]. given #573 (T,wt=9): 5715 Shorter(c3 * x,c7 * (x * y)). [resolve(155,b,1327,a)]. given #574 (T,wt=9): 6043 Shorter(c3,f11(f11(c7,c7),f11(c7,c7))). [resolve(6031,a,3210,a)]. given #575 (T,wt=9): 6044 Shorter(x * c3,f11(c7,c7) * x). [resolve(6031,a,64,a)]. given #576 (T,wt=9): 6045 Shorter(c3 * x,x * f11(c7,c7)). [resolve(6031,a,62,a)]. given #577 (A,wt=28): 168 c3 * c5 != x * y | c3 = x | c3 * f1(c3,x,c5,y) = x | f2(c3,x,c5,y) * c5 = y. [para(79(a,1),31(a,2)),rewrite([167(10),167(15),167(17)]),flip(a),flip(b)]. given #578 (F,wt=9): 3318 -Shorter(x * (f11(c5,c3) * y),c7). [ur(55,a,328,a,c,3197,a)]. given #579 (F,wt=9): 3319 -Shorter(x * (y * f11(c5,c3)),c7). [ur(55,a,147,a,c,3197,a)]. given #580 (F,wt=9): 3325 -Shorter(x * f11(y,y),y * x). [ur(65,a,3212,a)]. given #581 (F,wt=9): 3326 -Shorter(f11(x,x) * y,y * x). [ur(63,a,3212,a)]. given #582 (T,wt=9): 6046 Shorter(x * c3,x * f11(c7,c7)). [resolve(6031,a,60,a)]. given #583 (T,wt=9): 6047 Shorter(c3 * x,f11(c7,c7) * x). [resolve(6031,a,58,a)]. given #584 (T,wt=10): 282 -Power(x * y,z) | Power(f11(z,x),z). [resolve(163,a,82,b)]. given #585 (T,wt=5): 6975 Power(f11(c5,c3),c5). [resolve(282,a,504,a)]. given #586 (A,wt=11): 170 x * (c5 * c3) != x * (c3 * c5). [ur(27,b,80,a)]. given #587 (F,wt=9): 3327 -Shorter(x * f11(y,y),x * y). [ur(61,a,3212,a)]. given #588 (F,wt=9): 3328 -Shorter(f11(x,x) * y,x * y). [ur(59,a,3212,a)]. given #589 (F,wt=9): 3329 -Shorter(f11(f11(x,x),f11(x,x)),x). [ur(55,b,3180,a,c,3212,a)]. given #590 (F,wt=9): 3334 -Shorter(x * f11(c7,c7),c3 * x). [ur(65,a,3247,a)]. given #591 (T,wt=5): 6980 Power(f11(x,x),x). [resolve(282,a,429,a)]. given #592 (T,wt=7): 7005 Power(f11(c5,c3) * c5,c5). [resolve(6975,a,100,a)]. given #593 (T,wt=7): 7006 Power(c5 * f11(c5,c3),c5). [resolve(6975,a,99,a)]. given #594 (T,wt=7): 7104 Power(f11(x,x) * x,x). [resolve(6980,a,100,a)]. given #595 (A,wt=15): 171 f10(x,y * (z * x)) * x = y * (z * x). [resolve(81,a,26,a)]. given #596 (F,wt=9): 3335 -Shorter(f11(c7,c7) * x,x * c3). [ur(63,a,3247,a)]. given #597 (F,wt=9): 3336 -Shorter(x * f11(c7,c7),x * c3). [ur(61,a,3247,a)]. given #598 (F,wt=9): 3337 -Shorter(f11(c7,c7) * x,c3 * x). [ur(59,a,3247,a)]. given #599 (F,wt=9): 3338 -Shorter(f11(f11(c7,c7),f11(c7,c7)),c3). [ur(55,a,3180,a,c,3247,a)]. given #600 (T,wt=7): 7105 Power(x * f11(x,x),x). [resolve(6980,a,99,a)]. given #601 (T,wt=7): 7121 Power(f11(c5,f11(c5,c3)),c5). [resolve(7005,a,282,a)]. given #602 (T,wt=7): 7169 Power(f11(x,f11(x,x)),x). [resolve(7104,a,282,a)]. given #603 (T,wt=8): 7020 -Power(x,f11(c5,c3)) | Power(x,c5). [resolve(6975,a,33,b)]. given #604 (A,wt=11): 173 f10(x,y * x) * x = y * x. [xx_res(81,a)]. given #605 (F,wt=9): 3341 -Shorter(x * (f11(c7,c7) * y),c3). [ur(55,a,328,a,c,3247,a)]. given #606 (F,wt=9): 3342 -Shorter(x * (y * f11(c7,c7)),c3). [ur(55,a,147,a,c,3247,a)]. given #607 (F,wt=9): 3609 -Shorter(x * f11(c3,c3),c7 * x). [ur(65,a,3266,a)]. given #608 (F,wt=9): 3610 -Shorter(f11(c3,c3) * x,x * c7). [ur(63,a,3266,a)]. given #609 (T,wt=7): 7366 f10(x,y * x) = y. [resolve(173,a,28,a)]. given #610 (T,wt=7): 7410 f10(c7,c3 * c5) = c5. [para(87(a,1),7366(a,1,2))]. given #611 (T,wt=8): 7021 -Power(c5,x) | Power(f11(c5,c3),x). [resolve(6975,a,33,a)]. given #612 (T,wt=8): 7119 -Power(x,f11(y,y)) | Power(x,y). [resolve(6980,a,33,b)]. given #613 (A,wt=14): 174 x * (y * z) != u | f10(z,u) * z = u. [para(26(a,1),81(a,1))]. given #614 (F,wt=9): 3611 -Shorter(x * f11(c3,c3),x * c7). [ur(61,a,3266,a)]. given #615 (F,wt=9): 3612 -Shorter(f11(c3,c3) * x,c7 * x). [ur(59,a,3266,a)]. given #616 (F,wt=9): 3615 -Shorter(f11(f11(c3,c3),f11(c3,c3)),c7). [ur(55,a,3180,a,c,3266,a)]. given #617 (F,wt=9): 3618 -Shorter(x * (f11(c3,c3) * y),c7). [ur(55,a,328,a,c,3266,a)]. given #618 (T,wt=8): 7120 -Power(x,y) | Power(f11(x,x),y). [resolve(6980,a,33,a)]. given #619 (T,wt=9): 6994 Power(f11(x * y,x),x * y). [resolve(282,a,32,a)]. given #620 (T,wt=7): 7567 Power(f11(x * x,x),x). [resolve(6994,a,300,a)]. given #621 (T,wt=9): 7007 Power(f11(c5,c3) * f11(c5,c3),c5). [resolve(6975,a,84,a)]. given #622 (A,wt=13): 176 Power(c3 * (c5 * (c4 * (c3 * (c5 * c4)))),c5). [resolve(85,a,84,a),rewrite([26(11),26(10)])]. given #623 (F,wt=9): 3619 -Shorter(x * (y * f11(c3,c3)),c7). [ur(55,a,147,a,c,3266,a)]. given #624 (F,wt=9): 3643 -Shorter(x * f11(y * z,y),y). [ur(55,b,3281,a,c,146,a)]. given #625 (F,wt=9): 3644 -Shorter(f11(x * y,x) * z,x). [ur(55,b,3281,a,c,142,a)]. given #626 (F,wt=9): 3729 -Shorter(x * f11(c3 * c5,c5),c5). [ur(55,b,3711,a,c,146,a)]. given #627 (T,wt=9): 7091 Power(f11(x * x,x * x),x). [resolve(6980,a,300,a)]. given #628 (T,wt=9): 7106 Power(f11(x,x) * f11(x,x),x). [resolve(6980,a,84,a)]. given #629 (T,wt=9): 7122 Prefix(f11(c5,c3),f11(c5,f11(c5,c3))). [resolve(7005,a,281,a)]. given #630 (T,wt=9): 7129 Power(f11(c5,c3) * (c5 * c5),c5). [resolve(7005,a,100,a),rewrite([26(7)])]. given #631 (A,wt=23): 180 Power(c5 * c4,c5) | f5(c3,c5 * c4,c5) = c5 * c4 | Power(f7(c3,c5 * c4,c5),c5). [resolve(85,a,49,a)]. given #632 (F,wt=9): 3730 -Shorter(f11(c3 * c5,c5) * x,c5). [ur(55,b,3711,a,c,142,a)]. given #633 (F,wt=9): 3921 -Shorter(f11(c5,c3) * c7,c3 * c3). [ur(55,b,3184,a,c,660,a)]. given #634 (F,wt=9): 3922 -Shorter(c7 * f11(c5,c3),c3 * c3). [ur(55,b,3184,a,c,659,a)]. given #635 (F,wt=9): 4230 -Shorter(x * f11(c7 * y,c7),c3). [ur(145,b,3678,a)]. given #636 (T,wt=9): 7130 Power(c5 * (f11(c5,c3) * c5),c5). [resolve(7005,a,99,a)]. given #637 (T,wt=9): 7152 Power(c5 * (c5 * f11(c5,c3)),c5). [resolve(7006,a,99,a)]. given #638 (T,wt=9): 7170 Prefix(f11(x,x),f11(x,f11(x,x))). [resolve(7104,a,281,a)]. given #639 (T,wt=9): 7195 Power(f11(x,x) * (x * x),x). [resolve(7104,a,100,a),rewrite([26(3)])]. given #640 (A,wt=32): 181 Power(c5 * c4,c5) | f5(c3,c5 * c4,c5) = c5 * c4 | f5(c3,c5 * c4,c5) * f7(c3,c5 * c4,c5) = c5 * c4. [resolve(85,a,48,a)]. given #641 (F,wt=9): 4231 -Shorter(f11(c7 * x,c7) * y,c3). [ur(141,b,3678,a)]. given #642 (F,wt=9): 4245 -Shorter(x * f11(c3 * y,c3),c7). [ur(145,b,3697,a)]. given #643 (F,wt=9): 4246 -Shorter(f11(c3 * x,c3) * y,c7). [ur(141,b,3697,a)]. given #644 (F,wt=9): 4410 x * (f11(c5,c3) * y) != c3. [ur(67,a,3756,a),rewrite([26(5)])]. given #645 (T,wt=9): 7196 Power(x * (f11(x,x) * x),x). [resolve(7104,a,99,a)]. given #646 (T,wt=9): 7275 Power(x * (x * f11(x,x)),x). [resolve(7105,a,99,a)]. given #647 (T,wt=9): 7302 Power(f11(c5,f11(c5,c3)) * c5,c5). [resolve(7121,a,100,a)]. given #648 (T,wt=9): 7303 Power(c5 * f11(c5,f11(c5,c3)),c5). [resolve(7121,a,99,a)]. given #649 (A,wt=21): 182 Power(c5 * c4,c5) | f4(c3,c5 * c4,c5) = c3 | Power(f6(c3,c5 * c4,c5),c5). [resolve(85,a,47,a)]. given #650 (F,wt=9): 4411 -Prefix(x * (y * f11(c5,c3)),c3). [para(26(a,1),3756(a,1))]. given #651 (F,wt=9): 4412 x * (f11(y,y) * z) != y. [ur(67,a,3845,a),rewrite([26(3)])]. given #652 (F,wt=9): 4413 -Prefix(x * (y * f11(z,z)),z). [para(26(a,1),3845(a,1))]. given #653 (F,wt=9): 4533 -Shorter(f11(x,x) * c7,c3 * x). [ur(55,b,3206,a,c,660,a)]. given #654 (T,wt=9): 7332 Power(f11(x,f11(x,x)) * x,x). [resolve(7169,a,100,a)]. given #655 (T,wt=9): 7333 Power(x * f11(x,f11(x,x)),x). [resolve(7169,a,99,a)]. given #656 (T,wt=9): 7352 Power(f11(f11(c5,c3),f11(c5,c3)),c5). [resolve(7020,a,6980,a)]. given #657 (T,wt=9): 7449 Power(f11(c5,c3),f8(c5,c5,c5,c5)). [resolve(7021,a,454,a)]. given #658 (A,wt=28): 183 Power(c5 * c4,c5) | f4(c3,c5 * c4,c5) = c3 | f6(c3,c5 * c4,c5) * f4(c3,c5 * c4,c5) = c3. [resolve(85,a,46,a)]. given #659 (F,wt=9): 4534 -Shorter(c7 * f11(x,x),c3 * x). [ur(55,b,3206,a,c,659,a)]. given #660 (F,wt=9): 4539 -Shorter(f11(x,x) * c3,c7 * x). [ur(55,b,3206,a,c,565,a)]. given #661 (F,wt=9): 4540 -Shorter(c3 * f11(x,x),c7 * x). [ur(55,b,3206,a,c,564,a)]. given #662 (F,wt=9): 4559 -Shorter(f11(x,x) * c7,x * c3). [ur(55,a,3206,a,c,659,a)]. given #663 (T,wt=9): 7450 Power(f11(c5,c3),f8(c5,c5,c3,c4)). [resolve(7021,a,179,a)]. given #664 (T,wt=9): 7464 Power(f11(f11(x,x),f11(x,x)),x). [resolve(7119,a,6980,a)]. given #665 (T,wt=9): 7541 Power(f11(x,x),f8(x,x,x,x)). [resolve(7120,a,454,a)]. given #666 (T,wt=9): 7549 Power(f11(c5,c5),f8(c5,c5,c3,c4)). [resolve(7120,a,179,a)]. given #667 (A,wt=20): 184 Power(c5 * c4,c5) | f4(c3,c5 * c4,c5) * f5(c3,c5 * c4,c5) = c5. [resolve(85,a,45,a)]. given #668 (F,wt=9): 4566 -Shorter(f11(x,x) * c3,x * c7). [ur(55,a,3206,a,c,564,a)]. given #669 (F,wt=9): 4601 x * (f11(c5,c3) * y) != c7. [ur(67,a,3872,a),rewrite([26(5)])]. given #670 (F,wt=9): 4602 -Prefix(x * (y * f11(c5,c3)),c7). [para(26(a,1),3872(a,1))]. given #671 (F,wt=9): 4603 x * (f11(c7,c7) * y) != c3. [ur(67,a,3954,a),rewrite([26(5)])]. given #672 (T,wt=9): 7550 Power(f11(c3,c3),f8(c5,c5,c3,c4)). [resolve(7120,a,178,a)]. given #673 (T,wt=9): 7551 Power(f11(c4,c4),f8(c5,c5,c3,c4)). [resolve(7120,a,177,a)]. given #674 (T,wt=9): 7568 Power(f11(c3 * (c5 * c2),c3),c3). [resolve(6994,a,225,a)]. given #675 (T,wt=9): 7569 Power(f11(c3 * (c5 * c4),c3),c5). [resolve(6994,a,202,a)]. given #676 (A,wt=21): 185 Power(c3,c5) | f5(c3,c5 * c4,c5) = c5 * c4 | Power(f7(c3,c5 * c4,c5),c5). [resolve(85,a,44,a)]. given #677 (F,wt=9): 4604 -Prefix(x * (y * f11(c7,c7)),c3). [para(26(a,1),3954(a,1))]. given #678 (F,wt=9): 4635 -Shorter(c7 * f11(x,x),x * c3). [ur(55,b,3207,a,c,661,a)]. given #679 (F,wt=9): 4640 -Shorter(c3 * f11(x,x),x * c7). [ur(55,b,3207,a,c,566,a)]. given #680 (F,wt=9): 4678 x * (f11(c3,c3) * y) != c7. [ur(67,a,3974,a),rewrite([26(5)])]. given #681 (T,wt=9): 7598 Power(f11(c3 * c5,c5),c3 * c5). [para(87(a,1),6994(a,1,1)),rewrite([87(8)])]. given #682 (T,wt=9): 7615 Power(f11(x * x,x) * x,x). [resolve(7567,a,100,a)]. given #683 (T,wt=9): 7616 Power(x * f11(x * x,x),x). [resolve(7567,a,99,a)]. given #684 (T,wt=9): 7845 Shorter(f11(c5,c3),f11(c5,f11(c5,c3))). [resolve(7122,a,69,a)]. given #685 (A,wt=30): 186 Power(c3,c5) | f5(c3,c5 * c4,c5) = c5 * c4 | f5(c3,c5 * c4,c5) * f7(c3,c5 * c4,c5) = c5 * c4. [resolve(85,a,43,a)]. given #686 (F,wt=7): 9776 -Shorter(f11(c5,f11(c5,c3)),c7). [ur(55,a,7845,a,c,3197,a)]. given #687 (F,wt=7): 9777 -Shorter(f11(c5,f11(c5,c3)),c3). [ur(55,a,7845,a,c,3190,a)]. given #688 (F,wt=7): 9824 -Prefix(f11(c5,f11(c5,c3)),c7). [ur(69,b,9776,a)]. given #689 (F,wt=7): 9850 -Prefix(f11(c5,f11(c5,c3)),c3). [ur(69,b,9777,a)]. given #690 (T,wt=7): 9747 Shorter(c7,f11(c5,f11(c5,c3))). [resolve(7845,a,4030,a)]. given #691 (T,wt=7): 9749 Shorter(c3,f11(c5,f11(c5,c3))). [resolve(7845,a,3189,a)]. given #692 (T,wt=9): 7857 Power(c5,f8(c5,c5,f11(c5,c3),c5)). [resolve(7129,a,52,b),unit_del(a,32)]. given #693 (T,wt=9): 8025 Power(c5,f8(c5,f11(c5,c3),c5,c5)). [resolve(7130,a,52,b),unit_del(a,6975)]. given #694 (A,wt=19): 187 Power(c3,c5) | f4(c3,c5 * c4,c5) = c3 | Power(f6(c3,c5 * c4,c5),c5). [resolve(85,a,42,a)]. given #695 (F,wt=9): 4679 -Prefix(x * (y * f11(c3,c3)),c7). [para(26(a,1),3974(a,1))]. given #696 (F,wt=9): 4680 f11(x * y,x) * z != x. [ur(67,a,4178,a)]. given #697 (F,wt=9): 4753 f11(c7 * x,c7) * y != c3. [ur(67,a,4232,a)]. given #698 (F,wt=9): 4754 f11(c3 * x,c3) * y != c7. [ur(67,a,4247,a)]. given #699 (T,wt=9): 8051 Power(c5,f8(c5,c5,c5,f11(c5,c3))). [resolve(7152,a,51,b),unit_del(a,32)]. given #700 (T,wt=9): 8068 Shorter(f11(x,x),f11(x,f11(x,x))). [resolve(7170,a,69,a)]. given #701 (T,wt=7): 10325 Shorter(c3,f11(c7,f11(c7,c7))). [resolve(8068,a,6049,a)]. given #702 (T,wt=7): 10326 Shorter(c7,f11(c3,f11(c3,c3))). [resolve(8068,a,4661,a)]. given #703 (A,wt=26): 188 Power(c3,c5) | f4(c3,c5 * c4,c5) = c3 | f6(c3,c5 * c4,c5) * f4(c3,c5 * c4,c5) = c3. [resolve(85,a,41,a)]. given #704 (F,wt=7): 10362 -Shorter(f11(c3,f11(c3,c3)),c7). [ur(55,a,8068,a,c,3266,a)]. given #705 (F,wt=7): 10365 -Shorter(f11(c7,f11(c7,c7)),c3). [ur(55,a,8068,a,c,3247,a)]. given #706 (F,wt=7): 10368 -Shorter(f11(x,f11(x,x)),x). [ur(55,a,8068,a,c,3212,a)]. given #707 (F,wt=7): 10457 -Prefix(f11(c3,f11(c3,c3)),c7). [ur(69,b,10362,a)]. given #708 (T,wt=7): 10327 Shorter(x,f11(x,f11(x,x))). [resolve(8068,a,3211,a)]. given #709 (T,wt=9): 8091 Power(x,f8(x,x,f11(x,x),x)). [resolve(7195,a,52,b),unit_del(a,32)]. given #710 (T,wt=9): 8286 Power(x,f8(x,f11(x,x),x,x)). [resolve(7196,a,52,b),unit_del(a,6980)]. given #711 (T,wt=9): 8318 Power(x,f8(x,x,x,f11(x,x))). [resolve(7275,a,51,b),unit_del(a,32)]. given #712 (A,wt=18): 189 Power(c3,c5) | f4(c3,c5 * c4,c5) * f5(c3,c5 * c4,c5) = c5. [resolve(85,a,40,a)]. given #713 (F,wt=7): 10466 -Prefix(f11(c7,f11(c7,c7)),c3). [ur(69,b,10365,a)]. given #714 (F,wt=7): 10482 -Prefix(f11(x,f11(x,x)),x). [ur(69,b,10368,a)]. given #715 (F,wt=9): 4755 f11(c3 * c5,c5) * x != c5. [ur(67,a,4261,a)]. given #716 (F,wt=9): 5241 -Prefix(c7 * (c7 * x),c3 * c3). [ur(69,b,2352,a)]. given #717 (T,wt=9): 8335 Power(f11(c5,f11(c5,f11(c5,c3))),c5). [resolve(7302,a,282,a)]. given #718 (T,wt=9): 8629 Power(f11(x,f11(x,f11(x,x))),x). [resolve(7332,a,282,a)]. given #719 (T,wt=9): 9671 Power(f11(x,f11(x * x,x)),x). [resolve(7615,a,282,a)]. given #720 (T,wt=9): 9873 Shorter(c7,x * f11(c5,f11(c5,c3))). [resolve(9747,a,144,a)]. given #721 (A,wt=42): 190 -Power(x,c5) | c3 * (c5 * c4) = x | f3(c5,x,c3 * (c5 * c4)) * (c3 * (c5 * c4)) = x | f3(c5,x,c3 * (c5 * c4)) * x = c3 * (c5 * c4). [resolve(85,a,39,b)]. given #722 (F,wt=9): 5383 -Shorter(f11(f8(x,x,x,x),x),x). [resolve(3831,a,54,b)]. given #723 (F,wt=9): 5442 -Shorter(f11(f8(c7,c7,c7,c7),c7),c3). [ur(55,a,3831,a,c,650,a)]. given #724 (F,wt=9): 5461 -Shorter(f11(f8(c3,c3,c3,c3),c3),c7). [ur(55,a,3831,a,c,557,a)]. given #725 (F,wt=9): 5498 -Shorter(f11(f8(c5,c5,c3,c4),c5),c5). [resolve(3893,a,54,b)]. given #726 (T,wt=9): 9874 Shorter(c7,f11(c5,f11(c5,c3)) * x). [resolve(9747,a,140,a)]. given #727 (T,wt=9): 9882 Shorter(c3,x * f11(c5,f11(c5,c3))). [resolve(9749,a,144,a)]. given #728 (T,wt=9): 9883 Shorter(c3,f11(c5,f11(c5,c3)) * x). [resolve(9749,a,140,a)]. given #729 (T,wt=9): 10370 Shorter(c3,x * f11(c7,f11(c7,c7))). [resolve(10325,a,144,a)]. given #730 (A,wt=42): 191 -Power(x,c5) | c3 * (c5 * c4) = x | f3(c5,c3 * (c5 * c4),x) * x = c3 * (c5 * c4) | f3(c5,c3 * (c5 * c4),x) * (c3 * (c5 * c4)) = x. [resolve(85,a,39,a),flip(b)]. given #731 (F,wt=9): 5518 -Shorter(f11(f8(c5,c5,c3,c4),c3),c3). [resolve(3897,a,54,b)]. given #732 (F,wt=9): 5529 -Shorter(f11(f8(c5,c5,c3,c4),c3),c7). [ur(55,a,3897,a,c,557,a)]. given #733 (F,wt=9): 5539 -Shorter(f11(f8(c5,c5,c3,c4),c4),c4). [resolve(3901,a,54,b)]. given #734 (F,wt=9): 5671 -Shorter(f11(c5,c3) * c3,c7 * c7). [ur(55,b,4025,a,c,565,a)]. given #735 (T,wt=9): 10371 Shorter(c3,f11(c7,f11(c7,c7)) * x). [resolve(10325,a,140,a)]. given #736 (T,wt=9): 10396 Shorter(c7,x * f11(c3,f11(c3,c3))). [resolve(10326,a,144,a)]. given #737 (T,wt=9): 10397 Shorter(c7,f11(c3,f11(c3,c3)) * x). [resolve(10326,a,140,a)]. given #738 (T,wt=9): 10621 Shorter(x,y * f11(x,f11(x,x))). [resolve(10327,a,144,a)]. given #739 (A,wt=42): 192 -Power(x,c5) | c3 * (c5 * c4) = x | f3(c5,x,c3 * (c5 * c4)) * (c3 * (c5 * c4)) = x | x * f3(c5,x,c3 * (c5 * c4)) = c3 * (c5 * c4). [resolve(85,a,38,b)]. given #740 (F,wt=9): 5672 -Shorter(c3 * f11(c5,c3),c7 * c7). [ur(55,b,4025,a,c,564,a)]. given #741 (F,wt=9): 5725 -Prefix(c3 * (x * c3),c7 * c7). [ur(69,b,2775,a)]. given #742 (F,wt=9): 5932 -Prefix(c3 * (c3 * x),c7 * c7). [ur(69,b,2862,a)]. given #743 (F,wt=9): 5957 -Prefix(x * (c3 * c3),c7 * c7). [ur(69,b,2884,a)]. given #744 (T,wt=9): 10623 Shorter(x,f11(x,f11(x,x)) * y). [resolve(10327,a,140,a)]. given #745 (T,wt=10): 298 -Power(x,y) | Power(x * (y * y),y). [resolve(175,a,34,b)]. given #746 (T,wt=10): 299 -Power(x,y) | Power(y * (y * x),y). [resolve(175,a,34,a),rewrite([26(3)])]. given #747 (T,wt=10): 302 -Power(c3 * c5,x) | Prefix(c5,f11(x,c5)). [resolve(229,a,83,b)]. given #748 (A,wt=42): 193 -Power(x,c5) | c3 * (c5 * c4) = x | f3(c5,c3 * (c5 * c4),x) * x = c3 * (c5 * c4) | c3 * (c5 * (c4 * f3(c5,c3 * (c5 * c4),x))) = x. [resolve(85,a,38,a),rewrite([26(35),26(34)]),flip(b)]. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 3.14 (+ 0.02) seconds. % Length of proof is 30. % Level of proof is 6. % Maximum clause weight is 42.000. % Given clauses 748 (124.667 givens/level). 5 Power(y,x) & Power(z,x) -> Power(y * z,x) # label(non_clause). [assumption]. 6 Power(y,x) & Power(z,x) -> y = z | (exists u (Power(u,x) & (y = z * u & y = u * z | z = y * u & z = u * y))) # label(non_clause). [assumption]. 13 Shorter(x,y) <-> Shorter(x * z,z * y) # label(non_clause). [assumption]. 18 x * y = u * v -> Prefix(x,u) | Prefix(u,x) | x = u # label("Lemma 1") # label(non_clause). [assumption]. 19 Prefix(x,y) -> Shorter(x,y) # label("Lemma 2") # label(non_clause). [assumption]. 20 Power(u * u1,x) & Power(u * u2,y) & u = x * u3 & u = y * u4 & -Shorter(u,x * y) & u = x * y -> x * y = y * x # label("Case 1") # label(non_clause) # label(goal). [goal]. 26 (x * y) * z = x * (y * z). [assumption]. 30 x * y != y. [assumption]. 32 Power(x,x). [assumption]. 34 -Power(x,y) | -Power(z,y) | Power(x * z,y). [clausify(5)]. 38 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | x * f3(y,x,z) = z. [clausify(6)]. 53 -Shorter(x,x). [assumption]. 63 Shorter(x,y) | -Shorter(x * z,z * y). [clausify(13)]. 68 x * y != z * u | Prefix(z,x) | Prefix(x,z) | x = z # label("Lemma 1"). [clausify(18)]. 69 -Prefix(x,y) | Shorter(x,y) # label("Lemma 2"). [clausify(19)]. 71 Power(c1 * c4,c5) # label("Case 1"). [deny(20)]. 72 c3 * c6 = c1 # label("Case 1"). [deny(20)]. 73 c1 = c3 * c6. [copy(72),flip(a)]. 78 c3 * c5 = c1 # label("Case 1"). [deny(20)]. 79 c3 * c6 = c3 * c5. [copy(78),rewrite([73(4)]),flip(a)]. 80 c5 * c3 != c3 * c5 # label("Case 1"). [deny(20)]. 85 Power(c3 * (c5 * c4),c5). [back_rewrite(71),rewrite([73(1),79(3),26(5)])]. 93 x * (y * z) != z. [para(26(a,1),30(a,1))]. 99 -Power(x,y) | Power(y * x,y). [resolve(34,a,32,a)]. 154 -Shorter(x * y,y * x). [ur(63,a,53,a)]. 193 -Power(x,c5) | c3 * (c5 * c4) = x | f3(c5,c3 * (c5 * c4),x) * x = c3 * (c5 * c4) | c3 * (c5 * (c4 * f3(c5,c3 * (c5 * c4),x))) = x. [resolve(85,a,38,a),rewrite([26(35),26(34)]),flip(b)]. 374 -Prefix(x * y,y * x). [ur(69,b,154,a)]. 431 Power(c5 * (c3 * (c5 * c4)),c5). [resolve(99,a,85,a)]. 545 c5 * (c3 * x) != c3 * (c5 * y). [ur(68,b,374,a,c,374,a,d,80,a),rewrite([26(4),26(8)])]. 12102 $F. [resolve(193,a,431,a),flip(a),unit_del(a,30),unit_del(b,93),unit_del(c(flip),545)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=748. Generated=39776. Kept=12072. proofs=1. Usable=689. Sos=10634. Demods=147. Limbo=33, Disabled=775. Hints=0. Kept_by_rule=0, Deleted_by_rule=131. Forward_subsumed=27572. Back_subsumed=680. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=158 (0 lex), Back_demodulated=32. Back_unit_deleted=4. Demod_attempts=513976. Demod_rewrites=27183. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=117654. Nonunit_bsub_feature_tests=58551. Megabytes=25.05. User_CPU=3.14, System_CPU=0.02, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 17987 exit (max_proofs) ------  Process 17987 exit (max_proofs) Wed Jun 14 05:43:59 2017