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.

% inverses

x' * x = 1.

x * x' = 1.

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

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

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

end_of_list.

formulas(goals).

% Cheban

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

end_of_list.

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.

% inverses

x' * x = 1.

x * x' = 1.

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

% flexible

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

end_of_list.

formulas(goals).

% Cheban

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

end_of_list.

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.

% inverses

x' * x = 1.

x * x' = 1.

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

% RAP

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

end_of_list.

formulas(goals).

% Cheban

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

end_of_list.

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.

% inverses

x' * x = 1.

x * x' = 1.

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

% WIP

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

end_of_list.

formulas(goals).

% Cheban

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

end_of_list.