% In a ring, x^5 = x => commutativity.

assign(order,kbo).
set(lex_order_vars).

assign(max_megs, 8000).

formulas(assumptions).

% axioms

0 + x = x.
x + 0 = x.

-x + x = 0.
x + -x = 0.

x + y = y + x.
(x + y) + z = x + (y + z).

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

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

% theorem hypothesis

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

end_of_list.

formulas(goals).

x * y = y * x.

end_of_list.

formulas(extra_assumptions).

% 10x = 0
x + (x + (x + (x + (x + (x + (x + (x + (x + x)))))))) = 0.

% 5xy + 5yx = 0
(x*y) + ((x*y) + ((x*y) + ((x*y) + ((x*y)
    + ((y*x) + ((y*x) + ((y*x) + ((y*x) + (y*x))))))))) = 0.

% 4xy + 6yx = 0
(x*y) + ((x*y) + ((x*y) + ((x*y) + ((y*x)
    + ((y*x) + ((y*x) + ((y*x) + ((y*x) + (y*x))))))))) = 0.

% 3xy + 7yx = 0
(x*y) + ((x*y) + ((x*y) + ((y*x) + ((y*x)
    + ((y*x) + ((y*x) + ((y*x) + ((y*x) + (y*x))))))))) = 0.

% 2xy + 8yx = 0
(x*y) + ((x*y) + ((y*x) + ((y*x) + ((y*x)
    + ((y*x) + ((y*x) + ((y*x) + ((y*x) + (y*x))))))))) = 0.

%  xy + 9yx = 0
(x*y) + ((y*x) + ((y*x) + ((y*x) + ((y*x)
    + ((y*x) + ((y*x) + ((y*x) + ((y*x) + (y*x))))))))) = 0.

end_of_list.
