%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MED008+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 : n026.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:57 PM UTC 2026
% Result : Theorem 9.58s 2.07s
% Output : CNFRefutation 9.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 19
% Syntax : Number of formulae : 147 ( 23 unt; 9 def)
% Number of atoms : 675 ( 0 equ)
% Maximal formula atoms : 30 ( 4 avg)
% Number of connectives : 840 ( 312 ~; 304 |; 179 &)
% ( 15 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 1 con; 0-1 aty)
% Number of variables : 287 ( 265 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( ( gt(Y,Z)
& gt(X,Y) )
=> gt(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X0] :
( ~ conditionnormo(X0)
| ~ conditionhyper(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> drugi(X1) )
=> ! [X1] :
( ~ gt(X0,X1)
=> ( uptakepg(X1)
& uptakelg(X1) ) ) ),
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(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(f35,axiom,
! [X0,X1] :
( ~ gt(X0,X1)
=> ( ~ releaselg(X1)
=> uptakelg(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(f44,plain,
! [X,Y,Z] :
( gt(X,Z)
| ~ gt(Y,Z)
| ~ gt(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
! [X,Z] :
( gt(X,Z)
| ! [Y] :
( ~ gt(Y,Z)
| ~ gt(X,Y) ) ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0,X1,X2] :
( gt(X0,X2)
| ~ gt(X1,X2)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f53,plain,
! [X0] :
( ~ conditionnormo(X0)
| ~ conditionhyper(X0) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f55,plain,
! [X0] :
( ! [X1] :
( ( uptakepg(X1)
& uptakelg(X1) )
| gt(X0,X1) )
| ? [X1] :
( ~ drugi(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f56,definition,
! [X1] :
( sP0_prd(X1)
<=> ( uptakepg(X1)
& uptakelg(X1) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f57,plain,
! [X0] :
( ! [X1] :
( sP0_prd(X1)
| gt(X0,X1) )
| ? [X1] :
( ~ drugi(X1)
& ~ gt(X0,X1) ) ),
inference(formula_renaming,[status(thm)],[f55,f56]) ).
fof(f58,plain,
! [X0] :
( ! [X1] :
( sP0_prd(X1)
| gt(X0,X1) )
| ( ~ drugi(sK0_skl(X0))
& ~ gt(X0,sK0_skl(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X1,sK0_skl(X0))],[f57]) ).
fof(f59,plain,
! [X0,X1] :
( sP0_prd(X1)
| gt(X0,X1)
| ~ gt(X0,sK0_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0,X1] :
( sP0_prd(X1)
| gt(X0,X1)
| ~ drugi(sK0_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
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(f108,plain,
! [X0,X1] :
( uptakelg(X1)
| gt(X0,X1)
| sP6_prd(X0)
| sP5_prd(sK7_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
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(f132,plain,
! [X0,X1] :
( drugi(X1)
| gt(X0,X1)
| ~ gt(X0,sK8_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [X0,X1] :
( drugi(X1)
| gt(X0,X1)
| ~ uptakelg(sK8_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
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(f136,plain,
! [X0,X1] :
( uptakelg(X1)
| releaselg(X1)
| gt(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f137,plain,
! [X1] :
( uptakelg(X1)
| releaselg(X1)
| ! [X0] : gt(X0,X1) ),
inference(miniscoping,[status(thm)],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( uptakelg(X1)
| releaselg(X1)
| gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
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(f168,plain,
! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f169,plain,
~ bcapacitysn(n0),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f171,plain,
! [X0] :
( conditionnormo(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f172,plain,
! [X1] :
( ( ~ uptakepg(X1)
| ~ uptakelg(X1)
| sP0_prd(X1) )
& ( ( uptakepg(X1)
& uptakelg(X1) )
| ~ sP0_prd(X1) ) ),
inference(NNF_transformation,[status(thm)],[f56]) ).
fof(f173,plain,
( ! [X1] :
( ~ uptakepg(X1)
| ~ uptakelg(X1)
| sP0_prd(X1) )
& ! [X1] :
( ( uptakepg(X1)
& uptakelg(X1) )
| ~ sP0_prd(X1) ) ),
inference(miniscoping,[status(thm)],[f172]) ).
fof(f174,plain,
! [X0] :
( uptakelg(X0)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
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(f277,plain,
! [X0] :
( bcapacitysn(X0)
| ~ 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(f299,plain,
conditionnormo(n0),
inference(resolution,[status(thm)],[f43,f171]) ).
fof(f300,plain,
! [X0] :
( ~ gt(n0,X0)
| ~ conditionnormo(X0) ),
inference(resolution,[status(thm)],[f53,f168]) ).
fof(f303,plain,
! [X0,X1] :
( ~ conditionnormo(X1)
| ~ gt(X0,X1)
| ~ gt(n0,X0) ),
inference(resolution,[status(thm)],[f46,f300]) ).
fof(f304,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| ~ gt(X0,X1) ),
inference(resolution,[status(thm)],[f46,f43]) ).
fof(f308,plain,
! [X0,X1,X2] :
( ~ gt(X2,X0)
| ~ gt(X1,X2)
| ~ gt(X0,X1) ),
inference(resolution,[status(thm)],[f304,f46]) ).
fof(f315,plain,
! [X0,X1,X2] :
( ~ gt(X2,X0)
| ~ gt(n0,X2)
| ~ conditionnormo(X1)
| ~ gt(X0,X1) ),
inference(resolution,[status(thm)],[f303,f46]) ).
fof(f322,plain,
! [X0,X1,X2,X3] :
( ~ gt(X3,X0)
| ~ gt(X2,X3)
| ~ gt(X1,X2)
| ~ gt(X0,X1) ),
inference(resolution,[status(thm)],[f308,f46]) ).
fof(f342,plain,
! [X0] :
( ~ s1(X0)
| ~ drugi(X0) ),
inference(resolution,[status(thm)],[f129,f101]) ).
fof(f402,plain,
~ sP12_prd(n0),
inference(resolution,[status(thm)],[f277,f169]) ).
fof(f405,plain,
~ sP14_prd(n0),
inference(resolution,[status(thm)],[f294,f169]) ).
fof(f406,plain,
~ sP11_prd(n0),
inference(resolution,[status(thm)],[f405,f269]) ).
fof(f411,plain,
! [X0] :
( ~ conditionnormo(X0)
| sP0_prd(X0)
| ~ drugi(sK0_skl(n0)) ),
inference(resolution,[status(thm)],[f60,f300]) ).
fof(f524,plain,
! [X0] :
( conditionnormo(X0)
| ~ sP5_prd(X0,n0) ),
inference(resolution,[status(thm)],[f214,f171]) ).
fof(f529,plain,
! [X0] : ~ sP5_prd(X0,n0),
inference(forward_subsumption_resolution,[status(thm)],[f524,f215]) ).
fof(f680,plain,
( sP12_prd(n0)
| ~ sP9_prd(n0) ),
inference(resolution,[status(thm)],[f250,f406]) ).
fof(f683,plain,
~ sP9_prd(n0),
inference(forward_subsumption_resolution,[status(thm)],[f680,f402]) ).
fof(f856,plain,
! [X0] :
( uptakelg(X0)
| releaselg(X0) ),
inference(resolution,[status(thm)],[f138,f322]) ).
fof(f1301,plain,
! [X0] :
( uptakelg(X0)
| gt(n0,X0)
| sP6_prd(n0) ),
inference(resolution,[status(thm)],[f108,f529]) ).
fof(f1541,plain,
! [X0] :
( ~ conditionnormo(X0)
| uptakelg(X0)
| sP6_prd(n0) ),
inference(resolution,[status(thm)],[f1301,f300]) ).
fof(f1663,plain,
! [X0] :
( drugi(X0)
| ~ gt(X0,sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f132,f43]) ).
fof(f1670,plain,
( ~ conditionnormo(n0)
| drugi(n0)
| ~ uptakelg(sK8_skl(n0)) ),
inference(resolution,[status(thm)],[f133,f315]) ).
fof(f1688,plain,
! [X0] :
( drugi(X0)
| ~ uptakelg(sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f133,f322]) ).
fof(f1713,plain,
( drugi(n0)
| ~ uptakelg(sK8_skl(n0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1670,f299]) ).
fof(f1723,plain,
! [X0] :
( ~ conditionnormo(X0)
| drugi(X0)
| ~ gt(n0,sK9_skl(n0)) ),
inference(resolution,[status(thm)],[f134,f300]) ).
fof(f1768,plain,
( ~ s1(n0)
| ~ uptakelg(sK8_skl(n0)) ),
inference(resolution,[status(thm)],[f1713,f342]) ).
fof(f1770,plain,
~ uptakelg(sK8_skl(n0)),
inference(forward_subsumption_resolution,[status(thm)],[f1768,f167]) ).
fof(f1771,plain,
( ~ conditionnormo(sK8_skl(n0))
| sP6_prd(n0) ),
inference(resolution,[status(thm)],[f1770,f1541]) ).
fof(f1774,plain,
releaselg(sK8_skl(n0)),
inference(resolution,[status(thm)],[f1770,f856]) ).
fof(f1775,plain,
~ sP0_prd(sK8_skl(n0)),
inference(resolution,[status(thm)],[f1770,f174]) ).
fof(f1832,plain,
( ~ conditionnormo(sK8_skl(n0))
| ~ drugi(sK0_skl(n0)) ),
inference(resolution,[status(thm)],[f1775,f411]) ).
fof(f1837,plain,
! [X0] :
( ~ s1(X0)
| ~ uptakelg(sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f1688,f342]) ).
fof(f1839,plain,
! [X0] :
( ~ s1(X0)
| ~ gt(X0,sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f1663,f342]) ).
fof(f1850,plain,
! [X0] :
( ~ conditionnormo(X0)
| drugi(X0)
| ~ uptakepg(sK9_skl(n0)) ),
inference(resolution,[status(thm)],[f135,f300]) ).
fof(f1960,plain,
! [X0] :
( ~ sP0_prd(sK8_skl(X0))
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f1837,f174]) ).
fof(f2128,plain,
( conditionnormo(sK8_skl(n0))
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f1839,f171]) ).
fof(f2153,plain,
! [X0] :
( sP0_prd(sK8_skl(X0))
| ~ gt(X0,sK0_skl(X0))
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f1839,f59]) ).
fof(f2157,plain,
conditionnormo(sK8_skl(n0)),
inference(forward_subsumption_resolution,[status(thm)],[f2128,f167]) ).
fof(f2164,plain,
! [X0] :
( ~ gt(X0,sK0_skl(X0))
| ~ s1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2153,f1960]) ).
fof(f2166,plain,
sP6_prd(n0),
inference(backward_subsumption_resolution,[status(thm)],[f1771,f2157]) ).
fof(f2523,plain,
( conditionnormo(sK0_skl(n0))
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f2164,f171]) ).
fof(f2553,plain,
conditionnormo(sK0_skl(n0)),
inference(forward_subsumption_resolution,[status(thm)],[f2523,f167]) ).
fof(f4651,plain,
! [X0,X1] :
( ~ conditionnormo(X0)
| uptakepg(X1)
| gt(n0,X1)
| ~ releaselg(X0)
| ~ sP13_prd(n0) ),
inference(resolution,[status(thm)],[f284,f300]) ).
fof(f4779,plain,
~ drugi(sK0_skl(n0)),
inference(forward_subsumption_resolution,[status(thm)],[f1832,f2157]) ).
fof(f4780,plain,
( ~ conditionnormo(sK0_skl(n0))
| ~ uptakepg(sK9_skl(n0)) ),
inference(resolution,[status(thm)],[f4779,f1850]) ).
fof(f4781,plain,
( ~ conditionnormo(sK0_skl(n0))
| ~ gt(n0,sK9_skl(n0)) ),
inference(resolution,[status(thm)],[f4779,f1723]) ).
fof(f4788,plain,
~ uptakepg(sK9_skl(n0)),
inference(forward_subsumption_resolution,[status(thm)],[f4780,f2553]) ).
fof(f4789,plain,
~ gt(n0,sK9_skl(n0)),
inference(forward_subsumption_resolution,[status(thm)],[f4781,f2553]) ).
fof(f5501,plain,
! [X0] :
( ~ conditionnormo(X0)
| uptakepg(sK9_skl(n0))
| ~ releaselg(X0)
| ~ sP13_prd(n0) ),
inference(resolution,[status(thm)],[f4651,f4789]) ).
fof(f5578,plain,
! [X0] :
( ~ conditionnormo(X0)
| ~ releaselg(X0)
| ~ sP13_prd(n0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5501,f4788]) ).
fof(f5608,plain,
( ~ conditionnormo(sK8_skl(n0))
| ~ sP13_prd(n0) ),
inference(resolution,[status(thm)],[f5578,f1774]) ).
fof(f5611,plain,
~ sP13_prd(n0),
inference(forward_subsumption_resolution,[status(thm)],[f5608,f2157]) ).
fof(f5617,plain,
~ sP10_prd(n0),
inference(resolution,[status(thm)],[f5611,f260]) ).
fof(f5620,plain,
( sP9_prd(n0)
| ~ sP6_prd(n0) ),
inference(resolution,[status(thm)],[f5617,f224]) ).
fof(f5621,plain,
sP9_prd(n0),
inference(forward_subsumption_resolution,[status(thm)],[f5620,f2166]) ).
fof(f5622,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5621,f683]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED008+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.38 % Computer : n026.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Mon Sep 21 01:22:54 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.02/0.39 % Drodi V4.1.1
% 9.58/2.07 % Refutation found
% 9.58/2.07 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.58/2.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.73/2.11 % Elapsed time: 1.712388 seconds
% 12.73/2.11 % CPU time: 13.190559 seconds
% 12.73/2.11 % Total memory used: 80.189 MB
% 12.73/2.11 % Net memory used: 70.710 MB
%------------------------------------------------------------------------------