============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 27780 was started by Papuchino on HISOKA,
Sun Dec  8 15:38:44 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.01) seconds.
% Length of proof is 8.
% Level of proof is 3.
% Maximum clause weight is 13.
% Given clauses 5.

1 (exists x -(exists y y * x = x)) # 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 = y * (x * ((y * x) * y)) # label(677).  [assumption].
4 x * (y * ((x * y) * x)) = y.  [copy(3),flip(a)].
5 x * c1 != c1.  [clausify(1)].
6 x != y | f1(y,z,x,u,w) * u = w.  [clausify(2)].
7 f1(x,y,z * (x * ((z * x) * z)),u,w) * u = w.  [resolve(6,a,4,a)].
8 f1(x,y,x,z,u) * z = u.  [para(4(a,1),7(a,1,1,3))].
9 $F.  [resolve(8,a,5,a)].

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