%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG026-6 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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 9.06s 1.74s
% Output : CNFRefutation 9.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 37
% Syntax : Number of clauses : 345 ( 345 unt; 0 nHn; 287 RR)
% Number of literals : 345 ( 344 equ; 49 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 : 36 ( 36 usr; 32 con; 0-3 aty)
% Number of variables : 74 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t54,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t13,axiom,
sF0 = multiply(a,b),
introduced(definition) ).
cnf(t47,plain,
multiply(a,b) = sF0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sF1 = multiply(multiply(a,b),c),
introduced(definition) ).
cnf(t3603,plain,
sF1 = multiply(sF0,c),
inference(step,[status(thm)],[t14,t47]) ).
cnf(t66,plain,
multiply(sF0,c) = sF1,
inference(orient,[status(thm)],[t3603]) ).
cnf(t15,axiom,
sF2 = multiply(multiply(multiply(a,b),c),d),
introduced(definition) ).
cnf(t3626,plain,
sF2 = multiply(multiply(sF0,c),d),
inference(step,[status(thm)],[t15,t47]) ).
cnf(t3627,plain,
sF2 = multiply(sF1,d),
inference(step,[status(thm)],[t3626,t66]) ).
cnf(t289,plain,
multiply(sF1,d) = sF2,
inference(orient,[status(thm)],[t3627]) ).
cnf(t16,axiom,
sF3 = multiply(c,d),
introduced(definition) ).
cnf(t48,plain,
multiply(c,d) = sF3,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sF4 = multiply(multiply(a,b),multiply(c,d)),
introduced(definition) ).
cnf(t3630,plain,
sF4 = multiply(sF0,multiply(c,d)),
inference(step,[status(thm)],[t17,t47]) ).
cnf(t3631,plain,
sF4 = multiply(sF0,sF3),
inference(step,[status(thm)],[t3630,t48]) ).
cnf(t329,plain,
multiply(sF0,sF3) = sF4,
inference(orient,[status(thm)],[t3631]) ).
cnf(t18,axiom,
sF5 = additive_inverse(multiply(multiply(a,b),multiply(c,d))),
introduced(definition) ).
cnf(t3640,plain,
sF5 = additive_inverse(multiply(sF0,multiply(c,d))),
inference(step,[status(thm)],[t18,t47]) ).
cnf(t3641,plain,
sF5 = additive_inverse(multiply(sF0,sF3)),
inference(step,[status(thm)],[t3640,t48]) ).
cnf(t3642,plain,
sF5 = additive_inverse(sF4),
inference(step,[status(thm)],[t3641,t329]) ).
cnf(t395,plain,
additive_inverse(sF4) = sF5,
inference(orient,[status(thm)],[t3642]) ).
cnf(t19,axiom,
sF6 = add(multiply(multiply(multiply(a,b),c),d),additive_inverse(multiply(multiply(a,b),multiply(c,d)))),
introduced(definition) ).
cnf(t3649,plain,
sF6 = add(multiply(multiply(sF0,c),d),additive_inverse(multiply(multiply(a,b),multiply(c,d)))),
inference(step,[status(thm)],[t19,t47]) ).
cnf(t3650,plain,
sF6 = add(multiply(sF1,d),additive_inverse(multiply(multiply(a,b),multiply(c,d)))),
inference(step,[status(thm)],[t3649,t66]) ).
cnf(t3651,plain,
sF6 = add(sF2,additive_inverse(multiply(multiply(a,b),multiply(c,d)))),
inference(step,[status(thm)],[t3650,t289]) ).
cnf(t3652,plain,
sF6 = add(sF2,additive_inverse(multiply(sF0,multiply(c,d)))),
inference(step,[status(thm)],[t3651,t47]) ).
cnf(t3653,plain,
sF6 = add(sF2,additive_inverse(multiply(sF0,sF3))),
inference(step,[status(thm)],[t3652,t48]) ).
cnf(t3654,plain,
sF6 = add(sF2,additive_inverse(sF4)),
inference(step,[status(thm)],[t3653,t329]) ).
cnf(t3655,plain,
sF6 = add(sF2,sF5),
inference(step,[status(thm)],[t3654,t395]) ).
cnf(t441,plain,
add(sF2,sF5) = sF6,
inference(orient,[status(thm)],[t3655]) ).
cnf(t443,plain,
add(sF2,add(sF5,X1)) = add(sF6,X1),
inference(cp,[status(thm)],[t54,t441]) ).
cnf(t647,plain,
add(sF2,add(sF5,X1)) = add(sF6,X1),
inference(orient,[status(thm)],[t443]) ).
cnf(t20,axiom,
sF7 = multiply(b,multiply(c,d)),
introduced(definition) ).
cnf(t3604,plain,
sF7 = multiply(b,sF3),
inference(step,[status(thm)],[t20,t48]) ).
cnf(t68,plain,
multiply(b,sF3) = sF7,
inference(orient,[status(thm)],[t3604]) ).
cnf(t21,axiom,
sF8 = multiply(a,multiply(b,multiply(c,d))),
introduced(definition) ).
cnf(t3656,plain,
sF8 = multiply(a,multiply(b,sF3)),
inference(step,[status(thm)],[t21,t48]) ).
cnf(t3657,plain,
sF8 = multiply(a,sF7),
inference(step,[status(thm)],[t3656,t68]) ).
cnf(t466,plain,
multiply(a,sF7) = sF8,
inference(orient,[status(thm)],[t3657]) ).
cnf(t22,axiom,
sF9 = additive_inverse(multiply(a,multiply(b,multiply(c,d)))),
introduced(definition) ).
cnf(t3667,plain,
sF9 = additive_inverse(multiply(a,multiply(b,sF3))),
inference(step,[status(thm)],[t22,t48]) ).
cnf(t3668,plain,
sF9 = additive_inverse(multiply(a,sF7)),
inference(step,[status(thm)],[t3667,t68]) ).
cnf(t3669,plain,
sF9 = additive_inverse(sF8),
inference(step,[status(thm)],[t3668,t466]) ).
cnf(t538,plain,
additive_inverse(sF8) = sF9,
inference(orient,[status(thm)],[t3669]) ).
cnf(t23,axiom,
sF10 = add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),
introduced(definition) ).
cnf(t3673,plain,
sF10 = add(multiply(sF0,multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),
inference(step,[status(thm)],[t23,t47]) ).
cnf(t3674,plain,
sF10 = add(multiply(sF0,sF3),additive_inverse(multiply(a,multiply(b,multiply(c,d))))),
inference(step,[status(thm)],[t3673,t48]) ).
cnf(t3675,plain,
sF10 = add(sF4,additive_inverse(multiply(a,multiply(b,multiply(c,d))))),
inference(step,[status(thm)],[t3674,t329]) ).
cnf(t3676,plain,
sF10 = add(sF4,additive_inverse(multiply(a,multiply(b,sF3)))),
inference(step,[status(thm)],[t3675,t48]) ).
cnf(t3677,plain,
sF10 = add(sF4,additive_inverse(multiply(a,sF7))),
inference(step,[status(thm)],[t3676,t68]) ).
cnf(t3678,plain,
sF10 = add(sF4,additive_inverse(sF8)),
inference(step,[status(thm)],[t3677,t466]) ).
cnf(t3679,plain,
sF10 = add(sF4,sF9),
inference(step,[status(thm)],[t3678,t538]) ).
cnf(t584,plain,
add(sF4,sF9) = sF10,
inference(orient,[status(thm)],[t3679]) ).
cnf(t586,plain,
add(sF4,add(sF9,X1)) = add(sF10,X1),
inference(cp,[status(thm)],[t54,t584]) ).
cnf(t771,plain,
add(sF4,add(sF9,X1)) = add(sF10,X1),
inference(orient,[status(thm)],[t586]) ).
cnf(t24,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(t3685,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)],[t24,t54]) ).
cnf(t3686,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)],[t3685,t47]) ).
cnf(t3687,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)],[t3686,t66]) ).
cnf(t3688,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)],[t3687,t289]) ).
cnf(t3689,plain,
sF11 = add(sF2,add(additive_inverse(multiply(sF0,multiply(c,d))),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3688,t47]) ).
cnf(t3690,plain,
sF11 = add(sF2,add(additive_inverse(multiply(sF0,sF3)),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3689,t48]) ).
cnf(t3691,plain,
sF11 = add(sF2,add(additive_inverse(sF4),add(multiply(multiply(a,b),multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3690,t329]) ).
cnf(t3692,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)],[t3691,t395]) ).
cnf(t3693,plain,
sF11 = add(sF2,add(sF5,add(multiply(sF0,multiply(c,d)),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3692,t47]) ).
cnf(t3694,plain,
sF11 = add(sF2,add(sF5,add(multiply(sF0,sF3),additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3693,t48]) ).
cnf(t3695,plain,
sF11 = add(sF2,add(sF5,add(sF4,additive_inverse(multiply(a,multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3694,t329]) ).
cnf(t3696,plain,
sF11 = add(sF2,add(sF5,add(sF4,additive_inverse(multiply(a,multiply(b,sF3)))))),
inference(step,[status(thm)],[t3695,t48]) ).
cnf(t3697,plain,
sF11 = add(sF2,add(sF5,add(sF4,additive_inverse(multiply(a,sF7))))),
inference(step,[status(thm)],[t3696,t68]) ).
cnf(t3698,plain,
sF11 = add(sF2,add(sF5,add(sF4,additive_inverse(sF8)))),
inference(step,[status(thm)],[t3697,t466]) ).
cnf(t3699,plain,
sF11 = add(sF2,add(sF5,add(sF4,sF9))),
inference(step,[status(thm)],[t3698,t538]) ).
cnf(t3700,plain,
sF11 = add(sF2,add(sF5,sF10)),
inference(step,[status(thm)],[t3699,t584]) ).
cnf(t620,plain,
add(sF2,add(sF5,sF10)) = sF11,
inference(orient,[status(thm)],[t3700]) ).
cnf(t3703,plain,
add(sF6,sF10) = sF11,
inference(step,[status(thm)],[t620,t647]) ).
cnf(t648,plain,
add(sF6,sF10) = sF11,
inference(rw,[status(thm)],[t3703]) ).
cnf(t652,plain,
add(sF6,sF10) = sF11,
inference(orient,[status(thm)],[t648]) ).
cnf(t654,plain,
add(sF6,add(sF10,X1)) = add(sF11,X1),
inference(cp,[status(thm)],[t54,t652]) ).
cnf(t820,plain,
add(sF6,add(sF10,X1)) = add(sF11,X1),
inference(orient,[status(thm)],[t654]) ).
cnf(t25,axiom,
sF12 = multiply(b,c),
introduced(definition) ).
cnf(t49,plain,
multiply(b,c) = sF12,
inference(orient,[status(thm)],[t25]) ).
cnf(t26,axiom,
sF13 = multiply(a,multiply(b,c)),
introduced(definition) ).
cnf(t3605,plain,
sF13 = multiply(a,sF12),
inference(step,[status(thm)],[t26,t49]) ).
cnf(t70,plain,
multiply(a,sF12) = sF13,
inference(orient,[status(thm)],[t3605]) ).
cnf(t27,axiom,
sF14 = multiply(multiply(a,multiply(b,c)),d),
introduced(definition) ).
cnf(t3707,plain,
sF14 = multiply(multiply(a,sF12),d),
inference(step,[status(thm)],[t27,t49]) ).
cnf(t3708,plain,
sF14 = multiply(sF13,d),
inference(step,[status(thm)],[t3707,t70]) ).
cnf(t658,plain,
multiply(sF13,d) = sF14,
inference(orient,[status(thm)],[t3708]) ).
cnf(t28,axiom,
sF15 = multiply(multiply(b,c),d),
introduced(definition) ).
cnf(t3606,plain,
sF15 = multiply(sF12,d),
inference(step,[status(thm)],[t28,t49]) ).
cnf(t72,plain,
multiply(sF12,d) = sF15,
inference(orient,[status(thm)],[t3606]) ).
cnf(t29,axiom,
sF16 = multiply(a,multiply(multiply(b,c),d)),
introduced(definition) ).
cnf(t3716,plain,
sF16 = multiply(a,multiply(sF12,d)),
inference(step,[status(thm)],[t29,t49]) ).
cnf(t3717,plain,
sF16 = multiply(a,sF15),
inference(step,[status(thm)],[t3716,t72]) ).
cnf(t730,plain,
multiply(a,sF15) = sF16,
inference(orient,[status(thm)],[t3717]) ).
cnf(t30,axiom,
sF17 = additive_inverse(multiply(a,multiply(multiply(b,c),d))),
introduced(definition) ).
cnf(t3718,plain,
sF17 = additive_inverse(multiply(a,multiply(sF12,d))),
inference(step,[status(thm)],[t30,t49]) ).
cnf(t3719,plain,
sF17 = additive_inverse(multiply(a,sF15)),
inference(step,[status(thm)],[t3718,t72]) ).
cnf(t3720,plain,
sF17 = additive_inverse(sF16),
inference(step,[status(thm)],[t3719,t730]) ).
cnf(t754,plain,
additive_inverse(sF16) = sF17,
inference(orient,[status(thm)],[t3720]) ).
cnf(t31,axiom,
sF18 = add(multiply(multiply(a,multiply(b,c)),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),
introduced(definition) ).
cnf(t3725,plain,
sF18 = add(multiply(multiply(a,sF12),d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),
inference(step,[status(thm)],[t31,t49]) ).
cnf(t3726,plain,
sF18 = add(multiply(sF13,d),additive_inverse(multiply(a,multiply(multiply(b,c),d)))),
inference(step,[status(thm)],[t3725,t70]) ).
cnf(t3727,plain,
sF18 = add(sF14,additive_inverse(multiply(a,multiply(multiply(b,c),d)))),
inference(step,[status(thm)],[t3726,t658]) ).
cnf(t3728,plain,
sF18 = add(sF14,additive_inverse(multiply(a,multiply(sF12,d)))),
inference(step,[status(thm)],[t3727,t49]) ).
cnf(t3729,plain,
sF18 = add(sF14,additive_inverse(multiply(a,sF15))),
inference(step,[status(thm)],[t3728,t72]) ).
cnf(t3730,plain,
sF18 = add(sF14,additive_inverse(sF16)),
inference(step,[status(thm)],[t3729,t730]) ).
cnf(t3731,plain,
sF18 = add(sF14,sF17),
inference(step,[status(thm)],[t3730,t754]) ).
cnf(t778,plain,
add(sF14,sF17) = sF18,
inference(orient,[status(thm)],[t3731]) ).
cnf(t780,plain,
add(sF14,add(sF17,X1)) = add(sF18,X1),
inference(cp,[status(thm)],[t54,t778]) ).
cnf(t1074,plain,
add(sF14,add(sF17,X1)) = add(sF18,X1),
inference(orient,[status(thm)],[t780]) ).
cnf(t32,axiom,
sF19 = additive_inverse(multiply(b,multiply(c,d))),
introduced(definition) ).
cnf(t3607,plain,
sF19 = additive_inverse(multiply(b,sF3)),
inference(step,[status(thm)],[t32,t48]) ).
cnf(t3608,plain,
sF19 = additive_inverse(sF7),
inference(step,[status(thm)],[t3607,t68]) ).
cnf(t93,plain,
additive_inverse(sF7) = sF19,
inference(orient,[status(thm)],[t3608]) ).
cnf(t33,axiom,
sF20 = add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d)))),
introduced(definition) ).
cnf(t3735,plain,
sF20 = add(multiply(sF12,d),additive_inverse(multiply(b,multiply(c,d)))),
inference(step,[status(thm)],[t33,t49]) ).
cnf(t3736,plain,
sF20 = add(sF15,additive_inverse(multiply(b,multiply(c,d)))),
inference(step,[status(thm)],[t3735,t72]) ).
cnf(t3737,plain,
sF20 = add(sF15,additive_inverse(multiply(b,sF3))),
inference(step,[status(thm)],[t3736,t48]) ).
cnf(t3738,plain,
sF20 = add(sF15,additive_inverse(sF7)),
inference(step,[status(thm)],[t3737,t68]) ).
cnf(t3739,plain,
sF20 = add(sF15,sF19),
inference(step,[status(thm)],[t3738,t93]) ).
cnf(t800,plain,
add(sF15,sF19) = sF20,
inference(orient,[status(thm)],[t3739]) ).
cnf(t34,axiom,
sF21 = multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))),
introduced(definition) ).
cnf(t3741,plain,
sF21 = multiply(a,add(multiply(sF12,d),additive_inverse(multiply(b,multiply(c,d))))),
inference(step,[status(thm)],[t34,t49]) ).
cnf(t3742,plain,
sF21 = multiply(a,add(sF15,additive_inverse(multiply(b,multiply(c,d))))),
inference(step,[status(thm)],[t3741,t72]) ).
cnf(t3743,plain,
sF21 = multiply(a,add(sF15,additive_inverse(multiply(b,sF3)))),
inference(step,[status(thm)],[t3742,t48]) ).
cnf(t3744,plain,
sF21 = multiply(a,add(sF15,additive_inverse(sF7))),
inference(step,[status(thm)],[t3743,t68]) ).
cnf(t3745,plain,
sF21 = multiply(a,add(sF15,sF19)),
inference(step,[status(thm)],[t3744,t93]) ).
cnf(t3746,plain,
sF21 = multiply(a,sF20),
inference(step,[status(thm)],[t3745,t800]) ).
cnf(t824,plain,
multiply(a,sF20) = sF21,
inference(orient,[status(thm)],[t3746]) ).
cnf(t35,axiom,
sF22 = 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)))))),
introduced(definition) ).
cnf(t3751,plain,
sF22 = add(multiply(multiply(a,multiply(b,c)),d),add(additive_inverse(multiply(a,multiply(multiply(b,c),d))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t35,t54]) ).
cnf(t3752,plain,
sF22 = add(multiply(multiply(a,sF12),d),add(additive_inverse(multiply(a,multiply(multiply(b,c),d))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3751,t49]) ).
cnf(t3753,plain,
sF22 = add(multiply(sF13,d),add(additive_inverse(multiply(a,multiply(multiply(b,c),d))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3752,t70]) ).
cnf(t3754,plain,
sF22 = add(sF14,add(additive_inverse(multiply(a,multiply(multiply(b,c),d))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3753,t658]) ).
cnf(t3755,plain,
sF22 = add(sF14,add(additive_inverse(multiply(a,multiply(sF12,d))),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3754,t49]) ).
cnf(t3756,plain,
sF22 = add(sF14,add(additive_inverse(multiply(a,sF15)),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3755,t72]) ).
cnf(t3757,plain,
sF22 = add(sF14,add(additive_inverse(sF16),multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3756,t730]) ).
cnf(t3758,plain,
sF22 = add(sF14,add(sF17,multiply(a,add(multiply(multiply(b,c),d),additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3757,t754]) ).
cnf(t3759,plain,
sF22 = add(sF14,add(sF17,multiply(a,add(multiply(sF12,d),additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3758,t49]) ).
cnf(t3760,plain,
sF22 = add(sF14,add(sF17,multiply(a,add(sF15,additive_inverse(multiply(b,multiply(c,d))))))),
inference(step,[status(thm)],[t3759,t72]) ).
cnf(t3761,plain,
sF22 = add(sF14,add(sF17,multiply(a,add(sF15,additive_inverse(multiply(b,sF3)))))),
inference(step,[status(thm)],[t3760,t48]) ).
cnf(t3762,plain,
sF22 = add(sF14,add(sF17,multiply(a,add(sF15,additive_inverse(sF7))))),
inference(step,[status(thm)],[t3761,t68]) ).
cnf(t3763,plain,
sF22 = add(sF14,add(sF17,multiply(a,add(sF15,sF19)))),
inference(step,[status(thm)],[t3762,t93]) ).
cnf(t3764,plain,
sF22 = add(sF14,add(sF17,multiply(a,sF20))),
inference(step,[status(thm)],[t3763,t800]) ).
cnf(t3765,plain,
sF22 = add(sF14,add(sF17,sF21)),
inference(step,[status(thm)],[t3764,t824]) ).
cnf(t855,plain,
add(sF14,add(sF17,sF21)) = sF22,
inference(orient,[status(thm)],[t3765]) ).
cnf(t3817,plain,
add(sF18,sF21) = sF22,
inference(step,[status(thm)],[t855,t1074]) ).
cnf(t1075,plain,
add(sF18,sF21) = sF22,
inference(rw,[status(thm)],[t3817]) ).
cnf(t1080,plain,
add(sF18,sF21) = sF22,
inference(orient,[status(thm)],[t1075]) ).
cnf(t1082,plain,
add(sF18,add(sF21,X1)) = add(sF22,X1),
inference(cp,[status(thm)],[t54,t1080]) ).
cnf(t2113,plain,
add(sF18,add(sF21,X1)) = add(sF22,X1),
inference(orient,[status(thm)],[t1082]) ).
cnf(t36,axiom,
sF23 = additive_inverse(multiply(a,multiply(b,c))),
introduced(definition) ).
cnf(t3772,plain,
sF23 = additive_inverse(multiply(a,sF12)),
inference(step,[status(thm)],[t36,t49]) ).
cnf(t3773,plain,
sF23 = additive_inverse(sF13),
inference(step,[status(thm)],[t3772,t70]) ).
cnf(t921,plain,
additive_inverse(sF13) = sF23,
inference(orient,[status(thm)],[t3773]) ).
cnf(t37,axiom,
sF24 = add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),
introduced(definition) ).
cnf(t3774,plain,
sF24 = add(multiply(sF0,c),additive_inverse(multiply(a,multiply(b,c)))),
inference(step,[status(thm)],[t37,t47]) ).
cnf(t3775,plain,
sF24 = add(sF1,additive_inverse(multiply(a,multiply(b,c)))),
inference(step,[status(thm)],[t3774,t66]) ).
cnf(t3776,plain,
sF24 = add(sF1,additive_inverse(multiply(a,sF12))),
inference(step,[status(thm)],[t3775,t49]) ).
cnf(t3777,plain,
sF24 = add(sF1,additive_inverse(sF13)),
inference(step,[status(thm)],[t3776,t70]) ).
cnf(t3778,plain,
sF24 = add(sF1,sF23),
inference(step,[status(thm)],[t3777,t921]) ).
cnf(t969,plain,
add(sF1,sF23) = sF24,
inference(orient,[status(thm)],[t3778]) ).
cnf(t38,axiom,
sF25 = multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d),
introduced(definition) ).
cnf(t3786,plain,
sF25 = multiply(add(multiply(sF0,c),additive_inverse(multiply(a,multiply(b,c)))),d),
inference(step,[status(thm)],[t38,t47]) ).
cnf(t3787,plain,
sF25 = multiply(add(sF1,additive_inverse(multiply(a,multiply(b,c)))),d),
inference(step,[status(thm)],[t3786,t66]) ).
cnf(t3788,plain,
sF25 = multiply(add(sF1,additive_inverse(multiply(a,sF12))),d),
inference(step,[status(thm)],[t3787,t49]) ).
cnf(t3789,plain,
sF25 = multiply(add(sF1,additive_inverse(sF13)),d),
inference(step,[status(thm)],[t3788,t70]) ).
cnf(t3790,plain,
sF25 = multiply(add(sF1,sF23),d),
inference(step,[status(thm)],[t3789,t921]) ).
cnf(t3791,plain,
sF25 = multiply(sF24,d),
inference(step,[status(thm)],[t3790,t969]) ).
cnf(t1031,plain,
multiply(sF24,d) = sF25,
inference(orient,[status(thm)],[t3791]) ).
cnf(t39,axiom,
sF26 = 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)),
introduced(definition) ).
cnf(t3793,plain,
sF26 = 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))),
inference(step,[status(thm)],[t39,t54]) ).
cnf(t3794,plain,
sF26 = 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)))),
inference(step,[status(thm)],[t3793,t54]) ).
cnf(t3795,plain,
sF26 = 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)))),
inference(step,[status(thm)],[t3794,t49]) ).
cnf(t3796,plain,
sF26 = 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)))),
inference(step,[status(thm)],[t3795,t70]) ).
cnf(t3797,plain,
sF26 = 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)))),
inference(step,[status(thm)],[t3796,t658]) ).
cnf(t3798,plain,
sF26 = add(sF14,add(additive_inverse(multiply(a,multiply(sF12,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)))),
inference(step,[status(thm)],[t3797,t49]) ).
cnf(t3799,plain,
sF26 = add(sF14,add(additive_inverse(multiply(a,sF15)),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)))),
inference(step,[status(thm)],[t3798,t72]) ).
cnf(t3800,plain,
sF26 = add(sF14,add(additive_inverse(sF16),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)))),
inference(step,[status(thm)],[t3799,t730]) ).
cnf(t3801,plain,
sF26 = add(sF14,add(sF17,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)))),
inference(step,[status(thm)],[t3800,t754]) ).
cnf(t3802,plain,
sF26 = add(sF14,add(sF17,add(multiply(a,add(multiply(sF12,d),additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))),
inference(step,[status(thm)],[t3801,t49]) ).
cnf(t3803,plain,
sF26 = add(sF14,add(sF17,add(multiply(a,add(sF15,additive_inverse(multiply(b,multiply(c,d))))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))),
inference(step,[status(thm)],[t3802,t72]) ).
cnf(t3804,plain,
sF26 = add(sF14,add(sF17,add(multiply(a,add(sF15,additive_inverse(multiply(b,sF3)))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))),
inference(step,[status(thm)],[t3803,t48]) ).
cnf(t3805,plain,
sF26 = add(sF14,add(sF17,add(multiply(a,add(sF15,additive_inverse(sF7))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))),
inference(step,[status(thm)],[t3804,t68]) ).
cnf(t3806,plain,
sF26 = add(sF14,add(sF17,add(multiply(a,add(sF15,sF19)),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))),
inference(step,[status(thm)],[t3805,t93]) ).
cnf(t3807,plain,
sF26 = add(sF14,add(sF17,add(multiply(a,sF20),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))),
inference(step,[status(thm)],[t3806,t800]) ).
cnf(t3808,plain,
sF26 = add(sF14,add(sF17,add(sF21,multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))),
inference(step,[status(thm)],[t3807,t824]) ).
cnf(t3809,plain,
sF26 = add(sF14,add(sF17,add(sF21,multiply(add(multiply(sF0,c),additive_inverse(multiply(a,multiply(b,c)))),d)))),
inference(step,[status(thm)],[t3808,t47]) ).
cnf(t3810,plain,
sF26 = add(sF14,add(sF17,add(sF21,multiply(add(sF1,additive_inverse(multiply(a,multiply(b,c)))),d)))),
inference(step,[status(thm)],[t3809,t66]) ).
cnf(t3811,plain,
sF26 = add(sF14,add(sF17,add(sF21,multiply(add(sF1,additive_inverse(multiply(a,sF12))),d)))),
inference(step,[status(thm)],[t3810,t49]) ).
cnf(t3812,plain,
sF26 = add(sF14,add(sF17,add(sF21,multiply(add(sF1,additive_inverse(sF13)),d)))),
inference(step,[status(thm)],[t3811,t70]) ).
cnf(t3813,plain,
sF26 = add(sF14,add(sF17,add(sF21,multiply(add(sF1,sF23),d)))),
inference(step,[status(thm)],[t3812,t921]) ).
cnf(t3814,plain,
sF26 = add(sF14,add(sF17,add(sF21,multiply(sF24,d)))),
inference(step,[status(thm)],[t3813,t969]) ).
cnf(t3815,plain,
sF26 = add(sF14,add(sF17,add(sF21,sF25))),
inference(step,[status(thm)],[t3814,t1031]) ).
cnf(t1066,plain,
add(sF14,add(sF17,add(sF21,sF25))) = sF26,
inference(orient,[status(thm)],[t3815]) ).
cnf(t3818,plain,
add(sF18,add(sF21,sF25)) = sF26,
inference(step,[status(thm)],[t1066,t1074]) ).
cnf(t1076,plain,
add(sF18,add(sF21,sF25)) = sF26,
inference(rw,[status(thm)],[t3818]) ).
cnf(t2070,plain,
add(sF18,add(sF21,sF25)) = sF26,
inference(orient,[status(thm)],[t1076]) ).
cnf(t3936,plain,
add(sF22,sF25) = sF26,
inference(step,[status(thm)],[t2070,t2113]) ).
cnf(t2114,plain,
add(sF22,sF25) = sF26,
inference(rw,[status(thm)],[t3936]) ).
cnf(t2126,plain,
add(sF22,sF25) = sF26,
inference(orient,[status(thm)],[t2114]) ).
cnf(t5,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t50,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t756,plain,
additive_identity = add(sF16,sF17),
inference(cp,[status(thm)],[t50,t754]) ).
cnf(t759,plain,
add(sF16,sF17) = additive_identity,
inference(orient,[status(thm)],[t756]) ).
cnf(t760,plain,
add(sF16,add(sF17,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t54,t759]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t43,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t3784,plain,
add(sF16,add(sF17,X1)) = X1,
inference(step,[status(thm)],[t760,t43]) ).
cnf(t1021,plain,
add(sF16,add(sF17,X1)) = X1,
inference(orient,[status(thm)],[t3784]) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t80,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t1022,plain,
X1 = add(add(sF17,X1),sF16),
inference(cp,[status(thm)],[t1021,t80]) ).
cnf(t3917,plain,
X1 = add(sF17,add(X1,sF16)),
inference(step,[status(thm)],[t1022,t54]) ).
cnf(t1651,plain,
add(sF17,add(X1,sF16)) = X1,
inference(orient,[status(thm)],[t3917]) ).
cnf(t11,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t100,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t468,plain,
multiply(a,add(sF7,X1)) = add(sF8,multiply(a,X1)),
inference(cp,[status(thm)],[t100,t466]) ).
cnf(t681,plain,
add(sF8,multiply(a,X1)) = multiply(a,add(sF7,X1)),
inference(orient,[status(thm)],[t468]) ).
cnf(t832,plain,
multiply(a,add(sF7,sF20)) = add(sF8,sF21),
inference(cp,[status(thm)],[t681,t824]) ).
cnf(t95,plain,
additive_identity = add(sF7,sF19),
inference(cp,[status(thm)],[t50,t93]) ).
cnf(t98,plain,
add(sF7,sF19) = additive_identity,
inference(orient,[status(thm)],[t95]) ).
cnf(t99,plain,
add(sF7,add(sF19,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t54,t98]) ).
cnf(t3609,plain,
add(sF7,add(sF19,X1)) = X1,
inference(step,[status(thm)],[t99,t43]) ).
cnf(t133,plain,
add(sF7,add(sF19,X1)) = X1,
inference(orient,[status(thm)],[t3609]) ).
cnf(t135,plain,
X1 = add(sF7,add(X1,sF19)),
inference(cp,[status(thm)],[t133,t80]) ).
cnf(t270,plain,
add(sF7,add(X1,sF19)) = X1,
inference(orient,[status(thm)],[t135]) ).
cnf(t803,plain,
sF15 = add(sF7,sF20),
inference(cp,[status(thm)],[t270,t800]) ).
cnf(t804,plain,
add(sF7,sF20) = sF15,
inference(orient,[status(thm)],[t803]) ).
cnf(t3747,plain,
multiply(a,sF15) = add(sF8,sF21),
inference(step,[status(thm)],[t832,t804]) ).
cnf(t3748,plain,
sF16 = add(sF8,sF21),
inference(step,[status(thm)],[t3747,t730]) ).
cnf(t833,plain,
add(sF8,sF21) = sF16,
inference(orient,[status(thm)],[t3748]) ).
cnf(t835,plain,
add(sF8,add(sF21,X1)) = add(sF16,X1),
inference(cp,[status(thm)],[t54,t833]) ).
cnf(t1494,plain,
add(sF8,add(sF21,X1)) = add(sF16,X1),
inference(orient,[status(thm)],[t835]) ).
cnf(t540,plain,
additive_identity = add(sF8,sF9),
inference(cp,[status(thm)],[t50,t538]) ).
cnf(t543,plain,
add(sF8,sF9) = additive_identity,
inference(orient,[status(thm)],[t540]) ).
cnf(t544,plain,
add(sF8,add(sF9,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t54,t543]) ).
cnf(t3721,plain,
add(sF8,add(sF9,X1)) = X1,
inference(step,[status(thm)],[t544,t43]) ).
cnf(t768,plain,
add(sF8,add(sF9,X1)) = X1,
inference(orient,[status(thm)],[t3721]) ).
cnf(t770,plain,
X1 = add(sF8,add(X1,sF9)),
inference(cp,[status(thm)],[t768,t80]) ).
cnf(t1041,plain,
add(sF8,add(X1,sF9)) = X1,
inference(orient,[status(thm)],[t770]) ).
cnf(t1498,plain,
add(sF16,sF9) = sF21,
inference(cp,[status(thm)],[t1494,t1041]) ).
cnf(t3908,plain,
add(sF9,sF16) = sF21,
inference(step,[status(thm)],[t1498,t80]) ).
cnf(t1527,plain,
add(sF9,sF16) = sF21,
inference(orient,[status(thm)],[t3908]) ).
cnf(t1654,plain,
sF9 = add(sF17,sF21),
inference(cp,[status(thm)],[t1651,t1527]) ).
cnf(t1661,plain,
add(sF17,sF21) = sF9,
inference(orient,[status(thm)],[t1654]) ).
cnf(t1665,plain,
add(sF18,sF21) = add(sF14,sF9),
inference(cp,[status(thm)],[t1074,t1661]) ).
cnf(t3918,plain,
sF22 = add(sF14,sF9),
inference(step,[status(thm)],[t1665,t1080]) ).
cnf(t3919,plain,
sF22 = add(sF9,sF14),
inference(step,[status(thm)],[t3918,t80]) ).
cnf(t1778,plain,
add(sF9,sF14) = sF22,
inference(orient,[status(thm)],[t3919]) ).
cnf(t1780,plain,
add(sF9,add(sF14,X1)) = add(sF22,X1),
inference(cp,[status(thm)],[t54,t1778]) ).
cnf(t3313,plain,
add(sF9,add(sF14,X1)) = add(sF22,X1),
inference(orient,[status(thm)],[t1780]) ).
cnf(t12,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t187,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t662,plain,
multiply(add(sF13,X1),d) = add(sF14,multiply(X1,d)),
inference(cp,[status(thm)],[t187,t658]) ).
cnf(t871,plain,
add(sF14,multiply(X1,d)) = multiply(add(sF13,X1),d),
inference(orient,[status(thm)],[t662]) ).
cnf(t1040,plain,
multiply(add(sF13,sF24),d) = add(sF14,sF25),
inference(cp,[status(thm)],[t871,t1031]) ).
cnf(t971,plain,
add(sF1,add(sF23,X1)) = add(sF24,X1),
inference(cp,[status(thm)],[t54,t969]) ).
cnf(t1625,plain,
add(sF1,add(sF23,X1)) = add(sF24,X1),
inference(orient,[status(thm)],[t971]) ).
cnf(t1626,plain,
add(sF24,additive_inverse(sF23)) = add(sF1,additive_identity),
inference(cp,[status(thm)],[t1625,t50]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t44,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t922,plain,
sF13 = additive_inverse(sF23),
inference(cp,[status(thm)],[t44,t921]) ).
cnf(t924,plain,
additive_inverse(sF23) = sF13,
inference(orient,[status(thm)],[t922]) ).
cnf(t3913,plain,
add(sF24,sF13) = add(sF1,additive_identity),
inference(step,[status(thm)],[t1626,t924]) ).
cnf(t3914,plain,
add(sF13,sF24) = add(sF1,additive_identity),
inference(step,[status(thm)],[t3913,t80]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t3915,plain,
add(sF13,sF24) = sF1,
inference(step,[status(thm)],[t3914,t42]) ).
cnf(t1631,plain,
add(sF13,sF24) = sF1,
inference(orient,[status(thm)],[t3915]) ).
cnf(t3926,plain,
multiply(sF1,d) = add(sF14,sF25),
inference(step,[status(thm)],[t1040,t1631]) ).
cnf(t3927,plain,
sF2 = add(sF14,sF25),
inference(step,[status(thm)],[t3926,t289]) ).
cnf(t2014,plain,
add(sF14,sF25) = sF2,
inference(orient,[status(thm)],[t3927]) ).
cnf(t3325,plain,
add(sF22,sF25) = add(sF9,sF2),
inference(cp,[status(thm)],[t3313,t2014]) ).
cnf(t3999,plain,
sF26 = add(sF9,sF2),
inference(step,[status(thm)],[t3325,t2126]) ).
cnf(t4000,plain,
sF26 = add(sF2,sF9),
inference(step,[status(thm)],[t3999,t80]) ).
cnf(t397,plain,
additive_identity = add(sF4,sF5),
inference(cp,[status(thm)],[t50,t395]) ).
cnf(t400,plain,
add(sF4,sF5) = additive_identity,
inference(orient,[status(thm)],[t397]) ).
cnf(t401,plain,
add(sF4,add(sF5,X1)) = add(additive_identity,X1),
inference(cp,[status(thm)],[t54,t400]) ).
cnf(t3684,plain,
add(sF4,add(sF5,X1)) = X1,
inference(step,[status(thm)],[t401,t43]) ).
cnf(t617,plain,
add(sF4,add(sF5,X1)) = X1,
inference(orient,[status(thm)],[t3684]) ).
cnf(t619,plain,
X1 = add(sF4,add(X1,sF5)),
inference(cp,[status(thm)],[t617,t80]) ).
cnf(t788,plain,
add(sF4,add(X1,sF5)) = X1,
inference(orient,[status(thm)],[t619]) ).
cnf(t791,plain,
sF9 = add(sF10,sF5),
inference(cp,[status(thm)],[t788,t771]) ).
cnf(t3733,plain,
sF9 = add(sF5,sF10),
inference(step,[status(thm)],[t791,t80]) ).
cnf(t793,plain,
add(sF5,sF10) = sF9,
inference(orient,[status(thm)],[t3733]) ).
cnf(t796,plain,
add(sF6,sF10) = add(sF2,sF9),
inference(cp,[status(thm)],[t647,t793]) ).
cnf(t3734,plain,
sF11 = add(sF2,sF9),
inference(step,[status(thm)],[t796,t652]) ).
cnf(t797,plain,
add(sF2,sF9) = sF11,
inference(orient,[status(thm)],[t3734]) ).
cnf(t4001,plain,
sF26 = sF11,
inference(step,[status(thm)],[t4000,t797]) ).
cnf(t3595,plain,
sF26 = sF11,
inference(orient,[status(thm)],[t4001]) ).
cnf(t4005,plain,
add(sF22,sF25) = sF11,
inference(step,[status(thm)],[t2126,t3595]) ).
cnf(t3600,plain,
add(sF22,sF25) = sF11,
inference(orient,[status(thm)],[t4005]) ).
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/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
associator(X,Y,Z) = add(multiply(multiply(X,Y),Z),additive_inverse(multiply(X,multiply(Y,Z)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
add(add(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,t54]) ).
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,t54]) ).
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,t47]) ).
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,t66]) ).
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,t289]) ).
cnf(g0_5,plain,
add(sF2,add(additive_inverse(multiply(sF0,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,t47]) ).
cnf(g0_6,plain,
add(sF2,add(additive_inverse(multiply(sF0,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_5,t48]) ).
cnf(g0_7,plain,
add(sF2,add(additive_inverse(sF4),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,t329]) ).
cnf(g0_8,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_7,t395]) ).
cnf(g0_9,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_8,t647]) ).
cnf(g0_10,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_9,t54]) ).
cnf(g0_11,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_10,t47]) ).
cnf(g0_12,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_11,t48]) ).
cnf(g0_13,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_12,t329]) ).
cnf(g0_14,plain,
add(sF6,add(sF4,add(additive_inverse(multiply(a,multiply(b,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_13,t48]) ).
cnf(g0_15,plain,
add(sF6,add(sF4,add(additive_inverse(multiply(a,sF7)),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,t68]) ).
cnf(g0_16,plain,
add(sF6,add(sF4,add(additive_inverse(sF8),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,t466]) ).
cnf(g0_17,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_16,t538]) ).
cnf(g0_18,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_17,t771]) ).
cnf(g0_19,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_18,t820]) ).
cnf(g0_20,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_19,t54]) ).
cnf(g0_21,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_20,t54]) ).
cnf(g0_22,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_21,t49]) ).
cnf(g0_23,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_22,t70]) ).
cnf(g0_24,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_23,t658]) ).
cnf(g0_25,plain,
add(sF11,additive_inverse(add(sF14,add(additive_inverse(multiply(a,multiply(sF12,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,t49]) ).
cnf(g0_26,plain,
add(sF11,additive_inverse(add(sF14,add(additive_inverse(multiply(a,sF15)),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,t72]) ).
cnf(g0_27,plain,
add(sF11,additive_inverse(add(sF14,add(additive_inverse(sF16),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,t730]) ).
cnf(g0_28,plain,
add(sF11,additive_inverse(add(sF14,add(sF17,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,t754]) ).
cnf(g0_29,plain,
add(sF11,additive_inverse(add(sF18,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_28,t1074]) ).
cnf(g0_30,plain,
add(sF11,additive_inverse(add(sF18,add(multiply(a,add(multiply(sF12,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,t49]) ).
cnf(g0_31,plain,
add(sF11,additive_inverse(add(sF18,add(multiply(a,add(sF15,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,t72]) ).
cnf(g0_32,plain,
add(sF11,additive_inverse(add(sF18,add(multiply(a,add(sF15,additive_inverse(multiply(b,sF3)))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_31,t48]) ).
cnf(g0_33,plain,
add(sF11,additive_inverse(add(sF18,add(multiply(a,add(sF15,additive_inverse(sF7))),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_32,t68]) ).
cnf(g0_34,plain,
add(sF11,additive_inverse(add(sF18,add(multiply(a,add(sF15,sF19)),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_33,t93]) ).
cnf(g0_35,plain,
add(sF11,additive_inverse(add(sF18,add(multiply(a,sF20),multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_34,t800]) ).
cnf(g0_36,plain,
add(sF11,additive_inverse(add(sF18,add(sF21,multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d))))) != additive_identity,
inference(rw,[status(thm)],[g0_35,t824]) ).
cnf(g0_37,plain,
add(sF11,additive_inverse(add(sF22,multiply(add(multiply(multiply(a,b),c),additive_inverse(multiply(a,multiply(b,c)))),d)))) != additive_identity,
inference(rw,[status(thm)],[g0_36,t2113]) ).
cnf(g0_38,plain,
add(sF11,additive_inverse(add(sF22,multiply(add(multiply(sF0,c),additive_inverse(multiply(a,multiply(b,c)))),d)))) != additive_identity,
inference(rw,[status(thm)],[g0_37,t47]) ).
cnf(g0_39,plain,
add(sF11,additive_inverse(add(sF22,multiply(add(sF1,additive_inverse(multiply(a,multiply(b,c)))),d)))) != additive_identity,
inference(rw,[status(thm)],[g0_38,t66]) ).
cnf(g0_40,plain,
add(sF11,additive_inverse(add(sF22,multiply(add(sF1,additive_inverse(multiply(a,sF12))),d)))) != additive_identity,
inference(rw,[status(thm)],[g0_39,t49]) ).
cnf(g0_41,plain,
add(sF11,additive_inverse(add(sF22,multiply(add(sF1,additive_inverse(sF13)),d)))) != additive_identity,
inference(rw,[status(thm)],[g0_40,t70]) ).
cnf(g0_42,plain,
add(sF11,additive_inverse(add(sF22,multiply(add(sF1,sF23),d)))) != additive_identity,
inference(rw,[status(thm)],[g0_41,t921]) ).
cnf(g0_43,plain,
add(sF11,additive_inverse(add(sF22,multiply(sF24,d)))) != additive_identity,
inference(rw,[status(thm)],[g0_42,t969]) ).
cnf(g0_44,plain,
add(sF11,additive_inverse(add(sF22,sF25))) != additive_identity,
inference(rw,[status(thm)],[g0_43,t1031]) ).
cnf(g0_45,plain,
add(sF11,additive_inverse(sF11)) != additive_identity,
inference(rw,[status(thm)],[g0_44,t3600]) ).
cnf(g0_46,plain,
additive_identity != additive_identity,
inference(rw,[status(thm)],[g0_45,t50]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_46]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG026-6 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n017.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 07:44:49 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.06/1.74 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.06/1.74 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------