============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 10688 was started by Papuchino on HISOKA,
Sun Dec  8 15:37:55 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.08 (+ 0.05) seconds.
% Length of proof is 20.
% Level of proof is 8.
% Maximum clause weight is 21.
% Given clauses 66.

1 x * y = x * z -> y = z # label(non_clause).  [assumption].
2 (x * y = z * y -> x = z) <-> (all u all w exists v5 v5 * u = w) # label(non_clause).  [assumption].
3 x = ((x * x) * x) * x # label(255) # label(non_clause) # label(goal).  [goal].
4 x = y * (x * ((y * x) * y)) # label(677).  [assumption].
5 x * (y * ((x * y) * x)) = y.  [copy(4),flip(a)].
6 x * y != x * z | y = z.  [clausify(1)].
7 x != y | f1(y,z,x,u,w) * u = w.  [clausify(2)].
8 ((c1 * c1) * c1) * c1 != c1 # label(255).  [deny(3)].
9 x * ((y * ((x * y) * x)) * (y * x)) = y * ((x * y) * x).  [para(5(a,1),5(a,1,2,2,1))].
10 (x * y) * ((x * (x * y)) * x) = y.  [resolve(6,a,5,a)].
11 x != y * z | x * ((y * x) * y) = z.  [para(5(a,1),6(a,1))].
12 x * y != z | z * ((x * z) * x) = y.  [copy(11),flip(a)].
13 f1(x,y,z * (x * ((z * x) * z)),u,w) * u = w.  [resolve(7,a,5,a)].
14 f1(x,y,x,z,u) * z = u.  [para(5(a,1),13(a,1,1,3))].
15 (x * ((x * x) * x)) * (x * x) = (x * x) * x.  [resolve(9,a,6,a)].
16 f1(x,y,x,z,u) * (z * (u * f1(x,y,x,z,u))) = z.  [para(14(a,1),5(a,1,2,2,1))].
17 f1(x,y,x,z,u) * w != u | w = z.  [para(14(a,1),6(a,2))].
18 x * (x * f1(y,z,y,x,x)) = x.  [resolve(16,a,17,a)].
19 x * ((x * x) * x) = x * f1(y,z,y,x,x).  [resolve(18,a,12,a)].
20 x * f1(y,z,y,x,x) = x * ((x * x) * x).  [copy(19),flip(a)].
21 (x * f1(y,z,y,x,x)) * (x * x) = f1(y,z,y,x,x).  [para(18(a,1),10(a,1,2,1))].
22 (x * ((x * x) * x)) * (x * x) = f1(y,z,y,x,x).  [para(20(a,1),21(a,1,1))].
23 (x * x) * x = f1(y,z,y,x,x).  [para(15(a,1),22(a,1))].
24 f1(x,y,x,z,z) = (z * z) * z.  [copy(23),flip(a)].
25 ((x * x) * x) * x = x.  [para(24(a,1),14(a,1,1))].
26 $F.  [resolve(25,a,8,a)].

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