% --------------------------------------------------------------------------
% Gagola:  Normal 2 => Lemma List 2
% --------------------------------------------------------------------------

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.

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

% define D; A and B are arbitrary constants (for Normality Condition 2)

   R(C,A,B) = D # label("define D").

% commutator (for Normality Conditions 3 and 4)

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

% associator (for Normality Condition 4)

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

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

% defined D is in the commutant

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

end_of_list.

% -------------------------------------------------------------------------
% Lemma List 2: JD supplied lemmas that he believes are true.
% -------------------------------------------------------------------------

formulas(goals).

% D associates with cubes
a(D,x * (x * x),y) = 1 # label("Lemma 2-1").
a(D,x,y * (y * y)) = 1 # label("Lemma 2-2").
a(x,D,y * (y * y)) = 1 # label("Lemma 2-3").
a(x * (x * x),D,y) = 1 # label("Lemma 2-4").
a(x * (x * x),y,D) = 1 # label("Lemma 2-5").
a(x,y * (y * y),D) = 1 # label("Lemma 2-6").

% associators with D in an argument cube to zero
a(D,x,y) * (a(D,x,y) * a(D,x,y)) = 1 # label("Lemma 2-7").
a(x,y,D) * (a(x,y,D) * a(x,y,D)) = 1 # label("Lemma 2-8").
a(x,D,y) * (a(x,D,y) * a(x,D,y)) = 1 # label("Lemma 2-9").

% DR(x,y)^3 = D, xR(D,y)^3 = x, xR(y,D)^3 = x
R(R(R(D,x,y),x,y),x,y) = D # label("Lemma 2-10").
R(R(R(x,D,y),D,y),D,y) = x # label("Lemma 2-11").
R(R(R(x,y,D),y,D),y,D) = x # label("Lemma 2-12").

% R(D,y) and R(y,D) are automorphisms
R(u * v,D,y) = R(u,D,y) * R(v,D,y) # label("Lemma 2-13").
R(u * v,y,D) = R(u,y,D) * R(v,y,D) # label("Lemma 2-14").

