%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT065+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:11:53 PM UTC 2026
% Result : Theorem 82.28s 11.33s
% Output : Proof 82.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 74
% Syntax : Number of formulae : 444 ( 53 unt; 59 def)
% Number of atoms : 1211 ( 151 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 1271 ( 504 ~; 598 |; 93 &)
% ( 63 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 72 ( 70 usr; 60 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 13 con; 0-2 aty)
% Number of variables : 120 ( 0 sgn 65 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sdef11,definition,
( spl11
<=> sigma = tau ),
introduced(definition,[new_symbols(naming,[spl11])],[avatar_definition]) ).
cnf(p71,plain,
( ~ spl11
| sigma = tau ),
inference(avatar_component_clause,[status(thm)],[sdef11]) ).
fof(sdef14,definition,
( spl14
<=> smaller(eta,tau) ),
introduced(definition,[new_symbols(naming,[spl14])],[avatar_definition]) ).
cnf(p101,plain,
( ~ spl14
| smaller(eta,tau) ),
inference(avatar_component_clause,[status(thm)],[sdef14]) ).
cnf(p131,plain,
( ~ spl14
| ~ spl11
| smaller(eta,sigma) ),
inference(superposition,[status(thm)],[p71,p101]) ).
fof(f2,axiom,
! [X,Y] :
( smaller(X,Y)
<=> greater(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_smaller) ).
fof(f2_nnf,plain,
! [X,Y] :
( ( ~ greater(Y,X)
| smaller(X,Y) )
& ( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] :
( ( ~ greater(Y,X)
| smaller(X,Y) )
& ( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c6,plain,
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p160,plain,
( ~ spl14
| ~ spl11
| greater(sigma,eta) ),
inference(resolution,[status(thm)],[p131,c6]) ).
fof(sdef12,definition,
( spl12
<=> smaller(sigma,eta) ),
introduced(definition,[new_symbols(naming,[spl12])],[avatar_definition]) ).
cnf(p73,plain,
( ~ spl12
| smaller(sigma,eta) ),
inference(avatar_component_clause,[status(thm)],[sdef12]) ).
cnf(p98,plain,
( ~ spl12
| greater(eta,sigma) ),
inference(resolution,[status(thm)],[c6,p73]) ).
fof(f3,axiom,
! [X,Y] :
~ ( greater(Y,X)
& greater(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meaning_postulate_greater_strict) ).
fof(f3_nnf,plain,
! [X,Y] :
( ~ greater(Y,X)
| ~ greater(X,Y) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] :
( ~ greater(Y,X)
| ~ greater(X,Y) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c8,plain,
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p128,plain,
( ~ spl12
| ~ greater(sigma,eta) ),
inference(resolution,[status(thm)],[p98,c8]) ).
cnf(p182,plain,
( ~ spl14
| ~ spl12
| ~ spl11
| $false ),
inference(resolution,[status(thm)],[p160,p128]) ).
cnf(sct0,plain,
( ~ spl14
| ~ spl12
| ~ spl11 ),
inference(avatar_contradiction_clause,[status(thm)],[p182]) ).
fof(sdef7,definition,
( spl7
<=> age(sk1,sk3) = tau ),
introduced(definition,[new_symbols(naming,[spl7])],[avatar_definition]) ).
cnf(p61,plain,
( ~ spl7
| age(sk1,sk3) = tau ),
inference(avatar_component_clause,[status(thm)],[sdef7]) ).
fof(sdef4,definition,
( spl4
<=> smaller(age(sk1,sk3),sigma) ),
introduced(definition,[new_symbols(naming,[spl4])],[avatar_definition]) ).
cnf(p57,plain,
( ~ spl4
| smaller(age(sk1,sk3),sigma) ),
inference(avatar_component_clause,[status(thm)],[sdef4]) ).
cnf(p193,plain,
( ~ spl7
| ~ spl4
| smaller(tau,sigma) ),
inference(superposition,[status(thm)],[p61,p57]) ).
cnf(p204,plain,
( ~ spl7
| ~ spl4
| greater(sigma,tau) ),
inference(resolution,[status(thm)],[p193,c6]) ).
fof(sdef10,definition,
( spl10
<=> smaller(sigma,tau) ),
introduced(definition,[new_symbols(naming,[spl10])],[avatar_definition]) ).
cnf(p70,plain,
( ~ spl10
| smaller(sigma,tau) ),
inference(avatar_component_clause,[status(thm)],[sdef10]) ).
cnf(p97,plain,
( ~ spl10
| greater(tau,sigma) ),
inference(resolution,[status(thm)],[c6,p70]) ).
cnf(p120,plain,
( ~ spl10
| ~ greater(sigma,tau) ),
inference(resolution,[status(thm)],[p97,c8]) ).
cnf(p264,plain,
( ~ spl10
| ~ spl7
| ~ spl4
| $false ),
inference(resolution,[status(thm)],[p204,p120]) ).
cnf(sct1,plain,
( ~ spl10
| ~ spl7
| ~ spl4 ),
inference(avatar_contradiction_clause,[status(thm)],[p264]) ).
fof(sdef16,definition,
( spl16
<=> smaller(tau,sigma) ),
introduced(definition,[new_symbols(naming,[spl16])],[avatar_definition]) ).
cnf(p197,plain,
( ~ spl16
| smaller(tau,sigma) ),
inference(avatar_component_clause,[status(thm)],[sdef16]) ).
cnf(p210,plain,
( ~ spl16
| greater(sigma,tau) ),
inference(resolution,[status(thm)],[p197,c6]) ).
cnf(p277,plain,
( ~ spl16
| ~ spl10
| $false ),
inference(resolution,[status(thm)],[p210,p120]) ).
cnf(sct2,plain,
( ~ spl16
| ~ spl10 ),
inference(avatar_contradiction_clause,[status(thm)],[p277]) ).
fof(sdef17,definition,
( spl17
<=> tau = sigma ),
introduced(definition,[new_symbols(naming,[spl17])],[avatar_definition]) ).
cnf(p198,plain,
( ~ spl17
| tau = sigma ),
inference(avatar_component_clause,[status(thm)],[sdef17]) ).
cnf(p132,plain,
( ~ spl14
| greater(tau,eta) ),
inference(resolution,[status(thm)],[p101,c6]) ).
cnf(p220,plain,
( ~ spl17
| ~ spl14
| greater(sigma,eta) ),
inference(superposition,[status(thm)],[p198,p132]) ).
cnf(p290,plain,
( ~ spl17
| ~ spl14
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p220,p128]) ).
cnf(sct3,plain,
( ~ spl17
| ~ spl14
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p290]) ).
fof(sdef18,definition,
( spl18
<=> smaller(tau,eta) ),
introduced(definition,[new_symbols(naming,[spl18])],[avatar_definition]) ).
cnf(p201,plain,
( ~ spl18
| smaller(tau,eta) ),
inference(avatar_component_clause,[status(thm)],[sdef18]) ).
cnf(p235,plain,
( ~ spl18
| greater(eta,tau) ),
inference(resolution,[status(thm)],[p201,c6]) ).
cnf(p163,plain,
( ~ spl14
| ~ greater(eta,tau) ),
inference(resolution,[status(thm)],[p132,c8]) ).
cnf(p314,plain,
( ~ spl18
| ~ spl14
| $false ),
inference(resolution,[status(thm)],[p235,p163]) ).
cnf(sct4,plain,
( ~ spl18
| ~ spl14 ),
inference(avatar_contradiction_clause,[status(thm)],[p314]) ).
fof(sdef15,definition,
( spl15
<=> eta = tau ),
introduced(definition,[new_symbols(naming,[spl15])],[avatar_definition]) ).
cnf(p102,plain,
( ~ spl15
| eta = tau ),
inference(avatar_component_clause,[status(thm)],[sdef15]) ).
cnf(p276,plain,
( ~ spl16
| ~ spl15
| greater(sigma,eta) ),
inference(superposition,[status(thm)],[p102,p210]) ).
cnf(p384,plain,
( ~ spl16
| ~ spl15
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p276,p128]) ).
cnf(sct5,plain,
( ~ spl16
| ~ spl15
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p384]) ).
cnf(p112,plain,
~ greater(X0,X0),
inference(factoring,[status(thm)],[c8]) ).
cnf(p278,plain,
( ~ spl17
| ~ spl16
| greater(sigma,sigma) ),
inference(superposition,[status(thm)],[p198,p210]) ).
cnf(p460,plain,
( ~ spl17
| ~ spl16
| $false ),
inference(resolution,[status(thm)],[p112,p278]) ).
cnf(sct6,plain,
( ~ spl17
| ~ spl16 ),
inference(avatar_contradiction_clause,[status(thm)],[p460]) ).
cnf(p313,plain,
( ~ spl18
| ~ spl15
| greater(eta,eta) ),
inference(superposition,[status(thm)],[p102,p235]) ).
cnf(p461,plain,
( ~ spl18
| ~ spl15
| $false ),
inference(resolution,[status(thm)],[p112,p313]) ).
cnf(sct7,plain,
( ~ spl18
| ~ spl15 ),
inference(avatar_contradiction_clause,[status(thm)],[p461]) ).
fof(sdef19,definition,
( spl19
<=> tau = eta ),
introduced(definition,[new_symbols(naming,[spl19])],[avatar_definition]) ).
cnf(p202,plain,
( ~ spl19
| tau = eta ),
inference(avatar_component_clause,[status(thm)],[sdef19]) ).
cnf(p316,plain,
( ~ spl19
| ~ spl18
| greater(eta,eta) ),
inference(superposition,[status(thm)],[p202,p235]) ).
cnf(p462,plain,
( ~ spl19
| ~ spl18
| $false ),
inference(resolution,[status(thm)],[p112,p316]) ).
cnf(sct8,plain,
( ~ spl19
| ~ spl18 ),
inference(avatar_contradiction_clause,[status(thm)],[p462]) ).
fof(sdef13,definition,
( spl13
<=> sigma = eta ),
introduced(definition,[new_symbols(naming,[spl13])],[avatar_definition]) ).
cnf(p74,plain,
( ~ spl13
| sigma = eta ),
inference(avatar_component_clause,[status(thm)],[sdef13]) ).
cnf(p89,plain,
( ~ spl13
| ~ spl12
| smaller(eta,eta) ),
inference(superposition,[status(thm)],[p74,p73]) ).
cnf(p111,plain,
( ~ spl13
| ~ spl12
| greater(eta,eta) ),
inference(resolution,[status(thm)],[p89,c6]) ).
cnf(p465,plain,
( ~ spl13
| ~ spl12
| $false ),
inference(resolution,[status(thm)],[p111,p112]) ).
cnf(sct9,plain,
( ~ spl13
| ~ spl12 ),
inference(avatar_contradiction_clause,[status(thm)],[p465]) ).
fof(sdef20,definition,
( spl20
<=> smaller(eta,sigma) ),
introduced(definition,[new_symbols(naming,[spl20])],[avatar_definition]) ).
cnf(p232,plain,
( ~ spl20
| smaller(eta,sigma) ),
inference(avatar_component_clause,[status(thm)],[sdef20]) ).
cnf(p293,plain,
( ~ spl20
| ~ spl13
| smaller(eta,eta) ),
inference(superposition,[status(thm)],[p74,p232]) ).
cnf(p400,plain,
( ~ spl20
| ~ spl13
| greater(eta,eta) ),
inference(resolution,[status(thm)],[p293,c6]) ).
cnf(p466,plain,
( ~ spl20
| ~ spl13
| $false ),
inference(resolution,[status(thm)],[p400,p112]) ).
cnf(sct10,plain,
( ~ spl20
| ~ spl13 ),
inference(avatar_contradiction_clause,[status(thm)],[p466]) ).
fof(sdef21,definition,
( spl21
<=> eta = sigma ),
introduced(definition,[new_symbols(naming,[spl21])],[avatar_definition]) ).
cnf(p233,plain,
( ~ spl21
| eta = sigma ),
inference(avatar_component_clause,[status(thm)],[sdef21]) ).
cnf(p294,plain,
( ~ spl20
| greater(sigma,eta) ),
inference(resolution,[status(thm)],[p232,c6]) ).
cnf(p405,plain,
( ~ spl21
| ~ spl20
| greater(eta,eta) ),
inference(superposition,[status(thm)],[p233,p294]) ).
cnf(p467,plain,
( ~ spl21
| ~ spl20
| $false ),
inference(resolution,[status(thm)],[p405,p112]) ).
cnf(sct11,plain,
( ~ spl21
| ~ spl20 ),
inference(avatar_contradiction_clause,[status(thm)],[p467]) ).
fof(sdef24,definition,
( spl24
<=> ~ smaller_or_equal(zero,eta) ),
introduced(definition,[new_symbols(naming,[spl24])],[avatar_definition]) ).
cnf(p543,plain,
( ~ spl24
| ~ smaller_or_equal(zero,eta) ),
inference(avatar_component_clause,[status(thm)],[sdef24]) ).
cnf(c7,plain,
( ~ greater(X1,X0)
| smaller(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f16,conjecture,
! [X,T0,T1,T2] :
( ( greater(age(X,T2),eta)
& greater(age(X,T2),tau)
& greater(age(X,T2),sigma)
& smaller_or_equal(age(X,T1),eta)
& smaller_or_equal(age(X,T1),tau)
& smaller_or_equal(age(X,T1),sigma)
& greater(eta,zero)
& greater(tau,zero)
& greater(sigma,zero)
& age(X,T0) = zero
& has_endowment(X)
& ( fragile_position(X)
| robust_position(X) )
& organization(X) )
=> ( hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)
& greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_11) ).
fof(f16_neg,negated_conjecture,
~ ! [X,T0,T1,T2] :
( ( greater(age(X,T2),eta)
& greater(age(X,T2),tau)
& greater(age(X,T2),sigma)
& smaller_or_equal(age(X,T1),eta)
& smaller_or_equal(age(X,T1),tau)
& smaller_or_equal(age(X,T1),sigma)
& greater(eta,zero)
& greater(tau,zero)
& greater(sigma,zero)
& age(X,T0) = zero
& has_endowment(X)
& ( fragile_position(X)
| robust_position(X) )
& organization(X) )
=> ( hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)
& greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)) ) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X,T0,T1,T2] :
( ( hazard_of_mortality(X,T1) != hazard_of_mortality(X,T0)
| ~ greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)) )
& greater(age(X,T2),eta)
& greater(age(X,T2),tau)
& greater(age(X,T2),sigma)
& smaller_or_equal(age(X,T1),eta)
& smaller_or_equal(age(X,T1),tau)
& smaller_or_equal(age(X,T1),sigma)
& greater(eta,zero)
& greater(tau,zero)
& greater(sigma,zero)
& age(X,T0) = zero
& has_endowment(X)
& ( fragile_position(X)
| robust_position(X) )
& organization(X) ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( ( hazard_of_mortality(sk1,sk3) != hazard_of_mortality(sk1,sk2)
| ~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) )
& greater(age(sk1,sk4),eta)
& greater(age(sk1,sk4),tau)
& greater(age(sk1,sk4),sigma)
& smaller_or_equal(age(sk1,sk3),eta)
& smaller_or_equal(age(sk1,sk3),tau)
& smaller_or_equal(age(sk1,sk3),sigma)
& greater(eta,zero)
& greater(tau,zero)
& greater(sigma,zero)
& age(sk1,sk2) = zero
& has_endowment(sk1)
& ( fragile_position(sk1)
| robust_position(sk1) )
& organization(sk1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2,sk3,sk4])],[f16_nnf]) ).
cnf(c44,plain,
greater(eta,zero),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p107,plain,
smaller(zero,eta),
inference(resolution,[status(thm)],[c7,c44]) ).
fof(f0,axiom,
! [X,Y] :
( smaller_or_equal(X,Y)
<=> ( X = Y
| smaller(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_smaller_or_equal) ).
fof(f0_nnf,plain,
! [X,Y] :
( ( ( X != Y
& ~ smaller(X,Y) )
| smaller_or_equal(X,Y) )
& ( X = Y
| smaller(X,Y)
| ~ smaller_or_equal(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( ( ( X != Y
& ~ smaller(X,Y) )
| smaller_or_equal(X,Y) )
& ( X = Y
| smaller(X,Y)
| ~ smaller_or_equal(X,Y) ) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c1,plain,
( ~ smaller(X0,X1)
| smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p154,plain,
smaller_or_equal(zero,eta),
inference(resolution,[status(thm)],[p107,c1]) ).
cnf(p546,plain,
( ~ spl24
| $false ),
inference(resolution,[status(thm)],[p543,p154]) ).
cnf(sct12,plain,
~ spl24,
inference(avatar_contradiction_clause,[status(thm)],[p546]) ).
fof(f10,axiom,
! [X,T] :
( organization(X)
=> ( ( ~ has_immunity(X,T)
=> ( ( ( ~ positional_advantage(X,T)
& ~ is_aligned(X,T) )
=> hazard_of_mortality(X,T) = high )
& ( ( ~ positional_advantage(X,T)
& is_aligned(X,T) )
=> hazard_of_mortality(X,T) = mod2 )
& ( ( positional_advantage(X,T)
& ~ is_aligned(X,T) )
=> hazard_of_mortality(X,T) = mod1 )
& ( ( positional_advantage(X,T)
& is_aligned(X,T) )
=> hazard_of_mortality(X,T) = low ) ) )
& ( has_immunity(X,T)
=> hazard_of_mortality(X,T) = very_low ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_17) ).
fof(f10_nnf,plain,
! [X,T] :
( ( ( ( ( hazard_of_mortality(X,T) = high
| positional_advantage(X,T)
| is_aligned(X,T) )
& ( hazard_of_mortality(X,T) = mod2
| positional_advantage(X,T)
| ~ is_aligned(X,T) )
& ( hazard_of_mortality(X,T) = mod1
| ~ positional_advantage(X,T)
| is_aligned(X,T) )
& ( hazard_of_mortality(X,T) = low
| ~ positional_advantage(X,T)
| ~ is_aligned(X,T) ) )
| has_immunity(X,T) )
& ( hazard_of_mortality(X,T) = very_low
| ~ has_immunity(X,T) ) )
| ~ organization(X) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,T] :
( ( ( ( ( hazard_of_mortality(X,T) = high
| positional_advantage(X,T)
| is_aligned(X,T) )
& ( hazard_of_mortality(X,T) = mod2
| positional_advantage(X,T)
| ~ is_aligned(X,T) )
& ( hazard_of_mortality(X,T) = mod1
| ~ positional_advantage(X,T)
| is_aligned(X,T) )
& ( hazard_of_mortality(X,T) = low
| ~ positional_advantage(X,T)
| ~ is_aligned(X,T) ) )
| has_immunity(X,T) )
& ( hazard_of_mortality(X,T) = very_low
| ~ has_immunity(X,T) ) )
| ~ organization(X) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c28,plain,
( hazard_of_mortality(X0,X1) = very_low
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(c38,plain,
organization(sk1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p309,plain,
( hazard_of_mortality(sk1,X0) = very_low
| ~ has_immunity(sk1,X0) ),
inference(resolution,[status(thm)],[c28,c38]) ).
fof(f6,axiom,
! [X] :
( has_endowment(X)
<=> ! [T] :
( ( greater(age(X,T),eta)
=> ~ has_immunity(X,T) )
& ( smaller_or_equal(age(X,T),eta)
=> has_immunity(X,T) )
& organization(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_1) ).
fof(f6_nnf,plain,
! [X] :
( ( ? [T] :
( ( has_immunity(X,T)
& greater(age(X,T),eta) )
| ( ~ has_immunity(X,T)
& smaller_or_equal(age(X,T),eta) )
| ~ organization(X) )
| has_endowment(X) )
& ( ! [T] :
( ( ~ has_immunity(X,T)
| ~ greater(age(X,T),eta) )
& ( has_immunity(X,T)
| ~ smaller_or_equal(age(X,T),eta) )
& organization(X) )
| ~ has_endowment(X) ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,T] :
( ( ( has_immunity(X,sk0(X))
& greater(age(X,sk0(X)),eta) )
| ( ~ has_immunity(X,sk0(X))
& smaller_or_equal(age(X,sk0(X)),eta) )
| ~ organization(X)
| has_endowment(X) )
& ( ( ( ~ has_immunity(X,T)
| ~ greater(age(X,T),eta) )
& ( has_immunity(X,T)
| ~ smaller_or_equal(age(X,T),eta) )
& organization(X) )
| ~ has_endowment(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f6_nnf]) ).
cnf(c12,plain,
( has_immunity(X0,X1)
| ~ smaller_or_equal(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c40,plain,
has_endowment(sk1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p155,plain,
( has_immunity(sk1,X0)
| ~ smaller_or_equal(age(sk1,X0),eta) ),
inference(resolution,[status(thm)],[c12,c40]) ).
cnf(c47,plain,
smaller_or_equal(age(sk1,sk3),eta),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p545,plain,
has_immunity(sk1,sk3),
inference(resolution,[status(thm)],[p155,c47]) ).
cnf(p587,plain,
hazard_of_mortality(sk1,sk3) = very_low,
inference(resolution,[status(thm)],[p309,p545]) ).
fof(sdef23,definition,
( spl23
<=> hazard_of_mortality(sk1,sk4) = hazard_of_mortality(sk1,sk3) ),
introduced(definition,[new_symbols(naming,[spl23])],[avatar_definition]) ).
cnf(p399,plain,
( ~ spl23
| hazard_of_mortality(sk1,sk4) = hazard_of_mortality(sk1,sk3) ),
inference(avatar_component_clause,[status(thm)],[sdef23]) ).
fof(sdef22,definition,
( spl22
<=> smaller(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) ),
introduced(definition,[new_symbols(naming,[spl22])],[avatar_definition]) ).
cnf(p398,plain,
( ~ spl22
| smaller(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) ),
inference(avatar_component_clause,[status(thm)],[sdef22]) ).
cnf(p557,plain,
( ~ spl22
| greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk4)) ),
inference(resolution,[status(thm)],[p398,c6]) ).
cnf(p582,plain,
( ~ spl23
| ~ spl22
| greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk3)) ),
inference(superposition,[status(thm)],[p399,p557]) ).
cnf(p601,plain,
( ~ spl23
| ~ spl22
| greater(very_low,very_low) ),
inference(demodulation,[status(thm)],[p587,p582]) ).
cnf(p602,plain,
( ~ spl23
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p601,p112]) ).
cnf(sct13,plain,
( ~ spl23
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p602]) ).
fof(sdef25,definition,
( spl25
<=> has_immunity(sk1,sk2) ),
introduced(definition,[new_symbols(naming,[spl25])],[avatar_definition]) ).
cnf(p544,plain,
( ~ spl25
| has_immunity(sk1,sk2) ),
inference(avatar_component_clause,[status(thm)],[sdef25]) ).
cnf(p586,plain,
( ~ spl25
| hazard_of_mortality(sk1,sk2) = very_low ),
inference(resolution,[status(thm)],[p309,p544]) ).
fof(sdef3,definition,
( spl3
<=> hazard_of_mortality(sk1,sk3) != hazard_of_mortality(sk1,sk2) ),
introduced(definition,[new_symbols(naming,[spl3])],[avatar_definition]) ).
cnf(p55,plain,
( ~ spl3
| hazard_of_mortality(sk1,sk3) != hazard_of_mortality(sk1,sk2) ),
inference(avatar_component_clause,[status(thm)],[sdef3]) ).
cnf(p590,plain,
( ~ spl3
| very_low != hazard_of_mortality(sk1,sk2) ),
inference(demodulation,[status(thm)],[p587,p55]) ).
cnf(p606,plain,
( ~ spl25
| ~ spl3
| very_low != very_low ),
inference(superposition,[status(thm)],[p586,p590]) ).
cnf(p607,plain,
( ~ spl25
| ~ spl3
| $false ),
inference(equality_resolution,[status(thm)],[p606]) ).
cnf(sct14,plain,
( ~ spl25
| ~ spl3 ),
inference(avatar_contradiction_clause,[status(thm)],[p607]) ).
fof(sdef28,definition,
( spl28
<=> positional_advantage(sk1,sk2) ),
introduced(definition,[new_symbols(naming,[spl28])],[avatar_definition]) ).
cnf(p609,plain,
( ~ spl28
| positional_advantage(sk1,sk2) ),
inference(avatar_component_clause,[status(thm)],[sdef28]) ).
fof(sdef26,definition,
( spl26
<=> ~ positional_advantage(sk1,sk2) ),
introduced(definition,[new_symbols(naming,[spl26])],[avatar_definition]) ).
cnf(p604,plain,
( ~ spl26
| ~ positional_advantage(sk1,sk2) ),
inference(avatar_component_clause,[status(thm)],[sdef26]) ).
cnf(p611,plain,
( ~ spl28
| ~ spl26
| $false ),
inference(resolution,[status(thm)],[p609,p604]) ).
cnf(sct15,plain,
( ~ spl28
| ~ spl26 ),
inference(avatar_contradiction_clause,[status(thm)],[p611]) ).
fof(sdef27,definition,
( spl27
<=> hazard_of_mortality(sk1,sk2) = low ),
introduced(definition,[new_symbols(naming,[spl27])],[avatar_definition]) ).
cnf(p605,plain,
( ~ spl27
| hazard_of_mortality(sk1,sk2) = low ),
inference(avatar_component_clause,[status(thm)],[sdef27]) ).
cnf(p612,plain,
( ~ spl27
| ~ spl25
| low = very_low ),
inference(superposition,[status(thm)],[p605,p586]) ).
fof(f13,axiom,
greater(low,very_low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_18c) ).
fof(f13_nnf,plain,
greater(low,very_low),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c35,plain,
greater(low,very_low),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(p615,plain,
( ~ spl27
| ~ spl25
| greater(very_low,very_low) ),
inference(superposition,[status(thm)],[p612,c35]) ).
cnf(p639,plain,
( ~ spl27
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p615,p112]) ).
cnf(sct16,plain,
( ~ spl27
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p639]) ).
fof(sdef30,definition,
( spl30
<=> has_immunity(sk1,sk4) ),
introduced(definition,[new_symbols(naming,[spl30])],[avatar_definition]) ).
cnf(p620,plain,
( ~ spl30
| has_immunity(sk1,sk4) ),
inference(avatar_component_clause,[status(thm)],[sdef30]) ).
cnf(c13,plain,
( ~ has_immunity(X0,X1)
| ~ greater(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p157,plain,
( ~ has_immunity(sk1,X0)
| ~ greater(age(sk1,X0),eta) ),
inference(resolution,[status(thm)],[c13,c40]) ).
cnf(c50,plain,
greater(age(sk1,sk4),eta),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p548,plain,
~ has_immunity(sk1,sk4),
inference(resolution,[status(thm)],[p157,c50]) ).
cnf(p640,plain,
( ~ spl30
| $false ),
inference(resolution,[status(thm)],[p620,p548]) ).
cnf(sct17,plain,
~ spl30,
inference(avatar_contradiction_clause,[status(thm)],[p640]) ).
fof(sdef38,definition,
( spl38
<=> ~ positional_advantage(sk1,sk4) ),
introduced(definition,[new_symbols(naming,[spl38])],[avatar_definition]) ).
cnf(p644,plain,
( ~ spl38
| ~ positional_advantage(sk1,sk4) ),
inference(avatar_component_clause,[status(thm)],[sdef38]) ).
fof(sdef32,definition,
( spl32
<=> positional_advantage(sk1,sk4) ),
introduced(definition,[new_symbols(naming,[spl32])],[avatar_definition]) ).
cnf(p622,plain,
( ~ spl32
| positional_advantage(sk1,sk4) ),
inference(avatar_component_clause,[status(thm)],[sdef32]) ).
cnf(p663,plain,
( ~ spl38
| ~ spl32
| $false ),
inference(resolution,[status(thm)],[p644,p622]) ).
cnf(sct18,plain,
( ~ spl38
| ~ spl32 ),
inference(avatar_contradiction_clause,[status(thm)],[p663]) ).
fof(sdef29,definition,
( spl29
<=> hazard_of_mortality(sk1,sk2) = mod2 ),
introduced(definition,[new_symbols(naming,[spl29])],[avatar_definition]) ).
cnf(p610,plain,
( ~ spl29
| hazard_of_mortality(sk1,sk2) = mod2 ),
inference(avatar_component_clause,[status(thm)],[sdef29]) ).
cnf(p717,plain,
( ~ spl29
| ~ spl25
| mod2 = very_low ),
inference(superposition,[status(thm)],[p610,p586]) ).
fof(f15,axiom,
greater(mod2,low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_18e) ).
fof(f15_nnf,plain,
greater(mod2,low),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c37,plain,
greater(mod2,low),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(p720,plain,
( ~ spl29
| ~ spl25
| greater(very_low,low) ),
inference(superposition,[status(thm)],[p717,c37]) ).
cnf(p364,plain,
~ greater(very_low,low),
inference(resolution,[status(thm)],[c35,c8]) ).
cnf(p741,plain,
( ~ spl29
| ~ spl25
| $false ),
inference(resolution,[status(thm)],[p720,p364]) ).
cnf(sct19,plain,
( ~ spl29
| ~ spl25 ),
inference(avatar_contradiction_clause,[status(thm)],[p741]) ).
fof(f4,axiom,
! [X,Y,Z] :
( ( greater(Y,Z)
& greater(X,Y) )
=> greater(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meaning_postulate_greater_transitive) ).
fof(f4_nnf,plain,
! [X,Y,Z] :
( greater(X,Z)
| ~ greater(Y,Z)
| ~ greater(X,Y) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y,Z] :
( greater(X,Z)
| ~ greater(Y,Z)
| ~ greater(X,Y) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c9,plain,
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p365,plain,
( greater(low,X0)
| ~ greater(very_low,X0) ),
inference(resolution,[status(thm)],[c35,c9]) ).
fof(sdef42,definition,
( spl42
<=> high = very_low ),
introduced(definition,[new_symbols(naming,[spl42])],[avatar_definition]) ).
cnf(p651,plain,
( ~ spl42
| high = very_low ),
inference(avatar_component_clause,[status(thm)],[sdef42]) ).
fof(f11,axiom,
greater(high,mod1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_18a) ).
fof(f11_nnf,plain,
greater(high,mod1),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c33,plain,
greater(high,mod1),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(p664,plain,
( ~ spl42
| greater(very_low,mod1) ),
inference(superposition,[status(thm)],[p651,c33]) ).
cnf(p727,plain,
( ~ spl42
| greater(low,mod1) ),
inference(resolution,[status(thm)],[p365,p664]) ).
fof(f12,axiom,
greater(mod1,low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_18b) ).
fof(f12_nnf,plain,
greater(mod1,low),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c34,plain,
greater(mod1,low),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(p354,plain,
~ greater(low,mod1),
inference(resolution,[status(thm)],[c34,c8]) ).
cnf(p747,plain,
( ~ spl42
| $false ),
inference(resolution,[status(thm)],[p727,p354]) ).
cnf(sct20,plain,
~ spl42,
inference(avatar_contradiction_clause,[status(thm)],[p747]) ).
fof(sdef36,definition,
( spl36
<=> greater(very_low,high) ),
introduced(definition,[new_symbols(naming,[spl36])],[avatar_definition]) ).
cnf(p629,plain,
( ~ spl36
| greater(very_low,high) ),
inference(avatar_component_clause,[status(thm)],[sdef36]) ).
cnf(p748,plain,
( ~ spl36
| greater(low,high) ),
inference(resolution,[status(thm)],[p629,p365]) ).
cnf(p355,plain,
( greater(mod1,X0)
| ~ greater(low,X0) ),
inference(resolution,[status(thm)],[c34,c9]) ).
cnf(p759,plain,
( ~ spl36
| greater(mod1,high) ),
inference(resolution,[status(thm)],[p748,p355]) ).
cnf(p347,plain,
~ greater(mod1,high),
inference(resolution,[status(thm)],[c33,c8]) ).
cnf(p773,plain,
( ~ spl36
| $false ),
inference(resolution,[status(thm)],[p759,p347]) ).
cnf(sct21,plain,
~ spl36,
inference(avatar_contradiction_clause,[status(thm)],[p773]) ).
fof(sdef34,definition,
( spl34
<=> smaller(high,very_low) ),
introduced(definition,[new_symbols(naming,[spl34])],[avatar_definition]) ).
cnf(p625,plain,
( ~ spl34
| smaller(high,very_low) ),
inference(avatar_component_clause,[status(thm)],[sdef34]) ).
cnf(p653,plain,
( ~ spl34
| greater(very_low,high) ),
inference(resolution,[status(thm)],[p625,c6]) ).
cnf(p750,plain,
( ~ spl34
| greater(low,high) ),
inference(resolution,[status(thm)],[p653,p365]) ).
cnf(p765,plain,
( ~ spl34
| greater(mod1,high) ),
inference(resolution,[status(thm)],[p750,p355]) ).
cnf(p780,plain,
( ~ spl34
| $false ),
inference(resolution,[status(thm)],[p765,p347]) ).
cnf(sct22,plain,
~ spl34,
inference(avatar_contradiction_clause,[status(thm)],[p780]) ).
fof(sdef43,definition,
( spl43
<=> very_low = high ),
introduced(definition,[new_symbols(naming,[spl43])],[avatar_definition]) ).
cnf(p662,plain,
( ~ spl43
| very_low = high ),
inference(avatar_component_clause,[status(thm)],[sdef43]) ).
cnf(p683,plain,
( ~ spl43
| greater(very_low,mod1) ),
inference(superposition,[status(thm)],[p662,c33]) ).
cnf(p729,plain,
( ~ spl43
| greater(low,mod1) ),
inference(resolution,[status(thm)],[p365,p683]) ).
cnf(p788,plain,
( ~ spl43
| $false ),
inference(resolution,[status(thm)],[p729,p354]) ).
cnf(sct23,plain,
~ spl43,
inference(avatar_contradiction_clause,[status(thm)],[p788]) ).
fof(sdef39,definition,
( spl39
<=> hazard_of_mortality(sk1,sk4) = low ),
introduced(definition,[new_symbols(naming,[spl39])],[avatar_definition]) ).
cnf(p645,plain,
( ~ spl39
| hazard_of_mortality(sk1,sk4) = low ),
inference(avatar_component_clause,[status(thm)],[sdef39]) ).
fof(sdef2,definition,
( spl2
<=> ~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) ),
introduced(definition,[new_symbols(naming,[spl2])],[avatar_definition]) ).
cnf(p54,plain,
( ~ spl2
| ~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) ),
inference(avatar_component_clause,[status(thm)],[sdef2]) ).
cnf(p589,plain,
( ~ spl2
| ~ greater(hazard_of_mortality(sk1,sk4),very_low) ),
inference(demodulation,[status(thm)],[p587,p54]) ).
cnf(p789,plain,
( ~ spl39
| ~ spl2
| ~ greater(low,very_low) ),
inference(superposition,[status(thm)],[p645,p589]) ).
cnf(p803,plain,
( ~ spl39
| ~ spl2
| $false ),
inference(resolution,[status(thm)],[p789,c35]) ).
cnf(sct24,plain,
( ~ spl39
| ~ spl2 ),
inference(avatar_contradiction_clause,[status(thm)],[p803]) ).
fof(sdef44,definition,
( spl44
<=> low = high ),
introduced(definition,[new_symbols(naming,[spl44])],[avatar_definition]) ).
cnf(p796,plain,
( ~ spl44
| low = high ),
inference(avatar_component_clause,[status(thm)],[sdef44]) ).
cnf(p806,plain,
( ~ spl44
| greater(low,mod1) ),
inference(superposition,[status(thm)],[p796,c33]) ).
cnf(p847,plain,
( ~ spl44
| $false ),
inference(resolution,[status(thm)],[p806,p354]) ).
cnf(sct25,plain,
~ spl44,
inference(avatar_contradiction_clause,[status(thm)],[p847]) ).
fof(sdef45,definition,
( spl45
<=> high = low ),
introduced(definition,[new_symbols(naming,[spl45])],[avatar_definition]) ).
cnf(p798,plain,
( ~ spl45
| high = low ),
inference(avatar_component_clause,[status(thm)],[sdef45]) ).
cnf(p815,plain,
( ~ spl45
| greater(low,mod1) ),
inference(superposition,[status(thm)],[p798,c33]) ).
cnf(p855,plain,
( ~ spl45
| $false ),
inference(resolution,[status(thm)],[p815,p354]) ).
cnf(sct26,plain,
~ spl45,
inference(avatar_contradiction_clause,[status(thm)],[p855]) ).
fof(sdef46,definition,
( spl46
<=> smaller(low,very_low) ),
introduced(definition,[new_symbols(naming,[spl46])],[avatar_definition]) ).
cnf(p801,plain,
( ~ spl46
| smaller(low,very_low) ),
inference(avatar_component_clause,[status(thm)],[sdef46]) ).
cnf(p825,plain,
( ~ spl46
| greater(very_low,low) ),
inference(resolution,[status(thm)],[p801,c6]) ).
cnf(p860,plain,
( ~ spl46
| $false ),
inference(resolution,[status(thm)],[p825,p364]) ).
cnf(sct27,plain,
~ spl46,
inference(avatar_contradiction_clause,[status(thm)],[p860]) ).
fof(sdef47,definition,
( spl47
<=> low = very_low ),
introduced(definition,[new_symbols(naming,[spl47])],[avatar_definition]) ).
cnf(p802,plain,
( ~ spl47
| low = very_low ),
inference(avatar_component_clause,[status(thm)],[sdef47]) ).
cnf(p832,plain,
( ~ spl47
| greater(very_low,very_low) ),
inference(superposition,[status(thm)],[p802,c35]) ).
cnf(p861,plain,
( ~ spl47
| $false ),
inference(resolution,[status(thm)],[p832,p112]) ).
cnf(sct28,plain,
~ spl47,
inference(avatar_contradiction_clause,[status(thm)],[p861]) ).
fof(sdef40,definition,
( spl40
<=> hazard_of_mortality(sk1,sk4) = mod2 ),
introduced(definition,[new_symbols(naming,[spl40])],[avatar_definition]) ).
cnf(p647,plain,
( ~ spl40
| hazard_of_mortality(sk1,sk4) = mod2 ),
inference(avatar_component_clause,[status(thm)],[sdef40]) ).
cnf(p595,plain,
( ~ spl22
| greater(very_low,hazard_of_mortality(sk1,sk4)) ),
inference(demodulation,[status(thm)],[p587,p557]) ).
cnf(p866,plain,
( ~ spl40
| ~ spl22
| greater(very_low,mod2) ),
inference(superposition,[status(thm)],[p647,p595]) ).
cnf(p883,plain,
( ~ spl40
| ~ spl22
| greater(low,mod2) ),
inference(resolution,[status(thm)],[p866,p365]) ).
cnf(p389,plain,
~ greater(low,mod2),
inference(resolution,[status(thm)],[c37,c8]) ).
cnf(p921,plain,
( ~ spl40
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p883,p389]) ).
cnf(sct29,plain,
( ~ spl40
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p921]) ).
fof(sdef48,definition,
( spl48
<=> mod2 = high ),
introduced(definition,[new_symbols(naming,[spl48])],[avatar_definition]) ).
cnf(p870,plain,
( ~ spl48
| mod2 = high ),
inference(avatar_component_clause,[status(thm)],[sdef48]) ).
fof(f14,axiom,
greater(high,mod2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_18d) ).
fof(f14_nnf,plain,
greater(high,mod2),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c36,plain,
greater(high,mod2),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(p886,plain,
( ~ spl48
| greater(mod2,mod2) ),
inference(superposition,[status(thm)],[p870,c36]) ).
cnf(p931,plain,
( ~ spl48
| $false ),
inference(resolution,[status(thm)],[p886,p112]) ).
cnf(sct30,plain,
~ spl48,
inference(avatar_contradiction_clause,[status(thm)],[p931]) ).
fof(sdef49,definition,
( spl49
<=> high = mod2 ),
introduced(definition,[new_symbols(naming,[spl49])],[avatar_definition]) ).
cnf(p872,plain,
( ~ spl49
| high = mod2 ),
inference(avatar_component_clause,[status(thm)],[sdef49]) ).
cnf(p894,plain,
( ~ spl49
| greater(mod2,mod2) ),
inference(superposition,[status(thm)],[p872,c36]) ).
cnf(p940,plain,
( ~ spl49
| $false ),
inference(resolution,[status(thm)],[p894,p112]) ).
cnf(sct31,plain,
~ spl49,
inference(avatar_contradiction_clause,[status(thm)],[p940]) ).
fof(sdef51,definition,
( spl51
<=> mod2 = very_low ),
introduced(definition,[new_symbols(naming,[spl51])],[avatar_definition]) ).
cnf(p875,plain,
( ~ spl51
| mod2 = very_low ),
inference(avatar_component_clause,[status(thm)],[sdef51]) ).
cnf(p903,plain,
( ~ spl51
| greater(very_low,low) ),
inference(superposition,[status(thm)],[p875,c37]) ).
cnf(p951,plain,
( ~ spl51
| $false ),
inference(resolution,[status(thm)],[p903,p364]) ).
cnf(sct32,plain,
~ spl51,
inference(avatar_contradiction_clause,[status(thm)],[p951]) ).
fof(sdef50,definition,
( spl50
<=> smaller(mod2,very_low) ),
introduced(definition,[new_symbols(naming,[spl50])],[avatar_definition]) ).
cnf(p874,plain,
( ~ spl50
| smaller(mod2,very_low) ),
inference(avatar_component_clause,[status(thm)],[sdef50]) ).
cnf(p901,plain,
( ~ spl50
| greater(very_low,mod2) ),
inference(resolution,[status(thm)],[p874,c6]) ).
cnf(p945,plain,
( ~ spl50
| greater(low,mod2) ),
inference(resolution,[status(thm)],[p901,p365]) ).
cnf(p959,plain,
( ~ spl50
| $false ),
inference(resolution,[status(thm)],[p945,p389]) ).
cnf(sct33,plain,
~ spl50,
inference(avatar_contradiction_clause,[status(thm)],[p959]) ).
fof(sdef41,definition,
( spl41
<=> hazard_of_mortality(sk1,sk4) = mod1 ),
introduced(definition,[new_symbols(naming,[spl41])],[avatar_definition]) ).
cnf(p649,plain,
( ~ spl41
| hazard_of_mortality(sk1,sk4) = mod1 ),
inference(avatar_component_clause,[status(thm)],[sdef41]) ).
cnf(p963,plain,
( ~ spl41
| ~ spl22
| greater(very_low,mod1) ),
inference(superposition,[status(thm)],[p649,p595]) ).
cnf(p976,plain,
( ~ spl41
| ~ spl22
| greater(low,mod1) ),
inference(resolution,[status(thm)],[p963,p365]) ).
cnf(p1015,plain,
( ~ spl41
| ~ spl22
| $false ),
inference(resolution,[status(thm)],[p976,p354]) ).
cnf(sct34,plain,
( ~ spl41
| ~ spl22 ),
inference(avatar_contradiction_clause,[status(thm)],[p1015]) ).
fof(sdef52,definition,
( spl52
<=> mod1 = high ),
introduced(definition,[new_symbols(naming,[spl52])],[avatar_definition]) ).
cnf(p967,plain,
( ~ spl52
| mod1 = high ),
inference(avatar_component_clause,[status(thm)],[sdef52]) ).
cnf(p979,plain,
( ~ spl52
| greater(mod1,mod1) ),
inference(superposition,[status(thm)],[p967,c33]) ).
cnf(p1017,plain,
( ~ spl52
| $false ),
inference(resolution,[status(thm)],[p979,p112]) ).
cnf(sct35,plain,
~ spl52,
inference(avatar_contradiction_clause,[status(thm)],[p1017]) ).
fof(sdef53,definition,
( spl53
<=> high = mod1 ),
introduced(definition,[new_symbols(naming,[spl53])],[avatar_definition]) ).
cnf(p969,plain,
( ~ spl53
| high = mod1 ),
inference(avatar_component_clause,[status(thm)],[sdef53]) ).
cnf(p986,plain,
( ~ spl53
| greater(mod1,mod1) ),
inference(superposition,[status(thm)],[p969,c33]) ).
cnf(p1018,plain,
( ~ spl53
| $false ),
inference(resolution,[status(thm)],[p986,p112]) ).
cnf(sct36,plain,
~ spl53,
inference(avatar_contradiction_clause,[status(thm)],[p1018]) ).
fof(sdef55,definition,
( spl55
<=> mod1 = very_low ),
introduced(definition,[new_symbols(naming,[spl55])],[avatar_definition]) ).
cnf(p972,plain,
( ~ spl55
| mod1 = very_low ),
inference(avatar_component_clause,[status(thm)],[sdef55]) ).
cnf(p996,plain,
( ~ spl55
| greater(very_low,low) ),
inference(superposition,[status(thm)],[p972,c34]) ).
cnf(p1029,plain,
( ~ spl55
| $false ),
inference(resolution,[status(thm)],[p996,p364]) ).
cnf(sct37,plain,
~ spl55,
inference(avatar_contradiction_clause,[status(thm)],[p1029]) ).
fof(sdef54,definition,
( spl54
<=> smaller(mod1,very_low) ),
introduced(definition,[new_symbols(naming,[spl54])],[avatar_definition]) ).
cnf(p971,plain,
( ~ spl54
| smaller(mod1,very_low) ),
inference(avatar_component_clause,[status(thm)],[sdef54]) ).
cnf(p994,plain,
( ~ spl54
| greater(very_low,mod1) ),
inference(resolution,[status(thm)],[p971,c6]) ).
cnf(p1024,plain,
( ~ spl54
| greater(low,mod1) ),
inference(resolution,[status(thm)],[p994,p365]) ).
cnf(p1062,plain,
( ~ spl54
| $false ),
inference(resolution,[status(thm)],[p1024,p354]) ).
cnf(sct38,plain,
~ spl54,
inference(avatar_contradiction_clause,[status(thm)],[p1062]) ).
cnf(c39,plain,
( fragile_position(sk1)
| robust_position(sk1) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
fof(sdef0,definition,
( spl0
<=> robust_position(sk1) ),
introduced(definition,[new_symbols(naming,[spl0])],[avatar_definition]) ).
fof(sdef1,definition,
( spl1
<=> fragile_position(sk1) ),
introduced(definition,[new_symbols(naming,[spl1])],[avatar_definition]) ).
cnf(ssp0,plain,
( spl1
| spl0 ),
inference(avatar_split_clause,[status(thm)],[c39,sdef0,sdef1]) ).
cnf(c51,plain,
( hazard_of_mortality(sk1,sk3) != hazard_of_mortality(sk1,sk2)
| ~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(ssp1,plain,
( spl3
| spl2 ),
inference(avatar_split_clause,[status(thm)],[c51,sdef2,sdef3]) ).
cnf(c45,plain,
smaller_or_equal(age(sk1,sk3),sigma),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(c0,plain,
( X0 = X1
| smaller(X0,X1)
| ~ smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p56,plain,
( age(sk1,sk3) = sigma
| smaller(age(sk1,sk3),sigma) ),
inference(resolution,[status(thm)],[c45,c0]) ).
fof(sdef5,definition,
( spl5
<=> age(sk1,sk3) = sigma ),
introduced(definition,[new_symbols(naming,[spl5])],[avatar_definition]) ).
cnf(ssp2,plain,
( spl5
| spl4 ),
inference(avatar_split_clause,[status(thm)],[p56,sdef4,sdef5]) ).
cnf(c46,plain,
smaller_or_equal(age(sk1,sk3),tau),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p59,plain,
( age(sk1,sk3) = tau
| smaller(age(sk1,sk3),tau) ),
inference(resolution,[status(thm)],[c46,c0]) ).
fof(sdef6,definition,
( spl6
<=> smaller(age(sk1,sk3),tau) ),
introduced(definition,[new_symbols(naming,[spl6])],[avatar_definition]) ).
cnf(ssp3,plain,
( spl7
| spl6 ),
inference(avatar_split_clause,[status(thm)],[p59,sdef6,sdef7]) ).
cnf(p62,plain,
( age(sk1,sk3) = eta
| smaller(age(sk1,sk3),eta) ),
inference(resolution,[status(thm)],[c47,c0]) ).
fof(sdef8,definition,
( spl8
<=> smaller(age(sk1,sk3),eta) ),
introduced(definition,[new_symbols(naming,[spl8])],[avatar_definition]) ).
fof(sdef9,definition,
( spl9
<=> age(sk1,sk3) = eta ),
introduced(definition,[new_symbols(naming,[spl9])],[avatar_definition]) ).
cnf(ssp4,plain,
( spl9
| spl8 ),
inference(avatar_split_clause,[status(thm)],[p62,sdef8,sdef9]) ).
cnf(p58,plain,
( ~ spl5
| age(sk1,sk3) = sigma ),
inference(avatar_component_clause,[status(thm)],[sdef5]) ).
cnf(p66,plain,
( ~ spl5
| smaller_or_equal(sigma,tau) ),
inference(superposition,[status(thm)],[p58,c46]) ).
cnf(p69,plain,
( ~ spl5
| sigma = tau
| smaller(sigma,tau) ),
inference(resolution,[status(thm)],[p66,c0]) ).
cnf(ssp5,plain,
( spl11
| spl10
| ~ spl5 ),
inference(avatar_split_clause,[status(thm)],[p69,sdef10,sdef11]) ).
cnf(p67,plain,
( ~ spl5
| smaller_or_equal(sigma,eta) ),
inference(superposition,[status(thm)],[p58,c47]) ).
cnf(p72,plain,
( ~ spl5
| sigma = eta
| smaller(sigma,eta) ),
inference(resolution,[status(thm)],[p67,c0]) ).
cnf(ssp6,plain,
( spl13
| spl12
| ~ spl5 ),
inference(avatar_split_clause,[status(thm)],[p72,sdef12,sdef13]) ).
cnf(p85,plain,
( ~ spl13
| ~ spl5
| smaller_or_equal(eta,tau) ),
inference(superposition,[status(thm)],[p74,p66]) ).
cnf(p100,plain,
( ~ spl13
| ~ spl5
| eta = tau
| smaller(eta,tau) ),
inference(resolution,[status(thm)],[p85,c0]) ).
cnf(ssp7,plain,
( spl15
| spl14
| ~ spl13
| ~ spl5 ),
inference(avatar_split_clause,[status(thm)],[p100,sdef14,sdef15]) ).
cnf(p191,plain,
( ~ spl7
| smaller_or_equal(tau,sigma) ),
inference(superposition,[status(thm)],[p61,c45]) ).
cnf(p196,plain,
( ~ spl7
| tau = sigma
| smaller(tau,sigma) ),
inference(resolution,[status(thm)],[p191,c0]) ).
cnf(ssp8,plain,
( spl17
| spl16
| ~ spl7 ),
inference(avatar_split_clause,[status(thm)],[p196,sdef16,sdef17]) ).
cnf(p192,plain,
( ~ spl7
| smaller_or_equal(tau,eta) ),
inference(superposition,[status(thm)],[p61,c47]) ).
cnf(p200,plain,
( ~ spl7
| tau = eta
| smaller(tau,eta) ),
inference(resolution,[status(thm)],[p192,c0]) ).
cnf(ssp9,plain,
( spl19
| spl18
| ~ spl7 ),
inference(avatar_split_clause,[status(thm)],[p200,sdef18,sdef19]) ).
cnf(p199,plain,
( ~ spl15
| ~ spl7
| smaller_or_equal(eta,sigma) ),
inference(superposition,[status(thm)],[p102,p191]) ).
cnf(p231,plain,
( ~ spl15
| ~ spl7
| eta = sigma
| smaller(eta,sigma) ),
inference(resolution,[status(thm)],[p199,c0]) ).
cnf(ssp10,plain,
( spl21
| spl20
| ~ spl15
| ~ spl7 ),
inference(avatar_split_clause,[status(thm)],[p231,sdef20,sdef21]) ).
fof(f5,axiom,
! [X,Y] :
( greater(X,Y)
| X = Y
| smaller(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meaning_postulate_greater_comparable) ).
fof(f5_nnf,plain,
! [X,Y] :
( greater(X,Y)
| X = Y
| smaller(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] :
( greater(X,Y)
| X = Y
| smaller(X,Y) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c10,plain,
( greater(X0,X1)
| X0 = X1
| smaller(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p397,plain,
( ~ spl2
| hazard_of_mortality(sk1,sk4) = hazard_of_mortality(sk1,sk3)
| smaller(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) ),
inference(resolution,[status(thm)],[p54,c10]) ).
cnf(ssp11,plain,
( spl23
| spl22
| ~ spl2 ),
inference(avatar_split_clause,[status(thm)],[p397,sdef22,sdef23]) ).
cnf(p64,plain,
( ~ spl9
| age(sk1,sk3) = eta ),
inference(avatar_component_clause,[status(thm)],[sdef9]) ).
cnf(p415,plain,
( ~ spl9
| smaller_or_equal(eta,sigma) ),
inference(superposition,[status(thm)],[p64,c45]) ).
cnf(p468,plain,
( ~ spl9
| eta = sigma
| smaller(eta,sigma) ),
inference(resolution,[status(thm)],[p415,c0]) ).
cnf(ssp12,plain,
( spl21
| spl20
| ~ spl9 ),
inference(avatar_split_clause,[status(thm)],[p468,sdef20,sdef21]) ).
cnf(p416,plain,
( ~ spl9
| smaller_or_equal(eta,tau) ),
inference(superposition,[status(thm)],[p64,c46]) ).
cnf(p469,plain,
( ~ spl9
| eta = tau
| smaller(eta,tau) ),
inference(resolution,[status(thm)],[p416,c0]) ).
cnf(ssp13,plain,
( spl15
| spl14
| ~ spl9 ),
inference(avatar_split_clause,[status(thm)],[p469,sdef14,sdef15]) ).
cnf(c41,plain,
age(sk1,sk2) = zero,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p542,plain,
( has_immunity(sk1,sk2)
| ~ smaller_or_equal(zero,eta) ),
inference(superposition,[status(thm)],[c41,p155]) ).
cnf(ssp14,plain,
( spl25
| spl24 ),
inference(avatar_split_clause,[status(thm)],[p542,sdef24,sdef25]) ).
cnf(c29,plain,
( hazard_of_mortality(X0,X1) = low
| ~ positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p329,plain,
( hazard_of_mortality(sk1,X0) = low
| ~ positional_advantage(sk1,X0)
| ~ is_aligned(sk1,X0)
| has_immunity(sk1,X0) ),
inference(resolution,[status(thm)],[c29,c38]) ).
fof(f8,axiom,
! [X,T] :
( ( age(X,T) = zero
& organization(X) )
=> is_aligned(X,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_13) ).
fof(f8_nnf,plain,
! [X,T] :
( is_aligned(X,T)
| age(X,T) != zero
| ~ organization(X) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X,T] :
( is_aligned(X,T)
| age(X,T) != zero
| ~ organization(X) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c25,plain,
( is_aligned(X0,X1)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p272,plain,
( is_aligned(sk1,X0)
| age(sk1,X0) != zero ),
inference(resolution,[status(thm)],[c25,c38]) ).
cnf(p564,plain,
is_aligned(sk1,sk2),
inference(resolution,[status(thm)],[p272,c41]) ).
cnf(p603,plain,
( hazard_of_mortality(sk1,sk2) = low
| ~ positional_advantage(sk1,sk2)
| has_immunity(sk1,sk2) ),
inference(resolution,[status(thm)],[p329,p564]) ).
cnf(ssp15,plain,
( spl27
| spl26
| spl25 ),
inference(avatar_split_clause,[status(thm)],[p603,sdef25,sdef26,sdef27]) ).
cnf(c31,plain,
( hazard_of_mortality(X0,X1) = mod2
| positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p338,plain,
( hazard_of_mortality(sk1,X0) = mod2
| positional_advantage(sk1,X0)
| ~ is_aligned(sk1,X0)
| has_immunity(sk1,X0) ),
inference(resolution,[status(thm)],[c31,c38]) ).
cnf(p608,plain,
( hazard_of_mortality(sk1,sk2) = mod2
| positional_advantage(sk1,sk2)
| has_immunity(sk1,sk2) ),
inference(resolution,[status(thm)],[p338,p564]) ).
cnf(ssp16,plain,
( spl29
| spl28
| spl25 ),
inference(avatar_split_clause,[status(thm)],[p608,sdef25,sdef28,sdef29]) ).
cnf(c32,plain,
( hazard_of_mortality(X0,X1) = high
| positional_advantage(X0,X1)
| is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p344,plain,
( hazard_of_mortality(sk1,X0) = high
| positional_advantage(sk1,X0)
| is_aligned(sk1,X0)
| has_immunity(sk1,X0) ),
inference(resolution,[status(thm)],[c32,c38]) ).
cnf(p619,plain,
( ~ spl2
| ~ greater(high,very_low)
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p344,p589]) ).
fof(sdef31,definition,
( spl31
<=> is_aligned(sk1,sk4) ),
introduced(definition,[new_symbols(naming,[spl31])],[avatar_definition]) ).
fof(sdef33,definition,
( spl33
<=> ~ greater(high,very_low) ),
introduced(definition,[new_symbols(naming,[spl33])],[avatar_definition]) ).
cnf(ssp17,plain,
( spl33
| spl32
| spl31
| spl30
| ~ spl2 ),
inference(avatar_split_clause,[status(thm)],[p619,sdef30,sdef31,sdef32,sdef33]) ).
cnf(p592,plain,
( ~ spl22
| smaller(hazard_of_mortality(sk1,sk4),very_low) ),
inference(demodulation,[status(thm)],[p587,p398]) ).
cnf(p624,plain,
( ~ spl22
| smaller(high,very_low)
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p344,p592]) ).
cnf(ssp18,plain,
( spl34
| spl32
| spl31
| spl30
| ~ spl22 ),
inference(avatar_split_clause,[status(thm)],[p624,sdef30,sdef31,sdef32,sdef34]) ).
cnf(p556,plain,
( ~ spl22
| smaller_or_equal(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) ),
inference(resolution,[status(thm)],[p398,c1]) ).
cnf(p594,plain,
( ~ spl22
| smaller_or_equal(hazard_of_mortality(sk1,sk4),very_low) ),
inference(demodulation,[status(thm)],[p587,p556]) ).
cnf(p626,plain,
( ~ spl22
| smaller_or_equal(high,very_low)
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p344,p594]) ).
fof(sdef35,definition,
( spl35
<=> smaller_or_equal(high,very_low) ),
introduced(definition,[new_symbols(naming,[spl35])],[avatar_definition]) ).
cnf(ssp19,plain,
( spl35
| spl32
| spl31
| spl30
| ~ spl22 ),
inference(avatar_split_clause,[status(thm)],[p626,sdef30,sdef31,sdef32,sdef35]) ).
cnf(p628,plain,
( ~ spl22
| greater(very_low,high)
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p344,p595]) ).
cnf(ssp20,plain,
( spl36
| spl32
| spl31
| spl30
| ~ spl22 ),
inference(avatar_split_clause,[status(thm)],[p628,sdef30,sdef31,sdef32,sdef36]) ).
fof(f1,axiom,
! [X,Y] :
( greater_or_equal(X,Y)
<=> ( X = Y
| greater(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_greater_or_equal) ).
fof(f1_nnf,plain,
! [X,Y] :
( ( ( X != Y
& ~ greater(X,Y) )
| greater_or_equal(X,Y) )
& ( X = Y
| greater(X,Y)
| ~ greater_or_equal(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] :
( ( ( X != Y
& ~ greater(X,Y) )
| greater_or_equal(X,Y) )
& ( X = Y
| greater(X,Y)
| ~ greater_or_equal(X,Y) ) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c4,plain,
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p578,plain,
( ~ spl22
| greater_or_equal(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk4)) ),
inference(resolution,[status(thm)],[p557,c4]) ).
cnf(p597,plain,
( ~ spl22
| greater_or_equal(very_low,hazard_of_mortality(sk1,sk4)) ),
inference(demodulation,[status(thm)],[p587,p578]) ).
cnf(p630,plain,
( ~ spl22
| greater_or_equal(very_low,high)
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p344,p597]) ).
fof(sdef37,definition,
( spl37
<=> greater_or_equal(very_low,high) ),
introduced(definition,[new_symbols(naming,[spl37])],[avatar_definition]) ).
cnf(ssp21,plain,
( spl37
| spl32
| spl31
| spl30
| ~ spl22 ),
inference(avatar_split_clause,[status(thm)],[p630,sdef30,sdef31,sdef32,sdef37]) ).
cnf(p579,plain,
( ~ spl22
| ~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)) ),
inference(resolution,[status(thm)],[p557,c8]) ).
cnf(p598,plain,
( ~ spl22
| ~ greater(hazard_of_mortality(sk1,sk4),very_low) ),
inference(demodulation,[status(thm)],[p587,p579]) ).
cnf(p632,plain,
( ~ spl22
| ~ greater(high,very_low)
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p344,p598]) ).
cnf(ssp22,plain,
( spl33
| spl32
| spl31
| spl30
| ~ spl22 ),
inference(avatar_split_clause,[status(thm)],[p632,sdef30,sdef31,sdef32,sdef33]) ).
cnf(p621,plain,
( ~ spl31
| is_aligned(sk1,sk4) ),
inference(avatar_component_clause,[status(thm)],[sdef31]) ).
cnf(p643,plain,
( ~ spl31
| hazard_of_mortality(sk1,sk4) = low
| ~ positional_advantage(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(resolution,[status(thm)],[p621,p329]) ).
cnf(ssp23,plain,
( spl39
| spl38
| spl30
| ~ spl31 ),
inference(avatar_split_clause,[status(thm)],[p643,sdef30,sdef38,sdef39]) ).
cnf(p646,plain,
( ~ spl31
| hazard_of_mortality(sk1,sk4) = mod2
| positional_advantage(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(resolution,[status(thm)],[p621,p338]) ).
cnf(ssp24,plain,
( spl40
| spl32
| spl30
| ~ spl31 ),
inference(avatar_split_clause,[status(thm)],[p646,sdef30,sdef32,sdef40]) ).
cnf(c30,plain,
( hazard_of_mortality(X0,X1) = mod1
| ~ positional_advantage(X0,X1)
| is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p334,plain,
( hazard_of_mortality(sk1,X0) = mod1
| ~ positional_advantage(sk1,X0)
| is_aligned(sk1,X0)
| has_immunity(sk1,X0) ),
inference(resolution,[status(thm)],[c30,c38]) ).
cnf(p648,plain,
( ~ spl32
| hazard_of_mortality(sk1,sk4) = mod1
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(resolution,[status(thm)],[p622,p334]) ).
cnf(ssp25,plain,
( spl41
| spl31
| spl30
| ~ spl32 ),
inference(avatar_split_clause,[status(thm)],[p648,sdef30,sdef31,sdef41]) ).
cnf(p623,plain,
( ~ spl33
| ~ greater(high,very_low) ),
inference(avatar_component_clause,[status(thm)],[sdef33]) ).
cnf(p650,plain,
( ~ spl33
| high = very_low
| smaller(high,very_low) ),
inference(resolution,[status(thm)],[p623,c10]) ).
cnf(ssp26,plain,
( spl42
| spl34
| ~ spl33 ),
inference(avatar_split_clause,[status(thm)],[p650,sdef34,sdef42]) ).
cnf(p627,plain,
( ~ spl35
| smaller_or_equal(high,very_low) ),
inference(avatar_component_clause,[status(thm)],[sdef35]) ).
cnf(p655,plain,
( ~ spl35
| high = very_low
| smaller(high,very_low) ),
inference(resolution,[status(thm)],[p627,c0]) ).
cnf(ssp27,plain,
( spl42
| spl34
| ~ spl35 ),
inference(avatar_split_clause,[status(thm)],[p655,sdef34,sdef42]) ).
cnf(p631,plain,
( ~ spl37
| greater_or_equal(very_low,high) ),
inference(avatar_component_clause,[status(thm)],[sdef37]) ).
cnf(c3,plain,
( X0 = X1
| greater(X0,X1)
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p661,plain,
( ~ spl37
| very_low = high
| greater(very_low,high) ),
inference(resolution,[status(thm)],[p631,c3]) ).
cnf(ssp28,plain,
( spl43
| spl36
| ~ spl37 ),
inference(avatar_split_clause,[status(thm)],[p661,sdef36,sdef43]) ).
cnf(p795,plain,
( ~ spl39
| low = high
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p645,p344]) ).
cnf(ssp29,plain,
( spl44
| spl32
| spl31
| spl30
| ~ spl39 ),
inference(avatar_split_clause,[status(thm)],[p795,sdef30,sdef31,sdef32,sdef44]) ).
cnf(p797,plain,
( ~ spl39
| high = low
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p344,p645]) ).
cnf(ssp30,plain,
( spl45
| spl32
| spl31
| spl30
| ~ spl39 ),
inference(avatar_split_clause,[status(thm)],[p797,sdef30,sdef31,sdef32,sdef45]) ).
cnf(p800,plain,
( ~ spl39
| ~ spl2
| low = very_low
| smaller(low,very_low) ),
inference(resolution,[status(thm)],[p789,c10]) ).
cnf(ssp31,plain,
( spl47
| spl46
| ~ spl39
| ~ spl2 ),
inference(avatar_split_clause,[status(thm)],[p800,sdef46,sdef47]) ).
cnf(p869,plain,
( ~ spl40
| mod2 = high
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p647,p344]) ).
cnf(ssp32,plain,
( spl48
| spl32
| spl31
| spl30
| ~ spl40 ),
inference(avatar_split_clause,[status(thm)],[p869,sdef30,sdef31,sdef32,sdef48]) ).
cnf(p871,plain,
( ~ spl40
| high = mod2
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p344,p647]) ).
cnf(ssp33,plain,
( spl49
| spl32
| spl31
| spl30
| ~ spl40 ),
inference(avatar_split_clause,[status(thm)],[p871,sdef30,sdef31,sdef32,sdef49]) ).
cnf(p863,plain,
( ~ spl40
| ~ spl2
| ~ greater(mod2,very_low) ),
inference(superposition,[status(thm)],[p647,p589]) ).
cnf(p873,plain,
( ~ spl40
| ~ spl2
| mod2 = very_low
| smaller(mod2,very_low) ),
inference(resolution,[status(thm)],[p863,c10]) ).
cnf(ssp34,plain,
( spl51
| spl50
| ~ spl40
| ~ spl2 ),
inference(avatar_split_clause,[status(thm)],[p873,sdef50,sdef51]) ).
cnf(p966,plain,
( ~ spl41
| mod1 = high
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p649,p344]) ).
cnf(ssp35,plain,
( spl52
| spl32
| spl31
| spl30
| ~ spl41 ),
inference(avatar_split_clause,[status(thm)],[p966,sdef30,sdef31,sdef32,sdef52]) ).
cnf(p968,plain,
( ~ spl41
| high = mod1
| positional_advantage(sk1,sk4)
| is_aligned(sk1,sk4)
| has_immunity(sk1,sk4) ),
inference(superposition,[status(thm)],[p344,p649]) ).
cnf(ssp36,plain,
( spl53
| spl32
| spl31
| spl30
| ~ spl41 ),
inference(avatar_split_clause,[status(thm)],[p968,sdef30,sdef31,sdef32,sdef53]) ).
cnf(p960,plain,
( ~ spl41
| ~ spl2
| ~ greater(mod1,very_low) ),
inference(superposition,[status(thm)],[p649,p589]) ).
cnf(p970,plain,
( ~ spl41
| ~ spl2
| mod1 = very_low
| smaller(mod1,very_low) ),
inference(resolution,[status(thm)],[p960,c10]) ).
cnf(ssp37,plain,
( spl55
| spl54
| ~ spl41
| ~ spl2 ),
inference(avatar_split_clause,[status(thm)],[p970,sdef54,sdef55]) ).
cnf(p146,plain,
( smaller(X1,X0)
| X0 = X1
| smaller(X0,X1) ),
inference(resolution,[status(thm)],[c10,c7]) ).
cnf(p507,plain,
( greater(X1,X0)
| smaller(X1,X0)
| X0 = X1 ),
inference(resolution,[status(thm)],[p146,c6]) ).
cnf(p1040,plain,
( ~ spl2
| smaller(hazard_of_mortality(sk1,sk4),very_low)
| very_low = hazard_of_mortality(sk1,sk4) ),
inference(resolution,[status(thm)],[p507,p589]) ).
fof(sdef56,definition,
( spl56
<=> very_low = hazard_of_mortality(sk1,sk4) ),
introduced(definition,[new_symbols(naming,[spl56])],[avatar_definition]) ).
fof(sdef57,definition,
( spl57
<=> smaller(hazard_of_mortality(sk1,sk4),very_low) ),
introduced(definition,[new_symbols(naming,[spl57])],[avatar_definition]) ).
cnf(ssp38,plain,
( spl57
| spl56
| ~ spl2 ),
inference(avatar_split_clause,[status(thm)],[p1040,sdef56,sdef57]) ).
cnf(p1053,plain,
( ~ spl41
| ~ spl2
| smaller(mod1,very_low)
| very_low = mod1 ),
inference(resolution,[status(thm)],[p507,p960]) ).
fof(sdef58,definition,
( spl58
<=> very_low = mod1 ),
introduced(definition,[new_symbols(naming,[spl58])],[avatar_definition]) ).
cnf(ssp39,plain,
( spl58
| spl54
| ~ spl41
| ~ spl2 ),
inference(avatar_split_clause,[status(thm)],[p1053,sdef54,sdef58]) ).
cnf(sat_ref,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[ssp0,ssp1,ssp2,ssp3,ssp4,ssp5,ssp6,ssp7,ssp8,ssp9,ssp10,ssp11,ssp12,ssp13,ssp14,ssp15,ssp16,ssp17,ssp18,ssp19,ssp20,ssp21,ssp22,ssp23,ssp24,ssp25,ssp26,ssp27,ssp28,ssp29,ssp30,ssp31,ssp32,ssp33,ssp34,ssp35,ssp36,ssp37,ssp38,ssp39,sct0,sct1,sct2,sct3,sct4,sct5,sct6,sct7,sct8,sct9,sct10,sct11,sct12,sct13,sct14,sct15,sct16,sct17,sct18,sct19,sct20,sct21,sct22,sct23,sct24,sct25,sct26,sct27,sct28,sct29,sct30,sct31,sct32,sct33,sct34,sct35,sct36,sct37,sct38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT065+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.58 % Computer : n007.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Thu Sep 24 01:16:07 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.09/0.58 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 82.28/11.33 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 82.28/11.33 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------