% -----------------------------------------------------------
% Gagola:  Moufang + Drapal => {Normal 1, Normal 2, Normal 3}
% -----------------------------------------------------------

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

set(para_from_small).

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.

% *********************
% Normality Condition 1
% *********************

% condition from J.D.'s talk at ADAM 2013

% (((C * x) * y) * (y' * x')) * z = z * (((C * x) * y) * (y' * x'))
%    # label("Normal 1").

% *********************
% Normality Condition 2
% *********************

% condition used by J.D.

% define D; A and B are arbitrary constants

  R(C,A,B) = D.

% D is in the commutant

% D * x = x * D # label("Normal 2").

% *********************
% Normality Condition 3
% *********************

% condition used by MK (uses commutator K)

% x * y = (y * x) * K(x,y) # label("commutator").

% K(R(C,x,y),z) = 1 # label("Normal 3").

% ****************************************
% Normality Condition 4 (Drapal Condition)
% ****************************************

% uses associator (a) and commutator (K)

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

  x * y = (y * x) * K(x,y) # label("commutator").

  a(x,C,K(y,z)) = 1 # label("Drapal Condition").

end_of_list.

formulas(goals).

  (((C * x) * y) * (y' * x')) * z = z * (((C * x) * y) * (y' * x'))
     # label("Normal 1").

  D * x = x * D # label("Normal 2").

  K(R(C,x,y),z) = 1 # label("Normal 3").

% a(x,C,K(y,z)) = 1 # label("Drapal Condition").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

