%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG015-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 : n014.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 0.15s 11.05s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 15
% Syntax : Number of clauses : 107 ( 107 unt; 0 nHn; 65 RR)
% Number of literals : 107 ( 106 equ; 9 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 : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 64 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t13,axiom,
sFlat0 = multiply(x,y),
introduced(definition) ).
cnf(t52,plain,
multiply(x,y) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sFlat1 = multiply(x,z),
introduced(definition) ).
cnf(t46,plain,
multiply(x,z) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sFlat2 = additive_inverse(multiply(x,z)),
introduced(definition) ).
cnf(t788,plain,
sFlat2 = additive_inverse(sFlat1),
inference(step,[status(thm)],[t15,t46]) ).
cnf(t76,plain,
additive_inverse(sFlat1) = sFlat2,
inference(orient,[status(thm)],[t788]) ).
cnf(t16,axiom,
sFlat3 = add(multiply(x,y),additive_inverse(multiply(x,z))),
introduced(definition) ).
cnf(t785,plain,
sFlat3 = add(sFlat0,additive_inverse(multiply(x,z))),
inference(step,[status(thm)],[t16,t52]) ).
cnf(t786,plain,
sFlat3 = add(sFlat0,additive_inverse(sFlat1)),
inference(step,[status(thm)],[t785,t46]) ).
cnf(t71,plain,
add(sFlat0,additive_inverse(sFlat1)) = sFlat3,
inference(orient,[status(thm)],[t786]) ).
cnf(t789,plain,
add(sFlat0,sFlat2) = sFlat3,
inference(step,[status(thm)],[t71,t76]) ).
cnf(t79,plain,
add(sFlat0,sFlat2) = sFlat3,
inference(rw,[status(thm)],[t789]) ).
cnf(t97,plain,
add(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t79]) ).
cnf(t17,axiom,
sFlat4 = additive_inverse(z),
introduced(definition) ).
cnf(t80,plain,
additive_inverse(z) = sFlat4,
inference(orient,[status(thm)],[t17]) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t58,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t18,axiom,
sFlat5 = add(y,additive_inverse(z)),
introduced(definition) ).
cnf(t73,plain,
add(y,additive_inverse(z)) = sFlat5,
inference(orient,[status(thm)],[t18]) ).
cnf(t790,plain,
add(y,sFlat4) = sFlat5,
inference(step,[status(thm)],[t73,t80]) ).
cnf(t83,plain,
add(y,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t790]) ).
cnf(t792,plain,
add(sFlat4,y) = sFlat5,
inference(step,[status(thm)],[t83,t58]) ).
cnf(t101,plain,
add(sFlat4,y) = sFlat5,
inference(orient,[status(thm)],[t792]) ).
cnf(t19,axiom,
sFlat6 = multiply(x,add(y,additive_inverse(z))),
introduced(definition) ).
cnf(t40,plain,
multiply(x,add(y,additive_inverse(z))) = sFlat6,
inference(orient,[status(thm)],[t19]) ).
cnf(t787,plain,
multiply(x,sFlat5) = sFlat6,
inference(step,[status(thm)],[t40,t73]) ).
cnf(t75,plain,
multiply(x,sFlat5) = sFlat6,
inference(rw,[status(thm)],[t787]) ).
cnf(t89,plain,
multiply(x,sFlat5) = sFlat6,
inference(orient,[status(thm)],[t75]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t8,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t61,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(t66,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t70,plain,
add(X1,add(additive_inverse(X1),X2)) = add(additive_identity,X2),
inference(cp,[status(thm)],[t61,t66]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t797,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t70,t21]) ).
cnf(t171,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t797]) ).
cnf(t175,plain,
X1 = add(X2,add(X1,additive_inverse(X2))),
inference(cp,[status(thm)],[t171,t58]) ).
cnf(t296,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(orient,[status(thm)],[t175]) ).
cnf(t303,plain,
X1 = add(additive_inverse(X2),add(X1,X2)),
inference(cp,[status(thm)],[t296,t22]) ).
cnf(t357,plain,
add(additive_inverse(X1),add(X2,X1)) = X2,
inference(orient,[status(thm)],[t303]) ).
cnf(t393,plain,
additive_inverse(X1) = add(additive_inverse(add(X2,X1)),X2),
inference(cp,[status(thm)],[t357,t357]) ).
cnf(t819,plain,
additive_inverse(X1) = add(X2,additive_inverse(add(X2,X1))),
inference(step,[status(thm)],[t393,t58]) ).
cnf(t688,plain,
add(X1,additive_inverse(add(X1,X2))) = additive_inverse(X2),
inference(orient,[status(thm)],[t819]) ).
cnf(t11,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t49,plain,
multiply(x,add(z,X1)) = add(sFlat1,multiply(x,X1)),
inference(cp,[status(thm)],[t28,t46]) ).
cnf(t743,plain,
add(sFlat1,multiply(x,X1)) = multiply(x,add(z,X1)),
inference(orient,[status(thm)],[t49]) ).
cnf(t749,plain,
multiply(x,add(z,sFlat5)) = add(sFlat1,sFlat6),
inference(cp,[status(thm)],[t743,t89]) ).
cnf(t821,plain,
multiply(x,add(sFlat5,z)) = add(sFlat1,sFlat6),
inference(step,[status(thm)],[t749,t58]) ).
cnf(t102,plain,
add(sFlat4,add(y,X1)) = add(sFlat5,X1),
inference(cp,[status(thm)],[t61,t101]) ).
cnf(t137,plain,
add(sFlat4,add(y,X1)) = add(sFlat5,X1),
inference(orient,[status(thm)],[t102]) ).
cnf(t82,plain,
additive_identity = add(z,sFlat4),
inference(cp,[status(thm)],[t66,t80]) ).
cnf(t791,plain,
additive_identity = add(sFlat4,z),
inference(step,[status(thm)],[t82,t58]) ).
cnf(t99,plain,
add(sFlat4,z) = additive_identity,
inference(orient,[status(thm)],[t791]) ).
cnf(t100,plain,
add(sFlat4,add(z,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t61,t99]) ).
cnf(t794,plain,
add(sFlat4,add(z,X1)) = X1,
inference(step,[status(thm)],[t100,t21]) ).
cnf(t105,plain,
add(sFlat4,add(z,X1)) = X1,
inference(orient,[status(thm)],[t794]) ).
cnf(t106,plain,
X1 = add(sFlat4,add(X1,z)),
inference(cp,[status(thm)],[t105,t58]) ).
cnf(t113,plain,
add(sFlat4,add(X1,z)) = X1,
inference(orient,[status(thm)],[t106]) ).
cnf(t138,plain,
add(sFlat5,z) = y,
inference(cp,[status(thm)],[t137,t113]) ).
cnf(t141,plain,
add(sFlat5,z) = y,
inference(orient,[status(thm)],[t138]) ).
cnf(t822,plain,
multiply(x,y) = add(sFlat1,sFlat6),
inference(step,[status(thm)],[t821,t141]) ).
cnf(t823,plain,
sFlat0 = add(sFlat1,sFlat6),
inference(step,[status(thm)],[t822,t52]) ).
cnf(t760,plain,
add(sFlat1,sFlat6) = sFlat0,
inference(orient,[status(thm)],[t823]) ).
cnf(t767,plain,
additive_inverse(sFlat6) = add(sFlat1,additive_inverse(sFlat0)),
inference(cp,[status(thm)],[t688,t760]) ).
cnf(t178,plain,
X1 = add(additive_inverse(X2),add(X2,X1)),
inference(cp,[status(thm)],[t171,t22]) ).
cnf(t314,plain,
add(additive_inverse(X1),add(X1,X2)) = X2,
inference(orient,[status(thm)],[t178]) ).
cnf(t78,plain,
additive_identity = add(sFlat1,sFlat2),
inference(cp,[status(thm)],[t66,t76]) ).
cnf(t95,plain,
add(sFlat1,sFlat2) = additive_identity,
inference(orient,[status(thm)],[t78]) ).
cnf(t96,plain,
add(sFlat1,add(sFlat2,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t61,t95]) ).
cnf(t793,plain,
add(sFlat1,add(sFlat2,X1)) = X1,
inference(step,[status(thm)],[t96,t21]) ).
cnf(t103,plain,
add(sFlat1,add(sFlat2,X1)) = X1,
inference(orient,[status(thm)],[t793]) ).
cnf(t104,plain,
X1 = add(sFlat1,add(X1,sFlat2)),
inference(cp,[status(thm)],[t103,t58]) ).
cnf(t107,plain,
add(sFlat1,add(X1,sFlat2)) = X1,
inference(orient,[status(thm)],[t104]) ).
cnf(t108,plain,
sFlat0 = add(sFlat1,sFlat3),
inference(cp,[status(thm)],[t107,t97]) ).
cnf(t111,plain,
add(sFlat1,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t108]) ).
cnf(t112,plain,
add(sFlat1,add(sFlat3,X1)) = add(sFlat0,X1),
inference(cp,[status(thm)],[t61,t111]) ).
cnf(t145,plain,
add(sFlat1,add(sFlat3,X1)) = add(sFlat0,X1),
inference(orient,[status(thm)],[t112]) ).
cnf(t146,plain,
add(sFlat0,additive_inverse(sFlat3)) = add(sFlat1,additive_identity),
inference(cp,[status(thm)],[t145,t66]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t796,plain,
add(sFlat0,additive_inverse(sFlat3)) = sFlat1,
inference(step,[status(thm)],[t146,t20]) ).
cnf(t148,plain,
add(sFlat0,additive_inverse(sFlat3)) = sFlat1,
inference(orient,[status(thm)],[t796]) ).
cnf(t334,plain,
additive_inverse(sFlat3) = add(additive_inverse(sFlat0),sFlat1),
inference(cp,[status(thm)],[t314,t148]) ).
cnf(t803,plain,
additive_inverse(sFlat3) = add(sFlat1,additive_inverse(sFlat0)),
inference(step,[status(thm)],[t334,t58]) ).
cnf(t355,plain,
add(sFlat1,additive_inverse(sFlat0)) = additive_inverse(sFlat3),
inference(orient,[status(thm)],[t803]) ).
cnf(t824,plain,
additive_inverse(sFlat6) = additive_inverse(sFlat3),
inference(step,[status(thm)],[t767,t355]) ).
cnf(t769,plain,
additive_inverse(sFlat6) = additive_inverse(sFlat3),
inference(orient,[status(thm)],[t824]) ).
cnf(t770,plain,
sFlat6 = additive_inverse(additive_inverse(sFlat3)),
inference(cp,[status(thm)],[t22,t769]) ).
cnf(t825,plain,
sFlat6 = sFlat3,
inference(step,[status(thm)],[t770,t22]) ).
cnf(t780,plain,
sFlat6 = sFlat3,
inference(orient,[status(thm)],[t825]) ).
cnf(t826,plain,
multiply(x,sFlat5) = sFlat3,
inference(step,[status(thm)],[t89,t780]) ).
cnf(t781,plain,
multiply(x,sFlat5) = sFlat3,
inference(orient,[status(thm)],[t826]) ).
cnf(goal_0,negated_conjecture,
add(multiply(x,y),additive_inverse(multiply(x,z))) != multiply(x,add(y,additive_inverse(z))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
add(sFlat0,additive_inverse(multiply(x,z))) != multiply(x,add(y,additive_inverse(z))),
inference(rw,[status(thm)],[goal_0,t52]) ).
cnf(g0_1,plain,
add(sFlat0,additive_inverse(sFlat1)) != multiply(x,add(y,additive_inverse(z))),
inference(rw,[status(thm)],[g0_0,t46]) ).
cnf(g0_2,plain,
add(sFlat0,sFlat2) != multiply(x,add(y,additive_inverse(z))),
inference(rw,[status(thm)],[g0_1,t76]) ).
cnf(g0_3,plain,
sFlat3 != multiply(x,add(y,additive_inverse(z))),
inference(rw,[status(thm)],[g0_2,t97]) ).
cnf(g0_4,plain,
sFlat3 != multiply(x,add(y,sFlat4)),
inference(rw,[status(thm)],[g0_3,t80]) ).
cnf(g0_5,plain,
sFlat3 != multiply(x,add(sFlat4,y)),
inference(rw,[status(thm)],[g0_4,t58]) ).
cnf(g0_6,plain,
sFlat3 != multiply(x,sFlat5),
inference(rw,[status(thm)],[g0_5,t101]) ).
cnf(g0_7,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_6,t781]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG015-6 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/10.39 % Computer : n014.cluster.edu
% 0.10/10.39 % Model : x86_64 x86_64
% 0.10/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.39 % Memory : 8046.5625MB
% 0.10/10.39 % OS : Linux 6.8.0-71-generic
% 0.10/10.39 % CPULimit : 300
% 0.10/10.39 % WCLimit : 300
% 0.10/10.39 % DateTime : Thu Sep 24 07:45:42 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.10/10.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.15/11.05 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/11.05 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------