%--------------------------------------------------------------------------
% File     : RNG002-0 : TPTP v7.2.0. Released v1.0.0.
% Domain   : Ring Theory
% Axioms   : Ring theory (equality) axioms
% Version  : [PS81] (equality) axioms :
%            Reduced & Augmented > Complete.
% English  :

% Refs     : [PS81]  Peterson & Stickel (1981), Complete Sets of Reductions
% Source   : [ANL]
% Names    :

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

% Comments : Not sure if these are complete. I don't know if the reductions
%            given in [PS81] are suitable for ATP.
%--------------------------------------------------------------------------
%----Existence of left identity for addition
cnf(left_identity,axiom,
    ( add(additive_identity,X) = X )).

%----Existence of left additive additive_inverse
cnf(left_additive_inverse,axiom,
    ( add(additive_inverse(X),X) = additive_identity )).

%----Distributive property of product over sum
cnf(distribute1,axiom,
    ( multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)) )).

cnf(distribute2,axiom,
    ( multiply(add(X,Y),Z) = add(multiply(X,Z),multiply(Y,Z)) )).

%----Inverse of identity is identity, stupid
cnf(additive_inverse_identity,axiom,
    ( additive_inverse(additive_identity) = additive_identity )).

%----Inverse of additive_inverse of X is X
cnf(additive_inverse_additive_inverse,axiom,
    ( additive_inverse(additive_inverse(X)) = X )).

%----Behavior of 0 and the multiplication operation
cnf(multiply_additive_id1,axiom,
    ( multiply(X,additive_identity) = additive_identity )).

cnf(multiply_additive_id2,axiom,
    ( multiply(additive_identity,X) = additive_identity )).

%----Inverse of (x + y) is additive_inverse(x) + additive_inverse(y)
cnf(distribute_additive_inverse,axiom,
    ( additive_inverse(add(X,Y)) = add(additive_inverse(X),additive_inverse(Y)) )).

%----x * additive_inverse(y) = additive_inverse (x * y)
cnf(multiply_additive_inverse1,axiom,
    ( multiply(X,additive_inverse(Y)) = additive_inverse(multiply(X,Y)) )).

cnf(multiply_additive_inverse2,axiom,
    ( multiply(additive_inverse(X),Y) = additive_inverse(multiply(X,Y)) )).

%----Associativity of addition
cnf(associative_addition,axiom,
    ( add(add(X,Y),Z) = add(X,add(Y,Z)) )).

%----Commutativity of addition
cnf(commutative_addition,axiom,
    ( add(X,Y) = add(Y,X) )).

%----Associativity of product
cnf(associative_multiplication,axiom,
    ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) )).

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