%--------------------------------------------------------------------------
% File     : RNG034-1 : TPTP v2.1.0. Released v1.0.0.
% Domain   : Ring Theory (Alternative)
% Problem  : A skew symmetry relation of the associator
% Version  : [AH90] (equality) axioms.
% English  : 

% Refs     : [AH90]  Anantharaman & Hsiang (1990), Automated Proofs of the 
% Source   : [AH90]
% Names    : PROOF II [AH90]

% Status   : unsatisfiable
% Rating   : 0.67 v2.1.0, 1.00 v2.0.0
% Syntax   : Number of clauses    :   19 (   0 non-Horn;  17 unit;   4 RR)
%            Number of literals   :   21 (  21 equality)
%            Maximal clause size  :    2 (   1 average)
%            Number of predicates :    1 (   0 propositional; 2-2 arity)
%            Number of functors   :    8 (   4 constant; 0-3 arity)
%            Number of variables  :   35 (   2 singleton)
%            Maximal term depth   :    5 (   2 average)

% Comments : 
%          : tptp2X -f tptp -t rm_equality:rstfp RNG034-1.p 
%--------------------------------------------------------------------------
input_clause(left_additive_identity,axiom,
    [++ equal(add(additive_identity, X), X)]).

input_clause(left_multiplicative_zero,axiom,
    [++ equal(multiply(additive_identity, X), additive_identity)]).

input_clause(right_multiplicative_zero,axiom,
    [++ equal(multiply(X, additive_identity), additive_identity)]).

input_clause(add_inverse,axiom,
    [++ equal(add(additive_inverse(X), X), additive_identity)]).

input_clause(sum_of_inverses,axiom,
    [++ equal(additive_inverse(add(X, Y)), add(additive_inverse(X), additive_inverse(Y)))]).

input_clause(additive_inverse_additive_inverse,axiom,
    [++ equal(additive_inverse(additive_inverse(X)), X)]).

input_clause(multiply_over_add1,axiom,
    [++ equal(multiply(X, add(Y, Z)), add(multiply(X, Y), multiply(X, Z)))]).

input_clause(multiply_over_add2,axiom,
    [++ equal(multiply(add(X, Y), Z), add(multiply(X, Z), multiply(Y, Z)))]).

input_clause(right_alternative,axiom,
    [++ equal(multiply(multiply(X, Y), Y), multiply(X, multiply(Y, Y)))]).

input_clause(left_alternative,axiom,
    [++ equal(multiply(multiply(X, X), Y), multiply(X, multiply(X, Y)))]).

input_clause(inverse_product1,axiom,
    [++ equal(multiply(additive_inverse(X), Y), additive_inverse(multiply(X, Y)))]).

input_clause(inverse_product2,axiom,
    [++ equal(multiply(X, additive_inverse(Y)), additive_inverse(multiply(X, Y)))]).

input_clause(inverse_additive_identity,axiom,
    [++ equal(additive_inverse(additive_identity), additive_identity)]).

input_clause(commutativity_for_addition,axiom,
    [++ equal(add(X, Y), add(Y, X))]).

input_clause(associativity_for_addition,axiom,
    [++ equal(add(X, add(Y, Z)), add(add(X, Y), Z))]).

input_clause(left_cancellation_for_addition,axiom,
    [-- equal(add(X, Z), add(Y, Z)),
     ++ equal(X, Y)]).

input_clause(right_cancellation_for_addition,axiom,
    [-- equal(add(Z, X), add(Z, Y)),
     ++ equal(X, Y)]).

input_clause(associator,axiom,
    [++ equal(associator(X, Y, Z), add(multiply(multiply(X, Y), Z), additive_inverse(multiply(X, multiply(Y, Z)))))]).

input_clause(prove_skew_symmetry,conjecture,
    [-- equal(associator(cy, cx, cz), additive_inverse(associator(cx, cy, cz)))]).
%--------------------------------------------------------------------------