%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG019-7 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.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.21s 1.85s
% Output : CNFRefutation 9.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 28
% Syntax : Number of clauses : 261 ( 261 unt; 0 nHn; 193 RR)
% Number of literals : 261 ( 260 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 : 27 ( 27 usr; 23 con; 0-3 aty)
% Number of variables : 89 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t11,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t62,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t20,axiom,
sF0 = multiply(x,y),
introduced(definition) ).
cnf(t43,plain,
multiply(x,y) = sF0,
inference(orient,[status(thm)],[t20]) ).
cnf(t21,axiom,
sF1 = multiply(multiply(x,y),u),
introduced(definition) ).
cnf(t4129,plain,
sF1 = multiply(sF0,u),
inference(step,[status(thm)],[t21,t43]) ).
cnf(t86,plain,
multiply(sF0,u) = sF1,
inference(orient,[status(thm)],[t4129]) ).
cnf(t8,axiom,
multiply(X1,additive_inverse(X2)) = additive_inverse(multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t51,plain,
additive_inverse(multiply(X1,X2)) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t22,axiom,
sF2 = multiply(y,u),
introduced(definition) ).
cnf(t44,plain,
multiply(y,u) = sF2,
inference(orient,[status(thm)],[t22]) ).
cnf(t53,plain,
multiply(y,additive_inverse(u)) = additive_inverse(sF2),
inference(cp,[status(thm)],[t51,t44]) ).
cnf(t60,plain,
multiply(y,additive_inverse(u)) = additive_inverse(sF2),
inference(orient,[status(thm)],[t53]) ).
cnf(t23,axiom,
sF3 = multiply(x,multiply(y,u)),
introduced(definition) ).
cnf(t4130,plain,
sF3 = multiply(x,sF2),
inference(step,[status(thm)],[t23,t44]) ).
cnf(t90,plain,
multiply(x,sF2) = sF3,
inference(orient,[status(thm)],[t4130]) ).
cnf(t91,plain,
multiply(x,additive_inverse(sF2)) = additive_inverse(sF3),
inference(cp,[status(thm)],[t51,t90]) ).
cnf(t93,plain,
multiply(x,additive_inverse(sF2)) = additive_inverse(sF3),
inference(orient,[status(thm)],[t91]) ).
cnf(t24,axiom,
sF4 = additive_inverse(multiply(x,multiply(y,u))),
introduced(definition) ).
cnf(t4182,plain,
sF4 = multiply(x,additive_inverse(multiply(y,u))),
inference(step,[status(thm)],[t24,t51]) ).
cnf(t4183,plain,
sF4 = multiply(x,multiply(y,additive_inverse(u))),
inference(step,[status(thm)],[t4182,t51]) ).
cnf(t4184,plain,
sF4 = multiply(x,additive_inverse(sF2)),
inference(step,[status(thm)],[t4183,t60]) ).
cnf(t4185,plain,
sF4 = additive_inverse(sF3),
inference(step,[status(thm)],[t4184,t93]) ).
cnf(t593,plain,
additive_inverse(sF3) = sF4,
inference(orient,[status(thm)],[t4185]) ).
cnf(t4186,plain,
multiply(x,additive_inverse(sF2)) = sF4,
inference(step,[status(thm)],[t93,t593]) ).
cnf(t594,plain,
multiply(x,additive_inverse(sF2)) = sF4,
inference(orient,[status(thm)],[t4186]) ).
cnf(t25,axiom,
sF5 = add(multiply(multiply(x,y),u),additive_inverse(multiply(x,multiply(y,u)))),
introduced(definition) ).
cnf(t4190,plain,
sF5 = add(multiply(sF0,u),additive_inverse(multiply(x,multiply(y,u)))),
inference(step,[status(thm)],[t25,t43]) ).
cnf(t4191,plain,
sF5 = add(sF1,additive_inverse(multiply(x,multiply(y,u)))),
inference(step,[status(thm)],[t4190,t86]) ).
cnf(t4192,plain,
sF5 = add(sF1,multiply(x,additive_inverse(multiply(y,u)))),
inference(step,[status(thm)],[t4191,t51]) ).
cnf(t4193,plain,
sF5 = add(sF1,multiply(x,multiply(y,additive_inverse(u)))),
inference(step,[status(thm)],[t4192,t51]) ).
cnf(t4194,plain,
sF5 = add(sF1,multiply(x,additive_inverse(sF2))),
inference(step,[status(thm)],[t4193,t60]) ).
cnf(t4195,plain,
sF5 = add(sF1,sF4),
inference(step,[status(thm)],[t4194,t594]) ).
cnf(t675,plain,
add(sF1,sF4) = sF5,
inference(orient,[status(thm)],[t4195]) ).
cnf(t677,plain,
add(sF1,add(sF4,X1)) = add(sF5,X1),
inference(cp,[status(thm)],[t62,t675]) ).
cnf(t1225,plain,
add(sF1,add(sF4,X1)) = add(sF5,X1),
inference(orient,[status(thm)],[t677]) ).
cnf(t26,axiom,
sF6 = multiply(multiply(x,y),v),
introduced(definition) ).
cnf(t4131,plain,
sF6 = multiply(sF0,v),
inference(step,[status(thm)],[t26,t43]) ).
cnf(t94,plain,
multiply(sF0,v) = sF6,
inference(orient,[status(thm)],[t4131]) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t77,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t1229,plain,
add(sF5,X1) = add(sF1,add(X1,sF4)),
inference(cp,[status(thm)],[t1225,t77]) ).
cnf(t2148,plain,
add(sF1,add(X1,sF4)) = add(sF5,X1),
inference(orient,[status(thm)],[t1229]) ).
cnf(t14,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t98,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t123,plain,
multiply(sF0,add(v,X1)) = add(sF6,multiply(sF0,X1)),
inference(cp,[status(thm)],[t98,t94]) ).
cnf(t332,plain,
add(sF6,multiply(sF0,X1)) = multiply(sF0,add(v,X1)),
inference(orient,[status(thm)],[t123]) ).
cnf(t334,plain,
multiply(sF0,add(v,u)) = add(sF6,sF1),
inference(cp,[status(thm)],[t332,t86]) ).
cnf(t32,axiom,
sF12 = add(u,v),
introduced(definition) ).
cnf(t46,plain,
add(u,v) = sF12,
inference(orient,[status(thm)],[t32]) ).
cnf(t4128,plain,
add(v,u) = sF12,
inference(step,[status(thm)],[t46,t77]) ).
cnf(t78,plain,
add(v,u) = sF12,
inference(rw,[status(thm)],[t4128]) ).
cnf(t83,plain,
add(v,u) = sF12,
inference(orient,[status(thm)],[t78]) ).
cnf(t4150,plain,
multiply(sF0,sF12) = add(sF6,sF1),
inference(step,[status(thm)],[t334,t83]) ).
cnf(t4151,plain,
multiply(sF0,sF12) = add(sF1,sF6),
inference(step,[status(thm)],[t4150,t77]) ).
cnf(t341,plain,
add(sF1,sF6) = multiply(sF0,sF12),
inference(orient,[status(thm)],[t4151]) ).
cnf(t343,plain,
add(sF1,add(sF6,X1)) = add(multiply(sF0,sF12),X1),
inference(cp,[status(thm)],[t62,t341]) ).
cnf(t858,plain,
add(multiply(sF0,sF12),X1) = add(sF1,add(sF6,X1)),
inference(orient,[status(thm)],[t343]) ).
cnf(t33,axiom,
sF13 = multiply(multiply(x,y),add(u,v)),
introduced(definition) ).
cnf(t4225,plain,
sF13 = multiply(sF0,add(u,v)),
inference(step,[status(thm)],[t33,t43]) ).
cnf(t116,plain,
multiply(sF0,add(X1,u)) = add(multiply(sF0,X1),sF1),
inference(cp,[status(thm)],[t98,t86]) ).
cnf(t4145,plain,
multiply(sF0,add(X1,u)) = add(sF1,multiply(sF0,X1)),
inference(step,[status(thm)],[t116,t77]) ).
cnf(t115,plain,
multiply(sF0,add(u,X1)) = add(sF1,multiply(sF0,X1)),
inference(cp,[status(thm)],[t98,t86]) ).
cnf(t294,plain,
add(sF1,multiply(sF0,X1)) = multiply(sF0,add(u,X1)),
inference(orient,[status(thm)],[t115]) ).
cnf(t4146,plain,
multiply(sF0,add(X1,u)) = multiply(sF0,add(u,X1)),
inference(step,[status(thm)],[t4145,t294]) ).
cnf(t302,plain,
multiply(sF0,add(X1,u)) = multiply(sF0,add(u,X1)),
inference(orient,[status(thm)],[t4146]) ).
cnf(t4226,plain,
sF13 = multiply(sF0,add(v,u)),
inference(step,[status(thm)],[t4225,t302]) ).
cnf(t4227,plain,
sF13 = multiply(sF0,sF12),
inference(step,[status(thm)],[t4226,t83]) ).
cnf(t892,plain,
multiply(sF0,sF12) = sF13,
inference(orient,[status(thm)],[t4227]) ).
cnf(t4230,plain,
add(sF13,X1) = add(sF1,add(sF6,X1)),
inference(step,[status(thm)],[t858,t892]) ).
cnf(t895,plain,
add(sF13,X1) = add(sF1,add(sF6,X1)),
inference(rw,[status(thm)],[t4230]) ).
cnf(t1395,plain,
add(sF1,add(sF6,X1)) = add(sF13,X1),
inference(orient,[status(thm)],[t895]) ).
cnf(t2152,plain,
add(sF5,sF6) = add(sF13,sF4),
inference(cp,[status(thm)],[t2148,t1395]) ).
cnf(t4344,plain,
add(sF5,sF6) = add(sF4,sF13),
inference(step,[status(thm)],[t2152,t77]) ).
cnf(t2156,plain,
add(sF5,sF6) = add(sF4,sF13),
inference(orient,[status(thm)],[t4344]) ).
cnf(t2158,plain,
add(sF5,add(sF6,X1)) = add(add(sF4,sF13),X1),
inference(cp,[status(thm)],[t62,t2156]) ).
cnf(t4480,plain,
add(sF5,add(sF6,X1)) = add(sF4,add(sF13,X1)),
inference(step,[status(thm)],[t2158,t62]) ).
cnf(t4017,plain,
add(sF5,add(sF6,X1)) = add(sF4,add(sF13,X1)),
inference(orient,[status(thm)],[t4480]) ).
cnf(t27,axiom,
sF7 = multiply(y,v),
introduced(definition) ).
cnf(t45,plain,
multiply(y,v) = sF7,
inference(orient,[status(thm)],[t27]) ).
cnf(t54,plain,
multiply(y,additive_inverse(v)) = additive_inverse(sF7),
inference(cp,[status(thm)],[t51,t45]) ).
cnf(t61,plain,
multiply(y,additive_inverse(v)) = additive_inverse(sF7),
inference(orient,[status(thm)],[t54]) ).
cnf(t28,axiom,
sF8 = multiply(x,multiply(y,v)),
introduced(definition) ).
cnf(t4132,plain,
sF8 = multiply(x,sF7),
inference(step,[status(thm)],[t28,t45]) ).
cnf(t128,plain,
multiply(x,sF7) = sF8,
inference(orient,[status(thm)],[t4132]) ).
cnf(t129,plain,
multiply(x,additive_inverse(sF7)) = additive_inverse(sF8),
inference(cp,[status(thm)],[t51,t128]) ).
cnf(t133,plain,
multiply(x,additive_inverse(sF7)) = additive_inverse(sF8),
inference(orient,[status(thm)],[t129]) ).
cnf(t29,axiom,
sF9 = additive_inverse(multiply(x,multiply(y,v))),
introduced(definition) ).
cnf(t4199,plain,
sF9 = multiply(x,additive_inverse(multiply(y,v))),
inference(step,[status(thm)],[t29,t51]) ).
cnf(t4200,plain,
sF9 = multiply(x,multiply(y,additive_inverse(v))),
inference(step,[status(thm)],[t4199,t51]) ).
cnf(t4201,plain,
sF9 = multiply(x,additive_inverse(sF7)),
inference(step,[status(thm)],[t4200,t61]) ).
cnf(t4202,plain,
sF9 = additive_inverse(sF8),
inference(step,[status(thm)],[t4201,t133]) ).
cnf(t719,plain,
additive_inverse(sF8) = sF9,
inference(orient,[status(thm)],[t4202]) ).
cnf(t4203,plain,
multiply(x,additive_inverse(sF7)) = sF9,
inference(step,[status(thm)],[t133,t719]) ).
cnf(t720,plain,
multiply(x,additive_inverse(sF7)) = sF9,
inference(orient,[status(thm)],[t4203]) ).
cnf(t30,axiom,
sF10 = add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))),
introduced(definition) ).
cnf(t4205,plain,
sF10 = add(multiply(sF0,v),additive_inverse(multiply(x,multiply(y,v)))),
inference(step,[status(thm)],[t30,t43]) ).
cnf(t4206,plain,
sF10 = add(sF6,additive_inverse(multiply(x,multiply(y,v)))),
inference(step,[status(thm)],[t4205,t94]) ).
cnf(t4207,plain,
sF10 = add(sF6,multiply(x,additive_inverse(multiply(y,v)))),
inference(step,[status(thm)],[t4206,t51]) ).
cnf(t4208,plain,
sF10 = add(sF6,multiply(x,multiply(y,additive_inverse(v)))),
inference(step,[status(thm)],[t4207,t51]) ).
cnf(t4209,plain,
sF10 = add(sF6,multiply(x,additive_inverse(sF7))),
inference(step,[status(thm)],[t4208,t61]) ).
cnf(t4210,plain,
sF10 = add(sF6,sF9),
inference(step,[status(thm)],[t4209,t720]) ).
cnf(t785,plain,
add(sF6,sF9) = sF10,
inference(orient,[status(thm)],[t4210]) ).
cnf(t1401,plain,
add(sF13,sF9) = add(sF1,sF10),
inference(cp,[status(thm)],[t1395,t785]) ).
cnf(t4298,plain,
add(sF9,sF13) = add(sF1,sF10),
inference(step,[status(thm)],[t1401,t77]) ).
cnf(t1406,plain,
add(sF9,sF13) = add(sF1,sF10),
inference(orient,[status(thm)],[t4298]) ).
cnf(t81,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(cp,[status(thm)],[t77,t62]) ).
cnf(t1922,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(orient,[status(thm)],[t81]) ).
cnf(t31,axiom,
sF11 = add(add(multiply(multiply(x,y),u),additive_inverse(multiply(x,multiply(y,u)))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v))))),
introduced(definition) ).
cnf(t4211,plain,
sF11 = add(multiply(multiply(x,y),u),add(additive_inverse(multiply(x,multiply(y,u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t31,t62]) ).
cnf(t4212,plain,
sF11 = add(multiply(sF0,u),add(additive_inverse(multiply(x,multiply(y,u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t4211,t43]) ).
cnf(t4213,plain,
sF11 = add(sF1,add(additive_inverse(multiply(x,multiply(y,u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t4212,t86]) ).
cnf(t4214,plain,
sF11 = add(sF1,add(multiply(x,additive_inverse(multiply(y,u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t4213,t51]) ).
cnf(t4215,plain,
sF11 = add(sF1,add(multiply(x,multiply(y,additive_inverse(u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t4214,t51]) ).
cnf(t4216,plain,
sF11 = add(sF1,add(multiply(x,additive_inverse(sF2)),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t4215,t60]) ).
cnf(t4217,plain,
sF11 = add(sF1,add(sF4,add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t4216,t594]) ).
cnf(t4218,plain,
sF11 = add(sF1,add(sF4,add(multiply(sF0,v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t4217,t43]) ).
cnf(t4219,plain,
sF11 = add(sF1,add(sF4,add(sF6,additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t4218,t94]) ).
cnf(t4220,plain,
sF11 = add(sF1,add(sF4,add(sF6,multiply(x,additive_inverse(multiply(y,v)))))),
inference(step,[status(thm)],[t4219,t51]) ).
cnf(t4221,plain,
sF11 = add(sF1,add(sF4,add(sF6,multiply(x,multiply(y,additive_inverse(v)))))),
inference(step,[status(thm)],[t4220,t51]) ).
cnf(t4222,plain,
sF11 = add(sF1,add(sF4,add(sF6,multiply(x,additive_inverse(sF7))))),
inference(step,[status(thm)],[t4221,t61]) ).
cnf(t4223,plain,
sF11 = add(sF1,add(sF4,add(sF6,sF9))),
inference(step,[status(thm)],[t4222,t720]) ).
cnf(t4224,plain,
sF11 = add(sF1,add(sF4,sF10)),
inference(step,[status(thm)],[t4223,t785]) ).
cnf(t823,plain,
add(sF1,add(sF4,sF10)) = sF11,
inference(orient,[status(thm)],[t4224]) ).
cnf(t4271,plain,
add(sF5,sF10) = sF11,
inference(step,[status(thm)],[t823,t1225]) ).
cnf(t1226,plain,
add(sF5,sF10) = sF11,
inference(rw,[status(thm)],[t4271]) ).
cnf(t1230,plain,
add(sF5,sF10) = sF11,
inference(orient,[status(thm)],[t1226]) ).
cnf(t34,axiom,
sF14 = multiply(y,add(u,v)),
introduced(definition) ).
cnf(t4133,plain,
sF14 = multiply(y,add(v,u)),
inference(step,[status(thm)],[t34,t77]) ).
cnf(t4134,plain,
sF14 = multiply(y,sF12),
inference(step,[status(thm)],[t4133,t83]) ).
cnf(t136,plain,
multiply(y,sF12) = sF14,
inference(orient,[status(thm)],[t4134]) ).
cnf(t137,plain,
multiply(y,additive_inverse(sF12)) = additive_inverse(sF14),
inference(cp,[status(thm)],[t51,t136]) ).
cnf(t141,plain,
multiply(y,additive_inverse(sF12)) = additive_inverse(sF14),
inference(orient,[status(thm)],[t137]) ).
cnf(t35,axiom,
sF15 = multiply(x,multiply(y,add(u,v))),
introduced(definition) ).
cnf(t102,plain,
multiply(y,add(X1,u)) = add(multiply(y,X1),sF2),
inference(cp,[status(thm)],[t98,t44]) ).
cnf(t4138,plain,
multiply(y,add(X1,u)) = add(sF2,multiply(y,X1)),
inference(step,[status(thm)],[t102,t77]) ).
cnf(t101,plain,
multiply(y,add(u,X1)) = add(sF2,multiply(y,X1)),
inference(cp,[status(thm)],[t98,t44]) ).
cnf(t253,plain,
add(sF2,multiply(y,X1)) = multiply(y,add(u,X1)),
inference(orient,[status(thm)],[t101]) ).
cnf(t4139,plain,
multiply(y,add(X1,u)) = multiply(y,add(u,X1)),
inference(step,[status(thm)],[t4138,t253]) ).
cnf(t263,plain,
multiply(y,add(X1,u)) = multiply(y,add(u,X1)),
inference(orient,[status(thm)],[t4139]) ).
cnf(t4235,plain,
sF15 = multiply(x,multiply(y,add(v,u))),
inference(step,[status(thm)],[t35,t263]) ).
cnf(t4236,plain,
sF15 = multiply(x,multiply(y,sF12)),
inference(step,[status(thm)],[t4235,t83]) ).
cnf(t4237,plain,
sF15 = multiply(x,sF14),
inference(step,[status(thm)],[t4236,t136]) ).
cnf(t935,plain,
multiply(x,sF14) = sF15,
inference(orient,[status(thm)],[t4237]) ).
cnf(t939,plain,
multiply(x,additive_inverse(sF14)) = additive_inverse(sF15),
inference(cp,[status(thm)],[t51,t935]) ).
cnf(t949,plain,
multiply(x,additive_inverse(sF14)) = additive_inverse(sF15),
inference(orient,[status(thm)],[t939]) ).
cnf(t36,axiom,
sF16 = additive_inverse(multiply(x,multiply(y,add(u,v)))),
introduced(definition) ).
cnf(t4243,plain,
sF16 = multiply(x,additive_inverse(multiply(y,add(u,v)))),
inference(step,[status(thm)],[t36,t51]) ).
cnf(t4244,plain,
sF16 = multiply(x,multiply(y,additive_inverse(add(u,v)))),
inference(step,[status(thm)],[t4243,t51]) ).
cnf(t4245,plain,
sF16 = multiply(x,multiply(y,additive_inverse(add(v,u)))),
inference(step,[status(thm)],[t4244,t77]) ).
cnf(t4246,plain,
sF16 = multiply(x,multiply(y,additive_inverse(sF12))),
inference(step,[status(thm)],[t4245,t83]) ).
cnf(t4247,plain,
sF16 = multiply(x,additive_inverse(sF14)),
inference(step,[status(thm)],[t4246,t141]) ).
cnf(t4248,plain,
sF16 = additive_inverse(sF15),
inference(step,[status(thm)],[t4247,t949]) ).
cnf(t995,plain,
additive_inverse(sF15) = sF16,
inference(orient,[status(thm)],[t4248]) ).
cnf(t4249,plain,
multiply(x,additive_inverse(sF14)) = sF16,
inference(step,[status(thm)],[t949,t995]) ).
cnf(t996,plain,
multiply(x,additive_inverse(sF14)) = sF16,
inference(orient,[status(thm)],[t4249]) ).
cnf(t37,axiom,
sF17 = add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
introduced(definition) ).
cnf(t4251,plain,
sF17 = add(multiply(sF0,add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(step,[status(thm)],[t37,t43]) ).
cnf(t4252,plain,
sF17 = add(multiply(sF0,add(v,u)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(step,[status(thm)],[t4251,t302]) ).
cnf(t4253,plain,
sF17 = add(multiply(sF0,sF12),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(step,[status(thm)],[t4252,t83]) ).
cnf(t4254,plain,
sF17 = add(sF13,additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(step,[status(thm)],[t4253,t892]) ).
cnf(t4255,plain,
sF17 = add(sF13,multiply(x,additive_inverse(multiply(y,add(u,v))))),
inference(step,[status(thm)],[t4254,t51]) ).
cnf(t4256,plain,
sF17 = add(sF13,multiply(x,multiply(y,additive_inverse(add(u,v))))),
inference(step,[status(thm)],[t4255,t51]) ).
cnf(t4257,plain,
sF17 = add(sF13,multiply(x,multiply(y,additive_inverse(add(v,u))))),
inference(step,[status(thm)],[t4256,t77]) ).
cnf(t4258,plain,
sF17 = add(sF13,multiply(x,multiply(y,additive_inverse(sF12)))),
inference(step,[status(thm)],[t4257,t83]) ).
cnf(t4259,plain,
sF17 = add(sF13,multiply(x,additive_inverse(sF14))),
inference(step,[status(thm)],[t4258,t141]) ).
cnf(t4260,plain,
sF17 = add(sF13,sF16),
inference(step,[status(thm)],[t4259,t996]) ).
cnf(t1072,plain,
add(sF13,sF16) = sF17,
inference(orient,[status(thm)],[t4260]) ).
cnf(t119,plain,
multiply(x,add(sF2,X1)) = add(sF3,multiply(x,X1)),
inference(cp,[status(thm)],[t98,t90]) ).
cnf(t311,plain,
add(sF3,multiply(x,X1)) = multiply(x,add(sF2,X1)),
inference(orient,[status(thm)],[t119]) ).
cnf(t316,plain,
multiply(x,add(sF2,sF7)) = add(sF3,sF8),
inference(cp,[status(thm)],[t311,t128]) ).
cnf(t103,plain,
multiply(y,add(v,X1)) = add(sF7,multiply(y,X1)),
inference(cp,[status(thm)],[t98,t45]) ).
cnf(t272,plain,
add(sF7,multiply(y,X1)) = multiply(y,add(v,X1)),
inference(orient,[status(thm)],[t103]) ).
cnf(t273,plain,
multiply(y,add(v,u)) = add(sF7,sF2),
inference(cp,[status(thm)],[t272,t44]) ).
cnf(t4140,plain,
multiply(y,sF12) = add(sF7,sF2),
inference(step,[status(thm)],[t273,t83]) ).
cnf(t4141,plain,
sF14 = add(sF7,sF2),
inference(step,[status(thm)],[t4140,t136]) ).
cnf(t4142,plain,
sF14 = add(sF2,sF7),
inference(step,[status(thm)],[t4141,t77]) ).
cnf(t283,plain,
add(sF2,sF7) = sF14,
inference(orient,[status(thm)],[t4142]) ).
cnf(t4147,plain,
multiply(x,sF14) = add(sF3,sF8),
inference(step,[status(thm)],[t316,t283]) ).
cnf(t321,plain,
add(sF3,sF8) = multiply(x,sF14),
inference(orient,[status(thm)],[t4147]) ).
cnf(t323,plain,
add(sF3,add(sF8,X1)) = add(multiply(x,sF14),X1),
inference(cp,[status(thm)],[t62,t321]) ).
cnf(t827,plain,
add(multiply(x,sF14),X1) = add(sF3,add(sF8,X1)),
inference(orient,[status(thm)],[t323]) ).
cnf(t4240,plain,
add(sF15,X1) = add(sF3,add(sF8,X1)),
inference(step,[status(thm)],[t827,t935]) ).
cnf(t938,plain,
add(sF15,X1) = add(sF3,add(sF8,X1)),
inference(rw,[status(thm)],[t4240]) ).
cnf(t1581,plain,
add(sF3,add(sF8,X1)) = add(sF15,X1),
inference(orient,[status(thm)],[t938]) ).
cnf(t787,plain,
add(sF6,add(sF9,X1)) = add(sF10,X1),
inference(cp,[status(thm)],[t62,t785]) ).
cnf(t1327,plain,
add(sF6,add(sF9,X1)) = add(sF10,X1),
inference(orient,[status(thm)],[t787]) ).
cnf(t5,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t47,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t65,plain,
add(X1,add(additive_inverse(X1),X2)) = add(additive_identity,X2),
inference(cp,[status(thm)],[t62,t47]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t39,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t4279,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t65,t39]) ).
cnf(t1278,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t4279]) ).
cnf(t1332,plain,
add(sF10,add(additive_inverse(sF9),X1)) = add(sF6,X1),
inference(cp,[status(thm)],[t1327,t1278]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t722,plain,
sF8 = additive_inverse(sF9),
inference(cp,[status(thm)],[t40,t719]) ).
cnf(t730,plain,
additive_inverse(sF9) = sF8,
inference(orient,[status(thm)],[t722]) ).
cnf(t4356,plain,
add(sF10,add(sF8,X1)) = add(sF6,X1),
inference(step,[status(thm)],[t1332,t730]) ).
cnf(t4357,plain,
add(sF8,add(X1,sF10)) = add(sF6,X1),
inference(step,[status(thm)],[t4356,t1922]) ).
cnf(t2285,plain,
add(sF8,add(X1,sF10)) = add(sF6,X1),
inference(orient,[status(thm)],[t4357]) ).
cnf(t2288,plain,
add(sF6,sF5) = add(sF8,sF11),
inference(cp,[status(thm)],[t2285,t1230]) ).
cnf(t4358,plain,
add(sF5,sF6) = add(sF8,sF11),
inference(step,[status(thm)],[t2288,t77]) ).
cnf(t4359,plain,
add(sF4,sF13) = add(sF8,sF11),
inference(step,[status(thm)],[t4358,t2156]) ).
cnf(t2314,plain,
add(sF8,sF11) = add(sF4,sF13),
inference(orient,[status(thm)],[t4359]) ).
cnf(t2318,plain,
add(sF15,sF11) = add(sF3,add(sF4,sF13)),
inference(cp,[status(thm)],[t1581,t2314]) ).
cnf(t4360,plain,
add(sF11,sF15) = add(sF3,add(sF4,sF13)),
inference(step,[status(thm)],[t2318,t77]) ).
cnf(t597,plain,
additive_identity = add(sF3,sF4),
inference(cp,[status(thm)],[t47,t593]) ).
cnf(t608,plain,
add(sF3,sF4) = additive_identity,
inference(orient,[status(thm)],[t597]) ).
cnf(t609,plain,
add(sF3,add(sF4,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t62,t608]) ).
cnf(t4263,plain,
add(sF3,add(sF4,X1)) = X1,
inference(step,[status(thm)],[t609,t39]) ).
cnf(t1164,plain,
add(sF3,add(sF4,X1)) = X1,
inference(orient,[status(thm)],[t4263]) ).
cnf(t4361,plain,
add(sF11,sF15) = sF13,
inference(step,[status(thm)],[t4360,t1164]) ).
cnf(t2321,plain,
add(sF11,sF15) = sF13,
inference(orient,[status(thm)],[t4361]) ).
cnf(t2323,plain,
add(sF11,add(sF15,X1)) = add(sF13,X1),
inference(cp,[status(thm)],[t62,t2321]) ).
cnf(t4097,plain,
add(sF11,add(sF15,X1)) = add(sF13,X1),
inference(orient,[status(thm)],[t2323]) ).
cnf(t4098,plain,
add(sF13,additive_inverse(sF15)) = add(sF11,additive_identity),
inference(cp,[status(thm)],[t4097,t47]) ).
cnf(t4484,plain,
add(sF13,sF16) = add(sF11,additive_identity),
inference(step,[status(thm)],[t4098,t995]) ).
cnf(t4485,plain,
sF17 = add(sF11,additive_identity),
inference(step,[status(thm)],[t4484,t1072]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t38,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t4486,plain,
sF17 = sF11,
inference(step,[status(thm)],[t4485,t38]) ).
cnf(t4112,plain,
sF17 = sF11,
inference(orient,[status(thm)],[t4486]) ).
cnf(t4487,plain,
add(sF13,sF16) = sF11,
inference(step,[status(thm)],[t1072,t4112]) ).
cnf(t4113,plain,
add(sF13,sF16) = sF11,
inference(orient,[status(thm)],[t4487]) ).
cnf(u0,negated_conjecture,
associator(x,y,add(u,v)) != add(associator(x,y,u),associator(x,y,v)),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
add(add(multiply(multiply(x,y),u),additive_inverse(multiply(x,multiply(y,u)))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
add(multiply(multiply(x,y),u),add(additive_inverse(multiply(x,multiply(y,u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[goal_0,t62]) ).
cnf(g0_1,plain,
add(multiply(sF0,u),add(additive_inverse(multiply(x,multiply(y,u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_0,t43]) ).
cnf(g0_2,plain,
add(sF1,add(additive_inverse(multiply(x,multiply(y,u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_1,t86]) ).
cnf(g0_3,plain,
add(sF1,add(multiply(x,additive_inverse(multiply(y,u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_2,t51]) ).
cnf(g0_4,plain,
add(sF1,add(multiply(x,multiply(y,additive_inverse(u))),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_3,t51]) ).
cnf(g0_5,plain,
add(sF1,add(multiply(x,additive_inverse(sF2)),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_4,t60]) ).
cnf(g0_6,plain,
add(sF1,add(sF4,add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_5,t594]) ).
cnf(g0_7,plain,
add(sF5,add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_6,t1225]) ).
cnf(g0_8,plain,
add(sF5,add(multiply(sF0,v),additive_inverse(multiply(x,multiply(y,v))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_7,t43]) ).
cnf(g0_9,plain,
add(sF5,add(sF6,additive_inverse(multiply(x,multiply(y,v))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_8,t94]) ).
cnf(g0_10,plain,
add(sF4,add(sF13,additive_inverse(multiply(x,multiply(y,v))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_9,t4017]) ).
cnf(g0_11,plain,
add(sF4,add(sF13,multiply(x,additive_inverse(multiply(y,v))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_10,t51]) ).
cnf(g0_12,plain,
add(sF4,add(sF13,multiply(x,multiply(y,additive_inverse(v))))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_11,t51]) ).
cnf(g0_13,plain,
add(sF4,add(sF13,multiply(x,additive_inverse(sF7)))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_12,t61]) ).
cnf(g0_14,plain,
add(sF4,add(sF13,sF9)) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_13,t720]) ).
cnf(g0_15,plain,
add(sF4,add(sF9,sF13)) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_14,t77]) ).
cnf(g0_16,plain,
add(sF4,add(sF1,sF10)) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_15,t1406]) ).
cnf(g0_17,plain,
add(sF1,add(sF10,sF4)) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_16,t1922]) ).
cnf(g0_18,plain,
add(sF5,sF10) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_17,t2148]) ).
cnf(g0_19,plain,
sF11 != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_18,t1230]) ).
cnf(g0_20,plain,
sF11 != add(multiply(sF0,add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_19,t43]) ).
cnf(g0_21,plain,
sF11 != add(multiply(sF0,add(u,v)),multiply(x,additive_inverse(multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_20,t51]) ).
cnf(g0_22,plain,
sF11 != add(multiply(sF0,add(u,v)),multiply(x,multiply(y,additive_inverse(add(u,v))))),
inference(rw,[status(thm)],[g0_21,t51]) ).
cnf(g0_23,plain,
sF11 != add(multiply(sF0,add(v,u)),multiply(x,multiply(y,additive_inverse(add(u,v))))),
inference(rw,[status(thm)],[g0_22,t302]) ).
cnf(g0_24,plain,
sF11 != add(multiply(sF0,sF12),multiply(x,multiply(y,additive_inverse(add(u,v))))),
inference(rw,[status(thm)],[g0_23,t83]) ).
cnf(g0_25,plain,
sF11 != add(sF13,multiply(x,multiply(y,additive_inverse(add(u,v))))),
inference(rw,[status(thm)],[g0_24,t892]) ).
cnf(g0_26,plain,
sF11 != add(sF13,multiply(x,multiply(y,additive_inverse(add(v,u))))),
inference(rw,[status(thm)],[g0_25,t77]) ).
cnf(g0_27,plain,
sF11 != add(sF13,multiply(x,multiply(y,additive_inverse(sF12)))),
inference(rw,[status(thm)],[g0_26,t83]) ).
cnf(g0_28,plain,
sF11 != add(sF13,multiply(x,additive_inverse(sF14))),
inference(rw,[status(thm)],[g0_27,t141]) ).
cnf(g0_29,plain,
sF11 != add(sF13,sF16),
inference(rw,[status(thm)],[g0_28,t996]) ).
cnf(g0_30,plain,
sF11 != sF11,
inference(rw,[status(thm)],[g0_29,t4113]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG019-7 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 07:48:34 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.21/1.85 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.21/1.85 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------