assign(order, kbo).

formulas(assumptions).

% divisible groupoid

(x / y) * y = x.

x * (x \ y) = y.

% A2

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

end_of_list.

formulas(goals).

(x * y) / y = x.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% divisible groupoid

(x / y) * y = x.

x * (x \ y) = y.

% A2

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

end_of_list.

formulas(goals).

x \ (x * y) = y.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% divisible groupoid

(x / y) * y = x.

x * (x \ y) = y.

% C2

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

end_of_list.

formulas(goals).

(x * y) / y = x.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% divisible groupoid

(x / y) * y = x.

x * (x \ y) = y.

% C2

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

end_of_list.

formulas(goals).

x \ (x * y) = y.

end_of_list.

The proofs for (B) are dual to the proofs for (A), and the proofs for (D) are dual to the proofs for (C). Thus, we have shown that divisible groupoids satisfying any one of (A), (B), (C), or (D) are, in fact, quasigroups. Thus, by Kunen’s result, they are Moufang loops.