============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.16 (+ 0.01) seconds.
% Length of proof is 42.
% Level of proof is 21.
% Maximum clause weight is 33.000.
% Given clauses 67.


1 x = y # label(non_clause) # label(goal).  [goal].
2 x = (y * y) * (x * (x * y)).  [assumption].
3 (x * x) * (y * (y * x)) = y.  [copy(2),flip(a)].
4 x * x = 0 | x * x = 1.  [assumption].
5 c2 != c1.  [deny(1)].
6 ((x * (x * y)) * (x * (x * y))) * ((y * y) * x) = y * y.  [para(3(a,1),3(a,1,2,2))].
8 x * x = 0 | 1 * (y * (y * x)) = y.  [para(4(b,1),3(a,1,1))].
12 (((x * (x * y)) * ((x * (x * y)) * y)) * ((x * (x * y)) * ((x * (x * y)) * y))) * x = y * y.  [para(3(a,1),6(a,1,2))].
15 (x * (x * y)) * (x * (x * y)) = 0 | 1 * ((y * y) * x) = y * y.  [para(4(b,1),6(a,1,1))].
20 1 * (x * (x * y)) = x | 0 * (z * (z * y)) = z.  [para(8(a,1),3(a,1,1))].
25 x * x = 0 | 1 * (x * 1) = x.  [para(4(b,1),8(b,1,2,2)),merge(b)].
38 1 * (x * 1) = x | 0 * (y * (y * x)) = y.  [para(25(a,1),3(a,1,1))].
41 1 * 1 = 0 | (1 * 1) * 1 = 1.  [para(25(b,1),3(a,1,2))].
56 1 * 1 = 0 | 1 * ((1 * 1) * 1) = 1 * 1.  [para(41(b,1),8(b,1,2,2)),merge(b)].
130 1 * (x * 1) = x | 0 * (x * 0) = x.  [para(25(a,1),38(b,1,2,2)),merge(b)].
355 1 * 1 = 0 | 1 * (1 * 1) = 1 * 1.  [para(4(b,1),56(b,1,2,1)),merge(b)].
584 1 * (x * (x * y)) = x | 1 * (z * (z * y)) = z | 0 * (y * 0) = y.  [para(8(a,1),20(b,1,2,2))].
671 1 * (x * (x * y)) = x | 0 * (y * 0) = y.  [factor(584,a,b)].
783 0 * (1 * 0) = 1 | 1 * 1 = 1.  [para(130(a,1),671(a,1,2)),merge(c)].
1273 1 * x = y * y | 0 * x = y * y.  [para(15(a,1),12(a,1,1)),rewrite([3(5)])].
1379 0 * (x * 1) = y * y | x * x = 0 | y * y = x.  [para(1273(a,1),25(b,1))].
1585 0 * (0 * 1) = 0 * 0 | 0 * 0 = 0.  [factor(1379,b,c)].
1593 0 * 0 = 0 | 0 * (0 * 1) = 1.  [para(4(b,1),1585(a,2)),merge(c)].
1630 0 * 0 = 0 | (1 * 1) * 1 = 0.  [para(1593(b,1),3(a,1,2))].
1635 0 * 0 = 0 | 1 * 1 = 0.  [para(1593(b,1),8(b,1,2)),merge(c)].
1696 0 * 0 = 0 | x * x = 0 | 0 * 1 = x * x.  [para(1635(b,1),1273(a,1)),flip(b)].
1698 0 * 0 = 0 | 0 * 1 = 0 * 0.  [factor(1696,a,b)].
1891 0 * 0 = 0 | 0 * 1 = 0.  [para(1635(b,1),1630(b,1,1)),merge(b)].
1953 0 * 0 = 0.  [para(1698(b,1),1891(b,1)),merge(b),merge(c)].
2057 0 * (x * (x * 0)) = x.  [para(1953(a,1),3(a,1,1))].
2061 1 * x = 0 | 0 * x = 0.  [para(1953(a,1),1273(a,2)),rewrite([1953(9)])].
2071 x * x = 0 | 0 * (1 * (x * x)) = 1.  [para(1273(a,1),2057(a,1,2,2)),rewrite([1953(3)]),flip(a)].
2116 0 * (1 * 1) = 0 | 1 * 1 = 0.  [para(2061(a,1),355(b,1)),flip(c),merge(c)].
2163 0 * (1 * 0) = 0 | 1 = 0.  [para(2061(a,1),2057(a,1,2)),rewrite([1953(10)]),flip(b)].
2540 x * x = 0 | 0 * (1 * 1) = 1.  [para(4(b,1),2071(b,1,2,2)),merge(b)].
2900 x * x = 0 | 1 = 0 | 1 * 1 = 0.  [para(2540(b,1),2116(a,1))].
2922 1 * 1 = 0 | 1 = 0.  [factor(2900,a,c)].
2949 1 = 0 | 0 * (1 * 0) = 1.  [para(2922(a,1),783(b,1)),flip(c),merge(c)].
3237 1 = 0.  [para(2949(b,1),2163(a,1)),merge(b),merge(c)].
3619 0 * x = 0.  [back_rewrite(2061),rewrite([3237(1)]),merge(b)].
3651 0 = x.  [back_rewrite(130),rewrite([3237(1),3237(2),3619(4),3619(6)]),merge(b)].
3652 $F.  [para(3651(a,2),5(a,1)),flip(a),unit_del(a(flip),3651)].

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