% --------------------------------------------------------------------------
% Gagola:  Lemma List 4 (currently all but Lemmas 4-3 and 4-4)
% --------------------------------------------------------------------------

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.

% ***********
% Definitions
% ***********

% associator

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

% commutator

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

end_of_list.

formulas(goals).

R(x,C,y) * R(z,C,y) = R(x * z,C,y) # label("Lemma 4-1").
R(x,y,C) * R(z,y,C) = R(x * z,y,C) # label("Lemma 4-2").
%R(x,R(C,y,z),u) * R(w,R(C,y,z),u) = R(x * w,R(C,y,z),u) # label("Lemma 4-3").
%R(x,u,R(C,y,z)) * R(w,u,R(C,y,z)) = R(x * w,u,R(C,y,z)) # label("Lemma 4-4").

K(R(C,x,y) * R(C,y,x),z) = 1 # label("Lemma 4-5").

R(C,x * x,y) = R(C,y,x) # label("Lemma 4-6").
R(R(C,x,y),x * x,y) = C # label("Lemma 4-7").
R(R(C,y,x),x * x,y) = R(C,x,y) # label("Lemma 4-8").

R(C,x,y * y) = R(C,y,x) # label("Lemma 4-9").
R(R(C,y,x),x,y * y) = R(C,x,y) # label("Lemma 4-10").
R(R(C,x,y),x,y * y) = C # label("Lemma 4-11").

