%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG019-6 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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 6.75s 1.42s
% Output : CNFRefutation 6.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 26
% Syntax : Number of clauses : 207 ( 207 unt; 0 nHn; 151 RR)
% Number of literals : 207 ( 206 equ; 26 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 : 71 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t44,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t13,axiom,
sF0 = multiply(x,y),
introduced(definition) ).
cnf(t36,plain,
multiply(x,y) = sF0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sF1 = multiply(multiply(x,y),u),
introduced(definition) ).
cnf(t2491,plain,
sF1 = multiply(sF0,u),
inference(step,[status(thm)],[t14,t36]) ).
cnf(t57,plain,
multiply(sF0,u) = sF1,
inference(orient,[status(thm)],[t2491]) ).
cnf(t15,axiom,
sF2 = multiply(y,u),
introduced(definition) ).
cnf(t37,plain,
multiply(y,u) = sF2,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sF3 = multiply(x,multiply(y,u)),
introduced(definition) ).
cnf(t2492,plain,
sF3 = multiply(x,sF2),
inference(step,[status(thm)],[t16,t37]) ).
cnf(t59,plain,
multiply(x,sF2) = sF3,
inference(orient,[status(thm)],[t2492]) ).
cnf(t17,axiom,
sF4 = additive_inverse(multiply(x,multiply(y,u))),
introduced(definition) ).
cnf(t2509,plain,
sF4 = additive_inverse(multiply(x,sF2)),
inference(step,[status(thm)],[t17,t37]) ).
cnf(t2510,plain,
sF4 = additive_inverse(sF3),
inference(step,[status(thm)],[t2509,t59]) ).
cnf(t244,plain,
additive_inverse(sF3) = sF4,
inference(orient,[status(thm)],[t2510]) ).
cnf(t18,axiom,
sF5 = add(multiply(multiply(x,y),u),additive_inverse(multiply(x,multiply(y,u)))),
introduced(definition) ).
cnf(t2516,plain,
sF5 = add(multiply(sF0,u),additive_inverse(multiply(x,multiply(y,u)))),
inference(step,[status(thm)],[t18,t36]) ).
cnf(t2517,plain,
sF5 = add(sF1,additive_inverse(multiply(x,multiply(y,u)))),
inference(step,[status(thm)],[t2516,t57]) ).
cnf(t2518,plain,
sF5 = add(sF1,additive_inverse(multiply(x,sF2))),
inference(step,[status(thm)],[t2517,t37]) ).
cnf(t2519,plain,
sF5 = add(sF1,additive_inverse(sF3)),
inference(step,[status(thm)],[t2518,t59]) ).
cnf(t2520,plain,
sF5 = add(sF1,sF4),
inference(step,[status(thm)],[t2519,t244]) ).
cnf(t292,plain,
add(sF1,sF4) = sF5,
inference(orient,[status(thm)],[t2520]) ).
cnf(t294,plain,
add(sF1,add(sF4,X1)) = add(sF5,X1),
inference(cp,[status(thm)],[t44,t292]) ).
cnf(t586,plain,
add(sF1,add(sF4,X1)) = add(sF5,X1),
inference(orient,[status(thm)],[t294]) ).
cnf(t19,axiom,
sF6 = multiply(multiply(x,y),v),
introduced(definition) ).
cnf(t2493,plain,
sF6 = multiply(sF0,v),
inference(step,[status(thm)],[t19,t36]) ).
cnf(t61,plain,
multiply(sF0,v) = sF6,
inference(orient,[status(thm)],[t2493]) ).
cnf(t20,axiom,
sF7 = multiply(y,v),
introduced(definition) ).
cnf(t38,plain,
multiply(y,v) = sF7,
inference(orient,[status(thm)],[t20]) ).
cnf(t21,axiom,
sF8 = multiply(x,multiply(y,v)),
introduced(definition) ).
cnf(t2494,plain,
sF8 = multiply(x,sF7),
inference(step,[status(thm)],[t21,t38]) ).
cnf(t63,plain,
multiply(x,sF7) = sF8,
inference(orient,[status(thm)],[t2494]) ).
cnf(t22,axiom,
sF9 = additive_inverse(multiply(x,multiply(y,v))),
introduced(definition) ).
cnf(t2532,plain,
sF9 = additive_inverse(multiply(x,sF7)),
inference(step,[status(thm)],[t22,t38]) ).
cnf(t2533,plain,
sF9 = additive_inverse(sF8),
inference(step,[status(thm)],[t2532,t63]) ).
cnf(t342,plain,
additive_inverse(sF8) = sF9,
inference(orient,[status(thm)],[t2533]) ).
cnf(t23,axiom,
sF10 = add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))),
introduced(definition) ).
cnf(t2538,plain,
sF10 = add(multiply(sF0,v),additive_inverse(multiply(x,multiply(y,v)))),
inference(step,[status(thm)],[t23,t36]) ).
cnf(t2539,plain,
sF10 = add(sF6,additive_inverse(multiply(x,multiply(y,v)))),
inference(step,[status(thm)],[t2538,t61]) ).
cnf(t2540,plain,
sF10 = add(sF6,additive_inverse(multiply(x,sF7))),
inference(step,[status(thm)],[t2539,t38]) ).
cnf(t2541,plain,
sF10 = add(sF6,additive_inverse(sF8)),
inference(step,[status(thm)],[t2540,t63]) ).
cnf(t2542,plain,
sF10 = add(sF6,sF9),
inference(step,[status(thm)],[t2541,t342]) ).
cnf(t381,plain,
add(sF6,sF9) = sF10,
inference(orient,[status(thm)],[t2542]) ).
cnf(t24,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(t2553,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)],[t24,t44]) ).
cnf(t2554,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)],[t2553,t36]) ).
cnf(t2555,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)],[t2554,t57]) ).
cnf(t2556,plain,
sF11 = add(sF1,add(additive_inverse(multiply(x,sF2)),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t2555,t37]) ).
cnf(t2557,plain,
sF11 = add(sF1,add(additive_inverse(sF3),add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t2556,t59]) ).
cnf(t2558,plain,
sF11 = add(sF1,add(sF4,add(multiply(multiply(x,y),v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t2557,t244]) ).
cnf(t2559,plain,
sF11 = add(sF1,add(sF4,add(multiply(sF0,v),additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t2558,t36]) ).
cnf(t2560,plain,
sF11 = add(sF1,add(sF4,add(sF6,additive_inverse(multiply(x,multiply(y,v)))))),
inference(step,[status(thm)],[t2559,t61]) ).
cnf(t2561,plain,
sF11 = add(sF1,add(sF4,add(sF6,additive_inverse(multiply(x,sF7))))),
inference(step,[status(thm)],[t2560,t38]) ).
cnf(t2562,plain,
sF11 = add(sF1,add(sF4,add(sF6,additive_inverse(sF8)))),
inference(step,[status(thm)],[t2561,t63]) ).
cnf(t2563,plain,
sF11 = add(sF1,add(sF4,add(sF6,sF9))),
inference(step,[status(thm)],[t2562,t342]) ).
cnf(t2564,plain,
sF11 = add(sF1,add(sF4,sF10)),
inference(step,[status(thm)],[t2563,t381]) ).
cnf(t440,plain,
add(sF1,add(sF4,sF10)) = sF11,
inference(orient,[status(thm)],[t2564]) ).
cnf(t2591,plain,
add(sF5,sF10) = sF11,
inference(step,[status(thm)],[t440,t586]) ).
cnf(t587,plain,
add(sF5,sF10) = sF11,
inference(rw,[status(thm)],[t2591]) ).
cnf(t591,plain,
add(sF5,sF10) = sF11,
inference(orient,[status(thm)],[t587]) ).
cnf(t11,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t90,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t100,plain,
multiply(sF0,add(X1,u)) = add(multiply(sF0,X1),sF1),
inference(cp,[status(thm)],[t90,t57]) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t69,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t2511,plain,
multiply(sF0,add(X1,u)) = add(sF1,multiply(sF0,X1)),
inference(step,[status(thm)],[t100,t69]) ).
cnf(t99,plain,
multiply(sF0,add(u,X1)) = add(sF1,multiply(sF0,X1)),
inference(cp,[status(thm)],[t90,t57]) ).
cnf(t251,plain,
add(sF1,multiply(sF0,X1)) = multiply(sF0,add(u,X1)),
inference(orient,[status(thm)],[t99]) ).
cnf(t2512,plain,
multiply(sF0,add(X1,u)) = multiply(sF0,add(u,X1)),
inference(step,[status(thm)],[t2511,t251]) ).
cnf(t258,plain,
multiply(sF0,add(X1,u)) = multiply(sF0,add(u,X1)),
inference(orient,[status(thm)],[t2512]) ).
cnf(t25,axiom,
sF12 = add(u,v),
introduced(definition) ).
cnf(t39,plain,
add(u,v) = sF12,
inference(orient,[status(thm)],[t25]) ).
cnf(t2496,plain,
add(v,u) = sF12,
inference(step,[status(thm)],[t39,t69]) ).
cnf(t70,plain,
add(v,u) = sF12,
inference(rw,[status(thm)],[t2496]) ).
cnf(t77,plain,
add(v,u) = sF12,
inference(orient,[status(thm)],[t70]) ).
cnf(t26,axiom,
sF13 = multiply(multiply(x,y),add(u,v)),
introduced(definition) ).
cnf(t2570,plain,
sF13 = multiply(sF0,add(u,v)),
inference(step,[status(thm)],[t26,t36]) ).
cnf(t2571,plain,
sF13 = multiply(sF0,add(v,u)),
inference(step,[status(thm)],[t2570,t258]) ).
cnf(t2572,plain,
sF13 = multiply(sF0,sF12),
inference(step,[status(thm)],[t2571,t77]) ).
cnf(t499,plain,
multiply(sF0,sF12) = sF13,
inference(orient,[status(thm)],[t2572]) ).
cnf(t94,plain,
multiply(y,add(X1,u)) = add(multiply(y,X1),sF2),
inference(cp,[status(thm)],[t90,t37]) ).
cnf(t2502,plain,
multiply(y,add(X1,u)) = add(sF2,multiply(y,X1)),
inference(step,[status(thm)],[t94,t69]) ).
cnf(t93,plain,
multiply(y,add(u,X1)) = add(sF2,multiply(y,X1)),
inference(cp,[status(thm)],[t90,t37]) ).
cnf(t208,plain,
add(sF2,multiply(y,X1)) = multiply(y,add(u,X1)),
inference(orient,[status(thm)],[t93]) ).
cnf(t2503,plain,
multiply(y,add(X1,u)) = multiply(y,add(u,X1)),
inference(step,[status(thm)],[t2502,t208]) ).
cnf(t217,plain,
multiply(y,add(X1,u)) = multiply(y,add(u,X1)),
inference(orient,[status(thm)],[t2503]) ).
cnf(t27,axiom,
sF14 = multiply(y,add(u,v)),
introduced(definition) ).
cnf(t2495,plain,
sF14 = multiply(y,sF12),
inference(step,[status(thm)],[t27,t39]) ).
cnf(t65,plain,
multiply(y,sF12) = sF14,
inference(orient,[status(thm)],[t2495]) ).
cnf(t28,axiom,
sF15 = multiply(x,multiply(y,add(u,v))),
introduced(definition) ).
cnf(t2578,plain,
sF15 = multiply(x,multiply(y,add(v,u))),
inference(step,[status(thm)],[t28,t217]) ).
cnf(t2579,plain,
sF15 = multiply(x,multiply(y,sF12)),
inference(step,[status(thm)],[t2578,t77]) ).
cnf(t2580,plain,
sF15 = multiply(x,sF14),
inference(step,[status(thm)],[t2579,t65]) ).
cnf(t545,plain,
multiply(x,sF14) = sF15,
inference(orient,[status(thm)],[t2580]) ).
cnf(t29,axiom,
sF16 = additive_inverse(multiply(x,multiply(y,add(u,v)))),
introduced(definition) ).
cnf(t2587,plain,
sF16 = additive_inverse(multiply(x,multiply(y,add(v,u)))),
inference(step,[status(thm)],[t29,t217]) ).
cnf(t2588,plain,
sF16 = additive_inverse(multiply(x,multiply(y,sF12))),
inference(step,[status(thm)],[t2587,t77]) ).
cnf(t2589,plain,
sF16 = additive_inverse(multiply(x,sF14)),
inference(step,[status(thm)],[t2588,t65]) ).
cnf(t2590,plain,
sF16 = additive_inverse(sF15),
inference(step,[status(thm)],[t2589,t545]) ).
cnf(t579,plain,
additive_inverse(sF15) = sF16,
inference(orient,[status(thm)],[t2590]) ).
cnf(t30,axiom,
sF17 = add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
introduced(definition) ).
cnf(t2597,plain,
sF17 = add(multiply(sF0,add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(step,[status(thm)],[t30,t36]) ).
cnf(t2598,plain,
sF17 = add(multiply(sF0,add(v,u)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(step,[status(thm)],[t2597,t258]) ).
cnf(t2599,plain,
sF17 = add(multiply(sF0,sF12),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(step,[status(thm)],[t2598,t77]) ).
cnf(t2600,plain,
sF17 = add(sF13,additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(step,[status(thm)],[t2599,t499]) ).
cnf(t2601,plain,
sF17 = add(sF13,additive_inverse(multiply(x,multiply(y,add(v,u))))),
inference(step,[status(thm)],[t2600,t217]) ).
cnf(t2602,plain,
sF17 = add(sF13,additive_inverse(multiply(x,multiply(y,sF12)))),
inference(step,[status(thm)],[t2601,t77]) ).
cnf(t2603,plain,
sF17 = add(sF13,additive_inverse(multiply(x,sF14))),
inference(step,[status(thm)],[t2602,t65]) ).
cnf(t2604,plain,
sF17 = add(sF13,additive_inverse(sF15)),
inference(step,[status(thm)],[t2603,t545]) ).
cnf(t2605,plain,
sF17 = add(sF13,sF16),
inference(step,[status(thm)],[t2604,t579]) ).
cnf(t606,plain,
add(sF13,sF16) = sF17,
inference(orient,[status(thm)],[t2605]) ).
cnf(t103,plain,
multiply(sF0,add(v,X1)) = add(sF6,multiply(sF0,X1)),
inference(cp,[status(thm)],[t90,t61]) ).
cnf(t285,plain,
add(sF6,multiply(sF0,X1)) = multiply(sF0,add(v,X1)),
inference(orient,[status(thm)],[t103]) ).
cnf(t286,plain,
multiply(sF0,add(v,u)) = add(sF6,sF1),
inference(cp,[status(thm)],[t285,t57]) ).
cnf(t2521,plain,
multiply(sF0,sF12) = add(sF6,sF1),
inference(step,[status(thm)],[t286,t77]) ).
cnf(t2522,plain,
multiply(sF0,sF12) = add(sF1,sF6),
inference(step,[status(thm)],[t2521,t69]) ).
cnf(t295,plain,
add(sF1,sF6) = multiply(sF0,sF12),
inference(orient,[status(thm)],[t2522]) ).
cnf(t297,plain,
add(sF1,add(sF6,X1)) = add(multiply(sF0,sF12),X1),
inference(cp,[status(thm)],[t44,t295]) ).
cnf(t2595,plain,
add(sF1,add(sF6,X1)) = add(sF13,X1),
inference(step,[status(thm)],[t297,t499]) ).
cnf(t597,plain,
add(sF1,add(sF6,X1)) = add(sF13,X1),
inference(orient,[status(thm)],[t2595]) ).
cnf(t383,plain,
add(sF6,add(sF9,X1)) = add(sF10,X1),
inference(cp,[status(thm)],[t44,t381]) ).
cnf(t724,plain,
add(sF6,add(sF9,X1)) = add(sF10,X1),
inference(orient,[status(thm)],[t383]) ).
cnf(t727,plain,
add(sF10,X1) = add(sF6,add(X1,sF9)),
inference(cp,[status(thm)],[t724,t69]) ).
cnf(t1491,plain,
add(sF6,add(X1,sF9)) = add(sF10,X1),
inference(orient,[status(thm)],[t727]) ).
cnf(t101,plain,
multiply(x,add(sF2,X1)) = add(sF3,multiply(x,X1)),
inference(cp,[status(thm)],[t90,t59]) ).
cnf(t266,plain,
add(sF3,multiply(x,X1)) = multiply(x,add(sF2,X1)),
inference(orient,[status(thm)],[t101]) ).
cnf(t269,plain,
multiply(x,add(sF2,sF7)) = add(sF3,sF8),
inference(cp,[status(thm)],[t266,t63]) ).
cnf(t95,plain,
multiply(y,add(v,X1)) = add(sF7,multiply(y,X1)),
inference(cp,[status(thm)],[t90,t38]) ).
cnf(t225,plain,
add(sF7,multiply(y,X1)) = multiply(y,add(v,X1)),
inference(orient,[status(thm)],[t95]) ).
cnf(t226,plain,
multiply(y,add(v,u)) = add(sF7,sF2),
inference(cp,[status(thm)],[t225,t37]) ).
cnf(t2504,plain,
multiply(y,sF12) = add(sF7,sF2),
inference(step,[status(thm)],[t226,t77]) ).
cnf(t2505,plain,
sF14 = add(sF7,sF2),
inference(step,[status(thm)],[t2504,t65]) ).
cnf(t2506,plain,
sF14 = add(sF2,sF7),
inference(step,[status(thm)],[t2505,t69]) ).
cnf(t234,plain,
add(sF2,sF7) = sF14,
inference(orient,[status(thm)],[t2506]) ).
cnf(t2513,plain,
multiply(x,sF14) = add(sF3,sF8),
inference(step,[status(thm)],[t269,t234]) ).
cnf(t275,plain,
add(sF3,sF8) = multiply(x,sF14),
inference(orient,[status(thm)],[t2513]) ).
cnf(t277,plain,
add(sF3,add(sF8,X1)) = add(multiply(x,sF14),X1),
inference(cp,[status(thm)],[t44,t275]) ).
cnf(t2583,plain,
add(sF3,add(sF8,X1)) = add(sF15,X1),
inference(step,[status(thm)],[t277,t545]) ).
cnf(t564,plain,
add(sF3,add(sF8,X1)) = add(sF15,X1),
inference(orient,[status(thm)],[t2583]) ).
cnf(t5,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t565,plain,
add(sF15,additive_inverse(sF8)) = add(sF3,additive_identity),
inference(cp,[status(thm)],[t564,t40]) ).
cnf(t2584,plain,
add(sF15,sF9) = add(sF3,additive_identity),
inference(step,[status(thm)],[t565,t342]) ).
cnf(t2585,plain,
add(sF9,sF15) = add(sF3,additive_identity),
inference(step,[status(thm)],[t2584,t69]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t2586,plain,
add(sF9,sF15) = sF3,
inference(step,[status(thm)],[t2585,t31]) ).
cnf(t569,plain,
add(sF9,sF15) = sF3,
inference(orient,[status(thm)],[t2586]) ).
cnf(t571,plain,
add(sF9,add(sF15,X1)) = add(sF3,X1),
inference(cp,[status(thm)],[t44,t569]) ).
cnf(t1228,plain,
add(sF9,add(sF15,X1)) = add(sF3,X1),
inference(orient,[status(thm)],[t571]) ).
cnf(t47,plain,
add(X1,add(additive_inverse(X1),X2)) = add(additive_identity,X2),
inference(cp,[status(thm)],[t44,t40]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t2610,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t47,t32]) ).
cnf(t700,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t2610]) ).
cnf(t1233,plain,
add(sF3,add(additive_inverse(sF15),X1)) = add(sF9,X1),
inference(cp,[status(thm)],[t1228,t700]) ).
cnf(t2707,plain,
add(sF3,add(sF16,X1)) = add(sF9,X1),
inference(step,[status(thm)],[t1233,t579]) ).
cnf(t2423,plain,
add(sF3,add(sF16,X1)) = add(sF9,X1),
inference(orient,[status(thm)],[t2707]) ).
cnf(t246,plain,
additive_identity = add(sF3,sF4),
inference(cp,[status(thm)],[t40,t244]) ).
cnf(t249,plain,
add(sF3,sF4) = additive_identity,
inference(orient,[status(thm)],[t246]) ).
cnf(t250,plain,
add(sF3,add(sF4,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t44,t249]) ).
cnf(t2577,plain,
add(sF3,add(sF4,X1)) = X1,
inference(step,[status(thm)],[t250,t32]) ).
cnf(t535,plain,
add(sF3,add(sF4,X1)) = X1,
inference(orient,[status(thm)],[t2577]) ).
cnf(t537,plain,
X1 = add(sF3,add(X1,sF4)),
inference(cp,[status(thm)],[t535,t69]) ).
cnf(t1043,plain,
add(sF3,add(X1,sF4)) = X1,
inference(orient,[status(thm)],[t537]) ).
cnf(t2427,plain,
add(sF9,sF4) = sF16,
inference(cp,[status(thm)],[t2423,t1043]) ).
cnf(t2708,plain,
add(sF4,sF9) = sF16,
inference(step,[status(thm)],[t2427,t69]) ).
cnf(t2434,plain,
add(sF4,sF9) = sF16,
inference(orient,[status(thm)],[t2708]) ).
cnf(t2440,plain,
add(sF10,sF4) = add(sF6,sF16),
inference(cp,[status(thm)],[t1491,t2434]) ).
cnf(t2713,plain,
add(sF4,sF10) = add(sF6,sF16),
inference(step,[status(thm)],[t2440,t69]) ).
cnf(t2469,plain,
add(sF6,sF16) = add(sF4,sF10),
inference(orient,[status(thm)],[t2713]) ).
cnf(t2472,plain,
add(sF13,sF16) = add(sF1,add(sF4,sF10)),
inference(cp,[status(thm)],[t597,t2469]) ).
cnf(t2714,plain,
sF17 = add(sF1,add(sF4,sF10)),
inference(step,[status(thm)],[t2472,t606]) ).
cnf(t2715,plain,
sF17 = add(sF5,sF10),
inference(step,[status(thm)],[t2714,t586]) ).
cnf(t2716,plain,
sF17 = sF11,
inference(step,[status(thm)],[t2715,t591]) ).
cnf(t2479,plain,
sF17 = sF11,
inference(orient,[status(thm)],[t2716]) ).
cnf(t2717,plain,
add(sF13,sF16) = sF11,
inference(step,[status(thm)],[t606,t2479]) ).
cnf(t2480,plain,
add(sF13,sF16) = sF11,
inference(orient,[status(thm)],[t2717]) ).
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,t44]) ).
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,t36]) ).
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,t57]) ).
cnf(g0_3,plain,
add(sF1,add(additive_inverse(multiply(x,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_2,t37]) ).
cnf(g0_4,plain,
add(sF1,add(additive_inverse(sF3),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,t59]) ).
cnf(g0_5,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_4,t244]) ).
cnf(g0_6,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_5,t586]) ).
cnf(g0_7,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_6,t36]) ).
cnf(g0_8,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_7,t61]) ).
cnf(g0_9,plain,
add(sF5,add(sF6,additive_inverse(multiply(x,sF7)))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_8,t38]) ).
cnf(g0_10,plain,
add(sF5,add(sF6,additive_inverse(sF8))) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_9,t63]) ).
cnf(g0_11,plain,
add(sF5,add(sF6,sF9)) != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_10,t342]) ).
cnf(g0_12,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_11,t381]) ).
cnf(g0_13,plain,
sF11 != add(multiply(multiply(x,y),add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_12,t591]) ).
cnf(g0_14,plain,
sF11 != add(multiply(sF0,add(u,v)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_13,t36]) ).
cnf(g0_15,plain,
sF11 != add(multiply(sF0,add(v,u)),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_14,t258]) ).
cnf(g0_16,plain,
sF11 != add(multiply(sF0,sF12),additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_15,t77]) ).
cnf(g0_17,plain,
sF11 != add(sF13,additive_inverse(multiply(x,multiply(y,add(u,v))))),
inference(rw,[status(thm)],[g0_16,t499]) ).
cnf(g0_18,plain,
sF11 != add(sF13,additive_inverse(multiply(x,multiply(y,add(v,u))))),
inference(rw,[status(thm)],[g0_17,t217]) ).
cnf(g0_19,plain,
sF11 != add(sF13,additive_inverse(multiply(x,multiply(y,sF12)))),
inference(rw,[status(thm)],[g0_18,t77]) ).
cnf(g0_20,plain,
sF11 != add(sF13,additive_inverse(multiply(x,sF14))),
inference(rw,[status(thm)],[g0_19,t65]) ).
cnf(g0_21,plain,
sF11 != add(sF13,additive_inverse(sF15)),
inference(rw,[status(thm)],[g0_20,t545]) ).
cnf(g0_22,plain,
sF11 != add(sF13,sF16),
inference(rw,[status(thm)],[g0_21,t579]) ).
cnf(g0_23,plain,
sF11 != sF11,
inference(rw,[status(thm)],[g0_22,t2480]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_23]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG019-6 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.38 % Computer : n013.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Thu Sep 24 07:45:36 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.75/1.42 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.75/1.42 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------