% --------------------------------------------------------------------------
% Gagola:  Prove the 17 lemmas on Lemma List 1.
% --------------------------------------------------------------------------

assign(order, kbo).
set(lex_order_vars).

set(para_from_small).
set(para_into_vars).

clear(back_demod).
set(restrict_denials).

assign(max_weight, 5  ).

formulas(assumptions).

% two-sided identity
1 * x = x.
x * 1 = x.

% inverses (and IP and AAIP)
x * x' = 1.
x' * x = 1.
x' * (x * y) = y.
(y * x) * x' = y.
(x * y)' = y' * x'.

% alternative
(x * x) * y = x * (x * y).
(y * x) * x = y * (x * x).

% flexible
x * (y * x) = (x * y) * x.

% Moufang
((x * y) * x) * z = x * (y * (x * z)).
((z * x) * y) * x = z * (x * (y * x)).
(x * y) * (z * x) = x * ((y * z) * x).
(x * y) * (z * x) = (x * (y * z)) * x.

% R(u,x,y) = u R(x) R(y) R(xy)^{-1}
R(u,x,y) = ((u * x) * y) * (x * y)'.

% C in commutant
C * x = x * C.

% associator
(x * y) * z = (x * (y * z)) * a(x,y,z) # label("associator").

end_of_list.

formulas(goals).

% C^3 is nuclear
a(C * (C * C),x,y) = 1 # label("Lemma 1-1").

a(x,y,C * (C * C)) = 1 # label("Lemma 1-2").
a(x,C * (C * C),y) = 1 # label("Lemma 1-3").

% C associates with cubes
a(C,x * (x * x),y) = 1 # label("Lemma 1-4").
a(C,x,y * (y * y)) = 1 # label("Lemma 1-5").
a(x,C,y * (y * y)) = 1 # label("Lemma 1-6").
a(x * (x * x),C,y) = 1 # label("Lemma 1-7").
a(x * (x * x),y,C) = 1 # label("Lemma 1-8").
a(x,y * (y * y),C) = 1 # label("Lemma 1-9").

% associators with C in an argument cube to zero
a(C,x,y) * (a(C,x,y) * a(C,x,y)) = 1 # label("Lemma 1-10").
a(x,y,C) * (a(x,y,C) * a(x,y,C)) = 1 # label("Lemma 1-11").
a(x,C,y) * (a(x,C,y) * a(x,C,y)) = 1 # label("Lemma 1-12").

% CR(x,y)^3 = C, xR(C,y)^3 = x, xR(y,C)^3 = x
R(R(R(C,x,y),x,y),x,y) = C # label("Lemma 1-13").
R(R(R(x,C,y),C,y),C,y) = x # label("Lemma 1-14").
R(R(R(x,y,C),y,C),y,C) = x # label("Lemma 1-15").

% R(C,y) and R(y,C) are automorphisms
R(u * v,C,y) = R(u,C,y) * R(v,C,y) # label("Lemma 1-16").
R(u * v,y,C) = R(u,y,C) * R(v,y,C) # label("Lemma 1-17").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

