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

 

% A2

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

 

end_of_list.

 

formulas(goals).

 

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

 

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

 

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

 

end_of_list.

 

formulas(goals).

 

% C2

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

 

% C1x

z * (A * (z * y)) = ((z * A) * z) * y.

 

end_of_list.