%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG018-6 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.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:29 PM UTC 2026
% Result : Unsatisfiable 3.12s 0.86s
% Output : CNFRefutation 3.12s
% 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,z),
introduced(definition) ).
cnf(t29,plain,
multiply(x,z) = sF0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sF1 = additive_inverse(multiply(x,z)),
introduced(definition) ).
cnf(t1606,plain,
sF1 = additive_inverse(sF0),
inference(step,[status(thm)],[t14,t29]) ).
cnf(t40,plain,
additive_inverse(sF0) = sF1,
inference(orient,[status(thm)],[t1606]) ).
cnf(t15,axiom,
sF2 = multiply(y,z),
introduced(definition) ).
cnf(t30,plain,
multiply(y,z) = sF2,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sF3 = additive_inverse(multiply(y,z)),
introduced(definition) ).
cnf(t1607,plain,
sF3 = additive_inverse(sF2),
inference(step,[status(thm)],[t16,t30]) ).
cnf(t47,plain,
additive_inverse(sF2) = sF3,
inference(orient,[status(thm)],[t1607]) ).
cnf(t17,axiom,
sF4 = add(additive_inverse(multiply(x,z)),additive_inverse(multiply(y,z))),
introduced(definition) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t52,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t1621,plain,
sF4 = add(additive_inverse(multiply(y,z)),additive_inverse(multiply(x,z))),
inference(step,[status(thm)],[t17,t52]) ).
cnf(t1622,plain,
sF4 = add(additive_inverse(sF2),additive_inverse(multiply(x,z))),
inference(step,[status(thm)],[t1621,t30]) ).
cnf(t1623,plain,
sF4 = add(sF3,additive_inverse(multiply(x,z))),
inference(step,[status(thm)],[t1622,t47]) ).
cnf(t1624,plain,
sF4 = add(sF3,additive_inverse(sF0)),
inference(step,[status(thm)],[t1623,t29]) ).
cnf(t1625,plain,
sF4 = add(sF3,sF1),
inference(step,[status(thm)],[t1624,t40]) ).
cnf(t1626,plain,
sF4 = add(sF1,sF3),
inference(step,[status(thm)],[t1625,t52]) ).
cnf(t202,plain,
add(sF1,sF3) = sF4,
inference(orient,[status(thm)],[t1626]) ).
cnf(t19,axiom,
sF6 = additive_inverse(z),
introduced(definition) ).
cnf(t21,plain,
additive_inverse(z) = sF6,
inference(orient,[status(thm)],[t19]) ).
cnf(t12,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t149,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t154,plain,
multiply(add(X1,X2),X3) = add(multiply(X2,X3),multiply(X1,X3)),
inference(cp,[status(thm)],[t149,t52]) ).
cnf(t1704,plain,
multiply(add(X1,X2),X3) = multiply(add(X2,X1),X3),
inference(step,[status(thm)],[t154,t149]) ).
cnf(t1405,plain,
multiply(add(X1,X2),X3) = multiply(add(X2,X1),X3),
inference(orient,[status(thm)],[t1704]) ).
cnf(t18,axiom,
sF5 = add(x,y),
introduced(definition) ).
cnf(t31,plain,
add(x,y) = sF5,
inference(orient,[status(thm)],[t18]) ).
cnf(t1608,plain,
add(y,x) = sF5,
inference(step,[status(thm)],[t31,t52]) ).
cnf(t53,plain,
add(y,x) = sF5,
inference(rw,[status(thm)],[t1608]) ).
cnf(t62,plain,
add(y,x) = sF5,
inference(orient,[status(thm)],[t53]) ).
cnf(t20,axiom,
sF7 = multiply(add(x,y),additive_inverse(z)),
introduced(definition) ).
cnf(t1627,plain,
sF7 = multiply(add(y,x),additive_inverse(z)),
inference(step,[status(thm)],[t20,t52]) ).
cnf(t1628,plain,
sF7 = multiply(sF5,additive_inverse(z)),
inference(step,[status(thm)],[t1627,t62]) ).
cnf(t1629,plain,
sF7 = multiply(sF5,sF6),
inference(step,[status(thm)],[t1628,t21]) ).
cnf(t218,plain,
multiply(sF5,sF6) = sF7,
inference(orient,[status(thm)],[t1629]) ).
cnf(t8,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t1640,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t66,t23]) ).
cnf(t312,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t1640]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t313,plain,
X1 = add(additive_inverse(X2),add(X2,X1)),
inference(cp,[status(thm)],[t312,t24]) ).
cnf(t69,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(cp,[status(thm)],[t64,t52]) ).
cnf(t343,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(orient,[status(thm)],[t69]) ).
cnf(t1705,plain,
X1 = add(X2,add(X1,additive_inverse(X2))),
inference(step,[status(thm)],[t313,t343]) ).
cnf(t1557,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(orient,[status(thm)],[t1705]) ).
cnf(t11,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t100,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t220,plain,
multiply(sF5,add(sF6,X1)) = add(sF7,multiply(sF5,X1)),
inference(cp,[status(thm)],[t100,t218]) ).
cnf(t427,plain,
add(sF7,multiply(sF5,X1)) = multiply(sF5,add(sF6,X1)),
inference(orient,[status(thm)],[t220]) ).
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(t1611,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)],[t1611]) ).
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(t1610,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)],[t1610]) ).
cnf(t205,plain,
sF3 = add(sF0,sF4),
inference(cp,[status(thm)],[t83,t202]) ).
cnf(t207,plain,
add(sF0,sF4) = sF3,
inference(orient,[status(thm)],[t205]) ).
cnf(t209,plain,
add(sF0,add(sF4,X1)) = add(sF3,X1),
inference(cp,[status(thm)],[t64,t207]) ).
cnf(t331,plain,
add(sF0,add(sF4,X1)) = add(sF3,X1),
inference(orient,[status(thm)],[t209]) ).
cnf(t332,plain,
add(sF3,additive_inverse(sF4)) = add(sF0,additive_identity),
inference(cp,[status(thm)],[t331,t32]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t1641,plain,
add(sF3,additive_inverse(sF4)) = sF0,
inference(step,[status(thm)],[t332,t22]) ).
cnf(t338,plain,
add(sF3,additive_inverse(sF4)) = sF0,
inference(orient,[status(thm)],[t1641]) ).
cnf(t340,plain,
additive_inverse(sF4) = add(sF2,sF0),
inference(cp,[status(thm)],[t86,t338]) ).
cnf(t1642,plain,
additive_inverse(sF4) = add(sF0,sF2),
inference(step,[status(thm)],[t340,t52]) ).
cnf(t152,plain,
multiply(add(y,X1),z) = add(sF2,multiply(X1,z)),
inference(cp,[status(thm)],[t149,t30]) ).
cnf(t245,plain,
add(sF2,multiply(X1,z)) = multiply(add(y,X1),z),
inference(orient,[status(thm)],[t152]) ).
cnf(t246,plain,
multiply(add(y,x),z) = add(sF2,sF0),
inference(cp,[status(thm)],[t245,t29]) ).
cnf(t1633,plain,
multiply(sF5,z) = add(sF2,sF0),
inference(step,[status(thm)],[t246,t62]) ).
cnf(t1634,plain,
multiply(sF5,z) = add(sF0,sF2),
inference(step,[status(thm)],[t1633,t52]) ).
cnf(t253,plain,
add(sF0,sF2) = multiply(sF5,z),
inference(orient,[status(thm)],[t1634]) ).
cnf(t1643,plain,
additive_inverse(sF4) = multiply(sF5,z),
inference(step,[status(thm)],[t1642,t253]) ).
cnf(t399,plain,
multiply(sF5,z) = additive_inverse(sF4),
inference(orient,[status(thm)],[t1643]) ).
cnf(t430,plain,
multiply(sF5,add(sF6,z)) = add(sF7,additive_inverse(sF4)),
inference(cp,[status(thm)],[t427,t399]) ).
cnf(t25,plain,
z = additive_inverse(sF6),
inference(cp,[status(thm)],[t24,t21]) ).
cnf(t26,plain,
additive_inverse(sF6) = z,
inference(orient,[status(thm)],[t25]) ).
cnf(t35,plain,
additive_identity = add(sF6,z),
inference(cp,[status(thm)],[t32,t26]) ).
cnf(t38,plain,
add(sF6,z) = additive_identity,
inference(orient,[status(thm)],[t35]) ).
cnf(t1647,plain,
multiply(sF5,additive_identity) = add(sF7,additive_inverse(sF4)),
inference(step,[status(thm)],[t430,t38]) ).
cnf(t3,axiom,
multiply(X1,additive_identity) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
multiply(X1,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t3]) ).
cnf(t1648,plain,
additive_identity = add(sF7,additive_inverse(sF4)),
inference(step,[status(thm)],[t1647,t27]) ).
cnf(t435,plain,
add(sF7,additive_inverse(sF4)) = additive_identity,
inference(orient,[status(thm)],[t1648]) ).
cnf(t1569,plain,
sF7 = add(sF4,additive_identity),
inference(cp,[status(thm)],[t1557,t435]) ).
cnf(t1706,plain,
sF7 = sF4,
inference(step,[status(thm)],[t1569,t22]) ).
cnf(t1593,plain,
sF7 = sF4,
inference(orient,[status(thm)],[t1706]) ).
cnf(t1707,plain,
multiply(sF5,sF6) = sF4,
inference(step,[status(thm)],[t218,t1593]) ).
cnf(t1594,plain,
multiply(sF5,sF6) = sF4,
inference(orient,[status(thm)],[t1707]) ).
cnf(goal_0,negated_conjecture,
add(additive_inverse(multiply(x,z)),additive_inverse(multiply(y,z))) != multiply(add(x,y),additive_inverse(z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
add(additive_inverse(sF0),additive_inverse(multiply(y,z))) != multiply(add(x,y),additive_inverse(z)),
inference(rw,[status(thm)],[goal_0,t29]) ).
cnf(g0_1,plain,
add(sF1,additive_inverse(multiply(y,z))) != multiply(add(x,y),additive_inverse(z)),
inference(rw,[status(thm)],[g0_0,t40]) ).
cnf(g0_2,plain,
add(sF1,additive_inverse(sF2)) != multiply(add(x,y),additive_inverse(z)),
inference(rw,[status(thm)],[g0_1,t30]) ).
cnf(g0_3,plain,
add(sF1,sF3) != multiply(add(x,y),additive_inverse(z)),
inference(rw,[status(thm)],[g0_2,t47]) ).
cnf(g0_4,plain,
sF4 != multiply(add(x,y),additive_inverse(z)),
inference(rw,[status(thm)],[g0_3,t202]) ).
cnf(g0_5,plain,
sF4 != multiply(add(x,y),sF6),
inference(rw,[status(thm)],[g0_4,t21]) ).
cnf(g0_6,plain,
sF4 != multiply(add(y,x),sF6),
inference(rw,[status(thm)],[g0_5,t1405]) ).
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,t1594]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG018-6 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n015.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 07:49:40 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 3.12/0.86 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.12/0.86 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------