a(C,x,y * (y * y)) = 1.
x * 1 = x.
x' * x = 1.
x' * (x * y) = y.
(x * y) * y' = x.
(x * y)' = y' * x'.
(x * x) * y = x * (x * y).
(x * y) * y = x * (y * y).
x * (y * x) = (x * y) * x.
(x * y) * x = x * (y * x).
((x * y) * x) * z = x * (y * (x * z)).
((x * y) * z) * y = x * (y * (z * y)).
(x * y) * (z * x) = x * ((y * z) * x).
C * x = x * C.
(x * y) * z = (x * (y * z)) * a(x,y,z).
(x * (y * z)) * a(x,y,z) = (x * y) * z.
a(C,c9,c10 * (c10 * c10)) != 1.
x'' * 1 = x.
(x' * y') * (y * x) = 1.
(x' * y') * ((y * x) * z) = z.
(x * (y * x)) * z = x * (y * (x * z)).
(x * (y * y)) * y = x * (y * (y * y)).
(C * x) * C' = x.
(x * C) * (y * C) = C * ((x * y) * C).
(C * x) * (C * y) = C * ((x * y) * C).
(C * x) * (y * C) = C * (C * (x * y)).
x = x''.
x'' = x.
x * (x' * y) = y.
(x * y') * y = x.
x * C' = C' * x.
C' * x = x * C'.
(x * (x * y')) * y = x * x.
C * (x * C') = x.
C * (x * (C' * (y * C'))) = (x * C') * y.
((x * y) * C') * y = x * (y * (y * C')).
((x' * y') * z') * (z * (y * x)) = 1.
((x' * y') * z') * ((z * (y * x)) * u) = u.
(x * (y * (x * z))) * z' = x * (y * x).
(x * C) * (y * C) = C * (C * (x * y)).
(C * x) * (C * y) = C * (C * (x * y)).
x * (y * C) = C * (C * ((x * C') * y)).
C * (C * ((x * C') * y)) = x * (y * C).
(x * C) * (y * y) = C * (C * (x * (y * (y * C')))).
C * (C * (x * (y * (y * C')))) = (x * C) * (y * y).
(C * x) * y = C * (C * (x * (C' * y))).
C * (C * (x * (C' * y))) = (C * x) * y.
C * (C * (x * (y * (y * C')))) = (x * y) * (y * C).
C * (x * (C' * (y * (z * y)))) = (x * C') * (y * (z * (y * C))).
(x * C') * (y * (z * (y * C))) = C * (x * (C' * (y * (z * y)))).
((x' * y') * z') * ((z * y) * x) = a(z,y,x).
(x * y) * (y * C) = (x * C) * (y * y).
(x * C) * (y * y) = (x * y) * (y * C).
((x * C) * (y * y)) * y = x * (y * ((y * C) * y)).
x * (y * ((y * C) * y)) = (x * C) * (y * (y * y)).
(x * C) * (y * (y * y)) = x * (y * ((y * C) * y)).
(x * C) * (y * (y * y)) = x * (y * (y * (C * y))).
(x * C) * (y * (y * y)) = x * (y * (y * (y * C))).
x * (y * (y * y)) = (x * C') * (y * (y * (y * C))).
(x * C') * (y * (y * (y * C))) = x * (y * (y * y)).
C * (x * (C' * (y * (y * y)))) = x * (y * (y * y)).
C * (x * (y * (y * y))) = (C * x) * (y * (y * y)).
(C * x) * (y * (y * y)) = C * (x * (y * (y * y))).
(((x * (x * x))' * y') * C') * ((C * y) * (x * (x * x))) = 1.
1 = a(C,x,y * (y * y)).
a(x,y * (y * y),C) = 1.
a(c17,c18 * (c18 * c18),C) != 1.
x' * ((x * y) * (z * x)) = (y * z) * x.
(x * (y * z))' * ((x * y) * z) = a(x,y,z).
((x * y) * z) * a(x,y,z)' = x * (y * z).
(x' * y)' = y' * x.
(x * y) * z = (x * z') * (z * (y * z)).
(x * y') * (y * (z * y)) = (x * z) * y.
(x * y) * z = x * ((y * (z * x')) * x).
x * ((y * (z * x')) * x) = (x * y) * z.
(x * (y' * z))' = (z' * y) * x'.
x' * ((x * (y * x)) * z) = y * (x * z).
x' * ((x * y) * z) = (y * (z * x')) * x.
(x * (y * z')) * z = z' * ((z * x) * y).
(x * y') * (y * z) = (x * (z * y')) * y.
(x * (y * z')) * z = (x * z') * (z * y).
x' * ((x * y) * z) = (y * x') * (x * z).
(x * y') * (y * z) = y' * ((y * x) * z).
x' * (((x * y) * z) * u) = (y * (z * x')) * (x * u).
(x * (y * z')) * (z * u) = z' * (((z * x) * y) * u).
((x' * y) * z') * ((z * y') * x) = a(z,y',x).
(x' * (y * z)') * (y * (z * x)) = a(y,z,x)'.
((x' * y') * (z * u)') * (z * (u * (y * x))) = a(z,u,y * x)'.
(x' * (y' * z')) * (z * (y * x)) = a(z,y,x)'.
((x' * (y * z)') * y'') * (z * x) = a(y',y * z,x).
((x' * y') * (z * x)') * (z * (x * (y * x))) = a(z * x,y,x).
((x' * y) * (z * y)') * (z * x) = a(z * y,y',x).
x' * (((x * y') * z') * (z * y)) = a(x,z,y)'.
x' * (((x * y') * (y * z')) * z) = a(x,z,y)'.
(x' * ((x * y') * z')) * (z * y) = a(z,y,x)'.
((x' * y) * (y' * z')) * (z * x) = a(z * y,y',x).
((x' * y') * (y'' * z')) * (z * x) = a(z * y',y,x).
((x' * (y' * z')) * z'') * (y * x) = a(z',z * y,x).
((x' * y') * (y * z')) * (z * x) = a(z * y',y,x).
(x' * ((x * y') * z')) * (z * y) = a(z * x',x,y).
a(x * y',y,z) = a(x,z,y)'.
a(x,y,z) = a(x * y,z,y)'.
a(x * y,z,y)' = a(x,y,z).
((x' * (y' * z')) * z) * (y * x) = a(z',z * y,x).
(x' * ((x * y') * z')) * (z * y) = a(x',x * z,y).
a(x',x * y,z) = a(y,z,x)'.
a(x,x' * y,z) = a(y,z,x')'.
a(x,x' * (y * x'),z) = a(y,x',z).
1 = a(x,C',y * (y * y)).
a(x,C',y * (y * y)) = 1.
a(x,y,z * y)' = a(x * y,z,y).
a(x * y,z,y)' = a(x,y,z * y).
a(x * y',y,z * y)' = a(x,z,y).
a(x,y,z * y) = a(x,y,z).
a(x,C',y) = a(x,C',C * y).
a(x,C',C * y) = a(x,C',y).
a(x,y * z,z)'' = a(x,y,z).
a(x,y,z) = a(x,y * z,z).
a(x,y * z,z) = a(x,y,z).
a(x,y,z * y) = a(x,z',z * y).
a(x,y',y * z) = a(x,z,y * z).
a(x,y',y * z) = a(x,z,y).
a(x,y,C) = a(x,C',y).
a(x,C',y) = a(x,y,C).
a(x,C,y * (y * y)) = 1.
a(c11,C,c12 * (c12 * c12)) != 1.
(x * y')' = y * x'.
(x * (y * z'))' = (z * y') * x'.
a(x,y,z) = a(x,y,z * y').
a(x,y,z * y') = a(x,y,z).
a(x,y,y' * z) = a(x,z,y').
a(x,y,C * y') = a(x,C,y').
a(x,C,y') = a(x,y,C).
a(x,C,(y * (y * y))') = 1.
a(x,C,(y * y'') * y'') = 1.
a(x,C,(y * y) * y'') = 1.
a(x,C,(y * y) * y) = 1.
a(C,x * (x * x),y) = 1.
(x * y) * (z * x) = (x * (y * z)) * x.
(x * (y * z)) * x = (x * y) * (z * x).
a(C,c7 * (c7 * c7),c8) != 1.
x * y' = y' * ((y * x) * y').
x' * ((x * y) * x') = y * x'.
(x * (y * (z * y))) * y' = (x * y) * z.
((x * y) * (z * x)) * u = x * ((y * z) * (x * u)).
x' * (C * x) = C.
C * ((x * C) * y) = x * (C * (y * C)).
x * (C * x') = C.
(x * y) * z = y * ((y' * x) * (y * z)).
x * ((x' * y) * (x * z)) = (y * x) * z.
x * (y * C) = C * (((x * C') * y) * C).
C * (((x * C') * y) * C) = x * (y * C).
x * (y * x') = (x * y) * x'.
(x * y) * x' = x * (y * x').
C * (x * (y * x)) = x * (y * (x * C)).
x' * (C * (x * (y * x))) = y * (x * C).
(x * (y * z)) * y' = (x * y) * (z * y').
(x * (y * (x * C))) * x' = (C * x) * y.
x * ((x' * y) * C) = (y * x) * (C * x').
(x * y) * (C * y') = y * ((y' * x) * C).
C * (x * y) = x * ((y * (C * x')) * x).
x * ((y * (C * x')) * x) = C * (x * y).
x' * (C * (x * y)) = (y * x') * (x * C).
(x * y') * (y * C) = y' * (C * (y * x)).
(C * x) * y = x * ((y * (x * C)) * x').
x * ((y * (x * C)) * x') = (C * x) * y.
x' * ((C * (x * y)) * z) = (y * (C * x')) * (x * z).
(x * (C * y')) * (y * z) = y' * ((C * (y * x)) * z).
x * ((y * (x * C)) * x') = (x * C) * y.
x * ((y * x) * (C * x')) = (x * C) * y.
(x * y) * (C * y') = y * (C * (y' * x)).
x * (x * (C * (x' * y))) = (x * C) * y.
x' * ((x * C) * y) = x * (C * (x' * y)).
(x * (y * z)) * u = z * (((z' * x) * y) * (z * u)).
x * (((x' * y) * z) * (x * u)) = (y * (z * x)) * u.
((C' * x') * y') * (C * (y * x)) = a(y,x,C).
((x' * y') * C'') * ((y * C') * x) = a(C',y,x).
C * a(x,y,C) = (y' * (x' * C)) * (x * y).
(x' * (y' * C)) * (y * x) = C * a(y,x,C).
(x * (y' * C)) * (y * z) = y' * ((C * (y * x)) * z).
x' * ((C * (x * y')) * y) = C * a(x,y,C).
x' * (y' * ((y * C) * x)) = C * a(x,y,C).
x' * (y * (C * (y' * x))) = C * a(x,y,C).
((x' * y') * C) * ((y * C') * x) = a(C',y,x).
C * a(C',x,y) = (y' * x') * (C * (((x * C') * y) * C)).
(x' * y') * (C * (((y * C') * x) * C)) = C * a(C',y,x).
(x' * y') * (y * (x * C)) = C * a(C',y,x).
C * a(C',x,y) = x' * ((x * y') * (y * C)).
x' * ((x * y') * (y * C)) = C * a(C',x,y).
x' * (y' * (C * (y * x))) = C * a(C',x,y).
x' * (y * (C * (y' * x))) = C * a(C',x,y').
C * a(C',x,y') = C * a(x,y,C).
C' * (C * a(x,y,C)) = a(C',x,y').
a(C',x,y') = a(x,y,C).
a(C',x,y) = a(x,y',C).
a(x,y,z)' = a(x * y,z,y).
a(x * y,z,y) = a(x,y,z)'.
a(x,y,z * x) = a(z',z * x,y)'.
a(x,y,z * x) = a(x,y,z)''.
a(x,y,z * x) = a(x,y,z).
a(x * y,z,y) = a(x * y,z,x').
a(x * y,z,x') = a(x * y,z,y).
a(x,y,z) = a(x,y,z * x').
a(x,y,z * x') = a(x,y,z).
a(C,x * C',y) = a(x,y,C')'.
a(x * y,z,x') = a(x,y,z)'.
a(x,x' * y,z) = a(y * x,x',z).
a(x * y,y',z) = a(y,y' * x,z).
a(x,y * x',z) = a(x * y,x',z).
a(x * y,x',z) = a(x,y * x',z).
a(C',x,y') = a(x,C',y).
a(x,y * x',C) = a(x,C',y).
a(x * y,x',C) = a(x,y,C')'.
a(C',x,y') = a(x,y * x',C).
a(x,y * x',C) = a(C',x,y').
a(x,C,y' * z') = a(x,z * y,C).
a(x,y * z,C) = a(x,C,z' * y').
a(x,C,y) = a(x,y',C).
a(x,y',C) = a(x,C,y).
a(C',x,y) = a(x,C,y).
a(x * y,C,y) = a(y,y' * x,C).
a(x * y,x',C) = a(C',x,y').
a(C',x,y') = a(x,y,C')'.
a(x,y,C')' = a(C',x,y').
a(x,y,C')' = a(x,y,C).
a(x,y,C')' = a(x,C,y').
a(C,x * C',y) = a(x,y,C).
a(C,C' * x,y) = a(x,C,y').
a(x,C',y) = a(C,x * C',y).
a(C,x * C',y) = a(x,C',y).
a(C,x,y) = a(x * C,C',y).
a(x * C,C',y) = a(C,x,y).
a(C,x,y) = a(C,C' * x,y).
a(C,C' * x,y) = a(C,x,y).
a(C,x,y) = a(x,C,y').
a(x,C,y' * x) = a(C,x,y).
a(x * y,C,y) = a(y,C,x' * y'').
a(x * y,C,y) = a(y,C,x' * y).
a(x * y,C,y) = a(C,y,x).
a(x * (x * x),y,C) = 1.
a(c15 * (c15 * c15),c16,C) != 1.
a(C,x,y) = a(x,y,C).
1 = a(x * (x * x),y,C).
a(x * (x * x),C,y) = 1.
a(c13 * (c13 * c13),C,c14) != 1.
a(C,x,y') = a(x,C,y).
1 = a(x * (x * x),C,y).
a(x,C * (C * C),y) = 1.
a(c5,C * (C * C),c6) != 1.
((x * C) * C) * y = C * (x * (C * y)).
(x * (y' * z')) * (z * y) = x.
(x * (y' * (z * (u * z))')) * (z * (u * (z * y))) = x.
(x * (C * (C * C))) * y = C * ((x * C) * (C * y)).
C * ((x * C) * y) = x * (C * (C * y)).
(x * (C * (C * C))) * y = x * (C * (C * (C * y))).
((x' * (y' * z')) * u') * ((u * (z * y)) * x) = a(u,z * y,x).
(x * (y' * ((z * u)' * u'))) * (u * (z * (u * y))) = x.
(x * (y' * ((z' * u') * z'))) * (z * (u * (z * y))) = x.
(x * (y' * (z' * (u' * z')))) * (z * (u * (z * y))) = x.
x' * ((x * (y' * (z' * (u' * z')))) * (z * (u * (z * y)))) = 1.
((x' * (y' * (z' * y'))) * u') * (u * (y * (z * (y * x)))) = 1.
((x' * (C' * (C' * C'))) * y') * ((y * (C * (C * C))) * x) = 1.
((x' * ((C' * C') * C')) * y') * ((y * (C * (C * C))) * x) = 1.
((x' * ((C * C)' * C')) * y') * ((y * (C * (C * C))) * x) = 1.
1 = a(x,C * (C * C),y).
a(C * (C * C),x,y) = 1.
1 * x = x.
x * x' = 1.
a(C * (C * C),c1,c2) != 1.
1 = 1'.
1' = 1.
C * (x * C) = x * (C * C).
((x * C) * y) * C = x * (C * (C * y)).
((x * C) * y) * C = x * (y * (C * C)).
C * ((x * C) * y) = x * (y * (C * C)).
x * (y * (C * C)) = x * (C * (C * y)).
x * (C * (C * y)) = x * (y * (C * C)).
x * (C * ((x' * C) * y)) = y * (C * C).
x * (C * (x' * (C * C))) = C * (C * C).
a(x,y,z * (u * (z * x))) = a(x,y,z * (u * z)).
a(x,y,z) = a(x,y * z,y').
a(x,y * z,y') = a(x,y,z).
a(x * y,x,z) = a(x,y,x * z)'.
a(x,y,x * z)' = a(x * y,x,z).
a(x,C * (x' * (C * C)),x * y)' = a(C * (C * C),x,y).
1 = a(x,y,(C * (C * C))').
a(x,y,(C * (C * C))') = 1.
a(x,y,(C * C)' * C') = 1.
a(x,y,(C' * C') * C') = 1.
a(x,y,C' * (C' * C')) = 1.
a(x,y,C' * (C' * (C' * x))) = 1.
a(x,y,(C' * (C' * x)) * C') = 1.
a(x,y,((C' * x) * C') * C') = 1.
a(x,y,((x * C') * C') * C') = 1.
a(x',y,((C * x)' * C') * C') = 1.
a(x',y,(C * (C * x))' * C') = 1.
a(x',y,(C * (C * (C * x)))') = 1.
1 = a(x',C * (C * (C * x)),y).
a(x',C * (C * (C * x)),y) = 1.
a(x',C * (x * (C * C)),y) = 1.
a(x,C * (x' * (C * C)),y) = 1.
1' = a(C * (C * C),x,y).
a(C * (C * C),x,y) = 1'.
a(x,y,C * (C * C)) = 1.
a(c3,c4,C * (C * C)) != 1.
x' * (((x * y) * x) * z) = y * (x * z).
C' * (x * C) = x.
(C' * (C' * x)) * y = C' * (x * (C' * y)).
C * ((C * x) * y) = x * (C * (y * C)).
C' * (x * (C * (C * y))) = (x * C) * y.
x' * ((y * x) * z) = (x' * y) * (x * z).
(x' * y) * (x * z) = x' * ((y * x) * z).
C * (C * ((C' * x) * (C' * y))) = x * y.
(C' * x) * (C * y) = C' * ((C * x) * y).
(C * (C * ((C' * x') * (C' * y')))) * (y * x) = 1.
((C * ((C' * x') * (C' * y'))) * C) * (y * x) = 1.
C' * ((C * ((C' * x') * (C' * y'))) * (C * (C * (y * x)))) = 1.
(C' * ((C' * x') * (C' * y'))) * (C * (C * (C * (y * x)))) = 1.
(C' * ((C' * x') * (C' * y'))) * (C * ((C * (y * x)) * C)) = 1.
(C' * ((C' * x') * (C' * y'))) * ((y * x) * (C * (C * C))) = 1.
((C' * (C' * (C' * x'))) * y') * ((y * x) * (C * (C * C))) = 1.
((((C' * C') * C') * x') * y') * ((y * x) * (C * (C * C))) = 1.
((((C * C)' * C') * x') * y') * ((y * x) * (C * (C * C))) = 1.
(((C * (C * C))' * x') * y') * ((y * x) * (C * (C * C))) = 1.
1 = a(x,y,C * (C * C)).
R(R(R(x,C,y),C,y),C,y) = x.
R(x,y,z) = ((x * y) * z) * (y * z)'.
R(R(R(c27,C,c28),C,c28),C,c28) != c27.
(x * (y * z)) * (z' * y') = x.
(x * (y * (z * y))) * z = (x * y) * (z * (y * z)).
R(x,y,z) = ((x * y) * z) * (z' * y').
x * y = y * ((y' * x) * y).
x * ((x' * y) * x) = y * x.
x * (x * y') = (x * y') * (y * (x * y')).
(x * y') * (y * (x * y')) = x * (x * y').
(((x * y) * y') * (z * u)) * (u' * z') = x.
C * ((C * x) * y) = x * (C * (C * y)).
(x * (C * (C * y))) * (C * z) = C * (C * (((C * x) * y) * z)).
x' * ((C * x) * y) = (C * x') * (x * y).
(C * x') * (x * y) = x' * ((C * x) * y).
(x * (y * z)) * z' = (x * z) * (z' * y).
x * ((y * x) * (C * x')) = (C * x) * y.
(x * (y * (C * z))) * (z * C)' = (x * (z * C)) * ((z * C)' * y).
(x * ((y * z) * (u * z'))) * z = (x * z') * (z * (y * (z * u))).
x * (x * (C * (x' * y))) = (C * x) * y.
x' * ((C * x) * y) = x * (C * (x' * y)).
(C * x') * (x * y) = x * (C * (x' * y)).
(x * (C * (x' * y))) * (x * C)' = (x' * (x * C)) * (y * (x * C)').
(((x * y) * (z * y')) * y) * (z' * y') = x.
(x * (y * z)) * (z * y') = (x * y) * ((z * y') * (y * (z * y'))).
(x * y) * ((z * y') * (y * (z * y'))) = (x * (y * z)) * (z * y').
(x * (y * (C * z))) * (C' * z') = (x * (z * C)) * ((z * C)' * y).
(x * y) * (z * (z * y')) = (x * (y * z)) * (z * y').
(x * (y * z)) * (z * y') = (x * y) * (z * (z * y')).
(x * (y * (C * z))) * (C' * z') = (x * (z * C)) * ((C' * z') * y).
(x * (C * (x' * y))) * (C' * x') = (x' * (x * C)) * (y * (x * C)').
(x * (C * (C * y))) * (C' * y') = (x * (y * C)) * (C * (C' * y')).
(x * (C * (C * y))) * (C' * y') = (x * (y * C)) * y'.
(x * (C * (C * y))) * (C' * y') = (x * y) * (C * y').
(((x * (C * (C * y))) * (C' * y')) * y) * (C' * y') = x.
(((x * (C * (C * y))) * (z * (z' * (C' * y')))) * y) * (C' * y') = x.
(x * (C * (x' * y))) * (C' * x') = C * (y * (x * C)').
(x * (C * (x' * y))) * (C' * x') = C * (y * (C' * x')).
((C * (C * (((C * x) * y) * (C' * (C' * y'))))) * y) * (C' * y') = x.
((C * (C * (((C * x) * (y * C')) * (C' * y')))) * y) * (C' * y') = x.
((C * ((x * (C * (x' * ((C * y) * (x * C'))))) * (C' * x'))) * x) * (C' * x') = y.
((C * (((C * x') * (x * ((C * y) * (x * C')))) * (C' * x'))) * x) * (C' * x') = y.
((C * (((C * (((C * x) * y) * (C' * y'))) * y) * (C' * y'))) * y) * (C' * y') = x.
((C * (((C * (((C * x) * y) * (C' * y'))) * y) * (C' * y'))) * y) * (y' * C') = x.
((C * (((C * (((C * x) * y) * (C' * y'))) * y) * (y' * C'))) * y) * (y' * C') = x.
((C * (((C * (((C * x) * y) * (y' * C'))) * y) * (y' * C'))) * y) * (y' * C') = x.
(((((C * (((C * x) * y) * (y' * C'))) * y) * (y' * C')) * C) * y) * (y' * C') = x.
R(((C * (((C * x) * y) * (y' * C'))) * y) * (y' * C'),C,y) = x.
R((((((C * x) * y) * (y' * C')) * C) * y) * (y' * C'),C,y) = x.
R(R(((C * x) * y) * (y' * C'),C,y),C,y) = x.
R(R(((x * C) * y) * (y' * C'),C,y),C,y) = x.
R(R(R(x,y,C),y,C),y,C) = x.
R(R(R(c29,c30,C),c30,C),c30,C) != c29.
x' * ((x * y) * x) = y * x.
(x * y) * ((y' * x') * z) = z.
((x * y) * x) * (x' * z) = x * (y * z).
(x * (x * y')) * z = (x * y') * (y * ((x * y') * z)).
(x * y') * (y * ((x * y') * z)) = (x * (x * y')) * z.
(x * y') * ((y * x') * z) = z.
(C * x) * ((C' * x') * y) = y.
(x * y) * ((y' * x') * ((C * z) * ((C' * z') * u))) = u.
(x * (y * x)) * (x' * z) = x * (y * z).
(x * (x * C')) * y = x * (C' * (x * y)).
C * (x * y) = (x * C') * (C * (C * y)).
(x * C') * (C * (C * y)) = C * (x * y).
(x * C) * y = C * (C * (x * (y * C'))).
C * (C * (x * (y * C'))) = (x * C) * y.
R(x,y,C) = (C * (x * y)) * (C' * y').
(C * (x * y)) * (C' * y') = R(x,y,C).
x * ((x' * y) * z) = (y * x) * (x' * z).
(x * y) * (y' * z) = y * ((y' * x) * z).
(x * C) * (C' * y) = C * ((x * C') * y).
(x * y) * (x' * z) = x * ((y * x') * z).
(x * C') * (C * y) = C * (x * (y * C')).
(x * (y * z)) * z' = z * ((z' * x) * y).
x * (C * (x' * (y * x))) = (C * y) * x.
x * (C * (y * x)) = (C * (x * y)) * x.
(C * (x * y)) * x = x * (C * (y * x)).
(x * (C * (y * x))) * x' = C * (x * y).
C * (x * y) = x * ((C * (y * x)) * x').
x * ((C * (y * x)) * x') = C * (x * y).
x * (x * ((x' * C) * y)) = C * (x * y).
x * (x * ((C * x') * y)) = C * (x * y).
x' * (C * (x * y)) = x * ((C * x') * y).
(x * C') * (C * ((x * C') * y)) = x * (C' * (x * y)).
(x * C') * (C * y) = x * (C' * (x * ((C * x') * y))).
x * (C' * (x * ((C * x') * y))) = (x * C') * (C * y).
x * (C' * (x * ((C * x') * y))) = C * (x * (y * C')).
C * (C * (x * (((C' * x') * ((C * y) * ((C' * y') * z))) * C'))) = z.
C * (x * (C' * (x * ((C * x') * ((C' * x') * ((C * y) * ((C' * y') * z))))))) = z.
C * (x * (C' * (x' * (C * (x * ((C' * x') * ((C * y) * ((C' * y') * z)))))))) = z.
C * (x * (C' * (x' * (C * ((x * C') * (x' * ((C * y) * ((C' * y') * z)))))))) = z.
C * (x * (C' * (x' * ((x * C) * (C' * (x' * ((C * y) * ((C' * y') * z)))))))) = z.
C * (x * (C' * ((C * x') * (x * (C' * (x' * ((C * y) * ((C' * y') * z)))))))) = z.
C * (x * (C' * ((C * x') * (x * (C' * ((C * x') * (x * ((C' * x') * y)))))))) = y.
C * (x * ((x' * C') * (C * (x * (C' * ((C * x') * (x * ((C' * x') * y)))))))) = y.
C * ((C' * ((C * (x * (C' * ((C * x') * (x * ((C' * x') * y)))))) * x)) * x') = y.
C * ((C' * ((C * (x * ((x' * C') * (C * (x * ((C' * x') * y)))))) * x)) * x') = y.
C * ((C' * ((C * ((C' * ((C * (x * ((C' * x') * y))) * x)) * x')) * x)) * x') = y.
C * ((C' * ((C * ((C' * ((C * (x * ((x' * C') * y))) * x)) * x')) * x)) * x') = y.
C * ((C' * ((C * ((C' * ((C * ((C' * (x * y)) * y')) * y)) * y')) * y)) * y') = x.
C * ((C' * ((C * ((((C * ((C' * (x * y)) * y')) * y) * C') * y')) * y)) * y') = x.
C * ((C' * (((C * ((C * ((C' * (x * y)) * y')) * y)) * (C' * y')) * y)) * y') = x.
C * ((C' * (((C * ((C * (((x * y) * C') * y')) * y)) * (C' * y')) * y)) * y') = x.
C * ((C' * (((C * (((C * (x * y)) * (C' * y')) * y)) * (C' * y')) * y)) * y') = x.
((((C * (((C * (x * y)) * (C' * y')) * y)) * (C' * y')) * y) * C) * (C' * y') = x.
R((C * (((C * (x * y)) * (C' * y')) * y)) * (C' * y'),y,C) = x.
R(R((C * (x * y)) * (C' * y'),y,C),y,C) = x.
a(C,x,y) * (a(C,x,y) * a(C,x,y)) = 1.
a(C,c19,c20) * (a(C,c19,c20) * a(C,c19,c20)) != 1.
((x * (y * y)) * z) * y = (x * y) * (y * (z * y)).
x * (y * z') = z' * (((z * x) * y) * z').
x' * (((x * y) * z) * x') = y * (z * x').
(((x * y) * z) * u) * a(x,y,z) = (x * (y * z)) * (a(x,y,z) * (u * a(x,y,z))).
(x * (y * z)) * (a(x,y,z) * (u * a(x,y,z))) = (((x * y) * z) * u) * a(x,y,z).
x * x = C * (x * (C' * x)).
C * (x * (C' * x)) = x * x.
C' * (x * C') = x * (C' * C').
x * a(x * (y' * z'),z,y) = ((x * (y' * z')) * z) * y.
C' * (C' * x) = x * (C' * C').
(x * C') * (y * (z * C)) = C * (x * ((y * C') * z)).
x' * (((x * (y' * z')) * z) * y) = a(x * (y' * z'),z,y).
x * (x * y) = C * (x * ((x * C') * y)).
C * (x * ((x * C') * y)) = x * (x * y).
x * (y * (z * x')) = ((x * y) * z) * x'.
((x * y) * z) * x' = x * (y * (z * x')).
C * (x * (C' * (C' * y))) = (x * C') * y.
((x' * y') * (z' * u')) * (((u * z) * y) * x) = a(u * z,y,x).
(x * C') * (x * (y * C)) = x * (x * y).
(x * C') * (x * y) = x * (x * (y * C')).
(x * C') * (x * y) = x * (z * (z' * (x * (y * C')))).
x * (y * (y' * (x * (z * C')))) = (x * C') * (x * z).
x * (y * (y' * (x * ((x' * z) * C')))) = (x * C') * z.
x * (y * (y' * (x * (C' * (x' * z))))) = (x * C') * z.
x * (x * (C' * (x' * y))) = (x * C') * y.
x' * ((x * C') * y) = x * (C' * (x' * y)).
x' * ((C' * x) * y) = x * (C' * (x' * y)).
(x' * C') * (x * y) = x * (C' * (x' * y)).
(x' * ((x * y') * (C * C)')) * ((C * C) * y) = a(x',C * (x * C),y).
a(x',C * (x * C),y) = a(C * C,y,x)'.
(x * (y * (z * x'))) * a(x,y,z) = (x * y) * (z * x').
x' * (((x * y') * (y * z')) * z) = a(x * (z' * y'),y,z).
a(x * (y' * z'),z,y) = a(x,y,z)'.
x * a(x,y,z)' = ((x * (y' * z')) * z) * y.
((x * (y' * z')) * z) * y = x * a(x,y,z)'.
(x' * ((x * y) * z')) * z = y * a(y,z,x)'.
(x * (C' * (x' * y'))) * y = C' * a(C',y,x)'.
a(x,C,C * y) = a(x,C,y).
a(x,C,y) = a(x,C,C' * y).
a(x,C,C' * y) = a(x,C,y).
a(x,y,z) = a(x,y * z',z).
a(x,y * z',z) = a(x,y,z).
a(x,y,C') = a(x,C,y).
a(x,C,y) = a(x,y,C').
a(x,y,C')' * a(x,C,y) = 1.
a(x,y,C')'' = a(x,C,y).
a(C',x,y) = a(x,y,C').
a(x,y,C)' = a(x,C,y).
a(x,y,C) * a(x,C,y) = 1.
a(C,x,y)' = a(x,C,y).
a(C,x * y',y) = a(C,y',x).
a(C,x',y) = a(C,y,x).
a(C,x',y)' = a(y,C,x).
a(x,C,y) = a(y',C,x).
a(x',C,y) = a(y,C,x).
a(x,C,y) = a(y,C,x').
a(x,C,y') = a(y,C,x).
a(x,C,y') = a(y,x,C').
a(C,x,y) = a(y,C,x).
a(x,y',C) = a(C,y,x).
a(C,x,y) = a(y,x',C).
a(x,y,C) * a(C,y,x) = 1.
a(C,x',y) = a(x,y,C').
a(C,x,y) * a(C,x',y) = 1.
a(C,x,y) * (C * (a(C,x',y) * C')) = 1.
a(C,x,y) * (C * (a(x,y,C') * C')) = 1.
a(x * x,y,z) * x' = ((z' * y') * x') * (x' * ((((x * x) * y) * z) * x')).
((x' * y') * z') * (z' * ((((z * z) * y) * x) * z')) = a(z * z,y,x) * z'.
(x' * ((x * y') * (C' * C'))) * ((C * C) * y) = a(x',C * (x * C),y).
(x' * (C' * (C' * (x * y')))) * ((C * C) * y) = a(x',C * (x * C),y).
(x' * (C' * (C' * (x * y')))) * (C * (C * y)) = a(x',C * (x * C),y).
C * ((C * (x' * (C' * (C' * (x * y'))))) * y) = a(x',C * (x * C),y).
C * (((x' * C') * (x * y')) * y) = a(x',C * (x * C),y).
C * ((x * (C' * (x' * y'))) * y) = a(x',C * (x * C),y).
C * ((x * (C' * (x' * y'))) * y) = a(C * C,y,x)'.
C * (C' * a(C',x,y)') = a(C * C,x,y)'.
a(C * C,x,y)' = a(C',x,y)'.
a(C',x,y)'' = a(C * C,x,y).
a(C * C,x,y) = a(C',x,y)''.
a(C * C,x,y) = a(C',x,y).
a(C * C,x,y) = a(x,y,C').
a(C,x,y) * (C * (a(C * C,x,y) * C')) = 1.
((x' * y') * z') * ((((z * y) * x) * u) * a(z,y,x)) = a(z,y,x) * (u * a(z,y,x)).
((x' * y') * z') * (z' * (((z * (z * y)) * x) * z')) = a(z * z,y,x) * z'.
((x' * y') * z') * ((z * y) * (x * z')) = a(z * z,y,x) * z'.
((x' * y') * z') * ((z * (y * (x * z'))) * a(z,y,x)) = a(z,y,x) * (z' * a(z,y,x)).
((x' * y') * z') * ((z * y) * (x * z')) = a(z,y,x) * (z' * a(z,y,x)).
a(x,y,z) * (x' * a(x,y,z)) = a(x * x,y,z) * x'.
a(C,x,y) * (C * (a(C,x,y) * (C' * a(C,x,y)))) = 1.
a(x,y,C) * (a(x,y,C) * a(x,y,C)) = 1.
a(c21,c22,C) * (a(c21,c22,C) * a(c21,c22,C)) != 1.
a(x,C,y') * (a(C,x,y) * a(C,x,y)) = 1.
a(x,C,y') * (a(C,x,y) * a(x,y,C)) = 1.
a(x,C,y') * (a(x,y,C) * a(x,y,C)) = 1.
a(x,C,y) * (a(x,C,y) * a(x,C,y)) = 1.
a(c23,C,c24) * (a(c23,C,c24) * a(c23,C,c24)) != 1.
a(x,C,y) = a(y,x,C).
a(x,C,y) * (a(y,x,C) * a(y,x,C)) = 1.
a(x,C,y) * (a(x,C,y) * a(y,x,C)) = 1.
R(R(R(C,x,y),x,y),x,y) = C.
R(R(R(C,c25,c26),c25,c26),c25,c26) != C.
(x * (y * z)) * (y * x) = x * (y * (z * (y * x))).
(x * C) * x' = C.
(x * (x' * (y * C))) * y' = C.
(x * y) * z = x * ((y * x') * (x * z)).
x * ((y * x') * (x * z)) = (x * y) * z.
(x * y') * (z * y) = (x * (y' * z)) * y.
(x * (y' * z)) * y = (x * y') * (z * y).
((x * y) * z) * (x' * u) = x * ((y * (z * x')) * u).
x * ((y * x') * C) = (x * y) * (C * x').
(x * y) * (C * x') = x * ((y * x') * C).
(x * (y' * (C * (y * (x' * y))))) * y' = C.
(x * (C * (y * z))) * y' = (x * y) * (z * (C * y')).
(x * (C * y)) * y' = (x * y) * (C * y').
((x * y') * (y * z')) * z = z' * (y' * ((y * z) * x)).
(x * y) * (C * x') = x * (C * (y * x')).
x * ((C * x) * y) = C * (x * (x * y)).
C * (x * (x * y)) = x * ((C * x) * y).
C * ((x * y') * x) = (x * y') * ((C * (x * y')) * y).
(x * y') * ((C * (x * y')) * y) = C * ((x * y') * x).
((C * x) * y) * x' = x * (C * (y * x')).
((x * y) * z) * (x' * y) = x * ((y * z) * (x' * y)).
(x * y') * ((C * y') * (y * x)) = C * ((x * y') * x).
(x * y') * (y * (C * (y' * x))) = C * ((x * y') * x).
(x * y') * (y * (C * (y' * x))) = C * (x * (y' * x)).
(x * (y' * ((y * x') * (x * (C * (x' * y)))))) * y' = C.
(x * (y' * ((y * x') * (x * ((z * (C * z')) * (x' * y)))))) * y' = C.
(x * (y' * ((y * x') * (((x * y) * (C * y')) * (x' * y))))) * y' = C.
(x * (y' * ((y * x') * (((x * (C * y)) * y') * (x' * y))))) * y' = C.
(x * (y' * ((y * x') * (((x * (C * y)) * (y' * x')) * y)))) * y' = C.
(x * ((x' * ((x * (C * y)) * (y' * x'))) * y)) * y' = C.
C = (x * y) * (y' * (x' * ((x * (C * y)) * (y' * x')))).
(x * y) * (y' * (x' * ((x * (C * y)) * (y' * x')))) = C.
(x * y) * (y' * (x' * (z' * (z * ((x * (C * y)) * (y' * x')))))) = C.
(x * y) * ((y' * (x' * y')) * (y * ((x * (C * y)) * (y' * x')))) = C.
(x * y) * ((y' * (x' * y')) * (y * ((z' * (z * (x * (C * y)))) * (y' * x')))) = C.
(x * y) * ((y' * (x' * y')) * (((y * x') * (x * (x * (C * y)))) * (y' * x'))) = C.
(x * y) * (((y' * x') * y') * (((y * x') * (x * (x * (C * y)))) * (y' * x'))) = C.
(x * y'') * (((y' * x') * y') * (((y * x') * (x * (x * (C * y)))) * (y' * x'))) = C.
(x' * y')' * (((x' * y') * x') * (((x * y') * (y * (y * (C * x)))) * (x' * y'))) = C.
C = (x' * ((x * y') * (y * (y * (C * x))))) * (x' * y').
(x' * ((x * y') * (y * (y * (C * x))))) * (x' * y') = C.
(x' * ((x * y') * (y * (y * (x * C))))) * (x' * y') = C.
(x' * ((x * y') * (y * (y * (x * ((C * (z' * u')) * (u * z))))))) * (x' * y') = C.
(x' * ((x * y') * (y * ((y * (x * (C * (y' * x')))) * (x * y))))) * (x' * y') = C.
(x' * ((x * y') * (y * ((y * ((x * y') * (C * x'))) * (x * y))))) * (x' * y') = C.
(x' * ((x * y') * (y * (((y * x) * (y' * (C * x'))) * (x * y))))) * (x' * y') = C.
(x' * ((x * y') * (y * (((y * (C * (x * y'))) * x') * (x * y))))) * (x' * y') = C.
(x' * (y' * ((y * x) * (((y * (C * (x * y'))) * x') * (x * y))))) * (x' * y') = C.
((((((x * (C * (y * x'))) * y') * (y * x)) * x') * (x * y')) * y) * (y' * x') = C.
((((((x * (C * (y * x'))) * (x * y')) * y) * x') * (x * y')) * y) * (y' * x') = C.
((((((((C * x) * y) * x') * (x * y')) * y) * x') * (x * y')) * y) * (y' * x') = C.
((((((((C * x) * y) * x') * (x * y')) * y) * (y' * x')) * x) * y) * (y' * x') = C.
((((((((C * x) * y) * (y' * x')) * x) * y) * (y' * x')) * x) * y) * (y' * x') = C.
R((((((C * x) * y) * (y' * x')) * x) * y) * (y' * x'),x,y) = C.
R(R(((C * x) * y) * (y' * x'),x,y),x,y) = C.
R(x * y,z,C) = R(x,z,C) * R(y,z,C).
R(c34 * c35,c36,C) != R(c34,c36,C) * R(c35,c36,C).
R(c34,c36,C) * R(c35,c36,C) != R(c34 * c35,c36,C).
(x * y) * (z * x) = z' * ((z * x) * (y * (z * x))).
x' * ((x * y) * (z * (x * y))) = (y * z) * (x * y).
(C * (C * x)) * y = C * (x * (C * y)).
(x * (C * y)) * (C' * x) = x * (y * x).
(C * x) * y = (C' * x')' * y.
(C' * x')' * y = (C * x) * y.
x * (y * x') = (x * C) * (y * (C' * x')).
(x * C) * (y * (C' * x')) = x * (y * x').
(x * y') * (C * ((y * x') * (z * (x * y')))) = (C * z) * (x * y').
x * ((y * z) * (x * y)) = (x * y) * (z * (x * y)).
(x * y) * (z * (x * y)) = x * ((y * z) * (x * y)).
(C' * x') * R(y,x,C) = C' * ((x' * (C * (y * x))) * (C' * x')).
C' * ((x' * (C * (y * x))) * (C' * x')) = (C' * x') * R(y,x,C).
(x' * y') * (C * ((y * x) * (z * (x' * y')))) = (C * z) * (x' * y').
C' * (x' * ((y * x) * x')) = (C' * x') * R(y,x,C).
C' * (x' * y) = (C' * x') * R(y,x,C).
(C' * x') * R(y,x,C) = C' * (x' * y).
(C' * x') * ((C * (y * x)) * (C' * x')) = C' * (x' * y).
(C' * x') * (C * (x * (y * x'))) = (C * y) * (C' * x').
(C' * x') * (C * (x * y)) = (C * (y * x)) * (C' * x').
(C * (x * y)) * (C' * y') = (C' * y') * (C * (y * x)).
(C * ((x * y) * z)) * (C' * z') = (C' * z') * (C * ((z * (x * z)) * (z' * y))).
(C' * x') * (C * ((x * (y * x)) * (x' * z))) = (C * ((y * z) * x)) * (C' * x').
(C' * x') * (C * ((x * (y * x)) * (z * (z' * (x' * u))))) = (C * ((y * u) * x)) * (C' * x').
(C' * x') * ((C * (C * (x * (y * x)))) * (C' * (x' * z))) = (C * ((y * z) * x)) * (C' * x').
(C' * x') * ((C * (C * (x * (y * x)))) * ((C' * x') * ((C * (z * x)) * (C' * x')))) = (C * ((y * z) * x)) * (C' * x').
(C' * x') * (((C * x) * (C * (y * x))) * ((C' * x') * ((C * (z * x)) * (C' * x')))) = (C * ((y * z) * x)) * (C' * x').
(C' * x') * (((C' * x')' * (C * (y * x))) * ((C' * x') * ((C * (z * x)) * (C' * x')))) = (C * ((y * z) * x)) * (C' * x').
(C * ((x * y) * z)) * (C' * z') = ((C * (x * z)) * (C' * z')) * ((C * (y * z)) * (C' * z')).
((C * (x * y)) * (C' * y')) * ((C * (z * y)) * (C' * y')) = (C * ((x * z) * y)) * (C' * y').
((C * (x * y)) * (C' * y')) * R(z,y,C) = (C * ((x * z) * y)) * (C' * y').
R(x,y,C) * R(z,y,C) = (C * ((x * z) * y)) * (C' * y').
(C * ((x * y) * z)) * (C' * z') = R(x,z,C) * R(y,z,C).
R(x,y,C) * R(z,y,C) = R(x * z,y,C).
R(x * y,C,z) = R(x,C,z) * R(y,C,z).
R(c31 * c32,C,c33) != R(c31,C,c33) * R(c32,C,c33).
R(c31,C,c33) * R(c32,C,c33) != R(c31 * c32,C,c33).
(x * y)' * x = y'.
x * (y * x)' = y'.
(x * (x * y)) * y' = x * x.
(x * (y * y)) * y' = x * y.
R(x,y,x) = (x * (y * x)) * (y * x)'.
(x * (y * x)) * (y * x)' = R(x,y,x).
R(x,y,y' * z) = ((x * y) * (y' * z)) * z'.
((x * y) * (y' * z)) * z' = R(x,y,y' * z).
(x * y) * z' = x * ((y * (x * z)') * x).
x * ((y * (x * z)') * x) = (x * y) * z'.
x * (y * (x * x))' = (y * x)'.
R(x,y,C') = (C' * (x * y)) * (y * C')'.
(C' * (x * y)) * (y * C')' = R(x,y,C').
((x * y') * z)' = z' * (y * x').
((x' * y) * z)' = z' * (y' * x).
R(x,C,y * C) = ((x * C) * (y * C)) * (y * (C * C))'.
((x * C) * (y * C)) * (y * (C * C))' = R(x,C,y * C).
R(x,y,C * C) = (C * ((x * y) * C)) * (y * (C * C))'.
(C * ((x * y) * C)) * (y * (C * C))' = R(x,y,C * C).
((x * y) * x) * y'' = (x * y) * (x * y).
x * y' = (x * (y * y)') * y.
(x * (y * y)') * y = x * y'.
(x * (C * C)) * y = C * (x * (C * y)).
(x * ((y * ((x * z) * (x * z))') * x)) * z = x * (y * (x * z)').
R(x,y,x) = x.
R(x,y,C * C) = C * ((x * y) * (C * (y * (C * C))')).
C * ((x * y) * (C * (y * (C * C))')) = R(x,y,C * C).
C * R(x,y,C) = (x * y) * ((y * C)' * (C * C)).
(x * y) * ((y * C)' * (C * C)) = C * R(x,y,C).
(x * (y' * (y * z)')) * y'' = (x * y') * z'.
x * ((x' * y) * z') = (y * x) * (z * x)'.
(x * y) * (z * y)' = y * ((y' * x) * z').
(x * (y * x)) * y'' = (x * y) * (x * y).
R(x,y,z) = ((x * y) * (y' * z)) * z'.
x' * (y' * z) = y * ((y' * (y * x)') * z).
x * ((x' * (x * y)') * z) = y' * (x' * z).
(x * (y * x)) * y = (x * y) * (x * y).
(x * y) * (x * y) = x * (y * (x * y)).
C * (x * (x * y)) = x * ((x * C) * y).
C * (x * (x * ((x * C)' * y))) = x * y.
C' * (x * y) = x * (x * ((x * C)' * y)).
x * (x * ((x * C)' * y)) = C' * (x * y).
C * (x * (x * (((x * C)' * (y * (x * C)')) * z))) = x * (y * ((x * C)' * z)).
(C' * (x * y)) * (C * y') = R(x,y,C').
R(x,y,C') = C' * ((C * (x * y)) * y').
C' * ((C * (x * y)) * y') = R(x,y,C').
((x * (C * (y * x))') * C)' = R(y,x,C').
(C * (x * (C * (y * x))'))' = R(y,x,C').
(x * y) * (z * y)' = y * (z * (x' * y))'.
R(x,y,z) = R(x,y,y' * z).
R(x,y,y' * z) = R(x,y,z).
(x * ((x' * y) * z)) * z' = R(y,x,x' * z).
x * (((x * y) * x)' * z) = y' * (x' * z).
x * ((x * (y * x))' * z) = y' * (x' * z).
x * ((x * (x * C))' * y) = C' * (x' * y).
((x' * y) * C)' = y * ((y * (y * C))' * x).
x * ((x * (x * C))' * y) = ((y' * x) * C)'.
x * ((x * (x * C))' * y) = (C * (y' * x))'.
R(x,y,y' * z) = z * ((z' * y) * (y' * x)).
x * ((x' * y) * (y' * z)) = R(z,y,y' * x).
(C * ((C' * x) * (y * z))) * (y * z)' = R(x,C,y * (y * ((y * C)' * z))).
R(x,C,y * (y * ((y * C)' * z))) = (C * ((C' * x) * (y * z))) * (y * z)'.
x * (y * ((y' * x') * z)) = R(z,y,y' * x).
x * (y * ((x * y)' * z)) = R(z,y,y' * x).
x * (y * ((x * y)' * z)) = R(z,y,x).
R(x,y,z) = z * (y * ((z * y)' * x)).
(C * (C * (x * y))) * (y * (C * C))' = R(x,C,y * C).
(C * (C * (x * y))) * (y * (C * C))' = R(x,y,C * C).
C * ((x * y) * (y * C)') = R(x,y,C * C).
(x * ((y * z) * y)') * y'' = (x * y') * z'.
(x * (y * (z * y))') * y'' = (x * y') * z'.
(x * (y * (z * y))') * y = (x * y') * z'.
(x * (y * z'))' = (z * (y * (x * y))') * y.
(x * (y * (z * y))') * y = (z * (y * x'))'.
R(x,y,C * C) = R(x,C,y * C).
R(x,C,y * C) = R(x,y,C * C).
(x * ((y * (x * (z * (x * z)))') * x)) * z = x * (y * (x * z)').
((x * y) * (z * (x * z))') * z = x * (y * (x * z)').
x * (y * (x * z)') = (x * (z * (x * y)'))'.
(x * (y * (x * z)'))' = x * (z * (x * y)').
C * ((x * y) * (C * y)') = R(x,y,C').
C * ((x * y) * (y * C)') = R(x,y,C').
R(x,y,C') = R(x,y,C * C).
R(x,y,C * C) = R(x,y,C').
R(x,C,y * C) = R(x,y,C').
R(x,C,y * (y * ((y * C)' * z))) = (C * ((x * C') * (y * z))) * (y * z)'.
R(x,C,y * (y * ((y * C)' * z))) = (y * z) * (((y * z)' * C) * (x * C')).
C * (x * (x * (((x * C)' * x') * y))) = x * (C * ((x * C)' * y)).
C * (x * (x * ((x * (x * C))' * y))) = x * (C * ((x * C)' * y)).
C * (x * (C * (y' * x))') = x * (C * ((x * C)' * y)).
C * ((x * y) * (C * y)') = y * (C * ((y * C)' * x)).
x * (C * ((x * C)' * y)) = R(y,x,C').
R(x,C,y) = R(x,y,C').
R(C,x,C) * R(y,x,C) = R(y * C,x,C).
C * R(x,y,C) = R(x * C,y,C).
R(x * C,y,C) = C * R(x,y,C).
(x * y) * ((y * C)' * (C * C)) = R(x * C,y,C).
(x * y) * (C * (C * (y * C)')) = R(x * C,y,C).
(x * y) * (C * y') = R(x * C,y,C).
x * R(y * C,x,C) = (x * C) * y.
x' * ((x * C) * y) = R(y * C,x,C).
x * ((x' * C) * y) = R(y * C,x',C).
(C * x)'' * (x' * y) = R(y * C,(C * x)',C).
R(x * C,(C * y)',C) = (C * y)'' * (y' * x).
x * ((C * x') * y) = R(y * C,x',C).
R(x,C,y * (y * ((y * C)' * z))) = R((x * C') * C,(y * z)',C).
R(x * C,(C * y)',C) = (y * C)'' * (y' * x).
R(x * C,(C * y)',C) = (y * C) * (y' * x).
R(x * C,(C * y)',C) = y * ((C * y') * x).
R(x * C,(C * y)',C) = R(x * C,y',C).
R(x * C,(y * C)',C) = R(x * C,y',C).
R(x,C,y * (y * ((y * C)' * z))) = R(x,(y * z)',C).
R(x,C,C' * (y * z)) = R(x,(y * z)',C).
R(x,(y * z)',C) = R(x,C,y * z).
R(x * C,C,y * C) = R(x * C,y',C).
R(x * C,y',C) = R(x * C,y,C').
R(x * C,C,y) = R(x * C,y',C).
R(x * C,y',C) = R(x * C,C,y).
R(x,y',C) = R((x * C') * C,C,y).
R((x * C') * C,C,y) = R(x,y',C).
R(x,C,y) = R(x,y',C).
R(x,y',C) = R(x,C,y).
R(x,C,y) * R(z,y',C) = R(x * z,y',C).
R(x,C,y) * R(z,y',C) = R(x * z,C,y).
R(x,C,y) * R(z,C,y) = R(x * z,C,y).

end_of_list.
