GRP004-0.ax

%--------------------------------------------------------------------------
% File     : GRP004-0 : TPTP v7.0.0. Released v1.0.0.
% Domain   : Group Theory
% Axioms   : Group theory (equality) axioms
% Version  : [MOW76] (equality) axioms :
%            Reduced > Complete.
% English  :

% Refs     : [MOW76] McCharen et al. (1976), Problems and Experiments for a
%          : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr
% Source   : [ANL]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of clauses    :    3 (   0 non-Horn;   3 unit;   0 RR)
%            Number of atoms      :    3 (   3 equality)
%            Maximal clause size  :    1 (   1 average)
%            Number of predicates :    1 (   0 propositional; 2-2 arity)
%            Number of functors   :    3 (   1 constant; 0-2 arity)
%            Number of variables  :    5 (   0 singleton)
%            Maximal term depth   :    3 (   2 average)
% SPC      : 

% Comments : [MOW76] also contains redundant right_identity and
%            right_inverse axioms.
%          : These axioms are also used in [Wos88] p.186, also with
%            right_identity and right_inverse.
%--------------------------------------------------------------------------
%----For any x and y in the group x*y is also in the group. No clause
%----is needed here since this is an instance of reflexivity

%----There exists an identity element
cnf(left_identity,axiom,
    ( multiply(identity,X) = X )).

%----For any x in the group, there exists an element y such that x*y = y*x
%----= identity.
cnf(left_inverse,axiom,
    ( multiply(inverse(X),X) = identity )).

%----The operation '*' is associative
cnf(associativity,axiom,
    ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) )).

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