R(C,x * x,y') = R(C,x,y) # label("Lemma 4-12").
R(R(C,x,y),x * x,y') = R(C,y,x) # label("Lemma 4-13").
R(R(C,y,x),x * x,y') = C # label("Lemma 4-14").

R(R(C,x,y),y * y,x') = C # label("Lemma 4-15").
R(R(C,y,x),y * y,R(C,y,x) * x) = C # label("Lemma 4-16").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

R(C,x * x,y') = R(C,x,y).
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).
R(x,y,z) = ((x * y) * z) * (y * z)'.
C * x = x * C.
R(C,c22 * c22,c23') != R(C,c22,c23).
x'' * 1 = x.
(x * y)' * x = y'.
x * (y * x)' = y'.
(x' * x') * (x * y) = x' * y.
(x * y)' * (x * (y * y)) = y.
x' * ((x * y) * x) = y * x.
x * y' = y' * ((y * x) * y').
x' * ((x * y) * x') = y * x'.
(x * (y * x)) * z = x * (y * (x * z)).
(x * y) * (z * x) = z' * ((z * x) * (y * (z * x))).
x' * ((x * y) * (z * (x * y))) = (y * z) * (x * y).
(x * (y * (z * y))) * y' = (x * y) * z.
(x * (y * (z * y))) * z = (x * y) * (z * (y * z)).
x' * ((x * y) * (z * x)) = (y * z) * x.
R(x,y,z) = ((x * y) * z) * (z' * y').
R(x,y * z,z) = ((x * (y * z)) * z) * (y * (z * z))'.
((x * (y * z)) * z) * (y * (z * z))' = R(x,y * z,z).
C' * (x * C) = x.
x' * (C * x) = C.
C * (x * x) = x * (x * C).
((x * C) * y) * x = C * (x * (y * x)).
(x * y) * (x * C) = x * ((y * C) * x).
R(C,x,y) = ((x * C) * y) * (x * y)'.
((x * C) * y) * (x * y)' = R(C,x,y).
x = x''.
x'' = x.
x * (x' * y) = y.
(x * y') * y = x.
(x * y')' = y * x'.
(x' * y)' = y' * x.
x * (C * x') = C.
x * y = y * ((y' * x) * y).
x * ((x' * y) * x) = y * x.
(x * y) * z = y * ((y' * x) * (y * z)).
x * ((x' * y) * (x * z)) = (y * x) * z.
((x * y) * x) * (x' * z) = x * (y * z).
x * (y * z) = z * (((z' * x) * y) * z).
x * (((x' * y) * z) * x) = y * (z * x).
R(x,x' * y,z) = (y * z) * ((x' * y) * z)'.
(x * y) * z = (x * z') * (z * (y * z)).
(x * y') * (y * (z * y)) = (x * z) * y.
(x' * y) * z = (z * x)' * (z * (y * z)).
(x * y)' * (x * (z * x)) = (y' * z) * x.
x * (y * (x * x))' = (y * x)'.
x' * y = y * ((x * y)' * y).
x * ((y * x)' * x) = y' * x.
((x * y') * z)' = z' * (y * x').
R(x,y,z') = ((x * y) * z') * (z * y').
((x * y) * z') * (z * y') = R(x,y,z').
R(x,y,z)' = (y * z) * ((x * y) * z)'.
(x * y) * ((z * x) * y)' = R(z,x,y)'.
R(x,y',z) = ((x * y') * z) * (z' * y).
((x * y') * z) * (z' * y) = R(x,y',z).
C * (x * x) = x * (C * x).
C * (x * x)' = x' * (C * x').
x' * (C * x') = C * (x * x)'.
(x * x)' * (x * y) = x' * y.
R(x,(y * y)',y * z) = ((x * (y * y)') * (y * z)) * (y' * z)'.
((x * (y * y)') * (y * z)) * (y' * z)' = R(x,(y * y)',y * z).
x * (y * x') = (x * y) * x'.
(x * y) * x' = x * (y * x').
((x * y) * y) * z = (x * y) * (x' * ((x * y) * z)).
(x * y) * (x' * ((x * y) * z)) = ((x * y) * y) * z.
(x' * (y * x')) * (x * z) = x' * (y * z).
C * (x * (y * x)) = x * (y * (x * C)).
x * (y * C) = y * (((y' * x) * C) * y).
x * (((x' * y) * C) * x) = y * (x * C).
((x * C) * ((y * x)' * x)) * (y' * x)' = R(C,x,(y * x)' * x).
(x * (y * z)) * y' = (x * y) * (z * y').
(x * (y * z)) * z' = (x * z) * (z' * y).
(x * (y * (x * C))) * x' = (C * x) * y.
x * ((x' * y) * z) = (y * x) * (x' * z).
(x * y) * (y' * z) = y * ((y' * x) * z).
x * ((x' * y) * C) = (y * x) * (C * x').
(x * y) * (C * y') = y * ((y' * x) * C).
(x' * y) * (y' * z) = y * ((x * y)' * z).
(x * (y * (z * u))) * u' = (x * u) * ((u' * y) * z).
(x * y') * (y * z') = (x * (y * z)') * y.
(x * (y * z)') * y = (x * y') * (y * z').
(x * y') * (z * y) = (x * (y' * z)) * y.
(x * (y' * z)) * y = (x * y') * (z * y).
x * ((C * (x' * y)) * x) = y * (x * C).
(C * x) * y = x * ((y * (x * C)) * x').
x * ((y * (x * C)) * x') = (C * x) * y.
x * ((C * (y * x)') * x) = y' * (x * C).
x * ((y * (x * C)) * x') = (x * C) * y.
(x * y)' * (x * z) = (y' * (z * x')) * x.
(x' * (y * z')) * z = (z * x)' * (z * y).
((x * y) * (z * y)') * z = R(x,y,(z * y)').
(x' * y) * (y' * (x * z)) = R(z,(x * z)',y).
R(x,(y * x)',z) = (y' * z) * (z' * (y * x)).
x * ((y * x) * (C * x')) = (x * C) * y.
R(x,y,z) = ((x * y) * (y' * z)) * z'.
x * ((x' * (y * z')) * z) = R(y,z',x).
(x * (y * z)) * z' = z * ((z' * x) * y).
R(x,y,z) = (y * ((y' * x) * z)) * z'.
R(x * C,C,y) = (C * (x * y)) * y'.
(C * (x * y)) * y' = R(x * C,C,y).
(x * y) * (C * y') = y * (C * (y' * x)).
x * ((C * x') * (y * x)) = y * (x * C).
x * (((y * z') * x)' * y) = R(z,y',x).
x * ((x' * C) * y) = R(y * C,C,x).
x * ((C * x') * y) = R(y * C,C,x).
R((x * y) * C,C,y) = x * (y * C).
R(C * (x * y),C,y) = x * (y * C).
R(C * x',C,y) = (y * x)' * (y * C).
(x * y)' * (x * C) = R(C * y',C,x).
x * (x * (C * (x' * y))) = (x * C) * y.
x' * ((x * C) * y) = x * (C * (x' * y)).
(x * y) * ((y * ((z' * x) * y))' * y) = R(z,y',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 * R(y * C,C,x) = C * (x * y).
x' * (C * (x * y)) = R(y * C,C,x).
(C * (x * x)') * (x * y) = x' * (C * y).
(C * (x * x)') * (x * y) = x' * (y * C).
((x * y) * (z * y)') * z = R(x,y,z').
x * ((y * x)' * (y * z)) = R(z,y',x).
x * R(C * x',C,y) = R(C,y',x).
(x' * y) * (y' * (x * z)) = R(z,x',y).
x * ((y * x)' * (y * z)) = R(z,y',y * x).
R(x,y,(z * y)') = R(x,y,z').
R(x,y',y * z) = R(x,y',z).
R(x,y'',z) = R(x,y'',y * z).
R(x,y'',y * z) = R(x,y'',z).
R(x,y'',y * z) = R(x,y,z).
R(x,y,y * z) = R(x,y,z).
R(x,y,z' * y) = R(x,y,(z * y)' * y).
R(x,y,(z * y)' * y) = R(x,y,z' * y).
(x * ((y * z) * (z' * (y * z)))) * z' = (x * (y * z)) * (z' * y).
R(x,x' * y,z) = R(x',y,z)'.
R(x,(y * x)',z) = R(x,y',z).
R(x,y'',z) = R(x,(x * y)'',z).
R(x,(x * y)'',z) = R(x,y'',z).
R(x,(x * y)'',z) = R(x,y,z).
R(x,x * y,z) = R(x,y,z).
R(x,y,z) = R(x,x' * y,z).
R(x,x' * y,z) = R(x,y,z).
R(x,y,z) = R(x',y,z)'.
R(x',y,z)' = R(x,y,z).
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)).
(x * y) * (x' * ((x * y) * z)) = (x * (y * y)) * z.
(x * y)' * ((x * (y * y)) * z) = x' * ((x * y) * z).
((x * ((y * z) * x)) * x) * (z * (x * x))' = R(x * y,z * x,x).
(C * (x * ((y * x) * x))) * (y * (x * x))' = R(x * C,y * x,x).
R(C * ((x * y)' * (x * (y * y))),C,x * (y * y)) = x' * ((x * y) * C).
(x * y) * ((z' * x) * y)' = R(z,y',x * y).
R(x,y',z * y) = R(x',z,y)'.
R(x,y',z * y) = R(x,z,y).
R(x,y,z * y') = R(x,z,y').
R(x,y,z) = R(x,z * y,y').
R(x,y * z,z') = R(x,z,y).
R(x * y,z * x,x) = x * (((y * z) * x) * (x * (z * (x * x))')).
x * (((y * z) * x) * (x * (z * (x * x))')) = R(x * y,z * x,x).
(C * (x * (y * (x * x)))) * (y * (x * x))' = R(x * C,y * x,x).
x * (((y * z) * x) * (z * x)') = R(x * y,z * x,x).
x * R(y,z,x) = R(x * y,z * x,x).
R(x * y,z * x,x) = x * R(y,z,x).
R(x * C,y * x,x) = R(x * C,C,y * (x * x)).
R(x * C,C,y * (x * x)) = R(x * C,y * x,x).
((x * (y * y)') * (y * z)) * (z' * y) = R(x,(y * y)',y * z).
(x' * (y * C)) * (y' * x) = R(C,(x * x)',x * y).
R(C,(x * x)',x * y) = (x' * (y * C)) * (y' * x).
(x * ((C * (y * x)') * x)) * (y' * x)' = R(C,x,(y * x)' * x).
(x * (y * (z * ((z' * y) * z)))) * z' = (x * (y * z)) * (z' * y).
(x' * (y * C)) * (x' * y)' = R(C,y,(x * y)' * y).
R(C,x,(y * x)' * x) = (y' * (x * C)) * (y' * x)'.
R(C,x,(y * x)' * x) = (y' * (x * C)) * (x' * y).
(x * (y * (y * z))) * z' = (x * (y * z)) * (z' * y).
(x * (y * z)) * (z' * y) = (x * z) * ((z' * y) * y).
(x * (y * z)) * (z' * y) = (x * z) * (z' * (y * y)).
(x * (y * z)) * (z' * y) = z * ((z' * x) * (y * y)).
x * ((x' * (y * (z * z)')) * (z * z)) = R(y,(z * z)',z * x).
R(x,(y * y)',y * z) = R(x,(y * y)',z).
R(C,(x * x)',y) = (x' * (y * C)) * (y' * x).
(x' * (y * C)) * (y' * x) = R(C,(x * x)',y).
R(C * x,C,y * (x * x)) = y' * ((y * x) * C).
R(x * C,C,y * (x * x)) = y' * ((y * x) * C).
R(x * C,C,y * (x * x)) = y' * (C * (y * x)).
R(x * C,C,y * (x * x)) = R(x * C,C,y).
R(x * C,C,y) = R(x * C,y * x,x).
R(x * C,y * x,x) = R(x * C,C,y).
R(x * C,C,y) = x * R(C,y,x).
x * R(x' * C,C,y) = R(C,y,x').
x * R(C * x',C,y) = R(C,y,x').
R(C,x,y') = R(C,x',y).
R(C,x',y) = R(C,x,y').
R(C,x,y) = R(C,x',y').
R(C,x',y') = R(C,x,y).
R(C,x,(y * x)') = R(C,y,x).
(x' * (y * C)) * (y' * x) = R(C,x * x,y').
R(C,x,y) = R(C,y,x').
R(C,x,y') = R(C,y,x).
R(C,x,y * x) = R(C,x,y).
R(C,x,y') = R(C,y,x * y).
R(C,x,y * x) = R(C,y,x').
R(C,x,(y * x)' * x) = R(C,y * y,x').
R(C,x * x,y') = R(C,y,(x * y)' * y).
R(C,x * x,y') = R(C,y,x' * y).
R(C,x * x,y') = R(C,x',y').
$F.
R(C,x,y * y) = R(C,y,x).
R(C,c17,c16) != R(C,c16,c17 * c17).
R(C,c16,c17 * c17) != R(C,c17,c16).
R(C,x,y) = R(C,y,x * x).
R(C,x * x,y) = R(C,y,x).
R(C,c10 * c10,c11) != R(C,c11,c10).
R(C,x * x,y) = R(C,x,y').
R(R(C,x,y),x * x,y) = C.
R(R(C,c12,c13),c12 * c12,c13) != C.
x * (x * (y * x))' = (x * y)'.
x * (y * (x * (z * x)))' = ((y * x) * z)'.
(x * y) * (z * (u * (z * x))) = x * ((y * (z * (u * z))) * x).
x * (y * (z * x))' = (x * ((x' * y) * z))'.
(x * ((x' * y) * z))' = x * (y * (z * x))'.
x * (y * (z * x))' = ((y * x) * (x' * z))'.
((x * y) * (y' * z))' = y * (x * (z * y))'.
(x * (x * (y * z))) * z' = ((x * x) * z) * (z' * y).
R(x,y * z,y) = ((x * (y * z)) * z') * y'.
((x * (y * z)) * z') * y' = R(x,y * z,y).
R(x,y,z) = z * ((z' * y) * (y' * x)).
R(x,y,z) = z * (y * ((z * y)' * x)).
R((x * y) * z,y,x) = x * (y * z).
R(x,y,z) * z = z * ((y * ((z * y)' * x)) * z).
x * ((y * ((x * y)' * z)) * x) = R(z,y,x) * x.
R(x,y,(y' * z) * u) = ((x * y) * ((y' * z) * u)) * (y * (z * (u * y))').
((x * y) * ((y' * z) * u)) * (y * (z * (u * y))') = R(x,y,(y' * z) * u).
((x * y) * (y' * z)) * z' = R(x,z * y,z).
R(x,y,z) = R(x,y,y' * z).
R(x,y,y' * z) = R(x,y,z).
R(x,y,z) = R(x,z * y,z).
R(x,y * z,y) = R(x,z,y).
(x * (x * (y * z))) * z' = (x * (x * z)) * (z' * y).
(x * (x * y)) * (y' * z) = (x * y) * ((y' * x) * z).
R(x,x * y,y' * z) = ((x * y) * ((y' * x) * z)) * ((x * y) * (y' * z))'.
((x * y) * ((y' * x) * z)) * ((x * y) * (y' * z))' = R(x,x * y,y' * z).
R(x * y,x,y * z) = y * ((z * (x * (((y * z) * x)' * x))) * y).
x * ((y * (z * (((x * y) * z)' * z))) * x) = R(z * x,z,x * y).
((x * y) * ((y' * x) * z)) * (y * (x * (z * y))') = R(x,x * y,y' * z).
R(x,x * y,y' * z) = R(x,y,(y' * x) * z).
R(x,y,(y' * x) * z) = R(x,y,y' * z).
R(x,y,(y' * x) * z) = R(x,y,z).
R(x * y,x,y * z) = R(x * y,x,z).
x * ((y * (z * (((x * y) * z)' * z))) * x) = R(z * x,z,y).
x * ((y * ((x * y)' * z)) * x) = R(z * x,z,y).
R(x * y,x,z) = y * ((z * ((y * z)' * x)) * y).
R(x * y,x,z) = R(x,z,y) * y.
R((x * y) * z,x * y,x) = (R(x,z,y) * y) * z.
(R(x,y,z) * z) * y = R((x * z) * y,z,x).
R((x * y) * z,y,x) = (R(x,z,y) * y) * z.
(R(x,y,z) * z) * y = x * (z * y).
R(R(x,y,z),z,y) = (x * (z * y)) * (z * y)'.
(x * (y * z)) * (y * z)' = R(R(x,z,y),y,z).
R(R(x,y,z),z,y) = x.
R(R(C,x,y),x,y * y) = C.
R(R(C,c20,c21),c20,c21 * c21) != C.
R(R(C,x,y),y * y,x') = C.
R(R(C,c28,c29),c29 * c29,c28') != C.
R(R(C,c26,c27),c27 * c27,c26') != C.
R(x,y,C) * R(z,y,C) = R(x * z,y,C).
R(c4 * c6,c5,C) != R(c4,c5,C) * R(c6,c5,C).
R(c4,c5,C) * R(c6,c5,C) != R(c4 * c6,c5,C).
(C * x) * C' = x.
(C * (C * x)) * y = C * (x * (C * y)).
(C * x) * (C * y) = C * ((x * y) * C).
(x * (C * y)) * (C' * x) = x * (y * x).
(x * y) * ((y' * x') * z) = z.
(x * (y' * z')) * (z * y) = x.
(C * x) * ((C' * x') * y) = y.
(C * x) * y = (C' * x')' * y.
(C' * x')' * y = (C * x) * y.
(x * (y * x)) * (x' * z) = x * (y * z).
(C * x) * (C * y) = C * (C * (x * y)).
R(x,y,C) = (C * (x * y)) * (C' * y').
(C * (x * y)) * (C' * y') = R(x,y,C).
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').
(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,C,y) * R(z,C,y) = R(x * z,C,y).
R(c1 * c3,C,c2) != R(c1,C,c2) * R(c3,C,c2).
R(c1,C,c2) * R(c3,C,c2) != R(c1 * c3,C,c2).
R(x,x,y) = (x * (x * y)) * (x * y)'.
(x * (x * y)) * (x * y)' = R(x,x,y).
R(x,x,y) = x.
R(x * (y * z),x,y) = (x * y) * z.
R(x * (y * C),x,C) = (x * C) * y.
x * R(y,x,C) = R(x * y,x,C).
R(x * y,x,C) = x * R(y,x,C).
x * R(y * C,x,C) = (x * C) * y.
x * ((x' * C) * y) = R(y * C,x',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(R(C,x,y),x * x,R(C,x,y) * y) = C.
R(R(C,c30,c31),c30 * c30,R(C,c30,c31) * c31) != C.
R(x,y * y,z) = ((x * (y * y)) * z) * (y * (y * z))'.
((x * (y * y)) * z) * (y * (y * z))' = R(x,y * y,z).
R(x,y,x) = (x * (y * x)) * (y * x)'.
(x * (y * x)) * (y * x)' = R(x,y,x).
(C * x) * C = x * (C * C).
C * (x * C) = x * (C * C).
C * ((x * C) * y) = x * (C * (y * C)).
(x * (C * C)) * y = C * (x * (C * y)).
(x * (y * (z * (y * x)))) * u = x * ((y * (z * y)) * (x * u)).
R(x,y,x) = x.
R(x,(y * C) * z,y) = ((x * ((y * C) * z)) * y) * (C * (y * (z * y)))'.
((x * ((y * C) * z)) * y) * (C * (y * (z * y)))' = R(x,(y * C) * z,y).
C * ((x * C) * y) = x * (y * (C * C)).
(x * (C * C)) * y = C * (x * (y * C)).
(C * ((x * C) * y)) * x = x * ((y * (C * C)) * x).
x * R(y,C,x) = C * (x * (y * C')).
C * (x * (y * C')) = x * R(y,C,x).
(x * (y * ((z * y)' * y))) * (z * y)' = (x * y) * ((z * y)' * z').
(C * ((x * C) * y)) * x = x * (C * (y * (x * C))).
R(C,x * C,y) = R(C,x,y).
R(x,y,z)' = R(x',y,z).
(x * (y * (z * (y * x)))) * u = x * (y * (z * (y * (x * u)))).
R(x,y,(y * z)') = R(x,z',y').
R(C,x',(y * C)') = R(C,y,((y * C) * x)').
R(C,x,((x * C) * y)') = R(C,y',(x * C)').
(x * (C * (y * (x * C)))) * z = x * (C * (y * (C * (x * z)))).
(x * (C * (y * (x * C)))) * (C * (x * (y * x)))' = R(C,(x * C) * y,x).
(x * (y' * z)) * (y * z)' = (x * z) * ((y * z)' * y').
(x * (y' * z)) * (y * z)' = (x * z) * (y * (y * z))'.
(x * y) * (z * (z * y))' = (x * (z * y)) * (z * (z * (z * y)))'.
(x * (y * z)) * (y * (y * (y * z)))' = (x * z) * (y * (y * z))'.
((x * (y * y)) * z) * (y * (y * z))' = R(x,y * y,y * z).
R(x,y * y,y * z) = R(x,y * y,z).
R(C,(x * C) * y,x) = x * (C * (y * (C * (x * (C * (x * (y * x)))')))).
x * (C * (y * (C * (x * (C * (x * (y * x)))')))) = R(C,(x * C) * y,x).
x * (C * (y * (C * ((C * x) * y)'))) = R(C,(x * C) * y,x).
x * (C * (y * (C * ((x * C) * y)'))) = R(C,(x * C) * y,x).
R(C,x,((x * C) * y)') = R(C,y,x * C).
R(C,x,y * C) = R(C,(y * C) * x,y).
R(C,(x * C) * y,x) = R(C,y,x * 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).
R(x' * C,y,C) = C * R(x,y,C)'.
R(C * x',y,C) = C * R(x,y,C)'.
x * R(y,C,x) = R(x * y,C,x).
R(x * y,C,x) = x * R(y,C,x).
R(x * (y * C),C,x) = C * (x * y).
R(C * (x * y),x,C) = x * (y * C).
R(C * (x * y),x,C) = x * (C * y).
R(C * x',y,C) = y * ((x * y)' * C).
x * ((y * x)' * C) = R(C * y',x,C).
R(C * x',y,C) = y * (C * (x * y)').
x * (C * (y * x)') = R(C * y',x,C).
R(C,x,y) = y * R(C * y',x,C).
x * R(C * x',y,C) = R(C,y,x).
x * (C * R(C * (x * C)',y,C)) = R(C,(x * C) * y,x).
x * (C * R(x',y,C)) = R(C,(x * C) * y,x).
R(C,(x * C) * y,x) = x * (C * R(x',y,C)).
R(C,(x * C) * y,x) = x * (C * R(x,y,C)').
R(C,(x * C) * y,x) = x * R(C * x',y,C).
R(C,(x * C) * y,x) = R(C,y,x).
R(C,x,y) = R(C,x,y * C).
R(C,x,y * C) = R(C,x,y).
R(C,x,C * y) = R(C,x,y).
R(R(C,x,y),x * x,C * y) = C.
R(R(C,x,y),x * x,C * (x * y)) = C.
R(R(C,x,y),x * x,x * (C * (x * y))) = C.
R(R(C,x,y),x * x,x * (C * (x * ((C * y) * C')))) = C.
R(R(C,x,y),x * x,x * (x * R(C * y,C,x))) = C.
R(R(C,x,y),x * x,(x * x) * R(C * y,C,x)) = C.
C = R(R(C,x,y),x * x,R(C * y,C,x)).
R(R(C,x,y),x * x,R(C * y,C,x)) = C.
R(R(C,x,y),y * y,x) = R(C,y,x).
x * y = (y * x) * K(x,y).
(x * y) * K(y,x) = y * x.
(x * y) * z = (x * (y * z)) * a(x,y,z).
(x * (y * z)) * a(x,y,z) = (x * y) * z.
R(R(C,c14,c15),c15 * c15,c14) != R(C,c15,c14).
(x * C) * (y * C) = C * ((x * y) * C).
(x * y)' * (y * x) = K(y,x).
(x * (y * z))' * ((x * y) * z) = a(x,y,z).
x' * (y * (y' * (x * z))) = z.
x * C' = C' * x.
C' * x = x * C'.
(x * y) * z = x * ((y * (z * x')) * x).
x * ((y * (z * x')) * x) = (x * y) * z.
R(x,y,z) * (y * z) = (x * y) * z.
C * (x * C') = x.
C * (x * (x * C')) = x * x.
((x * y) * z)' * (x * (y * z)) = a(x,y,z)'.
((x * y) * C') * y = x * (y * (y * C')).
(x * (y * z'))' = (z * y') * x'.
(x * (y' * z))' = (z' * y) * x'.
((x' * y) * z)' = z' * (y' * x).
x' * (y * x) = (x' * y) * x.
(x' * y) * x = x' * (y * x).
x' * (y * (x * y')) = K(y,x * y').
(x' * y) * (x * y') = K(x,y').
(x * x) * (y * C) = C * (((x * (x * C')) * y) * C).
C * (((x * (x * C')) * y) * C) = (x * x) * (y * C).
((x * y') * z') * (z * y) = R(x,y',z').
((x * y)' * y) * x = K(x * y,y').
(x * (y * (x * z))) * z' = x * (y * x).
(x * (x * C')) * y = x * (C' * (x * y)).
(x * ((y * x)' * x)) * y = x * K(x,y).
(x * C) * (y * C) = C * (C * (x * y)).
((x * C) * (x * y))' * (x * ((y * C) * x)) = K(x * y,x * C).
(x * C) * (C * y) = C * (C * (x * y)).
(x * C) * y = C * (C * (x * (C' * y))).
C * (C * (x * (C' * y))) = (x * C) * y.
((x * y) * z) * u = x * ((y * (z * x')) * (x * u)).
x * ((y * (z * x')) * (x * u)) = ((x * y) * z) * u.
(x * y') * z' = x * (((x * z) * y)' * x).
x * (((x * y) * z)' * x) = (x * z') * y'.
(x' * y) * x = y * K(y,x).
(x * K(x,y')) * y = y'' * x.
x * (y * K(y,x)) = y * x.
x * K(x,y) = y' * (x * y).
x' * (y * x) = y * K(y,x).
x * (y * x') = y * K(y,x').
x * K(x,y') = y * (x * y').
x' * (y * (x * y')) = K(x,y').
(x * C)' * (x * ((y * C) * x)) = (x * y) * K(x * y,x * C).
(x * K(x,y')) * y = y * x.
R(x,y * K(y,z'),z) * (z * y) = (x * (y * K(y,z'))) * z.
K(x,y') = K(y,x * y').
K(x,y * x') = K(y,x').
K(x,y) = K(y * x,x').
K(x * y,y') = K(y,x).
((x * y)' * y) * x = K(y,x).
(x * y)' * ((x * (y * z)) * z') = a(x,y * z,z').
((x * y) * (y' * z))' * (x * z) = a(x * y,y',z).
((x * y) * (x * z))' * ((x * (y * x)) * z) = a(x * y,x,z).
((x * y) * (x * z))' * (x * (y * (x * z))) = a(x * y,x,z).
((x * y) * (z * y))' * (x * (y * (z * y))) = a(x * y,z,y).
(x * (y * (z * x)))' * (x * ((y * z) * x)) = a(x,y,z * x).
(x * y)' * ((x * z) * (z' * y)) = a(x,z,z' * y).
(x * ((x' * y) * z))' * (y * z) = a(x,x' * y,z).
((x * C) * (y * x))' * (C * (x * (y * x))) = a(x * C,y,x).
((x' * y) * z') * ((z * y') * x) = a(z,y',x).
x * (y * (x * (x * C')))' = ((y * x) * C')'.
(C' * (x * y)) * y = x * (y * (y * C')).
R(x * C,C,y) * y = C * (x * y).
(x * (((x * y) * z)' * x)) * (y * z) = x * a(x,y,z)'.
(x * (y * z'))' * (x * y) = R(z,y',x').
(x * (y * z'))' = z * (((z * x) * y)' * z).
x * (((x * y) * z)' * x) = (y * (z * x'))'.
((x * y') * z)' * x = (x * z)' * (x * y).
R(x,y',z')' = ((y * z')' * (y * x))' * z.
((x * y')' * (x * z))' * y = R(z,x',y')'.
R(x,(y * z)',z') = R(x,y',z').
R(x,y * K(y,z'),z) = R(x,y * z',z).
x * (y * (x * (x * C')))' = C * (y * x)'.
x * (y * (x * (x * C')))' = (y * x)' * C.
R(C,x,y) = y * (x * (x * (y * (x * (x * C')))')).
x * (y * (y * (x * (y * (y * C')))')) = R(C,y,x).
C * (((x * (x * C')) * y) * C) = x * (x * (y * C)).
(((x * y) * z) * u)' * x = ((y * (z * x')) * (x * u))'.
((x * (y * z')) * (z * u))' = (((z * x) * y) * u)' * z.
((x * y) * z') * ((z * y') * x') = a(z,y',x').
((x * y') * (y * z))' * x = R(z,y',x')'.
R(x,y',z')' = (z * (y * x))' * (z * y).
(x * (y * z))' * (x * y) = R(z,y',x')'.
x * ((y * y) * (x * (y * (y * C')))') = R(C,y,x).
C * ((x * (C' * (x * y))) * C) = x * (x * (y * C)).
C * (C * (x * (C' * (x * y)))) = x * (x * (y * C)).
x * (x * (y * C)) = (x * C) * (x * y).
(x * C) * (x * y) = x * (x * (y * C)).
(x * y)' * ((x * z) * (z' * y)) = a(x,y * z,z').
(x * (y * (z * x))') * (y * z) = a(y * x,x',z).
(x * (y * (z * x))') * (y * z) = a(x,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',z) = a(y,y' * (x * y'),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).
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',(x * y) * x,z) = a(y,x,z).
a(x',x * (y * x),z) = a(y,x,z).
a(x',x * y,z) = a(y * x',x,z).
a(x * y',y,z) = a(y',y * x,z).
((x * y) * z') * (x * (y * z'))' = a(z,y',x').
a(x,y * z,z') = a(x,z,z' * y).
a(x,y,z'') = a(x,z',z'' * (y * z)).
a(x,y',y'' * (z * y)) = a(x,z,y'').
a(x,y,z') = a(x,z,z' * (y * z')).
a(x,y,y' * (z * y')) = a(x,z,y').
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',y * (z * y)) = a(x,z,y).
a(x,y',(y * z) * y) = a(x,z,y).
a(x,C',(y * C) * C) = a(x,y,C).
((x * (y * z')) * (z * (x * y)'))' = a(z,y',x').
(x * (y * z'))' * (x * y) = z * a(z,x,y)'.
x * a(x,y,z)' = R(x,z',y').
(((x * y) * z) * (y * z)')' * x = a(x,z',y').
R(x,y,z)' * x = a(x,z',y').
(x * ((y * C) * x))' * ((x * (y * x)) * C) = a(x * y,x,C).
a(x * y,x,z) = a(x,y,x * z)'.
a(x,y,x * z)' = a(x * y,x,z).
a(C,x,y * C)' = a(C * x,C,y).
a(x * y,x,z)' = a(x,y,x * z).
a(C,x * C',C * y)' = a(x,C,y).
a(C,x * C',y * C)' = a(x,C,y).
a(x,y,z)' = a(y,y' * x,y * z).
a(x,x' * y,x * z) = a(y,x,z)'.
a(x * y,z,y) = a(x,y,z * y)'.
a(x,y,z * y)' = a(x * y,z,y).
a(x * y,z,y)' = a(x,y,z * y).
a(x * C,y,x)' = a(C,x,y * x).
a(x,y,z)' = a(x * z',z,y * z).
a(x * y',y,z * y) = a(x,z,y)'.
a(x,y,z)' = a(z',z * x,y * z).
a(x',x * y,z * x) = a(y,z,x)'.
a(x,y,z * x) = ((y * (z * x))' * (y * z)) * x.
((x * (y * z))' * (x * y)) * z = a(z,x,y * z).
R(x,y',z')' * x = a(x,z,y * x).
a(x,y,z * x) = R(x,z',y')' * x.
a(x,y,z * x) = a(x,y'',z'').
a(x,y,z * x) = a(x,y,z'').
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,y,x * C) = a(x,y,C).
a(C,x * C',y)' = a(x,C,y).
a(x,y,C)' = a(x * y,x,C).
a(x * y,x,C) = a(x,y,C)'.
a(x,x' * y,C) = a(y,x,C)'.
a(x',x * y,z) = a(y,z,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,x' * y,z) = a(y,z,x')'.
a(x * y,z,y)' = a(x,y,z).
a(x,y,z)' = a(x * y,z,y).
a(x * y,z,y) = a(x,y,z)'.
a(x,y,z) = a(x,y,z * y).
a(x,y,z * y) = a(x,y,z).
a(x,y',z) = a(x,y',z * y).
a(x,y',z * y) = a(x,y',z).
a(x,y,z) = a(x,y,z * y').
a(x,y,z * y') = a(x,y,z).
a(x,y,y' * C) = a(x,y,C).
a(x,y * z,y') = a(x,y,z).
a(x,y,z') = a(x,z,z' * y).
a(x,y,y' * z) = a(x,z,y').
a(x,y',y * z) = a(x,z,y).
a(x,C',y * C) = a(x,y,C).
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).
a(x,C,y) = a(x,y,C').
a(x,C,y') = a(x,y,C).
a(x * y,C',y) = a(x,C,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(x,C',y) = a(x,C,y').
a(x,y,C) = a(x,y',C').
a(x,y',C') = a(x,y,C).
a(x',y,x' * C)' = a(x' * y,C,x).
R(x,C,y)' * x = a(x,y,C).
a(x,y,C)' = x' * R(x,C,y).
x' * R(x,C,y) = a(x,y,C)'.
a(x,y,x * C) = R(x,C,y)' * x.
a(x,C,y)' = a(x * y,y,C).
a(x * y,y,C) = a(x,C,y)'.
a(x',y,x' * C) = R(x,C,y) * x'.
a(x,C,y' * x'') = a(y,x,C)'.
a(x,C,y' * x) = a(y,x,C)'.
a(x,y,C)' = 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,x' * y,C) = a(x,C',y).
a(x,x' * y,C) = a(x,y,C).
(R(x,C,y) * x')' = a(x' * y,C,x).
a(x' * y,C,x) = x * R(x,C,y)'.
(x * ((C * y) * x))' * (C * (x * (y * x))) = a(x * C,y,x).
R(x,y',z) = R(x,z * y',y).
R(x,y * z',z) = R(x,z',y).
R(x,y * K(y,z'),z) = R(x,z',y).
(x * ((y * C) * x))' * (C * (x * (y * x))) = a(x * y,x,C).
(x * ((y * C) * x))' * (C * (x * (y * x))) = a(x * C,y,x).
a(x * C,y,x) = a(x * y,x,C).
a(x * C,y,x)' = a(x,y,x * C).
a(x * C,y,x) = a(x,y,C)'.
a(C * x,y,x) = a(x,y,C)'.
a(x,y,C)' = a(C,x,y)'.
a(C,x,y)' = a(x,y,C)'.
a(x,y,x * C) = a(C,x,y * x).
a(C,x,y * x) = a(x,y,x * C).
a(C,x,y * x) = a(x,y,C).
a(x,y,C) = a(C,x,y).
a(C,x,y) = a(x,y,C).
a(x * y,y,C) = a(C,x,y).
a(C,x,y) = a(x,C,y)'.
a(x,C,y)' = a(C,x,y).
a(C,x,y)' = a(x,C,y).
C * a(x,C,y) = R(C,y',x').
a(x,C,y) = a(x,y,C)'.
a(x,y,C)' = a(x,C,y).
x' * R(x,C,y) = a(x,C,y).
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(x,x' * y,C) = x * R(x,C,y)'.
x * a(x,C,y) = R(x,C,y).
x * a(x,y,C) = R(x,C,y').
C * a(x,C,y') = R(C,y,x').
C * a(x,y,C) = R(C,y,x').
x * R(x,C,y)' = a(x,y,C).
a(x,y,C) * x = x * (R(x,C,y)' * x).
x * (R(x,C,y)' * x) = a(x,y,C) * x.
x * a(x,y,C) = a(x,y,C) * x.
a(x,y,C) * x = x * a(x,y,C).
(x * (x * (y * C)))' * (x * ((y * C) * x)) = K(x * y,x * C).
(x * y) * K(x * y,x * C) = (C' * (y * C)) * x.
(x * y) * K(x * y,x * C) = y * x.
R(x,y',z) * (y * z) = (x * (z * K(z,y'))) * y.
(x * (y * K(y,z'))) * z = R(x,z',y) * (z * y).
K(x * y,x * C) = ((x * (y * C))' * (y * C)) * x.
((x * (y * C))' * (y * C)) * x = K(x * y,x * C).
K(x * y,x * C) = K(y * C,x).
(x * y) * K(y * C,x) = y * x.
(x * y)' * (y * x) = K(y * C,x).
K(x * C,y) = K(x,y).
K(C * x,y) = K(x,y).
C * a(x,y,C) = R(C,x,y).
K(R(C,x,y),z) = K(a(x,y,C),z).
K(a(x,y,C),z) = K(R(C,x,y),z).
R(x,y,C) = R(x,C,y').
R(x,C,y') = R(x,y,C).
x * a(x,y,C) = R(x,y,C).
R(x,y,C)' * (a(x,y,C) * x) = K(a(x,y,C),x).
a(x,y,C) * x = R(x,y,C).
R(x,C,y) * y = R(x * y,C,y).
R(x * y,C,y) = R(x,C,y) * y.
R((x * C) * y,C,y) = C * (x * y).
R(C * (x * y),y,C) = (x * C) * y.
R(C * (x * y),x,C) = ((y * K(y,x')) * C) * x.
((x * K(x,y')) * C) * y = R(C * (y * x),y,C).
R(x,y,C)' * R(x,y,C) = K(a(x,y,C),x).
K(a(x,y,C),x) = 1.
1 = K(R(C,x,y),x).
K(R(C,x,y),x) = 1.
(x * R(C,x,y)) * 1 = R(C,x,y) * x.
R(C,x,y) * x = x * R(C,x,y).
R(C,x,y) * (y * x) = (y * x) * R(C,y * x,y).
(x * y) * R(C,x * y,x) = R(C,y,x) * (x * y).
(C * (x * K(x,y'))) * y = R(C * (y * x),y,C).
(x * y) * R(C,y,x) = R(C,y,x) * (x * y).
R(C,x,y) * (y * x) = (y * x) * R(C,x,y).
R(C * (x * y),x,C) = R(C,x',y) * (x * y).
R(C,x',y) * (x * y) = x * (y * C).
R(C,x,y') * (x * y) = x * (y * C).
R(C,x,y) * (y * x) = y * (x * C).
x * (y * C) = (x * y) * R(C,y,x).
(x * y) * R(C,y,x) = x * (y * C).
(x' * (y * x)') * R(C,y',x') = x' * ((y * x)' * C).
((x * y) * y)' * R(C,x',y') = y' * ((x * y)' * C).
(x * (y * y))' * R(C,x',y') = y' * ((x * y)' * C).
(x * (y * y))' * R(C,x,y) = y' * ((x * y)' * C).
((C' * (x * y)) * y)' = (x * (y * y))' * R(C,x,y).
(x * (y * y))' * R(C,x,y) = ((C' * (x * y)) * y)'.
(x * (y * y))' * R(C,x,y) = (x * (y * (y * C')))'.
x * ((y * y) * ((x * (y * y))' * R(C,x,y))) = R(C,y,x).
R(R(C,x,y),y,x * x) = R(C,y,x).
R(R(C,c18,c19),c19,c18 * c18) != R(C,c19,c18).
R(x * (y * ((x * y)' * z)),x,y) = z.
R(R(C,x,y),x * x,y') = R(C,y,x).
R(R(C,c24,c25),c24 * c24,c25') != R(C,c25,c24).
(x * (x * y'))' = y * (x * x)'.
((x * C) * (x * y')) * (y * (x * x)') = R(C,x,x * y').
(x * (x * (y' * C))) * (y * (x * x)') = R(C,x,x * y').
(x * (x * (C * y'))) * (y * (x * x)') = R(C,x,x * y').
(x * (x * (C * y'))) * (y * (x * x)') = R(C,x,y').
(x * (x * (C * y'))) * (y * (x * x)') = R(C,y,x).
(x * R(C,x,y)) * x = R(C,x,y) * (x * x).
(x * (x * R(C,x,y))) * z = x * (R(C,x,y) * (x * z)).
R(C,x,y) * (x * x) = x * (R(C,x,y) * x).
R(C,x,y) * (x * x) = x * (x * R(C,x,y)).
R(C,x',y) * (x * y) = x * (C * y).
R(C,x,y) * (x * y') = x * (C * y').
(x * (R(C,x,y) * (x * y'))) * (y * (x * x)') = R(C,y,x).
(x * (R(C,x,y) * (x * y'))) * (x * (x * y'))' = R(C,y,x).
((x * (x * R(C,x,y))) * y') * (x * (x * y'))' = R(C,y,x).
((R(C,x,y) * (x * x)) * y') * (x * (x * y'))' = R(C,y,x).
R(C,x,y) = R(R(C,y,x),y * y,x').
K(R(C,x,y) * R(C,y,x),z) = 1.
K(R(C,c7,c8) * R(C,c8,c7),c9) != 1.
(C * x) * (y * C) = C * (C * (x * y)).
C * (C * x)' = x'.
(x * (x * y')) * y = x * x.
(x * C)' * (x * C) = K(C,x).
K(C,x) = 1.
R(x,y * x,z) = (x * (y * (x * z))) * ((y * x) * z)'.
(x * (y * (x * z))) * ((y * x) * z)' = R(x,y * x,z).
(x * (y * (x * z')))' = z * (x * (y * x))'.
C * ((C * x) * y) = x * (C * (y * C)).
(C * (x * y)) * (C * y') = C * (x * C).
C * ((C * x) * y) = x * (C * (C * y)).
(C * (x * y)) * (C * y') = x * (C * C).
C * R(x * C,C,y) = (x * y) * (C * (C * y')).
(x * y) * (C * (C * y')) = C * R(x * C,C,y).
C * (x * (C * (y * C))') = (y * (C * x'))'.
C * (x * (y * (C * C))') = (y * (C * x'))'.
K(C * C,x) = 1.
R(C,C,x) * R(y,C,x) = R(y * C,C,x).
C * R(x,C,y) = R(x * C,C,y).
R(x * C,C,y) = C * R(x,C,y).
(C * R(x * C,C,y)) * z = C * (R(x,C,y) * (C * z)).
R(x * C,C,y) * (z * C) = C * (C * (R(x,C,y) * z)).
R(x' * C,C,y) = C * R(x,C,y)'.
(x * y) * (C * (C * y')) = R((x * C) * C,C,y).
R(C * x',C,y) = C * R(x,C,y)'.
(x * y) * (C * (C * y')) = R(x * (C * C),C,y).
(C * R(x * (C * C),C,y)) * (((x * y) * C) * (C * y'))' = R(C,(x * y) * C,C * y').
(C * R(x * (C * C),C,y)) * z = C * (R(x * C,C,y) * (C * z)).
R(C,x,C * y') = R(C,y,x).
R((x * (C * C)) * C,C,y) * z = C * (R(x * C,C,y) * (C * z)).
R(C * (x * (C * C)),C,y) * z = C * (R(x * C,C,y) * (C * z)).
R(C * (x * (C * C)),C,y) * z = C * (R(x * C,C,y) * (z * C)).
R(C * (x * (C * C)),C,y) * z = C * (C * (C * (R(x,C,y) * z))).
R((x * (C * C)) * C,C,y) * (((x * y) * C) * (C * y'))' = R(C,(x * y) * C,C * y').
R(C * (x * (C * C)),C,y) * (((x * y) * C) * (C * y'))' = R(C,(x * y) * C,C * y').
R(C * (x * (C * C)),C,y) * ((C * (x * y)) * (C * y'))' = R(C,(x * y) * C,C * y').
R(C * (x * (C * C)),C,y) * (x * (C * C))' = R(C,(x * y) * C,C * y').
R(C,(x * y) * C,C * y') = R(C * (x * (C * C)),C,y) * (x * (C * C))'.
R(C,(x * y) * C,C * y') = C * (C * (C * (R(x,C,y) * (x * (C * C))'))).
R(C,(x * y) * C,C * y') = C * (C * (x * (C * R(x,C,y)'))').
R(C,(x * y) * C,C * y') = C * (C * (x * R(C * x',C,y))').
R(C,(x * y) * C,C * y') = C * (C * R(C,y',x)').
C * (C * R(C,x',y)') = R(C,y * x,C * x').
R(C,x * y,C * y') = C * (C * R(C,y',x)').
R(C,x * y,C * y') = C * (C * R(C,y,x')').
R(C,x * y,C * y') = C * (C * R(C,x,y)').
C * (C * R(C,x,y)') = R(C,y,x * y).
R(C,x,y * x) = C * (C * R(C,y,x)').
C * (C * R(C,x,y)') = R(C,y,x).
R(C,x,y) * R(C,y,x) = C * C.

end_of_list.