(((C * x) * y) * (y' * x')) * z = z * (((C * x) * y) * (y' * x')).
1 * x = x.
x * 1 = x.
x * x' = 1.
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.
x * y = (y * x) * K(x,y).
(x * y) * K(y,x) = y * x.
a(x,C,K(y,z)) = 1.
(((C * c1) * c2) * (c2' * c1')) * c3 != c3 * (((C * c1) * c2) * (c2' * c1')).
x'' * 1 = x.
(x' * y') * ((y * x) * z) = z.
(x * (y * z)) * (z' * y') = x.
x * (y * x) = y' * ((y * x) * (y * x)).
x' * ((x * y) * (x * y)) = y * (x * y).
(x * (y * y)) * y' = x * y.
x' * ((x * y) * x) = y * x.
x * y' = y' * ((y * x) * y').
x' * ((x * y) * x') = y * x'.
x' * (((x * y) * x) * z) = y * (x * z).
(x * (y * x)) * z = x * (y * (x * z)).
(x * (y * (z * y))) * y' = (x * y) * z.
x * (y * ((x * y) * y)) = (x * y) * ((x * y) * y).
(x * y) * ((x * y) * y) = x * (y * ((x * y) * y)).
(x * (y * (z * y))) * z = (x * y) * (z * (y * z)).
x * (y * z') = z' * (((z * x) * y) * z').
x' * (((x * y) * z) * x') = y * (z * x').
x * (y * (x * z)) = (x * z) * ((z' * y) * (x * z)).
(x * y) * ((y' * z) * (x * y)) = x * (z * (x * y)).
(x' * y) * z = x' * ((y * (z * x)) * x').
x' * ((y * (z * x)) * x') = (x' * y) * z.
C' * (x * C) = x.
x' * (C * x) = C.
(x * C)' = x' * C'.
C * (x * C) = x * (C * C).
(C * (C * x)) * y = C * (x * (C * y)).
((x * C) * y) * x = C * (x * (y * x)).
((x * y) * C) * y = x * (y * (y * C)).
((C * x) * y) * C = x * (C * (y * C)).
C * ((x * C) * y) = x * (C * (y * C)).
(x * C) * (y * C) = C * ((x * y) * C).
(x * y) * (x * C) = x * ((y * C) * x).
(C * x) * (y * x) = x * ((C * y) * x).
(C * x) * (C * y) = C * ((x * y) * C).
(C * x) * (y * C) = C * (C * (x * y)).
((x * y) * z) * a(x,y,z)' = x * (y * z).
(x * y)' * (y * x) = K(y,x).
x = x''.
x'' = x.
x * (x' * y) = y.
(x * y') * y = x.
C' * (x * (C * (y * C))) = (x * C) * y.
(x' * y') * (C * (y * x)) = C.
x * (C * x') = C.
(x * y) * ((y' * x') * z) = z.
x * y = y * ((y' * x) * y).
x * ((x' * y) * x) = y * x.
x * ((x' * y) * x') = y * x'.
((x * y) * x) * (x' * z) = x * (y * z).
x * (y * z) = z * (((z' * x) * y) * z).
x * (((x' * y) * z) * x) = y * (z * x).
x * (y * (y' * (x' * z))) = z.
(x * (y' * z')) * (z * y) = x.
(x * (x * y')) * y = x * x.
x * y = (x * y') * (y * y).
(x * y') * (y * y) = x * y.
(x * (y' * y')) * y = x * y'.
(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.
C * (x * C') = x.
C' * x = x * C'.
C * (x * y) = y * (((C * y') * x) * y).
x * (((C * x') * y) * x) = C * (y * x).
C * (x * (x * C')) = x * x.
(x * C) * y = C * ((x * C') * (C * y)).
C * ((x * C') * (C * y)) = (x * C) * y.
C * (x * (C' * (y * C'))) = (x * C') * y.
x * (y * C) = C * (((x * C') * y) * C).
C * (((x * C') * y) * C) = x * (y * C).
C' * (x * C') = x * (C' * C').
(C' * (C' * x)) * y = C' * (x * (C' * y)).
((x * y) * C') * y = x * (y * (y * C')).
C' * ((x * C') * y) = x * (C' * (y * C')).
(x * C') * (y * C') = C' * ((x * y) * C').
(x * y) * (x * C') = x * ((y * C') * x).
(x' * C') * x = C'.
(x' * C') * ((x * C) * y) = y.
(x * (y * C)) * (y' * C') = x.
(x * C) * ((x' * C') * y) = y.
x' * (y * x) = (x' * y) * x.
(x' * y) * x = x' * (y * x).
(x' * y') * (x * y) = K(x,y).
C * (x * (C' * x)) = x * x.
((x' * y') * z') * ((z * (y * x)) * u) = u.
(C' * x') * ((C * x) * y) = y.
(x * y') * ((y * x') * z) = z.
(x' * y) * ((y' * x) * z) = z.
(x' * (y' * C')) * (((y * C) * x) * z) = z.
((x * C) * y) * ((y' * (x' * C')) * z) = z.
(x * (C' * y')) * (C * y) = x.
(x * (y' * (z' * C'))) * ((z * C) * y) = x.
(C * x) * y = (x * C) * y.
x * (C * y) = x * (y * C).
x' * (x * (y * C)) = C * y.
x * (C * ((y * C) * z)) = x * (y * (C * (z * C))).
(C * x) * (C * y) = (x * C) * (y * C).
a(x,C,(y' * z') * (y * z)) = 1.
x * (y * x') = (x * y) * x'.
(x * y) * x' = x * (y * x').
((x * y) * z) * (y' * x') = (x * y) * (z * (x * y)').
x' * ((x * (y * x)) * z) = y * (x * z).
(x * (y * (x * z))) * z = (x * (y * x)) * (z * z).
C * (x * (y * x)) = x * (y * (x * C)).
(C * (x * C)) * y = C * (x * (y * C)).
(x * (y * x)) * (x' * z) = x * (y * z).
(x * y) * z = x * ((y * x') * (x * z)).
x * ((y * x') * (x * z)) = (x * y) * z.
(C * (x * C)) * (y * C') = C * (x * y).
C' * (x * (y * x)) = x * (y * (x * C')).
(x * (C * C)) * y = C * (x * (C * y)).
(C' * x') * (((C * x) * (y * (C * x))) * z) = y * ((C * x) * z).
(C * (C * x)) * y = C * (x * (y * C)).
(C * (x * (y * x))) * y = (x * C) * (y * (x * y)).
(C * (x * y)) * y = x * (y * (y * C)).
C * ((C * x) * y) = x * (C * (y * C)).
C * ((x * C) * y) = x * (C * (C * y)).
(x * C) * (C * y) = C * ((x * y) * C).
(x * C) * (y * C) = C * (C * (x * y)).
(x * C) * y = C * ((x * (y * C')) * C).
C * ((x * (y * C')) * C) = (x * C) * y.
x * (y * C) = y * (((y' * x) * C) * y).
x * (((x' * y) * C) * x) = y * (x * C).
(C * x) * (y * x) = x * ((y * C) * x).
(C * x) * (C * y) = C * (C * (x * y)).
(C * x) * y = C * (C * (x * (y * C'))).
C * (C * (x * (y * C'))) = (C * x) * y.
x * (y * C) = C * (C * ((x * C') * y)).
C * (C * ((x * C') * y)) = x * (y * C).
(x * (C' * C')) * y = C' * (x * (C' * y)).
(C * (x * (y * x))) * x = x * ((y * (x * C)) * x).
x * (C * (x' * (y * x'))) = y * (x' * C).
(x * (C * C)) * y = C * (x * (y * C)).
(C * x) * y = C * ((C' * x) * (y * C)).
C * ((C' * x) * (y * C)) = (C * x) * y.
C * ((C * x) * y) = x * (C * (C * y)).
C * ((C * x) * y) = x * (y * (C * C)).
C' * (x * (C * (C * y))) = (x * C) * y.
(x * C) * (C * y) = C * (C * (x * y)).
(x * C) * (y * y) = C * (C * (x * (y * (y * C')))).
C * (C * (x * (y * (y * C')))) = (x * C) * (y * y).
(x * C) * (y * (z * (y * C))) = C * (C * (x * (y * (z * y)))).
x * (C * y) = C * (C * ((C' * x) * y)).
C * (C * ((C' * x) * y)) = x * (C * y).
(C * x) * y = C * (C * (x * (C' * y))).
C * (C * (x * (C' * y))) = (C * x) * y.
x * (C * y) = C * (C * ((x * C') * y)).
C * (C * ((x * C') * y)) = x * (C * y).
C' * (x * (C * (C * y))) = (C * x) * y.
C * ((C * x) * (C' * y)) = x * (C * y).
C * ((C * x) * (y * C')) = x * (y * C).
(x * C) * y = C * (C * (x * (C' * y))).
C * (C * (x * (C' * y))) = (x * C) * y.
x * (y * (x * y)) = (x * y) * (x * y).
(x * y) * (x * y) = x * (y * (x * y)).
(x * (y * (x * y))) * z = (x * y) * ((x * y) * z).
x' * ((y * x) * z) = (x' * y) * (x * z).
(x' * y) * (x * z) = x' * ((y * x) * z).
(x * (y' * z)) * y'' = (x * y') * (z * y).
(x * (y * z)) * y' = (x * y) * (z * y').
(x * (y * z)) * z' = (x * z) * (z' * y).
(x * y) * (y' * z) = y * ((y' * x) * z).
x' * (y * (z * x)) = ((x' * y) * z) * x.
((x' * y) * z) * x = x' * (y * (z * x)).
(x * (y * z)) * u = z * (((z' * x) * y) * (z * u)).
x * (((x' * y) * z) * (x * u)) = (y * (z * x)) * u.
(x * (y * (z * u))) * u' = (x * u) * ((u' * y) * z).
(x * y') * (y * z) = (x * (z * y')) * y.
(x * (y * z')) * z = (x * z') * (z * y).
(x * y') * (z * y) = (x * (y' * z)) * y.
(x * (y' * z)) * y = (x * y') * (z * y).
(x * y') * (z * (u * y)) = (x * ((y' * z) * u)) * y.
(x * ((y' * z) * u)) * y = (x * y') * (z * (u * y)).
x' * ((x * y) * z) = (y * (z * x')) * x.
(x * (y * z')) * z = z' * ((z * x) * y).
C' * ((C * x) * y) = C * (x * (y * C')).
x * ((y * (x * (z * x'))) * x) = (x * y) * (x * z).
((x * y) * z) * u = x * ((y * (z * x')) * (x * u)).
x * ((y * (z * x')) * (x * u)) = ((x * y) * z) * u.
(x * y') * ((y * z) * u) = (x * (z * (u * y'))) * y.
(x * (y * (z * u'))) * u = (x * u') * ((u * y) * z).
C * ((x * C') * y) = (x * C) * (y * C').
(x * C) * (y * C') = C * ((x * C') * y).
C' * (x * (y * C)) = C * ((x * C') * y).
C' * (x * (y * (z * C))) = (x * C) * ((y * C') * z).
(x * C) * ((y * C') * z) = C' * (x * (y * (z * C))).
x' * ((x * y) * z) = (y * x') * (x * z).
(x * y') * (y * z) = y' * ((y * x) * z).
x' * ((x * (y * x')) * z) = (y * (x' * x')) * (x * z).
(x * (y' * y')) * (y * z) = y' * ((y * (x * y')) * z).
x' * (((x * y) * z) * u) = (y * (z * x')) * (x * u).
(x * (y * z')) * (z * u) = z' * (((z * x) * y) * u).
x' * ((C * (y * x)) * z) = ((C * x') * y) * (x * z).
((C * x') * y) * (x * z) = x' * ((C * (y * x)) * z).
(x * y) * (x' * z) = x * ((y * x') * z).
(x * C') * (x' * y) = x * ((x' * C') * y).
(x * (y * z)) * (z' * u) = z * (((z' * x) * y) * u).
((x * y) * z) * (x' * u) = x * ((y * (z * x')) * u).
(x * (y * C)) * (C' * z) = C * (((x * C') * y) * z).
(x * y) * ((z * (x * y)') * x) = ((x * y) * z) * y'.
C * ((x * C') * y) = (C * x) * (y * C').
(C * x) * (y * C') = C * ((x * C') * y).
C * ((x * C') * (y * y)) = (C * x) * (y * (y * C')).
(C * x) * (y * (y * C')) = C * ((x * C') * (y * y)).
(x' * C') * (((x * C) * y) * z) = (y * (x * C)') * ((x * C) * z).
(x * (y * C)') * ((y * C) * z) = (y' * C') * (((y * C) * x) * z).
(x * (y * C)) * (z * C') = C * (((x * C') * y) * z).
C' * ((x * C) * y) = C * (x * (y * C')).
C' * (((x * C) * y) * z) = (x * (y * C')) * (C * z).
(x * (y * C')) * (C * z) = C' * (((x * C) * y) * z).
((x * C) * y) * (z * C') = C * ((x * (y * C')) * z).
x * ((C * (x' * y)) * x) = y * (x * C).
C * ((C' * x) * y) = (C * x) * (y * C').
(C * x) * (y * C') = C * ((C' * x) * y).
C' * (x * (C * y)) = C * ((C' * x) * y).
C' * ((C * x) * y) = C * (x * (C' * y)).
C' * (x * (C * y)) = C * ((x * C') * y).
C * (x * (C' * y)) = (x * C') * (C * y).
(x * C') * (C * y) = C * (x * (C' * y)).
C * (x * (y * C')) = (C' * x) * (y * C).
(C' * x) * (y * C) = C * (x * (y * C')).
C * (x * (y * C')) = (x * C') * (y * C).
(x * C') * (y * C) = C * (x * (y * C')).
C' * ((x * C) * y) = C * (x * (C' * y)).
C' * (x * ((y * C) * z)) = (x * C) * (y * (C' * z)).
(x * C) * (y * (C' * z)) = C' * (x * ((y * C) * z)).
x' * ((C * (x * y)) * x') = y * (x' * C).
(x * (y * (z * C))) * z' = (x * z) * (C * (z' * y)).
x' * ((y * (x * C)) * z) = (C * (x' * y)) * (x * z).
(C * (x' * y)) * (x * z) = x' * ((y * (x * C)) * z).
(x' * (y * z)') * (y * (z * x)) = a(y,z,x)'.
C * (C * ((x * y) * (C' * a(x,y,C)'))) = x * (y * C).
C * (C * (x * (y * (y * C')))) = (x * y) * (y * C).
x * (C' * (x' * (y * x'))) = y * (x' * C').
(C' * x) * (C * y) = C' * ((C * x) * y).
(x' * y') * (x * y) = x' * (y' * (x * y)).
x' * ((y' * x) * y) = K(x,y).
x' * (y' * (x * y)) = K(x,y).
(x * (x * (y * z))) * y' = ((x * x) * y) * (z * y').
(x * (x * y)) * (y' * z) = y * ((y' * (x * x)) * z).
(x * C) * (x' * y) = x * ((x' * C) * y).
(x * y) * (y' * C) = y * (C * (y' * x)).
(x * y) * (y' * C') = y * (C' * (y' * x)).
C * (C * (x * ((x' * C') * y))) = x * (C * (x' * y)).
(x * y) * (C' * (y' * (z * y'))) = y * ((y' * x) * (z * (y' * C'))).
(x * (y * z)) * z' = z * ((z' * x) * y).
((x' * y) * C') * x = x' * (y * (x * C')).
x * ((C * x') * (y * x)) = y * (x * C).
x' * (y * (x * C)) = (C * x') * (y * x).
(C * x') * (y * x) = x' * (y * (x * C)).
(x * y) * ((C * (x * y)') * y) = x' * ((x * y) * C).
x * ((x' * C) * (y * x)) = y * (x * C).
x * ((C * x') * y) = (y * x') * (x * C).
(x * y') * (y * C) = y * ((C * y') * x).
x * ((x' * C) * y) = (y * x') * (x * C).
(x * y') * (y * C) = y * ((y' * C) * x).
(x * (y * (z * y'))) * y = y' * ((y * x) * (y * z)).
(x * (C * y)) * C' = C * ((x * C') * y).
(x * (y' * (z * y'))) * (y * u) = y' * ((y * ((x * y') * z)) * u).
(x * y') * (C * (y * (z * y))) = y' * ((y * x) * (z * (y * C))).
(x * y') * (C' * (y * (z * y))) = y' * ((y * x) * (z * (y * C'))).
(x * C) * (x' * (y * x)) = y * (x * C).
(x * C)' * (y * (x * C)) = x' * (y * x).
C * (x * (y * C')) = ((x * C) * y) * C'.
((x * C) * y) * C' = C * (x * (y * C')).
C' * (x * (C * (x' * y))) = C * (x * ((x' * C') * y)).
C' * (C' * ((C * x) * y)) = x * (C' * y).
C' * (x * y) = C * ((x * C') * (C' * y)).
C * ((x * C') * (C' * y)) = C' * (x * y).
C' * (x * ((x' * C) * y)) = C * (x * (C' * (x' * y))).
C' * (C' * (x * (C * y))) = (x * C') * y.
(x * C') * y = C * (x * (C' * (C' * y))).
C * (x * (C' * (C' * y))) = (x * C') * y.
x * ((C * x') * ((C' * y) * x)) = C * (y * (x * C')).
x * ((x' * C) * y) = x * ((C * x') * y).
(x * y) * (C * y') = y * (C * (y' * x)).
(x * y') * (C * y) = y * ((C * y') * x).
x * ((C * x') * y) = x' * ((x * y) * C).
x' * ((x * y) * C) = x * ((C * x') * y).
(x * (C * y')) * y = y * ((y' * C) * x).
(x * (y * C)) * y' = y * (C * (y' * x)).
x' * (C * (x * y)) = x * ((C * x') * y).
(x * (x * (y * C))) * y' = y * (C * (y' * (x * x))).
(x * (y * (C * (y' * z)))) * y = y' * ((y * x) * (z * (y * C))).
(x * y)' * (C * x) = (x * y) * ((C * (x * y)') * y').
(x * y) * ((C * (x * y)') * y') = (x * y)' * (C * x).
x' * (C * (x * y)) = x * ((x' * C) * y).
x * (x * ((C * x') * y)) = C * (x * y).
x' * (C * (x * (x * y))) = (x * C) * y.
(x * y)' * (C * (x * ((y * C') * x))) = (x * y) * ((C * (x * y)') * (x * C')).
x * (x * ((x' * C) * y)) = C * (x * y).
(x' * y) * ((x' * y) * ((C * (x' * y)') * x)) = C * (x' * (y * x)).
x * (x * y) = C * (x * ((x * C') * y)).
C * (x * ((x * C') * y)) = x * (x * y).
x * (x * ((C * x') * (y * x'))) = C * ((x * y) * x').
x * ((x * C) * y) = C * (x * (x * y)).
C * (x * (x * y)) = x * ((x * C) * y).
C' * (x * ((x * C) * y)) = x * (x * y).
x * (C * (x' * (x' * y))) = (x' * C) * y.
(x * y')' * (C * ((x * y') * x)) = ((x * y') * C) * y.
(x * (y * C))' * (C * ((x * (y * C)) * x)) = ((x * (y * C)) * C) * (y' * C').
x * (C * (x' * y)) = x' * ((x'' * C) * y).
x' * ((x'' * C) * y) = x * (C * (x' * y)).
x * ((y * x') * (C * (x * z))) = (x * y) * (x * ((x' * C) * z)).
(x * y) * (x * ((x' * C) * z)) = x * ((y * x') * (C * (x * z))).
x * ((C * (y * x)) * x') = C * (x * y).
C' * (x * (x * y)) = x * ((x * C') * y).
C' * (x * y) = x * (x * ((x' * C') * y)).
x * (x * ((x' * C') * y)) = C' * (x * y).
C' * (x' * y) = x' * (x' * ((C' * x) * y)).
x' * (x' * ((C' * x) * y)) = C' * (x' * y).
(x * (C * (y * x))) * x' = C * (x * y).
(C * (x * y)) * x = x * (C * (y * x)).
(C * (x * (y * x))) * x = x * (C * (y * (x * x))).
((x * y) * C) * x = x * (C * (y * x)).
(x * C) * y = y * (C * ((y' * x) * y)).
x * (C * ((x' * y) * x)) = (y * C) * x.
x * (C * (x' * (y * x))) = (y * C) * x.
x' * ((y * C) * x) = C * (x' * (y * x)).
(x * y) * (y * ((y' * C) * z)) = y * ((y' * x) * (C * (y * z))).
C' * (x' * ((y * C) * x)) = x' * (y * x).
x * (y * (z * x')) = ((x * y) * z) * x'.
((x * y) * z) * x' = x * (y * (z * x')).
(x * ((x' * y) * z)) * y' = y * (x * ((x' * z) * y')).
(x * (C * (x' * y))) * y' = y * (x * ((C * x') * y')).
((x' * y') * z') * ((z * y) * x) = a(z,y,x).
((x' * (y * (C * C))') * z') * ((z * (C * (y * (x * C)))) * u) = u.
x * (C * ((x' * y) * z)) = (y * (z * x)) * (x' * C).
(x * (y * z)) * (z' * C) = z * (C * ((z' * x) * y)).
x' * ((C * x) * y) = (y * x) * (x' * C).
(x * y) * (y' * C) = y' * ((C * y) * x).
(x * y) * (y' * C) = y' * ((y * C) * x).
x' * ((C * x) * y) = x * (C * (x' * y)).
x' * ((x * C) * y) = x * (C * (x' * y)).
x * (x * (C * (x' * y))) = (C * x) * y.
(C * (x * C)) * (x' * y) = C * (x' * ((C * x) * y)).
x' * (C * ((x * C') * y)) = x * (C * (x' * (y * C'))).
x * (x * (C * (x' * y))) = (x * C) * y.
C' * ((C * x) * y) = x * ((x * C') * (C * (x' * y))).
x * ((x * C') * (C * (x' * y))) = C' * ((C * x) * y).
x * (x * (C * y)) = (x * C) * (x * y).
(x * C) * (x * y) = x * (x * (C * y)).
(x * C) * (x * y) = x * (x * (y * C)).
C' * (x * (x * (C * y))) = C * (x * (C' * (x * y))).
C' * (x * (x * (y * C))) = C * (x * (C' * (x * y))).
C' * (C' * (x * y)) = (x * C') * (C' * y).
(x * C') * (C' * y) = C' * (C' * (x * y)).
C' * (C * (x * (y * C'))) = x * (C' * y).
C' * (C' * (x * y)) = (x * C') * (y * C').
(x * C') * (y * C') = C' * (C' * (x * y)).
C * (x * ((y * C') * z)) = (x * C') * (y * (C * z)).
(x * C') * (y * (C * z)) = C * (x * ((y * C') * z)).
x' * (C' * (x * y)) = x * ((x' * C') * y).
C' * (x' * (y * x)) = x' * ((y * C') * x).
(x * y) * ((x * y) * y) = x * (y * (x * (y * y))).
(C' * (C' * x)) * y = C' * (x * (y * C')).
C' * ((x * C') * y) = x * (y * (C' * C')).
C * (x * ((y * C') * (z * C'))) = (x * C') * (y * z).
x * (C * ((y * C) * z)) = x * (y * (z * (C * C))).
(x * (y * (x * z))) * z = x * (y * (x * (z * z))).
(x * (y * (x * C))) * y = (x * C) * (y * (x * y)).
(x * (C' * C')) * y = C' * (x * (y * C')).
(x' * (y' * z')) * (z * (y * x)) = a(z,y,x)'.
(C' * (x' * y)) * x = x' * (y * (x * C')).
x * (C * (y * (x * x))) = x * ((y * (x * C)) * x).
x * ((y * (x * C)) * x) = x * (C * (y * (x * 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') * ((z * y') * x) = a(z,y',x).
((C'' * x') * y') * (C' * (y * x)) = a(y,x,C').
(((C * C)' * x') * y') * (C * ((y * x) * C)) = a(y,x,C * C).
((((x' * y') * (x * y))' * C') * z') * ((z * C) * ((x' * y') * (x * y))) = 1.
(((x * C)' * C') * y') * (C * (C * (y * x))) = a(y,C,x * C).
C' * ((x * y) * (((C'' * y') * x') * (x * y))) = (x * y) * a(x,y,C').
x * (x * (C' * (C' * (x' * y)))) = C' * (x * (y * C')).
(x * y)' * (C' * x) = (x * y) * (((x * y)' * C') * y').
(x * y) * (((x * y)' * C') * y') = (x * y)' * (C' * x).
(x * y)' * (C' * ((x * y) * x)) = x * ((y * ((x * y)' * C')) * x).
x' * ((x * y) * C') = x * ((x' * C') * y).
(x' * C') * (C * (x * y)) = C * (x * ((x' * C') * y)).
((x * y) * (y' * C')) * x' = x * (y' * (C' * (y * x'))).
x * (C' * (x' * (y * x))) = (y * C') * x.
(x * y) * (C' * (y' * (z * y))) = y * ((y' * x) * ((z * C') * y)).
(x * y) * (C' * ((x * y)' * y)) = (x' * C') * (x * y).
x * (C' * (y * x)) = ((x * y) * C') * x.
((x * y) * C') * x = x * (C' * (y * x)).
(x * y) * (C' * ((x * y)' * z)) = ((z * (y' * x')) * C') * (x * y).
((x * (y' * z')) * C') * (z * y) = (z * y) * (C' * ((z * y)' * x)).
x * (C * ((y * C)' * (C' * ((y * C) * z)))) = x * (y * ((((y * C)' * C') * z) * (C * C))).
(((x * C) * y) * (z * (((x * C) * y) * (y' * (x' * C'))))) * (y' * (x' * C')) = ((x * C) * y) * (z * (y' * (x' * C'))).
x' * (y * (x * C')) = (C' * x') * (y * x).
(C' * x') * (y * x) = x' * (y * (x * C')).
x' * (x * (C * (y * (x * x)))) = (y * (x * C)) * x.
(x * y') * (y * C') = y * ((y' * C') * x).
(x' * C') * (y * x) = x' * (y * (x * C')).
(C' * (x * y')) * (y * C) = C * (y * ((y' * C') * x)).
(x * y) * (z * (x * y)) = x * ((y * 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 * (y * ((C' * x) * y))) = (x * y) * (x * y).
(x * y) * ((z * C) * (x * y)) = x * (y * (((C * z) * x) * y)).
(x * (y * (z * ((u * y) * z)))) * (y * z)' = (x * (y * z)) * u.
x * (((x' * y) * z) * C) = (y * (z * x)) * (C * x').
(x * (y * z)) * (C * z') = z * (((z' * x) * y) * C).
x' * (((x * y) * (x * z)) * u) = (y * (x * (z * x'))) * (x * u).
(x * (y * (z * y'))) * (y * u) = y' * (((y * x) * (y * z)) * u).
x * ((y * (C' * x')) * (x * z)) = (C' * (x * y)) * z.
(x * y) * (y * C) = (x * C) * (y * y).
(x * C) * (y * y) = (x * y) * (y * C).
(x' * C) * ((x * y) * (x * y)) = y * ((x * y) * C).
(x * C) * ((y * C') * (y * C')) = (x * (y * C')) * y.
x * (C' * (x' * y)) = x' * ((C' * x) * y).
x' * ((C' * x) * y) = x * (C' * (x' * y)).
x' * ((x * C') * y) = x * (C' * (x' * y)).
(x' * C') * (x * y) = x * (C' * (x' * y)).
x * (x * (C' * (x' * y))) = (x * C') * y.
x' * y = x * (C' * (x' * ((C * x') * y))).
x * (C' * (x' * ((C * x') * y))) = x' * y.
(C' * (x * y')) * y = y * (C' * (y' * x)).
x * (x * ((x' * y) * C')) = (x * C') * y.
x * (x * (C' * (C' * (x' * (x' * y))))) = (x * C') * ((x' * C') * y).
x * (y * (x' * C')) = (x * C') * (y * x').
(x * C') * (y * x') = x * (y * (x' * C')).
x * (x * (y * C')) = (x * C') * (x * y).
(x * C') * (x * y) = x * (x * (y * C')).
C * (x * (x * (y * (x' * C')))) = x * (x * (y * x')).
((x' * y) * (z * y)') * (z * x) = a(z * y,y',x).
(x * (y * C)) * y = C * (x * (y * y)).
(C * (x * (y * y))) * y' = x * (y * C).
(x * (x * (y * C))) * y = C * ((x * x) * (y * y)).
(x * y) * (y * C') = C * (x * ((y * C') * (y * C'))).
C * (x * ((y * C') * (y * C'))) = (x * y) * (y * C').
(C * (x * (y * C'))) * y = C * ((x * C') * (y * y)).
(C * x) * y'' = (x * (y * y)) * (y' * C).
(x * (y * y)) * (y' * C) = (C * x) * y''.
(x * (y * y)) * (y' * C) = (x * C) * y''.
(x * (y * y)) * (y' * C) = (x * C) * y.
(x * (y * y)) * (C * y') = (x * C) * y.
(x * (y * (x * (z * z)))) * (C * z') = ((x * (y * x)) * C) * z.
(x' * ((x * y) * (x * y))) * (C * (x * y)') = x' * ((C * x) * y).
(x * (x * (y * C))) * y = C * (x * (x * (y * y))).
C * (x * (y * ((x * C') * y))) = (x * y) * (x * y).
(x' * C) * (x * (y * (x * y))) = y * ((x * y) * C).
C * (x * (y * ((x * C') * y))) = x * (y * (x * y)).
x * ((y * x) * C) = y' * ((C * y) * (x * (y * x))).
x' * ((C * x) * (y * (x * y))) = y * ((x * y) * C).
C * ((x * C) * (y * (x * y))) = (x * C) * (y * ((x * C) * y)).
(x * C) * (y * ((x * C) * y)) = C * ((x * C) * (y * (x * y))).
x' * ((x * C) * (y * (x * y))) = y * ((x * y) * C).
x' * ((x * C) * (y * (x * y))) = y * (C * (x * y)).
x * (y * (C * (x * y))) = (x * C) * (y * (x * y)).
(x * C) * (y * (x * y)) = x * (y * (C * (x * y))).
(C * x) * (y * (x * y)) = x * (y * (C * (x * y))).
(x * (y * (x * C))) * y = x * (y * (C * (x * y))).
(x * (y * (z * C'))) * z' = (x * z) * ((z' * y) * C').
(x * ((x' * C') * y)) * y' = (x' * y) * ((y' * C') * x).
(x * (y * (C' * (y' * z')))) * z = (x * z') * (y * ((y' * C') * z)).
(x' * ((y * x) * (z * u'))) * u = ((x' * y) * u') * ((u * x) * z).
(C * (x * (C' * (y * z')))) * z = (C' * z') * ((z * (x * C)) * y).
(x * C) * ((y * C') * (z * C')) = C' * (x * (y * z)).
C * (C * (x' * (((x * C') * y) * z))) = (y * x') * (C * (x * z)).
x' * (((x * y') * z') * (z * y)) = a(x,z,y)'.
x' * (y' * ((y * (x * z')) * z)) = a(x,y,z)'.
x' * (y' * (z' * ((z * y) * x))) = a(x,y,z)'.
(x * (x * (y * z))) * (z' * u) = z * (((z' * (x * x)) * y) * u).
(x * (y * (z * (C * (y * z))))) * (z' * u) = z * (((z' * x) * (y * (z * (y * C)))) * u).
(C * (x * y)) * (x' * z) = x * ((y * (C * x')) * z).
((x * y) * z) * y' = x * ((y * (z * (x * y)')) * x).
x * ((y * (z * (x * y)')) * x) = ((x * y) * z) * y'.
(x * (C * y)) * (z * C') = C * (((x * C') * y) * z).
(x * (y * C')) * (z * C) = C' * (((x * C) * y) * z).
(x * ((C * x') * y)) * (z * C') = C * ((x * ((x' * y) * C')) * z).
(x * (x * (y * z))) * y' = (x * (x * y)) * (z * y').
(x * y) * ((C * (x * y)') * y) = x * ((C * x') * y).
x * (C * (x' * (y * y))) = (y * x) * (C * (x' * y)).
(x * y) * (C * (y' * x)) = y * (C * (y' * (x * x))).
x * (C * ((x' * C') * y)) = C * ((y * x) * (x' * C')).
C * ((x * y) * (y' * C')) = y * (C * ((y' * C') * x)).
(x * C') * (y * (z * C)) = C * (x * ((y * C') * z)).
(C' * x) * (y * (C * z)) = C * (x * ((y * C') * z)).
(x * C') * (y' * (C * (y * z))) = C * (x * (y' * ((C' * y) * z))).
(C * x) * (C * (((x * C)' * y) * z)) = (y * (z * (x * C))) * (C * (x * C)').
(x * (y * (z * C))) * (C * (z * C)') = (C * z) * (C * (((z * C)' * x) * y)).
((x' * y) * (y' * z')) * (z * x) = a(z * y,y',x).
x * ((C * (C * x')) * y) = C * (x' * ((C * x) * y)).
C * (x' * ((C * x) * y)) = x * ((C * (C * x')) * y).
x * ((y * (z * (y' * x'))) * x) = ((x * y) * z) * y'.
((x * y) * ((x * C) * (y * y))) * y' = ((x * y) * ((x * y) * y)) * (C * y').
(x * y) * ((C * (y' * x')) * y) = x * ((C * x') * y).
(x * (C * (x' * (y * y)))) * y' = y * (x * ((C * (x' * y)) * y')).
(C' * x) * (y * (C * (C * z))) = C * (x * (C * (y * (C' * z)))).
C * (x' * ((C * x) * y)) = x * (C * (x' * (y * C))).
C * (x * (C * (x' * y))) = x * (C * (x' * (y * C))).
C * (x * (C * (x' * (y * C')))) = x * (C * (x' * y)).
((x * y) * z) * (y' * x') = (x * y) * (z * (y' * x')).
C' * (x * (y * (C * (y' * z)))) = (x * C) * (y * ((y' * C') * z)).
(x * C) * (y * ((y' * C') * z)) = C' * (x * (y * (C * (y' * z)))).
C' * (x * (y * (C * (y' * z)))) = (C * x) * (y * ((y' * C') * z)).
(C * x) * (y * ((y' * C') * z)) = C' * (x * (y * (C * (y' * z)))).
(x * y) * ((C * (x * y)') * y') = (y' * x') * (C * x).
x * (x * (x' * ((y * C) * x'))) = C * ((x * y) * x').
x * (C * (x * (C' * (x' * y)))) = C' * ((C * x) * y).
((C * x') * y') * (C' * (y * x)) = a(y,x,C').
a(x,y,C') = C * ((y' * (x' * C')) * (x * y)).
C * ((x' * (y' * C')) * (y * x)) = a(y,x,C').
x * ((y * (x' * C')) * (x * z)) = (C' * (x * y)) * z.
(x * y) * (y * C') = (x * C') * (y * y).
(x * C') * (y * y) = (x * y) * (y * C').
x' * ((x * y) * (y * C')) = x * (C' * (x' * (y * y))).
C' * (x * (y * y)) = (x * (y * C')) * y.
(x * (y * C')) * y = C' * (x * (y * y)).
(C' * (x * (y * y))) * y' = x * (y * C').
((x * (y * y))' * C') * ((x * (y * y)) * y') = (x * (y * y))' * (x * (y * C')).
((x' * y') * (y'' * z')) * (z * x) = a(z * y',y,x).
(x * y) * ((C * y') * (x' * y)) = x * ((C * x') * y).
C * (x * (C * (x' * (C' * y)))) = x * (C * (x' * y)).
x * ((y * C) * x') = C * ((x * y) * x').
C * ((x * y) * x') = x * ((y * C) * x').
C * (x * (y * x')) = x * ((y * C) * x').
C' * (x * ((y * C) * x')) = x * (y * x').
(x * (y * C')) * (((z * C) * ((x * C) * y)') * C) = C' * (C * (((x * C) * y) * (z * ((x * C) * y)'))).
C' * (x * (y * x')) = x * ((y * C') * x').
x * (C * (x * (C' * (x' * y)))) = C * (x * (y * C')).
x' * ((C' * (x * y)) * z) = (y * (x' * C')) * (x * z).
(x * (y' * C')) * (y * z) = y' * ((C' * (y * x)) * z).
(x * y) * (y' * (x' * (y * C))) = x * ((C * x') * y).
C * (x * ((x' * C') * y)) = x * (C * (x' * (y * C'))).
(x * y) * (C * ((x * y) * (C' * ((x * y)' * y')))) = C * (y * ((y' * x) * C')).
x * (C * (x' * ((x * C') * y))) = C * (x * (y * C')).
x * ((C * x') * y) = y * ((y' * x) * (x' * (y * C))).
x * ((x' * y) * (y' * (x * C))) = y * ((C * y') * x).
x * (C * ((C' * x') * (x * y))) = C * (x * (y * C')).
x * (y * ((y' * x') * (x * C))) = y * ((C * y') * x).
x * ((x' * C) * (C' * (x * y))) = C * (x * (y * C')).
x * (y * (x * ((C * x') * y'))) = y * ((C * y') * x).
x * (y * (x * ((x' * C) * y'))) = y * ((C * y') * x).
C * (x' * (y * C')) = x * (C * (x' * (C' * (x' * y)))).
x * (C * (x' * (C' * (x' * y)))) = C * (x' * (y * C')).
x' * (y * ((C * y') * x)) = y * (x * ((C * x') * y')).
x * (y * ((C * y') * x')) = y * (x' * ((C * x'') * y')).
x * (y' * ((C * y'') * x')) = y * (x * ((C * x') * y')).
C' * (x * ((x' * y) * (y * C))) = C * (x * (C' * (x' * (y * y)))).
(C * (x * (C' * (x' * y')))) * y = (C' * y') * ((y * x) * (x' * C)).
(x'' * y') * (C * ((y * x') * y)) = ((y * x') * C) * x.
(C' * ((x * C') * (x' * y))) * y' = y * (x * ((x' * (C' * C')) * y')).
C * (x' * (C * ((x * C') * y))) = x * (C * (x' * y)).
((x' * (y' * z')) * z'') * (y * x) = a(z',z * y,x).
(x * y) * (C' * ((y' * x') * y)) = (x' * C') * (x * y).
C * (x * ((x' * C') * y)) = C * ((y * x') * (x * C')).
C * ((x * y') * (y * C')) = C * (y * ((y' * C') * x)).
(x * y) * (((x * (z * x')) * C) * (x * y)) = x * (y * ((x' * ((x * C) * (x * z))) * y)).
(x * C) * (y * ((x * C) * y)) = C * (x * (y * (C * (x * y)))).
(x * (y * (z * C'))) * z' = (x * z) * (C' * (z' * y)).
C * ((x * y) * (y' * C')) = y * (C' * (y' * (x * C))).
C * (x * (C' * (x' * y))) = x * (C * ((x' * C') * y)).
(x * y) * ((C * (x * y)') * y') = x * ((C * x') * y').
C' * (x * (y * (C * (y' * (z * C'))))) = C * ((x * C') * (y * ((y' * C') * z))).
C * ((x * y') * (C' * y)) = C * (y * ((y' * C') * x)).
(C * (x * (y * (C * (x * y))))) * z = ((x * C) * y) * (((x * C) * y) * z).
(x * y) * (C' * (y' * x)) = (x * (x * y)) * (C' * y').
(x * (x * y)) * (C' * y') = (x * y) * (C' * (y' * x)).
((x * C) * y) * (y' * C') = C * ((x * y) * (y' * C')).
C * (x * (C' * (x' * (C' * y)))) = x * (C' * (x' * y)).
C * ((x * C') * y) = y * (C * ((y' * C') * (x * y))).
x * (C * ((x' * C') * (y * x))) = C * ((y * C') * x).
(x * y) * ((C * (y' * x')) * y') = x * ((C * x') * y').
C * ((x * (y' * C')) * y) = C * (y * ((y' * C') * x)).
(x * (x * y)) * (y' * C') = (x * y) * (C' * (y' * x)).
((C * x) * y) * (y' * C') = C * ((x * y) * (y' * C')).
(x * y) * (C' * (y' * x)) = y * ((y' * (x * x)) * C').
(C * (x * (y * C))) * (y' * C') = C * (((x * C) * y) * (y' * C')).
(x * y) * (C' * (y' * x)) = y * (C' * (y' * (x * x))).
(x * y) * (((x * y)' * C') * y') = (y' * x') * (C' * x).
(x * (y' * (z * (u * z)))) * (y' * z)' = (x * (y' * z)) * (u * y).
(x * (y * (x * (z * z)))) * (C * z') = (C * (x * (y * x))) * z.
((x' * y') * (y * z')) * (z * x) = a(z * y',y,x).
(x' * ((x * y') * z')) * (z * y) = a(z * x',x,y).
(x * y') * (C * ((y * x') * y)) = ((y * x') * C) * x.
(x * y') * (C * (y * (x' * y))) = ((y * x') * C) * x.
(x * y') * (C * (y * (x' * y))) = (C * (y * x')) * x.
(x * y') * (C * (y * (x' * y))) = x' * ((x * C) * y).
(x * y') * (C * (y * (x' * y))) = x * (C * (x' * y)).
((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) = y' * (((y * x') * (x * z')) * z).
x' * (((x * y') * (y * z')) * z) = a(y',y * x,z).
a(x',x * y,z) = a(y * x',x,z).
a(x * y',y,z) = a(y',y * x,z).
a(x,y,z) = a(y',y * (x * y),z).
a(x',x * (y * x),z) = a(y,x,z).
a(x,x' * (y * x'),z) = a(y,x',z).
a(x,y * x',z) = a(x * y,x',z).
a(x * y,x',z) = a(x,y * x',z).
x' * ((y' * ((y * x) * z')) * z) = a(y',y * x,z).
x' * (y' * ((y * z') * (z * x))) = a(z',z * x,y).
x' * (y' * (z' * ((z * y) * x))) = a(z',z * x,y).
a(x',x * y,z) = a(y,z,x)'.
(x * y) * (C' * (y' * (x' * y))) = (x' * C') * (x * y).
(x * y) * (y' * (C * (x' * y'))) = x * ((C * x') * y').
(x * y) * (C' * (y' * (x' * y))) = x * (C' * (x' * y)).
x * ((C * x') * y') = y * ((y' * x) * (C * (x' * y'))).
x * ((x' * y) * (C * (y' * x'))) = y * ((C * y') * x').
(x * y') * (C' * (y * (x' * y'))) = x * (C' * (x' * y')).
x * (y * (C * (y' * (x' * x')))) = y * ((C * y') * x').
(C' * x') * (((C * x) * y) * z) = (y * (C' * x')) * ((C * x) * z).
(x * (C' * y')) * ((C * y) * z) = (C' * y') * (((C * y) * x) * z).
x' * ((x * y) * (y' * (x * C))) = y * (C * (y' * x)).
x * (y * (C * (y' * x))) = (x * y) * (y' * (x * C)).
(x * y) * (y' * (x * C)) = x * (y * (C * (y' * x))).
x * (y * (C * (y' * x))) = y * ((y' * x) * (x * C)).
x * ((x' * y) * (y * C)) = y * (x * (C * (x' * y))).
x * (x * (y * ((y' * (x' * C')) * ((x' * C') * C)))) = C' * (x * (y * (C * (y' * (x' * C'))))).
(x * C') * (y * (C * (z * (C * (z' * (y * C')))))) = C * (x * (z * ((z' * (y * C')) * ((y * C') * C)))).
((x' * y') * (x' * z')) * (z * (x * (y * x))) = a(z * x,y,x).
(((C' * C') * x') * y') * (C * ((y * x) * C)) = a(y,x,C * C).
(((C' * x') * C') * y') * (C * (C * (y * x))) = a(y,C,x * C).
(x * (C' * (x' * y))) * y' = y * (x' * (C' * (x * y'))).
(x' * y) * ((y' * C') * x) = y * ((y' * x) * (x' * C')).
(x * (x * (y * (z * (u * z))))) * (z' * w) = z * (((z' * (x * x)) * ((y * z) * u)) * w).
x * (y' * ((C * y) * x')) = y * (x * ((C * x') * y')).
x * (y * (C * (y' * x'))) = y * (x * ((C * x') * y')).
x * (y * ((C * y') * x')) = y * (x * (C * (x' * y'))).
x' * (y * ((C * y') * x)) = x * (y * (C * (y' * x'))).
(x * y) * (((x * y)' * C') * y') = (y' * x') * (x * C').
x * (y' * (C' * (y * x'))) = (y * x) * ((x' * C') * y').
(x * y) * ((y' * C') * x') = y * (x' * (C' * (x * y'))).
(x' * y) * ((y' * C') * x) = y * (x * (C' * (x' * y'))).
(x * y) * (((x * y)' * C') * y') = x * ((x' * C') * y').
(x * y) * ((y' * C') * x') = y * (x * ((x' * C') * y')).
(x * y) * (((y' * x') * C') * y') = x * ((x' * C') * y').
(x * (y' * C')) * ((y * C) * z) = (y' * C') * (((y * C) * x) * z).
((x' * ((C * C)' * y')) * z') * ((z * (C * (y * (x * C)))) * u) = u.
(x * (y * x)) * (C * (y * x)') = y' * ((C * y) * x).
(x * (y * x)) * (C * (x' * y')) = y' * ((C * y) * x).
x' * ((C * x) * y) = y * (x * (y * (C * (y' * x')))).
x * (y * (x * (C * (x' * y')))) = y' * ((C * y) * x).
x * (y * (x * (C * (x' * y')))) = y * (C * (y' * x)).
x' * (y * (C * (y' * x))) = y * (x * (C * (x' * y'))).
(x * (C * (x' * y))) * y = y * ((x * (y * (C * (y' * x')))) * y).
x * ((y * (x * (C * (x' * y')))) * x) = (y * (C * (y' * x))) * x.
x * ((y * (z * x')) * (u * (C * (u' * x)))) = ((x * y) * z) * (u * (x * (C * (x' * u')))).
((x * y) * z) * (u * (x * (C * (x' * u')))) = x * ((y * (z * x')) * (u * (C * (u' * x)))).
x * (y * ((C * y') * x')) = x' * (y * (C * (y' * x))).
x' * (y * (C * (y' * x))) = x * (y * ((C * y') * x')).
(x * y') * (y * ((x' * C') * y')) = x * (C' * (x' * y')).
a(x * y,z,y) = x' * (((x * (y' * z')) * y') * (y * (z * y))).
x' * (((x * (y' * z')) * y') * (y * (z * y))) = a(x * y,z,y).
((C' * (C' * x')) * y') * (C * ((y * x) * C)) = a(y,x,C * C).
(C' * (x' * (C' * y'))) * (C * (C * (y * x))) = a(y,C,x * C).
(x * y) * (y' * (C' * (x' * y'))) = x * ((x' * C') * y').
x * (x' * ((x * y) * (y' * (x * C)))) = (y * (C * (y' * x))) * x.
x * (C' * (x' * y')) = y' * ((y * x) * ((x' * C') * y')).
x' * ((x * y) * ((y' * C') * x')) = y * (C' * (y' * x')).
x' * (y' * ((y * (x * (y' * z'))) * (z * y))) = a(x * y,z,y).
(C' * (x' * (y' * C'))) * (C * ((y * x) * C)) = a(y,x,C * C).
(C' * (x' * (y' * C'))) * (C * (C * (y * x))) = a(y,C,x * C).
x * ((x' * C') * y') = y * ((y' * x) * (C' * (x' * y'))).
x * ((x' * y) * (C' * (y' * x'))) = y * ((y' * C') * x').
x * (y * (C * (y' * x))) = (y * (C * (y' * x))) * x.
(x * (C * (x' * y))) * y = y * (x * (C * (x' * y))).
(x' * C') * (x * (y * (C * (y' * x)))) = x' * ((y * (C * (y' * x))) * (x * C')).
C * (x * (x * ((y * (C * (y' * x'))) * (x' * C')))) = x * (x * (x' * (y * (C * (y' * x'))))).
x' * (y * (x * ((x' * C') * y'))) = y * (C' * (y' * x')).
x' * (y' * (y * (((x * (y' * z')) * z) * y))) = a(x * y,z,y).
(C' * (x' * (y' * C'))) * (C * (C * (y * x))) = a(y,x,C * C).
x * (y * (C' * (y' * (x' * x')))) = y * ((y' * C') * x').
x * (y * (C' * (y' * x'))) = y * (x * ((x' * C') * y')).
x' * (y * (x * (C' * (x' * y')))) = y * ((y' * C') * x').
x * ((C * (C * y)) * (((C * (C * y))' * C') * x')) = C * (y * ((x * (C' * (x' * (C * (C * y))'))) * C)).
C * (x * ((y * (C' * (y' * (C * (C * x))'))) * C)) = y * ((C * (C * x)) * (((C * (C * x))' * C') * y')).
x' * (y' * (y * ((z' * ((z * x) * y')) * y))) = a(x * y,z,y).
a(x,y,C * C) = a(x,C,y * C).
a(x,C,y * C) = a(x,y,C * C).
a(x,C,C * y) = a(x,y,C * C).
a(x * y,C,x' * C) = a(x,y * x',C * C).
a(x,C,C * (y * x')) = a(x * y,C,x' * C).
a(x * y,C,x' * C) = a(x,C,C * (y * x')).
x' * ((C * x) * (y * (x * (C' * (x' * y'))))) = x * (C * (y * ((y' * C') * x'))).
x' * (y' * (y * (y' * ((y * z') * (z * x))))) = a(x * y,z,y).
x' * (y' * (y * (y' * (z' * ((z * y) * x))))) = a(x * y,z,y).
x' * (y' * (z' * ((z * y) * x))) = 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(x,y,z) = a(x,y,z * x').
a(x,y,z * x') = a(x,y,z).
a(x',x * y,z * x) = a(y,z,x)'.
a(x * y,z,x') = a(x,y,z)'.
a(x * y,z,y)' = a(x,y,z * y).
a(x,y,z)'' = a(x,y,z * y).
a(x,y,z * y) = a(x,y,z)''.
a(x,y,z * y) = a(x,y,z).
a(x,C,C * y) = a(x,C,y).
a(x * y,C,x') = a(x,C,C * (y * x')).
a(x,C,C * (y * x')) = a(x * y,C,x').
a(x,C,C * (y * x')) = a(x,y,C)'.
a(x,y,C)' = a(x,C,y * x').
a(x,C,y * x') = a(x,y,C)'.
a(x,y,C)' = a(x,C,y).
C * (C * ((x * y) * (C' * a(x,C,y)))) = x * (y * C).
x * (y * C) = (C * (x * y)) * a(x,C,y).
(C * (x * y)) * a(x,C,y) = x * (y * C).
(C * (x * y)) * a(y * x,C,K(x,y)) = (y * x) * (K(x,y) * C).
(C * (x * y)) * 1 = (y * x) * (K(x,y) * C).
(x * y) * (K(y,x) * C) = (C * (y * x)) * 1.
(x * y) * (K(y,x) * C) = C * (y * x).
(x * y) * (C * K(y,x)) = C * (y * x).
(x' * y') * (C * (x * y)) = C * K(x,y).
(x * y) * (C * (y' * (x' * (y * x)))) = C * (y * x).
(x' * (y' * C')) * (C * (x * (y * C))) = C * (x' * ((y * C)' * (x * (y * C)))).
(x' * y') * (C' * ((y * x) * y)) = y * ((x * ((y * x)' * C')) * y).
x * ((x' * y) * ((y' * C') * x)) = y * (C' * (y' * x)).
x * (y * (x * (C' * (x' * y')))) = y * (C' * (y' * x)).
x' * (y * (C' * (y' * x))) = y * (x * (C' * (x' * y'))).
x * (x * (y * ((y' * C') * x'))) = y * (C' * (y' * x)).
x' * (y * (C' * (y' * x))) = x * (y * ((y' * C') * x')).
(x * y) * (z * (y * (C' * (y' * z')))) = y * ((y' * x) * (z * (C' * (z' * y)))).
((x' * y) * z') * ((z * x) * u) = (x' * z') * ((z * (y * x)) * u).
(C * (x * (C' * (y * z')))) * z = (z' * C') * ((z * (x * C)) * y).
(x * ((C * x') * y)) * (z * C') = C * ((x * (C' * (x' * y))) * z).
(x * C') * (y * ((C * y') * z)) = C * (x * (y' * ((C' * y) * z))).
(x * (C * (x' * (y * y)))) * y' = y * (x * (y * ((y' * C) * x'))).
(x * C) * (y * ((y' * C') * x)) = C' * (y * ((y' * x) * (x * C))).
(C * x') * (y * ((y' * C') * x)) = C' * (x * (y * ((C * y') * x'))).
C' * (x * (y * (C * (y' * x)))) = C * (y * (C' * (y' * (x * x)))).
(((x * C) * y) * ((((x * C) * y)' * ((x * C) * y)) * z)) * ((x * C) * y)' = (C * (x * (y * (C * (x * y))))) * ((((x * C) * y)' * z) * ((x * C) * y)').
(C * (x * (y * C))) * (y' * C') = C * (C * ((x * y) * (y' * C'))).
(x * (y' * (z' * u))) * (y' * z')' = (x * (y' * z')) * ((u * z) * y).
(x * (y' * C')) * (C * (C * (y * z))) = (y' * C') * (((y * C) * x) * (z * C)).
((x' * ((C' * C') * y')) * z') * ((z * (C * (y * (x * C)))) * u) = u.
(x * C') * (y * ((C * y') * z)) = C * (x * (y * (C' * (y' * z)))).
(x * (C * (x' * (y * y)))) * y' = x * ((C * x') * y).
(x * ((C * x') * y)) * y = x * (C * (x' * (y * y))).
C * (x * (x * ((y * ((C * y') * x')) * (x' * C')))) = x * (x * (y * (C * (y' * (x' * x'))))).
x' * (C' * (y * ((y' * x) * (x * C)))) = x * (C * (x' * (y * ((y' * C') * x)))).
(C * x) * (y * ((y' * C') * x)) = C * (y * (C' * (y' * (x * x)))).
(C * (x * (y * C))) * (y' * C') = (C * (x * y)) * y'.
(C * (x * (y * C))) * (y' * C') = (C * y) * (y' * x).
(C * (x * (y * C))) * (y' * C') = (y * C) * (y' * x).
(C * (x * (y * C))) * (y' * C') = y * ((C * y') * x).
((x * (y * C)) * C) * (y' * C') = y * ((C * y') * x).
x * (x * (C * (y * (C' * (y' * (x' * x')))))) = C * (x * (y * ((y' * C') * x'))).
(x' * y) * ((x' * y) * ((C * (y' * x'')) * x)) = C * (x' * (y * x)).
((x * (y' * z')) * C') * (z * y) = (z * y) * (C' * ((y' * z') * x)).
(x' * y') * (C' * (y * (x * y))) = y * ((x * ((y * x)' * C')) * y).
((x' * (C' * (C' * y'))) * z') * ((z * (C * (y * (x * C)))) * u) = u.
x * ((y * ((x * y)' * C')) * x) = x' * ((x * y') * (y * (x * C'))).
x' * ((x * y') * (y * (x * C'))) = x * ((y * ((x * y)' * C')) * x).
((x' * (C' * (y' * C'))) * z') * ((z * (C * (y * (x * C)))) * u) = u.
x' * (y' * ((y * x) * (x * C'))) = x * ((y * ((x * y)' * C')) * x).
((x' * (C' * ((C' * C')' * C'))) * (C * y)') * ((C' * (y * (C * (C * (C' * (x * C)))))) * z) = z.
x' * (y * (C' * (y' * (x * x)))) = x * ((y * ((x * y)' * C')) * x).
x' * (y * (C' * (y' * (x * x)))) = x * ((y * ((y' * x') * C')) * x).
(x * (y * (z * C))) * (C * (C' * z')) = (C * z) * (C * (((z * C)' * x) * y)).
(C' * x') * ((x * y) * (y' * C)) = (C * x') * (y * ((y' * C') * x)).
(x' * y) * ((x' * y) * ((C * (y' * x)) * x)) = C * (x' * (y * x)).
(x' * y) * ((x' * y) * (y' * (x * (x * C)))) = C * (x' * (y * x)).
(x' * y) * (y * ((y' * x') * (x * (x * C)))) = C * (x' * (y * x)).
(x' * y) * (y * (x' * ((x * y') * (x * C)))) = C * (x' * (y * x)).
(x' * y) * (y * (x' * (x * ((y' * C) * x)))) = C * (x' * (y * x)).
(x' * y) * (y * ((y' * C) * x)) = C * (x' * (y * x)).
C * (x' * (y * x)) = y * ((y' * x') * (C * (y * x))).
x * ((x' * y') * (C * (x * y))) = C * (y' * (x * y)).
x * (C * K(x,y)) = C * (y' * (x * y)).
C * (x' * (y * x)) = y * (C * K(y,x)).
C * (x' * (y * x)) = y * (C * (y' * (x' * (y * x)))).
x * (C * (x' * (y' * (x * y)))) = C * (y' * (x * y)).
x' * (C * (y' * (x * y))) = C * (x' * (y' * (x * y))).
C' * (C' * (C * (x' * (y' * (x * y))))) = (x' * C') * (y' * (x * y)).
(C' * (x * (y' * z'))) * (z * y) = (z * y) * (C' * ((y' * z') * x)).
x' * (y * (C' * (y' * (x * x)))) = x * ((y * (C' * (y' * x'))) * x).
(C' * x') * ((x * y) * (y' * C)) = C' * (x * (y * ((C * y') * x'))).
x' * (y * (C' * (y' * (x * x)))) = ((x * y) * C') * y'.
x' * (y * (C' * (y' * (x * x)))) = (C' * (x * y)) * y'.
x' * (y * (C' * (y' * (x * x)))) = y * ((y' * C') * x).
x * (y * ((y' * C') * x)) = y * (C' * (y' * (x * x))).
x * (C' * (x' * (y * y))) = y * (x * ((x' * C') * y)).
(x * y) * (z * (C' * (z' * (y' * y')))) = y * ((y' * x) * (z * ((z' * C') * y'))).
(x' * C') * ((x * y) * (y' * C)) = C' * (x * (y * ((C * y') * x'))).
(x' * C') * (y * ((y' * x) * C)) = C' * (x * (y * ((C * y') * x'))).
C' * (x * (y * ((C * y') * x'))) = C * (x' * ((y * C') * (y' * x))).
C' * (x * (y * ((C * y') * x'))) = C * (x' * (y * ((y' * C') * x))).
((x * C)' * y') * (C * ((y * (x * C)) * y)) = ((y * (x * C)) * C) * (x' * C').
C' * ((x * y) * (((C * y') * x') * (x * y))) = (x * y) * a(x,y,C').
C' * ((x * y) * (x' * ((x * (C * y')) * y))) = (x * y) * a(x,y,C').
C' * ((x * y) * (x' * (y * ((y' * C) * x)))) = (x * y) * a(x,y,C').
C' * (x * ((y * x') * (y * ((y' * C) * x)))) = (x * y) * a(x,y,C').
C' * (x * ((y * x') * (y * ((y' * C) * x)))) = (x * y) * (C * ((y' * (x' * C')) * (x * y))).
(x * y) * (C * ((y' * (x' * C')) * (x * y))) = C' * (x * ((y * x') * (y * ((y' * C) * x)))).
(x * C') * ((x' * C') * y) = C' * (x * ((x' * y) * C')).
(x * C') * ((x' * C') * y) = C' * (x * (C' * (x' * y))).
(x * (y' * (z' * u))) * (z'' * y'') = (x * (y' * z')) * ((u * z) * y).
(x * (y * (z' * C))) * (C * (C' * z)) = (C * z') * (C * (((z' * C)' * x) * y)).
C' * (x' * (y' * (x * y))) = (x' * C') * (y' * (x * y)).
(x' * C') * (y' * (x * y)) = C' * (x' * (y' * (x * y))).
(x' * y') * (C * (y * ((x * C') * y))) = (y * x) * ((C * (y * x)') * (y * C')).
(C' * (x * ((x' * C') * y))) * y' = y * (x * ((x' * (C' * C')) * y')).
(x * (y' * C')) * (C * (C * (y * z))) = C * (y' * ((((y * C) * x) * C') * z)).
((x' * C') * y') * (C * ((y * (x * C)) * y)) = ((y * (x * C)) * C) * (x' * C').
(x * (y' * (z' * u))) * (z * y'') = (x * (y' * z')) * ((u * z) * y).
(x * (y' * (z' * u))) * (z * y) = (x * (y' * z')) * ((u * z) * y).
x * (y * ((y' * (C' * C')) * x')) = (C' * x) * ((x' * y) * (y' * C')).
(C' * x) * ((x' * y) * (y' * C')) = x * (y * ((y' * (C' * C')) * x')).
(x * (y' * C')) * (C * (C * (y * z))) = C * (y' * ((C * (y * (x * C'))) * z)).
(x * C') * ((x' * y) * (y' * C')) = x * (y * ((y' * (C' * C')) * x')).
(x * C') * (y * (C' * (y' * x'))) = x * (y * ((y' * (C' * C')) * x')).
(x * C') * (y * (C' * (y' * x'))) = x * (y * (C' * (y' * (x' * C')))).
((((x * y)' * (x' * y')') * C') * z') * ((z * C) * ((x' * y') * (x * y))) = 1.
(((x * x)' * y') * C') * ((y * (x * x)) * x') = (y * (x * x))' * (y * (x * C')).
(x * y) * (C * ((x * y) * (C' * ((y' * x') * y')))) = C * (y * ((y' * x) * C')).
C * (x' * ((y * C)' * (x * (y * C)))) = C' * (((C * x') * y') * (x * (y * C))).
C' * (((C * x') * y') * (x * (y * C))) = C * (x' * ((y * C)' * (x * (y * C)))).
(x * (y * (z' * C))) * z = (C * z') * (C * (((z' * C)' * x) * y)).
(C * x') * (C * (((x' * C)' * y) * z)) = (y * (z * (x' * C))) * x.
(C * x') * (C * (((C' * x'') * y) * z)) = (y * (z * (x' * C))) * x.
(C * x') * (C * (((C' * x) * y) * z)) = (y * (z * (x' * C))) * x.
(C * x') * (C * (((x * C') * y) * z)) = (y * (z * (x' * C))) * x.
(x * (y * (z' * C))) * z = C * (C * (z' * (((z * C') * x) * y))).
C * (C * (x' * (((x * C') * y) * z))) = (y * (z * (x' * C))) * x.
(x * (y * (z' * C))) * z = (x * z') * (C * (z * y)).
(C' * (x * (x * (y' * C)))) * y = (x * y') * (C * (y * (x * C'))).
(C * (x * (C' * (x * y')))) * y = (x * y') * (C * (y * (x * C'))).
(x * y') * (C * (y * (x * C'))) = (y' * C') * ((y * (x * C)) * x).
(x' * C') * ((x * (y * C)) * y) = (y * x') * (C * (x * (y * C'))).
(x' * C') * (C * (x * (y * y))) = (y * x') * (C * (x * (y * C'))).
(x * y') * (C * (y * (x * C'))) = C * (y * ((y' * C') * (x * x))).
(x * y) * ((C * (x * y)') * (x * C')) = x' * ((x * y') * ((y * C') * (x * C))).
((x' * C') * y') * (C * (y * ((x * C) * y))) = ((y * (x * C)) * C) * (x' * C').
C' * (x' * ((C * (y' * x)) * (y * C))) = C * (x' * ((y * C)' * (x * (y * C)))).
(x * y) * ((C * (x * y)') * (x * C')) = x' * ((x * y') * (C * (y * (x * C')))).
((x' * C') * y') * (C * (y * ((x * C) * y))) = x * ((C * x') * y).
x * ((C * x') * y) = y' * ((y * (x' * C')) * ((x * C) * (y * C))).
x' * ((x * (y' * C')) * ((y * C) * (x * C))) = y * ((C * y') * x).
x' * ((x * (y' * C')) * (C * (C * (y * x)))) = y * ((C * y') * x).
x' * (C * (y' * ((C * (y * (x * C'))) * x))) = y * ((C * y') * x).
x' * (C * (y' * (C * ((y * C') * (x * x))))) = y * ((C * y') * x).
x' * (y * (C * (y' * (x * x)))) = y * ((C * y') * x).
x * (y * ((C * y') * x)) = y * (C * (y' * (x * x))).
x * (C * (x' * (y * y))) = y * (x * ((C * x') * y)).
x' * (C' * (y * (C * (y' * (x * x))))) = x * ((x' * C') * (y * ((C * y') * x))).
x * (x * (C' * (y * (C * (y' * (x' * x')))))) = (x * C') * (y * ((C * y') * x')).
C' * (x' * (C * (((y' * x) * y) * C))) = C * (x' * ((y * C)' * (x * (y * C)))).
(x * y) * ((C * (y' * x')) * (x * C')) = x' * ((x * y') * (C * (y * (x * C')))).
C' * (x' * (C * ((y' * (x * y)) * C))) = C * (x' * ((y * C)' * (x * (y * C)))).
C * (x' * ((y * C)' * (x * (y * C)))) = (x' * C) * (y' * (x * y)).
C * (x' * (y' * (x * y))) = (x' * C) * (y' * (x * y)).
(x' * C) * (y' * (x * y)) = C * (x' * (y' * (x * y))).
(x * ((y' * (z' * (y * z)))' * C)) * (y' * (z' * (y * z))) = (x * (y' * (z' * (y * z)))') * ((y' * C) * (z' * (y * z))).
x * (C * (x' * (y' * (x * y)))) = x * ((C * x') * (y' * (x * y))).
x * ((C * x') * (y' * (x * y))) = x * (C * (x' * (y' * (x * y)))).
x * ((C * x') * (y' * (x * y))) = C * (y' * (x * y)).
x' * (C * (y' * (x * y))) = (C * x') * (y' * (x * y)).
(C * x') * (y' * (x * y)) = x' * (C * (y' * (x * y))).
x * (C' * (x' * (x' * (C * (y' * (x * y)))))) = x' * (y' * (x * y)).
x * (C * (x' * (C' * (x' * (y' * (x * y)))))) = x' * (y' * (x * y)).
x' * (y' * (x * y)) = C * (x' * ((y' * (x * y)) * C')).
C * (x' * ((y' * (x * y)) * C')) = x' * (y' * (x * y)).
C * (x' * (C' * (y' * (x * y)))) = x' * (y' * (x * y)).
C' * (C' * (x * (y' * (z' * (y * z))))) = (x * C') * (y' * (C' * (z' * (y * z)))).
(x * C') * (y' * (C' * (z' * (y * z)))) = C' * (C' * (x * (y' * (z' * (y * z))))).
C * (x' * (y' * ((x * C') * y))) = x' * (y' * (x * y)).
C' * (C' * (x * (y' * (z' * (y * z))))) = (x * C') * (y' * (z' * ((y * C') * z))).
(x * C') * (y' * (z' * ((y * C') * z))) = C' * (C' * (x * (y' * (z' * (y * z))))).
(x * y) * (((x * (z * x')) * C) * (x * y)) = x * (y * ((x' * (x * (x * (z * C)))) * y)).
((((x' * y') * (y' * x')') * C') * z') * ((z * C) * ((y' * x') * (y * x))) = 1.
(((x' * x') * y') * C') * ((y * (x * x)) * x') = (y * (x * x))' * (y * (x * C')).
(x * y) * (C * ((x * y) * (C' * (y' * (x' * y'))))) = C * (y * ((y' * x) * C')).
x' * (C * (y * ((y' * C') * (x * x)))) = x * ((x' * C') * (y * ((C * y') * x))).
(x * y) * (C * ((C' * (y' * x')) * x)) = x' * ((x * y') * (C * (y * (x * C')))).
(x * y) * (((x * (z * x')) * C) * (x * y)) = x * (y * ((x * (z * C)) * y)).
(x * y) * (((x * (y * x')) * C) * (x * y)) = x * (y * (C * (x * (y * y)))).
(x * y) * ((C * (x * (y * x'))) * (x * y)) = x * (y * (C * (x * (y * y)))).
(x * y) * (x' * (((x * C) * (x * y)) * y)) = x * (y * (C * (x * (y * y)))).
(x * y) * (x' * ((x * (x * (y * C))) * y)) = x * (y * (C * (x * (y * y)))).
(x * y) * (x' * (C * (x * (x * (y * y))))) = x * (y * (C * (x * (y * y)))).
(x * y) * ((x * C) * (y * y)) = x * (y * (C * (x * (y * y)))).
(x * (y * (C * (x * (y * y))))) * y' = ((x * y) * ((x * y) * y)) * (C * y').
((x * y) * ((x * y) * y)) * (C * y') = (x * y) * ((C * (x * (y * y))) * y').
((x * y) * ((x * y) * y)) * (C * y') = (x * y) * (x * (y * C)).
(x * (y * (x * (y * y)))) * (C * y') = (x * y) * (x * (y * C)).
(x * y) * (x * (y * C)) = (C * (x * (y * x))) * y.
(C * (x * (y * x))) * y = (x * y) * (x * (y * C)).
(x * y) * (x * (y * C)) = (C * x) * (y * (x * y)).
(C * x) * (y * (x * y)) = (x * y) * (x * (y * C)).
(x * y) * (x * (y * C)) = x * (y * (C * (x * y))).
(x * y) * (x * (C * y)) = x * (y * (C * (x * y))).
((x * (C' * (y' * C'))) * (y * C)) * x = (x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * (y' * C'))) * (y * C)))).
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * (y' * C'))) * (y * C)))) = ((x * (C' * (y' * C'))) * (y * C)) * x.
(x * (C' * (x' * y))) * y = x * ((C' * (x' * y)) * (C * (x * (C' * (x' * y))))).
x * ((C' * (x' * y)) * (C * (x * (C' * (x' * y))))) = (x * (C' * (x' * y))) * y.
(x * y) * (C * (y * ((y' * x) * (x' * (y' * C'))))) = C * (y * ((y' * x) * C')).
x' * (C * (y * ((y' * C') * (x * x)))) = x * (C * (x' * (y * (C' * (y' * x))))).
(x * y) * (C * (x * (C' * (x' * y')))) = x' * ((x * y') * (C * (y * (x * C')))).
x * (C' * ((C * (x' * y)) * (x * (C' * (x' * y))))) = (x * (C' * (x' * y))) * y.
(x * y) * (C * (y * (x * ((x' * y') * (y' * C'))))) = C * (y * ((y' * x) * C')).
(x * y) * (C * (x * (C' * (x' * y')))) = x' * (C * (y * ((y' * C') * (x * x)))).
x * (C' * (x' * ((y * (x * C)) * (C' * (x' * y))))) = (x * (C' * (x' * y))) * y.
(x * y) * (C * (x * (C' * (x' * y')))) = x * (C * (x' * (y * (C' * (y' * x))))).
x * (C' * (x' * (C * (((y * C') * x) * (x' * y))))) = (x * (C' * (x' * y))) * y.
x * (C' * (x' * (C * (x * ((x' * (y * C')) * y))))) = (x * (C' * (x' * y))) * y.
x * (C' * (x' * (C * (x * (C' * (x' * (y * y))))))) = (x * (C' * (x' * y))) * y.
x * (C' * (x * ((C * x') * (C' * (x' * (y * y)))))) = (x * (C' * (x' * y))) * y.
x * (C' * (x * (C * ((x' * C') * (x' * (y * y)))))) = (x * (C' * (x' * y))) * y.
x * (C' * (x * (C * (x' * (x' * ((y * y) * C')))))) = (x * (C' * (x' * y))) * y.
x * (C' * (x * (C * (x' * (x' * (C' * (y * y))))))) = (x * (C' * (x' * y))) * y.
x * (C' * ((x' * C) * (C' * (y * y)))) = (x * (C' * (x' * y))) * y.
x * (C' * (C * ((C' * x') * (y * y)))) = (x * (C' * (x' * y))) * y.
x * (C' * (C * ((x' * C') * (y * y)))) = (x * (C' * (x' * y))) * y.
x * ((x' * C') * (y * y)) = (x * (C' * (x' * y))) * y.
(x * (C' * (x' * y))) * y = x * ((x' * C') * (y * y)).
x' * (x * ((x' * C) * (y * (C' * (y' * x))))) = x * (C * (y * ((y' * C') * x'))).
x * (x * (C * (y * ((y' * C') * (x' * x'))))) = (x * C') * (y * ((C * y') * x')).
((((x' * y') * (x'' * y'')) * C') * z') * ((z * C) * ((y' * x') * (y * x))) = 1.
((x' * (x' * y')) * C') * ((y * (x * x)) * x') = (y * (x * x))' * (y * (x * C')).
x' * (x * (C' * (x' * ((y * C) * (y' * x))))) = x * (C * (y * ((y' * C') * x'))).
x * (x * (C * (y * ((y' * C') * (x' * x'))))) = C * (x * (y * (C' * (y' * x')))).
(C' * (x' * (x' * y'))) * ((y * (x * x)) * x') = (y * (x * x))' * (y * (x * C')).
x' * (x * (C' * (x' * (y * ((C * y') * x))))) = x * (C * (y * ((y' * C') * x'))).
(C' * (x' * (x' * y'))) * (y * x) = (y * (x * x))' * (y * (x * C')).
(x * (y * y))' * (x * (y * C')) = (x * y) * (C' * ((y' * x') * y')).
(x * (y * y))' * (x * (y * C')) = (x * y) * (C' * (y' * (x' * y'))).
(x * (y * y))' * (x * (y * C')) = y * ((y' * x) * (x' * (y' * C'))).
(x * (y * y))' * (x * (y * C')) = y * (x * ((x' * y') * (y' * C'))).
((x * x)' * y') * (y * (x * C')) = x * (y * ((y' * x') * (x' * C'))).
((x' * x') * y') * (y * (x * C')) = x * (y * ((y' * x') * (x' * C'))).
x * (y * ((y' * x') * (x' * C'))) = y' * ((y * (x' * x')) * (x * C')).
x' * ((x * (y' * y')) * (y * C')) = y * (x * ((x' * y') * (y' * C'))).
x' * (y' * ((y * (x * y')) * C')) = y * (x * ((x' * y') * (y' * C'))).
x' * (y * ((y' * C') * (x * y'))) = y * (x * ((x' * y') * (y' * C'))).
x' * (y * (y' * ((C' * x) * y'))) = y * (x * ((x' * y') * (y' * C'))).
x' * (y * (y' * ((x * C') * y'))) = y * (x * ((x' * y') * (y' * C'))).
x' * ((x * C') * y') = y * (x * ((x' * y') * (y' * C'))).
x * (y * ((y' * x') * (x' * C'))) = y' * ((y * C') * x').
x * (y * ((y' * x') * (x' * C'))) = y * (C' * (y' * x')).
(x * y) * (C * (x * (C' * (x' * y')))) = C * (y * ((y' * x) * C')).
C * (x * ((x' * y) * C')) = y * (C * (y' * (x * (C' * (x' * y))))).
x * (C * (x' * (y * (C' * (y' * x))))) = C * (y * ((y' * x) * C')).
x * (C * (x' * (y * (C' * (y' * x))))) = C * (y * (C' * (y' * x))).
x * (C * (y * (x * (C' * (x' * y'))))) = C * (y * (C' * (y' * x))).
x' * (x * (C' * (x * (y * (C * (y' * x')))))) = x * (C * (y * ((y' * C') * x'))).
x * (C * ((y' * C') * (C' * ((y * C) * z)))) = x * (y * ((((y * C)' * C') * z) * (C * C))).
(x * C') * (C' * (y' * (z' * (y * z)))) = (x * C') * (y' * (C' * (z' * (y * z)))).
(x * C') * (C' * (y' * (z' * (y * z)))) = (x * C') * (y' * (z' * ((y * C') * z))).
((((x' * y') * (x * y'')) * C') * z') * ((z * C) * ((y' * x') * (y * x))) = 1.
((((x' * y') * (x * y)) * C') * z') * ((z * C) * ((y' * x') * (y * x))) = 1.
((C' * ((x' * y') * (x * y))) * z') * ((z * C) * ((y' * x') * (y * x))) = 1.
((C' * (x' * (y' * (x * y)))) * z') * ((z * C) * ((y' * x') * (y * x))) = 1.
((C' * (x' * (y' * (x * y)))) * z') * ((z * C) * (y' * (x' * (y * x)))) = 1.
1 = (C' * x') * ((x * ((y' * (z' * (y * z))) * C)) * (z' * (y' * (z * y)))).
(C' * x') * ((x * ((y' * (z' * (y * z))) * C)) * (z' * (y' * (z * y)))) = 1.
(x' * C') * ((x * ((y' * (z' * (y * z))) * C)) * (z' * (y' * (z * y)))) = 1.
(x' * C') * ((x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y)))) = 1.
x * (C * ((y' * C') * (C * (y * (z * C'))))) = x * (y * ((((y * C)' * C') * z) * (C * C))).
x * (C * (C * (y * ((y' * C') * (z * C'))))) = x * (y * ((((y * C)' * C') * z) * (C * C))).
x * (C * ((y * C') * (y' * z))) = x * (y * ((((y * C)' * C') * z) * (C * C))).
x * (y * ((((y * C)' * C') * z) * (C * C))) = x * (C * ((y * C') * (y' * z))).
x * (y * ((((y * C)' * C') * z) * (C * C))) = x * (C * (y * ((y' * C') * z))).
x * (y * ((((C' * y') * C') * z) * (C * C))) = x * (C * (y * ((y' * C') * z))).
x * (y * ((C' * (y' * (C' * z))) * (C * C))) = x * (C * (y * ((y' * C') * z))).
x * (y * ((C' * (y' * (z * C'))) * (C * C))) = x * (C * (y * ((y' * C') * z))).
x * (y * (C * ((C' * (y' * (z * C'))) * C))) = x * (C * (y * ((y' * C') * z))).
x * (y * (C * (C * (C' * (y' * (z * C')))))) = x * (C * (y * ((y' * C') * z))).
x * (y * (C * (y' * (z * C')))) = x * (C * (y * ((y' * C') * z))).
x * (C * (y * ((y' * C') * z))) = x * (y * (C * (y' * (z * C')))).
x * (C * (y * ((y' * C') * z))) = x * (y * (C * (y' * (C' * z)))).
(x * y) * (C * ((y' * (x' * C')) * (x * y))) = C' * (x * (y * ((x' * y') * (C * (y * x))))).
(x * y) * (C * ((y' * (x' * C')) * (x * y))) = C' * (x * (y * C)).
(x * y) * (C * ((y' * (x' * C')) * (x * y))) = C * ((x * C') * y).
(x * y) * (C * (x' * ((C' * (x * y')) * y))) = C * ((x * C') * y).
(x * y) * (C * (x' * (y * (C' * (y' * x))))) = C * ((x * C') * y).
(x * y) * (C * (x * (y * ((y' * C') * x')))) = C * ((x * C') * y).
(x' * y') * (C * ((y * C') * x)) = C * (y * (x * ((x' * C') * y'))).
(x' * y') * (C * ((y * C') * x)) = C * (x * (y * (C' * (y' * x')))).
((C' * (x' * (y' * (x * y))))' * z') * (C * ((z * C') * (x' * (y' * ((x * C') * y))))) = C * ((C' * (x' * (y' * (x * y)))) * (z * (C' * (z' * (C' * (x' * (y' * (x * y))))')))).
C * (x * (x * (C * (((y * C') * (y' * x')) * x')))) = x * (x * (x' * (y * (C * (y' * x'))))).
C * (x * (x * (C * ((y * (C' * (y' * x'))) * x')))) = x * (x * (y * (C * (y' * (x' * x'))))).
C * (x * (x * (C * ((y * ((y' * C') * x')) * x')))) = x * (x * (x' * (y * (C * (y' * x'))))).
C * (x * (x * (C * (y * ((y' * C') * (x' * x')))))) = x * (x * (y * (C * (y' * (x' * x'))))).
C * (C * (x * (y * (C' * (y' * x'))))) = x * (x * (y * (C * (y' * (x' * x'))))).
C * (C * (x * (y * (C' * (y' * x'))))) = x * (y * ((C * y') * x')).
C' * (x * (y * ((C * y') * x'))) = C * (x * (y * (C' * (y' * x')))).
C' * (x * (y * (C * (y' * x')))) = C * (y * (x * (C' * (x' * y')))).
C * (x * (y * (C' * (y' * x')))) = C * (x' * (y * ((y' * C') * x))).
C * (x' * (y * ((y' * C') * x))) = C * (x * (y * (C' * (y' * x')))).
x' * (x * (C * (y * (x * (C' * (x' * y')))))) = x * (C * (y * ((y' * C') * x'))).
x' * (C' * (y * ((y' * x) * (x * C)))) = x * (C * (x * (y * (C' * (y' * x'))))).
x' * (C * (y * (C' * (y' * x)))) = x * (C * (y * ((y' * C') * x'))).
x' * (C * (y * (C' * (y' * x)))) = x * (y * (C * (y' * (x' * C')))).
(x * (y * C')) * (((z * C) * (y' * (x * C)')) * C) = C' * (C * (((x * C) * y) * (z * ((x * C) * y)'))).
x * (x * (y * ((y' * (x' * C')) * x'))) = C' * (x * (y * (C * (y' * (x' * C'))))).
C' * (x * (y * (C * (y' * (x' * C'))))) = x * (x * (y * ((y' * (x' * C')) * x'))).
C' * (x * (y * (C * (y' * (x' * C'))))) = x * (x * (y * (C' * (y' * (x' * x'))))).
C' * (x * (y * (C * (y' * (x' * C'))))) = x * (y * ((y' * C') * x')).
x * (y * ((y' * C') * x')) = C * ((x * C') * (y * ((y' * C') * x'))).
C * ((x * C') * (y * ((y' * C') * x'))) = x * (y * ((y' * C') * x')).
C * (x * (y * ((y' * C') * x'))) = x * (C * (y * ((y' * C') * x'))).
C * (x * (y * ((y' * C') * x'))) = x * (y * (C * (y' * (C' * x')))).
((x' * (C' * ((C'' * C'') * C'))) * (C * y)') * ((C' * (y * (C * (C * (C' * (x * C)))))) * z) = z.
(x * (y * C')) * (((z * C) * (y' * (C' * x'))) * C) = C' * (C * (((x * C) * y) * (z * ((x * C) * y)'))).
(x * C') * (y * (z * (C * (z' * y)))) = C * (x * (z * ((z' * (y * C')) * ((y * C') * C)))).
C * (x * (y * ((y' * (z * C')) * ((z * C') * C)))) = (x * C') * (z * (y * (C * (y' * z)))).
C * (x * (y * ((y' * (z * C')) * z))) = (x * C') * (z * (y * (C * (y' * z)))).
(x * C') * (y * (z * (C * (z' * y)))) = C * (x * (z * ((z' * (y * C')) * y))).
(x * C') * (y * (z * (C * (z' * y)))) = C * (x * (z * (C' * (z' * (y * y))))).
C * (x' * (y * (C' * (y' * (x * x))))) = x' * ((y * (C * (y' * x))) * (x * C')).
x' * ((y * (C * (y' * x))) * (x * C')) = C * (x' * (y * (C' * (y' * (x * x))))).
x' * ((y * (C * (y' * x))) * (x * C')) = C * (y * ((y' * C') * x)).
x' * (C * (((y * C') * (y' * x)) * x)) = C * (y * ((y' * C') * x)).
x' * (C * ((y * ((y' * C') * x)) * x)) = C * (y * ((y' * C') * x)).
C * (x * ((y * (C' * (y' * ((C * x)' * C')))) * C)) = y * ((C * (C * x)) * (((C * (C * x))' * C') * y')).
((x' * (C' * ((C * C'') * C'))) * (C * y)') * ((C' * (y * (C * (C * (C' * (x * C)))))) * z) = z.
((x' * (C' * C)) * (C * y)') * ((C' * (y * (C * (C * (C' * (x * C)))))) * z) = z.
((x' * 1) * (C * y)') * ((C' * (y * (C * (C * (C' * (x * C)))))) * z) = z.
(x' * (C * y)') * ((C' * (y * (C * (C * (C' * (x * C)))))) * z) = z.
(x' * (y' * C')) * ((C' * (y * (C * (C * (C' * (x * C)))))) * z) = z.
(x' * (C' * y')) * ((C' * (y * (C * (C * (C' * (x * C)))))) * z) = z.
(x' * (C' * y')) * ((C' * (y * (C * (C * x)))) * z) = z.
(x' * (C' * y')) * (((C * y) * x) * z) = z.
(x * (y' * (C' * z'))) * ((C * z) * y) = ((y' * (C' * z')) * ((C * z) * y)) * (x * ((y' * (C' * z')) * ((C * z) * y))).
((x' * (C' * y')) * ((C * y) * x)) * (z * ((x' * (C' * y')) * ((C * y) * x))) = (z * (x' * (C' * y'))) * ((C * y) * x).
(x * (y * C')) * ((C' * (z * ((y' * C) * x'))) * C) = C' * (C * (((x * C) * y) * (z * ((x * C) * y)'))).
(x * (y * C')) * (C * (C' * (z * ((y' * C) * x')))) = C' * (C * (((x * C) * y) * (z * ((x * C) * y)'))).
(x * (y * C')) * (z * ((y' * C) * x')) = C' * (C * (((x * C) * y) * (z * ((x * C) * y)'))).
C' * (C * (((x * C) * y) * (z * ((x * C) * y)'))) = (x * (y * C')) * (z * ((y' * C) * x')).
C' * (C * (((x * C) * y) * (z * (y' * (x * C)')))) = (x * (y * C')) * (z * ((y' * C) * x')).
C' * (C * (((x * C) * y) * (z * (y' * (x' * C'))))) = (x * (y * C')) * (z * ((y' * C) * x')).
(x * (y * C')) * (z * ((y' * C) * x')) = ((x * C) * y) * (z * (y' * (x' * C'))).
((x * C) * y) * (z * (y' * (x' * C'))) = (x * (y * C')) * (z * ((y' * C) * x')).
C * (x * ((y * (C' * (y' * ((x' * C') * C')))) * C)) = y * ((C * (C * x)) * (((C * (C * x))' * C') * y')).
C * (x * ((y * (C' * (y' * ((C' * x') * C')))) * C)) = y * ((C * (C * x)) * (((C * (C * x))' * C') * y')).
C * (x * ((y * (C' * (y' * (C' * (C' * x'))))) * C)) = y * ((C * (C * x)) * (((C * (C * x))' * C') * y')).
C * (x * (C * (y * (C' * (y' * (C' * (C' * x'))))))) = y * ((C * (C * x)) * (((C * (C * x))' * C') * y')).
C * (x * (y * (C' * (y' * (C' * x'))))) = y * ((C * (C * x)) * (((C * (C * x))' * C') * y')).
x * ((C * (C * y)) * (((C * (C * y))' * C') * x')) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * ((C * (C * y)) * ((((C * y)' * C') * C') * x')) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * ((C * (C * y)) * ((((y' * C') * C') * C') * x')) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * ((C * (C * y)) * ((((C' * y') * C') * C') * x')) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * ((C * (C * y)) * (((C' * (C' * y')) * C') * x')) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * ((C * (C * y)) * ((C' * (C' * (C' * y'))) * x')) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * ((C * (C * y)) * (C' * ((C' * y') * (x' * C')))) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * ((C * (C * y)) * (C' * (C' * ((y' * x') * C')))) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * ((C * (C * y)) * (C' * (C' * (C' * (y' * x'))))) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * (C * (((C * y) * C') * (C' * (C' * (y' * x'))))) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * (C * ((C' * (C * y)) * (C' * (C' * (y' * x'))))) = C * (y * (x * (C' * (x' * (C' * y'))))).
x * (C * (y * (C' * (C' * (y' * x'))))) = C * (y * (x * (C' * (x' * (C' * y'))))).
C * (x * (y * (C' * (y' * (C' * x'))))) = y * (C * (x * (C' * (C' * (x' * y'))))).
C * (x * (y * (C' * (y' * (C' * x'))))) = y * ((x * C') * (x' * y')).
C * (x * (y * (C' * (y' * (C' * x'))))) = y * (x * ((C' * x') * y')).
(((x * C) * y) * (z * (y * ((y' * (x * C)) * (x' * C'))))) * (y' * (x' * C')) = ((x * C) * y) * (z * (y' * (x' * C'))).
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * (y' * C'))) * (y * C)))) = ((x * (C' * y')) * ((C' * y) * C)) * x.
((C' * x') * (((C * x) * y') * y)) * (z * ((y' * (C' * x')) * ((C * x) * y))) = (z * (y' * (C' * x'))) * ((C * x) * y).
(((x * C) * y) * (z * (y * y'))) * (y' * (x' * C')) = ((x * C) * y) * (z * (y' * (x' * C'))).
(((x * C) * y) * (z * 1)) * (y' * (x' * C')) = ((x * C) * y) * (z * (y' * (x' * C'))).
(((x * C) * y) * z) * (y' * (x' * C')) = ((x * C) * y) * (z * (y' * (x' * C'))).
(((x * C) * y) * z) * (y' * (x' * C')) = (x * (y * C')) * (z * ((y' * C) * x')).
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * (y' * C'))) * (y * C)))) = ((x * (y' * C')) * ((C' * y) * C)) * x.
((C' * x') * (C * x)) * (y * ((z' * (C' * x')) * ((C * x) * z))) = (y * (z' * (C' * x'))) * ((C * x) * z).
(x * ((C * x') * C')) * (y * ((z' * (C' * x')) * ((C * x) * z))) = (y * (z' * (C' * x'))) * ((C * x) * z).
(x * (C' * (C * x'))) * (y * ((z' * (C' * x')) * ((C * x) * z))) = (y * (z' * (C' * x'))) * ((C * x) * z).
(x * x') * (y * ((z' * (C' * x')) * ((C * x) * z))) = (y * (z' * (C' * x'))) * ((C * x) * z).
1 * (x * ((y' * (C' * z')) * ((C * z) * y))) = (x * (y' * (C' * z'))) * ((C * z) * y).
1 * (x * ((C' * y') * (((C * y) * z') * z))) = (x * (z' * (C' * y'))) * ((C * y) * z).
1 * (x * ((C' * y') * (C * y))) = (x * (z' * (C' * y'))) * ((C * y) * z).
(x * (y' * (C' * z'))) * ((C * z) * y) = 1 * (x * ((C' * z') * (C * z))).
(x * (y' * (C' * z'))) * ((C * z) * y) = 1 * (x * (z * ((C * z') * C'))).
(x * (y' * (C' * z'))) * ((C * z) * y) = 1 * (x * (z * (C' * (C * z')))).
(x * (y' * (C' * z'))) * ((C * z) * y) = 1 * (x * (z * z')).
(x * (y' * (C' * z'))) * ((C * z) * y) = 1 * (x * 1).
(x * (y' * (C' * z'))) * ((C * z) * y) = 1 * x.
(x * (y' * (C' * z'))) * ((C * z) * y) = x.
(x * ((y * (C * (y' * (C * z)')))' * (C' * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * ((y * (C * (y' * (z' * C'))))' * (C' * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * ((y * (C * (y' * (C' * z'))))' * (C' * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * (((C * (y' * (C' * z')))' * y') * (C' * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * ((((y' * (C' * z'))' * C') * y') * (C' * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * (((((C' * y')' * z'') * C') * z') * (C' * y'))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (((((y'' * C'') * z'') * C') * z') * (C' * y'))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (((((y * C'') * z'') * C') * z') * (C' * y'))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (((((y * C) * z'') * C') * z') * (C' * y'))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (((((C * y) * z'') * C') * z') * (C' * y'))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (((((C * y) * z) * C') * z') * (C' * y'))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (((C * (y * (z * C'))) * z') * (C' * y'))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (((C * y) * (C' * (y' * z))) * (C' * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * ((C * ((y * C') * (y' * z))) * (C' * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * ((C * (y * ((y' * C') * z))) * (C' * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * (C * (((y * ((y' * C') * z)) * C') * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * (C * ((C' * (y * ((y' * C') * z))) * z'))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * (C * ((C' * y) * ((y' * z) * (z' * C'))))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (C * ((y * C') * ((y' * z) * (z' * C'))))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (C * ((y * C') * (z * (C' * (z' * y')))))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (C * (y * (z * (C' * (z' * (y' * C'))))))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (C * (y * (z * (C' * (z' * (C' * y'))))))) * ((C * y)' * (z * ((C * z') * (C * y)))) = x.
(x * (y * (z * ((C' * z') * y')))) * ((C * z)' * (y * ((C * y') * (C * z)))) = x.
(x * (y * (z * ((C' * z') * y')))) * ((z' * C') * (y * ((C * y') * (C * z)))) = x.
(x * (y * (z * ((C' * z') * y')))) * ((C' * z') * (y * ((C * y') * (C * z)))) = x.
(x * (y * (z * ((C' * z') * y')))) * ((C' * z') * (y * (C * (C * (y' * z))))) = x.
(x * (y * (z * ((C' * z') * y')))) * (C * (z' * (C * (y * (C' * (y' * z)))))) = x.
(x * (y * (z * ((C' * z') * y')))) * (C * (z * (y * (C * (y' * (z' * C')))))) = x.
(x * (y * (z * ((C' * z') * y')))) * (C * (z * (y * (C * (y' * (C' * z')))))) = x.
(x * (y * (z * ((C' * z') * y')))) * (C * (C * (z * (y * ((y' * C') * z'))))) = x.
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * (y' * C'))) * (y * C)))) = ((x * (y' * C')) * ((y * C') * C)) * x.
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * (y' * C'))) * (y * C)))) = ((x * (y' * C')) * y) * x.
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * (y' * C'))) * (y * C)))) = ((x * y') * (C' * y)) * x.
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * (y' * C'))) * (y * C)))) = ((x * y') * (y * C')) * x.
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * (y' * C'))) * (y * C)))) = (y * ((y' * C') * x)) * x.
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (C' * y')) * ((C' * y) * C)))) = (y * ((y' * C') * x)) * x.
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (y' * C')) * ((C' * y) * C)))) = (y * ((y' * C') * x)) * x.
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (y' * C')) * ((y * C') * C)))) = (y * ((y' * C') * x)) * x.
(x * (C' * (y' * C'))) * ((y * C) * (C * ((x * (y' * C')) * y))) = (y * ((y' * C') * x)) * x.
(x * (C' * (y' * C'))) * ((y * C) * (C * (y * ((y' * C') * x)))) = (y * ((y' * C') * x)) * x.
(x * (C' * (y' * C'))) * (C * (C * (y * (y * ((y' * C') * x))))) = (y * ((y' * C') * x)) * x.
(x * (C' * (y' * C'))) * (C * (C * (C' * (y * x)))) = (y * ((y' * C') * x)) * x.
(x * (C' * (y' * C'))) * (C * (y * x)) = (y * ((y' * C') * x)) * x.
(x * ((x' * C') * y)) * y = C' * ((C * ((y * C') * x')) * (x * y)).
C' * ((C * ((x * C') * y')) * (y * x)) = (y * ((y' * C') * x)) * x.
C' * (x' * (((x * C) * (y * C')) * y)) = (x * ((x' * C') * y)) * y.
C' * (x' * ((C * ((x * C') * y)) * y)) = (x * ((x' * C') * y)) * y.
C' * (x' * ((x * C') * (y * (y * C)))) = (x * ((x' * C') * y)) * y.
C' * (x' * (C * (x * ((y * C') * y)))) = (x * ((x' * C') * y)) * y.
C' * (x' * (C * (x * (y * (C' * y))))) = (x * ((x' * C') * y)) * y.
C' * (x' * (C * (x * (y * (y * C'))))) = (x * ((x' * C') * y)) * y.
C' * (x * ((C * x') * (y * (y * C')))) = (x * ((x' * C') * y)) * y.
C' * (x * (C * ((x' * C') * (y * y)))) = (x * ((x' * C') * y)) * y.
(x * ((x' * C') * y)) * y = C * ((x * C') * ((x' * C') * (y * y))).
C * ((x * C') * ((x' * C') * (y * y))) = (x * ((x' * C') * y)) * y.
C * (C' * (x * (C' * (x' * (y * y))))) = (x * ((x' * C') * y)) * y.
(x * ((x' * C') * y)) * y = x * (C' * (x' * (y * y))).
(x * ((C' * x') * y)) * y = x * (C' * (x' * (y * y))).
C * (x * (x * (C * (y * (C' * (y' * (x' * x'))))))) = x * (x * (x' * (y * (C * (y' * x'))))).
x' * (C * (y * (C' * (y' * (x * x))))) = C * (y * ((y' * C') * x)).
x' * (C' * (y * ((y' * x) * (x * C)))) = C * (y * ((y' * C') * x)).
C * (x * ((x' * C') * y)) = y * (C * (y * (x * (C' * (x' * y'))))).
x * (C * (x * (y * (C' * (y' * x'))))) = C * (y * ((y' * C') * x)).
(C' * (x' * (y' * (x * y)))) * (C * ((C' * (x' * (y' * (x * y)))) * (z * (C' * (z' * (C' * (x' * (y' * (x * y))))'))))) = C * (z * ((z' * C') * (x' * (C' * (y' * (x * y)))))).
C * (C * (x * (y * ((y' * C') * x')))) = x * (x * (x' * (y * (C * (y' * x'))))).
C * (C * (x * (y * ((y' * C') * x')))) = x * (y * (C * (y' * x'))).
(x * (y * (z * ((C' * z') * y')))) * (z * (y * (C * (y' * z')))) = x.
((x * (y * ((C' * y') * x')))' * (z * (x * (y * ((C' * y') * x'))))) * (y * (x * (C * (x' * y')))) = (x * (y * ((C' * y') * x')))' * z.
(x * (((y' * (z * y))' * z'') * C)) * (z' * (y' * (z * y))) = (x * (z' * (y' * (z * y)))') * ((z' * C) * (y' * (z * y))).
(x * ((((y * z)' * z'') * y'') * C)) * (y' * (z' * (y * z))) = (x * (y' * (z' * (y * z)))') * ((y' * C) * (z' * (y * z))).
(x * ((((y' * z') * y'') * z'') * C)) * (z' * (y' * (z * y))) = (x * (z' * (y' * (z * y)))') * ((z' * C) * (y' * (z * y))).
(x * ((((y' * z') * y) * z'') * C)) * (z' * (y' * (z * y))) = (x * (z' * (y' * (z * y)))') * ((z' * C) * (y' * (z * y))).
(x * (((y' * (z' * y)) * z'') * C)) * (z' * (y' * (z * y))) = (x * (z' * (y' * (z * y)))') * ((z' * C) * (y' * (z * y))).
(x * (((y' * z') * (y * z)) * C)) * (z' * (y' * (z * y))) = (x * (z' * (y' * (z * y)))') * ((z' * C) * (y' * (z * y))).
(x * ((y' * (z' * (y * z))) * C)) * (z' * (y' * (z * y))) = (x * (z' * (y' * (z * y)))') * ((z' * C) * (y' * (z * y))).
(x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))) = (x * (z' * (y' * (z * y)))') * ((z' * C) * (y' * (z * y))).
(x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))) = (x * ((y' * (z * y))' * z'')) * ((z' * C) * (y' * (z * y))).
(x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))) = (x * (((z * y)' * y'') * z'')) * ((z' * C) * (y' * (z * y))).
(x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))) = (x * (((y' * z') * y'') * z'')) * ((z' * C) * (y' * (z * y))).
(x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))) = (x * (((y' * z') * y) * z'')) * ((z' * C) * (y' * (z * y))).
(x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))) = (x * ((y' * (z' * y)) * z'')) * ((z' * C) * (y' * (z * y))).
(x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))) = (x * ((y' * z') * (y * z))) * ((z' * C) * (y' * (z * y))).
(x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))) = (x * (y' * (z' * (y * z)))) * ((z' * C) * (y' * (z * y))).
(x * (C * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))) = (x * (y' * (z' * (y * z)))) * (C * (z' * (y' * (z * y)))).
(x' * C') * ((x * (y' * (z' * (y * z)))) * (C * (z' * (y' * (z * y))))) = 1.
1 = C * (x' * (((x * (y' * (z' * (y * z)))) * C') * (z' * (y' * (z * y))))).
C * (x' * (((x * (y' * (z' * (y * z)))) * C') * (z' * (y' * (z * y))))) = 1.
C * (x' * ((C' * (x * (y' * (z' * (y * z))))) * (z' * (y' * (z * y))))) = 1.
(((x * C) * y) * (1 * z)) * ((x * C) * y)' = (C * (x * (y * (C * (x * y))))) * ((((x * C) * y)' * z) * ((x * C) * y)').
(C * (x * (y * (C * (x * y))))) * ((((x * C) * y)' * z) * ((x * C) * y)') = (((x * C) * y) * (1 * z)) * ((x * C) * y)'.
(C * (x * (y * (C * (x * y))))) * ((((x * C) * y)' * z) * ((x * C) * y)') = (((x * C) * y) * z) * ((x * C) * y)'.
(C * (x * (y * (C * (x * y))))) * ((((x * C) * y)' * z) * ((x * C) * y)') = (((x * C) * y) * z) * (y' * (x * C)').
(C * (x * (y * (C * (x * y))))) * ((((x * C) * y)' * z) * ((x * C) * y)') = (((x * C) * y) * z) * (y' * (x' * C')).
(C * (x * (y * (C * (x * y))))) * ((((x * C) * y)' * z) * ((x * C) * y)') = (x * (y * C')) * (z * ((y' * C) * x')).
(C * (x * (y * (C * (x * y))))) * (((y' * (x * C)') * z) * ((x * C) * y)') = (x * (y * C')) * (z * ((y' * C) * x')).
(C * (x * (y * (C * (x * y))))) * (((y' * (x' * C')) * z) * ((x * C) * y)') = (x * (y * C')) * (z * ((y' * C) * x')).
(C * (x * (y * (C * (x * y))))) * (((y' * (x' * C')) * z) * (y' * (x * C)')) = (x * (y * C')) * (z * ((y' * C) * x')).
(C * (x * (y * (C * (x * y))))) * (((y' * (x' * C')) * z) * (y' * (x' * C'))) = (x * (y * C')) * (z * ((y' * C) * x')).
(C * (x * (y * (C * (x * y))))) * ((y' * (x' * C')) * (z * (y' * (x' * C')))) = (x * (y * C')) * (z * ((y' * C) * x')).
(C * (x * (y * (C * (x * y))))) * (y' * ((x' * C') * ((z * y') * (x' * C')))) = (x * (y * C')) * (z * ((y' * C) * x')).
(C * (x * (y * (C * (x * y))))) * (y' * (x' * (C' * (((z * y') * x') * C')))) = (x * (y * C')) * (z * ((y' * C) * x')).
(C * (x * (y * (C * (x * y))))) * (y' * (x' * (C' * (C' * ((z * y') * x'))))) = (x * (y * C')) * (z * ((y' * C) * x')).
(x * (y * C')) * (z * ((y' * C) * x')) = y * (((y' * C) * (x * (y * (x * C)))) * (x' * (C' * (C' * ((z * y') * x'))))).
x * (((x' * C) * (y * (x * (y * C)))) * (y' * (C' * (C' * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * ((C * (C * (x' * (y * (x * y))))) * (y' * (C' * (C' * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (((y' * (C * C)) * ((x' * y) * x)) * (C' * (C' * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (((y' * (C * C)) * (x' * (y * x))) * (C' * (C' * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * ((C * (y' * (C * (x' * (y * x))))) * (C' * (C' * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (C * (((y' * (C * (x' * (y * x)))) * C') * (C' * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (C * ((C * ((y' * C') * (x' * (y * x)))) * (C' * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (C * ((C * (C' * (y' * (x' * (y * x))))) * (C' * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (C * ((y' * (x' * (y * x))) * (C' * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
(((x * ((C' * x') * y'))' * y') * (z * (y * (x * ((C' * x') * y'))))) * (x * (y * (C * (y' * x')))) = (y * (x * ((C' * x') * y')))' * z.
(((((C' * x') * y')' * x') * y') * (z * (y * (x * ((C' * x') * y'))))) * (x * (y * (C * (y' * x')))) = (y * (x * ((C' * x') * y')))' * z.
((((x'' * (C' * y')') * y') * x') * (z * (x * (y * ((C' * y') * x'))))) * (y * (x * (C * (x' * y')))) = (x * (y * ((C' * y') * x')))' * z.
((((x * (C' * y')') * y') * x') * (z * (x * (y * ((C' * y') * x'))))) * (y * (x * (C * (x' * y')))) = (x * (y * ((C' * y') * x')))' * z.
((((x * (y'' * C'')) * y') * x') * (z * (x * (y * ((C' * y') * x'))))) * (y * (x * (C * (x' * y')))) = (x * (y * ((C' * y') * x')))' * z.
((((x * (y * C'')) * y') * x') * (z * (x * (y * ((C' * y') * x'))))) * (y * (x * (C * (x' * y')))) = (x * (y * ((C' * y') * x')))' * z.
((((x * (y * C)) * y') * x') * (z * (x * (y * ((C' * y') * x'))))) * (y * (x * (C * (x' * y')))) = (x * (y * ((C' * y') * x')))' * z.
(((x * (C * (x' * y))) * y') * (z * (y * (x * ((C' * x') * y'))))) * (x * (y * (C * (y' * x')))) = (y * (x * ((C' * x') * y')))' * z.
((x * (y * ((C * y') * x'))) * (z * (x * (y * ((C' * y') * x'))))) * (y * (x * (C * (x' * y')))) = (x * (y * ((C' * y') * x')))' * z.
(x * (y * ((C' * y') * x')))' * z = x * (((y * ((C * y') * x')) * ((z * (x * (y * ((C' * y') * x')))) * x')) * (y * (C * (y' * x)))).
x * (((y * ((C * y') * x')) * ((z * (x * (y * ((C' * y') * x')))) * x')) * (y * (C * (y' * x)))) = (x * (y * ((C' * y') * x')))' * z.
x * (((y * ((C * y') * x')) * ((z * x) * ((y * ((C' * y') * x')) * x'))) * (y * (C * (y' * x)))) = (x * (y * ((C' * y') * x')))' * z.
x * (((y * ((C * y') * x')) * ((z * x) * (y * (C' * (y' * (x' * x')))))) * (y * (C * (y' * x)))) = (x * (y * ((C' * y') * x')))' * z.
x * (((y * ((C * y') * x')) * (x * ((x' * z) * (y * ((y' * C') * x'))))) * (y * (C * (y' * x)))) = (x * (y * ((C' * y') * x')))' * z.
x * (((y * ((C * y') * x')) * (x * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = (x * (y * ((C' * y') * x')))' * z.
x * ((x' * (((x * y) * (C * y')) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = (x * (y * ((C' * y') * x')))' * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = (x * (y * ((C' * y') * x')))' * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = ((y * ((C' * y') * x'))' * x') * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = ((((C' * y') * x')' * y') * x') * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = (((x'' * (C' * y')') * y') * x') * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = (((x * (C' * y')') * y') * x') * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = (((x * (y'' * C'')) * y') * x') * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = (((x * (y * C'')) * y') * x') * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = (((x * (y * C)) * y') * x') * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = ((y * (C * (y' * x))) * x') * z.
x * ((x' * ((y * (C * (y' * x))) * ((x' * z) * (y * ((C' * y') * x'))))) * (y * (C * (y' * x)))) = (x * (y * ((C * y') * x'))) * z.
(((x' * (y' * (x * y)))' * C'') * z') * (C * ((z * C') * (x' * (y' * ((x * C') * y))))) = C * ((C' * (x' * (y' * (x * y)))) * (z * (C' * (z' * (C' * (x' * (y' * (x * y))))')))).
((((x' * (y * x))' * y'') * C'') * z') * (C * ((z * C') * (y' * (x' * ((y * C') * x))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
(((((x * y)' * y'') * x'') * C'') * z') * (C * ((z * C') * (x' * (y' * ((x * C') * y))))) = C * ((C' * (x' * (y' * (x * y)))) * (z * (C' * (z' * (C' * (x' * (y' * (x * y))))')))).
(((((x' * y') * x'') * y'') * C'') * z') * (C * ((z * C') * (y' * (x' * ((y * C') * x))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
(((((x' * y') * x) * y'') * C'') * z') * (C * ((z * C') * (y' * (x' * ((y * C') * x))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
((((x' * (y' * x)) * y'') * C'') * z') * (C * ((z * C') * (y' * (x' * ((y * C') * x))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
((((x' * y') * (x * y)) * C'') * z') * (C * ((z * C') * (y' * (x' * ((y * C') * x))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
(((x' * (y' * (x * y))) * C'') * z') * (C * ((z * C') * (y' * (x' * ((y * C') * x))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
(((x' * (y' * (x * y))) * C) * z') * (C * ((z * C') * (y' * (x' * ((y * C') * x))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
((C * (x' * (y' * (x * y)))) * z') * (C * ((z * C') * (y' * (x' * ((y * C') * x))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
((C * (x' * (y' * (x * y)))) * z') * (C * (C' * (C' * (z * (y' * (x' * (y * x))))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
((C * (x' * (y' * (x * y)))) * z') * (C' * (z * (y' * (x' * (y * x))))) = C * ((C' * (y' * (x' * (y * x)))) * (z * (C' * (z' * (C' * (y' * (x' * (y * x))))')))).
C * ((C' * (x' * (y' * (x * y)))) * (z * (C' * (z' * (C' * (x' * (y' * (x * y))))')))) = ((C * (y' * (x' * (y * x)))) * z') * (C' * (z * (x' * (y' * (x * y))))).
C * ((C' * (x' * (y' * (x * y)))) * (z * (C' * (z' * (C' * (x' * (y' * (x * y))))')))) = C * (((y' * (x' * (y * x))) * (z' * C')) * (z * (x' * (y' * (x * y))))).
C * ((C' * (x' * (y' * (x * y)))) * (z * (C' * (z' * (C' * (x' * (y' * (x * y))))')))) = C * (z' * ((C' * (z * (y' * (x' * (y * x))))) * (x' * (y' * (x * y))))).
C * ((C' * (x' * (y' * (x * y)))) * (z * (C' * (z' * (C' * (x' * (y' * (x * y))))')))) = 1.
(C' * (x' * (y' * (x * y)))) * 1 = C * (z * ((z' * C') * (x' * (C' * (y' * (x * y)))))).
C * (x * ((x' * C') * (y' * (C' * (z' * (y * z)))))) = (C' * (y' * (z' * (y * z)))) * 1.
C * (x * ((x' * C') * (y' * (C' * (z' * (y * z)))))) = C' * (y' * (z' * (y * z))).
C * (x * (C' * (C' * (x' * (y' * (z' * (y * z))))))) = C' * (y' * (z' * (y * z))).
C' * (x' * (y' * (x * y))) = (z * C') * (z' * (x' * (y' * (x * y)))).
(x * C') * (x' * (y' * (z' * (y * z)))) = C' * (y' * (z' * (y * z))).
C' * (x' * (y' * (x * y))) = z * ((z' * C') * (x' * (y' * (x * y)))).
x * ((x' * C') * (y' * (z' * (y * z)))) = C' * (y' * (z' * (y * z))).
(C' * (x' * (y' * (x * y)))) * z = C * (z * ((((z * C)' * C') * (x' * (y' * (x * y)))) * z)).
C * (x * ((((x * C)' * C') * (y' * (z' * (y * z)))) * x)) = (C' * (y' * (z' * (y * z)))) * x.
C * (x * ((((C' * x') * C') * (y' * (z' * (y * z)))) * x)) = (C' * (y' * (z' * (y * z)))) * x.
C * (x * ((C' * (x' * (C' * (y' * (z' * (y * z)))))) * x)) = (C' * (y' * (z' * (y * z)))) * x.
C * (x * (x' * ((C' * (y' * (z' * (y * z)))) * (x * C')))) = (C' * (y' * (z' * (y * z)))) * x.
C * (x * (x' * (C' * (((y' * (z' * (y * z))) * x) * C')))) = (C' * (y' * (z' * (y * z)))) * x.
C * (x * (x' * (C' * (C' * ((y' * (z' * (y * z))) * x))))) = (C' * (y' * (z' * (y * z)))) * x.
(C' * (x' * (y' * (x * y)))) * z = C' * ((x' * (y' * (x * y))) * z).
x * ((C * x') * (C' * ((y' * (z' * (y * z))) * x))) = C * ((y' * (z' * (y * z))) * (x * C')).
x * (C * ((x' * C') * ((y' * (z' * (y * z))) * x))) = C * ((y' * (z' * (y * z))) * (x * C')).
C * ((x' * (y' * (x * y))) * (z * C')) = C * (((x' * (y' * (x * y))) * C') * z).
C * (((x' * (y' * (x * y))) * C') * z) = C * ((x' * (y' * (x * y))) * (z * C')).
C * ((C' * (x' * (y' * (x * y)))) * z) = C * ((x' * (y' * (x * y))) * (z * C')).
C * (C' * ((x' * (y' * (x * y))) * z)) = C * ((x' * (y' * (x * y))) * (z * C')).
C * ((x' * (y' * (x * y))) * (z * C')) = C * (C' * ((x' * (y' * (x * y))) * z)).
C * ((x' * (y' * (x * y))) * (z * C')) = (x' * (y' * (x * y))) * z.
C' * ((x' * (y' * (x * y))) * z) = (x' * (y' * (x * y))) * (C' * z).
(x' * (y' * (x * y))) * (C' * z) = C' * ((x' * (y' * (x * y))) * z).
x * (y * (C * (C' * ((y' * (x' * (y * x))) * ((z * x') * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (C * (C' * (y' * (((x' * (y * x)) * (z * x')) * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (C * (C' * (y' * ((x' * (((y * x) * z) * x')) * y'))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (C * (C' * (y' * (x' * (((y * x) * z) * (x' * y'))))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (y * (C * (C' * (y' * (x' * ((y * x) * (z * (x' * y')))))))) = (y * (x * C')) * (z * ((x' * C) * y')).
x * (x' * ((y * x) * (z * (x' * y')))) = (y * (x * C')) * (z * ((x' * C) * y')).
(x * (y * C')) * (z * ((y' * C) * x')) = y * (y' * ((x * y) * (z * (y' * x')))).
(x * (y * C')) * (z * ((y' * C) * x')) = (x * y) * (z * (y' * x')).
x * (y * ((z' * C) * (x * (z * C')')')) = ((x * (z * C')') * z) * (y * (z' * (x * (z * C')')')).
((x * (y * C')') * y) * (z * (y' * (x * (y * C')')')) = x * (z * ((y' * C) * (x * (y * C')')')).
((x * (y * C')') * y) * (z * (y' * (x * (y * C')')')) = x * (z * ((y' * C) * (x * (C'' * y'))')).
((x * (y * C')') * y) * (z * (y' * (x * (y * C')')')) = x * (z * ((y' * C) * (x * (C * y'))')).
((x * (y * C')') * y) * (z * (y' * (x * (y * C')')')) = x * (z * ((y' * C) * ((C * y')' * x'))).
((x * (y * C')') * y) * (z * (y' * (x * (y * C')')')) = x * (z * ((y' * C) * ((y'' * C') * x'))).
((x * (y * C')') * y) * (z * (y' * (x * (y * C')')')) = x * (z * x').
((x * (C'' * y')) * y) * (z * (y' * (x * (y * C')')')) = x * (z * x').
((x * (C * y')) * y) * (z * (y' * (x * (y * C')')')) = x * (z * x').
(x' * ((x * y) * C)) * (z * (x' * (y * (x * C')')')) = y * (z * y').
(x * ((C * x') * y)) * (z * (x' * (y * (x * C')')')) = y * (z * y').
(x * ((C * x') * y)) * (z * (x' * (y * (C'' * x'))')) = y * (z * y').
(x * ((C * x') * y)) * (z * (x' * (y * (C * x'))')) = y * (z * y').
(x * ((C * x') * y)) * (z * (x' * ((C * x')' * y'))) = y * (z * y').
(x * ((C * x') * y)) * (z * (x' * ((x'' * C') * y'))) = y * (z * y').
(x * ((C * x') * y)) * (z * (x' * ((x * C') * y'))) = y * (z * y').
(x * ((C * x') * y)) * (z * (x * (C' * (x' * y')))) = y * (z * y').
(x * ((x' * C) * y)) * (z * (x * (C' * (x' * y')))) = y * (z * y').
(x * ((x' * C) * y)) * (z * (x * ((x' * y') * C'))) = y * (z * y').
(x * ((x' * C) * y)) * (z * ((y' * (C' * x)) * x')) = y * (z * y').
(x * (C * (x' * y))) * (z * ((y' * (C' * x')) * x'')) = y * (z * y').
(x * (C * (x' * y))) * (z * ((y' * (C' * x')) * x)) = y * (z * y').
(x * (C * (x' * y))) * (z * (x' * ((x * y') * C'))) = y * (z * y').
(x * (C * (x' * y))) * (z * (x * ((x' * C') * y'))) = y * (z * y').
(x * (C * (x' * y))) * (z * (x * ((C' * x') * y'))) = y * (z * y').
x * ((x' * (x * ((x' * y) * x'))) * (z * (C * (z' * x)))) = (x * (z * ((C * z') * x'))) * y.
x * ((x' * (y * x')) * (z * (C * (z' * x)))) = (x * (z * ((C * z') * x'))) * y.
x * (x' * (y * (x' * (z * (C * (z' * x)))))) = (x * (z * ((C * z') * x'))) * y.
x * (x' * (y * (x * (z * ((C * z') * x'))))) = (x * (z * ((C * z') * x'))) * y.
(x * (y * ((C * y') * x'))) * z = z * (x * (y * ((C * y') * x'))).
(x * (y * ((C * y') * x'))) * z = z * (y * (x * (C * (x' * y')))).
(x * (y * (C * (y' * x')))) * z = z * (x * (y * (C * (y' * x')))).
(x * (y * (C * (y' * x')))) * z = z * (x * (y * ((y' * x') * C))).
(x * (y * (C * (y' * x')))) * z = z * (x * ((x' * (C * y)) * y')).
(x * (y * (C * (y' * x')))) * z = z * (((C * y) * x) * (x' * y')).
(x * (y * ((y' * x') * C))) * z = z * (((C * y) * x) * (x' * y')).
(x * ((x' * (C * y)) * y')) * z = z * (((C * y) * x) * (x' * y')).
D * x = x * D.
R(x,y,z) = ((x * y) * z) * (y * z)'.
R(C,A,B) = D.
D = R(C,A,B).
D * c4 != c4 * D.
c4 * D != D * c4.
R(x,y,z) = ((x * y) * z) * (z' * y').
D = ((C * A) * B) * (B' * A').
D * x = x * (((C * A) * B) * (B' * A')).
x * (((C * A) * B) * (B' * A')) = D * x.
x * D = D * x.
K(R(C,x,y),z) = 1.
K(R(C,c5,c6),c7) != 1.
(x' * y') * (y * x) = 1.
((((C * x) * y) * (y' * x'))' * z') * ((((C * x) * y) * (y' * x')) * z) = 1.
1 = K(((C * x) * y) * (y' * x'),z).
K(((C * x) * y) * (y' * x'),z) = 1.

end_of_list.
