============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 18428 was started by Papuchino on HISOKA,
Sat Dec  7 09:43:30 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.00 (+ 0.03) seconds.
% Length of proof is 19.
% Level of proof is 7.
% Maximum clause weight is 21.
% Given clauses 32.

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

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