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 is a fourth power

B * (B * (B * B)) = A.

end_of_list.

formulas(goals).

% A is in commutant (hence center)

x * A = A * 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.

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

% A is a fourth power

B * (B * (B * B)) = A.

% so A is in commutant

x * A = A * x.

% C is a sixth power

B * (B * (B * (B * (B * B)))) = C.

end_of_list.

formulas(goals).

% C is a WIP element

C * (x * C)' = 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.

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

% C is a WIP element

C * (x * C)' = x'.

end_of_list.

formulas(goals).

% C^2 in right nucleus

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

end_of_list.