% ****************
% AIM:  aa1 => aa2
% ****************

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

set(para_from_small).

clear(back_demod).
set(restrict_denials).

assign(max_weight,5).

formulas(assumptions).

   % loop axioms
   1 * x = x.
   x * 1 = x.
   x \ (x * y) = y.
   x * (x \ y) = y.
   (x * y) / y = x.
   (x / y) * y = x.

   % cancellation laws
   x * y = u & x * z = u -> y = z.
   y * x = u & z * x = u -> y = z.

      % other form
      x * y = x * z -> y = z.
      y * x = z * x -> y = z.

   % associator (right associated * a = left associated)
   (x * (y * z)) \ ((x * y) * z) = a(x,y,z) # label("associator").

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

   % inner mappings
   (y * x) \ (y * (x * u)) = L(u,x,y).
   ((u * x) * y) / (x * y) = R(u,x,y).
   x \ (u * x) = T(u,x).

   % obvious compatibility
   a(x,y,z) = 1 -> L(z,y,x) = z.
   L(x,y,z) = x -> a(z,y,x) = 1.
   T(x,y) = x -> T(y,x) = y.
   T(x,y) = x -> K(x,y) = 1.
   K(x,y) = 1 -> T(x,y) = x.

   % abelian inner mapping group
   T(T(u,x),y) = T(T(u,y),x).
   T(L(u,x,y),z) = L(T(u,z),x,y).
   T(R(u,x,y),z) = R(T(u,z),x,y).
   L(R(u,x,y),z,w) = R(L(u,z,w),x,y).
   L(L(u,x,y),z,w) = L(L(u,z,w),x,y).
   R(R(u,x,y),z,w) = R(R(u,z,w),x,y).

end_of_list.

formulas(assumptions).

   a(a(x,y,z),u,w) = 1            # label("aa1").

end_of_list.

formulas(goals).

   a(x,a(y,z,u),w) = 1            # label("aa2").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

