%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MED010+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 : n006.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:58 PM UTC 2026
% Result : Theorem 56.08s 12.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED010+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.12/5.41 % Computer : n006.cluster.edu
% 0.12/5.41 % Model : x86_64 x86_64
% 0.12/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.41 % Memory : 8046.5625MB
% 0.12/5.41 % OS : Linux 6.8.0-71-generic
% 0.12/5.41 % CPULimit : 300
% 0.12/5.41 % WCLimit : 300
% 0.12/5.41 % DateTime : Mon Sep 21 01:19:49 UTC 2026
% 0.12/5.41 % CPUTime :
% 0.12/5.42 % Drodi V4.1.1
% 56.08/12.72 % Refutation found
% 56.08/12.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 56.08/12.72 % SZS output start CNFRefutation for theBenchmark
% 56.08/12.72 fof(f1,axiom,(
% 56.08/12.72 (! [X] : ~ gt(X,X) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f6,axiom,(
% 56.08/12.72 (! [X0] :( ~ bcapacityex(X0)| ~ bcapacitysn(X0) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f7,axiom,(
% 56.08/12.72 (! [X0] :( conditionhyper(X0)| conditionhypo(X0)| conditionnormo(X0) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f8,axiom,(
% 56.08/12.72 (! [X0] :( ~ conditionhyper(X0)| ~ conditionhypo(X0) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f9,axiom,(
% 56.08/12.72 (! [X0] :( ~ conditionhyper(X0)| ~ conditionnormo(X0) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f11,axiom,(
% 56.08/12.72 (! [X0] :( (! [X1] :( ~ gt(X0,X1)=> drugi(X1) ))=> (! [X1] :( ~ gt(X0,X1)=> ( uptakelg(X1)& uptakepg(X1) ) ) )) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f14,axiom,(
% 56.08/12.72 (! [X0] :( (! [X1] :( ~ gt(X0,X1)=> drugbg(X1) ))=> (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ) )) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f23,axiom,(
% 56.08/12.72 (! [X0] :( ~ s1(X0)| ~ s2(X0) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f25,axiom,(
% 56.08/12.72 (! [X0] :( ~ s2(X0)| ~ s3(X0) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f26,axiom,(
% 56.08/12.72 (! [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) ) )) ) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f30,axiom,(
% 56.08/12.72 (! [X0] :( s3(X0)=> ( ( drugi(X0)& ( drugsu(X0)| drugbg(X0) ) )| drugi(X0) ) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f33,axiom,(
% 56.08/12.72 (! [X0] :( drugi(X0)=> s3(X0) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f34,axiom,(
% 56.08/12.72 (! [X0] :( ( (! [X1] :( ~ gt(X0,X1)=> uptakelg(X1) ))| (! [X1] :( ~ gt(X0,X1)=> uptakepg(X1) ) ))=> (! [X1] :( ~ gt(X0,X1)=> drugi(X1) ) )) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f35,axiom,(
% 56.08/12.72 (! [X0,X1] :( ~ gt(X0,X1)=> ( ~ releaselg(X1)=> uptakelg(X1) ) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f36,axiom,(
% 56.08/12.72 (! [X0] :( (! [X1] :( ~ gt(X0,X1)=> bsecretioni(X1) ))=> ( (! [X1] :( ~ gt(X0,X1)=> drugsu(X1) ))& ~ bcapacityex(X0) ) ) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f40,axiom,(
% 56.08/12.72 (! [X0] :( ( s2(X0)& ~ (! [X1] :( ~ gt(X0,X1)=> conditionnormo(X1) ) ))=> (? [X1] :( ~ gt(X0,X1)& s3(X1)& (! [X2] :( gt(X1,X2)=> conditionhyper(X2) ))& bcapacityex(X1) ) )) )),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f41,conjecture,(
% 56.08/12.72 ( ( s2(n0)& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ))& bcapacityex(n0) )=> (? [X0] :( ~ gt(n0,X0)& s3(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ))& bcapacityex(X0) ) )) ),
% 56.08/12.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 56.08/12.72 fof(f42,negated_conjecture,(
% 56.08/12.72 ~(( ( s2(n0)& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ))& bcapacityex(n0) )=> (? [X0] :( ~ gt(n0,X0)& s3(X0)& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ))& bcapacityex(X0) ) )) )),
% 56.08/12.72 inference(negated_conjecture,[status(cth)],[f41])).
% 56.08/12.72 fof(f43,plain,(
% 56.08/12.72 ![X0]: (~gt(X0,X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f1])).
% 56.08/12.72 fof(f50,plain,(
% 56.08/12.72 ![X0]: (~bcapacityex(X0)|~bcapacitysn(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f6])).
% 56.08/12.72 fof(f51,plain,(
% 56.08/12.72 ![X0]: (conditionhyper(X0)|conditionhypo(X0)|conditionnormo(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f7])).
% 56.08/12.72 fof(f52,plain,(
% 56.08/12.72 ![X0]: (~conditionhyper(X0)|~conditionhypo(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f8])).
% 56.08/12.72 fof(f53,plain,(
% 56.08/12.72 ![X0]: (~conditionhyper(X0)|~conditionnormo(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f9])).
% 56.08/12.72 fof(f55,plain,(
% 56.08/12.72 ![X0]: ((?[X1]: (~gt(X0,X1)&~drugi(X1)))|(![X1]: (gt(X0,X1)|(uptakelg(X1)&uptakepg(X1)))))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 56.08/12.72 fof(f56,definition,(
% 56.08/12.72 ![X1]: (sP0_prd(X1)<=>(uptakelg(X1)&uptakepg(X1)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 56.08/12.72 fof(f57,plain,(
% 56.08/12.72 ![X0]: ((?[X1]: (~gt(X0,X1)&~drugi(X1)))|(![X1]: (gt(X0,X1)|sP0_prd(X1))))),
% 56.08/12.72 inference(formula_renaming,[status(thm)],[f55,f56])).
% 56.08/12.72 fof(f58,plain,(
% 56.08/12.72 ![X0]: ((~gt(X0,sK0_skl(X0))&~drugi(sK0_skl(X0)))|(![X1]: (gt(X0,X1)|sP0_prd(X1))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X1,sK0_skl(X0))],[f57])).
% 56.08/12.72 fof(f60,plain,(
% 56.08/12.72 ![X0,X1]: (~drugi(sK0_skl(X0))|gt(X0,X1)|sP0_prd(X1))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f58])).
% 56.08/12.72 fof(f68,plain,(
% 56.08/12.72 ![X0]: ((?[X1]: (~gt(X0,X1)&~drugbg(X1)))|(![X1]: (gt(X0,X1)|~releaselg(X1))))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 56.08/12.72 fof(f69,plain,(
% 56.08/12.72 ![X0]: ((~gt(X0,sK2_skl(X0))&~drugbg(sK2_skl(X0)))|(![X1]: (gt(X0,X1)|~releaselg(X1))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X1,sK2_skl(X0))],[f68])).
% 56.08/12.72 fof(f71,plain,(
% 56.08/12.72 ![X0,X1]: (~drugbg(sK2_skl(X0))|gt(X0,X1)|~releaselg(X1))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f69])).
% 56.08/12.72 fof(f100,plain,(
% 56.08/12.72 ![X0]: (~s1(X0)|~s2(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f23])).
% 56.08/12.72 fof(f102,plain,(
% 56.08/12.72 ![X0]: (~s2(X0)|~s3(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f25])).
% 56.08/12.72 fof(f103,plain,(
% 56.08/12.72 ![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))))))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 56.08/12.72 fof(f104,definition,(
% 56.08/12.72 ![X0,X1]: (sP5_prd(X1,X0)<=>(~gt(X0,X1)&~conditionnormo(X1)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 56.08/12.72 fof(f105,definition,(
% 56.08/12.72 ![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))))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 56.08/12.72 fof(f106,plain,(
% 56.08/12.72 ![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))))))),
% 56.08/12.72 inference(formula_renaming,[status(thm)],[f103,f105,f104])).
% 56.08/12.72 fof(f107,plain,(
% 56.08/12.72 ![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))))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X1,sK7_skl(X0))],[f106])).
% 56.08/12.72 fof(f109,plain,(
% 56.08/12.72 ![X0,X1]: (sP5_prd(sK7_skl(X0),X0)|sP6_prd(X0)|gt(X0,X1)|uptakepg(X1))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f107])).
% 56.08/12.72 fof(f119,plain,(
% 56.08/12.72 ![X0]: (~s3(X0)|((drugi(X0)&(drugsu(X0)|drugbg(X0)))|drugi(X0)))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 56.08/12.72 fof(f120,plain,(
% 56.08/12.72 ![X0]: (~s3(X0)|drugi(X0)|drugi(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f119])).
% 56.08/12.72 fof(f128,plain,(
% 56.08/12.72 ![X0]: (~drugi(X0)|s3(X0))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 56.08/12.72 fof(f129,plain,(
% 56.08/12.72 ![X0]: (~drugi(X0)|s3(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f128])).
% 56.08/12.72 fof(f130,plain,(
% 56.08/12.72 ![X0]: (((?[X1]: (~gt(X0,X1)&~uptakelg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|(![X1]: (gt(X0,X1)|drugi(X1))))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 56.08/12.72 fof(f131,plain,(
% 56.08/12.72 ![X0]: (((~gt(X0,sK8_skl(X0))&~uptakelg(sK8_skl(X0)))&(~gt(X0,sK9_skl(X0))&~uptakepg(sK9_skl(X0))))|(![X1]: (gt(X0,X1)|drugi(X1))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(X1,sK8_skl(X0)),skolemize(X1,sK9_skl(X0))],[f130])).
% 56.08/12.72 fof(f132,plain,(
% 56.08/12.72 ![X0,X1]: (~gt(X0,sK8_skl(X0))|gt(X0,X1)|drugi(X1))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f131])).
% 56.08/12.72 fof(f133,plain,(
% 56.08/12.72 ![X0,X1]: (~uptakelg(sK8_skl(X0))|gt(X0,X1)|drugi(X1))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f131])).
% 56.08/12.72 fof(f134,plain,(
% 56.08/12.72 ![X0,X1]: (~gt(X0,sK9_skl(X0))|gt(X0,X1)|drugi(X1))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f131])).
% 56.08/12.72 fof(f135,plain,(
% 56.08/12.72 ![X0,X1]: (~uptakepg(sK9_skl(X0))|gt(X0,X1)|drugi(X1))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f131])).
% 56.08/12.72 fof(f136,plain,(
% 56.08/12.72 ![X0,X1]: (gt(X0,X1)|(releaselg(X1)|uptakelg(X1)))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 56.08/12.72 fof(f137,plain,(
% 56.08/12.72 ![X1]: ((![X0]: gt(X0,X1))|(releaselg(X1)|uptakelg(X1)))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f136])).
% 56.08/12.72 fof(f138,plain,(
% 56.08/12.72 ![X0,X1]: (gt(X0,X1)|releaselg(X1)|uptakelg(X1))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f137])).
% 56.08/12.72 fof(f139,plain,(
% 56.08/12.72 ![X0]: ((?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))|((![X1]: (gt(X0,X1)|drugsu(X1)))&~bcapacityex(X0)))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 56.08/12.72 fof(f140,definition,(
% 56.08/12.72 ![X0,X1]: (sP7_prd(X1,X0)<=>(~gt(X0,X1)&~bsecretioni(X1)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 56.08/12.72 fof(f141,plain,(
% 56.08/12.72 ![X0]: ((?[X1]: sP7_prd(X1,X0))|((![X1]: (gt(X0,X1)|drugsu(X1)))&~bcapacityex(X0)))),
% 56.08/12.72 inference(formula_renaming,[status(thm)],[f139,f140])).
% 56.08/12.72 fof(f142,plain,(
% 56.08/12.72 ![X0]: (sP7_prd(sK10_skl(X0),X0)|((![X1]: (gt(X0,X1)|drugsu(X1)))&~bcapacityex(X0)))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X1,sK10_skl(X0))],[f141])).
% 56.08/12.72 fof(f144,plain,(
% 56.08/12.72 ![X0]: (sP7_prd(sK10_skl(X0),X0)|~bcapacityex(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f142])).
% 56.08/12.72 fof(f160,plain,(
% 56.08/12.72 ![X0]: ((~s2(X0)|(![X1]: (gt(X0,X1)|conditionnormo(X1))))|(?[X1]: (((~gt(X0,X1)&s3(X1))&(![X2]: (~gt(X1,X2)|conditionhyper(X2))))&bcapacityex(X1))))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 56.08/12.72 fof(f161,plain,(
% 56.08/12.72 ![X0]: ((~s2(X0)|(![X1]: (gt(X0,X1)|conditionnormo(X1))))|(((~gt(X0,sK14_skl(X0))&s3(sK14_skl(X0)))&(![X2]: (~gt(sK14_skl(X0),X2)|conditionhyper(X2))))&bcapacityex(sK14_skl(X0))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X1,sK14_skl(X0))],[f160])).
% 56.08/12.72 fof(f162,plain,(
% 56.08/12.72 ![X0,X1]: (~s2(X0)|gt(X0,X1)|conditionnormo(X1)|~gt(X0,sK14_skl(X0)))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f161])).
% 56.08/12.72 fof(f163,plain,(
% 56.08/12.72 ![X0,X1]: (~s2(X0)|gt(X0,X1)|conditionnormo(X1)|s3(sK14_skl(X0)))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f161])).
% 56.08/12.72 fof(f164,plain,(
% 56.08/12.72 ![X0,X1,X2]: (~s2(X0)|gt(X0,X1)|conditionnormo(X1)|~gt(sK14_skl(X0),X2)|conditionhyper(X2))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f161])).
% 56.08/12.72 fof(f165,plain,(
% 56.08/12.72 ![X0,X1]: (~s2(X0)|gt(X0,X1)|conditionnormo(X1)|bcapacityex(sK14_skl(X0)))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f161])).
% 56.08/12.72 fof(f166,plain,(
% 56.08/12.72 (((s2(n0)&(![X0]: (~gt(n0,X0)|conditionhyper(X0))))&bcapacityex(n0))&(![X0]: (((gt(n0,X0)|~s3(X0))|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))|~bcapacityex(X0))))),
% 56.08/12.72 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 56.08/12.72 fof(f167,plain,(
% 56.08/12.72 ((s2(n0)&(![X0]: (~gt(n0,X0)|conditionhyper(X0))))&bcapacityex(n0))&(![X0]: (((gt(n0,X0)|~s3(X0))|(gt(X0,sK15_skl(X0))&~conditionhyper(sK15_skl(X0))))|~bcapacityex(X0)))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X1,sK15_skl(X0))],[f166])).
% 56.08/12.72 fof(f168,plain,(
% 56.08/12.72 s2(n0)),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f167])).
% 56.08/12.72 fof(f169,plain,(
% 56.08/12.72 ![X0]: (~gt(n0,X0)|conditionhyper(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f167])).
% 56.08/12.72 fof(f170,plain,(
% 56.08/12.72 bcapacityex(n0)),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f167])).
% 56.08/12.72 fof(f171,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|~s3(X0)|gt(X0,sK15_skl(X0))|~bcapacityex(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f167])).
% 56.08/12.72 fof(f172,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|~s3(X0)|~conditionhyper(sK15_skl(X0))|~bcapacityex(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f167])).
% 56.08/12.72 fof(f173,plain,(
% 56.08/12.72 ![X1]: ((~sP0_prd(X1)|(uptakelg(X1)&uptakepg(X1)))&(sP0_prd(X1)|(~uptakelg(X1)|~uptakepg(X1))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f56])).
% 56.08/12.72 fof(f174,plain,(
% 56.08/12.72 (![X1]: (~sP0_prd(X1)|(uptakelg(X1)&uptakepg(X1))))&(![X1]: (sP0_prd(X1)|(~uptakelg(X1)|~uptakepg(X1))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f173])).
% 56.08/12.72 fof(f175,plain,(
% 56.08/12.72 ![X0]: (~sP0_prd(X0)|uptakelg(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f174])).
% 56.08/12.72 fof(f213,plain,(
% 56.08/12.72 ![X0,X1]: ((~sP5_prd(X1,X0)|(~gt(X0,X1)&~conditionnormo(X1)))&(sP5_prd(X1,X0)|(gt(X0,X1)|conditionnormo(X1))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f104])).
% 56.08/12.72 fof(f214,plain,(
% 56.08/12.72 (![X0,X1]: (~sP5_prd(X1,X0)|(~gt(X0,X1)&~conditionnormo(X1))))&(![X0,X1]: (sP5_prd(X1,X0)|(gt(X0,X1)|conditionnormo(X1))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f213])).
% 56.08/12.72 fof(f215,plain,(
% 56.08/12.72 ![X0,X1]: (~sP5_prd(X0,X1)|~gt(X1,X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f214])).
% 56.08/12.72 fof(f216,plain,(
% 56.08/12.72 ![X0,X1]: (~sP5_prd(X0,X1)|~conditionnormo(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f214])).
% 56.08/12.72 fof(f218,definition,(
% 56.08/12.72 ![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))))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 56.08/12.72 fof(f219,plain,(
% 56.08/12.72 ![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))))))),
% 56.08/12.72 inference(formula_renaming,[status(thm)],[f105,f218])).
% 56.08/12.72 fof(f220,definition,(
% 56.08/12.72 ![X0]: (sP10_prd(X0)<=>((((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))&(![X1]: (gt(X0,X1)|bsecretioni(X1)))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 56.08/12.72 fof(f221,plain,(
% 56.08/12.72 ![X0]: (sP6_prd(X0)<=>(sP9_prd(X0)|(sP10_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 56.08/12.72 inference(formula_renaming,[status(thm)],[f219,f220])).
% 56.08/12.72 fof(f222,plain,(
% 56.08/12.72 ![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)))))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f221])).
% 56.08/12.72 fof(f223,plain,(
% 56.08/12.72 (![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)))))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f222])).
% 56.08/12.72 fof(f224,plain,(
% 56.08/12.72 (![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)))))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(X1,sK21_skl(X0))],[f223])).
% 56.08/12.72 fof(f225,plain,(
% 56.08/12.72 ![X0]: (~sP6_prd(X0)|sP9_prd(X0)|sP10_prd(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f224])).
% 56.08/12.72 fof(f230,plain,(
% 56.08/12.72 ![X0,X1]: ((~sP7_prd(X1,X0)|(~gt(X0,X1)&~bsecretioni(X1)))&(sP7_prd(X1,X0)|(gt(X0,X1)|bsecretioni(X1))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f140])).
% 56.08/12.72 fof(f231,plain,(
% 56.08/12.72 (![X0,X1]: (~sP7_prd(X1,X0)|(~gt(X0,X1)&~bsecretioni(X1))))&(![X0,X1]: (sP7_prd(X1,X0)|(gt(X0,X1)|bsecretioni(X1))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f230])).
% 56.08/12.72 fof(f232,plain,(
% 56.08/12.72 ![X0,X1]: (~sP7_prd(X0,X1)|~gt(X1,X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f231])).
% 56.08/12.72 fof(f244,definition,(
% 56.08/12.72 ![X0]: (sP11_prd(X0)<=>((((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 56.08/12.72 fof(f245,plain,(
% 56.08/12.72 ![X0]: (sP9_prd(X0)<=>(sP11_prd(X0)|((((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 56.08/12.72 inference(formula_renaming,[status(thm)],[f218,f244])).
% 56.08/12.72 fof(f246,definition,(
% 56.08/12.72 ![X0]: (sP12_prd(X0)<=>(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 56.08/12.72 fof(f247,plain,(
% 56.08/12.72 ![X0]: (sP9_prd(X0)<=>(sP11_prd(X0)|(sP12_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 56.08/12.72 inference(formula_renaming,[status(thm)],[f245,f246])).
% 56.08/12.72 fof(f248,plain,(
% 56.08/12.72 ![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)))))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f247])).
% 56.08/12.72 fof(f249,plain,(
% 56.08/12.72 (![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)))))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f248])).
% 56.08/12.72 fof(f250,plain,(
% 56.08/12.72 (![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)))))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(X1,sK24_skl(X0))],[f249])).
% 56.08/12.72 fof(f251,plain,(
% 56.08/12.72 ![X0]: (~sP9_prd(X0)|sP11_prd(X0)|sP12_prd(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f250])).
% 56.08/12.72 fof(f256,definition,(
% 56.08/12.72 ![X0]: (sP13_prd(X0)<=>(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 56.08/12.72 fof(f257,plain,(
% 56.08/12.72 ![X0]: (sP10_prd(X0)<=>(sP13_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1)))))),
% 56.08/12.72 inference(formula_renaming,[status(thm)],[f220,f256])).
% 56.08/12.72 fof(f258,plain,(
% 56.08/12.72 ![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))))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f257])).
% 56.08/12.72 fof(f259,plain,(
% 56.08/12.72 (![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))))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f258])).
% 56.08/12.72 fof(f260,plain,(
% 56.08/12.72 (![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))))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(X1,sK25_skl(X0))],[f259])).
% 56.08/12.72 fof(f261,plain,(
% 56.08/12.72 ![X0]: (~sP10_prd(X0)|sP13_prd(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f260])).
% 56.08/12.72 fof(f265,definition,(
% 56.08/12.72 ![X0]: (sP14_prd(X0)<=>(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 56.08/12.72 fof(f266,plain,(
% 56.08/12.72 ![X0]: (sP11_prd(X0)<=>(sP14_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))),
% 56.08/12.72 inference(formula_renaming,[status(thm)],[f244,f265])).
% 56.08/12.72 fof(f267,plain,(
% 56.08/12.72 ![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))))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f266])).
% 56.08/12.72 fof(f268,plain,(
% 56.08/12.72 (![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))))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f267])).
% 56.08/12.72 fof(f269,plain,(
% 56.08/12.72 (![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))))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(X1,sK26_skl(X0))],[f268])).
% 56.08/12.72 fof(f270,plain,(
% 56.08/12.72 ![X0]: (~sP11_prd(X0)|sP14_prd(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f269])).
% 56.08/12.72 fof(f274,plain,(
% 56.08/12.72 ![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))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f246])).
% 56.08/12.72 fof(f275,plain,(
% 56.08/12.72 (![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))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f274])).
% 56.08/12.72 fof(f276,plain,(
% 56.08/12.72 (![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))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(X1,sK27_skl(X0))],[f275])).
% 56.08/12.72 fof(f278,plain,(
% 56.08/12.72 ![X0]: (~sP12_prd(X0)|bcapacitysn(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f276])).
% 56.08/12.72 fof(f282,plain,(
% 56.08/12.72 ![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))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f256])).
% 56.08/12.72 fof(f283,plain,(
% 56.08/12.72 (![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))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f282])).
% 56.08/12.72 fof(f284,plain,(
% 56.08/12.72 (![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))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl]),skolemize(X1,sK28_skl(X0)),skolemize(X1,sK29_skl(X0))],[f283])).
% 56.08/12.72 fof(f285,plain,(
% 56.08/12.72 ![X0,X1,X2]: (~sP13_prd(X0)|gt(X0,X1)|~releaselg(X1)|gt(X0,X2)|uptakepg(X2))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f284])).
% 56.08/12.72 fof(f291,plain,(
% 56.08/12.72 ![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))))),
% 56.08/12.72 inference(NNF_transformation,[status(thm)],[f265])).
% 56.08/12.72 fof(f292,plain,(
% 56.08/12.72 (![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))))),
% 56.08/12.72 inference(miniscoping,[status(thm)],[f291])).
% 56.08/12.72 fof(f293,plain,(
% 56.08/12.72 (![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))))),
% 56.08/12.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(X1,sK30_skl(X0))],[f292])).
% 56.08/12.72 fof(f295,plain,(
% 56.08/12.72 ![X0]: (~sP14_prd(X0)|bcapacitysn(X0))),
% 56.08/12.72 inference(cnf_transformation,[status(thm)],[f293])).
% 56.08/12.72 fof(f299,plain,(
% 56.08/12.72 ![X0]: (~s3(X0)|drugi(X0))),
% 56.08/12.72 inference(duplicate_literals_removal,[status(thm)],[f120])).
% 56.08/12.72 fof(f304,plain,(
% 56.08/12.72 ![X0]: (conditionhypo(sK15_skl(X0))|conditionnormo(sK15_skl(X0))|gt(n0,X0)|~s3(X0)|~bcapacityex(X0))),
% 56.08/12.72 inference(resolution,[status(thm)],[f51,f172])).
% 56.08/12.72 fof(f328,definition,(
% 56.08/12.72 ![X0]: (sQ3_spl <=> (gt(n0,X0)|conditionnormo(X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f329,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|conditionnormo(X0)|~sQ3_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f328])).
% 56.08/12.72 fof(f667,plain,(
% 56.08/12.72 ![X0]: (~bcapacityex(X0)|~gt(X0,sK10_skl(X0)))),
% 56.08/12.72 inference(resolution,[status(thm)],[f144,f232])).
% 56.08/12.72 fof(f670,plain,(
% 56.08/12.72 ~gt(n0,sK10_skl(n0))),
% 56.08/12.72 inference(resolution,[status(thm)],[f667,f170])).
% 56.08/12.72 fof(f696,plain,(
% 56.08/12.72 ![X0]: (releaselg(X0)|uptakelg(X0))),
% 56.08/12.72 inference(resolution,[status(thm)],[f138,f43])).
% 56.08/12.72 fof(f809,definition,(
% 56.08/12.72 ![X0]: (sQ48_spl <=> (gt(n0,X0)|drugi(X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f810,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|drugi(X0)|~sQ48_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f809])).
% 56.08/12.72 fof(f816,definition,(
% 56.08/12.72 ![X0]: (sQ50_spl <=> (gt(n0,X0)|~releaselg(X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f817,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|~releaselg(X0)|~sQ50_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f816])).
% 56.08/12.72 fof(f823,definition,(
% 56.08/12.72 sQ52_spl <=> (bcapacityex(n0))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f825,plain,(
% 56.08/12.72 ~bcapacityex(n0)|sQ52_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f823])).
% 56.08/12.72 fof(f833,definition,(
% 56.08/12.72 ![X0]: (sQ55_spl <=> (gt(n0,X0)|sP0_prd(X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f834,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|sP0_prd(X0)|~sQ55_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f833])).
% 56.08/12.72 fof(f851,plain,(
% 56.08/12.72 ![X0]: (sP0_prd(sK8_skl(n0))|gt(n0,X0)|drugi(X0)|~sQ55_spl)),
% 56.08/12.72 inference(resolution,[status(thm)],[f834,f132])).
% 56.08/12.72 fof(f857,definition,(
% 56.08/12.72 sQ56_spl <=> (sP0_prd(sK8_skl(n0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f858,plain,(
% 56.08/12.72 sP0_prd(sK8_skl(n0))|~sQ56_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f857])).
% 56.08/12.72 fof(f860,plain,(
% 56.08/12.72 sQ56_spl|sQ48_spl|~sQ55_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f851,f857,f809,f833])).
% 56.08/12.72 fof(f879,plain,(
% 56.08/12.72 uptakelg(sK8_skl(n0))|~sQ56_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f858,f175])).
% 56.08/12.72 fof(f886,definition,(
% 56.08/12.72 ![X0]: (sQ61_spl <=> (gt(X0,sK1_skl(n0))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f887,plain,(
% 56.08/12.72 ![X0]: (gt(X0,sK1_skl(n0))|~sQ61_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f886])).
% 56.08/12.72 fof(f901,definition,(
% 56.08/12.72 ![X0]: (sQ64_spl <=> (gt(X0,sK2_skl(n0))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f902,plain,(
% 56.08/12.72 ![X0]: (gt(X0,sK2_skl(n0))|~sQ64_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f901])).
% 56.08/12.72 fof(f908,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|drugi(X0)|~sQ56_spl)),
% 56.08/12.72 inference(resolution,[status(thm)],[f879,f133])).
% 56.08/12.72 fof(f915,definition,(
% 56.08/12.72 ![X0]: (sQ67_spl <=> (gt(X0,sK8_skl(n0))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f916,plain,(
% 56.08/12.72 ![X0]: (gt(X0,sK8_skl(n0))|~sQ67_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f915])).
% 56.08/12.72 fof(f918,definition,(
% 56.08/12.72 sQ68_spl <=> (releaselg(sK8_skl(n0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f920,plain,(
% 56.08/12.72 ~releaselg(sK8_skl(n0))|sQ68_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f918])).
% 56.08/12.72 fof(f939,plain,(
% 56.08/12.72 $false|~sQ61_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f887,f43])).
% 56.08/12.72 fof(f951,plain,(
% 56.08/12.72 ~sQ61_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f939])).
% 56.08/12.72 fof(f956,plain,(
% 56.08/12.72 $false|~sQ64_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f902,f43])).
% 56.08/12.72 fof(f967,plain,(
% 56.08/12.72 ~sQ64_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f956])).
% 56.08/12.72 fof(f972,plain,(
% 56.08/12.72 $false|~sQ67_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f916,f43])).
% 56.08/12.72 fof(f979,definition,(
% 56.08/12.72 ![X1]: (sQ79_spl <=> (gt(X1,sK3_skl(sK8_skl(n0)))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f980,plain,(
% 56.08/12.72 ![X0]: (gt(X0,sK3_skl(sK8_skl(n0)))|~sQ79_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f979])).
% 56.08/12.72 fof(f983,plain,(
% 56.08/12.72 ~sQ67_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f972])).
% 56.08/12.72 fof(f1156,definition,(
% 56.08/12.72 sQ107_spl <=> (s3(n0))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f1157,plain,(
% 56.08/12.72 s3(n0)|~sQ107_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f1156])).
% 56.08/12.72 fof(f1160,definition,(
% 56.08/12.72 sQ108_spl <=> (s1(n0))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f1161,plain,(
% 56.08/12.72 s1(n0)|~sQ108_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f1160])).
% 56.08/12.72 fof(f1166,plain,(
% 56.08/12.72 ~s2(n0)|~sQ107_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f1157,f102])).
% 56.08/12.72 fof(f1167,definition,(
% 56.08/12.72 sQ109_spl <=> (gt(n0,n0))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f1168,plain,(
% 56.08/12.72 gt(n0,n0)|~sQ109_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f1167])).
% 56.08/12.72 fof(f1174,plain,(
% 56.08/12.72 $false|~sQ107_spl),
% 56.08/12.72 inference(forward_subsumption_resolution,[status(thm)],[f1166,f168])).
% 56.08/12.72 fof(f1175,plain,(
% 56.08/12.72 ~sQ107_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f1174])).
% 56.08/12.72 fof(f1176,plain,(
% 56.08/12.72 $false|~sQ109_spl),
% 56.08/12.72 inference(forward_subsumption_resolution,[status(thm)],[f1168,f43])).
% 56.08/12.72 fof(f1177,plain,(
% 56.08/12.72 ~sQ109_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f1176])).
% 56.08/12.72 fof(f1179,plain,(
% 56.08/12.72 ~s2(n0)|~sQ108_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f1161,f100])).
% 56.08/12.72 fof(f1180,plain,(
% 56.08/12.72 $false|~sQ108_spl),
% 56.08/12.72 inference(forward_subsumption_resolution,[status(thm)],[f1179,f168])).
% 56.08/12.72 fof(f1181,plain,(
% 56.08/12.72 ~sQ108_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f1180])).
% 56.08/12.72 fof(f1185,definition,(
% 56.08/12.72 sQ111_spl <=> (gt(n0,sK10_skl(n0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f1186,plain,(
% 56.08/12.72 gt(n0,sK10_skl(n0))|~sQ111_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f1185])).
% 56.08/12.72 fof(f1197,plain,(
% 56.08/12.72 $false|~sQ111_spl),
% 56.08/12.72 inference(forward_subsumption_resolution,[status(thm)],[f1186,f670])).
% 56.08/12.72 fof(f1198,plain,(
% 56.08/12.72 ~sQ111_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f1197])).
% 56.08/12.72 fof(f1269,definition,(
% 56.08/12.72 ![X0]: (sQ123_spl <=> (gt(X0,sK10_skl(n0))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f1270,plain,(
% 56.08/12.72 ![X0]: (gt(X0,sK10_skl(n0))|~sQ123_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f1269])).
% 56.08/12.72 fof(f1273,plain,(
% 56.08/12.72 $false|~sQ123_spl),
% 56.08/12.72 inference(backward_subsumption_resolution,[status(thm)],[f670,f1270])).
% 56.08/12.72 fof(f1274,plain,(
% 56.08/12.72 ~sQ123_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f1273])).
% 56.08/12.72 fof(f1422,plain,(
% 56.08/12.72 drugi(n0)|~sQ48_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f810,f43])).
% 56.08/12.72 fof(f1446,definition,(
% 56.08/12.72 sQ144_spl <=> (drugi(sK0_skl(n0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f1447,plain,(
% 56.08/12.72 drugi(sK0_skl(n0))|~sQ144_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f1446])).
% 56.08/12.72 fof(f1465,plain,(
% 56.08/12.72 sQ48_spl|~sQ56_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f908,f809,f857])).
% 56.08/12.72 fof(f1500,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|sP0_prd(X0)|~sQ144_spl)),
% 56.08/12.72 inference(resolution,[status(thm)],[f1447,f60])).
% 56.08/12.72 fof(f1502,plain,(
% 56.08/12.72 sQ55_spl|~sQ144_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f1500,f833,f1446])).
% 56.08/12.72 fof(f1749,definition,(
% 56.08/12.72 ![X0]: (sQ201_spl <=> (uptakepg(X0)|conditionhyper(X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f1750,plain,(
% 56.08/12.72 ![X0]: (uptakepg(X0)|conditionhyper(X0)|~sQ201_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f1749])).
% 56.08/12.72 fof(f1790,definition,(
% 56.08/12.72 ![X0]: (sQ210_spl <=> (gt(X0,sK3_skl(n0))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f1791,plain,(
% 56.08/12.72 ![X0]: (gt(X0,sK3_skl(n0))|~sQ210_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f1790])).
% 56.08/12.72 fof(f1800,plain,(
% 56.08/12.72 ![X0]: (uptakepg(X0)|~conditionnormo(X0)|~sQ201_spl)),
% 56.08/12.72 inference(resolution,[status(thm)],[f1750,f53])).
% 56.08/12.72 fof(f1905,definition,(
% 56.08/12.72 ![X0]: (sQ228_spl <=> (gt(X0,sK0_skl(n0))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f1906,plain,(
% 56.08/12.72 ![X0]: (gt(X0,sK0_skl(n0))|~sQ228_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f1905])).
% 56.08/12.72 fof(f2395,definition,(
% 56.08/12.72 ![X0]: (sQ283_spl <=> (gt(X0,n0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f2396,plain,(
% 56.08/12.72 ![X0]: (gt(X0,n0)|~sQ283_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2395])).
% 56.08/12.72 fof(f2418,plain,(
% 56.08/12.72 $false|~sQ283_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f2396,f43])).
% 56.08/12.72 fof(f2419,definition,(
% 56.08/12.72 ![X0]: (sQ285_spl <=> (gt(X0,sK4_skl(n0))))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f2420,plain,(
% 56.08/12.72 ![X0]: (gt(X0,sK4_skl(n0))|~sQ285_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2419])).
% 56.08/12.72 fof(f2427,definition,(
% 56.08/12.72 ![X0,X1]: (sQ287_spl <=> (uptakelg(X0)|gt(X1,X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f2428,plain,(
% 56.08/12.72 ![X0,X1]: (uptakelg(X0)|gt(X1,X0)|~sQ287_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2427])).
% 56.08/12.72 fof(f2449,plain,(
% 56.08/12.72 ~sQ283_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f2418])).
% 56.08/12.72 fof(f2508,plain,(
% 56.08/12.72 $false|~sQ285_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f2420,f43])).
% 56.08/12.72 fof(f2509,plain,(
% 56.08/12.72 ~sQ285_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f2508])).
% 56.08/12.72 fof(f2586,plain,(
% 56.08/12.72 ![X0]: (uptakelg(X0)|~sQ287_spl)),
% 56.08/12.72 inference(resolution,[status(thm)],[f2428,f43])).
% 56.08/12.72 fof(f2762,definition,(
% 56.08/12.72 sQ294_spl <=> (sP5_prd(sK7_skl(n0),n0))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f2763,plain,(
% 56.08/12.72 sP5_prd(sK7_skl(n0),n0)|~sQ294_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2762])).
% 56.08/12.72 fof(f2840,definition,(
% 56.08/12.72 ![X0]: (sQ296_spl <=> (uptakepg(X0)|gt(n0,X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f2841,plain,(
% 56.08/12.72 ![X0]: (uptakepg(X0)|gt(n0,X0)|~sQ296_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2840])).
% 56.08/12.72 fof(f2844,definition,(
% 56.08/12.72 ![X0]: (sQ297_spl <=> (uptakelg(X0)|gt(n0,X0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f2845,plain,(
% 56.08/12.72 ![X0]: (uptakelg(X0)|gt(n0,X0)|~sQ297_spl)),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2844])).
% 56.08/12.72 fof(f2950,definition,(
% 56.08/12.72 sQ304_spl <=> (sP14_prd(n0))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ304_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f2951,plain,(
% 56.08/12.72 sP14_prd(n0)|~sQ304_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2950])).
% 56.08/12.72 fof(f2953,definition,(
% 56.08/12.72 sQ305_spl <=> (bcapacitysn(n0))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ305_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f2954,plain,(
% 56.08/12.72 bcapacitysn(n0)|~sQ305_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2953])).
% 56.08/12.72 fof(f2955,plain,(
% 56.08/12.72 ~bcapacitysn(n0)|sQ305_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2953])).
% 56.08/12.72 fof(f2968,definition,(
% 56.08/12.72 sQ309_spl <=> (sP12_prd(n0))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f2969,plain,(
% 56.08/12.72 sP12_prd(n0)|~sQ309_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f2968])).
% 56.08/12.72 fof(f2983,plain,(
% 56.08/12.72 bcapacitysn(n0)|~sQ309_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f2969,f278])).
% 56.08/12.72 fof(f2984,plain,(
% 56.08/12.72 $false|sQ305_spl|~sQ309_spl),
% 56.08/12.72 inference(forward_subsumption_resolution,[status(thm)],[f2983,f2955])).
% 56.08/12.72 fof(f2985,plain,(
% 56.08/12.72 sQ305_spl|~sQ309_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f2984])).
% 56.08/12.72 fof(f2989,plain,(
% 56.08/12.72 bcapacitysn(n0)|~sQ304_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f2951,f295])).
% 56.08/12.72 fof(f2992,plain,(
% 56.08/12.72 ~bcapacityex(n0)|~sQ305_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f2954,f50])).
% 56.08/12.72 fof(f2997,plain,(
% 56.08/12.72 $false|~sQ305_spl),
% 56.08/12.72 inference(forward_subsumption_resolution,[status(thm)],[f2992,f170])).
% 56.08/12.72 fof(f2998,plain,(
% 56.08/12.72 ~sQ305_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f2997])).
% 56.08/12.72 fof(f3083,plain,(
% 56.08/12.72 sQ305_spl|~sQ304_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f2989,f2953,f2950])).
% 56.08/12.72 fof(f3101,plain,(
% 56.08/12.72 ~conditionnormo(sK7_skl(n0))|~sQ294_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f2763,f216])).
% 56.08/12.72 fof(f3118,definition,(
% 56.08/12.72 sQ321_spl <=> (drugi(n0))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f3119,plain,(
% 56.08/12.72 drugi(n0)|~sQ321_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f3118])).
% 56.08/12.72 fof(f3123,plain,(
% 56.08/12.72 s3(n0)|~sQ321_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f3119,f129])).
% 56.08/12.72 fof(f3124,plain,(
% 56.08/12.72 sQ107_spl|~sQ321_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f3123,f1156,f3118])).
% 56.08/12.72 fof(f3229,plain,(
% 56.08/12.72 ![X0]: (uptakelg(sK8_skl(n0))|gt(n0,X0)|drugi(X0)|~sQ297_spl)),
% 56.08/12.72 inference(resolution,[status(thm)],[f2845,f132])).
% 56.08/12.72 fof(f3249,definition,(
% 56.08/12.72 sQ325_spl <=> (uptakelg(sK8_skl(n0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f3250,plain,(
% 56.08/12.72 uptakelg(sK8_skl(n0))|~sQ325_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f3249])).
% 56.08/12.72 fof(f3251,plain,(
% 56.08/12.72 ~uptakelg(sK8_skl(n0))|sQ325_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f3249])).
% 56.08/12.72 fof(f3252,plain,(
% 56.08/12.72 sQ325_spl|sQ48_spl|~sQ297_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f3229,f3249,f809,f2844])).
% 56.08/12.72 fof(f3299,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|drugi(X0)|~sQ325_spl)),
% 56.08/12.72 inference(resolution,[status(thm)],[f3250,f133])).
% 56.08/12.72 fof(f3300,plain,(
% 56.08/12.72 sQ48_spl|~sQ325_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f3299,f809,f3249])).
% 56.08/12.72 fof(f3301,plain,(
% 56.08/12.72 releaselg(sK8_skl(n0))|sQ325_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f3251,f696])).
% 56.08/12.72 fof(f3302,plain,(
% 56.08/12.72 $false|sQ68_spl|sQ325_spl),
% 56.08/12.72 inference(forward_subsumption_resolution,[status(thm)],[f3301,f920])).
% 56.08/12.72 fof(f3303,plain,(
% 56.08/12.72 sQ68_spl|sQ325_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f3302])).
% 56.08/12.72 fof(f3312,plain,(
% 56.08/12.72 ![X0]: (uptakepg(sK9_skl(n0))|gt(n0,X0)|drugi(X0)|~sQ296_spl)),
% 56.08/12.72 inference(resolution,[status(thm)],[f2841,f134])).
% 56.08/12.72 fof(f3334,definition,(
% 56.08/12.72 sQ331_spl <=> (uptakepg(sK9_skl(n0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f3335,plain,(
% 56.08/12.72 uptakepg(sK9_skl(n0))|~sQ331_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f3334])).
% 56.08/12.72 fof(f3336,plain,(
% 56.08/12.72 ~uptakepg(sK9_skl(n0))|sQ331_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f3334])).
% 56.08/12.72 fof(f3337,plain,(
% 56.08/12.72 sQ331_spl|sQ48_spl|~sQ296_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f3312,f3334,f809,f2840])).
% 56.08/12.72 fof(f3485,plain,(
% 56.08/12.72 ![X0]: (gt(n0,X0)|drugi(X0)|~sQ331_spl)),
% 56.08/12.72 inference(resolution,[status(thm)],[f135,f3335])).
% 56.08/12.72 fof(f3486,plain,(
% 56.08/12.72 sQ48_spl|~sQ331_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f3485,f809,f3334])).
% 56.08/12.72 fof(f3488,plain,(
% 56.08/12.72 sQ321_spl|~sQ48_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f1422,f3118,f809])).
% 56.08/12.72 fof(f3530,plain,(
% 56.08/12.72 $false|~sQ79_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f980,f43])).
% 56.08/12.72 fof(f3581,plain,(
% 56.08/12.72 ~sQ79_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f3530])).
% 56.08/12.72 fof(f3584,plain,(
% 56.08/12.72 $false|~sQ287_spl|sQ325_spl),
% 56.08/12.72 inference(backward_subsumption_resolution,[status(thm)],[f3251,f2586])).
% 56.08/12.72 fof(f3585,plain,(
% 56.08/12.72 ~sQ287_spl|sQ325_spl),
% 56.08/12.72 inference(contradiction_clause,[status(thm)],[f3584])).
% 56.08/12.72 fof(f3784,definition,(
% 56.08/12.72 sQ396_spl <=> (s3(sK0_skl(n0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ396_spl])],[split_symbol_definition])).
% 56.08/12.72 fof(f3785,plain,(
% 56.08/12.72 s3(sK0_skl(n0))|~sQ396_spl),
% 56.08/12.72 inference(component_clause,[status(thm)],[f3784])).
% 56.08/12.72 fof(f3940,plain,(
% 56.08/12.72 drugi(sK0_skl(n0))|~sQ396_spl),
% 56.08/12.72 inference(resolution,[status(thm)],[f3785,f299])).
% 56.08/12.72 fof(f3964,plain,(
% 56.08/12.72 sQ144_spl|~sQ396_spl),
% 56.08/12.72 inference(split_clause,[status(thm)],[f3940,f1446,f3784])).
% 56.08/12.72 fof(f4118,definition,(
% 56.08/12.72 sQ434_spl <=> (gt(n0,sK8_skl(n0)))),
% 56.08/12.72 introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4119,plain,(
% 56.08/12.73 gt(n0,sK8_skl(n0))|~sQ434_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f4118])).
% 56.08/12.73 fof(f4144,definition,(
% 56.08/12.73 sQ439_spl <=> (conditionnormo(sK7_skl(n0)))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4145,plain,(
% 56.08/12.73 conditionnormo(sK7_skl(n0))|~sQ439_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f4144])).
% 56.08/12.73 fof(f4148,plain,(
% 56.08/12.73 ![X0]: (gt(n0,X0)|conditionnormo(X0)|bcapacityex(sK14_skl(n0)))),
% 56.08/12.73 inference(resolution,[status(thm)],[f165,f168])).
% 56.08/12.73 fof(f4149,definition,(
% 56.08/12.73 sQ440_spl <=> (bcapacityex(sK14_skl(n0)))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ440_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4150,plain,(
% 56.08/12.73 bcapacityex(sK14_skl(n0))|~sQ440_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f4149])).
% 56.08/12.73 fof(f4152,plain,(
% 56.08/12.73 sQ3_spl|sQ440_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f4148,f328,f4149])).
% 56.08/12.73 fof(f4153,plain,(
% 56.08/12.73 ![X0,X1]: (gt(n0,X0)|conditionnormo(X0)|~gt(sK14_skl(n0),X1)|conditionhyper(X1))),
% 56.08/12.73 inference(resolution,[status(thm)],[f164,f168])).
% 56.08/12.73 fof(f4154,definition,(
% 56.08/12.73 ![X1]: (sQ441_spl <=> (~gt(sK14_skl(n0),X1)|conditionhyper(X1)))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ441_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4155,plain,(
% 56.08/12.73 ![X0]: (~gt(sK14_skl(n0),X0)|conditionhyper(X0)|~sQ441_spl)),
% 56.08/12.73 inference(component_clause,[status(thm)],[f4154])).
% 56.08/12.73 fof(f4157,plain,(
% 56.08/12.73 sQ3_spl|sQ441_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f4153,f328,f4154])).
% 56.08/12.73 fof(f4238,plain,(
% 56.08/12.73 conditionhypo(sK15_skl(sK14_skl(n0)))|conditionnormo(sK15_skl(sK14_skl(n0)))|gt(n0,sK14_skl(n0))|~s3(sK14_skl(n0))|~sQ440_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f4150,f304])).
% 56.08/12.73 fof(f4239,definition,(
% 56.08/12.73 sQ460_spl <=> (conditionhypo(sK15_skl(sK14_skl(n0))))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ460_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4240,plain,(
% 56.08/12.73 conditionhypo(sK15_skl(sK14_skl(n0)))|~sQ460_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f4239])).
% 56.08/12.73 fof(f4242,definition,(
% 56.08/12.73 sQ461_spl <=> (conditionnormo(sK15_skl(sK14_skl(n0))))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ461_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4243,plain,(
% 56.08/12.73 conditionnormo(sK15_skl(sK14_skl(n0)))|~sQ461_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f4242])).
% 56.08/12.73 fof(f4245,definition,(
% 56.08/12.73 sQ462_spl <=> (gt(n0,sK14_skl(n0)))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ462_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4248,definition,(
% 56.08/12.73 sQ463_spl <=> (s3(sK14_skl(n0)))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ463_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4251,plain,(
% 56.08/12.73 sQ460_spl|sQ461_spl|sQ462_spl|~sQ463_spl|~sQ440_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f4238,f4239,f4242,f4245,f4248,f4149])).
% 56.08/12.73 fof(f4299,plain,(
% 56.08/12.73 ![X0,X1]: (sP6_prd(X0)|gt(X0,X1)|uptakepg(X1)|~gt(X0,sK7_skl(X0)))),
% 56.08/12.73 inference(resolution,[status(thm)],[f109,f215])).
% 56.08/12.73 fof(f4307,plain,(
% 56.08/12.73 ![X0]: (sP5_prd(sK7_skl(n0),n0)|sP6_prd(n0)|uptakepg(X0)|conditionhyper(X0))),
% 56.08/12.73 inference(resolution,[status(thm)],[f109,f169])).
% 56.08/12.73 fof(f4324,definition,(
% 56.08/12.73 sQ472_spl <=> (sP6_prd(n0))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ472_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4325,plain,(
% 56.08/12.73 sP6_prd(n0)|~sQ472_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f4324])).
% 56.08/12.73 fof(f4334,plain,(
% 56.08/12.73 sQ294_spl|sQ472_spl|sQ201_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f4307,f2762,f4324,f1749])).
% 56.08/12.73 fof(f4356,plain,(
% 56.08/12.73 $false|~sQ439_spl|~sQ294_spl),
% 56.08/12.73 inference(forward_subsumption_resolution,[status(thm)],[f3101,f4145])).
% 56.08/12.73 fof(f4357,plain,(
% 56.08/12.73 ~sQ439_spl|~sQ294_spl),
% 56.08/12.73 inference(contradiction_clause,[status(thm)],[f4356])).
% 56.08/12.73 fof(f4448,definition,(
% 56.08/12.73 ![X0]: (sQ481_spl <=> (gt(X0,sK11_skl(n0))))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ481_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4449,plain,(
% 56.08/12.73 ![X0]: (gt(X0,sK11_skl(n0))|~sQ481_spl)),
% 56.08/12.73 inference(component_clause,[status(thm)],[f4448])).
% 56.08/12.73 fof(f4785,plain,(
% 56.08/12.73 gt(n0,sK14_skl(n0))|~s3(sK14_skl(n0))|gt(sK14_skl(n0),sK15_skl(sK14_skl(n0)))|~sQ440_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f4150,f171])).
% 56.08/12.73 fof(f4786,definition,(
% 56.08/12.73 sQ495_spl <=> (gt(sK14_skl(n0),sK15_skl(sK14_skl(n0))))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ495_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f4787,plain,(
% 56.08/12.73 gt(sK14_skl(n0),sK15_skl(sK14_skl(n0)))|~sQ495_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f4786])).
% 56.08/12.73 fof(f4789,plain,(
% 56.08/12.73 sQ462_spl|~sQ463_spl|sQ495_spl|~sQ440_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f4785,f4245,f4248,f4786,f4149])).
% 56.08/12.73 fof(f5059,plain,(
% 56.08/12.73 $false|~sQ481_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f4449,f43])).
% 56.08/12.73 fof(f5104,plain,(
% 56.08/12.73 ~sQ481_spl),
% 56.08/12.73 inference(contradiction_clause,[status(thm)],[f5059])).
% 56.08/12.73 fof(f5124,plain,(
% 56.08/12.73 ![X0]: (gt(n0,X0)|conditionnormo(X0)|s3(sK14_skl(n0)))),
% 56.08/12.73 inference(resolution,[status(thm)],[f163,f168])).
% 56.08/12.73 fof(f5132,plain,(
% 56.08/12.73 sQ3_spl|sQ463_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f5124,f328,f4248])).
% 56.08/12.73 fof(f5175,plain,(
% 56.08/12.73 $false|~sQ210_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f1791,f43])).
% 56.08/12.73 fof(f5216,plain,(
% 56.08/12.73 ~sQ210_spl),
% 56.08/12.73 inference(contradiction_clause,[status(thm)],[f5175])).
% 56.08/12.73 fof(f5219,plain,(
% 56.08/12.73 ![X0]: (gt(n0,X0)|conditionnormo(X0)|~gt(n0,sK14_skl(n0)))),
% 56.08/12.73 inference(resolution,[status(thm)],[f162,f168])).
% 56.08/12.73 fof(f5220,plain,(
% 56.08/12.73 sQ3_spl|~sQ462_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f5219,f328,f4245])).
% 56.08/12.73 fof(f5461,plain,(
% 56.08/12.73 ![X0]: (conditionnormo(sK9_skl(n0))|gt(n0,X0)|drugi(X0)|~sQ3_spl)),
% 56.08/12.73 inference(resolution,[status(thm)],[f329,f134])).
% 56.08/12.73 fof(f5486,definition,(
% 56.08/12.73 sQ574_spl <=> (conditionnormo(sK9_skl(n0)))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ574_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f5487,plain,(
% 56.08/12.73 conditionnormo(sK9_skl(n0))|~sQ574_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f5486])).
% 56.08/12.73 fof(f5489,plain,(
% 56.08/12.73 sQ574_spl|sQ48_spl|~sQ3_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f5461,f5486,f809,f328])).
% 56.08/12.73 fof(f5658,plain,(
% 56.08/12.73 uptakepg(sK9_skl(n0))|~sQ201_spl|~sQ574_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f1800,f5487])).
% 56.08/12.73 fof(f5663,plain,(
% 56.08/12.73 sQ331_spl|~sQ201_spl|~sQ574_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f5658,f3334,f1749,f5486])).
% 56.08/12.73 fof(f6648,plain,(
% 56.08/12.73 conditionhyper(sK15_skl(sK14_skl(n0)))|~sQ495_spl|~sQ441_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f4787,f4155])).
% 56.08/12.73 fof(f7233,definition,(
% 56.08/12.73 sQ712_spl <=> (drugbg(sK2_skl(n0)))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ712_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f7234,plain,(
% 56.08/12.73 drugbg(sK2_skl(n0))|~sQ712_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f7233])).
% 56.08/12.73 fof(f7271,plain,(
% 56.08/12.73 ![X0]: (gt(n0,X0)|~releaselg(X0)|~sQ712_spl)),
% 56.08/12.73 inference(resolution,[status(thm)],[f7234,f71])).
% 56.08/12.73 fof(f7273,plain,(
% 56.08/12.73 sQ50_spl|~sQ712_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f7271,f816,f7233])).
% 56.08/12.73 fof(f7452,plain,(
% 56.08/12.73 sP9_prd(n0)|sP10_prd(n0)|~sQ472_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f4325,f225])).
% 56.08/12.73 fof(f7454,definition,(
% 56.08/12.73 sQ725_spl <=> (sP9_prd(n0))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ725_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f7455,plain,(
% 56.08/12.73 sP9_prd(n0)|~sQ725_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f7454])).
% 56.08/12.73 fof(f7457,definition,(
% 56.08/12.73 sQ726_spl <=> (sP10_prd(n0))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f7458,plain,(
% 56.08/12.73 sP10_prd(n0)|~sQ726_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f7457])).
% 56.08/12.73 fof(f7460,plain,(
% 56.08/12.73 sQ725_spl|sQ726_spl|~sQ472_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f7452,f7454,f7457,f4324])).
% 56.08/12.73 fof(f7464,plain,(
% 56.08/12.73 sP13_prd(n0)|~sQ726_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f7458,f261])).
% 56.08/12.73 fof(f7471,plain,(
% 56.08/12.73 sP11_prd(n0)|sP12_prd(n0)|~sQ725_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f7455,f251])).
% 56.08/12.73 fof(f7474,definition,(
% 56.08/12.73 sQ728_spl <=> (sP11_prd(n0))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ728_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f7475,plain,(
% 56.08/12.73 sP11_prd(n0)|~sQ728_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f7474])).
% 56.08/12.73 fof(f7477,plain,(
% 56.08/12.73 sQ728_spl|sQ309_spl|~sQ725_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f7471,f7474,f2968,f7454])).
% 56.08/12.73 fof(f7496,plain,(
% 56.08/12.73 ![X0,X1]: (gt(n0,X0)|~releaselg(X0)|gt(n0,X1)|uptakepg(X1)|~sQ726_spl)),
% 56.08/12.73 inference(resolution,[status(thm)],[f7464,f285])).
% 56.08/12.73 fof(f7499,plain,(
% 56.08/12.73 sQ50_spl|sQ296_spl|~sQ726_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f7496,f816,f2840,f7457])).
% 56.08/12.73 fof(f7539,plain,(
% 56.08/12.73 sP14_prd(n0)|~sQ728_spl),
% 56.08/12.73 inference(resolution,[status(thm)],[f7475,f270])).
% 56.08/12.73 fof(f7541,plain,(
% 56.08/12.73 sQ304_spl|~sQ728_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f7539,f2950,f7474])).
% 56.08/12.73 fof(f9745,plain,(
% 56.08/12.73 ![X0]: (gt(n0,X0)|drugi(X0)|~sQ434_spl)),
% 56.08/12.73 inference(resolution,[status(thm)],[f4119,f132])).
% 56.08/12.73 fof(f9760,plain,(
% 56.08/12.73 sQ48_spl|~sQ434_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f9745,f809,f4118])).
% 56.08/12.73 fof(f11466,plain,(
% 56.08/12.73 ![X0]: (conditionnormo(sK7_skl(n0))|sP6_prd(n0)|gt(n0,X0)|uptakepg(X0)|~sQ3_spl)),
% 56.08/12.73 inference(resolution,[status(thm)],[f329,f4299])).
% 56.08/12.73 fof(f11496,plain,(
% 56.08/12.73 sQ439_spl|sQ472_spl|sQ296_spl|~sQ3_spl),
% 56.08/12.73 inference(split_clause,[status(thm)],[f11466,f4144,f4324,f2840,f328])).
% 56.08/12.73 fof(f11500,definition,(
% 56.08/12.73 sQ1026_spl <=> (sP13_prd(n0))),
% 56.08/12.73 introduced(definition,[new_symbols(definition,[sQ1026_spl])],[split_symbol_definition])).
% 56.08/12.73 fof(f11501,plain,(
% 56.08/12.73 sP13_prd(n0)|~sQ1026_spl),
% 56.08/12.73 inference(component_clause,[status(thm)],[f11500])).
% 25.43/12.75 fof(f11526,plain,(
% 25.43/12.75 ![X0,X1]: (gt(n0,X0)|~releaselg(X0)|gt(n0,X1)|uptakepg(X1)|~sQ1026_spl)),
% 25.43/12.75 inference(resolution,[status(thm)],[f11501,f285])).
% 25.43/12.75 fof(f11529,plain,(
% 25.43/12.75 sQ50_spl|sQ296_spl|~sQ1026_spl),
% 25.43/12.75 inference(split_clause,[status(thm)],[f11526,f816,f2840,f11500])).
% 25.43/12.75 fof(f13459,definition,(
% 25.43/12.75 ![X1]: (sQ1145_spl <=> (uptakepg(X1)))),
% 25.43/12.75 introduced(definition,[new_symbols(definition,[sQ1145_spl])],[split_symbol_definition])).
% 25.43/12.75 fof(f13460,plain,(
% 25.43/12.75 ![X0]: (uptakepg(X0)|~sQ1145_spl)),
% 25.43/12.75 inference(component_clause,[status(thm)],[f13459])).
% 25.43/12.75 fof(f13561,plain,(
% 25.43/12.75 $false|~sQ1145_spl|sQ331_spl),
% 25.43/12.75 inference(backward_subsumption_resolution,[status(thm)],[f3336,f13460])).
% 25.43/12.75 fof(f13607,plain,(
% 25.43/12.75 ~sQ1145_spl|sQ331_spl),
% 25.43/12.75 inference(contradiction_clause,[status(thm)],[f13561])).
% 25.43/12.75 fof(f13713,definition,(
% 25.43/12.75 ![X0]: (sQ1152_spl <=> (gt(X0,sK27_skl(n0))))),
% 25.43/12.75 introduced(definition,[new_symbols(definition,[sQ1152_spl])],[split_symbol_definition])).
% 25.43/12.75 fof(f13714,plain,(
% 25.43/12.75 ![X0]: (gt(X0,sK27_skl(n0))|~sQ1152_spl)),
% 25.43/12.75 inference(component_clause,[status(thm)],[f13713])).
% 25.43/12.75 fof(f13788,definition,(
% 25.43/12.75 ![X0]: (sQ1166_spl <=> (gt(X0,sK20_skl(n0))))),
% 25.43/12.75 introduced(definition,[new_symbols(definition,[sQ1166_spl])],[split_symbol_definition])).
% 25.43/12.75 fof(f13789,plain,(
% 25.43/12.75 ![X0]: (gt(X0,sK20_skl(n0))|~sQ1166_spl)),
% 25.43/12.75 inference(component_clause,[status(thm)],[f13788])).
% 25.43/12.75 fof(f14109,plain,(
% 25.43/12.75 ~conditionhyper(sK15_skl(sK14_skl(n0)))|~sQ461_spl),
% 25.43/12.75 inference(resolution,[status(thm)],[f4243,f53])).
% 25.43/12.75 fof(f14110,plain,(
% 25.43/12.75 $false|~sQ495_spl|~sQ441_spl|~sQ461_spl),
% 25.43/12.75 inference(forward_subsumption_resolution,[status(thm)],[f14109,f6648])).
% 25.43/12.75 fof(f14111,plain,(
% 25.43/12.75 ~sQ495_spl|~sQ441_spl|~sQ461_spl),
% 25.43/12.75 inference(contradiction_clause,[status(thm)],[f14110])).
% 25.43/12.75 fof(f14148,plain,(
% 25.43/12.75 $false|~sQ228_spl),
% 25.43/12.75 inference(resolution,[status(thm)],[f1906,f43])).
% 25.43/12.75 fof(f14185,plain,(
% 25.43/12.75 ~sQ228_spl),
% 25.43/12.75 inference(contradiction_clause,[status(thm)],[f14148])).
% 25.43/12.75 fof(f14402,plain,(
% 25.43/12.75 $false|~sQ1152_spl),
% 25.43/12.75 inference(resolution,[status(thm)],[f13714,f43])).
% 25.43/12.75 fof(f14446,plain,(
% 25.43/12.75 ~sQ1152_spl),
% 25.43/12.75 inference(contradiction_clause,[status(thm)],[f14402])).
% 25.43/12.75 fof(f14697,plain,(
% 25.43/12.75 $false|~sQ1166_spl),
% 25.43/12.75 inference(resolution,[status(thm)],[f13789,f43])).
% 25.43/12.75 fof(f14747,plain,(
% 25.43/12.75 ~sQ1166_spl),
% 25.43/12.75 inference(contradiction_clause,[status(thm)],[f14697])).
% 25.43/12.75 fof(f14927,plain,(
% 25.43/12.75 gt(n0,sK8_skl(n0))|~sQ50_spl|sQ325_spl),
% 25.43/12.75 inference(resolution,[status(thm)],[f817,f3301])).
% 25.43/12.75 fof(f16838,plain,(
% 25.43/12.75 ~conditionhyper(sK15_skl(sK14_skl(n0)))|~sQ460_spl),
% 25.43/12.75 inference(resolution,[status(thm)],[f4240,f52])).
% 25.43/12.75 fof(f16840,plain,(
% 25.43/12.75 $false|~sQ495_spl|~sQ441_spl|~sQ460_spl),
% 25.43/12.75 inference(forward_subsumption_resolution,[status(thm)],[f16838,f6648])).
% 25.43/12.75 fof(f16841,plain,(
% 25.43/12.75 ~sQ495_spl|~sQ441_spl|~sQ460_spl),
% 25.43/12.75 inference(contradiction_clause,[status(thm)],[f16840])).
% 25.43/12.75 fof(f16873,plain,(
% 25.43/12.75 $false|sQ52_spl),
% 25.43/12.75 inference(forward_subsumption_resolution,[status(thm)],[f825,f170])).
% 25.43/12.75 fof(f16874,plain,(
% 25.43/12.75 sQ52_spl),
% 25.43/12.75 inference(contradiction_clause,[status(thm)],[f16873])).
% 25.43/12.75 fof(f16902,plain,(
% 25.43/12.75 sQ434_spl|~sQ50_spl|sQ325_spl),
% 25.43/12.75 inference(split_clause,[status(thm)],[f14927,f4118,f816,f3249])).
% 25.43/12.75 fof(f16958,plain,(
% 25.43/12.75 $false),
% 25.43/12.75 inference(sat_refutation,[status(thm)],[f860,f951,f967,f983,f1175,f1177,f1181,f1198,f1274,f1465,f1502,f2449,f2509,f2985,f2998,f3083,f3124,f3252,f3300,f3303,f3337,f3486,f3488,f3581,f3585,f3964,f4152,f4157,f4251,f4334,f4357,f4789,f5104,f5132,f5216,f5220,f5489,f5663,f7273,f7460,f7477,f7499,f7541,f9760,f11496,f11529,f13607,f14111,f14185,f14446,f14747,f16841,f16874,f16902])).
% 25.43/12.75 % SZS output end CNFRefutation for theBenchmark.p
% 25.43/12.76 % Elapsed time: 7.332411 seconds
% 25.43/12.76 % CPU time: 57.989382 seconds
% 25.43/12.76 % Total memory used: 236.456 MB
% 25.43/12.76 % Net memory used: 215.349 MB
%------------------------------------------------------------------------------