%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG021-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 : n005.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 5.93s 1.40s
% Output : CNFRefutation 5.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 27
% Syntax : Number of clauses : 224 ( 224 unt; 0 nHn; 162 RR)
% Number of literals : 224 ( 223 equ; 32 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 : 81 ( 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(u,x),
introduced(definition) ).
cnf(t36,plain,
multiply(u,x) = sF0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sF1 = multiply(multiply(u,x),y),
introduced(definition) ).
cnf(t2534,plain,
sF1 = multiply(sF0,y),
inference(step,[status(thm)],[t14,t36]) ).
cnf(t57,plain,
multiply(sF0,y) = sF1,
inference(orient,[status(thm)],[t2534]) ).
cnf(t15,axiom,
sF2 = multiply(x,y),
introduced(definition) ).
cnf(t37,plain,
multiply(x,y) = sF2,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sF3 = multiply(u,multiply(x,y)),
introduced(definition) ).
cnf(t2535,plain,
sF3 = multiply(u,sF2),
inference(step,[status(thm)],[t16,t37]) ).
cnf(t59,plain,
multiply(u,sF2) = sF3,
inference(orient,[status(thm)],[t2535]) ).
cnf(t17,axiom,
sF4 = additive_inverse(multiply(u,multiply(x,y))),
introduced(definition) ).
cnf(t2551,plain,
sF4 = additive_inverse(multiply(u,sF2)),
inference(step,[status(thm)],[t17,t37]) ).
cnf(t2552,plain,
sF4 = additive_inverse(sF3),
inference(step,[status(thm)],[t2551,t59]) ).
cnf(t244,plain,
additive_inverse(sF3) = sF4,
inference(orient,[status(thm)],[t2552]) ).
cnf(t18,axiom,
sF5 = add(multiply(multiply(u,x),y),additive_inverse(multiply(u,multiply(x,y)))),
introduced(definition) ).
cnf(t2559,plain,
sF5 = add(multiply(sF0,y),additive_inverse(multiply(u,multiply(x,y)))),
inference(step,[status(thm)],[t18,t36]) ).
cnf(t2560,plain,
sF5 = add(sF1,additive_inverse(multiply(u,multiply(x,y)))),
inference(step,[status(thm)],[t2559,t57]) ).
cnf(t2561,plain,
sF5 = add(sF1,additive_inverse(multiply(u,sF2))),
inference(step,[status(thm)],[t2560,t37]) ).
cnf(t2562,plain,
sF5 = add(sF1,additive_inverse(sF3)),
inference(step,[status(thm)],[t2561,t59]) ).
cnf(t2563,plain,
sF5 = add(sF1,sF4),
inference(step,[status(thm)],[t2562,t244]) ).
cnf(t296,plain,
add(sF1,sF4) = sF5,
inference(orient,[status(thm)],[t2563]) ).
cnf(t298,plain,
add(sF1,add(sF4,X1)) = add(sF5,X1),
inference(cp,[status(thm)],[t44,t296]) ).
cnf(t539,plain,
add(sF1,add(sF4,X1)) = add(sF5,X1),
inference(orient,[status(thm)],[t298]) ).
cnf(t19,axiom,
sF6 = multiply(v,x),
introduced(definition) ).
cnf(t38,plain,
multiply(v,x) = sF6,
inference(orient,[status(thm)],[t19]) ).
cnf(t20,axiom,
sF7 = multiply(multiply(v,x),y),
introduced(definition) ).
cnf(t2536,plain,
sF7 = multiply(sF6,y),
inference(step,[status(thm)],[t20,t38]) ).
cnf(t61,plain,
multiply(sF6,y) = sF7,
inference(orient,[status(thm)],[t2536]) ).
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(t543,plain,
add(sF5,X1) = add(sF1,add(X1,sF4)),
inference(cp,[status(thm)],[t539,t69]) ).
cnf(t1112,plain,
add(sF1,add(X1,sF4)) = add(sF5,X1),
inference(orient,[status(thm)],[t543]) ).
cnf(t12,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t149,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t160,plain,
multiply(add(sF0,X1),y) = add(sF1,multiply(X1,y)),
inference(cp,[status(thm)],[t149,t57]) ).
cnf(t363,plain,
add(sF1,multiply(X1,y)) = multiply(add(sF0,X1),y),
inference(orient,[status(thm)],[t160]) ).
cnf(t368,plain,
multiply(add(sF0,sF6),y) = add(sF1,sF7),
inference(cp,[status(thm)],[t363,t61]) ).
cnf(t154,plain,
multiply(add(v,X1),x) = add(sF6,multiply(X1,x)),
inference(cp,[status(thm)],[t149,t38]) ).
cnf(t346,plain,
add(sF6,multiply(X1,x)) = multiply(add(v,X1),x),
inference(orient,[status(thm)],[t154]) ).
cnf(t347,plain,
multiply(add(v,u),x) = add(sF6,sF0),
inference(cp,[status(thm)],[t346,t36]) ).
cnf(t25,axiom,
sF12 = add(u,v),
introduced(definition) ).
cnf(t39,plain,
add(u,v) = sF12,
inference(orient,[status(thm)],[t25]) ).
cnf(t2539,plain,
add(v,u) = sF12,
inference(step,[status(thm)],[t39,t69]) ).
cnf(t70,plain,
add(v,u) = sF12,
inference(rw,[status(thm)],[t2539]) ).
cnf(t77,plain,
add(v,u) = sF12,
inference(orient,[status(thm)],[t70]) ).
cnf(t2575,plain,
multiply(sF12,x) = add(sF6,sF0),
inference(step,[status(thm)],[t347,t77]) ).
cnf(t26,axiom,
sF13 = multiply(add(u,v),x),
introduced(definition) ).
cnf(t2538,plain,
sF13 = multiply(sF12,x),
inference(step,[status(thm)],[t26,t39]) ).
cnf(t65,plain,
multiply(sF12,x) = sF13,
inference(orient,[status(thm)],[t2538]) ).
cnf(t2576,plain,
sF13 = add(sF6,sF0),
inference(step,[status(thm)],[t2575,t65]) ).
cnf(t2577,plain,
sF13 = add(sF0,sF6),
inference(step,[status(thm)],[t2576,t69]) ).
cnf(t354,plain,
add(sF0,sF6) = sF13,
inference(orient,[status(thm)],[t2577]) ).
cnf(t2580,plain,
multiply(sF13,y) = add(sF1,sF7),
inference(step,[status(thm)],[t368,t354]) ).
cnf(t371,plain,
add(sF1,sF7) = multiply(sF13,y),
inference(orient,[status(thm)],[t2580]) ).
cnf(t373,plain,
add(sF1,add(sF7,X1)) = add(multiply(sF13,y),X1),
inference(cp,[status(thm)],[t44,t371]) ).
cnf(t27,axiom,
sF14 = multiply(multiply(add(u,v),x),y),
introduced(definition) ).
cnf(t151,plain,
multiply(add(X1,u),x) = add(multiply(X1,x),sF0),
inference(cp,[status(thm)],[t149,t36]) ).
cnf(t2569,plain,
multiply(add(X1,u),x) = add(sF0,multiply(X1,x)),
inference(step,[status(thm)],[t151,t69]) ).
cnf(t150,plain,
multiply(add(u,X1),x) = add(sF0,multiply(X1,x)),
inference(cp,[status(thm)],[t149,t36]) ).
cnf(t310,plain,
add(sF0,multiply(X1,x)) = multiply(add(u,X1),x),
inference(orient,[status(thm)],[t150]) ).
cnf(t2570,plain,
multiply(add(X1,u),x) = multiply(add(u,X1),x),
inference(step,[status(thm)],[t2569,t310]) ).
cnf(t318,plain,
multiply(add(X1,u),x) = multiply(add(u,X1),x),
inference(orient,[status(thm)],[t2570]) ).
cnf(t2612,plain,
sF14 = multiply(multiply(add(v,u),x),y),
inference(step,[status(thm)],[t27,t318]) ).
cnf(t2613,plain,
sF14 = multiply(multiply(sF12,x),y),
inference(step,[status(thm)],[t2612,t77]) ).
cnf(t2614,plain,
sF14 = multiply(sF13,y),
inference(step,[status(thm)],[t2613,t65]) ).
cnf(t482,plain,
multiply(sF13,y) = sF14,
inference(orient,[status(thm)],[t2614]) ).
cnf(t2647,plain,
add(sF1,add(sF7,X1)) = add(sF14,X1),
inference(step,[status(thm)],[t373,t482]) ).
cnf(t681,plain,
add(sF1,add(sF7,X1)) = add(sF14,X1),
inference(orient,[status(thm)],[t2647]) ).
cnf(t1115,plain,
add(sF5,sF7) = add(sF14,sF4),
inference(cp,[status(thm)],[t1112,t681]) ).
cnf(t2676,plain,
add(sF5,sF7) = add(sF4,sF14),
inference(step,[status(thm)],[t1115,t69]) ).
cnf(t1120,plain,
add(sF5,sF7) = add(sF4,sF14),
inference(orient,[status(thm)],[t2676]) ).
cnf(t1122,plain,
add(sF5,add(sF7,X1)) = add(add(sF4,sF14),X1),
inference(cp,[status(thm)],[t44,t1120]) ).
cnf(t2734,plain,
add(sF5,add(sF7,X1)) = add(sF4,add(sF14,X1)),
inference(step,[status(thm)],[t1122,t44]) ).
cnf(t2229,plain,
add(sF5,add(sF7,X1)) = add(sF4,add(sF14,X1)),
inference(orient,[status(thm)],[t2734]) ).
cnf(t21,axiom,
sF8 = multiply(v,multiply(x,y)),
introduced(definition) ).
cnf(t2537,plain,
sF8 = multiply(v,sF2),
inference(step,[status(thm)],[t21,t37]) ).
cnf(t63,plain,
multiply(v,sF2) = sF8,
inference(orient,[status(thm)],[t2537]) ).
cnf(t22,axiom,
sF9 = additive_inverse(multiply(v,multiply(x,y))),
introduced(definition) ).
cnf(t2573,plain,
sF9 = additive_inverse(multiply(v,sF2)),
inference(step,[status(thm)],[t22,t37]) ).
cnf(t2574,plain,
sF9 = additive_inverse(sF8),
inference(step,[status(thm)],[t2573,t63]) ).
cnf(t339,plain,
additive_inverse(sF8) = sF9,
inference(orient,[status(thm)],[t2574]) ).
cnf(t23,axiom,
sF10 = add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))),
introduced(definition) ).
cnf(t2581,plain,
sF10 = add(multiply(sF6,y),additive_inverse(multiply(v,multiply(x,y)))),
inference(step,[status(thm)],[t23,t38]) ).
cnf(t2582,plain,
sF10 = add(sF7,additive_inverse(multiply(v,multiply(x,y)))),
inference(step,[status(thm)],[t2581,t61]) ).
cnf(t2583,plain,
sF10 = add(sF7,additive_inverse(multiply(v,sF2))),
inference(step,[status(thm)],[t2582,t37]) ).
cnf(t2584,plain,
sF10 = add(sF7,additive_inverse(sF8)),
inference(step,[status(thm)],[t2583,t63]) ).
cnf(t2585,plain,
sF10 = add(sF7,sF9),
inference(step,[status(thm)],[t2584,t339]) ).
cnf(t374,plain,
add(sF7,sF9) = sF10,
inference(orient,[status(thm)],[t2585]) ).
cnf(t686,plain,
add(sF14,sF9) = add(sF1,sF10),
inference(cp,[status(thm)],[t681,t374]) ).
cnf(t2648,plain,
add(sF9,sF14) = add(sF1,sF10),
inference(step,[status(thm)],[t686,t69]) ).
cnf(t688,plain,
add(sF9,sF14) = add(sF1,sF10),
inference(orient,[status(thm)],[t2648]) ).
cnf(t73,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(cp,[status(thm)],[t69,t44]) ).
cnf(t990,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(orient,[status(thm)],[t73]) ).
cnf(t24,axiom,
sF11 = add(add(multiply(multiply(u,x),y),additive_inverse(multiply(u,multiply(x,y)))),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y))))),
introduced(definition) ).
cnf(t2596,plain,
sF11 = add(multiply(multiply(u,x),y),add(additive_inverse(multiply(u,multiply(x,y))),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))),
inference(step,[status(thm)],[t24,t44]) ).
cnf(t2597,plain,
sF11 = add(multiply(sF0,y),add(additive_inverse(multiply(u,multiply(x,y))),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))),
inference(step,[status(thm)],[t2596,t36]) ).
cnf(t2598,plain,
sF11 = add(sF1,add(additive_inverse(multiply(u,multiply(x,y))),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))),
inference(step,[status(thm)],[t2597,t57]) ).
cnf(t2599,plain,
sF11 = add(sF1,add(additive_inverse(multiply(u,sF2)),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))),
inference(step,[status(thm)],[t2598,t37]) ).
cnf(t2600,plain,
sF11 = add(sF1,add(additive_inverse(sF3),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))),
inference(step,[status(thm)],[t2599,t59]) ).
cnf(t2601,plain,
sF11 = add(sF1,add(sF4,add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))),
inference(step,[status(thm)],[t2600,t244]) ).
cnf(t2602,plain,
sF11 = add(sF1,add(sF4,add(multiply(sF6,y),additive_inverse(multiply(v,multiply(x,y)))))),
inference(step,[status(thm)],[t2601,t38]) ).
cnf(t2603,plain,
sF11 = add(sF1,add(sF4,add(sF7,additive_inverse(multiply(v,multiply(x,y)))))),
inference(step,[status(thm)],[t2602,t61]) ).
cnf(t2604,plain,
sF11 = add(sF1,add(sF4,add(sF7,additive_inverse(multiply(v,sF2))))),
inference(step,[status(thm)],[t2603,t37]) ).
cnf(t2605,plain,
sF11 = add(sF1,add(sF4,add(sF7,additive_inverse(sF8)))),
inference(step,[status(thm)],[t2604,t63]) ).
cnf(t2606,plain,
sF11 = add(sF1,add(sF4,add(sF7,sF9))),
inference(step,[status(thm)],[t2605,t339]) ).
cnf(t2607,plain,
sF11 = add(sF1,add(sF4,sF10)),
inference(step,[status(thm)],[t2606,t374]) ).
cnf(t428,plain,
add(sF1,add(sF4,sF10)) = sF11,
inference(orient,[status(thm)],[t2607]) ).
cnf(t2623,plain,
add(sF5,sF10) = sF11,
inference(step,[status(thm)],[t428,t539]) ).
cnf(t540,plain,
add(sF5,sF10) = sF11,
inference(rw,[status(thm)],[t2623]) ).
cnf(t544,plain,
add(sF5,sF10) = sF11,
inference(orient,[status(thm)],[t540]) ).
cnf(t163,plain,
multiply(add(X1,u),sF2) = add(multiply(X1,sF2),sF3),
inference(cp,[status(thm)],[t149,t59]) ).
cnf(t2588,plain,
multiply(add(X1,u),sF2) = add(sF3,multiply(X1,sF2)),
inference(step,[status(thm)],[t163,t69]) ).
cnf(t162,plain,
multiply(add(u,X1),sF2) = add(sF3,multiply(X1,sF2)),
inference(cp,[status(thm)],[t149,t59]) ).
cnf(t383,plain,
add(sF3,multiply(X1,sF2)) = multiply(add(u,X1),sF2),
inference(orient,[status(thm)],[t162]) ).
cnf(t2589,plain,
multiply(add(X1,u),sF2) = multiply(add(u,X1),sF2),
inference(step,[status(thm)],[t2588,t383]) ).
cnf(t390,plain,
multiply(add(X1,u),sF2) = multiply(add(u,X1),sF2),
inference(orient,[status(thm)],[t2589]) ).
cnf(t28,axiom,
sF15 = multiply(add(u,v),multiply(x,y)),
introduced(definition) ).
cnf(t2618,plain,
sF15 = multiply(add(v,u),multiply(x,y)),
inference(step,[status(thm)],[t28,t69]) ).
cnf(t2619,plain,
sF15 = multiply(sF12,multiply(x,y)),
inference(step,[status(thm)],[t2618,t77]) ).
cnf(t2620,plain,
sF15 = multiply(sF12,sF2),
inference(step,[status(thm)],[t2619,t37]) ).
cnf(t522,plain,
multiply(sF12,sF2) = sF15,
inference(orient,[status(thm)],[t2620]) ).
cnf(t29,axiom,
sF16 = additive_inverse(multiply(add(u,v),multiply(x,y))),
introduced(definition) ).
cnf(t2627,plain,
sF16 = additive_inverse(multiply(add(v,u),multiply(x,y))),
inference(step,[status(thm)],[t29,t69]) ).
cnf(t2628,plain,
sF16 = additive_inverse(multiply(sF12,multiply(x,y))),
inference(step,[status(thm)],[t2627,t77]) ).
cnf(t2629,plain,
sF16 = additive_inverse(multiply(sF12,sF2)),
inference(step,[status(thm)],[t2628,t37]) ).
cnf(t2630,plain,
sF16 = additive_inverse(sF15),
inference(step,[status(thm)],[t2629,t522]) ).
cnf(t558,plain,
additive_inverse(sF15) = sF16,
inference(orient,[status(thm)],[t2630]) ).
cnf(t30,axiom,
sF17 = add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
introduced(definition) ).
cnf(t2635,plain,
sF17 = add(multiply(multiply(add(v,u),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(step,[status(thm)],[t30,t318]) ).
cnf(t2636,plain,
sF17 = add(multiply(multiply(sF12,x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(step,[status(thm)],[t2635,t77]) ).
cnf(t2637,plain,
sF17 = add(multiply(sF13,y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(step,[status(thm)],[t2636,t65]) ).
cnf(t2638,plain,
sF17 = add(sF14,additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(step,[status(thm)],[t2637,t482]) ).
cnf(t2639,plain,
sF17 = add(sF14,additive_inverse(multiply(add(v,u),multiply(x,y)))),
inference(step,[status(thm)],[t2638,t69]) ).
cnf(t2640,plain,
sF17 = add(sF14,additive_inverse(multiply(sF12,multiply(x,y)))),
inference(step,[status(thm)],[t2639,t77]) ).
cnf(t2641,plain,
sF17 = add(sF14,additive_inverse(multiply(sF12,sF2))),
inference(step,[status(thm)],[t2640,t37]) ).
cnf(t2642,plain,
sF17 = add(sF14,additive_inverse(sF15)),
inference(step,[status(thm)],[t2641,t522]) ).
cnf(t2643,plain,
sF17 = add(sF14,sF16),
inference(step,[status(thm)],[t2642,t558]) ).
cnf(t600,plain,
add(sF14,sF16) = sF17,
inference(orient,[status(thm)],[t2643]) ).
cnf(t166,plain,
multiply(add(v,X1),sF2) = add(sF8,multiply(X1,sF2)),
inference(cp,[status(thm)],[t149,t63]) ).
cnf(t412,plain,
add(sF8,multiply(X1,sF2)) = multiply(add(v,X1),sF2),
inference(orient,[status(thm)],[t166]) ).
cnf(t415,plain,
multiply(add(v,u),sF2) = add(sF8,sF3),
inference(cp,[status(thm)],[t412,t59]) ).
cnf(t2592,plain,
multiply(sF12,sF2) = add(sF8,sF3),
inference(step,[status(thm)],[t415,t77]) ).
cnf(t2593,plain,
multiply(sF12,sF2) = add(sF3,sF8),
inference(step,[status(thm)],[t2592,t69]) ).
cnf(t419,plain,
add(sF3,sF8) = multiply(sF12,sF2),
inference(orient,[status(thm)],[t2593]) ).
cnf(t421,plain,
add(sF3,add(sF8,X1)) = add(multiply(sF12,sF2),X1),
inference(cp,[status(thm)],[t44,t419]) ).
cnf(t2656,plain,
add(sF3,add(sF8,X1)) = add(sF15,X1),
inference(step,[status(thm)],[t421,t522]) ).
cnf(t755,plain,
add(sF3,add(sF8,X1)) = add(sF15,X1),
inference(orient,[status(thm)],[t2656]) ).
cnf(t376,plain,
add(sF7,add(sF9,X1)) = add(sF10,X1),
inference(cp,[status(thm)],[t44,t374]) ).
cnf(t697,plain,
add(sF7,add(sF9,X1)) = add(sF10,X1),
inference(orient,[status(thm)],[t376]) ).
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(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(t2653,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t47,t32]) ).
cnf(t715,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t2653]) ).
cnf(t724,plain,
add(sF10,add(additive_inverse(sF9),X1)) = add(sF7,X1),
inference(cp,[status(thm)],[t697,t715]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t340,plain,
sF8 = additive_inverse(sF9),
inference(cp,[status(thm)],[t33,t339]) ).
cnf(t342,plain,
additive_inverse(sF9) = sF8,
inference(orient,[status(thm)],[t340]) ).
cnf(t2693,plain,
add(sF10,add(sF8,X1)) = add(sF7,X1),
inference(step,[status(thm)],[t724,t342]) ).
cnf(t2694,plain,
add(sF8,add(X1,sF10)) = add(sF7,X1),
inference(step,[status(thm)],[t2693,t990]) ).
cnf(t1474,plain,
add(sF8,add(X1,sF10)) = add(sF7,X1),
inference(orient,[status(thm)],[t2694]) ).
cnf(t1476,plain,
add(sF7,sF5) = add(sF8,sF11),
inference(cp,[status(thm)],[t1474,t544]) ).
cnf(t2695,plain,
add(sF5,sF7) = add(sF8,sF11),
inference(step,[status(thm)],[t1476,t69]) ).
cnf(t2696,plain,
add(sF4,sF14) = add(sF8,sF11),
inference(step,[status(thm)],[t2695,t1120]) ).
cnf(t1481,plain,
add(sF8,sF11) = add(sF4,sF14),
inference(orient,[status(thm)],[t2696]) ).
cnf(t1485,plain,
add(sF15,sF11) = add(sF3,add(sF4,sF14)),
inference(cp,[status(thm)],[t755,t1481]) ).
cnf(t2697,plain,
add(sF11,sF15) = add(sF3,add(sF4,sF14)),
inference(step,[status(thm)],[t1485,t69]) ).
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(t2617,plain,
add(sF3,add(sF4,X1)) = X1,
inference(step,[status(thm)],[t250,t32]) ).
cnf(t499,plain,
add(sF3,add(sF4,X1)) = X1,
inference(orient,[status(thm)],[t2617]) ).
cnf(t2698,plain,
add(sF11,sF15) = sF14,
inference(step,[status(thm)],[t2697,t499]) ).
cnf(t1562,plain,
add(sF11,sF15) = sF14,
inference(orient,[status(thm)],[t2698]) ).
cnf(t1564,plain,
add(sF11,add(sF15,X1)) = add(sF14,X1),
inference(cp,[status(thm)],[t44,t1562]) ).
cnf(t2501,plain,
add(sF11,add(sF15,X1)) = add(sF14,X1),
inference(orient,[status(thm)],[t1564]) ).
cnf(t2502,plain,
add(sF14,additive_inverse(sF15)) = add(sF11,additive_identity),
inference(cp,[status(thm)],[t2501,t40]) ).
cnf(t2751,plain,
add(sF14,sF16) = add(sF11,additive_identity),
inference(step,[status(thm)],[t2502,t558]) ).
cnf(t2752,plain,
sF17 = add(sF11,additive_identity),
inference(step,[status(thm)],[t2751,t600]) ).
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(t2753,plain,
sF17 = sF11,
inference(step,[status(thm)],[t2752,t31]) ).
cnf(t2517,plain,
sF17 = sF11,
inference(orient,[status(thm)],[t2753]) ).
cnf(t2754,plain,
add(sF14,sF16) = sF11,
inference(step,[status(thm)],[t600,t2517]) ).
cnf(t2518,plain,
add(sF14,sF16) = sF11,
inference(orient,[status(thm)],[t2754]) ).
cnf(u0,negated_conjecture,
associator(add(u,v),x,y) != add(associator(u,x,y),associator(v,x,y)),
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(u,x),y),additive_inverse(multiply(u,multiply(x,y)))),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
add(multiply(multiply(u,x),y),add(additive_inverse(multiply(u,multiply(x,y))),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[goal_0,t44]) ).
cnf(g0_1,plain,
add(multiply(sF0,y),add(additive_inverse(multiply(u,multiply(x,y))),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_0,t36]) ).
cnf(g0_2,plain,
add(sF1,add(additive_inverse(multiply(u,multiply(x,y))),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_1,t57]) ).
cnf(g0_3,plain,
add(sF1,add(additive_inverse(multiply(u,sF2)),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_2,t37]) ).
cnf(g0_4,plain,
add(sF1,add(additive_inverse(sF3),add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_3,t59]) ).
cnf(g0_5,plain,
add(sF1,add(sF4,add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_4,t244]) ).
cnf(g0_6,plain,
add(sF5,add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_5,t539]) ).
cnf(g0_7,plain,
add(sF5,add(multiply(sF6,y),additive_inverse(multiply(v,multiply(x,y))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_6,t38]) ).
cnf(g0_8,plain,
add(sF5,add(sF7,additive_inverse(multiply(v,multiply(x,y))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_7,t61]) ).
cnf(g0_9,plain,
add(sF4,add(sF14,additive_inverse(multiply(v,multiply(x,y))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_8,t2229]) ).
cnf(g0_10,plain,
add(sF4,add(sF14,additive_inverse(multiply(v,sF2)))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_9,t37]) ).
cnf(g0_11,plain,
add(sF4,add(sF14,additive_inverse(sF8))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_10,t63]) ).
cnf(g0_12,plain,
add(sF4,add(sF14,sF9)) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_11,t339]) ).
cnf(g0_13,plain,
add(sF4,add(sF9,sF14)) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_12,t69]) ).
cnf(g0_14,plain,
add(sF4,add(sF1,sF10)) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_13,t688]) ).
cnf(g0_15,plain,
add(sF1,add(sF10,sF4)) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_14,t990]) ).
cnf(g0_16,plain,
add(sF5,sF10) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_15,t1112]) ).
cnf(g0_17,plain,
sF11 != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_16,t544]) ).
cnf(g0_18,plain,
sF11 != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),sF2))),
inference(rw,[status(thm)],[g0_17,t37]) ).
cnf(g0_19,plain,
sF11 != add(additive_inverse(multiply(add(u,v),sF2)),multiply(multiply(add(u,v),x),y)),
inference(rw,[status(thm)],[g0_18,t69]) ).
cnf(g0_20,plain,
sF11 != add(additive_inverse(multiply(add(v,u),sF2)),multiply(multiply(add(u,v),x),y)),
inference(rw,[status(thm)],[g0_19,t390]) ).
cnf(g0_21,plain,
sF11 != add(additive_inverse(multiply(sF12,sF2)),multiply(multiply(add(u,v),x),y)),
inference(rw,[status(thm)],[g0_20,t77]) ).
cnf(g0_22,plain,
sF11 != add(additive_inverse(sF15),multiply(multiply(add(u,v),x),y)),
inference(rw,[status(thm)],[g0_21,t522]) ).
cnf(g0_23,plain,
sF11 != add(sF16,multiply(multiply(add(u,v),x),y)),
inference(rw,[status(thm)],[g0_22,t558]) ).
cnf(g0_24,plain,
sF11 != add(sF16,multiply(multiply(add(v,u),x),y)),
inference(rw,[status(thm)],[g0_23,t318]) ).
cnf(g0_25,plain,
sF11 != add(sF16,multiply(multiply(sF12,x),y)),
inference(rw,[status(thm)],[g0_24,t77]) ).
cnf(g0_26,plain,
sF11 != add(sF16,multiply(sF13,y)),
inference(rw,[status(thm)],[g0_25,t65]) ).
cnf(g0_27,plain,
sF11 != add(sF16,sF14),
inference(rw,[status(thm)],[g0_26,t482]) ).
cnf(g0_28,plain,
sF11 != add(sF14,sF16),
inference(rw,[status(thm)],[g0_27,t69]) ).
cnf(g0_29,plain,
sF11 != sF11,
inference(rw,[status(thm)],[g0_28,t2518]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_29]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG021-6 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 07:46:48 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.93/1.40 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.93/1.40 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------