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.

% Cheban

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

% LCC

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

% RCC

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

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

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

% WIP

x * ((y * x) \ 1) = y \ 1.

% 2-sided inverse

x' * x = 1.

x * x' = 1.

% associator, a(x,y,z), defined

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

% commatator, K(x,y), defined

x * y = (y * x) * K(x,y).

end_of_list.

formulas(goals).

K(K(x,y),z) = 1.

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.

% Cheban

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

% LCC

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

% RCC

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

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

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

% WIP

x * ((y * x) \ 1) = y \ 1.

% 2-sided inverse

x' * x = 1.

x * x' = 1.

% associator, a(x,y,z), defined

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

% commatator, K(x,y), defined

x * y = (y * x) * K(x,y).

% so

K(K(x,y),z) = 1.

end_of_list.

formulas(goals).

a(K(x,y),u,v) = 1.

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.

% Cheban

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

% LCC

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

% RCC

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

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

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

% WIP

x * ((y * x) \ 1) = y \ 1.

% 2-sided inverse

x' * x = 1.

x * x' = 1.

% associator, a(x,y,z), defined

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

% commatator, K(x,y), defined

x * y = (y * x) * K(x,y).

% so

K(K(x,y),z) = 1.

a(K(x,y),u,v) = 1.

end_of_list.

formulas(goals).

a(u,v,K(x,y)) = 1.

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.

% Cheban

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

% LCC

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

% RCC

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

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

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

% WIP

x * ((y * x) \ 1) = y \ 1.

% 2-sided inverse

x' * x = 1.

x * x' = 1.

% associator, a(x,y,z), defined

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

% commatator, K(x,y), defined

x * y = (y * x) * K(x,y).

% so

K(K(x,y),z) = 1.

a(K(x,y),u,v) = 1.

a(u,v,K(x,y)) = 1.

end_of_list.

formulas(goals).

K(a(x,y,z),u) = 1.

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.

% Cheban

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

% LCC

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

% RCC

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

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

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

% WIP

x * ((y * x) \ 1) = y \ 1.

% 2-sided inverse

x' * x = 1.

x * x' = 1.

% associator, a(x,y,z), defined

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

% commatator, K(x,y), defined

x * y = (y * x) * K(x,y).

% so

K(K(x,y),z) = 1.

a(K(x,y),u,v) = 1.

a(u,v,K(x,y)) = 1.

K(a(x,y,z),u) = 1.

end_of_list.

formulas(goals).

a(x,y,a(u,v,w)) = 1.

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.

% Cheban

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

% LCC

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

% RCC

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

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

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

% WIP

x * ((y * x) \ 1) = y \ 1.

% 2-sided inverse

x' * x = 1.

x * x' = 1.

% associator, a(x,y,z), defined

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

% commatator, K(x,y), defined

x * y = (y * x) * K(x,y).

% so

K(K(x,y),z) = 1.

a(K(x,y),u,v) = 1.

a(u,v,K(x,y)) = 1.

a(x,y,a(u,v,w)) = 1.

K(a(x,y,z),u) = 1.

a(x,y,a(u,v,w)) = 1.

end_of_list.

formulas(goals).

a(a(x,y,z),u,v) = 1.

end_of_list.