%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT060+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 : n018.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.14s 0.39s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 33
% Syntax : Number of formulae : 166 ( 24 unt; 23 def)
% Number of atoms : 479 ( 103 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 493 ( 180 ~; 249 |; 30 &)
% ( 24 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 24 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 81 ( 78 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X,Y] :
( smaller(X,Y)
<=> greater(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
~ ( greater(Y,X)
& greater(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] :
( ( greater(Y,Z)
& greater(X,Y) )
=> greater(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] :
( greater(X,Y)
| X = Y
| smaller(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,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(f8,axiom,
greater(high,mod1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
greater(mod1,low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
greater(low,very_low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
greater(mod2,low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,conjecture,
! [X,T0,T] :
( ( ~ has_immunity(X,T)
& has_immunity(X,T0)
& organization(X) )
=> greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
~ ! [X,T0,T] :
( ( ~ has_immunity(X,T)
& has_immunity(X,T0)
& organization(X) )
=> greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0)) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f25,plain,
! [X,Y] :
( ( ~ greater(Y,X)
| smaller(X,Y) )
& ( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f26,plain,
( ! [X,Y] :
( ~ greater(Y,X)
| smaller(X,Y) )
& ! [X,Y] :
( greater(Y,X)
| ~ smaller(X,Y) ) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f27,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f29,plain,
! [X,Y] :
( ~ greater(Y,X)
| ~ greater(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f30,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f31,plain,
! [X,Y,Z] :
( greater(X,Z)
| ~ greater(Y,Z)
| ~ greater(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f32,plain,
! [X,Z] :
( greater(X,Z)
| ! [Y] :
( ~ greater(Y,Z)
| ~ greater(X,Y) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f33,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f34,plain,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f35,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)],[f7]) ).
fof(f36,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)],[f35]) ).
fof(f37,plain,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = very_low
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,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)],[f36]) ).
fof(f39,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)],[f36]) ).
fof(f40,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)],[f36]) ).
fof(f41,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)],[f36]) ).
fof(f42,plain,
greater(high,mod1),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f43,plain,
greater(mod1,low),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f44,plain,
greater(low,very_low),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f46,plain,
greater(mod2,low),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f47,plain,
? [X,T0,T] :
( ~ greater(hazard_of_mortality(X,T),hazard_of_mortality(X,T0))
& ~ has_immunity(X,T)
& has_immunity(X,T0)
& organization(X) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f48,plain,
( ~ greater(hazard_of_mortality(sK0_skl,sK2_skl),hazard_of_mortality(sK0_skl,sK1_skl))
& ~ has_immunity(sK0_skl,sK2_skl)
& has_immunity(sK0_skl,sK1_skl)
& organization(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(X,sK0_skl),skolemize(T0,sK1_skl),skolemize(T,sK2_skl)],[f47]) ).
fof(f49,plain,
organization(sK0_skl),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
has_immunity(sK0_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f51,plain,
~ has_immunity(sK0_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f52,plain,
~ greater(hazard_of_mortality(sK0_skl,sK2_skl),hazard_of_mortality(sK0_skl,sK1_skl)),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f56,plain,
~ greater(mod1,high),
inference(resolution,[status(thm)],[f42,f30]) ).
fof(f57,plain,
! [X0] :
( greater(X0,low)
| ~ greater(X0,mod1) ),
inference(resolution,[status(thm)],[f43,f33]) ).
fof(f58,plain,
~ greater(low,mod1),
inference(resolution,[status(thm)],[f43,f30]) ).
fof(f59,plain,
! [X0] :
( greater(X0,very_low)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f44,f33]) ).
fof(f60,plain,
~ greater(very_low,low),
inference(resolution,[status(thm)],[f44,f30]) ).
fof(f63,plain,
! [X0] :
( greater(X0,low)
| ~ greater(X0,mod2) ),
inference(resolution,[status(thm)],[f46,f33]) ).
fof(f64,plain,
~ greater(low,mod2),
inference(resolution,[status(thm)],[f46,f30]) ).
fof(f68,plain,
greater(high,low),
inference(resolution,[status(thm)],[f57,f42]) ).
fof(f70,plain,
~ greater(low,high),
inference(resolution,[status(thm)],[f68,f30]) ).
fof(f95,plain,
! [X0,X1] :
( greater(X1,X0)
| greater(X0,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f34,f27]) ).
fof(f99,plain,
( greater(low,very_low)
| low = very_low ),
inference(resolution,[status(thm)],[f95,f60]) ).
fof(f102,plain,
( greater(high,low)
| high = low ),
inference(resolution,[status(thm)],[f95,f70]) ).
fof(f103,plain,
( greater(mod2,low)
| mod2 = low ),
inference(resolution,[status(thm)],[f95,f64]) ).
fof(f104,plain,
( greater(mod1,low)
| mod1 = low ),
inference(resolution,[status(thm)],[f95,f58]) ).
fof(f109,plain,
! [X0] :
( greater(X0,low)
| greater(mod2,X0)
| mod2 = X0 ),
inference(resolution,[status(thm)],[f95,f63]) ).
fof(f110,plain,
! [X0] :
( greater(X0,low)
| greater(mod1,X0)
| mod1 = X0 ),
inference(resolution,[status(thm)],[f95,f57]) ).
fof(f124,definition,
( sQ4_spl
<=> low = very_low ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f125,plain,
( ~ sQ4_spl
| low = very_low ),
inference(component_clause,[status(thm)],[f124]) ).
fof(f127,definition,
( sQ5_spl
<=> greater(low,very_low) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f128,plain,
( ~ sQ5_spl
| greater(low,very_low) ),
inference(component_clause,[status(thm)],[f127]) ).
fof(f130,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f99,f124,f127]) ).
fof(f131,definition,
( sQ6_spl
<=> high = low ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f132,plain,
( ~ sQ6_spl
| high = low ),
inference(component_clause,[status(thm)],[f131]) ).
fof(f134,definition,
( sQ7_spl
<=> greater(high,low) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f135,plain,
( ~ sQ7_spl
| greater(high,low) ),
inference(component_clause,[status(thm)],[f134]) ).
fof(f137,plain,
( sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f102,f131,f134]) ).
fof(f138,definition,
( sQ8_spl
<=> mod2 = low ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f139,plain,
( ~ sQ8_spl
| mod2 = low ),
inference(component_clause,[status(thm)],[f138]) ).
fof(f141,definition,
( sQ9_spl
<=> greater(mod2,low) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f142,plain,
( ~ sQ9_spl
| greater(mod2,low) ),
inference(component_clause,[status(thm)],[f141]) ).
fof(f144,plain,
( sQ9_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f103,f138,f141]) ).
fof(f145,definition,
( sQ10_spl
<=> mod1 = low ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f146,plain,
( ~ sQ10_spl
| mod1 = low ),
inference(component_clause,[status(thm)],[f145]) ).
fof(f148,definition,
( sQ11_spl
<=> greater(mod1,low) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f149,plain,
( ~ sQ11_spl
| greater(mod1,low) ),
inference(component_clause,[status(thm)],[f148]) ).
fof(f151,plain,
( sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f104,f145,f148]) ).
fof(f179,plain,
( ~ sQ10_spl
| greater(low,low) ),
inference(backward_demodulation,[status(thm)],[f146,f43]) ).
fof(f183,plain,
( ~ sQ8_spl
| greater(low,low) ),
inference(backward_demodulation,[status(thm)],[f139,f46]) ).
fof(f184,plain,
! [X0] :
( hazard_of_mortality(sK0_skl,X0) = very_low
| ~ has_immunity(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f37,f49]) ).
fof(f188,plain,
hazard_of_mortality(sK0_skl,sK1_skl) = very_low,
inference(resolution,[status(thm)],[f184,f50]) ).
fof(f203,plain,
~ greater(hazard_of_mortality(sK0_skl,sK2_skl),very_low),
inference(forward_demodulation,[status(thm)],[f188,f52]) ).
fof(f213,plain,
( ~ sQ4_spl
| greater(low,low) ),
inference(backward_demodulation,[status(thm)],[f125,f44]) ).
fof(f221,definition,
( sQ19_spl
<=> greater(low,low) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f222,plain,
( ~ sQ19_spl
| greater(low,low) ),
inference(component_clause,[status(thm)],[f221]) ).
fof(f229,plain,
( ~ sQ6_spl
| greater(low,low) ),
inference(forward_demodulation,[status(thm)],[f132,f68]) ).
fof(f261,plain,
( ~ sQ19_spl
| ~ greater(low,low) ),
inference(resolution,[status(thm)],[f222,f30]) ).
fof(f262,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f261,f222]) ).
fof(f263,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f262]) ).
fof(f295,plain,
! [X0] :
( hazard_of_mortality(sK0_skl,X0) = mod1
| ~ positional_advantage(sK0_skl,X0)
| is_aligned(sK0_skl,X0)
| has_immunity(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f39,f49]) ).
fof(f302,plain,
! [X0] :
( hazard_of_mortality(sK0_skl,X0) = low
| ~ positional_advantage(sK0_skl,X0)
| has_immunity(sK0_skl,X0)
| ~ organization(sK0_skl)
| hazard_of_mortality(sK0_skl,X0) = mod1
| ~ positional_advantage(sK0_skl,X0)
| has_immunity(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f295,f38]) ).
fof(f303,definition,
! [X0] :
( sQ22_spl
<=> ( hazard_of_mortality(sK0_skl,X0) = low
| ~ positional_advantage(sK0_skl,X0)
| has_immunity(sK0_skl,X0)
| hazard_of_mortality(sK0_skl,X0) = mod1
| ~ positional_advantage(sK0_skl,X0)
| has_immunity(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f304,plain,
! [X0] :
( ~ sQ22_spl
| hazard_of_mortality(sK0_skl,X0) = low
| ~ positional_advantage(sK0_skl,X0)
| has_immunity(sK0_skl,X0)
| hazard_of_mortality(sK0_skl,X0) = mod1
| ~ positional_advantage(sK0_skl,X0)
| has_immunity(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f303]) ).
fof(f306,definition,
( sQ23_spl
<=> organization(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f308,plain,
( sQ23_spl
| ~ organization(sK0_skl) ),
inference(component_clause,[status(thm)],[f306]) ).
fof(f309,plain,
( ~ sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f302,f303,f306]) ).
fof(f310,plain,
! [X0] :
( ~ sQ22_spl
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| ~ positional_advantage(sK0_skl,X0)
| has_immunity(sK0_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f304]) ).
fof(f313,plain,
( ~ sQ7_spl
| greater(high,very_low) ),
inference(resolution,[status(thm)],[f59,f135]) ).
fof(f314,plain,
( ~ sQ9_spl
| greater(mod2,very_low) ),
inference(resolution,[status(thm)],[f59,f142]) ).
fof(f315,plain,
( ~ sQ11_spl
| greater(mod1,very_low) ),
inference(resolution,[status(thm)],[f59,f149]) ).
fof(f318,plain,
( ~ sQ7_spl
| ~ greater(very_low,high) ),
inference(resolution,[status(thm)],[f313,f30]) ).
fof(f325,plain,
( ~ sQ7_spl
| greater(high,very_low)
| high = very_low ),
inference(resolution,[status(thm)],[f318,f95]) ).
fof(f326,definition,
( sQ24_spl
<=> high = very_low ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f327,plain,
( ~ sQ24_spl
| high = very_low ),
inference(component_clause,[status(thm)],[f326]) ).
fof(f329,definition,
( sQ25_spl
<=> greater(high,very_low) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f330,plain,
( ~ sQ25_spl
| greater(high,very_low) ),
inference(component_clause,[status(thm)],[f329]) ).
fof(f332,plain,
( ~ sQ7_spl
| sQ25_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f325,f326,f329,f134]) ).
fof(f335,plain,
( ~ sQ11_spl
| ~ sQ24_spl
| greater(mod1,high) ),
inference(backward_demodulation,[status(thm)],[f327,f315]) ).
fof(f347,plain,
( ~ sQ11_spl
| ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f335,f56]) ).
fof(f348,plain,
( ~ sQ11_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f347]) ).
fof(f349,plain,
( ~ sQ6_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f229,f221,f131]) ).
fof(f352,plain,
( ~ sQ10_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f179,f221,f145]) ).
fof(f354,plain,
( ~ sQ8_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f183,f221,f138]) ).
fof(f381,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f308,f49]) ).
fof(f382,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f381]) ).
fof(f384,definition,
( sQ27_spl
<=> low = hazard_of_mortality(sK0_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f385,plain,
( ~ sQ27_spl
| low = hazard_of_mortality(sK0_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f384]) ).
fof(f431,definition,
( sQ30_spl
<=> mod1 = very_low ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f432,plain,
( ~ sQ30_spl
| mod1 = very_low ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f434,definition,
( sQ31_spl
<=> greater(mod1,very_low) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( ~ sQ31_spl
| greater(mod1,very_low) ),
inference(component_clause,[status(thm)],[f434]) ).
fof(f442,plain,
( ~ sQ5_spl
| ~ sQ30_spl
| greater(low,mod1) ),
inference(backward_demodulation,[status(thm)],[f432,f128]) ).
fof(f450,plain,
( ~ sQ5_spl
| ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f442,f58]) ).
fof(f451,plain,
( ~ sQ5_spl
| ~ sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f450]) ).
fof(f452,plain,
( ~ sQ4_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f213,f221,f124]) ).
fof(f462,definition,
( sQ32_spl
<=> mod2 = very_low ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( ~ sQ32_spl
| mod2 = very_low ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,definition,
( sQ33_spl
<=> greater(mod2,very_low) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( ~ sQ33_spl
| greater(mod2,very_low) ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f476,plain,
( ~ sQ9_spl
| ~ sQ32_spl
| greater(mod2,mod2) ),
inference(forward_demodulation,[status(thm)],[f463,f314]) ).
fof(f479,plain,
( ~ sQ9_spl
| ~ sQ32_spl
| ~ greater(mod2,mod2) ),
inference(resolution,[status(thm)],[f476,f30]) ).
fof(f480,plain,
( ~ sQ9_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f479,f476]) ).
fof(f481,plain,
( ~ sQ9_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f480]) ).
fof(f489,plain,
( ~ sQ27_spl
| ~ greater(low,very_low) ),
inference(backward_demodulation,[status(thm)],[f385,f203]) ).
fof(f490,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f489,f44]) ).
fof(f491,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f490]) ).
fof(f521,plain,
( greater(mod2,very_low)
| mod2 = very_low ),
inference(resolution,[status(thm)],[f109,f60]) ).
fof(f525,plain,
( sQ33_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f521,f462,f465]) ).
fof(f535,plain,
( greater(mod1,very_low)
| mod1 = very_low ),
inference(resolution,[status(thm)],[f110,f60]) ).
fof(f540,plain,
( sQ31_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f535,f431,f434]) ).
fof(f564,plain,
! [X0] :
( ~ sQ22_spl
| hazard_of_mortality(sK0_skl,X0) = high
| is_aligned(sK0_skl,X0)
| has_immunity(sK0_skl,X0)
| ~ organization(sK0_skl)
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f310,f41]) ).
fof(f565,plain,
! [X0] :
( ~ sQ22_spl
| hazard_of_mortality(sK0_skl,X0) = mod2
| ~ is_aligned(sK0_skl,X0)
| has_immunity(sK0_skl,X0)
| ~ organization(sK0_skl)
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f310,f40]) ).
fof(f566,definition,
! [X0] :
( sQ34_spl
<=> ( hazard_of_mortality(sK0_skl,X0) = high
| is_aligned(sK0_skl,X0)
| has_immunity(sK0_skl,X0)
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f567,plain,
! [X0] :
( ~ sQ34_spl
| hazard_of_mortality(sK0_skl,X0) = high
| is_aligned(sK0_skl,X0)
| has_immunity(sK0_skl,X0)
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f566]) ).
fof(f569,plain,
( ~ sQ22_spl
| ~ sQ23_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f564,f566,f306,f303]) ).
fof(f570,definition,
! [X0] :
( sQ35_spl
<=> ( hazard_of_mortality(sK0_skl,X0) = mod2
| ~ is_aligned(sK0_skl,X0)
| has_immunity(sK0_skl,X0)
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f571,plain,
! [X0] :
( ~ sQ35_spl
| hazard_of_mortality(sK0_skl,X0) = mod2
| ~ is_aligned(sK0_skl,X0)
| has_immunity(sK0_skl,X0)
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f570]) ).
fof(f573,plain,
( ~ sQ22_spl
| ~ sQ23_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f565,f570,f306,f303]) ).
fof(f574,plain,
! [X0] :
( ~ sQ34_spl
| hazard_of_mortality(sK0_skl,X0) = high
| is_aligned(sK0_skl,X0)
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f567]) ).
fof(f575,plain,
! [X0] :
( ~ sQ35_spl
| hazard_of_mortality(sK0_skl,X0) = mod2
| ~ is_aligned(sK0_skl,X0)
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f571]) ).
fof(f617,plain,
! [X0] :
( ~ sQ34_spl
| ~ sQ35_spl
| hazard_of_mortality(sK0_skl,X0) = high
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0)
| hazard_of_mortality(sK0_skl,X0) = mod2
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f575,f574]) ).
fof(f619,plain,
! [X0] :
( ~ sQ34_spl
| ~ sQ35_spl
| hazard_of_mortality(sK0_skl,X0) = high
| hazard_of_mortality(sK0_skl,X0) = mod2
| hazard_of_mortality(sK0_skl,X0) = low
| hazard_of_mortality(sK0_skl,X0) = mod1
| has_immunity(sK0_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f617]) ).
fof(f621,plain,
( ~ sQ34_spl
| ~ sQ35_spl
| hazard_of_mortality(sK0_skl,sK2_skl) = high
| hazard_of_mortality(sK0_skl,sK2_skl) = mod2
| hazard_of_mortality(sK0_skl,sK2_skl) = low
| hazard_of_mortality(sK0_skl,sK2_skl) = mod1 ),
inference(resolution,[status(thm)],[f619,f51]) ).
fof(f623,definition,
( sQ37_spl
<=> hazard_of_mortality(sK0_skl,sK2_skl) = mod1 ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f624,plain,
( ~ sQ37_spl
| hazard_of_mortality(sK0_skl,sK2_skl) = mod1 ),
inference(component_clause,[status(thm)],[f623]) ).
fof(f626,definition,
( sQ38_spl
<=> hazard_of_mortality(sK0_skl,sK2_skl) = mod2 ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f627,plain,
( ~ sQ38_spl
| hazard_of_mortality(sK0_skl,sK2_skl) = mod2 ),
inference(component_clause,[status(thm)],[f626]) ).
fof(f629,definition,
( sQ39_spl
<=> hazard_of_mortality(sK0_skl,sK2_skl) = high ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f630,plain,
( ~ sQ39_spl
| hazard_of_mortality(sK0_skl,sK2_skl) = high ),
inference(component_clause,[status(thm)],[f629]) ).
fof(f632,plain,
( ~ sQ34_spl
| ~ sQ35_spl
| sQ39_spl
| sQ38_spl
| sQ27_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f621,f623,f384,f626,f629,f570,f566]) ).
fof(f642,plain,
( ~ sQ38_spl
| ~ greater(mod2,very_low) ),
inference(backward_demodulation,[status(thm)],[f627,f203]) ).
fof(f643,plain,
( ~ sQ38_spl
| ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f642,f466]) ).
fof(f644,plain,
( ~ sQ38_spl
| ~ sQ33_spl ),
inference(contradiction_clause,[status(thm)],[f643]) ).
fof(f648,plain,
( ~ sQ37_spl
| ~ greater(mod1,very_low) ),
inference(forward_demodulation,[status(thm)],[f624,f203]) ).
fof(f649,plain,
( ~ sQ37_spl
| ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f648,f435]) ).
fof(f650,plain,
( ~ sQ37_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f649]) ).
fof(f661,plain,
( ~ sQ39_spl
| ~ greater(high,very_low) ),
inference(backward_demodulation,[status(thm)],[f630,f203]) ).
fof(f662,plain,
( ~ sQ39_spl
| ~ sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f661,f330]) ).
fof(f663,plain,
( ~ sQ39_spl
| ~ sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f662]) ).
fof(f664,plain,
$false,
inference(sat_refutation,[status(thm)],[f130,f137,f144,f151,f263,f309,f332,f348,f349,f352,f354,f382,f451,f452,f481,f491,f525,f540,f569,f573,f632,f644,f650,f663]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT060+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n018.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 01:26:28 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Drodi V4.1.1
% 0.14/0.39 % Refutation found
% 0.14/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.41 % Elapsed time: 0.063410 seconds
% 0.14/0.41 % CPU time: 0.228528 seconds
% 0.14/0.41 % Total memory used: 82.544 MB
% 0.14/0.41 % Net memory used: 82.058 MB
%------------------------------------------------------------------------------