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

% works, Note: with formula_list, must quantify all

set(auto).

formula_list(usable).

% monoid axioms (f is the binary operator)

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


% Hypothesis

all x (f(x, x) = 1).

% Denial of conclusion

-(all x all y (f(x, y) = f(y, x))).

end_of_list.