assign(order, kbo).

formulas(assumptions).

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% A2

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

% C2

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

end_of_list.

formulas(goals).

% A / A is a two-sided identity element

(A / A) * x = x.

x * (A / A) = x.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% A2

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

% D2

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

end_of_list.

formulas(goals).

% A / A is a two-sided identity element

(A / A) * x = x.

x * (A / A) = x.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% C2

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

% D2

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

end_of_list.

formulas(goals).

% A / A is a two-sided identity element

(A / A) * x = x.

x * (A / A) = x.

end_of_list.