%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MED007+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:56 PM UTC 2026
% Result : Theorem 21.13s 3.20s
% Output : CNFRefutation 19.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 99
% Syntax : Number of formulae : 466 ( 13 unt; 79 def)
% Number of atoms : 1896 ( 0 equ)
% Maximal formula atoms : 30 ( 4 avg)
% Number of connectives : 2177 ( 747 ~;1051 |; 249 &)
% ( 85 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 97 ( 96 usr; 69 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 1 con; 0-1 aty)
% Number of variables : 572 ( 529 !; 43 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( ( gt(Y,Z)
& gt(X,Y) )
=> gt(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X0] :
( ~ bcapacitysn(X0)
| ~ bcapacityne(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X0] :
( conditionnormo(X0)
| conditionhypo(X0)
| conditionhyper(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X0] :
( ~ conditionhypo(X0)
| ~ conditionhyper(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X0] :
( ~ conditionnormo(X0)
| ~ conditionhyper(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> drugbg(X1) )
=> ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X0] :
( ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& bcapacityne(X0)
& ( ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) ) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X0] :
( ~ s2(X0)
| ~ s1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X0] :
( ~ s3(X0)
| ~ s1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X0] :
( ~ s3(X0)
| ~ s2(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
=> ( ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& bcapacityex(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) ) )
| ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& bcapacityne(X0)
& ( ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) ) ) )
| ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) ) )
| ( ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X0] :
( ( ~ qilt27(X0)
& s1(X0) )
=> drugbg(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X0] :
( drugbg(X0)
=> ( s3(X0)
| s2(X0)
| ( ~ qilt27(X0)
& s1(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X0] :
( drugi(X0)
=> s3(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X0] :
( ( ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> drugi(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
=> ! [X1] :
( ~ gt(X0,X1)
=> drugbg(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X0] :
( ( ~ ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
& s1(X0) )
=> ? [X1] :
( ( bcapacityex(X1)
| bcapacityne(X1) )
& ! [X2] :
( gt(X1,X2)
=> conditionhyper(X2) )
& s2(X1)
& ~ gt(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X0] :
( ( ~ ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
& s2(X0) )
=> ? [X1] :
( bcapacityex(X1)
& ! [X2] :
( gt(X1,X2)
=> conditionhyper(X2) )
& s3(X1)
& ~ gt(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,conjecture,
( ( qilt27(n0)
& ~ bcapacitysn(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& s1(n0) )
=> ? [X0] :
( ( bcapacityex(X0)
| bcapacityne(X0) )
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& s2(X0)
& ~ gt(n0,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
~ ( ( qilt27(n0)
& ~ bcapacitysn(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& s1(n0) )
=> ? [X0] :
( ( bcapacityex(X0)
| bcapacityne(X0) )
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& s2(X0)
& ~ gt(n0,X0) ) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f43,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f44,plain,
! [X,Y,Z] :
( gt(X,Z)
| ~ gt(Y,Z)
| ~ gt(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
! [X,Z] :
( gt(X,Z)
| ! [Y] :
( ~ gt(Y,Z)
| ~ gt(X,Y) ) ),
inference(miniscoping,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0,X1,X2] :
( gt(X0,X2)
| ~ gt(X1,X2)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f49,plain,
! [X0] :
( ~ bcapacitysn(X0)
| ~ bcapacityne(X0) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f51,plain,
! [X0] :
( conditionnormo(X0)
| conditionhypo(X0)
| conditionhyper(X0) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f52,plain,
! [X0] :
( ~ conditionhypo(X0)
| ~ conditionhyper(X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f53,plain,
! [X0] :
( ~ conditionnormo(X0)
| ~ conditionhyper(X0) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f68,plain,
! [X0] :
( ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) )
| ? [X1] :
( ~ drugbg(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f69,plain,
! [X0] :
( ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) )
| ( ~ drugbg(sK2_skl(X0))
& ~ gt(X0,sK2_skl(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X1,sK2_skl(X0))],[f68]) ).
fof(f70,plain,
! [X0,X1] :
( ~ releaselg(X1)
| gt(X0,X1)
| ~ gt(X0,sK2_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f71,plain,
! [X0,X1] :
( ~ releaselg(X1)
| gt(X0,X1)
| ~ drugbg(sK2_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f84,plain,
! [X0] :
( ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f85,definition,
! [X0] :
( sP3_prd(X0)
<=> ( ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f100,plain,
! [X0] :
( ~ s2(X0)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f101,plain,
! [X0] :
( ~ s3(X0)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f102,plain,
! [X0] :
( ~ s3(X0)
| ~ s2(X0) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f103,plain,
! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& bcapacityex(X0)
& ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
| gt(X0,X1) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) )
| ? [X1] :
( ~ conditionnormo(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f104,definition,
! [X0,X1] :
( sP5_prd(X1,X0)
<=> ( ~ conditionnormo(X1)
& ~ gt(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f105,definition,
! [X0] :
( sP6_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f106,plain,
! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& bcapacityex(X0)
& ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
| gt(X0,X1) ) )
| sP6_prd(X0)
| ? [X1] : sP5_prd(X1,X0) ),
inference(formula_renaming,[status(thm)],[f103,f105,f104]) ).
fof(f107,plain,
! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& bcapacityex(X0)
& ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
& ! [X1] :
( uptakelg(X1)
| gt(X0,X1) ) )
| sP6_prd(X0)
| sP5_prd(sK7_skl(X0),X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X1,sK7_skl(X0))],[f106]) ).
fof(f109,plain,
! [X0,X1] :
( uptakepg(X1)
| gt(X0,X1)
| sP6_prd(X0)
| sP5_prd(sK7_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f111,plain,
! [X0,X1] :
( conditionhyper(X1)
| ~ gt(X0,X1)
| sP6_prd(X0)
| sP5_prd(sK7_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f114,plain,
! [X0] :
( drugbg(X0)
| qilt27(X0)
| ~ s1(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f115,plain,
! [X0] :
( drugbg(X0)
| qilt27(X0)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f122,plain,
! [X0] :
( s3(X0)
| s2(X0)
| ( ~ qilt27(X0)
& s1(X0) )
| ~ drugbg(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f124,plain,
! [X0] :
( s3(X0)
| s2(X0)
| ~ qilt27(X0)
| ~ drugbg(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f128,plain,
! [X0] :
( s3(X0)
| ~ drugi(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f129,plain,
! [X0] :
( s3(X0)
| ~ drugi(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [X0] :
( ! [X1] :
( drugi(X1)
| gt(X0,X1) )
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( ~ uptakelg(X1)
& ~ gt(X0,X1) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f131,plain,
! [X0] :
( ! [X1] :
( drugi(X1)
| gt(X0,X1) )
| ( ~ uptakepg(sK9_skl(X0))
& ~ gt(X0,sK9_skl(X0))
& ~ uptakelg(sK8_skl(X0))
& ~ gt(X0,sK8_skl(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(X1,sK8_skl(X0)),skolemize(X1,sK9_skl(X0))],[f130]) ).
fof(f132,plain,
! [X0,X1] :
( drugi(X1)
| gt(X0,X1)
| ~ gt(X0,sK8_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [X0,X1] :
( drugi(X1)
| gt(X0,X1)
| ~ uptakelg(sK8_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f134,plain,
! [X0,X1] :
( drugi(X1)
| gt(X0,X1)
| ~ gt(X0,sK9_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f135,plain,
! [X0,X1] :
( drugi(X1)
| gt(X0,X1)
| ~ uptakepg(sK9_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f145,plain,
! [X0] :
( ! [X1] :
( drugbg(X1)
| gt(X0,X1) )
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f146,plain,
! [X0] :
( ! [X1] :
( drugbg(X1)
| gt(X0,X1) )
| ( releaselg(sK11_skl(X0))
& ~ gt(X0,sK11_skl(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X1,sK11_skl(X0))],[f145]) ).
fof(f147,plain,
! [X0,X1] :
( drugbg(X1)
| gt(X0,X1)
| ~ gt(X0,sK11_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
! [X0,X1] :
( drugbg(X1)
| gt(X0,X1)
| releaselg(sK11_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f154,plain,
! [X0] :
( ? [X1] :
( ( bcapacityex(X1)
| bcapacityne(X1) )
& ! [X2] :
( conditionhyper(X2)
| ~ gt(X1,X2) )
& s2(X1)
& ~ gt(X0,X1) )
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ~ s1(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f155,plain,
! [X0] :
( ( ( bcapacityex(sK13_skl(X0))
| bcapacityne(sK13_skl(X0)) )
& ! [X2] :
( conditionhyper(X2)
| ~ gt(sK13_skl(X0),X2) )
& s2(sK13_skl(X0))
& ~ gt(X0,sK13_skl(X0)) )
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ~ s1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X1,sK13_skl(X0))],[f154]) ).
fof(f156,plain,
! [X0,X1] :
( ~ gt(X0,sK13_skl(X0))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f157,plain,
! [X0,X1] :
( s2(sK13_skl(X0))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f158,plain,
! [X0,X1,X2] :
( conditionhyper(X2)
| ~ gt(sK13_skl(X0),X2)
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f159,plain,
! [X0,X1] :
( bcapacityex(sK13_skl(X0))
| bcapacityne(sK13_skl(X0))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f160,plain,
! [X0] :
( ? [X1] :
( bcapacityex(X1)
& ! [X2] :
( conditionhyper(X2)
| ~ gt(X1,X2) )
& s3(X1)
& ~ gt(X0,X1) )
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ~ s2(X0) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f161,plain,
! [X0] :
( ( bcapacityex(sK14_skl(X0))
& ! [X2] :
( conditionhyper(X2)
| ~ gt(sK14_skl(X0),X2) )
& s3(sK14_skl(X0))
& ~ gt(X0,sK14_skl(X0)) )
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) )
| ~ s2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X1,sK14_skl(X0))],[f160]) ).
fof(f164,plain,
! [X0,X1,X2] :
( conditionhyper(X2)
| ~ gt(sK14_skl(X0),X2)
| conditionnormo(X1)
| gt(X0,X1)
| ~ s2(X0) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f166,plain,
( ! [X0] :
( ( ~ bcapacityex(X0)
& ~ bcapacityne(X0) )
| ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ s2(X0)
| gt(n0,X0) )
& qilt27(n0)
& ~ bcapacitysn(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& s1(n0) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f167,definition,
! [X0,X1] :
( sP8_prd(X1,X0)
<=> ( ~ conditionhyper(X1)
& gt(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP8_prd])],[]) ).
fof(f168,plain,
( ! [X0] :
( ( ~ bcapacityex(X0)
& ~ bcapacityne(X0) )
| ? [X1] : sP8_prd(X1,X0)
| ~ s2(X0)
| gt(n0,X0) )
& qilt27(n0)
& ~ bcapacitysn(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& s1(n0) ),
inference(formula_renaming,[status(thm)],[f166,f167]) ).
fof(f169,plain,
( ! [X0] :
( ( ~ bcapacityex(X0)
& ~ bcapacityne(X0) )
| sP8_prd(sK15_skl(X0),X0)
| ~ s2(X0)
| gt(n0,X0) )
& qilt27(n0)
& ~ bcapacitysn(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) )
& s1(n0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X1,sK15_skl(X0))],[f168]) ).
fof(f170,plain,
s1(n0),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f171,plain,
! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f172,plain,
~ bcapacitysn(n0),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f173,plain,
qilt27(n0),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f174,plain,
! [X0] :
( ~ bcapacityne(X0)
| sP8_prd(sK15_skl(X0),X0)
| ~ s2(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f175,plain,
! [X0] :
( ~ bcapacityex(X0)
| sP8_prd(sK15_skl(X0),X0)
| ~ s2(X0)
| gt(n0,X0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f197,definition,
! [X0] :
( sP9_prd(X0)
<=> ( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP9_prd])],[]) ).
fof(f216,plain,
! [X0,X1] :
( ( conditionnormo(X1)
| gt(X0,X1)
| sP5_prd(X1,X0) )
& ( ( ~ conditionnormo(X1)
& ~ gt(X0,X1) )
| ~ sP5_prd(X1,X0) ) ),
inference(NNF_transformation,[status(thm)],[f104]) ).
fof(f217,plain,
( ! [X0,X1] :
( conditionnormo(X1)
| gt(X0,X1)
| sP5_prd(X1,X0) )
& ! [X0,X1] :
( ( ~ conditionnormo(X1)
& ~ gt(X0,X1) )
| ~ sP5_prd(X1,X0) ) ),
inference(miniscoping,[status(thm)],[f216]) ).
fof(f218,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f219,plain,
! [X0,X1] :
( ~ conditionnormo(X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f221,definition,
! [X0] :
( sP10_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP10_prd])],[]) ).
fof(f222,plain,
! [X0] :
( sP6_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| sP10_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f105,f221]) ).
fof(f223,definition,
! [X0] :
( sP11_prd(X0)
<=> ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP11_prd])],[]) ).
fof(f224,plain,
! [X0] :
( sP6_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP11_prd(X0) )
| sP10_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f222,f223]) ).
fof(f225,plain,
! [X0] :
( ( ( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP11_prd(X0) )
& ~ sP10_prd(X0) )
| sP6_prd(X0) )
& ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP11_prd(X0) )
| sP10_prd(X0)
| ~ sP6_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f224]) ).
fof(f226,plain,
( ! [X0] :
( ( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP11_prd(X0) )
& ~ sP10_prd(X0) )
| sP6_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP11_prd(X0) )
| sP10_prd(X0)
| ~ sP6_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f225]) ).
fof(f227,plain,
( ! [X0] :
( ( ( ( ~ conditionhyper(sK21_skl(X0))
& gt(X0,sK21_skl(X0)) )
| ~ sP11_prd(X0) )
& ~ sP10_prd(X0) )
| sP6_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP11_prd(X0) )
| sP10_prd(X0)
| ~ sP6_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(X1,sK21_skl(X0))],[f226]) ).
fof(f228,plain,
! [X0] :
( sP11_prd(X0)
| sP10_prd(X0)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f229,plain,
! [X0,X1] :
( conditionhyper(X1)
| ~ gt(X0,X1)
| sP10_prd(X0)
| ~ sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f230,plain,
! [X0] :
( ~ sP10_prd(X0)
| sP6_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f238,plain,
! [X0,X1] :
( ( conditionhyper(X1)
| ~ gt(X0,X1)
| sP8_prd(X1,X0) )
& ( ( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP8_prd(X1,X0) ) ),
inference(NNF_transformation,[status(thm)],[f167]) ).
fof(f239,plain,
( ! [X0,X1] :
( conditionhyper(X1)
| ~ gt(X0,X1)
| sP8_prd(X1,X0) )
& ! [X0,X1] :
( ( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP8_prd(X1,X0) ) ),
inference(miniscoping,[status(thm)],[f238]) ).
fof(f240,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ sP8_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f241,plain,
! [X0,X1] :
( ~ conditionhyper(X0)
| ~ sP8_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f239]) ).
fof(f243,plain,
! [X0] :
( ( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| sP9_prd(X0) )
& ( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) )
| ~ sP9_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f197]) ).
fof(f244,plain,
( ! [X0] :
( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| sP9_prd(X0) )
& ! [X0] :
( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) )
| ~ sP9_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f243]) ).
fof(f245,plain,
( ! [X0] :
( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| sP9_prd(X0) )
& ! [X0] :
( ~ bcapacityne(X0)
| ( ~ uptakepg(sK23_skl(X0))
& ~ gt(X0,sK23_skl(X0))
& releaselg(sK22_skl(X0))
& ~ gt(X0,sK22_skl(X0)) )
| ~ sP9_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl,sK23_skl]),skolemize(X1,sK22_skl(X0)),skolemize(X1,sK23_skl(X0))],[f244]) ).
fof(f250,plain,
! [X0,X1,X2] :
( uptakepg(X2)
| gt(X0,X2)
| ~ releaselg(X1)
| gt(X0,X1)
| sP9_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f252,definition,
! [X0] :
( sP12_prd(X0)
<=> ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP12_prd])],[]) ).
fof(f253,plain,
! [X0] :
( sP10_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| sP12_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f221,f252]) ).
fof(f254,definition,
! [X0] :
( sP13_prd(X0)
<=> ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP13_prd])],[]) ).
fof(f255,plain,
! [X0] :
( sP10_prd(X0)
<=> ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP13_prd(X0) )
| sP12_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f253,f254]) ).
fof(f256,plain,
! [X0] :
( ( ( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP13_prd(X0) )
& ~ sP12_prd(X0) )
| sP10_prd(X0) )
& ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP13_prd(X0) )
| sP12_prd(X0)
| ~ sP10_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f255]) ).
fof(f257,plain,
( ! [X0] :
( ( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP13_prd(X0) )
& ~ sP12_prd(X0) )
| sP10_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP13_prd(X0) )
| sP12_prd(X0)
| ~ sP10_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f256]) ).
fof(f258,plain,
( ! [X0] :
( ( ( ( ~ conditionhyper(sK24_skl(X0))
& gt(X0,sK24_skl(X0)) )
| ~ sP13_prd(X0) )
& ~ sP12_prd(X0) )
| sP10_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP13_prd(X0) )
| sP12_prd(X0)
| ~ sP10_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(X1,sK24_skl(X0))],[f257]) ).
fof(f259,plain,
! [X0] :
( sP13_prd(X0)
| sP12_prd(X0)
| ~ sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f260,plain,
! [X0,X1] :
( conditionhyper(X1)
| ~ gt(X0,X1)
| sP12_prd(X0)
| ~ sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f261,plain,
! [X0] :
( ~ sP12_prd(X0)
| sP10_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f264,definition,
! [X0] :
( sP14_prd(X0)
<=> ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP14_prd])],[]) ).
fof(f265,plain,
! [X0] :
( sP11_prd(X0)
<=> ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& sP14_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f223,f264]) ).
fof(f266,plain,
! [X0] :
( ( ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| ~ sP14_prd(X0)
| sP11_prd(X0) )
& ( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& sP14_prd(X0) )
| ~ sP11_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f265]) ).
fof(f267,plain,
( ! [X0] :
( ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| ~ sP14_prd(X0)
| sP11_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& sP14_prd(X0) )
| ~ sP11_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f266]) ).
fof(f268,plain,
( ! [X0] :
( ( ~ bsecretioni(sK25_skl(X0))
& ~ gt(X0,sK25_skl(X0)) )
| ~ sP14_prd(X0)
| sP11_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& sP14_prd(X0) )
| ~ sP11_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(X1,sK25_skl(X0))],[f267]) ).
fof(f269,plain,
! [X0] :
( sP14_prd(X0)
| ~ sP11_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f273,definition,
! [X0] :
( sP15_prd(X0)
<=> ( qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP15_prd])],[]) ).
fof(f274,plain,
! [X0] :
( sP12_prd(X0)
<=> ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP15_prd(X0) ) ),
inference(formula_renaming,[status(thm)],[f252,f273]) ).
fof(f275,plain,
! [X0] :
( ( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP15_prd(X0)
| sP12_prd(X0) )
& ( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP15_prd(X0) )
| ~ sP12_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f274]) ).
fof(f276,plain,
( ! [X0] :
( ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) )
| ~ sP15_prd(X0)
| sP12_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP15_prd(X0) )
| ~ sP12_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f275]) ).
fof(f277,plain,
( ! [X0] :
( ( ~ conditionhyper(sK26_skl(X0))
& gt(X0,sK26_skl(X0)) )
| ~ sP15_prd(X0)
| sP12_prd(X0) )
& ! [X0] :
( ( ! [X1] :
( conditionhyper(X1)
| ~ gt(X0,X1) )
& sP15_prd(X0) )
| ~ sP12_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(X1,sK26_skl(X0))],[f276]) ).
fof(f278,plain,
! [X0] :
( sP15_prd(X0)
| ~ sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f279,plain,
! [X0,X1] :
( conditionhyper(X1)
| ~ gt(X0,X1)
| ~ sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f280,plain,
! [X0] :
( gt(X0,sK26_skl(X0))
| ~ sP15_prd(X0)
| sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f281,plain,
! [X0] :
( ~ conditionhyper(sK26_skl(X0))
| ~ sP15_prd(X0)
| sP12_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f282,plain,
! [X0] :
( ( qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) )
| sP13_prd(X0) )
& ( ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ~ sP13_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f254]) ).
fof(f283,plain,
( ! [X0] :
( qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) )
| sP13_prd(X0) )
& ! [X0] :
( ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ~ sP13_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f282]) ).
fof(f284,plain,
( ! [X0] :
( qilt27(X0)
| ~ bcapacitysn(X0)
| ( releaselg(sK27_skl(X0))
& ~ gt(X0,sK27_skl(X0)) )
| sP13_prd(X0) )
& ! [X0] :
( ( ~ qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) )
| ~ sP13_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(X1,sK27_skl(X0))],[f283]) ).
fof(f285,plain,
! [X0,X1] :
( ~ releaselg(X1)
| gt(X0,X1)
| ~ sP13_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f287,plain,
! [X0] :
( ~ qilt27(X0)
| ~ sP13_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f290,plain,
! [X0] :
( ( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) )
| sP14_prd(X0) )
& ( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ~ sP14_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f264]) ).
fof(f291,plain,
( ! [X0] :
( ~ bcapacityne(X0)
| ( ? [X1] :
( ~ uptakepg(X1)
& ~ gt(X0,X1) )
& ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) )
| sP14_prd(X0) )
& ! [X0] :
( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ~ sP14_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f290]) ).
fof(f292,plain,
( ! [X0] :
( ~ bcapacityne(X0)
| ( ~ uptakepg(sK29_skl(X0))
& ~ gt(X0,sK29_skl(X0))
& releaselg(sK28_skl(X0))
& ~ gt(X0,sK28_skl(X0)) )
| sP14_prd(X0) )
& ! [X0] :
( ( bcapacityne(X0)
& ( ! [X1] :
( uptakepg(X1)
| gt(X0,X1) )
| ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) ) ) )
| ~ sP14_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl]),skolemize(X1,sK28_skl(X0)),skolemize(X1,sK29_skl(X0))],[f291]) ).
fof(f293,plain,
! [X0,X1,X2] :
( uptakepg(X2)
| gt(X0,X2)
| ~ releaselg(X1)
| gt(X0,X1)
| ~ sP14_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f292]) ).
fof(f299,plain,
! [X0] :
( ( ~ qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| sP15_prd(X0) )
& ( ( qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) )
| ~ sP15_prd(X0) ) ),
inference(NNF_transformation,[status(thm)],[f273]) ).
fof(f300,plain,
( ! [X0] :
( ~ qilt27(X0)
| ~ bcapacitysn(X0)
| ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) )
| sP15_prd(X0) )
& ! [X0] :
( ( qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) )
| ~ sP15_prd(X0) ) ),
inference(miniscoping,[status(thm)],[f299]) ).
fof(f301,plain,
( ! [X0] :
( ~ qilt27(X0)
| ~ bcapacitysn(X0)
| ( ~ bsecretioni(sK30_skl(X0))
& ~ gt(X0,sK30_skl(X0)) )
| sP15_prd(X0) )
& ! [X0] :
( ( qilt27(X0)
& bcapacitysn(X0)
& ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) ) )
| ~ sP15_prd(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(X1,sK30_skl(X0))],[f300]) ).
fof(f303,plain,
! [X0] :
( bcapacitysn(X0)
| ~ sP15_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f317,plain,
! [X0] :
( sP14_prd(X0)
| sP10_prd(X0)
| ~ sP6_prd(X0) ),
inference(resolution,[status(thm)],[f228,f269]) ).
fof(f323,plain,
( s3(n0)
| s2(n0)
| ~ drugbg(n0) ),
inference(resolution,[status(thm)],[f124,f173]) ).
fof(f324,definition,
( sQ0_spl
<=> drugbg(n0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f326,plain,
( sQ0_spl
| ~ drugbg(n0) ),
inference(component_clause,[status(thm)],[f324]) ).
fof(f327,definition,
( sQ1_spl
<=> s2(n0) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f328,plain,
( ~ sQ1_spl
| s2(n0) ),
inference(component_clause,[status(thm)],[f327]) ).
fof(f330,definition,
( sQ2_spl
<=> s3(n0) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f331,plain,
( ~ sQ2_spl
| s3(n0) ),
inference(component_clause,[status(thm)],[f330]) ).
fof(f332,plain,
( sQ2_spl
| ~ s3(n0) ),
inference(component_clause,[status(thm)],[f330]) ).
fof(f333,plain,
( sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f323,f324,f327,f330]) ).
fof(f336,plain,
( ~ sQ2_spl
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f331,f101]) ).
fof(f337,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f336,f170]) ).
fof(f338,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f337]) ).
fof(f339,plain,
( sQ0_spl
| qilt27(n0)
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f326,f115]) ).
fof(f341,definition,
( sQ3_spl
<=> s1(n0) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f343,plain,
( sQ3_spl
| ~ s1(n0) ),
inference(component_clause,[status(thm)],[f341]) ).
fof(f344,definition,
( sQ4_spl
<=> qilt27(n0) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f347,plain,
( sQ0_spl
| sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f339,f341,f344,f324]) ).
fof(f349,plain,
( ~ sQ1_spl
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f328,f100]) ).
fof(f350,definition,
( sQ5_spl
<=> gt(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f351,plain,
( ~ sQ5_spl
| gt(n0,n0) ),
inference(component_clause,[status(thm)],[f350]) ).
fof(f360,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f349,f170]) ).
fof(f361,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f360]) ).
fof(f362,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f343,f170]) ).
fof(f363,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f362]) ).
fof(f384,plain,
! [X0] :
( sQ0_spl
| gt(X0,n0)
| releaselg(sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f148,f326]) ).
fof(f385,plain,
! [X0,X1] :
( sQ0_spl
| gt(X1,sK11_skl(X0))
| ~ drugbg(sK2_skl(X1))
| gt(X0,n0) ),
inference(resolution,[status(thm)],[f384,f71]) ).
fof(f386,plain,
! [X0,X1] :
( sQ0_spl
| gt(X1,sK11_skl(X0))
| ~ gt(X1,sK2_skl(X1))
| gt(X0,n0) ),
inference(resolution,[status(thm)],[f384,f70]) ).
fof(f387,plain,
! [X0,X1,X2] :
( sQ0_spl
| gt(X2,n0)
| ~ gt(X2,X1)
| gt(X0,sK11_skl(X1))
| ~ drugbg(sK2_skl(X0)) ),
inference(resolution,[status(thm)],[f385,f46]) ).
fof(f388,plain,
! [X0] :
( sQ0_spl
| gt(X0,sK11_skl(n0))
| ~ drugbg(sK2_skl(X0)) ),
inference(resolution,[status(thm)],[f385,f43]) ).
fof(f418,plain,
! [X0,X1] :
( ~ conditionhyper(X1)
| s2(sK13_skl(X0))
| gt(X0,X1)
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f157,f53]) ).
fof(f419,plain,
! [X0,X1] :
( ~ conditionhyper(X1)
| bcapacityex(sK13_skl(X0))
| bcapacityne(sK13_skl(X0))
| gt(X0,X1)
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f159,f53]) ).
fof(f423,plain,
! [X0,X1] :
( ~ bcapacityex(sK13_skl(X0))
| sP8_prd(sK15_skl(sK13_skl(X0)),sK13_skl(X0))
| gt(n0,sK13_skl(X0))
| ~ conditionhyper(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f418,f175]) ).
fof(f432,plain,
! [X0,X1] :
( gt(sK13_skl(X0),sK15_skl(sK13_skl(X0)))
| ~ bcapacityex(sK13_skl(X0))
| gt(n0,sK13_skl(X0))
| ~ conditionhyper(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f423,f240]) ).
fof(f433,plain,
! [X0,X1] :
( ~ conditionhyper(sK15_skl(sK13_skl(X0)))
| ~ bcapacityex(sK13_skl(X0))
| gt(n0,sK13_skl(X0))
| ~ conditionhyper(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f423,f241]) ).
fof(f446,definition,
( sQ10_spl
<=> sP6_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( sQ10_spl
| ~ sP6_prd(n0) ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f458,plain,
! [X0] :
( sQ10_spl
| uptakepg(X0)
| gt(n0,X0)
| sP5_prd(sK7_skl(n0),n0) ),
inference(resolution,[status(thm)],[f448,f109]) ).
fof(f471,definition,
( sQ15_spl
<=> sP5_prd(sK7_skl(n0),n0) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f472,plain,
( ~ sQ15_spl
| sP5_prd(sK7_skl(n0),n0) ),
inference(component_clause,[status(thm)],[f471]) ).
fof(f479,definition,
! [X0] :
( sQ17_spl
<=> ( uptakepg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f480,plain,
! [X0] :
( ~ sQ17_spl
| uptakepg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f479]) ).
fof(f482,plain,
( sQ10_spl
| sQ17_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f458,f471,f479,f446]) ).
fof(f483,definition,
! [X0] :
( sQ18_spl
<=> ( uptakelg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f484,plain,
! [X0] :
( ~ sQ18_spl
| uptakelg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f483]) ).
fof(f489,definition,
( sQ19_spl
<=> sP10_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f490,plain,
( ~ sQ19_spl
| sP10_prd(n0) ),
inference(component_clause,[status(thm)],[f489]) ).
fof(f493,plain,
! [X0,X1] :
( conditionnormo(X1)
| gt(n0,X1)
| ~ s1(n0)
| ~ conditionhyper(sK15_skl(sK13_skl(n0)))
| ~ bcapacityex(sK13_skl(n0))
| ~ conditionhyper(X0)
| gt(n0,X0)
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f433,f156]) ).
fof(f494,plain,
! [X0,X1,X2] :
( sQ0_spl
| gt(n0,n0)
| gt(X2,sK11_skl(sK13_skl(X0)))
| ~ drugbg(sK2_skl(X2))
| ~ conditionhyper(sK15_skl(sK13_skl(X0)))
| ~ bcapacityex(sK13_skl(X0))
| ~ conditionhyper(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f433,f387]) ).
fof(f496,definition,
! [X0] :
( sQ20_spl
<=> ( ~ conditionhyper(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f497,plain,
! [X0] :
( ~ sQ20_spl
| ~ conditionhyper(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,definition,
( sQ21_spl
<=> bcapacityex(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f501,plain,
( sQ21_spl
| ~ bcapacityex(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,definition,
( sQ22_spl
<=> conditionhyper(sK15_skl(sK13_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f504,plain,
( sQ22_spl
| ~ conditionhyper(sK15_skl(sK13_skl(n0))) ),
inference(component_clause,[status(thm)],[f502]) ).
fof(f505,definition,
! [X1] :
( sQ23_spl
<=> ( conditionnormo(X1)
| gt(n0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f506,plain,
! [X0] :
( ~ sQ23_spl
| conditionnormo(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f505]) ).
fof(f508,plain,
( sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| sQ20_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f493,f341,f496,f499,f502,f505]) ).
fof(f509,definition,
! [X0,X1,X2] :
( sQ24_spl
<=> ( gt(X2,sK11_skl(sK13_skl(X0)))
| ~ drugbg(sK2_skl(X2))
| ~ conditionhyper(sK15_skl(sK13_skl(X0)))
| ~ bcapacityex(sK13_skl(X0))
| ~ conditionhyper(X1)
| gt(X0,X1)
| ~ s1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f512,plain,
( sQ0_spl
| sQ5_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f494,f509,f350,f324]) ).
fof(f513,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f351,f43]) ).
fof(f514,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f513]) ).
fof(f537,plain,
! [X0,X1] :
( conditionhyper(X1)
| ~ gt(X0,X1)
| ~ sP6_prd(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f229,f538]) ).
fof(f538,plain,
! [X0,X1] :
( conditionhyper(X1)
| ~ gt(X0,X1)
| ~ sP10_prd(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f260,f279]) ).
fof(f540,plain,
! [X0,X1] :
( conditionhyper(X1)
| ~ gt(X0,X1)
| sP5_prd(sK7_skl(X0),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f111,f537]) ).
fof(f557,plain,
! [X0,X1] :
( sQ22_spl
| ~ gt(sK13_skl(X0),sK15_skl(sK13_skl(n0)))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f504,f158]) ).
fof(f568,plain,
! [X0] :
( sQ21_spl
| ~ conditionhyper(X0)
| bcapacityne(sK13_skl(n0))
| gt(n0,X0)
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f501,f419]) ).
fof(f576,definition,
( sQ29_spl
<=> bcapacityne(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f577,plain,
( ~ sQ29_spl
| bcapacityne(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f576]) ).
fof(f579,plain,
( sQ21_spl
| sQ29_spl
| sQ20_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f568,f341,f496,f576,f499]) ).
fof(f623,plain,
( ~ sQ29_spl
| sP8_prd(sK15_skl(sK13_skl(n0)),sK13_skl(n0))
| ~ s2(sK13_skl(n0))
| gt(n0,sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f577,f174]) ).
fof(f625,definition,
( sQ38_spl
<=> sP14_prd(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f626,plain,
( ~ sQ38_spl
| sP14_prd(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f625]) ).
fof(f636,definition,
( sQ41_spl
<=> sP9_prd(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f638,plain,
( sQ41_spl
| ~ sP9_prd(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f636]) ).
fof(f666,definition,
( sQ48_spl
<=> gt(n0,sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f667,plain,
( ~ sQ48_spl
| gt(n0,sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f666]) ).
fof(f669,definition,
( sQ49_spl
<=> s2(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f670,plain,
( ~ sQ49_spl
| s2(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f669]) ).
fof(f671,plain,
( sQ49_spl
| ~ s2(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f669]) ).
fof(f672,definition,
( sQ50_spl
<=> sP8_prd(sK15_skl(sK13_skl(n0)),sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f673,plain,
( ~ sQ50_spl
| sP8_prd(sK15_skl(sK13_skl(n0)),sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f672]) ).
fof(f675,plain,
( ~ sQ29_spl
| sQ50_spl
| ~ sQ49_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f623,f666,f669,f672,f576]) ).
fof(f690,plain,
( ~ sQ19_spl
| sP6_prd(n0) ),
inference(resolution,[status(thm)],[f490,f230]) ).
fof(f691,definition,
( sQ54_spl
<=> sP12_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f692,plain,
( ~ sQ54_spl
| sP12_prd(n0) ),
inference(component_clause,[status(thm)],[f691]) ).
fof(f693,plain,
( sQ54_spl
| ~ sP12_prd(n0) ),
inference(component_clause,[status(thm)],[f691]) ).
fof(f694,definition,
( sQ55_spl
<=> sP13_prd(n0) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f695,plain,
( ~ sQ55_spl
| sP13_prd(n0) ),
inference(component_clause,[status(thm)],[f694]) ).
fof(f698,plain,
( ~ sQ19_spl
| sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f690,f448]) ).
fof(f699,plain,
( ~ sQ19_spl
| sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f698]) ).
fof(f774,plain,
( ~ sQ54_spl
| sP15_prd(n0) ),
inference(resolution,[status(thm)],[f692,f278]) ).
fof(f779,plain,
( ~ sQ55_spl
| ~ qilt27(n0) ),
inference(resolution,[status(thm)],[f695,f287]) ).
fof(f789,plain,
( ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f779,f173]) ).
fof(f790,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f789]) ).
fof(f817,plain,
( ~ sQ54_spl
| bcapacitysn(n0) ),
inference(resolution,[status(thm)],[f774,f303]) ).
fof(f826,plain,
( ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f817,f172]) ).
fof(f827,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f826]) ).
fof(f881,definition,
( sQ85_spl
<=> sP13_prd(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f882,plain,
( ~ sQ85_spl
| sP13_prd(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f881]) ).
fof(f962,plain,
( ~ sQ29_spl
| ~ bcapacitysn(sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f577,f49]) ).
fof(f982,definition,
( sQ94_spl
<=> sP10_prd(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f983,plain,
( ~ sQ94_spl
| sP10_prd(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f982]) ).
fof(f1005,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ gt(sK14_skl(X1),X0)
| conditionnormo(X2)
| gt(X1,X2)
| ~ s2(X1)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f497,f164]) ).
fof(f1006,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ gt(sK13_skl(X1),X0)
| conditionnormo(X2)
| gt(X1,X2)
| ~ s1(X1)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f497,f158]) ).
fof(f1011,plain,
( ~ sQ94_spl
| sP13_prd(sK13_skl(n0))
| sP12_prd(sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f983,f259]) ).
fof(f1013,definition,
( sQ97_spl
<=> sP12_prd(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1014,plain,
( ~ sQ97_spl
| sP12_prd(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f1013]) ).
fof(f1016,plain,
( ~ sQ94_spl
| sQ85_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1011,f1013,f881,f982]) ).
fof(f1043,plain,
( ~ sQ97_spl
| sP15_prd(sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f1014,f278]) ).
fof(f1044,plain,
( ~ sQ97_spl
| sP10_prd(sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f1014,f261]) ).
fof(f1108,plain,
( ~ sQ97_spl
| bcapacitysn(sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f1043,f303]) ).
fof(f1109,definition,
( sQ99_spl
<=> gt(sK13_skl(n0),sK26_skl(sK13_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1110,plain,
( ~ sQ99_spl
| gt(sK13_skl(n0),sK26_skl(sK13_skl(n0))) ),
inference(component_clause,[status(thm)],[f1109]) ).
fof(f1113,definition,
( sQ100_spl
<=> conditionhyper(sK26_skl(sK13_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1115,plain,
( sQ100_spl
| ~ conditionhyper(sK26_skl(sK13_skl(n0))) ),
inference(component_clause,[status(thm)],[f1113]) ).
fof(f1117,plain,
( ~ sQ97_spl
| ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1108,f962]) ).
fof(f1118,plain,
( ~ sQ97_spl
| ~ sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f1117]) ).
fof(f1125,plain,
! [X0] :
( ~ sQ48_spl
| conditionnormo(X0)
| gt(n0,X0)
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f667,f156]) ).
fof(f1132,plain,
( ~ sQ48_spl
| sQ23_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1125,f341,f505,f666]) ).
fof(f1182,plain,
! [X0,X1,X2] :
( sP10_prd(X0)
| ~ sP6_prd(X0)
| uptakepg(X2)
| gt(X0,X2)
| ~ releaselg(X1)
| gt(X0,X1) ),
inference(resolution,[status(thm)],[f293,f317]) ).
fof(f1184,plain,
! [X0,X1] :
( ~ sQ38_spl
| uptakepg(X1)
| gt(sK13_skl(n0),X1)
| ~ releaselg(X0)
| gt(sK13_skl(n0),X0) ),
inference(resolution,[status(thm)],[f626,f293]) ).
fof(f1187,definition,
! [X0] :
( sQ103_spl
<=> ( ~ releaselg(X0)
| gt(sK13_skl(n0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1188,plain,
! [X0] :
( ~ sQ103_spl
| ~ releaselg(X0)
| gt(sK13_skl(n0),X0) ),
inference(component_clause,[status(thm)],[f1187]) ).
fof(f1190,definition,
! [X1] :
( sQ104_spl
<=> ( uptakepg(X1)
| gt(sK13_skl(n0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1191,plain,
! [X0] :
( ~ sQ104_spl
| uptakepg(X0)
| gt(sK13_skl(n0),X0) ),
inference(component_clause,[status(thm)],[f1190]) ).
fof(f1193,plain,
( ~ sQ38_spl
| sQ104_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f1184,f1187,f1190,f625]) ).
fof(f1216,plain,
! [X0,X1] :
( ~ conditionnormo(sK7_skl(X0))
| conditionhyper(X1)
| ~ gt(X0,X1) ),
inference(resolution,[status(thm)],[f540,f219]) ).
fof(f1329,plain,
! [X0,X1] :
( sQ0_spl
| gt(X1,sK11_skl(X0))
| ~ drugbg(sK2_skl(X1))
| ~ conditionnormo(sK7_skl(X0))
| conditionhyper(n0) ),
inference(resolution,[status(thm)],[f1216,f385]) ).
fof(f1334,definition,
( sQ114_spl
<=> conditionnormo(sK7_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1336,plain,
( sQ114_spl
| ~ conditionnormo(sK7_skl(n0)) ),
inference(component_clause,[status(thm)],[f1334]) ).
fof(f1338,definition,
( sQ115_spl
<=> conditionhyper(n0) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1339,plain,
( ~ sQ115_spl
| conditionhyper(n0) ),
inference(component_clause,[status(thm)],[f1338]) ).
fof(f1341,definition,
! [X0,X1] :
( sQ116_spl
<=> ( gt(X1,sK11_skl(X0))
| ~ drugbg(sK2_skl(X1))
| ~ conditionnormo(sK7_skl(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1344,plain,
( sQ0_spl
| sQ116_spl
| sQ115_spl ),
inference(split_clause,[status(thm)],[f1329,f1338,f1341,f324]) ).
fof(f1345,plain,
( ~ sQ20_spl
| ~ sQ115_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f1339,f497]) ).
fof(f1346,plain,
( ~ sQ20_spl
| ~ sQ115_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1345,f350,f1338,f496]) ).
fof(f1437,plain,
! [X0,X1,X2,X3] :
( drugi(X3)
| gt(X2,X3)
| sP10_prd(X0)
| ~ sP6_prd(X0)
| gt(X0,sK9_skl(X2))
| ~ releaselg(X1)
| gt(X0,X1) ),
inference(resolution,[status(thm)],[f1182,f135]) ).
fof(f1453,plain,
! [X0] :
( sQ114_spl
| bcapacityex(sK13_skl(X0))
| bcapacityne(sK13_skl(X0))
| gt(X0,sK7_skl(n0))
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f1336,f159]) ).
fof(f1454,plain,
! [X0] :
( sQ114_spl
| s2(sK13_skl(X0))
| gt(X0,sK7_skl(n0))
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f1336,f157]) ).
fof(f1477,plain,
! [X0] :
( sQ0_spl
| ~ sQ103_spl
| gt(X0,n0)
| gt(sK13_skl(n0),sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f1188,f384]) ).
fof(f1483,plain,
! [X0,X1] :
( ~ sQ104_spl
| drugi(X1)
| gt(X0,X1)
| gt(sK13_skl(n0),sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f1191,f135]) ).
fof(f1539,plain,
! [X0,X1,X2,X3] :
( s3(X3)
| gt(X2,X3)
| sP10_prd(X0)
| ~ sP6_prd(X0)
| gt(X0,sK9_skl(X2))
| ~ releaselg(X1)
| gt(X0,X1) ),
inference(resolution,[status(thm)],[f1437,f129]) ).
fof(f1556,plain,
( ~ sQ50_spl
| gt(sK13_skl(n0),sK15_skl(sK13_skl(n0))) ),
inference(resolution,[status(thm)],[f673,f240]) ).
fof(f1751,plain,
! [X0,X1,X2,X3] :
( sP13_prd(X0)
| sP12_prd(X0)
| s3(X3)
| gt(X2,X3)
| ~ sP6_prd(X0)
| gt(X0,sK9_skl(X2))
| ~ releaselg(X1)
| gt(X0,X1) ),
inference(resolution,[status(thm)],[f1539,f259]) ).
fof(f1753,definition,
! [X0] :
( sQ135_spl
<=> ( ~ releaselg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f1754,plain,
! [X0] :
( ~ sQ135_spl
| ~ releaselg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f1753]) ).
fof(f1756,definition,
! [X1,X2] :
( sQ136_spl
<=> ( s3(X2)
| gt(X1,X2)
| gt(n0,sK9_skl(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1757,plain,
! [X0,X1] :
( ~ sQ136_spl
| s3(X1)
| gt(X0,X1)
| gt(n0,sK9_skl(X0)) ),
inference(component_clause,[status(thm)],[f1756]) ).
fof(f1760,plain,
! [X0,X1,X2,X3] :
( sP12_prd(X0)
| s3(X3)
| gt(X2,X3)
| ~ sP6_prd(X0)
| gt(X0,sK9_skl(X2))
| ~ releaselg(X1)
| gt(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1751,f285]) ).
fof(f1792,plain,
! [X0,X1] :
( ~ sQ18_spl
| drugi(X1)
| gt(X0,X1)
| gt(n0,sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f484,f133]) ).
fof(f1796,plain,
! [X0,X1] :
( ~ sQ17_spl
| drugi(X1)
| gt(X0,X1)
| gt(n0,sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f480,f135]) ).
fof(f1813,plain,
! [X0] :
( sQ0_spl
| ~ sQ135_spl
| gt(X0,n0)
| gt(n0,sK11_skl(X0)) ),
inference(resolution,[status(thm)],[f1754,f384]) ).
fof(f1818,plain,
! [X0,X1,X2] :
( sQ0_spl
| ~ sQ20_spl
| gt(X2,sK11_skl(sK14_skl(X0)))
| ~ drugbg(sK2_skl(X2))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s2(X0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f1005,f385]) ).
fof(f1819,definition,
! [X0,X1,X2] :
( sQ137_spl
<=> ( gt(X2,sK11_skl(sK14_skl(X0)))
| ~ drugbg(sK2_skl(X2))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s2(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1822,plain,
( sQ0_spl
| ~ sQ20_spl
| sQ137_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1818,f350,f1819,f496,f324]) ).
fof(f1829,plain,
( ~ sQ49_spl
| ~ bcapacityex(sK13_skl(n0))
| sP8_prd(sK15_skl(sK13_skl(n0)),sK13_skl(n0))
| gt(n0,sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f670,f175]) ).
fof(f1842,plain,
( ~ sQ49_spl
| ~ sQ21_spl
| sQ50_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1829,f666,f672,f499,f669]) ).
fof(f1849,definition,
( sQ142_spl
<=> s3(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1850,plain,
( ~ sQ142_spl
| s3(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f1849]) ).
fof(f1915,plain,
! [X0] :
( sQ0_spl
| ~ sQ135_spl
| drugbg(X0)
| gt(n0,X0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f1813,f147]) ).
fof(f1919,definition,
! [X0] :
( sQ149_spl
<=> ( drugbg(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1920,plain,
! [X0] :
( ~ sQ149_spl
| drugbg(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f1919]) ).
fof(f1922,plain,
( sQ0_spl
| ~ sQ135_spl
| sQ149_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1915,f350,f1919,f1753,f324]) ).
fof(f1942,plain,
( sQ0_spl
| ~ sQ149_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f1920,f326]) ).
fof(f1943,plain,
( sQ0_spl
| ~ sQ149_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f1942,f350,f1919,f324]) ).
fof(f1961,plain,
( ~ sQ50_spl
| ~ conditionhyper(sK15_skl(sK13_skl(n0))) ),
inference(resolution,[status(thm)],[f673,f241]) ).
fof(f1988,definition,
( sQ153_spl
<=> bcapacitysn(n0) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1989,plain,
( ~ sQ153_spl
| bcapacitysn(n0) ),
inference(component_clause,[status(thm)],[f1988]) ).
fof(f2004,plain,
( ~ sQ153_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1989,f172]) ).
fof(f2005,plain,
~ sQ153_spl,
inference(contradiction_clause,[status(thm)],[f2004]) ).
fof(f2149,plain,
! [X0,X1] :
( ~ sQ136_spl
| drugi(X1)
| gt(n0,X1)
| s3(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f1757,f134]) ).
fof(f2153,definition,
! [X0] :
( sQ166_spl
<=> ( s3(X0)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f2154,plain,
! [X0] :
( ~ sQ166_spl
| s3(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f2153]) ).
fof(f2156,definition,
! [X1] :
( sQ167_spl
<=> ( drugi(X1)
| gt(n0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f2157,plain,
! [X0] :
( ~ sQ167_spl
| drugi(X0)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f2156]) ).
fof(f2159,plain,
( ~ sQ136_spl
| sQ167_spl
| sQ166_spl ),
inference(split_clause,[status(thm)],[f2149,f2153,f2156,f1756]) ).
fof(f2160,definition,
! [X0,X1] :
( sQ168_spl
<=> ( conditionhyper(sK9_skl(X0))
| s3(X1)
| gt(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f2161,plain,
! [X0,X1] :
( ~ sQ168_spl
| conditionhyper(sK9_skl(X0))
| s3(X1)
| gt(X0,X1) ),
inference(component_clause,[status(thm)],[f2160]) ).
fof(f2174,plain,
! [X0] :
( ~ sQ167_spl
| s3(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f2157,f129]) ).
fof(f2175,plain,
( sQ2_spl
| ~ sQ166_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f2154,f332]) ).
fof(f2179,plain,
( sQ2_spl
| ~ sQ166_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f2175,f350,f2153,f330]) ).
fof(f2182,plain,
( sQ2_spl
| ~ sQ167_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f2174,f332]) ).
fof(f2186,plain,
( sQ2_spl
| ~ sQ167_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f2182,f350,f2156,f330]) ).
fof(f2188,plain,
! [X0,X1] :
( ~ sQ18_spl
| s3(X1)
| gt(X0,X1)
| gt(n0,sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f1792,f129]) ).
fof(f2190,plain,
! [X0,X1] :
( ~ sQ17_spl
| s3(X1)
| gt(X0,X1)
| gt(n0,sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f1796,f129]) ).
fof(f2191,plain,
( ~ sQ17_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f2190,f1756,f479]) ).
fof(f2212,plain,
! [X0,X1,X2] :
( sQ54_spl
| s3(X2)
| gt(X1,X2)
| ~ sP6_prd(n0)
| gt(n0,sK9_skl(X1))
| ~ releaselg(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f1760,f693]) ).
fof(f2216,plain,
( sQ54_spl
| ~ sQ10_spl
| sQ136_spl
| sQ135_spl ),
inference(split_clause,[status(thm)],[f2212,f1753,f1756,f446,f691]) ).
fof(f2224,plain,
! [X0,X1] :
( ~ sQ18_spl
| drugi(X1)
| gt(n0,X1)
| s3(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f2188,f132]) ).
fof(f2228,plain,
( ~ sQ18_spl
| sQ167_spl
| sQ166_spl ),
inference(split_clause,[status(thm)],[f2224,f2153,f2156,f483]) ).
fof(f2229,definition,
! [X0,X1] :
( sQ171_spl
<=> ( conditionhyper(sK8_skl(X0))
| s3(X1)
| gt(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f2230,plain,
! [X0,X1] :
( ~ sQ171_spl
| conditionhyper(sK8_skl(X0))
| s3(X1)
| gt(X0,X1) ),
inference(component_clause,[status(thm)],[f2229]) ).
fof(f2237,plain,
! [X0] :
( ~ sQ50_spl
| sQ22_spl
| conditionnormo(X0)
| gt(n0,X0)
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f557,f1556]) ).
fof(f2238,plain,
! [X0,X1] :
( sQ22_spl
| ~ bcapacityex(sK13_skl(n0))
| gt(n0,sK13_skl(n0))
| ~ conditionhyper(X1)
| gt(n0,X1)
| ~ s1(n0)
| conditionnormo(X0)
| gt(n0,X0)
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f557,f432]) ).
fof(f2239,plain,
( ~ sQ50_spl
| sQ22_spl
| sQ23_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2237,f341,f505,f502,f672]) ).
fof(f2240,plain,
( sQ22_spl
| ~ sQ21_spl
| sQ48_spl
| sQ20_spl
| sQ23_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2238,f341,f505,f496,f666,f499,f502]) ).
fof(f2269,plain,
( sQ114_spl
| sQ49_spl
| gt(n0,sK7_skl(n0))
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f671,f1454]) ).
fof(f2277,definition,
( sQ174_spl
<=> gt(n0,sK7_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f2280,plain,
( sQ114_spl
| sQ49_spl
| sQ174_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2269,f341,f2277,f669,f1334]) ).
fof(f2284,plain,
( ~ sQ50_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f1961,f502,f672]) ).
fof(f2302,plain,
! [X0,X1] :
( ~ sQ171_spl
| ~ sQ20_spl
| s3(X1)
| gt(X0,X1)
| gt(n0,sK8_skl(X0)) ),
inference(resolution,[status(thm)],[f497,f2230]) ).
fof(f2303,plain,
! [X0,X1] :
( ~ sQ168_spl
| ~ sQ20_spl
| s3(X1)
| gt(X0,X1)
| gt(n0,sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f497,f2161]) ).
fof(f2313,plain,
( ~ sQ168_spl
| ~ sQ20_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f2303,f1756,f496,f2160]) ).
fof(f2330,plain,
( sQ114_spl
| sQ21_spl
| bcapacityne(sK13_skl(n0))
| gt(n0,sK7_skl(n0))
| ~ s1(n0) ),
inference(resolution,[status(thm)],[f501,f1453]) ).
fof(f2341,plain,
( sQ114_spl
| sQ21_spl
| sQ29_spl
| sQ174_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f2330,f341,f2277,f576,f499,f1334]) ).
fof(f2383,definition,
( sQ175_spl
<=> sP15_prd(sK13_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f2384,plain,
( ~ sQ175_spl
| sP15_prd(sK13_skl(n0)) ),
inference(component_clause,[status(thm)],[f2383]) ).
fof(f2402,plain,
( ~ sQ175_spl
| gt(sK13_skl(n0),sK26_skl(sK13_skl(n0)))
| sP12_prd(sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f2384,f280]) ).
fof(f2403,plain,
( ~ sQ175_spl
| ~ conditionhyper(sK26_skl(sK13_skl(n0)))
| sP12_prd(sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f2384,f281]) ).
fof(f2407,plain,
( ~ sQ175_spl
| sQ99_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f2402,f1013,f1109,f2383]) ).
fof(f2408,plain,
( ~ sQ175_spl
| ~ sQ100_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f2403,f1013,f1113,f2383]) ).
fof(f2428,plain,
( ~ sQ142_spl
| ~ s2(sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f1850,f102]) ).
fof(f2430,plain,
( ~ sQ142_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f2428,f669,f1849]) ).
fof(f2451,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ bcapacityex(sK13_skl(X0))
| gt(n0,sK13_skl(X0))
| ~ conditionhyper(X2)
| gt(X0,X2)
| ~ s1(X0)
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0)
| gt(n0,sK15_skl(sK13_skl(X0))) ),
inference(resolution,[status(thm)],[f1006,f432]) ).
fof(f2452,plain,
! [X0,X1,X2] :
( sQ0_spl
| ~ sQ20_spl
| gt(X2,sK11_skl(sK13_skl(X0)))
| ~ drugbg(sK2_skl(X2))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f1006,f385]) ).
fof(f2453,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ bcapacityex(sK13_skl(X0))
| gt(n0,sK13_skl(X0))
| ~ conditionhyper(X2)
| gt(X0,X2)
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0)
| gt(n0,sK15_skl(sK13_skl(X0))) ),
inference(duplicate_literals_removal,[status(thm)],[f2451]) ).
fof(f2454,definition,
! [X0,X1,X2] :
( sQ182_spl
<=> ( gt(X2,sK11_skl(sK13_skl(X0)))
| ~ drugbg(sK2_skl(X2))
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition]) ).
fof(f2457,plain,
( sQ0_spl
| ~ sQ20_spl
| sQ182_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f2452,f350,f2454,f496,f324]) ).
fof(f2486,plain,
( sQ100_spl
| conditionnormo(sK26_skl(sK13_skl(n0)))
| conditionhypo(sK26_skl(sK13_skl(n0))) ),
inference(resolution,[status(thm)],[f1115,f51]) ).
fof(f2487,plain,
( sQ100_spl
| ~ gt(n0,sK26_skl(sK13_skl(n0))) ),
inference(resolution,[status(thm)],[f1115,f171]) ).
fof(f2488,definition,
( sQ183_spl
<=> conditionhypo(sK26_skl(sK13_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f2489,plain,
( ~ sQ183_spl
| conditionhypo(sK26_skl(sK13_skl(n0))) ),
inference(component_clause,[status(thm)],[f2488]) ).
fof(f2491,definition,
( sQ184_spl
<=> conditionnormo(sK26_skl(sK13_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f2494,plain,
( sQ100_spl
| sQ184_spl
| sQ183_spl ),
inference(split_clause,[status(thm)],[f2486,f2488,f2491,f1113]) ).
fof(f2503,plain,
( ~ sQ183_spl
| ~ conditionhyper(sK26_skl(sK13_skl(n0))) ),
inference(resolution,[status(thm)],[f2489,f52]) ).
fof(f2516,plain,
! [X0] :
( ~ sQ20_spl
| ~ sQ99_spl
| conditionnormo(X0)
| gt(n0,X0)
| ~ s1(n0)
| gt(n0,sK26_skl(sK13_skl(n0))) ),
inference(resolution,[status(thm)],[f1110,f1006]) ).
fof(f2520,definition,
( sQ185_spl
<=> gt(n0,sK26_skl(sK13_skl(n0))) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f2521,plain,
( ~ sQ185_spl
| gt(n0,sK26_skl(sK13_skl(n0))) ),
inference(component_clause,[status(thm)],[f2520]) ).
fof(f2523,plain,
( ~ sQ20_spl
| ~ sQ99_spl
| sQ23_spl
| ~ sQ3_spl
| sQ185_spl ),
inference(split_clause,[status(thm)],[f2516,f2520,f341,f505,f1109,f496]) ).
fof(f2525,definition,
! [X0] :
( sQ186_spl
<=> ( gt(X0,sK11_skl(sK26_skl(sK13_skl(n0))))
| ~ drugbg(sK2_skl(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f2529,plain,
( ~ sQ183_spl
| ~ sQ100_spl ),
inference(split_clause,[status(thm)],[f2503,f1113,f2488]) ).
fof(f2561,plain,
! [X0] :
( sQ0_spl
| ~ sQ185_spl
| gt(n0,n0)
| gt(X0,sK11_skl(sK26_skl(sK13_skl(n0))))
| ~ drugbg(sK2_skl(X0)) ),
inference(resolution,[status(thm)],[f2521,f387]) ).
fof(f2564,plain,
( sQ0_spl
| ~ sQ185_spl
| sQ5_spl
| sQ186_spl ),
inference(split_clause,[status(thm)],[f2561,f2525,f350,f2520,f324]) ).
fof(f2582,plain,
! [X0,X1] :
( sQ41_spl
| uptakepg(X1)
| gt(sK13_skl(n0),X1)
| ~ releaselg(X0)
| gt(sK13_skl(n0),X0) ),
inference(resolution,[status(thm)],[f638,f250]) ).
fof(f2586,plain,
( sQ41_spl
| sQ104_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f2582,f1187,f1190,f636]) ).
fof(f2632,plain,
( sQ114_spl
| ~ sQ23_spl
| gt(n0,sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f506,f1336]) ).
fof(f2636,plain,
( ~ sQ185_spl
| sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2521,f2487]) ).
fof(f2637,plain,
( ~ sQ185_spl
| sQ100_spl ),
inference(contradiction_clause,[status(thm)],[f2636]) ).
fof(f2854,plain,
! [X0,X1] :
( ~ sQ171_spl
| ~ sQ20_spl
| drugi(X1)
| gt(n0,X1)
| s3(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f2302,f132]) ).
fof(f2858,plain,
( ~ sQ171_spl
| ~ sQ20_spl
| sQ167_spl
| sQ166_spl ),
inference(split_clause,[status(thm)],[f2854,f2153,f2156,f496,f2229]) ).
fof(f3002,plain,
! [X0,X1] :
( ~ sQ104_spl
| s3(X1)
| gt(X0,X1)
| gt(sK13_skl(n0),sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f1483,f129]) ).
fof(f3081,plain,
! [X0] :
( sQ2_spl
| ~ sQ104_spl
| gt(X0,n0)
| gt(sK13_skl(n0),sK9_skl(X0)) ),
inference(resolution,[status(thm)],[f3002,f332]) ).
fof(f3085,plain,
! [X0,X1] :
( ~ sQ20_spl
| sQ2_spl
| ~ sQ104_spl
| conditionnormo(X1)
| gt(n0,X1)
| ~ s1(n0)
| gt(n0,sK9_skl(X0))
| gt(X0,n0) ),
inference(resolution,[status(thm)],[f3081,f1006]) ).
fof(f3090,definition,
! [X0] :
( sQ207_spl
<=> ( gt(n0,sK9_skl(X0))
| gt(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f3091,plain,
! [X0] :
( ~ sQ207_spl
| gt(n0,sK9_skl(X0))
| gt(X0,n0) ),
inference(component_clause,[status(thm)],[f3090]) ).
fof(f3093,plain,
( ~ sQ20_spl
| sQ2_spl
| ~ sQ104_spl
| sQ23_spl
| ~ sQ3_spl
| sQ207_spl ),
inference(split_clause,[status(thm)],[f3085,f3090,f341,f505,f1190,f330,f496]) ).
fof(f3094,definition,
! [X0] :
( sQ208_spl
<=> ( drugi(X0)
| gt(sK13_skl(n0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f3095,plain,
! [X0] :
( ~ sQ208_spl
| drugi(X0)
| gt(sK13_skl(n0),X0) ),
inference(component_clause,[status(thm)],[f3094]) ).
fof(f3107,plain,
! [X0] :
( ~ sQ208_spl
| s3(X0)
| gt(sK13_skl(n0),X0) ),
inference(resolution,[status(thm)],[f3095,f129]) ).
fof(f3110,plain,
! [X0] :
( ~ sQ208_spl
| ~ s2(X0)
| gt(sK13_skl(n0),X0) ),
inference(resolution,[status(thm)],[f3107,f102]) ).
fof(f3112,plain,
( ~ sQ49_spl
| ~ sQ208_spl
| gt(sK13_skl(n0),sK13_skl(n0)) ),
inference(resolution,[status(thm)],[f3110,f670]) ).
fof(f3117,plain,
( ~ sQ49_spl
| ~ sQ208_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3112,f43]) ).
fof(f3118,plain,
( ~ sQ49_spl
| ~ sQ208_spl ),
inference(contradiction_clause,[status(thm)],[f3117]) ).
fof(f3119,plain,
! [X0] :
( ~ sQ207_spl
| drugi(X0)
| gt(n0,X0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f3091,f134]) ).
fof(f3123,plain,
( ~ sQ207_spl
| sQ167_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f3119,f350,f2156,f3090]) ).
fof(f3344,plain,
! [X0] :
( ~ sQ85_spl
| ~ releaselg(X0)
| gt(sK13_skl(n0),X0) ),
inference(resolution,[status(thm)],[f882,f285]) ).
fof(f3459,plain,
! [X0,X1,X2,X3] :
( sQ0_spl
| ~ sQ20_spl
| gt(n0,n0)
| gt(X3,sK11_skl(sK15_skl(sK13_skl(X0))))
| ~ drugbg(sK2_skl(X3))
| ~ bcapacityex(sK13_skl(X0))
| gt(n0,sK13_skl(X0))
| ~ conditionhyper(X2)
| gt(X0,X2)
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0) ),
inference(resolution,[status(thm)],[f2453,f387]) ).
fof(f3465,definition,
! [X0,X1,X2,X3] :
( sQ235_spl
<=> ( gt(X3,sK11_skl(sK15_skl(sK13_skl(X0))))
| ~ drugbg(sK2_skl(X3))
| ~ bcapacityex(sK13_skl(X0))
| gt(n0,sK13_skl(X0))
| ~ conditionhyper(X2)
| gt(X0,X2)
| conditionnormo(X1)
| gt(X0,X1)
| ~ s1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f3468,plain,
( sQ0_spl
| ~ sQ20_spl
| sQ5_spl
| sQ235_spl ),
inference(split_clause,[status(thm)],[f3459,f3465,f350,f496,f324]) ).
fof(f3472,plain,
! [X0,X1] :
( ~ sQ20_spl
| sQ0_spl
| ~ sQ103_spl
| conditionnormo(X1)
| gt(n0,X1)
| ~ s1(n0)
| gt(n0,sK11_skl(X0))
| gt(X0,n0) ),
inference(resolution,[status(thm)],[f1477,f1006]) ).
fof(f3477,definition,
! [X0] :
( sQ236_spl
<=> ( gt(n0,sK11_skl(X0))
| gt(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition]) ).
fof(f3478,plain,
! [X0] :
( ~ sQ236_spl
| gt(n0,sK11_skl(X0))
| gt(X0,n0) ),
inference(component_clause,[status(thm)],[f3477]) ).
fof(f3480,plain,
( ~ sQ20_spl
| sQ0_spl
| ~ sQ103_spl
| sQ23_spl
| ~ sQ3_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f3472,f3477,f341,f505,f1187,f324,f496]) ).
fof(f3481,definition,
! [X0] :
( sQ237_spl
<=> ( drugbg(X0)
| gt(sK13_skl(n0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f3482,plain,
! [X0] :
( ~ sQ237_spl
| drugbg(X0)
| gt(sK13_skl(n0),X0) ),
inference(component_clause,[status(thm)],[f3481]) ).
fof(f3517,plain,
! [X0] :
( sQ0_spl
| ~ sQ237_spl
| gt(X0,sK11_skl(n0))
| gt(sK13_skl(n0),sK2_skl(X0)) ),
inference(resolution,[status(thm)],[f3482,f388]) ).
fof(f3534,plain,
! [X0] :
( ~ sQ236_spl
| drugbg(X0)
| gt(n0,X0)
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f3478,f147]) ).
fof(f3538,plain,
( ~ sQ236_spl
| sQ149_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f3534,f350,f1919,f3477]) ).
fof(f3541,plain,
( ~ sQ85_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f3344,f1187,f881]) ).
fof(f3669,plain,
! [X0] :
( sQ0_spl
| ~ sQ237_spl
| drugbg(X0)
| gt(n0,X0)
| gt(sK13_skl(n0),sK2_skl(n0)) ),
inference(resolution,[status(thm)],[f3517,f147]) ).
fof(f3677,definition,
( sQ240_spl
<=> gt(n0,sK11_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition]) ).
fof(f3678,plain,
( ~ sQ240_spl
| gt(n0,sK11_skl(n0)) ),
inference(component_clause,[status(thm)],[f3677]) ).
fof(f3685,definition,
( sQ242_spl
<=> gt(sK13_skl(n0),sK2_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f3686,plain,
( ~ sQ242_spl
| gt(sK13_skl(n0),sK2_skl(n0)) ),
inference(component_clause,[status(thm)],[f3685]) ).
fof(f3687,plain,
( sQ242_spl
| ~ gt(sK13_skl(n0),sK2_skl(n0)) ),
inference(component_clause,[status(thm)],[f3685]) ).
fof(f3688,plain,
( sQ0_spl
| ~ sQ237_spl
| sQ149_spl
| sQ242_spl ),
inference(split_clause,[status(thm)],[f3669,f3685,f1919,f3481,f324]) ).
fof(f3692,definition,
( sQ244_spl
<=> conditionhyper(sK11_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f3693,plain,
( ~ sQ244_spl
| conditionhyper(sK11_skl(n0)) ),
inference(component_clause,[status(thm)],[f3692]) ).
fof(f3694,plain,
( sQ244_spl
| ~ conditionhyper(sK11_skl(n0)) ),
inference(component_clause,[status(thm)],[f3692]) ).
fof(f3696,definition,
! [X0] :
( sQ245_spl
<=> ( gt(X0,n0)
| gt(sK13_skl(n0),sK2_skl(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f3697,plain,
! [X0] :
( ~ sQ245_spl
| gt(X0,n0)
| gt(sK13_skl(n0),sK2_skl(X0)) ),
inference(component_clause,[status(thm)],[f3696]) ).
fof(f3703,plain,
( ~ sQ20_spl
| ~ sQ244_spl
| gt(n0,sK11_skl(n0)) ),
inference(resolution,[status(thm)],[f3693,f497]) ).
fof(f3704,plain,
! [X0] :
( ~ sQ240_spl
| drugbg(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f3678,f147]) ).
fof(f3708,plain,
( ~ sQ240_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f3704,f1919,f3677]) ).
fof(f3711,plain,
! [X0] :
( ~ sQ20_spl
| ~ sQ244_spl
| drugbg(X0)
| gt(n0,X0) ),
inference(resolution,[status(thm)],[f3703,f147]) ).
fof(f3715,plain,
( ~ sQ20_spl
| ~ sQ244_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f3711,f1919,f3692,f496]) ).
fof(f3722,plain,
( sQ244_spl
| conditionnormo(sK11_skl(n0))
| conditionhypo(sK11_skl(n0)) ),
inference(resolution,[status(thm)],[f3694,f51]) ).
fof(f3724,definition,
( sQ247_spl
<=> conditionhypo(sK11_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition]) ).
fof(f3727,definition,
( sQ248_spl
<=> conditionnormo(sK11_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition]) ).
fof(f3730,plain,
( sQ244_spl
| sQ248_spl
| sQ247_spl ),
inference(split_clause,[status(thm)],[f3722,f3724,f3727,f3692]) ).
fof(f3740,plain,
! [X0] :
( ~ sQ20_spl
| ~ sQ242_spl
| conditionnormo(X0)
| gt(n0,X0)
| ~ s1(n0)
| gt(n0,sK2_skl(n0)) ),
inference(resolution,[status(thm)],[f3686,f1006]) ).
fof(f3744,definition,
( sQ249_spl
<=> gt(n0,sK2_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f3745,plain,
( ~ sQ249_spl
| gt(n0,sK2_skl(n0)) ),
inference(component_clause,[status(thm)],[f3744]) ).
fof(f3746,plain,
( sQ249_spl
| ~ gt(n0,sK2_skl(n0)) ),
inference(component_clause,[status(thm)],[f3744]) ).
fof(f3747,plain,
( ~ sQ20_spl
| ~ sQ242_spl
| sQ23_spl
| ~ sQ3_spl
| sQ249_spl ),
inference(split_clause,[status(thm)],[f3740,f3744,f341,f505,f3685,f496]) ).
fof(f3748,definition,
( sQ250_spl
<=> conditionhyper(sK2_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f3749,plain,
( ~ sQ250_spl
| conditionhyper(sK2_skl(n0)) ),
inference(component_clause,[status(thm)],[f3748]) ).
fof(f3750,plain,
( sQ250_spl
| ~ conditionhyper(sK2_skl(n0)) ),
inference(component_clause,[status(thm)],[f3748]) ).
fof(f3756,plain,
( ~ sQ20_spl
| ~ sQ250_spl
| gt(n0,sK2_skl(n0)) ),
inference(resolution,[status(thm)],[f3749,f497]) ).
fof(f3765,plain,
! [X0] :
( sQ0_spl
| ~ sQ249_spl
| gt(n0,sK11_skl(X0))
| gt(X0,n0) ),
inference(resolution,[status(thm)],[f3745,f386]) ).
fof(f3770,plain,
( sQ0_spl
| ~ sQ249_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f3765,f3477,f3744,f324]) ).
fof(f3804,plain,
! [X0] :
( sQ0_spl
| ~ sQ20_spl
| ~ sQ250_spl
| gt(n0,sK11_skl(X0))
| gt(X0,n0) ),
inference(resolution,[status(thm)],[f3756,f386]) ).
fof(f3809,plain,
( sQ0_spl
| ~ sQ20_spl
| ~ sQ250_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f3804,f3477,f3748,f496,f324]) ).
fof(f3816,plain,
( sQ250_spl
| conditionnormo(sK2_skl(n0))
| conditionhypo(sK2_skl(n0)) ),
inference(resolution,[status(thm)],[f3750,f51]) ).
fof(f3818,definition,
( sQ252_spl
<=> conditionhypo(sK2_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition]) ).
fof(f3821,definition,
( sQ253_spl
<=> conditionnormo(sK2_skl(n0)) ),
introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition]) ).
fof(f3824,plain,
( sQ250_spl
| sQ253_spl
| sQ252_spl ),
inference(split_clause,[status(thm)],[f3816,f3818,f3821,f3748]) ).
fof(f3830,plain,
( sQ242_spl
| ~ sQ245_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f3697,f3687]) ).
fof(f3845,plain,
( sQ242_spl
| ~ sQ245_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f3830,f350,f3696,f3685]) ).
fof(f3846,definition,
! [X0] :
( sQ254_spl
<=> ( gt(n0,sK2_skl(X0))
| gt(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[sQ254_spl])],[split_symbol_definition]) ).
fof(f3847,plain,
! [X0] :
( ~ sQ254_spl
| gt(n0,sK2_skl(X0))
| gt(X0,n0) ),
inference(component_clause,[status(thm)],[f3846]) ).
fof(f3883,definition,
! [X0] :
( sQ263_spl
<=> ( gt(sK13_skl(n0),sK11_skl(X0))
| gt(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f3884,plain,
! [X0] :
( ~ sQ263_spl
| gt(sK13_skl(n0),sK11_skl(X0))
| gt(X0,n0) ),
inference(component_clause,[status(thm)],[f3883]) ).
fof(f3914,plain,
( sQ249_spl
| ~ sQ254_spl
| gt(n0,n0) ),
inference(resolution,[status(thm)],[f3847,f3746]) ).
fof(f3928,plain,
( sQ249_spl
| ~ sQ254_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f3914,f350,f3846,f3744]) ).
fof(f3968,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ sQ263_spl
| conditionnormo(X1)
| gt(n0,X1)
| ~ s1(n0)
| gt(n0,sK11_skl(X0))
| gt(X0,n0) ),
inference(resolution,[status(thm)],[f3884,f1006]) ).
fof(f3974,plain,
( ~ sQ20_spl
| ~ sQ263_spl
| sQ23_spl
| ~ sQ3_spl
| sQ236_spl ),
inference(split_clause,[status(thm)],[f3968,f3477,f341,f505,f3883,f496]) ).
fof(f3984,plain,
( ~ sQ15_spl
| ~ conditionnormo(sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f472,f219]) ).
fof(f3985,plain,
( ~ sQ15_spl
| ~ gt(n0,sK7_skl(n0)) ),
inference(resolution,[status(thm)],[f472,f218]) ).
fof(f3986,plain,
( ~ sQ15_spl
| ~ sQ114_spl ),
inference(split_clause,[status(thm)],[f3984,f1334,f471]) ).
fof(f3987,plain,
( ~ sQ15_spl
| ~ sQ174_spl ),
inference(split_clause,[status(thm)],[f3985,f2277,f471]) ).
fof(f3989,plain,
( ~ sQ97_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f1044,f982,f1013]) ).
fof(f3992,plain,
( sQ114_spl
| ~ sQ23_spl
| sQ174_spl ),
inference(split_clause,[status(thm)],[f2632,f2277,f505,f1334]) ).
fof(f3999,plain,
$false,
inference(sat_refutation,[status(thm)],[f333,f338,f347,f361,f363,f482,f508,f512,f514,f579,f675,f699,f790,f827,f1016,f1118,f1132,f1193,f1344,f1346,f1822,f1842,f1922,f1943,f2005,f2159,f2179,f2186,f2191,f2216,f2228,f2239,f2240,f2280,f2284,f2313,f2341,f2407,f2408,f2430,f2457,f2494,f2523,f2529,f2564,f2586,f2637,f2858,f3093,f3118,f3123,f3468,f3480,f3538,f3541,f3688,f3708,f3715,f3730,f3747,f3770,f3809,f3824,f3845,f3928,f3974,f3986,f3987,f3989,f3992]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED007+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n005.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 01:19:48 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 21.13/3.20 % Refutation found
% 21.13/3.20 % SZS status Theorem for theBenchmark: Theorem is valid
% 21.13/3.20 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.06/3.25 % Elapsed time: 2.863478 seconds
% 19.06/3.25 % CPU time: 22.215731 seconds
% 19.06/3.25 % Total memory used: 112.326 MB
% 19.06/3.25 % Net memory used: 98.377 MB
%------------------------------------------------------------------------------