if(Prover9).
assign(order, kbo).
end_if.

formulas(assumptions).

% IP loop axioms
1 * x = x. x * 1 = x.
x' * (x * y) = y. x'' = x.
(x * y) * y' = x. 1' = 1.

% alt, flex
x * (x * y) = (x * x) * y.
(x * y) * y = x * (y * y).
x * (y * x) = (x * y) * x.

% ARIF
x * ((y * (x * y)) * z) = (x * (y * x)) * (y * z)		# label(ARIF1).
(z * ((y * x) * y)) * x = (z * y) * ((x * y) * x)		# label(ARIF2).

% Moufang element of type M_0
(C * (x * y)) * C = (C * x) * (y * C).
((C * x) * C) * y = C * (x * (C * y)).
((y * C) * x) * C = y * (C * (x * C)).

% Moufang element of type M_1
((x * C) * x) * y = x * (C * (x * y)).
((y * x) * C) * x = y * (x * (C * x)).

% M_0 and M_1 are equivalent in ARIF loops

end_of_list.

formulas(goals).

% Any one of these goals will suffice

% Moufang element of type M_2
(x * C) * (y * x) = x * ((C * y) * x).
((x * y) * x) * C = x * (y * (x * C)).

% Moufang element of type M_3
(x * y) * (C * x) = x * ((y * C) * x).
((C * x) * y) * x = C * (x * (y * x)).

end_of_list.

%BEGIN
% The result is known in two important special cases

% Case 1: C loops
x * (y * (y * z)) = ((x * y) * y) * z					# label(C).

% Case 2: RIF loops
(x * y) * (z * (x * y)) = ((x * (y * z)) * x) * y		# label(RIF1).
((y * x) * z) * (y * x) = y * (x * ((z * y) * x))		# label(RIF2).

END%