%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG026-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:31 PM UTC 2026
% Result : Unsatisfiable 16.40s 2.81s
% Output : CNFRefutation 16.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 32
% Syntax : Number of clauses : 275 ( 275 unt; 0 nHn; 223 RR)
% Number of literals : 275 ( 274 equ; 59 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 25 con; 0-3 aty)
% Number of variables : 80 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t11,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t72,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t20,axiom,
sF0 = multiply(a,b),
introduced(definition) ).
cnf(t54,plain,
multiply(a,b) = sF0,
inference(orient,[status(thm)],[t20]) ).
cnf(t21,axiom,
sF1 = multiply(multiply(a,b),c),
introduced(definition) ).
cnf(t7491,plain,
sF1 = multiply(sF0,c),
inference(step,[status(thm)],[t21,t54]) ).
cnf(t86,plain,
multiply(sF0,c) = sF1,
inference(orient,[status(thm)],[t7491]) ).
cnf(t22,axiom,
sF2 = multiply(multiply(multiply(a,b),c),d),
introduced(definition) ).
cnf(t7534,plain,
sF2 = multiply(multiply(sF0,c),d),
inference(step,[status(thm)],[t22,t54]) ).
cnf(t7535,plain,
sF2 = multiply(sF1,d),
inference(step,[status(thm)],[t7534,t86]) ).
cnf(t601,plain,
multiply(sF1,d) = sF2,
inference(orient,[status(thm)],[t7535]) ).
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(t23,axiom,
sF3 = multiply(c,d),
introduced(definition) ).
cnf(t55,plain,
multiply(c,d) = sF3,
inference(orient,[status(thm)],[t23]) ).
cnf(t63,plain,
multiply(c,additive_inverse(d)) = additive_inverse(sF3),
inference(cp,[status(thm)],[t61,t55]) ).
cnf(t70,plain,
multiply(c,additive_inverse(d)) = additive_inverse(sF3),
inference(orient,[status(thm)],[t63]) ).
cnf(t24,axiom,
sF4 = multiply(multiply(a,b),multiply(c,d)),
introduced(definition) ).
cnf(t7536,plain,
sF4 = multiply(sF0,multiply(c,d)),
inference(step,[status(thm)],[t24,t54]) ).
cnf(t7537,plain,
sF4 = multiply(sF0,sF3),
inference(step,[status(thm)],[t7536,t55]) ).
cnf(t643,plain,
multiply(sF0,sF3) = sF4,
inference(orient,[status(thm)],[t7537]) ).
cnf(t644,plain,
multiply(sF0,additive_inverse(sF3)) = additive_inverse(sF4),
inference(cp,[status(thm)],[t61,t643]) ).
cnf(t653,plain,
multiply(sF0,additive_inverse(sF3)) = additive_inverse(sF4),
inference(orient,[status(thm)],[t644]) ).
cnf(t25,axiom,
sF5 = additive_inverse(multiply(multiply(a,b),multiply(c,d))),
introduced(definition) ).
cnf(t7540,plain,
sF5 = multiply(multiply(a,b),additive_inverse(multiply(c,d))),
inference(step,[status(thm)],[t25,t61]) ).
cnf(t7541,plain,
sF5 = multiply(sF0,additive_inverse(multiply(c,d))),
inference(step,[status(thm)],[t7540,t54]) ).
cnf(t7542,plain,
sF5 = multiply(sF0,multiply(c,additive_inverse(d))),
inference(step,[status(thm)],[t7541,t61]) ).
cnf(t7543,plain,
sF5 = multiply(sF0,additive_inverse(sF3)),
inference(step,[status(thm)],[t7542,t70]) ).
cnf(t7544,plain,
sF5 = additive_inverse(sF4),
inference(step,[status(thm)],[t7543,t653]) ).
cnf(t702,plain,
additive_inverse(sF4) = sF5,
inference(orient,[status(thm)],[t7544]) ).
cnf(t7545,plain,
multiply(sF0,additive_inverse(sF3)) = sF5,
inference(step,[status(thm)],[t653,t702]) ).
cnf(t703,plain,
multiply(sF0,additive_inverse(sF3)) = sF5,
inference(orient,[status(thm)],[t7545]) ).
cnf(t26,axiom,
sF6 = add(multiply(multiply(multiply(a,b),c),d),additive_inverse(multiply(multiply(a,b),multiply(c,d)))),
introduced(definition) ).
cnf(t7553,plain,
sF6 = add(multiply(multiply(sF0,c),d),additive_inverse(multiply(multiply(a,b),multiply(c,d)))),
inference(step,[status(thm)],[t26,t54]) ).
cnf(t7554,plain,
sF6 = add(multiply(sF1,d),additive_inverse(multiply(multiply(a,b),multiply(c,d)))),
inference(step,[status(thm)],[t7553,t86]) ).
cnf(t7555,plain,
sF6 = add(sF2,additive_inverse(multiply(multiply(a,b),multiply(c,d)))),
inference(step,[status(thm)],[t7554,t601]) ).
cnf(t7556,plain,
sF6 = add(sF2,multiply(multiply(a,b),additive_inverse(multiply(c,d)))),
inference(step,[status(thm)],[t7555,t61]) ).
cnf(t7557,plain,
sF6 = add(sF2,multiply(sF0,additive_inverse(multiply(c,d)))),
inference(step,[status(thm)],[t7556,t54]) ).
cnf(t7558,plain,
sF6 = add(sF2,multiply(sF0,multiply(c,additive_inverse(d)))),
inference(step,[status(thm)],[t7557,t61]) ).
cnf(t7559,plain,
sF6 = add(sF2,multiply(sF0,additive_inverse(sF3))),
inference(step,[status(thm)],[t7558,t70]) ).
cnf(t7560,plain,
sF6 = add(sF2,sF5),
inference(step,[status(thm)],[t7559,t703]) ).
cnf(t780,plain,
add(sF2,sF5) = sF6,
inference(orient,[status(thm)],[t7560]) ).
cnf(t782,plain,
add(sF2,add(sF5,X1)) = add(sF6,X1),
inference(cp,[status(thm)],[t72,t780]) ).
cnf(t997,plain,
add(sF2,add(sF5,X1)) = add(sF6,X1),
inference(orient,[status(thm)],[t782]) ).
cnf(t27,axiom,
sF7 = multiply(b,multiply(c,d)),
introduced(definition) ).
cnf(t7492,plain,
sF7 = multiply(b,sF3),
inference(step,[status(thm)],[t27,t55]) ).
cnf(t95,plain,
multiply(b,sF3) = sF7,
inference(orient,[status(thm)],[t7492]) ).
cnf(t96,plain,
multiply(b,additive_inverse(sF3)) = additive_inverse(sF7),
inference(cp,[status(thm)],[t61,t95]) ).
cnf(t98,plain,
multiply(b,additive_inverse(sF3)) = additive_inverse(sF7),
inference(orient,[status(thm)],[t96]) ).
cnf(t39,axiom,
sF19 = additive_inverse(multiply(b,multiply(c,d))),
introduced(definition) ).
cnf(t7657,plain,
sF19 = multiply(b,additive_inverse(multiply(c,d))),
inference(step,[status(thm)],[t39,t61]) ).
cnf(t7658,plain,
sF19 = multiply(b,multiply(c,additive_inverse(d))),
inference(step,[status(thm)],[t7657,t61]) ).
cnf(t7659,plain,
sF19 = multiply(b,additive_inverse(sF3)),
inference(step,[status(thm)],[t7658,t70]) ).
cnf(t7660,plain,
sF19 = additive_inverse(sF7),
inference(step,[status(thm)],[t7659,t98]) ).
cnf(t1337,plain,
additive_inverse(sF7) = sF19,
inference(orient,[status(thm)],[t7660]) ).
cnf(t7661,plain,
multiply(b,additive_inverse(sF3)) = sF19,
inference(step,[status(thm)],[t98,t1337]) ).
cnf(t1338,plain,
multiply(b,additive_inverse(sF3)) = sF19,
inference(orient,[status(thm)],[t7661]) ).
cnf(t28,axiom,
sF8 = multiply(a,multiply(b,multiply(c,d))),
introduced(definition) ).
cnf(t7568,plain,
sF8 = multiply(a,multiply(b,sF3)),
inference(step,[status(thm)],[t28,t55]) ).
cnf(t7569,plain,
sF8 = multiply(a,sF7),
inference(step,[status(thm)],[t7568,t95]) ).
cnf(t851,plain,
multiply(a,sF7) = sF8,
inference(orient,[status(thm)],[t7569]) ).
cnf(t852,plain,
multiply(a,additive_inverse(sF7)) = additive_inverse(sF8),
inference(cp,[status(thm)],[t61,t851]) ).
cnf(t861,plain,
multiply(a,additive_inverse(sF7)) = additive_inverse(sF8),
inference(orient,[status(thm)],[t852]) ).
cnf(t29,axiom,
sF9 = additive_inverse(multiply(a,multiply(b,multiply(c,d)))),
introduced(definition) ).
cnf(t7576,plain,
sF9 = multiply(a,additive_inverse(multiply(b,multiply(c,d)))),
inference(step,[status(thm)],[t29,t61]) ).
cnf(t7577,plain,
sF9 = multiply(a,multiply(b,additive_inverse(multiply(c,d)))),
inference(step,[status(thm)],[t7576,t61]) ).
cnf(t7578,plain,
sF9 = multiply(a,multiply(b,multiply(c,additive_inverse(d)))),
inference(step,[status(thm)],[t7577,t61]) ).
cnf(t7579,plain,
sF9 = multiply(a,multiply(b,additive_inverse(sF3))),
inference(step,[status(thm)],[t7578,t70]) ).
cnf(t7580,plain,
sF9 = multiply(a,additive_inverse(sF7)),
inference(step,[status(thm)],[t7579,t98]) ).
cnf(t7581,plain,
sF9 = additive_inverse(sF8),
inference(step,[status(thm)],[t7580,t861]) ).
cnf(t910,plain,
additive_inverse(sF8) = sF9,
inference(orient,[status(thm)],[t7581]) ).
cnf(t7582,plain,
multiply(a,additive_inverse(sF7)) = sF9,
inference(step,[status(thm)],[t861,t910]) ).
cnf(t911,plain,
multiply(a,additive_inverse(sF7)) = sF9,
inference(orient,[status(thm)],[t7582]) ).
cnf(t7663,plain,
multiply(a,sF19) = sF9,
inference(step,[status(thm)],[t911,t1337]) ).
cnf(t1340,plain,
multiply(a,sF19) = sF9,
inference(rw,[status(thm)],[t7663]) ).
cnf(t1367,plain,
multiply(a,sF19) = sF9,
inference(orient,[status(thm)],[t1340]) ).
cnf(t30,axiom,
sF10 = add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),
introduced(definition) ).
cnf(t7584,plain,
sF10 = add(multiply(sF0,multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),
inference(step,[status(thm)],[t30,t54]) ).
cnf(t7585,plain,
sF10 = add(multiply(sF0,sF3),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),
inference(step,[status(thm)],[t7584,t55]) ).
cnf(t7586,plain,
sF10 = add(sF4,additive_inverse(multiply(a,multiply(b,multiply(c,d))))),
inference(step,[status(thm)],[t7585,t643]) ).
cnf(t7587,plain,
sF10 = add(sF4,multiply(a,additive_inverse(multiply(b,multiply(c,d))))),
inference(step,[status(thm)],[t7586,t61]) ).
cnf(t7588,plain,
sF10 = add(sF4,multiply(a,multiply(b,additive_inverse(multiply(c,d))))),
inference(step,[status(thm)],[t7587,t61]) ).
cnf(t7589,plain,
sF10 = add(sF4,multiply(a,multiply(b,multiply(c,additive_inverse(d))))),
inference(step,[status(thm)],[t7588,t61]) ).
cnf(t7590,plain,
sF10 = add(sF4,multiply(a,multiply(b,additive_inverse(sF3)))),
inference(step,[status(thm)],[t7589,t70]) ).
cnf(t7591,plain,
sF10 = add(sF4,multiply(a,additive_inverse(sF7))),
inference(step,[status(thm)],[t7590,t98]) ).
cnf(t7592,plain,
sF10 = add(sF4,sF9),
inference(step,[status(thm)],[t7591,t911]) ).
cnf(t986,plain,
add(sF4,sF9) = sF10,
inference(orient,[status(thm)],[t7592]) ).
cnf(t988,plain,
add(sF4,add(sF9,X1)) = add(sF10,X1),
inference(cp,[status(thm)],[t72,t986]) ).
cnf(t1218,plain,
add(sF4,add(sF9,X1)) = add(sF10,X1),
inference(orient,[status(thm)],[t988]) ).
cnf(t31,axiom,
sF11 = add(add(multiply(multiply(multiply(a,b),c),d),additive_inverse(multiply(multiply(a,b),multiply(c,d)))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d)))))),
introduced(definition) ).
cnf(t7596,plain,
sF11 = add(multiply(multiply(multiply(a,b),c),d),add(additive_inverse(multiply(multiply(a,b),multiply(c,d))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t31,t72]) ).
cnf(t7597,plain,
sF11 = add(multiply(multiply(sF0,c),d),add(additive_inverse(multiply(multiply(a,b),multiply(c,d))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t7596,t54]) ).
cnf(t7598,plain,
sF11 = add(multiply(sF1,d),add(additive_inverse(multiply(multiply(a,b),multiply(c,d))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t7597,t86]) ).
cnf(t7599,plain,
sF11 = add(sF2,add(additive_inverse(multiply(multiply(a,b),multiply(c,d))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t7598,t601]) ).
cnf(t7600,plain,
sF11 = add(sF2,add(multiply(multiply(a,b),additive_inverse(multiply(c,d))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t7599,t61]) ).
cnf(t7601,plain,
sF11 = add(sF2,add(multiply(sF0,additive_inverse(multiply(c,d))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t7600,t54]) ).
cnf(t7602,plain,
sF11 = add(sF2,add(multiply(sF0,multiply(c,additive_inverse(d))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t7601,t61]) ).
cnf(t7603,plain,
sF11 = add(sF2,add(multiply(sF0,additive_inverse(sF3)),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t7602,t70]) ).
cnf(t7604,plain,
sF11 = add(sF2,add(sF5,add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t7603,t703]) ).
cnf(t7605,plain,
sF11 = add(sF6,add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d)))))),
inference(step,[status(thm)],[t7604,t997]) ).
cnf(t7606,plain,
sF11 = add(sF6,add(multiply(sF0,multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d)))))),
inference(step,[status(thm)],[t7605,t54]) ).
cnf(t7607,plain,
sF11 = add(sF6,add(multiply(sF0,sF3),additive_inverse(multiply(a,multiply(b,multiply(c,d)))))),
inference(step,[status(thm)],[t7606,t55]) ).
cnf(t7608,plain,
sF11 = add(sF6,add(sF4,additive_inverse(multiply(a,multiply(b,multiply(c,d)))))),
inference(step,[status(thm)],[t7607,t643]) ).
cnf(t7609,plain,
sF11 = add(sF6,add(sF4,multiply(a,additive_inverse(multiply(b,multiply(c,d)))))),
inference(step,[status(thm)],[t7608,t61]) ).
cnf(t7610,plain,
sF11 = add(sF6,add(sF4,multiply(a,multiply(b,additive_inverse(multiply(c,d)))))),
inference(step,[status(thm)],[t7609,t61]) ).
cnf(t7611,plain,
sF11 = add(sF6,add(sF4,multiply(a,multiply(b,multiply(c,additive_inverse(d)))))),
inference(step,[status(thm)],[t7610,t61]) ).
cnf(t7612,plain,
sF11 = add(sF6,add(sF4,multiply(a,multiply(b,additive_inverse(sF3))))),
inference(step,[status(thm)],[t7611,t70]) ).
cnf(t7613,plain,
sF11 = add(sF6,add(sF4,multiply(a,additive_inverse(sF7)))),
inference(step,[status(thm)],[t7612,t98]) ).
cnf(t7614,plain,
sF11 = add(sF6,add(sF4,sF9)),
inference(step,[status(thm)],[t7613,t911]) ).
cnf(t7615,plain,
sF11 = add(sF6,sF10),
inference(step,[status(thm)],[t7614,t986]) ).
cnf(t1013,plain,
add(sF6,sF10) = sF11,
inference(orient,[status(thm)],[t7615]) ).
cnf(t1015,plain,
add(sF6,add(sF10,X1)) = add(sF11,X1),
inference(cp,[status(thm)],[t72,t1013]) ).
cnf(t1567,plain,
add(sF6,add(sF10,X1)) = add(sF11,X1),
inference(orient,[status(thm)],[t1015]) ).
cnf(t32,axiom,
sF12 = multiply(b,c),
introduced(definition) ).
cnf(t56,plain,
multiply(b,c) = sF12,
inference(orient,[status(thm)],[t32]) ).
cnf(t33,axiom,
sF13 = multiply(a,multiply(b,c)),
introduced(definition) ).
cnf(t7493,plain,
sF13 = multiply(a,sF12),
inference(step,[status(thm)],[t33,t56]) ).
cnf(t99,plain,
multiply(a,sF12) = sF13,
inference(orient,[status(thm)],[t7493]) ).
cnf(t34,axiom,
sF14 = multiply(multiply(a,multiply(b,c)),d),
introduced(definition) ).
cnf(t7619,plain,
sF14 = multiply(multiply(a,sF12),d),
inference(step,[status(thm)],[t34,t56]) ).
cnf(t7620,plain,
sF14 = multiply(sF13,d),
inference(step,[status(thm)],[t7619,t99]) ).
cnf(t1074,plain,
multiply(sF13,d) = sF14,
inference(orient,[status(thm)],[t7620]) ).
cnf(t14,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t110,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t145,plain,
add(multiply(X1,X2),add(multiply(X1,X3),Y3)) = add(multiply(X1,add(X2,X3)),Y3),
inference(cp,[status(thm)],[t72,t110]) ).
cnf(t6056,plain,
add(multiply(X1,X2),add(multiply(X1,X3),Y3)) = add(multiply(X1,add(X2,X3)),Y3),
inference(orient,[status(thm)],[t145]) ).
cnf(t64,plain,
multiply(b,additive_inverse(c)) = additive_inverse(sF12),
inference(cp,[status(thm)],[t61,t56]) ).
cnf(t71,plain,
multiply(b,additive_inverse(c)) = additive_inverse(sF12),
inference(orient,[status(thm)],[t64]) ).
cnf(t100,plain,
multiply(a,additive_inverse(sF12)) = additive_inverse(sF13),
inference(cp,[status(thm)],[t61,t99]) ).
cnf(t102,plain,
multiply(a,additive_inverse(sF12)) = additive_inverse(sF13),
inference(orient,[status(thm)],[t100]) ).
cnf(t43,axiom,
sF23 = additive_inverse(multiply(a,multiply(b,c))),
introduced(definition) ).
cnf(t7697,plain,
sF23 = multiply(a,additive_inverse(multiply(b,c))),
inference(step,[status(thm)],[t43,t61]) ).
cnf(t7698,plain,
sF23 = multiply(a,multiply(b,additive_inverse(c))),
inference(step,[status(thm)],[t7697,t61]) ).
cnf(t7699,plain,
sF23 = multiply(a,additive_inverse(sF12)),
inference(step,[status(thm)],[t7698,t71]) ).
cnf(t7700,plain,
sF23 = additive_inverse(sF13),
inference(step,[status(thm)],[t7699,t102]) ).
cnf(t1584,plain,
additive_inverse(sF13) = sF23,
inference(orient,[status(thm)],[t7700]) ).
cnf(t7701,plain,
multiply(a,additive_inverse(sF12)) = sF23,
inference(step,[status(thm)],[t102,t1584]) ).
cnf(t1585,plain,
multiply(a,additive_inverse(sF12)) = sF23,
inference(orient,[status(thm)],[t7701]) ).
cnf(t44,axiom,
sF24 = add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),
introduced(definition) ).
cnf(t7703,plain,
sF24 = add(multiply(sF0,c),additive_inverse(multiply(a,multiply(b,c)))),
inference(step,[status(thm)],[t44,t54]) ).
cnf(t7704,plain,
sF24 = add(sF1,additive_inverse(multiply(a,multiply(b,c)))),
inference(step,[status(thm)],[t7703,t86]) ).
cnf(t7705,plain,
sF24 = add(sF1,multiply(a,additive_inverse(multiply(b,c)))),
inference(step,[status(thm)],[t7704,t61]) ).
cnf(t7706,plain,
sF24 = add(sF1,multiply(a,multiply(b,additive_inverse(c)))),
inference(step,[status(thm)],[t7705,t61]) ).
cnf(t7707,plain,
sF24 = add(sF1,multiply(a,additive_inverse(sF12))),
inference(step,[status(thm)],[t7706,t71]) ).
cnf(t7708,plain,
sF24 = add(sF1,sF23),
inference(step,[status(thm)],[t7707,t1585]) ).
cnf(t1668,plain,
add(sF1,sF23) = sF24,
inference(orient,[status(thm)],[t7708]) ).
cnf(t45,axiom,
sF25 = multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d),
introduced(definition) ).
cnf(t7710,plain,
sF25 = multiply(add(multiply(sF0,c),additive_inverse(multiply(a,multiply(b,c)))),d),
inference(step,[status(thm)],[t45,t54]) ).
cnf(t7711,plain,
sF25 = multiply(add(sF1,additive_inverse(multiply(a,multiply(b,c)))),d),
inference(step,[status(thm)],[t7710,t86]) ).
cnf(t7712,plain,
sF25 = multiply(add(sF1,multiply(a,additive_inverse(multiply(b,c)))),d),
inference(step,[status(thm)],[t7711,t61]) ).
cnf(t7713,plain,
sF25 = multiply(add(sF1,multiply(a,multiply(b,additive_inverse(c)))),d),
inference(step,[status(thm)],[t7712,t61]) ).
cnf(t7714,plain,
sF25 = multiply(add(sF1,multiply(a,additive_inverse(sF12))),d),
inference(step,[status(thm)],[t7713,t71]) ).
cnf(t7715,plain,
sF25 = multiply(add(sF1,sF23),d),
inference(step,[status(thm)],[t7714,t1585]) ).
cnf(t7716,plain,
sF25 = multiply(sF24,d),
inference(step,[status(thm)],[t7715,t1668]) ).
cnf(t1743,plain,
multiply(sF24,d) = sF25,
inference(orient,[status(thm)],[t7716]) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t89,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t1370,plain,
multiply(a,add(X1,sF19)) = add(multiply(a,X1),sF9),
inference(cp,[status(thm)],[t110,t1367]) ).
cnf(t7863,plain,
multiply(a,add(X1,sF19)) = add(sF9,multiply(a,X1)),
inference(step,[status(thm)],[t1370,t89]) ).
cnf(t1369,plain,
multiply(a,add(sF19,X1)) = add(sF9,multiply(a,X1)),
inference(cp,[status(thm)],[t110,t1367]) ).
cnf(t3036,plain,
add(sF9,multiply(a,X1)) = multiply(a,add(sF19,X1)),
inference(orient,[status(thm)],[t1369]) ).
cnf(t7864,plain,
multiply(a,add(X1,sF19)) = multiply(a,add(sF19,X1)),
inference(step,[status(thm)],[t7863,t3036]) ).
cnf(t3066,plain,
multiply(a,add(X1,sF19)) = multiply(a,add(sF19,X1)),
inference(orient,[status(thm)],[t7864]) ).
cnf(t35,axiom,
sF15 = multiply(multiply(b,c),d),
introduced(definition) ).
cnf(t7494,plain,
sF15 = multiply(sF12,d),
inference(step,[status(thm)],[t35,t56]) ).
cnf(t103,plain,
multiply(sF12,d) = sF15,
inference(orient,[status(thm)],[t7494]) ).
cnf(t140,plain,
multiply(sF12,add(X1,d)) = add(multiply(sF12,X1),sF15),
inference(cp,[status(thm)],[t110,t103]) ).
cnf(t7507,plain,
multiply(sF12,add(X1,d)) = add(sF15,multiply(sF12,X1)),
inference(step,[status(thm)],[t140,t89]) ).
cnf(t139,plain,
multiply(sF12,add(d,X1)) = add(sF15,multiply(sF12,X1)),
inference(cp,[status(thm)],[t110,t103]) ).
cnf(t318,plain,
add(sF15,multiply(sF12,X1)) = multiply(sF12,add(d,X1)),
inference(orient,[status(thm)],[t139]) ).
cnf(t7508,plain,
multiply(sF12,add(X1,d)) = multiply(sF12,add(d,X1)),
inference(step,[status(thm)],[t7507,t318]) ).
cnf(t323,plain,
multiply(sF12,add(X1,d)) = multiply(sF12,add(d,X1)),
inference(orient,[status(thm)],[t7508]) ).
cnf(t5,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t57,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t3,axiom,
multiply(X1,additive_identity) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t52,plain,
multiply(X1,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t3]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t49,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t92,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(cp,[status(thm)],[t89,t72]) ).
cnf(t2915,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(orient,[status(thm)],[t92]) ).
cnf(t15,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t201,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t1079,plain,
multiply(add(sF13,X1),d) = add(sF14,multiply(X1,d)),
inference(cp,[status(thm)],[t201,t1074]) ).
cnf(t1836,plain,
add(sF14,multiply(X1,d)) = multiply(add(sF13,X1),d),
inference(orient,[status(thm)],[t1079]) ).
cnf(t1850,plain,
multiply(add(sF13,sF24),d) = add(sF14,sF25),
inference(cp,[status(thm)],[t1836,t1743]) ).
cnf(t1670,plain,
add(sF1,add(sF23,X1)) = add(sF24,X1),
inference(cp,[status(thm)],[t72,t1668]) ).
cnf(t3711,plain,
add(sF1,add(sF23,X1)) = add(sF24,X1),
inference(orient,[status(thm)],[t1670]) ).
cnf(t3712,plain,
add(sF24,additive_inverse(sF23)) = add(sF1,additive_identity),
inference(cp,[status(thm)],[t3711,t57]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t51,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t1587,plain,
sF13 = additive_inverse(sF23),
inference(cp,[status(thm)],[t51,t1584]) ).
cnf(t1601,plain,
additive_inverse(sF23) = sF13,
inference(orient,[status(thm)],[t1587]) ).
cnf(t7908,plain,
add(sF24,sF13) = add(sF1,additive_identity),
inference(step,[status(thm)],[t3712,t1601]) ).
cnf(t7909,plain,
add(sF13,sF24) = add(sF1,additive_identity),
inference(step,[status(thm)],[t7908,t89]) ).
cnf(t7910,plain,
add(sF13,sF24) = sF1,
inference(step,[status(thm)],[t7909,t49]) ).
cnf(t3731,plain,
add(sF13,sF24) = sF1,
inference(orient,[status(thm)],[t7910]) ).
cnf(t7933,plain,
multiply(sF1,d) = add(sF14,sF25),
inference(step,[status(thm)],[t1850,t3731]) ).
cnf(t7934,plain,
sF2 = add(sF14,sF25),
inference(step,[status(thm)],[t7933,t601]) ).
cnf(t4069,plain,
add(sF14,sF25) = sF2,
inference(orient,[status(thm)],[t7934]) ).
cnf(t706,plain,
additive_identity = add(sF4,sF5),
inference(cp,[status(thm)],[t57,t702]) ).
cnf(t717,plain,
add(sF4,sF5) = additive_identity,
inference(orient,[status(thm)],[t706]) ).
cnf(t718,plain,
add(sF4,add(sF5,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t72,t717]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t50,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t7570,plain,
add(sF4,add(sF5,X1)) = X1,
inference(step,[status(thm)],[t718,t50]) ).
cnf(t880,plain,
add(sF4,add(sF5,X1)) = X1,
inference(orient,[status(thm)],[t7570]) ).
cnf(t882,plain,
X1 = add(sF4,add(X1,sF5)),
inference(cp,[status(thm)],[t880,t89]) ).
cnf(t1116,plain,
add(sF4,add(X1,sF5)) = X1,
inference(orient,[status(thm)],[t882]) ).
cnf(t1222,plain,
add(sF10,sF5) = sF9,
inference(cp,[status(thm)],[t1218,t1116]) ).
cnf(t7647,plain,
add(sF5,sF10) = sF9,
inference(step,[status(thm)],[t1222,t89]) ).
cnf(t1245,plain,
add(sF5,sF10) = sF9,
inference(orient,[status(thm)],[t7647]) ).
cnf(t1248,plain,
add(sF6,sF10) = add(sF2,sF9),
inference(cp,[status(thm)],[t997,t1245]) ).
cnf(t7656,plain,
sF11 = add(sF2,sF9),
inference(step,[status(thm)],[t1248,t1013]) ).
cnf(t1285,plain,
add(sF2,sF9) = sF11,
inference(orient,[status(thm)],[t7656]) ).
cnf(u0,negated_conjecture,
add(add(associator(multiply(a,b),c,d),associator(a,b,multiply(c,d))),additive_inverse(add(add(associator(a,multiply(b,c),d),multiply(a,associator(b,c,d))),multiply(associator(a,b,c),d)))) != additive_identity,
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(add(multiply(multiply(multiply(a,b),c),d),additive_inverse(multiply(multiply(a,b),multiply(c,d)))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d)))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))) != additive_identity,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
add(add(multiply(multiply(multiply(a,b),c),d),additive_inverse(multiply(multiply(a,b),multiply(c,d)))),add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[goal_0,t72]) ).
cnf(g0_1,plain,
add(multiply(multiply(multiply(a,b),c),d),add(additive_inverse(multiply(multiply(a,b),multiply(c,d))),add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_0,t72]) ).
cnf(g0_2,plain,
add(multiply(multiply(sF0,c),d),add(additive_inverse(multiply(multiply(a,b),multiply(c,d))),add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_1,t54]) ).
cnf(g0_3,plain,
add(multiply(sF1,d),add(additive_inverse(multiply(multiply(a,b),multiply(c,d))),add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_2,t86]) ).
cnf(g0_4,plain,
add(sF2,add(additive_inverse(multiply(multiply(a,b),multiply(c,d))),add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_3,t601]) ).
cnf(g0_5,plain,
add(sF2,add(multiply(multiply(a,b),additive_inverse(multiply(c,d))),add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_4,t61]) ).
cnf(g0_6,plain,
add(sF2,add(multiply(sF0,additive_inverse(multiply(c,d))),add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_5,t54]) ).
cnf(g0_7,plain,
add(sF2,add(multiply(sF0,multiply(c,additive_inverse(d))),add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_6,t61]) ).
cnf(g0_8,plain,
add(sF2,add(multiply(sF0,additive_inverse(sF3)),add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_7,t70]) ).
cnf(g0_9,plain,
add(sF2,add(sF5,add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_8,t703]) ).
cnf(g0_10,plain,
add(sF6,add(add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_9,t997]) ).
cnf(g0_11,plain,
add(sF6,add(multiply(multiply(a,b),multiply(c,d)),add(additive_inverse(multiply(a,multiply(b,multiply(c,d)))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_10,t72]) ).
cnf(g0_12,plain,
add(sF6,add(multiply(sF0,multiply(c,d)),add(additive_inverse(multiply(a,multiply(b,multiply(c,d)))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_11,t54]) ).
cnf(g0_13,plain,
add(sF6,add(multiply(sF0,sF3),add(additive_inverse(multiply(a,multiply(b,multiply(c,d)))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_12,t55]) ).
cnf(g0_14,plain,
add(sF6,add(sF4,add(additive_inverse(multiply(a,multiply(b,multiply(c,d)))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_13,t643]) ).
cnf(g0_15,plain,
add(sF6,add(sF4,add(multiply(a,additive_inverse(multiply(b,multiply(c,d)))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_14,t61]) ).
cnf(g0_16,plain,
add(sF6,add(sF4,add(multiply(a,multiply(b,additive_inverse(multiply(c,d)))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_15,t61]) ).
cnf(g0_17,plain,
add(sF6,add(sF4,add(multiply(a,multiply(b,multiply(c,additive_inverse(d)))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_16,t61]) ).
cnf(g0_18,plain,
add(sF6,add(sF4,add(multiply(a,multiply(b,additive_inverse(sF3))),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_17,t70]) ).
cnf(g0_19,plain,
add(sF6,add(sF4,add(multiply(a,sF19),additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_18,t1338]) ).
cnf(g0_20,plain,
add(sF6,add(sF4,add(sF9,additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_19,t1367]) ).
cnf(g0_21,plain,
add(sF6,add(sF10,additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_20,t1218]) ).
cnf(g0_22,plain,
add(sF11,additive_inverse(add(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))) != additive_identity,
inference(rw,[status(thm)],[g0_21,t1567]) ).
cnf(g0_23,plain,
add(sF11,additive_inverse(add(add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),add(multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_22,t72]) ).
cnf(g0_24,plain,
add(sF11,additive_inverse(add(multiply(multiply(a,multiply(b,c)),d),add(additive_inverse(multiply(a,multiply(multiply(b,c),d))),add(multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_23,t72]) ).
cnf(g0_25,plain,
add(sF11,additive_inverse(add(multiply(multiply(a,sF12),d),add(additive_inverse(multiply(a,multiply(multiply(b,c),d))),add(multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_24,t56]) ).
cnf(g0_26,plain,
add(sF11,additive_inverse(add(multiply(sF13,d),add(additive_inverse(multiply(a,multiply(multiply(b,c),d))),add(multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_25,t99]) ).
cnf(g0_27,plain,
add(sF11,additive_inverse(add(sF14,add(additive_inverse(multiply(a,multiply(multiply(b,c),d))),add(multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_26,t1074]) ).
cnf(g0_28,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,additive_inverse(multiply(multiply(b,c),d))),add(multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))))) != additive_identity,
inference(rw,[status(thm)],[g0_27,t61]) ).
cnf(g0_29,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(additive_inverse(multiply(multiply(b,c),d)),add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_28,t6056]) ).
cnf(g0_30,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(multiply(b,c),additive_inverse(d)),add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_29,t61]) ).
cnf(g0_31,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(multiply(b,c),add(additive_inverse(d),d)),additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_30,t6056]) ).
cnf(g0_32,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_31,t56]) ).
cnf(g0_33,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),multiply(b,additive_inverse(multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_32,t61]) ).
cnf(g0_34,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),multiply(b,multiply(c,additive_inverse(d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_33,t61]) ).
cnf(g0_35,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),multiply(b,additive_inverse(sF3)))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_34,t70]) ).
cnf(g0_36,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_35,t1338]) ).
cnf(g0_37,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)),multiply(add(multiply(sF0,c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_36,t54]) ).
cnf(g0_38,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)),multiply(add(sF1,additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_37,t86]) ).
cnf(g0_39,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)),multiply(add(sF1,multiply(a,additive_inverse(multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_38,t61]) ).
cnf(g0_40,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)),multiply(add(sF1,multiply(a,multiply(b,additive_inverse(c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_39,t61]) ).
cnf(g0_41,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)),multiply(add(sF1,multiply(a,additive_inverse(sF12))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_40,t71]) ).
cnf(g0_42,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)),multiply(add(sF1,sF23),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_41,t1585]) ).
cnf(g0_43,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)),multiply(sF24,d))))) != additive_identity,
inference(rw,[status(thm)],[g0_42,t1668]) ).
cnf(g0_44,plain,
add(sF11,additive_inverse(add(sF14,add(multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)),sF25)))) != additive_identity,
inference(rw,[status(thm)],[g0_43,t1743]) ).
cnf(g0_45,plain,
add(sF11,additive_inverse(add(sF14,add(sF25,multiply(a,add(multiply(sF12,add(additive_inverse(d),d)),sF19)))))) != additive_identity,
inference(rw,[status(thm)],[g0_44,t89]) ).
cnf(g0_46,plain,
add(sF11,additive_inverse(add(sF14,add(sF25,multiply(a,add(sF19,multiply(sF12,add(additive_inverse(d),d)))))))) != additive_identity,
inference(rw,[status(thm)],[g0_45,t3066]) ).
cnf(g0_47,plain,
add(sF11,additive_inverse(add(sF14,add(sF25,multiply(a,add(sF19,multiply(sF12,add(d,additive_inverse(d))))))))) != additive_identity,
inference(rw,[status(thm)],[g0_46,t323]) ).
cnf(g0_48,plain,
add(sF11,additive_inverse(add(sF14,add(sF25,multiply(a,add(sF19,multiply(sF12,additive_identity))))))) != additive_identity,
inference(rw,[status(thm)],[g0_47,t57]) ).
cnf(g0_49,plain,
add(sF11,additive_inverse(add(sF14,add(sF25,multiply(a,add(sF19,additive_identity)))))) != additive_identity,
inference(rw,[status(thm)],[g0_48,t52]) ).
cnf(g0_50,plain,
add(sF11,additive_inverse(add(sF14,add(sF25,multiply(a,sF19))))) != additive_identity,
inference(rw,[status(thm)],[g0_49,t49]) ).
cnf(g0_51,plain,
add(sF11,additive_inverse(add(sF14,add(sF25,sF9)))) != additive_identity,
inference(rw,[status(thm)],[g0_50,t1367]) ).
cnf(g0_52,plain,
add(sF11,additive_inverse(add(sF9,add(sF14,sF25)))) != additive_identity,
inference(rw,[status(thm)],[g0_51,t2915]) ).
cnf(g0_53,plain,
add(sF11,additive_inverse(add(sF9,sF2))) != additive_identity,
inference(rw,[status(thm)],[g0_52,t4069]) ).
cnf(g0_54,plain,
add(sF11,additive_inverse(add(sF2,sF9))) != additive_identity,
inference(rw,[status(thm)],[g0_53,t89]) ).
cnf(g0_55,plain,
add(sF11,additive_inverse(sF11)) != additive_identity,
inference(rw,[status(thm)],[g0_54,t1285]) ).
cnf(g0_56,plain,
additive_identity != additive_identity,
inference(rw,[status(thm)],[g0_55,t57]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_56]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG026-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.37 % Computer : n001.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:55:08 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 16.40/2.81 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.40/2.81 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------