%
%  In a group, the inverse of a product is the product of the
%  inverses in reverse order.
%

$ 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(f(a, b)) != f(i(b), i(a)).  % Denial of conclusion (a,b are Skolem constants)

end_of_list.