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.

% Moufang

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

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

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

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

% IP

x' * (x * y) = y.

(y * x) * x' = y.

% 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,x,y),x,y),x,y) = C.

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

R(R(R(x,y,C),y,C),y,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.

% Moufang

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

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

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

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

% IP

x' * (x * y) = y.

(y * x) * x' = y.

% C and B in commutant

C * x = x * C.

B * x = x * B.

% a defined

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

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

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

% so

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

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

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

% facts

R(x * y,C,w) = R(x,C,w) * R(y,C,w).

R(x * y,w,C) = R(x,w,C) * R(y,w,C).

end_of_list.

formulas(goals).

R(C * B,x,y) = R(C,x,y) * R(B,x,y).

end_of_list.