%--------------------------------------------------------------------------
% 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 tptp -t rm_equality:rstfp RNG005-1.p 
%--------------------------------------------------------------------------
input_clause(additive_identity1,axiom,
    [++ sum(additive_identity, X, X)]).

input_clause(additive_identity2,axiom,
    [++ sum(X, additive_identity, X)]).

input_clause(closure_of_multiplication,axiom,
    [++ product(X, Y, multiply(X, Y))]).

input_clause(closure_of_addition,axiom,
    [++ sum(X, Y, add(X, Y))]).

input_clause(left_inverse,axiom,
    [++ sum(additive_inverse(X), X, additive_identity)]).

input_clause(right_inverse,axiom,
    [++ sum(X, additive_inverse(X), additive_identity)]).

input_clause(associativity_of_addition1,axiom,
    [-- sum(X, Y, U),
     -- sum(Y, Z, V),
     -- sum(U, Z, W),
     ++ sum(X, V, W)]).

input_clause(associativity_of_addition2,axiom,
    [-- sum(X, Y, U),
     -- sum(Y, Z, V),
     -- sum(X, V, W),
     ++ sum(U, Z, W)]).

input_clause(commutativity_of_addition,axiom,
    [-- sum(X, Y, Z),
     ++ sum(Y, X, Z)]).

input_clause(associativity_of_multiplication1,axiom,
    [-- product(X, Y, U),
     -- product(Y, Z, V),
     -- product(U, Z, W),
     ++ product(X, V, W)]).

input_clause(associativity_of_multiplication2,axiom,
    [-- product(X, Y, U),
     -- product(Y, Z, V),
     -- product(X, V, W),
     ++ product(U, Z, W)]).

input_clause(distributivity1,axiom,
    [-- product(X, Y, V1),
     -- product(X, Z, V2),
     -- sum(Y, Z, V3),
     -- product(X, V3, V4),
     ++ sum(V1, V2, V4)]).

input_clause(distributivity2,axiom,
    [-- product(X, Y, V1),
     -- product(X, Z, V2),
     -- sum(Y, Z, V3),
     -- sum(V1, V2, V4),
     ++ product(X, V3, V4)]).

input_clause(distributivity3,axiom,
    [-- product(Y, X, V1),
     -- product(Z, X, V2),
     -- sum(Y, Z, V3),
     -- product(V3, X, V4),
     ++ sum(V1, V2, V4)]).

input_clause(distributivity4,axiom,
    [-- product(Y, X, V1),
     -- product(Z, X, V2),
     -- sum(Y, Z, V3),
     -- sum(V1, V2, V4),
     ++ product(V3, X, V4)]).

input_clause(addition_is_well_defined,axiom,
    [-- sum(X, Y, U),
     -- sum(X, Y, V),
     ++ equal(U, V)]).

input_clause(multiplication_is_well_defined,axiom,
    [-- product(X, Y, U),
     -- product(X, Y, V),
     ++ equal(U, V)]).

input_clause(a_times_b,hypothesis,
    [++ product(a, b, d)]).

input_clause(a_inverse_times_b,hypothesis,
    [++ product(additive_inverse(a), b, c)]).

input_clause(prove_sum_is_additive_id,conjecture,
    [-- sum(c, d, additive_identity)]).
%--------------------------------------------------------------------------