%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MED010+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 : n002.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 0.13s 0.76s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 48
% Syntax : Number of formulae : 237 ( 19 unt; 36 def)
% Number of atoms : 965 ( 0 equ)
% Maximal formula atoms : 30 ( 4 avg)
% Number of connectives : 1127 ( 399 ~; 448 |; 206 &)
% ( 42 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 55 ( 54 usr; 28 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-1 aty)
% Number of variables : 298 ( 268 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X0] :
( ~ bcapacityex(X0)
| ~ bcapacityne(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X0] :
( ~ bcapacitysn(X0)
| ~ bcapacityex(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X0] :
( ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X0] :
( ~ s2(X0)
| ~ s0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X0] :
( ~ s2(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(f29,axiom,
! [X0] :
( s2(X0)
=> ( drugsu(X0)
& drugbg(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(f40,axiom,
! [X0] :
( ( ~ ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
& s2(X0) )
=> ? [X1] :
( bcapacityex(X1)
& ! [X2] :
( gt(X1,X2)
=> conditionhyper(X2) )
& s3(X1)
& ~ gt(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,conjecture,
( ( bcapacityex(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& s2(n0) )
=> ? [X0] :
( bcapacityex(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& s3(X0)
& ~ gt(n0,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
~ ( ( bcapacityex(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& s2(n0) )
=> ? [X0] :
( bcapacityex(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& s3(X0)
& ~ gt(n0,X0) ) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f43,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f48,plain,
! [X0] :
( ~ bcapacityex(X0)
| ~ bcapacityne(X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f50,plain,
! [X0] :
( ~ bcapacitysn(X0)
| ~ bcapacityex(X0) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f78,plain,
! [X0] :
( ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f79,definition,
! [X0] :
( sP2_prd(X0)
<=> ( qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f98,plain,
! [X0] :
( ~ s2(X0)
| ~ s0(X0) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f100,plain,
! [X0] :
( ~ s2(X0)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
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(f116,plain,
! [X0] :
( ( drugsu(X0)
& drugbg(X0) )
| ~ s2(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f117,plain,
! [X0] :
( drugbg(X0)
| ~ s2(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
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(f160,plain,
! [X0] :
( ? [X1] :
( bcapacityex(X1)
& ! [X2] :
( conditionhyper(X2)
| ~ gt(X1,X2) )
& s3(X1)
& ~ gt(X0,X1) )
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ~ s2(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f161,plain,
! [X0] :
( ( bcapacityex(sK14_skl(X0))
& ! [X2] :
( conditionhyper(X2)
| ~ gt(sK14_skl(X0),X2) )
& s3(sK14_skl(X0))
& ~ gt(X0,sK14_skl(X0)) )
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ~ s2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X1,sK14_skl(X0))],[f160]) ).
fof(f162,plain,
! [X0,X1] :
( ~ gt(X0,sK14_skl(X0))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s2(X0) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f163,plain,
! [X0,X1] :
( s3(sK14_skl(X0))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s2(X0) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f164,plain,
! [X0,X1,X2] :
( conditionhyper(X2)
| ~ gt(sK14_skl(X0),X2)
| conditionnormo(X1)
| gt(X0,X1)
| ~ s2(X0) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f165,plain,
! [X0,X1] :
( bcapacityex(sK14_skl(X0))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s2(X0) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f166,plain,
( ! [X0] :
( ~ bcapacityex(X0)
| ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ s3(X0)
| gt(n0,X0) )
& bcapacityex(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& s2(n0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f167,plain,
( ! [X0] :
( ~ bcapacityex(X0)
| ( ~ conditionhyper(sK15_skl(X0))
& gt(X0,sK15_skl(X0)) )
| ~ s3(X0)
| gt(n0,X0) )
& bcapacityex(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& s2(n0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X1,sK15_skl(X0))],[f166]) ).
fof(f168,plain,
s2(n0),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f170,plain,
bcapacityex(n0),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f171,plain,
! [X0] :
( ~ bcapacityex(X0)
| gt(X0,sK15_skl(X0))
| ~ s3(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f172,plain,
! [X0] :
( ~ bcapacityex(X0)
| ~ conditionhyper(sK15_skl(X0))
| ~ s3(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f186,plain,
! [X0] :
( ( ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| sP2_prd(X0) )
& ( qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) )
| ~ sP2_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f79]) ).
fof(f187,plain,
( ! [X0] :
( ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| sP2_prd(X0) )
& ! [X0] :
( qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) )
| ~ sP2_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f186]) ).
fof(f188,plain,
( ! [X0] :
( ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| sP2_prd(X0) )
& ! [X0] :
( qilt27(X0)
| ~ bcapacitysn(X0)
| ( releaselg(sK17_skl(X0))
& ~ gt(X0,sK17_skl(X0)) )
| ~ sP2_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(X1,sK17_skl(X0))],[f187]) ).
fof(f192,plain,
! [X0] :
( bcapacitysn(X0)
| sP2_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f213,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(f214,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)],[f213]) ).
fof(f215,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f216,plain,
! [X0,X1] :
( ~ conditionnormo(X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f218,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(f219,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,f218]) ).
fof(f220,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(f221,plain,
! [X0] :
( sP6_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP10_prd(X0) )
| sP9_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f219,f220]) ).
fof(f222,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)],[f221]) ).
fof(f223,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)],[f222]) ).
fof(f224,plain,
( ! [X0] :
( ( ( ( ~ conditionhyper(sK21_skl(X0))
& gt(X0,sK21_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,[sK21_skl]),skolemize(X1,sK21_skl(X0))],[f223]) ).
fof(f225,plain,
! [X0] :
( sP10_prd(X0)
| sP9_prd(X0)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f227,plain,
! [X0] :
( ~ sP9_prd(X0)
| sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f228,plain,
! [X0] :
( gt(X0,sK21_skl(X0))
| ~ sP10_prd(X0)
| sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f229,plain,
! [X0] :
( ~ conditionhyper(sK21_skl(X0))
| ~ sP10_prd(X0)
| sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f244,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(f245,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)],[f218,f244]) ).
fof(f246,definition,
! [X0] :
( sP12_prd(X0)
<=> ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP12_prd])],[]) ).
fof(f247,plain,
! [X0] :
( sP9_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP12_prd(X0) )
| sP11_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f245,f246]) ).
fof(f248,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)],[f247]) ).
fof(f249,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)],[f248]) ).
fof(f250,plain,
( ! [X0] :
( ( ( ( ~ conditionhyper(sK24_skl(X0))
& gt(X0,sK24_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,[sK24_skl]),skolemize(X1,sK24_skl(X0))],[f249]) ).
fof(f251,plain,
! [X0] :
( sP12_prd(X0)
| sP11_prd(X0)
| ~ sP9_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f253,plain,
! [X0] :
( ~ sP11_prd(X0)
| sP9_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f256,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(f257,plain,
! [X0] :
( sP10_prd(X0)
<=> ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& sP13_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f220,f256]) ).
fof(f258,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)],[f257]) ).
fof(f259,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)],[f258]) ).
fof(f260,plain,
( ! [X0] :
( ( ~ bsecretioni(sK25_skl(X0))
& ~ gt(X0,sK25_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,[sK25_skl]),skolemize(X1,sK25_skl(X0))],[f259]) ).
fof(f261,plain,
! [X0] :
( sP13_prd(X0)
| ~ sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f265,definition,
! [X0] :
( sP14_prd(X0)
<=> ( qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP14_prd])],[]) ).
fof(f266,plain,
! [X0] :
( sP11_prd(X0)
<=> ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP14_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f244,f265]) ).
fof(f267,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)],[f266]) ).
fof(f268,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)],[f267]) ).
fof(f269,plain,
( ! [X0] :
( ( ~ conditionhyper(sK26_skl(X0))
& gt(X0,sK26_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,[sK26_skl]),skolemize(X1,sK26_skl(X0))],[f268]) ).
fof(f270,plain,
! [X0] :
( sP14_prd(X0)
| ~ sP11_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f274,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)],[f246]) ).
fof(f275,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)],[f274]) ).
fof(f276,plain,
( ! [X0] :
( qilt27(X0)
| ~ bcapacitysn(X0)
| ( releaselg(sK27_skl(X0))
& ~ gt(X0,sK27_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,[sK27_skl]),skolemize(X1,sK27_skl(X0))],[f275]) ).
fof(f278,plain,
! [X0] :
( bcapacitysn(X0)
| ~ sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f276]) ).
fof(f282,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)],[f256]) ).
fof(f283,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)],[f282]) ).
fof(f284,plain,
( ! [X0] :
( ~ bcapacityne(X0)
| ( ~ uptakepg(sK29_skl(X0))
& ~ gt(X0,sK29_skl(X0))
& releaselg(sK28_skl(X0))
& ~ gt(X0,sK28_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,[sK28_skl,sK29_skl]),skolemize(X1,sK28_skl(X0)),skolemize(X1,sK29_skl(X0))],[f283]) ).
fof(f286,plain,
! [X0] :
( bcapacityne(X0)
| ~ sP13_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f291,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)],[f265]) ).
fof(f292,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)],[f291]) ).
fof(f293,plain,
( ! [X0] :
( ~ qilt27(X0)
| ~ bcapacitysn(X0)
| ( ~ bsecretioni(sK30_skl(X0))
& ~ gt(X0,sK30_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,[sK30_skl]),skolemize(X1,sK30_skl(X0))],[f292]) ).
fof(f295,plain,
! [X0] :
( bcapacitysn(X0)
| ~ sP14_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f293]) ).
fof(f303,plain,
drugbg(n0),
inference(resolution,[status(thm)],[f117,f168]) ).
fof(f318,plain,
! [X0] :
( ~ sP10_prd(X0)
| bcapacityne(X0) ),
inference(resolution,[status(thm)],[f286,f261]) ).
fof(f321,plain,
! [X0] :
( ~ sP11_prd(X0)
| bcapacitysn(X0) ),
inference(resolution,[status(thm)],[f295,f270]) ).
fof(f324,plain,
! [X0] :
( bcapacitysn(X0)
| sP11_prd(X0)
| ~ sP9_prd(X0) ),
inference(resolution,[status(thm)],[f251,f278]) ).
fof(f325,plain,
! [X0] :
( bcapacitysn(X0)
| ~ sP9_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f324,f321]) ).
fof(f328,plain,
! [X0] :
( sP10_prd(X0)
| ~ sP6_prd(X0)
| bcapacitysn(X0) ),
inference(resolution,[status(thm)],[f325,f225]) ).
fof(f331,plain,
! [X0] :
( bcapacityne(X0)
| ~ sP6_prd(X0)
| bcapacitysn(X0) ),
inference(resolution,[status(thm)],[f328,f318]) ).
fof(f333,plain,
! [X0] :
( ~ bcapacityex(X0)
| ~ sP6_prd(X0)
| bcapacitysn(X0) ),
inference(resolution,[status(thm)],[f331,f48]) ).
fof(f334,plain,
! [X0] :
( ~ bcapacityex(X0)
| ~ sP6_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f333,f50]) ).
fof(f338,plain,
~ sP6_prd(n0),
inference(resolution,[status(thm)],[f334,f170]) ).
fof(f340,plain,
( gt(n0,sK21_skl(n0))
| ~ sP10_prd(n0) ),
inference(resolution,[status(thm)],[f338,f228]) ).
fof(f341,plain,
~ sP9_prd(n0),
inference(resolution,[status(thm)],[f338,f227]) ).
fof(f343,plain,
! [X0] :
( uptakepg(X0)
| gt(n0,X0)
| sP5_prd(sK7_skl(n0),n0) ),
inference(resolution,[status(thm)],[f338,f109]) ).
fof(f345,definition,
( sQ0_spl
<=> sP10_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f348,definition,
( sQ1_spl
<=> gt(n0,sK21_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f349,plain,
( ~ sQ1_spl
| gt(n0,sK21_skl(n0)) ),
inference(component_clause,[status(thm)],[f348]) ).
fof(f351,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f340,f345,f348]) ).
fof(f352,definition,
( sQ2_spl
<=> sP5_prd(sK7_skl(n0),n0) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f353,plain,
( ~ sQ2_spl
| sP5_prd(sK7_skl(n0),n0) ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f355,definition,
( sQ3_spl
<=> bcapacityex(n0) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f357,plain,
( sQ3_spl
| ~ bcapacityex(n0) ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f359,definition,
! [X0] :
( sQ4_spl
<=> ( uptakepg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f360,plain,
! [X0] :
( ~ sQ4_spl
| uptakepg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f359]) ).
fof(f362,plain,
( sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f343,f352,f359]) ).
fof(f368,plain,
~ sP11_prd(n0),
inference(resolution,[status(thm)],[f341,f253]) ).
fof(f369,definition,
( sQ6_spl
<=> sP6_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f370,plain,
( ~ sQ6_spl
| sP6_prd(n0) ),
inference(component_clause,[status(thm)],[f369]) ).
fof(f373,plain,
( ~ sQ2_spl
| ~ conditionnormo(sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f353,f216]) ).
fof(f374,plain,
( ~ sQ2_spl
| ~ gt(n0,sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f353,f215]) ).
fof(f375,plain,
( ~ sQ1_spl
| conditionhyper(sK21_skl(n0)) ),
inference(resolution,[status(thm)],[f349,f169]) ).
fof(f383,plain,
! [X0] :
( ~ sQ2_spl
| s3(sK14_skl(X0))
| gt(X0,sK7_skl(n0))
| ~ s2(X0) ),
inference(resolution,[status(thm)],[f373,f163]) ).
fof(f384,plain,
( ~ sQ1_spl
| ~ sP10_prd(n0)
| sP6_prd(n0) ),
inference(resolution,[status(thm)],[f375,f229]) ).
fof(f388,plain,
( ~ sQ1_spl
| ~ sQ0_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f384,f369,f345,f348]) ).
fof(f389,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f370,f338]) ).
fof(f390,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f389]) ).
fof(f392,definition,
( sQ7_spl
<=> bcapacitysn(n0) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( ~ sQ7_spl
| bcapacitysn(n0) ),
inference(component_clause,[status(thm)],[f392]) ).
fof(f397,plain,
( ~ sQ2_spl
| s3(sK14_skl(n0))
| gt(n0,sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f383,f168]) ).
fof(f398,definition,
( sQ8_spl
<=> gt(n0,sK7_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( ~ sQ8_spl
| gt(n0,sK7_skl(n0)) ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f401,definition,
( sQ9_spl
<=> s3(sK14_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f402,plain,
( ~ sQ9_spl
| s3(sK14_skl(n0)) ),
inference(component_clause,[status(thm)],[f401]) ).
fof(f404,plain,
( ~ sQ2_spl
| sQ9_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f397,f398,f401,f352]) ).
fof(f405,plain,
( ~ sQ8_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f374]) ).
fof(f406,plain,
( ~ sQ8_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f405]) ).
fof(f409,plain,
! [X0,X1] :
( ~ sQ4_spl
| drugi(X1)
| gt(X0,X1)
| gt(n0,sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f360,f135]) ).
fof(f417,plain,
! [X0,X1] :
( ~ sQ4_spl
| s3(X1)
| gt(X0,X1)
| gt(n0,sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f409,f129]) ).
fof(f423,plain,
! [X0,X1] :
( ~ sQ4_spl
| drugi(X1)
| gt(n0,X1)
| s3(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f417,f134]) ).
fof(f427,definition,
! [X0] :
( sQ10_spl
<=> ( s3(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f428,plain,
! [X0] :
( ~ sQ10_spl
| s3(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f427]) ).
fof(f430,definition,
! [X1] :
( sQ11_spl
<=> ( drugi(X1)
| gt(n0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f431,plain,
! [X0] :
( ~ sQ11_spl
| drugi(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f433,plain,
( ~ sQ4_spl
| sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f423,f427,f430,f359]) ).
fof(f437,definition,
( sQ13_spl
<=> sP9_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f442,plain,
! [X0] :
( ~ sQ11_spl
| s3(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f431,f129]) ).
fof(f443,plain,
! [X0] :
( ~ sQ11_spl
| ~ bcapacityex(X0)
| ~ conditionhyper(sK15_skl(X0))
| gt(n0,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f172,f442]) ).
fof(f444,plain,
! [X0] :
( ~ sQ11_spl
| ~ bcapacityex(X0)
| gt(X0,sK15_skl(X0))
| gt(n0,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f171,f442]) ).
fof(f447,plain,
( ~ sQ11_spl
| gt(n0,sK15_skl(n0))
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f444,f170]) ).
fof(f449,definition,
( sQ14_spl
<=> gt(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f450,plain,
( ~ sQ14_spl
| gt(n0,n0) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,definition,
( sQ15_spl
<=> gt(n0,sK15_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f453,plain,
( ~ sQ15_spl
| gt(n0,sK15_skl(n0)) ),
inference(component_clause,[status(thm)],[f452]) ).
fof(f455,plain,
( ~ sQ11_spl
| sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f447,f449,f452,f430]) ).
fof(f456,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f450,f43]) ).
fof(f457,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f456]) ).
fof(f458,plain,
! [X0] :
( ~ sQ10_spl
| ~ bcapacityex(X0)
| ~ conditionhyper(sK15_skl(X0))
| gt(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f172,f428]) ).
fof(f459,plain,
! [X0] :
( ~ sQ10_spl
| ~ bcapacityex(X0)
| gt(X0,sK15_skl(X0))
| gt(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f171,f428]) ).
fof(f462,plain,
( ~ sQ10_spl
| gt(n0,sK15_skl(n0))
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f459,f170]) ).
fof(f464,plain,
( ~ sQ10_spl
| sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f462,f449,f452,f427]) ).
fof(f468,plain,
( ~ sQ7_spl
| ~ bcapacityex(n0) ),
inference(resolution,[status(thm)],[f393,f50]) ).
fof(f469,definition,
( sQ16_spl
<=> sP12_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( ~ sQ16_spl
| sP12_prd(n0) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f471,plain,
( sQ16_spl
| ~ sP12_prd(n0) ),
inference(component_clause,[status(thm)],[f469]) ).
fof(f479,definition,
( sQ19_spl
<=> sP2_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( sQ19_spl
| ~ sP2_prd(n0) ),
inference(component_clause,[status(thm)],[f479]) ).
fof(f486,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f170]) ).
fof(f487,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f486]) ).
fof(f490,definition,
( sQ21_spl
<=> drugbg(n0) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f492,plain,
( sQ21_spl
| ~ drugbg(n0) ),
inference(component_clause,[status(thm)],[f490]) ).
fof(f493,definition,
( sQ22_spl
<=> s2(n0) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f495,plain,
( sQ22_spl
| ~ s2(n0) ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f500,definition,
( sQ24_spl
<=> s1(n0) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f501,plain,
( ~ sQ24_spl
| s1(n0) ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f507,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f492,f303]) ).
fof(f508,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f507]) ).
fof(f511,plain,
( sQ19_spl
| bcapacitysn(n0) ),
inference(resolution,[status(thm)],[f481,f192]) ).
fof(f513,plain,
( sQ19_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f511,f392,f479]) ).
fof(f517,definition,
! [X0] :
( sQ27_spl
<=> ( conditionnormo(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f518,plain,
! [X0] :
( ~ sQ27_spl
| conditionnormo(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f517]) ).
fof(f526,plain,
( ~ sQ16_spl
| bcapacitysn(n0) ),
inference(resolution,[status(thm)],[f470,f278]) ).
fof(f531,plain,
( ~ sQ16_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f526,f392,f469]) ).
fof(f537,definition,
( sQ29_spl
<=> s0(n0) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f538,plain,
( ~ sQ29_spl
| s0(n0) ),
inference(component_clause,[status(thm)],[f537]) ).
fof(f541,plain,
( ~ sQ15_spl
| conditionhyper(sK15_skl(n0)) ),
inference(resolution,[status(thm)],[f453,f169]) ).
fof(f561,plain,
( sQ16_spl
| sP11_prd(n0)
| ~ sP9_prd(n0) ),
inference(resolution,[status(thm)],[f471,f251]) ).
fof(f562,definition,
( sQ32_spl
<=> sP11_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f563,plain,
( ~ sQ32_spl
| sP11_prd(n0) ),
inference(component_clause,[status(thm)],[f562]) ).
fof(f565,plain,
( sQ16_spl
| sQ32_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f561,f437,f562,f469]) ).
fof(f566,plain,
( ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f563,f368]) ).
fof(f567,plain,
~ sQ32_spl,
inference(contradiction_clause,[status(thm)],[f566]) ).
fof(f571,plain,
( ~ sQ29_spl
| ~ s2(n0) ),
inference(resolution,[status(thm)],[f538,f98]) ).
fof(f581,plain,
( ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f571,f168]) ).
fof(f582,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f581]) ).
fof(f590,plain,
( ~ sQ24_spl
| ~ s2(n0) ),
inference(resolution,[status(thm)],[f501,f100]) ).
fof(f591,plain,
( ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f590,f168]) ).
fof(f592,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f591]) ).
fof(f595,definition,
! [X0] :
( sQ35_spl
<=> gt(X0,sK15_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f596,plain,
! [X0] :
( ~ sQ35_spl
| gt(X0,sK15_skl(n0)) ),
inference(component_clause,[status(thm)],[f595]) ).
fof(f612,plain,
( ~ sQ35_spl
| $false ),
inference(resolution,[status(thm)],[f596,f43]) ).
fof(f633,plain,
~ sQ35_spl,
inference(contradiction_clause,[status(thm)],[f612]) ).
fof(f743,plain,
( ~ sQ15_spl
| ~ sQ11_spl
| ~ bcapacityex(n0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f443,f541]) ).
fof(f744,plain,
( ~ sQ15_spl
| ~ sQ11_spl
| ~ sQ3_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f743,f449,f355,f430,f452]) ).
fof(f745,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f357,f170]) ).
fof(f746,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f745]) ).
fof(f747,plain,
( ~ sQ15_spl
| ~ sQ10_spl
| ~ bcapacityex(n0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f458,f541]) ).
fof(f748,plain,
( ~ sQ15_spl
| ~ sQ10_spl
| ~ sQ3_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f747,f449,f355,f427,f452]) ).
fof(f768,plain,
( ~ sQ9_spl
| ~ bcapacityex(sK14_skl(n0))
| ~ conditionhyper(sK15_skl(sK14_skl(n0)))
| gt(n0,sK14_skl(n0)) ),
inference(resolution,[status(thm)],[f402,f172]) ).
fof(f769,plain,
( ~ sQ9_spl
| ~ bcapacityex(sK14_skl(n0))
| gt(sK14_skl(n0),sK15_skl(sK14_skl(n0)))
| gt(n0,sK14_skl(n0)) ),
inference(resolution,[status(thm)],[f402,f171]) ).
fof(f774,definition,
( sQ47_spl
<=> gt(n0,sK14_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f775,plain,
( ~ sQ47_spl
| gt(n0,sK14_skl(n0)) ),
inference(component_clause,[status(thm)],[f774]) ).
fof(f777,definition,
( sQ48_spl
<=> conditionhyper(sK15_skl(sK14_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f780,definition,
( sQ49_spl
<=> bcapacityex(sK14_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f782,plain,
( sQ49_spl
| ~ bcapacityex(sK14_skl(n0)) ),
inference(component_clause,[status(thm)],[f780]) ).
fof(f783,plain,
( ~ sQ9_spl
| ~ sQ49_spl
| ~ sQ48_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f768,f774,f777,f780,f401]) ).
fof(f784,definition,
( sQ50_spl
<=> gt(sK14_skl(n0),sK15_skl(sK14_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f785,plain,
( ~ sQ50_spl
| gt(sK14_skl(n0),sK15_skl(sK14_skl(n0))) ),
inference(component_clause,[status(thm)],[f784]) ).
fof(f787,plain,
( ~ sQ9_spl
| ~ sQ49_spl
| sQ50_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f769,f774,f784,f780,f401]) ).
fof(f832,plain,
! [X0] :
( sQ49_spl
| conditionnormo(X0)
| gt(n0,X0)
| ~ s2(n0) ),
inference(resolution,[status(thm)],[f782,f165]) ).
fof(f834,plain,
( sQ49_spl
| sQ27_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f832,f493,f517,f780]) ).
fof(f842,plain,
( ~ sQ2_spl
| ~ sQ27_spl
| gt(n0,sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f518,f373]) ).
fof(f845,plain,
( ~ sQ2_spl
| ~ sQ27_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f842,f398,f517,f352]) ).
fof(f855,plain,
! [X0] :
( ~ sQ47_spl
| conditionnormo(X0)
| gt(n0,X0)
| ~ s2(n0) ),
inference(resolution,[status(thm)],[f775,f162]) ).
fof(f859,plain,
( ~ sQ47_spl
| sQ27_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f855,f493,f517,f774]) ).
fof(f868,plain,
! [X0] :
( ~ sQ50_spl
| conditionhyper(sK15_skl(sK14_skl(n0)))
| conditionnormo(X0)
| gt(n0,X0)
| ~ s2(n0) ),
inference(resolution,[status(thm)],[f785,f164]) ).
fof(f872,plain,
( ~ sQ50_spl
| sQ48_spl
| sQ27_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f868,f493,f517,f777,f784]) ).
fof(f896,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f495,f168]) ).
fof(f897,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f896]) ).
fof(f898,plain,
$false,
inference(sat_refutation,[status(thm)],[f351,f362,f388,f390,f404,f406,f433,f455,f457,f464,f487,f508,f513,f531,f565,f567,f582,f592,f633,f744,f746,f748,f783,f787,f834,f845,f859,f872,f897]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MED010+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.53 % Computer : n002.cluster.edu
% 0.09/0.53 % Model : x86_64 x86_64
% 0.09/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.53 % Memory : 8046.5625MB
% 0.09/0.53 % OS : Linux 6.8.0-71-generic
% 0.09/0.53 % CPULimit : 300
% 0.09/0.53 % WCLimit : 300
% 0.09/0.53 % DateTime : Mon Sep 21 01:22:34 UTC 2026
% 0.09/0.53 % CPUTime :
% 0.09/0.54 % Drodi V4.1.1
% 0.13/0.76 % Refutation found
% 0.13/0.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.80 % Elapsed time: 0.256220 seconds
% 0.13/0.80 % CPU time: 1.779893 seconds
% 0.13/0.80 % Total memory used: 34.230 MB
% 0.13/0.80 % Net memory used: 31.992 MB
%------------------------------------------------------------------------------