%
%  In a monoid, if x*x = 1, then * is commutative.
%

set(auto).

list(usable).

% monoid axioms (f is the binary operator)

f(1,x) = x.

f(f(x,y),z) = f(x,f(y,z)).


f(x,x) = 1.        % Hypothesis


f(b,a) != f(a,b).  % Denial of conclusion (a, b are Skolem constants)

end_of_list.