============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 20880 was started by Papuchino on HISOKA,
Wed Dec 11 17:06:16 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.00) seconds: 255.
% Length of proof is 25.
% Level of proof is 7.
% Maximum clause weight is 24.
% Given clauses 43.

1 x * y = x * z -> y = z # label(non_clause).  [assumption].
2 (all x all y exists z x * z = y) # 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)).  [assumption].
5 x * (y * ((x * y) * x)) = y.  [copy(4),flip(a)].
6 x * x = (x * x) * x.  [assumption].
7 (x * x) * x = x * x.  [copy(6),flip(a)].
8 x * y != x * z | y = z.  [clausify(1)].
9 x * f1(x,y) = y.  [clausify(2)].
10 ((c1 * c1) * c1) * c1 != c1 # label(255) # answer(255).  [deny(3)].
11 (c1 * c1) * c1 != c1.  [para(7(a,1),10(a,1,1))].
12 c1 * c1 != c1.  [para(7(a,1),11(a,1))].
13 x * ((y * ((x * y) * x)) * (y * x)) = y * ((x * y) * x).  [para(5(a,1),5(a,1,2,2,1))].
14 (x * y) * ((x * (x * y)) * x) = y.  [resolve(8,a,5,a)].
15 (x * x) * y != x * x | y = x.  [para(7(a,1),8(a,2))].
16 f1(x,x * y) = y.  [resolve(8,a,9,a)].
17 x * (c1 * c1) != x * c1.  [resolve(8,b,12,a)].
18 (x * ((x * x) * x)) * (x * x) = (x * x) * x.  [resolve(8,a,13,a)].
19 (x * (x * x)) * (x * x) = (x * x) * x.  [para(7(a,1),18(a,1,1,2))].
20 (x * (x * x)) * (x * x) = x * x.  [para(7(a,1),19(a,2))].
21 x * ((y * x) * y) != y * z | (x * ((y * x) * y)) * (x * y) = z.  [para(13(a,1),8(a,1))].
22 x * (y * (c1 * c1)) != x * (y * c1).  [resolve(8,b,17,a)].
23 x * ((c1 * c1) * (c1 * c1)) != x * (c1 * c1) # answer(255).  [para(7(a,1),22(a,2,2))].
24 f1(x,y) = y * ((x * y) * x).  [para(5(a,1),16(a,1,2))].
25 f1(x * x,x * x) = x.  [para(7(a,1),16(a,1,2))].
26 (x * x) * (((x * x) * (x * x)) * (x * x)) = x.  [para(24(a,1),25(a,1))].
27 (x * x) * ((x * x) * (x * x)) = x.  [para(7(a,1),26(a,1,2))].
28 (x * x) * (((x * (x * x)) * ((x * (x * x)) * (x * x))) * (x * (x * x))) = x * x.  [para(20(a,1),14(a,1,1))].
29 (x * x) * (((x * (x * x)) * (x * x)) * (x * (x * x))) = x * x.  [para(20(a,1),28(a,1,2,1,2))].
30 (x * x) * ((x * x) * (x * (x * x))) = x * x.  [para(20(a,1),29(a,1,2,1))].
31 (c1 * c1) * (((c1 * c1) * (c1 * c1)) * (c1 * c1)) != (c1 * c1) * (((c1 * c1) * (((c1 * c1) * (c1 * c1)) * (c1 * c1))) * (c1 * c1)).  [resolve(21,b,23,a)].
32 (c1 * c1) * ((c1 * c1) * (c1 * c1)) != (c1 * c1) * (((c1 * c1) * (((c1 * c1) * (c1 * c1)) * (c1 * c1))) * (c1 * c1)).  [para(7(a,1),31(a,1,2))].
33 c1 != (c1 * c1) * (((c1 * c1) * (((c1 * c1) * (c1 * c1)) * (c1 * c1))) * (c1 * c1)).  [para(27(a,1),32(a,1))].
34 c1 != (c1 * c1) * (((c1 * c1) * ((c1 * c1) * (c1 * c1))) * (c1 * c1)).  [para(7(a,1),33(a,2,2,1,2))].
35 c1 != (c1 * c1) * (c1 * (c1 * c1)).  [para(27(a,1),34(a,2,2,1))].
36 (c1 * c1) * (c1 * (c1 * c1)) != c1.  [copy(35),flip(a)].
37 (c1 * c1) * ((c1 * c1) * (c1 * (c1 * c1))) != c1 * c1.  [resolve(15,b,36,a)].
38 c1 * c1 != c1 * c1.  [para(30(a,1),37(a,1))].
39 $F.  [copy(38),xx(a)].

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