============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 15128 was started by Papuchino on HISOKA,
Sat Nov 23 23:49:22 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 0.01 (+ 0.03) seconds.
% Length of proof is 24.
% Level of proof is 10.
% Maximum clause weight is 23.
% Given clauses 21.

1 x = y * ((((y * y) * x) * z) * (((y * y) * y) * z)) # label(non_clause) # label(goal).  [goal].
2 x = (y * y) * ((z * u) * ((x * (y * z)) * (u * y))).  [assumption].
3 (x * x) * ((y * z) * ((u * (x * y)) * (z * x))) = u.  [copy(2),flip(a)].
4 x * x = y * y.  [assumption].
5 c2 * ((((c2 * c2) * c1) * c3) * (((c2 * c2) * c2) * c3)) != c1.  [deny(1)].
6 (x * x) * ((y * z) * ((u * (w * y)) * (z * w))) = u.  [para(4(a,1),3(a,1,1))].
11 c2 * ((((x * x) * c1) * c3) * (((c2 * c2) * c2) * c3)) != c1.  [para(4(a,1),5(a,1,2,1,1,1))].
13 (x * x) * ((y * y) * ((z * (u * w)) * (w * u))) = z.  [para(4(a,1),6(a,1,2,1))].
15 (x * x) * ((y * z) * ((u * u) * (z * w))) = w * y.  [para(4(a,1),6(a,1,2,2,1))].
18 c2 * ((((x * x) * c1) * c3) * (((y * y) * c2) * c3)) != c1.  [para(4(a,1),11(a,1,2,2,1,1))].
19 (x * x) * ((y * y) * ((z * (u * u)) * (w * w))) = z.  [para(4(a,1),13(a,1,2,2,1,2))].
22 (x * y) * (z * (y * x)) = (u * u) * z.  [para(13(a,1),6(a,1,2)),flip(a)].
24 ((x * (y * z)) * (z * y)) * (u * u) = (w * w) * ((v5 * v5) * x).  [para(13(a,1),13(a,1,2,2)),flip(a)].
27 (x * y) * (z * z) = (u * u) * (y * x).  [para(4(a,1),22(a,1,2))].
29 (x * x) * ((y * y) * (z * (u * u))) = z.  [para(22(a,1),6(a,1,2))].
50 x * (y * y) = x.  [back_rewrite(19),rewrite([29(8)])].
56 (x * x) * ((y * y) * z) = z.  [back_rewrite(29),rewrite([50(4)])].
57 (x * x) * (y * z) = z * y.  [back_rewrite(27),rewrite([50(3)]),flip(a)].
58 (x * (y * z)) * (z * y) = x.  [back_rewrite(24),rewrite([50(6),56(8)])].
107 c2 * (((x * x) * (c3 * ((y * y) * c1))) * (((z * z) * c2) * c3)) != c1.  [para(57(a,2),18(a,1,2,1))].
116 ((x * x) * (y * z)) * (u * y) = z * u.  [para(57(a,1),15(a,1))].
124 c2 * (((x * x) * c1) * ((y * y) * c2)) != c1.  [back_rewrite(107),rewrite([116(14)])].
129 (x * ((y * y) * z)) * z = x.  [para(22(a,1),58(a,1,1,2)),rewrite([58(7)])].
152 $F.  [para(57(a,2),124(a,1)),rewrite([129(10),56(5)]),xx(a)].

============================== end of proof ==========================