% associator identities involving D
a(D,x',y) = a(x',y,D) # label("Lemma 2-15").
a(D,x',y) = a(D',y,x') # label("Lemma 2-16").
a(D,x',y) = a(y,D,x') # label("Lemma 2-17").
a(D,x',y) = a(x',D,y') # label("Lemma 2-18").
a(D,x',y) = a(D',x,y) # label("Lemma 2-19").
a(D,x',y) = a(D',x',y') # label("Lemma 2-20").
a(D,x',y) = a(y',x',D) # label("Lemma 2-21").
a(D,x',y) = a(D,y',x') # label("Lemma 2-22").
a(D,x',y) = a(D,x,y') # label("Lemma 2-23").
a(D,x',y) = a(x,y',D) # label("Lemma 2-24").
a(D,x',y) = a(D',y',x) # label("Lemma 2-25").
a(D,x',y) = a(y',D,x) # label("Lemma 2-26").
a(D,x',y) = a(y,D',x) # label("Lemma 2-27").
a(D,x',y) = a(x,D',y') # label("Lemma 2-28").
a(D,x',y) = a(y',D',x') # label("Lemma 2-29").
a(D,x',y) = a(x',D',y) # label("Lemma 2-30").
a(D,x',y) = a(x,y,D') # label("Lemma 2-31").
a(D,x',y) = a(y,x',D') # label("Lemma 2-32").
a(D,x',y) = a(y',x,D') # label("Lemma 2-33").
a(D,x',y) = a(x',y',D') # label("Lemma 2-34").
a(D,x',y) = a(D,y',x') # label("Lemma 2-35").
a(D,x',y) = a(x,D',y') # label("Lemma 2-36").
a(D,x',y) = a(D',y,x') # label("Lemma 2-37").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

R(R(R(x,y,D),y,D),y,D) = x.
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)'.
D * x = x * D.
R(R(R(c23,c24,D),c24,D),c24,D) != c23.
x'' * 1 = x.
(x * y)' * x = y'.
x * (y * x)' = y'.
(x * (y * x)) * z = x * (y * (x * z)).
(x * (y * (z * y))) * y' = (x * y) * z.
(x' * y) * z = x' * ((y * (z * x)) * x').
x' * ((y * (z * x)) * x') = (x' * y) * z.
R(x',x * y,z) = (y * z) * ((x * y) * z)'.
R(x,y * z,z') = ((x * (y * z)) * z') * y'.
((x * (y * z)) * z') * y' = R(x,y * z,z').
R(x,y,z) = ((x * y) * z) * (z' * y').
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,z,(y * z)') = R(x,y,z) * (z * (y * z)')'.
R(x,y,z) * (z * (y * z)')' = R(x * y,z,(y * z)').
D' * (x * D) = x.
(D * x) * D' = x.
D * (x * D) = x * (D * D).
(x * D) * (y * D) = D * ((x * y) * D).
R(x,y,D) = (D * (x * y)) * (y * D)'.
(D * (x * y)) * (y * D)' = R(x,y,D).
x = x''.
x'' = x.
x * (x' * y) = y.
(x * y') * y = x.
(x * y')' = y * x'.
(x' * y)' = y' * x.
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.
R(x,y,y' * z) = ((x * y) * (y' * z)) * z'.
((x * y) * (y' * z)) * z' = R(x,y,y' * z).
x * (D * x') = D.
x * D' = D' * x.
D' * x = x * D'.
(x * y) * z = (x * z') * (z * (y * z)).
(x * y') * (y * (z * y)) = (x * z) * y.
(x * (y * x)')' = y.
((x * y') * z)' = z' * (y * x').
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).
R(x,D,y * D) = ((x * D) * (y * D)) * (y * (D * D))'.
((x * D) * (y * D)) * (y * (D * D))' = R(x,D,y * D).
R(x,y,D * D) = (D * ((x * y) * D)) * (y * (D * D))'.
(D * ((x * y) * D)) * (y * (D * D))' = R(x,y,D * D).
D * (x * (y * x)) = x * (y * (x * D)).
(D * (x * D)) * y = D * (x * (y * D)).
(x * D) * (y * D) = D * (D * (x * y)).
(D * (x * y)) * (D * y)' = R(x,y,D).
x' * (D * (x * (y * x))) = y * (x * D).
(x * (D * D)) * y = D * (x * (y * D)).
(x * (y * z)) * z' = (x * z) * (z' * y).
x * ((x' * y) * z) = (y * x) * (x' * z).
(x * y) * (y' * z) = y * ((y' * x) * z).
(x * y') * (y * z) = (x * (z * y')) * y.
(x * (y * z')) * z = (x * z') * (z * 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 * D,D,y) = (D * (x * y)) * y'.
(D * (x * y)) * y' = R(x * D,D,y).
R(x * D,D,y)' = y * (D * (x * y))'.
x * (D * (y * x))' = R(y * D,D,x)'.
x * (((y * z') * x)' * y) = R(z,y',x).
x * ((x' * y') * (y * z)) = R(z,y',x).
x * ((x' * D) * y) = R(y * D,D,x).
x * ((D * x') * y) = R(y * D,D,x).
x * ((D * x') * y) = R(D * y,D,x).
x * ((y * x)' * (y * z)) = R(z,(y * z)',x).
R(x,(y * x)',z) = z * ((y * z)' * (y * x)).
x * ((y * x)' * (y * z)) = R(z,y',x).
((x * D)' * D) * ((x * y) * D) = D * R(y,x',D).
x' * R(y,z,x) = (x' * (y * z)) * z'.
x' * R(y,z,x) = z * ((z' * x') * y).
x' * R(y,z,x) = z * ((x * z)' * y).
x * (y * ((x * y)' * z)) = R(z,y,x).
R(x,y,z) = z * (y * ((z * y)' * x)).
R((x * y) * z,y,x) = x * (y * z).
R(x',x * y,z) = R(x,y,z)'.
R(x',y',z) = R(x,(y * x)',z)'.
R(x,(y * x)',z)' = R(x',y',z).
R(x,(y * x)',z) = R(x,y',z).
R(x,y',z)' = R(x',y',z).
R(x,y'',z)' = R(x',y,z).
R(x,y,z)' = R(x',y,z).
R(x * y',z,u)' = R(y * x',z,u).
(x * (y * z'))' = R(z * (x * y)',y,x).
R(x * (y * z)',z,y) = (y * (z * x'))'.
(x * ((x' * y) * z)) * z' = R(y,z * x,x').
R(x,y,z) = R(x,y,y' * z).
R(x,y,y' * z) = R(x,y,z).
R(x,y,(z * y)') = R(x,y,z').
R(x,D,y) = R(x,D,y * D).
R(x,D,y * D) = R(x,D,y).
R(x,y * z,z') = R(x,y * z,y).
R(x,D,y * D') = R(x,D,y).
R(x,y,z) = R(x,z * y,y').
R(x,y * z,z') = R(x,z,y).
R(x,y * z',z) = R(x,z',y).
R(x,y,z') = R(x,z,y * z').
R(x,y,z * y') = R(x,z,y').
R(x,y,z) = R(x,z * y,z).
R(x,y * z,y) = R(x,z,y).
R(x,y * D,D) = R(x,y,D).
R(x,D,y) = R(x,D * y',y).
R(x,D * y',y) = R(x,D,y).
(D * (x * (y * D))) * (D * (y * D))' = R(x,y,D).
R(x,y',D) = R(x,D,y).
R(x,y,D') = R(x,D,y).
R(x,D,y) = R(x,y,D').
(D * (x * D)') * ((x * y) * D) = D * R(y,x',D).
x' * ((x * y) * D) = D * R(y,x',D).
x' * (D * (x * y)) = D * R(y,x',D).
x' * (D * (x * y)) = D * R(y,D,x).
(D * (x * (y * D))) * (D * (D * y))' = R(x,D * D,y).
(D * (D * (x * y))) * (y * (D * D))' = R(x,D,y * D).
(D * (D * (x * y))) * (y * (D * D))' = R(x,y,D * D).
(D * (x * (y * D))) * (D * (y * D))' = R(x,D * D,y).
R(x,y,D * D) = R(x,D,y * D).
R(x,D,y * D) = R(x,y,D * D).
R(x,y,D * D) = R(x,D,y).
R(x,D * D,y) = R(x,y,D).
R(x,y,z) * y = R(x * y,z,(y * z)').
R(x * y,z,(y * z)') = R(x,y,z) * y.
R(x,y,z) * y = R(x * y,z,y').
R(x * y,z,y') = R(x,y,z) * y.
R(x * D,D,y) = R(x,D,y) * D.
R(x,y,D * D) * y = R(x * y,y',D).
D * R(x,D,y) = R(x * D,D,y).
R(x * D,D,y) = D * R(x,D,y).
R(x * D,D,y) = D * R(x,y,D').
x' * (D * (x * y)) = R(y * D,D,x).
x * ((D * x') * y) = D * R(y,x,D').
R((x * y) * D,D,y) = x * (y * D).
R((x * y) * D,D,y) * (y * D)' = x.
(R(x * y,D,y) * D) * (y * D)' = x.
R(x,D,y) * y = R(x * y,y',D).
R(x * y,y',D) = R(x,D,y) * y.
R(x,D,y) * y = R(x * y,D,y).
R(x * y,D,y) = R(x,D,y) * y.
((R(x,D,y) * y) * D) * (y * D)' = x.
R(R(x,D,y),y,D) = x.
R(R((D * x) * D',D,y),y,D) = x.
R(R(D * (D * x)',D,y)',y,D) = x.
x * ((D * x') * y') = D * R(y,x,D')'.
D * R(x,y,D')' = R(D * x',D,y).
R(D * x',D,y) = D * R(x,y,D')'.
R(D * x',D,y) = D * R(x,D,y)'.
R((D * R(D * x,D,y)')',y,D) = x.
R((D * R(x * D,D,y)')',y,D) = x.
R((D * (x * (D * (y * x))'))',x,D) = y.
R(R((D * (x * y)) * (D * y)',y,D),y,D) = x.
a(x * (x * x),y,D) = 1.
(x * y) * z = (x * (y * z)) * a(x,y,z).
(x * (y * z)) * a(x,y,z) = (x * y) * z.
a(c9 * (c9 * c9),c10,D) != 1.
(x * (y * z))' * ((x * y) * z) = a(x,y,z).
R(x,D,y) = ((x * D) * y) * (y * D)'.
((x * D) * y) * (y * D)' = R(x,D,y).
x * (y * (y' * (x' * z))) = z.
D * (x * D') = x.
D * (x * (x * D')) = x * x.
(x' * y) * z = (z * x)' * (z * (y * z)).
(x * y)' * (x * (z * x)) = (y' * z) * x.
R(x,y,z') = ((x * y) * z') * (z * y').
((x * y) * z') * (z * y') = R(x,y,z').
(x * x) * (y * D) = D * (((x * (x * D')) * y) * D).
D * (((x * (x * D')) * y) * D) = (x * x) * (y * D).
x * (y * (y' * z)) = x * z.
x' * ((x * (y * x)) * z) = y * (x * z).
(x * (y * (x * z))) * z' = x * (y * x).
(x * (x * (y * x))) * z = x * ((x * y) * (x * z)).
(x * (x * D')) * y = x * (D' * (x * y)).
(x * y') * (z * y) = (x * (y' * z)) * y.
(x * (y' * z)) * y = (x * y') * (z * y).
x' * ((x * y) * z) = (y * x') * (x * z).
(x * y') * (y * z) = y' * ((y * x) * z).
(x * (y * (z * x)))' * (x * ((y * z) * x)) = a(x,y,z * x).
D * (x * (D' * y)) = (x * D') * (y * D).
(x * D') * (y * D) = D * (x * (D' * y)).
(x * D') * (y * D) = D' * ((D * x) * y).
x' * ((x * (y * z)) * z') = R(y,z,x').
(x' * y') * (y * (x * z)) = y' * (x' * ((x * y) * z)).
(x * D') * (y * D) = D' * ((x * D) * y).
x' * (y * ((y' * x) * z)) = R(z,y,x').
D' * ((x * D) * y) = D * (x * (D' * y)).
x' * (y' * ((y * x) * z)) = R(z,y',x').
x * (D * (D * (y * (D' * z)))) = x * ((y * D) * 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).
(x * (x * (x * D))) * y = x * ((x * D) * (x * y)).
R(x,y,D) = R(x,y * D',D).
R(x,y * D',D) = R(x,y,D).
R(x,D',y) = R(x,y,D).
((x * (x * x)) * D) * y = x * ((x * D) * (x * y)).
(x * ((x * D) * (x * y))) * (y * D)' = R(x * (x * x),D,y).
D * (((x * (x * D')) * y) * D) = x * (x * (y * D)).
D * ((x * (D' * (x * y))) * D) = x * (x * (y * D)).
D * (D * (x * (D' * (x * y)))) = x * (x * (y * D)).
x * (y * (y * (z * D))) = x * ((y * D) * (y * z)).
x * ((y * D) * (y * z)) = x * (y * (y * (z * D))).
a(x,y,z * x) = ((y * (z * x))' * (y * z)) * x.
((x * (y * z))' * (x * y)) * z = a(z,x,y * z).
(x * y)' * (x * (y * z)) = x' * (y' * ((y * x) * z)).
(x * y)' * (x * (y * z)) = R(z,y',x').
R(x,y',z')' = (z * (y * x))' * (z * y).
(x * (y * z))' * (x * y) = R(z,y',x')'.
R(x,y',z')' * x = a(x,z,y * x).
a(x,y,z * x) = R(x,z',y')' * x.
a(x,y,z) = R(x,(z * x')',y')' * x.
R(x,(y * x')',z')' * x = a(x,z,y).
R(x,x * y',z')' * x = a(x,z,y).
R(x,y',z')' * x = a(x,z,y).
R(x,y',D)' * x = a(x,y,D).
R(x,D,y)' * x = a(x,y,D).
(x * (x * (x * (y * D)))) * (y * D)' = R(x * (x * x),D,y).
R(x * (x * x),D,y) = x * (x * x).
(x * (x * x))' * (x * (x * x)) = a(x * (x * x),y,D).
a(x * (x * x),y,D) = (x * (x * x))' * (x * (x * x)).
a(x * (x * x),D,y) = 1.
a(c7 * (c7 * c7),D,c8) != 1.
R(x,y',D) = R(x,y,D').
R(x,D',y') = R(x,y,D').
a(x,y,x * D) = R(x,D',y')' * x.
a(x,y,z' * x) = R(x,z,y')' * x.
a(x,y,x * D) = R(x,y,D')' * x.
a(x,y,x * D) = a(x,D,y' * x).
a(x,D,y' * x) = a(x,y,x * D).
a(x,y,z * x) = a(x,y,z).
a(x,y,x * D) = a(x,y,D).
a(x,D,y') = a(x,y,x * D).
a(x,y,x * D) = a(x,D,y').
a(x,D,y') = a(x,y,D).
a(x,D,y) = a(x,y',D).
a(x,y',D) = a(x,D,y).
1 = a(x * (x * x),D,y).
a(D,x',y) = a(x',D,y').
a(c37',D,c38') != a(D,c37',c38).
(x' * y') * ((y * x) * z) = z.
((x * y) * z) * a(x,y,z)' = x * (y * z).
(x * y) * z = x * ((y * (z * x')) * x).
x * ((y * (z * x')) * x) = (x * y) * z.
((x * y) * z)' * (x * (y * z)) = a(x,y,z)'.
(x * (y' * z))' = (z' * y) * x'.
x' * (((x * y) * z) * u) = (y * (z * x')) * (x * u).
(x * (y * z')) * (z * u) = z' * (((z * x) * y) * u).
((x * y) * (x * z))' * (x * (y * (x * z))) = a(x * y,x,z).
((x' * y) * z') * ((z * y') * x) = a(z,y',x).
(x' * (y * z)') * (y * (z * x)) = a(y,z,x)'.
(x' * (y' * z')) * (z * (y * x)) = a(z,y,x)'.
((x' * y) * (z * y)') * (z * x) = a(z * y,y',x).
x' * (((x * y') * z') * (z * y)) = a(x,z,y)'.
x' * (((x * y') * (y * z')) * z) = a(x,z,y)'.
(x' * ((x * y') * z')) * (z * y) = a(z,y,x)'.
((x' * y) * (y' * z')) * (z * x) = a(z * y,y',x).
((x' * y') * (y'' * z')) * (z * x) = a(z * y',y,x).
a(x * 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,x * z).
a(x * D,D,y)' = a(D,x,D * y).
a(x * D,D,y)' = a(D,x,y * D).
a(x,y,z'' * x) = a(x,y,z).
((x' * y') * (y * z')) * (z * x) = a(z * y',y,x).
(x' * ((x * y') * z')) * (z * y) = a(z * x',x,y).
a(x * y',y,z) = a(x,z,y)'.
a(x,y,z) = a(x * y,z,y)'.
a(x * y,z,y)' = a(x,y,z).
a(x * D,D,y')' = a(x,D,y).
a(x,D,y) = a(D,x,y' * D).
a(D,x,y' * D) = a(x,D,y).
a(x,D,y') = a(D,x,y).
a(D,x,y) = a(x,D,y').
a(D,x',y) = a(x',y,D).
a(c31',c32,D) != a(D,c31',c32).
a(D,x,y) = a(x,y,D).
a(D,x * (x * x),y) = 1.
a(D,c1 * (c1 * c1),c2) != 1.
a(D,x',y) = a(x',D',y).
a(c61',D',c62) != a(D,c61',c62).
((x * y') * (y * z))' * (x * z) = a(x * y',y,z).
((x * y') * (y * z))' * (x * z) = a(x,y',y * z)'.
a(x,y',y * z)' = a(x * y',y,z).
a(x',y,z)' = a(x' * y,x',x * z).
a(x' * y,x',x * z) = a(x',y,z)'.
a(x,y',y * 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',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,z) = a(x',y,z * x).
a(x',y,z * x) = a(x',y,z).
a(x,y,z)' = a(z',z * x,y).
a(x',x * y,z) = a(y,z,x)'.
a(x',x * y,z)' = a(y,z,x).
a(x',x * y,z * x) = a(y,z,x)'.
a(x,y,z) = a(x,z',z * y).
a(x,y',y * z) = a(x,z,y).
a(x,D',y * D) = a(x,y,D).
a(x * y,z,y)' = 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,D',y) = a(x,y,D).
a(D,x,y) = a(x,D',y).
a(D,x',y) = a(y',x',D).
a(c44',c43',D) != a(D,c43',c44).
x' * ((x * y) * (z * x)) = (y * z) * x.
(x * (y' * z')) * (z * y) = x.
R(x,y,z) * (y * z) = (x * y) * z.
((x * y') * z') * (z * y) = R(x,y',z').
x' * ((x * y) * z) = (y * (z * x')) * x.
(x * (y * z')) * z = z' * ((z * x) * y).
x * ((x' * y) * z') = (y * x) * (z * x)'.
(x * y) * (z * y)' = y * ((y' * x) * z').
x' * R(x,y',z') = a(x,z,y)'.
x' * (y' * (z' * ((z * y) * x))) = a(x,y,z)'.
x' * (y' * (z * ((z' * y) * x))) = a(x,y,z')'.
(x * ((x' * y') * z')) * (z * y) = a(z * x,x',y).
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 * ((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).
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')'.
a(x,D,y' * z) = a(x,z' * y,D).
a(x,y' * z,D) = a(x,D,z' * y).
a(x,D,y' * x) = a(y,D,x')'.
a(x,D,y')' = a(y,D,x').
a(x,D,y')' = a(y,x,D).
a(x,D,y)' = a(y',x,D).
a(x,y,D)' = a(y,x,D).
a(x,y,z)' = a(x * y,z,y).
a(x * y,z,y) = a(x,y,z)'.
a(D * x,y,D) = a(x,D,y)'.
a(D,x,y)' = a(y,x,D).
a(x,D * y,D) = a(x,y,D).
a(D,x,y)' = a(y,D * x,D).
a(x,D * y,D) = a(D,y,x)'.
a(D,x,y)'' = a(D * x,y,D).
a(D * x,y,D) = a(D,x,y)''.
a(D * x,y,D) = a(D,x,y).
a(D,x,y) = a(x,D,y)'.
a(x,D,y)' = a(D,x,y).
a(D,x,y) = a(y',x,D).
a(x',y,D) = a(D,y,x).
a(D,x',y) = a(D,y',x').
a(D,c72',c71') != a(D,c71',c72).
a(D,c71',c72) != a(D,c72',c71').
a(x,D,y)' = a(D,y',x).
a(D,x,y) = a(D,y',x).
a(D,x',y) = a(D,y,x).
a(D,c46',c45') != a(D,c45',c46).
a(D,c45',c46) != a(D,c46',c45').
a(D,x',y) = a(y,D,x').
a(D,c35',c36) != a(c36,D,c35').
a(c36,D,c35') != a(D,c35',c36).
a(D,x,y) = a(D,y,x)'.
a(D,x,y)' = a(D,y,x).
a(D,x,y)' = a(x,D,y).
a(x,D,y) = a(D,y,x).
a(D,x,y) = a(y,D,x).
a(x,D,y * (y * y)) = 1.
a(c5,D,c6 * (c6 * c6)) != 1.
a(x,D,y) = a(y,x,D).
a(x,y * (y * y),D) = 1.
a(c11,c12 * (c12 * c12),D) != 1.
a(D,x,y * (y * y)) = 1.
a(D,c3,c4 * (c4 * c4)) != 1.
a(D,x',y) = a(y',D,x).
a(c54',D,c53) != a(D,c53',c54).
a(x',D,y) = a(D,y',x).
a(D,x',y) = a(y',D',x').
a(c60',D',c59') != a(D,c59',c60).
a(x',D',y) = a(D,y,x).
a(D,x',y) = a(y,D',x).
a(D,c55',c56) != a(c56,D',c55).
a(c56,D',c55) != a(D,c55',c56).
a(D,x',y) = a(x,y',D).
a(D,c49',c50) != a(c49,c50',D).
a(c49,c50',D) != a(D,c49',c50).
a(D,x,y') = a(y,x,D).
a(D,x',y) = a(D,x,y').
a(D,c47',c48) != a(D,c47,c48').
a(D,x',y) = a(y,x,D).
a(D,x,y') = a(D,x',y).
a(D,x',y) = a(x,D',y').
a(D,c73',c74) != a(c73,D',c74').
a(c73,D',c74') != a(D,c73',c74).
a(x,D',y') = a(x,D,y).
a(D,x',y) = a(x,D,y).
a(x,D',y') = a(D,x',y).
a(D,c57',c58) != a(c57,D',c58').
a(c57,D',c58') != a(D,c57',c58).
a(D,x',y) = a(D',y,x').
a(D',c76,c75') != a(D,c75',c76).
a(x,D,y)' = a(D,x * D',y * D).
a(D,x * D',y * D) = a(x,D,y)'.
a(D,x * D',y) = a(x,D,y)'.
a(D',x,y) = a(x * D',y,D)'.
a(x * D',y,D)' = a(D',x,y).
a(x * D',y,D) = a(x,D,y)'.
a(x * D',y,D) = a(D,x,y).
a(D,x,y)' = a(D',x,y).
a(D',x,y) = a(D,y,x).
a(D',c34,c33') != a(D,c33',c34).
a(D,x',y) = a(D',x',y').
a(D',c41',c42') != a(D,c41',c42).
a(x,D,y) = a(D,x,y').
a(D,x,y') = a(x,D,y).
a(D,x,y')' = a(D,x,y).
a(D',x,y') = a(D,x,y).
a(D,x',y) = a(D',x,y).
a(D',c39,c40) != a(D,c39',c40).
a(D,x,y)' = a(y,D,x').
a(D,x,y)' = a(D,x',y).
a(D',x,y) = a(D,x',y).
a(D,x',y) = a(D',y',x).
a(D',c52',c51) != a(D,c51',c52).
a(D',x',y) = a(D,y',x).
a(D,x',y) = a(x',y',D').
a(c69',c70',D') != a(D,c69',c70).
a(x,y,y' * z) = a(x,z,y').
a(x,D,y) = a(x,y * D,D').
a(x,y * D,D') = a(x,D,y).
a(x,y',(y * z) * y) = a(x,z,y).
a(x,y',y * (z * y)) = a(x,z,y).
a(x,y,z) = a(x,y * z,z).
a(x,y * z,z) = a(x,y,z).
a(x,y,z') = a(x,y * z,z').
a(x,y * z,z') = a(x,y,z').
a(x,y,D') = a(x,D,y).
a(x,D,y) = a(x,y,D').
a(D,x,y) = a(x,y',D').
a(D,x',y) = a(y,x',D').
a(D,c65',c66) != a(c66,c65',D').
a(c66,c65',D') != a(D,c65',c66).
a(D,x,y) = a(y,x,D').
a(D,x',y) = a(x,y,D').
a(D,c63',c64) != a(c63,c64,D').
a(c63,c64,D') != a(D,c63',c64).
a(D,x',y) = a(y',x,D').
a(c68',c67,D') != a(D,c67',c68).
a(x',y,D') = a(D,y',x).
R(R(R(x,D,y),D,y),D,y) = x.
R(R(R(c21,D,c22),D,c22),D,c22) != c21.
(x * (x * y)) * y' = x * x.
R(x,y * z,z) = ((x * (y * z)) * z) * (y * (z * z))'.
((x * (y * z)) * z) * (y * (z * z))' = R(x,y * z,z).
D * (x * x) = x * (x * D).
D * ((x * D) * y) = x * (D * (y * D)).
x * (y * (x * x))' = (y * x)'.
(x * (y * z'))' = (z * y') * x'.
R(x,y * (y * z),z') = ((x * (y * (y * z))) * z') * (y * y)'.
((x * (y * (y * z))) * z') * (y * y)' = R(x,y * (y * z),z').
(x * (x * D)) * y = x * (D * (x * y)).
R(x,y,D)' = (y * D) * (D * (x * y))'.
(x * D) * (D * (y * x))' = R(y,x,D)'.
(x * (x * D)) * ((y * D) * (x * x))' = R(y,D,x * x)'.
D * R(x,y,D)' = y * (D * ((D * (x * y))' * D)).
x * (D * ((D * (y * x))' * D)) = D * R(y,x,D)'.
R(x,y * (y * z),z') = R(x,z,y * y).
R(x,y,D) = R(x,D,y').
R(x,D,y') = R(x,y,D).
x * (D * (y * x)') = D * R(y,x,D)'.
(((x * y) * z) * z) * (y * (z * z))' = R(R(x,y,z),y * z,z).
R(x * D,D,y') = R(x,y,D) * D.
R(x,y,D) * D = R(x * D,y,D).
R(x * D,y,D) = R(x,y,D) * D.
D * R(x * D,y,D)' = R(x,y,D)'.
R(x,D,y * y)' = y * (D * (y * ((x * D) * (y * y))')).
x * (D * (x * ((y * D) * (x * x))')) = R(y,D,x * x)'.
x * (D * ((y * D) * x)') = R(y,D,x * x)'.
R(x,D,y * y)' = D * R(x * D,y,D)'.
R(x,D,y * y)' = R(x,y,D)'.
((x * y) * (z * z)) * (y * (z * z))' = R(R(x,y,z),y * z,z).
R(x,y,z * z) = R(R(x,y,z),y * z,z).
R(R(x,y,z),y * z,z) = R(x,y,z * z).
((x * (y * (y * D))) * D') * (y * y)' = R(x,y * (D * y),D').
((x * x) * (y * (z * (x * (x * y)))'))' = R(z,x * (x * y),y').
((x * x) * (D * (y * (x * (x * D)))'))' = R(y,x * (D * x),D').
(x * (x * (y * (z * (x * (x * y)))')))' = R(z,x * (x * y),y').
(x * (x * (D * (y * (x * (x * D)))')))' = R(y,x * (D * x),D').
(x * (x * (y * (z * (x * (x * y)))')))' = R(z,y,x * x).
R(x,y,z * z)' = z * (z * (y * (x * (z * (z * y)))')).
x * (x * (y * (z * (x * (x * y)))')) = R(z,y,x * x)'.
x * (x * (D * (y * (x * (x * D)))')) = R(y,x,D)'.
R(x,y,D)'' = R(x,y * (D * y),D').
R(x,y * (D * y),D') = R(x,y,D)''.
R(x,y * (D * y),D') = R(x,y,D).
R(x,y * (y * D),D') = R(x,y,D).
R(x,y,D) = R(x,D,y * y).
R(x,D,y * y) = R(x,y,D).
R(R(x,D,y),D,y * y) = x.
R(R(R(x,D,y),D,y),D * y,y) = x.
R(R(R(x,D,y),D,y),y * D,y) = x.
x = R(R(R(x,D,y),D,y),D,y).
R(R(R(D,x,y),x,y),x,y) = D.
x * y = (y * x) * K(x,y).
(x * y) * K(y,x) = y * x.
R(R(R(D,c19,c20),c19,c20),c19,c20) != D.
(x * x)' * y = x' * (x' * y).
(x * y)' * (x * (y * y)) = y.
x' * ((x * y) * x) = y * x.
(x * y) * (z * x) = z' * ((z * x) * (y * (z * x))).
x' * ((x * y) * (z * (x * y))) = (y * z) * (x * y).
(x * y) * (x * (z * x)) = x * ((y * (x * z)) * x).
(x * y)' * (y * x) = K(y,x).
R(D,x,y) = ((x * D) * y) * (x * y)'.
((x * D) * y) * (x * y)' = R(D,x,y).
(x * (y * D)) * a(x,D,y) = (x * D) * y.
x * (y * z) = z * (((z' * x) * y) * z).
x * (((x' * y) * z) * x) = y * (z * x).
(x * (x * y')) * z = (x * y') * (y * ((x * y') * z)).
(x * y') * (y * ((x * y') * z)) = (x * (x * y')) * z.
R(x * y',y,z) = (x * z) * (y * z)'.
x' * y = (y * x)' * (y * y).
(x * y)' * (x * x) = y' * x.
(x * y)' * (y * x) = K(x,y)'.
x' * y = y * ((x * y)' * y).
x * ((y * x)' * x) = y' * x.
x * (x * (y * x))' = (x * y)'.
x * (y * (x * (z * x)))' = ((y * x) * z)'.
x' * (y * z) = z * (((x * z)' * y) * z).
x * (((y * x)' * z) * x) = y' * (z * x).
((x' * y) * z)' = z' * (y' * x).
((x * D) * y) * (x * (D * D)) = (x * D) * ((y * D) * (x * D)).
(x * y) * a(x,(z * y)',z * (y * y)) = (x * (z * y)') * (z * (y * y)).
x' * (y * x) = (x' * y) * x.
(x' * y) * x = x' * (y * x).
(x' * y') * (x * y) = K(x,y).
(x * y') * (x' * y) = K(x',y).
K(x,y)' = K(y,x).
x * (x * y)' = (x * (y * x'))'.
(x * (y * x'))' = x * (x * y)'.
(x * x)' * D = x' * (D * x').
x * ((x * x)' * y) = x' * y.
R(x,(y * z)',y * (z * z)) * z = (x * (y * z)') * (y * (z * z)).
(x * (x * y)') * y = K(x',x * y).
D * (x * x)' = x' * (D * x').
x' * (D * x') = D * (x * x)'.
(x' * (y * x')) * (x * z) = x' * (y * z).
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) * 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).
(x * (y * (x * z'))) * z = x * (y * x).
(x * y) * z = x * ((y * x') * (x * z)).
x * ((y * x') * (x * z)) = (x * y) * z.
D * ((x * D) * y) = x * (y * (D * D)).
((x * D) * ((y * x)' * x)) * (y' * x)' = R(D,x,(y * x)' * x).
(D * ((x * D) * y)) * x = x * ((y * (D * D)) * x).
D * ((D * x) * y) = x * (y * (D * D)).
(x * D) * ((x * ((y * (x * D)) * D)) * a(x,D,y * (x * D)))' = ((x * D) * y)'.
x * K(x,y) = (y' * x) * y.
(x' * y) * x = y * K(y,x).
x' * ((y' * x) * y) = K(x,y).
x * K(x,y) = y' * (x * y).
x' * (y * x) = y * K(y,x).
x' * (y' * (x * y)) = K(x,y).
x' * (y' * (x * y)) = K(x,x * y).
(((x * y)' * y) * x)' = K(x,y).
K(x,y)' = ((x * y)' * y) * x.
((x * y)' * y) * x = K(x,y)'.
((x * y)' * y) * x = K(y,x).
(x * (y * x'))' * y = K(x',y).
(x * (x * y)') * y = K(x',y).
K(x',y) = K(x',x * y).
K(x',x * y) = K(x',y).
K(x,x * y) = K(x,y).
K(x * y,x) = K(x * y,y').
K(x * y,y') = K(x * y,x).
K(x,y)' = K(x * y,x).
K(x * y,x) = K(x,y)'.
K(x * y,x) = K(y,x).
K(x * y,y') = K(y,x).
K(x * y',y) = K(y',x).
(x * (y * z)) * (z' * u) = z * (((z' * x) * y) * u).
x * ((y * x') * z') = (x * y) * (z * x)'.
(x * y) * (z * x)' = x * ((y * x') * z').
((x * y) * a(x,y,z')) * z = (x * y) * ((x * (y * z'))' * (x * y)).
x * (((y * x)' * D) * x) = y' * (x * D).
((x * (y * y)') * (y * z)) * (z' * y) = R(x,(y * y)',y * z).
x * ((D * (y * x)') * x) = y' * (x * D).
(x * (y * z'))' * (x * y) = R(z,y',x').
(D * (x * x)') * (x * y) = x' * (D * y).
(D * (x * x)') * (x * y) = x' * (y * D).
(x * y) * (z * y)' = y * (z * (x' * y))'.
(x * D) * (y * x)' = R(D * y',D,x).
R(x',y,z)' = R(x,y,z).
R(x,y,z)' = R(u * (x * u)',y,z).
R(x * (y * x)',z,u) = R(y,z,u)'.
R(D,x * D,y) = R(D,x,y).
R(x,y,z)' = z * (y * (x * (z * y))').
x * (y * (z * (x * y))') = R(z,y,x)'.
(x * ((D * (x * y)) * x)) * (x * (x * (y * x)))' = R(D,x,x * (y * x)).
R(x,y,z) = R(x,y,y * z).
R(x,y,y * z) = R(x,y,z).
R(x,(y * z)',z) = R(x,(y * z)',y * (z * z)).
R(x,(y * z)',y * (z * z)) = R(x,(y * z)',z).
R(x,y,z' * y) = R(x,y,(z * y)' * y).
R(x,y,(z * y)' * y) = R(x,y,z' * y).
R(x * y',y,z) = (x * (y * z)) * (y * (y * z))'.
(x * (y * z)) * (y * (y * z))' = R(x * y',y,z).
(D * ((x * D) * y)) * x = x * (D * (y * (x * D))).
R(x,y',z) = R(x,(y * z)',z).
R(x,(y * z)',z) = R(x,y',z).
R(x,y',D') = R(x,y,D).
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 * D)) * D)) * a(x,D,y * (x * D)) = x * (D * ((y * x) * D)).
x * a(x,y,z)' = R(x,z',y').
x * a(x,y,z')' = R(x,z,y').
(x * (y * z)) * (z' * y) = z * ((z' * x) * (y * y)).
D * R(x,y,D) = R(x * D,y,D).
R(x * D,y,D) = D * R(x,y,D).
R(x' * D,y,D) = D * R(x,y,D)'.
R(D * x',y,D) = D * R(x,y,D)'.
x * (D * (y * x)') = R(D * y',x,D).
x * ((y * x)' * D) = R(D * y',x,D).
R(D,x,y) = y * R(D * y',x,D).
x * R(D * x',y,D) = R(D,y,x).
(x * D') * (D * ((x * D') * y)) = x * (D' * (x * y)).
(x' * y) * (x * ((x' * y) * z)) = (x' * (y * y)) * z.
(x * D') * (D * ((D' * x) * y)) = (D' * (x * x)) * y.
(x * D') * (D * ((x * D') * y)) = (D' * (x * x)) * y.
(D' * (x * x)) * y = x * (D' * (x * y)).
R(D',x * x,y) * ((x * x) * y) = x * (D' * (x * y)).
R(D,x * x,y)' * ((x * x) * y) = x * (D' * (x * y)).
D * ((D * ((x * D) * y)) * x) = (x * D) * ((y * D) * (x * D)).
(x * D) * ((y * D) * (x * D)) = D * ((D * ((x * D) * y)) * x).
(x * y) * R(z,y',x') = x * (y * z).
R(x,y,D)' * x = a(x,D,y).
R(x,y,D) * x' = a(x',D,y).
K(a(x',D,y),x) = K(x',R(x,y,D)).
(x * D) * ((y * D) * (x * D)) = D * (x * (D * (y * (x * D)))).
(D * (x * (D * (y * (x * D))))) * z = (x * D) * ((y * D) * ((x * D) * z)).
D * a(x,y,D) = R(D,x',y').
a(x,y,D)' = a(D,x,y)'.
a(D,x,y)' = a(x,y,D)'.
a(D,x,y)' * a(x,y,D) = 1.
a(x,y,z * (y * y)) = a(x,y,z * y).
a(x,D,y)' = a(x,y,D).
a(D,x,y')' = a(x,y,D).
a(x,D,y) * a(x,y,D) = 1.
a(x',y,D) = a(y,x,D).
a(x,y,D) = a(x',D,y).
a(x',D,y) = a(x,y,D).
(a(x,y,D) * z)' = z' * a(x,D,y).
x * a(x,y,D) = R(x,y',D').
K(a(x,y,D),x) = K(x',R(x,y,D)).
D * a(x,y,D) = R(D,y,x').
D * a(x',y,D) = R(D,y,x).
D * a(x,y,D) = R(D,x,y).
D' * R(D,x,y) = a(x,y,D).
R(D,x,y) = R(D,x',y').
R(D,x',y') = R(D,x,y).
R(D,x,y) = R(D,y,x').
R(D,x,y') = R(D,y,x).
R(D,x',y) = R(D,y,x).
R(D,x,y * x) = R(D,x,y).
(D * (x * (D * (y * (x * D))))) * ((x * D) * (y * (x * D)))' = R(D,x * D,y).
D' * R(D,x,y) = a(x',y',D).
x * a(x,y,D) = R(x,y,D).
R(x,y,D) * K(a(x,y,D),x) = a(x,y,D) * x.
x * R(x',y,D) = a(x',y,D).
(x * R(x,y,D)') * a(x,y,D) = K(x',a(x,y,D)).
K(x',R(x,y,D)) = K(x',a(x,y,D)).
K(x',a(x,y,D)) = K(x',R(x,y,D)).
K(R(x,y,D),x) = K(a(x,y,D),x).
K(a(x,y,D),x) = K(R(x,y,D),x).
x * a(x,D,y) = R(x,y',D).
x * a(x,D,y) = R(x,D,y).
x * R((x * x)',D,y) = x' * a((x * x)',D,y).
x' * a((x * x)',D,y) = x * R((x * x)',D,y).
x * R(x,y,D)' = a(x',y,D).
a(D,x',y) = x * R(x,y,D)'.
x * R(x,y,D)' = a(D,x',y).
K(x',R(x,y,D)) = K(R(x,y,D),x).
K(R(x,y,D),x) = K(x',R(x,y,D)).
a(x,y,z * (y * y)) = a(x,(z * y)',z * (y * y)).
a(x,(y * z)',y * (z * z)) = a(x,z,y * (z * z)).
a(x,y,z * (y * y)) = a(x,y,z).
R(x,y,D) * K(R(x,y,D),x) = a(x,y,D) * x.
a(D,x',y) * a(x,y,D) = K(x',a(x,y,D)).
a(D,x',y) * a(x,y,D) = K(x',R(x,y,D)).
a(x,D,y) * a(x,y,D) = K(x',R(x,y,D)).
K(x',R(x,y,D)) = 1.
K(R(x,y,D),x) = 1.
R(x,y,D) * 1 = a(x,y,D) * x.
a(x,y,D) * x = R(x,y,D) * 1.
a(x,y,D) * x = R(x,y,D).
x' * a((x * x)',D,y) = x * R(x * x,D,y)'.
a(x,(y * z)',y * (z * z)) = a(x,z,y).
(a((x * x)',y,D) * x)' = x * R(x * x,D,y)'.
(a(D,(x * x)',y) * x)' = x * R(x * x,D,y)'.
(x' * (y * D)) * (y' * x) = R(D,(x * x)',x * y).
R(D,(x * x)',x * y) = (x' * (y * D)) * (y' * x).
R(x,(y * y)',y * z) = z * ((z' * (x * (y * y)')) * (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(D,(x * x)',y) = (x' * (y * D)) * (y' * x).
(x' * (y * D)) * (y' * x) = R(D,(x * x)',y).
(x' * (y * D)) * (y' * x) = R(D,y,x * x).
R(x,(y * z)',z) * z = (x * (y * z)') * (y * (z * z)).
(x * (y * z)') * (y * (z * z)) = R(x,(y * z)',z) * z.
(x * ((D * (y * x)') * x)) * (y' * x)' = R(D,x,(y * x)' * x).
(x' * (y * D)) * (x' * y)' = R(D,y,(x * y)' * y).
R(D,x,(y * x)' * x) = (y' * (x * D)) * (y' * x)'.
R(D,x,(y * x)' * x) = (y' * (x * D)) * (x' * y).
R(D,x,(y * x)' * x) = R(D,x,y * y).
R(D,x,y * y) = R(D,x,y' * x).
R(D,x,y' * x) = R(D,x,y * y).
R(D,x,y * y) = R(D,x,y').
R(D,x,y * y) = R(D,y,x).
D' * R(D,x,y) = a(y',(x * x)',D).
a(x',(y * y)',D) = D' * R(D,y,x).
a(x',(y * y)',D) = a(y,x,D).
a(x,y,D) = a(D,(x * x)',y).
a(D,(x * x)',y) = a(x,y,D).
(a(x,y,D) * x)' = x * R(x * x,D,y)'.
x * R(x * x,D,y)' = (a(x,y,D) * x)'.
x * R(x * x,D,y)' = R(x,y,D)'.
R(D,x,x * (y * x)) = x * ((D * (x * y)) * (x * (x * (x * (y * x)))')).
x * ((D * (x * y)) * (x * (x * (x * (y * x)))')) = R(D,x,x * (y * x)).
x * ((D * (x * y)) * ((x * x) * y)') = R(D,x,x * (y * x)).
x * ((D * (x * y)) * (x * (x * y))') = R(D,x,x * (y * x)).
x * R(D * x',x,y) = R(D,x,x * (y * x)).
R(D,x,x * (y * x)) = x * R(D * x',x,y).
x * R(D * x',x,y) = R(D,x,y * x).
x * R(D * x',x,y) = R(D,x,y).
(x * y) * a(x,(z * y)',z * (y * y)) = R(x,(z * y)',y) * y.
(x * y) * a(x,(z * y)',z * (y * y)) = R(x,z',y) * y.
(x * y) * a(x,y,z) = R(x,z',y) * y.
(R(x,y'',z) * z) * y = (x * z) * ((x * (z * y'))' * (x * z)).
(R(x,y,z) * z) * y = (x * z) * ((x * (z * y'))' * (x * z)).
(R(x,y,z) * z) * y = (x * z) * R(y,z',x').
(R(x,y,z) * z) * y = x * (z * y).
((R(x,y,z) * z) * y) * (z * y)' = x.
R(R(x,y,z),z,y) = x.
(x * ((y * (x * D)) * D)) * a(x,D,y * (x * D)) = x * (D * (D * (y * x))).
(D * (x * (D * (y * (x * D))))) * (x * (D * ((y * x) * D)))' = R(D,x * D,y).
(D * (x * (D * (y * (x * D))))) * (x * (D * (D * (y * x))))' = R(D,x * D,y).
(D * (x * (D * (y * (x * D))))) * (x * (D * (D * (y * x))))' = R(D,x,y).
R(D,x,y) = (x * D) * ((y * D) * ((x * D) * (x * (D * (D * (y * x))))')).
(x * D) * ((y * D) * ((x * D) * (x * (D * (D * (y * x))))')) = R(D,x,y).
(x * D) * (x * (D * (D * (y * x))))' = ((x * D) * y)'.
(x * D) * ((y * D) * ((x * D) * y)') = R(D,x,y).
(x * D) * R(D * (x * D)',D,y) = R(D,x,y).
(x * D) * R(x,D,y)' = R(D,x,y).
(x * (x * D)) * R(x * x,D,y)' = R(D,x * x,y).
R(D,x * x,y) = x * (D * (x * R(x * x,D,y)')).
x * (D * (x * R(x * x,D,y)')) = R(D,x * x,y).
x * (D * R(x,y,D)') = R(D,x * x,y).
x * R(D * x',y,D) = R(D,x * x,y).
R(D,x * x,y) = R(D,y,x).
R(D,x,y)' * ((y * y) * x) = y * (D' * (y * x)).
R(D,x,y)' * (y * (y * x)) = y * (D' * (y * x)).
x * ((x * y) * (x * (D' * (x * y)))') = R(R(D,y,x)',x * y,x)'.
x * ((D * (x * y)) * (x * (x * y))') = R(R(D,y,x)',x * y,x)'.
x * R(D * x',x,y) = R(R(D,y,x)',x * y,x)'.
R(R(D,x,y)',y * x,y)' = y * R(D * y',y,x).
R(R(D,x,y)',y * x,y)' = R(D,y,x).
R(R(D,x,y)',x,y)' = R(D,y,x).
R(D,x,y) = R(R(D,y,x),y,x).
R(R(D,x,y),x,y) = R(D,y,x).
a(x,D,y) * (a(x,D,y) * a(x,D,y)) = 1.
a(c17,D,c18) * (a(c17,D,c18) * a(c17,D,c18)) != 1.
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) * y = x * (x * (y * y)).
x * y = (x * y') * (y * y).
(x * y') * (y * y) = x * y.
D * (D * x)' = x'.
x * (y * (y * x))' = (y * y)'.
(x * y) * (R(z,x,y) * ((z * x) * y))' = (R(z,x,y) * R(z,x,y))'.
(x * (x * y)) * y = x * (x * (y * y)).
x * (y * (x * y)) = (x * y) * (x * y).
(x * y) * (x * y) = x * (y * (x * y)).
(x * (y * z)') * (y * (z * (y * z))) = x * (y * z).
(x * y) * ((z * (z * x)) * y)' = R(z * z,x,y)'.
(x * (y * (D * D)))' * ((x * D) * (y * D)) = a(x,D,y * D).
(x * (y * (D * D)))' * (D * ((x * y) * D)) = a(x,y,D * D).
R(x,y,z) * ((x * y) * z) = (x * (x * y)) * z.
(x * (y * (D * D)))' * (D * (D * (x * y))) = a(x,D,y * D).
(x * (y * (D * D)))' * (D * (D * (x * y))) = a(x,y,D * D).
R(x,y,z')' * x = a(x,z,y').
a(x',y,z) * x = R(x',z',y')'.
a(x * x,y,z) * x' = R(x * x,z',y')' * x.
R(x * x,y',z')' * x = a(x * x,z,y) * x'.
a(x * y,z,y) = a(x * y,z,x').
a(x * y,z,x') = a(x * y,z,y).
D * (R(D,x,y')' * R(D,x,y')') = R(D,x,y')' * a(D,y,x').
D * (R(D * D,x,y')' * D) = a(D * D,y,x').
a(x',y,z) * x = R(x,z',y').
x * R(x * x,y',z')' = (a((x * x)',z,y) * x)'.
(a((x * x)',y,z) * x)' = x * R(x * x,z',y')'.
D * (D * R(D * D,x,y')') = a(D * D,y,x').
D * R(D * D,x',y')' = a(D * D,y,x) * D'.
a(D * D,x,y) * D' = D * R(D * D,y',x')'.
a(D * D,x,y) * D' = (a((D * D)',x,y) * D)'.
(a((D * D)',x,y) * D)' = a(D * D,x,y) * D'.
a(x * y,z,x') = a(x,y,z)'.
a(x' * y,z,x) = a(x',y,z)'.
a(x,D,D * y) = a(x,D,y).
(x * (y * (D * D)))' * (D * (D * (x * y))) = a(x,D,y).
a(x,D,D * y') = a(x,y,D).
D * a(x,D,y) = R(D,y',x').
a(x,y,D)' = a(x,D,y).
(a(x,D,y) * z)' = z' * a(x,y,D).
(x * a(y,z,D))' = a(y,D,z) * x'.
D * R(D,x,y)' = a(x,y,D)'.
D * a(x,D,y) = R(D,y,x).
a(x,y,D) * R(D,x,y) = D' * (R(D,x,y) * R(D,x,y)).
D' * (R(D,x,y) * R(D,x,y)) = a(x,y,D) * R(D,x,y).
(D' * a(x,y,D)) * R(D,x,y) = D' * (D' * (R(D,x,y) * R(D,x,y))).
D' * (D' * (R(D,x,y) * R(D,x,y))) = (D' * a(x,y,D)) * R(D,x,y).
(x * a(y,z,D)') * (D' * (R(D,y,z) * (D' * R(D,y,z)))) = x * (D' * R(D,y,z)).
(a(x,D,y) * D) * a(x,D,y) = a(x,D,y) * R(D,y',x').
D * R(D,x,y)' = a(x,D,y).
a(x,D,y) * R(D,x,y)' = D * (R(D,x,y)' * R(D,x,y)').
D * (R(D,x,y)' * R(D,x,y)') = a(x,D,y) * R(D,x,y)'.
D * (R(D,x,y)' * a(x,D,y)) = R(D,x,y)' * (D * (R(D,x,y)' * D)).
R(D,x,y)' * (D * (R(D,x,y)' * D)) = D * (R(D,x,y)' * a(x,D,y)).
a(x,D,y) = a(x,y,D * D).
a(x,y,D * D) = a(x,D,y).
a((D * D)' * x,D,y) = a((D * D)',x,y)'.
a((D * D)',x,y)' = a(y,(D * D)' * x,D).
a(x,(D * D)' * y,D) = a((D * D)',y,x)'.
a((D * D)',x,y)' = a(y,D,x' * (D * D)).
a(x,D,y' * (D * D)) = a((D * D)',y,x)'.
a(x,D,D * (y' * D)) = a((D * D)',y,x)'.
a(x,D,D * (D * y')) = a((D * D)',y,x)'.
a((D * D)',x,y)' = a(y,D,D * x').
a((D * D)',x,y)' = a(y,x,D).
a(x,D,y) = a((D * D)',x,y)'.
a((D * D)',x,y)' = a(x,D,y).
a(x,D,y)' = a((D * D)',x,y).
a((D * D)',x,y) = a(x,D,y)'.
a((D * D)',x,y) = a(x,y,D).
(a(x,y,D) * D)' = a(D * D,x,y) * D'.
a(D * D,x,y) * D' = (a(x,y,D) * D)'.
a(D * D,x,y) * D' = (a(y,D,x) * D)'.
a(D * D,x,y) * D' = (D * a(y,D,x))'.
a(D * D,x,y) * D' = R(D,x,y)'.
D * R(D,x,y)' = a(D * D,x,y).
a(D * D,x,y) = D * R(D,x,y)'.
a(D * D,x,y) = a(x,D,y).
a(D * D,x,y') = a(x,y,D).
(D * a(x,D,y)) * a(x,D,y) = a(x,D,y) * R(D,y',x').
R(D,x,y) * a(y,D,x) = a(y,D,x) * R(D,x',y').
a(x,D,y) * R(D,y',x') = R(D,y,x) * a(x,D,y).
a(x,D,y) * R(D,y',x') = R(D,y,x) * a(y,x,D).
a(x,y,D) * R(D,x',y') = R(D,x,y) * a(x,y,D).
a(x,y,D) * R(D,y,x') = R(D,x,y) * a(x,y,D).
a(x,y,D) * R(D,x,y) = R(D,x,y) * a(x,y,D).
D' * (R(D,x,y) * R(D,x,y)) = R(D,x,y) * a(x,y,D).
(R(D,x,y) * a(x,y,D))' = D * (R(D,x,y)' * R(D,x,y)').
D * (R(D,x,y)' * R(D,x,y)') = (R(D,x,y) * a(x,y,D))'.
D * (R(D,x,y) * R(D,x,y))' = (R(D,x,y) * a(x,y,D))'.
(x * y) * ((z * (z * x)) * y)' = (R(z,x,y) * R(z,x,y))'.
(R(x,y,z) * R(x,y,z))' = R(x * x,y,z)'.
D * R(D * D,x,y)' = (R(D,x,y) * a(x,y,D))'.
(R(D,x,y) * a(x,y,D))' = D * R(D * D,x,y)'.
D * (R(D,x,y') * R(D,x,y'))' = R(D,x,y')' * a(D,y,x').
D * R(D * D,x,y')' = R(D,x,y')' * a(D,y,x').
R(D,x,y')' * a(D,y,x') = D * R(D * D,x,y')'.
R(D,x,y')' * a(y,D,x) = D * R(D * D,x,y')'.
(a(x,y,D) * R(D,y,x'))' = D * R(D * D,y,x')'.
(R(D,x,y) * a(x,y,D))' = D * R(D * D,y,x')'.
D * R(D * D,x,y')' = D * R(D * D,y,x)'.
D * (D * R(D * D,x,y)') = a(D * D,x,y').
D' * (D' * (R(D,x,y) * R(D,x,y))) = (a(x,D,y) * D)' * R(D,x,y).
R(D,x,y)' * (D * (R(D,x,y)' * D)) = D * (a(x,y,D) * R(D,x,y))'.
D' * (D' * (R(D,x,y) * R(D,x,y))) = (D * a(x,D,y))' * R(D,x,y).
R(D,x,y)' * (D * (R(D,x,y)' * D)) = D * (R(D,x,y) * a(x,y,D))'.
D' * (D' * (R(D,x,y) * R(D,x,y))) = R(D,y,x)' * R(D,x,y).
D' * (R(D,x,y) * a(x,y,D)) = R(D,y,x)' * R(D,x,y).
R(D,x,y)' * (D * (R(D,x,y)' * D)) = D * (D * R(D * D,x,y)').
R(D,x,y)' * (D * (R(D,x,y)' * D)) = a(D * D,x,y').
R(D,x,y)' * (D * (D * R(D,x,y)')) = a(D * D,x,y').
R(D,x,y)' * (D * a(x,D,y)) = a(D * D,x,y').
R(D,x,y)' * R(D,y,x) = a(D * D,x,y').
(x * a(y,D,z)) * (D' * (R(D,y,z) * (D' * R(D,y,z)))) = x * (D' * R(D,y,z)).
(x * a(y,D,z)) * (D' * (R(D,y,z) * a(y,z,D))) = x * (D' * R(D,y,z)).
(x * a(y,D,z)) * (R(D,z,y)' * R(D,y,z)) = x * (D' * R(D,y,z)).
(x * a(y,D,z)) * (R(D,z,y)' * R(D,y,z)) = x * a(y,z,D).
(x * a(y,D,z)) * a(D * D,z,y') = x * a(y,z,D).
(x * a(y,D,z)) * a(z,y,D) = x * a(y,z,D).
(x * a(y,D,z)) * a(y,D,z) = x * a(y,z,D).
x * a(y,z,D) = x * (a(y,D,z) * a(y,D,z)).
x * (a(y,D,z) * a(y,D,z)) = x * a(y,z,D).
a(D,x,y) * (a(D,x,y) * a(D,x,y)) = 1.
x * x' = 1.
a(D,c13,c14) * (a(D,c13,c14) * a(D,c13,c14)) != 1.
((x * (y * y)) * z) * y = (x * y) * (y * (z * y)).
x * (y * z') = z' * (((z * x) * y) * z').
x' * (((x * y) * z) * x') = y * (z * x').
(((x * y) * z) * u) * a(x,y,z) = (x * (y * z)) * (a(x,y,z) * (u * a(x,y,z))).
(x * (y * z)) * (a(x,y,z) * (u * a(x,y,z))) = (((x * y) * z) * u) * a(x,y,z).
((x' * y') * z') * ((z * (y * x)) * u) = u.
x * (y * (z * x')) = ((x * y) * z) * x'.
((x * y) * z) * x' = x * (y * (z * x')).
((x' * y') * z') * ((z * y) * x) = a(z,y,x).
((x' * y') * (z' * u')) * (((u * z) * y) * x) = a(u * z,y,x).
a(x,y,z * x') = a(x,y,z).
(x * (y * (z * x'))) * a(x,y,z) = (x * y) * (z * x').
(((x * y) * z) * x') * a(x,y,z) = (x * y) * (z * x').
a(D,x,y) * a(x,y,D)' = 1.
a(D,x,y) * (z * (a(x,y,D) * z)') = 1.
a(D,x,y) * (D * (a(D * D,x,y) * D')) = 1.
a(x * x,y,z) * x' = ((z' * y') * x') * (x' * ((((x * x) * y) * z) * x')).
((x' * y') * z') * (z' * ((((z * z) * y) * x) * z')) = a(z * z,y,x) * z'.
((x' * y') * z') * ((((z * y) * x) * u) * a(z,y,x)) = a(z,y,x) * (u * a(z,y,x)).
((x' * y') * z') * (z' * (((z * (z * y)) * x) * z')) = a(z * z,y,x) * z'.
((x' * y') * z') * ((z * y) * (x * z')) = a(z * z,y,x) * z'.
((x' * y') * z') * ((z * y) * (x * z')) = a(z,y,x) * (z' * a(z,y,x)).
a(x,y,z) * (x' * a(x,y,z)) = a(x * x,y,z) * x'.
a(D,x,y) * (D * (a(D,x,y) * (D' * a(D,x,y)))) = 1.
a(D,x,y) * (D * (a(D,x,y) * (a(D,x,y) * D'))) = 1.
a(x,y,D) * (a(x,y,D) * a(x,y,D)) = 1.
a(c15,c16,D) * (a(c15,c16,D) * a(c15,c16,D)) != 1.
a(D,x,y) * (D * (a(D,x,y) * (D' * a(x,y,D)))) = 1.
a(D,x,y) * (D * (a(x,y,D) * (D' * a(x,y,D)))) = 1.
a(x,y,D) * (D * (a(x,y,D) * (D' * a(x,y,D)))) = 1.
a(x,y,D) * (D * (a(x,y,D) * (a(x,y,D) * D'))) = 1.
R(x * y,z,D) = R(x,z,D) * R(y,z,D).
R(c28 * c29,c30,D) != R(c28,c30,D) * R(c29,c30,D).
R(c28,c30,D) * R(c29,c30,D) != R(c28 * c29,c30,D).
((x * D) * y) * x = D * (x * (y * x)).
x * (y * D) = D * (((x * D') * y) * D).
D * (((x * D') * y) * D) = x * (y * D).
((x * D) * y)' * x = D * (x * (((x * D) * (y * (x * D)))' * x)).
D * (x * (((x * D) * (y * (x * D)))' * x)) = ((x * D) * y)' * x.
(x * (y * z)) * y' = (x * y) * (z * y').
x * (y * (x * z))' = ((y * x) * (z * x'))'.
((x * y) * (z * y'))' = y * (x * (y * z))'.
(D * (((x * D') * y) * D)) * y' = D * R(x,D',y).
D' * R(x,y,D) = y * ((y * D)' * x).
x * ((x * D)' * y) = D' * R(y,x,D).
(((x * D) * y) * (D * y'))' = y * (D * (D * (x * y)))'.
(x * (y * ((z * x) * y))) * u = (x * y) * (z * ((x * y) * u)).
(x * (y' * z')) * (z * (y * u)) = z' * (y' * ((y * (z * x)) * u)).
(x * (y * D)) * y' = D * R(x,D',y).
D * R(x,D',y) = (x * y) * (D * y').
(x * y) * (D * y') = D * R(x,D',y).
(x * y) * (D * y') = D * R(x,y,D).
D' * R(x * D,y,D) = R(x,y,D).
(x * y) * (D * y') = R(x * D,y,D).
D' * R(D * x,y,D) = R(x,y,D).
D' * R(x,y,D) = R(x * D',y,D).
R(x * D',y,D) = D' * R(x,y,D).
x * ((x * D)' * y) = R(y * D',x,D).
R((x * D) * D,y,D)' = y * (D * (D * (x * y)))'.
x * (D * (D * (y * x)))' = R((y * D) * D,x,D)'.
x * (D * (D * (y * x)))' = R(y * (D * D),x,D)'.
(x * (D * (D * (y * x)))) * z = (x * D) * (y * ((x * D) * z)).
D * (x * ((x * (D * ((y * x) * D)))' * x)) = ((x * D) * y)' * x.
D * (x * ((x * (D * (D * (y * x))))' * x)) = ((x * D) * y)' * x.
D * (x * (D * (D * (y * x)))') = ((x * D) * y)' * x.
D * R(x * (D * D),y,D)' = ((y * D) * x)' * y.
((x * D) * y)' * x = D * R(y * (D * D),x,D)'.
R(D * (x * (D * D))',y,D) = ((y * D) * x)' * y.
R((x * D)',y,D) = ((y * D) * x)' * y.
((x * D) * y)' * x = R((y * D)',x,D).
R(x * D,y,D)' = ((y * D) * x)' * y.
((x * D) * y)' * x = R(y * D,x,D)'.
(x * (y * z)') * (y * (z * u)) = y' * (z' * ((z * (y * x)) * u)).
((((x * (y * z)) * u)' * x) * y)' = (z * (y * x)') * (y * (x * u)).
((((x * D) * (y * ((x * D) * z)))' * x) * D)' = ((D * (y * x)) * (D * x)') * (D * (x * z)).
(R((x * ((y * D) * z)) * D,y,D)' * D)' = ((D * (x * y)) * (D * y)') * (D * (y * z)).
((D * (x * y)) * (D * y)') * (D * (y * z)) = (R((x * ((y * D) * z)) * D,y,D)' * D)'.
((D * (x * y)) * (D * y)') * (D * (y * z)) = (R(D * (x * ((y * D) * z)),y,D)' * D)'.
((D * (x * y)) * (D * y)') * (D * (y * z)) = D' * R(D * (x * ((y * D) * z)),y,D).
R(x,y,D) * (D * (y * z)) = D' * R(D * (x * ((y * D) * z)),y,D).
D' * R(D * (x * ((y * D) * z)),y,D) = R(x,y,D) * (D * (y * z)).
R(x,y,D) * (D * (y * z)) = R(x * ((y * D) * z),y,D).
R(x * ((y * D) * z),y,D) = R(x,y,D) * (D * (y * z)).
R(x * y,z,D) = R(x,z,D) * (D * (z * ((z * D)' * y))).
R(x,y,D) * (D * (y * ((y * D)' * z))) = R(x * z,y,D).
R(x,y,D) * (D * R(z * D',y,D)) = R(x * z,y,D).
R(x,y,D) * R((z * D') * D,y,D) = R(x * z,y,D).
R(x,y,D) * R(z,y,D) = R(x * z,y,D).
R(x * y,D,z) = R(x,D,z) * R(y,D,z).
R(c25 * c26,D,c27) != R(c25,D,c27) * R(c26,D,c27).
R(c25,D,c27) * R(c26,D,c27) != R(c25 * c26,D,c27).
R(x,D,y) * R(z,y',D) = R(x * z,y',D).
R(x,D,y) * R(z,y',D) = R(x * z,D,y).
R(x,D,y) * R(z,D,y) = R(x * z,D,y).

end_of_list.
