%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MED006+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 7.14s 1.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED006+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 01:18:07 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 7.14/1.54 % Refutation found
% 7.14/1.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.14/1.54 % SZS output start CNFRefutation for theBenchmark
% 7.14/1.54 fof(f1,axiom,(
% 7.14/1.54 (! [X] : ~ gt(X,X) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f9,axiom,(
% 7.14/1.54 (! [X0] :( ~ conditionhyper(X0)| ~ conditionnormo(X0) ) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f12,axiom,(
% 7.14/1.54 (! [X0,X1] :( ~ gt(X0,X1)=> ( uptakelg(X1)=> ~ releaselg(X1) ) ) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f23,axiom,(
% 7.14/1.54 (! [X0] :( ~ s1(X0)| ~ s2(X0) ) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f24,axiom,(
% 7.14/1.54 (! [X0] :( ~ s1(X0)| ~ s3(X0) ) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f26,axiom,(
% 7.14/1.54 (! [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) ) )) ) ) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f31,axiom,(
% 7.14/1.54 (! [X0] :( drugbg(X0)=> ( ( s1(X0)& ~ qilt27(X0) )| s2(X0)| s3(X0) ) ) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f33,axiom,(
% 7.14/1.54 (! [X0] :( drugi(X0)=> s3(X0) ) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f34,axiom,(
% 7.14/1.54 (! [X0] :( ( (! [X1] :( ~ gt(X0,X1)=> uptakelg(X1) ))| (! [X1] :( ~ gt(X0,X1)=> uptakepg(X1) ) ))=> (! [X1] :( ~ gt(X0,X1)=> drugi(X1) ) )) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f35,axiom,(
% 7.14/1.54 (! [X0,X1] :( ~ gt(X0,X1)=> ( ~ releaselg(X1)=> uptakelg(X1) ) ) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f37,axiom,(
% 7.14/1.54 (! [X0] :( (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ))=> (! [X1] :( ~ gt(X0,X1)=> drugbg(X1) ) )) )),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f41,conjecture,(
% 7.14/1.54 ( ( s1(n0)& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ))& ~ bcapacitysn(n0)& qilt27(n0) )=> ~ (! [X0] :( ~ gt(n0,X0)=> conditionnormo(X0) ) )) ),
% 7.14/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.14/1.54 fof(f42,negated_conjecture,(
% 7.14/1.54 ~(( ( s1(n0)& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ))& ~ bcapacitysn(n0)& qilt27(n0) )=> ~ (! [X0] :( ~ gt(n0,X0)=> conditionnormo(X0) ) )) )),
% 7.14/1.54 inference(negated_conjecture,[status(cth)],[f41])).
% 7.14/1.54 fof(f43,plain,(
% 7.14/1.54 ![X0]: (~gt(X0,X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f1])).
% 7.14/1.54 fof(f53,plain,(
% 7.14/1.54 ![X0]: (~conditionhyper(X0)|~conditionnormo(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f9])).
% 7.14/1.54 fof(f61,plain,(
% 7.14/1.54 ![X0,X1]: (gt(X0,X1)|(~uptakelg(X1)|~releaselg(X1)))),
% 7.14/1.54 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 7.14/1.54 fof(f62,plain,(
% 7.14/1.54 ![X1]: ((![X0]: gt(X0,X1))|(~uptakelg(X1)|~releaselg(X1)))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f61])).
% 7.14/1.54 fof(f63,plain,(
% 7.14/1.54 ![X0,X1]: (gt(X0,X1)|~uptakelg(X1)|~releaselg(X1))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f62])).
% 7.14/1.54 fof(f100,plain,(
% 7.14/1.54 ![X0]: (~s1(X0)|~s2(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f23])).
% 7.14/1.54 fof(f101,plain,(
% 7.14/1.54 ![X0]: (~s1(X0)|~s3(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f24])).
% 7.14/1.54 fof(f103,plain,(
% 7.14/1.54 ![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))))))),
% 7.14/1.54 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 7.14/1.54 fof(f104,definition,(
% 7.14/1.54 ![X0,X1]: (sP5_prd(X1,X0)<=>(~gt(X0,X1)&~conditionnormo(X1)))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 7.14/1.54 fof(f105,definition,(
% 7.14/1.54 ![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))))))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 7.14/1.54 fof(f106,plain,(
% 7.14/1.54 ![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))))))),
% 7.14/1.54 inference(formula_renaming,[status(thm)],[f103,f105,f104])).
% 7.14/1.54 fof(f107,plain,(
% 7.14/1.54 ![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))))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X1,sK7_skl(X0))],[f106])).
% 7.14/1.54 fof(f108,plain,(
% 7.14/1.54 ![X0,X1]: (sP5_prd(sK7_skl(X0),X0)|sP6_prd(X0)|gt(X0,X1)|uptakelg(X1))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f107])).
% 7.14/1.54 fof(f122,plain,(
% 7.14/1.54 ![X0]: (~drugbg(X0)|(((s1(X0)&~qilt27(X0))|s2(X0))|s3(X0)))),
% 7.14/1.54 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 7.14/1.54 fof(f124,plain,(
% 7.14/1.54 ![X0]: (~drugbg(X0)|~qilt27(X0)|s2(X0)|s3(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f122])).
% 7.14/1.54 fof(f128,plain,(
% 7.14/1.54 ![X0]: (~drugi(X0)|s3(X0))),
% 7.14/1.54 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 7.14/1.54 fof(f129,plain,(
% 7.14/1.54 ![X0]: (~drugi(X0)|s3(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f128])).
% 7.14/1.54 fof(f130,plain,(
% 7.14/1.54 ![X0]: (((?[X1]: (~gt(X0,X1)&~uptakelg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|(![X1]: (gt(X0,X1)|drugi(X1))))),
% 7.14/1.54 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 7.14/1.54 fof(f131,plain,(
% 7.14/1.54 ![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))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(X1,sK8_skl(X0)),skolemize(X1,sK9_skl(X0))],[f130])).
% 7.14/1.54 fof(f134,plain,(
% 7.14/1.54 ![X0,X1]: (~gt(X0,sK9_skl(X0))|gt(X0,X1)|drugi(X1))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f131])).
% 7.14/1.54 fof(f135,plain,(
% 7.14/1.54 ![X0,X1]: (~uptakepg(sK9_skl(X0))|gt(X0,X1)|drugi(X1))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f131])).
% 7.14/1.54 fof(f136,plain,(
% 7.14/1.54 ![X0,X1]: (gt(X0,X1)|(releaselg(X1)|uptakelg(X1)))),
% 7.14/1.54 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 7.14/1.54 fof(f137,plain,(
% 7.14/1.54 ![X1]: ((![X0]: gt(X0,X1))|(releaselg(X1)|uptakelg(X1)))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f136])).
% 7.14/1.54 fof(f138,plain,(
% 7.14/1.54 ![X0,X1]: (gt(X0,X1)|releaselg(X1)|uptakelg(X1))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f137])).
% 7.14/1.54 fof(f145,plain,(
% 7.14/1.54 ![X0]: ((?[X1]: (~gt(X0,X1)&releaselg(X1)))|(![X1]: (gt(X0,X1)|drugbg(X1))))),
% 7.14/1.54 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 7.14/1.54 fof(f146,plain,(
% 7.14/1.54 ![X0]: ((~gt(X0,sK11_skl(X0))&releaselg(sK11_skl(X0)))|(![X1]: (gt(X0,X1)|drugbg(X1))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X1,sK11_skl(X0))],[f145])).
% 7.14/1.54 fof(f147,plain,(
% 7.14/1.54 ![X0,X1]: (~gt(X0,sK11_skl(X0))|gt(X0,X1)|drugbg(X1))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f146])).
% 7.14/1.54 fof(f148,plain,(
% 7.14/1.54 ![X0,X1]: (releaselg(sK11_skl(X0))|gt(X0,X1)|drugbg(X1))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f146])).
% 7.14/1.54 fof(f166,plain,(
% 7.14/1.54 ((((s1(n0)&(![X0]: (~gt(n0,X0)|conditionhyper(X0))))&~bcapacitysn(n0))&qilt27(n0))&(![X0]: (gt(n0,X0)|conditionnormo(X0))))),
% 7.14/1.54 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 7.14/1.54 fof(f167,plain,(
% 7.14/1.54 s1(n0)),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f166])).
% 7.14/1.54 fof(f168,plain,(
% 7.14/1.54 ![X0]: (~gt(n0,X0)|conditionhyper(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f166])).
% 7.14/1.54 fof(f169,plain,(
% 7.14/1.54 ~bcapacitysn(n0)),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f166])).
% 7.14/1.54 fof(f170,plain,(
% 7.14/1.54 qilt27(n0)),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f166])).
% 7.14/1.54 fof(f171,plain,(
% 7.14/1.54 ![X0]: (gt(n0,X0)|conditionnormo(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f166])).
% 7.14/1.54 fof(f212,plain,(
% 7.14/1.54 ![X0,X1]: ((~sP5_prd(X1,X0)|(~gt(X0,X1)&~conditionnormo(X1)))&(sP5_prd(X1,X0)|(gt(X0,X1)|conditionnormo(X1))))),
% 7.14/1.54 inference(NNF_transformation,[status(thm)],[f104])).
% 7.14/1.54 fof(f213,plain,(
% 7.14/1.54 (![X0,X1]: (~sP5_prd(X1,X0)|(~gt(X0,X1)&~conditionnormo(X1))))&(![X0,X1]: (sP5_prd(X1,X0)|(gt(X0,X1)|conditionnormo(X1))))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f212])).
% 7.14/1.54 fof(f214,plain,(
% 7.14/1.54 ![X0,X1]: (~sP5_prd(X0,X1)|~gt(X1,X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f213])).
% 7.14/1.54 fof(f215,plain,(
% 7.14/1.54 ![X0,X1]: (~sP5_prd(X0,X1)|~conditionnormo(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f213])).
% 7.14/1.54 fof(f217,definition,(
% 7.14/1.54 ![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))))))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 7.14/1.54 fof(f218,plain,(
% 7.14/1.54 ![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))))))),
% 7.14/1.54 inference(formula_renaming,[status(thm)],[f105,f217])).
% 7.14/1.54 fof(f219,definition,(
% 7.14/1.54 ![X0]: (sP10_prd(X0)<=>((((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))&(![X1]: (gt(X0,X1)|bsecretioni(X1)))))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 7.14/1.54 fof(f220,plain,(
% 7.14/1.54 ![X0]: (sP6_prd(X0)<=>(sP9_prd(X0)|(sP10_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 7.14/1.54 inference(formula_renaming,[status(thm)],[f218,f219])).
% 7.14/1.54 fof(f221,plain,(
% 7.14/1.54 ![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)))))))),
% 7.14/1.54 inference(NNF_transformation,[status(thm)],[f220])).
% 7.14/1.54 fof(f222,plain,(
% 7.14/1.54 (![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)))))))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f221])).
% 7.14/1.54 fof(f223,plain,(
% 7.14/1.54 (![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,sK20_skl(X0))&~conditionhyper(sK20_skl(X0)))))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(X1,sK20_skl(X0))],[f222])).
% 7.14/1.54 fof(f224,plain,(
% 7.14/1.54 ![X0]: (~sP6_prd(X0)|sP9_prd(X0)|sP10_prd(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f223])).
% 7.14/1.54 fof(f243,definition,(
% 7.14/1.54 ![X0]: (sP11_prd(X0)<=>((((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 7.14/1.54 fof(f244,plain,(
% 7.14/1.54 ![X0]: (sP9_prd(X0)<=>(sP11_prd(X0)|((((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 7.14/1.54 inference(formula_renaming,[status(thm)],[f217,f243])).
% 7.14/1.54 fof(f245,definition,(
% 7.14/1.54 ![X0]: (sP12_prd(X0)<=>(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0)))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 7.14/1.54 fof(f246,plain,(
% 7.14/1.54 ![X0]: (sP9_prd(X0)<=>(sP11_prd(X0)|(sP12_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 7.14/1.54 inference(formula_renaming,[status(thm)],[f244,f245])).
% 7.14/1.54 fof(f247,plain,(
% 7.14/1.54 ![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)))))))),
% 7.14/1.54 inference(NNF_transformation,[status(thm)],[f246])).
% 7.14/1.54 fof(f248,plain,(
% 7.14/1.54 (![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)))))))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f247])).
% 7.14/1.54 fof(f249,plain,(
% 7.14/1.54 (![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,sK23_skl(X0))&~conditionhyper(sK23_skl(X0)))))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(X1,sK23_skl(X0))],[f248])).
% 7.14/1.54 fof(f250,plain,(
% 7.14/1.54 ![X0]: (~sP9_prd(X0)|sP11_prd(X0)|sP12_prd(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f249])).
% 7.14/1.54 fof(f255,definition,(
% 7.14/1.54 ![X0]: (sP13_prd(X0)<=>(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0)))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 7.14/1.54 fof(f256,plain,(
% 7.14/1.54 ![X0]: (sP10_prd(X0)<=>(sP13_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1)))))),
% 7.14/1.54 inference(formula_renaming,[status(thm)],[f219,f255])).
% 7.14/1.54 fof(f257,plain,(
% 7.14/1.54 ![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))))))),
% 7.14/1.54 inference(NNF_transformation,[status(thm)],[f256])).
% 7.14/1.54 fof(f258,plain,(
% 7.14/1.54 (![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))))))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f257])).
% 7.14/1.54 fof(f259,plain,(
% 7.14/1.54 (![X0]: (~sP10_prd(X0)|(sP13_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1))))))&(![X0]: (sP10_prd(X0)|(~sP13_prd(X0)|(~gt(X0,sK24_skl(X0))&~bsecretioni(sK24_skl(X0))))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(X1,sK24_skl(X0))],[f258])).
% 7.14/1.54 fof(f260,plain,(
% 7.14/1.54 ![X0]: (~sP10_prd(X0)|sP13_prd(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f259])).
% 7.14/1.54 fof(f264,definition,(
% 7.14/1.54 ![X0]: (sP14_prd(X0)<=>(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0)))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 7.14/1.54 fof(f265,plain,(
% 7.14/1.54 ![X0]: (sP11_prd(X0)<=>(sP14_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))),
% 7.14/1.54 inference(formula_renaming,[status(thm)],[f243,f264])).
% 7.14/1.54 fof(f266,plain,(
% 7.14/1.54 ![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))))))),
% 7.14/1.54 inference(NNF_transformation,[status(thm)],[f265])).
% 7.14/1.54 fof(f267,plain,(
% 7.14/1.54 (![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))))))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f266])).
% 7.14/1.54 fof(f268,plain,(
% 7.14/1.54 (![X0]: (~sP11_prd(X0)|(sP14_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))&(![X0]: (sP11_prd(X0)|(~sP14_prd(X0)|(gt(X0,sK25_skl(X0))&~conditionhyper(sK25_skl(X0))))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(X1,sK25_skl(X0))],[f267])).
% 7.14/1.54 fof(f269,plain,(
% 7.14/1.54 ![X0]: (~sP11_prd(X0)|sP14_prd(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f268])).
% 7.14/1.54 fof(f273,plain,(
% 7.14/1.54 ![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))))),
% 7.14/1.54 inference(NNF_transformation,[status(thm)],[f245])).
% 7.14/1.54 fof(f274,plain,(
% 7.14/1.54 (![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))))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f273])).
% 7.14/1.54 fof(f275,plain,(
% 7.14/1.54 (![X0]: (~sP12_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))))&(![X0]: (sP12_prd(X0)|(((~gt(X0,sK26_skl(X0))&releaselg(sK26_skl(X0)))|~bcapacitysn(X0))|qilt27(X0))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(X1,sK26_skl(X0))],[f274])).
% 7.14/1.54 fof(f277,plain,(
% 7.14/1.54 ![X0]: (~sP12_prd(X0)|bcapacitysn(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f275])).
% 7.14/1.54 fof(f281,plain,(
% 7.14/1.54 ![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))))),
% 7.14/1.54 inference(NNF_transformation,[status(thm)],[f255])).
% 7.14/1.54 fof(f282,plain,(
% 7.14/1.54 (![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))))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f281])).
% 7.14/1.54 fof(f283,plain,(
% 7.14/1.54 (![X0]: (~sP13_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))))&(![X0]: (sP13_prd(X0)|(((~gt(X0,sK27_skl(X0))&releaselg(sK27_skl(X0)))&(~gt(X0,sK28_skl(X0))&~uptakepg(sK28_skl(X0))))|~bcapacityne(X0))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl]),skolemize(X1,sK27_skl(X0)),skolemize(X1,sK28_skl(X0))],[f282])).
% 7.14/1.54 fof(f284,plain,(
% 7.14/1.54 ![X0,X1,X2]: (~sP13_prd(X0)|gt(X0,X1)|~releaselg(X1)|gt(X0,X2)|uptakepg(X2))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f283])).
% 7.14/1.54 fof(f290,plain,(
% 7.14/1.54 ![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))))),
% 7.14/1.54 inference(NNF_transformation,[status(thm)],[f264])).
% 7.14/1.54 fof(f291,plain,(
% 7.14/1.54 (![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))))),
% 7.14/1.54 inference(miniscoping,[status(thm)],[f290])).
% 7.14/1.54 fof(f292,plain,(
% 7.14/1.54 (![X0]: (~sP14_prd(X0)|(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))))&(![X0]: (sP14_prd(X0)|(((~gt(X0,sK29_skl(X0))&~bsecretioni(sK29_skl(X0)))|~bcapacitysn(X0))|~qilt27(X0))))),
% 7.14/1.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(X1,sK29_skl(X0))],[f291])).
% 7.14/1.54 fof(f294,plain,(
% 7.14/1.54 ![X0]: (~sP14_prd(X0)|bcapacitysn(X0))),
% 7.14/1.54 inference(cnf_transformation,[status(thm)],[f292])).
% 7.14/1.54 fof(f303,plain,(
% 7.14/1.54 conditionnormo(n0)),
% 7.14/1.54 inference(resolution,[status(thm)],[f43,f171])).
% 7.14/1.54 fof(f355,plain,(
% 7.14/1.54 ![X0]: (bcapacitysn(X0)|~sP11_prd(X0))),
% 7.14/1.54 inference(resolution,[status(thm)],[f294,f269])).
% 7.14/1.54 fof(f358,definition,(
% 7.14/1.54 sQ10_spl <=> (qilt27(n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f360,plain,(
% 7.14/1.54 ~qilt27(n0)|sQ10_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f358])).
% 7.14/1.54 fof(f365,plain,(
% 7.14/1.54 $false|sQ10_spl),
% 7.14/1.54 inference(forward_subsumption_resolution,[status(thm)],[f360,f170])).
% 7.14/1.54 fof(f366,plain,(
% 7.14/1.54 sQ10_spl),
% 7.14/1.54 inference(contradiction_clause,[status(thm)],[f365])).
% 7.14/1.54 fof(f368,definition,(
% 7.14/1.54 sQ12_spl <=> (drugbg(n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f369,plain,(
% 7.14/1.54 drugbg(n0)|~sQ12_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f368])).
% 7.14/1.54 fof(f370,plain,(
% 7.14/1.54 ~drugbg(n0)|sQ12_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f368])).
% 7.14/1.54 fof(f1010,plain,(
% 7.14/1.54 ![X0]: (releaselg(X0)|uptakelg(X0))),
% 7.14/1.54 inference(resolution,[status(thm)],[f138,f43])).
% 7.14/1.54 fof(f1051,plain,(
% 7.14/1.54 ![X0]: (sP5_prd(sK7_skl(n0),n0)|sP6_prd(n0)|uptakelg(X0)|conditionhyper(X0))),
% 7.14/1.54 inference(resolution,[status(thm)],[f108,f168])).
% 7.14/1.54 fof(f1056,definition,(
% 7.14/1.54 sQ66_spl <=> (sP5_prd(sK7_skl(n0),n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1057,plain,(
% 7.14/1.54 sP5_prd(sK7_skl(n0),n0)|~sQ66_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1056])).
% 7.14/1.54 fof(f1059,definition,(
% 7.14/1.54 sQ67_spl <=> (sP6_prd(n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1060,plain,(
% 7.14/1.54 sP6_prd(n0)|~sQ67_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1059])).
% 7.14/1.54 fof(f1064,definition,(
% 7.14/1.54 ![X0]: (sQ68_spl <=> (uptakelg(X0)|conditionhyper(X0)))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1065,plain,(
% 7.14/1.54 ![X0]: (uptakelg(X0)|conditionhyper(X0)|~sQ68_spl)),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1064])).
% 7.14/1.54 fof(f1067,plain,(
% 7.14/1.54 sQ66_spl|sQ67_spl|sQ68_spl),
% 7.14/1.54 inference(split_clause,[status(thm)],[f1051,f1056,f1059,f1064])).
% 7.14/1.54 fof(f1090,plain,(
% 7.14/1.54 sP9_prd(n0)|sP10_prd(n0)|~sQ67_spl),
% 7.14/1.54 inference(resolution,[status(thm)],[f1060,f224])).
% 7.14/1.54 fof(f1091,definition,(
% 7.14/1.54 sQ72_spl <=> (sP9_prd(n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1092,plain,(
% 7.14/1.54 sP9_prd(n0)|~sQ72_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1091])).
% 7.14/1.54 fof(f1094,definition,(
% 7.14/1.54 sQ73_spl <=> (sP10_prd(n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1095,plain,(
% 7.14/1.54 sP10_prd(n0)|~sQ73_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1094])).
% 7.14/1.54 fof(f1097,plain,(
% 7.14/1.54 sQ72_spl|sQ73_spl|~sQ67_spl),
% 7.14/1.54 inference(split_clause,[status(thm)],[f1090,f1091,f1094,f1059])).
% 7.14/1.54 fof(f1099,plain,(
% 7.14/1.54 sP11_prd(n0)|sP12_prd(n0)|~sQ72_spl),
% 7.14/1.54 inference(resolution,[status(thm)],[f1092,f250])).
% 7.14/1.54 fof(f1101,definition,(
% 7.14/1.54 sQ74_spl <=> (sP11_prd(n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1102,plain,(
% 7.14/1.54 sP11_prd(n0)|~sQ74_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1101])).
% 7.14/1.54 fof(f1104,definition,(
% 7.14/1.54 sQ75_spl <=> (sP12_prd(n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1105,plain,(
% 7.14/1.54 sP12_prd(n0)|~sQ75_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1104])).
% 7.14/1.54 fof(f1107,plain,(
% 7.14/1.54 sQ74_spl|sQ75_spl|~sQ72_spl),
% 7.14/1.54 inference(split_clause,[status(thm)],[f1099,f1101,f1104,f1091])).
% 7.14/1.54 fof(f1109,plain,(
% 7.14/1.54 bcapacitysn(n0)|~sQ75_spl),
% 7.14/1.54 inference(resolution,[status(thm)],[f1105,f277])).
% 7.14/1.54 fof(f1111,plain,(
% 7.14/1.54 $false|~sQ75_spl),
% 7.14/1.54 inference(forward_subsumption_resolution,[status(thm)],[f1109,f169])).
% 7.14/1.54 fof(f1112,plain,(
% 7.14/1.54 ~sQ75_spl),
% 7.14/1.54 inference(contradiction_clause,[status(thm)],[f1111])).
% 7.14/1.54 fof(f1114,plain,(
% 7.14/1.54 bcapacitysn(n0)|~sQ74_spl),
% 7.14/1.54 inference(resolution,[status(thm)],[f1102,f355])).
% 7.14/1.54 fof(f1116,plain,(
% 7.14/1.54 $false|~sQ74_spl),
% 7.14/1.54 inference(forward_subsumption_resolution,[status(thm)],[f1114,f169])).
% 7.14/1.54 fof(f1117,plain,(
% 7.14/1.54 ~sQ74_spl),
% 7.14/1.54 inference(contradiction_clause,[status(thm)],[f1116])).
% 7.14/1.54 fof(f1257,definition,(
% 7.14/1.54 sQ81_spl <=> (s2(n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1258,plain,(
% 7.14/1.54 s2(n0)|~sQ81_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1257])).
% 7.14/1.54 fof(f1260,definition,(
% 7.14/1.54 sQ82_spl <=> (s3(n0))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1261,plain,(
% 7.14/1.54 s3(n0)|~sQ82_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1260])).
% 7.14/1.54 fof(f1265,definition,(
% 7.14/1.54 ![X0]: (sQ83_spl <=> (gt(n0,X0)|drugi(X0)))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1266,plain,(
% 7.14/1.54 ![X0]: (gt(n0,X0)|drugi(X0)|~sQ83_spl)),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1265])).
% 7.14/1.54 fof(f1274,plain,(
% 7.14/1.54 ~s1(n0)|~sQ82_spl),
% 7.14/1.54 inference(resolution,[status(thm)],[f1261,f101])).
% 7.14/1.54 fof(f1295,plain,(
% 7.14/1.54 drugi(n0)|~sQ83_spl),
% 7.14/1.54 inference(resolution,[status(thm)],[f1266,f43])).
% 7.14/1.54 fof(f1321,definition,(
% 7.14/1.54 ![X0]: (sQ91_spl <=> (uptakepg(X0)|gt(n0,X0)))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1322,plain,(
% 7.14/1.54 ![X0]: (uptakepg(X0)|gt(n0,X0)|~sQ91_spl)),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1321])).
% 7.14/1.54 fof(f1331,plain,(
% 7.14/1.54 ![X0]: (~sP5_prd(X0,n0)|conditionnormo(X0))),
% 7.14/1.54 inference(resolution,[status(thm)],[f214,f171])).
% 7.14/1.54 fof(f1332,plain,(
% 7.14/1.54 $false|~sQ66_spl),
% 7.14/1.54 inference(backward_subsumption_resolution,[status(thm)],[f1057,f1333])).
% 7.14/1.54 fof(f1333,plain,(
% 7.14/1.54 ![X0]: (~sP5_prd(X0,n0))),
% 7.14/1.54 inference(forward_subsumption_resolution,[status(thm)],[f1331,f215])).
% 7.14/1.54 fof(f1334,plain,(
% 7.14/1.54 ~sQ66_spl),
% 7.14/1.54 inference(contradiction_clause,[status(thm)],[f1332])).
% 7.14/1.54 fof(f1340,plain,(
% 7.14/1.54 s3(n0)|~sQ83_spl),
% 7.14/1.54 inference(resolution,[status(thm)],[f1295,f129])).
% 7.14/1.54 fof(f1344,plain,(
% 7.14/1.54 ~s1(n0)|~sQ83_spl),
% 7.14/1.54 inference(resolution,[status(thm)],[f1340,f101])).
% 7.14/1.54 fof(f1346,plain,(
% 7.14/1.54 $false|~sQ83_spl),
% 7.14/1.54 inference(forward_subsumption_resolution,[status(thm)],[f1344,f167])).
% 7.14/1.54 fof(f1347,plain,(
% 7.14/1.54 ~sQ83_spl),
% 7.14/1.54 inference(contradiction_clause,[status(thm)],[f1346])).
% 7.14/1.54 fof(f1415,plain,(
% 7.14/1.54 ![X0]: (uptakepg(sK9_skl(n0))|gt(n0,X0)|drugi(X0)|~sQ91_spl)),
% 7.14/1.54 inference(resolution,[status(thm)],[f1322,f134])).
% 7.14/1.54 fof(f1424,definition,(
% 7.14/1.54 sQ103_spl <=> (uptakepg(sK9_skl(n0)))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1425,plain,(
% 7.14/1.54 uptakepg(sK9_skl(n0))|~sQ103_spl),
% 7.14/1.54 inference(component_clause,[status(thm)],[f1424])).
% 7.14/1.54 fof(f1427,plain,(
% 7.14/1.54 sQ103_spl|sQ83_spl|~sQ91_spl),
% 7.14/1.54 inference(split_clause,[status(thm)],[f1415,f1424,f1265,f1321])).
% 7.14/1.54 fof(f1482,plain,(
% 7.14/1.54 ![X0]: (gt(n0,X0)|drugi(X0)|~sQ103_spl)),
% 7.14/1.54 inference(resolution,[status(thm)],[f1425,f135])).
% 7.14/1.54 fof(f1484,plain,(
% 7.14/1.54 sQ83_spl|~sQ103_spl),
% 7.14/1.54 inference(split_clause,[status(thm)],[f1482,f1265,f1424])).
% 7.14/1.54 fof(f1495,definition,(
% 7.14/1.54 ![X0]: (sQ113_spl <=> (uptakelg(X0)|gt(n0,X0)))),
% 7.14/1.54 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 7.14/1.54 fof(f1496,plain,(
% 7.14/1.54 ![X0]: (uptakelg(X0)|gt(n0,X0)|~sQ113_spl)),
% 7.14/1.55 inference(component_clause,[status(thm)],[f1495])).
% 7.14/1.55 fof(f1574,plain,(
% 7.14/1.55 ![X0]: (gt(n0,X0)|drugbg(X0)|conditionnormo(sK11_skl(n0)))),
% 7.14/1.55 inference(resolution,[status(thm)],[f147,f171])).
% 7.14/1.55 fof(f1576,definition,(
% 7.14/1.55 ![X0]: (sQ124_spl <=> (gt(n0,X0)|drugbg(X0)))),
% 7.14/1.55 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 7.14/1.55 fof(f1577,plain,(
% 7.14/1.55 ![X0]: (gt(n0,X0)|drugbg(X0)|~sQ124_spl)),
% 7.14/1.55 inference(component_clause,[status(thm)],[f1576])).
% 7.14/1.55 fof(f1579,definition,(
% 7.14/1.55 sQ125_spl <=> (conditionnormo(sK11_skl(n0)))),
% 7.14/1.55 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 7.14/1.55 fof(f1580,plain,(
% 7.14/1.55 conditionnormo(sK11_skl(n0))|~sQ125_spl),
% 7.14/1.55 inference(component_clause,[status(thm)],[f1579])).
% 7.14/1.55 fof(f1582,plain,(
% 7.14/1.55 sQ124_spl|sQ125_spl),
% 7.14/1.55 inference(split_clause,[status(thm)],[f1574,f1576,f1579])).
% 7.14/1.55 fof(f1583,plain,(
% 7.14/1.55 ![X0]: (releaselg(sK11_skl(n0))|drugbg(X0)|conditionhyper(X0))),
% 7.14/1.55 inference(resolution,[status(thm)],[f148,f168])).
% 7.14/1.55 fof(f1595,definition,(
% 7.14/1.55 sQ126_spl <=> (releaselg(sK11_skl(n0)))),
% 7.14/1.55 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 7.14/1.55 fof(f1596,plain,(
% 7.14/1.55 releaselg(sK11_skl(n0))|~sQ126_spl),
% 7.14/1.55 inference(component_clause,[status(thm)],[f1595])).
% 7.14/1.55 fof(f1598,definition,(
% 7.14/1.55 ![X0]: (sQ127_spl <=> (drugbg(X0)|conditionhyper(X0)))),
% 7.14/1.55 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 7.14/1.55 fof(f1599,plain,(
% 7.14/1.55 ![X0]: (drugbg(X0)|conditionhyper(X0)|~sQ127_spl)),
% 7.14/1.55 inference(component_clause,[status(thm)],[f1598])).
% 7.14/1.55 fof(f1601,plain,(
% 7.14/1.55 sQ126_spl|sQ127_spl),
% 7.14/1.55 inference(split_clause,[status(thm)],[f1583,f1595,f1598])).
% 7.14/1.55 fof(f1617,plain,(
% 7.14/1.55 ~qilt27(n0)|s2(n0)|s3(n0)|~sQ12_spl),
% 7.14/1.55 inference(resolution,[status(thm)],[f369,f124])).
% 7.14/1.55 fof(f1619,plain,(
% 7.14/1.55 ~sQ10_spl|sQ81_spl|sQ82_spl|~sQ12_spl),
% 7.14/1.55 inference(split_clause,[status(thm)],[f1617,f358,f1257,f1260,f368])).
% 7.14/1.55 fof(f1621,plain,(
% 7.14/1.55 $false|~sQ82_spl),
% 7.14/1.55 inference(forward_subsumption_resolution,[status(thm)],[f1274,f167])).
% 7.14/1.55 fof(f1622,plain,(
% 7.14/1.55 ~sQ82_spl),
% 7.14/1.55 inference(contradiction_clause,[status(thm)],[f1621])).
% 7.14/1.55 fof(f1626,plain,(
% 7.14/1.55 ~s1(n0)|~sQ81_spl),
% 7.14/1.55 inference(resolution,[status(thm)],[f1258,f100])).
% 7.14/1.55 fof(f1627,plain,(
% 7.14/1.55 $false|~sQ81_spl),
% 7.14/1.55 inference(forward_subsumption_resolution,[status(thm)],[f1626,f167])).
% 7.14/1.55 fof(f1628,plain,(
% 7.14/1.55 ~sQ81_spl),
% 7.14/1.55 inference(contradiction_clause,[status(thm)],[f1627])).
% 7.14/1.55 fof(f1675,plain,(
% 7.14/1.55 ![X0]: (gt(X0,sK11_skl(n0))|~uptakelg(sK11_skl(n0))|~sQ126_spl)),
% 7.14/1.55 inference(resolution,[status(thm)],[f1596,f63])).
% 7.14/1.55 fof(f1676,definition,(
% 7.14/1.55 ![X0]: (sQ136_spl <=> (gt(X0,sK11_skl(n0))))),
% 7.14/1.55 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 7.14/1.55 fof(f1677,plain,(
% 7.14/1.55 ![X0]: (gt(X0,sK11_skl(n0))|~sQ136_spl)),
% 7.14/1.55 inference(component_clause,[status(thm)],[f1676])).
% 7.14/1.55 fof(f1679,definition,(
% 7.14/1.55 sQ137_spl <=> (uptakelg(sK11_skl(n0)))),
% 7.14/1.55 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 7.14/1.55 fof(f1681,plain,(
% 7.14/1.55 ~uptakelg(sK11_skl(n0))|sQ137_spl),
% 7.14/1.55 inference(component_clause,[status(thm)],[f1679])).
% 7.14/1.55 fof(f1682,plain,(
% 7.14/1.55 sQ136_spl|~sQ137_spl|~sQ126_spl),
% 7.14/1.55 inference(split_clause,[status(thm)],[f1675,f1676,f1679,f1595])).
% 7.14/1.55 fof(f1683,plain,(
% 7.14/1.55 conditionhyper(n0)|~sQ127_spl|sQ12_spl),
% 7.14/1.55 inference(resolution,[status(thm)],[f1599,f370])).
% 7.14/1.55 fof(f1715,plain,(
% 7.14/1.55 ~conditionnormo(n0)|~sQ127_spl|sQ12_spl),
% 7.14/1.55 inference(resolution,[status(thm)],[f1683,f53])).
% 7.14/1.55 fof(f1716,plain,(
% 7.14/1.55 $false|~sQ127_spl|sQ12_spl),
% 7.14/1.55 inference(forward_subsumption_resolution,[status(thm)],[f1715,f303])).
% 7.14/1.55 fof(f1717,plain,(
% 7.14/1.55 ~sQ127_spl|sQ12_spl),
% 7.14/1.55 inference(contradiction_clause,[status(thm)],[f1716])).
% 7.14/1.55 fof(f1889,plain,(
% 7.14/1.55 ![X0]: (drugbg(X0)|conditionhyper(X0)|~sQ124_spl)),
% 7.14/1.55 inference(resolution,[status(thm)],[f1577,f168])).
% 7.14/1.55 fof(f1903,plain,(
% 7.14/1.55 sQ127_spl|~sQ124_spl),
% 7.14/1.55 inference(split_clause,[status(thm)],[f1889,f1598,f1576])).
% 7.14/1.55 fof(f3089,plain,(
% 7.14/1.55 conditionhyper(sK11_skl(n0))|~sQ68_spl|sQ137_spl),
% 7.14/1.55 inference(resolution,[status(thm)],[f1065,f1681])).
% 7.14/1.55 fof(f3737,definition,(
% 7.14/1.55 sQ390_spl <=> (sP13_prd(n0))),
% 7.14/1.55 introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition])).
% 7.14/1.55 fof(f3738,plain,(
% 7.14/1.55 sP13_prd(n0)|~sQ390_spl),
% 7.14/1.55 inference(component_clause,[status(thm)],[f3737])).
% 7.14/1.55 fof(f3739,plain,(
% 7.14/1.55 ~sP13_prd(n0)|sQ390_spl),
% 7.14/1.55 inference(component_clause,[status(thm)],[f3737])).
% 7.14/1.55 fof(f3749,plain,(
% 7.14/1.55 ![X0,X1]: (gt(n0,X0)|~releaselg(X0)|gt(n0,X1)|uptakepg(X1)|~sQ390_spl)),
% 7.14/1.55 inference(resolution,[status(thm)],[f3738,f284])).
% 7.14/1.55 fof(f3752,definition,(
% 7.14/1.55 ![X0]: (sQ393_spl <=> (gt(n0,X0)|~releaselg(X0)))),
% 7.14/1.55 introduced(definition,[new_symbols(definition,[sQ393_spl])],[split_symbol_definition])).
% 7.14/1.55 fof(f3753,plain,(
% 7.14/1.55 ![X0]: (gt(n0,X0)|~releaselg(X0)|~sQ393_spl)),
% 7.14/1.55 inference(component_clause,[status(thm)],[f3752])).
% 7.14/1.55 fof(f3755,plain,(
% 7.14/1.55 sQ393_spl|sQ91_spl|~sQ390_spl),
% 7.14/1.55 inference(split_clause,[status(thm)],[f3749,f3752,f1321,f3737])).
% 7.14/1.55 fof(f3799,plain,(
% 7.14/1.55 $false|~sQ136_spl),
% 7.14/1.55 inference(resolution,[status(thm)],[f1677,f43])).
% 7.14/1.55 fof(f3871,plain,(
% 7.14/1.55 ~sQ136_spl),
% 7.14/1.55 inference(contradiction_clause,[status(thm)],[f3799])).
% 7.14/1.55 fof(f3949,definition,(
% 7.14/1.55 sQ421_spl <=> (sP14_prd(n0))),
% 7.14/1.55 introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition])).
% 7.14/1.55 fof(f3950,plain,(
% 7.14/1.55 sP14_prd(n0)|~sQ421_spl),
% 7.14/1.55 inference(component_clause,[status(thm)],[f3949])).
% 7.14/1.55 fof(f3958,plain,(
% 7.14/1.55 bcapacitysn(n0)|~sQ421_spl),
% 7.14/1.55 inference(resolution,[status(thm)],[f3950,f294])).
% 7.14/1.55 fof(f3963,plain,(
% 7.14/1.55 $false|~sQ421_spl),
% 7.14/1.55 inference(forward_subsumption_resolution,[status(thm)],[f3958,f169])).
% 7.14/1.55 fof(f3964,plain,(
% 7.14/1.55 ~sQ421_spl),
% 7.14/1.55 inference(contradiction_clause,[status(thm)],[f3963])).
% 7.14/1.55 fof(f4370,plain,(
% 7.14/1.55 ![X0]: (gt(n0,X0)|uptakelg(X0)|~sQ393_spl)),
% 7.14/1.55 inference(resolution,[status(thm)],[f3753,f1010])).
% 7.14/1.55 fof(f4374,plain,(
% 7.14/1.55 ![X0]: (uptakelg(X0)|conditionhyper(X0)|~sQ113_spl)),
% 7.14/1.55 inference(resolution,[status(thm)],[f1496,f168])).
% 7.14/1.55 fof(f4388,plain,(
% 7.14/1.55 sQ68_spl|~sQ113_spl),
% 7.14/1.55 inference(split_clause,[status(thm)],[f4374,f1064,f1495])).
% 7.14/1.55 fof(f4410,plain,(
% 7.14/1.55 ~conditionnormo(sK11_skl(n0))|~sQ68_spl|sQ137_spl),
% 7.14/1.55 inference(resolution,[status(thm)],[f3089,f53])).
% 7.14/1.55 fof(f4411,plain,(
% 7.14/1.55 $false|~sQ125_spl|~sQ68_spl|sQ137_spl),
% 7.14/1.55 inference(forward_subsumption_resolution,[status(thm)],[f4410,f1580])).
% 7.14/1.55 fof(f4412,plain,(
% 7.14/1.55 ~sQ125_spl|~sQ68_spl|sQ137_spl),
% 7.14/1.55 inference(contradiction_clause,[status(thm)],[f4411])).
% 7.14/1.55 fof(f4413,plain,(
% 7.14/1.55 sQ113_spl|~sQ393_spl),
% 7.14/1.55 inference(split_clause,[status(thm)],[f4370,f1495,f3752])).
% 7.14/1.55 fof(f4431,plain,(
% 7.14/1.55 ~sP10_prd(n0)|sQ390_spl),
% 7.14/1.55 inference(resolution,[status(thm)],[f3739,f260])).
% 7.14/1.55 fof(f4432,plain,(
% 7.14/1.55 $false|~sQ73_spl|sQ390_spl),
% 7.14/1.55 inference(forward_subsumption_resolution,[status(thm)],[f4431,f1095])).
% 7.14/1.55 fof(f4433,plain,(
% 7.14/1.55 ~sQ73_spl|sQ390_spl),
% 7.14/1.55 inference(contradiction_clause,[status(thm)],[f4432])).
% 7.14/1.55 fof(f4434,plain,(
% 7.14/1.55 $false),
% 7.14/1.55 inference(sat_refutation,[status(thm)],[f366,f1067,f1097,f1107,f1112,f1117,f1334,f1347,f1427,f1484,f1582,f1601,f1619,f1622,f1628,f1682,f1717,f1903,f3755,f3871,f3964,f4388,f4412,f4413,f4433])).
% 7.14/1.55 % SZS output end CNFRefutation for theBenchmark.p
% 7.14/1.58 % Elapsed time: 1.206328 seconds
% 7.14/1.58 % CPU time: 9.156853 seconds
% 7.14/1.58 % Total memory used: 71.277 MB
% 7.14/1.58 % Net memory used: 64.170 MB
%------------------------------------------------------------------------------