%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MED008+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 : n026.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 39.48s 5.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED008+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n026.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 21 01:22:54 UTC 2026
% 0.08/0.38 % CPUTime :
% 0.13/0.39 % Drodi V4.1.1
% 39.48/5.50 % Refutation found
% 39.48/5.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 39.48/5.50 % SZS output start CNFRefutation for theBenchmark
% 39.48/5.50 fof(f1,axiom,(
% 39.48/5.50 (! [X] : ~ gt(X,X) )),
% 39.48/5.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.48/5.50 fof(f9,axiom,(
% 39.48/5.50 (! [X0] :( ~ conditionhyper(X0)| ~ conditionnormo(X0) ) )),
% 39.48/5.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.48/5.50 fof(f24,axiom,(
% 39.48/5.50 (! [X0] :( ~ s1(X0)| ~ s3(X0) ) )),
% 39.48/5.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.48/5.50 fof(f26,axiom,(
% 39.48/5.50 (! [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) ) )) ) ) )),
% 39.48/5.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.48/5.50 fof(f33,axiom,(
% 39.48/5.50 (! [X0] :( drugi(X0)=> s3(X0) ) )),
% 39.48/5.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.48/5.50 fof(f34,axiom,(
% 39.48/5.50 (! [X0] :( ( (! [X1] :( ~ gt(X0,X1)=> uptakelg(X1) ))| (! [X1] :( ~ gt(X0,X1)=> uptakepg(X1) ) ))=> (! [X1] :( ~ gt(X0,X1)=> drugi(X1) ) )) )),
% 39.48/5.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.48/5.50 fof(f35,axiom,(
% 39.48/5.50 (! [X0,X1] :( ~ gt(X0,X1)=> ( ~ releaselg(X1)=> uptakelg(X1) ) ) )),
% 39.48/5.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.48/5.50 fof(f41,conjecture,(
% 39.48/5.50 ( ( s1(n0)& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ))& ~ bcapacitysn(n0)& ~ qilt27(n0) )=> ~ (! [X0] :( ~ gt(n0,X0)=> conditionnormo(X0) ) )) ),
% 39.48/5.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 39.48/5.50 fof(f42,negated_conjecture,(
% 39.48/5.50 ~(( ( s1(n0)& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ))& ~ bcapacitysn(n0)& ~ qilt27(n0) )=> ~ (! [X0] :( ~ gt(n0,X0)=> conditionnormo(X0) ) )) )),
% 39.48/5.50 inference(negated_conjecture,[status(cth)],[f41])).
% 39.48/5.50 fof(f43,plain,(
% 39.48/5.50 ![X0]: (~gt(X0,X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f1])).
% 39.48/5.50 fof(f53,plain,(
% 39.48/5.50 ![X0]: (~conditionhyper(X0)|~conditionnormo(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f9])).
% 39.48/5.50 fof(f101,plain,(
% 39.48/5.50 ![X0]: (~s1(X0)|~s3(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f24])).
% 39.48/5.50 fof(f103,plain,(
% 39.48/5.50 ![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))))))),
% 39.48/5.50 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 39.48/5.50 fof(f104,definition,(
% 39.48/5.50 ![X0,X1]: (sP5_prd(X1,X0)<=>(~gt(X0,X1)&~conditionnormo(X1)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 39.48/5.50 fof(f105,definition,(
% 39.48/5.50 ![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))))))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 39.48/5.50 fof(f106,plain,(
% 39.48/5.50 ![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))))))),
% 39.48/5.50 inference(formula_renaming,[status(thm)],[f103,f105,f104])).
% 39.48/5.50 fof(f107,plain,(
% 39.48/5.50 ![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))))))),
% 39.48/5.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X1,sK7_skl(X0))],[f106])).
% 39.48/5.50 fof(f108,plain,(
% 39.48/5.50 ![X0,X1]: (sP5_prd(sK7_skl(X0),X0)|sP6_prd(X0)|gt(X0,X1)|uptakelg(X1))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f107])).
% 39.48/5.50 fof(f128,plain,(
% 39.48/5.50 ![X0]: (~drugi(X0)|s3(X0))),
% 39.48/5.50 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 39.48/5.50 fof(f129,plain,(
% 39.48/5.50 ![X0]: (~drugi(X0)|s3(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f128])).
% 39.48/5.50 fof(f130,plain,(
% 39.48/5.50 ![X0]: (((?[X1]: (~gt(X0,X1)&~uptakelg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|(![X1]: (gt(X0,X1)|drugi(X1))))),
% 39.48/5.50 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 39.48/5.50 fof(f131,plain,(
% 39.48/5.50 ![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))))),
% 39.48/5.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(X1,sK8_skl(X0)),skolemize(X1,sK9_skl(X0))],[f130])).
% 39.48/5.50 fof(f132,plain,(
% 39.48/5.50 ![X0,X1]: (~gt(X0,sK8_skl(X0))|gt(X0,X1)|drugi(X1))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f131])).
% 39.48/5.50 fof(f133,plain,(
% 39.48/5.50 ![X0,X1]: (~uptakelg(sK8_skl(X0))|gt(X0,X1)|drugi(X1))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f131])).
% 39.48/5.50 fof(f134,plain,(
% 39.48/5.50 ![X0,X1]: (~gt(X0,sK9_skl(X0))|gt(X0,X1)|drugi(X1))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f131])).
% 39.48/5.50 fof(f135,plain,(
% 39.48/5.50 ![X0,X1]: (~uptakepg(sK9_skl(X0))|gt(X0,X1)|drugi(X1))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f131])).
% 39.48/5.50 fof(f136,plain,(
% 39.48/5.50 ![X0,X1]: (gt(X0,X1)|(releaselg(X1)|uptakelg(X1)))),
% 39.48/5.50 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 39.48/5.50 fof(f137,plain,(
% 39.48/5.50 ![X1]: ((![X0]: gt(X0,X1))|(releaselg(X1)|uptakelg(X1)))),
% 39.48/5.50 inference(miniscoping,[status(thm)],[f136])).
% 39.48/5.50 fof(f138,plain,(
% 39.48/5.50 ![X0,X1]: (gt(X0,X1)|releaselg(X1)|uptakelg(X1))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f137])).
% 39.48/5.50 fof(f166,plain,(
% 39.48/5.50 ((((s1(n0)&(![X0]: (~gt(n0,X0)|conditionhyper(X0))))&~bcapacitysn(n0))&~qilt27(n0))&(![X0]: (gt(n0,X0)|conditionnormo(X0))))),
% 39.48/5.50 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 39.48/5.50 fof(f167,plain,(
% 39.48/5.50 s1(n0)),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f166])).
% 39.48/5.50 fof(f168,plain,(
% 39.48/5.50 ![X0]: (~gt(n0,X0)|conditionhyper(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f166])).
% 39.48/5.50 fof(f169,plain,(
% 39.48/5.50 ~bcapacitysn(n0)),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f166])).
% 39.48/5.50 fof(f170,plain,(
% 39.48/5.50 ~qilt27(n0)),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f166])).
% 39.48/5.50 fof(f171,plain,(
% 39.48/5.50 ![X0]: (gt(n0,X0)|conditionnormo(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f166])).
% 39.48/5.50 fof(f212,plain,(
% 39.48/5.50 ![X0,X1]: ((~sP5_prd(X1,X0)|(~gt(X0,X1)&~conditionnormo(X1)))&(sP5_prd(X1,X0)|(gt(X0,X1)|conditionnormo(X1))))),
% 39.48/5.50 inference(NNF_transformation,[status(thm)],[f104])).
% 39.48/5.50 fof(f213,plain,(
% 39.48/5.50 (![X0,X1]: (~sP5_prd(X1,X0)|(~gt(X0,X1)&~conditionnormo(X1))))&(![X0,X1]: (sP5_prd(X1,X0)|(gt(X0,X1)|conditionnormo(X1))))),
% 39.48/5.50 inference(miniscoping,[status(thm)],[f212])).
% 39.48/5.50 fof(f214,plain,(
% 39.48/5.50 ![X0,X1]: (~sP5_prd(X0,X1)|~gt(X1,X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f213])).
% 39.48/5.50 fof(f215,plain,(
% 39.48/5.50 ![X0,X1]: (~sP5_prd(X0,X1)|~conditionnormo(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f213])).
% 39.48/5.50 fof(f217,definition,(
% 39.48/5.50 ![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))))))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 39.48/5.50 fof(f218,plain,(
% 39.48/5.50 ![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))))))),
% 39.48/5.50 inference(formula_renaming,[status(thm)],[f105,f217])).
% 39.48/5.50 fof(f219,definition,(
% 39.48/5.50 ![X0]: (sP10_prd(X0)<=>((((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))&(![X1]: (gt(X0,X1)|bsecretioni(X1)))))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 39.48/5.50 fof(f220,plain,(
% 39.48/5.50 ![X0]: (sP6_prd(X0)<=>(sP9_prd(X0)|(sP10_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 39.48/5.50 inference(formula_renaming,[status(thm)],[f218,f219])).
% 39.48/5.50 fof(f221,plain,(
% 39.48/5.50 ![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)))))))),
% 39.48/5.50 inference(NNF_transformation,[status(thm)],[f220])).
% 39.48/5.50 fof(f222,plain,(
% 39.48/5.50 (![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)))))))),
% 39.48/5.50 inference(miniscoping,[status(thm)],[f221])).
% 39.48/5.50 fof(f223,plain,(
% 39.48/5.50 (![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)))))))),
% 39.48/5.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(X1,sK20_skl(X0))],[f222])).
% 39.48/5.50 fof(f224,plain,(
% 39.48/5.50 ![X0]: (~sP6_prd(X0)|sP9_prd(X0)|sP10_prd(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f223])).
% 39.48/5.50 fof(f243,definition,(
% 39.48/5.50 ![X0]: (sP11_prd(X0)<=>((((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 39.48/5.50 fof(f244,plain,(
% 39.48/5.50 ![X0]: (sP9_prd(X0)<=>(sP11_prd(X0)|((((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0))&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 39.48/5.50 inference(formula_renaming,[status(thm)],[f217,f243])).
% 39.48/5.50 fof(f245,definition,(
% 39.48/5.50 ![X0]: (sP12_prd(X0)<=>(((![X1]: (gt(X0,X1)|~releaselg(X1)))&bcapacitysn(X0))&~qilt27(X0)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 39.48/5.50 fof(f246,plain,(
% 39.48/5.50 ![X0]: (sP9_prd(X0)<=>(sP11_prd(X0)|(sP12_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1))))))),
% 39.48/5.50 inference(formula_renaming,[status(thm)],[f244,f245])).
% 39.48/5.50 fof(f247,plain,(
% 39.48/5.50 ![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)))))))),
% 39.48/5.50 inference(NNF_transformation,[status(thm)],[f246])).
% 39.48/5.50 fof(f248,plain,(
% 39.48/5.50 (![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)))))))),
% 39.48/5.50 inference(miniscoping,[status(thm)],[f247])).
% 39.48/5.50 fof(f249,plain,(
% 39.48/5.50 (![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)))))))),
% 39.48/5.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(X1,sK23_skl(X0))],[f248])).
% 39.48/5.50 fof(f250,plain,(
% 39.48/5.50 ![X0]: (~sP9_prd(X0)|sP11_prd(X0)|sP12_prd(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f249])).
% 39.48/5.50 fof(f255,definition,(
% 39.48/5.50 ![X0]: (sP13_prd(X0)<=>(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 39.48/5.50 fof(f256,plain,(
% 39.48/5.50 ![X0]: (sP10_prd(X0)<=>(sP13_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1)))))),
% 39.48/5.50 inference(formula_renaming,[status(thm)],[f219,f255])).
% 39.48/5.50 fof(f257,plain,(
% 39.48/5.50 ![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))))))),
% 39.48/5.50 inference(NNF_transformation,[status(thm)],[f256])).
% 39.48/5.50 fof(f258,plain,(
% 39.48/5.50 (![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))))))),
% 39.48/5.50 inference(miniscoping,[status(thm)],[f257])).
% 39.48/5.50 fof(f259,plain,(
% 39.48/5.50 (![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))))))),
% 39.48/5.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(X1,sK24_skl(X0))],[f258])).
% 39.48/5.50 fof(f260,plain,(
% 39.48/5.50 ![X0]: (~sP10_prd(X0)|sP13_prd(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f259])).
% 39.48/5.50 fof(f264,definition,(
% 39.48/5.50 ![X0]: (sP14_prd(X0)<=>(((![X1]: (gt(X0,X1)|bsecretioni(X1)))&bcapacitysn(X0))&qilt27(X0)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 39.48/5.50 fof(f265,plain,(
% 39.48/5.50 ![X0]: (sP11_prd(X0)<=>(sP14_prd(X0)&(![X1]: (~gt(X0,X1)|conditionhyper(X1)))))),
% 39.48/5.50 inference(formula_renaming,[status(thm)],[f243,f264])).
% 39.48/5.50 fof(f266,plain,(
% 39.48/5.50 ![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))))))),
% 39.48/5.50 inference(NNF_transformation,[status(thm)],[f265])).
% 39.48/5.50 fof(f267,plain,(
% 39.48/5.50 (![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))))))),
% 39.48/5.50 inference(miniscoping,[status(thm)],[f266])).
% 39.48/5.50 fof(f268,plain,(
% 39.48/5.50 (![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))))))),
% 39.48/5.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(X1,sK25_skl(X0))],[f267])).
% 39.48/5.50 fof(f269,plain,(
% 39.48/5.50 ![X0]: (~sP11_prd(X0)|sP14_prd(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f268])).
% 39.48/5.50 fof(f273,plain,(
% 39.48/5.50 ![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))))),
% 39.48/5.50 inference(NNF_transformation,[status(thm)],[f245])).
% 39.48/5.50 fof(f274,plain,(
% 39.48/5.50 (![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))))),
% 39.48/5.50 inference(miniscoping,[status(thm)],[f273])).
% 39.48/5.50 fof(f275,plain,(
% 39.48/5.50 (![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))))),
% 39.48/5.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(X1,sK26_skl(X0))],[f274])).
% 39.48/5.50 fof(f277,plain,(
% 39.48/5.50 ![X0]: (~sP12_prd(X0)|bcapacitysn(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f275])).
% 39.48/5.50 fof(f281,plain,(
% 39.48/5.50 ![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))))),
% 39.48/5.50 inference(NNF_transformation,[status(thm)],[f255])).
% 39.48/5.50 fof(f282,plain,(
% 39.48/5.50 (![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))))),
% 39.48/5.50 inference(miniscoping,[status(thm)],[f281])).
% 39.48/5.50 fof(f283,plain,(
% 39.48/5.50 (![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))))),
% 39.48/5.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl,sK28_skl]),skolemize(X1,sK27_skl(X0)),skolemize(X1,sK28_skl(X0))],[f282])).
% 39.48/5.50 fof(f284,plain,(
% 39.48/5.50 ![X0,X1,X2]: (~sP13_prd(X0)|gt(X0,X1)|~releaselg(X1)|gt(X0,X2)|uptakepg(X2))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f283])).
% 39.48/5.50 fof(f290,plain,(
% 39.48/5.50 ![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))))),
% 39.48/5.50 inference(NNF_transformation,[status(thm)],[f264])).
% 39.48/5.50 fof(f291,plain,(
% 39.48/5.50 (![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))))),
% 39.48/5.50 inference(miniscoping,[status(thm)],[f290])).
% 39.48/5.50 fof(f292,plain,(
% 39.48/5.50 (![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))))),
% 39.48/5.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(X1,sK29_skl(X0))],[f291])).
% 39.48/5.50 fof(f295,plain,(
% 39.48/5.50 ![X0]: (~sP14_prd(X0)|qilt27(X0))),
% 39.48/5.50 inference(cnf_transformation,[status(thm)],[f292])).
% 39.48/5.50 fof(f303,plain,(
% 39.48/5.50 conditionnormo(n0)),
% 39.48/5.50 inference(resolution,[status(thm)],[f43,f171])).
% 39.48/5.50 fof(f400,plain,(
% 39.48/5.50 ![X0]: (releaselg(X0)|uptakelg(X0))),
% 39.48/5.50 inference(resolution,[status(thm)],[f138,f43])).
% 39.48/5.50 fof(f415,plain,(
% 39.48/5.50 ![X0]: (sP5_prd(sK7_skl(n0),n0)|sP6_prd(n0)|uptakelg(X0)|conditionhyper(X0))),
% 39.48/5.50 inference(resolution,[status(thm)],[f108,f168])).
% 39.48/5.50 fof(f420,definition,(
% 39.48/5.50 sQ16_spl <=> (sP5_prd(sK7_skl(n0),n0))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f421,plain,(
% 39.48/5.50 sP5_prd(sK7_skl(n0),n0)|~sQ16_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f420])).
% 39.48/5.50 fof(f423,definition,(
% 39.48/5.50 sQ17_spl <=> (sP6_prd(n0))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f424,plain,(
% 39.48/5.50 sP6_prd(n0)|~sQ17_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f423])).
% 39.48/5.50 fof(f426,definition,(
% 39.48/5.50 ![X0]: (sQ18_spl <=> (uptakelg(X0)|conditionhyper(X0)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f427,plain,(
% 39.48/5.50 ![X0]: (uptakelg(X0)|conditionhyper(X0)|~sQ18_spl)),
% 39.48/5.50 inference(component_clause,[status(thm)],[f426])).
% 39.48/5.50 fof(f429,plain,(
% 39.48/5.50 sQ16_spl|sQ17_spl|sQ18_spl),
% 39.48/5.50 inference(split_clause,[status(thm)],[f415,f420,f423,f426])).
% 39.48/5.50 fof(f442,plain,(
% 39.48/5.50 sP9_prd(n0)|sP10_prd(n0)|~sQ17_spl),
% 39.48/5.50 inference(resolution,[status(thm)],[f424,f224])).
% 39.48/5.50 fof(f443,definition,(
% 39.48/5.50 sQ21_spl <=> (sP9_prd(n0))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f444,plain,(
% 39.48/5.50 sP9_prd(n0)|~sQ21_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f443])).
% 39.48/5.50 fof(f446,definition,(
% 39.48/5.50 sQ22_spl <=> (sP10_prd(n0))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f447,plain,(
% 39.48/5.50 sP10_prd(n0)|~sQ22_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f446])).
% 39.48/5.50 fof(f449,plain,(
% 39.48/5.50 sQ21_spl|sQ22_spl|~sQ17_spl),
% 39.48/5.50 inference(split_clause,[status(thm)],[f442,f443,f446,f423])).
% 39.48/5.50 fof(f453,plain,(
% 39.48/5.50 sP13_prd(n0)|~sQ22_spl),
% 39.48/5.50 inference(resolution,[status(thm)],[f447,f260])).
% 39.48/5.50 fof(f455,plain,(
% 39.48/5.50 sP11_prd(n0)|sP12_prd(n0)|~sQ21_spl),
% 39.48/5.50 inference(resolution,[status(thm)],[f444,f250])).
% 39.48/5.50 fof(f457,definition,(
% 39.48/5.50 sQ23_spl <=> (sP11_prd(n0))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f458,plain,(
% 39.48/5.50 sP11_prd(n0)|~sQ23_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f457])).
% 39.48/5.50 fof(f460,definition,(
% 39.48/5.50 sQ24_spl <=> (sP12_prd(n0))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f461,plain,(
% 39.48/5.50 sP12_prd(n0)|~sQ24_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f460])).
% 39.48/5.50 fof(f463,plain,(
% 39.48/5.50 sQ23_spl|sQ24_spl|~sQ21_spl),
% 39.48/5.50 inference(split_clause,[status(thm)],[f455,f457,f460,f443])).
% 39.48/5.50 fof(f472,plain,(
% 39.48/5.50 bcapacitysn(n0)|~sQ24_spl),
% 39.48/5.50 inference(resolution,[status(thm)],[f461,f277])).
% 39.48/5.50 fof(f473,plain,(
% 39.48/5.50 $false|~sQ24_spl),
% 39.48/5.50 inference(forward_subsumption_resolution,[status(thm)],[f472,f169])).
% 39.48/5.50 fof(f474,plain,(
% 39.48/5.50 ~sQ24_spl),
% 39.48/5.50 inference(contradiction_clause,[status(thm)],[f473])).
% 39.48/5.50 fof(f475,plain,(
% 39.48/5.50 sP14_prd(n0)|~sQ23_spl),
% 39.48/5.50 inference(resolution,[status(thm)],[f458,f269])).
% 39.48/5.50 fof(f503,plain,(
% 39.48/5.50 qilt27(n0)|~sQ23_spl),
% 39.48/5.50 inference(resolution,[status(thm)],[f475,f295])).
% 39.48/5.50 fof(f505,plain,(
% 39.48/5.50 $false|~sQ23_spl),
% 39.48/5.50 inference(forward_subsumption_resolution,[status(thm)],[f503,f170])).
% 39.48/5.50 fof(f506,plain,(
% 39.48/5.50 ~sQ23_spl),
% 39.48/5.50 inference(contradiction_clause,[status(thm)],[f505])).
% 39.48/5.50 fof(f660,plain,(
% 39.48/5.50 ![X0]: (~sP5_prd(n0,X0))),
% 39.48/5.50 inference(resolution,[status(thm)],[f303,f215])).
% 39.48/5.50 fof(f817,definition,(
% 39.48/5.50 ![X0]: (sQ48_spl <=> (uptakepg(X0)|conditionhyper(X0)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f818,plain,(
% 39.48/5.50 ![X0]: (uptakepg(X0)|conditionhyper(X0)|~sQ48_spl)),
% 39.48/5.50 inference(component_clause,[status(thm)],[f817])).
% 39.48/5.50 fof(f948,definition,(
% 39.48/5.50 ![X1]: (sQ60_spl <=> (uptakepg(X1)|gt(n0,X1)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f949,plain,(
% 39.48/5.50 ![X0]: (uptakepg(X0)|gt(n0,X0)|~sQ60_spl)),
% 39.48/5.50 inference(component_clause,[status(thm)],[f948])).
% 39.48/5.50 fof(f1598,plain,(
% 39.48/5.50 ![X0]: (conditionhyper(X0)|uptakepg(X0)|~sQ60_spl)),
% 39.48/5.50 inference(resolution,[status(thm)],[f168,f949])).
% 39.48/5.50 fof(f4050,plain,(
% 39.48/5.50 ~s3(n0)),
% 39.48/5.50 inference(resolution,[status(thm)],[f167,f101])).
% 39.48/5.50 fof(f4226,plain,(
% 39.48/5.50 ![X0]: (conditionnormo(sK8_skl(n0))|gt(n0,X0)|drugi(X0))),
% 39.48/5.50 inference(resolution,[status(thm)],[f171,f132])).
% 39.48/5.50 fof(f4227,plain,(
% 39.48/5.50 ![X0]: (conditionnormo(sK9_skl(n0))|gt(n0,X0)|drugi(X0))),
% 39.48/5.50 inference(resolution,[status(thm)],[f171,f134])).
% 39.48/5.50 fof(f4231,definition,(
% 39.48/5.50 sQ186_spl <=> (conditionnormo(sK8_skl(n0)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f4232,plain,(
% 39.48/5.50 conditionnormo(sK8_skl(n0))|~sQ186_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f4231])).
% 39.48/5.50 fof(f4234,definition,(
% 39.48/5.50 ![X0]: (sQ187_spl <=> (gt(n0,X0)|drugi(X0)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f4235,plain,(
% 39.48/5.50 ![X0]: (gt(n0,X0)|drugi(X0)|~sQ187_spl)),
% 39.48/5.50 inference(component_clause,[status(thm)],[f4234])).
% 39.48/5.50 fof(f4237,plain,(
% 39.48/5.50 sQ186_spl|sQ187_spl),
% 39.48/5.50 inference(split_clause,[status(thm)],[f4226,f4231,f4234])).
% 39.48/5.50 fof(f4238,definition,(
% 39.48/5.50 sQ188_spl <=> (conditionnormo(sK9_skl(n0)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f4239,plain,(
% 39.48/5.50 conditionnormo(sK9_skl(n0))|~sQ188_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f4238])).
% 39.48/5.50 fof(f4241,plain,(
% 39.48/5.50 sQ188_spl|sQ187_spl),
% 39.48/5.50 inference(split_clause,[status(thm)],[f4227,f4238,f4234])).
% 39.48/5.50 fof(f4261,plain,(
% 39.48/5.50 drugi(n0)|~sQ187_spl),
% 39.48/5.50 inference(resolution,[status(thm)],[f4235,f43])).
% 39.48/5.50 fof(f4262,definition,(
% 39.48/5.50 sQ189_spl <=> (drugi(n0))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f4263,plain,(
% 39.48/5.50 drugi(n0)|~sQ189_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f4262])).
% 39.48/5.50 fof(f4284,plain,(
% 39.48/5.50 s3(n0)|~sQ189_spl),
% 39.48/5.50 inference(resolution,[status(thm)],[f4263,f129])).
% 39.48/5.50 fof(f4285,plain,(
% 39.48/5.50 $false|~sQ189_spl),
% 39.48/5.50 inference(forward_subsumption_resolution,[status(thm)],[f4284,f4050])).
% 39.48/5.50 fof(f4286,plain,(
% 39.48/5.50 ~sQ189_spl),
% 39.48/5.50 inference(contradiction_clause,[status(thm)],[f4285])).
% 39.48/5.50 fof(f4307,plain,(
% 39.48/5.50 sQ189_spl|~sQ187_spl),
% 39.48/5.50 inference(split_clause,[status(thm)],[f4261,f4262,f4234])).
% 39.48/5.50 fof(f5279,plain,(
% 39.48/5.50 ![X0]: (conditionnormo(X0)|~sP5_prd(X0,n0))),
% 39.48/5.50 inference(resolution,[status(thm)],[f171,f214])).
% 39.48/5.50 fof(f5283,plain,(
% 39.48/5.50 ![X0]: (~sP5_prd(X0,n0))),
% 39.48/5.50 inference(forward_subsumption_resolution,[status(thm)],[f5279,f215])).
% 39.48/5.50 fof(f7533,definition,(
% 39.48/5.50 sQ349_spl <=> (qilt27(n0))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f7534,plain,(
% 39.48/5.50 qilt27(n0)|~sQ349_spl),
% 39.48/5.50 inference(component_clause,[status(thm)],[f7533])).
% 39.48/5.50 fof(f9582,plain,(
% 39.48/5.50 ![X0,X1]: (gt(X0,X1)|drugi(X1)|conditionhyper(sK8_skl(X0))|~sQ18_spl)),
% 39.48/5.50 inference(resolution,[status(thm)],[f133,f427])).
% 39.48/5.50 fof(f9595,plain,(
% 39.48/5.50 ![X0,X1]: (releaselg(sK8_skl(X0))|gt(X0,X1)|drugi(X1))),
% 39.48/5.50 inference(resolution,[status(thm)],[f400,f133])).
% 39.48/5.50 fof(f9893,plain,(
% 39.48/5.50 ![X0]: (drugi(X0)|conditionhyper(sK8_skl(X0))|~sQ18_spl)),
% 39.48/5.50 inference(resolution,[status(thm)],[f9582,f43])).
% 39.48/5.50 fof(f10396,plain,(
% 39.48/5.50 ![X0]: (releaselg(sK8_skl(X0))|drugi(X0))),
% 39.48/5.50 inference(resolution,[status(thm)],[f9595,f43])).
% 39.48/5.50 fof(f10727,definition,(
% 39.48/5.50 ![X0]: (sQ484_spl <=> (gt(n0,X0)|~releaselg(X0)))),
% 39.48/5.50 introduced(definition,[new_symbols(definition,[sQ484_spl])],[split_symbol_definition])).
% 39.48/5.50 fof(f10728,plain,(
% 39.48/5.50 ![X0]: (gt(n0,X0)|~releaselg(X0)|~sQ484_spl)),
% 39.48/5.50 inference(component_clause,[status(thm)],[f10727])).
% 39.48/5.50 fof(f10745,plain,(
% 39.48/5.50 ![X0]: (gt(n0,sK8_skl(X0))|drugi(X0)|~sQ484_spl)),
% 39.48/5.50 inference(resolution,[status(thm)],[f10728,f10396])).
% 39.48/5.50 fof(f10766,plain,(
% 39.48/5.50 ![X0]: (drugi(n0)|gt(n0,X0)|drugi(X0)|~sQ484_spl)),
% 39.48/5.53 inference(resolution,[status(thm)],[f10745,f132])).
% 39.48/5.53 fof(f10769,plain,(
% 39.48/5.53 sQ189_spl|sQ187_spl|~sQ484_spl),
% 39.48/5.53 inference(split_clause,[status(thm)],[f10766,f4262,f4234,f10727])).
% 39.48/5.53 fof(f11160,plain,(
% 39.48/5.53 ![X0,X1]: (gt(n0,X0)|~releaselg(X0)|gt(n0,X1)|uptakepg(X1)|~sQ22_spl)),
% 39.48/5.53 inference(resolution,[status(thm)],[f284,f453])).
% 39.48/5.53 fof(f11161,plain,(
% 39.48/5.53 sQ484_spl|sQ60_spl|~sQ22_spl),
% 39.48/5.53 inference(split_clause,[status(thm)],[f11160,f10727,f948,f446])).
% 39.48/5.53 fof(f11162,plain,(
% 39.48/5.53 sQ48_spl|~sQ60_spl),
% 39.48/5.53 inference(split_clause,[status(thm)],[f1598,f817,f948])).
% 39.48/5.53 fof(f11200,plain,(
% 39.48/5.53 $false|~sQ16_spl),
% 39.48/5.53 inference(forward_subsumption_resolution,[status(thm)],[f421,f5283])).
% 39.48/5.53 fof(f11201,plain,(
% 39.48/5.53 ~sQ16_spl),
% 39.48/5.53 inference(contradiction_clause,[status(thm)],[f11200])).
% 39.48/5.53 fof(f11376,plain,(
% 39.48/5.53 ![X0,X1]: (gt(X0,X1)|drugi(X1)|conditionhyper(sK9_skl(X0))|~sQ48_spl)),
% 39.48/5.53 inference(resolution,[status(thm)],[f135,f818])).
% 39.48/5.53 fof(f11435,plain,(
% 39.48/5.53 $false|~sQ349_spl),
% 39.48/5.53 inference(forward_subsumption_resolution,[status(thm)],[f7534,f170])).
% 39.48/5.53 fof(f11436,plain,(
% 39.48/5.53 ~sQ349_spl),
% 39.48/5.53 inference(contradiction_clause,[status(thm)],[f11435])).
% 39.48/5.53 fof(f12576,definition,(
% 39.48/5.53 sQ536_spl <=> (sP5_prd(n0,sK3_skl(n0)))),
% 39.48/5.53 introduced(definition,[new_symbols(definition,[sQ536_spl])],[split_symbol_definition])).
% 39.48/5.53 fof(f12577,plain,(
% 39.48/5.53 sP5_prd(n0,sK3_skl(n0))|~sQ536_spl),
% 39.48/5.53 inference(component_clause,[status(thm)],[f12576])).
% 39.48/5.53 fof(f12581,plain,(
% 39.48/5.53 $false|~sQ536_spl),
% 39.48/5.53 inference(forward_subsumption_resolution,[status(thm)],[f12577,f660])).
% 39.48/5.53 fof(f12582,plain,(
% 39.48/5.53 ~sQ536_spl),
% 39.48/5.53 inference(contradiction_clause,[status(thm)],[f12581])).
% 39.48/5.53 fof(f12786,plain,(
% 39.48/5.53 ![X0]: (drugi(X0)|~conditionnormo(sK8_skl(X0))|~sQ18_spl)),
% 39.48/5.53 inference(resolution,[status(thm)],[f9893,f53])).
% 39.48/5.53 fof(f12862,plain,(
% 39.48/5.53 drugi(n0)|~sQ18_spl|~sQ186_spl),
% 39.48/5.53 inference(resolution,[status(thm)],[f12786,f4232])).
% 39.48/5.53 fof(f12867,plain,(
% 39.48/5.53 sQ189_spl|~sQ18_spl|~sQ186_spl),
% 39.48/5.53 inference(split_clause,[status(thm)],[f12862,f4262,f426,f4231])).
% 39.48/5.53 fof(f15898,plain,(
% 39.48/5.53 ![X0]: (drugi(X0)|conditionhyper(sK9_skl(X0))|~sQ48_spl)),
% 39.48/5.53 inference(resolution,[status(thm)],[f11376,f43])).
% 39.48/5.53 fof(f15975,plain,(
% 39.48/5.53 ![X0]: (drugi(X0)|~conditionnormo(sK9_skl(X0))|~sQ48_spl)),
% 39.48/5.53 inference(resolution,[status(thm)],[f15898,f53])).
% 39.48/5.53 fof(f15986,plain,(
% 39.48/5.53 drugi(n0)|~sQ48_spl|~sQ188_spl),
% 39.48/5.53 inference(resolution,[status(thm)],[f15975,f4239])).
% 39.48/5.53 fof(f15990,plain,(
% 39.48/5.53 sQ189_spl|~sQ48_spl|~sQ188_spl),
% 39.48/5.53 inference(split_clause,[status(thm)],[f15986,f4262,f817,f4238])).
% 39.48/5.53 fof(f15991,plain,(
% 39.48/5.53 $false),
% 39.48/5.53 inference(sat_refutation,[status(thm)],[f429,f449,f463,f474,f506,f4237,f4241,f4286,f4307,f10769,f11161,f11162,f11201,f11436,f12582,f12867,f15990])).
% 39.48/5.53 % SZS output end CNFRefutation for theBenchmark.p
% 39.48/5.55 % Elapsed time: 5.158312 seconds
% 39.48/5.55 % CPU time: 40.554074 seconds
% 39.48/5.55 % Total memory used: 183.147 MB
% 39.48/5.55 % Net memory used: 163.349 MB
%------------------------------------------------------------------------------