%------------------------------------------------------------------------------
% 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/sandbox/benchmark/theBenchmark.p
% Computer : n006.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 : Unsatisfiable 0.19s 0.47s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 38
% Syntax : Number of formulae : 148 ( 34 unt; 21 def)
% Number of atoms : 322 ( 43 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 306 ( 132 ~; 153 |; 0 &)
% ( 21 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 22 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 52 ( 52 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [A,B] :
( greater(B,A)
| ~ smaller(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] :
( ~ greater(B,A)
| ~ greater(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B,C] :
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] :
( greater(A,B)
| A = B
| smaller(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A,B] :
( hazard_of_mortality(A,B) = very_low
| ~ has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B] :
( hazard_of_mortality(A,B) = low
| ~ positional_advantage(A,B)
| ~ is_aligned(A,B)
| has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B] :
( hazard_of_mortality(A,B) = mod1
| ~ positional_advantage(A,B)
| is_aligned(A,B)
| has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B] :
( hazard_of_mortality(A,B) = mod2
| positional_advantage(A,B)
| ~ is_aligned(A,B)
| has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A,B] :
( hazard_of_mortality(A,B) = high
| positional_advantage(A,B)
| is_aligned(A,B)
| has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
greater(mod1,low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
greater(low,very_low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
greater(high,mod2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
greater(mod2,low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
organization(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
has_immunity(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
~ has_immunity(sk1,sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f34,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f35,plain,
! [A,C] :
( greater(A,C)
| ! [B] :
( ~ greater(B,C)
| ~ greater(A,B) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f36,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f38,plain,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = very_low
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f39,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)],[f13]) ).
fof(f40,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)],[f14]) ).
fof(f41,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)],[f15]) ).
fof(f42,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)],[f16]) ).
fof(f44,plain,
greater(mod1,low),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f45,plain,
greater(low,very_low),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f46,plain,
greater(high,mod2),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f47,plain,
greater(mod2,low),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f48,plain,
organization(sk1),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f49,plain,
has_immunity(sk1,sk2),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f50,plain,
~ has_immunity(sk1,sk3),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f51,plain,
~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f57,plain,
~ greater(low,mod1),
inference(resolution,[status(thm)],[f44,f34]) ).
fof(f61,plain,
! [X0] :
( greater(X0,very_low)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f45,f36]) ).
fof(f62,plain,
~ greater(very_low,low),
inference(resolution,[status(thm)],[f45,f34]) ).
fof(f65,plain,
! [X0] :
( greater(X0,low)
| ~ greater(X0,mod2) ),
inference(resolution,[status(thm)],[f47,f36]) ).
fof(f66,plain,
~ greater(low,mod2),
inference(resolution,[status(thm)],[f47,f34]) ).
fof(f71,plain,
! [X0,X1] :
( greater(X1,X0)
| greater(X0,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f37,f32]) ).
fof(f72,plain,
! [X0,X1] :
( greater(X1,very_low)
| ~ greater(X1,X0)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f61,f36]) ).
fof(f73,plain,
! [X0] :
( ~ greater(very_low,X0)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f61,f34]) ).
fof(f75,plain,
! [X0] :
( hazard_of_mortality(sk1,X0) = very_low
| ~ has_immunity(sk1,X0) ),
inference(resolution,[status(thm)],[f38,f48]) ).
fof(f76,plain,
hazard_of_mortality(sk1,sk2) = very_low,
inference(resolution,[status(thm)],[f75,f49]) ).
fof(f77,plain,
~ greater(hazard_of_mortality(sk1,sk3),very_low),
inference(backward_demodulation,[status(thm)],[f76,f51]) ).
fof(f78,plain,
~ greater(hazard_of_mortality(sk1,sk3),low),
inference(resolution,[status(thm)],[f77,f61]) ).
fof(f79,plain,
( ~ greater(very_low,low)
| ~ greater(very_low,low) ),
inference(resolution,[status(thm)],[f73,f61]) ).
fof(f80,definition,
( sQ0_spl
<=> greater(very_low,low) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f83,plain,
~ sQ0_spl,
inference(split_clause,[status(thm)],[f79,f80]) ).
fof(f84,plain,
! [X0] :
( greater(X0,very_low)
| ~ greater(X0,mod2) ),
inference(resolution,[status(thm)],[f72,f47]) ).
fof(f87,plain,
greater(high,very_low),
inference(resolution,[status(thm)],[f84,f46]) ).
fof(f93,plain,
( greater(low,hazard_of_mortality(sk1,sk3))
| low = hazard_of_mortality(sk1,sk3) ),
inference(resolution,[status(thm)],[f71,f78]) ).
fof(f97,plain,
( greater(low,very_low)
| low = very_low ),
inference(resolution,[status(thm)],[f71,f62]) ).
fof(f99,plain,
( greater(mod2,low)
| mod2 = low ),
inference(resolution,[status(thm)],[f71,f66]) ).
fof(f101,plain,
( greater(mod1,low)
| mod1 = low ),
inference(resolution,[status(thm)],[f71,f57]) ).
fof(f114,definition,
( sQ1_spl
<=> low = hazard_of_mortality(sk1,sk3) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f115,plain,
( ~ sQ1_spl
| low = hazard_of_mortality(sk1,sk3) ),
inference(component_clause,[status(thm)],[f114]) ).
fof(f117,definition,
( sQ2_spl
<=> greater(low,hazard_of_mortality(sk1,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f118,plain,
( ~ sQ2_spl
| greater(low,hazard_of_mortality(sk1,sk3)) ),
inference(component_clause,[status(thm)],[f117]) ).
fof(f120,plain,
( sQ2_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f93,f114,f117]) ).
fof(f142,definition,
( sQ9_spl
<=> low = very_low ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f143,plain,
( ~ sQ9_spl
| low = very_low ),
inference(component_clause,[status(thm)],[f142]) ).
fof(f145,definition,
( sQ10_spl
<=> greater(low,very_low) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f148,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f97,f142,f145]) ).
fof(f149,definition,
( sQ11_spl
<=> mod2 = low ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f150,plain,
( ~ sQ11_spl
| mod2 = low ),
inference(component_clause,[status(thm)],[f149]) ).
fof(f152,definition,
( sQ12_spl
<=> greater(mod2,low) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f153,plain,
( ~ sQ12_spl
| greater(mod2,low) ),
inference(component_clause,[status(thm)],[f152]) ).
fof(f155,plain,
( sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f99,f149,f152]) ).
fof(f163,definition,
( sQ15_spl
<=> mod1 = low ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f164,plain,
( ~ sQ15_spl
| mod1 = low ),
inference(component_clause,[status(thm)],[f163]) ).
fof(f166,definition,
( sQ16_spl
<=> greater(mod1,low) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f169,plain,
( sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f101,f163,f166]) ).
fof(f202,plain,
! [X0] :
( ~ greater(low,X0)
| ~ greater(X0,mod2) ),
inference(resolution,[status(thm)],[f65,f34]) ).
fof(f239,definition,
( sQ19_spl
<=> low = low ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f242,definition,
( sQ20_spl
<=> greater(low,low) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f243,plain,
( ~ sQ20_spl
| greater(low,low) ),
inference(component_clause,[status(thm)],[f242]) ).
fof(f244,plain,
( sQ20_spl
| ~ greater(low,low) ),
inference(component_clause,[status(thm)],[f242]) ).
fof(f280,plain,
( ~ sQ15_spl
| greater(mod1,mod1) ),
inference(forward_demodulation,[status(thm)],[f164,f44]) ).
fof(f282,plain,
( ~ sQ15_spl
| ~ greater(mod1,mod1) ),
inference(resolution,[status(thm)],[f280,f34]) ).
fof(f283,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f282,f280]) ).
fof(f284,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f283]) ).
fof(f301,plain,
! [X0] :
( hazard_of_mortality(sk1,X0) = mod1
| ~ positional_advantage(sk1,X0)
| is_aligned(sk1,X0)
| has_immunity(sk1,X0) ),
inference(resolution,[status(thm)],[f40,f48]) ).
fof(f306,plain,
( ~ sQ20_spl
| ~ greater(low,low) ),
inference(resolution,[status(thm)],[f243,f34]) ).
fof(f307,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f306,f243]) ).
fof(f308,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f307]) ).
fof(f309,plain,
( sQ20_spl
| greater(low,low)
| low = low ),
inference(resolution,[status(thm)],[f244,f71]) ).
fof(f310,plain,
( sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f309,f239,f242]) ).
fof(f313,definition,
( sQ23_spl
<=> very_low = very_low ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f316,definition,
( sQ24_spl
<=> greater(very_low,very_low) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f317,plain,
( ~ sQ24_spl
| greater(very_low,very_low) ),
inference(component_clause,[status(thm)],[f316]) ).
fof(f318,plain,
( sQ24_spl
| ~ greater(very_low,very_low) ),
inference(component_clause,[status(thm)],[f316]) ).
fof(f337,plain,
( ~ sQ24_spl
| ~ greater(very_low,very_low) ),
inference(resolution,[status(thm)],[f317,f34]) ).
fof(f338,plain,
( ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f337,f317]) ).
fof(f339,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f338]) ).
fof(f340,plain,
( sQ24_spl
| greater(very_low,very_low)
| very_low = very_low ),
inference(resolution,[status(thm)],[f318,f71]) ).
fof(f341,plain,
( sQ24_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f340,f313,f316]) ).
fof(f360,plain,
( ~ sQ2_spl
| ~ greater(hazard_of_mortality(sk1,sk3),mod2) ),
inference(resolution,[status(thm)],[f118,f202]) ).
fof(f368,plain,
( ~ sQ2_spl
| greater(mod2,hazard_of_mortality(sk1,sk3))
| mod2 = hazard_of_mortality(sk1,sk3) ),
inference(resolution,[status(thm)],[f360,f71]) ).
fof(f369,definition,
( sQ27_spl
<=> mod2 = hazard_of_mortality(sk1,sk3) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f370,plain,
( ~ sQ27_spl
| mod2 = hazard_of_mortality(sk1,sk3) ),
inference(component_clause,[status(thm)],[f369]) ).
fof(f372,definition,
( sQ28_spl
<=> greater(mod2,hazard_of_mortality(sk1,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f375,plain,
( ~ sQ2_spl
| sQ28_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f368,f369,f372,f117]) ).
fof(f377,plain,
( ~ sQ27_spl
| ~ greater(mod2,low) ),
inference(backward_demodulation,[status(thm)],[f370,f78]) ).
fof(f379,plain,
( ~ sQ27_spl
| ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f377,f153]) ).
fof(f380,plain,
( ~ sQ27_spl
| ~ sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f379]) ).
fof(f384,plain,
( ~ sQ9_spl
| greater(low,low) ),
inference(backward_demodulation,[status(thm)],[f143,f45]) ).
fof(f394,plain,
( ~ sQ9_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f384,f242,f142]) ).
fof(f420,plain,
( ~ sQ11_spl
| greater(mod2,mod2) ),
inference(forward_demodulation,[status(thm)],[f150,f47]) ).
fof(f422,plain,
( ~ sQ11_spl
| ~ greater(mod2,mod2) ),
inference(resolution,[status(thm)],[f420,f34]) ).
fof(f423,plain,
( ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f422,f420]) ).
fof(f424,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f423]) ).
fof(f438,plain,
( ~ sQ1_spl
| ~ greater(low,very_low) ),
inference(backward_demodulation,[status(thm)],[f115,f77]) ).
fof(f439,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f438,f45]) ).
fof(f440,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f439]) ).
fof(f471,plain,
( hazard_of_mortality(sk1,sk3) = mod1
| ~ positional_advantage(sk1,sk3)
| is_aligned(sk1,sk3) ),
inference(resolution,[status(thm)],[f301,f50]) ).
fof(f472,definition,
( sQ29_spl
<=> is_aligned(sk1,sk3) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f473,plain,
( ~ sQ29_spl
| is_aligned(sk1,sk3) ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f475,definition,
( sQ30_spl
<=> positional_advantage(sk1,sk3) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( sQ30_spl
| ~ positional_advantage(sk1,sk3) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f478,definition,
( sQ31_spl
<=> hazard_of_mortality(sk1,sk3) = mod1 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( ~ sQ31_spl
| hazard_of_mortality(sk1,sk3) = mod1 ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f481,plain,
( sQ31_spl
| ~ sQ30_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f471,f472,f475,f478]) ).
fof(f485,plain,
( ~ sQ31_spl
| ~ greater(mod1,very_low) ),
inference(backward_demodulation,[status(thm)],[f479,f77]) ).
fof(f491,plain,
( ~ sQ31_spl
| ~ greater(mod1,low) ),
inference(resolution,[status(thm)],[f485,f61]) ).
fof(f493,plain,
( ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f491,f44]) ).
fof(f494,plain,
~ sQ31_spl,
inference(contradiction_clause,[status(thm)],[f493]) ).
fof(f495,plain,
( ~ sQ29_spl
| hazard_of_mortality(sk1,sk3) = mod2
| positional_advantage(sk1,sk3)
| has_immunity(sk1,sk3)
| ~ organization(sk1) ),
inference(resolution,[status(thm)],[f473,f41]) ).
fof(f496,plain,
( ~ sQ29_spl
| hazard_of_mortality(sk1,sk3) = low
| ~ positional_advantage(sk1,sk3)
| has_immunity(sk1,sk3)
| ~ organization(sk1) ),
inference(resolution,[status(thm)],[f473,f39]) ).
fof(f497,definition,
( sQ32_spl
<=> organization(sk1) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f499,plain,
( sQ32_spl
| ~ organization(sk1) ),
inference(component_clause,[status(thm)],[f497]) ).
fof(f500,definition,
( sQ33_spl
<=> has_immunity(sk1,sk3) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f501,plain,
( ~ sQ33_spl
| has_immunity(sk1,sk3) ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f503,plain,
( ~ sQ29_spl
| sQ27_spl
| sQ30_spl
| sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f495,f497,f500,f475,f369,f472]) ).
fof(f504,plain,
( ~ sQ29_spl
| sQ1_spl
| ~ sQ30_spl
| sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f496,f497,f500,f475,f114,f472]) ).
fof(f505,plain,
( ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f501,f50]) ).
fof(f506,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f505]) ).
fof(f507,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f499,f48]) ).
fof(f508,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f507]) ).
fof(f512,plain,
( sQ30_spl
| hazard_of_mortality(sk1,sk3) = high
| is_aligned(sk1,sk3)
| has_immunity(sk1,sk3)
| ~ organization(sk1) ),
inference(resolution,[status(thm)],[f477,f42]) ).
fof(f513,definition,
( sQ34_spl
<=> hazard_of_mortality(sk1,sk3) = high ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( ~ sQ34_spl
| hazard_of_mortality(sk1,sk3) = high ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,plain,
( sQ30_spl
| sQ34_spl
| sQ29_spl
| sQ33_spl
| ~ sQ32_spl ),
inference(split_clause,[status(thm)],[f512,f497,f500,f472,f513,f475]) ).
fof(f520,plain,
( ~ sQ34_spl
| ~ greater(high,very_low) ),
inference(backward_demodulation,[status(thm)],[f514,f77]) ).
fof(f521,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f520,f87]) ).
fof(f522,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f521]) ).
fof(f523,plain,
$false,
inference(sat_refutation,[status(thm)],[f83,f120,f148,f155,f169,f284,f308,f310,f339,f341,f375,f380,f394,f424,f440,f481,f494,f503,f504,f506,f508,f516,f522]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT060-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.40 % Computer : n006.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Mon Sep 21 01:24:12 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.19/0.43 % Drodi V4.1.1
% 0.19/0.47 % Refutation found
% 0.19/0.47 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.19/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.19/0.50 % Elapsed time: 0.077965 seconds
% 0.19/0.50 % CPU time: 0.276306 seconds
% 0.19/0.50 % Total memory used: 57.341 MB
% 0.19/0.50 % Net memory used: 57.127 MB
%------------------------------------------------------------------------------