% -------- Comments from original proof --------
% Proof 1 at 0.68 (+ 0.00) seconds..
% Length of proof: 27 (24 initial or hint matcher)
% Level of proof: 15
% Maximum clause weight: 37.000
% Given clauses in run: 49
% Given clauses in proof: 23 (23 initial or hint matcher)

1 x * y = x # label(non_clause) # label(goal).  [goal].
2 x * (y * ((z * x) * y)) = x # label("650").  [assumption].
3 c1 * c2 != c1.  [deny(1)].
4 (x * ((y * z) * x)) * (u * (z * u)) = x * ((y * z) * x).  [para(2(a,1),2(a,1,2,2,1))].
5 x * ((y * ((z * (u * x)) * y)) * (u * x)) = x.  [para(2(a,1),2(a,1,2,2))].
6 ((x * y) * z) * ((u * (y * u)) * (z * ((x * y) * z))) = (x * y) * z.  [para(2(a,1),5(a,1,2,1,2,1))].
7 (x * (y * x)) * (z * ((u * ((w * y) * u)) * z)) = x * (y * x).  [para(4(a,1),2(a,1,2,2,1))].
8 (x * y) * ((z * ((u * ((w * x) * u)) * z)) * (y * (x * y))) = x * y.  [para(4(a,1),5(a,1,2,1,2,1))].
9 x * (((y * (z * y)) * (x * ((u * z) * x))) * ((u * z) * x)) = x.  [para(4(a,1),5(a,1,2,1,2))].
10 (x * (y * x)) * ((z * (y * z)) * (u * ((w * y) * u))) = x * (y * x).  [para(4(a,1),7(a,1,2,2))].
11 ((x * (y * x)) * (z * ((u * y) * z))) * (w * (((u * y) * z) * w)) = (x * (y * x)) * (z * ((u * y) * z)).  [para(6(a,1),2(a,1,2,2,1))].
12 (x * y) * (((z * (x * z)) * (u * ((w * x) * u))) * (y * (x * y))) = x * y.  [para(4(a,1),8(a,1,2,1,2))].
13 ((x * (y * x)) * (y * ((z * y) * y))) * (y * ((z * y) * y)) = (x * (y * x)) * (y * ((z * y) * y)).  [para(4(a,1),11(a,1,2))].
14 (x * ((y * x) * x)) * ((x * ((y * x) * x)) * ((z * (x * z)) * (x * ((y * x) * x)))) = x * ((y * x) * x).  [para(13(a,1),2(a,1,2,2))].
15 (x * ((y * y) * x)) * (y * ((y * y) * y)) = x * ((y * y) * x).  [para(14(a,1),10(a,1,2))].
16 ((x * x) * y) * ((x * ((x * x) * x)) * (y * ((x * x) * y))) = (x * x) * y.  [para(14(a,1),12(a,1,2,1))].
17 ((x * x) * x) * (x * ((x * x) * x)) = (x * x) * x.  [para(15(a,1),16(a,1,2))].
18 x * ((((y * y) * y) * (x * ((z * y) * x))) * ((z * y) * x)) = x.  [para(17(a,1),9(a,1,2,1,1))].
19 ((x * y) * z) * (((y * y) * y) * (z * ((x * y) * z))) = (x * y) * z.  [para(17(a,1),6(a,1,2,1))].
20 x * (((x * x) * x) * ((x * x) * x)) = x.  [para(17(a,1),18(a,1,2,1))].
21 ((x * x) * x) * ((x * x) * x) = (x * x) * x.  [para(17(a,1),19(a,1,2))].
22 x * ((x * x) * x) = x.  [para(21(a,1),20(a,1,2))].
23 x * x = x.  [para(22(a,1),2(a,1,2))].
24 x * (x * x) = x.  [para(23(a,1),22(a,1,2,1))].
25 x * (y * x) = x.  [para(24(a,1),2(a,1,2))].
26 x * y = x.  [para(25(a,1),2(a,1,2))].
27 $F.  [resolve(26,a,3,a)].

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