#--------------------------------------------------------------------------
# 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 setheo:sign -t rm_equality:rstfp RNG034-1.p 
#--------------------------------------------------------------------------
# left_additive_identity, axiom.
equal(add(additive_identity, X), X) <- .

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

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

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

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

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

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

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

# 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))) <- .

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

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

# inverse_additive_identity, axiom.
equal(additive_inverse(additive_identity), additive_identity) <- .

# 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_cancellation_for_addition, axiom.
equal(X, Y) <- 
    equal(add(X, Z), add(Y, Z)).

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

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

# prove_skew_symmetry, conjecture.
 <- equal(associator(cy, cx, cz), additive_inverse(associator(cx, cy, cz))).

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