% *********************************************************
% AIM:  3 instances of aa1 => aa2
% *********************************************************

clear(back_demod).
set(restrict_denials).

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

set(para_from_small).

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) # label("AIM-TT condition").
   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).

   % extra assumptions for this special case (3 instances of aa1)

   a(a(x,1 / T(y,z * w),u),(((a(x,1 / T(y,z * w),u) \ ((x * ((1 / T(y,z * w)) * u)) \ (x * u))) * z) * w) / (z * w),z * w) = 1 # label("aa1_1").

   a(a(x,1 / T(y,z * w),u),a(x,1 / T(y,z * w),u) \ ((x * ((1 / T(y,z * w)) * u)) \ (x * u)),z) = 1 # label("aa1_2").

   a(a(x,1 / T(y,z * w),u),(a(x,1 / T(y,z * w),u) \ ((x * ((1 / T(y,z * w)) * u)) \ (x * u))) * z,w) = 1 # label("aa1_3").

end_of_list.

formulas(goals).

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

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

a(x,(y * (z * u)) \ ((y * z) * u),w) = 1.
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 \ R(x,y,z) = R(x,y,z) / x.
R(x,y,z) / x = x \ R(x,y,z).
T(x,x \ R(x,y,z)) = x.
T(x,x \ R(x,y,z)) = 1 \ x.
T(x,x \ R(x,y,z)) = 1 \ (x * 1).
T(x,x \ R(x,y,z)) = L((x \ 1) \ 1,x \ 1,x).
L((x \ 1) \ 1,x \ 1,x) = T(x,x \ R(x,y,z)).
L(x,y \ 1,R(y,z,u)) = L(x,y \ 1,y).
R(x,y,z) \ (R(x,y,z) * L(u,x \ 1,x)) = L(u,x \ 1,R(x,y,z)).
R(x,y,z) \ (x * (R(x,y,z) * ((x \ 1) * u))) = L(u,x \ 1,R(x,y,z)).
(x \ R(x,y,z)) \ u = R(x,y,z) \ (x * u).
L(x,y \ R(y,z,u),w) = x.
a(x,y \ R(y,z,u),w) = 1.
a(x,R(y,z,u) * (y \ 1),w) = 1.
(x * y) * (R(y,z,u) / y) = x * R(y,z,u).
a(x,(y \ 1) * R(T(y,y \ 1),z,u),w) = 1.
(x * R(y,z,u)) / y = x * (R(y,z,u) / y).
L(x,R(y,z,u) / y,w) = x.
a(x,(1 / y) * R(y,z,u),w) = 1.
L(x,(1 / y) * R(y,z,u),w) = x.
L(x,(1 / y) * R(T((y / (z * u)) * T(z * u,y),z * u),z,u),w) = x.
L(x,(1 / T(y,z * u)) * R(T(y,z * u),z,u),w) = x.
(x * ((1 / T(y,z * u)) * R(T(y,z * u),z,u))) * w = x * (((1 / T(y,z * u)) * R(T(y,z * u),z,u)) * w).
x * (((1 / T(y,z * u)) * R(T(y,z * u),z,u)) * w) = (x * ((1 / T(y,z * u)) * R(T(y,z * u),z,u))) * w.
x * (((1 / T(y,z * u)) * w) * R((1 * ((1 / T(y,z * u)) * w)) \ (1 * w),z,u)) = (x * ((1 / T(y,z * u)) * R(T(y,z * u),z,u))) * w.
(x * ((1 / T(y,z * u)) * R(T(y,z * u),z,u))) * w = x * (((1 / T(y,z * u)) * w) * R((1 * ((1 / T(y,z * u)) * w)) \ (1 * w),z,u)).
(x * ((1 / T(y,z * u)) * w)) * R((x * ((1 / T(y,z * u)) * w)) \ (x * w),z,u) = (x * ((1 / T(y,z * u)) * R(T(y,z * u),z,u))) * w.
a(x,1 / T(y,z * u),w) * R(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z,u) = R((x * ((1 / T(y,z * u)) * w)) \ (x * w),z,u).
x * (y * z) != (u * y) * z | x = R(u,y,z).
(a(x,1 / T(y,z * u),w) * R(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z,u)) * (z * u) = (((x * ((1 / T(y,z * u)) * w)) \ (x * w)) * z) * u.
(((x * ((1 / T(y,z * u)) * w)) \ (x * w)) * z) * u = (a(x,1 / T(y,z * u),w) * R(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z,u)) * (z * u).
(a(x,1 / T(y,z * u),w) * R(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z,u)) * (z * u) = ((((x * ((1 / T(y,z * u)) * w)) \ (x * w)) * z) * u) * 1.
a(x,1 / T(y,z * u),w) * (((a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w))) * z) * u) = (((x * ((1 / T(y,z * u)) * w)) \ (x * w)) * z) * u.
(((x * ((1 / T(y,z * u)) * w)) \ (x * w)) * z) * u = a(x,1 / T(y,z * u),w) * (((a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w))) * z) * u).
(a(x,1 / T(y,z * u),w) * R(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z,u)) * (z * u) = (a(x,1 / T(y,z * u),w) * (((a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w))) * z) * u)) * 1.
(a(x,1 / T(y,z * u),w) * (((a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w))) * z) * u)) * 1 = (a(x,1 / T(y,z * u),w) * R(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z,u)) * (z * u).
(((x * ((1 / T(y,z * u)) * w)) \ (x * w)) * L(z,a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),a(x,1 / T(y,z * u),w))) * u = a(x,1 / T(y,z * u),w) * (((a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w))) * z) * u).
(x * ((1 / y) * z)) * (a(x,1 / y,z) * R(a(x,1 / y,z) \ ((x * ((1 / y) * z)) \ (x * z)),u,w)) = (x * ((1 / y) * R(y,u,w))) * z.
(x * ((1 / y) * R(y,z,u))) * w = (x * ((1 / y) * w)) * (a(x,1 / y,w) * R(a(x,1 / y,w) \ ((x * ((1 / y) * w)) \ (x * w)),z,u)).
((x * ((1 / y) * z)) * a(x,1 / y,z)) * L(R(a(x,1 / y,z) \ ((x * ((1 / y) * z)) \ (x * z)),u,w),a(x,1 / y,z),x * ((1 / y) * z)) = (x * ((1 / y) * R(y,u,w))) * z.
(a(x,1 / T(y,z * u),w) * (R(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z,u) * (z * u))) * 1 = (a(x,1 / T(y,z * u),w) * R(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z,u)) * (z * u).
((x * (1 / y)) * z) * L(R(a(x,1 / y,z) \ ((x * ((1 / y) * z)) \ (x * z)),u,w),a(x,1 / y,z),x * ((1 / y) * z)) = (x * ((1 / y) * R(y,u,w))) * z.
(a(x,1 / T(y,z * u),w) * ((a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w))) * z)) * u = a(x,1 / T(y,z * u),w) * (((a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w))) * z) * u).
((x * (1 / y)) * z) * R(((x * ((1 / y) * z)) * a(x,1 / y,z)) \ (x * z),u,w) = (x * ((1 / y) * R(y,u,w))) * z.
((x * (1 / y)) * z) * R(((x * (1 / y)) * z) \ (x * z),u,w) = (x * ((1 / y) * R(y,u,w))) * z.
(x * (1 / y)) * (z * R(z \ ((x * (1 / y)) \ (x * z)),u,w)) = (x * ((1 / y) * R(y,u,w))) * z.
(x * y) * (z * R(z \ ((x * y) \ (x * z)),u,w)) = (x * (y * R(y \ 1,u,w))) * z.
(x * y) * (z * R(z \ L(y \ z,y,x),u,w)) = (x * (y * R(y \ 1,u,w))) * z.
(x * (y * R(y \ 1,z,u))) * w = (x * y) * (w * R(w \ L(y \ w,y,x),z,u)).
(x * (y * R(y \ (x \ x),z,u))) * w = (x * y) * (w * R(w \ L(y \ w,y,x),z,u)).
((x / y) * z) * R((1 * ((x / y) * z)) \ (x * z),u,w) = ((x / y) * R(y,u,w)) * z.
x * (R(x,y,z) * ((x \ 1) * u)) = R(x,y,z) * L(u,x \ 1,x).
x * (R(x,y,z) * (x \ u)) = R(x,y,z) * u.
x * R(x \ (y * x),z,u) = y * (R(y,z,u) * (y \ x)).
((x * y) * R((x * y) \ x,z,u)) * w = (x * y) * (w * R(w \ L(y \ w,y,x),z,u)).
(x * y) * (z * R(z \ L(y \ z,y,x),u,w)) = ((x * y) * R((x * y) \ x,u,w)) * z.
(1 / x) * R(x,y,z) = R(x,y,z) / x.
R(x,y,z) / x = (1 / x) * R(x,y,z).
(x * R(y,z,u)) / y = (x / y) * R(y,z,u).
((x * y) * R(y,z,u)) / y = x * R(y,z,u).
(x * R(y,z,u)) * y = (x * y) * R(y,z,u).
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 * R(x \ (x * y),z,u)) * y = (x * y) * R(y,z,u).
(x * y) * R(y,z,u) = (x * R(x \ (x * y),z,u)) * y.
(x * y) * R((1 * (x * y)) \ (z * y),u,w) = (x * R(x \ z,u,w)) * y.
(x * y) * R((x * y) \ (x * z),u,w) = x * (y * R((1 * y) \ (1 * z),u,w)).
(x * y) * R((x * y) \ (z * y),u,w) = (x * R(x \ z,u,w)) * y.
L((x \ 1) \ 1,x \ 1,R(x,y,z)) = T(x,x \ R(x,y,z)).
T(x,x \ R(x,y,z)) = L((x \ 1) \ 1,x \ 1,R(x,y,z)).
(x * y) * R((x * y) \ (x * z),u,w) = x * (y * R(y \ z,u,w)).
(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((x \ 1) \ 1,x \ 1,R(x,y,z)) = (x \ R(x,y,z)) \ R(x,y,z).
(x \ R(x,y,z)) \ (R(x,y,z) * ((x \ 1) * u)) = L(u,x \ 1,R(x,y,z)).
L(x,y \ 1,R(y,z,u)) = (y \ R(y,z,u)) \ (R(y,z,u) * ((y \ 1) * x)).
R(x,y,z) * (x \ 1) = x \ R(x,y,z).
x \ R(x,y,z) = R(x,y,z) * (x \ 1).
x \ R(1 \ x,y,z) = R(x,y,z) * (x \ 1).
x \ R(1 \ (x * 1),y,z) = R(x,y,z) * (x \ 1).
T((x / y) * T(y,x),y) = x.
T((x / y) * T(y,x),(x / y) \ x) = x.
T(x * T(x \ y,y),x \ y) = y.
T(x * T(x \ y,y),x \ y) = x * (x \ y).
(x \ y) \ ((x * T(x \ y,y)) * (x \ y)) = x * (x \ y).
x * L(R((y \ x) \ x,z,u),y \ x,y) = y * (R(y,z,u) * (y \ x)).
x \ L(R((x \ 1) \ 1,y,z),x \ 1,x) = R(x,y,z) * (x \ 1).
(x \ y) \ ((T(y / x,y) * x) * (x \ y)) = x * (x \ y).
R(T(x / y,x),y,y \ x) = y \ x.
R(T(x / y,x),y,T(x / y,y)) = y \ x.
(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(T(x / y,(x / y) * y),y,T(x / y,y)) = y \ x.
R(T(x,x * y),y,T(x,y)) = y \ (x * y).
T(R(x,y,T(x,y)),x * y) = y \ (x * y).
T(R(x,y,y \ (x * y)),x * y) = y \ (x * y).
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).
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 * R(x \ (y * x),z,u) = R(y,z,u) * x.
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).
(x * y) / L(z,y / z,x) = x * (y / z).
R(R(x,y,z),u,w) * (y * z) = (R(x,u,w) * y) * z.
R(x,y,y \ z) * z = (x * y) * (y \ z).
(1 * x) \ (1 * y) = x \ 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.
(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).
T(x / y,z) * y = y * T(y \ x,z).
x * T(x \ y,z) = T(y / x,z) * x.
L(x,y,1) = x.
x \ (x * y) = L(y,x,1).
x / T(y,y \ x) = y \ x.
T(T(x / y,z),y) = T(y \ x,z).
T(x \ y,z) = T(T(y / x,z),x).
x * R(T(y,x),z,u) = R(y,z,u) * x.
x * y != z * x | T(z,x) = y.
x * y != y * z | T(x,y) = z.
R(x,y,z) \ ((x * y) * z) = y * z.
(x * y) / T(x,y) = y.
(x * (y * z)) / L(z,y,x) = x * y.
L(x,(a(y,1 / T(z,u * x),w) \ ((y * ((1 / T(z,u * x)) * w)) \ (y * w))) * u,a(y,1 / T(z,u * x),w)) = x.
L(x,a(y,1 / T(z,x * u),w) \ ((y * ((1 / T(z,x * u)) * w)) \ (y * w)),a(y,1 / T(z,x * u),w)) = x.
a(a(x,1 / T(y,z * u),w),R(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z,u),z * u) = 1.
T(x / y,y) = y \ x.
T(x,x \ y) = (x \ y) \ y.
x * T(y,x) = y * x.
R(x / y,y,z) = (x * z) / (y * z).
R(x,y,z) * (y * z) = (x * y) * z.
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 \ (1 * (x * y)) = L(y,x,1).
L(x,y,1) = y \ (1 * (y * x)).
(x * (y * z)) * a(x,y,z) = (x * y) * z.
x * y != z | z / y = x.
x != y * z | x / z = y.
x * 1 != y | x = y.
x * y != z | x \ z = y.
x != y * z | y \ x = z.
(x / y) \ x = y.
x / (y \ x) = y.
x \ x = 1.
1 \ x = x.
a(c1,a(c2,c3,c4),c5) != 1.
a(a(x,1 / T(y,z * u),w),(a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w))) * z,u) = 1.
a(a(x,1 / T(y,z * u),w),a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w)),z) = 1.
a(a(x,1 / T(y,z * u),w),(((a(x,1 / T(y,z * u),w) \ ((x * ((1 / T(y,z * u)) * w)) \ (x * w))) * z) * u) / (z * u),z * u) = 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).
T(T(x,y),z) = T(T(x,z),y).
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).
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) * 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.
