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

set(auto).

list(usable).

% Group axioms, with left- and right-identity relationships expressed.

e(f(x, f(y, z)), f(f(x, y), z)).
e(f(x, 1), x).
e(f(1, x), x).
e(f(x, i(x)), 1).
e(f(i(x), x), 1).

% Equality axioms

e(x, x).
-e(x, y) | -e(v, w) | e(f(x, v), f(y, w)).
-e(x, y) | e(y, x).
-e(x, y) | -e(y, z) | e(x, z).

% Denial of conclusion

-e(i(i(b)), b).

end_of_list.