%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG008-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 : n001.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:25 PM UTC 2026
% Result : Unsatisfiable 8.17s 1.71s
% Output : CNFRefutation 8.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 12
% Syntax : Number of clauses : 255 ( 255 unt; 0 nHn; 125 RR)
% Number of literals : 255 ( 254 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 194 ( 16 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t11,axiom,
sFlat0 = multiply(b,a),
introduced(definition) ).
cnf(t39,plain,
multiply(b,a) = sFlat0,
inference(orient,[status(thm)],[t11]) ).
cnf(t7,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t4,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t4]) ).
cnf(t22,plain,
add(X1,add(additive_inverse(X1),X2)) = add(additive_identity,X2),
inference(cp,[status(thm)],[t16,t19]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t9521,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t22,t13]) ).
cnf(t189,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t9521]) ).
cnf(t191,plain,
additive_inverse(additive_inverse(X1)) = add(X1,additive_identity),
inference(cp,[status(thm)],[t189,t19]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t9522,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(step,[status(thm)],[t191,t12]) ).
cnf(t194,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t9522]) ).
cnf(t6,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t15,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t192,plain,
X1 = add(X2,add(X1,additive_inverse(X2))),
inference(cp,[status(thm)],[t189,t15]) ).
cnf(t197,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(orient,[status(thm)],[t192]) ).
cnf(t200,plain,
X1 = add(additive_inverse(X2),add(X1,X2)),
inference(cp,[status(thm)],[t197,t194]) ).
cnf(t210,plain,
add(additive_inverse(X1),add(X2,X1)) = X2,
inference(orient,[status(thm)],[t200]) ).
cnf(t219,plain,
additive_inverse(X1) = add(additive_inverse(add(X2,X1)),X2),
inference(cp,[status(thm)],[t210,t210]) ).
cnf(t9524,plain,
additive_inverse(X1) = add(X2,additive_inverse(add(X2,X1))),
inference(step,[status(thm)],[t219,t15]) ).
cnf(t265,plain,
add(X1,additive_inverse(add(X1,X2))) = additive_inverse(X2),
inference(orient,[status(thm)],[t9524]) ).
cnf(t8,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t34,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t3,axiom,
multiply(a,b) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t45,plain,
multiply(a,b) = c,
inference(orient,[status(thm)],[t3]) ).
cnf(t46,plain,
multiply(a,multiply(b,X1)) = multiply(c,X1),
inference(cp,[status(thm)],[t34,t45]) ).
cnf(t104,plain,
multiply(a,multiply(b,X1)) = multiply(c,X1),
inference(orient,[status(thm)],[t46]) ).
cnf(t2,axiom,
multiply(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t14,plain,
multiply(X1,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t36,plain,
multiply(X1,multiply(X1,X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t34,t14]) ).
cnf(t52,plain,
multiply(X1,multiply(X1,X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t36]) ).
cnf(t110,plain,
multiply(c,multiply(b,X1)) = multiply(a,multiply(b,X1)),
inference(cp,[status(thm)],[t104,t52]) ).
cnf(t9519,plain,
multiply(c,multiply(b,X1)) = multiply(c,X1),
inference(step,[status(thm)],[t110,t104]) ).
cnf(t176,plain,
multiply(c,multiply(b,X1)) = multiply(c,X1),
inference(orient,[status(thm)],[t9519]) ).
cnf(t9,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t31,plain,
multiply(X1,add(X1,X2)) = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t28,t14]) ).
cnf(t366,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(X1,X2)),
inference(orient,[status(thm)],[t31]) ).
cnf(t35,plain,
multiply(X1,multiply(X2,multiply(X1,X2))) = multiply(X1,X2),
inference(cp,[status(thm)],[t34,t14]) ).
cnf(t1406,plain,
multiply(X1,multiply(X2,multiply(X1,X2))) = multiply(X1,X2),
inference(orient,[status(thm)],[t35]) ).
cnf(t10,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t37,plain,
multiply(add(multiply(X1,X2),X3),Y3) = add(multiply(X1,multiply(X2,Y3)),multiply(X3,Y3)),
inference(cp,[status(thm)],[t23,t34]) ).
cnf(t5945,plain,
add(multiply(X1,multiply(X2,X3)),multiply(Y3,X3)) = multiply(add(multiply(X1,X2),Y3),X3),
inference(orient,[status(thm)],[t37]) ).
cnf(t5972,plain,
multiply(add(multiply(X1,X2),X3),X2) = add(multiply(X1,X2),multiply(X3,X2)),
inference(cp,[status(thm)],[t5945,t14]) ).
cnf(t9951,plain,
multiply(add(multiply(X1,X2),X3),X2) = multiply(add(X1,X3),X2),
inference(step,[status(thm)],[t5972,t23]) ).
cnf(t7771,plain,
multiply(add(multiply(X1,X2),X3),X2) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t9951]) ).
cnf(t7788,plain,
multiply(add(X1,additive_inverse(multiply(X1,X2))),X2) = multiply(additive_identity,X2),
inference(cp,[status(thm)],[t7771,t19]) ).
cnf(t25,plain,
multiply(add(X1,X2),X1) = add(X1,multiply(X2,X1)),
inference(cp,[status(thm)],[t23,t14]) ).
cnf(t277,plain,
add(X1,multiply(X2,X1)) = multiply(add(X1,X2),X1),
inference(orient,[status(thm)],[t25]) ).
cnf(t58,plain,
multiply(X1,add(X2,multiply(X1,X3))) = add(multiply(X1,X2),multiply(X1,X3)),
inference(cp,[status(thm)],[t28,t52]) ).
cnf(t9696,plain,
multiply(X1,add(X2,multiply(X1,X3))) = multiply(X1,add(X2,X3)),
inference(step,[status(thm)],[t58,t28]) ).
cnf(t2129,plain,
multiply(X1,add(X2,multiply(X1,X3))) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t9696]) ).
cnf(t49,plain,
multiply(add(a,X1),b) = add(c,multiply(X1,b)),
inference(cp,[status(thm)],[t23,t45]) ).
cnf(t663,plain,
add(c,multiply(X1,b)) = multiply(add(a,X1),b),
inference(orient,[status(thm)],[t49]) ).
cnf(t109,plain,
multiply(c,b) = multiply(a,b),
inference(cp,[status(thm)],[t104,t14]) ).
cnf(t9510,plain,
multiply(c,b) = c,
inference(step,[status(thm)],[t109,t45]) ).
cnf(t117,plain,
multiply(c,b) = c,
inference(orient,[status(thm)],[t9510]) ).
cnf(t121,plain,
multiply(add(c,X1),b) = add(c,multiply(X1,b)),
inference(cp,[status(thm)],[t23,t117]) ).
cnf(t9579,plain,
multiply(add(c,X1),b) = multiply(add(a,X1),b),
inference(step,[status(thm)],[t121,t663]) ).
cnf(t988,plain,
multiply(add(a,X1),b) = multiply(add(c,X1),b),
inference(orient,[status(thm)],[t9579]) ).
cnf(t9580,plain,
add(c,multiply(X1,b)) = multiply(add(c,X1),b),
inference(step,[status(thm)],[t663,t988]) ).
cnf(t989,plain,
add(c,multiply(X1,b)) = multiply(add(c,X1),b),
inference(orient,[status(thm)],[t9580]) ).
cnf(t2132,plain,
multiply(X1,add(c,b)) = multiply(X1,multiply(add(c,X1),b)),
inference(cp,[status(thm)],[t2129,t989]) ).
cnf(t4678,plain,
multiply(X1,multiply(add(c,X1),b)) = multiply(X1,add(c,b)),
inference(orient,[status(thm)],[t2132]) ).
cnf(t4695,plain,
multiply(additive_identity,add(c,b)) = multiply(additive_identity,multiply(c,b)),
inference(cp,[status(thm)],[t4678,t12]) ).
cnf(t9807,plain,
multiply(additive_identity,add(c,b)) = multiply(additive_identity,c),
inference(step,[status(thm)],[t4695,t117]) ).
cnf(t4723,plain,
multiply(additive_identity,add(c,b)) = multiply(additive_identity,c),
inference(orient,[status(thm)],[t9807]) ).
cnf(t4724,plain,
multiply(add(add(c,b),additive_identity),add(c,b)) = add(add(c,b),multiply(additive_identity,c)),
inference(cp,[status(thm)],[t277,t4723]) ).
cnf(t9808,plain,
multiply(add(c,add(b,additive_identity)),add(c,b)) = add(add(c,b),multiply(additive_identity,c)),
inference(step,[status(thm)],[t4724,t16]) ).
cnf(t9809,plain,
multiply(add(c,b),add(c,b)) = add(add(c,b),multiply(additive_identity,c)),
inference(step,[status(thm)],[t9808,t12]) ).
cnf(t9810,plain,
add(c,b) = add(add(c,b),multiply(additive_identity,c)),
inference(step,[status(thm)],[t9809,t14]) ).
cnf(t9811,plain,
add(c,b) = add(c,add(b,multiply(additive_identity,c))),
inference(step,[status(thm)],[t9810,t16]) ).
cnf(t4735,plain,
add(c,add(b,multiply(additive_identity,c))) = add(c,b),
inference(orient,[status(thm)],[t9811]) ).
cnf(t4738,plain,
additive_inverse(add(b,multiply(additive_identity,c))) = add(c,additive_inverse(add(c,b))),
inference(cp,[status(thm)],[t265,t4735]) ).
cnf(t9812,plain,
additive_inverse(add(b,multiply(additive_identity,c))) = additive_inverse(b),
inference(step,[status(thm)],[t4738,t265]) ).
cnf(t4743,plain,
additive_inverse(add(b,multiply(additive_identity,c))) = additive_inverse(b),
inference(orient,[status(thm)],[t9812]) ).
cnf(t4748,plain,
additive_identity = add(add(b,multiply(additive_identity,c)),additive_inverse(b)),
inference(cp,[status(thm)],[t19,t4743]) ).
cnf(t9813,plain,
additive_identity = add(b,add(multiply(additive_identity,c),additive_inverse(b))),
inference(step,[status(thm)],[t4748,t16]) ).
cnf(t9814,plain,
additive_identity = multiply(additive_identity,c),
inference(step,[status(thm)],[t9813,t197]) ).
cnf(t4757,plain,
multiply(additive_identity,c) = additive_identity,
inference(orient,[status(thm)],[t9814]) ).
cnf(t4767,plain,
multiply(additive_identity,add(c,X1)) = add(additive_identity,multiply(additive_identity,X1)),
inference(cp,[status(thm)],[t28,t4757]) ).
cnf(t9847,plain,
multiply(additive_identity,add(c,X1)) = multiply(additive_identity,X1),
inference(step,[status(thm)],[t4767,t13]) ).
cnf(t5300,plain,
multiply(additive_identity,add(c,X1)) = multiply(additive_identity,X1),
inference(orient,[status(thm)],[t9847]) ).
cnf(t4768,plain,
multiply(additive_identity,add(X1,c)) = add(multiply(additive_identity,X1),additive_identity),
inference(cp,[status(thm)],[t28,t4757]) ).
cnf(t9849,plain,
multiply(additive_identity,add(X1,c)) = multiply(additive_identity,X1),
inference(step,[status(thm)],[t4768,t12]) ).
cnf(t5331,plain,
multiply(additive_identity,add(X1,c)) = multiply(additive_identity,X1),
inference(orient,[status(thm)],[t9849]) ).
cnf(t5333,plain,
multiply(add(add(X1,c),additive_identity),add(X1,c)) = add(add(X1,c),multiply(additive_identity,X1)),
inference(cp,[status(thm)],[t277,t5331]) ).
cnf(t9883,plain,
multiply(add(X1,add(c,additive_identity)),add(X1,c)) = add(add(X1,c),multiply(additive_identity,X1)),
inference(step,[status(thm)],[t5333,t16]) ).
cnf(t9884,plain,
multiply(add(X1,c),add(X1,c)) = add(add(X1,c),multiply(additive_identity,X1)),
inference(step,[status(thm)],[t9883,t12]) ).
cnf(t9885,plain,
add(X1,c) = add(add(X1,c),multiply(additive_identity,X1)),
inference(step,[status(thm)],[t9884,t14]) ).
cnf(t9886,plain,
add(X1,c) = add(X1,add(c,multiply(additive_identity,X1))),
inference(step,[status(thm)],[t9885,t16]) ).
cnf(t6557,plain,
add(X1,add(c,multiply(additive_identity,X1))) = add(X1,c),
inference(orient,[status(thm)],[t9886]) ).
cnf(t6600,plain,
add(c,multiply(additive_identity,additive_inverse(X1))) = add(X1,add(additive_inverse(X1),c)),
inference(cp,[status(thm)],[t189,t6557]) ).
cnf(t9887,plain,
add(c,multiply(additive_identity,additive_inverse(X1))) = c,
inference(step,[status(thm)],[t6600,t189]) ).
cnf(t6611,plain,
add(c,multiply(additive_identity,additive_inverse(X1))) = c,
inference(orient,[status(thm)],[t9887]) ).
cnf(t6616,plain,
multiply(additive_identity,multiply(additive_identity,additive_inverse(X1))) = multiply(additive_identity,c),
inference(cp,[status(thm)],[t5300,t6611]) ).
cnf(t9888,plain,
multiply(additive_identity,additive_inverse(X1)) = multiply(additive_identity,c),
inference(step,[status(thm)],[t6616,t52]) ).
cnf(t9889,plain,
multiply(additive_identity,additive_inverse(X1)) = additive_identity,
inference(step,[status(thm)],[t9888,t4757]) ).
cnf(t6626,plain,
multiply(additive_identity,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t9889]) ).
cnf(t6631,plain,
additive_identity = multiply(additive_identity,X1),
inference(cp,[status(thm)],[t6626,t194]) ).
cnf(t6641,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t6631]) ).
cnf(t9952,plain,
multiply(add(X1,additive_inverse(multiply(X1,X2))),X2) = additive_identity,
inference(step,[status(thm)],[t7788,t6641]) ).
cnf(t8005,plain,
multiply(add(X1,additive_inverse(multiply(X1,X2))),X2) = additive_identity,
inference(orient,[status(thm)],[t9952]) ).
cnf(t55,plain,
multiply(b,a) = multiply(b,sFlat0),
inference(cp,[status(thm)],[t52,t39]) ).
cnf(t9505,plain,
sFlat0 = multiply(b,sFlat0),
inference(step,[status(thm)],[t55,t39]) ).
cnf(t67,plain,
multiply(b,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t9505]) ).
cnf(t397,plain,
multiply(b,add(b,sFlat0)) = add(b,sFlat0),
inference(cp,[status(thm)],[t366,t67]) ).
cnf(t9538,plain,
multiply(b,add(sFlat0,b)) = add(b,sFlat0),
inference(step,[status(thm)],[t397,t15]) ).
cnf(t9539,plain,
multiply(b,add(sFlat0,b)) = add(sFlat0,b),
inference(step,[status(thm)],[t9538,t15]) ).
cnf(t523,plain,
multiply(b,add(sFlat0,b)) = add(sFlat0,b),
inference(orient,[status(thm)],[t9539]) ).
cnf(t8177,plain,
additive_identity = multiply(add(b,additive_inverse(add(sFlat0,b))),add(sFlat0,b)),
inference(cp,[status(thm)],[t8005,t523]) ).
cnf(t196,plain,
X1 = add(additive_inverse(X2),add(X2,X1)),
inference(cp,[status(thm)],[t189,t194]) ).
cnf(t203,plain,
add(additive_inverse(X1),add(X1,X2)) = X2,
inference(orient,[status(thm)],[t196]) ).
cnf(t213,plain,
additive_inverse(X1) = add(additive_inverse(add(X1,X2)),X2),
inference(cp,[status(thm)],[t210,t203]) ).
cnf(t9523,plain,
additive_inverse(X1) = add(X2,additive_inverse(add(X1,X2))),
inference(step,[status(thm)],[t213,t15]) ).
cnf(t222,plain,
add(X1,additive_inverse(add(X2,X1))) = additive_inverse(X2),
inference(orient,[status(thm)],[t9523]) ).
cnf(t9988,plain,
additive_identity = multiply(additive_inverse(sFlat0),add(sFlat0,b)),
inference(step,[status(thm)],[t8177,t222]) ).
cnf(t8782,plain,
multiply(additive_inverse(sFlat0),add(sFlat0,b)) = additive_identity,
inference(orient,[status(thm)],[t9988]) ).
cnf(t8785,plain,
multiply(additive_inverse(sFlat0),multiply(add(sFlat0,b),X1)) = multiply(additive_identity,X1),
inference(cp,[status(thm)],[t34,t8782]) ).
cnf(t10040,plain,
multiply(additive_inverse(sFlat0),multiply(add(sFlat0,b),X1)) = additive_identity,
inference(step,[status(thm)],[t8785,t6641]) ).
cnf(t9249,plain,
multiply(additive_inverse(sFlat0),multiply(add(sFlat0,b),X1)) = additive_identity,
inference(orient,[status(thm)],[t10040]) ).
cnf(t9276,plain,
multiply(add(sFlat0,b),additive_inverse(sFlat0)) = multiply(add(sFlat0,b),additive_identity),
inference(cp,[status(thm)],[t1406,t9249]) ).
cnf(t367,plain,
multiply(X1,add(X1,X1)) = multiply(add(X1,X1),X1),
inference(cp,[status(thm)],[t366,t277]) ).
cnf(t280,plain,
multiply(add(X1,X1),X1) = add(X1,X1),
inference(cp,[status(thm)],[t277,t14]) ).
cnf(t310,plain,
multiply(add(X1,X1),X1) = add(X1,X1),
inference(orient,[status(thm)],[t280]) ).
cnf(t9532,plain,
multiply(X1,add(X1,X1)) = add(X1,X1),
inference(step,[status(thm)],[t367,t310]) ).
cnf(t406,plain,
multiply(X1,add(X1,X1)) = add(X1,X1),
inference(orient,[status(thm)],[t9532]) ).
cnf(t8016,plain,
additive_identity = multiply(add(X1,additive_inverse(add(X1,X1))),add(X1,X1)),
inference(cp,[status(thm)],[t8005,t406]) ).
cnf(t9953,plain,
additive_identity = multiply(additive_inverse(X1),add(X1,X1)),
inference(step,[status(thm)],[t8016,t222]) ).
cnf(t2131,plain,
multiply(X1,add(X2,X2)) = multiply(X1,multiply(add(X2,X1),X2)),
inference(cp,[status(thm)],[t2129,t277]) ).
cnf(t4469,plain,
multiply(X1,multiply(add(X2,X1),X2)) = multiply(X1,add(X2,X2)),
inference(orient,[status(thm)],[t2131]) ).
cnf(t4491,plain,
multiply(additive_inverse(X1),add(X1,X1)) = multiply(additive_inverse(X1),multiply(additive_identity,X1)),
inference(cp,[status(thm)],[t4469,t19]) ).
cnf(t4580,plain,
multiply(additive_inverse(X1),add(X1,X1)) = multiply(additive_inverse(X1),multiply(additive_identity,X1)),
inference(orient,[status(thm)],[t4491]) ).
cnf(t9892,plain,
multiply(additive_inverse(X1),add(X1,X1)) = multiply(additive_inverse(X1),additive_identity),
inference(step,[status(thm)],[t4580,t6641]) ).
cnf(t6642,plain,
multiply(additive_inverse(X1),add(X1,X1)) = multiply(additive_inverse(X1),additive_identity),
inference(orient,[status(thm)],[t9892]) ).
cnf(t9954,plain,
additive_identity = multiply(additive_inverse(X1),additive_identity),
inference(step,[status(thm)],[t9953,t6642]) ).
cnf(t8717,plain,
multiply(additive_inverse(X1),additive_identity) = additive_identity,
inference(orient,[status(thm)],[t9954]) ).
cnf(t8734,plain,
additive_identity = multiply(X1,additive_identity),
inference(cp,[status(thm)],[t8717,t194]) ).
cnf(t8744,plain,
multiply(X1,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t8734]) ).
cnf(t10041,plain,
multiply(add(sFlat0,b),additive_inverse(sFlat0)) = additive_identity,
inference(step,[status(thm)],[t9276,t8744]) ).
cnf(t9277,plain,
multiply(add(sFlat0,b),additive_inverse(sFlat0)) = additive_identity,
inference(orient,[status(thm)],[t10041]) ).
cnf(t9279,plain,
multiply(add(sFlat0,b),add(add(sFlat0,b),additive_inverse(sFlat0))) = add(add(sFlat0,b),additive_identity),
inference(cp,[status(thm)],[t366,t9277]) ).
cnf(t10042,plain,
multiply(add(sFlat0,b),add(sFlat0,add(b,additive_inverse(sFlat0)))) = add(add(sFlat0,b),additive_identity),
inference(step,[status(thm)],[t9279,t16]) ).
cnf(t10043,plain,
multiply(add(sFlat0,b),b) = add(add(sFlat0,b),additive_identity),
inference(step,[status(thm)],[t10042,t197]) ).
cnf(t40,plain,
multiply(b,multiply(a,X1)) = multiply(sFlat0,X1),
inference(cp,[status(thm)],[t34,t39]) ).
cnf(t73,plain,
multiply(b,multiply(a,X1)) = multiply(sFlat0,X1),
inference(orient,[status(thm)],[t40]) ).
cnf(t74,plain,
multiply(sFlat0,b) = multiply(b,c),
inference(cp,[status(thm)],[t73,t45]) ).
cnf(t89,plain,
multiply(b,c) = multiply(sFlat0,b),
inference(orient,[status(thm)],[t74]) ).
cnf(t54,plain,
multiply(a,b) = multiply(a,c),
inference(cp,[status(thm)],[t52,t45]) ).
cnf(t9504,plain,
c = multiply(a,c),
inference(step,[status(thm)],[t54,t45]) ).
cnf(t61,plain,
multiply(a,c) = c,
inference(orient,[status(thm)],[t9504]) ).
cnf(t75,plain,
multiply(sFlat0,c) = multiply(b,c),
inference(cp,[status(thm)],[t73,t61]) ).
cnf(t9507,plain,
multiply(sFlat0,c) = multiply(sFlat0,b),
inference(step,[status(thm)],[t75,t89]) ).
cnf(t96,plain,
multiply(sFlat0,b) = multiply(sFlat0,c),
inference(orient,[status(thm)],[t9507]) ).
cnf(t9508,plain,
multiply(b,c) = multiply(sFlat0,c),
inference(step,[status(thm)],[t89,t96]) ).
cnf(t97,plain,
multiply(b,c) = multiply(sFlat0,c),
inference(orient,[status(thm)],[t9508]) ).
cnf(t393,plain,
multiply(b,add(b,c)) = add(b,multiply(sFlat0,c)),
inference(cp,[status(thm)],[t366,t97]) ).
cnf(t9596,plain,
multiply(b,add(c,b)) = add(b,multiply(sFlat0,c)),
inference(step,[status(thm)],[t393,t15]) ).
cnf(t289,plain,
multiply(add(b,sFlat0),b) = add(b,multiply(sFlat0,c)),
inference(cp,[status(thm)],[t277,t96]) ).
cnf(t9588,plain,
multiply(add(sFlat0,b),b) = add(b,multiply(sFlat0,c)),
inference(step,[status(thm)],[t289,t15]) ).
cnf(t1062,plain,
add(b,multiply(sFlat0,c)) = multiply(add(sFlat0,b),b),
inference(orient,[status(thm)],[t9588]) ).
cnf(t9597,plain,
multiply(b,add(c,b)) = multiply(add(sFlat0,b),b),
inference(step,[status(thm)],[t9596,t1062]) ).
cnf(t1103,plain,
multiply(add(sFlat0,b),b) = multiply(b,add(c,b)),
inference(orient,[status(thm)],[t9597]) ).
cnf(t10044,plain,
multiply(b,add(c,b)) = add(add(sFlat0,b),additive_identity),
inference(step,[status(thm)],[t10043,t1103]) ).
cnf(t10045,plain,
multiply(b,add(c,b)) = add(sFlat0,add(b,additive_identity)),
inference(step,[status(thm)],[t10044,t16]) ).
cnf(t10046,plain,
multiply(b,add(c,b)) = add(sFlat0,b),
inference(step,[status(thm)],[t10045,t12]) ).
cnf(t9297,plain,
multiply(b,add(c,b)) = add(sFlat0,b),
inference(orient,[status(thm)],[t10046]) ).
cnf(t9312,plain,
multiply(c,add(c,b)) = multiply(c,add(sFlat0,b)),
inference(cp,[status(thm)],[t176,t9297]) ).
cnf(t120,plain,
multiply(c,add(X1,b)) = add(multiply(c,X1),c),
inference(cp,[status(thm)],[t28,t117]) ).
cnf(t9577,plain,
multiply(c,add(X1,b)) = add(c,multiply(c,X1)),
inference(step,[status(thm)],[t120,t15]) ).
cnf(t9578,plain,
multiply(c,add(X1,b)) = multiply(c,add(c,X1)),
inference(step,[status(thm)],[t9577,t366]) ).
cnf(t964,plain,
multiply(c,add(X1,b)) = multiply(c,add(c,X1)),
inference(orient,[status(thm)],[t9578]) ).
cnf(t976,plain,
multiply(c,add(X1,b)) = multiply(c,add(X1,c)),
inference(cp,[status(thm)],[t964,t15]) ).
cnf(t1286,plain,
multiply(c,add(X1,b)) = multiply(c,add(X1,c)),
inference(orient,[status(thm)],[t976]) ).
cnf(t10051,plain,
multiply(c,add(c,c)) = multiply(c,add(sFlat0,b)),
inference(step,[status(thm)],[t9312,t1286]) ).
cnf(t10052,plain,
add(c,c) = multiply(c,add(sFlat0,b)),
inference(step,[status(thm)],[t10051,t406]) ).
cnf(t10053,plain,
add(c,c) = multiply(c,add(sFlat0,c)),
inference(step,[status(thm)],[t10052,t1286]) ).
cnf(t77,plain,
multiply(sFlat0,multiply(a,X1)) = multiply(b,multiply(a,X1)),
inference(cp,[status(thm)],[t73,t52]) ).
cnf(t9517,plain,
multiply(sFlat0,multiply(a,X1)) = multiply(sFlat0,X1),
inference(step,[status(thm)],[t77,t73]) ).
cnf(t163,plain,
multiply(sFlat0,multiply(a,X1)) = multiply(sFlat0,X1),
inference(orient,[status(thm)],[t9517]) ).
cnf(t391,plain,
multiply(a,add(a,c)) = add(a,c),
inference(cp,[status(thm)],[t366,t61]) ).
cnf(t9535,plain,
multiply(a,add(c,a)) = add(a,c),
inference(step,[status(thm)],[t391,t15]) ).
cnf(t9536,plain,
multiply(a,add(c,a)) = add(c,a),
inference(step,[status(thm)],[t9535,t15]) ).
cnf(t503,plain,
multiply(a,add(c,a)) = add(c,a),
inference(orient,[status(thm)],[t9536]) ).
cnf(t8151,plain,
additive_identity = multiply(add(a,additive_inverse(add(c,a))),add(c,a)),
inference(cp,[status(thm)],[t8005,t503]) ).
cnf(t9987,plain,
additive_identity = multiply(additive_inverse(c),add(c,a)),
inference(step,[status(thm)],[t8151,t222]) ).
cnf(t8763,plain,
multiply(additive_inverse(c),add(c,a)) = additive_identity,
inference(orient,[status(thm)],[t9987]) ).
cnf(t8766,plain,
multiply(additive_inverse(c),multiply(add(c,a),X1)) = multiply(additive_identity,X1),
inference(cp,[status(thm)],[t34,t8763]) ).
cnf(t9997,plain,
multiply(additive_inverse(c),multiply(add(c,a),X1)) = additive_identity,
inference(step,[status(thm)],[t8766,t6641]) ).
cnf(t8999,plain,
multiply(additive_inverse(c),multiply(add(c,a),X1)) = additive_identity,
inference(orient,[status(thm)],[t9997]) ).
cnf(t9026,plain,
multiply(add(c,a),additive_inverse(c)) = multiply(add(c,a),additive_identity),
inference(cp,[status(thm)],[t1406,t8999]) ).
cnf(t9998,plain,
multiply(add(c,a),additive_inverse(c)) = additive_identity,
inference(step,[status(thm)],[t9026,t8744]) ).
cnf(t9027,plain,
multiply(add(c,a),additive_inverse(c)) = additive_identity,
inference(orient,[status(thm)],[t9998]) ).
cnf(t9029,plain,
multiply(add(c,a),add(add(c,a),additive_inverse(c))) = add(add(c,a),additive_identity),
inference(cp,[status(thm)],[t366,t9027]) ).
cnf(t9999,plain,
multiply(add(c,a),add(c,add(a,additive_inverse(c)))) = add(add(c,a),additive_identity),
inference(step,[status(thm)],[t9029,t16]) ).
cnf(t10000,plain,
multiply(add(c,a),a) = add(add(c,a),additive_identity),
inference(step,[status(thm)],[t9999,t197]) ).
cnf(t107,plain,
multiply(c,a) = multiply(a,sFlat0),
inference(cp,[status(thm)],[t104,t39]) ).
cnf(t123,plain,
multiply(a,sFlat0) = multiply(c,a),
inference(orient,[status(thm)],[t107]) ).
cnf(t108,plain,
multiply(c,sFlat0) = multiply(a,sFlat0),
inference(cp,[status(thm)],[t104,t67]) ).
cnf(t9511,plain,
multiply(c,sFlat0) = multiply(c,a),
inference(step,[status(thm)],[t108,t123]) ).
cnf(t131,plain,
multiply(c,a) = multiply(c,sFlat0),
inference(orient,[status(thm)],[t9511]) ).
cnf(t9512,plain,
multiply(a,sFlat0) = multiply(c,sFlat0),
inference(step,[status(thm)],[t123,t131]) ).
cnf(t132,plain,
multiply(a,sFlat0) = multiply(c,sFlat0),
inference(orient,[status(thm)],[t9512]) ).
cnf(t387,plain,
multiply(a,add(a,sFlat0)) = add(a,multiply(c,sFlat0)),
inference(cp,[status(thm)],[t366,t132]) ).
cnf(t9592,plain,
multiply(a,add(sFlat0,a)) = add(a,multiply(c,sFlat0)),
inference(step,[status(thm)],[t387,t15]) ).
cnf(t285,plain,
multiply(add(a,c),a) = add(a,multiply(c,sFlat0)),
inference(cp,[status(thm)],[t277,t131]) ).
cnf(t9587,plain,
multiply(add(c,a),a) = add(a,multiply(c,sFlat0)),
inference(step,[status(thm)],[t285,t15]) ).
cnf(t1051,plain,
add(a,multiply(c,sFlat0)) = multiply(add(c,a),a),
inference(orient,[status(thm)],[t9587]) ).
cnf(t9593,plain,
multiply(a,add(sFlat0,a)) = multiply(add(c,a),a),
inference(step,[status(thm)],[t9592,t1051]) ).
cnf(t1091,plain,
multiply(add(c,a),a) = multiply(a,add(sFlat0,a)),
inference(orient,[status(thm)],[t9593]) ).
cnf(t10001,plain,
multiply(a,add(sFlat0,a)) = add(add(c,a),additive_identity),
inference(step,[status(thm)],[t10000,t1091]) ).
cnf(t10002,plain,
multiply(a,add(sFlat0,a)) = add(c,add(a,additive_identity)),
inference(step,[status(thm)],[t10001,t16]) ).
cnf(t10003,plain,
multiply(a,add(sFlat0,a)) = add(c,a),
inference(step,[status(thm)],[t10002,t12]) ).
cnf(t9047,plain,
multiply(a,add(sFlat0,a)) = add(c,a),
inference(orient,[status(thm)],[t10003]) ).
cnf(t9061,plain,
multiply(sFlat0,add(sFlat0,a)) = multiply(sFlat0,add(c,a)),
inference(cp,[status(thm)],[t163,t9047]) ).
cnf(t76,plain,
multiply(sFlat0,a) = multiply(b,a),
inference(cp,[status(thm)],[t73,t14]) ).
cnf(t9506,plain,
multiply(sFlat0,a) = sFlat0,
inference(step,[status(thm)],[t76,t39]) ).
cnf(t83,plain,
multiply(sFlat0,a) = sFlat0,
inference(orient,[status(thm)],[t9506]) ).
cnf(t86,plain,
multiply(sFlat0,add(X1,a)) = add(multiply(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t28,t83]) ).
cnf(t9565,plain,
multiply(sFlat0,add(X1,a)) = add(sFlat0,multiply(sFlat0,X1)),
inference(step,[status(thm)],[t86,t15]) ).
cnf(t9566,plain,
multiply(sFlat0,add(X1,a)) = multiply(sFlat0,add(sFlat0,X1)),
inference(step,[status(thm)],[t9565,t366]) ).
cnf(t833,plain,
multiply(sFlat0,add(X1,a)) = multiply(sFlat0,add(sFlat0,X1)),
inference(orient,[status(thm)],[t9566]) ).
cnf(t844,plain,
multiply(sFlat0,add(X1,a)) = multiply(sFlat0,add(X1,sFlat0)),
inference(cp,[status(thm)],[t833,t15]) ).
cnf(t1275,plain,
multiply(sFlat0,add(X1,a)) = multiply(sFlat0,add(X1,sFlat0)),
inference(orient,[status(thm)],[t844]) ).
cnf(t10008,plain,
multiply(sFlat0,add(sFlat0,sFlat0)) = multiply(sFlat0,add(c,a)),
inference(step,[status(thm)],[t9061,t1275]) ).
cnf(t10009,plain,
add(sFlat0,sFlat0) = multiply(sFlat0,add(c,a)),
inference(step,[status(thm)],[t10008,t406]) ).
cnf(t10010,plain,
add(sFlat0,sFlat0) = multiply(sFlat0,add(c,sFlat0)),
inference(step,[status(thm)],[t10009,t1275]) ).
cnf(t10011,plain,
add(sFlat0,sFlat0) = multiply(sFlat0,add(sFlat0,c)),
inference(step,[status(thm)],[t10010,t15]) ).
cnf(t9086,plain,
multiply(sFlat0,add(sFlat0,c)) = add(sFlat0,sFlat0),
inference(orient,[status(thm)],[t10011]) ).
cnf(t9114,plain,
additive_identity = multiply(add(sFlat0,additive_inverse(add(sFlat0,sFlat0))),add(sFlat0,c)),
inference(cp,[status(thm)],[t8005,t9086]) ).
cnf(t10020,plain,
additive_identity = multiply(additive_inverse(sFlat0),add(sFlat0,c)),
inference(step,[status(thm)],[t9114,t222]) ).
cnf(t9136,plain,
multiply(additive_inverse(sFlat0),add(sFlat0,c)) = additive_identity,
inference(orient,[status(thm)],[t10020]) ).
cnf(t9139,plain,
multiply(add(add(sFlat0,c),additive_inverse(sFlat0)),add(sFlat0,c)) = add(add(sFlat0,c),additive_identity),
inference(cp,[status(thm)],[t277,t9136]) ).
cnf(t10021,plain,
multiply(add(sFlat0,add(c,additive_inverse(sFlat0))),add(sFlat0,c)) = add(add(sFlat0,c),additive_identity),
inference(step,[status(thm)],[t9139,t16]) ).
cnf(t10022,plain,
multiply(c,add(sFlat0,c)) = add(add(sFlat0,c),additive_identity),
inference(step,[status(thm)],[t10021,t197]) ).
cnf(t10023,plain,
multiply(c,add(sFlat0,c)) = add(sFlat0,add(c,additive_identity)),
inference(step,[status(thm)],[t10022,t16]) ).
cnf(t10024,plain,
multiply(c,add(sFlat0,c)) = add(sFlat0,c),
inference(step,[status(thm)],[t10023,t12]) ).
cnf(t9156,plain,
multiply(c,add(sFlat0,c)) = add(sFlat0,c),
inference(orient,[status(thm)],[t10024]) ).
cnf(t10054,plain,
add(c,c) = add(sFlat0,c),
inference(step,[status(thm)],[t10053,t9156]) ).
cnf(t9337,plain,
add(c,c) = add(sFlat0,c),
inference(orient,[status(thm)],[t10054]) ).
cnf(t9367,plain,
additive_inverse(c) = add(c,additive_inverse(add(sFlat0,c))),
inference(cp,[status(thm)],[t265,t9337]) ).
cnf(t10102,plain,
additive_inverse(c) = additive_inverse(sFlat0),
inference(step,[status(thm)],[t9367,t222]) ).
cnf(t9383,plain,
additive_inverse(c) = additive_inverse(sFlat0),
inference(orient,[status(thm)],[t10102]) ).
cnf(t9386,plain,
c = additive_inverse(additive_inverse(sFlat0)),
inference(cp,[status(thm)],[t194,t9383]) ).
cnf(t10109,plain,
c = sFlat0,
inference(step,[status(thm)],[t9386,t194]) ).
cnf(t9400,plain,
c = sFlat0,
inference(orient,[status(thm)],[t10109]) ).
cnf(goal_0,negated_conjecture,
multiply(b,a) != c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
sFlat0 != c,
inference(rw,[status(thm)],[goal_0,t39]) ).
cnf(g0_1,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_0,t9400]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG008-7 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 07:49:22 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.17/1.71 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.17/1.71 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------