%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT065+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:25:31 PM UTC 2026
% Result : Theorem 0.14s 0.64s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 73
% Syntax : Number of formulae : 342 ( 40 unt; 61 def)
% Number of atoms : 937 ( 113 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 977 ( 382 ~; 423 |; 95 &)
% ( 65 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 73 ( 71 usr; 62 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 13 con; 0-2 aty)
% Number of variables : 117 ( 110 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( smaller_or_equal(X,Y)
<=> ( X = Y
| smaller(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( smaller(X,Y)
<=> greater(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
~ ( greater(Y,X)
& greater(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] :
( ( greater(Y,Z)
& greater(X,Y) )
=> greater(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] :
( greater(X,Y)
| X = Y
| smaller(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
greater(high,mod1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
greater(mod1,low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
greater(low,very_low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
greater(mod2,low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,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)],[f17]) ).
fof(f19,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)],[f1]) ).
fof(f20,plain,
( ! [X,Y] :
( ( X != Y
& ~ smaller(X,Y) )
| smaller_or_equal(X,Y) )
& ! [X,Y] :
( X = Y
| smaller(X,Y)
| ~ smaller_or_equal(X,Y) ) ),
inference(miniscoping,[status(thm)],[f19]) ).
fof(f21,plain,
! [X0,X1] :
( X0 = X1
| smaller(X0,X1)
| ~ smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f22,plain,
! [X0,X1] :
( ~ smaller(X0,X1)
| smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f29,plain,
! [X,Y] :
( ( ~ greater(Y,X)
| smaller(X,Y) )
& ( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f30,plain,
( ! [X,Y] :
( ~ greater(Y,X)
| smaller(X,Y) )
& ! [X,Y] :
( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f31,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f32,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f33,plain,
! [X,Y] :
( ~ greater(Y,X)
| ~ greater(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f34,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [X,Y,Z] :
( greater(X,Z)
| ~ greater(Y,Z)
| ~ greater(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f36,plain,
! [X,Z] :
( greater(X,Z)
| ! [Y] :
( ~ greater(Y,Z)
| ~ greater(X,Y) ) ),
inference(miniscoping,[status(thm)],[f35]) ).
fof(f37,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,plain,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f39,plain,
! [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) ) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f40,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)],[f39]) ).
fof(f41,plain,
( ! [X] :
( ? [T] :
( has_immunity(X,T)
& greater(age(X,T),eta) )
| ? [T] :
( ~ has_immunity(X,T)
& smaller_or_equal(age(X,T),eta) )
| ~ organization(X)
| has_endowment(X) )
& ! [X] :
( ( ! [T] :
( ~ has_immunity(X,T)
| ~ greater(age(X,T),eta) )
& ! [T] :
( has_immunity(X,T)
| ~ smaller_or_equal(age(X,T),eta) )
& organization(X) )
| ~ has_endowment(X) ) ),
inference(miniscoping,[status(thm)],[f40]) ).
fof(f42,plain,
( ! [X] :
( ( has_immunity(X,sK1_skl(X))
& greater(age(X,sK1_skl(X)),eta) )
| ( ~ has_immunity(X,sK0_skl(X))
& smaller_or_equal(age(X,sK0_skl(X)),eta) )
| ~ organization(X)
| has_endowment(X) )
& ! [X] :
( ( ! [T] :
( ~ has_immunity(X,T)
| ~ greater(age(X,T),eta) )
& ! [T] :
( has_immunity(X,T)
| ~ smaller_or_equal(age(X,T),eta) )
& organization(X) )
| ~ has_endowment(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(T,sK0_skl(X)),skolemize(T,sK1_skl(X))],[f41]) ).
fof(f44,plain,
! [X0,X1] :
( has_immunity(X0,X1)
| ~ smaller_or_equal(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f45,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| ~ greater(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f65,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(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f66,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) )
& ! [T] :
( hazard_of_mortality(X,T) = very_low
| ~ has_immunity(X,T) ) )
| ~ organization(X) ),
inference(miniscoping,[status(thm)],[f65]) ).
fof(f67,plain,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = very_low
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = low
| ~ positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f69,plain,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = mod1
| ~ positional_advantage(X0,X1)
| is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f70,plain,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = mod2
| positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f71,plain,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = high
| positional_advantage(X0,X1)
| is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f72,plain,
greater(high,mod1),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f73,plain,
greater(mod1,low),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f74,plain,
greater(low,very_low),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f76,plain,
greater(mod2,low),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f77,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(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f78,plain,
( ( hazard_of_mortality(sK2_skl,sK4_skl) != hazard_of_mortality(sK2_skl,sK3_skl)
| ~ greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)) )
& greater(age(sK2_skl,sK5_skl),eta)
& greater(age(sK2_skl,sK5_skl),tau)
& greater(age(sK2_skl,sK5_skl),sigma)
& smaller_or_equal(age(sK2_skl,sK4_skl),eta)
& smaller_or_equal(age(sK2_skl,sK4_skl),tau)
& smaller_or_equal(age(sK2_skl,sK4_skl),sigma)
& greater(eta,zero)
& greater(tau,zero)
& greater(sigma,zero)
& age(sK2_skl,sK3_skl) = zero
& has_endowment(sK2_skl)
& ( fragile_position(sK2_skl)
| robust_position(sK2_skl) )
& organization(sK2_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(X,sK2_skl),skolemize(T0,sK3_skl),skolemize(T1,sK4_skl),skolemize(T2,sK5_skl)],[f77]) ).
fof(f79,plain,
organization(sK2_skl),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f81,plain,
has_endowment(sK2_skl),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f82,plain,
age(sK2_skl,sK3_skl) = zero,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f83,plain,
greater(sigma,zero),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f85,plain,
greater(eta,zero),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f86,plain,
smaller_or_equal(age(sK2_skl,sK4_skl),sigma),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f87,plain,
smaller_or_equal(age(sK2_skl,sK4_skl),tau),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f88,plain,
smaller_or_equal(age(sK2_skl,sK4_skl),eta),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f89,plain,
greater(age(sK2_skl,sK5_skl),sigma),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f91,plain,
greater(age(sK2_skl,sK5_skl),eta),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f92,plain,
( hazard_of_mortality(sK2_skl,sK4_skl) != hazard_of_mortality(sK2_skl,sK3_skl)
| ~ greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f100,definition,
( sQ2_spl
<=> greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f102,plain,
( sQ2_spl
| ~ greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f100]) ).
fof(f103,definition,
( sQ3_spl
<=> hazard_of_mortality(sK2_skl,sK4_skl) = hazard_of_mortality(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f105,plain,
( sQ3_spl
| hazard_of_mortality(sK2_skl,sK4_skl) != hazard_of_mortality(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f103]) ).
fof(f106,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f92,f100,f103]) ).
fof(f109,plain,
~ greater(zero,eta),
inference(resolution,[status(thm)],[f34,f85]) ).
fof(f111,plain,
~ greater(zero,sigma),
inference(resolution,[status(thm)],[f34,f83]) ).
fof(f112,plain,
! [X0] :
( greater(X0,zero)
| ~ greater(X0,eta) ),
inference(resolution,[status(thm)],[f37,f85]) ).
fof(f116,plain,
~ greater(mod1,high),
inference(resolution,[status(thm)],[f72,f34]) ).
fof(f117,plain,
! [X0] :
( greater(X0,low)
| ~ greater(X0,mod1) ),
inference(resolution,[status(thm)],[f73,f37]) ).
fof(f119,plain,
! [X0] :
( greater(X0,very_low)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f74,f37]) ).
fof(f128,plain,
~ greater(sigma,age(sK2_skl,sK5_skl)),
inference(resolution,[status(thm)],[f89,f34]) ).
fof(f132,plain,
~ greater(eta,age(sK2_skl,sK5_skl)),
inference(resolution,[status(thm)],[f91,f34]) ).
fof(f133,plain,
greater(age(sK2_skl,sK5_skl),zero),
inference(resolution,[status(thm)],[f112,f91]) ).
fof(f136,plain,
greater(high,low),
inference(resolution,[status(thm)],[f117,f72]) ).
fof(f139,plain,
! [X0] :
( ~ has_immunity(sK2_skl,X0)
| ~ greater(age(sK2_skl,X0),eta) ),
inference(resolution,[status(thm)],[f45,f81]) ).
fof(f140,plain,
! [X0,X1] :
( X1 = X0
| ~ smaller_or_equal(X1,X0)
| greater(X0,X1) ),
inference(resolution,[status(thm)],[f31,f21]) ).
fof(f142,plain,
! [X0,X1] :
( greater(X1,X0)
| greater(X0,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f38,f31]) ).
fof(f143,plain,
! [X0,X1] :
( greater(X1,very_low)
| ~ greater(X1,X0)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f119,f37]) ).
fof(f144,plain,
! [X0] :
( ~ greater(very_low,X0)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f119,f34]) ).
fof(f147,plain,
~ greater(zero,age(sK2_skl,sK5_skl)),
inference(resolution,[status(thm)],[f133,f34]) ).
fof(f149,plain,
( ~ greater(very_low,low)
| ~ greater(very_low,low) ),
inference(resolution,[status(thm)],[f144,f119]) ).
fof(f150,definition,
( sQ4_spl
<=> greater(very_low,low) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f153,plain,
~ sQ4_spl,
inference(split_clause,[status(thm)],[f149,f150]) ).
fof(f154,plain,
! [X0] :
( ~ smaller_or_equal(age(sK2_skl,X0),eta)
| ~ has_endowment(sK2_skl)
| ~ greater(age(sK2_skl,X0),eta) ),
inference(resolution,[status(thm)],[f139,f44]) ).
fof(f155,definition,
! [X0] :
( sQ5_spl
<=> ( ~ smaller_or_equal(age(sK2_skl,X0),eta)
| ~ greater(age(sK2_skl,X0),eta) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f156,plain,
! [X0] :
( ~ sQ5_spl
| ~ smaller_or_equal(age(sK2_skl,X0),eta)
| ~ greater(age(sK2_skl,X0),eta) ),
inference(component_clause,[status(thm)],[f155]) ).
fof(f158,definition,
( sQ6_spl
<=> has_endowment(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f160,plain,
( sQ6_spl
| ~ has_endowment(sK2_skl) ),
inference(component_clause,[status(thm)],[f158]) ).
fof(f161,plain,
( ~ sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f154,f155,f158]) ).
fof(f164,plain,
! [X0,X1] :
( ~ greater(very_low,X1)
| ~ greater(X1,X0)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f143,f34]) ).
fof(f165,definition,
! [X0] :
( sQ7_spl
<=> ( ~ greater(very_low,X0)
| ~ greater(X0,low) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f169,plain,
! [X0,X1] :
( ~ greater(very_low,X1)
| ~ greater(X1,low)
| ~ greater(very_low,X0)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f164,f143]) ).
fof(f171,plain,
sQ7_spl,
inference(split_clause,[status(thm)],[f169,f165]) ).
fof(f173,plain,
( ~ sQ5_spl
| ~ smaller_or_equal(age(sK2_skl,sK5_skl),eta) ),
inference(resolution,[status(thm)],[f156,f91]) ).
fof(f175,definition,
( sQ8_spl
<=> greater(zero,eta) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f178,definition,
( sQ9_spl
<=> smaller_or_equal(age(sK2_skl,sK3_skl),eta) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f180,plain,
( sQ9_spl
| ~ smaller_or_equal(age(sK2_skl,sK3_skl),eta) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f182,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f160,f81]) ).
fof(f183,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f182]) ).
fof(f186,plain,
( age(sK2_skl,sK4_skl) = eta
| greater(eta,age(sK2_skl,sK4_skl)) ),
inference(resolution,[status(thm)],[f140,f88]) ).
fof(f187,plain,
( age(sK2_skl,sK4_skl) = tau
| greater(tau,age(sK2_skl,sK4_skl)) ),
inference(resolution,[status(thm)],[f140,f87]) ).
fof(f188,plain,
( age(sK2_skl,sK4_skl) = sigma
| greater(sigma,age(sK2_skl,sK4_skl)) ),
inference(resolution,[status(thm)],[f140,f86]) ).
fof(f193,definition,
( sQ10_spl
<=> greater(eta,age(sK2_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f196,definition,
( sQ11_spl
<=> age(sK2_skl,sK4_skl) = eta ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( ~ sQ11_spl
| age(sK2_skl,sK4_skl) = eta ),
inference(component_clause,[status(thm)],[f196]) ).
fof(f199,plain,
( sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f186,f193,f196]) ).
fof(f200,definition,
( sQ12_spl
<=> greater(tau,age(sK2_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f203,definition,
( sQ13_spl
<=> age(sK2_skl,sK4_skl) = tau ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f204,plain,
( ~ sQ13_spl
| age(sK2_skl,sK4_skl) = tau ),
inference(component_clause,[status(thm)],[f203]) ).
fof(f206,plain,
( sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f187,f200,f203]) ).
fof(f207,definition,
( sQ14_spl
<=> greater(sigma,age(sK2_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f208,plain,
( ~ sQ14_spl
| greater(sigma,age(sK2_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f207]) ).
fof(f210,definition,
( sQ15_spl
<=> age(sK2_skl,sK4_skl) = sigma ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f211,plain,
( ~ sQ15_spl
| age(sK2_skl,sK4_skl) = sigma ),
inference(component_clause,[status(thm)],[f210]) ).
fof(f213,plain,
( sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f188,f207,f210]) ).
fof(f215,plain,
( greater(age(sK2_skl,sK5_skl),eta)
| age(sK2_skl,sK5_skl) = eta ),
inference(resolution,[status(thm)],[f142,f132]) ).
fof(f217,plain,
( greater(age(sK2_skl,sK5_skl),sigma)
| age(sK2_skl,sK5_skl) = sigma ),
inference(resolution,[status(thm)],[f142,f128]) ).
fof(f225,plain,
( greater(high,mod1)
| high = mod1 ),
inference(resolution,[status(thm)],[f142,f116]) ).
fof(f226,plain,
( greater(age(sK2_skl,sK5_skl),zero)
| age(sK2_skl,sK5_skl) = zero ),
inference(resolution,[status(thm)],[f142,f147]) ).
fof(f227,plain,
( greater(sigma,zero)
| sigma = zero ),
inference(resolution,[status(thm)],[f142,f111]) ).
fof(f229,plain,
( greater(eta,zero)
| eta = zero ),
inference(resolution,[status(thm)],[f142,f109]) ).
fof(f251,definition,
( sQ18_spl
<=> age(sK2_skl,sK5_skl) = eta ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f252,plain,
( ~ sQ18_spl
| age(sK2_skl,sK5_skl) = eta ),
inference(component_clause,[status(thm)],[f251]) ).
fof(f254,definition,
( sQ19_spl
<=> greater(age(sK2_skl,sK5_skl),eta) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f257,plain,
( sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f215,f251,f254]) ).
fof(f265,definition,
( sQ22_spl
<=> age(sK2_skl,sK5_skl) = sigma ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f266,plain,
( ~ sQ22_spl
| age(sK2_skl,sK5_skl) = sigma ),
inference(component_clause,[status(thm)],[f265]) ).
fof(f268,definition,
( sQ23_spl
<=> greater(age(sK2_skl,sK5_skl),sigma) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f271,plain,
( sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f217,f265,f268]) ).
fof(f307,definition,
( sQ34_spl
<=> high = mod1 ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f308,plain,
( ~ sQ34_spl
| high = mod1 ),
inference(component_clause,[status(thm)],[f307]) ).
fof(f310,definition,
( sQ35_spl
<=> greater(high,mod1) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f313,plain,
( sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f225,f307,f310]) ).
fof(f314,definition,
( sQ36_spl
<=> age(sK2_skl,sK5_skl) = zero ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f315,plain,
( ~ sQ36_spl
| age(sK2_skl,sK5_skl) = zero ),
inference(component_clause,[status(thm)],[f314]) ).
fof(f317,definition,
( sQ37_spl
<=> greater(age(sK2_skl,sK5_skl),zero) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f320,plain,
( sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f226,f314,f317]) ).
fof(f321,definition,
( sQ38_spl
<=> sigma = zero ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f322,plain,
( ~ sQ38_spl
| sigma = zero ),
inference(component_clause,[status(thm)],[f321]) ).
fof(f323,plain,
( sQ38_spl
| sigma != zero ),
inference(component_clause,[status(thm)],[f321]) ).
fof(f324,definition,
( sQ39_spl
<=> greater(sigma,zero) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f327,plain,
( sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f227,f321,f324]) ).
fof(f335,definition,
( sQ42_spl
<=> eta = zero ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f336,plain,
( ~ sQ42_spl
| eta = zero ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f338,definition,
( sQ43_spl
<=> greater(eta,zero) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f341,plain,
( sQ43_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f229,f335,f338]) ).
fof(f380,plain,
( ~ sQ34_spl
| greater(high,high) ),
inference(backward_demodulation,[status(thm)],[f308,f72]) ).
fof(f404,definition,
( sQ44_spl
<=> tau = tau ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f407,definition,
( sQ45_spl
<=> greater(tau,tau) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f408,plain,
( ~ sQ45_spl
| greater(tau,tau) ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f409,plain,
( sQ45_spl
| ~ greater(tau,tau) ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f412,plain,
( ~ sQ45_spl
| ~ greater(tau,tau) ),
inference(resolution,[status(thm)],[f408,f34]) ).
fof(f413,plain,
( ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f412,f408]) ).
fof(f414,plain,
~ sQ45_spl,
inference(contradiction_clause,[status(thm)],[f413]) ).
fof(f417,definition,
( sQ46_spl
<=> eta = sigma ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f418,plain,
( ~ sQ46_spl
| eta = sigma ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f420,definition,
( sQ47_spl
<=> greater(eta,sigma) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f421,plain,
( ~ sQ47_spl
| greater(eta,sigma) ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f422,plain,
( sQ47_spl
| ~ greater(eta,sigma) ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f427,definition,
( sQ48_spl
<=> high = high ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f430,definition,
( sQ49_spl
<=> greater(high,high) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f431,plain,
( ~ sQ49_spl
| greater(high,high) ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f432,plain,
( sQ49_spl
| ~ greater(high,high) ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f445,definition,
( sQ50_spl
<=> low = low ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f448,definition,
( sQ51_spl
<=> greater(low,low) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( ~ sQ51_spl
| greater(low,low) ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f450,plain,
( sQ51_spl
| ~ greater(low,low) ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f472,plain,
( sQ45_spl
| greater(tau,tau)
| tau = tau ),
inference(resolution,[status(thm)],[f409,f142]) ).
fof(f473,plain,
( sQ45_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f472,f404,f407]) ).
fof(f474,plain,
( ~ sQ47_spl
| ~ sQ46_spl
| greater(sigma,sigma) ),
inference(forward_demodulation,[status(thm)],[f418,f421]) ).
fof(f476,plain,
( ~ sQ47_spl
| ~ sQ46_spl
| ~ greater(sigma,sigma) ),
inference(resolution,[status(thm)],[f474,f34]) ).
fof(f477,plain,
( ~ sQ47_spl
| ~ sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f474]) ).
fof(f478,plain,
( ~ sQ47_spl
| ~ sQ46_spl ),
inference(contradiction_clause,[status(thm)],[f477]) ).
fof(f484,plain,
( ~ sQ49_spl
| ~ greater(high,high) ),
inference(resolution,[status(thm)],[f431,f34]) ).
fof(f485,plain,
( ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f484,f431]) ).
fof(f486,plain,
~ sQ49_spl,
inference(contradiction_clause,[status(thm)],[f485]) ).
fof(f493,plain,
( ~ sQ51_spl
| ~ greater(low,low) ),
inference(resolution,[status(thm)],[f449,f34]) ).
fof(f494,plain,
( ~ sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f449]) ).
fof(f495,plain,
~ sQ51_spl,
inference(contradiction_clause,[status(thm)],[f494]) ).
fof(f505,plain,
( ~ sQ47_spl
| ~ greater(sigma,eta) ),
inference(resolution,[status(thm)],[f421,f34]) ).
fof(f510,plain,
( sQ49_spl
| greater(high,high)
| high = high ),
inference(resolution,[status(thm)],[f432,f142]) ).
fof(f511,plain,
( sQ49_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f510,f427,f430]) ).
fof(f518,plain,
( sQ51_spl
| greater(low,low)
| low = low ),
inference(resolution,[status(thm)],[f450,f142]) ).
fof(f519,plain,
( sQ51_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f518,f445,f448]) ).
fof(f524,plain,
( ~ sQ36_spl
| greater(zero,sigma) ),
inference(backward_demodulation,[status(thm)],[f315,f89]) ).
fof(f528,plain,
( ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f524,f111]) ).
fof(f529,plain,
~ sQ36_spl,
inference(contradiction_clause,[status(thm)],[f528]) ).
fof(f539,definition,
( sQ52_spl
<=> eta = tau ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f540,plain,
( ~ sQ52_spl
| eta = tau ),
inference(component_clause,[status(thm)],[f539]) ).
fof(f541,plain,
( sQ52_spl
| eta != tau ),
inference(component_clause,[status(thm)],[f539]) ).
fof(f542,definition,
( sQ53_spl
<=> greater(eta,tau) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f543,plain,
( ~ sQ53_spl
| greater(eta,tau) ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f551,plain,
( ~ sQ53_spl
| ~ sQ52_spl
| greater(tau,tau) ),
inference(forward_demodulation,[status(thm)],[f540,f543]) ).
fof(f552,plain,
( ~ sQ53_spl
| ~ sQ52_spl
| sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f551,f409]) ).
fof(f553,plain,
( ~ sQ53_spl
| ~ sQ52_spl
| sQ45_spl ),
inference(contradiction_clause,[status(thm)],[f552]) ).
fof(f557,definition,
( sQ54_spl
<=> sigma = sigma ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f560,definition,
( sQ55_spl
<=> greater(sigma,sigma) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f561,plain,
( ~ sQ55_spl
| greater(sigma,sigma) ),
inference(component_clause,[status(thm)],[f560]) ).
fof(f562,plain,
( sQ55_spl
| ~ greater(sigma,sigma) ),
inference(component_clause,[status(thm)],[f560]) ).
fof(f574,plain,
( ~ sQ55_spl
| ~ greater(sigma,sigma) ),
inference(resolution,[status(thm)],[f561,f34]) ).
fof(f575,plain,
( ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f574,f561]) ).
fof(f576,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f575]) ).
fof(f583,plain,
( sQ55_spl
| greater(sigma,sigma)
| sigma = sigma ),
inference(resolution,[status(thm)],[f562,f142]) ).
fof(f584,plain,
( sQ55_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f583,f557,f560]) ).
fof(f588,definition,
( sQ56_spl
<=> organization(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f590,plain,
( sQ56_spl
| ~ organization(sK2_skl) ),
inference(component_clause,[status(thm)],[f588]) ).
fof(f595,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f590,f79]) ).
fof(f596,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f595]) ).
fof(f606,plain,
( ~ sQ15_spl
| smaller_or_equal(sigma,tau) ),
inference(backward_demodulation,[status(thm)],[f211,f87]) ).
fof(f612,plain,
( ~ sQ15_spl
| sigma = tau
| greater(tau,sigma) ),
inference(resolution,[status(thm)],[f606,f140]) ).
fof(f613,definition,
( sQ61_spl
<=> greater(tau,sigma) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f614,plain,
( ~ sQ61_spl
| greater(tau,sigma) ),
inference(component_clause,[status(thm)],[f613]) ).
fof(f616,definition,
( sQ62_spl
<=> sigma = tau ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f617,plain,
( ~ sQ62_spl
| sigma = tau ),
inference(component_clause,[status(thm)],[f616]) ).
fof(f619,plain,
( ~ sQ15_spl
| sQ62_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f612,f613,f616,f210]) ).
fof(f629,plain,
( ~ sQ61_spl
| ~ sQ62_spl
| greater(tau,tau) ),
inference(forward_demodulation,[status(thm)],[f617,f614]) ).
fof(f630,plain,
( ~ sQ61_spl
| ~ sQ62_spl
| sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f629,f409]) ).
fof(f631,plain,
( ~ sQ61_spl
| ~ sQ62_spl
| sQ45_spl ),
inference(contradiction_clause,[status(thm)],[f630]) ).
fof(f634,plain,
( ~ sQ18_spl
| greater(eta,eta) ),
inference(forward_demodulation,[status(thm)],[f252,f91]) ).
fof(f636,plain,
( ~ sQ18_spl
| ~ greater(eta,eta) ),
inference(resolution,[status(thm)],[f634,f34]) ).
fof(f637,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f636,f634]) ).
fof(f638,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f637]) ).
fof(f651,plain,
( ~ sQ11_spl
| ~ sQ13_spl
| tau = eta ),
inference(forward_demodulation,[status(thm)],[f204,f197]) ).
fof(f652,plain,
( ~ sQ11_spl
| ~ sQ13_spl
| sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f651,f541]) ).
fof(f653,plain,
( ~ sQ11_spl
| ~ sQ13_spl
| sQ52_spl ),
inference(contradiction_clause,[status(thm)],[f652]) ).
fof(f660,plain,
( ~ sQ5_spl
| ~ smaller(age(sK2_skl,sK5_skl),eta) ),
inference(resolution,[status(thm)],[f173,f22]) ).
fof(f661,plain,
( ~ sQ14_spl
| ~ sQ11_spl
| greater(sigma,eta) ),
inference(forward_demodulation,[status(thm)],[f197,f208]) ).
fof(f662,plain,
( ~ sQ14_spl
| ~ sQ11_spl
| ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f661,f505]) ).
fof(f663,plain,
( ~ sQ14_spl
| ~ sQ11_spl
| ~ sQ47_spl ),
inference(contradiction_clause,[status(thm)],[f662]) ).
fof(f725,plain,
( ~ sQ5_spl
| ~ sQ46_spl
| ~ smaller(age(sK2_skl,sK5_skl),sigma) ),
inference(forward_demodulation,[status(thm)],[f418,f660]) ).
fof(f728,plain,
( ~ sQ5_spl
| ~ sQ46_spl
| age(sK2_skl,sK5_skl) = sigma
| ~ smaller_or_equal(age(sK2_skl,sK5_skl),sigma) ),
inference(resolution,[status(thm)],[f725,f21]) ).
fof(f730,definition,
( sQ63_spl
<=> smaller_or_equal(age(sK2_skl,sK5_skl),sigma) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f733,plain,
( ~ sQ5_spl
| ~ sQ46_spl
| sQ22_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f728,f730,f265,f417,f155]) ).
fof(f754,plain,
! [X0] :
( hazard_of_mortality(sK2_skl,X0) = mod2
| positional_advantage(sK2_skl,X0)
| ~ is_aligned(sK2_skl,X0)
| ~ organization(sK2_skl)
| ~ greater(age(sK2_skl,X0),eta) ),
inference(resolution,[status(thm)],[f139,f70]) ).
fof(f756,definition,
! [X0] :
( sQ64_spl
<=> ( hazard_of_mortality(sK2_skl,X0) = mod2
| positional_advantage(sK2_skl,X0)
| ~ is_aligned(sK2_skl,X0)
| ~ greater(age(sK2_skl,X0),eta) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f759,plain,
( ~ sQ56_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f754,f756,f588]) ).
fof(f761,plain,
( ~ sQ22_spl
| greater(sigma,eta) ),
inference(backward_demodulation,[status(thm)],[f266,f91]) ).
fof(f768,plain,
( ~ sQ22_spl
| ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f761,f505]) ).
fof(f769,plain,
( ~ sQ22_spl
| ~ sQ47_spl ),
inference(contradiction_clause,[status(thm)],[f768]) ).
fof(f921,definition,
( sQ70_spl
<=> smaller_or_equal(zero,sigma) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f923,plain,
( sQ70_spl
| ~ smaller_or_equal(zero,sigma) ),
inference(component_clause,[status(thm)],[f921]) ).
fof(f924,definition,
( sQ71_spl
<=> has_immunity(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f925,plain,
( ~ sQ71_spl
| has_immunity(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f924]) ).
fof(f930,plain,
( ~ sQ71_spl
| hazard_of_mortality(sK2_skl,sK3_skl) = very_low
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f925,f67]) ).
fof(f931,definition,
( sQ72_spl
<=> hazard_of_mortality(sK2_skl,sK3_skl) = very_low ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f932,plain,
( ~ sQ72_spl
| hazard_of_mortality(sK2_skl,sK3_skl) = very_low ),
inference(component_clause,[status(thm)],[f931]) ).
fof(f934,plain,
( ~ sQ71_spl
| sQ72_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f930,f588,f931,f924]) ).
fof(f935,plain,
( sQ70_spl
| ~ smaller(zero,sigma) ),
inference(resolution,[status(thm)],[f923,f22]) ).
fof(f947,plain,
( sQ70_spl
| ~ greater(sigma,zero) ),
inference(resolution,[status(thm)],[f935,f32]) ).
fof(f950,plain,
( sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f947,f83]) ).
fof(f951,plain,
sQ70_spl,
inference(contradiction_clause,[status(thm)],[f950]) ).
fof(f961,plain,
( ~ sQ38_spl
| greater(sigma,sigma) ),
inference(backward_demodulation,[status(thm)],[f322,f83]) ).
fof(f965,plain,
( ~ sQ38_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f961,f560,f321]) ).
fof(f970,plain,
( sQ47_spl
| greater(sigma,eta)
| sigma = eta ),
inference(resolution,[status(thm)],[f422,f142]) ).
fof(f971,definition,
( sQ73_spl
<=> greater(sigma,eta) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f972,plain,
( ~ sQ73_spl
| greater(sigma,eta) ),
inference(component_clause,[status(thm)],[f971]) ).
fof(f974,plain,
( sQ47_spl
| sQ73_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f970,f417,f971,f420]) ).
fof(f994,plain,
( ~ sQ73_spl
| ~ greater(eta,sigma) ),
inference(resolution,[status(thm)],[f972,f34]) ).
fof(f995,plain,
( ~ sQ73_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f994,f420,f971]) ).
fof(f1004,plain,
( has_immunity(sK2_skl,sK4_skl)
| ~ has_endowment(sK2_skl) ),
inference(resolution,[status(thm)],[f44,f88]) ).
fof(f1006,definition,
( sQ74_spl
<=> has_immunity(sK2_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1007,plain,
( ~ sQ74_spl
| has_immunity(sK2_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f1006]) ).
fof(f1009,plain,
( sQ74_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1004,f158,f1006]) ).
fof(f1010,plain,
( ~ sQ74_spl
| ~ greater(age(sK2_skl,sK4_skl),eta)
| ~ has_endowment(sK2_skl) ),
inference(resolution,[status(thm)],[f1007,f45]) ).
fof(f1011,plain,
( ~ sQ74_spl
| hazard_of_mortality(sK2_skl,sK4_skl) = very_low
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f1007,f67]) ).
fof(f1012,definition,
( sQ75_spl
<=> greater(age(sK2_skl,sK4_skl),eta) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1015,plain,
( ~ sQ74_spl
| ~ sQ75_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1010,f158,f1012,f1006]) ).
fof(f1016,definition,
( sQ76_spl
<=> hazard_of_mortality(sK2_skl,sK4_skl) = very_low ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1017,plain,
( ~ sQ76_spl
| hazard_of_mortality(sK2_skl,sK4_skl) = very_low ),
inference(component_clause,[status(thm)],[f1016]) ).
fof(f1019,plain,
( ~ sQ74_spl
| sQ76_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f1011,f588,f1016,f1006]) ).
fof(f1020,plain,
( sQ3_spl
| ~ sQ72_spl
| hazard_of_mortality(sK2_skl,sK4_skl) != very_low ),
inference(backward_demodulation,[status(thm)],[f932,f105]) ).
fof(f1021,plain,
( has_immunity(sK2_skl,sK3_skl)
| ~ smaller_or_equal(zero,eta)
| ~ has_endowment(sK2_skl) ),
inference(paramodulation,[status(thm)],[f82,f44]) ).
fof(f1022,definition,
( sQ77_spl
<=> smaller_or_equal(zero,eta) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1023,plain,
( ~ sQ77_spl
| smaller_or_equal(zero,eta) ),
inference(component_clause,[status(thm)],[f1022]) ).
fof(f1024,plain,
( sQ77_spl
| ~ smaller_or_equal(zero,eta) ),
inference(component_clause,[status(thm)],[f1022]) ).
fof(f1025,plain,
( sQ71_spl
| ~ sQ77_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1021,f158,f1022,f924]) ).
fof(f1026,plain,
( sQ77_spl
| ~ smaller(zero,eta) ),
inference(resolution,[status(thm)],[f1024,f22]) ).
fof(f1028,plain,
( sQ77_spl
| ~ greater(eta,zero) ),
inference(resolution,[status(thm)],[f1026,f32]) ).
fof(f1031,plain,
( sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1028,f85]) ).
fof(f1032,plain,
sQ77_spl,
inference(contradiction_clause,[status(thm)],[f1031]) ).
fof(f1033,plain,
( sQ9_spl
| ~ smaller_or_equal(zero,eta) ),
inference(forward_demodulation,[status(thm)],[f82,f180]) ).
fof(f1043,plain,
( ~ sQ42_spl
| ~ sQ46_spl
| sigma = zero ),
inference(forward_demodulation,[status(thm)],[f418,f336]) ).
fof(f1044,plain,
( ~ sQ42_spl
| ~ sQ46_spl
| sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1043,f323]) ).
fof(f1045,plain,
( ~ sQ42_spl
| ~ sQ46_spl
| sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f1044]) ).
fof(f1047,plain,
( ~ sQ77_spl
| sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1023,f1033]) ).
fof(f1048,plain,
( ~ sQ77_spl
| sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f1047]) ).
fof(f1062,plain,
( ~ sQ76_spl
| sQ3_spl
| ~ sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1017,f1020]) ).
fof(f1063,plain,
( ~ sQ76_spl
| sQ3_spl
| ~ sQ72_spl ),
inference(contradiction_clause,[status(thm)],[f1062]) ).
fof(f1101,plain,
( ~ has_immunity(sK2_skl,sK3_skl)
| ~ greater(zero,eta)
| ~ has_endowment(sK2_skl) ),
inference(paramodulation,[status(thm)],[f82,f45]) ).
fof(f1102,plain,
( ~ sQ71_spl
| ~ sQ8_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1101,f158,f175,f924]) ).
fof(f1108,definition,
( sQ79_spl
<=> very_low = very_low ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1111,definition,
( sQ80_spl
<=> greater(very_low,very_low) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1112,plain,
( ~ sQ80_spl
| greater(very_low,very_low) ),
inference(component_clause,[status(thm)],[f1111]) ).
fof(f1113,plain,
( sQ80_spl
| ~ greater(very_low,very_low) ),
inference(component_clause,[status(thm)],[f1111]) ).
fof(f1121,plain,
( ~ has_immunity(sK2_skl,sK5_skl)
| ~ has_endowment(sK2_skl) ),
inference(resolution,[status(thm)],[f91,f45]) ).
fof(f1124,definition,
( sQ81_spl
<=> has_immunity(sK2_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1126,plain,
( sQ81_spl
| ~ has_immunity(sK2_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f1124]) ).
fof(f1127,plain,
( ~ sQ81_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1121,f158,f1124]) ).
fof(f1138,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ greater(hazard_of_mortality(sK2_skl,sK5_skl),very_low) ),
inference(forward_demodulation,[status(thm)],[f1017,f102]) ).
fof(f1158,plain,
( sQ81_spl
| ~ smaller_or_equal(age(sK2_skl,sK5_skl),eta)
| ~ has_endowment(sK2_skl) ),
inference(resolution,[status(thm)],[f1126,f44]) ).
fof(f1159,plain,
( sQ81_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = mod2
| positional_advantage(sK2_skl,sK5_skl)
| ~ is_aligned(sK2_skl,sK5_skl)
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f1126,f70]) ).
fof(f1160,definition,
( sQ84_spl
<=> smaller_or_equal(age(sK2_skl,sK5_skl),eta) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1163,plain,
( sQ81_spl
| ~ sQ84_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1158,f158,f1160,f1124]) ).
fof(f1164,definition,
( sQ85_spl
<=> is_aligned(sK2_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1166,plain,
( sQ85_spl
| ~ is_aligned(sK2_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f1164]) ).
fof(f1167,definition,
( sQ86_spl
<=> positional_advantage(sK2_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1168,plain,
( ~ sQ86_spl
| positional_advantage(sK2_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f1167]) ).
fof(f1170,definition,
( sQ87_spl
<=> hazard_of_mortality(sK2_skl,sK5_skl) = mod2 ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1171,plain,
( ~ sQ87_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = mod2 ),
inference(component_clause,[status(thm)],[f1170]) ).
fof(f1173,plain,
( sQ81_spl
| sQ87_spl
| sQ86_spl
| ~ sQ85_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f1159,f588,f1164,f1167,f1170,f1124]) ).
fof(f1180,plain,
( ~ sQ80_spl
| ~ greater(very_low,very_low) ),
inference(resolution,[status(thm)],[f1112,f34]) ).
fof(f1181,plain,
( ~ sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1180,f1112]) ).
fof(f1182,plain,
~ sQ80_spl,
inference(contradiction_clause,[status(thm)],[f1181]) ).
fof(f1184,plain,
( sQ80_spl
| greater(very_low,very_low)
| very_low = very_low ),
inference(resolution,[status(thm)],[f1113,f142]) ).
fof(f1185,plain,
( sQ80_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1184,f1108,f1111]) ).
fof(f1198,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ87_spl
| ~ greater(mod2,very_low) ),
inference(forward_demodulation,[status(thm)],[f1171,f1138]) ).
fof(f1199,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ87_spl
| ~ greater(mod2,low) ),
inference(resolution,[status(thm)],[f1198,f119]) ).
fof(f1201,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1199,f76]) ).
fof(f1202,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ87_spl ),
inference(contradiction_clause,[status(thm)],[f1201]) ).
fof(f1204,plain,
( sQ85_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = high
| positional_advantage(sK2_skl,sK5_skl)
| has_immunity(sK2_skl,sK5_skl)
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f1166,f71]) ).
fof(f1205,plain,
( sQ85_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = mod1
| ~ positional_advantage(sK2_skl,sK5_skl)
| has_immunity(sK2_skl,sK5_skl)
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f1166,f69]) ).
fof(f1210,definition,
( sQ88_spl
<=> hazard_of_mortality(sK2_skl,sK5_skl) = high ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1211,plain,
( ~ sQ88_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = high ),
inference(component_clause,[status(thm)],[f1210]) ).
fof(f1213,plain,
( sQ85_spl
| sQ88_spl
| sQ86_spl
| sQ81_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f1204,f588,f1124,f1167,f1210,f1164]) ).
fof(f1214,definition,
( sQ89_spl
<=> hazard_of_mortality(sK2_skl,sK5_skl) = mod1 ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1215,plain,
( ~ sQ89_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = mod1 ),
inference(component_clause,[status(thm)],[f1214]) ).
fof(f1217,plain,
( sQ85_spl
| sQ89_spl
| ~ sQ86_spl
| sQ81_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f1205,f588,f1124,f1167,f1214,f1164]) ).
fof(f1226,plain,
( ~ sQ86_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = low
| ~ is_aligned(sK2_skl,sK5_skl)
| has_immunity(sK2_skl,sK5_skl)
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f1168,f68]) ).
fof(f1227,definition,
( sQ92_spl
<=> hazard_of_mortality(sK2_skl,sK5_skl) = low ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1228,plain,
( ~ sQ92_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = low ),
inference(component_clause,[status(thm)],[f1227]) ).
fof(f1230,plain,
( ~ sQ86_spl
| sQ92_spl
| ~ sQ85_spl
| sQ81_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f1226,f588,f1124,f1164,f1227,f1167]) ).
fof(f1235,plain,
( ~ sQ34_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f380,f430,f307]) ).
fof(f1244,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ92_spl
| ~ greater(low,very_low) ),
inference(backward_demodulation,[status(thm)],[f1228,f1138]) ).
fof(f1245,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1244,f74]) ).
fof(f1246,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ92_spl ),
inference(contradiction_clause,[status(thm)],[f1245]) ).
fof(f1263,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ88_spl
| ~ greater(high,very_low) ),
inference(forward_demodulation,[status(thm)],[f1211,f1138]) ).
fof(f1264,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ88_spl
| ~ greater(high,low) ),
inference(resolution,[status(thm)],[f1263,f119]) ).
fof(f1266,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1264,f136]) ).
fof(f1267,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ88_spl ),
inference(contradiction_clause,[status(thm)],[f1266]) ).
fof(f1278,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ89_spl
| ~ greater(mod1,very_low) ),
inference(backward_demodulation,[status(thm)],[f1215,f1138]) ).
fof(f1279,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ89_spl
| ~ greater(mod1,low) ),
inference(resolution,[status(thm)],[f1278,f119]) ).
fof(f1281,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1279,f73]) ).
fof(f1282,plain,
( sQ2_spl
| ~ sQ76_spl
| ~ sQ89_spl ),
inference(contradiction_clause,[status(thm)],[f1281]) ).
fof(f1283,plain,
$false,
inference(sat_refutation,[status(thm)],[f106,f153,f161,f171,f183,f199,f206,f213,f257,f271,f313,f320,f327,f341,f414,f473,f478,f486,f495,f511,f519,f529,f553,f576,f584,f596,f619,f631,f638,f653,f663,f733,f759,f769,f934,f951,f965,f974,f995,f1009,f1015,f1019,f1025,f1032,f1045,f1048,f1063,f1102,f1127,f1163,f1173,f1182,f1185,f1202,f1213,f1217,f1230,f1235,f1246,f1267,f1282]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT065+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n014.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Mon Sep 21 01:24:35 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.09/0.58 % Drodi V4.1.1
% 0.14/0.64 % Refutation found
% 0.14/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.66 % Elapsed time: 0.095540 seconds
% 0.14/0.66 % CPU time: 0.434143 seconds
% 0.14/0.66 % Total memory used: 108.289 MB
% 0.14/0.66 % Net memory used: 107.747 MB
%------------------------------------------------------------------------------