% 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).