#--------------------------------------------------------------------------
# File     : RNG019-6 : TPTP v2.1.0. 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.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 setheo:sign -t rm_equality:rstfp RNG019-6.p 
#--------------------------------------------------------------------------
# commutativity_for_addition, axiom.
equal(add(X, Y), add(Y, X)) <- .

# associativity_for_addition, axiom.
equal(add(X, add(Y, Z)), add(add(X, Y), Z)) <- .

# left_additive_identity, axiom.
equal(add(additive_identity, X), X) <- .

# right_additive_identity, axiom.
equal(add(X, additive_identity), X) <- .

# left_multiplicative_zero, axiom.
equal(multiply(additive_identity, X), additive_identity) <- .

# right_multiplicative_zero, axiom.
equal(multiply(X, additive_identity), additive_identity) <- .

# left_additive_inverse, axiom.
equal(add(additive_inverse(X), X), additive_identity) <- .

# right_additive_inverse, axiom.
equal(add(X, additive_inverse(X)), additive_identity) <- .

# distribute1, axiom.
equal(multiply(X, add(Y, Z)), add(multiply(X, Y), multiply(X, Z))) <- .

# distribute2, axiom.
equal(multiply(add(X, Y), Z), add(multiply(X, Z), multiply(Y, Z))) <- .

# additive_inverse_additive_inverse, axiom.
equal(additive_inverse(additive_inverse(X)), X) <- .

# right_alternative, axiom.
equal(multiply(multiply(X, Y), Y), multiply(X, multiply(Y, Y))) <- .

# left_alternative, axiom.
equal(multiply(multiply(X, X), Y), multiply(X, multiply(X, Y))) <- .

# associator, axiom.
equal(associator(X, Y, Z), add(multiply(multiply(X, Y), Z), additive_inverse(multiply(X, multiply(Y, Z))))) <- .

# commutator, axiom.
equal(commutator(X, Y), add(multiply(Y, X), additive_inverse(multiply(X, Y)))) <- .

# prove_linearised_form1, conjecture.
 <- equal(associator(x, y, add(u, v)), add(associator(x, y, u), associator(x, y, v))).

#--------------------------------------------------------------------------