#--------------------------------------------------------------------------
# File     : RNG005-1 : TPTP v2.1.0. Released v1.0.0.
# Domain   : Ring Theory
# Problem  : (-X*Y) + (X*Y) = additive_identity
# Version  : [Wos65] axioms.
# English  : 

# Refs     : [Wos65] Wos (1965), Unpublished Note
#          : [MOW76] McCharen et al. (1976), Problems and Experiments for a
# Source   : [SPRFN]
# Names    : Problem 23 [Wos65]

# Status   : unsatisfiable
# Rating   : 0.33 v2.1.0, 0.00 v2.0.0
# Syntax   : Number of clauses    :   20 (   0 non-Horn;   9 unit;  14 RR)
#            Number of literals   :   53 (   2 equality)
#            Maximal clause size  :    5 (   2 average)
#            Number of predicates :    3 (   0 propositional; 2-3 arity)
#            Number of functors   :    8 (   5 constant; 0-2 arity)
#            Number of variables  :   71 (   0 singleton)
#            Maximal term depth   :    2 (   1 average)

# Comments : These are the same axioms as in [MOW76].
#          : tptp2X -f setheo:sign -t rm_equality:rstfp RNG005-1.p 
#--------------------------------------------------------------------------
# additive_identity1, axiom.
sum(additive_identity, X, X) <- .

# additive_identity2, axiom.
sum(X, additive_identity, X) <- .

# closure_of_multiplication, axiom.
product(X, Y, multiply(X, Y)) <- .

# closure_of_addition, axiom.
sum(X, Y, add(X, Y)) <- .

# left_inverse, axiom.
sum(additive_inverse(X), X, additive_identity) <- .

# right_inverse, axiom.
sum(X, additive_inverse(X), additive_identity) <- .

# associativity_of_addition1, axiom.
sum(X, V, W) <- 
    sum(X, Y, U),
    sum(Y, Z, V),
    sum(U, Z, W).

# associativity_of_addition2, axiom.
sum(U, Z, W) <- 
    sum(X, Y, U),
    sum(Y, Z, V),
    sum(X, V, W).

# commutativity_of_addition, axiom.
sum(Y, X, Z) <- 
    sum(X, Y, Z).

# associativity_of_multiplication1, axiom.
product(X, V, W) <- 
    product(X, Y, U),
    product(Y, Z, V),
    product(U, Z, W).

# associativity_of_multiplication2, axiom.
product(U, Z, W) <- 
    product(X, Y, U),
    product(Y, Z, V),
    product(X, V, W).

# distributivity1, axiom.
sum(V1, V2, V4) <- 
    product(X, Y, V1),
    product(X, Z, V2),
    sum(Y, Z, V3),
    product(X, V3, V4).

# distributivity2, axiom.
product(X, V3, V4) <- 
    product(X, Y, V1),
    product(X, Z, V2),
    sum(Y, Z, V3),
    sum(V1, V2, V4).

# distributivity3, axiom.
sum(V1, V2, V4) <- 
    product(Y, X, V1),
    product(Z, X, V2),
    sum(Y, Z, V3),
    product(V3, X, V4).

# distributivity4, axiom.
product(V3, X, V4) <- 
    product(Y, X, V1),
    product(Z, X, V2),
    sum(Y, Z, V3),
    sum(V1, V2, V4).

# addition_is_well_defined, axiom.
equal(U, V) <- 
    sum(X, Y, U),
    sum(X, Y, V).

# multiplication_is_well_defined, axiom.
equal(U, V) <- 
    product(X, Y, U),
    product(X, Y, V).

# a_times_b, hypothesis.
product(a, b, d) <- .

# a_inverse_times_b, hypothesis.
product(additive_inverse(a), b, c) <- .

# prove_sum_is_additive_id, conjecture.
 <- sum(c, d, additive_identity).

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