%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : MED005+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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 : Tue Sep 29 12:01:37 PM UTC 2026
% Result : Theorem 2.62s 1.51s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 35
% Syntax : Number of formulae : 231 ( 29 unt; 23 def)
% Number of atoms : 909 ( 0 equ)
% Maximal formula atoms : 30 ( 3 avg)
% Number of connectives : 1000 ( 322 ~; 461 |; 139 &)
% ( 20 <=>; 58 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 42 ( 41 usr; 21 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-1 aty)
% Number of variables : 272 ( 0 sgn 253 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexivity_gt) ).
fof(f12,axiom,
! [X0,X1] :
( ~ gt(X0,X1)
=> ( uptakelg(X1)
=> ~ releaselg(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',liver_glucose) ).
fof(f20,axiom,
! [X0] :
( ~ s0(X0)
| ~ s1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xorstep2) ).
fof(f21,axiom,
! [X0] :
( ~ s0(X0)
| ~ s2(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xorstep3) ).
fof(f22,axiom,
! [X0] :
( ~ s0(X0)
| ~ s3(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xorstep4) ).
fof(f26,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
=> ( ( ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
| ( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
& bcapacitysn(X0)
& ~ qilt27(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
| ( ( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) ) )
& bcapacityne(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
| ( ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
& bcapacityex(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',normo) ).
fof(f31,axiom,
! [X0] :
( drugbg(X0)
=> ( ( s1(X0)
& ~ qilt27(X0) )
| s2(X0)
| s3(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bgcomp) ).
fof(f32,axiom,
! [X0] :
( drugsu(X0)
=> ( ( s1(X0)
& qillt27(X0) )
| s2(X0)
| s3(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sucomp) ).
fof(f36,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
=> ( ! [X1] :
( ~ gt(X0,X1)
=> drugsu(X1) )
& ~ bcapacityex(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',su_completion) ).
fof(f37,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
=> ! [X1] :
( ~ gt(X0,X1)
=> drugbg(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bg_completion) ).
fof(f38,axiom,
! [X0] :
( ( s0(X0)
& ~ ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) ) )
=> ? [X1] :
( ~ gt(X0,X1)
& s1(X1)
& ! [X2] :
( gt(X1,X2)
=> conditionhyper(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',trans_ax1) ).
fof(f41,conjecture,
( ( s0(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) ) )
=> ? [X0] :
( ~ gt(n0,X0)
& s1(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transs0s1) ).
fof(f42,negated_conjecture,
~ ( ( s0(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) ) )
=> ? [X0] :
( ~ gt(n0,X0)
& s1(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f43,plain,
~ ( ( s0(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) ) )
=> ? [X1] :
( ~ gt(n0,X1)
& s1(X1)
& ! [X2] :
( gt(X1,X2)
=> conditionhyper(X2) ) ) ),
inference(rectify,[],[f42]) ).
fof(f46,plain,
! [X0] :
( ( s0(X0)
& ~ ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) ) )
=> ? [X2] :
( ~ gt(X0,X2)
& s1(X2)
& ! [X3] :
( gt(X2,X3)
=> conditionhyper(X3) ) ) ),
inference(rectify,[],[f38]) ).
fof(f47,plain,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
=> ! [X2] :
( ~ gt(X0,X2)
=> drugbg(X2) ) ),
inference(rectify,[],[f37]) ).
fof(f48,plain,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
=> ( ! [X2] :
( ~ gt(X0,X2)
=> drugsu(X2) )
& ~ bcapacityex(X0) ) ),
inference(rectify,[],[f36]) ).
fof(f50,plain,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
=> ( ( ! [X2] :
( ~ gt(X0,X2)
=> bsecretioni(X2) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X3] :
( gt(X0,X3)
=> conditionhyper(X3) ) )
| ( ! [X4] :
( ~ gt(X0,X4)
=> ~ releaselg(X4) )
& bcapacitysn(X0)
& ~ qilt27(X0)
& ! [X5] :
( gt(X0,X5)
=> conditionhyper(X5) ) )
| ( ( ! [X6] :
( ~ gt(X0,X6)
=> ~ releaselg(X6) )
| ! [X7] :
( ~ gt(X0,X7)
=> uptakepg(X7) ) )
& bcapacityne(X0)
& ! [X8] :
( ~ gt(X0,X8)
=> bsecretioni(X8) )
& ! [X9] :
( gt(X0,X9)
=> conditionhyper(X9) ) )
| ( ! [X10] :
( ~ gt(X0,X10)
=> uptakelg(X10) )
& ! [X11] :
( ~ gt(X0,X11)
=> uptakepg(X11) )
& bcapacityex(X0)
& ! [X12] :
( gt(X0,X12)
=> conditionhyper(X12) ) ) ) ),
inference(rectify,[],[f26]) ).
fof(f58,plain,
! [X0] :
( drugsu(X0)
=> ( s1(X0)
| s2(X0)
| s3(X0) ) ),
inference(pure_predicate_removal,[],[f32]) ).
fof(f59,plain,
( ! [X1] :
( gt(n0,X1)
| ~ s1(X1)
| ? [X2] :
( ~ conditionhyper(X2)
& gt(X1,X2) ) )
& s0(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) ) ),
inference(ennf_transformation,[],[f43]) ).
fof(f60,plain,
( ! [X1] :
( gt(n0,X1)
| ~ s1(X1)
| ? [X2] :
( ~ conditionhyper(X2)
& gt(X1,X2) ) )
& s0(n0)
& ! [X0] :
( conditionhyper(X0)
| ~ gt(n0,X0) ) ),
inference(flattening,[],[f59]) ).
fof(f65,plain,
! [X0] :
( ? [X2] :
( ~ gt(X0,X2)
& s1(X2)
& ! [X3] :
( conditionhyper(X3)
| ~ gt(X2,X3) ) )
| ~ s0(X0)
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) ) ),
inference(ennf_transformation,[],[f46]) ).
fof(f66,plain,
! [X0] :
( ? [X2] :
( ~ gt(X0,X2)
& s1(X2)
& ! [X3] :
( conditionhyper(X3)
| ~ gt(X2,X3) ) )
| ~ s0(X0)
| ! [X1] :
( conditionnormo(X1)
| gt(X0,X1) ) ),
inference(flattening,[],[f65]) ).
fof(f67,plain,
! [X0] :
( ! [X2] :
( drugbg(X2)
| gt(X0,X2) )
| ? [X1] :
( releaselg(X1)
& ~ gt(X0,X1) ) ),
inference(ennf_transformation,[],[f47]) ).
fof(f68,plain,
! [X0] :
( ( ! [X2] :
( drugsu(X2)
| gt(X0,X2) )
& ~ bcapacityex(X0) )
| ? [X1] :
( ~ bsecretioni(X1)
& ~ gt(X0,X1) ) ),
inference(ennf_transformation,[],[f48]) ).
fof(f72,plain,
! [X0] :
( ( ! [X2] :
( bsecretioni(X2)
| gt(X0,X2) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X3] :
( conditionhyper(X3)
| ~ gt(X0,X3) ) )
| ( ! [X4] :
( ~ releaselg(X4)
| gt(X0,X4) )
& bcapacitysn(X0)
& ~ qilt27(X0)
& ! [X5] :
( conditionhyper(X5)
| ~ gt(X0,X5) ) )
| ( ( ! [X6] :
( ~ releaselg(X6)
| gt(X0,X6) )
| ! [X7] :
( uptakepg(X7)
| gt(X0,X7) ) )
& bcapacityne(X0)
& ! [X8] :
( bsecretioni(X8)
| gt(X0,X8) )
& ! [X9] :
( conditionhyper(X9)
| ~ gt(X0,X9) ) )
| ( ! [X10] :
( uptakelg(X10)
| gt(X0,X10) )
& ! [X11] :
( uptakepg(X11)
| gt(X0,X11) )
& bcapacityex(X0)
& ! [X12] :
( conditionhyper(X12)
| ~ gt(X0,X12) ) )
| ? [X1] :
( ~ conditionnormo(X1)
& ~ gt(X0,X1) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f73,plain,
! [X0] :
( ( ! [X2] :
( bsecretioni(X2)
| gt(X0,X2) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X3] :
( conditionhyper(X3)
| ~ gt(X0,X3) ) )
| ( ! [X4] :
( ~ releaselg(X4)
| gt(X0,X4) )
& bcapacitysn(X0)
& ~ qilt27(X0)
& ! [X5] :
( conditionhyper(X5)
| ~ gt(X0,X5) ) )
| ( ( ! [X6] :
( ~ releaselg(X6)
| gt(X0,X6) )
| ! [X7] :
( uptakepg(X7)
| gt(X0,X7) ) )
& bcapacityne(X0)
& ! [X8] :
( bsecretioni(X8)
| gt(X0,X8) )
& ! [X9] :
( conditionhyper(X9)
| ~ gt(X0,X9) ) )
| ( ! [X10] :
( uptakelg(X10)
| gt(X0,X10) )
& ! [X11] :
( uptakepg(X11)
| gt(X0,X11) )
& bcapacityex(X0)
& ! [X12] :
( conditionhyper(X12)
| ~ gt(X0,X12) ) )
| ? [X1] :
( ~ conditionnormo(X1)
& ~ gt(X0,X1) ) ),
inference(flattening,[],[f72]) ).
fof(f85,plain,
! [X0,X1] :
( ~ releaselg(X1)
| ~ uptakelg(X1)
| gt(X0,X1) ),
inference(ennf_transformation,[],[f12]) ).
fof(f86,plain,
! [X0,X1] :
( ~ releaselg(X1)
| ~ uptakelg(X1)
| gt(X0,X1) ),
inference(flattening,[],[f85]) ).
fof(f90,plain,
! [X0] :
( s1(X0)
| s2(X0)
| s3(X0)
| ~ drugsu(X0) ),
inference(ennf_transformation,[],[f58]) ).
fof(f91,plain,
! [X0] :
( s1(X0)
| s2(X0)
| s3(X0)
| ~ drugsu(X0) ),
inference(flattening,[],[f90]) ).
fof(f92,plain,
! [X0] :
( ( s1(X0)
& ~ qilt27(X0) )
| s2(X0)
| s3(X0)
| ~ drugbg(X0) ),
inference(ennf_transformation,[],[f31]) ).
fof(f93,plain,
! [X0] :
( ( s1(X0)
& ~ qilt27(X0) )
| s2(X0)
| s3(X0)
| ~ drugbg(X0) ),
inference(flattening,[],[f92]) ).
fof(f98,definition,
! [X0] :
( ( ! [X10] :
( uptakelg(X10)
| gt(X0,X10) )
& ! [X11] :
( uptakepg(X11)
| gt(X0,X11) )
& bcapacityex(X0)
& ! [X12] :
( conditionhyper(X12)
| ~ gt(X0,X12) ) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f99,definition,
! [X0] :
( ( ( ! [X6] :
( ~ releaselg(X6)
| gt(X0,X6) )
| ! [X7] :
( uptakepg(X7)
| gt(X0,X7) ) )
& bcapacityne(X0)
& ! [X8] :
( bsecretioni(X8)
| gt(X0,X8) )
& ! [X9] :
( conditionhyper(X9)
| ~ gt(X0,X9) ) )
| ~ sP1(X0) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f100,definition,
! [X0] :
( ( ! [X4] :
( ~ releaselg(X4)
| gt(X0,X4) )
& bcapacitysn(X0)
& ~ qilt27(X0)
& ! [X5] :
( conditionhyper(X5)
| ~ gt(X0,X5) ) )
| ~ sP2(X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f101,plain,
! [X0] :
( ( ! [X2] :
( bsecretioni(X2)
| gt(X0,X2) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X3] :
( conditionhyper(X3)
| ~ gt(X0,X3) ) )
| sP2(X0)
| sP1(X0)
| sP0(X0)
| ? [X1] :
( ~ conditionnormo(X1)
& ~ gt(X0,X1) ) ),
inference(definition_folding,[],[f73,f100,f99,f98]) ).
fof(f104,plain,
( ! [X0] :
( gt(n0,X0)
| ~ s1(X0)
| ? [X1] :
( ~ conditionhyper(X1)
& gt(X0,X1) ) )
& s0(n0)
& ! [X2] :
( conditionhyper(X2)
| ~ gt(n0,X2) ) ),
inference(rectify,[],[f60]) ).
fof(f105,plain,
( ! [X0] :
( gt(n0,X0)
| ~ s1(X0)
| ( ~ conditionhyper(sK4(X0))
& gt(X0,sK4(X0)) ) )
& s0(n0)
& ! [X2] :
( conditionhyper(X2)
| ~ gt(n0,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f104]) ).
fof(f110,plain,
! [X0] :
( ? [X1] :
( ~ gt(X0,X1)
& s1(X1)
& ! [X2] :
( conditionhyper(X2)
| ~ gt(X1,X2) ) )
| ~ s0(X0)
| ! [X3] :
( conditionnormo(X3)
| gt(X0,X3) ) ),
inference(rectify,[],[f66]) ).
fof(f111,plain,
! [X0] :
( ( ~ gt(X0,sK7(X0))
& s1(sK7(X0))
& ! [X2] :
( conditionhyper(X2)
| ~ gt(sK7(X0),X2) ) )
| ~ s0(X0)
| ! [X3] :
( conditionnormo(X3)
| gt(X0,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X1,sK7(X0))],[f110]) ).
fof(f112,plain,
! [X0] :
( ! [X1] :
( drugbg(X1)
| gt(X0,X1) )
| ? [X2] :
( releaselg(X2)
& ~ gt(X0,X2) ) ),
inference(rectify,[],[f67]) ).
fof(f113,plain,
! [X0] :
( ! [X1] :
( drugbg(X1)
| gt(X0,X1) )
| ( releaselg(sK8(X0))
& ~ gt(X0,sK8(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X2,sK8(X0))],[f112]) ).
fof(f114,plain,
! [X0] :
( ( ! [X1] :
( drugsu(X1)
| gt(X0,X1) )
& ~ bcapacityex(X0) )
| ? [X2] :
( ~ bsecretioni(X2)
& ~ gt(X0,X2) ) ),
inference(rectify,[],[f68]) ).
fof(f115,plain,
! [X0] :
( ( ! [X1] :
( drugsu(X1)
| gt(X0,X1) )
& ~ bcapacityex(X0) )
| ( ~ bsecretioni(sK9(X0))
& ~ gt(X0,sK9(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X2,sK9(X0))],[f114]) ).
fof(f118,plain,
! [X0] :
( ( ! [X4] :
( ~ releaselg(X4)
| gt(X0,X4) )
& bcapacitysn(X0)
& ~ qilt27(X0)
& ! [X5] :
( conditionhyper(X5)
| ~ gt(X0,X5) ) )
| ~ sP2(X0) ),
inference(nnf_transformation,[],[f100]) ).
fof(f119,plain,
! [X0] :
( ( ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) )
& bcapacitysn(X0)
& ~ qilt27(X0)
& ! [X2] :
( conditionhyper(X2)
| ~ gt(X0,X2) ) )
| ~ sP2(X0) ),
inference(rectify,[],[f118]) ).
fof(f120,plain,
! [X0] :
( ( ( ! [X6] :
( ~ releaselg(X6)
| gt(X0,X6) )
| ! [X7] :
( uptakepg(X7)
| gt(X0,X7) ) )
& bcapacityne(X0)
& ! [X8] :
( bsecretioni(X8)
| gt(X0,X8) )
& ! [X9] :
( conditionhyper(X9)
| ~ gt(X0,X9) ) )
| ~ sP1(X0) ),
inference(nnf_transformation,[],[f99]) ).
fof(f121,plain,
! [X0] :
( ( ( ! [X1] :
( ~ releaselg(X1)
| gt(X0,X1) )
| ! [X2] :
( uptakepg(X2)
| gt(X0,X2) ) )
& bcapacityne(X0)
& ! [X3] :
( bsecretioni(X3)
| gt(X0,X3) )
& ! [X4] :
( conditionhyper(X4)
| ~ gt(X0,X4) ) )
| ~ sP1(X0) ),
inference(rectify,[],[f120]) ).
fof(f122,plain,
! [X0] :
( ( ! [X10] :
( uptakelg(X10)
| gt(X0,X10) )
& ! [X11] :
( uptakepg(X11)
| gt(X0,X11) )
& bcapacityex(X0)
& ! [X12] :
( conditionhyper(X12)
| ~ gt(X0,X12) ) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f98]) ).
fof(f123,plain,
! [X0] :
( ( ! [X1] :
( uptakelg(X1)
| gt(X0,X1) )
& ! [X2] :
( uptakepg(X2)
| gt(X0,X2) )
& bcapacityex(X0)
& ! [X3] :
( conditionhyper(X3)
| ~ gt(X0,X3) ) )
| ~ sP0(X0) ),
inference(rectify,[],[f122]) ).
fof(f124,plain,
! [X0] :
( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X2] :
( conditionhyper(X2)
| ~ gt(X0,X2) ) )
| sP2(X0)
| sP1(X0)
| sP0(X0)
| ? [X3] :
( ~ conditionnormo(X3)
& ~ gt(X0,X3) ) ),
inference(rectify,[],[f101]) ).
fof(f125,plain,
! [X0] :
( ( ! [X1] :
( bsecretioni(X1)
| gt(X0,X1) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X2] :
( conditionhyper(X2)
| ~ gt(X0,X2) ) )
| sP2(X0)
| sP1(X0)
| sP0(X0)
| ( ~ conditionnormo(sK12(X0))
& ~ gt(X0,sK12(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X3,sK12(X0))],[f124]) ).
fof(f143,plain,
s0(n0),
inference(cnf_transformation,[],[f105]) ).
fof(f144,plain,
! [X0] :
( ~ s1(X0)
| gt(n0,X0)
| gt(X0,sK4(X0)) ),
inference(cnf_transformation,[],[f105]) ).
fof(f145,plain,
! [X0] :
( ~ s1(X0)
| gt(n0,X0)
| ~ conditionhyper(sK4(X0)) ),
inference(cnf_transformation,[],[f105]) ).
fof(f154,plain,
! [X2,X3,X0] :
( conditionhyper(X2)
| ~ gt(sK7(X0),X2)
| ~ s0(X0)
| conditionnormo(X3)
| gt(X0,X3) ),
inference(cnf_transformation,[],[f111]) ).
fof(f155,plain,
! [X3,X0] :
( conditionnormo(X3)
| ~ s0(X0)
| s1(sK7(X0))
| gt(X0,X3) ),
inference(cnf_transformation,[],[f111]) ).
fof(f156,plain,
! [X3,X0] :
( ~ gt(X0,sK7(X0))
| ~ s0(X0)
| conditionnormo(X3)
| gt(X0,X3) ),
inference(cnf_transformation,[],[f111]) ).
fof(f157,plain,
! [X0,X1] :
( ~ gt(X0,sK8(X0))
| gt(X0,X1)
| drugbg(X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f158,plain,
! [X0,X1] :
( releaselg(sK8(X0))
| gt(X0,X1)
| drugbg(X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f161,plain,
! [X0,X1] :
( ~ gt(X0,sK9(X0))
| gt(X0,X1)
| drugsu(X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f162,plain,
! [X0,X1] :
( ~ bsecretioni(sK9(X0))
| gt(X0,X1)
| drugsu(X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f171,plain,
! [X0,X1] :
( ~ sP2(X0)
| gt(X0,X1)
| ~ releaselg(X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f173,plain,
! [X3,X0] :
( ~ sP1(X0)
| gt(X0,X3)
| bsecretioni(X3) ),
inference(cnf_transformation,[],[f121]) ).
fof(f179,plain,
! [X0,X1] :
( ~ sP0(X0)
| gt(X0,X1)
| uptakelg(X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f186,plain,
! [X0,X1] :
( ~ gt(X0,sK12(X0))
| gt(X0,X1)
| sP2(X0)
| sP1(X0)
| sP0(X0)
| bsecretioni(X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f187,plain,
! [X0,X1] :
( ~ conditionnormo(sK12(X0))
| gt(X0,X1)
| sP2(X0)
| sP1(X0)
| sP0(X0)
| bsecretioni(X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f216,plain,
! [X0,X1] :
( ~ uptakelg(X1)
| ~ releaselg(X1)
| gt(X0,X1) ),
inference(cnf_transformation,[],[f86]) ).
fof(f222,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f226,plain,
! [X0] :
( ~ s3(X0)
| ~ s0(X0) ),
inference(cnf_transformation,[],[f22]) ).
fof(f227,plain,
! [X0] :
( ~ s2(X0)
| ~ s0(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f228,plain,
! [X0] :
( ~ s1(X0)
| ~ s0(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f230,plain,
! [X0] :
( ~ drugsu(X0)
| s2(X0)
| s3(X0)
| s1(X0) ),
inference(cnf_transformation,[],[f91]) ).
fof(f232,plain,
! [X0] :
( ~ drugbg(X0)
| s2(X0)
| s3(X0)
| s1(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f244,definition,
( spl27_2
<=> s1(sK7(n0)) ),
introduced(definition,[new_symbols(definition,[spl27_2])],[avatar_definition]) ).
fof(f245,plain,
( ~ s1(sK7(n0))
| spl27_2 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f246,plain,
( s1(sK7(n0))
| ~ spl27_2 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f252,plain,
( gt(n0,sK7(n0))
| gt(sK7(n0),sK4(sK7(n0)))
| ~ spl27_2 ),
inference(resolution,[],[f246,f144]) ).
fof(f253,plain,
( gt(n0,sK7(n0))
| ~ conditionhyper(sK4(sK7(n0)))
| ~ spl27_2 ),
inference(resolution,[],[f246,f145]) ).
fof(f255,definition,
( spl27_3
<=> conditionhyper(sK4(sK7(n0))) ),
introduced(definition,[new_symbols(definition,[spl27_3])],[avatar_definition]) ).
fof(f257,plain,
( ~ conditionhyper(sK4(sK7(n0)))
| spl27_3 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f259,definition,
( spl27_4
<=> gt(n0,sK7(n0)) ),
introduced(definition,[new_symbols(definition,[spl27_4])],[avatar_definition]) ).
fof(f261,plain,
( gt(n0,sK7(n0))
| ~ spl27_4 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f262,plain,
( ~ spl27_3
| spl27_4
| ~ spl27_2 ),
inference(avatar_split_clause,[],[f253,f244,f259,f255]) ).
fof(f264,definition,
( spl27_5
<=> gt(sK7(n0),sK4(sK7(n0))) ),
introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition]) ).
fof(f266,plain,
( gt(sK7(n0),sK4(sK7(n0)))
| ~ spl27_5 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f267,plain,
( spl27_5
| spl27_4
| ~ spl27_2 ),
inference(avatar_split_clause,[],[f252,f244,f259,f264]) ).
fof(f468,definition,
( spl27_20
<=> drugbg(n0) ),
introduced(definition,[new_symbols(definition,[spl27_20])],[avatar_definition]) ).
fof(f469,plain,
( drugbg(n0)
| ~ spl27_20 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f470,plain,
( ~ drugbg(n0)
| spl27_20 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f472,definition,
( spl27_21
<=> sP2(n0) ),
introduced(definition,[new_symbols(definition,[spl27_21])],[avatar_definition]) ).
fof(f473,plain,
( ~ sP2(n0)
| spl27_21 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f474,plain,
( sP2(n0)
| ~ spl27_21 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f480,definition,
( spl27_23
<=> sP0(n0) ),
introduced(definition,[new_symbols(definition,[spl27_23])],[avatar_definition]) ).
fof(f481,plain,
( ~ sP0(n0)
| spl27_23 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f482,plain,
( sP0(n0)
| ~ spl27_23 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f522,definition,
( spl27_30
<=> ! [X2] :
( conditionnormo(X2)
| gt(n0,X2) ) ),
introduced(definition,[new_symbols(definition,[spl27_30])],[avatar_definition]) ).
fof(f523,plain,
( ! [X2] :
( conditionnormo(X2)
| gt(n0,X2) )
| ~ spl27_30 ),
inference(avatar_component_clause,[],[f522]) ).
fof(f597,plain,
( s2(n0)
| s3(n0)
| s1(n0)
| ~ spl27_20 ),
inference(resolution,[],[f469,f232]) ).
fof(f599,definition,
( spl27_33
<=> s1(n0) ),
introduced(definition,[new_symbols(definition,[spl27_33])],[avatar_definition]) ).
fof(f600,plain,
( ~ s1(n0)
| spl27_33 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f601,plain,
( s1(n0)
| ~ spl27_33 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f603,definition,
( spl27_34
<=> s3(n0) ),
introduced(definition,[new_symbols(definition,[spl27_34])],[avatar_definition]) ).
fof(f604,plain,
( ~ s3(n0)
| spl27_34 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f605,plain,
( s3(n0)
| ~ spl27_34 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f607,definition,
( spl27_35
<=> s2(n0) ),
introduced(definition,[new_symbols(definition,[spl27_35])],[avatar_definition]) ).
fof(f608,plain,
( ~ s2(n0)
| spl27_35 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f609,plain,
( s2(n0)
| ~ spl27_35 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f610,plain,
( spl27_33
| spl27_34
| spl27_35
| ~ spl27_20 ),
inference(avatar_split_clause,[],[f597,f468,f607,f603,f599]) ).
fof(f612,definition,
( spl27_36
<=> gt(n0,sK12(n0)) ),
introduced(definition,[new_symbols(definition,[spl27_36])],[avatar_definition]) ).
fof(f613,plain,
( ~ gt(n0,sK12(n0))
| spl27_36 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f614,plain,
( gt(n0,sK12(n0))
| ~ spl27_36 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f618,plain,
( ~ s0(n0)
| ~ spl27_34 ),
inference(resolution,[],[f605,f226]) ).
fof(f619,plain,
( $false
| ~ spl27_34 ),
inference(forward_subsumption_resolution,[],[f618,f143]) ).
fof(f620,plain,
~ spl27_34,
inference(avatar_contradiction_clause,[],[f619]) ).
fof(f638,plain,
( ~ s0(n0)
| ~ spl27_35 ),
inference(resolution,[],[f609,f227]) ).
fof(f639,plain,
( $false
| ~ spl27_35 ),
inference(forward_subsumption_resolution,[],[f638,f143]) ).
fof(f640,plain,
~ spl27_35,
inference(avatar_contradiction_clause,[],[f639]) ).
fof(f665,plain,
( ~ s0(n0)
| ~ spl27_33 ),
inference(resolution,[],[f601,f228]) ).
fof(f678,plain,
( $false
| ~ spl27_33 ),
inference(forward_subsumption_resolution,[],[f665,f143]) ).
fof(f679,plain,
~ spl27_33,
inference(avatar_contradiction_clause,[],[f678]) ).
fof(f707,plain,
( ! [X0] :
( gt(n0,X0)
| sP2(n0)
| sP1(n0)
| sP0(n0)
| bsecretioni(X0) )
| ~ spl27_36 ),
inference(resolution,[],[f614,f186]) ).
fof(f722,plain,
( ! [X0] :
( gt(n0,X0)
| sP2(n0)
| sP0(n0)
| bsecretioni(X0) )
| ~ spl27_36 ),
inference(forward_subsumption_resolution,[],[f707,f173]) ).
fof(f724,definition,
( spl27_45
<=> conditionnormo(sK12(n0)) ),
introduced(definition,[new_symbols(definition,[spl27_45])],[avatar_definition]) ).
fof(f725,plain,
( conditionnormo(sK12(n0))
| ~ spl27_45 ),
inference(avatar_component_clause,[],[f724]) ).
fof(f726,plain,
( ~ conditionnormo(sK12(n0))
| spl27_45 ),
inference(avatar_component_clause,[],[f724]) ).
fof(f730,definition,
( spl27_46
<=> ! [X0] :
( gt(n0,X0)
| bsecretioni(X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_46])],[avatar_definition]) ).
fof(f731,plain,
( ! [X0] :
( bsecretioni(X0)
| gt(n0,X0) )
| ~ spl27_46 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f732,plain,
( spl27_23
| spl27_21
| spl27_46
| ~ spl27_36 ),
inference(avatar_split_clause,[],[f722,f612,f730,f472,f480]) ).
fof(f746,definition,
( spl27_48
<=> ! [X0] :
( gt(n0,X0)
| ~ releaselg(X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_48])],[avatar_definition]) ).
fof(f747,plain,
( ! [X0] :
( ~ releaselg(X0)
| gt(n0,X0) )
| ~ spl27_48 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f1044,plain,
( ! [X0,X1] :
( ~ gt(sK7(X0),sK4(sK7(n0)))
| ~ s0(X0)
| conditionnormo(X1)
| gt(X0,X1) )
| spl27_3 ),
inference(resolution,[],[f257,f154]) ).
fof(f1088,plain,
( ! [X0] :
( ~ s0(n0)
| conditionnormo(X0)
| gt(n0,X0) )
| spl27_3
| ~ spl27_5 ),
inference(resolution,[],[f1044,f266]) ).
fof(f1089,plain,
( ! [X0] :
( conditionnormo(X0)
| gt(n0,X0) )
| spl27_3
| ~ spl27_5 ),
inference(forward_subsumption_resolution,[],[f1088,f143]) ).
fof(f1090,plain,
( spl27_30
| spl27_3
| ~ spl27_5 ),
inference(avatar_split_clause,[],[f1089,f264,f255,f522]) ).
fof(f1223,plain,
( ! [X0] :
( gt(n0,X0)
| ~ releaselg(X0) )
| ~ spl27_21 ),
inference(resolution,[],[f474,f171]) ).
fof(f1228,plain,
( spl27_48
| ~ spl27_21 ),
inference(avatar_split_clause,[],[f1223,f472,f746]) ).
fof(f1273,definition,
( spl27_75
<=> ! [X1] :
( gt(n0,X1)
| uptakelg(X1) ) ),
introduced(definition,[new_symbols(definition,[spl27_75])],[avatar_definition]) ).
fof(f1274,plain,
( ! [X1] :
( uptakelg(X1)
| gt(n0,X1) )
| ~ spl27_75 ),
inference(avatar_component_clause,[],[f1273]) ).
fof(f1427,plain,
( ! [X0,X1] :
( gt(n0,sK8(X0))
| gt(X0,X1)
| drugbg(X1) )
| ~ spl27_48 ),
inference(resolution,[],[f747,f158]) ).
fof(f1436,plain,
( ! [X0,X1] :
( gt(n0,X0)
| drugbg(X0)
| gt(n0,X1)
| drugbg(X1) )
| ~ spl27_48 ),
inference(resolution,[],[f1427,f157]) ).
fof(f1450,definition,
( spl27_95
<=> ! [X1] :
( gt(n0,X1)
| drugbg(X1) ) ),
introduced(definition,[new_symbols(definition,[spl27_95])],[avatar_definition]) ).
fof(f1451,plain,
( ! [X1] :
( drugbg(X1)
| gt(n0,X1) )
| ~ spl27_95 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1452,plain,
( spl27_95
| spl27_95
| ~ spl27_48 ),
inference(avatar_split_clause,[],[f1436,f746,f1450,f1450]) ).
fof(f1498,plain,
( gt(n0,n0)
| spl27_20
| ~ spl27_95 ),
inference(resolution,[],[f1451,f470]) ).
fof(f1499,plain,
( $false
| spl27_20
| ~ spl27_95 ),
inference(forward_subsumption_resolution,[],[f1498,f222]) ).
fof(f1500,plain,
( spl27_20
| ~ spl27_95 ),
inference(avatar_contradiction_clause,[],[f1499]) ).
fof(f1533,plain,
( ! [X0] :
( ~ s0(X0)
| s1(sK7(X0))
| gt(X0,sK12(n0)) )
| spl27_45 ),
inference(resolution,[],[f726,f155]) ).
fof(f1534,plain,
( s1(sK7(n0))
| gt(n0,sK12(n0))
| spl27_45 ),
inference(resolution,[],[f1533,f143]) ).
fof(f1559,plain,
( gt(n0,sK12(n0))
| spl27_2
| spl27_45 ),
inference(forward_subsumption_resolution,[],[f1534,f245]) ).
fof(f1560,plain,
( $false
| spl27_2
| spl27_36
| spl27_45 ),
inference(forward_subsumption_resolution,[],[f1559,f613]) ).
fof(f1561,plain,
( spl27_2
| spl27_36
| spl27_45 ),
inference(avatar_contradiction_clause,[],[f1560]) ).
fof(f1632,plain,
( ! [X0] :
( ~ s0(n0)
| conditionnormo(X0)
| gt(n0,X0) )
| ~ spl27_4 ),
inference(resolution,[],[f261,f156]) ).
fof(f1635,plain,
( ! [X0] :
( conditionnormo(X0)
| gt(n0,X0) )
| ~ spl27_4 ),
inference(forward_subsumption_resolution,[],[f1632,f143]) ).
fof(f1636,plain,
( spl27_30
| ~ spl27_4 ),
inference(avatar_split_clause,[],[f1635,f259,f522]) ).
fof(f1702,plain,
( ! [X0] :
( gt(n0,X0)
| uptakelg(X0) )
| ~ spl27_23 ),
inference(resolution,[],[f482,f179]) ).
fof(f1757,plain,
( ! [X0] :
( gt(n0,X0)
| sP2(n0)
| sP1(n0)
| sP0(n0)
| bsecretioni(X0) )
| ~ spl27_45 ),
inference(resolution,[],[f725,f187]) ).
fof(f1843,plain,
( ! [X0,X1] :
( ~ releaselg(X0)
| gt(n0,X0)
| gt(X1,X0) )
| ~ spl27_75 ),
inference(resolution,[],[f1274,f216]) ).
fof(f1861,plain,
( ! [X2,X0,X1] :
( gt(n0,sK8(X0))
| gt(X1,sK8(X0))
| gt(X0,X2)
| drugbg(X2) )
| ~ spl27_75 ),
inference(resolution,[],[f1843,f158]) ).
fof(f1878,plain,
( ! [X2,X0,X1] :
( gt(X0,sK8(n0))
| gt(n0,X1)
| drugbg(X1)
| gt(n0,X2)
| drugbg(X2) )
| ~ spl27_75 ),
inference(resolution,[],[f1861,f157]) ).
fof(f1884,definition,
( spl27_128
<=> ! [X0] : gt(X0,sK8(n0)) ),
introduced(definition,[new_symbols(definition,[spl27_128])],[avatar_definition]) ).
fof(f1885,plain,
( ! [X0] : gt(X0,sK8(n0))
| ~ spl27_128 ),
inference(avatar_component_clause,[],[f1884]) ).
fof(f1886,plain,
( spl27_95
| spl27_95
| spl27_128
| ~ spl27_75 ),
inference(avatar_split_clause,[],[f1878,f1273,f1884,f1450,f1450]) ).
fof(f1890,plain,
( $false
| ~ spl27_128 ),
inference(resolution,[],[f1885,f222]) ).
fof(f1907,plain,
~ spl27_128,
inference(avatar_contradiction_clause,[],[f1890]) ).
fof(f1909,plain,
( spl27_75
| ~ spl27_23 ),
inference(avatar_split_clause,[],[f1702,f480,f1273]) ).
fof(f1912,plain,
( ! [X0] :
( gt(n0,X0)
| sP2(n0)
| sP0(n0)
| bsecretioni(X0) )
| ~ spl27_45 ),
inference(forward_subsumption_resolution,[],[f1757,f173]) ).
fof(f1916,plain,
( ! [X0] :
( gt(n0,X0)
| sP0(n0)
| bsecretioni(X0) )
| spl27_21
| ~ spl27_45 ),
inference(forward_subsumption_resolution,[],[f1912,f473]) ).
fof(f1920,plain,
( ! [X0] :
( gt(n0,X0)
| bsecretioni(X0) )
| spl27_21
| spl27_23
| ~ spl27_45 ),
inference(forward_subsumption_resolution,[],[f1916,f481]) ).
fof(f1924,plain,
( spl27_46
| spl27_21
| spl27_23
| ~ spl27_45 ),
inference(avatar_split_clause,[],[f1920,f724,f480,f472,f730]) ).
fof(f1950,plain,
( gt(n0,sK12(n0))
| ~ spl27_30
| spl27_45 ),
inference(resolution,[],[f523,f726]) ).
fof(f1952,plain,
( $false
| ~ spl27_30
| spl27_36
| spl27_45 ),
inference(forward_subsumption_resolution,[],[f1950,f613]) ).
fof(f1953,plain,
( ~ spl27_30
| spl27_36
| spl27_45 ),
inference(avatar_contradiction_clause,[],[f1952]) ).
fof(f1960,plain,
( ! [X0,X1] :
( drugsu(X1)
| gt(X0,X1)
| gt(n0,sK9(X0)) )
| ~ spl27_46 ),
inference(resolution,[],[f731,f162]) ).
fof(f1977,plain,
( ! [X0,X1] :
( gt(n0,sK9(X0))
| gt(X0,X1)
| s2(X1)
| s3(X1)
| s1(X1) )
| ~ spl27_46 ),
inference(resolution,[],[f1960,f230]) ).
fof(f2005,plain,
( ! [X0,X1] :
( gt(n0,X0)
| s2(X0)
| s3(X0)
| s1(X0)
| gt(n0,X1)
| drugsu(X1) )
| ~ spl27_46 ),
inference(resolution,[],[f1977,f161]) ).
fof(f2028,definition,
( spl27_133
<=> ! [X1] :
( gt(n0,X1)
| drugsu(X1) ) ),
introduced(definition,[new_symbols(definition,[spl27_133])],[avatar_definition]) ).
fof(f2029,plain,
( ! [X1] :
( drugsu(X1)
| gt(n0,X1) )
| ~ spl27_133 ),
inference(avatar_component_clause,[],[f2028]) ).
fof(f2031,definition,
( spl27_134
<=> ! [X0] :
( gt(n0,X0)
| s1(X0)
| s3(X0)
| s2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_134])],[avatar_definition]) ).
fof(f2032,plain,
( ! [X0] :
( s3(X0)
| s1(X0)
| gt(n0,X0)
| s2(X0) )
| ~ spl27_134 ),
inference(avatar_component_clause,[],[f2031]) ).
fof(f2033,plain,
( spl27_133
| spl27_134
| ~ spl27_46 ),
inference(avatar_split_clause,[],[f2005,f730,f2031,f2028]) ).
fof(f2107,plain,
( s1(n0)
| gt(n0,n0)
| s2(n0)
| spl27_34
| ~ spl27_134 ),
inference(resolution,[],[f2032,f604]) ).
fof(f2109,plain,
( gt(n0,n0)
| s2(n0)
| spl27_33
| spl27_34
| ~ spl27_134 ),
inference(forward_subsumption_resolution,[],[f2107,f600]) ).
fof(f2111,plain,
( s2(n0)
| spl27_33
| spl27_34
| ~ spl27_134 ),
inference(forward_subsumption_resolution,[],[f2109,f222]) ).
fof(f2113,plain,
( $false
| spl27_33
| spl27_34
| spl27_35
| ~ spl27_134 ),
inference(forward_subsumption_resolution,[],[f2111,f608]) ).
fof(f2114,plain,
( spl27_33
| spl27_34
| spl27_35
| ~ spl27_134 ),
inference(avatar_contradiction_clause,[],[f2113]) ).
fof(f2120,plain,
( ! [X0] :
( gt(n0,X0)
| s2(X0)
| s3(X0)
| s1(X0) )
| ~ spl27_133 ),
inference(resolution,[],[f2029,f230]) ).
fof(f2122,plain,
( spl27_134
| ~ spl27_133 ),
inference(avatar_split_clause,[],[f2120,f2028,f2031]) ).
cnf(s2,plain,
( ~ spl27_2
| ~ spl27_3
| spl27_4 ),
inference(sat_conversion,[],[f262]) ).
cnf(s3,plain,
( ~ spl27_2
| spl27_4
| spl27_5 ),
inference(sat_conversion,[],[f267]) ).
cnf(s23,plain,
( ~ spl27_20
| spl27_33
| spl27_34
| spl27_35 ),
inference(sat_conversion,[],[f610]) ).
cnf(s25,plain,
~ spl27_34,
inference(sat_conversion,[],[f620]) ).
cnf(s27,plain,
~ spl27_35,
inference(sat_conversion,[],[f640]) ).
cnf(s34,plain,
~ spl27_33,
inference(sat_conversion,[],[f679]) ).
cnf(s39,plain,
( spl27_21
| spl27_23
| ~ spl27_36
| spl27_46 ),
inference(sat_conversion,[],[f732]) ).
cnf(s67,plain,
( spl27_3
| ~ spl27_5
| spl27_30 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s76,plain,
( ~ spl27_21
| spl27_48 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s103,plain,
( spl27_95
| ~ spl27_48
| spl27_95 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s104,plain,
( ~ spl27_48
| spl27_95 ),
inference(rat,[],[s103]) ).
cnf(s108,plain,
( spl27_20
| ~ spl27_95 ),
inference(sat_conversion,[],[f1500]) ).
cnf(s115,plain,
( spl27_2
| spl27_36
| spl27_45 ),
inference(sat_conversion,[],[f1561]) ).
cnf(s123,plain,
( ~ spl27_4
| spl27_30 ),
inference(sat_conversion,[],[f1636]) ).
cnf(s152,plain,
( spl27_95
| ~ spl27_75
| spl27_95
| spl27_128 ),
inference(sat_conversion,[],[f1886]) ).
cnf(s153,plain,
( ~ spl27_75
| spl27_95
| spl27_128 ),
inference(rat,[],[s152]) ).
cnf(s154,plain,
~ spl27_128,
inference(sat_conversion,[],[f1907]) ).
cnf(s156,plain,
( ~ spl27_23
| spl27_75 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s160,plain,
( spl27_21
| spl27_23
| ~ spl27_45
| spl27_46 ),
inference(sat_conversion,[],[f1924]) ).
cnf(s161,plain,
( ~ spl27_30
| spl27_36
| spl27_45 ),
inference(sat_conversion,[],[f1953]) ).
cnf(s164,plain,
( ~ spl27_46
| spl27_133
| spl27_134 ),
inference(sat_conversion,[],[f2033]) ).
cnf(s171,plain,
( spl27_33
| spl27_34
| spl27_35
| ~ spl27_134 ),
inference(sat_conversion,[],[f2114]) ).
cnf(s173,plain,
( ~ spl27_133
| spl27_134 ),
inference(sat_conversion,[],[f2122]) ).
cnf(s174,plain,
( ~ spl27_75
| spl27_95 ),
inference(rat,[],[s153,s154]) ).
cnf(s175,plain,
~ spl27_134,
inference(rat,[],[s171,s27,s34,s25]) ).
cnf(s176,plain,
~ spl27_133,
inference(rat,[],[s173,s175]) ).
cnf(s178,plain,
~ spl27_46,
inference(rat,[],[s164,s175,s176]) ).
cnf(s181,plain,
~ spl27_20,
inference(rat,[],[s23,s27,s25,s34]) ).
cnf(s182,plain,
~ spl27_95,
inference(rat,[],[s108,s181]) ).
cnf(s184,plain,
~ spl27_75,
inference(rat,[],[s174,s182]) ).
cnf(s185,plain,
~ spl27_48,
inference(rat,[],[s104,s182]) ).
cnf(s186,plain,
~ spl27_23,
inference(rat,[],[s156,s184]) ).
cnf(s188,plain,
~ spl27_21,
inference(rat,[],[s76,s185]) ).
cnf(s190,plain,
~ spl27_45,
inference(rat,[],[s160,s178,s186,s188]) ).
cnf(s191,plain,
~ spl27_36,
inference(rat,[],[s39,s178,s186,s188]) ).
cnf(s193,plain,
~ spl27_30,
inference(rat,[],[s161,s190,s191]) ).
cnf(s194,plain,
spl27_2,
inference(rat,[],[s115,s190,s191]) ).
cnf(s195,plain,
~ spl27_4,
inference(rat,[],[s123,s193]) ).
cnf(s205,plain,
spl27_5,
inference(rat,[],[s3,s195,s194]) ).
cnf(s206,plain,
spl27_3,
inference(rat,[],[s67,s193,s205]) ).
cnf(s207,plain,
$false,
inference(rat,[],[s2,s195,s206,s194]) ).
fof(f2123,plain,
$false,
inference(avatar_sat_refutation,[],[s207]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MED005+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 17:16:08 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.62/1.51 % (3624698)Detected formulas, will run a generic FOF schedule.
% 2.62/1.51 % (3624708)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1978712164:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.62/1.51 % (3624709)dis-21_1_sil=8000:lcm=predicate:random_seed=1418302223:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.62/1.51 % (3624706)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2522594863:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.62/1.51 % (3624707)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2750253605:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.62/1.51 % (3624703)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2020831448:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.62/1.51 % (3624705)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2644777443:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.62/1.51 % (3624704)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2673611325:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.62/1.51 % (3624706)Refutation not found, incomplete strategy
% 2.62/1.51 % (3624706)------------------------------
% 2.62/1.51 % (3624706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.62/1.51 % (3624706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.62/1.51 % (3624706)CaDiCaL version: 2.1.3
% 2.62/1.51 % (3624706)Termination reason: Refutation not found, incomplete strategy
% 2.62/1.51 % (3624706)Time elapsed: 0.001 s
% 2.62/1.51 % (3624706)Peak memory usage: 87 MB
% 2.62/1.51 % (3624708)Instruction limit reached!
% 2.62/1.51 % (3624708)------------------------------
% 2.62/1.51 % (3624708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.62/1.51 % (3624708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.62/1.51 % (3624708)CaDiCaL version: 2.1.3
% 2.62/1.51 % (3624708)Termination reason: Instruction limit
% 2.62/1.51 % (3624708)Termination phase: Saturation
% 2.62/1.51 % (3624708)Time elapsed: 0.042 s
% 2.62/1.51 % (3624708)Peak memory usage: 89 MB
% 2.62/1.51 % (3624708)Instructions burned: 141 (million)
% 2.62/1.51 % (3624707)Instruction limit reached!
% 2.62/1.51 % (3624707)------------------------------
% 2.62/1.51 % (3624707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.62/1.51 % (3624707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.62/1.51 % (3624707)CaDiCaL version: 2.1.3
% 2.62/1.51 % (3624707)Termination reason: Instruction limit
% 2.62/1.51 % (3624707)Termination phase: Saturation
% 2.62/1.51 % (3624707)Time elapsed: 0.042 s
% 2.62/1.51 % (3624707)Peak memory usage: 87 MB
% 2.62/1.51 % (3624707)Instructions burned: 120 (million)
% 2.62/1.51 % (3624709)Instruction limit reached!
% 2.62/1.51 % (3624709)------------------------------
% 2.62/1.51 % (3624709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.62/1.51 % (3624709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.62/1.51 % (3624709)CaDiCaL version: 2.1.3
% 2.62/1.51 % (3624709)Termination reason: Instruction limit
% 2.62/1.51 % (3624709)Termination phase: Saturation
% 2.62/1.51 % (3624709)Time elapsed: 0.065 s
% 2.62/1.51 % (3624709)Peak memory usage: 88 MB
% 2.62/1.51 % (3624709)Instructions burned: 130 (million)
% 2.62/1.51 % (3624718)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4283075484:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 2.62/1.51 % (3624718)Refutation not found, incomplete strategy
% 2.62/1.51 % (3624718)------------------------------
% 2.62/1.51 % (3624718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.62/1.51 % (3624718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.62/1.51 % (3624718)CaDiCaL version: 2.1.3
% 2.62/1.51 % (3624718)Termination reason: Refutation not found, incomplete strategy
% 2.62/1.51 % (3624718)Time elapsed: 0.001 s
% 2.62/1.51 % (3624718)Peak memory usage: 88 MB
% 2.62/1.51 % (3624718)Instructions burned: 1 (million)
% 2.62/1.51 % (3624717)lrs+10_1_sil=8000:sp=occurrence:random_seed=1292141519:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.62/1.51 % (3624719)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1532770454:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 2.62/1.51 % (3624706)------------------------------
% 2.62/1.51 % (3624706)------------------------------
% 2.62/1.51 % (3624719)First to succeed.
% 2.62/1.51 % (3624719)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3624698"
% 2.62/1.51 % (3624717)Instruction limit reached!
% 2.62/1.51 % (3624717)------------------------------
% 2.62/1.51 % (3624717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.62/1.51 % (3624717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.62/1.51 % (3624717)CaDiCaL version: 2.1.3
% 2.62/1.51 % (3624717)Termination reason: Instruction limit
% 2.62/1.51 % (3624717)Termination phase: Saturation
% 2.62/1.51 % (3624717)Time elapsed: 0.132 s
% 2.62/1.51 % (3624717)Peak memory usage: 89 MB
% 2.62/1.51 % (3624717)Instructions burned: 285 (million)
% 2.62/1.51 % (3624718)------------------------------
% 2.62/1.51 % (3624718)------------------------------
% 2.62/1.51 % (3624725)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4114429972:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 2.62/1.51 % (3624723)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4200265984:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 2.62/1.51 % (3624724)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2289536610:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 2.62/1.51 % (3624723)Also succeeded, but the first one will report.
% 2.62/1.51 % (3624719)Refutation found. Thanks to Tanya!
% 2.62/1.51 % SZS status Theorem for theBenchmark
% 2.62/1.51 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/1.71 % (3624719)------------------------------
% 0.16/1.71 % (3624719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/1.71 % (3624719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/1.71 % (3624719)CaDiCaL version: 2.1.3
% 0.16/1.71 % (3624719)Termination reason: Refutation
% 0.16/1.71 % (3624719)Time elapsed: 0.058 s
% 0.16/1.71 % (3624719)Peak memory usage: 90 MB
% 0.16/1.71 % (3624719)Instructions burned: 89 (million)
% 0.16/1.71 % (3624719)------------------------------
% 0.16/1.71 % (3624719)------------------------------
% 0.16/1.71 % (3624698)Success in time 0.654 s
% 0.16/1.71 % Vampire exiting
%------------------------------------------------------------------------------