%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MED006+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 : Thu Sep 24 01:24:56 PM UTC 2026
% Result : Theorem 1.17s 0.75s
% Output : CNFRefutation 1.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 32
% Syntax : Number of formulae : 163 ( 14 unt; 23 def)
% Number of atoms : 751 ( 0 equ)
% Maximal formula atoms : 30 ( 4 avg)
% Number of connectives : 880 ( 292 ~; 359 |; 172 &)
% ( 29 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 40 ( 39 usr; 16 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 1 con; 0-1 aty)
% Number of variables : 272 ( 251 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X0] :
( ~ s2(X0)
| ~ s1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X0] :
( ~ s3(X0)
| ~ s1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
=> ( ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& bcapacityex(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) ) )
| ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& bcapacityne(X0)
& ( ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) ) ) )
| ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) ) )
| ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X0] :
( drugbg(X0)
=> ( s3(X0)
| s2(X0)
| ( ~ qilt27(X0)
& s1(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X0] :
( drugi(X0)
=> s3(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X0] :
( ( ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> drugi(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
=> ! [X1] :
( ~ gt(X0,X1)
=> drugbg(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,conjecture,
( ( qilt27(n0)
& ~ bcapacitysn(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& s1(n0) )
=> ~ ! [X0] :
( ~ gt(n0,X0)
=> conditionnormo(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
~ ( ( qilt27(n0)
& ~ bcapacitysn(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& s1(n0) )
=> ~ ! [X0] :
( ~ gt(n0,X0)
=> conditionnormo(X0) ) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f43,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f100,plain,
! [X0] :
( ~ s2(X0)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f101,plain,
! [X0] :
( ~ s3(X0)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f103,plain,
! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& bcapacityex(X0)
& ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
| gt(X0,X1) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) )
| ? [X1] :
( ~ conditionnormo(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f104,definition,
! [X0,X1] :
( sP5_prd(X1,X0)
<=> ( ~ conditionnormo(X1)
& ~ gt(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f105,definition,
! [X0] :
( sP6_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f106,plain,
! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& bcapacityex(X0)
& ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
| gt(X0,X1) ) )
| sP6_prd(X0)
| ? [X1] : sP5_prd(X1,X0) ),
inference(formula_renaming,[status(thm)],[f103,f105,f104]) ).
fof(f107,plain,
! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& bcapacityex(X0)
& ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
| gt(X0,X1) ) )
| sP6_prd(X0)
| sP5_prd(sK7_skl(X0),X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X1,sK7_skl(X0))],[f106]) ).
fof(f109,plain,
! [X0,X1] :
( uptakepg(X1)
| gt(X0,X1)
| sP6_prd(X0)
| sP5_prd(sK7_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f122,plain,
! [X0] :
( s3(X0)
| s2(X0)
| ( ~ qilt27(X0)
& s1(X0) )
| ~ drugbg(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f124,plain,
! [X0] :
( s3(X0)
| s2(X0)
| ~ qilt27(X0)
| ~ drugbg(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f128,plain,
! [X0] :
( s3(X0)
| ~ drugi(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f129,plain,
! [X0] :
( s3(X0)
| ~ drugi(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [X0] :
( ! [X1] :
( drugi(X1)
| gt(X0,X1) )
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( ~ uptakelg(X1)
& ~ gt(X0,X1) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f131,plain,
! [X0] :
( ! [X1] :
( drugi(X1)
| gt(X0,X1) )
| ( ~ uptakepg(sK9_skl(X0))
& ~ gt(X0,sK9_skl(X0))
& ~ uptakelg(sK8_skl(X0))
& ~ gt(X0,sK8_skl(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(X1,sK8_skl(X0)),skolemize(X1,sK9_skl(X0))],[f130]) ).
fof(f134,plain,
! [X0,X1] :
( drugi(X1)
| gt(X0,X1)
| ~ gt(X0,sK9_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f135,plain,
! [X0,X1] :
( drugi(X1)
| gt(X0,X1)
| ~ uptakepg(sK9_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f145,plain,
! [X0] :
( ! [X1] :
( drugbg(X1)
| gt(X0,X1) )
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f146,plain,
! [X0] :
( ! [X1] :
( drugbg(X1)
| gt(X0,X1) )
| ( releaselg(sK11_skl(X0))
& ~ gt(X0,sK11_skl(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X1,sK11_skl(X0))],[f145]) ).
fof(f147,plain,
! [X0,X1] :
( drugbg(X1)
| gt(X0,X1)
| ~ gt(X0,sK11_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
! [X0,X1] :
( drugbg(X1)
| gt(X0,X1)
| releaselg(sK11_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f166,plain,
( ! [X0] :
( conditionnormo(X0)
| gt(n0,X0) )
& qilt27(n0)
& ~ bcapacitysn(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& s1(n0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f167,plain,
s1(n0),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f169,plain,
~ bcapacitysn(n0),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f170,plain,
qilt27(n0),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f171,plain,
! [X0] :
( conditionnormo(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f212,plain,
! [X0,X1] :
( ( conditionnormo(X1)
| gt(X0,X1)
| sP5_prd(X1,X0) )
& ( ( ~ conditionnormo(X1)
& ~ gt(X0,X1) )
| ~ sP5_prd(X1,X0) ) ),
inference(NNF_transformation,[status(thm)],[f104]) ).
fof(f213,plain,
( ! [X0,X1] :
( conditionnormo(X1)
| gt(X0,X1)
| sP5_prd(X1,X0) )
& ! [X0,X1] :
( ( ~ conditionnormo(X1)
& ~ gt(X0,X1) )
| ~ sP5_prd(X1,X0) ) ),
inference(miniscoping,[status(thm)],[f212]) ).
fof(f214,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f215,plain,
! [X0,X1] :
( ~ conditionnormo(X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f217,definition,
! [X0] :
( sP9_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP9_prd])],[]) ).
fof(f218,plain,
! [X0] :
( sP6_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| sP9_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f105,f217]) ).
fof(f219,definition,
! [X0] :
( sP10_prd(X0)
<=> ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP10_prd])],[]) ).
fof(f220,plain,
! [X0] :
( sP6_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP10_prd(X0) )
| sP9_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f218,f219]) ).
fof(f221,plain,
! [X0] :
( ( ( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP10_prd(X0) )
& ~ sP9_prd(X0) )
| sP6_prd(X0) )
& ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP10_prd(X0) )
| sP9_prd(X0)
| ~ sP6_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f220]) ).
fof(f222,plain,
( ! [X0] :
( ( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP10_prd(X0) )
& ~ sP9_prd(X0) )
| sP6_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP10_prd(X0) )
| sP9_prd(X0)
| ~ sP6_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f221]) ).
fof(f223,plain,
( ! [X0] :
( ( ( ( ~ conditionhyper(sK20_skl(X0))
& gt(X0,sK20_skl(X0)) )
| ~ sP10_prd(X0) )
& ~ sP9_prd(X0) )
| sP6_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP10_prd(X0) )
| sP9_prd(X0)
| ~ sP6_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(X1,sK20_skl(X0))],[f222]) ).
fof(f224,plain,
! [X0] :
( sP10_prd(X0)
| sP9_prd(X0)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f243,definition,
! [X0] :
( sP11_prd(X0)
<=> ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP11_prd])],[]) ).
fof(f244,plain,
! [X0] :
( sP9_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| sP11_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f217,f243]) ).
fof(f245,definition,
! [X0] :
( sP12_prd(X0)
<=> ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP12_prd])],[]) ).
fof(f246,plain,
! [X0] :
( sP9_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP12_prd(X0) )
| sP11_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f244,f245]) ).
fof(f247,plain,
! [X0] :
( ( ( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP12_prd(X0) )
& ~ sP11_prd(X0) )
| sP9_prd(X0) )
& ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP12_prd(X0) )
| sP11_prd(X0)
| ~ sP9_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f246]) ).
fof(f248,plain,
( ! [X0] :
( ( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP12_prd(X0) )
& ~ sP11_prd(X0) )
| sP9_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP12_prd(X0) )
| sP11_prd(X0)
| ~ sP9_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f247]) ).
fof(f249,plain,
( ! [X0] :
( ( ( ( ~ conditionhyper(sK23_skl(X0))
& gt(X0,sK23_skl(X0)) )
| ~ sP12_prd(X0) )
& ~ sP11_prd(X0) )
| sP9_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP12_prd(X0) )
| sP11_prd(X0)
| ~ sP9_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(X1,sK23_skl(X0))],[f248]) ).
fof(f250,plain,
! [X0] :
( sP12_prd(X0)
| sP11_prd(X0)
| ~ sP9_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f255,definition,
! [X0] :
( sP13_prd(X0)
<=> ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP13_prd])],[]) ).
fof(f256,plain,
! [X0] :
( sP10_prd(X0)
<=> ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& sP13_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f219,f255]) ).
fof(f257,plain,
! [X0] :
( ( ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| ~ sP13_prd(X0)
| sP10_prd(X0) )
& ( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& sP13_prd(X0) )
| ~ sP10_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f256]) ).
fof(f258,plain,
( ! [X0] :
( ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| ~ sP13_prd(X0)
| sP10_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& sP13_prd(X0) )
| ~ sP10_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f257]) ).
fof(f259,plain,
( ! [X0] :
( ( ~ bsecretioni(sK24_skl(X0))
& ~ gt(X0,sK24_skl(X0)) )
| ~ sP13_prd(X0)
| sP10_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& sP13_prd(X0) )
| ~ sP10_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(X1,sK24_skl(X0))],[f258]) ).
fof(f260,plain,
! [X0] :
( sP13_prd(X0)
| ~ sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f259]) ).
fof(f264,definition,
! [X0] :
( sP14_prd(X0)
<=> ( qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP14_prd])],[]) ).
fof(f265,plain,
! [X0] :
( sP11_prd(X0)
<=> ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP14_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f243,f264]) ).
fof(f266,plain,
! [X0] :
( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP14_prd(X0)
| sP11_prd(X0) )
& ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP14_prd(X0) )
| ~ sP11_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f265]) ).
fof(f267,plain,
( ! [X0] :
( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP14_prd(X0)
| sP11_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP14_prd(X0) )
| ~ sP11_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f266]) ).
fof(f268,plain,
( ! [X0] :
( ( ~ conditionhyper(sK25_skl(X0))
& gt(X0,sK25_skl(X0)) )
| ~ sP14_prd(X0)
| sP11_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP14_prd(X0) )
| ~ sP11_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(X1,sK25_skl(X0))],[f267]) ).
fof(f269,plain,
! [X0] :
( sP14_prd(X0)
| ~ sP11_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f273,plain,
! [X0] :
( ( qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) )
| sP12_prd(X0) )
& ( ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ~ sP12_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f245]) ).
fof(f274,plain,
( ! [X0] :
( qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) )
| sP12_prd(X0) )
& ! [X0] :
( ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ~ sP12_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f273]) ).
fof(f275,plain,
( ! [X0] :
( qilt27(X0)
| ~ bcapacitysn(X0)
| ( releaselg(sK26_skl(X0))
& ~ gt(X0,sK26_skl(X0)) )
| sP12_prd(X0) )
& ! [X0] :
( ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ~ sP12_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(X1,sK26_skl(X0))],[f274]) ).
fof(f276,plain,
! [X0,X1] :
( ~ releaselg(X1)
| gt(X0,X1)
| ~ sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f281,plain,
! [X0] :
( ( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) )
| sP13_prd(X0) )
& ( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ~ sP13_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f255]) ).
fof(f282,plain,
( ! [X0] :
( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) )
| sP13_prd(X0) )
& ! [X0] :
( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ~ sP13_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f281]) ).
fof(f283,plain,
( ! [X0] :
( ~ bcapacityne(X0)
| ( ~ uptakepg(sK28_skl(X0))
& ~ gt(X0,sK28_skl(X0))
& releaselg(sK27_skl(X0))
& ~ gt(X0,sK27_skl(X0)) )
| sP13_prd(X0) )
& ! [X0] :
( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ~ sP13_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl]),skolemize(X1,sK27_skl(X0)),skolemize(X1,sK28_skl(X0))],[f282]) ).
fof(f284,plain,
! [X0,X1,X2] :
( uptakepg(X2)
| gt(X0,X2)
| ~ releaselg(X1)
| gt(X0,X1)
| ~ sP13_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f290,plain,
! [X0] :
( ( ~ qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| sP14_prd(X0) )
& ( ( qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) )
| ~ sP14_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f264]) ).
fof(f291,plain,
( ! [X0] :
( ~ qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| sP14_prd(X0) )
& ! [X0] :
( ( qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) )
| ~ sP14_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f290]) ).
fof(f292,plain,
( ! [X0] :
( ~ qilt27(X0)
| ~ bcapacitysn(X0)
| ( ~ bsecretioni(sK29_skl(X0))
& ~ gt(X0,sK29_skl(X0)) )
| sP14_prd(X0) )
& ! [X0] :
( ( qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) )
| ~ sP14_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(X1,sK29_skl(X0))],[f291]) ).
fof(f294,plain,
! [X0] :
( bcapacitysn(X0)
| ~ sP14_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f306,definition,
( sQ0_spl
<=> s1(n0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f308,plain,
( sQ0_spl
| ~ s1(n0) ),
inference(component_clause,[status(thm)],[f306]) ).
fof(f313,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f308,f167]) ).
fof(f314,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f313]) ).
fof(f325,plain,
! [X0] :
( ~ sP11_prd(X0)
| bcapacitysn(X0) ),
inference(resolution,[status(thm)],[f294,f269]) ).
fof(f346,plain,
! [X0,X1] :
( sP11_prd(X0)
| ~ sP9_prd(X0)
| ~ releaselg(X1)
| gt(X0,X1) ),
inference(resolution,[status(thm)],[f276,f250]) ).
fof(f349,plain,
! [X0,X1,X2] :
( ~ sP10_prd(X0)
| uptakepg(X2)
| gt(X0,X2)
| ~ releaselg(X1)
| gt(X0,X1) ),
inference(resolution,[status(thm)],[f284,f260]) ).
fof(f367,definition,
( sQ2_spl
<=> sP11_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f368,plain,
( ~ sQ2_spl
| sP11_prd(n0) ),
inference(component_clause,[status(thm)],[f367]) ).
fof(f411,definition,
( sQ12_spl
<=> sP5_prd(sK7_skl(n0),n0) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f412,plain,
( ~ sQ12_spl
| sP5_prd(sK7_skl(n0),n0) ),
inference(component_clause,[status(thm)],[f411]) ).
fof(f413,plain,
( sQ12_spl
| ~ sP5_prd(sK7_skl(n0),n0) ),
inference(component_clause,[status(thm)],[f411]) ).
fof(f418,definition,
! [X0] :
( sQ14_spl
<=> ( uptakepg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f419,plain,
! [X0] :
( ~ sQ14_spl
| uptakepg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f429,plain,
( ~ sQ2_spl
| bcapacitysn(n0) ),
inference(resolution,[status(thm)],[f368,f325]) ).
fof(f430,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f429,f169]) ).
fof(f431,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f430]) ).
fof(f443,definition,
! [X0] :
( sQ16_spl
<=> ( ~ releaselg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f444,plain,
! [X0] :
( ~ sQ16_spl
| ~ releaselg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f499,plain,
( ~ sQ12_spl
| ~ gt(n0,sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f412,f214]) ).
fof(f500,plain,
( ~ sQ12_spl
| ~ conditionnormo(sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f412,f215]) ).
fof(f504,plain,
! [X0,X1] :
( ~ sQ14_spl
| drugi(X1)
| gt(X0,X1)
| gt(n0,sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f419,f135]) ).
fof(f526,plain,
( ~ sQ12_spl
| gt(n0,sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f500,f171]) ).
fof(f527,plain,
( ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f526,f499]) ).
fof(f528,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f527]) ).
fof(f567,plain,
! [X0,X1] :
( ~ sQ16_spl
| drugbg(X1)
| gt(X0,X1)
| gt(n0,sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f444,f148]) ).
fof(f602,plain,
! [X0,X1] :
( ~ sQ14_spl
| s3(X1)
| gt(X0,X1)
| gt(n0,sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f504,f129]) ).
fof(f606,plain,
! [X0,X1] :
( ~ sQ16_spl
| s3(X1)
| s2(X1)
| ~ qilt27(X1)
| gt(X0,X1)
| gt(n0,sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f567,f124]) ).
fof(f622,definition,
( sQ25_spl
<=> sP9_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( ~ sQ25_spl
| sP9_prd(n0) ),
inference(component_clause,[status(thm)],[f622]) ).
fof(f831,definition,
! [X2] :
( sQ42_spl
<=> ( drugi(X2)
| gt(n0,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f832,plain,
! [X0] :
( ~ sQ42_spl
| drugi(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f831]) ).
fof(f855,plain,
! [X0] :
( ~ sQ42_spl
| s3(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f832,f129]) ).
fof(f858,plain,
! [X0] :
( ~ sQ42_spl
| ~ s1(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f855,f101]) ).
fof(f866,plain,
! [X0,X1] :
( uptakepg(X1)
| gt(X0,X1)
| sP5_prd(sK7_skl(X0),X0)
| sP10_prd(X0)
| sP9_prd(X0) ),
inference(resolution,[status(thm)],[f224,f109]) ).
fof(f921,plain,
( ~ sQ42_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f858,f167]) ).
fof(f925,plain,
( ~ sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f921,f43]) ).
fof(f926,plain,
~ sQ42_spl,
inference(contradiction_clause,[status(thm)],[f925]) ).
fof(f933,plain,
! [X0,X1,X2,X3] :
( uptakepg(X3)
| gt(X0,X3)
| ~ releaselg(X2)
| gt(X0,X2)
| uptakepg(X1)
| gt(X0,X1)
| sP5_prd(sK7_skl(X0),X0)
| sP9_prd(X0) ),
inference(resolution,[status(thm)],[f866,f349]) ).
fof(f984,plain,
! [X0,X1,X2] :
( sQ12_spl
| uptakepg(X2)
| gt(n0,X2)
| ~ releaselg(X1)
| gt(n0,X1)
| uptakepg(X0)
| gt(n0,X0)
| sP9_prd(n0) ),
inference(resolution,[status(thm)],[f933,f413]) ).
fof(f987,plain,
( sQ12_spl
| sQ16_spl
| sQ14_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f984,f622,f418,f443,f411]) ).
fof(f1002,definition,
( sQ50_spl
<=> gt(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1003,plain,
( ~ sQ50_spl
| gt(n0,n0) ),
inference(component_clause,[status(thm)],[f1002]) ).
fof(f1011,plain,
( ~ sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1003,f43]) ).
fof(f1012,plain,
~ sQ50_spl,
inference(contradiction_clause,[status(thm)],[f1011]) ).
fof(f1068,plain,
! [X0] :
( ~ sQ25_spl
| sP11_prd(n0)
| ~ releaselg(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f623,f346]) ).
fof(f1074,plain,
( ~ sQ25_spl
| sQ2_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f1068,f443,f367,f622]) ).
fof(f1166,definition,
! [X0] :
( sQ61_spl
<=> gt(X0,sK22_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1167,plain,
! [X0] :
( ~ sQ61_spl
| gt(X0,sK22_skl(n0)) ),
inference(component_clause,[status(thm)],[f1166]) ).
fof(f1170,definition,
! [X0] :
( sQ62_spl
<=> gt(X0,sK28_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1171,plain,
! [X0] :
( ~ sQ62_spl
| gt(X0,sK28_skl(n0)) ),
inference(component_clause,[status(thm)],[f1170]) ).
fof(f1208,plain,
( ~ sQ62_spl
| $false ),
inference(resolution,[status(thm)],[f1171,f43]) ).
fof(f1212,plain,
~ sQ62_spl,
inference(contradiction_clause,[status(thm)],[f1208]) ).
fof(f1228,plain,
( ~ sQ61_spl
| $false ),
inference(resolution,[status(thm)],[f1167,f43]) ).
fof(f1235,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f1228]) ).
fof(f1327,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ s1(X1)
| gt(X0,X1)
| gt(n0,sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f602,f101]) ).
fof(f1494,plain,
! [X0] :
( ~ sQ14_spl
| gt(X0,n0)
| gt(n0,sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f1327,f167]) ).
fof(f1499,plain,
! [X0] :
( ~ sQ14_spl
| drugi(X0)
| gt(n0,X0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f1494,f134]) ).
fof(f1504,plain,
( ~ sQ14_spl
| sQ42_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f1499,f1002,f831,f418]) ).
fof(f1518,definition,
( sQ81_spl
<=> s2(n0) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1519,plain,
( ~ sQ81_spl
| s2(n0) ),
inference(component_clause,[status(thm)],[f1518]) ).
fof(f1521,definition,
( sQ82_spl
<=> s3(n0) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1522,plain,
( ~ sQ82_spl
| s3(n0) ),
inference(component_clause,[status(thm)],[f1521]) ).
fof(f1537,plain,
( ~ sQ82_spl
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f1522,f101]) ).
fof(f1538,plain,
( ~ sQ82_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1537,f306,f1521]) ).
fof(f1545,plain,
( ~ sQ81_spl
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f1519,f100]) ).
fof(f1554,plain,
( ~ sQ81_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1545,f306,f1518]) ).
fof(f1860,definition,
! [X0] :
( sQ96_spl
<=> gt(X0,sK26_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1861,plain,
! [X0] :
( ~ sQ96_spl
| gt(X0,sK26_skl(n0)) ),
inference(component_clause,[status(thm)],[f1860]) ).
fof(f1908,plain,
( ~ sQ96_spl
| $false ),
inference(resolution,[status(thm)],[f1861,f43]) ).
fof(f1915,plain,
~ sQ96_spl,
inference(contradiction_clause,[status(thm)],[f1908]) ).
fof(f1955,plain,
! [X0] :
( ~ sQ16_spl
| s3(n0)
| s2(n0)
| gt(X0,n0)
| gt(n0,sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f606,f170]) ).
fof(f1957,definition,
! [X0] :
( sQ103_spl
<=> ( gt(X0,n0)
| gt(n0,sK11_skl(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1958,plain,
! [X0] :
( ~ sQ103_spl
| gt(X0,n0)
| gt(n0,sK11_skl(X0)) ),
inference(component_clause,[status(thm)],[f1957]) ).
fof(f1960,plain,
( ~ sQ16_spl
| sQ82_spl
| sQ81_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f1955,f1957,f1518,f1521,f443]) ).
fof(f1983,plain,
! [X0] :
( ~ sQ103_spl
| drugbg(X0)
| gt(n0,X0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f1958,f147]) ).
fof(f1988,definition,
! [X0] :
( sQ105_spl
<=> ( drugbg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1989,plain,
! [X0] :
( ~ sQ105_spl
| drugbg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f1988]) ).
fof(f1991,plain,
( ~ sQ103_spl
| sQ105_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f1983,f1002,f1988,f1957]) ).
fof(f1998,plain,
! [X0] :
( ~ sQ105_spl
| s3(X0)
| s2(X0)
| ~ qilt27(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f1989,f124]) ).
fof(f2110,plain,
( ~ sQ105_spl
| s3(n0)
| s2(n0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f1998,f170]) ).
fof(f2112,plain,
( ~ sQ105_spl
| sQ82_spl
| sQ81_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f2110,f1002,f1518,f1521,f1988]) ).
fof(f2113,plain,
$false,
inference(sat_refutation,[status(thm)],[f314,f431,f528,f926,f987,f1012,f1074,f1212,f1235,f1504,f1538,f1554,f1915,f1960,f1991,f2112]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED006+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.40 % Computer : n020.cluster.edu
% 0.09/0.40 % Model : x86_64 x86_64
% 0.09/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.40 % Memory : 8046.5625MB
% 0.09/0.40 % OS : Linux 6.8.0-71-generic
% 0.09/0.40 % CPULimit : 300
% 0.09/0.40 % WCLimit : 300
% 0.09/0.40 % DateTime : Mon Sep 21 01:21:02 UTC 2026
% 0.09/0.41 % CPUTime :
% 0.09/0.42 % Drodi V4.1.1
% 1.17/0.75 % Refutation found
% 1.17/0.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.17/0.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.17/0.79 % Elapsed time: 0.368024 seconds
% 1.17/0.79 % CPU time: 2.577036 seconds
% 1.17/0.79 % Total memory used: 38.343 MB
% 1.17/0.79 % Net memory used: 35.886 MB
%------------------------------------------------------------------------------