if(Prover9).
  assign(max_megs,500).

  assign(order, kbo).
  function_order([1,a,K,L,R,T,*,\,/]).

  clear(auto_inference).
  set(paramodulation).
  set(pos_ur_resolution).
  set(para_units_only).

end_if.

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
% (comment out if they clog the search)
x * y = u & x * z = u -> y = z.
y * x = u & z * x = u -> y = z.

% associator
(x * (y * z)) \ ((x * y) * z) = a(x,y,z).
% commutator
(x * y) \ (y * x) = K(y,x).

% inner mappings
% L(u,x,y) = u L(x) L(y) L(yx)^{-1}
(y * x) \ (y * (x * u)) = L(u,x,y).
% R(u,x,y) = u R(x) R(y) R(xy)^{-1}
((u * x) * y) / (x * y) = R(u,x,y).
% T(u,x) = u R(x) L(x)^{-1}
x \ (u * x) = T(u,x).

% obvious compatibility
% (comment out if they clog the search)
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(goals).

% nilpotent of class 3

% a proof of just one of these would be a good start

K(K(K(x,y),z),u) = 1           # label("KKK").
K(K(a(x,y,z),u),w) = 1         # label("KKa").
K(a(K(x,y),z,u),w) = 1         # label("KaK").
a(K(K(x,y),z),u,w) = 1         # label("aKK").
a(K(a(x,y,z),u),w,v5) = 1      # label("aKa").
K(a(a(x,y,z),u,w),v5) = 1      # label("Kaa").
a(a(K(x,y),z,u),w,v5) = 1      # label("aaK").
a(a(a(x,y,z),u,w),v5,v6) = 1   # label("aaa").

% all known examples which achieve class 3 satisfy
% these stronger conditions

a(K(x,y),z,u) = 1              # label("aK"). % subsumes aKK, aKa, KaK, aaK
K(a(x,y,z),u) = 1              # label("Ka"). % subsumes Kaa, KaK, KKa, aKa
a(a(x,y,z),u,w) = 1            # label("aa"). % subsumes aaa, aaK, Kaa, aaa

end_of_list.

%BEGIN

% Special cases where the result is known:

% Case 1: Moufang (equiv identities)
((x * y) * x) * z = x * (y * (x * z)).
((x * y) * z) * y = x * (y * (z * y)).
(x * y) * (z * x) = x * ((y * z) * x).

% Case 2: A-loop (better results hold in this case)
L(x,y,z) * L(u,y,z) = L(x * u,y,z).
R(x,y,z) * R(u,y,z) = R(x * u,y,z).
T(x,y) * T(z,y) = T(x * z,y).

% Case 3: Left conjugacy closed (better results hold in this case)
((x * y) / x) * (x * z) = x * (y * z).

% Case 4: Right conjugacy closed (better results hold in this case)
(x * y) * (y \ (z * y)) = (x * z) * y.

END%