%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MED005+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:24:57 PM UTC 2026
% Result : Theorem 220.28s 28.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED005+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.41 % Computer : n020.cluster.edu
% 0.08/0.41 % Model : x86_64 x86_64
% 0.08/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.41 % Memory : 8046.5625MB
% 0.08/0.41 % OS : Linux 6.8.0-71-generic
% 0.08/0.41 % CPULimit : 300
% 0.08/0.41 % WCLimit : 300
% 0.08/0.41 % DateTime : Mon Sep 21 01:21:02 UTC 2026
% 0.08/0.41 % CPUTime :
% 0.08/0.43 % Drodi V4.1.1
% 220.28/28.27 % Refutation found
% 220.28/28.27 % SZS status Theorem for theBenchmark: Theorem is valid
% 220.28/28.27 % SZS output start CNFRefutation for theBenchmark
% 220.28/28.27 fof(f1,axiom,(
% 220.28/28.27 (! [X] : ~ gt(X,X) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f2,axiom,(
% 220.28/28.27 (! [X,Y,Z] :( ( gt(X,Y)& gt(Y,Z) )=> gt(X,Z) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f4,axiom,(
% 220.28/28.27 (! [X0] :( ~ bcapacityne(X0)| ~ bcapacityex(X0) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f6,axiom,(
% 220.28/28.27 (! [X0] :( ~ bcapacityex(X0)| ~ bcapacitysn(X0) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f9,axiom,(
% 220.28/28.27 (! [X0] :( ~ conditionhyper(X0)| ~ conditionnormo(X0) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f12,axiom,(
% 220.28/28.27 (! [X0,X1] :( ~ gt(X0,X1)=> ( uptakelg(X1)=> ~ releaselg(X1) ) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f14,axiom,(
% 220.28/28.27 (! [X0] :( (! [X1] :( ~ gt(X0,X1)=> drugbg(X1) ))=> (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ) )) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f15,axiom,(
% 220.28/28.27 (! [X0] :( ( (! [X1] :( ~ gt(X0,X1)=> bsecretioni(X1) ))& bcapacitysn(X0)& qilt27(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) ))=> (! [X1] :( ~ gt(X0,X1)=> conditionnormo(X1) ) )) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f16,axiom,(
% 220.28/28.27 (! [X0] :( ( (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ))& bcapacitysn(X0)& ~ qilt27(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) ))=> (! [X1] :( ~ gt(X0,X1)=> conditionnormo(X1) ) )) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f17,axiom,(
% 220.28/28.27 (! [X0] :( ( ( (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ))| (! [X1] :( ~ gt(X0,X1)=> uptakepg(X1) ) ))& bcapacityne(X0)& (! [X1] :( ~ gt(X0,X1)=> bsecretioni(X1) ))& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) ))=> (! [X1] :( ~ gt(X0,X1)=> conditionnormo(X1) ) )) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f18,axiom,(
% 220.28/28.27 (! [X0] :( ( (! [X1] :( ~ gt(X0,X1)=> uptakelg(X1) ))& (! [X1] :( ~ gt(X0,X1)=> uptakepg(X1) ))& bcapacityex(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) ))=> (! [X1] :( ~ gt(X0,X1)=> ( conditionnormo(X1)| conditionhypo(X1) ) ) )) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f19,axiom,(
% 220.28/28.27 (! [X0] :( s0(X0)| s1(X0)| s2(X0)| s3(X0) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f20,axiom,(
% 220.28/28.27 (! [X0] :( ~ s0(X0)| ~ s1(X0) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f21,axiom,(
% 220.28/28.27 (! [X0] :( ~ s0(X0)| ~ s2(X0) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f22,axiom,(
% 220.28/28.27 (! [X0] :( ~ s0(X0)| ~ s3(X0) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f26,axiom,(
% 220.28/28.27 (! [X0] :( (! [X1] :( ~ gt(X0,X1)=> conditionnormo(X1) ))=> ( ( (! [X1] :( ~ gt(X0,X1)=> bsecretioni(X1) ))& bcapacitysn(X0)& qilt27(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) ))| ( (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ))& bcapacitysn(X0)& ~ qilt27(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) ))| ( ( (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ))| (! [X1] :( ~ gt(X0,X1)=> uptakepg(X1) ) ))& bcapacityne(X0)& (! [X1] :( ~ gt(X0,X1)=> bsecretioni(X1) ))& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) ))| ( (! [X1] :( ~ gt(X0,X1)=> uptakelg(X1) ))& (! [X1] :( ~ gt(X0,X1)=> uptakepg(X1) ))& bcapacityex(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) )) ) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f29,axiom,(
% 220.28/28.27 (! [X0] :( s2(X0)=> ( drugbg(X0)& drugsu(X0) ) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f30,axiom,(
% 220.28/28.27 (! [X0] :( s3(X0)=> ( ( drugi(X0)& ( drugsu(X0)| drugbg(X0) ) )| drugi(X0) ) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f31,axiom,(
% 220.28/28.27 (! [X0] :( drugbg(X0)=> ( ( s1(X0)& ~ qilt27(X0) )| s2(X0)| s3(X0) ) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f32,axiom,(
% 220.28/28.27 (! [X0] :( drugsu(X0)=> ( ( s1(X0)& qillt27(X0) )| s2(X0)| s3(X0) ) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f33,axiom,(
% 220.28/28.27 (! [X0] :( drugi(X0)=> s3(X0) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f35,axiom,(
% 220.28/28.27 (! [X0,X1] :( ~ gt(X0,X1)=> ( ~ releaselg(X1)=> uptakelg(X1) ) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f36,axiom,(
% 220.28/28.27 (! [X0] :( (! [X1] :( ~ gt(X0,X1)=> bsecretioni(X1) ))=> ( (! [X1] :( ~ gt(X0,X1)=> drugsu(X1) ))& ~ bcapacityex(X0) ) ) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f37,axiom,(
% 220.28/28.27 (! [X0] :( (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ))=> (! [X1] :( ~ gt(X0,X1)=> drugbg(X1) ) )) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f38,axiom,(
% 220.28/28.27 (! [X0] :( ( s0(X0)& ~ (! [X1] :( ~ gt(X0,X1)=> conditionnormo(X1) ) ))=> (? [X1] :( ~ gt(X0,X1)& s1(X1)& (! [X2] :( gt(X1,X2)=> conditionhyper(X2) ) )) )) )),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f41,conjecture,(
% 220.28/28.27 ( ( s0(n0)& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ) ))=> (? [X0] :( ~ gt(n0,X0)& s1(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) )) )) ),
% 220.28/28.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 220.28/28.27 fof(f42,negated_conjecture,(
% 220.28/28.27 ~(( ( s0(n0)& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ) ))=> (? [X0] :( ~ gt(n0,X0)& s1(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) )) )) )),
% 220.28/28.27 inference(negated_conjecture,[status(cth)],[f41])).
% 220.28/28.27 fof(f43,plain,(
% 220.28/28.27 ![X0]: (~gt(X0,X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f1])).
% 220.28/28.27 fof(f44,plain,(
% 220.28/28.27 ![X,Y,Z]: ((~gt(X,Y)|~gt(Y,Z))|gt(X,Z))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 220.28/28.27 fof(f45,plain,(
% 220.28/28.27 ![X,Z]: ((![Y]: (~gt(X,Y)|~gt(Y,Z)))|gt(X,Z))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f44])).
% 220.28/28.27 fof(f46,plain,(
% 220.28/28.27 ![X0,X1,X2]: (~gt(X0,X1)|~gt(X1,X2)|gt(X0,X2))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f45])).
% 220.28/28.27 fof(f48,plain,(
% 220.28/28.27 ![X0]: (~bcapacityne(X0)|~bcapacityex(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f4])).
% 220.28/28.27 fof(f50,plain,(
% 220.28/28.27 ![X0]: (~bcapacityex(X0)|~bcapacitysn(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f6])).
% 220.28/28.27 fof(f53,plain,(
% 220.28/28.27 ![X0]: (~conditionhyper(X0)|~conditionnormo(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f9])).
% 220.28/28.27 fof(f61,plain,(
% 220.28/28.27 ![X0,X1]: (gt(X0,X1)|(~uptakelg(X1)|~releaselg(X1)))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 220.28/28.27 fof(f62,plain,(
% 220.28/28.27 ![X1]: ((![X0]: gt(X0,X1))|(~uptakelg(X1)|~releaselg(X1)))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f61])).
% 220.28/28.27 fof(f63,plain,(
% 220.28/28.27 ![X0,X1]: (gt(X0,X1)|~uptakelg(X1)|~releaselg(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f62])).
% 220.28/28.27 fof(f68,plain,(
% 220.28/28.27 ![X0]: ((?[X1]: (~gt(X0,X1)&~drugbg(X1)))|(![X1]: (gt(X0,X1)|~releaselg(X1))))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 220.28/28.27 fof(f69,plain,(
% 220.28/28.27 ![X0]: ((~gt(X0,sK2_skl(X0))&~drugbg(sK2_skl(X0)))|(![X1]: (gt(X0,X1)|~releaselg(X1))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X1,sK2_skl(X0))],[f68])).
% 220.28/28.27 fof(f70,plain,(
% 220.28/28.27 ![X0,X1]: (~gt(X0,sK2_skl(X0))|gt(X0,X1)|~releaselg(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f69])).
% 220.28/28.27 fof(f72,plain,(
% 220.28/28.27 ![X0]: (((((?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))|~bcapacitysn(X0))|~qilt27(X0))|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))|(![X1]: (gt(X0,X1)|conditionnormo(X1))))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 220.28/28.27 fof(f73,definition,(
% 220.28/28.27 ![X0]: (sP1_prd(X0)<=>(((?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))|~bcapacitysn(X0))|~qilt27(X0)))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 220.28/28.27 fof(f78,plain,(
% 220.28/28.27 ![X0]: (((((?[X1]: (~gt(X0,X1)&releaselg(X1)))|~bcapacitysn(X0))|qilt27(X0))|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))|(![X1]: (gt(X0,X1)|conditionnormo(X1))))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 220.28/28.27 fof(f79,definition,(
% 220.28/28.27 ![X0]: (sP2_prd(X0)<=>(((?[X1]: (~gt(X0,X1)&releaselg(X1)))|~bcapacitysn(X0))|qilt27(X0)))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 220.28/28.27 fof(f84,plain,(
% 220.28/28.27 ![X0]: ((((((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0))|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1))))|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))|(![X1]: (gt(X0,X1)|conditionnormo(X1))))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 220.28/28.27 fof(f85,definition,(
% 220.28/28.27 ![X0]: (sP3_prd(X0)<=>((((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0))|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 220.28/28.27 fof(f90,plain,(
% 220.28/28.27 ![X0]: (((((?[X1]: (~gt(X0,X1)&~uptakelg(X1)))|(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityex(X0))|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))|(![X1]: (gt(X0,X1)|(conditionnormo(X1)|conditionhypo(X1)))))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 220.28/28.27 fof(f91,definition,(
% 220.28/28.27 ![X0]: (sP4_prd(X0)<=>(((?[X1]: (~gt(X0,X1)&~uptakelg(X1)))|(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityex(X0)))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 220.28/28.27 fof(f96,plain,(
% 220.28/28.27 ![X0]: (s0(X0)|s1(X0)|s2(X0)|s3(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f19])).
% 220.28/28.27 fof(f97,plain,(
% 220.28/28.27 ![X0]: (~s0(X0)|~s1(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f20])).
% 220.28/28.27 fof(f98,plain,(
% 220.28/28.27 ![X0]: (~s0(X0)|~s2(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f21])).
% 220.28/28.27 fof(f99,plain,(
% 220.28/28.27 ![X0]: (~s0(X0)|~s3(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f22])).
% 220.28/28.27 fof(f103,plain,(
% 220.28/28.27 ![X0]: ((?[X1]: (~gt(X0,X1)&~conditionnormo(X1)))|(((((((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))|((((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))|(((((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))&(![X1]: (gt(X0,X1)|bsecretioni(X1))))&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))|((((![X1]: (gt(X0,X1)|uptakelg(X1)))&(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityex(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 220.28/28.27 fof(f104,definition,(
% 220.28/28.27 ![X0,X1]: (sP5_prd(X1,X0)<=>(~gt(X0,X1)&~conditionnormo(X1)))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 220.28/28.27 fof(f105,definition,(
% 220.28/28.27 ![X0]: (sP6_prd(X0)<=>((((((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))|((((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))|(((((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))&(![X1]: (gt(X0,X1)|bsecretioni(X1))))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 220.28/28.27 fof(f106,plain,(
% 220.28/28.27 ![X0]: ((?[X1]: sP5_prd(X1,X0))|(sP6_prd(X0)|((((![X1]: (gt(X0,X1)|uptakelg(X1)))&(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityex(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 220.28/28.27 inference(formula_renaming,[status(thm)],[f103,f105,f104])).
% 220.28/28.27 fof(f107,plain,(
% 220.28/28.27 ![X0]: (sP5_prd(sK7_skl(X0),X0)|(sP6_prd(X0)|((((![X1]: (gt(X0,X1)|uptakelg(X1)))&(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityex(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X1,sK7_skl(X0))],[f106])).
% 220.28/28.27 fof(f108,plain,(
% 220.28/28.27 ![X0,X1]: (sP5_prd(sK7_skl(X0),X0)|sP6_prd(X0)|gt(X0,X1)|uptakelg(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f107])).
% 220.28/28.27 fof(f116,plain,(
% 220.28/28.27 ![X0]: (~s2(X0)|(drugbg(X0)&drugsu(X0)))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 220.28/28.27 fof(f117,plain,(
% 220.28/28.27 ![X0]: (~s2(X0)|drugbg(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f116])).
% 220.28/28.27 fof(f119,plain,(
% 220.28/28.27 ![X0]: (~s3(X0)|((drugi(X0)&(drugsu(X0)|drugbg(X0)))|drugi(X0)))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 220.28/28.27 fof(f120,plain,(
% 220.28/28.27 ![X0]: (~s3(X0)|drugi(X0)|drugi(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f119])).
% 220.28/28.27 fof(f122,plain,(
% 220.28/28.27 ![X0]: (~drugbg(X0)|(((s1(X0)&~qilt27(X0))|s2(X0))|s3(X0)))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 220.28/28.27 fof(f123,plain,(
% 220.28/28.27 ![X0]: (~drugbg(X0)|s1(X0)|s2(X0)|s3(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f122])).
% 220.28/28.27 fof(f125,plain,(
% 220.28/28.27 ![X0]: (~drugsu(X0)|(((s1(X0)&qillt27(X0))|s2(X0))|s3(X0)))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 220.28/28.27 fof(f126,plain,(
% 220.28/28.27 ![X0]: (~drugsu(X0)|s1(X0)|s2(X0)|s3(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f125])).
% 220.28/28.27 fof(f128,plain,(
% 220.28/28.27 ![X0]: (~drugi(X0)|s3(X0))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 220.28/28.27 fof(f129,plain,(
% 220.28/28.27 ![X0]: (~drugi(X0)|s3(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f128])).
% 220.28/28.27 fof(f136,plain,(
% 220.28/28.27 ![X0,X1]: (gt(X0,X1)|(releaselg(X1)|uptakelg(X1)))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 220.28/28.27 fof(f137,plain,(
% 220.28/28.27 ![X1]: ((![X0]: gt(X0,X1))|(releaselg(X1)|uptakelg(X1)))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f136])).
% 220.28/28.27 fof(f138,plain,(
% 220.28/28.27 ![X0,X1]: (gt(X0,X1)|releaselg(X1)|uptakelg(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f137])).
% 220.28/28.27 fof(f139,plain,(
% 220.28/28.27 ![X0]: ((?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))|((![X1]: (gt(X0,X1)|drugsu(X1)))&~bcapacityex(X0)))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 220.28/28.27 fof(f140,definition,(
% 220.28/28.27 ![X0,X1]: (sP7_prd(X1,X0)<=>(~gt(X0,X1)&~bsecretioni(X1)))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 220.28/28.27 fof(f141,plain,(
% 220.28/28.27 ![X0]: ((?[X1]: sP7_prd(X1,X0))|((![X1]: (gt(X0,X1)|drugsu(X1)))&~bcapacityex(X0)))),
% 220.28/28.27 inference(formula_renaming,[status(thm)],[f139,f140])).
% 220.28/28.27 fof(f142,plain,(
% 220.28/28.27 ![X0]: (sP7_prd(sK10_skl(X0),X0)|((![X1]: (gt(X0,X1)|drugsu(X1)))&~bcapacityex(X0)))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X1,sK10_skl(X0))],[f141])).
% 220.28/28.27 fof(f143,plain,(
% 220.28/28.27 ![X0,X1]: (sP7_prd(sK10_skl(X0),X0)|gt(X0,X1)|drugsu(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f142])).
% 220.28/28.27 fof(f145,plain,(
% 220.28/28.27 ![X0]: ((?[X1]: (~gt(X0,X1)&releaselg(X1)))|(![X1]: (gt(X0,X1)|drugbg(X1))))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 220.28/28.27 fof(f146,plain,(
% 220.28/28.27 ![X0]: ((~gt(X0,sK11_skl(X0))&releaselg(sK11_skl(X0)))|(![X1]: (gt(X0,X1)|drugbg(X1))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X1,sK11_skl(X0))],[f145])).
% 220.28/28.27 fof(f147,plain,(
% 220.28/28.27 ![X0,X1]: (~gt(X0,sK11_skl(X0))|gt(X0,X1)|drugbg(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f146])).
% 220.28/28.27 fof(f148,plain,(
% 220.28/28.27 ![X0,X1]: (releaselg(sK11_skl(X0))|gt(X0,X1)|drugbg(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f146])).
% 220.28/28.27 fof(f149,plain,(
% 220.28/28.27 ![X0]: ((~s0(X0)|(![X1]: (gt(X0,X1)|conditionnormo(X1))))|(?[X1]: ((~gt(X0,X1)&s1(X1))&(![X2]: (~gt(X1,X2)|conditionhyper(X2))))))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 220.28/28.27 fof(f150,plain,(
% 220.28/28.27 ![X0]: ((~s0(X0)|(![X1]: (gt(X0,X1)|conditionnormo(X1))))|((~gt(X0,sK12_skl(X0))&s1(sK12_skl(X0)))&(![X2]: (~gt(sK12_skl(X0),X2)|conditionhyper(X2)))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(X1,sK12_skl(X0))],[f149])).
% 220.28/28.27 fof(f151,plain,(
% 220.28/28.27 ![X0,X1]: (~s0(X0)|gt(X0,X1)|conditionnormo(X1)|~gt(X0,sK12_skl(X0)))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f150])).
% 220.28/28.27 fof(f152,plain,(
% 220.28/28.27 ![X0,X1]: (~s0(X0)|gt(X0,X1)|conditionnormo(X1)|s1(sK12_skl(X0)))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f150])).
% 220.28/28.27 fof(f153,plain,(
% 220.28/28.27 ![X0,X1,X2]: (~s0(X0)|gt(X0,X1)|conditionnormo(X1)|~gt(sK12_skl(X0),X2)|conditionhyper(X2))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f150])).
% 220.28/28.27 fof(f166,plain,(
% 220.28/28.27 ((s0(n0)&(![X0]: (~gt(n0,X0)|conditionhyper(X0))))&(![X0]: ((gt(n0,X0)|~s1(X0))|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))))),
% 220.28/28.27 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 220.28/28.27 fof(f167,plain,(
% 220.28/28.27 (s0(n0)&(![X0]: (~gt(n0,X0)|conditionhyper(X0))))&(![X0]: ((gt(n0,X0)|~s1(X0))|(gt(X0,sK15_skl(X0))&~conditionhyper(sK15_skl(X0)))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X1,sK15_skl(X0))],[f166])).
% 220.28/28.27 fof(f168,plain,(
% 220.28/28.27 s0(n0)),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f167])).
% 220.28/28.27 fof(f169,plain,(
% 220.28/28.27 ![X0]: (~gt(n0,X0)|conditionhyper(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f167])).
% 220.28/28.27 fof(f170,plain,(
% 220.28/28.27 ![X0]: (gt(n0,X0)|~s1(X0)|gt(X0,sK15_skl(X0)))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f167])).
% 220.28/28.27 fof(f171,plain,(
% 220.28/28.27 ![X0]: (gt(n0,X0)|~s1(X0)|~conditionhyper(sK15_skl(X0)))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f167])).
% 220.28/28.27 fof(f177,plain,(
% 220.28/28.27 ![X0]: ((~sP1_prd(X0)|(((?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))|~bcapacitysn(X0))|~qilt27(X0)))&(sP1_prd(X0)|(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f73])).
% 220.28/28.27 fof(f178,plain,(
% 220.28/28.27 (![X0]: (~sP1_prd(X0)|(((?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))|~bcapacitysn(X0))|~qilt27(X0))))&(![X0]: (sP1_prd(X0)|(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f177])).
% 220.28/28.27 fof(f179,plain,(
% 220.28/28.27 (![X0]: (~sP1_prd(X0)|(((~gt(X0,sK16_skl(X0))&~bsecretioni(sK16_skl(X0)))|~bcapacitysn(X0))|~qilt27(X0))))&(![X0]: (sP1_prd(X0)|(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(X1,sK16_skl(X0))],[f178])).
% 220.28/28.27 fof(f182,plain,(
% 220.28/28.27 ![X0,X1]: (sP1_prd(X0)|gt(X0,X1)|bsecretioni(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f179])).
% 220.28/28.27 fof(f185,plain,(
% 220.28/28.27 ![X0]: ((~sP2_prd(X0)|(((?[X1]: (~gt(X0,X1)&releaselg(X1)))|~bcapacitysn(X0))|qilt27(X0)))&(sP2_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f79])).
% 220.28/28.27 fof(f186,plain,(
% 220.28/28.27 (![X0]: (~sP2_prd(X0)|(((?[X1]: (~gt(X0,X1)&releaselg(X1)))|~bcapacitysn(X0))|qilt27(X0))))&(![X0]: (sP2_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f185])).
% 220.28/28.27 fof(f187,plain,(
% 220.28/28.27 (![X0]: (~sP2_prd(X0)|(((~gt(X0,sK17_skl(X0))&releaselg(sK17_skl(X0)))|~bcapacitysn(X0))|qilt27(X0))))&(![X0]: (sP2_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(X1,sK17_skl(X0))],[f186])).
% 220.28/28.27 fof(f190,plain,(
% 220.28/28.27 ![X0,X1]: (sP2_prd(X0)|gt(X0,X1)|~releaselg(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f187])).
% 220.28/28.27 fof(f193,definition,(
% 220.28/28.27 ![X0]: (sP8_prd(X0)<=>(((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0)))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 220.28/28.27 fof(f194,plain,(
% 220.28/28.27 ![X0]: (sP3_prd(X0)<=>(sP8_prd(X0)|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))))),
% 220.28/28.27 inference(formula_renaming,[status(thm)],[f85,f193])).
% 220.28/28.27 fof(f195,plain,(
% 220.28/28.27 ![X0]: ((~sP3_prd(X0)|(sP8_prd(X0)|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))))&(sP3_prd(X0)|(~sP8_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1))))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f194])).
% 220.28/28.27 fof(f196,plain,(
% 220.28/28.27 (![X0]: (~sP3_prd(X0)|(sP8_prd(X0)|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1))))))&(![X0]: (sP3_prd(X0)|(~sP8_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1))))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f195])).
% 220.28/28.27 fof(f197,plain,(
% 220.28/28.27 (![X0]: (~sP3_prd(X0)|(sP8_prd(X0)|(~gt(X0,sK18_skl(X0))&~bsecretioni(sK18_skl(X0))))))&(![X0]: (sP3_prd(X0)|(~sP8_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1))))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(X1,sK18_skl(X0))],[f196])).
% 220.28/28.27 fof(f201,plain,(
% 220.28/28.27 ![X0,X1]: (sP3_prd(X0)|gt(X0,X1)|bsecretioni(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f197])).
% 220.28/28.27 fof(f202,plain,(
% 220.28/28.27 ![X0]: ((~sP4_prd(X0)|(((?[X1]: (~gt(X0,X1)&~uptakelg(X1)))|(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityex(X0)))&(sP4_prd(X0)|(((![X1]: (gt(X0,X1)|uptakelg(X1)))&(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityex(X0))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f91])).
% 220.28/28.27 fof(f203,plain,(
% 220.28/28.27 (![X0]: (~sP4_prd(X0)|(((?[X1]: (~gt(X0,X1)&~uptakelg(X1)))|(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityex(X0))))&(![X0]: (sP4_prd(X0)|(((![X1]: (gt(X0,X1)|uptakelg(X1)))&(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityex(X0))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f202])).
% 220.28/28.27 fof(f204,plain,(
% 220.28/28.27 (![X0]: (~sP4_prd(X0)|(((~gt(X0,sK19_skl(X0))&~uptakelg(sK19_skl(X0)))|(~gt(X0,sK20_skl(X0))&~uptakepg(sK20_skl(X0))))|~bcapacityex(X0))))&(![X0]: (sP4_prd(X0)|(((![X1]: (gt(X0,X1)|uptakelg(X1)))&(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityex(X0))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(X1,sK19_skl(X0)),skolemize(X1,sK20_skl(X0))],[f203])).
% 220.28/28.27 fof(f209,plain,(
% 220.28/28.27 ![X0,X1]: (sP4_prd(X0)|gt(X0,X1)|uptakelg(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f204])).
% 220.28/28.27 fof(f212,plain,(
% 220.28/28.27 ![X0,X1]: ((~sP5_prd(X1,X0)|(~gt(X0,X1)&~conditionnormo(X1)))&(sP5_prd(X1,X0)|(gt(X0,X1)|conditionnormo(X1))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f104])).
% 220.28/28.27 fof(f213,plain,(
% 220.28/28.27 (![X0,X1]: (~sP5_prd(X1,X0)|(~gt(X0,X1)&~conditionnormo(X1))))&(![X0,X1]: (sP5_prd(X1,X0)|(gt(X0,X1)|conditionnormo(X1))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f212])).
% 220.28/28.27 fof(f214,plain,(
% 220.28/28.27 ![X0,X1]: (~sP5_prd(X0,X1)|~gt(X1,X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f213])).
% 220.28/28.27 fof(f215,plain,(
% 220.28/28.27 ![X0,X1]: (~sP5_prd(X0,X1)|~conditionnormo(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f213])).
% 220.28/28.27 fof(f217,definition,(
% 220.28/28.27 ![X0]: (sP9_prd(X0)<=>(((((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))|((((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 220.28/28.27 fof(f218,plain,(
% 220.28/28.27 ![X0]: (sP6_prd(X0)<=>(sP9_prd(X0)|(((((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))&(![X1]: (gt(X0,X1)|bsecretioni(X1))))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 220.28/28.27 inference(formula_renaming,[status(thm)],[f105,f217])).
% 220.28/28.27 fof(f219,definition,(
% 220.28/28.27 ![X0]: (sP10_prd(X0)<=>((((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))&(![X1]: (gt(X0,X1)|bsecretioni(X1)))))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 220.28/28.27 fof(f220,plain,(
% 220.28/28.27 ![X0]: (sP6_prd(X0)<=>(sP9_prd(X0)|(sP10_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 220.28/28.27 inference(formula_renaming,[status(thm)],[f218,f219])).
% 220.28/28.27 fof(f221,plain,(
% 220.28/28.27 ![X0]: ((~sP6_prd(X0)|(sP9_prd(X0)|(sP10_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))&(sP6_prd(X0)|(~sP9_prd(X0)&(~sP10_prd(X0)|(?[X1]: (gt(X0,X1)&~conditionhyper(X1)))))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f220])).
% 220.28/28.27 fof(f222,plain,(
% 220.28/28.27 (![X0]: (~sP6_prd(X0)|(sP9_prd(X0)|(sP10_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))))&(![X0]: (sP6_prd(X0)|(~sP9_prd(X0)&(~sP10_prd(X0)|(?[X1]: (gt(X0,X1)&~conditionhyper(X1)))))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f221])).
% 220.28/28.27 fof(f223,plain,(
% 220.28/28.27 (![X0]: (~sP6_prd(X0)|(sP9_prd(X0)|(sP10_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))))&(![X0]: (sP6_prd(X0)|(~sP9_prd(X0)&(~sP10_prd(X0)|(gt(X0,sK21_skl(X0))&~conditionhyper(sK21_skl(X0)))))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(X1,sK21_skl(X0))],[f222])).
% 220.28/28.27 fof(f224,plain,(
% 220.28/28.27 ![X0]: (~sP6_prd(X0)|sP9_prd(X0)|sP10_prd(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f223])).
% 220.28/28.27 fof(f229,plain,(
% 220.28/28.27 ![X0,X1]: ((~sP7_prd(X1,X0)|(~gt(X0,X1)&~bsecretioni(X1)))&(sP7_prd(X1,X0)|(gt(X0,X1)|bsecretioni(X1))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f140])).
% 220.28/28.27 fof(f230,plain,(
% 220.28/28.27 (![X0,X1]: (~sP7_prd(X1,X0)|(~gt(X0,X1)&~bsecretioni(X1))))&(![X0,X1]: (sP7_prd(X1,X0)|(gt(X0,X1)|bsecretioni(X1))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f229])).
% 220.28/28.27 fof(f231,plain,(
% 220.28/28.27 ![X0,X1]: (~sP7_prd(X0,X1)|~gt(X1,X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f230])).
% 220.28/28.27 fof(f232,plain,(
% 220.28/28.27 ![X0,X1]: (~sP7_prd(X0,X1)|~bsecretioni(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f230])).
% 220.28/28.27 fof(f243,definition,(
% 220.28/28.27 ![X0]: (sP11_prd(X0)<=>((((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 220.28/28.27 fof(f244,plain,(
% 220.28/28.27 ![X0]: (sP9_prd(X0)<=>(sP11_prd(X0)|((((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 220.28/28.27 inference(formula_renaming,[status(thm)],[f217,f243])).
% 220.28/28.27 fof(f245,definition,(
% 220.28/28.27 ![X0]: (sP12_prd(X0)<=>(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0)))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 220.28/28.27 fof(f246,plain,(
% 220.28/28.27 ![X0]: (sP9_prd(X0)<=>(sP11_prd(X0)|(sP12_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 220.28/28.27 inference(formula_renaming,[status(thm)],[f244,f245])).
% 220.28/28.27 fof(f247,plain,(
% 220.28/28.27 ![X0]: ((~sP9_prd(X0)|(sP11_prd(X0)|(sP12_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))&(sP9_prd(X0)|(~sP11_prd(X0)&(~sP12_prd(X0)|(?[X1]: (gt(X0,X1)&~conditionhyper(X1)))))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f246])).
% 220.28/28.27 fof(f248,plain,(
% 220.28/28.27 (![X0]: (~sP9_prd(X0)|(sP11_prd(X0)|(sP12_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))))&(![X0]: (sP9_prd(X0)|(~sP11_prd(X0)&(~sP12_prd(X0)|(?[X1]: (gt(X0,X1)&~conditionhyper(X1)))))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f247])).
% 220.28/28.27 fof(f249,plain,(
% 220.28/28.27 (![X0]: (~sP9_prd(X0)|(sP11_prd(X0)|(sP12_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))))&(![X0]: (sP9_prd(X0)|(~sP11_prd(X0)&(~sP12_prd(X0)|(gt(X0,sK24_skl(X0))&~conditionhyper(sK24_skl(X0)))))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(X1,sK24_skl(X0))],[f248])).
% 220.28/28.27 fof(f250,plain,(
% 220.28/28.27 ![X0]: (~sP9_prd(X0)|sP11_prd(X0)|sP12_prd(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f249])).
% 220.28/28.27 fof(f255,definition,(
% 220.28/28.27 ![X0]: (sP13_prd(X0)<=>(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0)))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 220.28/28.27 fof(f256,plain,(
% 220.28/28.27 ![X0]: (sP10_prd(X0)<=>(sP13_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1)))))),
% 220.28/28.27 inference(formula_renaming,[status(thm)],[f219,f255])).
% 220.28/28.27 fof(f257,plain,(
% 220.28/28.27 ![X0]: ((~sP10_prd(X0)|(sP13_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1)))))&(sP10_prd(X0)|(~sP13_prd(X0)|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1))))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f256])).
% 220.28/28.27 fof(f258,plain,(
% 220.28/28.27 (![X0]: (~sP10_prd(X0)|(sP13_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1))))))&(![X0]: (sP10_prd(X0)|(~sP13_prd(X0)|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1))))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f257])).
% 220.28/28.27 fof(f259,plain,(
% 220.28/28.27 (![X0]: (~sP10_prd(X0)|(sP13_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1))))))&(![X0]: (sP10_prd(X0)|(~sP13_prd(X0)|(~gt(X0,sK25_skl(X0))&~bsecretioni(sK25_skl(X0))))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(X1,sK25_skl(X0))],[f258])).
% 220.28/28.27 fof(f260,plain,(
% 220.28/28.27 ![X0]: (~sP10_prd(X0)|sP13_prd(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f259])).
% 220.28/28.27 fof(f261,plain,(
% 220.28/28.27 ![X0,X1]: (~sP10_prd(X0)|gt(X0,X1)|bsecretioni(X1))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f259])).
% 220.28/28.27 fof(f264,definition,(
% 220.28/28.27 ![X0]: (sP14_prd(X0)<=>(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0)))),
% 220.28/28.27 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 220.28/28.27 fof(f265,plain,(
% 220.28/28.27 ![X0]: (sP11_prd(X0)<=>(sP14_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))),
% 220.28/28.27 inference(formula_renaming,[status(thm)],[f243,f264])).
% 220.28/28.27 fof(f266,plain,(
% 220.28/28.27 ![X0]: ((~sP11_prd(X0)|(sP14_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))&(sP11_prd(X0)|(~sP14_prd(X0)|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f265])).
% 220.28/28.27 fof(f267,plain,(
% 220.28/28.27 (![X0]: (~sP11_prd(X0)|(sP14_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))&(![X0]: (sP11_prd(X0)|(~sP14_prd(X0)|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))))),
% 220.28/28.27 inference(miniscoping,[status(thm)],[f266])).
% 220.28/28.27 fof(f268,plain,(
% 220.28/28.27 (![X0]: (~sP11_prd(X0)|(sP14_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))&(![X0]: (sP11_prd(X0)|(~sP14_prd(X0)|(gt(X0,sK26_skl(X0))&~conditionhyper(sK26_skl(X0))))))),
% 220.28/28.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(X1,sK26_skl(X0))],[f267])).
% 220.28/28.27 fof(f269,plain,(
% 220.28/28.27 ![X0]: (~sP11_prd(X0)|sP14_prd(X0))),
% 220.28/28.27 inference(cnf_transformation,[status(thm)],[f268])).
% 220.28/28.27 fof(f273,plain,(
% 220.28/28.27 ![X0]: ((~sP12_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0)))&(sP12_prd(X0)|(((?[X1]: (~gt(X0,X1)&releaselg(X1)))|~bcapacitysn(X0))|qilt27(X0))))),
% 220.28/28.27 inference(NNF_transformation,[status(thm)],[f245])).
% 220.28/28.27 fof(f274,plain,(
% 220.28/28.27 (![X0]: (~sP12_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))))&(![X0]: (sP12_prd(X0)|(((?[X1]: (~gt(X0,X1)&releaselg(X1)))|~bcapacitysn(X0))|qilt27(X0))))),
% 220.28/28.28 inference(miniscoping,[status(thm)],[f273])).
% 220.28/28.28 fof(f275,plain,(
% 220.28/28.28 (![X0]: (~sP12_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))))&(![X0]: (sP12_prd(X0)|(((~gt(X0,sK27_skl(X0))&releaselg(sK27_skl(X0)))|~bcapacitysn(X0))|qilt27(X0))))),
% 220.28/28.28 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(X1,sK27_skl(X0))],[f274])).
% 220.28/28.28 fof(f276,plain,(
% 220.28/28.28 ![X0,X1]: (~sP12_prd(X0)|gt(X0,X1)|~releaselg(X1))),
% 220.28/28.28 inference(cnf_transformation,[status(thm)],[f275])).
% 220.28/28.28 fof(f281,plain,(
% 220.28/28.28 ![X0]: ((~sP13_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0)))&(sP13_prd(X0)|(((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0))))),
% 220.28/28.28 inference(NNF_transformation,[status(thm)],[f255])).
% 220.28/28.28 fof(f282,plain,(
% 220.28/28.28 (![X0]: (~sP13_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))))&(![X0]: (sP13_prd(X0)|(((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0))))),
% 220.28/28.28 inference(miniscoping,[status(thm)],[f281])).
% 220.28/28.28 fof(f283,plain,(
% 220.28/28.28 (![X0]: (~sP13_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))))&(![X0]: (sP13_prd(X0)|(((~gt(X0,sK28_skl(X0))&releaselg(sK28_skl(X0)))&(~gt(X0,sK29_skl(X0))&~uptakepg(sK29_skl(X0))))|~bcapacityne(X0))))),
% 220.28/28.28 inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl]),skolemize(X1,sK28_skl(X0)),skolemize(X1,sK29_skl(X0))],[f282])).
% 220.28/28.28 fof(f285,plain,(
% 220.28/28.28 ![X0]: (~sP13_prd(X0)|bcapacityne(X0))),
% 220.28/28.28 inference(cnf_transformation,[status(thm)],[f283])).
% 220.28/28.28 fof(f290,plain,(
% 220.28/28.28 ![X0]: ((~sP14_prd(X0)|(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0)))&(sP14_prd(X0)|(((?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))|~bcapacitysn(X0))|~qilt27(X0))))),
% 220.28/28.28 inference(NNF_transformation,[status(thm)],[f264])).
% 220.28/28.28 fof(f291,plain,(
% 220.28/28.28 (![X0]: (~sP14_prd(X0)|(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))))&(![X0]: (sP14_prd(X0)|(((?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))|~bcapacitysn(X0))|~qilt27(X0))))),
% 220.28/28.28 inference(miniscoping,[status(thm)],[f290])).
% 220.28/28.28 fof(f292,plain,(
% 220.28/28.28 (![X0]: (~sP14_prd(X0)|(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))))&(![X0]: (sP14_prd(X0)|(((~gt(X0,sK30_skl(X0))&~bsecretioni(sK30_skl(X0)))|~bcapacitysn(X0))|~qilt27(X0))))),
% 220.28/28.28 inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(X1,sK30_skl(X0))],[f291])).
% 220.28/28.28 fof(f293,plain,(
% 220.28/28.28 ![X0,X1]: (~sP14_prd(X0)|gt(X0,X1)|bsecretioni(X1))),
% 220.28/28.28 inference(cnf_transformation,[status(thm)],[f292])).
% 220.28/28.28 fof(f294,plain,(
% 220.28/28.28 ![X0]: (~sP14_prd(X0)|bcapacitysn(X0))),
% 220.28/28.28 inference(cnf_transformation,[status(thm)],[f292])).
% 220.28/28.28 fof(f298,plain,(
% 220.28/28.28 ![X0]: (~s3(X0)|drugi(X0))),
% 220.28/28.28 inference(duplicate_literals_removal,[status(thm)],[f120])).
% 220.28/28.28 fof(f306,plain,(
% 220.28/28.28 ![X0]: (drugi(X0)|s0(X0)|s1(X0)|s2(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f298,f96])).
% 220.28/28.28 fof(f308,plain,(
% 220.28/28.28 ![X0]: (drugi(X0)|s0(X0)|s1(X0)|drugbg(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f306,f117])).
% 220.28/28.28 fof(f317,definition,(
% 220.28/28.28 sQ0_spl <=> (drugi(n0))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f318,plain,(
% 220.28/28.28 drugi(n0)|~sQ0_spl),
% 220.28/28.28 inference(component_clause,[status(thm)],[f317])).
% 220.28/28.28 fof(f320,definition,(
% 220.28/28.28 sQ1_spl <=> (s0(n0))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f323,definition,(
% 220.28/28.28 sQ2_spl <=> (drugsu(n0))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f325,plain,(
% 220.28/28.28 ~drugsu(n0)|sQ2_spl),
% 220.28/28.28 inference(component_clause,[status(thm)],[f323])).
% 220.28/28.28 fof(f326,definition,(
% 220.28/28.28 sQ3_spl <=> (gt(n0,n0))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f327,plain,(
% 220.28/28.28 gt(n0,n0)|~sQ3_spl),
% 220.28/28.28 inference(component_clause,[status(thm)],[f326])).
% 220.28/28.28 fof(f334,definition,(
% 220.28/28.28 sQ5_spl <=> (s1(n0))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f335,plain,(
% 220.28/28.28 s1(n0)|~sQ5_spl),
% 220.28/28.28 inference(component_clause,[status(thm)],[f334])).
% 220.28/28.28 fof(f338,plain,(
% 220.28/28.28 $false|~sQ3_spl),
% 220.28/28.28 inference(forward_subsumption_resolution,[status(thm)],[f327,f43])).
% 220.28/28.28 fof(f339,plain,(
% 220.28/28.28 ~sQ3_spl),
% 220.28/28.28 inference(contradiction_clause,[status(thm)],[f338])).
% 220.28/28.28 fof(f346,plain,(
% 220.28/28.28 ![X0]: (drugi(X0)|s0(X0)|drugbg(X0)|gt(n0,X0)|gt(X0,sK15_skl(X0)))),
% 220.28/28.28 inference(resolution,[status(thm)],[f308,f170])).
% 220.28/28.28 fof(f347,definition,(
% 220.28/28.28 sQ6_spl <=> (drugbg(n0))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f349,plain,(
% 220.28/28.28 ~drugbg(n0)|sQ6_spl),
% 220.28/28.28 inference(component_clause,[status(thm)],[f347])).
% 220.28/28.28 fof(f353,plain,(
% 220.28/28.28 ![X0,X1]: (drugi(X0)|s0(X0)|drugbg(X0)|gt(n0,X0)|~gt(X1,X0)|gt(X1,sK15_skl(X0)))),
% 220.28/28.28 inference(resolution,[status(thm)],[f346,f46])).
% 220.28/28.28 fof(f430,plain,(
% 220.28/28.28 ![X0]: (bcapacityne(X0)|~sP10_prd(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f285,f260])).
% 220.28/28.28 fof(f431,plain,(
% 220.28/28.28 ![X0]: (bcapacitysn(X0)|~sP11_prd(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f294,f269])).
% 220.28/28.28 fof(f621,plain,(
% 220.28/28.28 ![X0]: (releaselg(X0)|uptakelg(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f138,f43])).
% 220.28/28.28 fof(f635,plain,(
% 220.28/28.28 ![X0,X1]: (sP1_prd(X0)|bsecretioni(X1)|drugi(X1)|s0(X1)|drugbg(X1)|gt(n0,X1)|gt(X0,sK15_skl(X1)))),
% 220.28/28.28 inference(resolution,[status(thm)],[f182,f353])).
% 220.28/28.28 fof(f637,plain,(
% 220.28/28.28 ![X0,X1,X2]: (sP1_prd(X0)|bsecretioni(X1)|~gt(X2,X0)|gt(X2,X1))),
% 220.28/28.28 inference(resolution,[status(thm)],[f182,f46])).
% 220.28/28.28 fof(f642,definition,(
% 220.28/28.28 ![X0]: (sQ20_spl <=> (bsecretioni(X0)|conditionhyper(X0)))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f643,plain,(
% 220.28/28.28 ![X0]: (bsecretioni(X0)|conditionhyper(X0)|~sQ20_spl)),
% 220.28/28.28 inference(component_clause,[status(thm)],[f642])).
% 220.28/28.28 fof(f646,plain,(
% 220.28/28.28 ![X0,X1]: (sP2_prd(X0)|gt(X0,X1)|uptakelg(X1))),
% 220.28/28.28 inference(resolution,[status(thm)],[f190,f621])).
% 220.28/28.28 fof(f686,definition,(
% 220.28/28.28 ![X0]: (sQ23_spl <=> (gt(n0,X0)|conditionnormo(X0)))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f687,plain,(
% 220.28/28.28 ![X0]: (gt(n0,X0)|conditionnormo(X0)|~sQ23_spl)),
% 220.28/28.28 inference(component_clause,[status(thm)],[f686])).
% 220.28/28.28 fof(f708,plain,(
% 220.28/28.28 ![X0,X1,X2]: (sP1_prd(X0)|bsecretioni(X1)|drugi(X1)|s0(X1)|drugbg(X1)|gt(n0,X1)|~gt(X2,X0)|gt(X2,sK15_skl(X1)))),
% 220.28/28.28 inference(resolution,[status(thm)],[f635,f46])).
% 220.28/28.28 fof(f743,plain,(
% 220.28/28.28 ![X0,X1]: (sP1_prd(X0)|bsecretioni(X1)|drugi(X1)|s0(X1)|drugbg(X1)|gt(n0,X1)|~gt(sK15_skl(X1),X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f708,f43])).
% 220.28/28.28 fof(f783,plain,(
% 220.28/28.28 ![X0,X1,X2]: (sP2_prd(X0)|uptakelg(X1)|~gt(X2,X0)|gt(X2,X1))),
% 220.28/28.28 inference(resolution,[status(thm)],[f646,f46])).
% 220.28/28.28 fof(f788,definition,(
% 220.28/28.28 ![X0]: (sQ34_spl <=> (uptakelg(X0)|conditionhyper(X0)))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f789,plain,(
% 220.28/28.28 ![X0]: (uptakelg(X0)|conditionhyper(X0)|~sQ34_spl)),
% 220.28/28.28 inference(component_clause,[status(thm)],[f788])).
% 220.28/28.28 fof(f800,definition,(
% 220.28/28.28 sQ35_spl <=> (conditionnormo(n0))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f801,plain,(
% 220.28/28.28 conditionnormo(n0)|~sQ35_spl),
% 220.28/28.28 inference(component_clause,[status(thm)],[f800])).
% 220.28/28.28 fof(f819,plain,(
% 220.28/28.28 ![X0,X1]: (sP1_prd(X0)|bsecretioni(X1)|~gt(X1,X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f637,f43])).
% 220.28/28.28 fof(f878,definition,(
% 220.28/28.28 ![X0]: (sQ40_spl <=> (sP1_prd(sK15_skl(X0))|bsecretioni(X0)|drugi(X0)|s0(X0)|drugbg(X0)|gt(n0,X0)))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f892,definition,(
% 220.28/28.28 ![X0]: (sQ43_spl <=> (sP1_prd(X0)|bsecretioni(X0)))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f937,plain,(
% 220.28/28.28 ![X0,X1]: (sP1_prd(X0)|bsecretioni(X1)|sP1_prd(X1)|bsecretioni(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f819,f182])).
% 220.28/28.28 fof(f953,plain,(
% 220.28/28.28 sQ43_spl),
% 220.28/28.28 inference(split_clause,[status(thm)],[f937,f892])).
% 220.28/28.28 fof(f1018,plain,(
% 220.28/28.28 ![X0,X1,X2]: (sP3_prd(X0)|bsecretioni(X1)|~gt(X2,X0)|gt(X2,X1))),
% 220.28/28.28 inference(resolution,[status(thm)],[f201,f46])).
% 220.28/28.28 fof(f1025,definition,(
% 220.28/28.28 ![X0]: (sQ50_spl <=> (sP3_prd(X0)|bsecretioni(X0)))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f1029,plain,(
% 220.28/28.28 ![X0,X1]: (conditionhyper(X0)|~sP7_prd(X0,X1)|~sQ20_spl)),
% 220.28/28.28 inference(resolution,[status(thm)],[f643,f232])).
% 220.28/28.28 fof(f1047,plain,(
% 220.28/28.28 ![X0,X1,X2]: (sP4_prd(X0)|uptakelg(X1)|~gt(X2,X0)|gt(X2,X1))),
% 220.28/28.28 inference(resolution,[status(thm)],[f209,f46])).
% 220.28/28.28 fof(f1054,definition,(
% 220.28/28.28 ![X0]: (sQ52_spl <=> (sP4_prd(X0)|bsecretioni(X0)))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f1086,plain,(
% 220.28/28.28 ![X0,X1]: (gt(X0,X1)|bsecretioni(X1)|~sP11_prd(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f293,f269])).
% 220.28/28.28 fof(f1241,plain,(
% 220.28/28.28 ![X0,X1]: (sP1_prd(sK15_skl(X0))|bsecretioni(X1)|drugi(X1)|s0(X1)|drugbg(X1)|gt(n0,X1)|sP1_prd(sK15_skl(X1))|bsecretioni(X0)|drugi(X0)|s0(X0)|drugbg(X0)|gt(n0,X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f743,f635])).
% 220.28/28.28 fof(f1261,plain,(
% 220.28/28.28 sQ40_spl),
% 220.28/28.28 inference(split_clause,[status(thm)],[f1241,f878])).
% 220.28/28.28 fof(f1420,plain,(
% 220.28/28.28 ![X0,X1]: (sP2_prd(X0)|uptakelg(X1)|~gt(X1,X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f783,f43])).
% 220.28/28.28 fof(f1479,plain,(
% 220.28/28.28 ![X0,X1]: (sP2_prd(X0)|uptakelg(X1)|sP2_prd(X1)|uptakelg(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f1420,f646])).
% 220.28/28.28 fof(f1493,definition,(
% 220.28/28.28 ![X1]: (sQ85_spl <=> (uptakelg(X1)|sP2_prd(X1)))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f1521,definition,(
% 220.28/28.28 ![X1]: (sQ92_spl <=> (uptakelg(X1)|sP4_prd(X1)))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f1531,plain,(
% 220.28/28.28 sQ85_spl),
% 220.28/28.28 inference(split_clause,[status(thm)],[f1479,f1493])).
% 220.28/28.28 fof(f1582,plain,(
% 220.28/28.28 ![X0,X1]: (sP3_prd(X0)|bsecretioni(X1)|~gt(X1,X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f1018,f43])).
% 220.28/28.28 fof(f1600,plain,(
% 220.28/28.28 s3(n0)|~sQ0_spl),
% 220.28/28.28 inference(resolution,[status(thm)],[f318,f129])).
% 220.28/28.28 fof(f1732,plain,(
% 220.28/28.28 ![X0,X1]: (sP4_prd(X0)|uptakelg(X1)|~gt(X1,X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f1047,f43])).
% 220.28/28.28 fof(f1791,plain,(
% 220.28/28.28 ![X0,X1]: (sP3_prd(X0)|bsecretioni(X1)|sP3_prd(X1)|bsecretioni(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f1582,f201])).
% 220.28/28.28 fof(f1817,plain,(
% 220.28/28.28 sQ50_spl),
% 220.28/28.28 inference(split_clause,[status(thm)],[f1791,f1025])).
% 220.28/28.28 fof(f1942,plain,(
% 220.28/28.28 ![X0,X1]: (sP4_prd(X0)|uptakelg(X1)|sP4_prd(X1)|uptakelg(X0))),
% 220.28/28.28 inference(resolution,[status(thm)],[f1732,f209])).
% 220.28/28.28 fof(f1971,plain,(
% 220.28/28.28 sQ92_spl),
% 220.28/28.28 inference(split_clause,[status(thm)],[f1942,f1521])).
% 220.28/28.28 fof(f2002,plain,(
% 220.28/28.28 ![X0,X1,X2]: (sP5_prd(sK7_skl(X0),X0)|sP6_prd(X0)|uptakelg(X1)|~gt(X2,X0)|gt(X2,X1))),
% 220.28/28.28 inference(resolution,[status(thm)],[f108,f46])).
% 220.28/28.28 fof(f2008,definition,(
% 220.28/28.28 sQ128_spl <=> (sP5_prd(sK7_skl(n0),n0))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 220.28/28.28 fof(f2009,plain,(
% 220.28/28.28 sP5_prd(sK7_skl(n0),n0)|~sQ128_spl),
% 220.28/28.28 inference(component_clause,[status(thm)],[f2008])).
% 220.28/28.28 fof(f2010,plain,(
% 220.28/28.28 ~sP5_prd(sK7_skl(n0),n0)|sQ128_spl),
% 220.28/28.28 inference(component_clause,[status(thm)],[f2008])).
% 220.28/28.28 fof(f2011,definition,(
% 220.28/28.28 sQ129_spl <=> (sP6_prd(n0))),
% 220.28/28.28 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2012,plain,(
% 220.28/28.29 sP6_prd(n0)|~sQ129_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2011])).
% 220.28/28.29 fof(f2020,definition,(
% 220.28/28.29 ![X0]: (sQ131_spl <=> (sP5_prd(sK7_skl(X0),X0)|sP6_prd(X0)|bsecretioni(X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2060,plain,(
% 220.28/28.29 ~s0(n0)|~sQ0_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f1600,f99])).
% 220.28/28.29 fof(f2061,plain,(
% 220.28/28.29 $false|~sQ0_spl),
% 220.28/28.29 inference(forward_subsumption_resolution,[status(thm)],[f2060,f168])).
% 220.28/28.29 fof(f2062,plain,(
% 220.28/28.29 ~sQ0_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f2061])).
% 220.28/28.29 fof(f2063,plain,(
% 220.28/28.29 ~conditionhyper(n0)|~sQ35_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f801,f53])).
% 220.28/28.29 fof(f2066,plain,(
% 220.28/28.29 sP9_prd(n0)|sP10_prd(n0)|~sQ129_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2012,f224])).
% 220.28/28.29 fof(f2067,definition,(
% 220.28/28.29 sQ132_spl <=> (sP9_prd(n0))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2068,plain,(
% 220.28/28.29 sP9_prd(n0)|~sQ132_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2067])).
% 220.28/28.29 fof(f2070,definition,(
% 220.28/28.29 sQ133_spl <=> (sP10_prd(n0))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2071,plain,(
% 220.28/28.29 sP10_prd(n0)|~sQ133_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2070])).
% 220.28/28.29 fof(f2073,plain,(
% 220.28/28.29 sQ132_spl|sQ133_spl|~sQ129_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f2066,f2067,f2070,f2011])).
% 220.28/28.29 fof(f2074,plain,(
% 220.28/28.29 ![X0]: (gt(n0,X0)|bsecretioni(X0)|~sQ133_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2071,f261])).
% 220.28/28.29 fof(f2075,plain,(
% 220.28/28.29 bcapacityne(n0)|~sQ133_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2071,f430])).
% 220.28/28.29 fof(f2160,plain,(
% 220.28/28.29 conditionnormo(n0)|~sQ23_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f687,f43])).
% 220.28/28.29 fof(f2164,definition,(
% 220.28/28.29 ![X0]: (sQ135_spl <=> (gt(n0,X0)|~releaselg(X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2165,plain,(
% 220.28/28.29 ![X0]: (gt(n0,X0)|~releaselg(X0)|~sQ135_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2164])).
% 220.28/28.29 fof(f2171,definition,(
% 220.28/28.29 sQ137_spl <=> (bcapacityex(n0))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2172,plain,(
% 220.28/28.29 bcapacityex(n0)|~sQ137_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2171])).
% 220.28/28.29 fof(f2174,definition,(
% 220.28/28.29 ![X0]: (sQ138_spl <=> (gt(n0,X0)|bsecretioni(X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2175,plain,(
% 220.28/28.29 ![X0]: (gt(n0,X0)|bsecretioni(X0)|~sQ138_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2174])).
% 220.28/28.29 fof(f2197,plain,(
% 220.28/28.29 ~bcapacityne(n0)|~sQ137_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2172,f48])).
% 220.28/28.29 fof(f2198,plain,(
% 220.28/28.29 $false|~sQ133_spl|~sQ137_spl),
% 220.28/28.29 inference(forward_subsumption_resolution,[status(thm)],[f2197,f2075])).
% 220.28/28.29 fof(f2199,plain,(
% 220.28/28.29 ~sQ133_spl|~sQ137_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f2198])).
% 220.28/28.29 fof(f2342,plain,(
% 220.28/28.29 sP11_prd(n0)|sP12_prd(n0)|~sQ132_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2068,f250])).
% 220.28/28.29 fof(f2344,definition,(
% 220.28/28.29 sQ152_spl <=> (sP11_prd(n0))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2345,plain,(
% 220.28/28.29 sP11_prd(n0)|~sQ152_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2344])).
% 220.28/28.29 fof(f2347,definition,(
% 220.28/28.29 sQ153_spl <=> (sP12_prd(n0))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2348,plain,(
% 220.28/28.29 sP12_prd(n0)|~sQ153_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2347])).
% 220.28/28.29 fof(f2350,plain,(
% 220.28/28.29 sQ152_spl|sQ153_spl|~sQ132_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f2342,f2344,f2347,f2067])).
% 220.28/28.29 fof(f2352,plain,(
% 220.28/28.29 ![X0]: (gt(n0,X0)|bsecretioni(X0)|~sQ152_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2345,f1086])).
% 220.28/28.29 fof(f2355,plain,(
% 220.28/28.29 bcapacitysn(n0)|~sQ152_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2345,f431])).
% 220.28/28.29 fof(f2600,definition,(
% 220.28/28.29 ![X0]: (sQ176_spl <=> (uptakelg(X0)|gt(n0,X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2601,plain,(
% 220.28/28.29 ![X0]: (uptakelg(X0)|gt(n0,X0)|~sQ176_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2600])).
% 220.28/28.29 fof(f2678,plain,(
% 220.28/28.29 ~s0(n0)|~sQ5_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f335,f97])).
% 220.28/28.29 fof(f2684,plain,(
% 220.28/28.29 $false|~sQ5_spl),
% 220.28/28.29 inference(forward_subsumption_resolution,[status(thm)],[f2678,f168])).
% 220.28/28.29 fof(f2685,plain,(
% 220.28/28.29 ~sQ5_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f2684])).
% 220.28/28.29 fof(f2688,definition,(
% 220.28/28.29 sQ185_spl <=> (s2(n0))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2689,plain,(
% 220.28/28.29 s2(n0)|~sQ185_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2688])).
% 220.28/28.29 fof(f2690,plain,(
% 220.28/28.29 ~s2(n0)|sQ185_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2688])).
% 220.28/28.29 fof(f2691,definition,(
% 220.28/28.29 sQ186_spl <=> (s3(n0))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2692,plain,(
% 220.28/28.29 s3(n0)|~sQ186_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2691])).
% 220.28/28.29 fof(f2693,plain,(
% 220.28/28.29 ~s3(n0)|sQ186_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2691])).
% 220.28/28.29 fof(f2701,plain,(
% 220.28/28.29 ~s0(n0)|~sQ186_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2692,f99])).
% 220.28/28.29 fof(f2703,plain,(
% 220.28/28.29 $false|~sQ186_spl),
% 220.28/28.29 inference(forward_subsumption_resolution,[status(thm)],[f2701,f168])).
% 220.28/28.29 fof(f2704,plain,(
% 220.28/28.29 ~sQ186_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f2703])).
% 220.28/28.29 fof(f2709,plain,(
% 220.28/28.29 ~s0(n0)|~sQ185_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2689,f98])).
% 220.28/28.29 fof(f2710,plain,(
% 220.28/28.29 $false|~sQ185_spl),
% 220.28/28.29 inference(forward_subsumption_resolution,[status(thm)],[f2709,f168])).
% 220.28/28.29 fof(f2711,plain,(
% 220.28/28.29 ~sQ185_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f2710])).
% 220.28/28.29 fof(f2712,plain,(
% 220.28/28.29 ~drugsu(n0)|s1(n0)|s2(n0)|sQ186_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2693,f126])).
% 220.28/28.29 fof(f2713,plain,(
% 220.28/28.29 ~drugbg(n0)|s1(n0)|s2(n0)|sQ186_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2693,f123])).
% 220.28/28.29 fof(f2715,plain,(
% 220.28/28.29 ~sQ2_spl|sQ5_spl|sQ185_spl|sQ186_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f2712,f323,f334,f2688,f2691])).
% 220.28/28.29 fof(f2716,plain,(
% 220.28/28.29 ~sQ6_spl|sQ5_spl|sQ185_spl|sQ186_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f2713,f347,f334,f2688,f2691])).
% 220.28/28.29 fof(f2797,plain,(
% 220.28/28.29 drugi(n0)|s0(n0)|s1(n0)|sQ185_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2690,f306])).
% 220.28/28.29 fof(f2798,plain,(
% 220.28/28.29 sQ0_spl|sQ1_spl|sQ5_spl|sQ185_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f2797,f317,f320,f334,f2688])).
% 220.28/28.29 fof(f2820,plain,(
% 220.28/28.29 ![X0]: (sP7_prd(sK10_skl(n0),n0)|drugsu(X0)|conditionhyper(X0))),
% 220.28/28.29 inference(resolution,[status(thm)],[f143,f169])).
% 220.28/28.29 fof(f2834,plain,(
% 220.28/28.29 ![X0,X1,X2]: (sP7_prd(sK10_skl(X0),X0)|drugsu(X1)|~gt(X2,X0)|gt(X2,X1))),
% 220.28/28.29 inference(resolution,[status(thm)],[f143,f46])).
% 220.28/28.29 fof(f2838,definition,(
% 220.28/28.29 sQ196_spl <=> (sP7_prd(sK10_skl(n0),n0))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2839,plain,(
% 220.28/28.29 sP7_prd(sK10_skl(n0),n0)|~sQ196_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2838])).
% 220.28/28.29 fof(f2845,definition,(
% 220.28/28.29 ![X0]: (sQ198_spl <=> (drugsu(X0)|conditionhyper(X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2846,plain,(
% 220.28/28.29 ![X0]: (drugsu(X0)|conditionhyper(X0)|~sQ198_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2845])).
% 220.28/28.29 fof(f2848,plain,(
% 220.28/28.29 sQ196_spl|sQ198_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f2820,f2838,f2845])).
% 220.28/28.29 fof(f2868,definition,(
% 220.28/28.29 ![X0]: (sQ204_spl <=> (sP7_prd(sK10_skl(X0),X0)|bsecretioni(X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2922,plain,(
% 220.28/28.29 ![X0,X1,X2]: (releaselg(sK11_skl(X0))|drugbg(X1)|~gt(X2,X0)|gt(X2,X1))),
% 220.28/28.29 inference(resolution,[status(thm)],[f148,f46])).
% 220.28/28.29 fof(f2923,plain,(
% 220.28/28.29 ![X0]: (releaselg(sK11_skl(X0))|drugbg(X0))),
% 220.28/28.29 inference(resolution,[status(thm)],[f148,f43])).
% 220.28/28.29 fof(f2926,definition,(
% 220.28/28.29 sQ207_spl <=> (releaselg(sK11_skl(n0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2927,plain,(
% 220.28/28.29 releaselg(sK11_skl(n0))|~sQ207_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2926])).
% 220.28/28.29 fof(f2928,plain,(
% 220.28/28.29 ~releaselg(sK11_skl(n0))|sQ207_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2926])).
% 220.28/28.29 fof(f2956,definition,(
% 220.28/28.29 ![X0]: (sQ215_spl <=> (releaselg(sK11_skl(X0))|bsecretioni(X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2985,plain,(
% 220.28/28.29 conditionhyper(n0)|~sQ198_spl|sQ2_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2846,f325])).
% 220.28/28.29 fof(f2987,plain,(
% 220.28/28.29 $false|~sQ35_spl|~sQ198_spl|sQ2_spl),
% 220.28/28.29 inference(forward_subsumption_resolution,[status(thm)],[f2985,f2063])).
% 220.28/28.29 fof(f2988,plain,(
% 220.28/28.29 ~sQ35_spl|~sQ198_spl|sQ2_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f2987])).
% 220.28/28.29 fof(f2991,plain,(
% 220.28/28.29 ![X0]: (gt(X0,sK11_skl(n0))|~uptakelg(sK11_skl(n0))|~sQ207_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2927,f63])).
% 220.28/28.29 fof(f2992,definition,(
% 220.28/28.29 ![X0]: (sQ218_spl <=> (gt(X0,sK11_skl(n0))))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2993,plain,(
% 220.28/28.29 ![X0]: (gt(X0,sK11_skl(n0))|~sQ218_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2992])).
% 220.28/28.29 fof(f2995,definition,(
% 220.28/28.29 sQ219_spl <=> (uptakelg(sK11_skl(n0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f2997,plain,(
% 220.28/28.29 ~uptakelg(sK11_skl(n0))|sQ219_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f2995])).
% 220.28/28.29 fof(f2998,plain,(
% 220.28/28.29 sQ218_spl|~sQ219_spl|~sQ207_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f2991,f2992,f2995,f2926])).
% 220.28/28.29 fof(f3020,plain,(
% 220.28/28.29 ![X0]: (gt(n0,X0)|conditionnormo(X0)|~gt(n0,sK12_skl(n0)))),
% 220.28/28.29 inference(resolution,[status(thm)],[f151,f168])).
% 220.28/28.29 fof(f3026,definition,(
% 220.28/28.29 sQ221_spl <=> (gt(n0,sK12_skl(n0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f3029,plain,(
% 220.28/28.29 sQ23_spl|~sQ221_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f3020,f686,f3026])).
% 220.28/28.29 fof(f3030,plain,(
% 220.28/28.29 sQ35_spl|~sQ23_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f2160,f800,f686])).
% 220.28/28.29 fof(f3032,plain,(
% 220.28/28.29 ![X0]: (gt(n0,X0)|conditionnormo(X0)|s1(sK12_skl(n0)))),
% 220.28/28.29 inference(resolution,[status(thm)],[f152,f168])).
% 220.28/28.29 fof(f3038,definition,(
% 220.28/28.29 sQ223_spl <=> (s1(sK12_skl(n0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f3039,plain,(
% 220.28/28.29 s1(sK12_skl(n0))|~sQ223_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f3038])).
% 220.28/28.29 fof(f3041,plain,(
% 220.28/28.29 sQ23_spl|sQ223_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f3032,f686,f3038])).
% 220.28/28.29 fof(f3043,plain,(
% 220.28/28.29 ![X0,X1]: (gt(n0,X0)|conditionnormo(X0)|~gt(sK12_skl(n0),X1)|conditionhyper(X1))),
% 220.28/28.29 inference(resolution,[status(thm)],[f153,f168])).
% 220.28/28.29 fof(f3049,definition,(
% 220.28/28.29 ![X1]: (sQ225_spl <=> (~gt(sK12_skl(n0),X1)|conditionhyper(X1)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f3050,plain,(
% 220.28/28.29 ![X0]: (~gt(sK12_skl(n0),X0)|conditionhyper(X0)|~sQ225_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f3049])).
% 220.28/28.29 fof(f3052,plain,(
% 220.28/28.29 sQ23_spl|sQ225_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f3043,f686,f3049])).
% 220.28/28.29 fof(f3057,plain,(
% 220.28/28.29 conditionhyper(sK11_skl(n0))|sQ219_spl|~sQ34_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2997,f789])).
% 220.28/28.29 fof(f3119,plain,(
% 220.28/28.29 gt(n0,sK12_skl(n0))|gt(sK12_skl(n0),sK15_skl(sK12_skl(n0)))|~sQ223_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f3039,f170])).
% 220.28/28.29 fof(f3124,definition,(
% 220.28/28.29 sQ233_spl <=> (gt(sK12_skl(n0),sK15_skl(sK12_skl(n0))))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f3125,plain,(
% 220.28/28.29 gt(sK12_skl(n0),sK15_skl(sK12_skl(n0)))|~sQ233_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f3124])).
% 220.28/28.29 fof(f3127,plain,(
% 220.28/28.29 sQ221_spl|sQ233_spl|~sQ223_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f3119,f3026,f3124,f3038])).
% 220.28/28.29 fof(f3308,plain,(
% 220.28/28.29 $false|~sQ218_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2993,f43])).
% 220.28/28.29 fof(f3367,definition,(
% 220.28/28.29 ![X0,X1]: (sQ271_spl <=> (uptakelg(X0)|gt(X1,X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f3368,plain,(
% 220.28/28.29 ![X0,X1]: (uptakelg(X0)|gt(X1,X0)|~sQ271_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f3367])).
% 220.28/28.29 fof(f3374,definition,(
% 220.28/28.29 ![X0]: (sQ273_spl <=> (uptakelg(X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f3375,plain,(
% 220.28/28.29 ![X0]: (uptakelg(X0)|~sQ273_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f3374])).
% 220.28/28.29 fof(f3395,plain,(
% 220.28/28.29 ~sQ218_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f3308])).
% 220.28/28.29 fof(f3403,plain,(
% 220.28/28.29 $false|~sQ273_spl|sQ219_spl),
% 220.28/28.29 inference(backward_subsumption_resolution,[status(thm)],[f2997,f3375])).
% 220.28/28.29 fof(f3420,plain,(
% 220.28/28.29 ~sQ273_spl|sQ219_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f3403])).
% 220.28/28.29 fof(f3435,plain,(
% 220.28/28.29 ![X0,X1]: (gt(X0,X1)|~releaselg(X1)|~sQ271_spl)),
% 220.28/28.29 inference(backward_subsumption_resolution,[status(thm)],[f63,f3368])).
% 220.28/28.29 fof(f3526,plain,(
% 220.28/28.29 drugbg(n0)|sQ207_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2923,f2928])).
% 220.28/28.29 fof(f3528,plain,(
% 220.28/28.29 sQ6_spl|sQ207_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f3526,f347,f2926])).
% 220.28/28.29 fof(f3588,plain,(
% 220.28/28.29 ![X0]: (gt(X0,sK11_skl(n0))|~sQ207_spl|~sQ271_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2927,f3435])).
% 220.28/28.29 fof(f3589,plain,(
% 220.28/28.29 sQ218_spl|~sQ207_spl|~sQ271_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f3588,f2992,f2926,f3367])).
% 220.28/28.29 fof(f3660,plain,(
% 220.28/28.29 conditionhyper(sK15_skl(sK12_skl(n0)))|~sQ233_spl|~sQ225_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f3125,f3050])).
% 220.28/28.29 fof(f3826,definition,(
% 220.28/28.29 ![X1,X2]: (sQ325_spl <=> (drugbg(X1)|gt(X2,X1)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f3827,plain,(
% 220.28/28.29 ![X0,X1]: (drugbg(X0)|gt(X1,X0)|~sQ325_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f3826])).
% 220.28/28.29 fof(f4009,plain,(
% 220.28/28.29 ![X0]: (drugbg(X0)|~sQ325_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f3827,f43])).
% 220.28/28.29 fof(f4015,plain,(
% 220.28/28.29 $false|~sQ325_spl|sQ6_spl),
% 220.28/28.29 inference(backward_subsumption_resolution,[status(thm)],[f349,f4009])).
% 220.28/28.29 fof(f4019,plain,(
% 220.28/28.29 ~sQ325_spl|sQ6_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f4015])).
% 220.28/28.29 fof(f4043,plain,(
% 220.28/28.29 ~gt(n0,sK7_skl(n0))|~sQ128_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2009,f214])).
% 220.28/28.29 fof(f4044,plain,(
% 220.28/28.29 ~conditionnormo(sK7_skl(n0))|~sQ128_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2009,f215])).
% 220.28/28.29 fof(f4243,definition,(
% 220.28/28.29 ![X0]: (sQ361_spl <=> (drugsu(X0)|gt(n0,X0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f4244,plain,(
% 220.28/28.29 ![X0]: (drugsu(X0)|gt(n0,X0)|~sQ361_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f4243])).
% 220.28/28.29 fof(f4376,plain,(
% 220.28/28.29 ![X0]: (bsecretioni(X0)|conditionhyper(X0)|~sQ138_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2175,f169])).
% 220.28/28.29 fof(f4380,plain,(
% 220.28/28.29 ![X0,X1]: (bsecretioni(X0)|sP7_prd(sK10_skl(X0),X0)|drugsu(X1)|gt(n0,X1)|~sQ138_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2175,f2834])).
% 220.28/28.29 fof(f4383,plain,(
% 220.28/28.29 ![X0,X1]: (bsecretioni(X0)|sP5_prd(sK7_skl(X0),X0)|sP6_prd(X0)|uptakelg(X1)|gt(n0,X1)|~sQ138_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2175,f2002])).
% 220.28/28.29 fof(f4384,plain,(
% 220.28/28.29 ![X0,X1]: (bsecretioni(X0)|sP4_prd(X0)|uptakelg(X1)|gt(n0,X1)|~sQ138_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2175,f1047])).
% 220.28/28.29 fof(f4393,plain,(
% 220.28/28.29 sQ204_spl|sQ361_spl|~sQ138_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f4380,f2868,f4243,f2174])).
% 220.28/28.29 fof(f4396,plain,(
% 220.28/28.29 sQ131_spl|sQ176_spl|~sQ138_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f4383,f2020,f2600,f2174])).
% 220.28/28.29 fof(f4397,plain,(
% 220.28/28.29 sQ52_spl|sQ176_spl|~sQ138_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f4384,f1054,f2600,f2174])).
% 220.28/28.29 fof(f4409,plain,(
% 220.28/28.29 conditionhyper(sK10_skl(n0))|~sQ196_spl|~sQ20_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f2839,f1029])).
% 220.28/28.29 fof(f4425,plain,(
% 220.28/28.29 ~gt(n0,sK10_skl(n0))|~sQ196_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f231,f2839])).
% 220.28/28.29 fof(f4431,plain,(
% 220.28/28.29 ![X0]: (uptakelg(X0)|conditionhyper(X0)|~sQ176_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2601,f169])).
% 220.28/28.29 fof(f4444,plain,(
% 220.28/28.29 sQ34_spl|~sQ176_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f4431,f788,f2600])).
% 220.28/28.29 fof(f4449,definition,(
% 220.28/28.29 ![X1]: (sQ377_spl <=> (drugbg(X1)|gt(n0,X1)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f4450,plain,(
% 220.28/28.29 ![X0]: (drugbg(X0)|gt(n0,X0)|~sQ377_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f4449])).
% 220.28/28.29 fof(f4460,plain,(
% 220.28/28.29 gt(n0,sK12_skl(n0))|~s1(sK12_skl(n0))|~sQ233_spl|~sQ225_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f3660,f171])).
% 220.28/28.29 fof(f4461,plain,(
% 220.28/28.29 sQ221_spl|~sQ223_spl|~sQ233_spl|~sQ225_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f4460,f3026,f3038,f3124,f3049])).
% 220.28/28.29 fof(f4627,plain,(
% 220.28/28.29 conditionnormo(sK7_skl(n0))|~sQ128_spl|~sQ23_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f4043,f687])).
% 220.28/28.29 fof(f4630,plain,(
% 220.28/28.29 $false|~sQ128_spl|~sQ23_spl),
% 220.28/28.29 inference(forward_subsumption_resolution,[status(thm)],[f4627,f4044])).
% 220.28/28.29 fof(f4631,plain,(
% 220.28/28.29 ~sQ128_spl|~sQ23_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f4630])).
% 220.28/28.29 fof(f4696,definition,(
% 220.28/28.29 sQ403_spl <=> (bcapacitysn(n0))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ403_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f4698,plain,(
% 220.28/28.29 ~bcapacitysn(n0)|sQ403_spl),
% 220.28/28.29 inference(component_clause,[status(thm)],[f4696])).
% 220.28/28.29 fof(f4707,plain,(
% 220.28/28.29 $false|~sQ152_spl|sQ403_spl),
% 220.28/28.29 inference(forward_subsumption_resolution,[status(thm)],[f4698,f2355])).
% 220.28/28.29 fof(f4708,plain,(
% 220.28/28.29 ~sQ152_spl|sQ403_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f4707])).
% 220.28/28.29 fof(f4786,plain,(
% 220.28/28.29 drugsu(n0)|~sQ361_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f4244,f43])).
% 220.28/28.29 fof(f4803,plain,(
% 220.28/28.29 sQ2_spl|~sQ361_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f4786,f323,f4243])).
% 220.28/28.29 fof(f5225,plain,(
% 220.28/28.29 conditionnormo(sK10_skl(n0))|~sQ196_spl|~sQ23_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f4425,f687])).
% 220.28/28.29 fof(f5242,plain,(
% 220.28/28.29 ~conditionhyper(sK10_skl(n0))|~sQ196_spl|~sQ23_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f5225,f53])).
% 220.28/28.29 fof(f5243,plain,(
% 220.28/28.29 $false|~sQ20_spl|~sQ196_spl|~sQ23_spl),
% 220.28/28.29 inference(forward_subsumption_resolution,[status(thm)],[f5242,f4409])).
% 220.28/28.29 fof(f5244,plain,(
% 220.28/28.29 ~sQ20_spl|~sQ196_spl|~sQ23_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f5243])).
% 220.28/28.29 fof(f5277,plain,(
% 220.28/28.29 drugbg(n0)|~sQ377_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f4450,f43])).
% 220.28/28.29 fof(f5303,plain,(
% 220.28/28.29 sQ6_spl|~sQ377_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f5277,f347,f4449])).
% 220.28/28.29 fof(f5394,plain,(
% 220.28/28.29 ![X0]: (sP6_prd(n0)|gt(n0,X0)|uptakelg(X0)|sQ128_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2010,f108])).
% 220.28/28.29 fof(f5399,plain,(
% 220.28/28.29 sQ129_spl|sQ176_spl|sQ128_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f5394,f2011,f2600,f2008])).
% 220.28/28.29 fof(f5409,plain,(
% 220.28/28.29 ![X0]: (bsecretioni(X0)|conditionhyper(X0)|~sQ152_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2352,f169])).
% 220.28/28.29 fof(f5413,plain,(
% 220.28/28.29 ![X0]: (bsecretioni(sK2_skl(n0))|gt(n0,X0)|~releaselg(X0)|~sQ152_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2352,f70])).
% 220.28/28.29 fof(f5417,plain,(
% 220.28/28.29 ![X0,X1]: (bsecretioni(X0)|releaselg(sK11_skl(X0))|drugbg(X1)|gt(n0,X1)|~sQ152_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2352,f2922])).
% 220.28/28.29 fof(f5420,plain,(
% 220.28/28.29 ![X0,X1]: (bsecretioni(X0)|sP7_prd(sK10_skl(X0),X0)|drugsu(X1)|gt(n0,X1)|~sQ152_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2352,f2834])).
% 220.28/28.29 fof(f5423,plain,(
% 220.28/28.29 ![X0,X1]: (bsecretioni(X0)|sP5_prd(sK7_skl(X0),X0)|sP6_prd(X0)|uptakelg(X1)|gt(n0,X1)|~sQ152_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2352,f2002])).
% 220.28/28.29 fof(f5424,plain,(
% 220.28/28.29 ![X0,X1]: (bsecretioni(X0)|sP4_prd(X0)|uptakelg(X1)|gt(n0,X1)|~sQ152_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2352,f1047])).
% 220.28/28.29 fof(f5427,plain,(
% 220.28/28.29 sQ20_spl|~sQ152_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f5409,f642,f2344])).
% 220.28/28.29 fof(f5437,definition,(
% 220.28/28.29 sQ474_spl <=> (bsecretioni(sK2_skl(n0)))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ474_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f5440,plain,(
% 220.28/28.29 sQ474_spl|sQ135_spl|~sQ152_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f5413,f5437,f2164,f2344])).
% 220.28/28.29 fof(f5444,plain,(
% 220.28/28.29 sQ215_spl|sQ377_spl|~sQ152_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f5417,f2956,f4449,f2344])).
% 220.28/28.29 fof(f5447,plain,(
% 220.28/28.29 sQ204_spl|sQ361_spl|~sQ152_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f5420,f2868,f4243,f2344])).
% 220.28/28.29 fof(f5450,plain,(
% 220.28/28.29 sQ131_spl|sQ176_spl|~sQ152_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f5423,f2020,f2600,f2344])).
% 220.28/28.29 fof(f5451,plain,(
% 220.28/28.29 sQ52_spl|sQ176_spl|~sQ152_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f5424,f1054,f2600,f2344])).
% 220.28/28.29 fof(f5454,plain,(
% 220.28/28.29 ![X0]: (gt(n0,X0)|~releaselg(X0)|~sQ153_spl)),
% 220.28/28.29 inference(resolution,[status(thm)],[f2348,f276])).
% 220.28/28.29 fof(f5467,plain,(
% 220.28/28.29 sQ20_spl|~sQ138_spl),
% 220.28/28.29 inference(split_clause,[status(thm)],[f4376,f642,f2174])).
% 220.28/28.29 fof(f5513,definition,(
% 220.28/28.29 ![X0]: (sQ476_spl <=> (gt(X0,sK12_skl(n0))))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ476_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f5514,plain,(
% 220.28/28.29 ![X0]: (gt(X0,sK12_skl(n0))|~sQ476_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f5513])).
% 220.28/28.29 fof(f5724,plain,(
% 220.28/28.29 $false|~sQ476_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f5514,f43])).
% 220.28/28.29 fof(f5746,plain,(
% 220.28/28.29 ~sQ476_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f5724])).
% 220.28/28.29 fof(f5784,definition,(
% 220.28/28.29 ![X0]: (sQ486_spl <=> (gt(X0,sK30_skl(n0))))),
% 220.28/28.29 introduced(definition,[new_symbols(definition,[sQ486_spl])],[split_symbol_definition])).
% 220.28/28.29 fof(f5785,plain,(
% 220.28/28.29 ![X0]: (gt(X0,sK30_skl(n0))|~sQ486_spl)),
% 220.28/28.29 inference(component_clause,[status(thm)],[f5784])).
% 220.28/28.29 fof(f5808,plain,(
% 220.28/28.29 $false|~sQ486_spl),
% 220.28/28.29 inference(resolution,[status(thm)],[f5785,f43])).
% 220.28/28.29 fof(f5847,plain,(
% 220.28/28.29 ~sQ486_spl),
% 220.28/28.29 inference(contradiction_clause,[status(thm)],[f5808])).
% 220.28/28.30 fof(f5987,definition,(
% 220.28/28.30 ![X0]: (sQ513_spl <=> (gt(X0,sK16_skl(n0))))),
% 220.28/28.30 introduced(definition,[new_symbols(definition,[sQ513_spl])],[split_symbol_definition])).
% 220.28/28.30 fof(f5988,plain,(
% 220.28/28.30 ![X0]: (gt(X0,sK16_skl(n0))|~sQ513_spl)),
% 220.28/28.30 inference(component_clause,[status(thm)],[f5987])).
% 220.28/28.30 fof(f6010,plain,(
% 220.28/28.30 $false|~sQ513_spl),
% 220.28/28.30 inference(resolution,[status(thm)],[f5988,f43])).
% 220.28/28.30 fof(f6053,plain,(
% 220.28/28.30 ~sQ513_spl),
% 220.28/28.30 inference(contradiction_clause,[status(thm)],[f6010])).
% 220.28/28.30 fof(f6239,definition,(
% 220.28/28.30 ![X0]: (sQ547_spl <=> (gt(X0,sK17_skl(n0))))),
% 220.28/28.30 introduced(definition,[new_symbols(definition,[sQ547_spl])],[split_symbol_definition])).
% 220.28/28.30 fof(f6240,plain,(
% 220.28/28.30 ![X0]: (gt(X0,sK17_skl(n0))|~sQ547_spl)),
% 220.28/28.30 inference(component_clause,[status(thm)],[f6239])).
% 220.28/28.30 fof(f6268,plain,(
% 220.28/28.30 $false|~sQ547_spl),
% 220.28/28.30 inference(resolution,[status(thm)],[f6240,f43])).
% 220.28/28.30 fof(f6319,plain,(
% 220.28/28.30 ~sQ547_spl),
% 220.28/28.30 inference(contradiction_clause,[status(thm)],[f6268])).
% 220.28/28.30 fof(f6421,plain,(
% 220.28/28.30 ![X0]: (gt(n0,X0)|uptakelg(X0)|~sQ135_spl)),
% 220.28/28.30 inference(resolution,[status(thm)],[f2165,f621])).
% 220.28/28.30 fof(f6422,plain,(
% 220.28/28.30 sQ176_spl|~sQ135_spl),
% 220.28/28.30 inference(split_clause,[status(thm)],[f6421,f2600,f2164])).
% 220.28/28.30 fof(f6423,plain,(
% 220.28/28.30 sQ135_spl|~sQ153_spl),
% 220.28/28.30 inference(split_clause,[status(thm)],[f5454,f2164,f2347])).
% 220.28/28.30 fof(f6426,plain,(
% 220.28/28.30 sQ138_spl|~sQ133_spl),
% 220.28/28.30 inference(split_clause,[status(thm)],[f2074,f2174,f2070])).
% 220.28/28.30 fof(f6906,plain,(
% 220.28/28.30 ~conditionnormo(sK11_skl(n0))|sQ219_spl|~sQ34_spl),
% 220.28/28.30 inference(resolution,[status(thm)],[f53,f3057])).
% 220.28/28.30 fof(f6953,definition,(
% 220.28/28.30 ![X0]: (sQ612_spl <=> (gt(X0,sK27_skl(n0))))),
% 220.28/28.30 introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition])).
% 220.28/28.30 fof(f6954,plain,(
% 220.28/28.30 ![X0]: (gt(X0,sK27_skl(n0))|~sQ612_spl)),
% 220.28/28.30 inference(component_clause,[status(thm)],[f6953])).
% 220.28/28.30 fof(f6973,plain,(
% 220.28/28.30 $false|~sQ612_spl),
% 220.28/28.30 inference(resolution,[status(thm)],[f6954,f43])).
% 220.28/28.30 fof(f7000,plain,(
% 220.28/28.30 ~sQ612_spl),
% 220.28/28.30 inference(contradiction_clause,[status(thm)],[f6973])).
% 220.28/28.30 fof(f7396,plain,(
% 220.28/28.30 ~bcapacitysn(n0)|~sQ137_spl),
% 220.28/28.30 inference(resolution,[status(thm)],[f2172,f50])).
% 220.28/28.30 fof(f7404,plain,(
% 220.28/28.30 ~sQ403_spl|~sQ137_spl),
% 220.28/28.30 inference(split_clause,[status(thm)],[f7396,f4696,f2171])).
% 220.28/28.30 fof(f7646,plain,(
% 220.28/28.30 ![X0]: (gt(n0,X0)|drugbg(X0)|conditionnormo(sK11_skl(n0))|~sQ23_spl)),
% 220.28/28.30 inference(resolution,[status(thm)],[f147,f687])).
% 220.28/28.30 fof(f7654,definition,(
% 220.28/28.30 sQ689_spl <=> (conditionnormo(sK11_skl(n0)))),
% 220.28/28.30 introduced(definition,[new_symbols(definition,[sQ689_spl])],[split_symbol_definition])).
% 220.28/28.30 fof(f7655,plain,(
% 220.28/28.30 conditionnormo(sK11_skl(n0))|~sQ689_spl),
% 220.28/28.30 inference(component_clause,[status(thm)],[f7654])).
% 220.28/28.30 fof(f7657,plain,(
% 220.28/28.30 sQ377_spl|sQ689_spl|~sQ23_spl),
% 220.28/28.30 inference(split_clause,[status(thm)],[f7646,f4449,f7654,f686])).
% 220.28/28.30 fof(f7658,plain,(
% 220.28/28.30 $false|sQ219_spl|~sQ34_spl|~sQ689_spl),
% 220.28/28.30 inference(forward_subsumption_resolution,[status(thm)],[f7655,f6906])).
% 220.28/28.30 fof(f7659,plain,(
% 220.28/28.30 sQ219_spl|~sQ34_spl|~sQ689_spl),
% 220.28/28.30 inference(contradiction_clause,[status(thm)],[f7658])).
% 220.28/28.30 fof(f7660,plain,(
% 220.28/28.30 $false),
% 220.28/28.30 inference(sat_refutation,[status(thm)],[f339,f953,f1261,f1531,f1817,f1971,f2062,f2073,f2199,f2350,f2685,f2704,f2711,f2715,f2716,f2798,f2848,f2988,f2998,f3029,f3030,f3041,f3052,f3127,f3395,f3420,f3528,f3589,f4019,f4393,f4396,f4397,f4444,f4461,f4631,f4708,f4803,f5244,f5303,f5399,f5427,f5440,f5444,f5447,f5450,f5451,f5467,f5746,f5847,f6053,f6319,f6422,f6423,f6426,f7000,f7404,f7657,f7659])).
% 220.28/28.30 % SZS output end CNFRefutation for theBenchmark.p
% 165.70/28.38 % Elapsed time: 27.946735 seconds
% 165.70/28.38 % CPU time: 221.485728 seconds
% 165.70/28.38 % Total memory used: 449.162 MB
% 165.70/28.38 % Net memory used: 400.463 MB
%------------------------------------------------------------------------------