assign(order, kbo).

formulas(assumptions).

% identity element

1 * x = x.

x * 1 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% flexible, alternative

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

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

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

% A is an (A) element

% A2

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

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

% consequences

% B2

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

end_of_list.

formulas(goals).

% B1x

(z * (A * y)) * z = (z * A) * (y * z).

end_of_list.

assign(order, kbo).

formulas(assumptions).

% identity element

1 * x = x.

x * 1 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% flexible, alternative

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

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

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

% A is an (A) element

% A2

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

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

% consequences

% B2

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

% B1x

(z * (A * y)) * z = (z * A) * (y * z).

end_of_list.

formulas(goals).

% B1y

(z * (x * A)) * z = (z * x) * (A * z).

end_of_list.

assign(order, kbo).

formulas(assumptions).

% identity element

1 * x = x.

x * 1 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% flexible, alternative

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

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

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

% A is an (A) element

% A2

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

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

% consequences

% B2

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

% B1x

(z * (A * y)) * z = (z * A) * (y * z).

% B1y

(z * (x * A)) * z = (z * x) * (A * z).

end_of_list.

formulas(goals).

% C1x

z * (A * (z * y)) = ((z * A) * z) * y.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% identity element

1 * x = x.

x * 1 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% flexible, alternative

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

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

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

% A is an (A) element

% A2

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

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

% consequences

% B2

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

% B1x

(z * (A * y)) * z = (z * A) * (y * z).

% B1y

(z * (x * A)) * z = (z * x) * (A * z).

% C1x

z * (A * (z * y)) = ((z * A) * z) * y.

end_of_list.

formulas(goals).

% D1y

((x * z) * A) * z = x * (z * (A * z)).

end_of_list.

assign(order, kbo).

formulas(assumptions).

% identity element

1 * x = x.

x * 1 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% flexible, alternative

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

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

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

% A is an (A) element

% A2

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

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

% consequences

% B2

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

% B1x

(z * (A * y)) * z = (z * A) * (y * z).

% B1y

(z * (x * A)) * z = (z * x) * (A * z).

% C1x

z * (A * (z * y)) = ((z * A) * z) * y.

% D1y

((x * z) * A) * z = x * (z * (A * z)).

end_of_list.

formulas(goals).

% C2

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

end_of_list.

assign(order, kbo).

formulas(assumptions).

% identity element

1 * x = x.

x * 1 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% flexible, alternative

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

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

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

% A is an (A) element

% A2

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

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

% consequences

% B2

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

% B1x

(z * (A * y)) * z = (z * A) * (y * z).

% B1y

(z * (x * A)) * z = (z * x) * (A * z).

% C1x

z * (A * (z * y)) = ((z * A) * z) * y.

% D1y

((x * z) * A) * z = x * (z * (A * z)).

% C2

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

end_of_list.

formulas(goals).

% D2

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

end_of_list.

assign(order, kbo).

formulas(assumptions).

% identity element

1 * x = x.

x * 1 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% flexible, alternative

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

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

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

% A is an (A) element

% A2

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

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

% consequences

% B2

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

% B1x

(z * (A * y)) * z = (z * A) * (y * z).

% B1y

(z * (x * A)) * z = (z * x) * (A * z).

% C1x

z * (A * (z * y)) = ((z * A) * z) * y.

% D1y

((x * z) * A) * z = x * (z * (A * z)).

% C2

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

% D2

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

end_of_list.

formulas(goals).

% C1y

z * (x * (z * A)) = ((z * x) * z) * A.

end_of_list.

assign(order, kbo).

formulas(assumptions).

% identity element

1 * x = x.

x * 1 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% flexible, alternative

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

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

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

% A is an (A) element

% A2

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

% A1x

z * ((A * y) * z) = (z * A) * (y * z).

% A1y

z * ((x * A) * z) = (z * x) * (A * z).

% consequences

% B2

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

% B1x

(z * (A * y)) * z = (z * A) * (y * z).

% B1y

(z * (x * A)) * z = (z * x) * (A * z).

% C1x

z * (A * (z * y)) = ((z * A) * z) * y.

% D1y

((x * z) * A) * z = x * (z * (A * z)).

% C2

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

% D2

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

% C1y

z * (x * (z * A)) = ((z * x) * z) * A.

end_of_list.

formulas(goals).

% D1x

((A * z) * y) * z = A * (z * (y * z)).

end_of_list.