%
%  In a group, the inverse of the inverse is the original element.
%

% works

set(auto).

list(usable).

% Group axioms

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

i(i(a)) != a.	 % Denial of conclusion (a is Skolem constant)

end_of_list.