%-------------------------------------------------------------------------- % File : RNG039-1 : TPTP v2.1.0. Released v1.0.0. % Domain : Ring Theory % Problem : Ring property 2 % Version : [Wos65] axioms. % English : % Refs : [Wos65] Wos (1965), Unpublished Note % : [MOW76] McCharen et al. (1976), Problems and Experiments for a % Source : [SPRFN] % Names : Problem 28 [Wos65] % Status : unsatisfiable % Rating : 0.50 v2.1.0, 0.60 v2.0.0 % Syntax : Number of clauses : 60 ( 0 non-Horn; 49 unit; 40 RR) % Number of literals : 93 ( 8 equality) % Maximal clause size : 5 ( 1 average) % Number of predicates : 3 ( 0 propositional; 2-3 arity) % Number of functors : 8 ( 5 constant; 0-2 arity) % Number of variables : 91 ( 1 singleton) % Maximal term depth : 2 ( 1 average) % Comments : These are the same axioms as in [MOW76]. % : tptp2X -f tptp -t rm_equality:rstfp RNG039-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(absorbtion1,axiom, [++ sum(A, add(A, B), B)]). input_clause(absorbtion2,axiom, [++ sum(add(A, B), B, A)]). input_clause(clause32,axiom, [++ sum(A, A, additive_identity)]). input_clause(clause33,axiom, [++ equal(add(A, additive_identity), A)]). input_clause(clause34,axiom, [++ equal(add(A, A), additive_identity)]). input_clause(clause35,axiom, [++ equal(multiply(A, A), A)]). input_clause(clause36,axiom, [++ equal(multiply(a, b), c)]). input_clause(clause37,axiom, [++ equal(multiply(b, a), d)]). input_clause(clause38,axiom, [++ sum(A, B, add(B, A))]). input_clause(clause39,axiom, [++ product(a, c, c)]). input_clause(clause40,axiom, [++ product(b, d, d)]). input_clause(clause41,axiom, [++ product(c, b, c)]). input_clause(clause42,axiom, [++ product(d, a, d)]). input_clause(clause43,axiom, [++ product(A, multiply(A, B), multiply(A, B))]). input_clause(clause44,axiom, [++ product(a, multiply(b, A), multiply(B, A))]). input_clause(clause45,axiom, [++ product(a, b, multiply(c, b))]). input_clause(clause46,axiom, [++ product(a, multiply(b, c), c)]). input_clause(clause47,axiom, [++ product(b, multiply(a, A), multiply(d, A))]). input_clause(clause48,axiom, [++ product(b, a, multiply(d, a))]). input_clause(clause49,axiom, [++ product(b, multiply(a, d), d)]). input_clause(clause50,axiom, [++ product(b, c, multiply(d, b))]). input_clause(clause51,axiom, [++ product(a, d, multiply(c, a))]). input_clause(clause52,axiom, [++ product(multiply(A, B), B, multiply(A, B))]). input_clause(clause53,axiom, [++ product(multiply(A, a), b, multiply(A, c))]). input_clause(clause54,axiom, [++ product(a, b, multiply(a, c))]). input_clause(clause55,axiom, [++ product(multiply(c, a), b, c)]). input_clause(clause56,axiom, [++ product(d, b, multiply(b, c))]). input_clause(clause57,axiom, [++ product(multiply(A, b), a, multiply(A, d))]). input_clause(clause58,axiom, [++ product(b, a, multiply(b, d))]). input_clause(clause59,axiom, [++ product(multiply(d, b), a, d)]). input_clause(clause60,axiom, [++ product(c, a, multiply(a, d))]). input_clause(clause63,axiom, [++ product(a, add(b, a), add(c, a))]). input_clause(clause64,axiom, [++ product(a, add(a, b), add(a, c))]). input_clause(clause65,axiom, [++ product(b, add(a, b), add(d, b))]). input_clause(clause66,axiom, [++ product(b, add(b, a), add(b, d))]). input_clause(clause67,axiom, [++ product(add(a, b), b, add(c, b))]). input_clause(clause68,axiom, [++ product(add(b, a), b, add(b, c))]). input_clause(clause69,axiom, [++ product(add(b, a), a, add(d, a))]). input_clause(clause70,axiom, [++ product(add(a, b), a, add(a, d))]). input_clause(clause71,axiom, [++ product(A, A, A)]). input_clause(a_times_b,conjecture, [++ product(a, b, c)]). input_clause(b_times_a,conjecture, [++ product(b, a, d)]). input_clause(prove_c_equals_d,conjecture, [-- equal(c, d)]). %--------------------------------------------------------------------------