============================== Prover9 =============================== Prover9 (64) version 2017-05A, May 2017. Process 17966 was started by veroff on theorem, Wed Jun 14 05:43:51 2017 The command was "prover9 -f p9header axioms.in Lemma_4.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 Lemma_4.in formulas(goals). 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) # 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)]. c4 * c1 = c5 * c2 # label("Lemma 4"). [deny(18)]. -Shorter(c4,c5 * c3) # label("Lemma 4"). [deny(18)]. c5 * x != c4 # label("Lemma 4"). [deny(18)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating Prefix/2 19 Prefix(x,y) | x * z != y. [clausify(15)]. 20 -Prefix(x,y) | x * f9(x,y) = y. [clausify(15)]. Derived: x * y != z | x * f9(x,z) = z. [resolve(19,a,20,a)]. 21 -Period(x,y) | Prefix(y,f11(x,y)). [clausify(17)]. Derived: -Period(x,y) | y * f9(y,f11(x,y)) = f11(x,y). [resolve(21,b,20,a)]. 22 Period(x,y) | -Power(z,x) | -Prefix(y,z). [clausify(17)]. Derived: Period(x,y) | -Power(z,x) | y * u != z. [resolve(22,c,19,a)]. Derived: Period(x,y) | -Power(f11(z,y),x) | -Period(z,y). [resolve(22,c,21,b)]. Eliminating Suffix/2 23 Suffix(x,y) | z * x != y. [clausify(16)]. 24 -Suffix(x,y) | f10(x,y) * x = y. [clausify(16)]. Derived: x * y != z | f10(y,z) * y = z. [resolve(23,a,24,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, c4, c5, *, f9, f10, f11, f3, f4, f5, f6, f7, f1, f2, f8 ]). 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: 25 (x * y) * z = x * (y * z). [assumption]. kept: 26 x * y != x * z | y = z. [clausify(1)]. kept: 27 x * y != z * y | x = z. [clausify(2)]. kept: 28 x * y != x. [assumption]. kept: 29 x * y != y. [assumption]. kept: 30 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: 31 Power(x,x). [assumption]. kept: 32 -Power(x,y) | -Power(y,z) | Power(x,z). [clausify(4)]. kept: 33 -Power(x,y) | -Power(z,y) | Power(x * z,y). [clausify(5)]. kept: 34 -Power(x,y) | -Power(z,y) | z = x | Power(f3(y,x,z),y). [clausify(6)]. kept: 35 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | x * f3(y,x,z) = z. [clausify(6)]. kept: 36 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | f3(y,x,z) * x = z. [clausify(6)]. kept: 37 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | x * f3(y,x,z) = z. [clausify(6)]. kept: 38 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | f3(y,x,z) * x = z. [clausify(6)]. kept: 39 -Power(x * y,z) | Power(x,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. kept: 40 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. kept: 41 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. kept: 42 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. kept: 43 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. kept: 44 -Power(x * y,z) | Power(y,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. kept: 45 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. kept: 46 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. kept: 47 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. kept: 48 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. kept: 49 -Power(x,y) | -Power(z * (x * u),y) | Power(x,f8(y,x,z,u)). [clausify(8)]. kept: 50 -Power(x,y) | -Power(z * (x * u),y) | Power(z,f8(y,x,z,u)). [clausify(8)]. kept: 51 -Power(x,y) | -Power(z * (x * u),y) | Power(u,f8(y,x,z,u)). [clausify(8)]. kept: 52 -Shorter(x,x). [assumption]. kept: 53 -Shorter(x,y) | -Shorter(y,x). [clausify(9)]. kept: 54 -Shorter(x,y) | -Shorter(y,z) | Shorter(x,z). [clausify(10)]. kept: 55 Shorter(x,x * y). [assumption]. kept: 56 Shorter(x,y * x). [assumption]. kept: 57 -Shorter(x,y) | Shorter(x * z,y * z). [clausify(11)]. kept: 58 Shorter(x,y) | -Shorter(x * z,y * z). [clausify(11)]. kept: 59 -Shorter(x,y) | Shorter(z * x,z * y). [clausify(12)]. kept: 60 Shorter(x,y) | -Shorter(z * x,z * y). [clausify(12)]. kept: 61 -Shorter(x,y) | Shorter(x * z,z * y). [clausify(13)]. kept: 62 Shorter(x,y) | -Shorter(x * z,z * y). [clausify(13)]. kept: 63 -Shorter(x,y) | Shorter(z * x,y * z). [clausify(14)]. kept: 64 Shorter(x,y) | -Shorter(z * x,y * z). [clausify(14)]. kept: 65 -Period(x,y) | Power(f11(x,y),x). [clausify(17)]. 66 c4 * c1 = c5 * c2 # label("Lemma 4"). [deny(18)]. kept: 67 c5 * c2 = c4 * c1. [copy(66),flip(a)]. kept: 68 -Shorter(c4,c5 * c3) # label("Lemma 4"). [deny(18)]. kept: 69 c5 * x != c4 # label("Lemma 4"). [deny(18)]. kept: 70 x * y != z | x * f9(x,z) = z. [resolve(19,a,20,a)]. kept: 71 -Period(x,y) | y * f9(y,f11(x,y)) = f11(x,y). [resolve(21,b,20,a)]. kept: 72 Period(x,y) | -Power(z,x) | y * u != z. [resolve(22,c,19,a)]. kept: 73 Period(x,y) | -Power(f11(z,y),x) | -Period(z,y). [resolve(22,c,21,b)]. kept: 74 x * y != z | f10(y,z) * y = z. [resolve(23,a,24,a)]. kept: 75 -Power(x,y) | Power(x * x,y). [factor(33,a,b)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 25 (x * y) * z = x * (y * z). [assumption]. 26 x * y != x * z | y = z. [clausify(1)]. 27 x * y != z * y | x = z. [clausify(2)]. 28 x * y != x. [assumption]. 29 x * y != y. [assumption]. 30 x * y != z * u | x = z | z * f1(z,x,u,y) = x | f2(z,x,u,y) * u = y # label("EQD"). [clausify(3)]. 31 Power(x,x). [assumption]. 32 -Power(x,y) | -Power(y,z) | Power(x,z). [clausify(4)]. 33 -Power(x,y) | -Power(z,y) | Power(x * z,y). [clausify(5)]. 34 -Power(x,y) | -Power(z,y) | z = x | Power(f3(y,x,z),y). [clausify(6)]. 35 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | x * f3(y,x,z) = z. [clausify(6)]. 36 -Power(x,y) | -Power(z,y) | z = x | z * f3(y,x,z) = x | f3(y,x,z) * x = z. [clausify(6)]. 37 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | x * f3(y,x,z) = z. [clausify(6)]. 38 -Power(x,y) | -Power(z,y) | z = x | f3(y,x,z) * z = x | f3(y,x,z) * x = z. [clausify(6)]. 39 -Power(x * y,z) | Power(x,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. 40 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. 41 -Power(x * y,z) | Power(x,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. 42 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. 43 -Power(x * y,z) | Power(x,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. 44 -Power(x * y,z) | Power(y,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. 45 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | f6(x,y,z) * f4(x,y,z) = x. [clausify(7)]. 46 -Power(x * y,z) | Power(y,z) | f4(x,y,z) = x | Power(f6(x,y,z),z). [clausify(7)]. 47 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | f5(x,y,z) * f7(x,y,z) = y. [clausify(7)]. 48 -Power(x * y,z) | Power(y,z) | f5(x,y,z) = y | Power(f7(x,y,z),z). [clausify(7)]. 49 -Power(x,y) | -Power(z * (x * u),y) | Power(x,f8(y,x,z,u)). [clausify(8)]. 50 -Power(x,y) | -Power(z * (x * u),y) | Power(z,f8(y,x,z,u)). [clausify(8)]. 51 -Power(x,y) | -Power(z * (x * u),y) | Power(u,f8(y,x,z,u)). [clausify(8)]. 52 -Shorter(x,x). [assumption]. 53 -Shorter(x,y) | -Shorter(y,x). [clausify(9)]. 54 -Shorter(x,y) | -Shorter(y,z) | Shorter(x,z). [clausify(10)]. 55 Shorter(x,x * y). [assumption]. 56 Shorter(x,y * x). [assumption]. 57 -Shorter(x,y) | Shorter(x * z,y * z). [clausify(11)]. 58 Shorter(x,y) | -Shorter(x * z,y * z). [clausify(11)]. 59 -Shorter(x,y) | Shorter(z * x,z * y). [clausify(12)]. 60 Shorter(x,y) | -Shorter(z * x,z * y). [clausify(12)]. 61 -Shorter(x,y) | Shorter(x * z,z * y). [clausify(13)]. 62 Shorter(x,y) | -Shorter(x * z,z * y). [clausify(13)]. 63 -Shorter(x,y) | Shorter(z * x,y * z). [clausify(14)]. 64 Shorter(x,y) | -Shorter(z * x,y * z). [clausify(14)]. 65 -Period(x,y) | Power(f11(x,y),x). [clausify(17)]. 67 c5 * c2 = c4 * c1. [copy(66),flip(a)]. 68 -Shorter(c4,c5 * c3) # label("Lemma 4"). [deny(18)]. 69 c5 * x != c4 # label("Lemma 4"). [deny(18)]. 70 x * y != z | x * f9(x,z) = z. [resolve(19,a,20,a)]. 71 -Period(x,y) | y * f9(y,f11(x,y)) = f11(x,y). [resolve(21,b,20,a)]. 72 Period(x,y) | -Power(z,x) | y * u != z. [resolve(22,c,19,a)]. 73 Period(x,y) | -Power(f11(z,y),x) | -Period(z,y). [resolve(22,c,21,b)]. 74 x * y != z | f10(y,z) * y = z. [resolve(23,a,24,a)]. 75 -Power(x,y) | Power(x * x,y). [factor(33,a,b)]. end_of_list. formulas(demodulators). 25 (x * y) * z = x * (y * z). [assumption]. 67 c5 * c2 = c4 * c1. [copy(66),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=11): 25 (x * y) * z = x * (y * z). [assumption]. given #2 (I,wt=10): 26 x * y != x * z | y = z. [clausify(1)]. given #3 (I,wt=10): 27 x * y != z * y | x = z. [clausify(2)]. given #4 (I,wt=5): 28 x * y != x. [assumption]. given #5 (I,wt=5): 29 x * y != y. [assumption]. given #6 (I,wt=28): 30 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): 31 Power(x,x). [assumption]. given #8 (I,wt=9): 32 -Power(x,y) | -Power(y,z) | Power(x,z). [clausify(4)]. given #9 (I,wt=11): 33 -Power(x,y) | -Power(z,y) | Power(x * z,y). [clausify(5)]. given #10 (I,wt=15): 34 -Power(x,y) | -Power(z,y) | z = x | Power(f3(y,x,z),y). [clausify(6)]. given #11 (I,wt=25): 35 -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): 36 -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): 37 -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): 38 -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): 39 -Power(x * y,z) | Power(x,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. given #16 (I,wt=25): 40 -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): 41 -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): 42 -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): 43 -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): 44 -Power(x * y,z) | Power(y,z) | f4(x,y,z) * f5(x,y,z) = z. [clausify(7)]. given #21 (I,wt=25): 45 -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): 46 -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): 47 -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): 48 -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): 49 -Power(x,y) | -Power(z * (x * u),y) | Power(x,f8(y,x,z,u)). [clausify(8)]. given #26 (I,wt=17): 50 -Power(x,y) | -Power(z * (x * u),y) | Power(z,f8(y,x,z,u)). [clausify(8)]. given #27 (I,wt=17): 51 -Power(x,y) | -Power(z * (x * u),y) | Power(u,f8(y,x,z,u)). [clausify(8)]. given #28 (I,wt=3): 52 -Shorter(x,x). [assumption]. given #29 (I,wt=6): 53 -Shorter(x,y) | -Shorter(y,x). [clausify(9)]. given #30 (I,wt=9): 54 -Shorter(x,y) | -Shorter(y,z) | Shorter(x,z). [clausify(10)]. given #31 (I,wt=5): 55 Shorter(x,x * y). [assumption]. given #32 (I,wt=5): 56 Shorter(x,y * x). [assumption]. given #33 (I,wt=10): 57 -Shorter(x,y) | Shorter(x * z,y * z). [clausify(11)]. given #34 (I,wt=10): 58 Shorter(x,y) | -Shorter(x * z,y * z). [clausify(11)]. given #35 (I,wt=10): 59 -Shorter(x,y) | Shorter(z * x,z * y). [clausify(12)]. given #36 (I,wt=10): 60 Shorter(x,y) | -Shorter(z * x,z * y). [clausify(12)]. given #37 (I,wt=10): 61 -Shorter(x,y) | Shorter(x * z,z * y). [clausify(13)]. given #38 (I,wt=10): 62 Shorter(x,y) | -Shorter(x * z,z * y). [clausify(13)]. given #39 (I,wt=10): 63 -Shorter(x,y) | Shorter(z * x,y * z). [clausify(14)]. given #40 (I,wt=10): 64 Shorter(x,y) | -Shorter(z * x,y * z). [clausify(14)]. given #41 (I,wt=8): 65 -Period(x,y) | Power(f11(x,y),x). [clausify(17)]. given #42 (I,wt=7): 67 c5 * c2 = c4 * c1. [copy(66),flip(a)]. given #43 (I,wt=5): 68 -Shorter(c4,c5 * c3) # label("Lemma 4"). [deny(18)]. given #44 (I,wt=5): 69 c5 * x != c4 # label("Lemma 4"). [deny(18)]. given #45 (I,wt=12): 70 x * y != z | x * f9(x,z) = z. [resolve(19,a,20,a)]. given #46 (I,wt=14): 71 -Period(x,y) | y * f9(y,f11(x,y)) = f11(x,y). [resolve(21,b,20,a)]. given #47 (I,wt=11): 72 Period(x,y) | -Power(z,x) | y * u != z. [resolve(22,c,19,a)]. given #48 (I,wt=11): 73 Period(x,y) | -Power(f11(z,y),x) | -Period(z,y). [resolve(22,c,21,b)]. given #49 (I,wt=12): 74 x * y != z | f10(y,z) * y = z. [resolve(23,a,24,a)]. given #50 (I,wt=8): 75 -Power(x,y) | Power(x * x,y). [factor(33,a,b)]. given #51 (A,wt=14): 76 x * (y * z) != x * (y * u) | z = u. [para(25(a,1),26(a,1)),rewrite([25(4)])]. given #52 (F,wt=3): 184 -Shorter(c4,c3). [ur(54,b,56,a,c,68,a)]. given #53 (F,wt=3): 185 -Shorter(c4,c5). [ur(54,b,55,a,c,68,a)]. given #54 (F,wt=5): 129 -Shorter(x * y,x). [resolve(55,a,53,b)]. given #55 (F,wt=5): 133 -Shorter(x * y,y). [resolve(56,a,53,b)]. given #56 (T,wt=5): 170 Shorter(c5,c4 * c1). [para(67(a,1),55(a,2))]. given #57 (T,wt=5): 171 Shorter(c2,c4 * c1). [para(67(a,1),56(a,2))]. given #58 (T,wt=5): 205 Power(x * x,x). [resolve(75,a,31,a)]. given #59 (T,wt=7): 134 Shorter(x,y * (z * x)). [para(25(a,1),56(a,2))]. given #60 (A,wt=14): 77 x * (y * z) != u * z | x * y = u. [para(25(a,1),27(a,1))]. given #61 (F,wt=5): 152 c4 * c1 != c5. [para(67(a,1),28(a,1))]. given #62 (F,wt=5): 153 c4 * c1 != c2. [para(67(a,1),29(a,1))]. given #63 (F,wt=5): 215 -Shorter(x * c4,c3). [ur(54,a,56,a,c,184,a)]. given #64 (F,wt=5): 216 -Shorter(c4 * x,c3). [ur(54,a,55,a,c,184,a)]. given #65 (T,wt=7): 266 Shorter(x,y * (x * z)). [resolve(134,a,62,b)]. given #66 (T,wt=7): 277 Shorter(c2,x * (c4 * c1)). [para(67(a,1),134(a,2,2))]. given #67 (T,wt=7): 310 Shorter(c5,x * (c4 * c1)). [para(67(a,1),266(a,2,2))]. given #68 (T,wt=8): 86 -Power(x,y) | Power(y * x,y). [resolve(33,a,31,a)]. given #69 (A,wt=9): 78 x * (y * z) != x * z. [ur(27,b,28,a),rewrite([25(2)])]. given #70 (F,wt=5): 221 -Shorter(x * c4,c5). [ur(54,a,56,a,c,185,a)]. given #71 (F,wt=5): 222 -Shorter(c4 * x,c5). [ur(54,a,55,a,c,185,a)]. given #72 (F,wt=5): 230 -Shorter(c4 * c1,c2). [para(67(a,1),133(a,1))]. given #73 (F,wt=7): 80 x * (y * z) != z. [para(25(a,1),29(a,1))]. given #74 (T,wt=7): 328 Power(x * (x * x),x). [resolve(86,a,205,a)]. given #75 (T,wt=7): 351 Power(x,f8(x,x,x,x)). [resolve(328,a,51,b),unit_del(a,31)]. given #76 (T,wt=8): 87 -Power(x,y) | Power(x * y,y). [resolve(33,b,31,a)]. given #77 (T,wt=8): 127 -Shorter(x,y) | Shorter(x,y * z). [resolve(55,a,54,b)]. given #78 (A,wt=9): 79 x * (y * z) != x * y. [ur(26,b,28,a)]. given #79 (F,wt=7): 141 -Shorter(x * y,y * x). [ur(62,a,52,a)]. given #80 (F,wt=5): 406 -Shorter(c1 * c4,c2). [ur(54,b,171,a,c,141,a)]. given #81 (F,wt=7): 186 -Shorter(x * c4,c5 * c3). [ur(54,a,56,a,c,68,a)]. given #82 (F,wt=7): 187 -Shorter(c4 * x,c5 * c3). [ur(54,a,55,a,c,68,a)]. given #83 (T,wt=7): 400 Shorter(c2,c4 * (c1 * x)). [resolve(127,a,171,a),rewrite([25(5)])]. given #84 (T,wt=7): 401 Shorter(c5,c4 * (c1 * x)). [resolve(127,a,170,a),rewrite([25(5)])]. given #85 (T,wt=8): 128 -Shorter(x * y,z) | Shorter(x,z). [resolve(55,a,54,a)]. given #86 (T,wt=8): 131 -Shorter(x,y) | Shorter(x,z * y). [resolve(56,a,54,b)]. given #87 (A,wt=15): 81 x * f1(x,x * y,y * z,z) = x * y. [resolve(30,a,25,a),unit_del(a,28),unit_del(c,80)]. given #88 (F,wt=7): 211 -Shorter(x * c4,c3 * x). [ur(64,a,184,a)]. given #89 (F,wt=7): 212 -Shorter(c4 * x,x * c3). [ur(62,a,184,a)]. given #90 (F,wt=7): 213 -Shorter(x * c4,x * c3). [ur(60,a,184,a)]. given #91 (F,wt=7): 214 -Shorter(c4 * x,c3 * x). [ur(58,a,184,a)]. given #92 (T,wt=8): 132 -Shorter(x * y,z) | Shorter(y,z). [resolve(56,a,54,a)]. given #93 (T,wt=8): 197 Period(x,y) | y * z != x. [resolve(72,b,31,a)]. given #94 (T,wt=5): 478 Period(c4 * c1,c5). [resolve(197,b,67,a)]. given #95 (T,wt=5): 482 Period(x * y,x). [xx_res(197,b)]. given #96 (A,wt=15): 82 f2(x * y,x,z,y * z) * z = y * z. [resolve(30,a,25,a(flip)),rewrite([25(7)]),flip(a),unit_del(a,28),unit_del(b,28)]. given #97 (F,wt=7): 217 -Shorter(x * c4,c5 * x). [ur(64,a,185,a)]. given #98 (F,wt=7): 218 -Shorter(c4 * x,x * c5). [ur(62,a,185,a)]. given #99 (F,wt=7): 219 -Shorter(x * c4,x * c5). [ur(60,a,185,a)]. given #100 (F,wt=7): 220 -Shorter(c4 * x,c5 * x). [ur(58,a,185,a)]. given #101 (T,wt=8): 235 -Shorter(x,c5) | Shorter(x,c4 * c1). [resolve(170,a,54,b)]. given #102 (T,wt=8): 236 -Shorter(c4 * c1,x) | Shorter(c5,x). [resolve(170,a,54,a)]. given #103 (T,wt=8): 242 -Shorter(x,c2) | Shorter(x,c4 * c1). [resolve(171,a,54,b)]. given #104 (T,wt=8): 243 -Shorter(c4 * c1,x) | Shorter(c2,x). [resolve(171,a,54,a)]. given #105 (A,wt=38): 83 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(25(a,1),30(a,1))]. given #106 (F,wt=7): 227 -Shorter(x * (y * z),y). [ur(54,b,56,a,c,129,a),rewrite([25(2)])]. given #107 (F,wt=7): 229 -Shorter(x * (y * z),z). [ur(54,b,56,a,c,133,a)]. given #108 (F,wt=7): 244 -Shorter(x * (c4 * c1),c2). [ur(54,b,171,a,c,133,a)]. given #109 (F,wt=7): 245 -Shorter(c4 * (c1 * x),c2). [ur(54,b,171,a,c,129,a),rewrite([25(4)])]. given #110 (T,wt=8): 263 -Power(x,y * y) | Power(x,y). [resolve(205,a,32,b)]. given #111 (T,wt=8): 484 Period(x,c5) | c4 * c1 != x. [para(67(a,1),197(b,1))]. given #112 (T,wt=9): 130 Shorter(x * y,x * (y * z)). [para(25(a,1),55(a,2))]. given #113 (T,wt=9): 135 Shorter(x * y,x * (z * y)). [resolve(57,a,55,a),rewrite([25(3)])]. given #114 (A,wt=38): 84 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(25(a,1),30(a,2)),rewrite([25(10)]),flip(a),flip(b)]. given #115 (F,wt=7): 273 -Shorter(x * (y * c4),c5). [ur(54,a,134,a,c,185,a)]. given #116 (F,wt=7): 274 -Shorter(x * (y * c4),c3). [ur(54,a,134,a,c,184,a)]. given #117 (F,wt=7): 294 -Shorter(x * (c4 * y),c3). [ur(54,a,55,a,c,215,a),rewrite([25(3)])]. given #118 (F,wt=7): 306 -Shorter(x * (c4 * y),c5). [ur(54,a,266,a,c,185,a)]. given #119 (T,wt=7): 560 Shorter(c2,c4 * (x * c1)). [resolve(135,a,243,a)]. given #120 (T,wt=7): 561 Shorter(c5,c4 * (x * c1)). [resolve(135,a,236,a)]. given #121 (T,wt=9): 139 Shorter(x * y,y * (z * x)). [resolve(61,a,56,a)]. given #122 (T,wt=7): 616 Shorter(c2,c1 * (x * c4)). [resolve(139,a,243,a)]. given #123 (A,wt=36): 85 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(25(a,2),30(a,2)),rewrite([25(3)]),flip(a)]. given #124 (F,wt=7): 348 x * (c4 * c1) != c2. [para(67(a,1),80(a,1,2))]. given #125 (F,wt=7): 411 -Shorter(c4 * c1,c2 * c5). [para(67(a,1),141(a,1))]. given #126 (F,wt=7): 412 -Shorter(c2 * c5,c4 * c1). [para(67(a,1),141(a,2))]. given #127 (F,wt=5): 664 -Shorter(c2 * c5,c1). [ur(131,b,412,a)]. given #128 (T,wt=7): 617 Shorter(c5,c1 * (x * c4)). [resolve(139,a,236,a)]. given #129 (T,wt=9): 140 Shorter(x * y,y * (x * z)). [resolve(61,a,55,a)]. given #130 (T,wt=7): 694 Shorter(c2,c1 * (c4 * x)). [resolve(140,a,243,a)]. given #131 (T,wt=7): 695 Shorter(c5,c1 * (c4 * x)). [resolve(140,a,236,a)]. given #132 (A,wt=12): 88 -Power(x,y) | x = y | Power(f3(y,y,x),y). [resolve(34,a,31,a)]. given #133 (F,wt=5): 666 -Shorter(c2 * c5,c4). [ur(127,b,412,a)]. given #134 (F,wt=7): 419 -Shorter(x * (c1 * c4),c2). [ur(54,a,56,a,c,406,a)]. given #135 (F,wt=7): 420 -Shorter(c1 * (c4 * x),c2). [ur(54,a,55,a,c,406,a),rewrite([25(4)])]. given #136 (F,wt=7): 437 -Shorter(c1 * (x * c4),c2). [ur(54,b,400,a,c,141,a),rewrite([25(4)])]. given #137 (T,wt=8): 723 Power(f3(x,x,x * x),x). [resolve(88,a,205,a),unit_del(a,28)]. given #138 (T,wt=9): 144 Shorter(x * y,z * (y * x)). [resolve(63,a,56,a),rewrite([25(3)])]. given #139 (T,wt=7): 769 Shorter(c2,x * (c1 * c4)). [resolve(144,a,243,a)]. given #140 (T,wt=7): 770 Shorter(c5,x * (c1 * c4)). [resolve(144,a,236,a)]. given #141 (A,wt=12): 89 -Power(x,y) | y = x | Power(f3(y,x,y),y). [resolve(34,b,31,a)]. given #142 (F,wt=7): 507 -Shorter(c2 * c4,c4 * c1). [para(67(a,1),217(a,2))]. given #143 (F,wt=3): 805 -Shorter(c2,c1). [ur(61,b,507,a)]. given #144 (F,wt=5): 814 -Shorter(x * c2,c1). [ur(132,b,805,a)]. given #145 (F,wt=5): 815 -Shorter(c2 * x,c1). [ur(128,b,805,a)]. given #146 (T,wt=8): 799 Power(f3(x,x * x,x),x). [resolve(89,a,205,a),flip(a),unit_del(a,28)]. given #147 (T,wt=9): 231 Shorter(x * c5,c4 * (c1 * x)). [resolve(170,a,63,a),rewrite([25(6)])]. given #148 (T,wt=5): 857 Shorter(c5,c1 * c4). [resolve(231,a,60,b)]. given #149 (T,wt=8): 872 -Shorter(x,c5) | Shorter(x,c1 * c4). [resolve(857,a,54,b)]. given #150 (A,wt=22): 90 -Power(x,y) | x = y | x * f3(y,y,x) = y | y * f3(y,y,x) = x. [resolve(35,a,31,a)]. given #151 (F,wt=7): 569 -Shorter(c4 * (x * c1),c2). [ur(54,a,135,a,c,230,a)]. given #152 (F,wt=7): 724 -Shorter(x * (c2 * c5),c4). [ur(132,b,666,a)]. given #153 (F,wt=7): 725 -Shorter(c2 * (c5 * x),c4). [ur(128,b,666,a),rewrite([25(4)])]. given #154 (F,wt=7): 731 -Shorter(c5 * (x * c2),c4). [ur(54,a,139,a,c,666,a)]. given #155 (T,wt=8): 873 -Shorter(c1 * c4,x) | Shorter(c5,x). [resolve(857,a,54,a)]. given #156 (T,wt=9): 232 Shorter(c5 * x,x * (c4 * c1)). [resolve(170,a,61,a)]. given #157 (T,wt=9): 233 Shorter(x * c5,x * (c4 * c1)). [resolve(170,a,59,a)]. given #158 (T,wt=9): 234 Shorter(c5 * x,c4 * (c1 * x)). [resolve(170,a,57,a),rewrite([25(6)])]. given #159 (A,wt=22): 91 -Power(x,y) | y = x | y * f3(y,x,y) = x | x * f3(y,x,y) = y. [resolve(35,b,31,a)]. given #160 (F,wt=7): 732 -Shorter(c2 * (x * c5),c4). [ur(54,a,135,a,c,666,a)]. given #161 (F,wt=7): 816 -Shorter(x * c2,c1 * x). [ur(64,a,805,a)]. given #162 (F,wt=7): 817 -Shorter(c2 * x,x * c1). [ur(62,a,805,a)]. given #163 (F,wt=7): 818 -Shorter(x * c2,x * c1). [ur(60,a,805,a)]. given #164 (T,wt=9): 238 Shorter(x * c2,c4 * (c1 * x)). [resolve(171,a,63,a),rewrite([25(6)])]. given #165 (T,wt=5): 968 Shorter(c2,c1 * c4). [resolve(238,a,60,b)]. given #166 (T,wt=8): 984 -Shorter(x,c2) | Shorter(x,c1 * c4). [resolve(968,a,54,b)]. given #167 (T,wt=8): 985 -Shorter(c1 * c4,x) | Shorter(c2,x). [resolve(968,a,54,a)]. given #168 (A,wt=22): 92 -Power(x,y) | x = y | x * f3(y,y,x) = y | f3(y,y,x) * y = x. [resolve(36,a,31,a)]. given #169 (F,wt=7): 819 -Shorter(c2 * x,c1 * x). [ur(58,a,805,a)]. given #170 (F,wt=7): 820 -Shorter(x * (c2 * y),c1). [ur(54,a,266,a,c,805,a)]. given #171 (F,wt=7): 821 -Shorter(x * (y * c2),c1). [ur(54,a,134,a,c,805,a)]. given #172 (F,wt=9): 180 -Shorter(x * c4,c5 * (c3 * x)). [ur(64,a,68,a),rewrite([25(6)])]. given #173 (T,wt=9): 239 Shorter(c2 * x,x * (c4 * c1)). [resolve(171,a,61,a)]. given #174 (T,wt=9): 240 Shorter(x * c2,x * (c4 * c1)). [resolve(171,a,59,a)]. given #175 (T,wt=9): 241 Shorter(c2 * x,c4 * (c1 * x)). [resolve(171,a,57,a),rewrite([25(6)])]. given #176 (T,wt=9): 246 Power(x * (x * (x * x)),x). [resolve(205,a,75,a),rewrite([25(3)])]. given #177 (A,wt=22): 93 -Power(x,y) | y = x | y * f3(y,x,y) = x | f3(y,x,y) * x = y. [resolve(36,b,31,a)]. given #178 (F,wt=5): 1007 -Shorter(c4,c3 * c5). [ur(59,b,180,a)]. given #179 (F,wt=7): 1009 -Shorter(x * c4,c3 * c5). [ur(54,b,140,a,c,180,a)]. given #180 (F,wt=7): 1077 -Shorter(c4 * x,c3 * c5). [ur(128,b,1007,a)]. given #181 (F,wt=9): 181 -Shorter(c4 * x,x * (c5 * c3)). [ur(62,a,68,a)]. given #182 (T,wt=9): 276 Shorter(x,y * (z * (u * x))). [para(25(a,1),134(a,2,2))]. given #183 (T,wt=9): 309 Shorter(x,y * (z * (x * u))). [para(25(a,1),266(a,2))]. given #184 (T,wt=9): 319 Shorter(c2,x * (y * (c4 * c1))). [para(25(a,1),277(a,2))]. given #185 (T,wt=9): 327 Shorter(c5,x * (y * (c4 * c1))). [para(25(a,1),310(a,2))]. given #186 (A,wt=22): 94 -Power(x,y) | x = y | f3(y,y,x) * x = y | y * f3(y,y,x) = x. [resolve(37,a,31,a)]. given #187 (F,wt=9): 182 -Shorter(x * c4,x * (c5 * c3)). [ur(60,a,68,a)]. given #188 (F,wt=9): 183 -Shorter(c4 * x,c5 * (c3 * x)). [ur(58,a,68,a),rewrite([25(6)])]. given #189 (F,wt=9): 188 c5 * (x * y) != c4 * y. [ur(27,b,69,a),rewrite([25(3)])]. given #190 (F,wt=9): 189 x * (c5 * y) != x * c4. [ur(26,b,69,a)]. given #191 (T,wt=9): 368 Power(x * x,f8(x,x,x,x)). [resolve(351,a,75,a)]. given #192 (T,wt=9): 398 Shorter(c5,x * (c4 * (c1 * y))). [resolve(127,a,310,a),rewrite([25(6),25(5)])]. given #193 (T,wt=9): 399 Shorter(c2,x * (c4 * (c1 * y))). [resolve(127,a,277,a),rewrite([25(6),25(5)])]. given #194 (T,wt=9): 479 Period(x * (y * z),x * y). [resolve(197,b,25,a)]. given #195 (A,wt=22): 95 -Power(x,y) | y = x | f3(y,x,y) * y = x | x * f3(y,x,y) = y. [resolve(37,b,31,a)]. given #196 (F,wt=9): 223 -Shorter(x * (y * z),y * x). [ur(64,a,129,a)]. given #197 (F,wt=9): 224 -Shorter(x * (y * z),z * x). [ur(62,a,129,a),rewrite([25(2)])]. given #198 (F,wt=9): 225 -Shorter(x * (y * z),x * y). [ur(60,a,129,a)]. given #199 (F,wt=9): 226 -Shorter(x * (y * z),x * z). [ur(58,a,129,a),rewrite([25(2)])]. given #200 (T,wt=9): 487 Power(f11(c4 * c1,c5),c4 * c1). [resolve(478,a,65,a)]. given #201 (T,wt=9): 490 Power(f11(x * y,x),x * y). [resolve(482,a,65,a)]. given #202 (T,wt=7): 1329 Power(f11(x * x,x),x). [resolve(490,a,263,a)]. given #203 (T,wt=9): 570 Shorter(c4 * c1,c5 * (x * c2)). [para(67(a,1),135(a,1))]. given #204 (A,wt=22): 96 -Power(x,y) | x = y | f3(y,y,x) * x = y | f3(y,y,x) * y = x. [resolve(38,a,31,a)]. given #205 (F,wt=7): 1401 -Shorter(c5 * (x * c2),c3). [ur(54,a,570,a,c,216,a)]. given #206 (F,wt=9): 228 -Shorter(x * (y * z),z * y). [ur(62,a,133,a),rewrite([25(2)])]. given #207 (F,wt=9): 271 -Shorter(x * (y * (z * u)),u). [ur(54,b,134,a,c,133,a)]. given #208 (F,wt=9): 272 -Shorter(x * (y * (z * u)),z). [ur(54,b,134,a,c,129,a),rewrite([25(3),25(2)])]. given #209 (T,wt=7): 1384 Shorter(c1,c5 * (x * c2)). [resolve(570,a,132,a)]. given #210 (T,wt=7): 1386 Shorter(c4,c5 * (x * c2)). [resolve(570,a,128,a)]. given #211 (T,wt=9): 595 Shorter(c2,x * (c4 * (y * c1))). [resolve(560,a,131,a)]. given #212 (T,wt=9): 596 Shorter(c2,c4 * (x * (c1 * y))). [resolve(560,a,127,a),rewrite([25(6),25(5)])]. given #213 (A,wt=22): 97 -Power(x,y) | y = x | f3(y,x,y) * y = x | f3(y,x,y) * x = y. [resolve(38,b,31,a)]. given #214 (F,wt=9): 275 -Shorter(x * (y * c4),c5 * c3). [ur(54,a,134,a,c,68,a)]. given #215 (F,wt=9): 283 c5 * x != c4 * (c1 * x). [ur(77,b,152,a),flip(a)]. given #216 (F,wt=9): 285 x * (c4 * c1) != x * c5. [ur(26,b,152,a)]. given #217 (F,wt=9): 286 c4 * (c1 * x) != c2 * x. [ur(77,b,153,a)]. given #218 (T,wt=9): 606 Shorter(c2,c4 * (x * (y * c1))). [para(25(a,1),560(a,2,2))]. given #219 (T,wt=9): 607 Shorter(c5,x * (c4 * (y * c1))). [resolve(561,a,131,a)]. given #220 (T,wt=9): 608 Shorter(c5,c4 * (x * (c1 * y))). [resolve(561,a,127,a),rewrite([25(6),25(5)])]. given #221 (T,wt=9): 615 Shorter(c5,c4 * (x * (y * c1))). [para(25(a,1),561(a,2,2))]. given #222 (A,wt=22): 98 Power(x,x * y) | f4(x,y,x * y) * f5(x,y,x * y) = x * y. [resolve(39,a,31,a)]. given #223 (F,wt=9): 288 x * (c4 * c1) != x * c2. [ur(26,b,153,a)]. given #224 (F,wt=9): 289 -Shorter(x * (y * c4),c3 * x). [ur(64,a,215,a)]. given #225 (F,wt=9): 290 -Shorter(x * (c4 * y),y * c3). [ur(62,a,215,a),rewrite([25(3)])]. given #226 (F,wt=9): 291 -Shorter(x * (y * c4),x * c3). [ur(60,a,215,a)]. given #227 (T,wt=9): 628 Shorter(c4 * c1,c2 * (x * c5)). [para(67(a,1),139(a,1))]. given #228 (T,wt=7): 1637 Shorter(c1,c2 * (x * c5)). [resolve(628,a,132,a)]. given #229 (T,wt=7): 1639 Shorter(c4,c2 * (x * c5)). [resolve(628,a,128,a)]. given #230 (T,wt=9): 629 Shorter(c2,x * (c1 * (y * c4))). [resolve(616,a,131,a)]. given #231 (A,wt=27): 99 -Power(x * (y * z),u) | Power(x * y,u) | f4(x * y,z,u) * f5(x * y,z,u) = u. [para(25(a,1),39(a,1))]. given #232 (F,wt=7): 1654 -Shorter(c2 * (x * c5),c3). [ur(54,a,628,a,c,216,a)]. given #233 (F,wt=9): 292 -Shorter(x * (c4 * y),c3 * y). [ur(58,a,215,a),rewrite([25(3)])]. given #234 (F,wt=9): 293 -Shorter(x * (y * (z * c4)),c3). [ur(54,a,134,a,c,215,a)]. given #235 (F,wt=9): 295 -Shorter(x * (c4 * y),c3 * x). [ur(64,a,216,a)]. given #236 (T,wt=9): 630 Shorter(c2,c1 * (x * (c4 * y))). [resolve(616,a,127,a),rewrite([25(6),25(5)])]. given #237 (T,wt=9): 641 Shorter(c2,c1 * (x * (y * c4))). [para(25(a,1),616(a,2,2))]. given #238 (T,wt=9): 685 Shorter(c5,x * (c1 * (y * c4))). [resolve(617,a,131,a)]. given #239 (T,wt=9): 686 Shorter(c5,c1 * (x * (c4 * y))). [resolve(617,a,127,a),rewrite([25(6),25(5)])]. given #240 (A,wt=28): 100 Power(x,x * y) | f4(x,y,x * y) = x | f6(x,y,x * y) * f4(x,y,x * y) = x. [resolve(40,a,31,a)]. given #241 (F,wt=9): 296 -Shorter(c4 * (x * y),y * c3). [ur(62,a,216,a),rewrite([25(3)])]. given #242 (F,wt=9): 297 -Shorter(x * (c4 * y),x * c3). [ur(60,a,216,a)]. given #243 (F,wt=9): 298 -Shorter(c4 * (x * y),c3 * y). [ur(58,a,216,a),rewrite([25(3)])]. given #244 (F,wt=9): 299 -Shorter(x * (y * (c4 * z)),c3). [ur(54,a,134,a,c,216,a)]. given #245 (T,wt=9): 693 Shorter(c5,c1 * (x * (y * c4))). [para(25(a,1),617(a,2,2))]. given #246 (T,wt=9): 705 Shorter(c4 * c1,c2 * (c5 * x)). [para(67(a,1),140(a,1))]. given #247 (T,wt=7): 1858 Shorter(c1,c2 * (c5 * x)). [resolve(705,a,132,a)]. given #248 (T,wt=7): 1860 Shorter(c4,c2 * (c5 * x)). [resolve(705,a,128,a)]. given #249 (A,wt=39): 101 -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(25(a,1),40(a,1))]. given #250 (F,wt=7): 1869 -Shorter(c2 * (c5 * x),c3). [ur(54,a,705,a,c,216,a)]. given #251 (F,wt=9): 307 -Shorter(x * (c4 * y),c5 * c3). [ur(54,a,266,a,c,68,a)]. given #252 (F,wt=9): 317 -Shorter(x * (y * (c4 * c1)),c2). [ur(54,b,277,a,c,133,a)]. given #253 (F,wt=9): 318 -Shorter(x * (c4 * (c1 * y)),c2). [ur(54,b,277,a,c,129,a),rewrite([25(5),25(4)])]. given #254 (T,wt=9): 706 Shorter(c2,x * (c1 * (c4 * y))). [resolve(694,a,131,a)]. given #255 (T,wt=9): 714 Shorter(c5,x * (c1 * (c4 * y))). [resolve(695,a,131,a)]. given #256 (T,wt=9): 780 Shorter(c4 * c1,x * (c2 * c5)). [para(67(a,1),144(a,1))]. given #257 (T,wt=5): 1930 Shorter(c4,c2 * c5). [resolve(780,a,62,b)]. given #258 (A,wt=23): 102 Power(x,x * y) | f4(x,y,x * y) = x | Power(f6(x,y,x * y),x * y). [resolve(41,a,31,a)]. given #259 (F,wt=5): 1953 -Shorter(c2 * c5,c3). [ur(54,a,1930,a,c,184,a)]. given #260 (F,wt=7): 1939 -Shorter(x * (c2 * c5),c3). [ur(54,a,780,a,c,216,a)]. given #261 (F,wt=7): 1952 -Shorter(c2 * c5,c3 * c5). [ur(54,a,1930,a,c,1007,a)]. given #262 (F,wt=3): 2054 -Shorter(c2,c3). [ur(57,b,1952,a)]. given #263 (T,wt=5): 1932 Shorter(c1,c2 * c5). [resolve(780,a,60,b)]. given #264 (T,wt=7): 1926 Shorter(c1,x * (c2 * c5)). [resolve(780,a,132,a)]. given #265 (T,wt=7): 1928 Shorter(c4,x * (c2 * c5)). [resolve(780,a,128,a)]. given #266 (T,wt=8): 1950 -Shorter(x,c4) | Shorter(x,c2 * c5). [resolve(1930,a,54,b)]. given #267 (A,wt=30): 103 -Power(x * (y * z),u) | Power(x * y,u) | f4(x * y,z,u) = x * y | Power(f6(x * y,z,u),u). [para(25(a,1),41(a,1))]. given #268 (F,wt=5): 2059 -Shorter(x * c2,c3). [ur(132,b,2054,a)]. given #269 (F,wt=5): 2060 -Shorter(c2 * x,c3). [ur(128,b,2054,a)]. given #270 (F,wt=7): 2061 -Shorter(x * c2,c3 * x). [ur(64,a,2054,a)]. given #271 (F,wt=7): 2062 -Shorter(c2 * x,x * c3). [ur(62,a,2054,a)]. given #272 (T,wt=8): 1951 -Shorter(c2 * c5,x) | Shorter(c4,x). [resolve(1930,a,54,a)]. given #273 (T,wt=8): 2073 -Shorter(x,c1) | Shorter(x,c2 * c5). [resolve(1932,a,54,b)]. given #274 (T,wt=8): 2074 -Shorter(c2 * c5,x) | Shorter(c1,x). [resolve(1932,a,54,a)]. given #275 (T,wt=9): 781 Shorter(c2 * c5,x * (c4 * c1)). [para(67(a,1),144(a,2,2))]. given #276 (A,wt=28): 104 Power(x,x * y) | f5(x,y,x * y) = y | f5(x,y,x * y) * f7(x,y,x * y) = y. [resolve(42,a,31,a)]. given #277 (F,wt=7): 2063 -Shorter(x * c2,x * c3). [ur(60,a,2054,a)]. given #278 (F,wt=7): 2064 -Shorter(c2 * x,c3 * x). [ur(58,a,2054,a)]. given #279 (F,wt=7): 2067 -Shorter(x * (c2 * y),c3). [ur(54,a,266,a,c,2054,a)]. given #280 (F,wt=7): 2068 -Shorter(x * (y * c2),c3). [ur(54,a,134,a,c,2054,a)]. given #281 (T,wt=9): 782 Shorter(c2,x * (y * (c1 * c4))). [resolve(769,a,131,a)]. given #282 (T,wt=9): 789 Shorter(c5,x * (y * (c1 * c4))). [resolve(770,a,131,a)]. given #283 (T,wt=9): 868 Shorter(x * c5,c1 * (c4 * x)). [resolve(857,a,63,a),rewrite([25(6)])]. given #284 (T,wt=9): 869 Shorter(c5 * x,x * (c1 * c4)). [resolve(857,a,61,a)]. given #285 (A,wt=35): 105 -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(25(a,1),42(a,1))]. given #286 (F,wt=9): 331 c5 * (x * c2) != c4 * c1. [para(67(a,1),78(a,2))]. given #287 (F,wt=9): 332 -Shorter(x * (y * c4),c5 * x). [ur(64,a,221,a)]. given #288 (F,wt=9): 333 -Shorter(x * (c4 * y),y * c5). [ur(62,a,221,a),rewrite([25(3)])]. given #289 (F,wt=9): 334 -Shorter(x * (y * c4),x * c5). [ur(60,a,221,a)]. given #290 (T,wt=9): 870 Shorter(x * c5,x * (c1 * c4)). [resolve(857,a,59,a)]. given #291 (T,wt=9): 871 Shorter(c5 * x,c1 * (c4 * x)). [resolve(857,a,57,a),rewrite([25(6)])]. given #292 (T,wt=9): 980 Shorter(x * c2,c1 * (c4 * x)). [resolve(968,a,63,a),rewrite([25(6)])]. given #293 (T,wt=9): 981 Shorter(c2 * x,x * (c1 * c4)). [resolve(968,a,61,a)]. given #294 (A,wt=23): 106 Power(x,x * y) | f5(x,y,x * y) = y | Power(f7(x,y,x * y),x * y). [resolve(43,a,31,a)]. given #295 (F,wt=9): 335 -Shorter(x * (c4 * y),c5 * y). [ur(58,a,221,a),rewrite([25(3)])]. given #296 (F,wt=9): 336 -Shorter(x * (y * (c4 * z)),c5). [ur(54,a,266,a,c,221,a),rewrite([25(3)])]. given #297 (F,wt=9): 337 -Shorter(x * (y * (z * c4)),c5). [ur(54,a,134,a,c,221,a)]. given #298 (F,wt=9): 338 -Shorter(x * (c4 * y),c5 * x). [ur(64,a,222,a)]. given #299 (T,wt=9): 982 Shorter(x * c2,x * (c1 * c4)). [resolve(968,a,59,a)]. given #300 (T,wt=9): 983 Shorter(c2 * x,c1 * (c4 * x)). [resolve(968,a,57,a),rewrite([25(6)])]. given #301 (T,wt=9): 1058 Power(x,f8(x,x,x,x * x)). [resolve(246,a,50,b),unit_del(a,31)]. given #302 (T,wt=9): 1264 Period(x * (c4 * c1),x * c5). [para(67(a,1),479(a,1,2))]. given #303 (A,wt=28): 107 -Power(x * (y * z),u) | Power(x * y,u) | f5(x * y,z,u) = z | Power(f7(x * y,z,u),u). [para(25(a,1),43(a,1))]. given #304 (F,wt=9): 339 -Shorter(c4 * (x * y),y * c5). [ur(62,a,222,a),rewrite([25(3)])]. given #305 (F,wt=9): 340 -Shorter(x * (c4 * y),x * c5). [ur(60,a,222,a)]. given #306 (F,wt=9): 341 -Shorter(c4 * (x * y),c5 * y). [ur(58,a,222,a),rewrite([25(3)])]. given #307 (F,wt=9): 342 -Shorter(x * (c4 * c1),c2 * x). [ur(64,a,230,a)]. given #308 (T,wt=9): 1365 Power(f11(x * x,x) * x,x). [resolve(1329,a,87,a)]. given #309 (T,wt=9): 1366 Power(x * f11(x * x,x),x). [resolve(1329,a,86,a)]. given #310 (T,wt=9): 1463 Shorter(c1,x * (c5 * (y * c2))). [resolve(1384,a,131,a)]. given #311 (T,wt=9): 1464 Shorter(c1,c5 * (x * (c2 * y))). [resolve(1384,a,127,a),rewrite([25(6),25(5)])]. given #312 (A,wt=22): 108 Power(x,y * x) | f4(y,x,y * x) * f5(y,x,y * x) = y * x. [resolve(44,a,31,a)]. given #313 (F,wt=9): 343 -Shorter(c4 * (c1 * x),x * c2). [ur(62,a,230,a),rewrite([25(4)])]. given #314 (F,wt=9): 344 -Shorter(x * (c4 * c1),x * c2). [ur(60,a,230,a)]. given #315 (F,wt=9): 345 -Shorter(c4 * (c1 * x),c2 * x). [ur(58,a,230,a),rewrite([25(4)])]. given #316 (F,wt=9): 347 x * (y * (z * u)) != u. [para(25(a,1),80(a,1,2))]. given #317 (T,wt=9): 1471 Shorter(c1,c5 * (x * (y * c2))). [para(25(a,1),1384(a,2,2))]. given #318 (T,wt=9): 1472 Shorter(c4,x * (c5 * (y * c2))). [resolve(1386,a,131,a)]. given #319 (T,wt=9): 1473 Shorter(c4,c5 * (x * (c2 * y))). [resolve(1386,a,127,a),rewrite([25(6),25(5)])]. given #320 (T,wt=9): 1480 Shorter(c4,c5 * (x * (y * c2))). [para(25(a,1),1386(a,2,2))]. given #321 (A,wt=25): 109 -Power(x * (y * z),u) | Power(z,u) | f4(x * y,z,u) * f5(x * y,z,u) = u. [para(25(a,1),44(a,1))]. given #322 (F,wt=9): 413 -Shorter(x * (c1 * c4),c2 * x). [ur(64,a,406,a)]. given #323 (F,wt=9): 414 -Shorter(c1 * (c4 * x),x * c2). [ur(62,a,406,a),rewrite([25(4)])]. given #324 (F,wt=9): 415 -Shorter(x * (c1 * c4),x * c2). [ur(60,a,406,a)]. given #325 (F,wt=9): 416 -Shorter(c1 * (c4 * x),c2 * x). [ur(58,a,406,a),rewrite([25(4)])]. given #326 (T,wt=9): 1662 Shorter(c1,x * (c2 * (y * c5))). [resolve(1637,a,131,a)]. given #327 (T,wt=9): 1663 Shorter(c1,c2 * (x * (c5 * y))). [resolve(1637,a,127,a),rewrite([25(6),25(5)])]. given #328 (T,wt=9): 1670 Shorter(c1,c2 * (x * (y * c5))). [para(25(a,1),1637(a,2,2))]. given #329 (T,wt=9): 1671 Shorter(c4,x * (c2 * (y * c5))). [resolve(1639,a,131,a)]. given #330 (A,wt=28): 110 Power(x,y * x) | f4(y,x,y * x) = y | f6(y,x,y * x) * f4(y,x,y * x) = y. [resolve(45,a,31,a)]. given #331 (F,wt=9): 417 -Shorter(x * (c1 * (c4 * y)),c2). [ur(54,a,266,a,c,406,a),rewrite([25(4)])]. given #332 (F,wt=9): 418 -Shorter(x * (y * (c1 * c4)),c2). [ur(54,a,134,a,c,406,a)]. given #333 (F,wt=9): 457 -Shorter(x * (y * c4),c3 * y). [ur(54,a,56,a,c,211,a)]. given #334 (F,wt=9): 459 -Shorter(c4 * (x * y),x * c3). [ur(128,b,212,a),rewrite([25(3)])]. given #335 (T,wt=9): 1672 Shorter(c4,c2 * (x * (c5 * y))). [resolve(1639,a,127,a),rewrite([25(6),25(5)])]. given #336 (T,wt=9): 1679 Shorter(c4,c2 * (x * (y * c5))). [para(25(a,1),1639(a,2,2))]. given #337 (T,wt=9): 1876 Shorter(c1,x * (c2 * (c5 * y))). [resolve(1858,a,131,a)]. given #338 (T,wt=9): 1883 Shorter(c4,x * (c2 * (c5 * y))). [resolve(1860,a,131,a)]. given #339 (A,wt=37): 111 -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(25(a,1),45(a,1))]. given #340 (F,wt=9): 472 -Shorter(x * (y * c4),y * c3). [ur(54,a,56,a,c,213,a)]. given #341 (F,wt=9): 473 -Shorter(c4 * (x * y),c3 * x). [ur(128,b,214,a),rewrite([25(3)])]. given #342 (F,wt=9): 499 -Shorter(x * (y * c4),c5 * y). [ur(132,b,217,a)]. given #343 (F,wt=9): 508 -Shorter(c4 * (x * y),x * c5). [ur(128,b,218,a),rewrite([25(3)])]. given #344 (T,wt=9): 1946 Shorter(x * c4,c2 * (c5 * x)). [resolve(1930,a,63,a),rewrite([25(6)])]. given #345 (T,wt=9): 1947 Shorter(c4 * x,x * (c2 * c5)). [resolve(1930,a,61,a)]. given #346 (T,wt=9): 1948 Shorter(x * c4,x * (c2 * c5)). [resolve(1930,a,59,a)]. given #347 (T,wt=9): 1949 Shorter(c4 * x,c2 * (c5 * x)). [resolve(1930,a,57,a),rewrite([25(6)])]. given #348 (A,wt=23): 112 Power(x,y * x) | f4(y,x,y * x) = y | Power(f6(y,x,y * x),y * x). [resolve(46,a,31,a)]. given #349 (F,wt=9): 515 -Shorter(x * (y * c4),y * c5). [ur(132,b,219,a)]. given #350 (F,wt=9): 522 -Shorter(c4 * (x * y),c5 * x). [ur(128,b,220,a),rewrite([25(3)])]. given #351 (F,wt=9): 568 -Shorter(c4 * (x * (c1 * y)),c2). [ur(54,a,135,a,c,245,a)]. given #352 (F,wt=9): 605 -Shorter(x * (c4 * (y * c1)),c2). [ur(54,b,560,a,c,133,a)]. given #353 (T,wt=9): 2069 Shorter(x * c1,c2 * (c5 * x)). [resolve(1932,a,63,a),rewrite([25(6)])]. given #354 (T,wt=9): 2070 Shorter(c1 * x,x * (c2 * c5)). [resolve(1932,a,61,a)]. given #355 (T,wt=9): 2071 Shorter(x * c1,x * (c2 * c5)). [resolve(1932,a,59,a)]. given #356 (T,wt=9): 2072 Shorter(c1 * x,c2 * (c5 * x)). [resolve(1932,a,57,a),rewrite([25(6)])]. given #357 (A,wt=28): 113 -Power(x * (y * z),u) | Power(z,u) | f4(x * y,z,u) = x * y | Power(f6(x * y,z,u),u). [para(25(a,1),46(a,1))]. given #358 (F,wt=7): 3164 -Shorter(c2 * c4,c3 * c1). [ur(54,b,2069,a,c,182,a)]. given #359 (F,wt=7): 3165 -Shorter(c4 * c2,c3 * c1). [ur(54,b,2069,a,c,181,a)]. given #360 (F,wt=7): 3206 -Shorter(c2 * c4,c1 * c3). [ur(54,b,2072,a,c,182,a)]. given #361 (F,wt=7): 3207 -Shorter(c4 * c2,c1 * c3). [ur(54,b,2072,a,c,181,a)]. given #362 (T,wt=9): 2075 Shorter(c1,x * (y * (c2 * c5))). [resolve(1926,a,131,a)]. given #363 (T,wt=9): 2082 Shorter(c4,x * (y * (c2 * c5))). [resolve(1928,a,131,a)]. given #364 (T,wt=10): 150 c5 * x != c4 * c1 | c2 = x. [para(67(a,1),26(a,1)),flip(a)]. given #365 (T,wt=10): 151 c4 * c1 != x * c2 | c5 = x. [para(67(a,1),27(a,1))]. given #366 (A,wt=28): 114 Power(x,y * x) | f5(y,x,y * x) = x | f5(y,x,y * x) * f7(y,x,y * x) = x. [resolve(47,a,31,a)]. given #367 (F,wt=9): 626 -Shorter(c1 * (x * (y * c4)),c2). [ur(54,a,139,a,c,245,a),rewrite([25(5)])]. given #368 (F,wt=9): 639 -Shorter(x * (c1 * (y * c4)),c2). [ur(54,b,616,a,c,133,a)]. given #369 (F,wt=9): 640 -Shorter(c1 * (x * (c4 * y)),c2). [ur(54,b,616,a,c,129,a),rewrite([25(5),25(4)])]. given #370 (F,wt=9): 652 x * (y * (c4 * c1)) != c2. [para(25(a,1),348(a,1))]. given #371 (T,wt=10): 172 Shorter(c5,x) | -Shorter(c4 * c1,x * c2). [para(67(a,1),58(b,1))]. given #372 (T,wt=10): 173 Shorter(x,c5) | -Shorter(x * c2,c4 * c1). [para(67(a,1),58(b,2))]. given #373 (T,wt=10): 174 Shorter(c2,x) | -Shorter(c4 * c1,c5 * x). [para(67(a,1),60(b,1))]. given #374 (T,wt=10): 175 Shorter(x,c2) | -Shorter(c5 * x,c4 * c1). [para(67(a,1),60(b,2))]. given #375 (A,wt=33): 115 -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(25(a,1),47(a,1))]. given #376 (F,wt=9): 653 -Shorter(x * (c4 * c1),c2 * c5). [ur(132,b,411,a)]. given #377 (F,wt=9): 654 -Shorter(c4 * (c1 * x),c2 * c5). [ur(128,b,411,a),rewrite([25(4)])]. given #378 (F,wt=9): 660 -Shorter(c1 * (x * c4),c2 * c5). [ur(54,a,139,a,c,411,a)]. given #379 (F,wt=9): 661 -Shorter(c4 * (x * c1),c2 * c5). [ur(54,a,135,a,c,411,a)]. given #380 (T,wt=10): 176 Shorter(c5,x) | -Shorter(c4 * c1,c2 * x). [para(67(a,1),62(b,1))]. given #381 (T,wt=10): 177 Shorter(x,c2) | -Shorter(x * c5,c4 * c1). [para(67(a,1),62(b,2))]. given #382 (T,wt=10): 178 Shorter(c2,x) | -Shorter(c4 * c1,x * c5). [para(67(a,1),64(b,1))]. given #383 (T,wt=10): 179 Shorter(x,c5) | -Shorter(c2 * x,c4 * c1). [para(67(a,1),64(b,2))]. given #384 (A,wt=23): 116 Power(x,y * x) | f5(y,x,y * x) = x | Power(f7(y,x,y * x),y * x). [resolve(48,a,31,a)]. given #385 (F,wt=9): 663 -Shorter(x * (c2 * c5),c4 * c1). [ur(132,b,412,a)]. given #386 (F,wt=9): 665 -Shorter(c2 * (c5 * x),c4 * c1). [ur(128,b,412,a),rewrite([25(4)])]. given #387 (F,wt=9): 672 -Shorter(c5 * (x * c2),c4 * c1). [ur(54,a,139,a,c,412,a)]. given #388 (F,wt=9): 673 -Shorter(c2 * (x * c5),c4 * c1). [ur(54,a,135,a,c,412,a)]. given #389 (T,wt=10): 247 Period(x,y) | y * z != x * x. [resolve(205,a,72,b)]. given #390 (T,wt=3): 3535 Period(x,x). [xx_res(247,b)]. given #391 (T,wt=5): 3541 Power(f11(x,x),x). [resolve(3535,a,65,a)]. given #392 (T,wt=7): 3553 Power(f11(x,x) * x,x). [resolve(3541,a,87,a)]. given #393 (A,wt=26): 117 -Power(x * (y * z),u) | Power(z,u) | f5(x * y,z,u) = z | Power(f7(x * y,z,u),u). [para(25(a,1),48(a,1))]. given #394 (F,wt=9): 703 -Shorter(c1 * (c4 * x),c2 * c5). [ur(54,a,140,a,c,411,a)]. given #395 (F,wt=9): 726 -Shorter(x * (c2 * c5),c4 * x). [ur(64,a,666,a)]. given #396 (F,wt=9): 727 -Shorter(c2 * (c5 * x),x * c4). [ur(62,a,666,a),rewrite([25(4)])]. given #397 (F,wt=9): 728 -Shorter(x * (c2 * c5),x * c4). [ur(60,a,666,a)]. given #398 (T,wt=7): 3554 Power(x * f11(x,x),x). [resolve(3541,a,86,a)]. given #399 (T,wt=8): 3539 Period(x,y) | -Power(f11(y,y),x). [resolve(3535,a,73,c)]. given #400 (T,wt=5): 3687 Period(f11(x,x),x). [resolve(3539,b,31,a)]. given #401 (T,wt=8): 3569 -Power(x,f11(y,y)) | Power(x,y). [resolve(3541,a,32,b)]. given #402 (A,wt=18): 118 -Power(x,y * (x * z)) | Power(x,f8(y * (x * z),x,y,z)). [resolve(49,b,31,a)]. given #403 (F,wt=9): 729 -Shorter(c2 * (c5 * x),c4 * x). [ur(58,a,666,a),rewrite([25(4)])]. given #404 (F,wt=9): 730 -Shorter(x * (c2 * (c5 * y)),c4). [ur(54,a,266,a,c,666,a),rewrite([25(4)])]. given #405 (F,wt=9): 733 -Shorter(x * (y * (c2 * c5)),c4). [ur(54,a,134,a,c,666,a)]. given #406 (F,wt=9): 743 -Shorter(c4 * (x * (y * c1)),c2). [ur(54,a,139,a,c,420,a),rewrite([25(5)])]. given #407 (T,wt=8): 3570 -Power(x,y) | Power(f11(x,x),y). [resolve(3541,a,32,a)]. given #408 (T,wt=9): 3534 Period(x * y,x * (y * x)). [resolve(247,b,25,a),rewrite([25(3)])]. given #409 (T,wt=9): 3542 Power(f11(x * x,x * x),x). [resolve(3541,a,263,a)]. given #410 (T,wt=5): 3759 Period(x,x * x). [resolve(3542,a,3539,b)]. given #411 (A,wt=25): 119 -Power(x * y,z) | -Power(u * (x * (y * w)),z) | Power(x * y,f8(z,x * y,u,w)). [para(25(a,1),49(b,1,2))]. given #412 (F,wt=9): 777 -Shorter(x * (c1 * c4),c2 * c5). [ur(54,a,144,a,c,411,a)]. given #413 (F,wt=9): 822 -Shorter(x * (y * c2),c1 * x). [ur(64,a,814,a)]. given #414 (F,wt=9): 823 -Shorter(x * (c2 * y),y * c1). [ur(62,a,814,a),rewrite([25(3)])]. given #415 (F,wt=9): 824 -Shorter(x * (y * c2),x * c1). [ur(60,a,814,a)]. given #416 (T,wt=7): 3791 Power(f11(x,x * x),x). [resolve(3759,a,65,a)]. given #417 (T,wt=9): 3555 Power(f11(x,x) * f11(x,x),x). [resolve(3541,a,75,a)]. given #418 (T,wt=9): 3587 Power(f11(x,x) * (x * x),x). [resolve(3553,a,87,a),rewrite([25(3)])]. given #419 (T,wt=9): 3588 Power(x * (f11(x,x) * x),x). [resolve(3553,a,86,a)]. given #420 (A,wt=21): 120 -Power(x,y) | -Power(z * (u * (x * w)),y) | Power(x,f8(y,x,z * u,w)). [para(25(a,1),49(b,1))]. given #421 (F,wt=9): 825 -Shorter(x * (c2 * y),c1 * y). [ur(58,a,814,a),rewrite([25(3)])]. given #422 (F,wt=9): 826 -Shorter(x * (y * (c2 * z)),c1). [ur(54,a,266,a,c,814,a),rewrite([25(3)])]. given #423 (F,wt=9): 827 -Shorter(x * (y * (z * c2)),c1). [ur(54,a,134,a,c,814,a)]. given #424 (F,wt=9): 828 -Shorter(x * (c2 * y),c1 * x). [ur(64,a,815,a)]. given #425 (T,wt=9): 3657 Power(x * (x * f11(x,x)),x). [resolve(3554,a,86,a)]. given #426 (T,wt=9): 3690 Power(f11(f11(x,x),x),f11(x,x)). [resolve(3687,a,65,a)]. given #427 (T,wt=7): 4046 Power(f11(f11(x,x),x),x). [resolve(3690,a,3569,a)]. given #428 (T,wt=9): 3693 Power(f11(f11(x,x),f11(x,x)),x). [resolve(3569,a,3541,a)]. given #429 (A,wt=18): 121 -Power(x,y * (x * z)) | Power(y,f8(y * (x * z),x,y,z)). [resolve(50,b,31,a)]. given #430 (F,wt=9): 829 -Shorter(c2 * (x * y),y * c1). [ur(62,a,815,a),rewrite([25(3)])]. given #431 (F,wt=9): 830 -Shorter(x * (c2 * y),x * c1). [ur(60,a,815,a)]. given #432 (F,wt=9): 831 -Shorter(c2 * (x * y),c1 * y). [ur(58,a,815,a),rewrite([25(3)])]. given #433 (F,wt=9): 865 -Shorter(c4 * (c1 * c4),c5 * c5). [ur(54,a,231,a,c,220,a)]. given #434 (T,wt=5): 4107 Period(x,f11(x,x)). [resolve(3693,a,3539,b)]. given #435 (T,wt=7): 4167 Power(f11(x,f11(x,x)),x). [resolve(4107,a,65,a)]. given #436 (T,wt=9): 3733 Power(f11(x,x),f8(x,x,x,x)). [resolve(3570,a,351,a)]. given #437 (T,wt=7): 4200 Period(f8(x,x,x,x),x). [resolve(3733,a,3539,b)]. given #438 (A,wt=23): 122 -Power(x * y,z) | -Power(u * (x * (y * w)),z) | Power(u,f8(z,x * y,u,w)). [para(25(a,1),50(b,1,2))]. given #439 (F,wt=9): 893 -Shorter(x * (c5 * (y * c2)),c4). [ur(54,a,144,a,c,725,a),rewrite([25(4)])]. given #440 (F,wt=9): 894 -Shorter(c5 * (x * (c2 * y)),c4). [ur(54,a,140,a,c,725,a),rewrite([25(5)])]. given #441 (F,wt=9): 895 -Shorter(c5 * (x * (y * c2)),c4). [ur(54,a,139,a,c,725,a),rewrite([25(5)])]. given #442 (F,wt=9): 896 -Shorter(c2 * (x * (c5 * y)),c4). [ur(54,a,135,a,c,725,a)]. given #443 (T,wt=9): 3755 Period(c4 * c1,c4 * (c1 * c5)). [para(67(a,1),3534(a,1)),rewrite([149(8)])]. given #444 (T,wt=9): 3756 Period(c2 * c5,c2 * (c4 * c1)). [para(67(a,1),3534(a,2,2))]. given #445 (T,wt=9): 3859 Power(f11(x,x * x) * x,x). [resolve(3791,a,87,a)]. given #446 (T,wt=9): 3860 Power(x * f11(x,x * x),x). [resolve(3791,a,86,a)]. given #447 (A,wt=23): 123 -Power(x,y) | -Power(z * (u * (x * w)),y) | Power(z * u,f8(y,x,z * u,w)). [para(25(a,1),50(b,1))]. given #448 (F,wt=9): 902 -Shorter(x * (c2 * (y * c5)),c4). [ur(54,a,139,a,c,731,a),rewrite([25(5)])]. given #449 (F,wt=9): 911 -Shorter(c4 * (c4 * c1),c5 * c5). [ur(54,b,232,a,c,220,a)]. given #450 (F,wt=9): 940 -Shorter(c2 * (x * (y * c5)),c4). [ur(54,a,135,a,c,732,a)]. given #451 (F,wt=9): 942 -Shorter(x * (y * c2),c1 * y). [ur(132,b,816,a)]. given #452 (T,wt=9): 3920 Power(x,f8(x,x,f11(x,x),x)). [resolve(3587,a,51,b),unit_del(a,31)]. given #453 (T,wt=9): 3950 Power(x,f8(x,f11(x,x),x,x)). [resolve(3588,a,51,b),unit_del(a,3541)]. given #454 (T,wt=9): 3975 Power(x,f8(x,x,x * x,x)). [resolve(120,b,246,a),unit_del(a,31)]. given #455 (T,wt=9): 4029 Power(x,f8(x,x,x,f11(x,x))). [resolve(3657,a,50,b),unit_del(a,31)]. given #456 (A,wt=18): 124 -Power(x,y * (x * z)) | Power(z,f8(y * (x * z),x,y,z)). [resolve(51,b,31,a)]. given #457 (F,wt=9): 947 -Shorter(x * (y * c2),y * c1). [ur(54,b,139,a,c,816,a),rewrite([25(3)])]. given #458 (F,wt=9): 949 -Shorter(c2 * (x * y),c1 * x). [ur(54,a,140,a,c,816,a)]. given #459 (F,wt=9): 952 -Shorter(c2 * (x * y),x * c1). [ur(128,b,817,a),rewrite([25(3)])]. given #460 (F,wt=9): 975 -Shorter(c1 * (x * c4),x * c2). [ur(54,b,238,a,c,141,a),rewrite([25(4)])]. given #461 (T,wt=9): 4088 Power(f11(f11(x,x),x) * x,x). [resolve(4046,a,87,a)]. given #462 (T,wt=9): 4089 Power(x * f11(f11(x,x),x),x). [resolve(4046,a,86,a)]. given #463 (T,wt=9): 4181 Power(f11(x,f11(x,x)) * x,x). [resolve(4167,a,87,a)]. given #464 (T,wt=9): 4182 Power(x * f11(x,f11(x,x)),x). [resolve(4167,a,86,a)]. given #465 (A,wt=23): 125 -Power(x * y,z) | -Power(u * (x * (y * w)),z) | Power(w,f8(z,x * y,u,w)). [para(25(a,1),51(b,1,2))]. given #466 (F,wt=9): 977 -Shorter(c4 * (c1 * c4),c3 * c2). [ur(54,a,238,a,c,214,a)]. given #467 (F,wt=9): 978 -Shorter(c4 * (c1 * c4),c2 * c3). [ur(54,a,238,a,c,212,a)]. given #468 (F,wt=9): 1024 -Shorter(c4 * (c4 * c1),c2 * c3). [ur(54,b,239,a,c,214,a)]. given #469 (F,wt=9): 1026 -Shorter(c4 * (c4 * c1),c3 * c2). [ur(54,a,239,a,c,211,a)]. given #470 (T,wt=9): 4240 Power(x,f8(x,x * x,x,x)). [resolve(122,b,246,a),unit_del(a,205)]. given #471 (T,wt=10): 261 -Power(x,y) | Power(x * (y * y),y). [resolve(205,a,33,b)]. given #472 (T,wt=10): 262 -Power(x,y) | Power(y * (y * x),y). [resolve(205,a,33,a),rewrite([25(3)])]. given #473 (T,wt=10): 269 -Shorter(x,y) | Shorter(x,z * (u * y)). [resolve(134,a,54,b)]. given #474 (A,wt=21): 126 -Power(x,y) | -Power(z * (u * (x * w)),y) | Power(w,f8(y,x,z * u,w)). [para(25(a,1),51(b,1))]. given #475 (F,wt=9): 1046 -Shorter(c1 * (x * c4),c2 * x). [ur(54,b,241,a,c,141,a),rewrite([25(4)])]. given #476 (F,wt=9): 1078 -Shorter(x * c4,c3 * (c5 * x)). [ur(64,a,1007,a),rewrite([25(6)])]. given #477 (F,wt=9): 1079 -Shorter(c4 * x,x * (c3 * c5)). [ur(62,a,1007,a)]. given #478 (F,wt=9): 1080 -Shorter(x * c4,x * (c3 * c5)). [ur(60,a,1007,a)]. given #479 (T,wt=10): 270 -Shorter(x * (y * z),u) | Shorter(z,u). [resolve(134,a,54,a)]. given #480 (T,wt=10): 304 -Shorter(x,y) | Shorter(x,z * (y * u)). [resolve(266,a,54,b)]. given #481 (T,wt=10): 305 -Shorter(x * (y * z),u) | Shorter(y,u). [resolve(266,a,54,a)]. given #482 (T,wt=10): 315 -Shorter(x,c2) | Shorter(x,y * (c4 * c1)). [resolve(277,a,54,b)]. given #483 (A,wt=14): 136 Shorter(x * y,z) | -Shorter(x * (y * u),z * u). [para(25(a,1),58(b,1))]. given #484 (F,wt=9): 1081 -Shorter(c4 * x,c3 * (c5 * x)). [ur(58,a,1007,a),rewrite([25(6)])]. given #485 (F,wt=9): 1082 -Shorter(x * (c4 * y),c3 * c5). [ur(54,a,266,a,c,1007,a)]. given #486 (F,wt=9): 1083 -Shorter(x * (y * c4),c3 * c5). [ur(54,a,134,a,c,1007,a)]. given #487 (F,wt=9): 1217 c5 * (c4 * c1) != c4 * c2. [para(67(a,1),188(a,1,2))]. given #488 (T,wt=10): 316 -Shorter(x * (c4 * c1),y) | Shorter(c2,y). [resolve(277,a,54,a)]. given #489 (T,wt=10): 324 -Shorter(x,c5) | Shorter(x,y * (c4 * c1)). [resolve(310,a,54,b)]. given #490 (T,wt=10): 325 -Shorter(x * (c4 * c1),y) | Shorter(c5,y). [resolve(310,a,54,a)]. given #491 (T,wt=10): 364 -Power(x,y * (y * y)) | Power(x,y). [resolve(328,a,32,b)]. given #492 (A,wt=14): 137 Shorter(x,y * z) | -Shorter(x * u,y * (z * u)). [para(25(a,1),58(b,2))]. given #493 (F,wt=9): 1402 -Shorter(c5 * (x * c2),c3 * c1). [ur(54,a,570,a,c,214,a)]. given #494 (F,wt=9): 1403 -Shorter(c5 * (x * c2),c1 * c3). [ur(54,a,570,a,c,212,a)]. given #495 (F,wt=9): 1407 -Shorter(c5 * (x * c2),c1 * c4). [ur(54,a,570,a,c,141,a)]. given #496 (F,wt=9): 1655 -Shorter(c2 * (x * c5),c3 * c1). [ur(54,a,628,a,c,214,a)]. given #497 (T,wt=9): 5174 Power(f11(x * (x * x),x),x). [resolve(364,a,490,a)]. given #498 (T,wt=10): 365 -Power(x,y) | Power(x * (x * x),y). [resolve(328,a,32,a)]. given #499 (T,wt=10): 395 -Power(x,y) | Power(x,f8(y,y,y,y)). [resolve(351,a,32,b)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 21 (0.00 of 0.93 sec). given #500 (T,wt=10): 396 -Power(f8(x,x,x,x),y) | Power(x,y). [resolve(351,a,32,a)]. given #501 (A,wt=14): 138 Shorter(x,y) | -Shorter(z * (u * x),z * (u * y)). [para(25(a,1),60(b,1)),rewrite([25(5)])]. given #502 (F,wt=9): 1656 -Shorter(c2 * (x * c5),c1 * c3). [ur(54,a,628,a,c,212,a)]. given #503 (F,wt=9): 1660 -Shorter(c2 * (x * c5),c1 * c4). [ur(54,a,628,a,c,141,a)]. given #504 (F,wt=9): 1870 -Shorter(c2 * (c5 * x),c3 * c1). [ur(54,a,705,a,c,214,a)]. given #505 (F,wt=9): 1871 -Shorter(c2 * (c5 * x),c1 * c3). [ur(54,a,705,a,c,212,a)]. given #506 (T,wt=10): 435 -Shorter(x,c2) | Shorter(x,c4 * (c1 * y)). [resolve(400,a,54,b)]. given #507 (T,wt=10): 436 -Shorter(c4 * (c1 * x),y) | Shorter(c2,y). [resolve(400,a,54,a)]. given #508 (T,wt=10): 442 -Shorter(x,c5) | Shorter(x,c4 * (c1 * y)). [resolve(401,a,54,b)]. given #509 (T,wt=10): 443 -Shorter(c4 * (c1 * x),y) | Shorter(c5,y). [resolve(401,a,54,a)]. given #510 (A,wt=14): 142 Shorter(x * y,z) | -Shorter(x * (y * u),u * z). [para(25(a,1),62(b,1))]. given #511 (F,wt=9): 1875 -Shorter(c2 * (c5 * x),c1 * c4). [ur(54,a,705,a,c,141,a)]. given #512 (F,wt=9): 1940 -Shorter(x * (c2 * c5),c3 * c1). [ur(54,a,780,a,c,214,a)]. given #513 (F,wt=9): 1941 -Shorter(x * (c2 * c5),c1 * c3). [ur(54,a,780,a,c,212,a)]. given #514 (F,wt=9): 1945 -Shorter(x * (c2 * c5),c1 * c4). [ur(54,a,780,a,c,141,a)]. given #515 (T,wt=9): 5585 Shorter(c1 * x,c5 * (x * c2)). [resolve(142,b,2072,a)]. given #516 (T,wt=9): 5586 Shorter(c4 * x,c5 * (x * c2)). [resolve(142,b,1949,a)]. given #517 (T,wt=9): 5587 Shorter(c2 * x,c4 * (x * c1)). [resolve(142,b,983,a)]. given #518 (T,wt=9): 5588 Shorter(c5 * x,c4 * (x * c1)). [resolve(142,b,871,a)]. given #519 (A,wt=14): 143 Shorter(x,y) | -Shorter(x * (z * u),z * (u * y)). [para(25(a,1),62(b,2))]. given #520 (F,wt=9): 2065 -Shorter(x * (y * (c2 * z)),c3). [ur(54,a,309,a,c,2054,a)]. given #521 (F,wt=9): 2066 -Shorter(x * (y * (z * c2)),c3). [ur(54,a,276,a,c,2054,a)]. given #522 (F,wt=9): 2095 -Shorter(x * (y * c2),c3 * x). [ur(64,a,2059,a)]. given #523 (F,wt=9): 2096 -Shorter(x * (c2 * y),y * c3). [ur(62,a,2059,a),rewrite([25(3)])]. given #524 (T,wt=9): 5589 Shorter(c2 * x,c1 * (x * c4)). [resolve(142,b,241,a)]. given #525 (T,wt=9): 5590 Shorter(c5 * x,c1 * (x * c4)). [resolve(142,b,234,a)]. given #526 (T,wt=10): 485 Period(x,c5) | -Power(f11(c4 * c1,c5),x). [resolve(478,a,73,c)]. given #527 (T,wt=7): 5937 Period(f11(c4 * c1,c5),c5). [resolve(485,b,31,a)]. given #528 (A,wt=14): 145 Shorter(x,y) | -Shorter(z * (u * x),y * (z * u)). [para(25(a,1),64(b,1))]. given #529 (F,wt=9): 2097 -Shorter(x * (y * c2),x * c3). [ur(60,a,2059,a)]. given #530 (F,wt=9): 2098 -Shorter(x * (c2 * y),c3 * y). [ur(58,a,2059,a),rewrite([25(3)])]. given #531 (F,wt=9): 2101 -Shorter(x * (c2 * y),c3 * x). [ur(64,a,2060,a)]. given #532 (F,wt=9): 2102 -Shorter(c2 * (x * y),y * c3). [ur(62,a,2060,a),rewrite([25(3)])]. given #533 (T,wt=10): 488 Period(x,y) | -Power(f11(y * z,y),x). [resolve(482,a,73,c)]. given #534 (T,wt=7): 6175 Period(f11(x * y,x),x). [resolve(488,b,31,a)]. given #535 (T,wt=10): 601 -Shorter(x,c2) | Shorter(x,c4 * (y * c1)). [resolve(560,a,54,b)]. given #536 (T,wt=10): 602 -Shorter(c4 * (x * c1),y) | Shorter(c2,y). [resolve(560,a,54,a)]. given #537 (A,wt=14): 146 Shorter(x,y * z) | -Shorter(u * x,y * (z * u)). [para(25(a,1),64(b,2))]. given #538 (F,wt=9): 2103 -Shorter(x * (c2 * y),x * c3). [ur(60,a,2060,a)]. given #539 (F,wt=9): 2104 -Shorter(c2 * (x * y),c3 * y). [ur(58,a,2060,a),rewrite([25(3)])]. given #540 (F,wt=9): 2105 -Shorter(x * (y * c2),c3 * y). [ur(132,b,2061,a)]. given #541 (F,wt=9): 2110 -Shorter(x * (y * c2),y * c3). [ur(54,b,139,a,c,2061,a),rewrite([25(3)])]. given #542 (T,wt=10): 613 -Shorter(x,c5) | Shorter(x,c4 * (y * c1)). [resolve(561,a,54,b)]. given #543 (T,wt=10): 614 -Shorter(c4 * (x * c1),y) | Shorter(c5,y). [resolve(561,a,54,a)]. given #544 (T,wt=10): 635 -Shorter(x,c2) | Shorter(x,c1 * (y * c4)). [resolve(616,a,54,b)]. given #545 (T,wt=10): 636 -Shorter(c1 * (x * c4),y) | Shorter(c2,y). [resolve(616,a,54,a)]. given #546 (A,wt=21): 147 c5 = c4 | c4 * f1(c4,c5,c1,c2) = c5 | f2(c4,c5,c1,c2) * c1 = c2. [resolve(67,a,30,a)]. given #547 (F,wt=9): 2114 -Shorter(c2 * (x * y),c3 * x). [ur(54,a,140,a,c,2061,a)]. given #548 (F,wt=9): 2117 -Shorter(c2 * (x * y),x * c3). [ur(128,b,2062,a),rewrite([25(3)])]. given #549 (F,wt=9): 2247 -Shorter(c1 * (c4 * c4),c5 * c5). [ur(54,a,868,a,c,220,a)]. given #550 (F,wt=9): 2333 -Shorter(c4 * (x * c1),x * c2). [ur(54,b,980,a,c,141,a),rewrite([25(4)])]. given #551 (T,wt=10): 691 -Shorter(x,c5) | Shorter(x,c1 * (y * c4)). [resolve(617,a,54,b)]. given #552 (T,wt=10): 692 -Shorter(c1 * (x * c4),y) | Shorter(c5,y). [resolve(617,a,54,a)]. given #553 (T,wt=10): 711 -Shorter(x,c2) | Shorter(x,c1 * (c4 * y)). [resolve(694,a,54,b)]. given #554 (T,wt=10): 712 -Shorter(c1 * (c4 * x),y) | Shorter(c2,y). [resolve(694,a,54,a)]. given #555 (A,wt=12): 148 c5 = c4 | f2(c5,c4,c2,c1) * c2 = c1. [resolve(67,a,30,a(flip)),flip(a),unit_del(b,69)]. -------- Proof 1 -------- ============================== PROOF ================================= % Proof 1 at 1.10 (+ 0.01) seconds. % Length of proof is 31. % Level of proof is 8. % Maximum clause weight is 28.000. % Given clauses 555 (69.375 givens/level). 3 x * y = u * v -> x = u | (exists w1 x * w1 = u) | (exists w2 w2 * y = v) # label("EQD") # 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]. 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]. 18 u * u1 = x * x1 & -Shorter(u,x * y) -> (exists u3 u = x * u3) # label("Lemma 4") # label(non_clause) # label(goal). [goal]. 25 (x * y) * z = x * (y * z). [assumption]. 30 x * y != z * u | x = z | z * f1(z,x,u,y) = x | f2(z,x,u,y) * u = y # label("EQD"). [clausify(3)]. 54 -Shorter(x,y) | -Shorter(y,z) | Shorter(x,z). [clausify(10)]. 55 Shorter(x,x * y). [assumption]. 56 Shorter(x,y * x). [assumption]. 57 -Shorter(x,y) | Shorter(x * z,y * z). [clausify(11)]. 61 -Shorter(x,y) | Shorter(x * z,z * y). [clausify(13)]. 64 Shorter(x,y) | -Shorter(z * x,y * z). [clausify(14)]. 66 c4 * c1 = c5 * c2 # label("Lemma 4"). [deny(18)]. 67 c5 * c2 = c4 * c1. [copy(66),flip(a)]. 68 -Shorter(c4,c5 * c3) # label("Lemma 4"). [deny(18)]. 69 c5 * x != c4 # label("Lemma 4"). [deny(18)]. 140 Shorter(x * y,y * (x * z)). [resolve(61,a,55,a)]. 145 Shorter(x,y) | -Shorter(z * (u * x),y * (z * u)). [para(25(a,1),64(b,1))]. 148 c5 = c4 | f2(c5,c4,c2,c1) * c2 = c1. [resolve(67,a,30,a(flip)),flip(a),unit_del(b,69)]. 180 -Shorter(x * c4,c5 * (c3 * x)). [ur(64,a,68,a),rewrite([25(6)])]. 185 -Shorter(c4,c5). [ur(54,b,55,a,c,68,a)]. 217 -Shorter(x * c4,c5 * x). [ur(64,a,185,a)]. 507 -Shorter(c2 * c4,c4 * c1). [para(67(a,1),217(a,2))]. 699 Shorter(x * (y * z),y * (x * (u * z))). [resolve(140,a,57,a),rewrite([25(2),25(5),25(4)])]. 805 -Shorter(c2,c1). [ur(61,b,507,a)]. 6112 -Shorter(x * (y * (z * c4)),c5 * (c3 * (z * (x * y)))). [ur(145,a,180,a),rewrite([25(10),25(9)])]. 6324 c5 = c4. [para(148(b,1),56(a,2)),unit_del(b,805)]. 6327 -Shorter(x * (y * (z * c4)),c4 * (c3 * (z * (x * y)))). [back_rewrite(6112),rewrite([6324(5)])]. 6328 $F. [resolve(6327,a,699,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=555. Generated=22550. Kept=6302. proofs=1. Usable=545. Sos=5415. Demods=98. Limbo=3, Disabled=393. Hints=0. Kept_by_rule=0, Deleted_by_rule=127. Forward_subsumed=16121. Back_subsumed=246. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=106 (0 lex), Back_demodulated=92. Back_unit_deleted=0. Demod_attempts=264356. Demod_rewrites=19055. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=71138. Nonunit_bsub_feature_tests=56490. Megabytes=12.50. User_CPU=1.10, System_CPU=0.01, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED THEOREM PROVED Exiting with 1 proof. ------ process 17966 exit (max_proofs) ------  Process 17966 exit (max_proofs) Wed Jun 14 05:43:52 2017