a(x,y \ R(y,z,u),w) = 1.
L(x,y \ R(y,z,u),w) = x.
(x * (y \ R(y,z,u))) * w = x * ((y \ R(y,z,u)) * w).
(x * ((1 / y) * R(y,z,u))) * w = x * ((y \ R(y,z,u)) * w).
((x * (1 / y)) * L(R(y,z,u),1 / y,x)) * w = x * ((y \ R(y,z,u)) * w).
((x * (1 / y)) * R(L(y,1 / y,x),z,u)) * w = x * ((y \ R(y,z,u)) * w).
((x * (1 / y)) * R(L(y,1 / y,x),z,u)) * w = x * (((1 / y) * R(y,z,u)) * w).
((x * (1 / y)) * R(L(y,1 / y,x),z,u)) * w = x * (((1 / y) * R((1 / y) \ 1,z,u)) * w).
((x * (1 / y)) * R(L(y,1 / y,x),z,u)) * w = x * ((1 / y) * (w * R(w \ ((1 / y) \ w),z,u))).
x * ((1 / y) * (z * R(z \ ((1 / y) \ z),u,w))) = ((x * (1 / y)) * R(L(y,1 / y,x),u,w)) * z.
(x * y) * (z * R(z \ L(y \ u,y,x),w,v5)) = x * (y * (z * R(z \ (y \ u),w,v5))).
(x * y) * (z * R(z \ L(y \ u,y,x),w,v5)) = x * (y * (z * R(z \ (y \ (x \ (x * u))),w,v5))).
(x * y) * (z * R(z \ ((x * y) \ u),w,v5)) = x * (y * (z * R(z \ (y \ (x \ u)),w,v5))).
(x * y) * (z * R(z \ ((x * y) \ u),w,v5)) = x * ((y * z) * R((y * z) \ (x \ u),w,v5)).
(x * (y * z)) * R((x * (y * z)) \ u,w,v5) = (x * y) * (z * R(z \ ((x * y) \ u),w,v5)).
(x * (y * z)) * R(a(x,y,z) * (a(x,y,z) \ ((x * (y * z)) \ u)),w,v5) = (x * y) * (z * R(z \ ((x * y) \ u),w,v5)).
(x * (y * z)) * (a(x,y,z) * R(a(x,y,z) \ ((x * (y * z)) \ u),w,v5)) = (x * y) * (z * R(z \ ((x * y) \ u),w,v5)).
(x * (y * z)) * (a(x,y,z) * R(a(x,y,z) \ ((x * (y * z)) \ u),w,v5)) = ((x * y) * z) * R(((x * y) * z) \ u,w,v5).
a(x,y,z) = T(x,y * z) \ R(T(x,y * z),y,z).
T(x,y * z) \ R(T(x,y * z),y,z) = (x * (y * z)) \ ((x * y) * z).
T(x,y) \ R(T(x,y),z,u) = (x * y) \ (R(x,z,u) * y).
(x * y) \ (R(x,z,u) * y) = T(x,y) \ R(T(x,y),z,u).
(x * y) \ (y * R(T(x,y),z,u)) = T(x,y) \ R(T(x,y),z,u).
(x * y) \ (x * R(y,z,u)) = y \ R(y,z,u).
(x * y) * (y \ R(y,z,u)) = x * R(y,z,u).
(x * y) * (R(y,z,u) * (y \ 1)) = x * R(y,z,u).
(x * y) * ((y \ 1) * R(T(y,y \ 1),z,u)) = x * R(y,z,u).
x * R(y,z,u) = (x * y) * ((y \ 1) * R(T(y,y \ 1),z,u)).
R(x,y,y \ 1) * L(R(T(y,y \ 1),z,u),y \ 1,x * y) = x * R(y,z,u).
R(x,y,y \ 1) * R(L(T(y,y \ 1),y \ 1,x * y),z,u) = x * R(y,z,u).
R(x,y,y \ 1) * R(L(T(y,y \ 1),y \ 1,x * y),z,u) = x * R(a(x,y,y \ 1) * (a(x,y,y \ 1) \ y),z,u).
R(x,y,y \ 1) * R(L(T(y,y \ 1),y \ 1,x * y),z,u) = x * (a(x,y,y \ 1) * R(a(x,y,y \ 1) \ y,z,u)).
R(x,y,y \ 1) * R(L(T(y,y \ 1),y \ 1,x * y),z,u) = x * (a(x,y,y \ 1) * R((x \ R(x,y,y \ 1)) \ y,z,u)).
(x * (1 / y)) * (z * R(z \ L((1 / y) \ z,1 / y,x),u,w)) = ((x * (1 / y)) * R(L(y,1 / y,x),u,w)) * z.
((x * (1 / y)) * R(L(y,1 / y,x),z,u)) * w = (x * (1 / y)) * (w * R(w \ L((1 / y) \ w,1 / y,x),z,u)).
(1 / x) * R(x,y,z) = x \ R(x,y,z).
R(x,y,z) / x = x \ R(x,y,z).
(x \ R(x,y,z)) * x = R(x,y,z).
R(x,y,z) = (x \ R(x,y,z)) * x.
R(K(x \ 1,x) * (K(x,x \ 1) * x),y,z) = (x \ R(x,y,z)) * x.
K(x \ 1,x) * R(K(x,x \ 1) * x,y,z) = (x \ R(x,y,z)) * x.
K(x \ 1,x) * R(K(x \ 1,x) \ x,y,z) = (x \ R(x,y,z)) * x.
K(x \ 1,x) * R(K(x \ 1,x) \ x,y,z) = (R(x,y,z) * (x \ 1)) * x.
K(x \ 1,x) \ y = K(x,x \ 1) * y.
K(x,x \ 1) * y = K(x \ 1,x) \ y.
K(x \ 1,x) * (K(x,x \ 1) * y) = y.
K(x,x \ 1) * (K(x \ 1,x) * y) = y.
x * y != L(x * z,u,K(w \ 1,w)) | y = z.
K(x \ 1,x) * (K(x,x \ 1) * y) = L(y,K(x,x \ 1),K(x \ 1,x)).
K(x \ 1,x) * (K(x,x \ 1) * y) = L(y,K(x,x \ 1),(x \ 1) * x).
L(x,K(y,y \ 1),(y \ 1) * y) = K(y \ 1,y) * (K(y,y \ 1) * x).
1 \ (K(x \ 1,x) * (K(x,x \ 1) * y)) = L(y,K(x,x \ 1),(x \ 1) * x).
R(K(x \ 1,x) * y,z,u) = K(x \ 1,x) * R(y,z,u).
R(((1 / x) \ (x \ 1)) * y,z,u) = K(x \ 1,x) * R(y,z,u).
R(((1 / x) \ (x \ 1)) * y,z,u) = ((1 / x) \ (x \ 1)) * R(y,z,u).
((x * (1 / y)) * R(L(y,1 / y,x),z,u)) * w = (x * (1 / y)) * (w * R(w \ ((x * (1 / y)) \ (x * w)),z,u)).
(x * (1 / y)) * (z * R(z \ ((x * (1 / y)) \ (x * z)),u,w)) = ((x * (1 / y)) * R(L(y,1 / y,x),u,w)) * z.
x * (y * R(y \ (x \ (z * y)),u,w)) = (x * R(x \ z,u,w)) * y.
(x * R(x \ y,z,u)) * w = x * (w * R(w \ (x \ (y * w)),z,u)).
(x * y) * R((x * y) \ (z * y),u,w) = (x * R(x \ z,u,w)) * y.
R(x,y,y \ 1) * R(L(T(y,y \ 1),y \ 1,x * y),z,u) = x * ((x \ R(x,y,y \ 1)) * R((x \ R(x,y,y \ 1)) \ y,z,u)).
x * ((x \ R(x,y,y \ 1)) * R((x \ R(x,y,y \ 1)) \ y,z,u)) = R(x,y,y \ 1) * R(L(T(y,y \ 1),y \ 1,x * y),z,u).
x * (y * R(y \ (x \ y),z,u)) = (x * R(x \ 1,z,u)) * y.
(x * (y * z)) * (a(x,y,z) * R(a(x,y,z) \ ((x * (y * z)) \ u),w,v5)) = ((x * y) * z) * R(((x * (y * z)) * a(x,y,z)) \ u,w,v5).
((x * y) * z) * R(((x * (y * z)) * a(x,y,z)) \ u,w,v5) = (x * (y * z)) * (a(x,y,z) * R(a(x,y,z) \ ((x * (y * z)) \ u),w,v5)).
(x * y) * R((x * y) \ (z * y),u,w) = (R(z / x,u,w) * x) * y.
(R(x / y,z,u) * y) * w = (y * w) * R((y * w) \ (x * w),z,u).
L(T(x,x \ 1),x \ 1,y * x) = R(y,x,x \ 1) \ (y * x).
(1 / x) * R(x,y,z) = R(x,y,z) / x.
(1 / x) * R((1 / x) \ 1,y,z) = R(x,y,z) / x.
R(x,y,z) / x = (1 / x) * R((1 / x) \ 1,y,z).
R(1 / (1 / x),y,z) * (1 / x) = R(x,y,z) / x.
R(1 / (1 / x),y,z) * (1 / x) = R(x / 1,y,z) / x.
R(x / 1,y,z) / x = R(1 / (1 / x),y,z) * (1 / x).
R(a(1 / x,x,x \ 1) * y,z,u) = ((1 / x) \ (x \ 1)) * R(y,z,u).
R(a(x,y,z) * u,w,v5) = a(x,y,z) * R(u,w,v5).
a(x,y,z) * R(u,w,v5) = R(a(x,y,z) * u,w,v5).
a(x,y,z) * (((u * w) * v5) / (w * v5)) = R(a(x,y,z) * u,w,v5).
R(a(x,y,z) * u,w,v5) = a(x,y,z) * (((u * w) * v5) / (w * v5)).
(a(x,y,z) * ((u * w) * v5)) / (w * v5) = R(a(x,y,z) * u,w,v5).
(x * y) * R((x * y) \ y,z,u) = (x * R(x \ 1,z,u)) * y.
R(x,y,z) * (x \ 1) = x \ R(x,y,z).
x \ R(x,y,z) = R(x,y,z) * (x \ 1).
(x \ 1) * R((x \ 1) \ 1,y,z) = x \ R(x,y,z).
(x * y) * R((x * y) \ y,z,u) = (R(1 / x,z,u) * x) * y.
(R(1 / x,y,z) * x) * u = (x * u) * R((x * u) \ u,y,z).
x * ((x \ y) * R((x \ y) \ z,u,w)) = y * R(y \ (x * z),u,w).
x * R(x \ (y * z),u,w) = y * ((y \ x) * R((y \ x) \ z,u,w)).
(x \ 1) * R((x \ 1) \ y,z,u) = x \ R(1 \ (x * y),z,u).
x \ R(1 \ (x * y),z,u) = (x \ 1) * R((x \ 1) \ y,z,u).
x \ (((y \ x) * y) * (K(y,y \ x) * z)) = L(z,K(y,y \ x),(y \ x) * y).
(x * y) * R((x * y) \ z,u,w) = x * (y * R(y \ (x \ z),u,w)).
R((x * y) / (z * y),u,w) * (z * y) = (R(x / z,u,w) * z) * y.
R(R(x,y \ 1,y),z,u) * K(y \ 1,y) = (R(x,z,u) * (y \ 1)) * y.
L(T(x,x \ 1),x \ 1,y * x) = R(y,x,x \ 1) \ ((y * x) * 1).
L(x,y,K(z \ 1,z)) = x.
L(x,y,(1 / z) \ (z \ 1)) = x.
a(1 / x,x,x \ 1) = (1 / x) \ (x \ 1).
(1 / x) \ (x \ 1) = K(x \ 1,x).
(1 / x) * K(x \ 1,x) = x \ 1.
(1 / x) * ((x \ 1) * x) = x \ 1.
(1 / x) * ((x \ 1) * x) = T(1 / x,x).
(1 / x) * ((x \ 1) * x) = T(1 \ (1 / x),x).
T(1 \ (1 / x),x) = (1 / x) * ((x \ 1) * x).
R(x / ((1 / x) * x),y,z) / x = R(1 / (1 / x),y,z) * (1 / x).
R(x / (y * x),z,u) * (y * x) = (R(1 / y,z,u) * y) * x.
x \ R(x,y,y \ 1) = a(x,y,y \ 1).
a(x / y,y,y \ 1) = (x / y) \ (x * (y \ 1)).
(x / y) \ (x * (y \ 1)) = a(x / y,y,y \ 1).
x \ ((x * y) * (y \ 1)) = a(x,y,y \ 1).
K(x \ 1,x) * R(K(x \ 1,x) \ x,y,z) = R(R(x,x \ 1,x),y,z) * K(x \ 1,x).
R(R(x,x \ 1,x),y,z) * K(x \ 1,x) = K(x \ 1,x) * R(K(x \ 1,x) \ x,y,z).
((a(x,y,z) * (u * w)) * v5) / (w * v5) = R(a(x,y,z) * u,w,v5).
R(a(x,y,z) * u,w,v5) = ((a(x,y,z) * (u * w)) * v5) / (w * v5).
(a(x,y,z) * u) / w = a(x,y,z) * (u / w).
L(R((x \ y) \ z,u,w),x \ y,x) = R(y \ (x * z),u,w).
R(x \ (y * z),u,w) = L(R((y \ x) \ z,u,w),y \ x,y).
R(x,1 / y,y) / y = x * (1 / y).
(x * (1 / y)) * y = R(x,1 / y,y).
R(x,1 / y,y) = (x * (1 / y)) * y.
R(x,y,y \ 1) * L(z,y \ 1,x * y) = (x * y) * ((y \ 1) * z).
(x * y) * (y \ 1) = R(x,y,y \ 1).
R(x,y,y \ 1) = (x * y) * (y \ 1).
(x * y) / L(z,y / z,x) = x * (y / z).
L(T(x,y),y,1 / y) = (1 / y) * (x * y).
(1 / x) * (y * x) = L(T(y,x),x,1 / x).
(1 / x) * (x * y) = L(y,x,1 / x).
L(x,y,1 / y) = (1 / y) * (y * x).
x \ L(y,x \ 1,x) = (x \ 1) * y.
x * ((x \ 1) * y) = L(y,x \ 1,x).
L(x,y \ 1,y) = y * ((y \ 1) * x).
(x \ y) * R((x \ y) \ y,z,u) = R(x,z,u) * (x \ y).
R(x / y,z,u) * y = y * R(y \ x,z,u).
x * R(x \ y,z,u) = R(y / x,z,u) * x.
x / K(x \ 1,x) = R(x,x \ 1,x).
R(x,x \ 1,x) = x / K(x \ 1,x).
T(x \ (x / y),z) = L(T(y \ 1,z),y,x / y).
L(T(x \ 1,y),x,z / x) = T(z \ (z / x),y).
L(R(x \ (y \ z),u,w),x,y) = R((y * x) \ z,u,w).
R((x * y) \ z,u,w) = L(R(y \ (x \ z),u,w),y,x).
R(x,x \ 1,y) = y / ((x \ 1) * y).
R(R(1 / x,y,z),x,u) = R(u / (x * u),y,z).
R(x / (y * x),z,u) = R(R(1 / y,z,u),y,x).
R(1 / x,x,y) = y / (x * y).
R(R(x,y,z),u,w) * (y * z) = (R(x,u,w) * y) * z.
L(x,1 / x,y) = (y * (1 / x)) \ y.
L(x \ 1,x,y / x) = y \ (y / x).
L(T(x,x \ y),x \ y,z) = (z * (x \ y)) \ (z * y).
L(x \ (y \ z),x,y) = (y * x) \ z.
L((x \ y) \ z,x \ y,x) = y \ (x * z).
L(x \ 1,x,y) = (y * x) \ y.
(a(x,y,z) * u) * w = a(x,y,z) * (u * w).
(x * y) * z != x * (y * u) | L(u,y,x) = z.
x * (y * z) != (x * y) * u | L(z,y,x) = u.
x * L(y,z \ x,z) = z * ((z \ x) * y).
K(x \ 1,x) = (x \ 1) * x.
(x * y) \ ((y * x) * (K(x,y) * z)) = L(z,K(x,y),y * x).
L(x,K(y,z),z * y) = (y * z) \ ((z * y) * (K(y,z) * x)).
x * R(T(y,x),z,u) = R(y,z,u) * x.
1 \ (x * 1) = x.
x = 1 \ (x * 1).
x * 1 != y | x = y.
L(x,y,a(z,u,w)) = x.
T(x / y,y) = y \ x.
T(x,x \ y) = (x \ y) \ y.
x * T(y,x) = y * x.
((x * (y / z)) * z) / y = R(x,y / z,z).
R(x,y / z,z) = ((x * (y / z)) * z) / y.
R(x / y,y,z) = (x * z) / (y * z).
R(x,y,z) * (y * z) = (x * y) * z.
((x * y) * (y \ z)) / z = R(x,y,y \ z).
R(x,y,y \ z) = ((x * y) * (y \ z)) / z.
L(x,y / x,z) = (z * (y / x)) \ (z * y).
x \ ((x / y) * (y * z)) = L(z,y,x / y).
L(x,y,z / y) = z \ ((z / y) * (y * x)).
L(x \ y,x,z) = (z * x) \ (z * y).
x \ (y * ((y \ x) * z)) = L(z,y \ x,y).
L(x,y \ z,y) = z \ (y * ((y \ z) * x)).
(x * y) * L(z,y,x) = x * (y * z).
x \ ((y \ x) * y) = K(y \ x,y).
K(x \ y,x) = y \ ((x \ y) * x).
(x * y) * K(y,x) = y * x.
(x * y) \ ((x * z) * (z \ y)) = a(x,z,z \ y).
a(x,y,y \ z) = (x * z) \ ((x * y) * (y \ z)).
(x * (y * z)) * a(x,y,z) = (x * y) * z.
x * y != z | z / y = x.
x != y * z | x / z = y.
x * y != z | x \ z = y.
x != y * z | y \ x = z.
(x / y) \ x = y.
x / (y \ x) = y.
x / 1 = x.
1 \ x = x.
a(c1,a(c2,c3,c4),c5) != 1.
a(a(x,y,z),u,w) = 1.
R(R(x,y,z),u,w) = R(R(x,u,w),y,z).
R(L(x,y,z),u,w) = L(R(x,u,w),y,z).
L(R(x,y,z),u,w) = R(L(x,u,w),y,z).
R(T(x,y),z,u) = T(R(x,z,u),y).
T(R(x,y,z),u) = R(T(x,u),y,z).
L(T(x,y),z,u) = T(L(x,z,u),y).
T(L(x,y,z),u) = L(T(x,u),y,z).
L(x,y,z) != x | a(z,y,x) = 1.
a(x,y,z) != 1 | L(z,y,x) = z.
T(x,y) = y \ (x * y).
x \ (y * x) = T(y,x).
R(x,y,z) = ((x * y) * z) / (y * z).
((x * y) * z) / (y * z) = R(x,y,z).
L(x,y,z) = (z * y) \ (z * (y * x)).
(x * y) \ (x * (y * z)) = L(z,y,x).
K(x,y) = (y * x) \ (x * y).
(x * y) \ (y * x) = K(y,x).
a(x,y,z) = (x * (y * z)) \ ((x * y) * z).
(x * (y * z)) \ ((x * y) * z) = a(x,y,z).
x * y != z * y | x = z.
x * y != x * z | y = z.
x * y != z | u * y != z | u = x.
x * y != z | x * u != z | u = y.
(x / y) * y = x.
(x * y) / y = x.
x * (x \ y) = y.
x \ (x * y) = y.
x * 1 = x.
1 * x = x.
a(x,a(y,z,u),w) = 1.

end_of_list.
