%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MED002+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 : n017.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 0.15s 5.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED002+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.10/5.37 % Computer : n017.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 01:15:20 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 0.15/5.81 % Refutation found
% 0.15/5.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.81 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.81 fof(f4,axiom,(
% 0.15/5.81 (! [X0] :( ~ bcapacityne(X0)| ~ bcapacityex(X0) ) )),
% 0.15/5.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.81 fof(f13,axiom,(
% 0.15/5.81 (! [X0] :( ( (! [X1] :( ~ gt(X0,X1)=> drugsu(X1) ))& ~ bcapacityex(X0) )=> (! [X1] :( ~ gt(X0,X1)=> bsecretioni(X1) ) )) )),
% 0.15/5.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.81 fof(f14,axiom,(
% 0.15/5.81 (! [X0] :( (! [X1] :( ~ gt(X0,X1)=> drugbg(X1) ))=> (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ) )) )),
% 0.15/5.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.81 fof(f17,axiom,(
% 0.15/5.81 (! [X0] :( ( ( (! [X1] :( ~ gt(X0,X1)=> ~ releaselg(X1) ))| (! [X1] :( ~ gt(X0,X1)=> uptakepg(X1) ) ))& bcapacityne(X0)& (! [X1] :( ~ gt(X0,X1)=> bsecretioni(X1) ))& (! [X1] :( gt(X0,X1)=> conditionhyper(X1) ) ))=> (! [X1] :( ~ gt(X0,X1)=> conditionnormo(X1) ) )) )),
% 0.15/5.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.81 fof(f19,conjecture,(
% 0.15/5.81 ( ( (! [X0] :( ~ gt(n0,X0)=> ( drugbg(X0)& drugsu(X0) ) ))& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ))& bcapacityne(n0) )=> (! [X0] :( ~ gt(n0,X0)=> conditionnormo(X0) ) )) ),
% 0.15/5.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.81 fof(f20,negated_conjecture,(
% 0.15/5.81 ~(( ( (! [X0] :( ~ gt(n0,X0)=> ( drugbg(X0)& drugsu(X0) ) ))& (! [X0] :( gt(n0,X0)=> conditionhyper(X0) ))& bcapacityne(n0) )=> (! [X0] :( ~ gt(n0,X0)=> conditionnormo(X0) ) )) )),
% 0.15/5.81 inference(negated_conjecture,[status(cth)],[f19])).
% 0.15/5.81 fof(f26,plain,(
% 0.15/5.81 ![X0]: (~bcapacityne(X0)|~bcapacityex(X0))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/5.81 fof(f42,plain,(
% 0.15/5.81 ![X0]: (((?[X1]: (~gt(X0,X1)&~drugsu(X1)))|bcapacityex(X0))|(![X1]: (gt(X0,X1)|bsecretioni(X1))))),
% 0.15/5.81 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.15/5.81 fof(f43,plain,(
% 0.15/5.81 ![X0]: (((~gt(X0,sK1_skl(X0))&~drugsu(sK1_skl(X0)))|bcapacityex(X0))|(![X1]: (gt(X0,X1)|bsecretioni(X1))))),
% 0.15/5.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X1,sK1_skl(X0))],[f42])).
% 0.15/5.81 fof(f44,plain,(
% 0.15/5.81 ![X0,X1]: (~gt(X0,sK1_skl(X0))|bcapacityex(X0)|gt(X0,X1)|bsecretioni(X1))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f43])).
% 0.15/5.81 fof(f45,plain,(
% 0.15/5.81 ![X0,X1]: (~drugsu(sK1_skl(X0))|bcapacityex(X0)|gt(X0,X1)|bsecretioni(X1))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f43])).
% 0.15/5.81 fof(f46,plain,(
% 0.15/5.81 ![X0]: ((?[X1]: (~gt(X0,X1)&~drugbg(X1)))|(![X1]: (gt(X0,X1)|~releaselg(X1))))),
% 0.15/5.81 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.15/5.81 fof(f47,plain,(
% 0.15/5.81 ![X0]: ((~gt(X0,sK2_skl(X0))&~drugbg(sK2_skl(X0)))|(![X1]: (gt(X0,X1)|~releaselg(X1))))),
% 0.15/5.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X1,sK2_skl(X0))],[f46])).
% 0.15/5.81 fof(f48,plain,(
% 0.15/5.81 ![X0,X1]: (~gt(X0,sK2_skl(X0))|gt(X0,X1)|~releaselg(X1))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/5.81 fof(f49,plain,(
% 0.15/5.81 ![X0,X1]: (~drugbg(sK2_skl(X0))|gt(X0,X1)|~releaselg(X1))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/5.81 fof(f62,plain,(
% 0.15/5.81 ![X0]: ((((((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0))|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1))))|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))|(![X1]: (gt(X0,X1)|conditionnormo(X1))))),
% 0.15/5.81 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.15/5.81 fof(f63,definition,(
% 0.15/5.81 ![X0]: (sP3_prd(X0)<=>((((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0))|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))))),
% 0.15/5.81 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.15/5.81 fof(f64,plain,(
% 0.15/5.81 ![X0]: ((sP3_prd(X0)|(?[X1]: (gt(X0,X1)&~conditionhyper(X1))))|(![X1]: (gt(X0,X1)|conditionnormo(X1))))),
% 0.15/5.81 inference(formula_renaming,[status(thm)],[f62,f63])).
% 0.15/5.81 fof(f65,plain,(
% 0.15/5.81 ![X0]: ((sP3_prd(X0)|(gt(X0,sK5_skl(X0))&~conditionhyper(sK5_skl(X0))))|(![X1]: (gt(X0,X1)|conditionnormo(X1))))),
% 0.15/5.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(X1,sK5_skl(X0))],[f64])).
% 0.15/5.81 fof(f66,plain,(
% 0.15/5.81 ![X0,X1]: (sP3_prd(X0)|gt(X0,sK5_skl(X0))|gt(X0,X1)|conditionnormo(X1))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f65])).
% 0.15/5.81 fof(f67,plain,(
% 0.15/5.81 ![X0,X1]: (sP3_prd(X0)|~conditionhyper(sK5_skl(X0))|gt(X0,X1)|conditionnormo(X1))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f65])).
% 0.15/5.81 fof(f74,plain,(
% 0.15/5.81 ((((![X0]: (gt(n0,X0)|(drugbg(X0)&drugsu(X0))))&(![X0]: (~gt(n0,X0)|conditionhyper(X0))))&bcapacityne(n0))&(?[X0]: (~gt(n0,X0)&~conditionnormo(X0))))),
% 0.15/5.81 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.15/5.81 fof(f75,plain,(
% 0.15/5.81 (((![X0]: (gt(n0,X0)|(drugbg(X0)&drugsu(X0))))&(![X0]: (~gt(n0,X0)|conditionhyper(X0))))&bcapacityne(n0))&(~gt(n0,sK7_skl)&~conditionnormo(sK7_skl))),
% 0.15/5.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X0,sK7_skl)],[f74])).
% 0.15/5.81 fof(f76,plain,(
% 0.15/5.81 ![X0]: (gt(n0,X0)|drugbg(X0))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f75])).
% 0.15/5.81 fof(f77,plain,(
% 0.15/5.81 ![X0]: (gt(n0,X0)|drugsu(X0))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f75])).
% 0.15/5.81 fof(f78,plain,(
% 0.15/5.81 ![X0]: (~gt(n0,X0)|conditionhyper(X0))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f75])).
% 0.15/5.81 fof(f79,plain,(
% 0.15/5.81 bcapacityne(n0)),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f75])).
% 0.15/5.81 fof(f80,plain,(
% 0.15/5.81 ~gt(n0,sK7_skl)),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f75])).
% 0.15/5.81 fof(f81,plain,(
% 0.15/5.81 ~conditionnormo(sK7_skl)),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f75])).
% 0.15/5.81 fof(f103,definition,(
% 0.15/5.81 ![X0]: (sP5_prd(X0)<=>(((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0)))),
% 0.15/5.81 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.15/5.81 fof(f104,plain,(
% 0.15/5.81 ![X0]: (sP3_prd(X0)<=>(sP5_prd(X0)|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))))),
% 0.15/5.81 inference(formula_renaming,[status(thm)],[f63,f103])).
% 0.15/5.81 fof(f105,plain,(
% 0.15/5.81 ![X0]: ((~sP3_prd(X0)|(sP5_prd(X0)|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1)))))&(sP3_prd(X0)|(~sP5_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1))))))),
% 0.15/5.81 inference(NNF_transformation,[status(thm)],[f104])).
% 0.15/5.81 fof(f106,plain,(
% 0.15/5.81 (![X0]: (~sP3_prd(X0)|(sP5_prd(X0)|(?[X1]: (~gt(X0,X1)&~bsecretioni(X1))))))&(![X0]: (sP3_prd(X0)|(~sP5_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1))))))),
% 0.15/5.81 inference(miniscoping,[status(thm)],[f105])).
% 0.15/5.81 fof(f107,plain,(
% 0.15/5.81 (![X0]: (~sP3_prd(X0)|(sP5_prd(X0)|(~gt(X0,sK10_skl(X0))&~bsecretioni(sK10_skl(X0))))))&(![X0]: (sP3_prd(X0)|(~sP5_prd(X0)&(![X1]: (gt(X0,X1)|bsecretioni(X1))))))),
% 0.15/5.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X1,sK10_skl(X0))],[f106])).
% 0.15/5.81 fof(f108,plain,(
% 0.15/5.81 ![X0]: (~sP3_prd(X0)|sP5_prd(X0)|~gt(X0,sK10_skl(X0)))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f107])).
% 0.15/5.81 fof(f109,plain,(
% 0.15/5.81 ![X0]: (~sP3_prd(X0)|sP5_prd(X0)|~bsecretioni(sK10_skl(X0)))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f107])).
% 0.15/5.81 fof(f122,plain,(
% 0.15/5.81 ![X0]: ((~sP5_prd(X0)|(((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0)))&(sP5_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))))),
% 0.15/5.81 inference(NNF_transformation,[status(thm)],[f103])).
% 0.15/5.81 fof(f123,plain,(
% 0.15/5.81 (![X0]: (~sP5_prd(X0)|(((?[X1]: (~gt(X0,X1)&releaselg(X1)))&(?[X1]: (~gt(X0,X1)&~uptakepg(X1))))|~bcapacityne(X0))))&(![X0]: (sP5_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))))),
% 0.15/5.81 inference(miniscoping,[status(thm)],[f122])).
% 0.15/5.81 fof(f124,plain,(
% 0.15/5.81 (![X0]: (~sP5_prd(X0)|(((~gt(X0,sK13_skl(X0))&releaselg(sK13_skl(X0)))&(~gt(X0,sK14_skl(X0))&~uptakepg(sK14_skl(X0))))|~bcapacityne(X0))))&(![X0]: (sP5_prd(X0)|(((![X1]: (gt(X0,X1)|~releaselg(X1)))|(![X1]: (gt(X0,X1)|uptakepg(X1))))&bcapacityne(X0))))),
% 0.15/5.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(X1,sK13_skl(X0)),skolemize(X1,sK14_skl(X0))],[f123])).
% 0.15/5.81 fof(f125,plain,(
% 0.15/5.81 ![X0]: (~sP5_prd(X0)|~gt(X0,sK13_skl(X0))|~bcapacityne(X0))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f124])).
% 0.15/5.81 fof(f126,plain,(
% 0.15/5.81 ![X0]: (~sP5_prd(X0)|releaselg(sK13_skl(X0))|~bcapacityne(X0))),
% 0.15/5.81 inference(cnf_transformation,[status(thm)],[f124])).
% 0.15/5.81 fof(f132,plain,(
% 0.15/5.81 ~bcapacityex(n0)),
% 0.15/5.81 inference(resolution,[status(thm)],[f26,f79])).
% 0.15/5.81 fof(f156,plain,(
% 0.15/5.81 ![X0]: (bcapacityex(n0)|gt(n0,X0)|bsecretioni(X0)|drugsu(sK1_skl(n0)))),
% 0.15/5.81 inference(resolution,[status(thm)],[f44,f77])).
% 0.15/5.81 fof(f158,plain,(
% 0.15/5.81 ![X0]: (gt(n0,X0)|bsecretioni(X0)|drugsu(sK1_skl(n0)))),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f156,f132])).
% 0.15/5.81 fof(f161,plain,(
% 0.15/5.81 ![X0]: (gt(n0,X0)|~releaselg(X0)|drugbg(sK2_skl(n0)))),
% 0.15/5.81 inference(resolution,[status(thm)],[f48,f76])).
% 0.15/5.81 fof(f162,plain,(
% 0.15/5.81 ![X0]: (gt(n0,X0)|~releaselg(X0))),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f161,f49])).
% 0.15/5.81 fof(f352,plain,(
% 0.15/5.81 sP3_prd(n0)|gt(n0,sK5_skl(n0))|conditionnormo(sK7_skl)),
% 0.15/5.81 inference(resolution,[status(thm)],[f66,f80])).
% 0.15/5.81 fof(f366,plain,(
% 0.15/5.81 sP3_prd(n0)|gt(n0,sK5_skl(n0))),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f352,f81])).
% 0.15/5.81 fof(f403,plain,(
% 0.15/5.81 ![X0,X1]: (gt(n0,X0)|bsecretioni(X0)|bcapacityex(n0)|gt(n0,X1)|bsecretioni(X1))),
% 0.15/5.81 inference(resolution,[status(thm)],[f158,f45])).
% 0.15/5.81 fof(f406,plain,(
% 0.15/5.81 ![X0,X1]: (gt(n0,X0)|bsecretioni(X0)|gt(n0,X1)|bsecretioni(X1))),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f403,f132])).
% 0.15/5.81 fof(f446,plain,(
% 0.15/5.81 ![X0]: (gt(n0,X0)|bsecretioni(X0)|bsecretioni(X0))),
% 0.15/5.81 inference(factoring,[status(thm)],[f406])).
% 0.15/5.81 fof(f467,plain,(
% 0.15/5.81 ![X0]: (gt(n0,X0)|bsecretioni(X0))),
% 0.15/5.81 inference(duplicate_literals_removal,[status(thm)],[f446])).
% 0.15/5.81 fof(f664,plain,(
% 0.15/5.81 ~sP3_prd(n0)|sP5_prd(n0)|bsecretioni(sK10_skl(n0))),
% 0.15/5.81 inference(resolution,[status(thm)],[f108,f467])).
% 0.15/5.81 fof(f866,plain,(
% 0.15/5.81 sP3_prd(n0)|conditionhyper(sK5_skl(n0))),
% 0.15/5.81 inference(resolution,[status(thm)],[f366,f78])).
% 0.15/5.81 fof(f874,plain,(
% 0.15/5.81 ![X0]: (sP3_prd(n0)|sP3_prd(n0)|gt(n0,X0)|conditionnormo(X0))),
% 0.15/5.81 inference(resolution,[status(thm)],[f866,f67])).
% 0.15/5.81 fof(f876,plain,(
% 0.15/5.81 ![X0]: (sP3_prd(n0)|gt(n0,X0)|conditionnormo(X0))),
% 0.15/5.81 inference(duplicate_literals_removal,[status(thm)],[f874])).
% 0.15/5.81 fof(f930,plain,(
% 0.15/5.81 sP3_prd(n0)|conditionnormo(sK7_skl)),
% 0.15/5.81 inference(resolution,[status(thm)],[f876,f80])).
% 0.15/5.81 fof(f955,plain,(
% 0.15/5.81 sP3_prd(n0)),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f930,f81])).
% 0.15/5.81 fof(f2006,plain,(
% 0.15/5.81 sP5_prd(n0)|bsecretioni(sK10_skl(n0))),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f664,f955])).
% 0.15/5.81 fof(f2007,plain,(
% 0.15/5.81 sP5_prd(n0)|~sP3_prd(n0)|sP5_prd(n0)),
% 0.15/5.81 inference(resolution,[status(thm)],[f2006,f109])).
% 0.15/5.81 fof(f2008,plain,(
% 0.15/5.81 sP5_prd(n0)|~sP3_prd(n0)),
% 0.15/5.81 inference(duplicate_literals_removal,[status(thm)],[f2007])).
% 0.15/5.81 fof(f2009,plain,(
% 0.15/5.81 sP5_prd(n0)),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f2008,f955])).
% 0.15/5.81 fof(f2024,plain,(
% 0.15/5.81 releaselg(sK13_skl(n0))|~bcapacityne(n0)),
% 0.15/5.81 inference(resolution,[status(thm)],[f2009,f126])).
% 0.15/5.81 fof(f2030,plain,(
% 0.15/5.81 releaselg(sK13_skl(n0))),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f2024,f79])).
% 0.15/5.81 fof(f2114,plain,(
% 0.15/5.81 gt(n0,sK13_skl(n0))),
% 0.15/5.81 inference(resolution,[status(thm)],[f2030,f162])).
% 0.15/5.81 fof(f2116,plain,(
% 0.15/5.81 ~sP5_prd(n0)|~bcapacityne(n0)),
% 0.15/5.81 inference(resolution,[status(thm)],[f2114,f125])).
% 0.15/5.81 fof(f2134,plain,(
% 0.15/5.81 ~bcapacityne(n0)),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f2116,f2009])).
% 0.15/5.81 fof(f2135,plain,(
% 0.15/5.81 $false),
% 0.15/5.81 inference(forward_subsumption_resolution,[status(thm)],[f2134,f79])).
% 0.15/5.81 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.82 % Elapsed time: 0.439142 seconds
% 0.15/5.82 % CPU time: 3.351321 seconds
% 0.15/5.82 % Total memory used: 52.936 MB
% 0.15/5.82 % Net memory used: 48.517 MB
%------------------------------------------------------------------------------