%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG021-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 8.57s 11.88s
% Output : CNFRefutation 8.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 25
% Syntax : Number of clauses : 245 ( 245 unt; 0 nHn; 179 RR)
% Number of literals : 245 ( 244 equ; 28 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 : 25 ( 25 usr; 21 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/sandbox/benchmark/theBenchmark.p') ).
cnf(t200,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t20,axiom,
sFlat0 = multiply(u,x),
introduced(definition) ).
cnf(t165,plain,
multiply(u,x) = sFlat0,
inference(orient,[status(thm)],[t20]) ).
cnf(t21,axiom,
sFlat1 = multiply(multiply(u,x),y),
introduced(definition) ).
cnf(t73,plain,
multiply(multiply(u,x),y) = sFlat1,
inference(orient,[status(thm)],[t21]) ).
cnf(t3206,plain,
multiply(sFlat0,y) = sFlat1,
inference(step,[status(thm)],[t73,t165]) ).
cnf(t173,plain,
multiply(sFlat0,y) = sFlat1,
inference(rw,[status(thm)],[t3206]) ).
cnf(t285,plain,
multiply(sFlat0,y) = sFlat1,
inference(orient,[status(thm)],[t173]) ).
cnf(t8,axiom,
multiply(X1,additive_inverse(X2)) = additive_inverse(multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t61,plain,
additive_inverse(multiply(X1,X2)) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t22,axiom,
sFlat2 = multiply(x,y),
introduced(definition) ).
cnf(t148,plain,
multiply(x,y) = sFlat2,
inference(orient,[status(thm)],[t22]) ).
cnf(t151,plain,
multiply(x,additive_inverse(y)) = additive_inverse(sFlat2),
inference(cp,[status(thm)],[t61,t148]) ).
cnf(t321,plain,
multiply(x,additive_inverse(y)) = additive_inverse(sFlat2),
inference(orient,[status(thm)],[t151]) ).
cnf(t24,axiom,
sFlat4 = additive_inverse(multiply(u,multiply(x,y))),
introduced(definition) ).
cnf(t3235,plain,
sFlat4 = multiply(u,additive_inverse(multiply(x,y))),
inference(step,[status(thm)],[t24,t61]) ).
cnf(t3236,plain,
sFlat4 = multiply(u,multiply(x,additive_inverse(y))),
inference(step,[status(thm)],[t3235,t61]) ).
cnf(t231,plain,
multiply(u,multiply(x,additive_inverse(y))) = sFlat4,
inference(orient,[status(thm)],[t3236]) ).
cnf(t3258,plain,
multiply(u,additive_inverse(sFlat2)) = sFlat4,
inference(step,[status(thm)],[t231,t321]) ).
cnf(t330,plain,
multiply(u,additive_inverse(sFlat2)) = sFlat4,
inference(rw,[status(thm)],[t3258]) ).
cnf(t339,plain,
multiply(u,additive_inverse(sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t330]) ).
cnf(t25,axiom,
sFlat5 = add(multiply(multiply(u,x),y),additive_inverse(multiply(u,multiply(x,y)))),
introduced(definition) ).
cnf(t3213,plain,
sFlat5 = add(multiply(sFlat0,y),additive_inverse(multiply(u,multiply(x,y)))),
inference(step,[status(thm)],[t25,t165]) ).
cnf(t3214,plain,
sFlat5 = add(multiply(sFlat0,y),multiply(u,additive_inverse(multiply(x,y)))),
inference(step,[status(thm)],[t3213,t61]) ).
cnf(t3215,plain,
sFlat5 = add(multiply(sFlat0,y),multiply(u,multiply(x,additive_inverse(y)))),
inference(step,[status(thm)],[t3214,t61]) ).
cnf(t214,plain,
add(multiply(sFlat0,y),multiply(u,multiply(x,additive_inverse(y)))) = sFlat5,
inference(orient,[status(thm)],[t3215]) ).
cnf(t3237,plain,
add(multiply(sFlat0,y),sFlat4) = sFlat5,
inference(step,[status(thm)],[t214,t231]) ).
cnf(t239,plain,
add(multiply(sFlat0,y),sFlat4) = sFlat5,
inference(rw,[status(thm)],[t3237]) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t194,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t3267,plain,
add(sFlat4,multiply(sFlat0,y)) = sFlat5,
inference(step,[status(thm)],[t239,t194]) ).
cnf(t3268,plain,
add(sFlat4,sFlat1) = sFlat5,
inference(step,[status(thm)],[t3267,t285]) ).
cnf(t3269,plain,
add(sFlat1,sFlat4) = sFlat5,
inference(step,[status(thm)],[t3268,t194]) ).
cnf(t643,plain,
add(sFlat1,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t3269]) ).
cnf(t644,plain,
add(sFlat1,add(sFlat4,X1)) = add(sFlat5,X1),
inference(cp,[status(thm)],[t200,t643]) ).
cnf(t815,plain,
add(sFlat1,add(sFlat4,X1)) = add(sFlat5,X1),
inference(orient,[status(thm)],[t644]) ).
cnf(t26,axiom,
sFlat6 = multiply(v,x),
introduced(definition) ).
cnf(t182,plain,
multiply(v,x) = sFlat6,
inference(orient,[status(thm)],[t26]) ).
cnf(t27,axiom,
sFlat7 = multiply(multiply(v,x),y),
introduced(definition) ).
cnf(t78,plain,
multiply(multiply(v,x),y) = sFlat7,
inference(orient,[status(thm)],[t27]) ).
cnf(t3208,plain,
multiply(sFlat6,y) = sFlat7,
inference(step,[status(thm)],[t78,t182]) ).
cnf(t190,plain,
multiply(sFlat6,y) = sFlat7,
inference(rw,[status(thm)],[t3208]) ).
cnf(t293,plain,
multiply(sFlat6,y) = sFlat7,
inference(orient,[status(thm)],[t190]) ).
cnf(t29,axiom,
sFlat9 = additive_inverse(multiply(v,multiply(x,y))),
introduced(definition) ).
cnf(t3239,plain,
sFlat9 = multiply(v,additive_inverse(multiply(x,y))),
inference(step,[status(thm)],[t29,t61]) ).
cnf(t3240,plain,
sFlat9 = multiply(v,multiply(x,additive_inverse(y))),
inference(step,[status(thm)],[t3239,t61]) ).
cnf(t241,plain,
multiply(v,multiply(x,additive_inverse(y))) = sFlat9,
inference(orient,[status(thm)],[t3240]) ).
cnf(t3257,plain,
multiply(v,additive_inverse(sFlat2)) = sFlat9,
inference(step,[status(thm)],[t241,t321]) ).
cnf(t329,plain,
multiply(v,additive_inverse(sFlat2)) = sFlat9,
inference(rw,[status(thm)],[t3257]) ).
cnf(t331,plain,
multiply(v,additive_inverse(sFlat2)) = sFlat9,
inference(orient,[status(thm)],[t329]) ).
cnf(t30,axiom,
sFlat10 = add(multiply(multiply(v,x),y),additive_inverse(multiply(v,multiply(x,y)))),
introduced(definition) ).
cnf(t3216,plain,
sFlat10 = add(multiply(sFlat6,y),additive_inverse(multiply(v,multiply(x,y)))),
inference(step,[status(thm)],[t30,t182]) ).
cnf(t3217,plain,
sFlat10 = add(multiply(sFlat6,y),multiply(v,additive_inverse(multiply(x,y)))),
inference(step,[status(thm)],[t3216,t61]) ).
cnf(t3218,plain,
sFlat10 = add(multiply(sFlat6,y),multiply(v,multiply(x,additive_inverse(y)))),
inference(step,[status(thm)],[t3217,t61]) ).
cnf(t216,plain,
add(multiply(sFlat6,y),multiply(v,multiply(x,additive_inverse(y)))) = sFlat10,
inference(orient,[status(thm)],[t3218]) ).
cnf(t3241,plain,
add(multiply(sFlat6,y),sFlat9) = sFlat10,
inference(step,[status(thm)],[t216,t241]) ).
cnf(t249,plain,
add(multiply(sFlat6,y),sFlat9) = sFlat10,
inference(rw,[status(thm)],[t3241]) ).
cnf(t3270,plain,
add(sFlat9,multiply(sFlat6,y)) = sFlat10,
inference(step,[status(thm)],[t249,t194]) ).
cnf(t3271,plain,
add(sFlat9,sFlat7) = sFlat10,
inference(step,[status(thm)],[t3270,t293]) ).
cnf(t3272,plain,
add(sFlat7,sFlat9) = sFlat10,
inference(step,[status(thm)],[t3271,t194]) ).
cnf(t645,plain,
add(sFlat7,sFlat9) = sFlat10,
inference(orient,[status(thm)],[t3272]) ).
cnf(t32,axiom,
sFlat12 = add(u,v),
introduced(definition) ).
cnf(t3228,plain,
sFlat12 = add(v,u),
inference(step,[status(thm)],[t32,t194]) ).
cnf(t220,plain,
add(v,u) = sFlat12,
inference(orient,[status(thm)],[t3228]) ).
cnf(t33,axiom,
sFlat13 = multiply(add(u,v),x),
introduced(definition) ).
cnf(t118,plain,
multiply(add(u,v),x) = sFlat13,
inference(orient,[status(thm)],[t33]) ).
cnf(t199,plain,
multiply(add(u,v),x) = sFlat13,
inference(rw,[status(thm)],[t118]) ).
cnf(t3265,plain,
multiply(add(v,u),x) = sFlat13,
inference(step,[status(thm)],[t199,t194]) ).
cnf(t3266,plain,
multiply(sFlat12,x) = sFlat13,
inference(step,[status(thm)],[t3265,t220]) ).
cnf(t627,plain,
multiply(sFlat12,x) = sFlat13,
inference(orient,[status(thm)],[t3266]) ).
cnf(t34,axiom,
sFlat14 = multiply(multiply(add(u,v),x),y),
introduced(definition) ).
cnf(t68,plain,
multiply(multiply(add(u,v),x),y) = sFlat14,
inference(orient,[status(thm)],[t34]) ).
cnf(t3199,plain,
multiply(sFlat13,y) = sFlat14,
inference(step,[status(thm)],[t68,t118]) ).
cnf(t126,plain,
multiply(sFlat13,y) = sFlat14,
inference(rw,[status(thm)],[t3199]) ).
cnf(t277,plain,
multiply(sFlat13,y) = sFlat14,
inference(orient,[status(thm)],[t126]) ).
cnf(t36,axiom,
sFlat16 = additive_inverse(multiply(add(u,v),multiply(x,y))),
introduced(definition) ).
cnf(t3231,plain,
sFlat16 = multiply(add(u,v),additive_inverse(multiply(x,y))),
inference(step,[status(thm)],[t36,t61]) ).
cnf(t3232,plain,
sFlat16 = multiply(add(v,u),additive_inverse(multiply(x,y))),
inference(step,[status(thm)],[t3231,t194]) ).
cnf(t3233,plain,
sFlat16 = multiply(sFlat12,additive_inverse(multiply(x,y))),
inference(step,[status(thm)],[t3232,t220]) ).
cnf(t3234,plain,
sFlat16 = multiply(sFlat12,multiply(x,additive_inverse(y))),
inference(step,[status(thm)],[t3233,t61]) ).
cnf(t223,plain,
multiply(sFlat12,multiply(x,additive_inverse(y))) = sFlat16,
inference(orient,[status(thm)],[t3234]) ).
cnf(t226,plain,
multiply(sFlat12,additive_inverse(multiply(x,additive_inverse(y)))) = additive_inverse(sFlat16),
inference(cp,[status(thm)],[t61,t223]) ).
cnf(t3253,plain,
multiply(sFlat12,multiply(x,additive_inverse(additive_inverse(y)))) = additive_inverse(sFlat16),
inference(step,[status(thm)],[t226,t61]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t40,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t3254,plain,
multiply(sFlat12,multiply(x,y)) = additive_inverse(sFlat16),
inference(step,[status(thm)],[t3253,t40]) ).
cnf(t3255,plain,
multiply(sFlat12,sFlat2) = additive_inverse(sFlat16),
inference(step,[status(thm)],[t3254,t148]) ).
cnf(t305,plain,
multiply(sFlat12,sFlat2) = additive_inverse(sFlat16),
inference(orient,[status(thm)],[t3255]) ).
cnf(t308,plain,
multiply(sFlat12,additive_inverse(sFlat2)) = additive_inverse(additive_inverse(sFlat16)),
inference(cp,[status(thm)],[t61,t305]) ).
cnf(t3256,plain,
multiply(sFlat12,additive_inverse(sFlat2)) = sFlat16,
inference(step,[status(thm)],[t308,t40]) ).
cnf(t313,plain,
multiply(sFlat12,additive_inverse(sFlat2)) = sFlat16,
inference(orient,[status(thm)],[t3256]) ).
cnf(t5,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t206,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t210,plain,
add(X1,add(additive_inverse(X1),X2)) = add(additive_identity,X2),
inference(cp,[status(thm)],[t200,t206]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t39,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t3280,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t210,t39]) ).
cnf(t853,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t3280]) ).
cnf(t862,plain,
X1 = add(additive_inverse(X2),add(X2,X1)),
inference(cp,[status(thm)],[t853,t40]) ).
cnf(t995,plain,
add(additive_inverse(X1),add(X1,X2)) = X2,
inference(orient,[status(thm)],[t862]) ).
cnf(t858,plain,
X1 = add(X2,add(X1,additive_inverse(X2))),
inference(cp,[status(thm)],[t853,t194]) ).
cnf(t972,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(orient,[status(thm)],[t858]) ).
cnf(t980,plain,
X1 = add(additive_inverse(X2),add(X1,X2)),
inference(cp,[status(thm)],[t972,t40]) ).
cnf(t1054,plain,
add(additive_inverse(X1),add(X2,X1)) = X2,
inference(orient,[status(thm)],[t980]) ).
cnf(t244,plain,
multiply(v,additive_inverse(multiply(x,additive_inverse(y)))) = additive_inverse(sFlat9),
inference(cp,[status(thm)],[t61,t241]) ).
cnf(t3247,plain,
multiply(v,multiply(x,additive_inverse(additive_inverse(y)))) = additive_inverse(sFlat9),
inference(step,[status(thm)],[t244,t61]) ).
cnf(t3248,plain,
multiply(v,multiply(x,y)) = additive_inverse(sFlat9),
inference(step,[status(thm)],[t3247,t40]) ).
cnf(t3249,plain,
multiply(v,sFlat2) = additive_inverse(sFlat9),
inference(step,[status(thm)],[t3248,t148]) ).
cnf(t28,axiom,
sFlat8 = multiply(v,multiply(x,y)),
introduced(definition) ).
cnf(t3207,plain,
sFlat8 = multiply(v,sFlat2),
inference(step,[status(thm)],[t28,t148]) ).
cnf(t174,plain,
multiply(v,sFlat2) = sFlat8,
inference(orient,[status(thm)],[t3207]) ).
cnf(t3250,plain,
sFlat8 = additive_inverse(sFlat9),
inference(step,[status(thm)],[t3249,t174]) ).
cnf(t258,plain,
additive_inverse(sFlat9) = sFlat8,
inference(orient,[status(thm)],[t3250]) ).
cnf(t860,plain,
X1 = add(sFlat9,add(sFlat8,X1)),
inference(cp,[status(thm)],[t853,t258]) ).
cnf(t879,plain,
add(sFlat9,add(sFlat8,X1)) = X1,
inference(orient,[status(thm)],[t860]) ).
cnf(t1064,plain,
sFlat9 = add(additive_inverse(add(sFlat8,X1)),X1),
inference(cp,[status(thm)],[t1054,t879]) ).
cnf(t3297,plain,
sFlat9 = add(X1,additive_inverse(add(sFlat8,X1))),
inference(step,[status(thm)],[t1064,t194]) ).
cnf(t1465,plain,
add(X1,additive_inverse(add(sFlat8,X1))) = sFlat9,
inference(orient,[status(thm)],[t3297]) ).
cnf(t1471,plain,
additive_inverse(add(sFlat8,X1)) = add(additive_inverse(X1),sFlat9),
inference(cp,[status(thm)],[t995,t1465]) ).
cnf(t3300,plain,
additive_inverse(add(sFlat8,X1)) = add(sFlat9,additive_inverse(X1)),
inference(step,[status(thm)],[t1471,t194]) ).
cnf(t1581,plain,
additive_inverse(add(sFlat8,X1)) = add(sFlat9,additive_inverse(X1)),
inference(orient,[status(thm)],[t3300]) ).
cnf(t1592,plain,
add(sFlat9,additive_inverse(X1)) = additive_inverse(add(X1,sFlat8)),
inference(cp,[status(thm)],[t1581,t194]) ).
cnf(t1609,plain,
additive_inverse(add(X1,sFlat8)) = add(sFlat9,additive_inverse(X1)),
inference(orient,[status(thm)],[t1592]) ).
cnf(t15,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t83,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t23,axiom,
sFlat3 = multiply(u,multiply(x,y)),
introduced(definition) ).
cnf(t3205,plain,
sFlat3 = multiply(u,sFlat2),
inference(step,[status(thm)],[t23,t148]) ).
cnf(t157,plain,
multiply(u,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t3205]) ).
cnf(t158,plain,
multiply(add(u,X1),sFlat2) = add(sFlat3,multiply(X1,sFlat2)),
inference(cp,[status(thm)],[t83,t157]) ).
cnf(t2139,plain,
add(sFlat3,multiply(X1,sFlat2)) = multiply(add(u,X1),sFlat2),
inference(orient,[status(thm)],[t158]) ).
cnf(t2143,plain,
multiply(add(u,v),sFlat2) = add(sFlat3,sFlat8),
inference(cp,[status(thm)],[t2139,t174]) ).
cnf(t3315,plain,
multiply(add(v,u),sFlat2) = add(sFlat3,sFlat8),
inference(step,[status(thm)],[t2143,t194]) ).
cnf(t3316,plain,
multiply(sFlat12,sFlat2) = add(sFlat3,sFlat8),
inference(step,[status(thm)],[t3315,t220]) ).
cnf(t35,axiom,
sFlat15 = multiply(add(u,v),multiply(x,y)),
introduced(definition) ).
cnf(t110,plain,
multiply(add(u,v),multiply(x,y)) = sFlat15,
inference(orient,[status(thm)],[t35]) ).
cnf(t3204,plain,
multiply(add(u,v),sFlat2) = sFlat15,
inference(step,[status(thm)],[t110,t148]) ).
cnf(t156,plain,
multiply(add(u,v),sFlat2) = sFlat15,
inference(rw,[status(thm)],[t3204]) ).
cnf(t3259,plain,
multiply(add(v,u),sFlat2) = sFlat15,
inference(step,[status(thm)],[t156,t194]) ).
cnf(t3260,plain,
multiply(sFlat12,sFlat2) = sFlat15,
inference(step,[status(thm)],[t3259,t220]) ).
cnf(t3261,plain,
additive_inverse(sFlat16) = sFlat15,
inference(step,[status(thm)],[t3260,t305]) ).
cnf(t505,plain,
additive_inverse(sFlat16) = sFlat15,
inference(orient,[status(thm)],[t3261]) ).
cnf(t3262,plain,
multiply(sFlat12,sFlat2) = sFlat15,
inference(step,[status(thm)],[t305,t505]) ).
cnf(t506,plain,
multiply(sFlat12,sFlat2) = sFlat15,
inference(orient,[status(thm)],[t3262]) ).
cnf(t3317,plain,
sFlat15 = add(sFlat3,sFlat8),
inference(step,[status(thm)],[t3316,t506]) ).
cnf(t2166,plain,
add(sFlat3,sFlat8) = sFlat15,
inference(orient,[status(thm)],[t3317]) ).
cnf(t2167,plain,
add(sFlat9,additive_inverse(sFlat3)) = additive_inverse(sFlat15),
inference(cp,[status(thm)],[t1609,t2166]) ).
cnf(t234,plain,
multiply(u,additive_inverse(multiply(x,additive_inverse(y)))) = additive_inverse(sFlat4),
inference(cp,[status(thm)],[t61,t231]) ).
cnf(t3243,plain,
multiply(u,multiply(x,additive_inverse(additive_inverse(y)))) = additive_inverse(sFlat4),
inference(step,[status(thm)],[t234,t61]) ).
cnf(t3244,plain,
multiply(u,multiply(x,y)) = additive_inverse(sFlat4),
inference(step,[status(thm)],[t3243,t40]) ).
cnf(t3245,plain,
multiply(u,sFlat2) = additive_inverse(sFlat4),
inference(step,[status(thm)],[t3244,t148]) ).
cnf(t3246,plain,
sFlat3 = additive_inverse(sFlat4),
inference(step,[status(thm)],[t3245,t157]) ).
cnf(t251,plain,
additive_inverse(sFlat4) = sFlat3,
inference(orient,[status(thm)],[t3246]) ).
cnf(t252,plain,
sFlat4 = additive_inverse(sFlat3),
inference(cp,[status(thm)],[t40,t251]) ).
cnf(t265,plain,
additive_inverse(sFlat3) = sFlat4,
inference(orient,[status(thm)],[t252]) ).
cnf(t3318,plain,
add(sFlat9,sFlat4) = additive_inverse(sFlat15),
inference(step,[status(thm)],[t2167,t265]) ).
cnf(t3319,plain,
add(sFlat4,sFlat9) = additive_inverse(sFlat15),
inference(step,[status(thm)],[t3318,t194]) ).
cnf(t508,plain,
sFlat16 = additive_inverse(sFlat15),
inference(cp,[status(thm)],[t40,t505]) ).
cnf(t518,plain,
additive_inverse(sFlat15) = sFlat16,
inference(orient,[status(thm)],[t508]) ).
cnf(t3320,plain,
add(sFlat4,sFlat9) = sFlat16,
inference(step,[status(thm)],[t3319,t518]) ).
cnf(t2178,plain,
add(sFlat4,sFlat9) = sFlat16,
inference(orient,[status(thm)],[t3320]) ).
cnf(t2186,plain,
add(sFlat4,add(sFlat9,X1)) = add(sFlat16,X1),
inference(cp,[status(thm)],[t200,t2178]) ).
cnf(t2398,plain,
add(sFlat4,add(sFlat9,X1)) = add(sFlat16,X1),
inference(orient,[status(thm)],[t2186]) ).
cnf(t260,plain,
additive_identity = add(sFlat9,sFlat8),
inference(cp,[status(thm)],[t206,t258]) ).
cnf(t3252,plain,
additive_identity = add(sFlat8,sFlat9),
inference(step,[status(thm)],[t260,t194]) ).
cnf(t303,plain,
add(sFlat8,sFlat9) = additive_identity,
inference(orient,[status(thm)],[t3252]) ).
cnf(t304,plain,
add(sFlat8,add(sFlat9,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t200,t303]) ).
cnf(t3274,plain,
add(sFlat8,add(sFlat9,X1)) = X1,
inference(step,[status(thm)],[t304,t39]) ).
cnf(t649,plain,
add(sFlat8,add(sFlat9,X1)) = X1,
inference(orient,[status(thm)],[t3274]) ).
cnf(t650,plain,
X1 = add(sFlat8,add(X1,sFlat9)),
inference(cp,[status(thm)],[t649,t194]) ).
cnf(t659,plain,
add(sFlat8,add(X1,sFlat9)) = X1,
inference(orient,[status(thm)],[t650]) ).
cnf(t660,plain,
sFlat7 = add(sFlat8,sFlat10),
inference(cp,[status(thm)],[t659,t645]) ).
cnf(t663,plain,
add(sFlat8,sFlat10) = sFlat7,
inference(orient,[status(thm)],[t660]) ).
cnf(t664,plain,
add(sFlat8,add(sFlat10,X1)) = add(sFlat7,X1),
inference(cp,[status(thm)],[t200,t663]) ).
cnf(t826,plain,
add(sFlat8,add(sFlat10,X1)) = add(sFlat7,X1),
inference(orient,[status(thm)],[t664]) ).
cnf(t880,plain,
add(sFlat10,X1) = add(sFlat9,add(sFlat7,X1)),
inference(cp,[status(thm)],[t879,t826]) ).
cnf(t926,plain,
add(sFlat9,add(sFlat7,X1)) = add(sFlat10,X1),
inference(orient,[status(thm)],[t880]) ).
cnf(t934,plain,
add(sFlat10,X1) = add(sFlat9,add(X1,sFlat7)),
inference(cp,[status(thm)],[t926,t194]) ).
cnf(t956,plain,
add(sFlat9,add(X1,sFlat7)) = add(sFlat10,X1),
inference(orient,[status(thm)],[t934]) ).
cnf(t286,plain,
multiply(add(sFlat0,X1),y) = add(sFlat1,multiply(X1,y)),
inference(cp,[status(thm)],[t83,t285]) ).
cnf(t3143,plain,
add(sFlat1,multiply(X1,y)) = multiply(add(sFlat0,X1),y),
inference(orient,[status(thm)],[t286]) ).
cnf(t3152,plain,
multiply(add(sFlat0,sFlat6),y) = add(sFlat1,sFlat7),
inference(cp,[status(thm)],[t3143,t293]) ).
cnf(t166,plain,
multiply(add(u,X1),x) = add(sFlat0,multiply(X1,x)),
inference(cp,[status(thm)],[t83,t165]) ).
cnf(t2859,plain,
add(sFlat0,multiply(X1,x)) = multiply(add(u,X1),x),
inference(orient,[status(thm)],[t166]) ).
cnf(t2864,plain,
multiply(add(u,v),x) = add(sFlat0,sFlat6),
inference(cp,[status(thm)],[t2859,t182]) ).
cnf(t3363,plain,
multiply(add(v,u),x) = add(sFlat0,sFlat6),
inference(step,[status(thm)],[t2864,t194]) ).
cnf(t3364,plain,
multiply(sFlat12,x) = add(sFlat0,sFlat6),
inference(step,[status(thm)],[t3363,t220]) ).
cnf(t3365,plain,
sFlat13 = add(sFlat0,sFlat6),
inference(step,[status(thm)],[t3364,t627]) ).
cnf(t2885,plain,
add(sFlat0,sFlat6) = sFlat13,
inference(orient,[status(thm)],[t3365]) ).
cnf(t3382,plain,
multiply(sFlat13,y) = add(sFlat1,sFlat7),
inference(step,[status(thm)],[t3152,t2885]) ).
cnf(t3383,plain,
sFlat14 = add(sFlat1,sFlat7),
inference(step,[status(thm)],[t3382,t277]) ).
cnf(t3163,plain,
add(sFlat1,sFlat7) = sFlat14,
inference(orient,[status(thm)],[t3383]) ).
cnf(t3166,plain,
add(sFlat10,sFlat1) = add(sFlat9,sFlat14),
inference(cp,[status(thm)],[t956,t3163]) ).
cnf(t3384,plain,
add(sFlat1,sFlat10) = add(sFlat9,sFlat14),
inference(step,[status(thm)],[t3166,t194]) ).
cnf(t3171,plain,
add(sFlat9,sFlat14) = add(sFlat1,sFlat10),
inference(orient,[status(thm)],[t3384]) ).
cnf(t3173,plain,
add(sFlat16,sFlat14) = add(sFlat4,add(sFlat1,sFlat10)),
inference(cp,[status(thm)],[t2398,t3171]) ).
cnf(t3385,plain,
add(sFlat14,sFlat16) = add(sFlat4,add(sFlat1,sFlat10)),
inference(step,[status(thm)],[t3173,t194]) ).
cnf(t861,plain,
X1 = add(sFlat4,add(sFlat3,X1)),
inference(cp,[status(thm)],[t853,t251]) ).
cnf(t887,plain,
add(sFlat4,add(sFlat3,X1)) = X1,
inference(orient,[status(thm)],[t861]) ).
cnf(t253,plain,
additive_identity = add(sFlat4,sFlat3),
inference(cp,[status(thm)],[t206,t251]) ).
cnf(t3251,plain,
additive_identity = add(sFlat3,sFlat4),
inference(step,[status(thm)],[t253,t194]) ).
cnf(t301,plain,
add(sFlat3,sFlat4) = additive_identity,
inference(orient,[status(thm)],[t3251]) ).
cnf(t302,plain,
add(sFlat3,add(sFlat4,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t200,t301]) ).
cnf(t3273,plain,
add(sFlat3,add(sFlat4,X1)) = X1,
inference(step,[status(thm)],[t302,t39]) ).
cnf(t647,plain,
add(sFlat3,add(sFlat4,X1)) = X1,
inference(orient,[status(thm)],[t3273]) ).
cnf(t648,plain,
X1 = add(sFlat3,add(X1,sFlat4)),
inference(cp,[status(thm)],[t647,t194]) ).
cnf(t653,plain,
add(sFlat3,add(X1,sFlat4)) = X1,
inference(orient,[status(thm)],[t648]) ).
cnf(t654,plain,
sFlat1 = add(sFlat3,sFlat5),
inference(cp,[status(thm)],[t653,t643]) ).
cnf(t657,plain,
add(sFlat3,sFlat5) = sFlat1,
inference(orient,[status(thm)],[t654]) ).
cnf(t658,plain,
add(sFlat3,add(sFlat5,X1)) = add(sFlat1,X1),
inference(cp,[status(thm)],[t200,t657]) ).
cnf(t821,plain,
add(sFlat3,add(sFlat5,X1)) = add(sFlat1,X1),
inference(orient,[status(thm)],[t658]) ).
cnf(t888,plain,
add(sFlat5,X1) = add(sFlat4,add(sFlat1,X1)),
inference(cp,[status(thm)],[t887,t821]) ).
cnf(t936,plain,
add(sFlat4,add(sFlat1,X1)) = add(sFlat5,X1),
inference(orient,[status(thm)],[t888]) ).
cnf(t3386,plain,
add(sFlat14,sFlat16) = add(sFlat5,sFlat10),
inference(step,[status(thm)],[t3385,t936]) ).
cnf(t3189,plain,
add(sFlat14,sFlat16) = add(sFlat5,sFlat10),
inference(orient,[status(thm)],[t3386]) ).
cnf(u0,negated_conjecture,
associator(add(u,v),x,y) != add(associator(u,x,y),associator(v,x,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(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,t200]) ).
cnf(g0_1,plain,
add(multiply(sFlat0,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,t165]) ).
cnf(g0_2,plain,
add(sFlat1,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,t285]) ).
cnf(g0_3,plain,
add(sFlat1,add(multiply(u,additive_inverse(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_2,t61]) ).
cnf(g0_4,plain,
add(sFlat1,add(multiply(u,multiply(x,additive_inverse(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_3,t61]) ).
cnf(g0_5,plain,
add(sFlat1,add(multiply(u,additive_inverse(sFlat2)),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,t321]) ).
cnf(g0_6,plain,
add(sFlat1,add(sFlat4,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,t339]) ).
cnf(g0_7,plain,
add(sFlat5,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_6,t815]) ).
cnf(g0_8,plain,
add(sFlat5,add(multiply(sFlat6,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_7,t182]) ).
cnf(g0_9,plain,
add(sFlat5,add(sFlat7,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,t293]) ).
cnf(g0_10,plain,
add(sFlat5,add(sFlat7,multiply(v,additive_inverse(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_9,t61]) ).
cnf(g0_11,plain,
add(sFlat5,add(sFlat7,multiply(v,multiply(x,additive_inverse(y))))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_10,t61]) ).
cnf(g0_12,plain,
add(sFlat5,add(sFlat7,multiply(v,additive_inverse(sFlat2)))) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_11,t321]) ).
cnf(g0_13,plain,
add(sFlat5,add(sFlat7,sFlat9)) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_12,t331]) ).
cnf(g0_14,plain,
add(sFlat5,sFlat10) != add(multiply(multiply(add(u,v),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_13,t645]) ).
cnf(g0_15,plain,
add(sFlat5,sFlat10) != add(multiply(multiply(add(v,u),x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_14,t194]) ).
cnf(g0_16,plain,
add(sFlat5,sFlat10) != add(multiply(multiply(sFlat12,x),y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_15,t220]) ).
cnf(g0_17,plain,
add(sFlat5,sFlat10) != add(multiply(sFlat13,y),additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_16,t627]) ).
cnf(g0_18,plain,
add(sFlat5,sFlat10) != add(sFlat14,additive_inverse(multiply(add(u,v),multiply(x,y)))),
inference(rw,[status(thm)],[g0_17,t277]) ).
cnf(g0_19,plain,
add(sFlat5,sFlat10) != add(sFlat14,multiply(add(u,v),additive_inverse(multiply(x,y)))),
inference(rw,[status(thm)],[g0_18,t61]) ).
cnf(g0_20,plain,
add(sFlat5,sFlat10) != add(sFlat14,multiply(add(v,u),additive_inverse(multiply(x,y)))),
inference(rw,[status(thm)],[g0_19,t194]) ).
cnf(g0_21,plain,
add(sFlat5,sFlat10) != add(sFlat14,multiply(sFlat12,additive_inverse(multiply(x,y)))),
inference(rw,[status(thm)],[g0_20,t220]) ).
cnf(g0_22,plain,
add(sFlat5,sFlat10) != add(sFlat14,multiply(sFlat12,multiply(x,additive_inverse(y)))),
inference(rw,[status(thm)],[g0_21,t61]) ).
cnf(g0_23,plain,
add(sFlat5,sFlat10) != add(sFlat14,multiply(sFlat12,additive_inverse(sFlat2))),
inference(rw,[status(thm)],[g0_22,t321]) ).
cnf(g0_24,plain,
add(sFlat5,sFlat10) != add(sFlat14,sFlat16),
inference(rw,[status(thm)],[g0_23,t313]) ).
cnf(g0_25,plain,
add(sFlat5,sFlat10) != add(sFlat5,sFlat10),
inference(rw,[status(thm)],[g0_24,t3189]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG021-7 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/10.36 % Computer : n016.cluster.edu
% 0.09/10.36 % Model : x86_64 x86_64
% 0.09/10.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.36 % Memory : 8046.5625MB
% 0.09/10.36 % OS : Linux 6.8.0-71-generic
% 0.09/10.37 % CPULimit : 300
% 0.09/10.37 % WCLimit : 300
% 0.09/10.37 % DateTime : Thu Sep 24 07:52:08 UTC 2026
% 0.09/10.37 % CPUTime :
% 0.09/10.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.57/11.88 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.57/11.88 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------