% these are the group axioms:

fof(assoc,axiom,
    ! [X,Y,Z] : times(X,times(Y,Z)) = times(times(X,Y),Z)).

fof(right_identity,axiom,
    ! [X] : times(X,e) = X).

fof(right_inverse,axiom,
    ! [X] : times(X,inv(X)) = e).

% boolean connectives:
%   or:       _ | _ | _
%   and:      _ & _ & _
%   not:      ~ _
%   implies:  _ => _
%
% quantification:
%   universal:    ! [X,Y,Z] : _
%   existential:  ? [X,Y,Z] : _

% formulas marked as "axiom" are converted directly into CNF,
% formulas marked as "conjecture" are negated first:

fof(right_identity_is_also_left_identity,conjecture,
    ! [X] : times(e,X) = X).