%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MED005+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 : n011.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 94.12s 12.32s
% Output : CNFRefutation 94.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 98
% Syntax : Number of formulae : 433 ( 62 unt; 85 def)
% Number of atoms : 1272 ( 0 equ)
% Maximal formula atoms : 30 ( 2 avg)
% Number of connectives : 1338 ( 499 ~; 543 |; 172 &)
% ( 91 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 105 ( 104 usr; 77 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 1 con; 0-1 aty)
% Number of variables : 409 ( 387 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X0,X1] :
( ~ gt(X0,X1)
=> ( uptakelg(X1)
=> ~ releaselg(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X0] :
( ~ s1(X0)
| ~ s0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X0] :
( ~ s2(X0)
| ~ s0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X0] :
( ~ s3(X0)
| ~ s0(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(f32,axiom,
! [X0] :
( drugsu(X0)
=> ( s3(X0)
| s2(X0)
| ( qillt27(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(f36,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
=> ( ~ bcapacityex(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> drugsu(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(f38,axiom,
! [X0] :
( ( ~ ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
& s0(X0) )
=> ? [X1] :
( ! [X2] :
( gt(X1,X2)
=> conditionhyper(X2) )
& s1(X1)
& ~ gt(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,conjecture,
( ( ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& s0(n0) )
=> ? [X0] :
( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& s1(X0)
& ~ gt(n0,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
~ ( ( ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& s0(n0) )
=> ? [X0] :
( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& s1(X0)
& ~ gt(n0,X0) ) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f43,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f61,plain,
! [X0,X1] :
( ~ releaselg(X1)
| ~ uptakelg(X1)
| gt(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f62,plain,
! [X1] :
( ~ releaselg(X1)
| ~ uptakelg(X1)
| ! [X0] : gt(X0,X1) ),
inference(miniscoping,[status(thm)],[f61]) ).
fof(f63,plain,
! [X0,X1] :
( ~ releaselg(X1)
| ~ uptakelg(X1)
| gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f97,plain,
! [X0] :
( ~ s1(X0)
| ~ s0(X0) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f98,plain,
! [X0] :
( ~ s2(X0)
| ~ s0(X0) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f99,plain,
! [X0] :
( ~ s3(X0)
| ~ s0(X0) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
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(f122,plain,
! [X0] :
( s3(X0)
| s2(X0)
| ( ~ qilt27(X0)
& s1(X0) )
| ~ drugbg(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f123,plain,
! [X0] :
( s3(X0)
| s2(X0)
| s1(X0)
| ~ drugbg(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f125,plain,
! [X0] :
( s3(X0)
| s2(X0)
| ( qillt27(X0)
& s1(X0) )
| ~ drugsu(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f126,plain,
! [X0] :
( s3(X0)
| s2(X0)
| s1(X0)
| ~ drugsu(X0) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
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(f139,plain,
! [X0] :
( ( ~ bcapacityex(X0)
& ! [X1] :
( drugsu(X1)
| gt(X0,X1) ) )
| ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f140,definition,
! [X0,X1] :
( sP7_prd(X1,X0)
<=> ( ~ bsecretioni(X1)
& ~ gt(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP7_prd])],[]) ).
fof(f141,plain,
! [X0] :
( ( ~ bcapacityex(X0)
& ! [X1] :
( drugsu(X1)
| gt(X0,X1) ) )
| ? [X1] : sP7_prd(X1,X0) ),
inference(formula_renaming,[status(thm)],[f139,f140]) ).
fof(f142,plain,
! [X0] :
( ( ~ bcapacityex(X0)
& ! [X1] :
( drugsu(X1)
| gt(X0,X1) ) )
| sP7_prd(sK10_skl(X0),X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X1,sK10_skl(X0))],[f141]) ).
fof(f143,plain,
! [X0,X1] :
( drugsu(X1)
| gt(X0,X1)
| sP7_prd(sK10_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
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(f149,plain,
! [X0] :
( ? [X1] :
( ! [X2] :
( conditionhyper(X2)
| ~ gt(X1,X2) )
& s1(X1)
& ~ gt(X0,X1) )
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ~ s0(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f150,plain,
! [X0] :
( ( ! [X2] :
( conditionhyper(X2)
| ~ gt(sK12_skl(X0),X2) )
& s1(sK12_skl(X0))
& ~ gt(X0,sK12_skl(X0)) )
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ~ s0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(X1,sK12_skl(X0))],[f149]) ).
fof(f151,plain,
! [X0,X1] :
( ~ gt(X0,sK12_skl(X0))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s0(X0) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f152,plain,
! [X0,X1] :
( s1(sK12_skl(X0))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s0(X0) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f153,plain,
! [X0,X1,X2] :
( conditionhyper(X2)
| ~ gt(sK12_skl(X0),X2)
| conditionnormo(X1)
| gt(X0,X1)
| ~ s0(X0) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f166,plain,
( ! [X0] :
( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ s1(X0)
| gt(n0,X0) )
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& s0(n0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f167,plain,
( ! [X0] :
( ( ~ conditionhyper(sK15_skl(X0))
& gt(X0,sK15_skl(X0)) )
| ~ s1(X0)
| gt(n0,X0) )
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& s0(n0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X1,sK15_skl(X0))],[f166]) ).
fof(f168,plain,
s0(n0),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f170,plain,
! [X0] :
( gt(X0,sK15_skl(X0))
| ~ s1(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f171,plain,
! [X0] :
( ~ conditionhyper(sK15_skl(X0))
| ~ s1(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
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(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))],[f222]) ).
fof(f224,plain,
! [X0] :
( sP10_prd(X0)
| sP9_prd(X0)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f229,plain,
! [X0,X1] :
( ( bsecretioni(X1)
| gt(X0,X1)
| sP7_prd(X1,X0) )
& ( ( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| ~ sP7_prd(X1,X0) ) ),
inference(NNF_transformation,[status(thm)],[f140]) ).
fof(f230,plain,
( ! [X0,X1] :
( bsecretioni(X1)
| gt(X0,X1)
| sP7_prd(X1,X0) )
& ! [X0,X1] :
( ( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| ~ sP7_prd(X1,X0) ) ),
inference(miniscoping,[status(thm)],[f229]) ).
fof(f231,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| ~ sP7_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f232,plain,
! [X0,X1] :
( ~ bsecretioni(X0)
| ~ sP7_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f230]) ).
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(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))],[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(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))],[f258]) ).
fof(f261,plain,
! [X0,X1] :
( bsecretioni(X1)
| gt(X0,X1)
| ~ 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(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))],[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(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))],[f274]) ).
fof(f276,plain,
! [X0,X1] :
( ~ releaselg(X1)
| gt(X0,X1)
| ~ sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f275]) ).
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(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))],[f291]) ).
fof(f293,plain,
! [X0,X1] :
( bsecretioni(X1)
| gt(X0,X1)
| ~ sP14_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f307,plain,
! [X0,X1] :
( s3(X1)
| s2(X1)
| s1(X1)
| gt(X0,X1)
| releaselg(sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f148,f123]) ).
fof(f353,plain,
! [X0] :
( s1(sK12_skl(n0))
| conditionnormo(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f152,f168]) ).
fof(f355,definition,
! [X0] :
( sQ0_spl
<=> ( conditionnormo(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f356,plain,
! [X0] :
( ~ sQ0_spl
| conditionnormo(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f358,definition,
( sQ1_spl
<=> s1(sK12_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f359,plain,
( ~ sQ1_spl
| s1(sK12_skl(n0)) ),
inference(component_clause,[status(thm)],[f358]) ).
fof(f361,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f353,f355,f358]) ).
fof(f427,plain,
( ~ sQ1_spl
| gt(sK12_skl(n0),sK15_skl(sK12_skl(n0)))
| gt(n0,sK12_skl(n0)) ),
inference(resolution,[status(thm)],[f359,f170]) ).
fof(f428,plain,
( ~ sQ1_spl
| ~ conditionhyper(sK15_skl(sK12_skl(n0)))
| gt(n0,sK12_skl(n0)) ),
inference(resolution,[status(thm)],[f359,f171]) ).
fof(f451,definition,
( sQ9_spl
<=> gt(n0,sK12_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f452,plain,
( ~ sQ9_spl
| gt(n0,sK12_skl(n0)) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,definition,
( sQ10_spl
<=> gt(sK12_skl(n0),sK15_skl(sK12_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( ~ sQ1_spl
| sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f427,f451,f454,f358]) ).
fof(f458,definition,
( sQ11_spl
<=> conditionhyper(sK15_skl(sK12_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( sQ11_spl
| ~ conditionhyper(sK15_skl(sK12_skl(n0))) ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,plain,
( ~ sQ1_spl
| ~ sQ11_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f428,f451,f458,f358]) ).
fof(f565,plain,
! [X0] :
( ~ sQ9_spl
| conditionnormo(X0)
| gt(n0,X0)
| ~ s0(n0) ),
inference(resolution,[status(thm)],[f452,f151]) ).
fof(f567,definition,
( sQ23_spl
<=> s0(n0) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f569,plain,
( sQ23_spl
| ~ s0(n0) ),
inference(component_clause,[status(thm)],[f567]) ).
fof(f570,plain,
( ~ sQ9_spl
| sQ0_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f565,f567,f355,f451]) ).
fof(f579,plain,
! [X0,X1] :
( ~ bsecretioni(sK10_skl(X0))
| drugsu(X1)
| gt(X0,X1) ),
inference(resolution,[status(thm)],[f143,f232]) ).
fof(f607,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f569,f168]) ).
fof(f608,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f607]) ).
fof(f638,plain,
! [X0,X1] :
( sQ11_spl
| ~ gt(sK12_skl(X0),sK15_skl(sK12_skl(n0)))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s0(X0) ),
inference(resolution,[status(thm)],[f460,f153]) ).
fof(f874,plain,
! [X0,X1] :
( uptakelg(X1)
| gt(X0,X1)
| sP6_prd(X0)
| ~ gt(X0,sK7_skl(X0)) ),
inference(resolution,[status(thm)],[f214,f108]) ).
fof(f875,plain,
! [X0,X1] :
( ~ sQ0_spl
| gt(n0,X0)
| ~ sP5_prd(X0,X1) ),
inference(resolution,[status(thm)],[f215,f356]) ).
fof(f881,plain,
! [X0,X1] :
( ~ sQ0_spl
| uptakelg(X1)
| gt(X0,X1)
| sP6_prd(X0)
| gt(n0,sK7_skl(X0)) ),
inference(resolution,[status(thm)],[f875,f108]) ).
fof(f1069,plain,
! [X0,X1] :
( drugsu(X1)
| gt(X0,X1)
| ~ gt(X0,sK10_skl(X0)) ),
inference(resolution,[status(thm)],[f231,f143]) ).
fof(f1284,plain,
! [X0,X1] :
( ~ s0(X1)
| s2(X1)
| s1(X1)
| gt(X0,X1)
| releaselg(sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f307,f99]) ).
fof(f1285,plain,
! [X0,X1] :
( ~ s0(X1)
| s2(X1)
| gt(X0,X1)
| releaselg(sK11_skl(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1284,f97]) ).
fof(f1376,definition,
( sQ127_spl
<=> sP12_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1377,plain,
( ~ sQ127_spl
| sP12_prd(n0) ),
inference(component_clause,[status(thm)],[f1376]) ).
fof(f1420,definition,
( sQ136_spl
<=> sP9_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1421,plain,
( ~ sQ136_spl
| sP9_prd(n0) ),
inference(component_clause,[status(thm)],[f1420]) ).
fof(f1439,definition,
( sQ139_spl
<=> sP14_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1441,plain,
( sQ139_spl
| ~ sP14_prd(n0) ),
inference(component_clause,[status(thm)],[f1439]) ).
fof(f1464,plain,
( ~ sQ136_spl
| sP12_prd(n0)
| sP11_prd(n0) ),
inference(resolution,[status(thm)],[f1421,f250]) ).
fof(f1466,definition,
( sQ145_spl
<=> sP11_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1469,plain,
( ~ sQ136_spl
| sQ127_spl
| sQ145_spl ),
inference(split_clause,[status(thm)],[f1464,f1466,f1376,f1420]) ).
fof(f1516,plain,
! [X0,X1] :
( s3(X1)
| s2(X1)
| s1(X1)
| ~ bsecretioni(sK10_skl(X0))
| gt(X0,X1) ),
inference(resolution,[status(thm)],[f579,f126]) ).
fof(f1565,plain,
! [X0,X1] :
( ~ s0(X1)
| gt(X0,X1)
| releaselg(sK11_skl(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1285,f98]) ).
fof(f1566,plain,
! [X0] :
( gt(X0,n0)
| releaselg(sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f1565,f168]) ).
fof(f1607,definition,
( sQ160_spl
<=> sP6_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1609,plain,
( sQ160_spl
| ~ sP6_prd(n0) ),
inference(component_clause,[status(thm)],[f1607]) ).
fof(f1758,definition,
! [X0] :
( sQ164_spl
<=> ( uptakelg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f1759,plain,
! [X0] :
( ~ sQ164_spl
| uptakelg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f1758]) ).
fof(f1781,plain,
! [X0] :
( ~ sQ0_spl
| sQ160_spl
| uptakelg(X0)
| gt(n0,X0)
| gt(n0,sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f1609,f881]) ).
fof(f1786,definition,
( sQ165_spl
<=> gt(n0,sK7_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f1787,plain,
( ~ sQ165_spl
| gt(n0,sK7_skl(n0)) ),
inference(component_clause,[status(thm)],[f1786]) ).
fof(f1789,plain,
( ~ sQ0_spl
| sQ160_spl
| sQ164_spl
| sQ165_spl ),
inference(split_clause,[status(thm)],[f1781,f1786,f1758,f1607,f355]) ).
fof(f1792,definition,
( sQ166_spl
<=> sP10_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f1793,plain,
( ~ sQ166_spl
| sP10_prd(n0) ),
inference(component_clause,[status(thm)],[f1792]) ).
fof(f1794,plain,
( sQ166_spl
| ~ sP10_prd(n0) ),
inference(component_clause,[status(thm)],[f1792]) ).
fof(f2439,plain,
! [X0,X1] :
( ~ s0(X1)
| s2(X1)
| s1(X1)
| ~ bsecretioni(sK10_skl(X0))
| gt(X0,X1) ),
inference(resolution,[status(thm)],[f1516,f99]) ).
fof(f2440,plain,
! [X0,X1] :
( ~ s0(X1)
| s2(X1)
| ~ bsecretioni(sK10_skl(X0))
| gt(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2439,f97]) ).
fof(f2465,plain,
releaselg(sK11_skl(n0)),
inference(resolution,[status(thm)],[f1566,f43]) ).
fof(f2498,plain,
! [X0] :
( gt(X0,sK11_skl(n0))
| ~ sP12_prd(X0) ),
inference(resolution,[status(thm)],[f2465,f276]) ).
fof(f2501,plain,
! [X0] :
( ~ uptakelg(sK11_skl(n0))
| gt(X0,sK11_skl(n0)) ),
inference(resolution,[status(thm)],[f2465,f63]) ).
fof(f2502,definition,
! [X0] :
( sQ253_spl
<=> gt(X0,sK11_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f2503,plain,
! [X0] :
( ~ sQ253_spl
| gt(X0,sK11_skl(n0)) ),
inference(component_clause,[status(thm)],[f2502]) ).
fof(f2505,definition,
( sQ254_spl
<=> uptakelg(sK11_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f2507,plain,
( sQ254_spl
| ~ uptakelg(sK11_skl(n0)) ),
inference(component_clause,[status(thm)],[f2505]) ).
fof(f2508,plain,
( ~ sQ254_spl
| sQ253_spl ),
inference(split_clause,[status(thm)],[f2501,f2502,f2505]) ).
fof(f2793,plain,
( sQ139_spl
| ~ sP11_prd(n0) ),
inference(resolution,[status(thm)],[f1441,f269]) ).
fof(f3044,plain,
( sQ166_spl
| sP9_prd(n0)
| ~ sP6_prd(n0) ),
inference(resolution,[status(thm)],[f1794,f224]) ).
fof(f3046,plain,
( sQ166_spl
| sQ136_spl
| ~ sQ160_spl ),
inference(split_clause,[status(thm)],[f3044,f1607,f1420,f1792]) ).
fof(f3388,plain,
! [X0,X1] :
( ~ s0(X1)
| ~ bsecretioni(sK10_skl(X0))
| gt(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2440,f98]) ).
fof(f3389,plain,
! [X0] :
( ~ bsecretioni(sK10_skl(X0))
| gt(X0,n0) ),
inference(resolution,[status(thm)],[f3388,f168]) ).
fof(f3644,plain,
( ~ sQ253_spl
| $false ),
inference(resolution,[status(thm)],[f2503,f43]) ).
fof(f3665,plain,
~ sQ253_spl,
inference(contradiction_clause,[status(thm)],[f3644]) ).
fof(f3917,plain,
! [X0] :
( ~ sQ165_spl
| uptakelg(X0)
| gt(n0,X0)
| sP6_prd(n0) ),
inference(resolution,[status(thm)],[f1787,f874]) ).
fof(f3922,plain,
( ~ sQ165_spl
| sQ164_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f3917,f1607,f1758,f1786]) ).
fof(f4017,definition,
! [X0] :
( sQ462_spl
<=> gt(X0,sK15_skl(sK12_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ462_spl])],[split_symbol_definition]) ).
fof(f4018,plain,
! [X0] :
( ~ sQ462_spl
| gt(X0,sK15_skl(sK12_skl(n0))) ),
inference(component_clause,[status(thm)],[f4017]) ).
fof(f4106,definition,
! [X0] :
( sQ466_spl
<=> gt(X0,sK22_skl(sK17_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ466_spl])],[split_symbol_definition]) ).
fof(f4107,plain,
! [X0] :
( ~ sQ466_spl
| gt(X0,sK22_skl(sK17_skl(n0))) ),
inference(component_clause,[status(thm)],[f4106]) ).
fof(f4180,definition,
! [X0] :
( sQ477_spl
<=> gt(X0,sK28_skl(sK17_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ477_spl])],[split_symbol_definition]) ).
fof(f4181,plain,
! [X0] :
( ~ sQ477_spl
| gt(X0,sK28_skl(sK17_skl(n0))) ),
inference(component_clause,[status(thm)],[f4180]) ).
fof(f4194,definition,
! [X0] :
( sQ479_spl
<=> gt(X0,sK11_skl(sK5_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ479_spl])],[split_symbol_definition]) ).
fof(f4195,plain,
! [X0] :
( ~ sQ479_spl
| gt(X0,sK11_skl(sK5_skl(n0))) ),
inference(component_clause,[status(thm)],[f4194]) ).
fof(f4220,definition,
! [X0] :
( sQ481_spl
<=> gt(X0,sK22_skl(sK5_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ481_spl])],[split_symbol_definition]) ).
fof(f4221,plain,
! [X0] :
( ~ sQ481_spl
| gt(X0,sK22_skl(sK5_skl(n0))) ),
inference(component_clause,[status(thm)],[f4220]) ).
fof(f4326,definition,
! [X0] :
( sQ498_spl
<=> gt(X0,sK28_skl(sK5_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ498_spl])],[split_symbol_definition]) ).
fof(f4327,plain,
! [X0] :
( ~ sQ498_spl
| gt(X0,sK28_skl(sK5_skl(n0))) ),
inference(component_clause,[status(thm)],[f4326]) ).
fof(f4375,definition,
! [X0] :
( sQ506_spl
<=> gt(X0,sK22_skl(sK27_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ506_spl])],[split_symbol_definition]) ).
fof(f4376,plain,
! [X0] :
( ~ sQ506_spl
| gt(X0,sK22_skl(sK27_skl(n0))) ),
inference(component_clause,[status(thm)],[f4375]) ).
fof(f4487,definition,
! [X0] :
( sQ526_spl
<=> gt(X0,sK28_skl(sK27_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ526_spl])],[split_symbol_definition]) ).
fof(f4488,plain,
! [X0] :
( ~ sQ526_spl
| gt(X0,sK28_skl(sK27_skl(n0))) ),
inference(component_clause,[status(thm)],[f4487]) ).
fof(f4528,definition,
! [X0] :
( sQ533_spl
<=> gt(X0,sK22_skl(sK28_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ533_spl])],[split_symbol_definition]) ).
fof(f4529,plain,
! [X0] :
( ~ sQ533_spl
| gt(X0,sK22_skl(sK28_skl(n0))) ),
inference(component_clause,[status(thm)],[f4528]) ).
fof(f4609,definition,
! [X0] :
( sQ543_spl
<=> gt(X0,sK28_skl(sK28_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ543_spl])],[split_symbol_definition]) ).
fof(f4610,plain,
! [X0] :
( ~ sQ543_spl
| gt(X0,sK28_skl(sK28_skl(n0))) ),
inference(component_clause,[status(thm)],[f4609]) ).
fof(f4651,definition,
! [X0] :
( sQ550_spl
<=> gt(X0,sK22_skl(sK22_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ550_spl])],[split_symbol_definition]) ).
fof(f4652,plain,
! [X0] :
( ~ sQ550_spl
| gt(X0,sK22_skl(sK22_skl(n0))) ),
inference(component_clause,[status(thm)],[f4651]) ).
fof(f4717,definition,
! [X0] :
( sQ560_spl
<=> gt(X0,sK28_skl(sK22_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ560_spl])],[split_symbol_definition]) ).
fof(f4718,plain,
! [X0] :
( ~ sQ560_spl
| gt(X0,sK28_skl(sK22_skl(n0))) ),
inference(component_clause,[status(thm)],[f4717]) ).
fof(f4765,definition,
! [X0] :
( sQ567_spl
<=> gt(X0,sK22_skl(sK11_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ567_spl])],[split_symbol_definition]) ).
fof(f4766,plain,
! [X0] :
( ~ sQ567_spl
| gt(X0,sK22_skl(sK11_skl(n0))) ),
inference(component_clause,[status(thm)],[f4765]) ).
fof(f4831,definition,
! [X0] :
( sQ577_spl
<=> gt(X0,sK28_skl(sK11_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ577_spl])],[split_symbol_definition]) ).
fof(f4832,plain,
! [X0] :
( ~ sQ577_spl
| gt(X0,sK28_skl(sK11_skl(n0))) ),
inference(component_clause,[status(thm)],[f4831]) ).
fof(f5088,definition,
! [X0] :
( sQ593_spl
<=> gt(X0,sK8_skl(sK5_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ593_spl])],[split_symbol_definition]) ).
fof(f5089,plain,
! [X0] :
( ~ sQ593_spl
| gt(X0,sK8_skl(sK5_skl(n0))) ),
inference(component_clause,[status(thm)],[f5088]) ).
fof(f5095,definition,
! [X0] :
( sQ595_spl
<=> gt(X0,sK8_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ595_spl])],[split_symbol_definition]) ).
fof(f5096,plain,
! [X0] :
( ~ sQ595_spl
| gt(X0,sK8_skl(n0)) ),
inference(component_clause,[status(thm)],[f5095]) ).
fof(f5129,plain,
( ~ sQ595_spl
| $false ),
inference(resolution,[status(thm)],[f5096,f43]) ).
fof(f5150,plain,
~ sQ595_spl,
inference(contradiction_clause,[status(thm)],[f5129]) ).
fof(f5637,plain,
~ bsecretioni(sK10_skl(n0)),
inference(resolution,[status(thm)],[f3389,f43]) ).
fof(f5648,plain,
! [X0] :
( gt(X0,sK10_skl(n0))
| ~ sP14_prd(X0) ),
inference(resolution,[status(thm)],[f5637,f293]) ).
fof(f5649,plain,
! [X0] :
( gt(X0,sK10_skl(n0))
| ~ sP10_prd(X0) ),
inference(resolution,[status(thm)],[f5637,f261]) ).
fof(f5872,definition,
! [X0] :
( sQ654_spl
<=> ( drugsu(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ654_spl])],[split_symbol_definition]) ).
fof(f5873,plain,
! [X0] :
( ~ sQ654_spl
| drugsu(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f5872]) ).
fof(f5915,definition,
! [X0] :
( sQ665_spl
<=> ( drugbg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ665_spl])],[split_symbol_definition]) ).
fof(f5916,plain,
! [X0] :
( ~ sQ665_spl
| drugbg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f5915]) ).
fof(f5922,definition,
! [X0] :
( sQ667_spl
<=> ( drugi(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ667_spl])],[split_symbol_definition]) ).
fof(f5923,plain,
! [X0] :
( ~ sQ667_spl
| drugi(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f5922]) ).
fof(f5992,definition,
! [X0] :
( sQ680_spl
<=> gt(X0,sK19_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ680_spl])],[split_symbol_definition]) ).
fof(f5993,plain,
! [X0] :
( ~ sQ680_spl
| gt(X0,sK19_skl(n0)) ),
inference(component_clause,[status(thm)],[f5992]) ).
fof(f6087,plain,
( ~ sQ680_spl
| $false ),
inference(resolution,[status(thm)],[f5993,f43]) ).
fof(f6109,plain,
~ sQ680_spl,
inference(contradiction_clause,[status(thm)],[f6087]) ).
fof(f6240,plain,
( sQ254_spl
| ~ sQ164_spl
| gt(n0,sK11_skl(n0)) ),
inference(resolution,[status(thm)],[f1759,f2507]) ).
fof(f6549,definition,
! [X0] :
( sQ733_spl
<=> gt(X0,sK22_skl(sK8_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ733_spl])],[split_symbol_definition]) ).
fof(f6550,plain,
! [X0] :
( ~ sQ733_spl
| gt(X0,sK22_skl(sK8_skl(n0))) ),
inference(component_clause,[status(thm)],[f6549]) ).
fof(f6635,definition,
! [X0] :
( sQ744_spl
<=> gt(X0,sK28_skl(sK8_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ744_spl])],[split_symbol_definition]) ).
fof(f6636,plain,
! [X0] :
( ~ sQ744_spl
| gt(X0,sK28_skl(sK8_skl(n0))) ),
inference(component_clause,[status(thm)],[f6635]) ).
fof(f6810,plain,
! [X0] :
( ~ sQ667_spl
| s3(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f5923,f129]) ).
fof(f7091,definition,
! [X0] :
( sQ793_spl
<=> gt(X0,sK22_skl(sK19_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ793_spl])],[split_symbol_definition]) ).
fof(f7092,plain,
! [X0] :
( ~ sQ793_spl
| gt(X0,sK22_skl(sK19_skl(n0))) ),
inference(component_clause,[status(thm)],[f7091]) ).
fof(f7194,definition,
! [X0] :
( sQ803_spl
<=> gt(X0,sK28_skl(sK19_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ803_spl])],[split_symbol_definition]) ).
fof(f7195,plain,
! [X0] :
( ~ sQ803_spl
| gt(X0,sK28_skl(sK19_skl(n0))) ),
inference(component_clause,[status(thm)],[f7194]) ).
fof(f7358,plain,
! [X0] :
( ~ sQ667_spl
| ~ s0(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f6810,f99]) ).
fof(f7884,plain,
( ~ sQ667_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f7358,f168]) ).
fof(f7886,plain,
( ~ sQ667_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7884,f43]) ).
fof(f7887,plain,
~ sQ667_spl,
inference(contradiction_clause,[status(thm)],[f7886]) ).
fof(f8025,plain,
( ~ sQ466_spl
| $false ),
inference(resolution,[status(thm)],[f4107,f43]) ).
fof(f8047,plain,
~ sQ466_spl,
inference(contradiction_clause,[status(thm)],[f8025]) ).
fof(f8142,plain,
( ~ sQ477_spl
| $false ),
inference(resolution,[status(thm)],[f4181,f43]) ).
fof(f8164,plain,
~ sQ477_spl,
inference(contradiction_clause,[status(thm)],[f8142]) ).
fof(f8183,plain,
( ~ sQ479_spl
| $false ),
inference(resolution,[status(thm)],[f4195,f43]) ).
fof(f8204,plain,
~ sQ479_spl,
inference(contradiction_clause,[status(thm)],[f8183]) ).
fof(f8228,plain,
( ~ sQ481_spl
| $false ),
inference(resolution,[status(thm)],[f4221,f43]) ).
fof(f8250,plain,
~ sQ481_spl,
inference(contradiction_clause,[status(thm)],[f8228]) ).
fof(f8416,plain,
( ~ sQ498_spl
| $false ),
inference(resolution,[status(thm)],[f4327,f43]) ).
fof(f8438,plain,
~ sQ498_spl,
inference(contradiction_clause,[status(thm)],[f8416]) ).
fof(f8457,plain,
( ~ sQ506_spl
| $false ),
inference(resolution,[status(thm)],[f4376,f43]) ).
fof(f8479,plain,
~ sQ506_spl,
inference(contradiction_clause,[status(thm)],[f8457]) ).
fof(f8585,plain,
( ~ sQ526_spl
| $false ),
inference(resolution,[status(thm)],[f4488,f43]) ).
fof(f8607,plain,
~ sQ526_spl,
inference(contradiction_clause,[status(thm)],[f8585]) ).
fof(f8626,plain,
( ~ sQ533_spl
| $false ),
inference(resolution,[status(thm)],[f4529,f43]) ).
fof(f8648,plain,
~ sQ533_spl,
inference(contradiction_clause,[status(thm)],[f8626]) ).
fof(f9087,plain,
( ~ sQ543_spl
| $false ),
inference(resolution,[status(thm)],[f4610,f43]) ).
fof(f9109,plain,
~ sQ543_spl,
inference(contradiction_clause,[status(thm)],[f9087]) ).
fof(f9133,plain,
( ~ sQ550_spl
| $false ),
inference(resolution,[status(thm)],[f4652,f43]) ).
fof(f9155,plain,
~ sQ550_spl,
inference(contradiction_clause,[status(thm)],[f9133]) ).
fof(f9250,plain,
( ~ sQ560_spl
| $false ),
inference(resolution,[status(thm)],[f4718,f43]) ).
fof(f9272,plain,
~ sQ560_spl,
inference(contradiction_clause,[status(thm)],[f9250]) ).
fof(f9291,plain,
( ~ sQ567_spl
| $false ),
inference(resolution,[status(thm)],[f4766,f43]) ).
fof(f9313,plain,
~ sQ567_spl,
inference(contradiction_clause,[status(thm)],[f9291]) ).
fof(f9354,plain,
( ~ sQ577_spl
| $false ),
inference(resolution,[status(thm)],[f4832,f43]) ).
fof(f9376,plain,
~ sQ577_spl,
inference(contradiction_clause,[status(thm)],[f9354]) ).
fof(f9395,plain,
( ~ sQ593_spl
| $false ),
inference(resolution,[status(thm)],[f5089,f43]) ).
fof(f9416,plain,
~ sQ593_spl,
inference(contradiction_clause,[status(thm)],[f9395]) ).
fof(f9435,plain,
( ~ sQ733_spl
| $false ),
inference(resolution,[status(thm)],[f6550,f43]) ).
fof(f9457,plain,
~ sQ733_spl,
inference(contradiction_clause,[status(thm)],[f9435]) ).
fof(f9612,plain,
( ~ sQ744_spl
| $false ),
inference(resolution,[status(thm)],[f6636,f43]) ).
fof(f9634,plain,
~ sQ744_spl,
inference(contradiction_clause,[status(thm)],[f9612]) ).
fof(f9652,plain,
( ~ sQ462_spl
| $false ),
inference(resolution,[status(thm)],[f4018,f43]) ).
fof(f9673,plain,
~ sQ462_spl,
inference(contradiction_clause,[status(thm)],[f9652]) ).
fof(f9692,plain,
( ~ sQ793_spl
| $false ),
inference(resolution,[status(thm)],[f7092,f43]) ).
fof(f9714,plain,
~ sQ793_spl,
inference(contradiction_clause,[status(thm)],[f9692]) ).
fof(f9793,plain,
( ~ sQ803_spl
| $false ),
inference(resolution,[status(thm)],[f7195,f43]) ).
fof(f9815,plain,
~ sQ803_spl,
inference(contradiction_clause,[status(thm)],[f9793]) ).
fof(f9982,definition,
! [X0] :
( sQ1133_spl
<=> gt(X0,sK17_skl(sK19_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1133_spl])],[split_symbol_definition]) ).
fof(f9983,plain,
! [X0] :
( ~ sQ1133_spl
| gt(X0,sK17_skl(sK19_skl(n0))) ),
inference(component_clause,[status(thm)],[f9982]) ).
fof(f10003,definition,
( sQ1135_spl
<=> gt(n0,sK11_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ1135_spl])],[split_symbol_definition]) ).
fof(f10004,plain,
( ~ sQ1135_spl
| gt(n0,sK11_skl(n0)) ),
inference(component_clause,[status(thm)],[f10003]) ).
fof(f10379,definition,
! [X0] :
( sQ1154_spl
<=> gt(X0,sK27_skl(sK19_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1154_spl])],[split_symbol_definition]) ).
fof(f10380,plain,
! [X0] :
( ~ sQ1154_spl
| gt(X0,sK27_skl(sK19_skl(n0))) ),
inference(component_clause,[status(thm)],[f10379]) ).
fof(f10393,definition,
! [X0] :
( sQ1156_spl
<=> gt(X0,sK17_skl(sK8_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1156_spl])],[split_symbol_definition]) ).
fof(f10394,plain,
! [X0] :
( ~ sQ1156_spl
| gt(X0,sK17_skl(sK8_skl(n0))) ),
inference(component_clause,[status(thm)],[f10393]) ).
fof(f10407,definition,
! [X0] :
( sQ1158_spl
<=> gt(X0,sK27_skl(sK8_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1158_spl])],[split_symbol_definition]) ).
fof(f10408,plain,
! [X0] :
( ~ sQ1158_spl
| gt(X0,sK27_skl(sK8_skl(n0))) ),
inference(component_clause,[status(thm)],[f10407]) ).
fof(f10421,definition,
! [X0] :
( sQ1160_spl
<=> gt(X0,sK17_skl(sK11_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1160_spl])],[split_symbol_definition]) ).
fof(f10422,plain,
! [X0] :
( ~ sQ1160_spl
| gt(X0,sK17_skl(sK11_skl(n0))) ),
inference(component_clause,[status(thm)],[f10421]) ).
fof(f10435,definition,
! [X0] :
( sQ1162_spl
<=> gt(X0,sK27_skl(sK11_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1162_spl])],[split_symbol_definition]) ).
fof(f10436,plain,
! [X0] :
( ~ sQ1162_spl
| gt(X0,sK27_skl(sK11_skl(n0))) ),
inference(component_clause,[status(thm)],[f10435]) ).
fof(f10466,definition,
! [X0] :
( sQ1164_spl
<=> gt(X0,sK17_skl(sK22_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1164_spl])],[split_symbol_definition]) ).
fof(f10467,plain,
! [X0] :
( ~ sQ1164_spl
| gt(X0,sK17_skl(sK22_skl(n0))) ),
inference(component_clause,[status(thm)],[f10466]) ).
fof(f10484,definition,
! [X0] :
( sQ1166_spl
<=> gt(X0,sK27_skl(sK22_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1166_spl])],[split_symbol_definition]) ).
fof(f10485,plain,
! [X0] :
( ~ sQ1166_spl
| gt(X0,sK27_skl(sK22_skl(n0))) ),
inference(component_clause,[status(thm)],[f10484]) ).
fof(f10498,definition,
! [X0] :
( sQ1168_spl
<=> gt(X0,sK17_skl(sK28_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1168_spl])],[split_symbol_definition]) ).
fof(f10499,plain,
! [X0] :
( ~ sQ1168_spl
| gt(X0,sK17_skl(sK28_skl(n0))) ),
inference(component_clause,[status(thm)],[f10498]) ).
fof(f10527,definition,
! [X0] :
( sQ1171_spl
<=> gt(X0,sK27_skl(sK28_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1171_spl])],[split_symbol_definition]) ).
fof(f10528,plain,
! [X0] :
( ~ sQ1171_spl
| gt(X0,sK27_skl(sK28_skl(n0))) ),
inference(component_clause,[status(thm)],[f10527]) ).
fof(f10541,definition,
! [X0] :
( sQ1173_spl
<=> gt(X0,sK17_skl(sK27_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1173_spl])],[split_symbol_definition]) ).
fof(f10542,plain,
! [X0] :
( ~ sQ1173_spl
| gt(X0,sK17_skl(sK27_skl(n0))) ),
inference(component_clause,[status(thm)],[f10541]) ).
fof(f10555,definition,
! [X0] :
( sQ1175_spl
<=> gt(X0,sK27_skl(sK27_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1175_spl])],[split_symbol_definition]) ).
fof(f10556,plain,
! [X0] :
( ~ sQ1175_spl
| gt(X0,sK27_skl(sK27_skl(n0))) ),
inference(component_clause,[status(thm)],[f10555]) ).
fof(f10569,definition,
! [X0] :
( sQ1177_spl
<=> gt(X0,sK17_skl(sK5_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1177_spl])],[split_symbol_definition]) ).
fof(f10570,plain,
! [X0] :
( ~ sQ1177_spl
| gt(X0,sK17_skl(sK5_skl(n0))) ),
inference(component_clause,[status(thm)],[f10569]) ).
fof(f10583,definition,
! [X0] :
( sQ1179_spl
<=> gt(X0,sK27_skl(sK5_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1179_spl])],[split_symbol_definition]) ).
fof(f10584,plain,
! [X0] :
( ~ sQ1179_spl
| gt(X0,sK27_skl(sK5_skl(n0))) ),
inference(component_clause,[status(thm)],[f10583]) ).
fof(f10608,definition,
! [X0] :
( sQ1182_spl
<=> gt(X0,sK17_skl(sK17_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1182_spl])],[split_symbol_definition]) ).
fof(f10609,plain,
! [X0] :
( ~ sQ1182_spl
| gt(X0,sK17_skl(sK17_skl(n0))) ),
inference(component_clause,[status(thm)],[f10608]) ).
fof(f10623,definition,
! [X0] :
( sQ1184_spl
<=> gt(X0,sK27_skl(sK17_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1184_spl])],[split_symbol_definition]) ).
fof(f10624,plain,
! [X0] :
( ~ sQ1184_spl
| gt(X0,sK27_skl(sK17_skl(n0))) ),
inference(component_clause,[status(thm)],[f10623]) ).
fof(f10659,plain,
( ~ sQ1133_spl
| $false ),
inference(resolution,[status(thm)],[f9983,f43]) ).
fof(f10680,plain,
~ sQ1133_spl,
inference(contradiction_clause,[status(thm)],[f10659]) ).
fof(f10698,plain,
( ~ sQ1154_spl
| $false ),
inference(resolution,[status(thm)],[f10380,f43]) ).
fof(f10719,plain,
~ sQ1154_spl,
inference(contradiction_clause,[status(thm)],[f10698]) ).
fof(f10737,plain,
( ~ sQ1156_spl
| $false ),
inference(resolution,[status(thm)],[f10394,f43]) ).
fof(f10758,plain,
~ sQ1156_spl,
inference(contradiction_clause,[status(thm)],[f10737]) ).
fof(f10776,plain,
( ~ sQ1158_spl
| $false ),
inference(resolution,[status(thm)],[f10408,f43]) ).
fof(f10797,plain,
~ sQ1158_spl,
inference(contradiction_clause,[status(thm)],[f10776]) ).
fof(f10815,plain,
( ~ sQ1160_spl
| $false ),
inference(resolution,[status(thm)],[f10422,f43]) ).
fof(f10836,plain,
~ sQ1160_spl,
inference(contradiction_clause,[status(thm)],[f10815]) ).
fof(f10854,plain,
( ~ sQ1162_spl
| $false ),
inference(resolution,[status(thm)],[f10436,f43]) ).
fof(f10875,plain,
~ sQ1162_spl,
inference(contradiction_clause,[status(thm)],[f10854]) ).
fof(f10893,plain,
( ~ sQ1164_spl
| $false ),
inference(resolution,[status(thm)],[f10467,f43]) ).
fof(f10914,plain,
~ sQ1164_spl,
inference(contradiction_clause,[status(thm)],[f10893]) ).
fof(f10939,plain,
( ~ sQ1166_spl
| $false ),
inference(resolution,[status(thm)],[f10485,f43]) ).
fof(f10960,plain,
~ sQ1166_spl,
inference(contradiction_clause,[status(thm)],[f10939]) ).
fof(f10978,plain,
( ~ sQ1168_spl
| $false ),
inference(resolution,[status(thm)],[f10499,f43]) ).
fof(f10999,plain,
~ sQ1168_spl,
inference(contradiction_clause,[status(thm)],[f10978]) ).
fof(f11017,plain,
( ~ sQ1171_spl
| $false ),
inference(resolution,[status(thm)],[f10528,f43]) ).
fof(f11038,plain,
~ sQ1171_spl,
inference(contradiction_clause,[status(thm)],[f11017]) ).
fof(f11056,plain,
( ~ sQ1173_spl
| $false ),
inference(resolution,[status(thm)],[f10542,f43]) ).
fof(f11077,plain,
~ sQ1173_spl,
inference(contradiction_clause,[status(thm)],[f11056]) ).
fof(f11095,plain,
( ~ sQ1175_spl
| $false ),
inference(resolution,[status(thm)],[f10556,f43]) ).
fof(f11116,plain,
~ sQ1175_spl,
inference(contradiction_clause,[status(thm)],[f11095]) ).
fof(f11134,plain,
( ~ sQ1177_spl
| $false ),
inference(resolution,[status(thm)],[f10570,f43]) ).
fof(f11155,plain,
~ sQ1177_spl,
inference(contradiction_clause,[status(thm)],[f11134]) ).
fof(f11173,plain,
( ~ sQ1179_spl
| $false ),
inference(resolution,[status(thm)],[f10584,f43]) ).
fof(f11194,plain,
~ sQ1179_spl,
inference(contradiction_clause,[status(thm)],[f11173]) ).
fof(f11213,plain,
( ~ sQ1182_spl
| $false ),
inference(resolution,[status(thm)],[f10609,f43]) ).
fof(f11234,plain,
~ sQ1182_spl,
inference(contradiction_clause,[status(thm)],[f11213]) ).
fof(f11252,plain,
( ~ sQ1184_spl
| $false ),
inference(resolution,[status(thm)],[f10624,f43]) ).
fof(f11273,plain,
~ sQ1184_spl,
inference(contradiction_clause,[status(thm)],[f11252]) ).
fof(f12071,plain,
! [X0] :
( drugsu(X0)
| gt(n0,X0)
| ~ sP14_prd(n0) ),
inference(resolution,[status(thm)],[f5648,f1069]) ).
fof(f12073,plain,
~ sP14_prd(sK10_skl(n0)),
inference(resolution,[status(thm)],[f5648,f43]) ).
fof(f12100,plain,
( sQ654_spl
| ~ sQ139_spl ),
inference(split_clause,[status(thm)],[f12071,f1439,f5872]) ).
fof(f12101,plain,
~ sP11_prd(sK10_skl(n0)),
inference(resolution,[status(thm)],[f12073,f269]) ).
fof(f12156,definition,
( sQ1428_spl
<=> sP14_prd(sK10_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ1428_spl])],[split_symbol_definition]) ).
fof(f12157,plain,
( ~ sQ1428_spl
| sP14_prd(sK10_skl(n0)) ),
inference(component_clause,[status(thm)],[f12156]) ).
fof(f12195,plain,
( ~ sQ1428_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12157,f12073]) ).
fof(f12196,plain,
~ sQ1428_spl,
inference(contradiction_clause,[status(thm)],[f12195]) ).
fof(f12281,definition,
( sQ1452_spl
<=> sP11_prd(sK10_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ1452_spl])],[split_symbol_definition]) ).
fof(f12282,plain,
( ~ sQ1452_spl
| sP11_prd(sK10_skl(n0)) ),
inference(component_clause,[status(thm)],[f12281]) ).
fof(f12285,plain,
( ~ sQ1452_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12282,f12101]) ).
fof(f12286,plain,
~ sQ1452_spl,
inference(contradiction_clause,[status(thm)],[f12285]) ).
fof(f12448,definition,
! [X0] :
( sQ1468_spl
<=> gt(X0,sK22_skl(sK10_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1468_spl])],[split_symbol_definition]) ).
fof(f12449,plain,
! [X0] :
( ~ sQ1468_spl
| gt(X0,sK22_skl(sK10_skl(n0))) ),
inference(component_clause,[status(thm)],[f12448]) ).
fof(f12512,definition,
! [X0] :
( sQ1476_spl
<=> gt(X0,sK17_skl(sK10_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1476_spl])],[split_symbol_definition]) ).
fof(f12513,plain,
! [X0] :
( ~ sQ1476_spl
| gt(X0,sK17_skl(sK10_skl(n0))) ),
inference(component_clause,[status(thm)],[f12512]) ).
fof(f12540,definition,
! [X0] :
( sQ1478_spl
<=> gt(X0,sK27_skl(sK10_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1478_spl])],[split_symbol_definition]) ).
fof(f12541,plain,
! [X0] :
( ~ sQ1478_spl
| gt(X0,sK27_skl(sK10_skl(n0))) ),
inference(component_clause,[status(thm)],[f12540]) ).
fof(f12567,definition,
! [X0] :
( sQ1482_spl
<=> gt(X0,sK28_skl(sK10_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1482_spl])],[split_symbol_definition]) ).
fof(f12568,plain,
! [X0] :
( ~ sQ1482_spl
| gt(X0,sK28_skl(sK10_skl(n0))) ),
inference(component_clause,[status(thm)],[f12567]) ).
fof(f12860,plain,
( ~ sQ1468_spl
| $false ),
inference(resolution,[status(thm)],[f12449,f43]) ).
fof(f12882,plain,
~ sQ1468_spl,
inference(contradiction_clause,[status(thm)],[f12860]) ).
fof(f12902,plain,
( ~ sQ1476_spl
| $false ),
inference(resolution,[status(thm)],[f12513,f43]) ).
fof(f12923,plain,
~ sQ1476_spl,
inference(contradiction_clause,[status(thm)],[f12902]) ).
fof(f12943,plain,
( ~ sQ1478_spl
| $false ),
inference(resolution,[status(thm)],[f12541,f43]) ).
fof(f12964,plain,
~ sQ1478_spl,
inference(contradiction_clause,[status(thm)],[f12943]) ).
fof(f12992,plain,
( ~ sQ1482_spl
| $false ),
inference(resolution,[status(thm)],[f12568,f43]) ).
fof(f13014,plain,
~ sQ1482_spl,
inference(contradiction_clause,[status(thm)],[f12992]) ).
fof(f13031,plain,
( ~ sQ166_spl
| gt(n0,sK10_skl(n0)) ),
inference(resolution,[status(thm)],[f5649,f1793]) ).
fof(f13094,plain,
( sQ254_spl
| ~ sQ164_spl
| sQ1135_spl ),
inference(split_clause,[status(thm)],[f6240,f10003,f1758,f2505]) ).
fof(f13602,plain,
! [X0] :
( ~ sQ166_spl
| drugsu(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f13031,f1069]) ).
fof(f13837,definition,
! [X3] :
( sQ1560_spl
<=> gt(X3,sK8_skl(sK12_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1560_spl])],[split_symbol_definition]) ).
fof(f13838,plain,
! [X0] :
( ~ sQ1560_spl
| gt(X0,sK8_skl(sK12_skl(n0))) ),
inference(component_clause,[status(thm)],[f13837]) ).
fof(f14083,plain,
! [X0] :
( sQ11_spl
| ~ gt(sK12_skl(n0),sK15_skl(sK12_skl(n0)))
| conditionnormo(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f638,f168]) ).
fof(f14085,plain,
( sQ11_spl
| ~ sQ10_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f14083,f355,f454,f458]) ).
fof(f14524,definition,
! [X0] :
( sQ1633_spl
<=> gt(X0,sK11_skl(sK12_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1633_spl])],[split_symbol_definition]) ).
fof(f14525,plain,
! [X0] :
( ~ sQ1633_spl
| gt(X0,sK11_skl(sK12_skl(n0))) ),
inference(component_clause,[status(thm)],[f14524]) ).
fof(f14694,definition,
! [X0] :
( sQ1648_spl
<=> gt(X0,sK17_skl(sK0_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1648_spl])],[split_symbol_definition]) ).
fof(f14695,plain,
! [X0] :
( ~ sQ1648_spl
| gt(X0,sK17_skl(sK0_skl(n0))) ),
inference(component_clause,[status(thm)],[f14694]) ).
fof(f14708,definition,
! [X0] :
( sQ1650_spl
<=> gt(X0,sK27_skl(sK0_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1650_spl])],[split_symbol_definition]) ).
fof(f14709,plain,
! [X0] :
( ~ sQ1650_spl
| gt(X0,sK27_skl(sK0_skl(n0))) ),
inference(component_clause,[status(thm)],[f14708]) ).
fof(f14761,definition,
! [X0] :
( sQ1658_spl
<=> gt(X0,sK28_skl(sK0_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1658_spl])],[split_symbol_definition]) ).
fof(f14762,plain,
! [X0] :
( ~ sQ1658_spl
| gt(X0,sK28_skl(sK0_skl(n0))) ),
inference(component_clause,[status(thm)],[f14761]) ).
fof(f14775,definition,
! [X0] :
( sQ1660_spl
<=> gt(X0,sK22_skl(sK0_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1660_spl])],[split_symbol_definition]) ).
fof(f14776,plain,
! [X0] :
( ~ sQ1660_spl
| gt(X0,sK22_skl(sK0_skl(n0))) ),
inference(component_clause,[status(thm)],[f14775]) ).
fof(f14802,definition,
! [X0] :
( sQ1664_spl
<=> gt(X0,sK11_skl(sK0_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1664_spl])],[split_symbol_definition]) ).
fof(f14803,plain,
! [X0] :
( ~ sQ1664_spl
| gt(X0,sK11_skl(sK0_skl(n0))) ),
inference(component_clause,[status(thm)],[f14802]) ).
fof(f15159,plain,
( ~ sQ1560_spl
| $false ),
inference(resolution,[status(thm)],[f13838,f43]) ).
fof(f15180,plain,
~ sQ1560_spl,
inference(contradiction_clause,[status(thm)],[f15159]) ).
fof(f15201,plain,
( ~ sQ1633_spl
| $false ),
inference(resolution,[status(thm)],[f14525,f43]) ).
fof(f15222,plain,
~ sQ1633_spl,
inference(contradiction_clause,[status(thm)],[f15201]) ).
fof(f15242,plain,
( ~ sQ1648_spl
| $false ),
inference(resolution,[status(thm)],[f14695,f43]) ).
fof(f15263,plain,
~ sQ1648_spl,
inference(contradiction_clause,[status(thm)],[f15242]) ).
fof(f15283,plain,
( ~ sQ1650_spl
| $false ),
inference(resolution,[status(thm)],[f14709,f43]) ).
fof(f15304,plain,
~ sQ1650_spl,
inference(contradiction_clause,[status(thm)],[f15283]) ).
fof(f15325,plain,
( ~ sQ1658_spl
| $false ),
inference(resolution,[status(thm)],[f14762,f43]) ).
fof(f15347,plain,
~ sQ1658_spl,
inference(contradiction_clause,[status(thm)],[f15325]) ).
fof(f15368,plain,
( ~ sQ1660_spl
| $false ),
inference(resolution,[status(thm)],[f14776,f43]) ).
fof(f15390,plain,
~ sQ1660_spl,
inference(contradiction_clause,[status(thm)],[f15368]) ).
fof(f15483,plain,
( ~ sQ1664_spl
| $false ),
inference(resolution,[status(thm)],[f14803,f43]) ).
fof(f15504,plain,
~ sQ1664_spl,
inference(contradiction_clause,[status(thm)],[f15483]) ).
fof(f16232,plain,
! [X0] :
( ~ sQ1135_spl
| drugbg(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f10004,f147]) ).
fof(f16355,definition,
! [X2] :
( sQ1817_spl
<=> gt(X2,sK8_skl(sK0_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ1817_spl])],[split_symbol_definition]) ).
fof(f16356,plain,
! [X0] :
( ~ sQ1817_spl
| gt(X0,sK8_skl(sK0_skl(n0))) ),
inference(component_clause,[status(thm)],[f16355]) ).
fof(f16504,plain,
( ~ sQ1817_spl
| $false ),
inference(resolution,[status(thm)],[f16356,f43]) ).
fof(f16525,plain,
~ sQ1817_spl,
inference(contradiction_clause,[status(thm)],[f16504]) ).
fof(f17808,definition,
( sQ1943_spl
<=> s1(n0) ),
introduced(definition,[new_symbols(definition,[sQ1943_spl])],[split_symbol_definition]) ).
fof(f17809,plain,
( ~ sQ1943_spl
| s1(n0) ),
inference(component_clause,[status(thm)],[f17808]) ).
fof(f17811,definition,
( sQ1944_spl
<=> s2(n0) ),
introduced(definition,[new_symbols(definition,[sQ1944_spl])],[split_symbol_definition]) ).
fof(f17812,plain,
( ~ sQ1944_spl
| s2(n0) ),
inference(component_clause,[status(thm)],[f17811]) ).
fof(f17814,definition,
( sQ1945_spl
<=> s3(n0) ),
introduced(definition,[new_symbols(definition,[sQ1945_spl])],[split_symbol_definition]) ).
fof(f17815,plain,
( ~ sQ1945_spl
| s3(n0) ),
inference(component_clause,[status(thm)],[f17814]) ).
fof(f17835,plain,
( ~ sQ1945_spl
| ~ s0(n0) ),
inference(resolution,[status(thm)],[f17815,f99]) ).
fof(f17836,plain,
( ~ sQ1945_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f17835,f567,f17814]) ).
fof(f17846,plain,
( ~ sQ1944_spl
| ~ s0(n0) ),
inference(resolution,[status(thm)],[f17812,f98]) ).
fof(f17863,plain,
( ~ sQ1944_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f17846,f567,f17811]) ).
fof(f17875,plain,
( ~ sQ1943_spl
| ~ s0(n0) ),
inference(resolution,[status(thm)],[f17809,f97]) ).
fof(f17904,definition,
( sQ1957_spl
<=> drugbg(n0) ),
introduced(definition,[new_symbols(definition,[sQ1957_spl])],[split_symbol_definition]) ).
fof(f17905,plain,
( ~ sQ1957_spl
| drugbg(n0) ),
inference(component_clause,[status(thm)],[f17904]) ).
fof(f17906,plain,
( sQ1957_spl
| ~ drugbg(n0) ),
inference(component_clause,[status(thm)],[f17904]) ).
fof(f17908,definition,
( sQ1958_spl
<=> drugsu(n0) ),
introduced(definition,[new_symbols(definition,[sQ1958_spl])],[split_symbol_definition]) ).
fof(f17909,plain,
( ~ sQ1958_spl
| drugsu(n0) ),
inference(component_clause,[status(thm)],[f17908]) ).
fof(f17910,plain,
( sQ1958_spl
| ~ drugsu(n0) ),
inference(component_clause,[status(thm)],[f17908]) ).
fof(f17912,plain,
( ~ sQ1943_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f17875,f567,f17808]) ).
fof(f17930,plain,
( ~ sQ1958_spl
| s3(n0)
| s2(n0)
| s1(n0) ),
inference(resolution,[status(thm)],[f17909,f126]) ).
fof(f17931,plain,
( ~ sQ1958_spl
| sQ1945_spl
| sQ1944_spl
| sQ1943_spl ),
inference(split_clause,[status(thm)],[f17930,f17808,f17811,f17814,f17908]) ).
fof(f17933,plain,
( ~ sQ1957_spl
| s3(n0)
| s2(n0)
| s1(n0) ),
inference(resolution,[status(thm)],[f17905,f123]) ).
fof(f17935,plain,
( ~ sQ1957_spl
| sQ1945_spl
| sQ1944_spl
| sQ1943_spl ),
inference(split_clause,[status(thm)],[f17933,f17808,f17811,f17814,f17904]) ).
fof(f17937,plain,
( ~ sQ654_spl
| sQ1958_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f17910,f5873]) ).
fof(f17939,plain,
( ~ sQ654_spl
| sQ1958_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17937,f43]) ).
fof(f17940,plain,
( ~ sQ654_spl
| sQ1958_spl ),
inference(contradiction_clause,[status(thm)],[f17939]) ).
fof(f17941,plain,
( ~ sQ166_spl
| sQ654_spl ),
inference(split_clause,[status(thm)],[f13602,f5872,f1792]) ).
fof(f17946,plain,
( ~ sQ665_spl
| sQ1957_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f17906,f5916]) ).
fof(f17948,plain,
( ~ sQ665_spl
| sQ1957_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17946,f43]) ).
fof(f17949,plain,
( ~ sQ665_spl
| sQ1957_spl ),
inference(contradiction_clause,[status(thm)],[f17948]) ).
fof(f17950,plain,
( ~ sQ1135_spl
| sQ665_spl ),
inference(split_clause,[status(thm)],[f16232,f5915,f10003]) ).
fof(f17954,plain,
( sQ139_spl
| ~ sQ145_spl ),
inference(split_clause,[status(thm)],[f2793,f1466,f1439]) ).
fof(f18022,plain,
( ~ sQ127_spl
| gt(n0,sK11_skl(n0)) ),
inference(resolution,[status(thm)],[f1377,f2498]) ).
fof(f18028,plain,
( ~ sQ127_spl
| sQ1135_spl ),
inference(split_clause,[status(thm)],[f18022,f10003,f1376]) ).
fof(f18031,plain,
$false,
inference(sat_refutation,[status(thm)],[f361,f457,f461,f570,f608,f1469,f1789,f2508,f3046,f3665,f3922,f5150,f6109,f7887,f8047,f8164,f8204,f8250,f8438,f8479,f8607,f8648,f9109,f9155,f9272,f9313,f9376,f9416,f9457,f9634,f9673,f9714,f9815,f10680,f10719,f10758,f10797,f10836,f10875,f10914,f10960,f10999,f11038,f11077,f11116,f11155,f11194,f11234,f11273,f12100,f12196,f12286,f12882,f12923,f12964,f13014,f13094,f14085,f15180,f15222,f15263,f15304,f15347,f15390,f15504,f16525,f17836,f17863,f17912,f17931,f17935,f17940,f17941,f17949,f17950,f17954,f18028]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MED005+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.40 % Computer : n011.cluster.edu
% 0.07/0.40 % Model : x86_64 x86_64
% 0.07/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.40 % Memory : 8046.5625MB
% 0.07/0.40 % OS : Linux 6.8.0-71-generic
% 0.07/0.40 % CPULimit : 300
% 0.07/0.40 % WCLimit : 300
% 0.07/0.40 % DateTime : Mon Sep 21 01:20:10 UTC 2026
% 0.07/0.40 % CPUTime :
% 0.09/0.42 % Drodi V4.1.1
% 94.12/12.32 % Refutation found
% 94.12/12.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 94.12/12.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 94.12/12.38 % Elapsed time: 11.958022 seconds
% 94.12/12.38 % CPU time: 94.644960 seconds
% 94.12/12.38 % Total memory used: 274.850 MB
% 94.12/12.38 % Net memory used: 237.004 MB
%------------------------------------------------------------------------------