assign(order, kbo).

assign(eq_defs,fold).

formulas(assumptions).

% id

1 * x = x.

x * 1 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% left Cheban

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

% R(x)^2 = L(x)^2

(u * x) * x = x * (x * u).

% LCC

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

% A right nuclear and in commutant

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

x * A = A * x.

end_of_list.

formulas(goals).

% A middle nuclear

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

end_of_list.