%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT064+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 : 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 : Thu Sep 24 01:25:31 PM UTC 2026
% Result : Theorem 3.84s 0.94s
% Output : CNFRefutation 3.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 141
% Syntax : Number of formulae : 662 ( 71 unt; 123 def)
% Number of atoms : 1831 ( 254 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 2016 ( 847 ~; 922 |; 99 &)
% ( 132 <=>; 15 =>; 0 <=; 1 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 135 ( 133 usr; 124 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 13 con; 0-2 aty)
% Number of variables : 342 ( 334 !; 8 ?)
% 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(f8,axiom,
! [X,T] :
( ( ~ has_endowment(X)
& organization(X) )
=> ~ has_immunity(X,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,T0,T] :
( dissimilar(X,T0,T)
<=> ( ~ ( is_aligned(X,T0)
<=> is_aligned(X,T) )
& organization(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,T] :
( ( age(X,T) = zero
& organization(X) )
=> is_aligned(X,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,T0,T] :
( ( age(X,T0) = zero
& organization(X) )
=> ( greater(age(X,T),sigma)
<=> dissimilar(X,T0,T) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] :
( robust_position(X)
<=> ! [T] :
( ( greater(age(X,T),tau)
=> positional_advantage(X,T) )
& ( smaller_or_equal(age(X,T),tau)
=> ~ positional_advantage(X,T) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,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(f14,axiom,
greater(high,mod1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
greater(mod1,low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
greater(low,very_low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
greater(high,mod2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
greater(mod2,low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
greater(mod2,mod1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,conjecture,
! [X,T0,T1,T2,T3] :
( ( greater(age(X,T3),sigma)
& smaller_or_equal(age(X,T2),sigma)
& greater(age(X,T2),tau)
& smaller_or_equal(age(X,T1),tau)
& greater(sigma,tau)
& greater(tau,zero)
& greater(sigma,zero)
& age(X,T0) = zero
& ~ has_endowment(X)
& robust_position(X)
& organization(X) )
=> ( hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)
& smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))
& smaller(hazard_of_mortality(X,T2),hazard_of_mortality(X,T3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
~ ! [X,T0,T1,T2,T3] :
( ( greater(age(X,T3),sigma)
& smaller_or_equal(age(X,T2),sigma)
& greater(age(X,T2),tau)
& smaller_or_equal(age(X,T1),tau)
& greater(sigma,tau)
& greater(tau,zero)
& greater(sigma,zero)
& age(X,T0) = zero
& ~ has_endowment(X)
& robust_position(X)
& organization(X) )
=> ( hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)
& smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))
& smaller(hazard_of_mortality(X,T2),hazard_of_mortality(X,T3)) ) ),
inference(negated_conjecture,[status(cth)],[f20]) ).
fof(f22,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(f23,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)],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( X0 = X1
| smaller(X0,X1)
| ~ smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f25,plain,
! [X0,X1] :
( ~ smaller(X0,X1)
| smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f26,plain,
! [X0,X1] :
( X0 != X1
| smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f32,plain,
! [X,Y] :
( ( ~ greater(Y,X)
| smaller(X,Y) )
& ( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f33,plain,
( ! [X,Y] :
( ~ greater(Y,X)
| smaller(X,Y) )
& ! [X,Y] :
( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(miniscoping,[status(thm)],[f32]) ).
fof(f34,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f36,plain,
! [X,Y] :
( ~ greater(Y,X)
| ~ greater(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f37,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,plain,
! [X,Y,Z] :
( greater(X,Z)
| ~ greater(Y,Z)
| ~ greater(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f39,plain,
! [X,Z] :
( greater(X,Z)
| ! [Y] :
( ~ greater(Y,Z)
| ~ greater(X,Y) ) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f40,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f41,plain,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f53,plain,
! [X,T] :
( ~ has_immunity(X,T)
| has_endowment(X)
| ~ organization(X) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f54,plain,
! [X] :
( ! [T] : ~ has_immunity(X,T)
| has_endowment(X)
| ~ organization(X) ),
inference(miniscoping,[status(thm)],[f53]) ).
fof(f55,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| has_endowment(X0)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
! [X,T0,T] :
( dissimilar(X,T0,T)
<=> ( ( is_aligned(X,T0)
<~> is_aligned(X,T) )
& organization(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f57,plain,
! [X,T0,T] :
( ( ( ( ~ is_aligned(X,T)
| is_aligned(X,T0) )
& ( is_aligned(X,T)
| ~ is_aligned(X,T0) ) )
| ~ organization(X)
| dissimilar(X,T0,T) )
& ( ( ( ~ is_aligned(X,T)
| ~ is_aligned(X,T0) )
& ( is_aligned(X,T)
| is_aligned(X,T0) )
& organization(X) )
| ~ dissimilar(X,T0,T) ) ),
inference(NNF_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
( ! [X,T0,T] :
( ( ( ~ is_aligned(X,T)
| is_aligned(X,T0) )
& ( is_aligned(X,T)
| ~ is_aligned(X,T0) ) )
| ~ organization(X)
| dissimilar(X,T0,T) )
& ! [X,T0,T] :
( ( ( ~ is_aligned(X,T)
| ~ is_aligned(X,T0) )
& ( is_aligned(X,T)
| is_aligned(X,T0) )
& organization(X) )
| ~ dissimilar(X,T0,T) ) ),
inference(miniscoping,[status(thm)],[f57]) ).
fof(f59,plain,
! [X0,X1,X2] :
( organization(X0)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( is_aligned(X0,X2)
| is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f61,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f62,plain,
! [X0,X1,X2] :
( is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ organization(X0)
| dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| is_aligned(X0,X1)
| ~ organization(X0)
| dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f64,plain,
! [X,T] :
( is_aligned(X,T)
| age(X,T) != zero
| ~ organization(X) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f65,plain,
! [X0,X1] :
( is_aligned(X0,X1)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [X,T0,T] :
( ( greater(age(X,T),sigma)
<=> dissimilar(X,T0,T) )
| age(X,T0) != zero
| ~ organization(X) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f67,plain,
! [X,T0,T] :
( ( ( ~ dissimilar(X,T0,T)
| greater(age(X,T),sigma) )
& ( dissimilar(X,T0,T)
| ~ greater(age(X,T),sigma) ) )
| age(X,T0) != zero
| ~ organization(X) ),
inference(NNF_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [X,T0] :
( ( ! [T] :
( ~ dissimilar(X,T0,T)
| greater(age(X,T),sigma) )
& ! [T] :
( dissimilar(X,T0,T)
| ~ greater(age(X,T),sigma) ) )
| age(X,T0) != zero
| ~ organization(X) ),
inference(miniscoping,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0,X1,X2] :
( dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ~ dissimilar(X0,X1,X2)
| greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f71,plain,
! [X] :
( robust_position(X)
<=> ! [T] :
( ( positional_advantage(X,T)
| ~ greater(age(X,T),tau) )
& ( ~ positional_advantage(X,T)
| ~ smaller_or_equal(age(X,T),tau) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f72,plain,
! [X] :
( ( ? [T] :
( ( ~ positional_advantage(X,T)
& greater(age(X,T),tau) )
| ( positional_advantage(X,T)
& smaller_or_equal(age(X,T),tau) ) )
| robust_position(X) )
& ( ! [T] :
( ( positional_advantage(X,T)
| ~ greater(age(X,T),tau) )
& ( ~ positional_advantage(X,T)
| ~ smaller_or_equal(age(X,T),tau) ) )
| ~ robust_position(X) ) ),
inference(NNF_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
( ! [X] :
( ? [T] :
( ~ positional_advantage(X,T)
& greater(age(X,T),tau) )
| ? [T] :
( positional_advantage(X,T)
& smaller_or_equal(age(X,T),tau) )
| robust_position(X) )
& ! [X] :
( ( ! [T] :
( positional_advantage(X,T)
| ~ greater(age(X,T),tau) )
& ! [T] :
( ~ positional_advantage(X,T)
| ~ smaller_or_equal(age(X,T),tau) ) )
| ~ robust_position(X) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f74,plain,
( ! [X] :
( ( ~ positional_advantage(X,sK3_skl(X))
& greater(age(X,sK3_skl(X)),tau) )
| ( positional_advantage(X,sK2_skl(X))
& smaller_or_equal(age(X,sK2_skl(X)),tau) )
| robust_position(X) )
& ! [X] :
( ( ! [T] :
( positional_advantage(X,T)
| ~ greater(age(X,T),tau) )
& ! [T] :
( ~ positional_advantage(X,T)
| ~ smaller_or_equal(age(X,T),tau) ) )
| ~ robust_position(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(T,sK2_skl(X)),skolemize(T,sK3_skl(X))],[f73]) ).
fof(f75,plain,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| ~ smaller_or_equal(age(X0,X1),tau)
| ~ robust_position(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
! [X0,X1] :
( positional_advantage(X0,X1)
| ~ greater(age(X0,X1),tau)
| ~ robust_position(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f81,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)],[f13]) ).
fof(f82,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)],[f81]) ).
fof(f83,plain,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = very_low
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f84,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)],[f82]) ).
fof(f85,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)],[f82]) ).
fof(f86,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)],[f82]) ).
fof(f87,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)],[f82]) ).
fof(f88,plain,
greater(high,mod1),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f89,plain,
greater(mod1,low),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f90,plain,
greater(low,very_low),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f91,plain,
greater(high,mod2),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f92,plain,
greater(mod2,low),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f93,plain,
greater(mod2,mod1),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f94,plain,
? [X,T0,T1,T2,T3] :
( ( hazard_of_mortality(X,T1) != hazard_of_mortality(X,T0)
| ~ smaller(hazard_of_mortality(X,T3),hazard_of_mortality(X,T1))
| ~ smaller(hazard_of_mortality(X,T2),hazard_of_mortality(X,T3)) )
& greater(age(X,T3),sigma)
& smaller_or_equal(age(X,T2),sigma)
& greater(age(X,T2),tau)
& smaller_or_equal(age(X,T1),tau)
& greater(sigma,tau)
& greater(tau,zero)
& greater(sigma,zero)
& age(X,T0) = zero
& ~ has_endowment(X)
& robust_position(X)
& organization(X) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f95,plain,
( ( hazard_of_mortality(sK4_skl,sK6_skl) != hazard_of_mortality(sK4_skl,sK5_skl)
| ~ smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl))
| ~ smaller(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) )
& greater(age(sK4_skl,sK8_skl),sigma)
& smaller_or_equal(age(sK4_skl,sK7_skl),sigma)
& greater(age(sK4_skl,sK7_skl),tau)
& smaller_or_equal(age(sK4_skl,sK6_skl),tau)
& greater(sigma,tau)
& greater(tau,zero)
& greater(sigma,zero)
& age(sK4_skl,sK5_skl) = zero
& ~ has_endowment(sK4_skl)
& robust_position(sK4_skl)
& organization(sK4_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl]),skolemize(X,sK4_skl),skolemize(T0,sK5_skl),skolemize(T1,sK6_skl),skolemize(T2,sK7_skl),skolemize(T3,sK8_skl)],[f94]) ).
fof(f96,plain,
organization(sK4_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
robust_position(sK4_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f98,plain,
~ has_endowment(sK4_skl),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f99,plain,
age(sK4_skl,sK5_skl) = zero,
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f100,plain,
greater(sigma,zero),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f101,plain,
greater(tau,zero),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f102,plain,
greater(sigma,tau),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f103,plain,
smaller_or_equal(age(sK4_skl,sK6_skl),tau),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f104,plain,
greater(age(sK4_skl,sK7_skl),tau),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f105,plain,
smaller_or_equal(age(sK4_skl,sK7_skl),sigma),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f106,plain,
greater(age(sK4_skl,sK8_skl),sigma),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f107,plain,
( hazard_of_mortality(sK4_skl,sK6_skl) != hazard_of_mortality(sK4_skl,sK5_skl)
| ~ smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl))
| ~ smaller(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f108,definition,
( sQ0_spl
<=> smaller(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f109,plain,
( ~ sQ0_spl
| smaller(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f108]) ).
fof(f110,plain,
( sQ0_spl
| ~ smaller(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f108]) ).
fof(f111,definition,
( sQ1_spl
<=> smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f113,plain,
( sQ1_spl
| ~ smaller(hazard_of_mortality(sK4_skl,sK8_skl),hazard_of_mortality(sK4_skl,sK6_skl)) ),
inference(component_clause,[status(thm)],[f111]) ).
fof(f114,definition,
( sQ2_spl
<=> hazard_of_mortality(sK4_skl,sK6_skl) = hazard_of_mortality(sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f115,plain,
( ~ sQ2_spl
| hazard_of_mortality(sK4_skl,sK6_skl) = hazard_of_mortality(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f114]) ).
fof(f116,plain,
( sQ2_spl
| hazard_of_mortality(sK4_skl,sK6_skl) != hazard_of_mortality(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f114]) ).
fof(f117,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f107,f108,f111,f114]) ).
fof(f118,plain,
! [X0] : smaller_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f26]) ).
fof(f121,plain,
~ greater(zero,tau),
inference(resolution,[status(thm)],[f37,f101]) ).
fof(f122,plain,
~ greater(tau,sigma),
inference(resolution,[status(thm)],[f37,f102]) ).
fof(f123,plain,
~ greater(zero,sigma),
inference(resolution,[status(thm)],[f37,f100]) ).
fof(f124,plain,
! [X0,X1] :
( greater(X1,X0)
| X0 = X1
| ~ smaller_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f24,f34]) ).
fof(f125,plain,
! [X0,X1,X2] :
( ~ greater(X2,X0)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(resolution,[status(thm)],[f40,f37]) ).
fof(f126,plain,
~ greater(mod1,high),
inference(resolution,[status(thm)],[f88,f37]) ).
fof(f127,plain,
~ greater(low,mod1),
inference(resolution,[status(thm)],[f89,f37]) ).
fof(f129,plain,
~ greater(mod2,high),
inference(resolution,[status(thm)],[f91,f37]) ).
fof(f130,plain,
~ greater(low,mod2),
inference(resolution,[status(thm)],[f92,f37]) ).
fof(f131,plain,
~ greater(mod1,mod2),
inference(resolution,[status(thm)],[f93,f37]) ).
fof(f133,plain,
! [X0] :
( ~ greater(X0,sigma)
| ~ greater(tau,X0) ),
inference(resolution,[status(thm)],[f122,f40]) ).
fof(f136,plain,
! [X0] :
( ~ greater(X0,mod1)
| ~ greater(low,X0) ),
inference(resolution,[status(thm)],[f127,f40]) ).
fof(f139,plain,
! [X0,X1] :
( greater(X1,X0)
| greater(X0,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f41,f34]) ).
fof(f140,plain,
~ greater(tau,age(sK4_skl,sK7_skl)),
inference(resolution,[status(thm)],[f104,f37]) ).
fof(f141,plain,
~ greater(sigma,age(sK4_skl,sK8_skl)),
inference(resolution,[status(thm)],[f106,f37]) ).
fof(f144,plain,
! [X0] :
( ~ greater(X0,mod2)
| ~ greater(low,X0) ),
inference(resolution,[status(thm)],[f130,f40]) ).
fof(f146,plain,
( greater(sigma,age(sK4_skl,sK7_skl))
| age(sK4_skl,sK7_skl) = sigma ),
inference(resolution,[status(thm)],[f124,f105]) ).
fof(f147,plain,
( greater(tau,age(sK4_skl,sK6_skl))
| age(sK4_skl,sK6_skl) = tau ),
inference(resolution,[status(thm)],[f124,f103]) ).
fof(f150,definition,
( sQ3_spl
<=> age(sK4_skl,sK7_skl) = sigma ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f151,plain,
( ~ sQ3_spl
| age(sK4_skl,sK7_skl) = sigma ),
inference(component_clause,[status(thm)],[f150]) ).
fof(f153,definition,
( sQ4_spl
<=> greater(sigma,age(sK4_skl,sK7_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f154,plain,
( ~ sQ4_spl
| greater(sigma,age(sK4_skl,sK7_skl)) ),
inference(component_clause,[status(thm)],[f153]) ).
fof(f156,plain,
( sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f146,f150,f153]) ).
fof(f157,definition,
( sQ5_spl
<=> age(sK4_skl,sK6_skl) = tau ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f158,plain,
( ~ sQ5_spl
| age(sK4_skl,sK6_skl) = tau ),
inference(component_clause,[status(thm)],[f157]) ).
fof(f160,definition,
( sQ6_spl
<=> greater(tau,age(sK4_skl,sK6_skl)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f161,plain,
( ~ sQ6_spl
| greater(tau,age(sK4_skl,sK6_skl)) ),
inference(component_clause,[status(thm)],[f160]) ).
fof(f163,plain,
( sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f147,f157,f160]) ).
fof(f172,plain,
~ greater(very_low,mod1),
inference(resolution,[status(thm)],[f136,f90]) ).
fof(f175,plain,
( greater(high,mod2)
| high = mod2 ),
inference(resolution,[status(thm)],[f139,f129]) ).
fof(f176,plain,
( greater(mod1,very_low)
| mod1 = very_low ),
inference(resolution,[status(thm)],[f139,f172]) ).
fof(f179,plain,
( greater(mod1,low)
| mod1 = low ),
inference(resolution,[status(thm)],[f139,f127]) ).
fof(f182,plain,
( greater(high,mod1)
| high = mod1 ),
inference(resolution,[status(thm)],[f139,f126]) ).
fof(f183,plain,
( greater(sigma,tau)
| sigma = tau ),
inference(resolution,[status(thm)],[f139,f122]) ).
fof(f186,plain,
( greater(tau,zero)
| tau = zero ),
inference(resolution,[status(thm)],[f139,f121]) ).
fof(f191,definition,
( sQ7_spl
<=> high = mod2 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( ~ sQ7_spl
| high = mod2 ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f193,plain,
( sQ7_spl
| high != mod2 ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,definition,
( sQ8_spl
<=> greater(high,mod2) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f175,f191,f194]) ).
fof(f198,definition,
( sQ9_spl
<=> mod1 = very_low ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( ~ sQ9_spl
| mod1 = very_low ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,definition,
( sQ10_spl
<=> greater(mod1,very_low) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( ~ sQ10_spl
| greater(mod1,very_low) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f176,f198,f201]) ).
fof(f219,definition,
( sQ15_spl
<=> mod1 = low ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f220,plain,
( ~ sQ15_spl
| mod1 = low ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f221,plain,
( sQ15_spl
| mod1 != low ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f222,definition,
( sQ16_spl
<=> greater(mod1,low) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f225,plain,
( sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f179,f219,f222]) ).
fof(f233,definition,
( sQ19_spl
<=> high = mod1 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( ~ sQ19_spl
| high = mod1 ),
inference(component_clause,[status(thm)],[f233]) ).
fof(f236,definition,
( sQ20_spl
<=> greater(high,mod1) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f239,plain,
( sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f182,f233,f236]) ).
fof(f240,definition,
( sQ21_spl
<=> sigma = tau ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f241,plain,
( ~ sQ21_spl
| sigma = tau ),
inference(component_clause,[status(thm)],[f240]) ).
fof(f243,definition,
( sQ22_spl
<=> greater(sigma,tau) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f246,plain,
( sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f183,f240,f243]) ).
fof(f254,definition,
( sQ25_spl
<=> tau = zero ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f255,plain,
( ~ sQ25_spl
| tau = zero ),
inference(component_clause,[status(thm)],[f254]) ).
fof(f256,plain,
( sQ25_spl
| tau != zero ),
inference(component_clause,[status(thm)],[f254]) ).
fof(f257,definition,
( sQ26_spl
<=> greater(tau,zero) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f260,plain,
( sQ26_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f186,f254,f257]) ).
fof(f267,plain,
( ~ sQ25_spl
| greater(tau,tau) ),
inference(backward_demodulation,[status(thm)],[f255,f101]) ).
fof(f279,plain,
( ~ sQ19_spl
| ~ greater(high,mod2) ),
inference(backward_demodulation,[status(thm)],[f234,f131]) ).
fof(f285,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f279,f91]) ).
fof(f286,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f285]) ).
fof(f290,definition,
( sQ27_spl
<=> tau = tau ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f293,definition,
( sQ28_spl
<=> greater(tau,tau) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f294,plain,
( ~ sQ28_spl
| greater(tau,tau) ),
inference(component_clause,[status(thm)],[f293]) ).
fof(f295,plain,
( sQ28_spl
| ~ greater(tau,tau) ),
inference(component_clause,[status(thm)],[f293]) ).
fof(f298,plain,
( ~ sQ28_spl
| ~ greater(tau,tau) ),
inference(resolution,[status(thm)],[f294,f37]) ).
fof(f299,plain,
( ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f298,f294]) ).
fof(f300,plain,
~ sQ28_spl,
inference(contradiction_clause,[status(thm)],[f299]) ).
fof(f314,plain,
( ~ sQ7_spl
| greater(high,high) ),
inference(backward_demodulation,[status(thm)],[f192,f91]) ).
fof(f340,plain,
! [X0,X1,X2] :
( ~ dissimilar(X0,X1,X2)
| greater(age(X0,X2),sigma)
| age(X0,X1) != zero ),
inference(forward_subsumption_resolution,[status(thm)],[f70,f59]) ).
fof(f345,definition,
( sQ29_spl
<=> sigma = sigma ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f348,definition,
( sQ30_spl
<=> greater(sigma,sigma) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f349,plain,
( ~ sQ30_spl
| greater(sigma,sigma) ),
inference(component_clause,[status(thm)],[f348]) ).
fof(f350,plain,
( sQ30_spl
| ~ greater(sigma,sigma) ),
inference(component_clause,[status(thm)],[f348]) ).
fof(f372,plain,
! [X0] :
( positional_advantage(sK4_skl,X0)
| ~ greater(age(sK4_skl,X0),tau) ),
inference(resolution,[status(thm)],[f76,f97]) ).
fof(f390,plain,
! [X0,X1,X2,X3] :
( is_aligned(X0,X3)
| ~ dissimilar(X0,X3,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(resolution,[status(thm)],[f61,f60]) ).
fof(f392,plain,
( sQ28_spl
| greater(tau,tau)
| tau = tau ),
inference(resolution,[status(thm)],[f295,f139]) ).
fof(f394,plain,
( sQ28_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f392,f290,f293]) ).
fof(f407,definition,
( sQ33_spl
<=> greater(low,mod1) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f408,plain,
( ~ sQ33_spl
| greater(low,mod1) ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f411,plain,
( ~ sQ30_spl
| ~ greater(sigma,sigma) ),
inference(resolution,[status(thm)],[f349,f37]) ).
fof(f412,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f411,f349]) ).
fof(f413,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f412]) ).
fof(f424,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ dissimilar(X0,X2,X1)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(resolution,[status(thm)],[f65,f61]) ).
fof(f425,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ dissimilar(X0,X2,X1)
| age(X0,X1) != zero ),
inference(forward_subsumption_resolution,[status(thm)],[f424,f59]) ).
fof(f426,plain,
! [X0,X1,X2] :
( is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ organization(X0)
| greater(age(X0,X2),sigma)
| age(X0,X1) != zero ),
inference(resolution,[status(thm)],[f340,f62]) ).
fof(f428,plain,
! [X0,X1,X2] :
( is_aligned(X0,X2)
| ~ organization(X0)
| greater(age(X0,X2),sigma)
| age(X0,X1) != zero ),
inference(forward_subsumption_resolution,[status(thm)],[f426,f65]) ).
fof(f431,plain,
( ~ sQ9_spl
| greater(low,mod1) ),
inference(forward_demodulation,[status(thm)],[f199,f90]) ).
fof(f432,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f127]) ).
fof(f433,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f432]) ).
fof(f437,plain,
( ~ sQ15_spl
| greater(mod1,mod1) ),
inference(forward_demodulation,[status(thm)],[f220,f89]) ).
fof(f438,plain,
( ~ sQ15_spl
| ~ greater(mod1,mod1) ),
inference(resolution,[status(thm)],[f437,f37]) ).
fof(f439,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f438,f437]) ).
fof(f440,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f439]) ).
fof(f442,plain,
( sQ30_spl
| greater(sigma,sigma)
| sigma = sigma ),
inference(resolution,[status(thm)],[f350,f139]) ).
fof(f444,plain,
( sQ30_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f442,f345,f348]) ).
fof(f449,plain,
! [X0,X1,X2,X3] :
( ~ is_aligned(X0,X3)
| ~ dissimilar(X0,X3,X1)
| ~ is_aligned(X0,X2)
| ~ organization(X0)
| dissimilar(X0,X1,X2) ),
inference(resolution,[status(thm)],[f63,f61]) ).
fof(f450,plain,
! [X0,X1,X2,X3] :
( ~ is_aligned(X0,X3)
| ~ dissimilar(X0,X3,X1)
| ~ is_aligned(X0,X2)
| dissimilar(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f449,f59]) ).
fof(f453,plain,
( greater(age(sK4_skl,sK8_skl),sigma)
| age(sK4_skl,sK8_skl) = sigma ),
inference(resolution,[status(thm)],[f141,f139]) ).
fof(f455,definition,
( sQ34_spl
<=> age(sK4_skl,sK8_skl) = sigma ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f456,plain,
( ~ sQ34_spl
| age(sK4_skl,sK8_skl) = sigma ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f458,definition,
( sQ35_spl
<=> greater(age(sK4_skl,sK8_skl),sigma) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f453,f455,f458]) ).
fof(f463,plain,
( ~ sQ34_spl
| greater(sigma,sigma) ),
inference(forward_demodulation,[status(thm)],[f456,f106]) ).
fof(f464,plain,
( ~ sQ34_spl
| sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f463,f350]) ).
fof(f465,plain,
( ~ sQ34_spl
| sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f464]) ).
fof(f470,plain,
( ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f127,f408]) ).
fof(f471,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f470]) ).
fof(f491,plain,
! [X0,X1,X2,X3] :
( ~ greater(X3,X2)
| ~ greater(X1,X3)
| ~ greater(X2,X0)
| ~ greater(X0,X1) ),
inference(resolution,[status(thm)],[f125,f40]) ).
fof(f513,plain,
~ greater(very_low,mod2),
inference(resolution,[status(thm)],[f144,f90]) ).
fof(f516,plain,
( greater(mod2,very_low)
| mod2 = very_low ),
inference(resolution,[status(thm)],[f513,f139]) ).
fof(f518,definition,
( sQ36_spl
<=> mod2 = very_low ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f519,plain,
( ~ sQ36_spl
| mod2 = very_low ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f520,plain,
( sQ36_spl
| mod2 != very_low ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f521,definition,
( sQ37_spl
<=> greater(mod2,very_low) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f522,plain,
( ~ sQ37_spl
| greater(mod2,very_low) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,plain,
( sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f516,f518,f521]) ).
fof(f527,plain,
( ~ sQ10_spl
| ~ sQ36_spl
| greater(mod1,mod2) ),
inference(backward_demodulation,[status(thm)],[f519,f202]) ).
fof(f532,plain,
( ~ sQ10_spl
| ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f527,f131]) ).
fof(f533,plain,
( ~ sQ10_spl
| ~ sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f532]) ).
fof(f584,plain,
! [X0] :
( hazard_of_mortality(sK4_skl,X0) = mod2
| positional_advantage(sK4_skl,X0)
| ~ is_aligned(sK4_skl,X0)
| has_immunity(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f86,f96]) ).
fof(f585,plain,
! [X0,X1,X2,X3] :
( ~ dissimilar(X0,X2,X3)
| hazard_of_mortality(X0,X1) = mod2
| positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| has_immunity(X0,X1) ),
inference(resolution,[status(thm)],[f86,f59]) ).
fof(f589,plain,
positional_advantage(sK4_skl,sK7_skl),
inference(resolution,[status(thm)],[f372,f104]) ).
fof(f590,plain,
! [X0] :
( greater(tau,age(sK4_skl,X0))
| tau = age(sK4_skl,X0)
| positional_advantage(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f372,f139]) ).
fof(f593,definition,
( sQ38_spl
<=> greater(zero,tau) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f596,definition,
( sQ39_spl
<=> positional_advantage(sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f597,plain,
( ~ sQ39_spl
| positional_advantage(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f596]) ).
fof(f598,plain,
( sQ39_spl
| ~ positional_advantage(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f596]) ).
fof(f600,plain,
( hazard_of_mortality(sK4_skl,sK7_skl) = mod1
| is_aligned(sK4_skl,sK7_skl)
| has_immunity(sK4_skl,sK7_skl)
| ~ organization(sK4_skl) ),
inference(resolution,[status(thm)],[f589,f85]) ).
fof(f602,plain,
( ~ smaller_or_equal(age(sK4_skl,sK7_skl),tau)
| ~ robust_position(sK4_skl) ),
inference(resolution,[status(thm)],[f589,f75]) ).
fof(f603,definition,
( sQ40_spl
<=> organization(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f605,plain,
( sQ40_spl
| ~ organization(sK4_skl) ),
inference(component_clause,[status(thm)],[f603]) ).
fof(f606,definition,
( sQ41_spl
<=> has_immunity(sK4_skl,sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f607,plain,
( ~ sQ41_spl
| has_immunity(sK4_skl,sK7_skl) ),
inference(component_clause,[status(thm)],[f606]) ).
fof(f608,plain,
( sQ41_spl
| ~ has_immunity(sK4_skl,sK7_skl) ),
inference(component_clause,[status(thm)],[f606]) ).
fof(f609,definition,
( sQ42_spl
<=> is_aligned(sK4_skl,sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f610,plain,
( ~ sQ42_spl
| is_aligned(sK4_skl,sK7_skl) ),
inference(component_clause,[status(thm)],[f609]) ).
fof(f611,plain,
( sQ42_spl
| ~ is_aligned(sK4_skl,sK7_skl) ),
inference(component_clause,[status(thm)],[f609]) ).
fof(f612,definition,
( sQ43_spl
<=> hazard_of_mortality(sK4_skl,sK7_skl) = mod1 ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( ~ sQ43_spl
| hazard_of_mortality(sK4_skl,sK7_skl) = mod1 ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f615,plain,
( sQ43_spl
| sQ42_spl
| sQ41_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f600,f603,f606,f609,f612]) ).
fof(f616,definition,
( sQ44_spl
<=> hazard_of_mortality(sK4_skl,sK7_skl) = low ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f617,plain,
( ~ sQ44_spl
| hazard_of_mortality(sK4_skl,sK7_skl) = low ),
inference(component_clause,[status(thm)],[f616]) ).
fof(f620,definition,
( sQ45_spl
<=> robust_position(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f622,plain,
( sQ45_spl
| ~ robust_position(sK4_skl) ),
inference(component_clause,[status(thm)],[f620]) ).
fof(f623,definition,
( sQ46_spl
<=> smaller_or_equal(age(sK4_skl,sK7_skl),tau) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f625,plain,
( sQ46_spl
| ~ smaller_or_equal(age(sK4_skl,sK7_skl),tau) ),
inference(component_clause,[status(thm)],[f623]) ).
fof(f626,plain,
( ~ sQ46_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f602,f620,f623]) ).
fof(f627,plain,
( sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f605,f96]) ).
fof(f628,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f627]) ).
fof(f629,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f622,f97]) ).
fof(f630,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f629]) ).
fof(f633,plain,
( ~ sQ39_spl
| ~ smaller_or_equal(age(sK4_skl,sK5_skl),tau)
| ~ robust_position(sK4_skl) ),
inference(resolution,[status(thm)],[f597,f75]) ).
fof(f634,definition,
( sQ47_spl
<=> has_immunity(sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f635,plain,
( ~ sQ47_spl
| has_immunity(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f634]) ).
fof(f636,plain,
( sQ47_spl
| ~ has_immunity(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f634]) ).
fof(f637,definition,
( sQ48_spl
<=> is_aligned(sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f638,plain,
( ~ sQ48_spl
| is_aligned(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f637]) ).
fof(f639,plain,
( sQ48_spl
| ~ is_aligned(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f637]) ).
fof(f648,definition,
( sQ51_spl
<=> smaller_or_equal(age(sK4_skl,sK5_skl),tau) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( ~ sQ51_spl
| smaller_or_equal(age(sK4_skl,sK5_skl),tau) ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f650,plain,
( sQ51_spl
| ~ smaller_or_equal(age(sK4_skl,sK5_skl),tau) ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f651,plain,
( ~ sQ39_spl
| ~ sQ51_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f633,f620,f648,f596]) ).
fof(f652,plain,
( sQ51_spl
| ~ smaller_or_equal(zero,tau) ),
inference(forward_demodulation,[status(thm)],[f99,f650]) ).
fof(f654,plain,
( ~ sQ41_spl
| has_endowment(sK4_skl)
| ~ organization(sK4_skl) ),
inference(resolution,[status(thm)],[f607,f55]) ).
fof(f655,definition,
( sQ52_spl
<=> hazard_of_mortality(sK4_skl,sK7_skl) = very_low ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f656,plain,
( ~ sQ52_spl
| hazard_of_mortality(sK4_skl,sK7_skl) = very_low ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f659,definition,
( sQ53_spl
<=> has_endowment(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f660,plain,
( ~ sQ53_spl
| has_endowment(sK4_skl) ),
inference(component_clause,[status(thm)],[f659]) ).
fof(f662,plain,
( ~ sQ41_spl
| sQ53_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f654,f603,f659,f606]) ).
fof(f663,plain,
( ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f660,f98]) ).
fof(f664,plain,
~ sQ53_spl,
inference(contradiction_clause,[status(thm)],[f663]) ).
fof(f666,plain,
( ~ sQ47_spl
| has_endowment(sK4_skl)
| ~ organization(sK4_skl) ),
inference(resolution,[status(thm)],[f635,f55]) ).
fof(f667,definition,
( sQ54_spl
<=> hazard_of_mortality(sK4_skl,sK5_skl) = very_low ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f668,plain,
( ~ sQ54_spl
| hazard_of_mortality(sK4_skl,sK5_skl) = very_low ),
inference(component_clause,[status(thm)],[f667]) ).
fof(f671,plain,
( ~ sQ47_spl
| sQ53_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f666,f603,f659,f634]) ).
fof(f672,plain,
( sQ51_spl
| ~ smaller(zero,tau) ),
inference(resolution,[status(thm)],[f652,f25]) ).
fof(f674,plain,
! [X0,X1,X2] :
( ~ greater(age(X0,X1),sigma)
| age(X0,X2) != zero
| ~ organization(X0)
| ~ is_aligned(X0,X2)
| age(X0,X1) != zero ),
inference(resolution,[status(thm)],[f425,f69]) ).
fof(f676,plain,
! [X0,X1,X2] :
( ~ greater(age(X0,X1),sigma)
| age(X0,X2) != zero
| ~ organization(X0)
| age(X0,X1) != zero ),
inference(forward_subsumption_resolution,[status(thm)],[f674,f65]) ).
fof(f681,plain,
( sQ51_spl
| ~ greater(tau,zero) ),
inference(resolution,[status(thm)],[f672,f35]) ).
fof(f683,definition,
( sQ55_spl
<=> smaller_or_equal(zero,tau) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f685,plain,
( sQ55_spl
| ~ smaller_or_equal(zero,tau) ),
inference(component_clause,[status(thm)],[f683]) ).
fof(f687,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f681,f101]) ).
fof(f688,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f687]) ).
fof(f689,plain,
( ~ sQ51_spl
| smaller_or_equal(zero,tau) ),
inference(forward_demodulation,[status(thm)],[f99,f649]) ).
fof(f690,plain,
( ~ sQ25_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f267,f293,f254]) ).
fof(f693,plain,
( ~ sQ51_spl
| sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f689,f685]) ).
fof(f694,plain,
( ~ sQ51_spl
| sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f693]) ).
fof(f697,plain,
( ~ sQ43_spl
| ~ sQ44_spl
| low = mod1 ),
inference(forward_demodulation,[status(thm)],[f617,f613]) ).
fof(f698,plain,
( ~ sQ43_spl
| ~ sQ44_spl
| sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f697,f221]) ).
fof(f699,plain,
( ~ sQ43_spl
| ~ sQ44_spl
| sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f698]) ).
fof(f706,plain,
( ~ sQ52_spl
| ~ sQ44_spl
| greater(low,low) ),
inference(backward_demodulation,[status(thm)],[f716,f90]) ).
fof(f716,plain,
( ~ sQ52_spl
| ~ sQ44_spl
| low = very_low ),
inference(forward_demodulation,[status(thm)],[f617,f656]) ).
fof(f717,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ dissimilar(X0,X2,X1)
| hazard_of_mortality(X0,X1) = high
| positional_advantage(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(resolution,[status(thm)],[f87,f61]) ).
fof(f718,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ dissimilar(X0,X2,X1)
| hazard_of_mortality(X0,X1) = high
| positional_advantage(X0,X1)
| has_immunity(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f59]) ).
fof(f721,plain,
( ~ sQ52_spl
| ~ sQ44_spl
| ~ greater(low,low) ),
inference(resolution,[status(thm)],[f706,f125]) ).
fof(f726,plain,
( ~ sQ52_spl
| ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f721,f706]) ).
fof(f727,plain,
( ~ sQ52_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f726]) ).
fof(f731,plain,
( greater(age(sK4_skl,sK7_skl),tau)
| age(sK4_skl,sK7_skl) = tau ),
inference(resolution,[status(thm)],[f140,f139]) ).
fof(f733,definition,
( sQ56_spl
<=> age(sK4_skl,sK7_skl) = tau ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f734,plain,
( ~ sQ56_spl
| age(sK4_skl,sK7_skl) = tau ),
inference(component_clause,[status(thm)],[f733]) ).
fof(f736,definition,
( sQ57_spl
<=> greater(age(sK4_skl,sK7_skl),tau) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f739,plain,
( sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f731,f733,f736]) ).
fof(f756,plain,
( ~ sQ56_spl
| greater(tau,tau) ),
inference(backward_demodulation,[status(thm)],[f734,f104]) ).
fof(f760,plain,
( ~ sQ56_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f756,f293,f733]) ).
fof(f761,definition,
( sQ58_spl
<=> positional_advantage(sK4_skl,sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f780,plain,
! [X0,X1,X2,X3,X4] :
( ~ is_aligned(X0,X4)
| ~ dissimilar(X0,X4,X3)
| ~ dissimilar(X0,X3,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(resolution,[status(thm)],[f390,f61]) ).
fof(f782,plain,
! [X0,X1,X2,X3] :
( ~ greater(age(X0,X1),sigma)
| age(X0,X3) != zero
| ~ organization(X0)
| ~ is_aligned(X0,X3)
| ~ is_aligned(X0,X2)
| dissimilar(X0,X1,X2) ),
inference(resolution,[status(thm)],[f450,f69]) ).
fof(f784,plain,
! [X0,X1,X2,X3] :
( ~ greater(age(X0,X1),sigma)
| age(X0,X3) != zero
| ~ organization(X0)
| ~ is_aligned(X0,X2)
| dissimilar(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f65]) ).
fof(f791,plain,
( sQ47_spl
| hazard_of_mortality(sK4_skl,sK5_skl) = mod2
| positional_advantage(sK4_skl,sK5_skl)
| ~ is_aligned(sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f584,f636]) ).
fof(f792,plain,
( sQ41_spl
| hazard_of_mortality(sK4_skl,sK7_skl) = mod2
| positional_advantage(sK4_skl,sK7_skl)
| ~ is_aligned(sK4_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f584,f608]) ).
fof(f793,plain,
! [X0] :
( hazard_of_mortality(sK4_skl,X0) = very_low
| ~ organization(sK4_skl)
| hazard_of_mortality(sK4_skl,X0) = mod2
| positional_advantage(sK4_skl,X0)
| ~ is_aligned(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f584,f83]) ).
fof(f794,plain,
! [X0] :
( has_endowment(sK4_skl)
| ~ organization(sK4_skl)
| hazard_of_mortality(sK4_skl,X0) = mod2
| positional_advantage(sK4_skl,X0)
| ~ is_aligned(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f584,f55]) ).
fof(f795,definition,
( sQ59_spl
<=> hazard_of_mortality(sK4_skl,sK5_skl) = mod2 ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f796,plain,
( ~ sQ59_spl
| hazard_of_mortality(sK4_skl,sK5_skl) = mod2 ),
inference(component_clause,[status(thm)],[f795]) ).
fof(f798,plain,
( sQ47_spl
| sQ59_spl
| sQ39_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f791,f637,f596,f795,f634]) ).
fof(f799,definition,
( sQ60_spl
<=> hazard_of_mortality(sK4_skl,sK7_skl) = mod2 ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f800,plain,
( ~ sQ60_spl
| hazard_of_mortality(sK4_skl,sK7_skl) = mod2 ),
inference(component_clause,[status(thm)],[f799]) ).
fof(f802,plain,
( sQ41_spl
| sQ60_spl
| sQ58_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f792,f609,f761,f799,f606]) ).
fof(f803,definition,
! [X0] :
( sQ61_spl
<=> ( hazard_of_mortality(sK4_skl,X0) = very_low
| hazard_of_mortality(sK4_skl,X0) = mod2
| positional_advantage(sK4_skl,X0)
| ~ is_aligned(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f804,plain,
! [X0] :
( ~ sQ61_spl
| hazard_of_mortality(sK4_skl,X0) = very_low
| hazard_of_mortality(sK4_skl,X0) = mod2
| positional_advantage(sK4_skl,X0)
| ~ is_aligned(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f803]) ).
fof(f806,plain,
( ~ sQ40_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f793,f803,f603]) ).
fof(f807,definition,
! [X0] :
( sQ62_spl
<=> ( hazard_of_mortality(sK4_skl,X0) = mod2
| positional_advantage(sK4_skl,X0)
| ~ is_aligned(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f808,plain,
! [X0] :
( ~ sQ62_spl
| hazard_of_mortality(sK4_skl,X0) = mod2
| positional_advantage(sK4_skl,X0)
| ~ is_aligned(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f807]) ).
fof(f810,plain,
( sQ53_spl
| ~ sQ40_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f794,f807,f603,f659]) ).
fof(f811,plain,
( ~ sQ60_spl
| ~ sQ44_spl
| low = mod2 ),
inference(forward_demodulation,[status(thm)],[f617,f800]) ).
fof(f812,plain,
( ~ sQ59_spl
| ~ sQ54_spl
| very_low = mod2 ),
inference(forward_demodulation,[status(thm)],[f668,f796]) ).
fof(f813,plain,
( ~ sQ59_spl
| ~ sQ54_spl
| sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f812,f520]) ).
fof(f814,plain,
( ~ sQ59_spl
| ~ sQ54_spl
| sQ36_spl ),
inference(contradiction_clause,[status(thm)],[f813]) ).
fof(f824,plain,
( ~ sQ60_spl
| ~ sQ44_spl
| greater(mod1,mod2) ),
inference(backward_demodulation,[status(thm)],[f811,f89]) ).
fof(f829,plain,
( ~ sQ60_spl
| ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f824,f131]) ).
fof(f830,plain,
( ~ sQ60_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f829]) ).
fof(f833,plain,
! [X0] :
( sQ48_spl
| ~ organization(sK4_skl)
| greater(age(sK4_skl,sK5_skl),sigma)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f639,f428]) ).
fof(f837,definition,
( sQ63_spl
<=> hazard_of_mortality(sK4_skl,sK5_skl) = high ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f838,plain,
( ~ sQ63_spl
| hazard_of_mortality(sK4_skl,sK5_skl) = high ),
inference(component_clause,[status(thm)],[f837]) ).
fof(f841,definition,
! [X0] :
( sQ64_spl
<=> age(sK4_skl,X0) != zero ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f842,plain,
! [X0] :
( ~ sQ64_spl
| age(sK4_skl,X0) != zero ),
inference(component_clause,[status(thm)],[f841]) ).
fof(f844,definition,
( sQ65_spl
<=> greater(age(sK4_skl,sK5_skl),sigma) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f845,plain,
( ~ sQ65_spl
| greater(age(sK4_skl,sK5_skl),sigma) ),
inference(component_clause,[status(thm)],[f844]) ).
fof(f847,plain,
( sQ48_spl
| ~ sQ40_spl
| sQ65_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f833,f841,f844,f603,f637]) ).
fof(f852,definition,
( sQ67_spl
<=> age(sK4_skl,sK5_skl) = zero ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f854,plain,
( sQ67_spl
| age(sK4_skl,sK5_skl) != zero ),
inference(component_clause,[status(thm)],[f852]) ).
fof(f856,plain,
( sQ67_spl
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f99,f854]) ).
fof(f857,plain,
( sQ67_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f856]) ).
fof(f858,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f857]) ).
fof(f859,plain,
( ~ sQ65_spl
| greater(zero,sigma) ),
inference(forward_demodulation,[status(thm)],[f99,f845]) ).
fof(f860,plain,
( ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f859,f123]) ).
fof(f861,plain,
~ sQ65_spl,
inference(contradiction_clause,[status(thm)],[f860]) ).
fof(f882,plain,
! [X0] :
( hazard_of_mortality(sK4_skl,X0) = low
| ~ positional_advantage(sK4_skl,X0)
| ~ is_aligned(sK4_skl,X0)
| has_immunity(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f84,f96]) ).
fof(f886,plain,
( ~ sQ64_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f99,f842]) ).
fof(f887,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f886]) ).
fof(f894,plain,
( ~ sQ59_spl
| ~ sQ63_spl
| high = mod2 ),
inference(forward_demodulation,[status(thm)],[f838,f796]) ).
fof(f895,plain,
( ~ sQ59_spl
| ~ sQ63_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f894,f193]) ).
fof(f896,plain,
( ~ sQ59_spl
| ~ sQ63_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f895]) ).
fof(f914,plain,
( ~ sQ7_spl
| ~ greater(high,high) ),
inference(resolution,[status(thm)],[f314,f125]) ).
fof(f919,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f914,f314]) ).
fof(f920,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f919]) ).
fof(f948,plain,
! [X0,X1,X2] :
( ~ greater(age(X0,X1),sigma)
| age(X0,X2) != zero
| ~ organization(X0)
| ~ is_aligned(X0,X2)
| hazard_of_mortality(X0,X1) = high
| positional_advantage(X0,X1)
| has_immunity(X0,X1) ),
inference(resolution,[status(thm)],[f718,f69]) ).
fof(f950,plain,
! [X0,X1,X2] :
( ~ greater(age(X0,X1),sigma)
| age(X0,X2) != zero
| ~ organization(X0)
| hazard_of_mortality(X0,X1) = high
| positional_advantage(X0,X1)
| has_immunity(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f948,f65]) ).
fof(f951,plain,
( sQ2_spl
| ~ sQ59_spl
| hazard_of_mortality(sK4_skl,sK6_skl) != mod2 ),
inference(backward_demodulation,[status(thm)],[f796,f116]) ).
fof(f962,plain,
( hazard_of_mortality(sK4_skl,sK7_skl) = low
| ~ is_aligned(sK4_skl,sK7_skl)
| has_immunity(sK4_skl,sK7_skl) ),
inference(resolution,[status(thm)],[f882,f589]) ).
fof(f964,plain,
( sQ44_spl
| ~ sQ42_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f962,f606,f609,f616]) ).
fof(f965,definition,
( sQ68_spl
<=> has_immunity(sK4_skl,sK2_skl(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f966,plain,
( ~ sQ68_spl
| has_immunity(sK4_skl,sK2_skl(sK4_skl)) ),
inference(component_clause,[status(thm)],[f965]) ).
fof(f1007,plain,
( ~ sQ68_spl
| has_endowment(sK4_skl)
| ~ organization(sK4_skl) ),
inference(resolution,[status(thm)],[f966,f55]) ).
fof(f1012,plain,
( ~ sQ68_spl
| sQ53_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f1007,f603,f659,f965]) ).
fof(f1028,plain,
( ~ sQ6_spl
| ~ greater(age(sK4_skl,sK6_skl),sigma) ),
inference(resolution,[status(thm)],[f161,f133]) ).
fof(f1034,plain,
( ~ sQ4_spl
| ~ greater(age(sK4_skl,sK7_skl),sigma) ),
inference(resolution,[status(thm)],[f154,f37]) ).
fof(f1113,plain,
! [X0,X1,X2,X3] :
( ~ dissimilar(X0,X2,X3)
| hazard_of_mortality(X0,X1) = low
| ~ positional_advantage(X0,X1)
| ~ is_aligned(X0,X1)
| has_immunity(X0,X1) ),
inference(resolution,[status(thm)],[f84,f59]) ).
fof(f1122,definition,
( sQ86_spl
<=> sigma = age(sK4_skl,sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1123,plain,
( ~ sQ86_spl
| sigma = age(sK4_skl,sK6_skl) ),
inference(component_clause,[status(thm)],[f1122]) ).
fof(f1130,plain,
( ~ sQ86_spl
| positional_advantage(sK4_skl,sK6_skl)
| ~ greater(sigma,tau) ),
inference(paramodulation,[status(thm)],[f1123,f372]) ).
fof(f1131,definition,
( sQ88_spl
<=> positional_advantage(sK4_skl,sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1132,plain,
( ~ sQ88_spl
| positional_advantage(sK4_skl,sK6_skl) ),
inference(component_clause,[status(thm)],[f1131]) ).
fof(f1134,plain,
( ~ sQ86_spl
| sQ88_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f1130,f243,f1131,f1122]) ).
fof(f1141,plain,
( ~ sQ21_spl
| smaller_or_equal(age(sK4_skl,sK7_skl),tau) ),
inference(backward_demodulation,[status(thm)],[f241,f105]) ).
fof(f1157,plain,
( ~ sQ21_spl
| sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1141,f625]) ).
fof(f1158,plain,
( ~ sQ21_spl
| sQ46_spl ),
inference(contradiction_clause,[status(thm)],[f1157]) ).
fof(f1162,plain,
( ~ sQ88_spl
| ~ smaller_or_equal(age(sK4_skl,sK6_skl),tau)
| ~ robust_position(sK4_skl) ),
inference(resolution,[status(thm)],[f1132,f75]) ).
fof(f1163,definition,
( sQ89_spl
<=> has_immunity(sK4_skl,sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1164,plain,
( ~ sQ89_spl
| has_immunity(sK4_skl,sK6_skl) ),
inference(component_clause,[status(thm)],[f1163]) ).
fof(f1165,plain,
( sQ89_spl
| ~ has_immunity(sK4_skl,sK6_skl) ),
inference(component_clause,[status(thm)],[f1163]) ).
fof(f1166,definition,
( sQ90_spl
<=> is_aligned(sK4_skl,sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1168,plain,
( sQ90_spl
| ~ is_aligned(sK4_skl,sK6_skl) ),
inference(component_clause,[status(thm)],[f1166]) ).
fof(f1178,definition,
( sQ93_spl
<=> smaller_or_equal(age(sK4_skl,sK6_skl),tau) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1180,plain,
( sQ93_spl
| ~ smaller_or_equal(age(sK4_skl,sK6_skl),tau) ),
inference(component_clause,[status(thm)],[f1178]) ).
fof(f1181,plain,
( ~ sQ88_spl
| ~ sQ93_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f1162,f620,f1178,f1131]) ).
fof(f1202,plain,
( ~ sQ89_spl
| has_endowment(sK4_skl)
| ~ organization(sK4_skl) ),
inference(resolution,[status(thm)],[f1164,f55]) ).
fof(f1207,plain,
( ~ sQ89_spl
| sQ53_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f1202,f603,f659,f1163]) ).
fof(f1208,plain,
( sQ89_spl
| hazard_of_mortality(sK4_skl,sK6_skl) = mod2
| positional_advantage(sK4_skl,sK6_skl)
| ~ is_aligned(sK4_skl,sK6_skl) ),
inference(resolution,[status(thm)],[f1165,f584]) ).
fof(f1209,definition,
( sQ95_spl
<=> hazard_of_mortality(sK4_skl,sK6_skl) = mod2 ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1210,plain,
( ~ sQ95_spl
| hazard_of_mortality(sK4_skl,sK6_skl) = mod2 ),
inference(component_clause,[status(thm)],[f1209]) ).
fof(f1212,plain,
( sQ89_spl
| sQ95_spl
| sQ88_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f1208,f1166,f1131,f1209,f1163]) ).
fof(f1213,plain,
( ~ sQ95_spl
| sQ2_spl
| ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1210,f951]) ).
fof(f1214,plain,
( ~ sQ95_spl
| sQ2_spl
| ~ sQ59_spl ),
inference(contradiction_clause,[status(thm)],[f1213]) ).
fof(f1215,plain,
( sQ0_spl
| ~ sQ44_spl
| ~ smaller(low,hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(forward_demodulation,[status(thm)],[f617,f110]) ).
fof(f1216,plain,
( ~ sQ2_spl
| ~ sQ59_spl
| hazard_of_mortality(sK4_skl,sK6_skl) = mod2 ),
inference(forward_demodulation,[status(thm)],[f796,f115]) ).
fof(f1270,definition,
( sQ99_spl
<=> mod2 = mod2 ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1273,definition,
( sQ100_spl
<=> greater(mod2,mod2) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1274,plain,
( ~ sQ100_spl
| greater(mod2,mod2) ),
inference(component_clause,[status(thm)],[f1273]) ).
fof(f1275,plain,
( sQ100_spl
| ~ greater(mod2,mod2) ),
inference(component_clause,[status(thm)],[f1273]) ).
fof(f1284,plain,
! [X0,X1] :
( dissimilar(sK4_skl,X0,X1)
| ~ greater(age(sK4_skl,X1),sigma)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f69,f96]) ).
fof(f1285,plain,
! [X0,X1,X2,X3,X4] :
( ~ dissimilar(X0,X3,X4)
| dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma)
| age(X0,X1) != zero ),
inference(resolution,[status(thm)],[f69,f59]) ).
fof(f1291,definition,
( sQ101_spl
<=> low = hazard_of_mortality(sK4_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1292,plain,
( ~ sQ101_spl
| low = hazard_of_mortality(sK4_skl,sK8_skl) ),
inference(component_clause,[status(thm)],[f1291]) ).
fof(f1340,definition,
( sQ104_spl
<=> low = low ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1343,definition,
( sQ105_spl
<=> greater(low,low) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1344,plain,
( ~ sQ105_spl
| greater(low,low) ),
inference(component_clause,[status(thm)],[f1343]) ).
fof(f1345,plain,
( sQ105_spl
| ~ greater(low,low) ),
inference(component_clause,[status(thm)],[f1343]) ).
fof(f1347,definition,
( sQ106_spl
<=> smaller_or_equal(low,low) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1349,plain,
( sQ106_spl
| ~ smaller_or_equal(low,low) ),
inference(component_clause,[status(thm)],[f1347]) ).
fof(f1351,plain,
( sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1349,f118]) ).
fof(f1352,plain,
sQ106_spl,
inference(contradiction_clause,[status(thm)],[f1351]) ).
fof(f1353,plain,
( ~ sQ105_spl
| ~ greater(low,low) ),
inference(resolution,[status(thm)],[f1344,f125]) ).
fof(f1358,plain,
( ~ sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1353,f1344]) ).
fof(f1359,plain,
~ sQ105_spl,
inference(contradiction_clause,[status(thm)],[f1358]) ).
fof(f1360,plain,
( sQ105_spl
| greater(low,low)
| low = low ),
inference(resolution,[status(thm)],[f1345,f139]) ).
fof(f1362,plain,
( sQ105_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f1360,f1340,f1343]) ).
fof(f1366,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ dissimilar(X0,X2,X1)
| hazard_of_mortality(X0,X1) = mod1
| ~ positional_advantage(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(resolution,[status(thm)],[f85,f61]) ).
fof(f1367,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ dissimilar(X0,X2,X1)
| hazard_of_mortality(X0,X1) = mod1
| ~ positional_advantage(X0,X1)
| has_immunity(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1366,f59]) ).
fof(f1389,definition,
( sQ107_spl
<=> hazard_of_mortality(sK4_skl,sK7_skl) = hazard_of_mortality(sK4_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1390,plain,
( ~ sQ107_spl
| hazard_of_mortality(sK4_skl,sK7_skl) = hazard_of_mortality(sK4_skl,sK8_skl) ),
inference(component_clause,[status(thm)],[f1389]) ).
fof(f1391,plain,
( sQ107_spl
| hazard_of_mortality(sK4_skl,sK7_skl) != hazard_of_mortality(sK4_skl,sK8_skl) ),
inference(component_clause,[status(thm)],[f1389]) ).
fof(f1392,definition,
( sQ108_spl
<=> greater(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1393,plain,
( ~ sQ108_spl
| greater(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f1392]) ).
fof(f1396,definition,
( sQ109_spl
<=> smaller_or_equal(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1397,plain,
( ~ sQ109_spl
| smaller_or_equal(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f1396]) ).
fof(f1398,plain,
( sQ109_spl
| ~ smaller_or_equal(hazard_of_mortality(sK4_skl,sK7_skl),hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f1396]) ).
fof(f1481,plain,
! [X0] :
( dissimilar(sK4_skl,X0,sK8_skl)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1284,f106]) ).
fof(f1482,plain,
! [X0,X1] :
( greater(sigma,age(sK4_skl,X1))
| sigma = age(sK4_skl,X1)
| dissimilar(sK4_skl,X0,X1)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1284,f139]) ).
fof(f1489,definition,
( sQ111_spl
<=> greater(tau,sigma) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1496,definition,
( sQ113_spl
<=> greater(zero,sigma) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1522,plain,
( sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1180,f103]) ).
fof(f1523,plain,
sQ93_spl,
inference(contradiction_clause,[status(thm)],[f1522]) ).
fof(f1524,plain,
! [X0] :
( sQ90_spl
| ~ organization(sK4_skl)
| greater(age(sK4_skl,sK6_skl),sigma)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1168,f428]) ).
fof(f1531,definition,
( sQ114_spl
<=> greater(age(sK4_skl,sK6_skl),sigma) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1532,plain,
( ~ sQ114_spl
| greater(age(sK4_skl,sK6_skl),sigma) ),
inference(component_clause,[status(thm)],[f1531]) ).
fof(f1534,plain,
( sQ90_spl
| ~ sQ40_spl
| sQ114_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1524,f841,f1531,f603,f1166]) ).
fof(f1550,plain,
( ~ sQ107_spl
| ~ sQ44_spl
| low = hazard_of_mortality(sK4_skl,sK8_skl) ),
inference(forward_demodulation,[status(thm)],[f617,f1390]) ).
fof(f1553,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| smaller(low,hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(forward_demodulation,[status(thm)],[f617,f109]) ).
fof(f1554,plain,
( sQ107_spl
| ~ sQ44_spl
| low != hazard_of_mortality(sK4_skl,sK8_skl) ),
inference(forward_demodulation,[status(thm)],[f617,f1391]) ).
fof(f1566,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| greater(hazard_of_mortality(sK4_skl,sK8_skl),low) ),
inference(resolution,[status(thm)],[f1553,f34]) ).
fof(f1567,plain,
( sQ109_spl
| ~ sQ44_spl
| ~ smaller_or_equal(low,hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(forward_demodulation,[status(thm)],[f617,f1398]) ).
fof(f1568,plain,
( sQ109_spl
| ~ sQ44_spl
| ~ smaller(low,hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(resolution,[status(thm)],[f1567,f25]) ).
fof(f1569,plain,
( sQ109_spl
| ~ sQ44_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1568,f1553]) ).
fof(f1570,plain,
( sQ109_spl
| ~ sQ44_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f1569]) ).
fof(f1571,plain,
( ~ sQ109_spl
| ~ sQ44_spl
| smaller_or_equal(low,hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(forward_demodulation,[status(thm)],[f617,f1397]) ).
fof(f1572,plain,
( ~ sQ108_spl
| ~ sQ44_spl
| greater(low,hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(forward_demodulation,[status(thm)],[f617,f1393]) ).
fof(f1582,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| ~ greater(low,hazard_of_mortality(sK4_skl,sK8_skl)) ),
inference(resolution,[status(thm)],[f1566,f37]) ).
fof(f1583,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| ~ sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1582,f1572]) ).
fof(f1584,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| ~ sQ108_spl ),
inference(contradiction_clause,[status(thm)],[f1583]) ).
fof(f1586,plain,
( ~ sQ109_spl
| ~ sQ44_spl
| greater(hazard_of_mortality(sK4_skl,sK8_skl),low)
| low = hazard_of_mortality(sK4_skl,sK8_skl) ),
inference(resolution,[status(thm)],[f1571,f124]) ).
fof(f1587,definition,
( sQ115_spl
<=> greater(hazard_of_mortality(sK4_skl,sK8_skl),low) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1590,plain,
( ~ sQ109_spl
| ~ sQ44_spl
| sQ115_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f1586,f1291,f1587,f616,f1396]) ).
fof(f1591,plain,
( ~ sQ101_spl
| sQ107_spl
| ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1292,f1554]) ).
fof(f1592,plain,
( ~ sQ101_spl
| sQ107_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f1591]) ).
fof(f1610,plain,
( ~ sQ114_spl
| ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1532,f1028]) ).
fof(f1611,plain,
( ~ sQ114_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f1610]) ).
fof(f1684,definition,
( sQ125_spl
<=> has_immunity(sK4_skl,sK0_skl(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1685,plain,
( ~ sQ125_spl
| has_immunity(sK4_skl,sK0_skl(sK4_skl)) ),
inference(component_clause,[status(thm)],[f1684]) ).
fof(f1734,plain,
( ~ sQ125_spl
| has_endowment(sK4_skl)
| ~ organization(sK4_skl) ),
inference(resolution,[status(thm)],[f1685,f55]) ).
fof(f1739,plain,
( ~ sQ125_spl
| sQ53_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f1734,f603,f659,f1684]) ).
fof(f1749,plain,
( ~ sQ114_spl
| ~ sQ5_spl
| greater(tau,sigma) ),
inference(forward_demodulation,[status(thm)],[f158,f1532]) ).
fof(f1750,plain,
( ~ sQ114_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1749,f122]) ).
fof(f1751,plain,
( ~ sQ114_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f1750]) ).
fof(f1754,plain,
! [X0] :
( sQ42_spl
| ~ organization(sK4_skl)
| greater(age(sK4_skl,sK7_skl),sigma)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f611,f428]) ).
fof(f1761,definition,
( sQ136_spl
<=> greater(age(sK4_skl,sK7_skl),sigma) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1762,plain,
( ~ sQ136_spl
| greater(age(sK4_skl,sK7_skl),sigma) ),
inference(component_clause,[status(thm)],[f1761]) ).
fof(f1764,plain,
( sQ42_spl
| ~ sQ40_spl
| sQ136_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1754,f841,f1761,f603,f609]) ).
fof(f1778,plain,
( ~ sQ136_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1762,f1034]) ).
fof(f1779,plain,
( ~ sQ136_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f1778]) ).
fof(f1820,definition,
( sQ142_spl
<=> high = low ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1821,plain,
( ~ sQ142_spl
| high = low ),
inference(component_clause,[status(thm)],[f1820]) ).
fof(f1823,definition,
( sQ143_spl
<=> greater(high,low) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f1831,plain,
( sQ1_spl
| ~ sQ2_spl
| ~ sQ59_spl
| ~ smaller(hazard_of_mortality(sK4_skl,sK8_skl),mod2) ),
inference(forward_demodulation,[status(thm)],[f1216,f113]) ).
fof(f1835,definition,
( sQ145_spl
<=> hazard_of_mortality(sK4_skl,sK8_skl) = mod2 ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1836,plain,
( ~ sQ145_spl
| hazard_of_mortality(sK4_skl,sK8_skl) = mod2 ),
inference(component_clause,[status(thm)],[f1835]) ).
fof(f1859,plain,
( ~ sQ142_spl
| greater(mod2,high) ),
inference(backward_demodulation,[status(thm)],[f1821,f92]) ).
fof(f1867,plain,
( ~ sQ142_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1859,f129]) ).
fof(f1868,plain,
~ sQ142_spl,
inference(contradiction_clause,[status(thm)],[f1867]) ).
fof(f1942,definition,
( sQ148_spl
<=> mod1 = hazard_of_mortality(sK4_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition]) ).
fof(f1943,plain,
( ~ sQ148_spl
| mod1 = hazard_of_mortality(sK4_skl,sK8_skl) ),
inference(component_clause,[status(thm)],[f1942]) ).
fof(f1959,definition,
( sQ151_spl
<=> smaller_or_equal(mod1,mod1) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1961,plain,
( sQ151_spl
| ~ smaller_or_equal(mod1,mod1) ),
inference(component_clause,[status(thm)],[f1959]) ).
fof(f1963,plain,
( sQ151_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1961,f118]) ).
fof(f1964,plain,
sQ151_spl,
inference(contradiction_clause,[status(thm)],[f1963]) ).
fof(f1996,definition,
( sQ152_spl
<=> greater(mod1,mod2) ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f1997,plain,
( ~ sQ152_spl
| greater(mod1,mod2) ),
inference(component_clause,[status(thm)],[f1996]) ).
fof(f2006,plain,
( ~ sQ152_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1997,f131]) ).
fof(f2007,plain,
~ sQ152_spl,
inference(contradiction_clause,[status(thm)],[f2006]) ).
fof(f2012,plain,
( ~ sQ100_spl
| ~ greater(mod2,mod2) ),
inference(resolution,[status(thm)],[f1274,f125]) ).
fof(f2017,plain,
~ sQ100_spl,
inference(split_clause,[status(thm)],[f2012,f1273]) ).
fof(f2026,plain,
( sQ100_spl
| greater(mod2,mod2)
| mod2 = mod2 ),
inference(resolution,[status(thm)],[f1275,f139]) ).
fof(f2028,plain,
( sQ100_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f2026,f1270,f1273]) ).
fof(f2054,plain,
( ~ sQ136_spl
| ~ sQ3_spl
| greater(sigma,sigma) ),
inference(forward_demodulation,[status(thm)],[f151,f1762]) ).
fof(f2055,plain,
( ~ sQ136_spl
| ~ sQ3_spl
| sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2054,f350]) ).
fof(f2056,plain,
( ~ sQ136_spl
| ~ sQ3_spl
| sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f2055]) ).
fof(f2077,plain,
( ~ sQ148_spl
| ~ sQ107_spl
| ~ sQ44_spl
| mod1 = low ),
inference(forward_demodulation,[status(thm)],[f1550,f1943]) ).
fof(f2078,plain,
( ~ sQ148_spl
| ~ sQ107_spl
| ~ sQ44_spl
| sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2077,f221]) ).
fof(f2079,plain,
( ~ sQ148_spl
| ~ sQ107_spl
| ~ sQ44_spl
| sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f2078]) ).
fof(f2148,definition,
! [X0] :
( sQ156_spl
<=> ~ is_aligned(sK4_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f2149,plain,
! [X0] :
( ~ sQ156_spl
| ~ is_aligned(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f2148]) ).
fof(f2151,definition,
! [X1] :
( sQ157_spl
<=> ( hazard_of_mortality(sK4_skl,X1) = low
| ~ positional_advantage(sK4_skl,X1)
| ~ is_aligned(sK4_skl,X1)
| has_immunity(sK4_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f2159,definition,
! [X1,X2] :
( sQ159_spl
<=> ( dissimilar(sK4_skl,X1,X2)
| ~ greater(age(sK4_skl,X2),sigma)
| age(sK4_skl,X1) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f2167,definition,
! [X1] :
( sQ161_spl
<=> ( hazard_of_mortality(sK4_skl,X1) = mod2
| positional_advantage(sK4_skl,X1)
| ~ is_aligned(sK4_skl,X1)
| has_immunity(sK4_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f2175,definition,
! [X0,X1] :
( sQ163_spl
<=> ( ~ is_aligned(sK4_skl,X1)
| dissimilar(sK4_skl,X0,X1)
| ~ is_aligned(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f2176,plain,
! [X0,X1] :
( ~ sQ163_spl
| ~ is_aligned(sK4_skl,X1)
| dissimilar(sK4_skl,X0,X1)
| ~ is_aligned(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f2175]) ).
fof(f2179,definition,
! [X0] :
( sQ164_spl
<=> ( age(sK4_skl,X0) != zero
| ~ is_aligned(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f2180,plain,
! [X0] :
( ~ sQ164_spl
| age(sK4_skl,X0) != zero
| ~ is_aligned(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f2179]) ).
fof(f2183,plain,
! [X0,X1] :
( ~ sQ163_spl
| ~ is_aligned(sK4_skl,X1)
| ~ is_aligned(sK4_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2176,f61]) ).
fof(f2184,plain,
( ~ sQ42_spl
| ~ sQ156_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f610,f2149]) ).
fof(f2194,plain,
( ~ sQ42_spl
| ~ sQ156_spl ),
inference(contradiction_clause,[status(thm)],[f2184]) ).
fof(f2245,plain,
! [X0] :
( ~ sQ48_spl
| ~ sQ163_spl
| ~ is_aligned(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f2183,f638]) ).
fof(f2255,plain,
( ~ sQ48_spl
| ~ sQ163_spl
| sQ156_spl ),
inference(split_clause,[status(thm)],[f2245,f2148,f2175,f637]) ).
fof(f2274,definition,
! [X1,X2] :
( sQ169_spl
<=> ( ~ is_aligned(sK4_skl,X2)
| dissimilar(sK4_skl,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f2275,plain,
! [X0,X1] :
( ~ sQ169_spl
| ~ is_aligned(sK4_skl,X1)
| dissimilar(sK4_skl,X0,X1) ),
inference(component_clause,[status(thm)],[f2274]) ).
fof(f2327,plain,
! [X0] :
( ~ smaller_or_equal(age(sK4_skl,X0),tau)
| ~ robust_position(sK4_skl)
| hazard_of_mortality(sK4_skl,X0) = mod2
| ~ is_aligned(sK4_skl,X0)
| has_immunity(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f584,f75]) ).
fof(f2331,definition,
( sQ173_spl
<=> has_immunity(sK4_skl,sK3_skl(sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition]) ).
fof(f2332,plain,
( ~ sQ173_spl
| has_immunity(sK4_skl,sK3_skl(sK4_skl)) ),
inference(component_clause,[status(thm)],[f2331]) ).
fof(f2342,definition,
! [X0] :
( sQ176_spl
<=> ( ~ smaller_or_equal(age(sK4_skl,X0),tau)
| hazard_of_mortality(sK4_skl,X0) = mod2
| ~ is_aligned(sK4_skl,X0)
| has_immunity(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f2345,plain,
( ~ sQ45_spl
| sQ176_spl ),
inference(split_clause,[status(thm)],[f2327,f2342,f620]) ).
fof(f2401,plain,
( ~ sQ173_spl
| has_endowment(sK4_skl)
| ~ organization(sK4_skl) ),
inference(resolution,[status(thm)],[f2332,f55]) ).
fof(f2406,plain,
( ~ sQ173_spl
| sQ53_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f2401,f603,f659,f2331]) ).
fof(f2416,plain,
! [X0] :
( hazard_of_mortality(sK4_skl,X0) = mod2
| ~ is_aligned(sK4_skl,X0)
| has_immunity(sK4_skl,X0)
| hazard_of_mortality(sK4_skl,X0) = low
| ~ is_aligned(sK4_skl,X0)
| has_immunity(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f882,f584]) ).
fof(f2420,plain,
! [X0] :
( hazard_of_mortality(sK4_skl,X0) = mod2
| hazard_of_mortality(sK4_skl,X0) = low
| ~ is_aligned(sK4_skl,X0)
| has_immunity(sK4_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2416]) ).
fof(f2422,plain,
( ~ greater(sigma,age(sK4_skl,sK8_skl))
| ~ greater(sigma,age(sK4_skl,sK8_skl)) ),
inference(resolution,[status(thm)],[f491,f106]) ).
fof(f2424,plain,
( ~ greater(very_low,low)
| ~ greater(very_low,low) ),
inference(resolution,[status(thm)],[f491,f90]) ).
fof(f2428,plain,
( ~ sQ10_spl
| ~ greater(very_low,mod1)
| ~ greater(very_low,mod1) ),
inference(resolution,[status(thm)],[f491,f202]) ).
fof(f2430,plain,
( ~ greater(tau,sigma)
| ~ greater(tau,sigma) ),
inference(resolution,[status(thm)],[f491,f102]) ).
fof(f2432,plain,
( ~ greater(zero,sigma)
| ~ greater(zero,sigma) ),
inference(resolution,[status(thm)],[f491,f100]) ).
fof(f2434,plain,
( ~ greater(low,mod2)
| ~ greater(low,mod2) ),
inference(resolution,[status(thm)],[f491,f92]) ).
fof(f2438,plain,
( ~ sQ37_spl
| ~ greater(very_low,mod2)
| ~ greater(very_low,mod2) ),
inference(resolution,[status(thm)],[f491,f522]) ).
fof(f2442,plain,
( ~ greater(mod1,high)
| ~ greater(mod1,high) ),
inference(resolution,[status(thm)],[f491,f88]) ).
fof(f2444,plain,
( ~ greater(mod2,high)
| ~ greater(mod2,high) ),
inference(resolution,[status(thm)],[f491,f91]) ).
fof(f2446,plain,
( ~ greater(zero,tau)
| ~ greater(zero,tau) ),
inference(resolution,[status(thm)],[f491,f101]) ).
fof(f2484,definition,
( sQ184_spl
<=> greater(sigma,age(sK4_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition]) ).
fof(f2487,plain,
~ sQ184_spl,
inference(split_clause,[status(thm)],[f2422,f2484]) ).
fof(f2488,definition,
( sQ185_spl
<=> greater(very_low,low) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f2491,plain,
~ sQ185_spl,
inference(split_clause,[status(thm)],[f2424,f2488]) ).
fof(f2493,definition,
( sQ186_spl
<=> greater(very_low,mod1) ),
introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition]) ).
fof(f2496,plain,
( ~ sQ10_spl
| ~ sQ186_spl ),
inference(split_clause,[status(thm)],[f2428,f2493,f201]) ).
fof(f2497,plain,
~ sQ111_spl,
inference(split_clause,[status(thm)],[f2430,f1489]) ).
fof(f2498,plain,
~ sQ113_spl,
inference(split_clause,[status(thm)],[f2432,f1496]) ).
fof(f2499,definition,
( sQ187_spl
<=> greater(low,mod2) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f2502,plain,
~ sQ187_spl,
inference(split_clause,[status(thm)],[f2434,f2499]) ).
fof(f2504,definition,
( sQ188_spl
<=> greater(very_low,mod2) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f2507,plain,
( ~ sQ37_spl
| ~ sQ188_spl ),
inference(split_clause,[status(thm)],[f2438,f2504,f521]) ).
fof(f2508,definition,
( sQ189_spl
<=> greater(low,high) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f2512,definition,
( sQ190_spl
<=> greater(mod1,high) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f2515,plain,
~ sQ190_spl,
inference(split_clause,[status(thm)],[f2442,f2512]) ).
fof(f2516,definition,
( sQ191_spl
<=> greater(mod2,high) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f2519,plain,
~ sQ191_spl,
inference(split_clause,[status(thm)],[f2444,f2516]) ).
fof(f2520,plain,
~ sQ38_spl,
inference(split_clause,[status(thm)],[f2446,f593]) ).
fof(f2527,plain,
! [X0,X1,X2] :
( ~ sQ169_spl
| ~ is_aligned(sK4_skl,X2)
| ~ is_aligned(sK4_skl,X1)
| dissimilar(sK4_skl,X0,X1)
| ~ is_aligned(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f2275,f450]) ).
fof(f2535,plain,
( ~ sQ169_spl
| sQ156_spl
| sQ163_spl ),
inference(split_clause,[status(thm)],[f2527,f2175,f2148,f2274]) ).
fof(f2628,plain,
( sQ39_spl
| greater(tau,age(sK4_skl,sK5_skl))
| tau = age(sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f590,f598]) ).
fof(f2632,plain,
! [X0] :
( ~ smaller_or_equal(age(sK4_skl,X0),tau)
| ~ robust_position(sK4_skl)
| greater(tau,age(sK4_skl,X0))
| tau = age(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f590,f75]) ).
fof(f2641,definition,
( sQ196_spl
<=> tau = age(sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f2642,plain,
( ~ sQ196_spl
| tau = age(sK4_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f2641]) ).
fof(f2644,definition,
( sQ197_spl
<=> greater(tau,age(sK4_skl,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f2647,plain,
( sQ39_spl
| sQ197_spl
| sQ196_spl ),
inference(split_clause,[status(thm)],[f2628,f2641,f2644,f596]) ).
fof(f2656,definition,
! [X0] :
( sQ200_spl
<=> ( ~ smaller_or_equal(age(sK4_skl,X0),tau)
| greater(tau,age(sK4_skl,X0))
| tau = age(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f2659,plain,
( ~ sQ45_spl
| sQ200_spl ),
inference(split_clause,[status(thm)],[f2632,f2656,f620]) ).
fof(f2660,plain,
( ~ sQ196_spl
| tau = zero ),
inference(forward_demodulation,[status(thm)],[f99,f2642]) ).
fof(f2661,plain,
( ~ sQ196_spl
| sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2660,f256]) ).
fof(f2662,plain,
( ~ sQ196_spl
| sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f2661]) ).
fof(f2691,plain,
! [X0,X1] :
( ~ greater(age(sK4_skl,X0),sigma)
| age(sK4_skl,X1) != zero
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f676,f96]) ).
fof(f2693,definition,
! [X0] :
( sQ202_spl
<=> ( ~ greater(age(sK4_skl,X0),sigma)
| age(sK4_skl,X0) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f2696,plain,
( sQ64_spl
| sQ202_spl ),
inference(split_clause,[status(thm)],[f2691,f2693,f841]) ).
fof(f2782,plain,
! [X0,X1,X2] :
( ~ greater(age(sK4_skl,X0),sigma)
| age(sK4_skl,X2) != zero
| ~ is_aligned(sK4_skl,X1)
| dissimilar(sK4_skl,X0,X1) ),
inference(resolution,[status(thm)],[f784,f96]) ).
fof(f2784,definition,
! [X0,X1] :
( sQ209_spl
<=> ( ~ greater(age(sK4_skl,X0),sigma)
| ~ is_aligned(sK4_skl,X1)
| dissimilar(sK4_skl,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f2787,plain,
( sQ64_spl
| sQ209_spl ),
inference(split_clause,[status(thm)],[f2782,f2784,f841]) ).
fof(f2820,plain,
! [X0] :
( ~ sQ61_spl
| ~ smaller_or_equal(age(sK4_skl,X0),tau)
| ~ robust_position(sK4_skl)
| hazard_of_mortality(sK4_skl,X0) = very_low
| hazard_of_mortality(sK4_skl,X0) = mod2
| ~ is_aligned(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f804,f75]) ).
fof(f2827,definition,
! [X0] :
( sQ210_spl
<=> ( ~ smaller_or_equal(age(sK4_skl,X0),tau)
| hazard_of_mortality(sK4_skl,X0) = very_low
| hazard_of_mortality(sK4_skl,X0) = mod2
| ~ is_aligned(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f2830,plain,
( ~ sQ61_spl
| ~ sQ45_spl
| sQ210_spl ),
inference(split_clause,[status(thm)],[f2820,f2827,f620,f803]) ).
fof(f2869,plain,
( ~ greater(tau,age(sK4_skl,sK7_skl))
| ~ greater(tau,age(sK4_skl,sK7_skl)) ),
inference(resolution,[status(thm)],[f104,f491]) ).
fof(f2876,definition,
( sQ211_spl
<=> greater(tau,age(sK4_skl,sK7_skl)) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f2879,plain,
~ sQ211_spl,
inference(split_clause,[status(thm)],[f2869,f2876]) ).
fof(f2970,plain,
! [X0] :
( ~ sQ62_spl
| ~ smaller_or_equal(age(sK4_skl,X0),tau)
| ~ robust_position(sK4_skl)
| hazard_of_mortality(sK4_skl,X0) = mod2
| ~ is_aligned(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f808,f75]) ).
fof(f2976,definition,
! [X0] :
( sQ213_spl
<=> ( ~ smaller_or_equal(age(sK4_skl,X0),tau)
| hazard_of_mortality(sK4_skl,X0) = mod2
| ~ is_aligned(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f2979,plain,
( ~ sQ62_spl
| ~ sQ45_spl
| sQ213_spl ),
inference(split_clause,[status(thm)],[f2970,f2976,f620,f807]) ).
fof(f3031,plain,
! [X0,X1] :
( ~ greater(age(sK4_skl,X0),sigma)
| age(sK4_skl,X1) != zero
| hazard_of_mortality(sK4_skl,X0) = high
| positional_advantage(sK4_skl,X0)
| has_immunity(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f950,f96]) ).
fof(f3033,definition,
! [X0] :
( sQ216_spl
<=> ( ~ greater(age(sK4_skl,X0),sigma)
| hazard_of_mortality(sK4_skl,X0) = high
| positional_advantage(sK4_skl,X0)
| has_immunity(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f3036,plain,
( sQ64_spl
| sQ216_spl ),
inference(split_clause,[status(thm)],[f3031,f3033,f841]) ).
fof(f3161,plain,
! [X0,X1,X2] :
( ~ is_aligned(sK4_skl,X0)
| ~ dissimilar(sK4_skl,sK8_skl,X2)
| ~ is_aligned(sK4_skl,X1)
| ~ dissimilar(sK4_skl,X1,X2)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1481,f780]) ).
fof(f3165,plain,
! [X0,X1] :
( hazard_of_mortality(sK4_skl,X1) = low
| ~ positional_advantage(sK4_skl,X1)
| ~ is_aligned(sK4_skl,X1)
| has_immunity(sK4_skl,X1)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1481,f1113]) ).
fof(f3166,plain,
! [X0] :
( ~ is_aligned(sK4_skl,X0)
| hazard_of_mortality(sK4_skl,sK8_skl) = mod1
| ~ positional_advantage(sK4_skl,sK8_skl)
| has_immunity(sK4_skl,sK8_skl)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1481,f1367]) ).
fof(f3167,plain,
! [X0,X1,X2] :
( dissimilar(sK4_skl,X1,X2)
| ~ greater(age(sK4_skl,X2),sigma)
| age(sK4_skl,X1) != zero
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1481,f1285]) ).
fof(f3169,plain,
! [X0,X1] :
( hazard_of_mortality(sK4_skl,X1) = mod2
| positional_advantage(sK4_skl,X1)
| ~ is_aligned(sK4_skl,X1)
| has_immunity(sK4_skl,X1)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1481,f585]) ).
fof(f3171,plain,
! [X0,X1] :
( ~ is_aligned(sK4_skl,X0)
| ~ is_aligned(sK4_skl,X1)
| dissimilar(sK4_skl,sK8_skl,X1)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1481,f450]) ).
fof(f3172,plain,
! [X0] :
( ~ is_aligned(sK4_skl,X0)
| age(sK4_skl,sK8_skl) != zero
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1481,f425]) ).
fof(f3174,definition,
( sQ218_spl
<=> age(sK4_skl,sK8_skl) = zero ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f3180,definition,
( sQ220_spl
<=> is_aligned(sK4_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f3184,definition,
! [X1,X2] :
( sQ221_spl
<=> ( ~ dissimilar(sK4_skl,sK8_skl,X2)
| ~ is_aligned(sK4_skl,X1)
| ~ dissimilar(sK4_skl,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f3187,plain,
( sQ221_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f3161,f2179,f3184]) ).
fof(f3194,plain,
( sQ157_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f3165,f841,f2151]) ).
fof(f3195,definition,
( sQ223_spl
<=> has_immunity(sK4_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f3196,plain,
( ~ sQ223_spl
| has_immunity(sK4_skl,sK8_skl) ),
inference(component_clause,[status(thm)],[f3195]) ).
fof(f3198,definition,
( sQ224_spl
<=> positional_advantage(sK4_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f3199,plain,
( ~ sQ224_spl
| positional_advantage(sK4_skl,sK8_skl) ),
inference(component_clause,[status(thm)],[f3198]) ).
fof(f3200,plain,
( sQ224_spl
| ~ positional_advantage(sK4_skl,sK8_skl) ),
inference(component_clause,[status(thm)],[f3198]) ).
fof(f3201,plain,
( sQ148_spl
| ~ sQ224_spl
| sQ223_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f3166,f2179,f3195,f3198,f1942]) ).
fof(f3202,plain,
( sQ159_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f3167,f841,f2159]) ).
fof(f3207,plain,
( sQ161_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f3169,f841,f2167]) ).
fof(f3208,definition,
( sQ226_spl
<=> hazard_of_mortality(sK4_skl,sK8_skl) = high ),
introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition]) ).
fof(f3209,plain,
( ~ sQ226_spl
| hazard_of_mortality(sK4_skl,sK8_skl) = high ),
inference(component_clause,[status(thm)],[f3208]) ).
fof(f3212,definition,
! [X1] :
( sQ227_spl
<=> ( ~ is_aligned(sK4_skl,X1)
| dissimilar(sK4_skl,sK8_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f3215,plain,
( sQ227_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f3171,f2179,f3212]) ).
fof(f3216,plain,
( ~ sQ218_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f3172,f2179,f3174]) ).
fof(f3223,plain,
! [X0] :
( sigma = age(sK4_skl,sK8_skl)
| dissimilar(sK4_skl,X0,sK8_skl)
| age(sK4_skl,X0) != zero ),
inference(resolution,[status(thm)],[f1482,f141]) ).
fof(f3241,definition,
! [X0] :
( sQ229_spl
<=> ( dissimilar(sK4_skl,X0,sK8_skl)
| age(sK4_skl,X0) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f3244,plain,
( sQ34_spl
| sQ229_spl ),
inference(split_clause,[status(thm)],[f3223,f3241,f455]) ).
fof(f3367,plain,
! [X0] :
( hazard_of_mortality(sK4_skl,X0) = very_low
| ~ organization(sK4_skl)
| hazard_of_mortality(sK4_skl,X0) = mod2
| hazard_of_mortality(sK4_skl,X0) = low
| ~ is_aligned(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f2420,f83]) ).
fof(f3368,plain,
! [X0] :
( has_endowment(sK4_skl)
| ~ organization(sK4_skl)
| hazard_of_mortality(sK4_skl,X0) = mod2
| hazard_of_mortality(sK4_skl,X0) = low
| ~ is_aligned(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f2420,f55]) ).
fof(f3375,definition,
! [X0] :
( sQ232_spl
<=> ( hazard_of_mortality(sK4_skl,X0) = very_low
| hazard_of_mortality(sK4_skl,X0) = mod2
| hazard_of_mortality(sK4_skl,X0) = low
| ~ is_aligned(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f3378,plain,
( ~ sQ40_spl
| sQ232_spl ),
inference(split_clause,[status(thm)],[f3367,f3375,f603]) ).
fof(f3379,definition,
! [X0] :
( sQ233_spl
<=> ( hazard_of_mortality(sK4_skl,X0) = mod2
| hazard_of_mortality(sK4_skl,X0) = low
| ~ is_aligned(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f3382,plain,
( sQ53_spl
| ~ sQ40_spl
| sQ233_spl ),
inference(split_clause,[status(thm)],[f3368,f3379,f603,f659]) ).
fof(f3390,plain,
( ~ sQ223_spl
| has_endowment(sK4_skl)
| ~ organization(sK4_skl) ),
inference(resolution,[status(thm)],[f3196,f55]) ).
fof(f3395,plain,
( ~ sQ223_spl
| sQ53_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f3390,f603,f659,f3195]) ).
fof(f3426,plain,
( ~ sQ145_spl
| ~ sQ226_spl
| high = mod2 ),
inference(forward_demodulation,[status(thm)],[f3209,f1836]) ).
fof(f3427,plain,
( ~ sQ145_spl
| ~ sQ226_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3426,f193]) ).
fof(f3428,plain,
( ~ sQ145_spl
| ~ sQ226_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f3427]) ).
fof(f3439,definition,
( sQ235_spl
<=> smaller_or_equal(mod2,mod2) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f3441,plain,
( sQ235_spl
| ~ smaller_or_equal(mod2,mod2) ),
inference(component_clause,[status(thm)],[f3439]) ).
fof(f3443,plain,
( sQ235_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3441,f118]) ).
fof(f3444,plain,
sQ235_spl,
inference(contradiction_clause,[status(thm)],[f3443]) ).
fof(f3469,plain,
( sQ1_spl
| ~ sQ2_spl
| ~ sQ59_spl
| ~ sQ148_spl
| ~ smaller(mod1,mod2) ),
inference(backward_demodulation,[status(thm)],[f1943,f1831]) ).
fof(f3475,plain,
( sQ1_spl
| ~ sQ2_spl
| ~ sQ59_spl
| ~ sQ148_spl
| ~ greater(mod2,mod1) ),
inference(resolution,[status(thm)],[f3469,f35]) ).
fof(f3478,plain,
( sQ1_spl
| ~ sQ2_spl
| ~ sQ59_spl
| ~ sQ148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3475,f93]) ).
fof(f3479,plain,
( sQ1_spl
| ~ sQ2_spl
| ~ sQ59_spl
| ~ sQ148_spl ),
inference(contradiction_clause,[status(thm)],[f3478]) ).
fof(f3488,plain,
( sQ0_spl
| ~ sQ44_spl
| ~ greater(hazard_of_mortality(sK4_skl,sK8_skl),low) ),
inference(resolution,[status(thm)],[f1215,f35]) ).
fof(f3588,plain,
( ~ sQ48_spl
| ~ sQ164_spl
| age(sK4_skl,sK5_skl) != zero ),
inference(resolution,[status(thm)],[f2180,f638]) ).
fof(f3597,plain,
( ~ sQ48_spl
| ~ sQ164_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f3588,f852,f2179,f637]) ).
fof(f3631,plain,
( ~ sQ224_spl
| hazard_of_mortality(sK4_skl,sK8_skl) = low
| ~ is_aligned(sK4_skl,sK8_skl)
| has_immunity(sK4_skl,sK8_skl) ),
inference(resolution,[status(thm)],[f3199,f882]) ).
fof(f3632,plain,
( ~ sQ224_spl
| ~ smaller_or_equal(age(sK4_skl,sK8_skl),tau)
| ~ robust_position(sK4_skl) ),
inference(resolution,[status(thm)],[f3199,f75]) ).
fof(f3633,plain,
( ~ sQ224_spl
| sQ101_spl
| ~ sQ220_spl
| sQ223_spl ),
inference(split_clause,[status(thm)],[f3631,f3195,f3180,f1291,f3198]) ).
fof(f3634,definition,
( sQ241_spl
<=> smaller_or_equal(age(sK4_skl,sK8_skl),tau) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f3637,plain,
( ~ sQ224_spl
| ~ sQ241_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f3632,f620,f3634,f3198]) ).
fof(f3639,plain,
( sQ224_spl
| greater(tau,age(sK4_skl,sK8_skl))
| tau = age(sK4_skl,sK8_skl) ),
inference(resolution,[status(thm)],[f3200,f590]) ).
fof(f3641,definition,
( sQ242_spl
<=> tau = age(sK4_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition]) ).
fof(f3642,plain,
( ~ sQ242_spl
| tau = age(sK4_skl,sK8_skl) ),
inference(component_clause,[status(thm)],[f3641]) ).
fof(f3644,definition,
( sQ243_spl
<=> greater(tau,age(sK4_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f3645,plain,
( ~ sQ243_spl
| greater(tau,age(sK4_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f3644]) ).
fof(f3647,plain,
( sQ224_spl
| sQ243_spl
| sQ242_spl ),
inference(split_clause,[status(thm)],[f3639,f3641,f3644,f3198]) ).
fof(f3674,plain,
( sQ0_spl
| ~ sQ44_spl
| ~ sQ148_spl
| ~ greater(mod1,low) ),
inference(backward_demodulation,[status(thm)],[f1943,f3488]) ).
fof(f3677,plain,
( sQ0_spl
| ~ sQ44_spl
| ~ sQ148_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3674,f89]) ).
fof(f3678,plain,
( sQ0_spl
| ~ sQ44_spl
| ~ sQ148_spl ),
inference(contradiction_clause,[status(thm)],[f3677]) ).
fof(f3684,plain,
( ~ sQ242_spl
| greater(tau,sigma) ),
inference(backward_demodulation,[status(thm)],[f3642,f106]) ).
fof(f3692,plain,
( ~ sQ242_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3684,f122]) ).
fof(f3693,plain,
~ sQ242_spl,
inference(contradiction_clause,[status(thm)],[f3692]) ).
fof(f3712,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| ~ sQ226_spl
| greater(high,low) ),
inference(forward_demodulation,[status(thm)],[f3209,f1566]) ).
fof(f3715,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| ~ sQ226_spl
| ~ greater(low,high) ),
inference(forward_demodulation,[status(thm)],[f3209,f1582]) ).
fof(f3731,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| ~ sQ226_spl
| ~ greater(low,high)
| ~ greater(low,high) ),
inference(resolution,[status(thm)],[f3712,f491]) ).
fof(f3738,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| ~ sQ226_spl
| ~ sQ189_spl ),
inference(split_clause,[status(thm)],[f3731,f2508,f3208,f616,f108]) ).
fof(f3740,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| ~ sQ226_spl
| greater(high,low)
| high = low ),
inference(resolution,[status(thm)],[f3715,f139]) ).
fof(f3742,plain,
( ~ sQ0_spl
| ~ sQ44_spl
| ~ sQ226_spl
| sQ143_spl
| sQ142_spl ),
inference(split_clause,[status(thm)],[f3740,f1820,f1823,f3208,f616,f108]) ).
fof(f3772,plain,
( ~ sQ243_spl
| ~ greater(age(sK4_skl,sK8_skl),sigma) ),
inference(resolution,[status(thm)],[f3645,f133]) ).
fof(f3781,plain,
( ~ sQ243_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3772,f106]) ).
fof(f3782,plain,
~ sQ243_spl,
inference(contradiction_clause,[status(thm)],[f3781]) ).
fof(f3783,plain,
$false,
inference(sat_refutation,[status(thm)],[f117,f156,f163,f197,f204,f225,f239,f246,f260,f286,f300,f394,f413,f433,f440,f444,f461,f465,f471,f524,f533,f615,f626,f628,f630,f651,f662,f664,f671,f688,f690,f694,f699,f727,f739,f760,f798,f802,f806,f810,f814,f830,f847,f858,f861,f887,f896,f920,f964,f1012,f1134,f1158,f1181,f1207,f1212,f1214,f1352,f1359,f1362,f1523,f1534,f1570,f1584,f1590,f1592,f1611,f1739,f1751,f1764,f1779,f1868,f1964,f2007,f2017,f2028,f2056,f2079,f2194,f2255,f2345,f2406,f2487,f2491,f2496,f2497,f2498,f2502,f2507,f2515,f2519,f2520,f2535,f2647,f2659,f2662,f2696,f2787,f2830,f2879,f2979,f3036,f3187,f3194,f3201,f3202,f3207,f3215,f3216,f3244,f3378,f3382,f3395,f3428,f3444,f3479,f3597,f3633,f3637,f3647,f3678,f3693,f3738,f3742,f3782]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT064+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 01:22:35 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 3.84/0.94 % Refutation found
% 3.84/0.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.84/0.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.84/0.97 % Elapsed time: 0.597841 seconds
% 3.84/0.97 % CPU time: 4.360656 seconds
% 3.84/0.97 % Total memory used: 146.297 MB
% 3.84/0.97 % Net memory used: 140.498 MB
%------------------------------------------------------------------------------