============================== prooftrans ============================ Prover9 (32) version Dec-2007, Dec 2007. Process 36280 was started by Papuchino on HISOKA, Sun Nov 24 11:07:42 2024 The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace4/bin-win32/prover9". ============================== end of head =========================== ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 277.81 (+ 32.08) seconds. % Length of proof is 67. % Level of proof is 27. % Maximum clause weight is 87. % Given clauses 583. 1 x * x = y * y # label(non_clause) # label(goal). [goal]. 2 x = (y * y) * ((z * u) * ((x * (y * z)) * (u * y))) # label(71557731highresources). [assumption]. 3 (x * x) * ((y * z) * ((u * (x * y)) * (z * x))) = u. [copy(2),flip(a)]. 4 c2 * c2 != c1 * c1. [deny(1)]. 5 (x * x) * (y * ((z * (x * (u * u))) * (((w * v5) * ((y * (u * w)) * (v5 * u))) * x))) = z. [para(3(a,1),3(a,1,2,1))]. 6 ((x * x) * (x * x)) * ((((y * z) * ((u * (x * y)) * (z * x))) * w) * ((v5 * u) * (w * (x * x)))) = v5. [para(3(a,1),3(a,1,2,2,1,2))]. 7 ((x * y) * (x * y)) * ((((z * (u * x)) * (y * u)) * w) * (z * (w * (x * y)))) = u * u. [para(3(a,1),3(a,1,2,2,1))]. 8 (x * x) * ((((y * (z * (u * u))) * (((w * v5) * ((x * (u * w)) * (v5 * u))) * z)) * v6) * (y * (v6 * x))) = z * z. [para(5(a,1),3(a,1,2,2,1))]. 9 (((x * y) * (x * y)) * ((x * y) * (x * y))) * ((((((z * (u * x)) * (y * u)) * w) * (z * (w * (x * y)))) * v5) * ((v6 * (u * u)) * (v5 * ((x * y) * (x * y))))) = v6. [para(7(a,1),3(a,1,2,2,1,2))]. 10 (((x * y) * ((z * (u * x)) * (y * u))) * ((x * y) * ((z * (u * x)) * (y * u)))) * ((((w * (v5 * (x * y))) * (((z * (u * x)) * (y * u)) * v5)) * (u * u)) * (w * z)) = v5 * v5. [para(3(a,1),7(a,1,2,2,2))]. 11 (((x * y) * ((z * (u * x)) * (y * u))) * ((x * y) * ((z * (u * x)) * (y * u)))) * ((((w * (v5 * (v6 * v6))) * (((v7 * v8) * ((((x * y) * ((z * (u * x)) * (y * u))) * (v6 * v7)) * (v8 * v6))) * v5)) * (u * u)) * (w * z)) = v5 * v5. [para(3(a,1),8(a,1,2,2,2))]. 12 ((x * x) * (x * x)) * (y * y) = (((z * u) * (((x * x) * (x * z)) * (u * x))) * (y * (z * u))) * ((((x * x) * (x * z)) * (u * x)) * y). [para(10(a,1),6(a,1,2))]. 13 (((x * y) * (((z * z) * (z * x)) * (y * z))) * (u * (x * y))) * ((((z * z) * (z * x)) * (y * z)) * u) = ((z * z) * (z * z)) * (u * u). [copy(12),flip(a)]. 14 (((x * y) * (x * y)) * ((x * y) * (x * y))) * ((((((z * ((((u * u) * (u * w)) * (v5 * u)) * x)) * (y * (((u * u) * (u * w)) * (v5 * u)))) * v6) * (z * (v6 * (x * y)))) * v7) * ((((u * u) * (u * u)) * ((((u * u) * (u * w)) * (v5 * u)) * (((u * u) * (u * w)) * (v5 * u)))) * (v7 * ((x * y) * (x * y))))) = ((w * v5) * (((u * u) * (u * w)) * (v5 * u))) * ((((u * u) * (u * w)) * (v5 * u)) * (w * v5)). [para(13(a,1),9(a,1,2,2,1))]. 15 (u * u) * (u * u) = ((w * v5) * (((u * u) * (u * w)) * (v5 * u))) * ((((u * u) * (u * w)) * (v5 * u)) * (w * v5)). [para(9(a,1),14(a,1))]. 16 ((x * y) * (((z * z) * (z * x)) * (y * z))) * ((((z * z) * (z * x)) * (y * z)) * (x * y)) = (z * z) * (z * z). [copy(15),flip(a)]. 17 (x * x) * (((y * y) * (y * y)) * ((z * (x * ((u * w) * (((y * y) * (y * u)) * (w * y))))) * (((((y * y) * (y * u)) * (w * y)) * (u * w)) * x))) = z. [para(16(a,1),3(a,1,2,1))]. 18 (x * (((y * y) * (y * (z * z))) * (((u * w) * ((x * (z * u)) * (w * z))) * y))) * ((((y * y) * (y * (z * z))) * (((u * w) * ((x * (z * u)) * (w * z))) * y)) * ((z * z) * ((u * w) * ((x * (z * u)) * (w * z))))) = (y * y) * (y * y). [para(3(a,1),16(a,1,1,1))]. 19 (x * (((y * y) * (y * (z * z))) * (((u * w) * ((x * (z * u)) * (w * z))) * y))) * ((((y * y) * (y * (z * z))) * (((u * w) * ((x * (z * u)) * (w * z))) * y)) * x) = (y * y) * (y * y). [para(3(a,1),18(a,1,2,2))]. 20 ((x * x) * (x * x)) * (((x * x) * (x * x)) * ((y * (x * x)) * (((((x * x) * (x * z)) * (u * x)) * (z * u)) * (x * x)))) = y. [para(16(a,1),6(a,1,2,1))]. 21 ((x * x) * (x * x)) * (y * y) = (((z * u) * (((x * x) * (x * z)) * (u * x))) * (y * (w * w))) * (((v5 * v6) * ((((z * u) * (((x * x) * (x * z)) * (u * x))) * (w * v5)) * (v6 * w))) * y). [para(11(a,1),6(a,1,2))]. 22 (((x * y) * (((z * z) * (z * x)) * (y * z))) * (u * (w * w))) * (((v5 * v6) * ((((x * y) * (((z * z) * (z * x)) * (y * z))) * (w * v5)) * (v6 * w))) * u) = ((z * z) * (z * z)) * (u * u). [copy(21),flip(a)]. 23 (((x * y) * (x * y)) * ((x * y) * (x * y))) * ((((((z * (((u * w) * ((((v5 * v6) * (((v7 * v7) * (v7 * v5)) * (v6 * v7))) * (v8 * u)) * (w * v8))) * x)) * (y * ((u * w) * ((((v5 * v6) * (((v7 * v7) * (v7 * v5)) * (v6 * v7))) * (v8 * u)) * (w * v8))))) * v9) * (z * (v9 * (x * y)))) * v10) * ((((v7 * v7) * (v7 * v7)) * (((u * w) * ((((v5 * v6) * (((v7 * v7) * (v7 * v5)) * (v6 * v7))) * (v8 * u)) * (w * v8))) * ((u * w) * ((((v5 * v6) * (((v7 * v7) * (v7 * v5)) * (v6 * v7))) * (v8 * u)) * (w * v8))))) * (v10 * ((x * y) * (x * y))))) = ((v5 * v6) * (((v7 * v7) * (v7 * v5)) * (v6 * v7))) * (((u * w) * ((((v5 * v6) * (((v7 * v7) * (v7 * v5)) * (v6 * v7))) * (v8 * u)) * (w * v8))) * (v8 * v8)). [para(22(a,1),9(a,1,2,2,1))]. 24 (v7 * v7) * (v7 * v7) = ((v5 * v6) * (((v7 * v7) * (v7 * v5)) * (v6 * v7))) * (((u * w) * ((((v5 * v6) * (((v7 * v7) * (v7 * v5)) * (v6 * v7))) * (v8 * u)) * (w * v8))) * (v8 * v8)). [para(9(a,1),23(a,1))]. 25 ((x * y) * (((z * z) * (z * x)) * (y * z))) * (((u * w) * ((((x * y) * (((z * z) * (z * x)) * (y * z))) * (v5 * u)) * (w * v5))) * (v5 * v5)) = (z * z) * (z * z). [copy(24),flip(a)]. 26 ((((x * ((y * z) * y)) * (z * (y * z))) * u) * (x * (u * (y * z)))) * (((w * v5) * ((((((x * ((y * z) * y)) * (z * (y * z))) * u) * ((((y * z) * (y * z)) * ((y * z) * ((x * ((y * z) * y)) * (z * (y * z))))) * (u * (y * z)))) * (v6 * w)) * (v5 * v6))) * (v6 * v6)) = ((y * z) * (y * z)) * ((y * z) * (y * z)). [para(3(a,1),25(a,1,1,2,1))]. 27 ((((x * ((y * z) * y)) * (z * (y * z))) * u) * (x * (u * (y * z)))) * (((w * v5) * ((((((x * ((y * z) * y)) * (z * (y * z))) * u) * (x * (u * (y * z)))) * (v6 * w)) * (v5 * v6))) * (v6 * v6)) = ((y * z) * (y * z)) * ((y * z) * (y * z)). [para(3(a,1),26(a,1,2,1,2,1,1,2,1))]. 28 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))))) * v5) * (x * (v5 * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))))) * (((v6 * v7) * ((((((x * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))))) * v5) * (x * (v5 * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))) * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))). [para(3(a,1),27(a,1,1,1,1,1,2,1))]. 29 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))))) * (((v6 * v7) * ((((((x * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))))) * v5) * (x * (v5 * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))) * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))). [para(3(a,1),28(a,1,1,1,1,2,2))]. 30 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (((v6 * v7) * ((((((x * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))))) * v5) * (x * (v5 * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))) * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))). [para(3(a,1),29(a,1,1,2,2,2))]. 31 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (((v6 * v7) * ((((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))))) * v5) * (x * (v5 * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))) * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))). [para(3(a,1),30(a,1,2,1,2,1,1,1,1,1,2,1))]. 32 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (((v6 * v7) * ((((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))) * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))). [para(3(a,1),31(a,1,2,1,2,1,1,1,1,2,2))]. 33 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (((v6 * v7) * ((((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))) * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))). [para(3(a,1),32(a,1,2,1,2,1,1,2,2,2))]. 34 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (((v6 * v7) * ((((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (y * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))) * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))). [para(3(a,1),33(a,2,1,1))]. 35 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (((v6 * v7) * ((((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (y * y) * (((z * z) * ((u * w) * ((y * (z * u)) * (w * z)))) * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))). [para(3(a,1),34(a,2,1,2))]. 36 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (((v6 * v7) * ((((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (y * y) * (y * ((z * z) * ((u * w) * ((y * (z * u)) * (w * z))))). [para(3(a,1),35(a,2,2,1))]. 37 ((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (((v6 * v7) * ((((((x * (y * (z * z))) * (((u * w) * ((y * (z * u)) * (w * z))) * y)) * v5) * (x * (v5 * y))) * (v8 * v6)) * (v7 * v8))) * (v8 * v8)) = (y * y) * (y * y). [para(3(a,1),36(a,2,2,2))]. 38 ((x * x) * (x * x)) * ((((((x * x) * (x * (y * y))) * (((z * u) * ((x * (y * z)) * (u * y))) * x)) * x) * ((x * x) * (x * x))) * ((x * x) * (x * x))) = (((x * x) * (x * (y * y))) * (((z * u) * ((x * (y * z)) * (u * y))) * x)) * x. [para(37(a,1),5(a,1,2,2))]. 39 ((x * x) * (x * x)) * ((((x * x) * (x * (y * y))) * (((z * u) * ((x * (y * z)) * (u * y))) * x)) * x) = (((x * x) * (x * (y * y))) * (((z * u) * ((x * (y * z)) * (u * y))) * x)) * x. [para(38(a,1),3(a,1,2))]. 40 (x * x) * ((x * (((x * x) * (x * (y * y))) * (((z * u) * ((x * (y * z)) * (u * y))) * x))) * ((((x * x) * (x * (y * y))) * (((z * u) * ((x * (y * z)) * (u * y))) * x)) * x)) = x * x. [para(39(a,1),3(a,1,2,2))]. 41 (x * x) * ((x * x) * (x * x)) = x * x. [para(19(a,1),40(a,1,2))]. 42 (x * x) * ((y * y) * ((z * (x * (y * y))) * (((y * (((y * y) * (y * (u * u))) * (((w * v5) * ((y * (u * w)) * (v5 * u))) * y))) * ((((y * y) * (y * (u * u))) * (((w * v5) * ((y * (u * w)) * (v5 * u))) * y)) * y)) * x))) = z. [para(39(a,1),5(a,1,2,2,2,1,2))]. 43 (x * x) * ((y * y) * ((z * (x * (y * y))) * (((y * y) * (y * y)) * x))) = z. [para(19(a,1),42(a,1,2,2,2,1))]. 44 ((x * x) * (x * x)) * (((((x * x) * (y * x)) * (x * y)) * (x * x)) * (x * x)) = y * y. [para(41(a,1),7(a,1,2,2))]. 45 ((x * x) * (x * x)) * ((((y * z) * ((x * (x * y)) * (z * x))) * (x * x)) * (x * x)) = x. [para(41(a,1),6(a,1,2,2))]. 46 ((x * x) * (x * x)) * ((x * x) * ((x * x) * (((x * x) * (x * x)) * (x * x)))) = x * x. [para(41(a,1),43(a,1,2,2,1))]. 47 ((x * x) * (x * x)) * (x * x) = x * x. [para(3(a,1),46(a,1,2))]. 48 (x * x) * ((y * y) * ((z * (x * ((y * y) * (y * y)))) * ((y * y) * x))) = z. [para(47(a,1),3(a,1,2,1))]. 49 (x * x) * ((x * y) * ((x * x) * (y * x))) = (x * x) * (x * x). [para(47(a,1),3(a,1,2,2,1))]. 50 ((x * x) * (x * x)) * ((((x * x) * (x * x)) * (x * x)) * (x * x)) = (x * x) * (x * x). [para(47(a,1),16(a,1,1,2))]. 51 ((x * x) * (x * x)) * ((x * x) * (x * x)) = (x * x) * (x * x). [para(47(a,1),50(a,1,2,1))]. 52 ((x * x) * (x * x)) * (((x * x) * (x * x)) * ((y * (x * x)) * (((x * x) * (x * x)) * (x * x)))) = y. [para(47(a,1),20(a,1,2,2,2,1,1))]. 53 ((x * x) * (x * x)) * (((x * x) * (x * x)) * ((y * (x * x)) * (x * x))) = y. [para(47(a,1),52(a,1,2,2,2))]. 54 (x * x) * (((y * y) * (y * y)) * ((z * (x * ((y * y) * (y * y)))) * (((((y * y) * (y * y)) * (y * y)) * (y * y)) * x))) = z. [para(47(a,1),17(a,1,2,2,1,2,2,2))]. 55 (x * x) * (((y * y) * (y * y)) * ((z * (x * ((y * y) * (y * y)))) * (((y * y) * (y * y)) * x))) = z. [para(47(a,1),54(a,1,2,2,2,1,1))]. 56 ((x * x) * (x * x)) * (y * y) = ((x * x) * (y * x)) * (x * y). [para(44(a,1),53(a,1,2))]. 57 ((x * x) * (y * x)) * (x * y) = ((x * x) * (x * x)) * (y * y). [copy(56),flip(a)]. 58 ((x * x) * (x * x)) * x = (y * z) * ((x * (x * y)) * (z * x)). [para(45(a,1),53(a,1,2))]. 59 (((x * x) * (x * x)) * ((x * x) * (x * x))) * (x * x) = (((y * z) * ((u * (x * y)) * (z * x))) * w) * (((x * x) * u) * (w * (x * x))). [para(3(a,1),58(a,2,2,1,2))]. 60 ((x * x) * (x * x)) * (x * x) = (((y * z) * ((u * (x * y)) * (z * x))) * w) * (((x * x) * u) * (w * (x * x))). [para(51(a,1),59(a,1,1))]. 61 x * x = (((y * z) * ((u * (x * y)) * (z * x))) * w) * (((x * x) * u) * (w * (x * x))). [para(47(a,1),60(a,1))]. 62 (((x * y) * ((z * (u * x)) * (y * u))) * w) * (((u * u) * z) * (w * (u * u))) = u * u. [copy(61),flip(a)]. 63 (((x * x) * (x * x)) * ((x * x) * (x * x))) * (x * x) = (((y * (x * x)) * (x * x)) * z) * (y * (z * (x * x))). [para(3(a,1),58(a,2,2,1))]. 64 ((x * x) * (x * x)) * (x * x) = (((y * (x * x)) * (x * x)) * z) * (y * (z * (x * x))). [para(51(a,1),63(a,1,1))]. 65 x * x = (((y * (x * x)) * (x * x)) * z) * (y * (z * (x * x))). [para(47(a,1),64(a,1))]. 66 (((x * (y * y)) * (y * y)) * z) * (x * (z * (y * y))) = y * y. [copy(65),flip(a)]. 67 (((x * x) * (x * x)) * ((x * x) * (x * x))) * (x * x) = ((x * x) * y) * ((x * x) * (y * (x * x))). [para(41(a,1),58(a,2,2,1))]. 68 ((x * x) * (x * x)) * (x * x) = ((x * x) * y) * ((x * x) * (y * (x * x))). [para(51(a,1),67(a,1,1))]. 69 x * x = ((x * x) * y) * ((x * x) * (y * (x * x))). [para(47(a,1),68(a,1))]. 70 ((x * x) * y) * ((x * x) * (y * (x * x))) = x * x. [copy(69),flip(a)]. 71 (x * x) * ((x * ((x * x) * (x * x))) * ((x * x) * ((y * z) * ((x * (x * y)) * (z * x))))) = (x * x) * (x * x). [para(58(a,1),49(a,1,2,2,2))]. 72 (x * x) * ((x * ((x * x) * (x * x))) * x) = (x * x) * (x * x). [para(3(a,1),71(a,1,2,2))]. 73 ((x * x) * ((y * z) * ((x * (x * y)) * (z * x)))) * (x * ((x * x) * (x * x))) = ((x * x) * (x * x)) * (((x * x) * (x * x)) * ((x * x) * (x * x))). [para(58(a,1),57(a,1,1,2))]. 74 x * (x * ((x * x) * (x * x))) = ((x * x) * (x * x)) * (((x * x) * (x * x)) * ((x * x) * (x * x))). [para(3(a,1),73(a,1,1))]. 75 x * (x * ((x * x) * (x * x))) = ((x * x) * (x * x)) * ((x * x) * (x * x)). [para(51(a,1),74(a,2,2))]. 76 x * (x * ((x * x) * (x * x))) = (x * x) * (x * x). [para(51(a,1),75(a,2))]. 77 ((x * x) * (x * x)) * (((y * (x * x)) * z) * ((x * x) * (z * (x * x)))) = (x * x) * y. [para(70(a,1),3(a,1,2,2,1))]. 78 x * ((y * y) * (((z * z) * ((x * (y * ((z * z) * (z * z)))) * ((z * z) * y))) * (y * y))) = y * y. [para(48(a,1),70(a,1,1))]. 79 (x * x) * ((((x * x) * (x * x)) * y) * (((x * x) * (x * x)) * (y * x))) = x. [para(76(a,1),3(a,1,2,2,1))]. 80 (x * x) * (((x * x) * (x * x)) * ((x * x) * ((x * ((x * x) * (x * x))) * x))) = (x * x) * (x * x). [para(76(a,1),49(a,1,2,1))]. 81 (x * x) * (((x * x) * (x * x)) * ((x * x) * (x * x))) = (x * x) * (x * x). [para(72(a,1),80(a,1,2,2))]. 82 (x * x) * ((x * x) * (x * x)) = (x * x) * (x * x). [para(51(a,1),81(a,1,2))]. 83 x * x = (x * x) * (x * x). [para(41(a,1),82(a,1))]. 84 (x * x) * (x * x) = x * x. [copy(83),flip(a)]. 85 ((x * x) * (x * x)) * x = ((x * ((x * x) * (x * x))) * y) * ((x * ((x * x) * (x * x))) * (y * x)). [para(76(a,1),58(a,2,2,1,2))]. 86 (x * x) * x = ((x * ((x * x) * (x * x))) * y) * ((x * ((x * x) * (x * x))) * (y * x)). [para(84(a,1),85(a,1,1))]. 87 (x * x) * x = ((x * (x * x)) * y) * ((x * ((x * x) * (x * x))) * (y * x)). [para(84(a,1),86(a,2,1,1,2))]. 88 (x * x) * x = ((x * (x * x)) * y) * ((x * (x * x)) * (y * x)). [para(84(a,1),87(a,2,2,1,2))]. 89 ((x * (x * x)) * y) * ((x * (x * x)) * (y * x)) = (x * x) * x. [copy(88),flip(a)]. 90 ((x * x) * (x * x)) * x = (((x * x) * (x * x)) * y) * (((x * x) * (x * x)) * (y * x)). [para(76(a,1),58(a,2,2,1))]. 91 (x * x) * x = (((x * x) * (x * x)) * y) * (((x * x) * (x * x)) * (y * x)). [para(84(a,1),90(a,1,1))]. 92 (x * x) * x = ((x * x) * y) * (((x * x) * (x * x)) * (y * x)). [para(84(a,1),91(a,2,1,1))]. 93 (x * x) * x = ((x * x) * y) * ((x * x) * (y * x)). [para(84(a,1),92(a,2,2,1))]. 94 ((x * x) * y) * ((x * x) * (y * x)) = (x * x) * x. [copy(93),flip(a)]. 95 (x * x) * (((x * x) * y) * (((x * x) * (x * x)) * (y * x))) = x. [para(84(a,1),79(a,1,2,1,1))]. 96 (x * x) * (((x * x) * y) * ((x * x) * (y * x))) = x. [para(84(a,1),95(a,1,2,2,1))]. 97 (x * x) * ((x * x) * x) = x. [para(94(a,1),96(a,1,2))]. 98 x * ((y * y) * (((z * z) * ((x * (y * (z * z))) * ((z * z) * y))) * (y * y))) = y * y. [para(84(a,1),78(a,1,2,2,1,2,1,2,2))]. 99 (x * x) * (((y * (x * x)) * z) * ((x * x) * (z * (x * x)))) = (x * x) * y. [para(84(a,1),77(a,1,1))]. 100 (x * x) * x = (y * z) * ((x * (x * y)) * (z * x)). [para(84(a,1),58(a,1,1))]. 101 (x * y) * ((z * (z * x)) * (y * z)) = (z * z) * z. [copy(100),flip(a)]. 102 (x * x) * ((y * y) * ((z * (x * ((y * y) * (y * y)))) * (((y * y) * (y * y)) * x))) = z. [para(84(a,1),55(a,1,2,1))]. 103 (x * x) * ((y * y) * ((z * (x * (y * y))) * (((y * y) * (y * y)) * x))) = z. [para(84(a,1),102(a,1,2,2,1,2,2))]. 104 (x * x) * ((y * y) * ((z * (x * (y * y))) * ((y * y) * x))) = z. [para(84(a,1),103(a,1,2,2,2,1))]. 105 ((x * x) * x) * (x * x) = (x * x) * x. [para(84(a,1),94(a,1,2))]. 106 (((x * y) * ((z * (z * x)) * (y * z))) * (z * z)) * ((z * z) * z) = z * z. [para(94(a,1),62(a,1,2))]. 107 (((z * z) * z) * (z * z)) * ((z * z) * z) = z * z. [para(101(a,1),106(a,1,1,1))]. 108 ((x * x) * x) * ((x * x) * x) = x * x. [para(105(a,1),107(a,1,1))]. 109 ((x * x) * y) * ((((x * x) * x) * ((x * x) * x)) * (y * ((x * x) * x))) = (((x * x) * x) * ((x * x) * x)) * ((x * x) * x). [para(108(a,1),94(a,1,1,1))]. 110 ((x * x) * y) * ((x * x) * (y * ((x * x) * x))) = (((x * x) * x) * ((x * x) * x)) * ((x * x) * x). [para(108(a,1),109(a,1,2,1))]. 111 ((x * x) * y) * ((x * x) * (y * ((x * x) * x))) = (x * x) * ((x * x) * x). [para(108(a,1),110(a,2,1))]. 112 ((x * x) * y) * ((x * x) * (y * ((x * x) * x))) = x. [para(97(a,1),111(a,2))]. 113 ((((x * x) * x) * ((x * x) * x)) * ((x * x) * x)) * ((((x * x) * x) * ((x * x) * x)) * (x * x)) = (((x * x) * x) * ((x * x) * x)) * ((x * x) * x). [para(108(a,1),94(a,1,2,2))]. 114 ((x * x) * ((x * x) * x)) * ((((x * x) * x) * ((x * x) * x)) * (x * x)) = (((x * x) * x) * ((x * x) * x)) * ((x * x) * x). [para(108(a,1),113(a,1,1,1))]. 115 x * ((((x * x) * x) * ((x * x) * x)) * (x * x)) = (((x * x) * x) * ((x * x) * x)) * ((x * x) * x). [para(97(a,1),114(a,1,1))]. 116 x * ((x * x) * (x * x)) = (((x * x) * x) * ((x * x) * x)) * ((x * x) * x). [para(108(a,1),115(a,1,2,1))]. 117 x * (x * x) = (((x * x) * x) * ((x * x) * x)) * ((x * x) * x). [para(84(a,1),116(a,1,2))]. 118 x * (x * x) = (x * x) * ((x * x) * x). [para(108(a,1),117(a,2,1))]. 119 x * (x * x) = x. [para(97(a,1),118(a,2))]. 120 (x * y) * ((x * (x * x)) * (y * x)) = (x * x) * x. [para(119(a,1),89(a,1,1,1))]. 121 (x * y) * (x * (y * x)) = (x * x) * x. [para(119(a,1),120(a,1,2,1))]. 122 ((x * (x * x)) * y) * (x * (y * (x * x))) = x * x. [para(119(a,1),66(a,1,1,1,1))]. 123 (x * y) * (x * (y * (x * x))) = x * x. [para(119(a,1),122(a,1,1,1))]. 124 (((x * (y * y)) * (y * y)) * y) * (x * y) = y * y. [para(119(a,1),66(a,1,2,2))]. 125 x * (x * ((x * x) * x)) = (x * x) * x. [para(119(a,1),121(a,1,1))]. 126 (x * ((x * x) * x)) * (x * ((x * x) * x)) = x * x. [para(105(a,1),123(a,1,2,2))]. 127 (((x * ((x * x) * x)) * (x * ((x * x) * x))) * x) * (((x * ((x * x) * x)) * (x * ((x * x) * x))) * ((x * x) * x)) = ((x * ((x * x) * x)) * (x * ((x * x) * x))) * (x * ((x * x) * x)). [para(125(a,1),94(a,1,2,2))]. 128 ((x * x) * x) * (((x * ((x * x) * x)) * (x * ((x * x) * x))) * ((x * x) * x)) = ((x * ((x * x) * x)) * (x * ((x * x) * x))) * (x * ((x * x) * x)). [para(126(a,1),127(a,1,1,1))]. 129 ((x * x) * x) * ((x * x) * ((x * x) * x)) = ((x * ((x * x) * x)) * (x * ((x * x) * x))) * (x * ((x * x) * x)). [para(126(a,1),128(a,1,2,1))]. 130 ((x * x) * x) * x = ((x * ((x * x) * x)) * (x * ((x * x) * x))) * (x * ((x * x) * x)). [para(97(a,1),129(a,1,2))]. 131 ((x * x) * x) * x = (x * x) * (x * ((x * x) * x)). [para(126(a,1),130(a,2,1))]. 132 (x * y) * ((((x * x) * x) * ((x * x) * (x * ((x * x) * x)))) * (y * ((x * x) * x))) = (((x * x) * x) * ((x * x) * x)) * ((x * x) * x). [para(131(a,1),101(a,1,2,1,2))]. 133 (x * y) * (x * (y * ((x * x) * x))) = (((x * x) * x) * ((x * x) * x)) * ((x * x) * x). [para(112(a,1),132(a,1,2,1))]. 134 (x * y) * (x * (y * ((x * x) * x))) = (x * x) * ((x * x) * x). [para(108(a,1),133(a,2,1))]. 135 (x * y) * (x * (y * ((x * x) * x))) = x. [para(97(a,1),134(a,2))]. 136 (x * x) * (((x * x) * (x * x)) * ((x * x) * ((y * (x * x)) * (x * x)))) = (x * x) * ((y * ((x * x) * (x * x))) * ((x * x) * (x * x))). [para(124(a,1),99(a,1,2,1))]. 137 (x * x) * ((x * x) * ((x * x) * ((y * (x * x)) * (x * x)))) = (x * x) * ((y * ((x * x) * (x * x))) * ((x * x) * (x * x))). [para(84(a,1),136(a,1,2,1))]. 138 (x * x) * y = (x * x) * ((y * ((x * x) * (x * x))) * ((x * x) * (x * x))). [para(3(a,1),137(a,1,2))]. 139 (x * x) * y = (x * x) * ((y * (x * x)) * ((x * x) * (x * x))). [para(84(a,1),138(a,2,2,1,2))]. 140 (x * x) * y = (x * x) * ((y * (x * x)) * (x * x)). [para(84(a,1),139(a,2,2,2))]. 141 (x * x) * ((y * (x * x)) * (x * x)) = (x * x) * y. [copy(140),flip(a)]. 142 (x * x) * (((y * (x * x)) * (((x * (x * x)) * (x * x)) * x)) * ((x * x) * (x * x))) = (x * x) * y. [para(124(a,1),99(a,1,2,2,2))]. 143 (x * x) * (((y * (x * x)) * ((x * (x * x)) * x)) * ((x * x) * (x * x))) = (x * x) * y. [para(119(a,1),142(a,1,2,1,2,1,1))]. 144 (x * x) * (((y * (x * x)) * (x * x)) * ((x * x) * (x * x))) = (x * x) * y. [para(119(a,1),143(a,1,2,1,2,1))]. 145 (x * x) * (((y * (x * x)) * (x * x)) * (x * x)) = (x * x) * y. [para(84(a,1),144(a,1,2,2))]. 146 (x * x) * (y * (x * x)) = (x * x) * y. [para(141(a,1),145(a,1))]. 147 (x * x) * (((y * ((x * ((x * x) * x)) * (x * ((x * x) * x)))) * z) * (((x * ((x * x) * x)) * (x * ((x * x) * x))) * (z * ((x * ((x * x) * x)) * (x * ((x * x) * x)))))) = ((x * ((x * x) * x)) * (x * ((x * x) * x))) * y. [para(126(a,1),99(a,1,1))]. 148 (x * x) * (((y * (x * x)) * z) * (((x * ((x * x) * x)) * (x * ((x * x) * x))) * (z * ((x * ((x * x) * x)) * (x * ((x * x) * x)))))) = ((x * ((x * x) * x)) * (x * ((x * x) * x))) * y. [para(126(a,1),147(a,1,2,1,1,2))]. 149 (x * x) * (((y * (x * x)) * z) * ((x * x) * (z * ((x * ((x * x) * x)) * (x * ((x * x) * x)))))) = ((x * ((x * x) * x)) * (x * ((x * x) * x))) * y. [para(126(a,1),148(a,1,2,2,1))]. 150 (x * x) * (((y * (x * x)) * z) * ((x * x) * (z * (x * x)))) = ((x * ((x * x) * x)) * (x * ((x * x) * x))) * y. [para(126(a,1),149(a,1,2,2,2,2))]. 151 (x * x) * (((y * (x * x)) * z) * ((x * x) * z)) = ((x * ((x * x) * x)) * (x * ((x * x) * x))) * y. [para(146(a,1),150(a,1,2,2))]. 152 (x * x) * (((y * (x * x)) * z) * ((x * x) * z)) = (x * x) * y. [para(126(a,1),151(a,2,1))]. 153 ((x * x) * y) * ((x * x) * ((((y * (x * x)) * z) * ((x * x) * (z * (x * x)))) * (((x * x) * (x * x)) * (x * x)))) = x * x. [para(99(a,1),135(a,1,1))]. 154 ((x * x) * y) * ((x * x) * ((((y * (x * x)) * z) * ((x * x) * z)) * (((x * x) * (x * x)) * (x * x)))) = x * x. [para(146(a,1),153(a,1,2,2,1,2))]. 155 ((x * x) * y) * ((x * x) * ((((y * (x * x)) * z) * ((x * x) * z)) * ((x * x) * (x * x)))) = x * x. [para(84(a,1),154(a,1,2,2,2,1))]. 156 ((x * x) * y) * ((x * x) * ((((y * (x * x)) * z) * ((x * x) * z)) * (x * x))) = x * x. [para(84(a,1),155(a,1,2,2,2))]. 157 ((x * x) * y) * ((x * x) * (((y * (x * x)) * z) * ((x * x) * z))) = x * x. [para(146(a,1),156(a,1,2))]. 158 ((x * x) * y) * ((x * x) * y) = x * x. [para(152(a,1),157(a,1,2))]. 159 (x * x) * (((((y * y) * (((z * z) * (((x * x) * (y * (z * z))) * ((z * z) * y))) * (y * y))) * (x * x)) * u) * ((x * x) * (u * (x * x)))) = y * y. [para(98(a,1),99(a,2))]. 160 (x * x) * (((((y * y) * ((z * z) * (((x * x) * (y * (z * z))) * ((z * z) * y)))) * (x * x)) * u) * ((x * x) * (u * (x * x)))) = y * y. [para(146(a,1),159(a,1,2,1,1,1))]. 161 (x * x) * ((((x * x) * (x * x)) * u) * ((x * x) * (u * (x * x)))) = y * y. [para(104(a,1),160(a,1,2,1,1,1))]. 162 (x * x) * (((x * x) * u) * ((x * x) * (u * (x * x)))) = y * y. [para(84(a,1),161(a,1,2,1,1))]. 163 (x * x) * (((x * x) * u) * ((x * x) * u)) = y * y. [para(146(a,1),162(a,1,2,2))]. 164 (x * x) * (x * x) = y * y. [para(158(a,1),163(a,1,2))]. 165 x * x = y * y. [para(84(a,1),164(a,1))]. 166 $F. [resolve(165,a,4,a)]. ============================== end of proof ==========================