%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT061+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 : n004.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:30 PM UTC 2026
% Result : Theorem 0.73s 0.63s
% Output : CNFRefutation 0.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 33
% Syntax : Number of formulae : 166 ( 21 unt; 21 def)
% Number of atoms : 545 ( 70 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 628 ( 249 ~; 253 |; 80 &)
% ( 30 <=>; 15 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 22 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-2 aty)
% Number of variables : 150 ( 143 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( smaller_or_equal(X,Y)
<=> ( X = Y
| smaller(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( smaller(X,Y)
<=> greater(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] :
( ( greater(Y,Z)
& greater(X,Y) )
=> greater(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,T] :
( ( ~ has_endowment(X)
& organization(X) )
=> ~ has_immunity(X,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,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(f9,axiom,
! [X,T] :
( ( age(X,T) = zero
& organization(X) )
=> is_aligned(X,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,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(f11,axiom,
! [X] :
( fragile_position(X)
<=> ! [T] :
( ( greater(age(X,T),sigma)
=> ~ positional_advantage(X,T) )
& ( smaller_or_equal(age(X,T),sigma)
=> positional_advantage(X,T) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,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(f13,axiom,
greater(high,mod1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
greater(mod1,low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,conjecture,
! [X,T0,T1,T2] :
( ( greater(age(X,T2),sigma)
& smaller_or_equal(age(X,T1),sigma)
& greater(sigma,zero)
& age(X,T0) = zero
& ~ has_endowment(X)
& fragile_position(X)
& organization(X) )
=> ( hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)
& greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
~ ! [X,T0,T1,T2] :
( ( greater(age(X,T2),sigma)
& smaller_or_equal(age(X,T1),sigma)
& greater(sigma,zero)
& age(X,T0) = zero
& ~ has_endowment(X)
& fragile_position(X)
& organization(X) )
=> ( hazard_of_mortality(X,T1) = hazard_of_mortality(X,T0)
& greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,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(f21,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)],[f20]) ).
fof(f23,plain,
! [X0,X1] :
( ~ smaller(X0,X1)
| smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f30,plain,
! [X,Y] :
( ( ~ greater(Y,X)
| smaller(X,Y) )
& ( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f31,plain,
( ! [X,Y] :
( ~ greater(Y,X)
| smaller(X,Y) )
& ! [X,Y] :
( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(miniscoping,[status(thm)],[f30]) ).
fof(f33,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f36,plain,
! [X,Y,Z] :
( greater(X,Z)
| ~ greater(Y,Z)
| ~ greater(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f37,plain,
! [X,Z] :
( greater(X,Z)
| ! [Y] :
( ~ greater(Y,Z)
| ~ greater(X,Y) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f38,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f40,plain,
! [X,T] :
( ~ has_immunity(X,T)
| has_endowment(X)
| ~ organization(X) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f41,plain,
! [X] :
( ! [T] : ~ has_immunity(X,T)
| has_endowment(X)
| ~ organization(X) ),
inference(miniscoping,[status(thm)],[f40]) ).
fof(f42,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| has_endowment(X0)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f43,plain,
! [X,T0,T] :
( dissimilar(X,T0,T)
<=> ( ( is_aligned(X,T0)
<~> is_aligned(X,T) )
& organization(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f44,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)],[f43]) ).
fof(f45,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)],[f44]) ).
fof(f46,plain,
! [X0,X1,X2] :
( organization(X0)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f48,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f49,plain,
! [X0,X1,X2] :
( is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ organization(X0)
| dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f51,plain,
! [X,T] :
( is_aligned(X,T)
| age(X,T) != zero
| ~ organization(X) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f52,plain,
! [X0,X1] :
( is_aligned(X0,X1)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f53,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)],[f10]) ).
fof(f54,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)],[f53]) ).
fof(f55,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)],[f54]) ).
fof(f56,plain,
! [X0,X1,X2] :
( dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [X0,X1,X2] :
( ~ dissimilar(X0,X1,X2)
| greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f58,plain,
! [X] :
( fragile_position(X)
<=> ! [T] :
( ( ~ positional_advantage(X,T)
| ~ greater(age(X,T),sigma) )
& ( positional_advantage(X,T)
| ~ smaller_or_equal(age(X,T),sigma) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f59,plain,
! [X] :
( ( ? [T] :
( ( positional_advantage(X,T)
& greater(age(X,T),sigma) )
| ( ~ positional_advantage(X,T)
& smaller_or_equal(age(X,T),sigma) ) )
| fragile_position(X) )
& ( ! [T] :
( ( ~ positional_advantage(X,T)
| ~ greater(age(X,T),sigma) )
& ( positional_advantage(X,T)
| ~ smaller_or_equal(age(X,T),sigma) ) )
| ~ fragile_position(X) ) ),
inference(NNF_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
( ! [X] :
( ? [T] :
( positional_advantage(X,T)
& greater(age(X,T),sigma) )
| ? [T] :
( ~ positional_advantage(X,T)
& smaller_or_equal(age(X,T),sigma) )
| fragile_position(X) )
& ! [X] :
( ( ! [T] :
( ~ positional_advantage(X,T)
| ~ greater(age(X,T),sigma) )
& ! [T] :
( positional_advantage(X,T)
| ~ smaller_or_equal(age(X,T),sigma) ) )
| ~ fragile_position(X) ) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f61,plain,
( ! [X] :
( ( positional_advantage(X,sK1_skl(X))
& greater(age(X,sK1_skl(X)),sigma) )
| ( ~ positional_advantage(X,sK0_skl(X))
& smaller_or_equal(age(X,sK0_skl(X)),sigma) )
| fragile_position(X) )
& ! [X] :
( ( ! [T] :
( ~ positional_advantage(X,T)
| ~ greater(age(X,T),sigma) )
& ! [T] :
( positional_advantage(X,T)
| ~ smaller_or_equal(age(X,T),sigma) ) )
| ~ fragile_position(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(T,sK0_skl(X)),skolemize(T,sK1_skl(X))],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( positional_advantage(X0,X1)
| ~ smaller_or_equal(age(X0,X1),sigma)
| ~ fragile_position(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| ~ greater(age(X0,X1),sigma)
| ~ fragile_position(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f68,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)],[f12]) ).
fof(f69,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)],[f68]) ).
fof(f71,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)],[f69]) ).
fof(f74,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)],[f69]) ).
fof(f75,plain,
greater(high,mod1),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f76,plain,
greater(mod1,low),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f80,plain,
? [X,T0,T1,T2] :
( ( hazard_of_mortality(X,T1) != hazard_of_mortality(X,T0)
| ~ greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)) )
& greater(age(X,T2),sigma)
& smaller_or_equal(age(X,T1),sigma)
& greater(sigma,zero)
& age(X,T0) = zero
& ~ has_endowment(X)
& fragile_position(X)
& organization(X) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f81,plain,
( ( hazard_of_mortality(sK2_skl,sK4_skl) != hazard_of_mortality(sK2_skl,sK3_skl)
| ~ greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)) )
& greater(age(sK2_skl,sK5_skl),sigma)
& smaller_or_equal(age(sK2_skl,sK4_skl),sigma)
& greater(sigma,zero)
& age(sK2_skl,sK3_skl) = zero
& ~ has_endowment(sK2_skl)
& fragile_position(sK2_skl)
& organization(sK2_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(X,sK2_skl),skolemize(T0,sK3_skl),skolemize(T1,sK4_skl),skolemize(T2,sK5_skl)],[f80]) ).
fof(f82,plain,
organization(sK2_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
fragile_position(sK2_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f84,plain,
~ has_endowment(sK2_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f85,plain,
age(sK2_skl,sK3_skl) = zero,
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f86,plain,
greater(sigma,zero),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f87,plain,
smaller_or_equal(age(sK2_skl,sK4_skl),sigma),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f88,plain,
greater(age(sK2_skl,sK5_skl),sigma),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f89,plain,
( hazard_of_mortality(sK2_skl,sK4_skl) != hazard_of_mortality(sK2_skl,sK3_skl)
| ~ greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f90,definition,
( sQ0_spl
<=> greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f92,plain,
( sQ0_spl
| ~ greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK4_skl)) ),
inference(component_clause,[status(thm)],[f90]) ).
fof(f93,definition,
( sQ1_spl
<=> hazard_of_mortality(sK2_skl,sK4_skl) = hazard_of_mortality(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f94,plain,
( ~ sQ1_spl
| hazard_of_mortality(sK2_skl,sK4_skl) = hazard_of_mortality(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f93]) ).
fof(f95,plain,
( sQ1_spl
| hazard_of_mortality(sK2_skl,sK4_skl) != hazard_of_mortality(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f93]) ).
fof(f96,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f89,f90,f93]) ).
fof(f103,plain,
! [X0] :
( greater(X0,low)
| ~ greater(X0,mod1) ),
inference(resolution,[status(thm)],[f76,f38]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ~ dissimilar(X0,X1,X2)
| greater(age(X0,X2),sigma)
| age(X0,X1) != zero ),
inference(backward_subsumption_resolution,[status(thm)],[f57,f46]) ).
fof(f138,definition,
( sQ4_spl
<=> organization(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f140,plain,
( sQ4_spl
| ~ organization(sK2_skl) ),
inference(component_clause,[status(thm)],[f138]) ).
fof(f142,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f140,f82]) ).
fof(f143,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f142]) ).
fof(f156,plain,
! [X0] :
( ~ positional_advantage(sK2_skl,X0)
| ~ greater(age(sK2_skl,X0),sigma) ),
inference(resolution,[status(thm)],[f63,f83]) ).
fof(f396,plain,
! [X0] :
( positional_advantage(sK2_skl,X0)
| ~ smaller_or_equal(age(sK2_skl,X0),sigma) ),
inference(resolution,[status(thm)],[f62,f83]) ).
fof(f440,plain,
! [X0] :
( dissimilar(sK2_skl,X0,sK5_skl)
| age(sK2_skl,X0) != zero
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f88,f56]) ).
fof(f443,definition,
! [X0] :
( sQ38_spl
<=> ( dissimilar(sK2_skl,X0,sK5_skl)
| age(sK2_skl,X0) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f444,plain,
! [X0] :
( ~ sQ38_spl
| dissimilar(sK2_skl,X0,sK5_skl)
| age(sK2_skl,X0) != zero ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f446,plain,
( sQ38_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f440,f138,f443]) ).
fof(f572,plain,
positional_advantage(sK2_skl,sK4_skl),
inference(resolution,[status(thm)],[f396,f87]) ).
fof(f576,plain,
( positional_advantage(sK2_skl,sK3_skl)
| ~ smaller_or_equal(zero,sigma) ),
inference(paramodulation,[status(thm)],[f85,f396]) ).
fof(f582,definition,
( sQ49_spl
<=> smaller_or_equal(zero,sigma) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f584,plain,
( sQ49_spl
| ~ smaller_or_equal(zero,sigma) ),
inference(component_clause,[status(thm)],[f582]) ).
fof(f585,definition,
( sQ50_spl
<=> positional_advantage(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f586,plain,
( ~ sQ50_spl
| positional_advantage(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f585]) ).
fof(f588,plain,
( sQ50_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f576,f582,f585]) ).
fof(f589,plain,
~ greater(age(sK2_skl,sK4_skl),sigma),
inference(resolution,[status(thm)],[f572,f156]) ).
fof(f591,definition,
( sQ51_spl
<=> has_immunity(sK2_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f592,plain,
( ~ sQ51_spl
| has_immunity(sK2_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f591]) ).
fof(f594,definition,
( sQ52_spl
<=> is_aligned(sK2_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f596,plain,
( sQ52_spl
| ~ is_aligned(sK2_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f594]) ).
fof(f597,definition,
( sQ53_spl
<=> hazard_of_mortality(sK2_skl,sK4_skl) = low ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f598,plain,
( ~ sQ53_spl
| hazard_of_mortality(sK2_skl,sK4_skl) = low ),
inference(component_clause,[status(thm)],[f597]) ).
fof(f601,plain,
( sQ49_spl
| ~ smaller(zero,sigma) ),
inference(resolution,[status(thm)],[f584,f23]) ).
fof(f605,definition,
( sQ54_spl
<=> has_immunity(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f606,plain,
( ~ sQ54_spl
| has_immunity(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f605]) ).
fof(f608,definition,
( sQ55_spl
<=> is_aligned(sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f609,plain,
( ~ sQ55_spl
| is_aligned(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f608]) ).
fof(f610,plain,
( sQ55_spl
| ~ is_aligned(sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f608]) ).
fof(f611,definition,
( sQ56_spl
<=> hazard_of_mortality(sK2_skl,sK3_skl) = low ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f612,plain,
( ~ sQ56_spl
| hazard_of_mortality(sK2_skl,sK3_skl) = low ),
inference(component_clause,[status(thm)],[f611]) ).
fof(f618,plain,
! [X0] :
( sQ52_spl
| ~ is_aligned(sK2_skl,X0)
| ~ organization(sK2_skl)
| dissimilar(sK2_skl,X0,sK4_skl) ),
inference(resolution,[status(thm)],[f596,f49]) ).
fof(f636,definition,
! [X0] :
( sQ61_spl
<=> ( ~ is_aligned(sK2_skl,X0)
| dissimilar(sK2_skl,X0,sK4_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f637,plain,
! [X0] :
( ~ sQ61_spl
| ~ is_aligned(sK2_skl,X0)
| dissimilar(sK2_skl,X0,sK4_skl) ),
inference(component_clause,[status(thm)],[f636]) ).
fof(f639,plain,
( sQ52_spl
| ~ sQ4_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f618,f636,f138,f594]) ).
fof(f645,plain,
( ~ sQ51_spl
| has_endowment(sK2_skl)
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f592,f42]) ).
fof(f650,definition,
( sQ64_spl
<=> has_endowment(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f651,plain,
( ~ sQ64_spl
| has_endowment(sK2_skl) ),
inference(component_clause,[status(thm)],[f650]) ).
fof(f653,plain,
( ~ sQ51_spl
| sQ64_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f645,f138,f650,f591]) ).
fof(f654,plain,
( ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f651,f84]) ).
fof(f655,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f654]) ).
fof(f657,plain,
( sQ49_spl
| ~ greater(sigma,zero) ),
inference(resolution,[status(thm)],[f601,f33]) ).
fof(f660,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f86]) ).
fof(f661,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f660]) ).
fof(f668,plain,
( sQ55_spl
| age(sK2_skl,sK3_skl) != zero
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f610,f52]) ).
fof(f685,definition,
( sQ69_spl
<=> age(sK2_skl,sK3_skl) = zero ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f687,plain,
( sQ69_spl
| age(sK2_skl,sK3_skl) != zero ),
inference(component_clause,[status(thm)],[f685]) ).
fof(f688,plain,
( sQ55_spl
| ~ sQ69_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f668,f138,f685,f608]) ).
fof(f689,plain,
( sQ69_spl
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f85,f687]) ).
fof(f690,plain,
( sQ69_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f689]) ).
fof(f691,plain,
sQ69_spl,
inference(contradiction_clause,[status(thm)],[f690]) ).
fof(f693,plain,
( ~ sQ54_spl
| has_endowment(sK2_skl)
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f606,f42]) ).
fof(f698,plain,
( ~ sQ54_spl
| sQ64_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f693,f138,f650,f605]) ).
fof(f722,definition,
! [X0] :
( sQ72_spl
<=> ( ~ is_aligned(sK2_skl,X0)
| age(sK2_skl,X0) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f723,plain,
! [X0] :
( ~ sQ72_spl
| ~ is_aligned(sK2_skl,X0)
| age(sK2_skl,X0) != zero ),
inference(component_clause,[status(thm)],[f722]) ).
fof(f742,plain,
( sQ1_spl
| ~ sQ53_spl
| low != hazard_of_mortality(sK2_skl,sK3_skl) ),
inference(backward_demodulation,[status(thm)],[f598,f95]) ).
fof(f743,plain,
( sQ1_spl
| ~ sQ53_spl
| ~ sQ56_spl
| low != low ),
inference(forward_demodulation,[status(thm)],[f612,f742]) ).
fof(f744,plain,
( sQ1_spl
| ~ sQ53_spl
| ~ sQ56_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f743]) ).
fof(f745,plain,
( sQ1_spl
| ~ sQ53_spl
| ~ sQ56_spl ),
inference(contradiction_clause,[status(thm)],[f744]) ).
fof(f826,plain,
! [X0] :
( ~ sQ38_spl
| ~ is_aligned(sK2_skl,sK5_skl)
| ~ is_aligned(sK2_skl,X0)
| age(sK2_skl,X0) != zero ),
inference(resolution,[status(thm)],[f444,f48]) ).
fof(f828,definition,
( sQ82_spl
<=> is_aligned(sK2_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f830,plain,
( sQ82_spl
| ~ is_aligned(sK2_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f828]) ).
fof(f831,plain,
( ~ sQ38_spl
| ~ sQ82_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f826,f722,f828,f443]) ).
fof(f904,plain,
( sQ82_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = high
| positional_advantage(sK2_skl,sK5_skl)
| has_immunity(sK2_skl,sK5_skl)
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f830,f74]) ).
fof(f910,definition,
( sQ88_spl
<=> has_immunity(sK2_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f911,plain,
( ~ sQ88_spl
| has_immunity(sK2_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f910]) ).
fof(f913,definition,
( sQ89_spl
<=> positional_advantage(sK2_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f914,plain,
( ~ sQ89_spl
| positional_advantage(sK2_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f913]) ).
fof(f916,definition,
( sQ90_spl
<=> hazard_of_mortality(sK2_skl,sK5_skl) = high ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f917,plain,
( ~ sQ90_spl
| hazard_of_mortality(sK2_skl,sK5_skl) = high ),
inference(component_clause,[status(thm)],[f916]) ).
fof(f919,plain,
( sQ82_spl
| sQ90_spl
| sQ89_spl
| sQ88_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f904,f138,f910,f913,f916,f828]) ).
fof(f940,plain,
! [X0] :
( hazard_of_mortality(sK2_skl,X0) = low
| ~ positional_advantage(sK2_skl,X0)
| ~ is_aligned(sK2_skl,X0)
| has_immunity(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f71,f82]) ).
fof(f945,plain,
( ~ sQ88_spl
| has_endowment(sK2_skl)
| ~ organization(sK2_skl) ),
inference(resolution,[status(thm)],[f911,f42]) ).
fof(f950,plain,
( ~ sQ88_spl
| sQ64_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f945,f138,f650,f910]) ).
fof(f974,plain,
! [X0] :
( ~ sQ61_spl
| greater(age(sK2_skl,sK4_skl),sigma)
| age(sK2_skl,X0) != zero
| ~ is_aligned(sK2_skl,X0) ),
inference(resolution,[status(thm)],[f637,f122]) ).
fof(f980,definition,
( sQ96_spl
<=> greater(age(sK2_skl,sK4_skl),sigma) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f981,plain,
( ~ sQ96_spl
| greater(age(sK2_skl,sK4_skl),sigma) ),
inference(component_clause,[status(thm)],[f980]) ).
fof(f983,plain,
( ~ sQ61_spl
| sQ96_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f974,f722,f980,f636]) ).
fof(f1144,plain,
( ~ sQ50_spl
| hazard_of_mortality(sK2_skl,sK3_skl) = low
| ~ is_aligned(sK2_skl,sK3_skl)
| has_immunity(sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f940,f586]) ).
fof(f1145,plain,
( hazard_of_mortality(sK2_skl,sK4_skl) = low
| ~ is_aligned(sK2_skl,sK4_skl)
| has_immunity(sK2_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f940,f572]) ).
fof(f1148,plain,
( ~ sQ50_spl
| sQ56_spl
| ~ sQ55_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1144,f605,f608,f611,f585]) ).
fof(f1149,plain,
( sQ53_spl
| ~ sQ52_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1145,f591,f594,f597]) ).
fof(f1342,plain,
greater(high,low),
inference(resolution,[status(thm)],[f103,f75]) ).
fof(f2227,plain,
( ~ sQ55_spl
| ~ sQ72_spl
| age(sK2_skl,sK3_skl) != zero ),
inference(resolution,[status(thm)],[f723,f609]) ).
fof(f2239,plain,
( ~ sQ55_spl
| ~ sQ72_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f2227,f685,f722,f608]) ).
fof(f2258,plain,
( ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f981,f589]) ).
fof(f2259,plain,
~ sQ96_spl,
inference(contradiction_clause,[status(thm)],[f2258]) ).
fof(f2337,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ greater(hazard_of_mortality(sK2_skl,sK5_skl),hazard_of_mortality(sK2_skl,sK3_skl)) ),
inference(forward_demodulation,[status(thm)],[f94,f92]) ).
fof(f2406,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ sQ53_spl
| ~ greater(hazard_of_mortality(sK2_skl,sK5_skl),low) ),
inference(backward_demodulation,[status(thm)],[f2408,f2337]) ).
fof(f2408,plain,
( ~ sQ53_spl
| ~ sQ1_spl
| hazard_of_mortality(sK2_skl,sK3_skl) = low ),
inference(forward_demodulation,[status(thm)],[f94,f598]) ).
fof(f2428,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ sQ53_spl
| ~ sQ90_spl
| ~ greater(high,low) ),
inference(forward_demodulation,[status(thm)],[f917,f2406]) ).
fof(f2429,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ sQ53_spl
| ~ sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2428,f1342]) ).
fof(f2430,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ sQ53_spl
| ~ sQ90_spl ),
inference(contradiction_clause,[status(thm)],[f2429]) ).
fof(f2495,plain,
( ~ sQ89_spl
| ~ greater(age(sK2_skl,sK5_skl),sigma) ),
inference(resolution,[status(thm)],[f914,f156]) ).
fof(f2496,plain,
( ~ sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2495,f88]) ).
fof(f2497,plain,
~ sQ89_spl,
inference(contradiction_clause,[status(thm)],[f2496]) ).
fof(f2498,plain,
$false,
inference(sat_refutation,[status(thm)],[f96,f143,f446,f588,f639,f653,f655,f661,f688,f691,f698,f745,f831,f919,f950,f983,f1148,f1149,f2239,f2259,f2430,f2497]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT061+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 : n004.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:24:19 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.73/0.63 % Refutation found
% 0.73/0.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.73/0.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.73/0.66 % Elapsed time: 0.282034 seconds
% 0.73/0.66 % CPU time: 1.928243 seconds
% 0.73/0.66 % Total memory used: 126.245 MB
% 0.73/0.66 % Net memory used: 123.062 MB
%------------------------------------------------------------------------------