%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MED002+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 0.09s 0.42s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 25
% Syntax : Number of formulae : 120 ( 9 unt; 18 def)
% Number of atoms : 460 ( 0 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 545 ( 205 ~; 210 |; 86 &)
% ( 19 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 31 ( 30 usr; 16 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-1 aty)
% Number of variables : 146 ( 117 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X0] :
( ~ bcapacityex(X0)
| ~ bcapacityne(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X0] :
( ( ~ bcapacityex(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> drugsu(X1) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> drugbg(X1) )
=> ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X0] :
( ( ! [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)
=> conditionnormo(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X0] :
( ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& bcapacityex(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> ( conditionhypo(X1)
| conditionnormo(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
( ( bcapacityne(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& ! [X0] :
( ~ gt(n0,X0)
=> ( drugsu(X0)
& drugbg(X0) ) ) )
=> ! [X0] :
( ~ gt(n0,X0)
=> conditionnormo(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
~ ( ( bcapacityne(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& ! [X0] :
( ~ gt(n0,X0)
=> ( drugsu(X0)
& drugbg(X0) ) ) )
=> ! [X0] :
( ~ gt(n0,X0)
=> conditionnormo(X0) ) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f26,plain,
! [X0] :
( ~ bcapacityex(X0)
| ~ bcapacityne(X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f42,plain,
! [X0] :
( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
| bcapacityex(X0)
| ? [X1] :
( ~ drugsu(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f43,plain,
! [X0] :
( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
| bcapacityex(X0)
| ( ~ drugsu(sK1_skl(X0))
& ~ gt(X0,sK1_skl(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X1,sK1_skl(X0))],[f42]) ).
fof(f44,plain,
! [X0,X1] :
( bsecretioni(X1)
| gt(X0,X1)
| bcapacityex(X0)
| ~ gt(X0,sK1_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f45,plain,
! [X0,X1] :
( bsecretioni(X1)
| gt(X0,X1)
| bcapacityex(X0)
| ~ drugsu(sK1_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f46,plain,
! [X0] :
( ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) )
| ? [X1] :
( ~ drugbg(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f47,plain,
! [X0] :
( ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) )
| ( ~ drugbg(sK2_skl(X0))
& ~ gt(X0,sK2_skl(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X1,sK2_skl(X0))],[f46]) ).
fof(f48,plain,
! [X0,X1] :
( ~ releaselg(X1)
| gt(X0,X1)
| ~ gt(X0,sK2_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( ~ releaselg(X1)
| gt(X0,X1)
| ~ drugbg(sK2_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f62,plain,
! [X0] :
( ! [X1] :
( conditionnormo(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) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f63,definition,
! [X0] :
( sP3_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,[sP3_prd])],[]) ).
fof(f64,plain,
! [X0] :
( ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| sP3_prd(X0) ),
inference(formula_renaming,[status(thm)],[f62,f63]) ).
fof(f65,plain,
! [X0] :
( ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ( ~ conditionhyper(sK5_skl(X0))
& gt(X0,sK5_skl(X0)) )
| sP3_prd(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(X1,sK5_skl(X0))],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( conditionnormo(X1)
| gt(X0,X1)
| gt(X0,sK5_skl(X0))
| sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [X0,X1] :
( conditionnormo(X1)
| gt(X0,X1)
| ~ conditionhyper(sK5_skl(X0))
| sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f68,plain,
! [X0] :
( ! [X1] :
( conditionhypo(X1)
| conditionnormo(X1)
| gt(X0,X1) )
| ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ bcapacityex(X0)
| ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
| ? [X1] :
( ~ uptakelg(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f69,definition,
! [X0] :
( sP4_prd(X0)
<=> ( ~ bcapacityex(X0)
| ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
| ? [X1] :
( ~ uptakelg(X1)
& ~ gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f74,plain,
( ? [X0] :
( ~ conditionnormo(X0)
& ~ gt(n0,X0) )
& bcapacityne(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& ! [X0] :
( ( drugsu(X0)
& drugbg(X0) )
| gt(n0,X0) ) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f75,plain,
( ~ conditionnormo(sK7_skl)
& ~ gt(n0,sK7_skl)
& bcapacityne(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& ! [X0] :
( ( drugsu(X0)
& drugbg(X0) )
| gt(n0,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X0,sK7_skl)],[f74]) ).
fof(f76,plain,
! [X0] :
( drugbg(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f77,plain,
! [X0] :
( drugsu(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f78,plain,
! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f79,plain,
bcapacityne(n0),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f80,plain,
~ gt(n0,sK7_skl),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f81,plain,
~ conditionnormo(sK7_skl),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f103,definition,
! [X0] :
( sP5_prd(X0)
<=> ( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f104,plain,
! [X0] :
( sP3_prd(X0)
<=> ( ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| sP5_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f63,f103]) ).
fof(f105,plain,
! [X0] :
( ( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& ~ sP5_prd(X0) )
| sP3_prd(X0) )
& ( ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| sP5_prd(X0)
| ~ sP3_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f104]) ).
fof(f106,plain,
( ! [X0] :
( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& ~ sP5_prd(X0) )
| sP3_prd(X0) )
& ! [X0] :
( ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| sP5_prd(X0)
| ~ sP3_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f105]) ).
fof(f107,plain,
( ! [X0] :
( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& ~ sP5_prd(X0) )
| sP3_prd(X0) )
& ! [X0] :
( ( ~ bsecretioni(sK10_skl(X0))
& ~ gt(X0,sK10_skl(X0)) )
| sP5_prd(X0)
| ~ sP3_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X1,sK10_skl(X0))],[f106]) ).
fof(f108,plain,
! [X0] :
( ~ gt(X0,sK10_skl(X0))
| sP5_prd(X0)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [X0] :
( ~ bsecretioni(sK10_skl(X0))
| sP5_prd(X0)
| ~ sP3_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f112,plain,
! [X0] :
( ( ( bcapacityex(X0)
& ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
| gt(X0,X1) ) )
| sP4_prd(X0) )
& ( ~ bcapacityex(X0)
| ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
| ? [X1] :
( ~ uptakelg(X1)
& ~ gt(X0,X1) )
| ~ sP4_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f69]) ).
fof(f113,plain,
( ! [X0] :
( ( bcapacityex(X0)
& ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
| gt(X0,X1) ) )
| sP4_prd(X0) )
& ! [X0] :
( ~ bcapacityex(X0)
| ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
| ? [X1] :
( ~ uptakelg(X1)
& ~ gt(X0,X1) )
| ~ sP4_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f112]) ).
fof(f114,plain,
( ! [X0] :
( ( bcapacityex(X0)
& ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
| gt(X0,X1) ) )
| sP4_prd(X0) )
& ! [X0] :
( ~ bcapacityex(X0)
| ( ~ uptakepg(sK12_skl(X0))
& ~ gt(X0,sK12_skl(X0)) )
| ( ~ uptakelg(sK11_skl(X0))
& ~ gt(X0,sK11_skl(X0)) )
| ~ sP4_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl]),skolemize(X1,sK11_skl(X0)),skolemize(X1,sK12_skl(X0))],[f113]) ).
fof(f121,plain,
! [X0] :
( bcapacityex(X0)
| sP4_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f122,plain,
! [X0] :
( ( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| sP5_prd(X0) )
& ( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) )
| ~ sP5_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f103]) ).
fof(f123,plain,
( ! [X0] :
( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| sP5_prd(X0) )
& ! [X0] :
( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) )
| ~ sP5_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f122]) ).
fof(f124,plain,
( ! [X0] :
( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| sP5_prd(X0) )
& ! [X0] :
( ~ bcapacityne(X0)
| ( ~ uptakepg(sK14_skl(X0))
& ~ gt(X0,sK14_skl(X0))
& releaselg(sK13_skl(X0))
& ~ gt(X0,sK13_skl(X0)) )
| ~ sP5_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(X1,sK13_skl(X0)),skolemize(X1,sK14_skl(X0))],[f123]) ).
fof(f125,plain,
! [X0] :
( ~ bcapacityne(X0)
| ~ gt(X0,sK13_skl(X0))
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
! [X0] :
( ~ bcapacityne(X0)
| releaselg(sK13_skl(X0))
| ~ sP5_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f134,definition,
( sQ0_spl
<=> sP5_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f135,plain,
( ~ sQ0_spl
| sP5_prd(n0) ),
inference(component_clause,[status(thm)],[f134]) ).
fof(f137,definition,
( sQ1_spl
<=> bsecretioni(sK10_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f139,plain,
( sQ1_spl
| ~ bsecretioni(sK10_skl(n0)) ),
inference(component_clause,[status(thm)],[f137]) ).
fof(f140,definition,
! [X0] :
( sQ2_spl
<=> ( conditionnormo(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f141,plain,
! [X0] :
( ~ sQ2_spl
| conditionnormo(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f140]) ).
fof(f143,definition,
( sQ3_spl
<=> conditionhyper(sK5_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f144,plain,
( ~ sQ3_spl
| conditionhyper(sK5_skl(n0)) ),
inference(component_clause,[status(thm)],[f143]) ).
fof(f147,plain,
! [X0] :
( ~ sQ3_spl
| conditionnormo(X0)
| gt(n0,X0)
| sP3_prd(n0) ),
inference(resolution,[status(thm)],[f144,f67]) ).
fof(f149,definition,
( sQ4_spl
<=> sP3_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f150,plain,
( ~ sQ4_spl
| sP3_prd(n0) ),
inference(component_clause,[status(thm)],[f149]) ).
fof(f151,plain,
( sQ4_spl
| ~ sP3_prd(n0) ),
inference(component_clause,[status(thm)],[f149]) ).
fof(f152,plain,
( ~ sQ3_spl
| sQ2_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f147,f149,f140,f143]) ).
fof(f153,plain,
( ~ sQ2_spl
| gt(n0,sK7_skl) ),
inference(resolution,[status(thm)],[f141,f81]) ).
fof(f156,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f153,f80]) ).
fof(f157,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f156]) ).
fof(f158,plain,
( ~ sQ4_spl
| ~ bsecretioni(sK10_skl(n0))
| sP5_prd(n0) ),
inference(resolution,[status(thm)],[f150,f109]) ).
fof(f159,plain,
( ~ sQ4_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f158,f134,f137,f149]) ).
fof(f161,plain,
( ~ sQ0_spl
| ~ bcapacityne(n0)
| releaselg(sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f135,f126]) ).
fof(f166,definition,
( sQ6_spl
<=> bcapacityne(n0) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f168,plain,
( sQ6_spl
| ~ bcapacityne(n0) ),
inference(component_clause,[status(thm)],[f166]) ).
fof(f170,definition,
( sQ7_spl
<=> releaselg(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f171,plain,
( ~ sQ7_spl
| releaselg(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f170]) ).
fof(f173,plain,
( ~ sQ0_spl
| ~ sQ6_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f161,f170,f166,f134]) ).
fof(f174,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f168,f79]) ).
fof(f175,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f174]) ).
fof(f178,plain,
! [X0] :
( sQ1_spl
| gt(X0,sK10_skl(n0))
| bcapacityex(X0)
| ~ drugsu(sK1_skl(X0)) ),
inference(resolution,[status(thm)],[f139,f45]) ).
fof(f182,plain,
! [X0] :
( sQ1_spl
| gt(n0,sK1_skl(X0))
| gt(X0,sK10_skl(n0))
| bcapacityex(X0) ),
inference(resolution,[status(thm)],[f178,f77]) ).
fof(f187,plain,
! [X0] :
( ~ sQ7_spl
| gt(X0,sK13_skl(n0))
| ~ drugbg(sK2_skl(X0)) ),
inference(resolution,[status(thm)],[f171,f49]) ).
fof(f188,definition,
! [X0] :
( sQ8_spl
<=> gt(X0,sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f189,plain,
! [X0] :
( ~ sQ8_spl
| gt(X0,sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f188]) ).
fof(f199,plain,
( ~ sQ8_spl
| $false ),
inference(resolution,[status(thm)],[f189,f21]) ).
fof(f214,plain,
~ sQ8_spl,
inference(contradiction_clause,[status(thm)],[f199]) ).
fof(f237,plain,
! [X0] :
( sQ1_spl
| bsecretioni(X0)
| gt(n0,X0)
| bcapacityex(n0)
| gt(n0,sK10_skl(n0))
| bcapacityex(n0) ),
inference(resolution,[status(thm)],[f182,f44]) ).
fof(f240,definition,
( sQ16_spl
<=> bcapacityex(n0) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f241,plain,
( ~ sQ16_spl
| bcapacityex(n0) ),
inference(component_clause,[status(thm)],[f240]) ).
fof(f243,definition,
( sQ17_spl
<=> gt(n0,sK10_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f244,plain,
( ~ sQ17_spl
| gt(n0,sK10_skl(n0)) ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f246,definition,
! [X0] :
( sQ18_spl
<=> ( bsecretioni(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f247,plain,
! [X0] :
( ~ sQ18_spl
| bsecretioni(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f246]) ).
fof(f249,plain,
( sQ1_spl
| sQ18_spl
| sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f237,f240,f243,f246,f137]) ).
fof(f257,plain,
! [X0] :
( ~ sQ7_spl
| gt(n0,sK2_skl(X0))
| gt(X0,sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f187,f76]) ).
fof(f265,plain,
! [X0] :
( ~ sQ7_spl
| ~ releaselg(X0)
| gt(n0,X0)
| gt(n0,sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f257,f48]) ).
fof(f268,definition,
( sQ19_spl
<=> gt(n0,sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f269,plain,
( ~ sQ19_spl
| gt(n0,sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f268]) ).
fof(f271,definition,
! [X0] :
( sQ20_spl
<=> ( ~ releaselg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f272,plain,
! [X0] :
( ~ sQ20_spl
| ~ releaselg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f271]) ).
fof(f274,plain,
( ~ sQ7_spl
| sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f265,f268,f271,f170]) ).
fof(f276,plain,
( ~ sQ19_spl
| ~ bcapacityne(n0)
| ~ sP5_prd(n0) ),
inference(resolution,[status(thm)],[f269,f125]) ).
fof(f279,plain,
( ~ sQ19_spl
| ~ sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f276,f134,f166,f268]) ).
fof(f284,plain,
( ~ sQ7_spl
| ~ sQ20_spl
| gt(n0,sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f272,f171]) ).
fof(f285,plain,
( ~ sQ7_spl
| ~ sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f284,f268,f271,f170]) ).
fof(f286,plain,
( ~ sQ18_spl
| sQ1_spl
| gt(n0,sK10_skl(n0)) ),
inference(resolution,[status(thm)],[f139,f247]) ).
fof(f291,plain,
( ~ sQ18_spl
| sQ1_spl
| sP5_prd(n0)
| ~ sP3_prd(n0) ),
inference(resolution,[status(thm)],[f286,f108]) ).
fof(f294,plain,
( ~ sQ18_spl
| sQ1_spl
| sQ0_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f291,f149,f134,f137,f246]) ).
fof(f311,plain,
( ~ sQ16_spl
| ~ bcapacityne(n0) ),
inference(resolution,[status(thm)],[f241,f26]) ).
fof(f312,definition,
( sQ26_spl
<=> sP4_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f314,plain,
( sQ26_spl
| ~ sP4_prd(n0) ),
inference(component_clause,[status(thm)],[f312]) ).
fof(f329,plain,
( ~ sQ16_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f311,f166,f240]) ).
fof(f330,plain,
( sQ26_spl
| bcapacityex(n0) ),
inference(resolution,[status(thm)],[f314,f121]) ).
fof(f331,plain,
( sQ26_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f330,f240,f312]) ).
fof(f333,plain,
( ~ sQ17_spl
| sP5_prd(n0)
| ~ sP3_prd(n0) ),
inference(resolution,[status(thm)],[f244,f108]) ).
fof(f336,plain,
( ~ sQ17_spl
| sQ0_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f333,f149,f134,f243]) ).
fof(f339,plain,
! [X0] :
( sQ4_spl
| conditionnormo(X0)
| gt(n0,X0)
| gt(n0,sK5_skl(n0)) ),
inference(resolution,[status(thm)],[f151,f66]) ).
fof(f340,definition,
( sQ31_spl
<=> gt(n0,sK5_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f341,plain,
( ~ sQ31_spl
| gt(n0,sK5_skl(n0)) ),
inference(component_clause,[status(thm)],[f340]) ).
fof(f343,plain,
( sQ4_spl
| sQ2_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f339,f340,f140,f149]) ).
fof(f354,plain,
( ~ sQ31_spl
| conditionhyper(sK5_skl(n0)) ),
inference(resolution,[status(thm)],[f341,f78]) ).
fof(f357,plain,
( ~ sQ31_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f354,f143,f340]) ).
fof(f371,plain,
$false,
inference(sat_refutation,[status(thm)],[f152,f157,f159,f173,f175,f214,f249,f274,f279,f285,f294,f329,f331,f336,f343,f357]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED002+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 01:22:01 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.42 % Refutation found
% 0.09/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.44 % Elapsed time: 0.061648 seconds
% 0.09/0.44 % CPU time: 0.258194 seconds
% 0.09/0.44 % Total memory used: 20.622 MB
% 0.09/0.44 % Net memory used: 20.308 MB
%------------------------------------------------------------------------------