%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG017-6 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:37:28 PM UTC 2026
% Result : Unsatisfiable 6.25s 1.29s
% Output : CNFRefutation 6.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 18
% Syntax : Number of clauses : 112 ( 112 unt; 0 nHn; 71 RR)
% Number of literals : 112 ( 111 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% Number of variables : 71 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t13,axiom,
sF0 = multiply(x,y),
introduced(definition) ).
cnf(t29,plain,
multiply(x,y) = sF0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sF1 = additive_inverse(multiply(x,y)),
introduced(definition) ).
cnf(t1723,plain,
sF1 = additive_inverse(sF0),
inference(step,[status(thm)],[t14,t29]) ).
cnf(t40,plain,
additive_inverse(sF0) = sF1,
inference(orient,[status(thm)],[t1723]) ).
cnf(t15,axiom,
sF2 = multiply(x,z),
introduced(definition) ).
cnf(t30,plain,
multiply(x,z) = sF2,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sF3 = additive_inverse(multiply(x,z)),
introduced(definition) ).
cnf(t1724,plain,
sF3 = additive_inverse(sF2),
inference(step,[status(thm)],[t16,t30]) ).
cnf(t47,plain,
additive_inverse(sF2) = sF3,
inference(orient,[status(thm)],[t1724]) ).
cnf(t17,axiom,
sF4 = add(additive_inverse(multiply(x,y)),additive_inverse(multiply(x,z))),
introduced(definition) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t52,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t1740,plain,
sF4 = add(additive_inverse(multiply(x,z)),additive_inverse(multiply(x,y))),
inference(step,[status(thm)],[t17,t52]) ).
cnf(t1741,plain,
sF4 = add(additive_inverse(sF2),additive_inverse(multiply(x,y))),
inference(step,[status(thm)],[t1740,t30]) ).
cnf(t1742,plain,
sF4 = add(sF3,additive_inverse(multiply(x,y))),
inference(step,[status(thm)],[t1741,t47]) ).
cnf(t1743,plain,
sF4 = add(sF3,additive_inverse(sF0)),
inference(step,[status(thm)],[t1742,t29]) ).
cnf(t1744,plain,
sF4 = add(sF3,sF1),
inference(step,[status(thm)],[t1743,t40]) ).
cnf(t1745,plain,
sF4 = add(sF1,sF3),
inference(step,[status(thm)],[t1744,t52]) ).
cnf(t206,plain,
add(sF1,sF3) = sF4,
inference(orient,[status(thm)],[t1745]) ).
cnf(t18,axiom,
sF5 = additive_inverse(x),
introduced(definition) ).
cnf(t21,plain,
additive_inverse(x) = sF5,
inference(orient,[status(thm)],[t18]) ).
cnf(t11,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t100,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t105,plain,
multiply(X1,add(X2,X3)) = add(multiply(X1,X3),multiply(X1,X2)),
inference(cp,[status(thm)],[t100,t52]) ).
cnf(t1791,plain,
multiply(X1,add(X2,X3)) = multiply(X1,add(X3,X2)),
inference(step,[status(thm)],[t105,t100]) ).
cnf(t714,plain,
multiply(X1,add(X2,X3)) = multiply(X1,add(X3,X2)),
inference(orient,[status(thm)],[t1791]) ).
cnf(t19,axiom,
sF6 = add(y,z),
introduced(definition) ).
cnf(t31,plain,
add(y,z) = sF6,
inference(orient,[status(thm)],[t19]) ).
cnf(t1725,plain,
add(z,y) = sF6,
inference(step,[status(thm)],[t31,t52]) ).
cnf(t53,plain,
add(z,y) = sF6,
inference(rw,[status(thm)],[t1725]) ).
cnf(t62,plain,
add(z,y) = sF6,
inference(orient,[status(thm)],[t53]) ).
cnf(t20,axiom,
sF7 = multiply(additive_inverse(x),add(y,z)),
introduced(definition) ).
cnf(t1746,plain,
sF7 = multiply(sF5,add(y,z)),
inference(step,[status(thm)],[t20,t21]) ).
cnf(t1747,plain,
sF7 = multiply(sF5,add(z,y)),
inference(step,[status(thm)],[t1746,t52]) ).
cnf(t1748,plain,
sF7 = multiply(sF5,sF6),
inference(step,[status(thm)],[t1747,t62]) ).
cnf(t227,plain,
multiply(sF5,sF6) = sF7,
inference(orient,[status(thm)],[t1748]) ).
cnf(t8,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t64,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t5,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t66,plain,
add(X1,add(additive_inverse(X1),X2)) = add(additive_identity,X2),
inference(cp,[status(thm)],[t64,t32]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t1757,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t66,t23]) ).
cnf(t316,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t1757]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t317,plain,
X1 = add(additive_inverse(X2),add(X2,X1)),
inference(cp,[status(thm)],[t316,t24]) ).
cnf(t69,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(cp,[status(thm)],[t64,t52]) ).
cnf(t355,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(orient,[status(thm)],[t69]) ).
cnf(t1828,plain,
X1 = add(X2,add(X1,additive_inverse(X2))),
inference(step,[status(thm)],[t317,t355]) ).
cnf(t1603,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(orient,[status(thm)],[t1828]) ).
cnf(t12,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t149,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t231,plain,
multiply(add(sF5,X1),sF6) = add(sF7,multiply(X1,sF6)),
inference(cp,[status(thm)],[t149,t227]) ).
cnf(t502,plain,
add(sF7,multiply(X1,sF6)) = multiply(add(sF5,X1),sF6),
inference(orient,[status(thm)],[t231]) ).
cnf(t49,plain,
additive_identity = add(sF2,sF3),
inference(cp,[status(thm)],[t32,t47]) ).
cnf(t60,plain,
add(sF2,sF3) = additive_identity,
inference(orient,[status(thm)],[t49]) ).
cnf(t71,plain,
add(sF2,add(sF3,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t64,t60]) ).
cnf(t1728,plain,
add(sF2,add(sF3,X1)) = X1,
inference(step,[status(thm)],[t71,t23]) ).
cnf(t86,plain,
add(sF2,add(sF3,X1)) = X1,
inference(orient,[status(thm)],[t1728]) ).
cnf(t42,plain,
additive_identity = add(sF0,sF1),
inference(cp,[status(thm)],[t32,t40]) ).
cnf(t45,plain,
add(sF0,sF1) = additive_identity,
inference(orient,[status(thm)],[t42]) ).
cnf(t68,plain,
add(sF0,add(sF1,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t64,t45]) ).
cnf(t1727,plain,
add(sF0,add(sF1,X1)) = X1,
inference(step,[status(thm)],[t68,t23]) ).
cnf(t83,plain,
add(sF0,add(sF1,X1)) = X1,
inference(orient,[status(thm)],[t1727]) ).
cnf(t209,plain,
sF3 = add(sF0,sF4),
inference(cp,[status(thm)],[t83,t206]) ).
cnf(t211,plain,
add(sF0,sF4) = sF3,
inference(orient,[status(thm)],[t209]) ).
cnf(t213,plain,
add(sF0,add(sF4,X1)) = add(sF3,X1),
inference(cp,[status(thm)],[t64,t211]) ).
cnf(t409,plain,
add(sF0,add(sF4,X1)) = add(sF3,X1),
inference(orient,[status(thm)],[t213]) ).
cnf(t410,plain,
add(sF3,additive_inverse(sF4)) = add(sF0,additive_identity),
inference(cp,[status(thm)],[t409,t32]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t1758,plain,
add(sF3,additive_inverse(sF4)) = sF0,
inference(step,[status(thm)],[t410,t22]) ).
cnf(t418,plain,
add(sF3,additive_inverse(sF4)) = sF0,
inference(orient,[status(thm)],[t1758]) ).
cnf(t420,plain,
additive_inverse(sF4) = add(sF2,sF0),
inference(cp,[status(thm)],[t86,t418]) ).
cnf(t1759,plain,
additive_inverse(sF4) = add(sF0,sF2),
inference(step,[status(thm)],[t420,t52]) ).
cnf(t103,plain,
multiply(x,add(z,X1)) = add(sF2,multiply(x,X1)),
inference(cp,[status(thm)],[t100,t30]) ).
cnf(t184,plain,
add(sF2,multiply(x,X1)) = multiply(x,add(z,X1)),
inference(orient,[status(thm)],[t103]) ).
cnf(t185,plain,
multiply(x,add(z,y)) = add(sF2,sF0),
inference(cp,[status(thm)],[t184,t29]) ).
cnf(t1736,plain,
multiply(x,sF6) = add(sF2,sF0),
inference(step,[status(thm)],[t185,t62]) ).
cnf(t1737,plain,
multiply(x,sF6) = add(sF0,sF2),
inference(step,[status(thm)],[t1736,t52]) ).
cnf(t191,plain,
add(sF0,sF2) = multiply(x,sF6),
inference(orient,[status(thm)],[t1737]) ).
cnf(t1760,plain,
additive_inverse(sF4) = multiply(x,sF6),
inference(step,[status(thm)],[t1759,t191]) ).
cnf(t424,plain,
multiply(x,sF6) = additive_inverse(sF4),
inference(orient,[status(thm)],[t1760]) ).
cnf(t507,plain,
multiply(add(sF5,x),sF6) = add(sF7,additive_inverse(sF4)),
inference(cp,[status(thm)],[t502,t424]) ).
cnf(t25,plain,
x = additive_inverse(sF5),
inference(cp,[status(thm)],[t24,t21]) ).
cnf(t26,plain,
additive_inverse(sF5) = x,
inference(orient,[status(thm)],[t25]) ).
cnf(t35,plain,
additive_identity = add(sF5,x),
inference(cp,[status(thm)],[t32,t26]) ).
cnf(t38,plain,
add(sF5,x) = additive_identity,
inference(orient,[status(thm)],[t35]) ).
cnf(t1768,plain,
multiply(additive_identity,sF6) = add(sF7,additive_inverse(sF4)),
inference(step,[status(thm)],[t507,t38]) ).
cnf(t4,axiom,
multiply(additive_identity,X1) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t4]) ).
cnf(t1769,plain,
additive_identity = add(sF7,additive_inverse(sF4)),
inference(step,[status(thm)],[t1768,t28]) ).
cnf(t512,plain,
add(sF7,additive_inverse(sF4)) = additive_identity,
inference(orient,[status(thm)],[t1769]) ).
cnf(t1615,plain,
sF7 = add(sF4,additive_identity),
inference(cp,[status(thm)],[t1603,t512]) ).
cnf(t1829,plain,
sF7 = sF4,
inference(step,[status(thm)],[t1615,t22]) ).
cnf(t1710,plain,
sF7 = sF4,
inference(orient,[status(thm)],[t1829]) ).
cnf(t1830,plain,
multiply(sF5,sF6) = sF4,
inference(step,[status(thm)],[t227,t1710]) ).
cnf(t1711,plain,
multiply(sF5,sF6) = sF4,
inference(orient,[status(thm)],[t1830]) ).
cnf(goal_0,negated_conjecture,
add(additive_inverse(multiply(x,y)),additive_inverse(multiply(x,z))) != multiply(additive_inverse(x),add(y,z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
add(additive_inverse(sF0),additive_inverse(multiply(x,z))) != multiply(additive_inverse(x),add(y,z)),
inference(rw,[status(thm)],[goal_0,t29]) ).
cnf(g0_1,plain,
add(sF1,additive_inverse(multiply(x,z))) != multiply(additive_inverse(x),add(y,z)),
inference(rw,[status(thm)],[g0_0,t40]) ).
cnf(g0_2,plain,
add(sF1,additive_inverse(sF2)) != multiply(additive_inverse(x),add(y,z)),
inference(rw,[status(thm)],[g0_1,t30]) ).
cnf(g0_3,plain,
add(sF1,sF3) != multiply(additive_inverse(x),add(y,z)),
inference(rw,[status(thm)],[g0_2,t47]) ).
cnf(g0_4,plain,
sF4 != multiply(additive_inverse(x),add(y,z)),
inference(rw,[status(thm)],[g0_3,t206]) ).
cnf(g0_5,plain,
sF4 != multiply(sF5,add(y,z)),
inference(rw,[status(thm)],[g0_4,t21]) ).
cnf(g0_6,plain,
sF4 != multiply(sF5,add(z,y)),
inference(rw,[status(thm)],[g0_5,t714]) ).
cnf(g0_7,plain,
sF4 != multiply(sF5,sF6),
inference(rw,[status(thm)],[g0_6,t62]) ).
cnf(g0_8,plain,
sF4 != sF4,
inference(rw,[status(thm)],[g0_7,t1711]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG017-6 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n007.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 07:44:22 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.25/1.29 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.25/1.29 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------