============================== Prover9 =============================== Prover9 (64) version 2017-05A, May 2017. Process 17977 was started by veroff on theorem, Wed Jun 14 05:43:54 2017 The command was "prover9 -f p9header axioms.in Reform_2a.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 Reform_2a.in formulas(goals). Period(x,u) & Period(y,u) & -Shorter(u,x * y) -> (exists u3 u = x * u3) # label("Lemma Reform-2a"). end_of_list. formulas(assumptions). u * u1 = x * x1 & -Shorter(u,x * y) -> (exists u3 u = x * u3) # label("Lemma 4"). 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 u * u1 = x * x1 & -Shorter(u,x * y) -> (exists u3 u = x * u3) # label("Lemma 4") # label(non_clause). [assumption]. 19 Period(x,u) & Period(y,u) & -Shorter(u,x * y) -> (exists u3 u = x * u3) # label("Lemma Reform-2a") # 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 | Shorter(x,z * w) | z * f12(y,u,w,x,z) = x # label("Lemma 4"). [clausify(18)]. Period(c3,c2) # label("Lemma Reform-2a"). [deny(19)]. Period(c1,c2) # label("Lemma Reform-2a"). [deny(19)]. -Shorter(c2,c3 * c1) # label("Lemma Reform-2a"). [deny(19)]. c3 * x != c2 # label("Lemma Reform-2a"). [deny(19)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating Prefix/2 20 Prefix(x,y) | x * z != y. [clausify(15)]. 21 -Prefix(x,y) | x * f9(x,y) = y. [clausify(15)]. Derived: x * y != z | x * f9(x,z) = z. [resolve(20,a,21,a)]. 22 -Period(x,y) | Prefix(y,f11(x,y)). [clausify(17)]. Derived: -Period(x,y) | y * f9(y,f11(x,y)) = f11(x,y). [resolve(22,b,21,a)]. 23 Period(x,y) | -Power(z,x) | -Prefix(y,z). [clausify(17)]. Derived: Period(x,y) | -Power(z,x) | y * u != z. [resolve(23,c,20,a)]. Derived: Period(x,y) | -Power(f11(z,y),x) | -Period(z,y). [resolve(23,c,22,b)]. Eliminating Suffix/2 24 Suffix(x,y) | z * x != y. [clausify(16)]. 25 -Suffix(x,y) | f10(x,y) * x = y. [clausify(16)]. Derived: x * y != z | f10(y,z) * y = z. [resolve(24,a,25,a)]. ============================== end predicate elimination ============= Auto_denials: (non-Horn, no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ =, Power, Shorter, Period ]). Function symbol precedence: function_order([ c1, c2, c3, *, f9, f10, f11, f3, f4, f5, f6, f7, f1, f2, f8, f12 ]). After inverse_order: (no changes). Unfolding symbols: (none). 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 -Period(x,y) | Power(f11(x,y),x). [clausify(17)]. kept: 67 x * y != z * u | Shorter(x,z * w) | z * f12(y,u,w,x,z) = x # label("Lemma 4"). [clausify(18)]. kept: 68 Period(c3,c2) # label("Lemma Reform-2a"). [deny(19)]. kept: 69 Period(c1,c2) # label("Lemma Reform-2a"). [deny(19)]. kept: 70 -Shorter(c2,c3 * c1) # label("Lemma Reform-2a"). [deny(19)]. kept: 71 c3 * x != c2 # label("Lemma Reform-2a"). [deny(19)]. kept: 72 x * y != z | x * f9(x,z) = z. [resolve(20,a,21,a)]. kept: 73 -Period(x,y) | y * f9(y,f11(x,y)) = f11(x,y). [resolve(22,b,21,a)]. kept: 74 Period(x,y) | -Power(z,x) | y * u != z. [resolve(23,c,20,a)]. kept: 75 Period(x,y) | -Power(f11(z,y),x) | -Period(z,y). [resolve(23,c,22,b)]. kept: 76 x * y != z | f10(y,z) * y = z. [resolve(24,a,25,a)]. kept: 77 -Power(x,y) | Power(x * x,y). [factor(34,a,b)]. ============================== 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 -Period(x,y) | Power(f11(x,y),x). [clausify(17)]. 67 x * y != z * u | Shorter(x,z * w) | z * f12(y,u,w,x,z) = x # label("Lemma 4"). [clausify(18)]. 68 Period(c3,c2) # label("Lemma Reform-2a"). [deny(19)]. 69 Period(c1,c2) # label("Lemma Reform-2a"). [deny(19)]. 70 -Shorter(c2,c3 * c1) # label("Lemma Reform-2a"). [deny(19)]. 71 c3 * x != c2 # label("Lemma Reform-2a"). [deny(19)]. 72 x * y != z | x * f9(x,z) = z. [resolve(20,a,21,a)]. 73 -Period(x,y) | y * f9(y,f11(x,y)) = f11(x,y). [resolve(22,b,21,a)]. 74 Period(x,y) | -Power(z,x) | y * u != z. [resolve(23,c,20,a)]. 75 Period(x,y) | -Power(f11(z,y),x) | -Period(z,y). [resolve(23,c,22,b)]. 76 x * y != z | f10(y,z) * y = z. [resolve(24,a,25,a)]. 77 -Power(x,y) | Power(x * x,y). [factor(34,a,b)]. end_of_list. formulas(demodulators). 26 (x * y) * z = x * (y * z). [assumption]. 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=8): 66 -Period(x,y) | Power(f11(x,y),x). [clausify(17)]. given #42 (I,wt=22): 67 x * y != z * u | Shorter(x,z * w) | z * f12(y,u,w,x,z) = x # label("Lemma 4"). [clausify(18)]. given #43 (I,wt=3): 68 Period(c3,c2) # label("Lemma Reform-2a"). [deny(19)]. given #44 (I,wt=3): 69 Period(c1,c2) # label("Lemma Reform-2a"). [deny(19)]. given #45 (I,wt=5): 70 -Shorter(c2,c3 * c1) # label("Lemma Reform-2a"). [deny(19)]. given #46 (I,wt=5): 71 c3 * x != c2 # label("Lemma Reform-2a"). [deny(19)]. given #47 (I,wt=12): 72 x * y != z | x * f9(x,z) = z. [resolve(20,a,21,a)]. given #48 (I,wt=14): 73 -Period(x,y) | y * f9(y,f11(x,y)) = f11(x,y). [resolve(22,b,21,a)]. given #49 (I,wt=11): 74 Period(x,y) | -Power(z,x) | y * u != z. [resolve(23,c,20,a)]. given #50 (I,wt=11): 75 Period(x,y) | -Power(f11(z,y),x) | -Period(z,y). [resolve(23,c,22,b)]. given #51 (I,wt=12): 76 x * y != z | f10(y,z) * y = z. [resolve(24,a,25,a)]. given #52 (I,wt=8): 77 -Power(x,y) | Power(x * x,y). [factor(34,a,b)]. given #53 (A,wt=14): 78 x * (y * z) != x * (y * u) | z = u. [para(26(a,1),27(a,1)),rewrite([26(4)])]. given #54 (F,wt=3): 159 -Shorter(c2,c1). [ur(55,b,57,a,c,70,a)]. given #55 (F,wt=3): 160 -Shorter(c2,c3). [ur(55,b,56,a,c,70,a)]. given #56 (F,wt=5): 131 -Shorter(x * y,x). [resolve(56,a,54,b)]. given #57 (F,wt=5): 135 -Shorter(x * y,y). [resolve(57,a,54,b)]. given #58 (T,wt=5): 153 Power(f11(c3,c2),c3). [resolve(68,a,66,a)]. given #59 (T,wt=5): 154 Power(f11(c1,c2),c1). [resolve(69,a,66,a)]. given #60 (T,wt=5): 178 Power(x * x,x). [resolve(77,a,32,a)]. given #61 (T,wt=7): 136 Shorter(x,y * (z * x)). [para(26(a,1),57(a,2))]. given #62 (A,wt=14): 79 x * (y * z) != u * z | x * y = u. [para(26(a,1),28(a,1))]. given #63 (F,wt=5): 187 -Shorter(x * c2,c1). [ur(55,a,57,a,c,159,a)]. given #64 (F,wt=5): 188 -Shorter(c2 * x,c1). [ur(55,a,56,a,c,159,a)]. given #65 (F,wt=5): 193 -Shorter(x * c2,c3). [ur(55,a,57,a,c,160,a)]. given #66 (F,wt=5): 194 -Shorter(c2 * x,c3). [ur(55,a,56,a,c,160,a)]. given #67 (T,wt=7): 254 Shorter(x,y * (x * z)). [resolve(136,a,63,b)]. given #68 (T,wt=8): 88 -Power(x,y) | Power(y * x,y). [resolve(34,a,32,a)]. given #69 (T,wt=7): 298 Power(x * (x * x),x). [resolve(88,a,178,a)]. given #70 (T,wt=7): 299 Power(c1 * f11(c1,c2),c1). [resolve(88,a,154,a)]. given #71 (A,wt=9): 80 x * (y * z) != x * z. [ur(28,b,29,a),rewrite([26(2)])]. given #72 (F,wt=7): 82 x * (y * z) != z. [para(26(a,1),30(a,1))]. given #73 (F,wt=7): 143 -Shorter(x * y,y * x). [ur(63,a,53,a)]. given #74 (F,wt=7): 161 -Shorter(x * c2,c3 * c1). [ur(55,a,57,a,c,70,a)]. given #75 (F,wt=7): 162 -Shorter(c2 * x,c3 * c1). [ur(55,a,56,a,c,70,a)]. given #76 (T,wt=7): 300 Power(c3 * f11(c3,c2),c3). [resolve(88,a,153,a)]. given #77 (T,wt=7): 303 Power(x,f8(x,x,x,x)). [resolve(298,a,52,b),unit_del(a,32)]. given #78 (T,wt=8): 89 -Power(x,y) | Power(x * y,y). [resolve(34,b,32,a)]. given #79 (T,wt=7): 407 Power(f11(c1,c2) * c1,c1). [resolve(89,a,154,a)]. given #80 (A,wt=9): 81 x * (y * z) != x * y. [ur(27,b,29,a)]. given #81 (F,wt=7): 163 c3 * x != c2 * y. [ur(67,b,70,a,c,71,a),flip(a)]. given #82 (F,wt=5): 429 -Power(c3,c2 * c3). [ur(38,b,32,a,c,30,a,d,82,a,e,163,a)]. given #83 (F,wt=5): 431 -Power(c2 * c3,c3). [ur(38,a,32,a,c,30,a,d,82,a,e,163,a)]. given #84 (F,wt=3): 440 -Power(c2,c3). [ur(89,b,431,a)]. given #85 (T,wt=7): 408 Power(f11(c3,c2) * c3,c3). [resolve(89,a,153,a)]. given #86 (T,wt=8): 129 -Shorter(x,y) | Shorter(x,y * z). [resolve(56,a,55,b)]. given #87 (T,wt=8): 130 -Shorter(x * y,z) | Shorter(x,z). [resolve(56,a,55,a)]. given #88 (T,wt=8): 133 -Shorter(x,y) | Shorter(x,z * y). [resolve(57,a,55,b)]. given #89 (A,wt=15): 83 x * f1(x,x * y,y * z,z) = x * y. [resolve(31,a,26,a),unit_del(a,29),unit_del(c,82)]. given #90 (F,wt=5): 434 -Power(c2,c3 * c2). [ur(38,b,32,a,c,71,a,d,82,a,e,163,a(flip))]. given #91 (F,wt=5): 436 -Power(c3 * c2,c2). [ur(38,a,32,a,c,71,a,d,82,a,e,163,a(flip))]. given #92 (F,wt=3): 478 -Power(c3,c2). [ur(89,b,436,a)]. given #93 (F,wt=5): 448 -Power(c2,c3 * c3). [ur(33,b,178,a,c,440,a)]. given #94 (T,wt=8): 134 -Shorter(x * y,z) | Shorter(y,z). [resolve(57,a,55,a)]. given #95 (T,wt=8): 171 Period(x,y) | y * z != x. [resolve(74,b,32,a)]. given #96 (T,wt=5): 490 Period(x * y,x). [xx_res(171,b)]. given #97 (T,wt=8): 172 Period(x,c2) | -Power(f11(c1,c2),x). [resolve(75,c,69,a)]. given #98 (A,wt=15): 84 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 #99 (F,wt=5): 449 -Power(c2,f11(c3,c2)). [ur(33,b,153,a,c,440,a)]. given #100 (F,wt=5): 483 -Power(c3,c2 * c2). [ur(33,b,178,a,c,478,a)]. given #101 (F,wt=7): 183 -Shorter(x * c2,c1 * x). [ur(65,a,159,a)]. given #102 (F,wt=7): 184 -Shorter(c2 * x,x * c1). [ur(63,a,159,a)]. given #103 (T,wt=5): 496 Period(f11(c1,c2),c2). [resolve(172,b,32,a)]. given #104 (T,wt=8): 173 Period(x,c2) | -Power(f11(c3,c2),x). [resolve(75,c,68,a)]. given #105 (T,wt=5): 529 Period(f11(c3,c2),c2). [resolve(173,b,32,a)]. given #106 (T,wt=8): 216 -Power(x,f11(c3,c2)) | Power(x,c3). [resolve(153,a,33,b)]. given #107 (A,wt=38): 85 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 #108 (F,wt=7): 185 -Shorter(x * c2,x * c1). [ur(61,a,159,a)]. given #109 (F,wt=7): 186 -Shorter(c2 * x,c1 * x). [ur(59,a,159,a)]. given #110 (F,wt=7): 189 -Shorter(x * c2,c3 * x). [ur(65,a,160,a)]. given #111 (F,wt=7): 190 -Shorter(c2 * x,x * c3). [ur(63,a,160,a)]. given #112 (T,wt=8): 217 -Power(c3,x) | Power(f11(c3,c2),x). [resolve(153,a,33,a)]. given #113 (T,wt=8): 232 -Power(x,f11(c1,c2)) | Power(x,c1). [resolve(154,a,33,b)]. given #114 (T,wt=8): 233 -Power(c1,x) | Power(f11(c1,c2),x). [resolve(154,a,33,a)]. given #115 (T,wt=8): 251 -Power(x,y * y) | Power(x,y). [resolve(178,a,33,b)]. given #116 (A,wt=38): 86 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 #117 (F,wt=7): 191 -Shorter(x * c2,x * c3). [ur(61,a,160,a)]. given #118 (F,wt=7): 192 -Shorter(c2 * x,c3 * x). [ur(59,a,160,a)]. given #119 (F,wt=7): 199 -Shorter(x * (y * z),y). [ur(55,b,57,a,c,131,a),rewrite([26(2)])]. given #120 (F,wt=7): 201 -Shorter(x * (y * z),z). [ur(55,b,57,a,c,135,a)]. given #121 (T,wt=9): 132 Shorter(x * y,x * (y * z)). [para(26(a,1),56(a,2))]. given #122 (T,wt=9): 137 Shorter(x * y,x * (z * y)). [resolve(58,a,56,a),rewrite([26(3)])]. given #123 (T,wt=9): 141 Shorter(x * y,y * (z * x)). [resolve(62,a,57,a)]. given #124 (T,wt=9): 142 Shorter(x * y,y * (x * z)). [resolve(62,a,56,a)]. given #125 (A,wt=36): 87 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 #126 (F,wt=7): 261 -Shorter(x * (y * c2),c3). [ur(55,a,136,a,c,160,a)]. given #127 (F,wt=7): 262 -Shorter(x * (y * c2),c1). [ur(55,a,136,a,c,159,a)]. given #128 (F,wt=7): 272 -Shorter(x * (c2 * y),c1). [ur(55,a,56,a,c,187,a),rewrite([26(3)])]. given #129 (F,wt=7): 283 -Shorter(x * (c2 * y),c3). [ur(55,a,56,a,c,193,a),rewrite([26(3)])]. given #130 (T,wt=9): 146 Shorter(x * y,z * (y * x)). [resolve(64,a,57,a),rewrite([26(3)])]. given #131 (T,wt=9): 202 Power(f11(c3,c2) * f11(c3,c2),c3). [resolve(153,a,77,a)]. given #132 (T,wt=9): 218 Power(f11(c1,c2) * f11(c1,c2),c1). [resolve(154,a,77,a)]. given #133 (T,wt=9): 234 Power(x * (x * (x * x)),x). [resolve(178,a,77,a),rewrite([26(3)])]. given #134 (A,wt=12): 90 -Power(x,y) | x = y | Power(f3(y,y,x),y). [resolve(35,a,32,a)]. given #135 (F,wt=7): 443 -Power(c2 * c3,c3 * c3). [ur(33,b,178,a,c,431,a)]. given #136 (F,wt=7): 444 -Power(c2 * c3,f11(c3,c2)). [ur(33,b,153,a,c,431,a)]. given #137 (F,wt=7): 446 -Power(c2,c3 * f11(c3,c2)). [ur(33,b,300,a,c,440,a)]. given #138 (F,wt=7): 447 -Power(c2,c3 * (c3 * c3)). [ur(33,b,298,a,c,440,a)]. given #139 (T,wt=8): 720 Power(f3(x,x,x * x),x). [resolve(90,a,178,a),unit_del(a,29)]. given #140 (T,wt=9): 264 Shorter(x,y * (z * (u * x))). [para(26(a,1),136(a,2,2))]. given #141 (T,wt=9): 297 Shorter(x,y * (z * (x * u))). [para(26(a,1),254(a,2))]. given #142 (T,wt=9): 319 Power(c1 * (c1 * f11(c1,c2)),c1). [resolve(299,a,88,a)]. given #143 (A,wt=12): 91 -Power(x,y) | y = x | Power(f3(y,x,y),y). [resolve(35,b,32,a)]. given #144 (F,wt=7): 450 -Power(f8(c2,c2,c2,c2),c3). [ur(33,a,303,a,c,440,a)]. given #145 (F,wt=7): 468 -Power(c2,f11(c3,c2) * c3). [ur(33,b,408,a,c,440,a)]. given #146 (F,wt=7): 480 -Power(c3 * c2,c2 * c2). [ur(33,b,178,a,c,436,a)]. given #147 (F,wt=7): 482 -Power(c3,c2 * (c2 * c2)). [ur(33,b,298,a,c,478,a)]. given #148 (T,wt=8): 842 Power(f3(x,x * x,x),x). [resolve(91,a,178,a),flip(a),unit_del(a,29)]. given #149 (T,wt=9): 357 Power(c3 * (c3 * f11(c3,c2)),c3). [resolve(300,a,88,a)]. given #150 (T,wt=9): 375 Power(x * x,f8(x,x,x,x)). [resolve(303,a,77,a)]. given #151 (T,wt=9): 405 Power(c3 * (f11(c3,c2) * c3),c3). [resolve(89,a,300,a),rewrite([26(7)])]. given #152 (A,wt=22): 92 -Power(x,y) | x = y | x * f3(y,y,x) = y | y * f3(y,y,x) = x. [resolve(36,a,32,a)]. given #153 (F,wt=7): 484 -Power(f8(c3,c3,c3,c3),c2). [ur(33,a,303,a,c,478,a)]. given #154 (F,wt=8): 759 -Power(c3,f3(c2,c2,c2 * c2)). [ur(33,b,720,a,c,478,a)]. given #155 (F,wt=8): 766 -Power(c2,f3(c3,c3,c3 * c3)). [ur(33,b,720,a,c,440,a)]. given #156 (F,wt=8): 888 -Power(c3,f3(c2,c2 * c2,c2)). [ur(33,b,842,a,c,478,a)]. given #157 (T,wt=9): 406 Power(c1 * (f11(c1,c2) * c1),c1). [resolve(89,a,299,a),rewrite([26(7)])]. given #158 (T,wt=9): 409 Power(f11(c1,c2) * (c1 * c1),c1). [resolve(407,a,89,a),rewrite([26(7)])]. given #159 (T,wt=9): 451 Power(f11(c3,c2) * (c3 * c3),c3). [resolve(408,a,89,a),rewrite([26(7)])]. given #160 (T,wt=9): 488 Period(x * (y * z),x * y). [resolve(171,b,26,a)]. given #161 (A,wt=22): 93 -Power(x,y) | y = x | y * f3(y,x,y) = x | x * f3(y,x,y) = y. [resolve(36,b,32,a)]. given #162 (F,wt=8): 897 -Power(c2,f3(c3,c3 * c3,c3)). [ur(33,b,842,a,c,440,a)]. given #163 (F,wt=9): 155 -Shorter(x * c2,c3 * (c1 * x)). [ur(65,a,70,a),rewrite([26(6)])]. given #164 (F,wt=5): 1116 -Shorter(c2,c1 * c3). [ur(60,b,155,a)]. given #165 (F,wt=7): 1118 -Shorter(x * c2,c1 * c3). [ur(55,b,142,a,c,155,a)]. given #166 (T,wt=9): 494 Power(f11(x * y,x),x * y). [resolve(490,a,66,a)]. given #167 (T,wt=7): 1140 Power(f11(x * x,x),x). [resolve(494,a,251,a)]. given #168 (T,wt=9): 527 Power(f11(f11(c1,c2),c2),f11(c1,c2)). [resolve(496,a,66,a)]. given #169 (T,wt=7): 1217 Power(f11(f11(c1,c2),c2),c1). [resolve(527,a,232,a)]. given #170 (A,wt=22): 94 -Power(x,y) | x = y | x * f3(y,y,x) = y | f3(y,y,x) * y = x. [resolve(37,a,32,a)]. given #171 (F,wt=7): 1125 -Shorter(c2 * x,c1 * c3). [ur(130,b,1116,a)]. given #172 (F,wt=7): 1163 -Power(c3,f11(c2 * c2,c2)). [ur(33,b,494,a,c,483,a)]. given #173 (F,wt=7): 1167 -Power(c2,f11(c3 * c3,c3)). [ur(33,b,494,a,c,448,a)]. given #174 (F,wt=7): 1171 -Power(c2,f11(c3 * c2,c3)). [ur(33,b,494,a,c,434,a)]. given #175 (T,wt=9): 532 Power(f11(f11(c3,c2),c2),f11(c3,c2)). [resolve(529,a,66,a)]. given #176 (T,wt=7): 1310 Power(f11(f11(c3,c2),c2),c3). [resolve(532,a,216,a)]. given #177 (T,wt=9): 563 Power(f11(c3,c2),f8(c3,c3,c3,c3)). [resolve(217,a,303,a)]. given #178 (T,wt=7): 1360 Period(f8(c3,c3,c3,c3),c2). [resolve(563,a,173,b)]. given #179 (A,wt=22): 95 -Power(x,y) | y = x | y * f3(y,x,y) = x | f3(y,x,y) * x = y. [resolve(37,b,32,a)]. given #180 (F,wt=7): 1172 -Power(c3,f11(c2 * c3,c2)). [ur(33,b,494,a,c,429,a)]. given #181 (F,wt=7): 1334 -Power(c2,f11(f11(c3,c2),c2)). [ur(33,b,532,a,c,449,a)]. given #182 (F,wt=9): 156 -Shorter(c2 * x,x * (c3 * c1)). [ur(63,a,70,a)]. given #183 (F,wt=9): 157 -Shorter(x * c2,x * (c3 * c1)). [ur(61,a,70,a)]. given #184 (T,wt=9): 565 Power(f11(c1,c2),f8(c1,c1,c1,c1)). [resolve(233,a,303,a)]. given #185 (T,wt=7): 1437 Period(f8(c1,c1,c1,c1),c2). [resolve(565,a,172,b)]. given #186 (T,wt=9): 688 Power(x,f8(x,x,x,x * x)). [resolve(234,a,51,b),unit_del(a,32)]. given #187 (T,wt=9): 816 Power(c1,f8(c1,c1,c1,f11(c1,c2))). [resolve(319,a,51,b),unit_del(a,32)]. given #188 (A,wt=22): 96 -Power(x,y) | x = y | f3(y,y,x) * x = y | y * f3(y,y,x) = x. [resolve(38,a,32,a)]. given #189 (F,wt=9): 158 -Shorter(c2 * x,c3 * (c1 * x)). [ur(59,a,70,a),rewrite([26(6)])]. given #190 (F,wt=9): 164 x * (c3 * y) != x * c2. [ur(27,b,71,a)]. given #191 (F,wt=9): 195 -Shorter(x * (y * z),y * x). [ur(65,a,131,a)]. given #192 (F,wt=9): 196 -Shorter(x * (y * z),z * x). [ur(63,a,131,a),rewrite([26(2)])]. given #193 (T,wt=9): 910 Power(c3,f8(c3,c3,c3,f11(c3,c2))). [resolve(357,a,51,b),unit_del(a,32)]. given #194 (T,wt=9): 957 Power(c3,f8(c3,f11(c3,c2),c3,c3)). [resolve(405,a,52,b),unit_del(a,153)]. given #195 (T,wt=9): 1019 Power(c1,f8(c1,f11(c1,c2),c1,c1)). [resolve(406,a,52,b),unit_del(a,154)]. given #196 (T,wt=9): 1041 Power(c1,f8(c1,c1,f11(c1,c2),c1)). [resolve(409,a,52,b),unit_del(a,32)]. given #197 (A,wt=22): 97 -Power(x,y) | y = x | f3(y,x,y) * y = x | x * f3(y,x,y) = y. [resolve(38,b,32,a)]. given #198 (F,wt=9): 197 -Shorter(x * (y * z),x * y). [ur(61,a,131,a)]. given #199 (F,wt=9): 198 -Shorter(x * (y * z),x * z). [ur(59,a,131,a),rewrite([26(2)])]. given #200 (F,wt=9): 200 -Shorter(x * (y * z),z * y). [ur(63,a,135,a),rewrite([26(2)])]. given #201 (F,wt=9): 259 -Shorter(x * (y * (z * u)),u). [ur(55,b,136,a,c,135,a)]. given #202 (T,wt=9): 1063 Power(c3,f8(c3,c3,f11(c3,c2),c3)). [resolve(451,a,52,b),unit_del(a,32)]. given #203 (T,wt=9): 1180 Power(f11(x * x,x) * x,x). [resolve(1140,a,89,a)]. given #204 (T,wt=9): 1181 Power(x * f11(x * x,x),x). [resolve(1140,a,88,a)]. given #205 (T,wt=9): 1244 Power(f11(f11(c1,c2),c2) * c1,c1). [resolve(1217,a,89,a)]. given #206 (A,wt=22): 98 -Power(x,y) | x = y | f3(y,y,x) * x = y | f3(y,y,x) * y = x. [resolve(39,a,32,a)]. given #207 (F,wt=9): 260 -Shorter(x * (y * (z * u)),z). [ur(55,b,136,a,c,131,a),rewrite([26(3),26(2)])]. given #208 (F,wt=9): 263 -Shorter(x * (y * c2),c3 * c1). [ur(55,a,136,a,c,70,a)]. given #209 (F,wt=9): 267 -Shorter(x * (y * c2),c1 * x). [ur(65,a,187,a)]. given #210 (F,wt=9): 268 -Shorter(x * (c2 * y),y * c1). [ur(63,a,187,a),rewrite([26(3)])]. given #211 (T,wt=9): 1245 Power(c1 * f11(f11(c1,c2),c2),c1). [resolve(1217,a,88,a)]. given #212 (T,wt=9): 1341 Power(f11(f11(c3,c2),c2) * c3,c3). [resolve(1310,a,89,a)]. given #213 (T,wt=9): 1342 Power(c3 * f11(f11(c3,c2),c2),c3). [resolve(1310,a,88,a)]. given #214 (T,wt=10): 203 Period(c3,x) | f11(c3,c2) != x * y. [resolve(153,a,74,b),flip(b)]. given #215 (A,wt=22): 99 -Power(x,y) | y = x | f3(y,x,y) * y = x | f3(y,x,y) * x = y. [resolve(39,b,32,a)]. given #216 (F,wt=9): 269 -Shorter(x * (y * c2),x * c1). [ur(61,a,187,a)]. given #217 (F,wt=9): 270 -Shorter(x * (c2 * y),c1 * y). [ur(59,a,187,a),rewrite([26(3)])]. given #218 (F,wt=9): 271 -Shorter(x * (y * (z * c2)),c1). [ur(55,a,136,a,c,187,a)]. given #219 (F,wt=9): 273 -Shorter(x * (c2 * y),c1 * x). [ur(65,a,188,a)]. given #220 (T,wt=10): 214 -Power(x,c3) | Power(x * f11(c3,c2),c3). [resolve(153,a,34,b)]. given #221 (T,wt=10): 215 -Power(x,c3) | Power(f11(c3,c2) * x,c3). [resolve(153,a,34,a)]. given #222 (T,wt=10): 219 Period(c1,x) | f11(c1,c2) != x * y. [resolve(154,a,74,b),flip(b)]. given #223 (T,wt=10): 230 -Power(x,c1) | Power(x * f11(c1,c2),c1). [resolve(154,a,34,b)]. given #224 (A,wt=22): 100 Power(x,x * y) | f4(x,y,x * y) * f5(x,y,x * y) = x * y. [resolve(40,a,32,a)]. given #225 (F,wt=9): 274 -Shorter(c2 * (x * y),y * c1). [ur(63,a,188,a),rewrite([26(3)])]. given #226 (F,wt=9): 275 -Shorter(x * (c2 * y),x * c1). [ur(61,a,188,a)]. given #227 (F,wt=9): 276 -Shorter(c2 * (x * y),c1 * y). [ur(59,a,188,a),rewrite([26(3)])]. given #228 (F,wt=9): 277 -Shorter(x * (y * (c2 * z)),c1). [ur(55,a,136,a,c,188,a)]. given #229 (T,wt=10): 231 -Power(x,c1) | Power(f11(c1,c2) * x,c1). [resolve(154,a,34,a)]. given #230 (T,wt=10): 235 Period(x,y) | y * z != x * x. [resolve(178,a,74,b)]. given #231 (T,wt=3): 2262 Period(x,x). [xx_res(235,b)]. given #232 (T,wt=5): 2267 Power(f11(x,x),x). [resolve(2262,a,66,a)]. given #233 (A,wt=27): 101 -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 #234 (F,wt=5): 2316 -Power(c3,f11(c2,c2)). [ur(33,b,2267,a,c,478,a)]. given #235 (F,wt=5): 2325 -Power(c2,f11(c3,c3)). [ur(33,b,2267,a,c,440,a)]. given #236 (F,wt=7): 2326 -Power(c3 * c2,f11(c2,c2)). [ur(33,b,2267,a,c,436,a)]. given #237 (F,wt=7): 2328 -Power(c2 * c3,f11(c3,c3)). [ur(33,b,2267,a,c,431,a)]. given #238 (T,wt=7): 2285 Power(f11(x,x) * x,x). [resolve(2267,a,89,a)]. given #239 (T,wt=7): 2286 Power(x * f11(x,x),x). [resolve(2267,a,88,a)]. given #240 (T,wt=8): 2265 Period(x,y) | -Power(f11(y,y),x). [resolve(2262,a,75,c)]. given #241 (T,wt=5): 2516 Period(f11(x,x),x). [resolve(2265,b,32,a)]. given #242 (A,wt=28): 102 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 #243 (F,wt=7): 2433 -Power(c3,f11(c2,c2) * c2). [ur(33,b,2285,a,c,478,a)]. given #244 (F,wt=7): 2442 -Power(c2,f11(c3,c3) * c3). [ur(33,b,2285,a,c,440,a)]. given #245 (F,wt=7): 2498 -Power(c3,c2 * f11(c2,c2)). [ur(33,b,2286,a,c,478,a)]. given #246 (F,wt=7): 2507 -Power(c2,c3 * f11(c3,c3)). [ur(33,b,2286,a,c,440,a)]. given #247 (T,wt=8): 2301 -Power(x,f11(y,y)) | Power(x,y). [resolve(2267,a,33,b)]. given #248 (T,wt=8): 2302 -Power(x,y) | Power(f11(x,x),y). [resolve(2267,a,33,a)]. given #249 (T,wt=9): 2261 Period(x * y,x * (y * x)). [resolve(235,b,26,a),rewrite([26(3)])]. given #250 (T,wt=9): 2268 Power(f11(x * x,x * x),x). [resolve(2267,a,251,a)]. given #251 (A,wt=39): 103 -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 #252 (F,wt=9): 278 -Shorter(x * (y * c2),c3 * x). [ur(65,a,193,a)]. given #253 (F,wt=9): 279 -Shorter(x * (c2 * y),y * c3). [ur(63,a,193,a),rewrite([26(3)])]. given #254 (F,wt=9): 280 -Shorter(x * (y * c2),x * c3). [ur(61,a,193,a)]. given #255 (F,wt=9): 281 -Shorter(x * (c2 * y),c3 * y). [ur(59,a,193,a),rewrite([26(3)])]. given #256 (T,wt=5): 2706 Period(x,x * x). [resolve(2268,a,2265,b)]. given #257 (T,wt=7): 2808 Power(f11(x,x * x),x). [resolve(2706,a,66,a)]. given #258 (T,wt=9): 2269 Power(f11(f11(c1,c2),f11(c1,c2)),c1). [resolve(2267,a,232,a)]. given #259 (T,wt=5): 2884 Period(c1,f11(c1,c2)). [resolve(2269,a,2265,b)]. given #260 (A,wt=23): 104 Power(x,x * y) | f4(x,y,x * y) = x | Power(f6(x,y,x * y),x * y). [resolve(42,a,32,a)]. given #261 (F,wt=7): 2868 -Power(c3,f11(c2,c2 * c2)). [ur(33,b,2808,a,c,478,a)]. given #262 (F,wt=7): 2877 -Power(c2,f11(c3,c3 * c3)). [ur(33,b,2808,a,c,440,a)]. given #263 (F,wt=9): 282 -Shorter(x * (y * (z * c2)),c3). [ur(55,a,136,a,c,193,a)]. given #264 (F,wt=9): 284 -Shorter(x * (c2 * y),c3 * x). [ur(65,a,194,a)]. given #265 (T,wt=7): 2915 Power(f11(c1,f11(c1,c2)),c1). [resolve(2884,a,66,a)]. given #266 (T,wt=9): 2270 Power(f11(c1,c2) * f11(c1,c1),c1). [resolve(2267,a,231,a)]. given #267 (T,wt=9): 2271 Power(f11(c1,c1) * f11(c1,c2),c1). [resolve(2267,a,230,a)]. given #268 (T,wt=9): 2272 Power(f11(f11(c3,c2),f11(c3,c2)),c3). [resolve(2267,a,216,a)]. given #269 (A,wt=30): 105 -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 #270 (F,wt=9): 285 -Shorter(c2 * (x * y),y * c3). [ur(63,a,194,a),rewrite([26(3)])]. given #271 (F,wt=9): 286 -Shorter(x * (c2 * y),x * c3). [ur(61,a,194,a)]. given #272 (F,wt=9): 287 -Shorter(c2 * (x * y),c3 * y). [ur(59,a,194,a),rewrite([26(3)])]. given #273 (F,wt=9): 288 -Shorter(x * (y * (c2 * z)),c3). [ur(55,a,136,a,c,194,a)]. given #274 (T,wt=5): 3140 Period(c3,f11(c3,c2)). [resolve(2272,a,2265,b)]. given #275 (T,wt=7): 3202 Power(f11(c3,f11(c3,c2)),c3). [resolve(3140,a,66,a)]. given #276 (T,wt=9): 2273 Power(f11(c3,c2) * f11(c3,c3),c3). [resolve(2267,a,215,a)]. given #277 (T,wt=9): 2274 Power(f11(c3,c3) * f11(c3,c2),c3). [resolve(2267,a,214,a)]. given #278 (A,wt=28): 106 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 #279 (F,wt=7): 3235 -Power(c2,f11(c3,f11(c3,c2))). [ur(33,b,3202,a,c,440,a)]. given #280 (F,wt=9): 295 -Shorter(x * (c2 * y),c3 * c1). [ur(55,a,254,a,c,70,a)]. given #281 (F,wt=9): 339 x * (y * (z * u)) != u. [para(26(a,1),82(a,1,2))]. given #282 (F,wt=7): 3390 -Power(c3,c2 * (x * c3)). [ur(97,b,82,a,c,339,a,d,163,a)]. given #283 (T,wt=9): 2287 Power(f11(x,x) * f11(x,x),x). [resolve(2267,a,77,a)]. given #284 (T,wt=9): 2395 Power(f11(x,x) * (x * x),x). [resolve(2285,a,89,a),rewrite([26(3)])]. given #285 (T,wt=9): 2396 Power(x * (f11(x,x) * x),x). [resolve(2285,a,88,a)]. given #286 (T,wt=9): 2464 Power(x * (x * f11(x,x)),x). [resolve(2286,a,88,a)]. given #287 (A,wt=35): 107 -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 #288 (F,wt=7): 3391 -Power(c2,c3 * (x * c2)). [ur(97,b,82,a,c,339,a,d,163,a(flip))]. given #289 (F,wt=7): 3392 -Power(c2 * (x * c3),c3). [ur(96,b,82,a,c,339,a,d,163,a)]. given #290 (F,wt=7): 3393 -Power(c3 * (x * c2),c2). [ur(96,b,82,a,c,339,a,d,163,a(flip))]. given #291 (F,wt=9): 430 -Power(c2 * c3,f8(c3,c3,c3,c3)). [ur(38,a,303,a,c,30,a,d,82,a,e,163,a)]. given #292 (T,wt=9): 2519 Power(f11(f11(x,x),x),f11(x,x)). [resolve(2516,a,66,a)]. given #293 (T,wt=7): 3834 Power(f11(f11(x,x),x),x). [resolve(2519,a,2301,a)]. given #294 (T,wt=9): 2648 Power(f11(f11(x,x),f11(x,x)),x). [resolve(2301,a,2267,a)]. given #295 (T,wt=5): 3944 Period(x,f11(x,x)). [resolve(2648,a,2265,b)]. given #296 (A,wt=23): 108 Power(x,x * y) | f5(x,y,x * y) = y | Power(f7(x,y,x * y),x * y). [resolve(44,a,32,a)]. given #297 (F,wt=7): 3815 -Power(c2,f8(c3,c3,c3,c3)). [ur(34,b,303,a,c,430,a)]. given #298 (F,wt=7): 3865 -Power(c2,f11(f11(c3,c3),c3)). [ur(33,b,2519,a,c,2325,a)]. given #299 (F,wt=7): 3866 -Power(c3,f11(f11(c2,c2),c2)). [ur(33,b,2519,a,c,2316,a)]. given #300 (F,wt=9): 435 -Power(c3 * c2,f8(c2,c2,c2,c2)). [ur(38,a,303,a,c,71,a,d,82,a,e,163,a(flip))]. given #301 (T,wt=7): 4017 Power(f11(x,f11(x,x)),x). [resolve(3944,a,66,a)]. given #302 (T,wt=9): 2690 Power(f11(x,x),f8(x,x,x,x)). [resolve(2302,a,303,a)]. given #303 (T,wt=7): 4281 Period(f8(x,x,x,x),x). [resolve(2690,a,2265,b)]. given #304 (T,wt=9): 2829 Power(f11(x,x * x) * x,x). [resolve(2808,a,89,a)]. given #305 (A,wt=28): 109 -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 #306 (F,wt=7): 4176 -Power(c3,f8(c2,c2,c2,c2)). [ur(34,b,303,a,c,435,a)]. given #307 (F,wt=7): 4264 -Power(c3,f11(c2,f11(c2,c2))). [ur(33,b,4017,a,c,478,a)]. given #308 (F,wt=7): 4273 -Power(c2,f11(c3,f11(c3,c3))). [ur(33,b,4017,a,c,440,a)]. given #309 (F,wt=9): 439 -Power(f8(c3,c3,c3,c3),c2 * c3). [ur(33,a,303,a,c,429,a)]. given #310 (T,wt=9): 2830 Power(x * f11(x,x * x),x). [resolve(2808,a,88,a)]. given #311 (T,wt=9): 3062 Power(f11(c1,f11(c1,c2)) * c1,c1). [resolve(2915,a,89,a)]. given #312 (T,wt=9): 3063 Power(c1 * f11(c1,f11(c1,c2)),c1). [resolve(2915,a,88,a)]. given #313 (T,wt=9): 3216 Power(f11(c3,f11(c3,c2)) * c3,c3). [resolve(3202,a,89,a)]. given #314 (A,wt=22): 110 Power(x,y * x) | f4(y,x,y * x) * f5(y,x,y * x) = y * x. [resolve(45,a,32,a)]. given #315 (F,wt=9): 441 -Power(c2 * c3,c3 * f11(c3,c2)). [ur(33,b,300,a,c,431,a)]. given #316 (F,wt=9): 442 -Power(c2 * c3,c3 * (c3 * c3)). [ur(33,b,298,a,c,431,a)]. given #317 (F,wt=9): 469 -Power(c2 * c3,f11(c3,c2) * c3). [ur(33,b,408,a,c,431,a)]. given #318 (F,wt=9): 477 -Power(f8(c2,c2,c2,c2),c3 * c2). [ur(33,a,303,a,c,434,a)]. given #319 (T,wt=9): 3217 Power(c3 * f11(c3,f11(c3,c2)),c3). [resolve(3202,a,88,a)]. given #320 (T,wt=9): 3522 Power(x,f8(x,x,f11(x,x),x)). [resolve(2395,a,52,b),unit_del(a,32)]. given #321 (T,wt=9): 3596 Power(x,f8(x,f11(x,x),x,x)). [resolve(2396,a,52,b),unit_del(a,2267)]. given #322 (T,wt=9): 3675 Power(x,f8(x,x,x,f11(x,x))). [resolve(2464,a,51,b),unit_del(a,32)]. given #323 (A,wt=25): 111 -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 #324 (F,wt=9): 479 -Power(c3 * c2,c2 * (c2 * c2)). [ur(33,b,298,a,c,436,a)]. given #325 (F,wt=9): 486 -Power(c2,c3 * (c3 * (c3 * c3))). [ur(33,b,178,a,c,448,a),rewrite([26(8)])]. given #326 (F,wt=9): 487 -Power(f8(c2,c2,c2,c2),c3 * c3). [ur(33,a,303,a,c,448,a)]. given #327 (F,wt=9): 505 -Power(c2,f11(c3,c2) * f11(c3,c2)). [ur(33,b,178,a,c,449,a)]. given #328 (T,wt=9): 3886 Power(f11(f11(x,x),x) * x,x). [resolve(3834,a,89,a)]. given #329 (T,wt=9): 3887 Power(x * f11(f11(x,x),x),x). [resolve(3834,a,88,a)]. given #330 (T,wt=9): 4215 Power(f11(x,f11(x,x)) * x,x). [resolve(4017,a,89,a)]. given #331 (T,wt=9): 4216 Power(x * f11(x,f11(x,x)),x). [resolve(4017,a,88,a)]. given #332 (A,wt=28): 112 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 #333 (F,wt=9): 506 -Power(f8(c2,c2,c2,c2),f11(c3,c2)). [ur(33,a,303,a,c,449,a)]. given #334 (F,wt=9): 508 -Power(c3,c2 * (c2 * (c2 * c2))). [ur(33,b,178,a,c,483,a),rewrite([26(8)])]. given #335 (F,wt=9): 509 -Power(f8(c3,c3,c3,c3),c2 * c2). [ur(33,a,303,a,c,483,a)]. given #336 (F,wt=9): 510 -Shorter(x * (y * c2),c1 * y). [ur(134,b,183,a)]. given #337 (T,wt=10): 249 -Power(x,y) | Power(x * (y * y),y). [resolve(178,a,34,b)]. given #338 (T,wt=10): 250 -Power(x,y) | Power(y * (y * x),y). [resolve(178,a,34,a),rewrite([26(3)])]. given #339 (T,wt=10): 257 -Shorter(x,y) | Shorter(x,z * (u * y)). [resolve(136,a,55,b)]. given #340 (T,wt=10): 258 -Shorter(x * (y * z),u) | Shorter(z,u). [resolve(136,a,55,a)]. given #341 (A,wt=37): 113 -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 #342 (F,wt=9): 518 -Shorter(c2 * (x * y),x * c1). [ur(130,b,184,a),rewrite([26(3)])]. given #343 (F,wt=9): 536 -Shorter(x * (y * c2),y * c1). [ur(134,b,185,a)]. given #344 (F,wt=9): 543 -Shorter(c2 * (x * y),c1 * x). [ur(130,b,186,a),rewrite([26(3)])]. given #345 (F,wt=9): 548 -Shorter(x * (y * c2),c3 * y). [ur(134,b,189,a)]. given #346 (T,wt=10): 293 -Shorter(x,y) | Shorter(x,z * (y * u)). [resolve(254,a,55,b)]. given #347 (T,wt=10): 294 -Shorter(x * (y * z),u) | Shorter(y,u). [resolve(254,a,55,a)]. given #348 (T,wt=10): 316 -Power(x,y * (y * y)) | Power(x,y). [resolve(298,a,33,b)]. given #349 (T,wt=9): 6046 Power(f11(x * (x * x),x),x). [resolve(316,a,494,a)]. given #350 (A,wt=23): 114 Power(x,y * x) | f4(y,x,y * x) = y | Power(f6(y,x,y * x),y * x). [resolve(47,a,32,a)]. given #351 (F,wt=9): 556 -Shorter(c2 * (x * y),x * c3). [ur(130,b,190,a),rewrite([26(3)])]. given #352 (F,wt=9): 572 -Shorter(x * (y * c2),y * c3). [ur(134,b,191,a)]. given #353 (F,wt=9): 579 -Shorter(c2 * (x * y),c3 * x). [ur(130,b,192,a),rewrite([26(3)])]. given #354 (F,wt=9): 926 -Power(c2,c3 * (c3 * f11(c3,c2))). [ur(33,b,357,a,c,440,a)]. given #355 (T,wt=10): 317 -Power(x,y) | Power(x * (x * x),y). [resolve(298,a,33,a)]. given #356 (T,wt=10): 334 -Power(x,c1 * f11(c1,c2)) | Power(x,c1). [resolve(299,a,33,b)]. given #357 (T,wt=9): 6397 Power(f11(c1 * f11(c1,c2),c1),c1). [resolve(334,a,494,a)]. given #358 (T,wt=10): 335 -Power(c1,x) | Power(c1 * f11(c1,c2),x). [resolve(299,a,33,a)]. given #359 (A,wt=28): 115 -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 #360 (F,wt=9): 974 -Power(c2,c3 * (f11(c3,c2) * c3)). [ur(33,b,405,a,c,440,a)]. given #361 (F,wt=9): 1080 -Power(c2,f11(c3,c2) * (c3 * c3)). [ur(33,b,451,a,c,440,a)]. given #362 (F,wt=9): 1126 -Shorter(x * c2,c1 * (c3 * x)). [ur(65,a,1116,a),rewrite([26(6)])]. given #363 (F,wt=9): 1127 -Shorter(c2 * x,x * (c1 * c3)). [ur(63,a,1116,a)]. given #364 (T,wt=10): 372 -Power(x,c3 * f11(c3,c2)) | Power(x,c3). [resolve(300,a,33,b)]. given #365 (T,wt=9): 6576 Power(f11(c3 * f11(c3,c2),c3),c3). [resolve(372,a,494,a)]. given #366 (T,wt=10): 373 -Power(c3,x) | Power(c3 * f11(c3,c2),x). [resolve(300,a,33,a)]. given #367 (T,wt=10): 402 -Power(x,y) | Power(x,f8(y,y,y,y)). [resolve(303,a,33,b)]. given #368 (A,wt=28): 116 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 #369 (F,wt=9): 1128 -Shorter(x * c2,x * (c1 * c3)). [ur(61,a,1116,a)]. given #370 (F,wt=9): 1129 -Shorter(c2 * x,c1 * (c3 * x)). [ur(59,a,1116,a),rewrite([26(6)])]. given #371 (F,wt=9): 1132 -Shorter(x * (c2 * y),c1 * c3). [ur(55,a,254,a,c,1116,a)]. given #372 (F,wt=9): 1133 -Shorter(x * (y * c2),c1 * c3). [ur(55,a,136,a,c,1116,a)]. given #373 (T,wt=10): 403 -Power(f8(x,x,x,x),y) | Power(x,y). [resolve(303,a,33,a)]. given #374 (T,wt=10): 424 -Power(x,f11(c1,c2) * c1) | Power(x,c1). [resolve(407,a,33,b)]. given #375 (T,wt=10): 425 -Power(c1,x) | Power(f11(c1,c2) * c1,x). [resolve(407,a,33,a)]. given #376 (T,wt=10): 466 -Power(x,f11(c3,c2) * c3) | Power(x,c3). [resolve(408,a,33,b)]. given #377 (A,wt=33): 117 -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 #378 (F,wt=9): 1164 -Power(c3,f11(c2 * (c2 * c2),c2)). [ur(33,b,494,a,c,482,a)]. given #379 (F,wt=9): 1165 -Power(c3 * c2,f11(c2 * c2,c2)). [ur(33,b,494,a,c,480,a)]. given #380 (F,wt=9): 1168 -Power(c2,f11(c3 * (c3 * c3),c3)). [ur(33,b,494,a,c,447,a)]. given #381 (F,wt=9): 1169 -Power(c2,f11(c3 * f11(c3,c2),c3)). [ur(33,b,494,a,c,446,a)]. given #382 (T,wt=10): 467 -Power(c3,x) | Power(f11(c3,c2) * c3,x). [resolve(408,a,33,a)]. given #383 (T,wt=10): 492 Period(x,y) | -Power(f11(y * z,y),x). [resolve(490,a,75,c)]. given #384 (T,wt=7): 7065 Period(f11(x * y,x),x). [resolve(492,b,32,a)]. given #385 (T,wt=10): 525 Period(x,c2) | -Power(f11(f11(c1,c2),c2),x). [resolve(496,a,75,c)]. given #386 (A,wt=23): 118 Power(x,y * x) | f5(y,x,y * x) = x | Power(f7(y,x,y * x),y * x). [resolve(49,a,32,a)]. given #387 (F,wt=9): 1170 -Power(c2 * c3,f11(c3 * c3,c3)). [ur(33,b,494,a,c,443,a)]. given #388 (F,wt=9): 1335 -Power(c2 * c3,f11(f11(c3,c2),c2)). [ur(33,b,532,a,c,444,a)]. given #389 (F,wt=9): 1522 -Power(f8(c3,c3,c3,c3 * c3),c2). [ur(33,a,688,a,c,478,a)]. given #390 (F,wt=9): 1531 -Power(f8(c2,c2,c2,c2 * c2),c3). [ur(33,a,688,a,c,440,a)]. given #391 (T,wt=7): 7084 Period(f11(f11(c1,c2),c2),c2). [resolve(525,b,32,a)]. given #392 (T,wt=10): 530 Period(x,c2) | -Power(f11(f11(c3,c2),c2),x). [resolve(529,a,75,c)]. given #393 (T,wt=7): 7326 Period(f11(f11(c3,c2),c2),c2). [resolve(530,b,32,a)]. given #394 (T,wt=10): 711 Power(f3(c3,c3,f11(c3,c2) * c3),c3). [resolve(90,a,408,a),unit_del(a,30)]. given #395 (A,wt=26): 119 -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 #396 (F,wt=9): 1640 -Power(f8(c3,c3,c3,f11(c3,c2)),c2). [ur(33,a,910,a,c,478,a)]. given #397 (F,wt=9): 1674 -Power(f8(c3,f11(c3,c2),c3,c3),c2). [ur(33,a,957,a,c,478,a)]. given #398 (F,wt=9): 1811 -Power(f8(c3,c3,f11(c3,c2),c3),c2). [ur(33,a,1063,a,c,478,a)]. given #399 (F,wt=9): 1856 -Power(c3,f11(c2 * c2,c2) * c2). [ur(33,b,1180,a,c,478,a)]. given #400 (T,wt=10): 712 Power(f3(c1,c1,f11(c1,c2) * c1),c1). [resolve(90,a,407,a),unit_del(a,30)]. given #401 (T,wt=10): 714 Power(f3(c3,c3,c3 * f11(c3,c2)),c3). [resolve(90,a,300,a),unit_del(a,29)]. given #402 (T,wt=10): 715 Power(f3(c1,c1,c1 * f11(c1,c2)),c1). [resolve(90,a,299,a),unit_del(a,29)]. given #403 (T,wt=10): 716 Power(f3(x,x,x * (x * x)),x). [resolve(90,a,298,a),unit_del(a,29)]. given #404 (A,wt=18): 120 -Power(x,y * (x * z)) | Power(x,f8(y * (x * z),x,y,z)). [resolve(50,b,32,a)]. given #405 (F,wt=9): 1865 -Power(c2,f11(c3 * c3,c3) * c3). [ur(33,b,1180,a,c,440,a)]. given #406 (F,wt=9): 1913 -Power(c3,c2 * f11(c2 * c2,c2)). [ur(33,b,1181,a,c,478,a)]. given #407 (F,wt=9): 1922 -Power(c2,c3 * f11(c3 * c3,c3)). [ur(33,b,1181,a,c,440,a)]. given #408 (F,wt=9): 2052 -Power(c2,f11(f11(c3,c2),c2) * c3). [ur(33,b,1341,a,c,440,a)]. given #409 (T,wt=10): 832 Power(f3(c3,f11(c3,c2) * c3,c3),c3). [resolve(91,a,408,a),flip(a),unit_del(a,30)]. given #410 (T,wt=10): 833 Power(f3(c1,f11(c1,c2) * c1,c1),c1). [resolve(91,a,407,a),flip(a),unit_del(a,30)]. given #411 (T,wt=10): 836 Power(f3(c3,c3 * f11(c3,c2),c3),c3). [resolve(91,a,300,a),flip(a),unit_del(a,29)]. given #412 (T,wt=10): 837 Power(f3(c1,c1 * f11(c1,c2),c1),c1). [resolve(91,a,299,a),flip(a),unit_del(a,29)]. given #413 (A,wt=25): 121 -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 #414 (F,wt=9): 2082 -Power(c2,c3 * f11(f11(c3,c2),c2)). [ur(33,b,1342,a,c,440,a)]. given #415 (F,wt=9): 2312 -Power(f8(c3,c3,c3,c3),f11(c2,c2)). [ur(33,b,2267,a,c,484,a)]. given #416 (F,wt=9): 2313 -Power(c3,f11(c2 * c2,c2 * c2)). [ur(33,b,2267,a,c,483,a)]. given #417 (F,wt=9): 2318 -Power(f8(c2,c2,c2,c2),f11(c3,c3)). [ur(33,b,2267,a,c,450,a)]. given #418 (T,wt=10): 838 Power(f3(x,x * (x * x),x),x). [resolve(91,a,298,a),flip(a),unit_del(a,29)]. given #419 (T,wt=10): 1196 -Power(x,f11(y * y,y)) | Power(x,y). [resolve(1140,a,33,b)]. given #420 (T,wt=10): 1197 -Power(x,y) | Power(f11(x * x,x),y). [resolve(1140,a,33,a)]. given #421 (T,wt=10): 1260 -Power(x,f11(f11(c1,c2),c2)) | Power(x,c1). [resolve(1217,a,33,b)]. given #422 (A,wt=21): 122 -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 #423 (F,wt=9): 2319 -Power(c2,f11(f11(c3,c2),f11(c3,c2))). [ur(33,b,2267,a,c,449,a)]. given #424 (F,wt=9): 2320 -Power(c2,f11(c3 * c3,c3 * c3)). [ur(33,b,2267,a,c,448,a)]. given #425 (F,wt=9): 2327 -Power(c2,f11(c3 * c2,c3 * c2)). [ur(33,b,2267,a,c,434,a)]. given #426 (F,wt=9): 2329 -Power(c3,f11(c2 * c3,c2 * c3)). [ur(33,b,2267,a,c,429,a)]. given #427 (T,wt=9): 8406 Power(x,f8(x,x,x * x,x)). [resolve(122,b,234,a),unit_del(a,32)]. given #428 (T,wt=10): 1261 -Power(c1,x) | Power(f11(f11(c1,c2),c2),x). [resolve(1217,a,33,a)]. given #429 (T,wt=10): 1357 -Power(x,f11(f11(c3,c2),c2)) | Power(x,c3). [resolve(1310,a,33,b)]. given #430 (T,wt=10): 1358 -Power(c3,x) | Power(f11(f11(c3,c2),c2),x). [resolve(1310,a,33,a)]. given #431 (A,wt=18): 123 -Power(x,y * (x * z)) | Power(y,f8(y * (x * z),x,y,z)). [resolve(51,b,32,a)]. given #432 (F,wt=9): 2336 -Power(c3,f11(c2,c2) * f11(c2,c2)). [ur(251,b,2316,a)]. given #433 (F,wt=9): 2337 -Power(c3,f11(f11(c2,c2),f11(c2,c2))). [ur(33,b,2267,a,c,2316,a)]. given #434 (F,wt=9): 2349 -Power(c2,f11(c3,c3) * f11(c3,c3)). [ur(251,b,2325,a)]. given #435 (F,wt=9): 2350 -Power(c2,f11(f11(c3,c3),f11(c3,c3))). [ur(33,b,2267,a,c,2325,a)]. given #436 (T,wt=10): 2288 Period(x,y) | f11(x,x) != y * z. [resolve(2267,a,74,b),flip(b)]. given #437 (T,wt=10): 2299 -Power(x,y) | Power(x * f11(y,y),y). [resolve(2267,a,34,b)]. given #438 (T,wt=10): 2300 -Power(x,y) | Power(f11(y,y) * x,y). [resolve(2267,a,34,a)]. given #439 (T,wt=10): 2393 Power(f3(x,f11(x,x) * x,x),x). [resolve(2285,a,91,a),flip(a),unit_del(a,30)]. given #440 (A,wt=23): 124 -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 #441 (F,wt=9): 2443 -Power(c3 * c2,f11(c2,c2) * c2). [ur(33,b,2285,a,c,436,a)]. given #442 (F,wt=9): 2445 -Power(c2 * c3,f11(c3,c3) * c3). [ur(33,b,2285,a,c,431,a)]. given #443 (F,wt=9): 2508 -Power(c3 * c2,c2 * f11(c2,c2)). [ur(33,b,2286,a,c,436,a)]. given #444 (F,wt=9): 2510 -Power(c2 * c3,c3 * f11(c3,c3)). [ur(33,b,2286,a,c,431,a)]. given #445 (T,wt=9): 9213 Power(x,f8(x,x * x,x,x)). [resolve(124,b,234,a),unit_del(a,178)]. given #446 (T,wt=10): 2394 Power(f3(x,x,f11(x,x) * x),x). [resolve(2285,a,90,a),unit_del(a,30)]. given #447 (T,wt=10): 2414 -Power(x,f11(y,y) * y) | Power(x,y). [resolve(2285,a,33,b)]. given #448 (T,wt=10): 2415 -Power(x,y) | Power(f11(x,x) * x,y). [resolve(2285,a,33,a)]. given #449 (A,wt=23): 125 -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 #450 (F,wt=9): 2626 -Power(c3,f11(c2 * f11(c2,c2),c2)). [ur(33,b,494,a,c,2498,a)]. given #451 (F,wt=9): 2642 -Power(c2,f11(c3 * f11(c3,c3),c3)). [ur(33,b,494,a,c,2507,a)]. given #452 (F,wt=9): 2878 -Power(c3 * c2,f11(c2,c2 * c2)). [ur(33,b,2808,a,c,436,a)]. given #453 (F,wt=9): 2880 -Power(c2 * c3,f11(c3,c3 * c3)). [ur(33,b,2808,a,c,431,a)]. given #454 (T,wt=10): 2462 Power(f3(x,x * f11(x,x),x),x). [resolve(2286,a,91,a),flip(a),unit_del(a,29)]. given #455 (T,wt=10): 2463 Power(f3(x,x,x * f11(x,x)),x). [resolve(2286,a,90,a),unit_del(a,29)]. given #456 (T,wt=10): 2479 -Power(x,y * f11(y,y)) | Power(x,y). [resolve(2286,a,33,b)]. given #457 (T,wt=9): 10331 Power(f11(x * f11(x,x),x),x). [resolve(2479,a,494,a)]. given #458 (A,wt=18): 126 -Power(x,y * (x * z)) | Power(z,f8(y * (x * z),x,y,z)). [resolve(52,b,32,a)]. given #459 (F,wt=9): 3236 -Power(c2 * c3,f11(c3,f11(c3,c2))). [ur(33,b,3202,a,c,431,a)]. given #460 (F,wt=9): 3268 -Power(c2,f11(c3,c2) * f11(c3,c3)). [ur(33,b,2273,a,c,440,a)]. given #461 (F,wt=9): 3300 -Power(c2,f11(c3,c3) * f11(c3,c2)). [ur(33,b,2274,a,c,440,a)]. given #462 (F,wt=9): 3427 -Power(c3,f11(c2 * (x * c3),c2)). [ur(33,b,494,a,c,3390,a)]. given #463 (T,wt=10): 2480 -Power(x,y) | Power(x * f11(x,x),y). [resolve(2286,a,33,a)]. given #464 (T,wt=10): 2517 Period(x,y) | -Power(f11(f11(y,y),y),x). [resolve(2516,a,75,c)]. given #465 (T,wt=7): 10770 Period(f11(f11(x,x),x),x). [resolve(2517,b,32,a)]. given #466 (T,wt=10): 2845 -Power(x,f11(y,y * y)) | Power(x,y). [resolve(2808,a,33,b)]. given #467 (A,wt=23): 127 -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 #468 (F,wt=9): 3435 -Power(c3,c2 * (x * (y * c3))). [para(26(a,1),3390(a,2,2))]. given #469 (F,wt=9): 3563 -Power(c3,f11(c2,c2) * (c2 * c2)). [ur(33,b,2395,a,c,478,a)]. given #470 (F,wt=9): 3572 -Power(c2,f11(c3,c3) * (c3 * c3)). [ur(33,b,2395,a,c,440,a)]. given #471 (F,wt=9): 3637 -Power(c3,c2 * (f11(c2,c2) * c2)). [ur(33,b,2396,a,c,478,a)]. given #472 (T,wt=10): 2846 -Power(x,y) | Power(f11(x,x * x),y). [resolve(2808,a,33,a)]. given #473 (T,wt=10): 3078 -Power(x,f11(c1,f11(c1,c2))) | Power(x,c1). [resolve(2915,a,33,b)]. given #474 (T,wt=10): 3079 -Power(c1,x) | Power(f11(c1,f11(c1,c2)),x). [resolve(2915,a,33,a)]. given #475 (T,wt=10): 3232 -Power(x,f11(c3,f11(c3,c2))) | Power(x,c3). [resolve(3202,a,33,b)]. given #476 (A,wt=21): 128 -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 #477 (F,wt=9): 3646 -Power(c2,c3 * (f11(c3,c3) * c3)). [ur(33,b,2396,a,c,440,a)]. given #478 (F,wt=9): 3715 -Power(c3,c2 * (c2 * f11(c2,c2))). [ur(33,b,2464,a,c,478,a)]. given #479 (F,wt=9): 3724 -Power(c2,c3 * (c3 * f11(c3,c3))). [ur(33,b,2464,a,c,440,a)]. given #480 (F,wt=9): 3753 -Power(c2,f11(c3 * (x * c2),c3)). [ur(33,b,494,a,c,3391,a)]. given #481 (T,wt=10): 3233 -Power(c3,x) | Power(f11(c3,f11(c3,c2)),x). [resolve(3202,a,33,a)]. given #482 (T,wt=10): 3902 -Power(x,f11(f11(y,y),y)) | Power(x,y). [resolve(3834,a,33,b)]. given #483 (T,wt=10): 3903 -Power(x,y) | Power(f11(f11(x,x),x),y). [resolve(3834,a,33,a)]. given #484 (T,wt=10): 4231 -Power(x,f11(y,f11(y,y))) | Power(x,y). [resolve(4017,a,33,b)]. given #485 (A,wt=14): 138 Shorter(x * y,z) | -Shorter(x * (y * u),z * u). [para(26(a,1),59(b,1))]. given #486 (F,wt=9): 3758 -Power(c2,c3 * (x * (y * c2))). [para(26(a,1),3391(a,2,2))]. given #487 (F,wt=9): 3759 -Power(c2 * (x * c3),f11(c3,c3)). [ur(2301,b,3392,a)]. given #488 (F,wt=9): 3760 -Power(c2 * (x * c3),c3 * c3). [ur(251,b,3392,a)]. given #489 (F,wt=9): 3761 -Power(c2 * (x * c3),f11(c3,c2)). [ur(216,b,3392,a)]. given #490 (T,wt=10): 4232 -Power(x,y) | Power(f11(x,f11(x,x)),y). [resolve(4017,a,33,a)]. given #491 (T,wt=11): 167 x * f9(x,x * y) = x * y. [xx_res(72,a)]. given #492 (T,wt=7): 11773 f9(x,x * y) = y. [resolve(167,a,27,a)]. given #493 (T,wt=11): 169 c2 * f9(c2,f11(c1,c2)) = f11(c1,c2). [resolve(73,a,69,a)]. given #494 (A,wt=14): 139 Shorter(x,y * z) | -Shorter(x * u,y * (z * u)). [para(26(a,1),59(b,2))]. given #495 (F,wt=5): 11779 f11(c1,c2) != c2. [para(169(a,1),29(a,1))]. given #496 (F,wt=5): 11811 -Shorter(f11(c1,c2),c2). [para(169(a,1),131(a,1))]. given #497 (F,wt=5): 11816 -Shorter(f11(c1,c2),c1). [para(169(a,1),188(a,1))]. given #498 (F,wt=5): 11817 -Shorter(f11(c1,c2),c3). [para(169(a,1),194(a,1))]. given #499 (T,wt=5): 11796 Shorter(c2,f11(c1,c2)). [para(169(a,1),56(a,2))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 125 (0.00 of 1.87 sec). given #500 (T,wt=7): 11818 Shorter(c2,x * f11(c1,c2)). [para(169(a,1),254(a,2,2))]. given #501 (T,wt=7): 11947 Shorter(c2,f11(c1,c2) * x). [resolve(11796,a,129,a)]. given #502 (T,wt=8): 11827 -Shorter(f11(c1,c2),x) | Shorter(c2,x). [para(169(a,1),130(a,1))]. given #503 (A,wt=14): 140 Shorter(x,y) | -Shorter(z * (u * x),z * (u * y)). [para(26(a,1),61(b,1)),rewrite([26(5)])]. given #504 (F,wt=7): 11824 -Shorter(f11(c1,c2),c3 * c1). [para(169(a,1),162(a,1))]. given #505 (F,wt=7): 11826 f11(c1,c2) != c3 * x. [para(169(a,1),163(a,2)),flip(a)]. given #506 (F,wt=7): 11838 -Shorter(x * f11(c1,c2),c2). [para(169(a,1),199(a,1,2))]. given #507 (F,wt=7): 11848 -Shorter(x * f11(c1,c2),c1). [para(169(a,1),272(a,1,2))]. given #508 (T,wt=8): 11829 Period(x,c2) | f11(c1,c2) != x. [para(169(a,1),171(b,1))]. given #509 (T,wt=8): 11950 -Shorter(x,c2) | Shorter(x,f11(c1,c2)). [resolve(11796,a,55,b)]. given #510 (T,wt=9): 11797 Shorter(f9(c2,f11(c1,c2)),f11(c1,c2)). [para(169(a,1),57(a,2))]. given #511 (T,wt=9): 11840 Shorter(x * c2,x * f11(c1,c2)). [para(169(a,1),132(a,2,2))]. given #512 (A,wt=14): 144 Shorter(x * y,z) | -Shorter(x * (y * u),u * z). [para(26(a,1),63(b,1))]. given #513 (F,wt=7): 11849 -Shorter(x * f11(c1,c2),c3). [para(169(a,1),283(a,1,2))]. given #514 (F,wt=7): 11855 -Shorter(f11(c1,c2),c1 * c3). [para(169(a,1),1125(a,1))]. given #515 (F,wt=7): 11929 -Shorter(f11(c1,c2) * x,c2). [ur(130,b,11811,a)]. given #516 (F,wt=7): 11935 -Shorter(f11(c1,c2) * x,c1). [ur(130,b,11816,a)]. given #517 (T,wt=9): 11846 Shorter(c2 * x,x * f11(c1,c2)). [para(169(a,1),142(a,2,2))]. given #518 (T,wt=9): 11853 Shorter(c2,x * (y * f11(c1,c2))). [para(169(a,1),297(a,2,2,2))]. given #519 (T,wt=9): 11854 Period(x * f11(c1,c2),x * c2). [para(169(a,1),488(a,1,2))]. given #520 (T,wt=9): 11878 Period(f11(c1,c2),f11(c1,c2) * c2). [para(169(a,1),2261(a,1)),rewrite([11776(12)])]. given #521 (A,wt=14): 145 Shorter(x,y) | -Shorter(x * (z * u),z * (u * y)). [para(26(a,1),63(b,2))]. given #522 (F,wt=7): 11941 -Shorter(f11(c1,c2) * x,c3). [ur(130,b,11817,a)]. given #523 (F,wt=9): 3792 -Power(c2 * (x * (y * c3)),c3). [para(26(a,1),3392(a,1,2))]. given #524 (F,wt=9): 3793 -Power(c3 * (x * c2),f11(c2,c2)). [ur(2301,b,3393,a)]. given #525 (F,wt=9): 3794 -Power(c3 * (x * c2),c2 * c2). [ur(251,b,3393,a)]. given #526 (T,wt=9): 11946 Shorter(c2,x * (f11(c1,c2) * y)). [resolve(11796,a,293,a)]. given #527 (T,wt=9): 11948 Shorter(x * c2,f11(c1,c2) * x). [resolve(11796,a,64,a)]. given #528 (T,wt=9): 11949 Shorter(c2 * x,f11(c1,c2) * x). [resolve(11796,a,58,a)]. given #529 (T,wt=10): 11875 Period(x,c2) | f11(c1,c2) != x * x. [para(169(a,1),235(b,1))]. given #530 (A,wt=14): 147 Shorter(x,y) | -Shorter(z * (u * x),y * (z * u)). [para(26(a,1),65(b,1))]. given #531 (F,wt=9): 3812 -Power(c3 * (x * (y * c2)),c2). [para(26(a,1),3393(a,1,2))]. given #532 (F,wt=9): 3863 -Power(c2 * c3,f11(f11(c3,c3),c3)). [ur(33,b,2519,a,c,2328,a)]. given #533 (F,wt=9): 3864 -Power(c3 * c2,f11(f11(c2,c2),c2)). [ur(33,b,2519,a,c,2326,a)]. given #534 (F,wt=9): 4274 -Power(c3 * c2,f11(c2,f11(c2,c2))). [ur(33,b,4017,a,c,436,a)]. given #535 (T,wt=10): 11899 -Shorter(x * f11(c1,c2),y) | Shorter(c2,y). [para(169(a,1),294(a,1,2))]. given #536 (T,wt=10): 11913 Period(x,c2) | f11(c1,c2) != f11(x,x). [para(169(a,1),2288(b,2)),flip(b)]. given #537 (T,wt=10): 11957 -Shorter(x,c2) | Shorter(x,y * f11(c1,c2)). [resolve(11818,a,55,b)]. given #538 (T,wt=10): 11964 -Shorter(x,c2) | Shorter(x,f11(c1,c2) * y). [resolve(11947,a,55,b)]. given #539 (A,wt=14): 148 Shorter(x,y * z) | -Shorter(u * x,y * (z * u)). [para(26(a,1),65(b,2))]. given #540 (F,wt=9): 4277 -Power(c2 * c3,f11(c3,f11(c3,c3))). [ur(33,b,4017,a,c,431,a)]. given #541 (F,wt=9): 4384 -Power(c3,f11(c2,c2 * c2) * c2). [ur(33,b,2829,a,c,478,a)]. given #542 (F,wt=9): 4393 -Power(c2,f11(c3,c3 * c3) * c3). [ur(33,b,2829,a,c,440,a)]. Low Water (keep): wt=40.000, iters=6696 given #543 (F,wt=9): 4578 -Power(c3,c2 * f11(c2,c2 * c2)). [ur(33,b,2830,a,c,478,a)]. given #544 (T,wt=10): 11965 -Shorter(f11(c1,c2) * x,y) | Shorter(c2,y). [resolve(11947,a,55,a)]. given #545 (T,wt=11): 170 c2 * f9(c2,f11(c3,c2)) = f11(c3,c2). [resolve(73,a,68,a)]. given #546 (T,wt=5): 12870 Shorter(c2,f11(c3,c2)). [para(170(a,1),56(a,2))]. given #547 (T,wt=7): 12892 Shorter(c2,x * f11(c3,c2)). [para(170(a,1),254(a,2,2))]. given #548 (A,wt=23): 149 Shorter(x * y,x * z) | x * f12(u,y * u,z,x * y,x) = x * y. [resolve(67,a,26,a)]. given #549 (F,wt=5): 12853 f11(c3,c2) != c2. [para(170(a,1),29(a,1))]. given #550 (F,wt=5): 12885 -Shorter(f11(c3,c2),c2). [para(170(a,1),131(a,1))]. given #551 (F,wt=5): 12890 -Shorter(f11(c3,c2),c1). [para(170(a,1),188(a,1))]. given #552 (F,wt=5): 12891 -Shorter(f11(c3,c2),c3). [para(170(a,1),194(a,1))]. given #553 (T,wt=7): 13007 Shorter(c2,f11(c3,c2) * x). [resolve(12870,a,129,a)]. given #554 (T,wt=8): 12901 -Shorter(f11(c3,c2),x) | Shorter(c2,x). [para(170(a,1),130(a,1))]. given #555 (T,wt=8): 12903 Period(x,c2) | f11(c3,c2) != x. [para(170(a,1),171(b,1))]. given #556 (T,wt=8): 13010 -Shorter(x,c2) | Shorter(x,f11(c3,c2)). [resolve(12870,a,55,b)]. given #557 (A,wt=30): 150 x * (y * z) != u * w | Shorter(x * y,u * v5) | u * f12(z,w,v5,x * y,u) = x * y. [para(26(a,1),67(a,1))]. given #558 (F,wt=7): 12898 -Shorter(f11(c3,c2),c3 * c1). [para(170(a,1),162(a,1))]. given #559 (F,wt=7): 12900 f11(c3,c2) != c3 * x. [para(170(a,1),163(a,2)),flip(a)]. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 1.99 (+ 0.01) seconds. % Length of proof is 35. % Level of proof is 6. % Maximum clause weight is 25.000. % Given clauses 559 (93.167 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]. 10 Shorter(x,y) & Shorter(y,z) -> Shorter(x,z) # label(non_clause). [assumption]. 15 Prefix(x,y) <-> (exists z x * z = y) # label(non_clause). [assumption]. 17 Period(x,y) <-> (exists z (Power(z,x) & Prefix(y,z))) # label(non_clause). [assumption]. 18 u * u1 = x * x1 & -Shorter(u,x * y) -> (exists u3 u = x * u3) # label("Lemma 4") # label(non_clause). [assumption]. 19 Period(x,u) & Period(y,u) & -Shorter(u,x * y) -> (exists u3 u = x * u3) # label("Lemma Reform-2a") # label(non_clause) # label(goal). [goal]. 21 -Prefix(x,y) | x * f9(x,y) = y. [clausify(15)]. 22 -Period(x,y) | Prefix(y,f11(x,y)). [clausify(17)]. 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)]. 55 -Shorter(x,y) | -Shorter(y,z) | Shorter(x,z). [clausify(10)]. 56 Shorter(x,x * y). [assumption]. 66 -Period(x,y) | Power(f11(x,y),x). [clausify(17)]. 67 x * y != z * u | Shorter(x,z * w) | z * f12(y,u,w,x,z) = x # label("Lemma 4"). [clausify(18)]. 68 Period(c3,c2) # label("Lemma Reform-2a"). [deny(19)]. 70 -Shorter(c2,c3 * c1) # label("Lemma Reform-2a"). [deny(19)]. 71 c3 * x != c2 # label("Lemma Reform-2a"). [deny(19)]. 73 -Period(x,y) | y * f9(y,f11(x,y)) = f11(x,y). [resolve(22,b,21,a)]. 82 x * (y * z) != z. [para(26(a,1),30(a,1))]. 89 -Power(x,y) | Power(x * y,y). [resolve(34,b,32,a)]. 96 -Power(x,y) | x = y | f3(y,y,x) * x = y | y * f3(y,y,x) = x. [resolve(38,a,32,a)]. 153 Power(f11(c3,c2),c3). [resolve(68,a,66,a)]. 162 -Shorter(c2 * x,c3 * c1). [ur(55,a,56,a,c,70,a)]. 163 c3 * x != c2 * y. [ur(67,b,70,a,c,71,a),flip(a)]. 170 c2 * f9(c2,f11(c3,c2)) = f11(c3,c2). [resolve(73,a,68,a)]. 408 Power(f11(c3,c2) * c3,c3). [resolve(89,a,153,a)]. 1575 c3 * f3(c3,c3,f11(c3,c2) * c3) = f11(c3,c2) * c3. [resolve(96,a,408,a),unit_del(a,30),unit_del(b,82)]. 12898 -Shorter(f11(c3,c2),c3 * c1). [para(170(a,1),162(a,1))]. 12900 f11(c3,c2) != c3 * x. [para(170(a,1),163(a,2)),flip(a)]. 13164 f11(c3,c2) * x != c3 * y. [ur(67,b,12898,a,c,12900,a(flip))]. 13165 $F. [resolve(13164,a,1575,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=559. Generated=25088. Kept=13139. proofs=1. Usable=556. Sos=12435. Demods=191. Limbo=11, Disabled=193. Hints=0. Kept_by_rule=0, Deleted_by_rule=131. Forward_subsumed=11804. Back_subsumed=95. Sos_limit_deleted=14. Sos_displaced=0. Sos_removed=0. New_demodulators=217 (0 lex), Back_demodulated=37. Back_unit_deleted=4. Demod_attempts=430840. Demod_rewrites=15650. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=141276. Nonunit_bsub_feature_tests=145986. Megabytes=32.68. User_CPU=1.99, System_CPU=0.01, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 17977 exit (max_proofs) ------  Process 17977 exit (max_proofs) Wed Jun 14 05:43:56 2017