%--------------------------------------------------------------------------
% File     : GRP003+0 : TPTP v7.2.0. Released v2.5.0.
% Domain   : Group Theory
% Axioms   : Group theory axioms
% Version  : [MOW76] axioms.
% English  :

% Refs     : [MOW76] McCharen et al. (1976), Problems and Experiments for a
%          : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr
%          : [Ver93] Veroff (1993), Email to G. Sutcliffe
% Source   : TPTP
% Names    :

% Status   : Satisfiable
% Syntax   : Number of formulae    :    8 (   5 unit)
%            Number of atoms       :   16 (   1 equality)
%            Maximal formula depth :   10 (   5 average)
%            Number of connectives :    8 (   0 ~  ;   0  |;   5  &)
%                                         (   0 <=>;   3 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    2 (   0 propositional; 2-3 arity)
%            Number of functors    :    3 (   1 constant; 0-2 arity)
%            Number of variables   :   22 (   0 singleton;  22 !;   0 ?)
%            Maximal term depth    :    2 (   1 average)
% SPC      : 

% Comments :
%--------------------------------------------------------------------------
fof(left_identity,axiom,
    ( ! [X] : product(identity,X,X) )).

fof(right_identity,axiom,
    ( ! [X] : product(X,identity,X) )).

fof(left_inverse,axiom,
    ( ! [X] : product(inverse(X),X,identity) )).

fof(right_inverse,axiom,
    ( ! [X] : product(X,inverse(X),identity) )).

%----This axiom is called closure or totality in some axiomatisations
fof(total_function1,axiom,
    ( ! [X,Y] : product(X,Y,multiply(X,Y)) )).

%----This axiom is called well_definedness in some axiomatisations
fof(total_function2,axiom,
    ( ! [W,X,Y,Z] :
        ( ( product(X,Y,Z)
          & product(X,Y,W) )
       => Z = W ) )).

fof(associativity1,axiom,
    ( ! [X,Y,Z,U,V,W] :
        ( ( product(X,Y,U)
          & product(Y,Z,V)
          & product(U,Z,W) )
       => product(X,V,W) ) )).

fof(associativity2,axiom,
    ( ! [X,Y,Z,U,V,W] :
        ( ( product(X,Y,U)
          & product(Y,Z,V)
          & product(X,V,W) )
       => product(U,Z,W) ) )).

%--------------------------------------------------------------------------