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.

% semiuniversal flexibility
(x * (y * z)) * (y * x) = x * (y * (z * (y * x))).
(((x * y) * z) * y) * x = (x * y) * ((z * y) * x).

end_of_list.

formulas(goals).

% Moufang?
x * (y * (x * z)) = ((x * y) * x) * z # answer(M1).
((z * x) * y) * x = z * (x * (y * x)) # answer(M2).
x * ((y * z) * x) = (x * y) * (z * x) # answer(N1).

end_of_list.

%BEGIN
% additional assumptions, possibly useful for sketches
x * (y * (y * z)) = ((x * y) * y) * z					# label(C).
x * ((y * (z * z)) * x) = (x * y) * ((z * z) * x)		# label(SM).
(x * y) * (x * (y * z)) = x * (y * ((x * y) * z))		# label(S1).
((z * y) * x) * (y * x) = ((z * (y * x)) * y) * x		# label(S2).
(x * y) * (z * (x * y)) = ((x * (y * z)) * x) * y		# label(RIF1).
((y * x) * z) * (y * x) = y * (x * ((z * y) * x))		# label(RIF2).
x * ((y * (x * y)) * z) = (x * (y * x)) * (y * z)		# label(ARIF1).
(z * ((y * x) * y)) * x = (z * y) * ((x * y) * x)		# label(ARIF2).
x * ((x' * (y * y)) * (x * z)) = (y * (y * x)) * z		# label(H1).
((z * x) * ((y * y) * x')) * x = z * ((x * y) * y)		# label(H2).
x * ((y * z) * (x * y)) = ((x * y) * (z * x)) * y		# label(TSI1).
((y * x) * (z * y)) * x = y * ((x * z) * (y * x))		# label(TSI2).
(x * y) * (y * ((z * y) * (y * x))) = (((x * y) * (y * z)) * y) * (y * x)	# answer(MSUF).
END%
