Note: that $(A2)_L$ is a subloop is well known, so we don’t include a proof, here.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% inverses

x * x' = 0.

x' * x = 0.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% A and B are A1y

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

z * ((x * B) * z) = (z * x) * (B * z).

end_of_list.

formulas(goals).

% A * B, A / B, and A \ B are A1y

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

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

z * ((x * (A \ B)) * z) = (z * x) * ((A \ B) * 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.

% inverses

x * x' = 0.

x' * x = 0.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% A and B are A1x

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

z * ((B * y) * z) = (z * B) * (y * z).

end_of_list.

formulas(goals).

% A * B, A \ B, and A / B are A1x

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

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

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

end_of_list.