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 an A1y-element

z * ((x * C) * z) = (z * x) * (C * z).

% C in commutant

C * x = x * C.

end_of_list.

formulas(goals).

% conditions

(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 an A1y-element

z * ((x * C) * z) = (z * x) * (C * z).

%C * x = x * C.

% condition

(C * C) * (x * y) = (C * x) * (C * y).

end_of_list.

formulas(goals).

% condition

(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 an A1y-element

z * ((x * C) * z) = (z * x) * (C * z).

% condition

(C * C) * (x * y) = (C * x) * (C * y).

end_of_list.

formulas(goals).

% condition

(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)).

% A an A1y-element

z * ((x * A) * z) = (z * x) * (A * z).

% C in commutant

C * x = x * C.

end_of_list.

formulas(goals).

% condition

(C * C) * (x * A) = (C * x) * (C * A).

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)).

% A an A1y-element

z * ((x * A) * z) = (z * x) * (A * z).

% condition

(C * C) * (x * A) = (C * x) * (C * A).

end_of_list.

formulas(goals).

% condition

(x * x) * (C * A) = (x * C) * (x * A).

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)).

% A an A1y-element

z * ((x * A) * z) = (z * x) * (A * z).

% C in commutant

%C * x = x * C.

% conditions

(x * x) * (C * A) = (x * C) * (x * A).

end_of_list.

formulas(goals).

% C in commutant

C * x = x * C.

end_of_list.