%--------------------------------------------------------------------------
% File     : RNG019-6 : TPTP v2.4.1. Released v1.0.0.
% Domain   : Ring Theory (Alternative)
% Problem  : First part of the linearised form of the associator
% Version  : [Ste87] (equality) axioms.
% English  : The associator can be expressed in another form called 
%            a linearised form. There are three clauses to be proved 
%            to establish the equivalence of the two forms.

% Refs     : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin
% Source   : [Ste87]
% Names    : c24 [Ste87]

% Status   : unsatisfiable
% Rating   : 0.25 v2.4.0, 0.67 v2.2.1, 0.78 v2.2.0, 0.71 v2.1.0, 0.50 v2.0.0
% Syntax   : Number of clauses    :   16 (   0 non-Horn;  16 unit;   1 RR)
%            Number of literals   :   16 (  16 equality)
%            Maximal clause size  :    1 (   1 average)
%            Number of predicates :    1 (   0 propositional; 2-2 arity)
%            Number of functors   :   10 (   5 constant; 0-3 arity)
%            Number of variables  :   27 (   2 singleton)
%            Maximal term depth   :    5 (   2 average)

% Comments : 
%          : tptp2X -f tptp -t rm_equality:rstfp RNG019-6.p 
%--------------------------------------------------------------------------
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_additive_identity,axiom,
    [++ equal(add(additive_identity, X), X)]).

input_clause(right_additive_identity,axiom,
    [++ equal(add(X, additive_identity), 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(left_additive_inverse,axiom,
    [++ equal(add(additive_inverse(X), X), additive_identity)]).

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

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

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

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

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(associator,axiom,
    [++ equal(associator(X, Y, Z), add(multiply(multiply(X, Y), Z), additive_inverse(multiply(X, multiply(Y, Z)))))]).

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

input_clause(prove_linearised_form1,conjecture,
    [-- equal(associator(x, y, add(u, v)), add(associator(x, y, u), associator(x, y, v)))]).
%--------------------------------------------------------------------------