%==========================
% Overbeek's problem 1
%==========================

/*
In a group, if x * x * x = e for all x in the group, then
h(h(x, y), y) = e for all x and y, where the commutator h(x, y) is defined
as x * y * i(x) * i(y).
*/

axiom( [ [], [e+X=X] ] ).
axiom( [ [], [i(X)+X=e] ] ).
axiom( [ [], [(X+Y)+Z=X+(Y+Z)] ] ).
axiom( [ [], [X+(X+X)=e] ] ).
axiom( [ [], [h(X, Y) = X+(Y+(i(X)+i(Y))) ] ] ).

axiom( [ [h(h(a,b),b)=e], [] ] ).

precedence( [h, i, +, e, a, b] ).
predicates( [] ).