%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG020-7 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.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 9.00s 6.86s
% Output : CNFRefutation 9.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 31
% Syntax : Number of clauses : 281 ( 281 unt; 0 nHn; 207 RR)
% Number of literals : 281 ( 280 equ; 33 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 25 con; 0-3 aty)
% Number of variables : 102 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t11,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t67,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t20,axiom,
sF0 = multiply(x,u),
introduced(definition) ).
cnf(t45,plain,
multiply(x,u) = sF0,
inference(orient,[status(thm)],[t20]) ).
cnf(t21,axiom,
sF1 = multiply(multiply(x,u),y),
introduced(definition) ).
cnf(t5771,plain,
sF1 = multiply(sF0,y),
inference(step,[status(thm)],[t21,t45]) ).
cnf(t92,plain,
multiply(sF0,y) = sF1,
inference(orient,[status(thm)],[t5771]) ).
cnf(t8,axiom,
multiply(X1,additive_inverse(X2)) = additive_inverse(multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t54,plain,
additive_inverse(multiply(X1,X2)) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t22,axiom,
sF2 = multiply(u,y),
introduced(definition) ).
cnf(t46,plain,
multiply(u,y) = sF2,
inference(orient,[status(thm)],[t22]) ).
cnf(t56,plain,
multiply(u,additive_inverse(y)) = additive_inverse(sF2),
inference(cp,[status(thm)],[t54,t46]) ).
cnf(t64,plain,
multiply(u,additive_inverse(y)) = additive_inverse(sF2),
inference(orient,[status(thm)],[t56]) ).
cnf(t23,axiom,
sF3 = multiply(x,multiply(u,y)),
introduced(definition) ).
cnf(t5772,plain,
sF3 = multiply(x,sF2),
inference(step,[status(thm)],[t23,t46]) ).
cnf(t96,plain,
multiply(x,sF2) = sF3,
inference(orient,[status(thm)],[t5772]) ).
cnf(t97,plain,
multiply(x,additive_inverse(sF2)) = additive_inverse(sF3),
inference(cp,[status(thm)],[t54,t96]) ).
cnf(t99,plain,
multiply(x,additive_inverse(sF2)) = additive_inverse(sF3),
inference(orient,[status(thm)],[t97]) ).
cnf(t24,axiom,
sF4 = additive_inverse(multiply(x,multiply(u,y))),
introduced(definition) ).
cnf(t5823,plain,
sF4 = multiply(x,additive_inverse(multiply(u,y))),
inference(step,[status(thm)],[t24,t54]) ).
cnf(t5824,plain,
sF4 = multiply(x,multiply(u,additive_inverse(y))),
inference(step,[status(thm)],[t5823,t54]) ).
cnf(t5825,plain,
sF4 = multiply(x,additive_inverse(sF2)),
inference(step,[status(thm)],[t5824,t64]) ).
cnf(t5826,plain,
sF4 = additive_inverse(sF3),
inference(step,[status(thm)],[t5825,t99]) ).
cnf(t641,plain,
additive_inverse(sF3) = sF4,
inference(orient,[status(thm)],[t5826]) ).
cnf(t5827,plain,
multiply(x,additive_inverse(sF2)) = sF4,
inference(step,[status(thm)],[t99,t641]) ).
cnf(t642,plain,
multiply(x,additive_inverse(sF2)) = sF4,
inference(orient,[status(thm)],[t5827]) ).
cnf(t25,axiom,
sF5 = add(multiply(multiply(x,u),y),additive_inverse(multiply(x,multiply(u,y)))),
introduced(definition) ).
cnf(t5831,plain,
sF5 = add(multiply(sF0,y),additive_inverse(multiply(x,multiply(u,y)))),
inference(step,[status(thm)],[t25,t45]) ).
cnf(t5832,plain,
sF5 = add(sF1,additive_inverse(multiply(x,multiply(u,y)))),
inference(step,[status(thm)],[t5831,t92]) ).
cnf(t5833,plain,
sF5 = add(sF1,multiply(x,additive_inverse(multiply(u,y)))),
inference(step,[status(thm)],[t5832,t54]) ).
cnf(t5834,plain,
sF5 = add(sF1,multiply(x,multiply(u,additive_inverse(y)))),
inference(step,[status(thm)],[t5833,t54]) ).
cnf(t5835,plain,
sF5 = add(sF1,multiply(x,additive_inverse(sF2))),
inference(step,[status(thm)],[t5834,t64]) ).
cnf(t5836,plain,
sF5 = add(sF1,sF4),
inference(step,[status(thm)],[t5835,t642]) ).
cnf(t703,plain,
add(sF1,sF4) = sF5,
inference(orient,[status(thm)],[t5836]) ).
cnf(t705,plain,
add(sF1,add(sF4,X1)) = add(sF5,X1),
inference(cp,[status(thm)],[t67,t703]) ).
cnf(t1578,plain,
add(sF1,add(sF4,X1)) = add(sF5,X1),
inference(orient,[status(thm)],[t705]) ).
cnf(t26,axiom,
sF6 = multiply(x,v),
introduced(definition) ).
cnf(t47,plain,
multiply(x,v) = sF6,
inference(orient,[status(thm)],[t26]) ).
cnf(t27,axiom,
sF7 = multiply(multiply(x,v),y),
introduced(definition) ).
cnf(t5773,plain,
sF7 = multiply(sF6,y),
inference(step,[status(thm)],[t27,t47]) ).
cnf(t130,plain,
multiply(sF6,y) = sF7,
inference(orient,[status(thm)],[t5773]) ).
cnf(t15,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t169,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t193,plain,
multiply(add(sF0,X1),y) = add(sF1,multiply(X1,y)),
inference(cp,[status(thm)],[t169,t92]) ).
cnf(t628,plain,
add(sF1,multiply(X1,y)) = multiply(add(sF0,X1),y),
inference(orient,[status(thm)],[t193]) ).
cnf(t635,plain,
multiply(add(sF0,sF6),y) = add(sF1,sF7),
inference(cp,[status(thm)],[t628,t130]) ).
cnf(t14,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)],[t14]) ).
cnf(t105,plain,
multiply(x,add(v,X1)) = add(sF6,multiply(x,X1)),
inference(cp,[status(thm)],[t100,t47]) ).
cnf(t298,plain,
add(sF6,multiply(x,X1)) = multiply(x,add(v,X1)),
inference(orient,[status(thm)],[t105]) ).
cnf(t299,plain,
multiply(x,add(v,u)) = add(sF6,sF0),
inference(cp,[status(thm)],[t298,t45]) ).
cnf(t33,axiom,
sF13 = add(u,v),
introduced(definition) ).
cnf(t49,plain,
add(u,v) = sF13,
inference(orient,[status(thm)],[t33]) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t72,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t5770,plain,
add(v,u) = sF13,
inference(step,[status(thm)],[t49,t72]) ).
cnf(t73,plain,
add(v,u) = sF13,
inference(rw,[status(thm)],[t5770]) ).
cnf(t78,plain,
add(v,u) = sF13,
inference(orient,[status(thm)],[t73]) ).
cnf(t5784,plain,
multiply(x,sF13) = add(sF6,sF0),
inference(step,[status(thm)],[t299,t78]) ).
cnf(t34,axiom,
sF14 = multiply(x,add(u,v)),
introduced(definition) ).
cnf(t5775,plain,
sF14 = multiply(x,add(v,u)),
inference(step,[status(thm)],[t34,t72]) ).
cnf(t5776,plain,
sF14 = multiply(x,sF13),
inference(step,[status(thm)],[t5775,t78]) ).
cnf(t146,plain,
multiply(x,sF13) = sF14,
inference(orient,[status(thm)],[t5776]) ).
cnf(t5785,plain,
sF14 = add(sF6,sF0),
inference(step,[status(thm)],[t5784,t146]) ).
cnf(t5786,plain,
sF14 = add(sF0,sF6),
inference(step,[status(thm)],[t5785,t72]) ).
cnf(t314,plain,
add(sF0,sF6) = sF14,
inference(orient,[status(thm)],[t5786]) ).
cnf(t5822,plain,
multiply(sF14,y) = add(sF1,sF7),
inference(step,[status(thm)],[t635,t314]) ).
cnf(t638,plain,
add(sF1,sF7) = multiply(sF14,y),
inference(orient,[status(thm)],[t5822]) ).
cnf(t640,plain,
add(sF1,add(sF7,X1)) = add(multiply(sF14,y),X1),
inference(cp,[status(thm)],[t67,t638]) ).
cnf(t35,axiom,
sF15 = multiply(multiply(x,add(u,v)),y),
introduced(definition) ).
cnf(t102,plain,
multiply(x,add(X1,u)) = add(multiply(x,X1),sF0),
inference(cp,[status(thm)],[t100,t45]) ).
cnf(t5780,plain,
multiply(x,add(X1,u)) = add(sF0,multiply(x,X1)),
inference(step,[status(thm)],[t102,t72]) ).
cnf(t101,plain,
multiply(x,add(u,X1)) = add(sF0,multiply(x,X1)),
inference(cp,[status(thm)],[t100,t45]) ).
cnf(t261,plain,
add(sF0,multiply(x,X1)) = multiply(x,add(u,X1)),
inference(orient,[status(thm)],[t101]) ).
cnf(t5781,plain,
multiply(x,add(X1,u)) = multiply(x,add(u,X1)),
inference(step,[status(thm)],[t5780,t261]) ).
cnf(t276,plain,
multiply(x,add(X1,u)) = multiply(x,add(u,X1)),
inference(orient,[status(thm)],[t5781]) ).
cnf(t5881,plain,
sF15 = multiply(multiply(x,add(v,u)),y),
inference(step,[status(thm)],[t35,t276]) ).
cnf(t5882,plain,
sF15 = multiply(multiply(x,sF13),y),
inference(step,[status(thm)],[t5881,t78]) ).
cnf(t5883,plain,
sF15 = multiply(sF14,y),
inference(step,[status(thm)],[t5882,t146]) ).
cnf(t985,plain,
multiply(sF14,y) = sF15,
inference(orient,[status(thm)],[t5883]) ).
cnf(t5925,plain,
add(sF1,add(sF7,X1)) = add(sF15,X1),
inference(step,[status(thm)],[t640,t985]) ).
cnf(t1463,plain,
add(sF1,add(sF7,X1)) = add(sF15,X1),
inference(orient,[status(thm)],[t5925]) ).
cnf(t1466,plain,
add(sF15,X1) = add(sF1,add(X1,sF7)),
inference(cp,[status(thm)],[t1463,t72]) ).
cnf(t2730,plain,
add(sF1,add(X1,sF7)) = add(sF15,X1),
inference(orient,[status(thm)],[t1466]) ).
cnf(t2734,plain,
add(sF15,sF4) = add(sF5,sF7),
inference(cp,[status(thm)],[t2730,t1578]) ).
cnf(t6010,plain,
add(sF4,sF15) = add(sF5,sF7),
inference(step,[status(thm)],[t2734,t72]) ).
cnf(t2738,plain,
add(sF5,sF7) = add(sF4,sF15),
inference(orient,[status(thm)],[t6010]) ).
cnf(t2740,plain,
add(sF5,add(sF7,X1)) = add(add(sF4,sF15),X1),
inference(cp,[status(thm)],[t67,t2738]) ).
cnf(t6156,plain,
add(sF5,add(sF7,X1)) = add(sF4,add(sF15,X1)),
inference(step,[status(thm)],[t2740,t67]) ).
cnf(t5082,plain,
add(sF5,add(sF7,X1)) = add(sF4,add(sF15,X1)),
inference(orient,[status(thm)],[t6156]) ).
cnf(t28,axiom,
sF8 = multiply(v,y),
introduced(definition) ).
cnf(t48,plain,
multiply(v,y) = sF8,
inference(orient,[status(thm)],[t28]) ).
cnf(t58,plain,
multiply(v,additive_inverse(y)) = additive_inverse(sF8),
inference(cp,[status(thm)],[t54,t48]) ).
cnf(t66,plain,
multiply(v,additive_inverse(y)) = additive_inverse(sF8),
inference(orient,[status(thm)],[t58]) ).
cnf(t29,axiom,
sF9 = multiply(x,multiply(v,y)),
introduced(definition) ).
cnf(t5774,plain,
sF9 = multiply(x,sF8),
inference(step,[status(thm)],[t29,t48]) ).
cnf(t138,plain,
multiply(x,sF8) = sF9,
inference(orient,[status(thm)],[t5774]) ).
cnf(t139,plain,
multiply(x,additive_inverse(sF8)) = additive_inverse(sF9),
inference(cp,[status(thm)],[t54,t138]) ).
cnf(t143,plain,
multiply(x,additive_inverse(sF8)) = additive_inverse(sF9),
inference(orient,[status(thm)],[t139]) ).
cnf(t30,axiom,
sF10 = additive_inverse(multiply(x,multiply(v,y))),
introduced(definition) ).
cnf(t5847,plain,
sF10 = multiply(x,additive_inverse(multiply(v,y))),
inference(step,[status(thm)],[t30,t54]) ).
cnf(t5848,plain,
sF10 = multiply(x,multiply(v,additive_inverse(y))),
inference(step,[status(thm)],[t5847,t54]) ).
cnf(t5849,plain,
sF10 = multiply(x,additive_inverse(sF8)),
inference(step,[status(thm)],[t5848,t66]) ).
cnf(t5850,plain,
sF10 = additive_inverse(sF9),
inference(step,[status(thm)],[t5849,t143]) ).
cnf(t769,plain,
additive_inverse(sF9) = sF10,
inference(orient,[status(thm)],[t5850]) ).
cnf(t5851,plain,
multiply(x,additive_inverse(sF8)) = sF10,
inference(step,[status(thm)],[t143,t769]) ).
cnf(t770,plain,
multiply(x,additive_inverse(sF8)) = sF10,
inference(orient,[status(thm)],[t5851]) ).
cnf(t31,axiom,
sF11 = add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))),
introduced(definition) ).
cnf(t5853,plain,
sF11 = add(multiply(sF6,y),additive_inverse(multiply(x,multiply(v,y)))),
inference(step,[status(thm)],[t31,t47]) ).
cnf(t5854,plain,
sF11 = add(sF7,additive_inverse(multiply(x,multiply(v,y)))),
inference(step,[status(thm)],[t5853,t130]) ).
cnf(t5855,plain,
sF11 = add(sF7,multiply(x,additive_inverse(multiply(v,y)))),
inference(step,[status(thm)],[t5854,t54]) ).
cnf(t5856,plain,
sF11 = add(sF7,multiply(x,multiply(v,additive_inverse(y)))),
inference(step,[status(thm)],[t5855,t54]) ).
cnf(t5857,plain,
sF11 = add(sF7,multiply(x,additive_inverse(sF8))),
inference(step,[status(thm)],[t5856,t66]) ).
cnf(t5858,plain,
sF11 = add(sF7,sF10),
inference(step,[status(thm)],[t5857,t770]) ).
cnf(t843,plain,
add(sF7,sF10) = sF11,
inference(orient,[status(thm)],[t5858]) ).
cnf(t1468,plain,
add(sF15,sF10) = add(sF1,sF11),
inference(cp,[status(thm)],[t1463,t843]) ).
cnf(t5926,plain,
add(sF10,sF15) = add(sF1,sF11),
inference(step,[status(thm)],[t1468,t72]) ).
cnf(t1471,plain,
add(sF10,sF15) = add(sF1,sF11),
inference(orient,[status(thm)],[t5926]) ).
cnf(t76,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(cp,[status(thm)],[t72,t67]) ).
cnf(t1475,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(orient,[status(thm)],[t76]) ).
cnf(t1582,plain,
add(sF5,X1) = add(sF1,add(X1,sF4)),
inference(cp,[status(thm)],[t1578,t72]) ).
cnf(t2938,plain,
add(sF1,add(X1,sF4)) = add(sF5,X1),
inference(orient,[status(thm)],[t1582]) ).
cnf(t32,axiom,
sF12 = add(add(multiply(multiply(x,u),y),additive_inverse(multiply(x,multiply(u,y)))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y))))),
introduced(definition) ).
cnf(t5862,plain,
sF12 = add(multiply(multiply(x,u),y),add(additive_inverse(multiply(x,multiply(u,y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))),
inference(step,[status(thm)],[t32,t67]) ).
cnf(t5863,plain,
sF12 = add(multiply(sF0,y),add(additive_inverse(multiply(x,multiply(u,y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))),
inference(step,[status(thm)],[t5862,t45]) ).
cnf(t5864,plain,
sF12 = add(sF1,add(additive_inverse(multiply(x,multiply(u,y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))),
inference(step,[status(thm)],[t5863,t92]) ).
cnf(t5865,plain,
sF12 = add(sF1,add(multiply(x,additive_inverse(multiply(u,y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))),
inference(step,[status(thm)],[t5864,t54]) ).
cnf(t5866,plain,
sF12 = add(sF1,add(multiply(x,multiply(u,additive_inverse(y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))),
inference(step,[status(thm)],[t5865,t54]) ).
cnf(t5867,plain,
sF12 = add(sF1,add(multiply(x,additive_inverse(sF2)),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))),
inference(step,[status(thm)],[t5866,t64]) ).
cnf(t5868,plain,
sF12 = add(sF1,add(sF4,add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))),
inference(step,[status(thm)],[t5867,t642]) ).
cnf(t5869,plain,
sF12 = add(sF1,add(sF4,add(multiply(sF6,y),additive_inverse(multiply(x,multiply(v,y)))))),
inference(step,[status(thm)],[t5868,t47]) ).
cnf(t5870,plain,
sF12 = add(sF1,add(sF4,add(sF7,additive_inverse(multiply(x,multiply(v,y)))))),
inference(step,[status(thm)],[t5869,t130]) ).
cnf(t5871,plain,
sF12 = add(sF1,add(sF4,add(sF7,multiply(x,additive_inverse(multiply(v,y)))))),
inference(step,[status(thm)],[t5870,t54]) ).
cnf(t5872,plain,
sF12 = add(sF1,add(sF4,add(sF7,multiply(x,multiply(v,additive_inverse(y)))))),
inference(step,[status(thm)],[t5871,t54]) ).
cnf(t5873,plain,
sF12 = add(sF1,add(sF4,add(sF7,multiply(x,additive_inverse(sF8))))),
inference(step,[status(thm)],[t5872,t66]) ).
cnf(t5874,plain,
sF12 = add(sF1,add(sF4,add(sF7,sF10))),
inference(step,[status(thm)],[t5873,t770]) ).
cnf(t5875,plain,
sF12 = add(sF1,add(sF4,sF11)),
inference(step,[status(thm)],[t5874,t843]) ).
cnf(t913,plain,
add(sF1,add(sF4,sF11)) = sF12,
inference(orient,[status(thm)],[t5875]) ).
cnf(t5934,plain,
add(sF5,sF11) = sF12,
inference(step,[status(thm)],[t913,t1578]) ).
cnf(t1579,plain,
add(sF5,sF11) = sF12,
inference(rw,[status(thm)],[t5934]) ).
cnf(t1587,plain,
add(sF5,sF11) = sF12,
inference(orient,[status(thm)],[t1579]) ).
cnf(t183,plain,
multiply(add(X1,u),additive_inverse(y)) = add(multiply(X1,additive_inverse(y)),additive_inverse(sF2)),
inference(cp,[status(thm)],[t169,t64]) ).
cnf(t6153,plain,
multiply(add(X1,u),additive_inverse(y)) = add(additive_inverse(sF2),multiply(X1,additive_inverse(y))),
inference(step,[status(thm)],[t183,t72]) ).
cnf(t182,plain,
multiply(add(u,X1),additive_inverse(y)) = add(additive_inverse(sF2),multiply(X1,additive_inverse(y))),
inference(cp,[status(thm)],[t169,t64]) ).
cnf(t5009,plain,
add(additive_inverse(sF2),multiply(X1,additive_inverse(y))) = multiply(add(u,X1),additive_inverse(y)),
inference(orient,[status(thm)],[t182]) ).
cnf(t6154,plain,
multiply(add(X1,u),additive_inverse(y)) = multiply(add(u,X1),additive_inverse(y)),
inference(step,[status(thm)],[t6153,t5009]) ).
cnf(t5051,plain,
multiply(add(X1,u),additive_inverse(y)) = multiply(add(u,X1),additive_inverse(y)),
inference(orient,[status(thm)],[t6154]) ).
cnf(t36,axiom,
sF16 = multiply(add(u,v),y),
introduced(definition) ).
cnf(t5777,plain,
sF16 = multiply(add(v,u),y),
inference(step,[status(thm)],[t36,t72]) ).
cnf(t5778,plain,
sF16 = multiply(sF13,y),
inference(step,[status(thm)],[t5777,t78]) ).
cnf(t154,plain,
multiply(sF13,y) = sF16,
inference(orient,[status(thm)],[t5778]) ).
cnf(t155,plain,
multiply(sF13,additive_inverse(y)) = additive_inverse(sF16),
inference(cp,[status(thm)],[t54,t154]) ).
cnf(t159,plain,
multiply(sF13,additive_inverse(y)) = additive_inverse(sF16),
inference(orient,[status(thm)],[t155]) ).
cnf(t37,axiom,
sF17 = multiply(x,multiply(add(u,v),y)),
introduced(definition) ).
cnf(t173,plain,
multiply(add(X1,u),y) = add(multiply(X1,y),sF2),
inference(cp,[status(thm)],[t169,t46]) ).
cnf(t5813,plain,
multiply(add(X1,u),y) = add(sF2,multiply(X1,y)),
inference(step,[status(thm)],[t173,t72]) ).
cnf(t172,plain,
multiply(add(u,X1),y) = add(sF2,multiply(X1,y)),
inference(cp,[status(thm)],[t169,t46]) ).
cnf(t578,plain,
add(sF2,multiply(X1,y)) = multiply(add(u,X1),y),
inference(orient,[status(thm)],[t172]) ).
cnf(t5814,plain,
multiply(add(X1,u),y) = multiply(add(u,X1),y),
inference(step,[status(thm)],[t5813,t578]) ).
cnf(t588,plain,
multiply(add(X1,u),y) = multiply(add(u,X1),y),
inference(orient,[status(thm)],[t5814]) ).
cnf(t5887,plain,
sF17 = multiply(x,multiply(add(v,u),y)),
inference(step,[status(thm)],[t37,t588]) ).
cnf(t5888,plain,
sF17 = multiply(x,multiply(sF13,y)),
inference(step,[status(thm)],[t5887,t78]) ).
cnf(t5889,plain,
sF17 = multiply(x,sF16),
inference(step,[status(thm)],[t5888,t154]) ).
cnf(t1030,plain,
multiply(x,sF16) = sF17,
inference(orient,[status(thm)],[t5889]) ).
cnf(t1033,plain,
multiply(x,additive_inverse(sF16)) = additive_inverse(sF17),
inference(cp,[status(thm)],[t54,t1030]) ).
cnf(t1045,plain,
multiply(x,additive_inverse(sF16)) = additive_inverse(sF17),
inference(orient,[status(thm)],[t1033]) ).
cnf(t38,axiom,
sF18 = additive_inverse(multiply(x,multiply(add(u,v),y))),
introduced(definition) ).
cnf(t5892,plain,
sF18 = multiply(x,additive_inverse(multiply(add(u,v),y))),
inference(step,[status(thm)],[t38,t54]) ).
cnf(t5893,plain,
sF18 = multiply(x,multiply(add(u,v),additive_inverse(y))),
inference(step,[status(thm)],[t5892,t54]) ).
cnf(t5894,plain,
sF18 = multiply(x,multiply(add(v,u),additive_inverse(y))),
inference(step,[status(thm)],[t5893,t72]) ).
cnf(t5895,plain,
sF18 = multiply(x,multiply(sF13,additive_inverse(y))),
inference(step,[status(thm)],[t5894,t78]) ).
cnf(t5896,plain,
sF18 = multiply(x,additive_inverse(sF16)),
inference(step,[status(thm)],[t5895,t159]) ).
cnf(t5897,plain,
sF18 = additive_inverse(sF17),
inference(step,[status(thm)],[t5896,t1045]) ).
cnf(t1103,plain,
additive_inverse(sF17) = sF18,
inference(orient,[status(thm)],[t5897]) ).
cnf(t5898,plain,
multiply(x,additive_inverse(sF16)) = sF18,
inference(step,[status(thm)],[t1045,t1103]) ).
cnf(t1104,plain,
multiply(x,additive_inverse(sF16)) = sF18,
inference(orient,[status(thm)],[t5898]) ).
cnf(t39,axiom,
sF19 = add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
introduced(definition) ).
cnf(t5900,plain,
sF19 = add(multiply(multiply(x,add(v,u)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(step,[status(thm)],[t39,t276]) ).
cnf(t5901,plain,
sF19 = add(multiply(multiply(x,sF13),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(step,[status(thm)],[t5900,t78]) ).
cnf(t5902,plain,
sF19 = add(multiply(sF14,y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(step,[status(thm)],[t5901,t146]) ).
cnf(t5903,plain,
sF19 = add(sF15,additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(step,[status(thm)],[t5902,t985]) ).
cnf(t5904,plain,
sF19 = add(sF15,multiply(x,additive_inverse(multiply(add(u,v),y)))),
inference(step,[status(thm)],[t5903,t54]) ).
cnf(t5905,plain,
sF19 = add(sF15,multiply(x,multiply(add(u,v),additive_inverse(y)))),
inference(step,[status(thm)],[t5904,t54]) ).
cnf(t5906,plain,
sF19 = add(sF15,multiply(x,multiply(add(v,u),additive_inverse(y)))),
inference(step,[status(thm)],[t5905,t72]) ).
cnf(t5907,plain,
sF19 = add(sF15,multiply(x,multiply(sF13,additive_inverse(y)))),
inference(step,[status(thm)],[t5906,t78]) ).
cnf(t5908,plain,
sF19 = add(sF15,multiply(x,additive_inverse(sF16))),
inference(step,[status(thm)],[t5907,t159]) ).
cnf(t5909,plain,
sF19 = add(sF15,sF18),
inference(step,[status(thm)],[t5908,t1104]) ).
cnf(t1180,plain,
add(sF15,sF18) = sF19,
inference(orient,[status(thm)],[t5909]) ).
cnf(t125,plain,
multiply(x,add(sF2,X1)) = add(sF3,multiply(x,X1)),
inference(cp,[status(thm)],[t100,t96]) ).
cnf(t351,plain,
add(sF3,multiply(x,X1)) = multiply(x,add(sF2,X1)),
inference(orient,[status(thm)],[t125]) ).
cnf(t358,plain,
multiply(x,add(sF2,sF8)) = add(sF3,sF9),
inference(cp,[status(thm)],[t351,t138]) ).
cnf(t176,plain,
multiply(add(v,X1),y) = add(sF8,multiply(X1,y)),
inference(cp,[status(thm)],[t169,t48]) ).
cnf(t607,plain,
add(sF8,multiply(X1,y)) = multiply(add(v,X1),y),
inference(orient,[status(thm)],[t176]) ).
cnf(t608,plain,
multiply(add(v,u),y) = add(sF8,sF2),
inference(cp,[status(thm)],[t607,t46]) ).
cnf(t5817,plain,
multiply(sF13,y) = add(sF8,sF2),
inference(step,[status(thm)],[t608,t78]) ).
cnf(t5818,plain,
sF16 = add(sF8,sF2),
inference(step,[status(thm)],[t5817,t154]) ).
cnf(t5819,plain,
sF16 = add(sF2,sF8),
inference(step,[status(thm)],[t5818,t72]) ).
cnf(t617,plain,
add(sF2,sF8) = sF16,
inference(orient,[status(thm)],[t5819]) ).
cnf(t5886,plain,
multiply(x,sF16) = add(sF3,sF9),
inference(step,[status(thm)],[t358,t617]) ).
cnf(t1027,plain,
add(sF3,sF9) = multiply(x,sF16),
inference(orient,[status(thm)],[t5886]) ).
cnf(t1029,plain,
add(sF3,add(sF9,X1)) = add(multiply(x,sF16),X1),
inference(cp,[status(thm)],[t67,t1027]) ).
cnf(t5968,plain,
add(sF3,add(sF9,X1)) = add(sF17,X1),
inference(step,[status(thm)],[t1029,t1030]) ).
cnf(t2240,plain,
add(sF3,add(sF9,X1)) = add(sF17,X1),
inference(orient,[status(thm)],[t5968]) ).
cnf(t77,plain,
add(X1,add(X2,X3)) = add(add(X2,X1),X3),
inference(cp,[status(thm)],[t67,t72]) ).
cnf(t5935,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(step,[status(thm)],[t77,t67]) ).
cnf(t1592,plain,
add(X1,add(X2,X3)) = add(X2,add(X1,X3)),
inference(orient,[status(thm)],[t5935]) ).
cnf(t1648,plain,
add(sF5,add(X1,sF11)) = add(X1,sF12),
inference(cp,[status(thm)],[t1592,t1587]) ).
cnf(t3408,plain,
add(sF5,add(X1,sF11)) = add(X1,sF12),
inference(orient,[status(thm)],[t1648]) ).
cnf(t845,plain,
add(sF7,add(sF10,X1)) = add(sF11,X1),
inference(cp,[status(thm)],[t67,t843]) ).
cnf(t1905,plain,
add(sF7,add(sF10,X1)) = add(sF11,X1),
inference(orient,[status(thm)],[t845]) ).
cnf(t5,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t50,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t1906,plain,
add(sF11,additive_inverse(sF10)) = add(sF7,additive_identity),
inference(cp,[status(thm)],[t1905,t50]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t42,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t772,plain,
sF9 = additive_inverse(sF10),
inference(cp,[status(thm)],[t42,t769]) ).
cnf(t780,plain,
additive_inverse(sF10) = sF9,
inference(orient,[status(thm)],[t772]) ).
cnf(t5952,plain,
add(sF11,sF9) = add(sF7,additive_identity),
inference(step,[status(thm)],[t1906,t780]) ).
cnf(t5953,plain,
add(sF9,sF11) = add(sF7,additive_identity),
inference(step,[status(thm)],[t5952,t72]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t40,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t5954,plain,
add(sF9,sF11) = sF7,
inference(step,[status(thm)],[t5953,t40]) ).
cnf(t1917,plain,
add(sF9,sF11) = sF7,
inference(orient,[status(thm)],[t5954]) ).
cnf(t3412,plain,
add(sF9,sF12) = add(sF5,sF7),
inference(cp,[status(thm)],[t3408,t1917]) ).
cnf(t6035,plain,
add(sF9,sF12) = add(sF4,sF15),
inference(step,[status(thm)],[t3412,t2738]) ).
cnf(t3416,plain,
add(sF9,sF12) = add(sF4,sF15),
inference(orient,[status(thm)],[t6035]) ).
cnf(t3422,plain,
add(sF17,sF12) = add(sF3,add(sF4,sF15)),
inference(cp,[status(thm)],[t2240,t3416]) ).
cnf(t6038,plain,
add(sF12,sF17) = add(sF3,add(sF4,sF15)),
inference(step,[status(thm)],[t3422,t72]) ).
cnf(t645,plain,
additive_identity = add(sF3,sF4),
inference(cp,[status(thm)],[t50,t641]) ).
cnf(t656,plain,
add(sF3,sF4) = additive_identity,
inference(orient,[status(thm)],[t645]) ).
cnf(t657,plain,
add(sF3,add(sF4,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t67,t656]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t41,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t5928,plain,
add(sF3,add(sF4,X1)) = X1,
inference(step,[status(thm)],[t657,t41]) ).
cnf(t1534,plain,
add(sF3,add(sF4,X1)) = X1,
inference(orient,[status(thm)],[t5928]) ).
cnf(t6039,plain,
add(sF12,sF17) = sF15,
inference(step,[status(thm)],[t6038,t1534]) ).
cnf(t3445,plain,
add(sF12,sF17) = sF15,
inference(orient,[status(thm)],[t6039]) ).
cnf(t3447,plain,
add(sF12,add(sF17,X1)) = add(sF15,X1),
inference(cp,[status(thm)],[t67,t3445]) ).
cnf(t5735,plain,
add(sF12,add(sF17,X1)) = add(sF15,X1),
inference(orient,[status(thm)],[t3447]) ).
cnf(t5736,plain,
add(sF15,additive_inverse(sF17)) = add(sF12,additive_identity),
inference(cp,[status(thm)],[t5735,t50]) ).
cnf(t6166,plain,
add(sF15,sF18) = add(sF12,additive_identity),
inference(step,[status(thm)],[t5736,t1103]) ).
cnf(t6167,plain,
sF19 = add(sF12,additive_identity),
inference(step,[status(thm)],[t6166,t1180]) ).
cnf(t6168,plain,
sF19 = sF12,
inference(step,[status(thm)],[t6167,t40]) ).
cnf(t5752,plain,
sF19 = sF12,
inference(orient,[status(thm)],[t6168]) ).
cnf(t6169,plain,
add(sF15,sF18) = sF12,
inference(step,[status(thm)],[t1180,t5752]) ).
cnf(t5753,plain,
add(sF15,sF18) = sF12,
inference(orient,[status(thm)],[t6169]) ).
cnf(u0,negated_conjecture,
associator(x,add(u,v),y) != add(associator(x,u,y),associator(x,v,y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
associator(X,Y,Z) = add(multiply(multiply(X,Y),Z),additive_inverse(multiply(X,multiply(Y,Z)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
add(add(multiply(multiply(x,u),y),additive_inverse(multiply(x,multiply(u,y)))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
add(multiply(multiply(x,u),y),add(additive_inverse(multiply(x,multiply(u,y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[goal_0,t67]) ).
cnf(g0_1,plain,
add(multiply(sF0,y),add(additive_inverse(multiply(x,multiply(u,y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_0,t45]) ).
cnf(g0_2,plain,
add(sF1,add(additive_inverse(multiply(x,multiply(u,y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_1,t92]) ).
cnf(g0_3,plain,
add(sF1,add(multiply(x,additive_inverse(multiply(u,y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_2,t54]) ).
cnf(g0_4,plain,
add(sF1,add(multiply(x,multiply(u,additive_inverse(y))),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_3,t54]) ).
cnf(g0_5,plain,
add(sF1,add(multiply(x,additive_inverse(sF2)),add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_4,t64]) ).
cnf(g0_6,plain,
add(sF1,add(sF4,add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y)))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_5,t642]) ).
cnf(g0_7,plain,
add(sF5,add(multiply(multiply(x,v),y),additive_inverse(multiply(x,multiply(v,y))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_6,t1578]) ).
cnf(g0_8,plain,
add(sF5,add(multiply(sF6,y),additive_inverse(multiply(x,multiply(v,y))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_7,t47]) ).
cnf(g0_9,plain,
add(sF5,add(sF7,additive_inverse(multiply(x,multiply(v,y))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_8,t130]) ).
cnf(g0_10,plain,
add(sF4,add(sF15,additive_inverse(multiply(x,multiply(v,y))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_9,t5082]) ).
cnf(g0_11,plain,
add(sF4,add(sF15,multiply(x,additive_inverse(multiply(v,y))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_10,t54]) ).
cnf(g0_12,plain,
add(sF4,add(sF15,multiply(x,multiply(v,additive_inverse(y))))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_11,t54]) ).
cnf(g0_13,plain,
add(sF4,add(sF15,multiply(x,additive_inverse(sF8)))) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_12,t66]) ).
cnf(g0_14,plain,
add(sF4,add(sF15,sF10)) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_13,t770]) ).
cnf(g0_15,plain,
add(sF4,add(sF10,sF15)) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_14,t72]) ).
cnf(g0_16,plain,
add(sF4,add(sF1,sF11)) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_15,t1471]) ).
cnf(g0_17,plain,
add(sF1,add(sF11,sF4)) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_16,t1475]) ).
cnf(g0_18,plain,
add(sF5,sF11) != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_17,t2938]) ).
cnf(g0_19,plain,
sF12 != add(multiply(multiply(x,add(u,v)),y),additive_inverse(multiply(x,multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_18,t1587]) ).
cnf(g0_20,plain,
sF12 != add(multiply(multiply(x,add(u,v)),y),multiply(x,additive_inverse(multiply(add(u,v),y)))),
inference(rw,[status(thm)],[g0_19,t54]) ).
cnf(g0_21,plain,
sF12 != add(multiply(multiply(x,add(u,v)),y),multiply(x,multiply(add(u,v),additive_inverse(y)))),
inference(rw,[status(thm)],[g0_20,t54]) ).
cnf(g0_22,plain,
sF12 != add(multiply(multiply(x,add(v,u)),y),multiply(x,multiply(add(u,v),additive_inverse(y)))),
inference(rw,[status(thm)],[g0_21,t276]) ).
cnf(g0_23,plain,
sF12 != add(multiply(multiply(x,sF13),y),multiply(x,multiply(add(u,v),additive_inverse(y)))),
inference(rw,[status(thm)],[g0_22,t78]) ).
cnf(g0_24,plain,
sF12 != add(multiply(sF14,y),multiply(x,multiply(add(u,v),additive_inverse(y)))),
inference(rw,[status(thm)],[g0_23,t146]) ).
cnf(g0_25,plain,
sF12 != add(sF15,multiply(x,multiply(add(u,v),additive_inverse(y)))),
inference(rw,[status(thm)],[g0_24,t985]) ).
cnf(g0_26,plain,
sF12 != add(sF15,multiply(x,multiply(add(v,u),additive_inverse(y)))),
inference(rw,[status(thm)],[g0_25,t5051]) ).
cnf(g0_27,plain,
sF12 != add(sF15,multiply(x,multiply(sF13,additive_inverse(y)))),
inference(rw,[status(thm)],[g0_26,t78]) ).
cnf(g0_28,plain,
sF12 != add(sF15,multiply(x,additive_inverse(sF16))),
inference(rw,[status(thm)],[g0_27,t159]) ).
cnf(g0_29,plain,
sF12 != add(sF15,sF18),
inference(rw,[status(thm)],[g0_28,t1104]) ).
cnf(g0_30,plain,
sF12 != sF12,
inference(rw,[status(thm)],[g0_29,t5753]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG020-7 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.37 % Computer : n016.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Thu Sep 24 07:51:50 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.00/6.86 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.00/6.86 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------