%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MED006+1 : TPTP v9.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 11:03:01 AM UTC 2025
% Result : Theorem 180.66s 23.07s
% Output : CNFRefutation 180.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 10
% Syntax : Number of formulae : 74 ( 15 unt; 0 def)
% Number of atoms : 217 ( 0 equ)
% Maximal formula atoms : 30 ( 2 avg)
% Number of connectives : 248 ( 105 ~; 94 |; 20 &)
% ( 0 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-12 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-1 aty)
% Number of variables : 127 ( 54 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(unsuccessfuls1_qilt27,plain,
( ( s1(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& ~ bcapacitysn(n0)
& qilt27(n0) )
=> ~ ! [X0] :
( ~ gt(n0,X0)
=> conditionnormo(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unsuccessfuls1_qilt27) ).
fof(unsuccessfuls1_qilt27_negated,plain,
~ ( ( s1(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& ~ bcapacitysn(n0)
& qilt27(n0) )
=> ~ ! [X0] :
( ~ gt(n0,X0)
=> conditionnormo(X0) ) ),
inference(negate_conjecture,[status(cth)],[unsuccessfuls1_qilt27]) ).
cnf(99,plain,
s1(n0),
inference(cnf,[status(esa)],[unsuccessfuls1_qilt27_negated]) ).
cnf(l0,plain,
s1(n0),
inference(instantiation,[status(thm)],[99]) ).
fof(step2,plain,
! [X0] :
( ( s1(X0)
& ~ qilt27(X0) )
=> drugbg(X0) ),
file('Axioms/MED001+1.ax',step2) ).
cnf(67,plain,
( ~ s1(X0)
| drugbg(X0)
| qilt27(X0) ),
inference(cnf,[status(esa)],[step2]) ).
cnf(l1,plain,
( ~ s1(n0)
| drugbg(n0)
| qilt27(n0) ),
inference(instantiation,[status(thm)],[67]) ).
fof(bgcomp,plain,
! [X0] :
( drugbg(X0)
=> ( ( s1(X0)
& ~ qilt27(X0) )
| s2(X0)
| s3(X0) ) ),
file('Axioms/MED001+1.ax',bgcomp) ).
cnf(73,plain,
( ~ drugbg(X0)
| ~ qilt27(X0)
| s2(X0)
| s3(X0) ),
inference(cnf,[status(esa)],[bgcomp]) ).
cnf(l972,plain,
( ~ drugbg(n0)
| ~ qilt27(n0)
| s2(n0)
| s3(n0) ),
inference(instantiation,[status(thm)],[73]) ).
fof(xorstep6,plain,
! [X0] :
( ~ s1(X0)
| ~ s3(X0) ),
file('Axioms/MED001+1.ax',xorstep6) ).
cnf(46,plain,
( ~ s3(X0)
| ~ s1(X0) ),
inference(cnf,[status(esa)],[xorstep6]) ).
cnf(l1665,plain,
( ~ s3(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[46]) ).
fof(normo,plain,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
=> ( ( ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
| ( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
& bcapacitysn(X0)
& ~ qilt27(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
| ( ( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) ) )
& bcapacityne(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
| ( ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
& bcapacityex(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) ) ) ),
file('Axioms/MED001+1.ax',normo) ).
cnf(63,plain,
( ~ qilt27(X0)
| ~ sP7(X1,X2,X0) ),
inference(cnf,[status(esa)],[normo]) ).
cnf(l336,plain,
( ~ qilt27(n0)
| ~ sP7(X1_1071,X2_1071,n0) ),
inference(instantiation,[status(thm)],[63]) ).
cnf(102,plain,
qilt27(n0),
inference(cnf,[status(esa)],[unsuccessfuls1_qilt27_negated]) ).
cnf(l979,plain,
qilt27(n0),
inference(instantiation,[status(thm)],[102]) ).
cnf(52,plain,
( sP7(X0,X1,X2)
| bcapacitysn(X2)
| sP9(X3,X2,X4,X5)
| sP8(X6,X7,X8,X2,X9)
| ~ sP10(X0,X1,X6,X7,X2,X10,X11,X3,X8,X9,X4,X5) ),
inference(cnf,[status(esa)],[normo]) ).
cnf(l973,plain,
( sP7(X1_1071,X2_1071,n0)
| bcapacitysn(n0)
| sP9(X7_1071,n0,X10_1071,sK16(n0))
| sP8(sK17(n0),sK19(n0),X8_1071,n0,X9_1071)
| ~ sP10(X1_1071,X2_1071,sK17(n0),sK19(n0),n0,X5_1071,X6_1071,X7_1071,X8_1071,X9_1071,X10_1071,sK16(n0)) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(57,plain,
( gt(X0,X1)
| uptakelg(X1)
| ~ sP9(X2,X0,X3,X1) ),
inference(cnf,[status(esa)],[normo]) ).
cnf(l976,plain,
( gt(n0,sK16(n0))
| uptakelg(sK16(n0))
| ~ sP9(X7_1071,n0,X10_1071,sK16(n0)) ),
inference(instantiation,[status(thm)],[57]) ).
fof(insulin_completion,plain,
! [X0] :
( ( ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> drugi(X1) ) ),
file('Axioms/MED001+1.ax',insulin_completion) ).
cnf(78,plain,
( ~ uptakelg(sK16(X0))
| gt(X0,X1)
| drugi(X1) ),
inference(cnf,[status(esa)],[insulin_completion]) ).
cnf(l1096,plain,
( ~ uptakelg(sK16(n0))
| gt(n0,n0)
| drugi(n0) ),
inference(instantiation,[status(thm)],[78]) ).
cnf(77,plain,
( ~ gt(X0,sK16(X0))
| gt(X0,X1)
| drugi(X1) ),
inference(cnf,[status(esa)],[insulin_completion]) ).
cnf(l980,plain,
( ~ gt(n0,sK16(n0))
| gt(n0,n0)
| drugi(n0) ),
inference(instantiation,[status(thm)],[77]) ).
cnf(61,plain,
( ~ releaselg(X0)
| gt(X1,X0)
| gt(X1,X2)
| uptakepg(X2)
| ~ sP8(X2,X0,X3,X1,X4) ),
inference(cnf,[status(esa)],[normo]) ).
cnf(l974,plain,
( ~ releaselg(sK19(n0))
| gt(n0,sK19(n0))
| gt(n0,sK17(n0))
| uptakepg(sK17(n0))
| ~ sP8(sK17(n0),sK19(n0),X8_1071,n0,X9_1071) ),
inference(instantiation,[status(thm)],[61]) ).
fof(irreflexivity_gt,plain,
! [X] : ~ gt(X,X),
file('Axioms/MED001+0.ax',irreflexivity_gt) ).
cnf(0,plain,
~ gt(X0,X0),
inference(cnf,[status(esa)],[irreflexivity_gt]) ).
cnf(l1116,plain,
~ gt(n0,n0),
inference(instantiation,[status(thm)],[0]) ).
cnf(101,plain,
~ bcapacitysn(n0),
inference(cnf,[status(esa)],[unsuccessfuls1_qilt27_negated]) ).
cnf(l983,plain,
~ bcapacitysn(n0),
inference(instantiation,[status(thm)],[101]) ).
fof(bg_completion,plain,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
=> ! [X1] :
( ~ gt(X0,X1)
=> drugbg(X1) ) ),
file('Axioms/MED001+1.ax',bg_completion) ).
cnf(87,plain,
( gt(X0,X1)
| releaselg(sK19(X0))
| drugbg(X1) ),
inference(cnf,[status(esa)],[bg_completion]) ).
cnf(l975,plain,
( gt(n0,n0)
| releaselg(sK19(n0))
| drugbg(n0) ),
inference(instantiation,[status(thm)],[87]) ).
fof(insulincomp,plain,
! [X0] :
( drugi(X0)
=> s3(X0) ),
file('Axioms/MED001+1.ax',insulincomp) ).
cnf(76,plain,
( ~ drugi(X0)
| s3(X0) ),
inference(cnf,[status(esa)],[insulincomp]) ).
cnf(l1103,plain,
( ~ drugi(n0)
| s3(n0) ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l982,plain,
~ gt(n0,n0),
inference(instantiation,[status(thm)],[0]) ).
cnf(80,plain,
( ~ uptakepg(sK17(X0))
| gt(X0,X1)
| drugi(X1) ),
inference(cnf,[status(esa)],[insulin_completion]) ).
cnf(l7601,plain,
( ~ uptakepg(sK17(n0))
| gt(n0,n0)
| drugi(n0) ),
inference(instantiation,[status(thm)],[80]) ).
cnf(86,plain,
( ~ gt(X0,sK19(X0))
| gt(X0,X1)
| drugbg(X1) ),
inference(cnf,[status(esa)],[bg_completion]) ).
cnf(l1147,plain,
( ~ gt(n0,sK19(n0))
| gt(n0,n0)
| drugbg(n0) ),
inference(instantiation,[status(thm)],[86]) ).
cnf(l977,plain,
~ gt(n0,n0),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1799,plain,
( ~ drugi(n0)
| s3(n0) ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l3618,plain,
( ~ drugbg(n0)
| ~ qilt27(n0)
| s2(n0)
| s3(n0) ),
inference(instantiation,[status(thm)],[73]) ).
cnf(l2341,plain,
( ~ s3(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l1194,plain,
~ gt(n0,n0),
inference(instantiation,[status(thm)],[0]) ).
cnf(l7629,plain,
( ~ drugbg(n0)
| ~ qilt27(n0)
| s2(n0)
| s3(n0) ),
inference(instantiation,[status(thm)],[73]) ).
cnf(79,plain,
( ~ gt(X0,sK17(X0))
| gt(X0,X1)
| drugi(X1) ),
inference(cnf,[status(esa)],[insulin_completion]) ).
cnf(l7602,plain,
( ~ gt(n0,sK17(n0))
| gt(n0,n0)
| drugi(n0) ),
inference(instantiation,[status(thm)],[79]) ).
cnf(l10209,plain,
( ~ s3(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l1198,plain,
( ~ s3(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[46]) ).
fof(xorstep5,plain,
! [X0] :
( ~ s1(X0)
| ~ s2(X0) ),
file('Axioms/MED001+1.ax',xorstep5) ).
cnf(45,plain,
( ~ s2(X0)
| ~ s1(X0) ),
inference(cnf,[status(esa)],[xorstep5]) ).
cnf(l7660,plain,
( ~ s2(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l13831,plain,
( ~ drugi(n0)
| s3(n0) ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l7636,plain,
( ~ s3(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l13837,plain,
( ~ s3(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l7605,plain,
( ~ drugi(n0)
| s3(n0) ),
inference(instantiation,[status(thm)],[76]) ).
cnf(l7603,plain,
~ gt(n0,n0),
inference(instantiation,[status(thm)],[0]) ).
cnf(48,plain,
( ~ gt(X0,sK15(X0))
| sP10(X1,X2,X3,X4,X0,X5,X6,X7,X8,X9,X10,X11) ),
inference(cnf,[status(esa)],[normo]) ).
cnf(l1051,plain,
( ~ gt(n0,sK15(n0))
| sP10(X1_1071,X2_1071,sK17(n0),sK19(n0),n0,X5_1071,X6_1071,X7_1071,X8_1071,X9_1071,X10_1071,sK16(n0)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l10207,plain,
( ~ s2(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(103,plain,
( gt(n0,X0)
| conditionnormo(X0) ),
inference(cnf,[status(esa)],[unsuccessfuls1_qilt27_negated]) ).
cnf(l1058,plain,
( gt(n0,sK15(n0))
| conditionnormo(sK15(n0)) ),
inference(instantiation,[status(thm)],[103]) ).
cnf(l1045,plain,
( ~ s2(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l7606,plain,
~ gt(n0,n0),
inference(instantiation,[status(thm)],[0]) ).
cnf(49,plain,
( ~ conditionnormo(sK15(X0))
| sP10(X1,X2,X3,X4,X0,X5,X6,X7,X8,X9,X10,X11) ),
inference(cnf,[status(esa)],[normo]) ).
cnf(l1071,plain,
( ~ conditionnormo(sK15(n0))
| sP10(X1_1071,X2_1071,sK17(n0),sK19(n0),n0,X5_1071,X6_1071,X7_1071,X8_1071,X9_1071,X10_1071,sK16(n0)) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l7608,plain,
( ~ s3(n0)
| ~ s1(n0) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l972,l1665,l336,l979,l973,l976,l1096,l980,l974,l1116,l983,l975,l1103,l982,l7601,l1147,l977,l1799,l3618,l2341,l1194,l7629,l7602,l10209,l1198,l7660,l13831,l7636,l13837,l7605,l7603,l1051,l10207,l1058,l1045,l7606,l1071,l7608]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : MED006+1 : TPTP v9.0.0. Released v3.2.0.
% 0.11/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n022.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Jul 21 07:13:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.35 % launching worker at depth: 10
% 0.18/0.44 % launching worker at depth: 11
% 3.75/0.81 % launching worker at depth: 12
% 28.47/3.97 % launching worker at depth: 13
% 180.66/23.07 % SZS status Theorem for theBenchmark
% 180.66/23.07 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------