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.

% a defined

(x * y) * z = (x * (y * z)) * a(x,y,z).

end_of_list.

formulas(goals).

a(C,x * (x * x),y) = 0.

a(C,y,x * (x * x)) = 0.

a(x * (x * x),C,y) = 0.

a(x * (x * x),y,C) = 0.

a(y,x * (x * x),C) = 0.

a(y,C,x * (x * x)) = 0.

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

A * ((x * y) * A) = (A * x) * (y * A).

% C in commutant

C * x = x * C.

% a defined

(x * y) * z = (x * (y * z)) * a(x,y,z).

end_of_list.

formulas(goals).

a(C,A * (A * A),x) = 0.

a(C,x,A * (A * A)) = 0.

a(A * (A * A),C,x) = 0.

a(A * (A * A),x,C) = 0.

a(x,A * (A * A),C) = 0.

a(x,C,A * (A * A)) = 0.

end_of_list.