if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% C is an A2-element

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

% C in commutant

C * x = x * C.

% R(u,x,y) = u R(x) R(y) R(xy)^{-1}

R(u,x,y) = ((u * x) * y) / (x * y).

end_of_list.

formulas(goals).

R(R(R(C,A,B),A,B),A,B) = C.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% A is an A2-element

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

% C in commutant

C * x = x * C.

% R(u,x,y) = u R(x) R(y) R(xy)^{-1}

R(u,x,y) = ((u * x) * y) / (x * y).

end_of_list.

formulas(goals).

R(R(R(C,A,B),A,B),A,B) = C.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% B is an A2-element

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

% C in commutant

C * x = x * C.

% R(u,x,y) = u R(x) R(y) R(xy)^{-1}

R(u,x,y) = ((u * x) * y) / (x * y).

end_of_list.

formulas(goals).

R(R(R(C,A,B),A,B),A,B) = C.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% C is an A2-element

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

% C in commutant

C * x = x * C.

% L(u,x,y) = u L(x) L(y) L(yx)^{-1}

L(u,x,y) = (y * x)' * (y * (x * u)).

end_of_list.

formulas(goals).

L(L(L(C,A,B),A,B),A,B) = C.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% A is an A2-element

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

% C in commutant

C * x = x * C.

% L(u,x,y) = u L(x) L(y) L(yx)^{-1}

L(u,x,y) = (y * x)' * (y * (x * u)).

end_of_list.

formulas(goals).

L(L(L(C,A,B),A,B),A,B) = C.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% B is an A2-element

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

% C in commutant

C * x = x * C.

% L(u,x,y) = u L(x) L(y) L(yx)^{-1}

L(u,x,y) = (y * x)' * (y * (x * u)).

end_of_list.

formulas(goals).

L(L(L(C,A,B),A,B),A,B) = C.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% C is an A2-element

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

% C in commutant

C * x = x * C.

% R(u,x,y) = u R(x) R(y) R(xy)^{-1}

R(u,x,y) = ((u * x) * y) / (x * y).

end_of_list.

formulas(goals).

R(R(R(x,C,A),C,A),C,A) = x.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% C is an A2-element

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

% C in commutant

C * x = x * C.

% R(u,x,y) = u R(x) R(y) R(xy)^{-1}

R(u,x,y) = ((u * x) * y) / (x * y).

end_of_list.

formulas(goals).

R(R(R(x,A,C),A,C),A,C) = x.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% A is an A2-element

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

% C in commutant

C * x = x * C.

% R(u,x,y) = u R(x) R(y) R(xy)^{-1}

R(u,x,y) = ((u * x) * y) / (x * y).

end_of_list.

formulas(goals).

R(R(R(x,C,A),C,A),C,A) = x.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% A is an A2-element

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

% C in commutant

C * x = x * C.

% L(u,x,y) = u L(x) L(y) L(yx)^{-1}

%L(u,x,y) = (y * x)' * (y * (x * u)).

% R(u,x,y) = u R(x) R(y) R(xy)^{-1}

R(u,x,y) = ((u * x) * y) / (x * y).

end_of_list.

formulas(goals).

R(R(R(x,A,C),A,C),A,C) = x.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% C is an A2-element

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

% C in commutant

C * x = x * C.

% L(u,x,y) = u L(x) L(y) L(yx)^{-1}

L(u,x,y) = (y * x)' * (y * (x * u)).

end_of_list.

formulas(goals).

L(L(L(x,C,A),C,A),C,A) = x.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% C is an A2-element

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

% C in commutant

C * x = x * C.

% L(u,x,y) = u L(x) L(y) L(yx)^{-1}

L(u,x,y) = (y * x)' * (y * (x * u)).

end_of_list.

formulas(goals).

L(L(L(x,A,C),A,C),A,C) = x.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% A is an A2-element

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

% C in commutant

C * x = x * C.

% L(u,x,y) = u L(x) L(y) L(yx)^{-1}

L(u,x,y) = (y * x)' * (y * (x * u)).

end_of_list.

formulas(goals).

L(L(L(x,C,A),C,A),C,A) = x.

end_of_list.

if(Prover9).

assign(order, kbo).

assign(eq_defs,fold).

end_if.

formulas(assumptions).

% identity element

0 * x = x.

x * 0 = x.

% quasigroup

x * (x \ y) = y.

x \ (x * y) = y.

(x * y) / y = x.

(x / y) * y = x.

% 2-sided inverses

x' * x = 0.

x * x' = 0.

% LIP

x' * (x * y) = y.

% LAP

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

% left Bol (universally LIP, universally LAP)

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

% A is an A2-element

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

% C in commutant

C * x = x * C.

% L(u,x,y) = u L(x) L(y) L(yx)^{-1}

L(u,x,y) = (y * x)' * (y * (x * u)).

end_of_list.

formulas(goals).

L(L(L(x,A,C),A,C),A,C) = x.

end_of_list.