if(Prover9).
assign(order, kbo).
assign(eq_defs,fold).
end_if.
formulas(assumptions).
% identity element
0 * x = x.
x * 0 = x.
% quasigroup
x * (x \ y) = y.
x \ (x * y) = y.
(x * y) / y = x.
(x / y) * y = x.
% left Bol (universally
LIP, universally LAP)
(x * (y * x)) * z = x * (y * (x * z)).
% C a Moufang element
C * ((x * y) * C) = (C * x) * (y * C).
% C in commutant
C * x = x * C.
end_of_list.
formulas(goals).
(C * C) * (x * y) = (C * x) * (C * y).
end_of_list.
if(Prover9).
assign(order,
kbo).
assign(eq_defs,fold).
end_if.
formulas(assumptions).
%
identity element
0 * x =
x.
x * 0 =
x.
% quasigroup
x * (x \
y) = y.
x \ (x *
y) = y.
(x * y)
/ y = x.
(x / y)
* y = x.
% left Bol (universally LIP, universally LAP)
(x * (y
* x)) * z = x * (y * (x * z)).
% C a Moufang element
C * ((x
* y) * C) = (C * x) * (y * C).
% assumption
(C * C)
* (x * y) = (C * x) * (C * y).
end_of_list.
formulas(goals).
(x * x) * (C * y) = (x * C) * (x * y).
end_of_list.
if(Prover9).
assign(order,
kbo).
assign(eq_defs,fold).
end_if.
formulas(assumptions).
%
identity element
0 * x =
x.
x * 0 =
x.
% quasigroup
x * (x \
y) = y.
x \ (x *
y) = y.
(x * y)
/ y = x.
(x / y)
* y = x.
% left Bol (universally LIP, universally LAP)
(x * (y
* x)) * z = x * (y * (x * z)).
% C a Moufang element
C * ((x
* y) * C) = (C * x) * (y * C).
% assumption
(x * x) * (C * y) = (x * C) * (x * y).
end_of_list.
formulas(goals).
% C in commutant
C * x =
x * C.
end_of_list.