%------------------------------------------------------------------------------
% 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/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 1.05s 0.64s
% Output : CNFRefutation 1.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 48
% Syntax : Number of formulae : 168 ( 27 unt; 24 def)
% Number of atoms : 414 ( 49 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 464 ( 218 ~; 222 |; 0 &)
% ( 24 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 25 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 107 ( 107 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A,B] :
( smaller_or_equal(A,B)
| ~ smaller(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B] :
( smaller(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(f12,axiom,
! [A,B] :
( ~ has_immunity(A,B)
| has_endowment(A)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B,C] :
( organization(A)
| ~ dissimilar(A,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B,C] :
( ~ is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ dissimilar(A,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A,B,C] :
( dissimilar(A,B,C)
| is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,B] :
( is_aligned(A,B)
| age(A,B) != zero
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B,C] :
( dissimilar(A,B,C)
| ~ greater(age(A,C),sigma)
| age(A,B) != zero
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A,B,C] :
( greater(age(A,C),sigma)
| ~ dissimilar(A,B,C)
| age(A,B) != zero
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A,B] :
( positional_advantage(A,B)
| ~ smaller_or_equal(age(A,B),sigma)
| ~ fragile_position(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A,B] :
( ~ positional_advantage(A,B)
| ~ greater(age(A,B),sigma)
| ~ fragile_position(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,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(f33,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(f34,axiom,
greater(high,mod1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
greater(mod1,low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
organization(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,negated_conjecture,
fragile_position(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
~ has_endowment(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
age(sk2,sk3) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
greater(sigma,zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
smaller_or_equal(age(sk2,sk4),sigma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
greater(age(sk2,sk5),sigma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,plain,
! [X0,X1] :
( smaller_or_equal(X0,X1)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f54,plain,
! [X0,X1] :
( smaller(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f56,plain,
! [A,C] :
( greater(A,C)
| ! [B] :
( ~ greater(B,C)
| ~ greater(A,B) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f57,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f59,plain,
! [A] :
( ! [B] : ~ has_immunity(A,B)
| has_endowment(A)
| ~ organization(A) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f60,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| has_endowment(X0)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [A] :
( organization(A)
| ! [B,C] : ~ dissimilar(A,B,C) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f62,plain,
! [X0,X1,X2] :
( organization(X0)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f65,plain,
! [A,C] :
( ~ is_aligned(A,C)
| ! [B] :
( ~ is_aligned(A,B)
| ~ dissimilar(A,B,C) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f66,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f69,plain,
! [X0,X1,X2] :
( dissimilar(X0,X1,X2)
| is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f73,plain,
! [X0,X1] :
( is_aligned(X0,X1)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f74,plain,
! [X0,X1,X2] :
( dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f75,plain,
! [A,C] :
( greater(age(A,C),sigma)
| ! [B] :
( ~ dissimilar(A,B,C)
| age(A,B) != zero
| ~ organization(A) ) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f76,plain,
! [X0,X1,X2] :
( greater(age(X0,X2),sigma)
| ~ dissimilar(X0,X1,X2)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f77,plain,
! [X0,X1] :
( positional_advantage(X0,X1)
| ~ smaller_or_equal(age(X0,X1),sigma)
| ~ fragile_position(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f78,plain,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| ~ greater(age(X0,X1),sigma)
| ~ fragile_position(X0) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
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)],[f30]) ).
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)],[f33]) ).
fof(f88,plain,
greater(high,mod1),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f89,plain,
greater(mod1,low),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f93,plain,
organization(sk2),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f94,plain,
fragile_position(sk2),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f95,plain,
~ has_endowment(sk2),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f96,plain,
age(sk2,sk3) = zero,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f97,plain,
greater(sigma,zero),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f98,plain,
smaller_or_equal(age(sk2,sk4),sigma),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f99,plain,
greater(age(sk2,sk5),sigma),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f100,plain,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f101,definition,
( sQ0_spl
<=> greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f103,plain,
( sQ0_spl
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
inference(component_clause,[status(thm)],[f101]) ).
fof(f104,definition,
( sQ1_spl
<=> hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f105,plain,
( ~ sQ1_spl
| hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3) ),
inference(component_clause,[status(thm)],[f104]) ).
fof(f106,plain,
( sQ1_spl
| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ),
inference(component_clause,[status(thm)],[f104]) ).
fof(f107,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f100,f101,f104]) ).
fof(f116,plain,
! [X0] :
( greater(X0,low)
| ~ greater(X0,mod1) ),
inference(resolution,[status(thm)],[f89,f57]) ).
fof(f129,plain,
greater(high,low),
inference(resolution,[status(thm)],[f116,f88]) ).
fof(f138,plain,
! [X0,X1,X2] :
( greater(age(X0,X2),sigma)
| ~ dissimilar(X0,X1,X2)
| age(X0,X1) != zero ),
inference(backward_subsumption_resolution,[status(thm)],[f76,f62]) ).
fof(f303,plain,
! [X0] :
( ~ positional_advantage(sk2,X0)
| ~ greater(age(sk2,X0),sigma) ),
inference(resolution,[status(thm)],[f78,f94]) ).
fof(f363,definition,
( sQ31_spl
<=> organization(sk2) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f365,plain,
( sQ31_spl
| ~ organization(sk2) ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f373,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f365,f93]) ).
fof(f374,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f373]) ).
fof(f393,plain,
! [X0] :
( hazard_of_mortality(sk2,X0) = low
| ~ positional_advantage(sk2,X0)
| ~ is_aligned(sk2,X0)
| has_immunity(sk2,X0) ),
inference(resolution,[status(thm)],[f84,f93]) ).
fof(f400,plain,
! [X0] :
( dissimilar(sk2,X0,sk5)
| age(sk2,X0) != zero
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f99,f74]) ).
fof(f404,definition,
! [X0] :
( sQ34_spl
<=> ( dissimilar(sk2,X0,sk5)
| age(sk2,X0) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f405,plain,
! [X0] :
( ~ sQ34_spl
| dissimilar(sk2,X0,sk5)
| age(sk2,X0) != zero ),
inference(component_clause,[status(thm)],[f404]) ).
fof(f407,plain,
( sQ34_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f400,f363,f404]) ).
fof(f578,plain,
! [X0,X1] :
( ~ greater(age(X0,X1),sigma)
| ~ fragile_position(X0)
| ~ smaller_or_equal(age(X0,X1),sigma)
| ~ fragile_position(X0) ),
inference(resolution,[status(thm)],[f77,f78]) ).
fof(f579,plain,
! [X0,X1] :
( ~ greater(age(X0,X1),sigma)
| ~ smaller_or_equal(age(X0,X1),sigma)
| ~ fragile_position(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f578]) ).
fof(f650,definition,
( sQ49_spl
<=> fragile_position(sk2) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f652,plain,
( sQ49_spl
| ~ fragile_position(sk2) ),
inference(component_clause,[status(thm)],[f650]) ).
fof(f658,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f652,f94]) ).
fof(f659,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f658]) ).
fof(f694,definition,
! [X0] :
( sQ53_spl
<=> ( age(sk2,X0) != zero
| age(sk2,X0) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f695,plain,
! [X0] :
( ~ sQ53_spl
| age(sk2,X0) != zero
| age(sk2,X0) != zero ),
inference(component_clause,[status(thm)],[f694]) ).
fof(f701,definition,
! [X0] :
( sQ55_spl
<=> ( ~ is_aligned(sk2,X0)
| age(sk2,X0) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f702,plain,
! [X0] :
( ~ sQ55_spl
| ~ is_aligned(sk2,X0)
| age(sk2,X0) != zero ),
inference(component_clause,[status(thm)],[f701]) ).
fof(f704,definition,
( sQ56_spl
<=> is_aligned(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f706,plain,
( sQ56_spl
| ~ is_aligned(sk2,sk3) ),
inference(component_clause,[status(thm)],[f704]) ).
fof(f708,plain,
! [X0] :
( ~ sQ53_spl
| age(sk2,X0) != zero ),
inference(duplicate_literals_removal,[status(thm)],[f695]) ).
fof(f740,definition,
( sQ57_spl
<=> has_immunity(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f741,plain,
( ~ sQ57_spl
| has_immunity(sk2,sk3) ),
inference(component_clause,[status(thm)],[f740]) ).
fof(f743,definition,
( sQ58_spl
<=> positional_advantage(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f744,plain,
( ~ sQ58_spl
| positional_advantage(sk2,sk3) ),
inference(component_clause,[status(thm)],[f743]) ).
fof(f781,plain,
( ~ sQ57_spl
| has_endowment(sk2)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f741,f60]) ).
fof(f786,definition,
( sQ64_spl
<=> has_endowment(sk2) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f787,plain,
( ~ sQ64_spl
| has_endowment(sk2) ),
inference(component_clause,[status(thm)],[f786]) ).
fof(f789,plain,
( ~ sQ57_spl
| sQ64_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f781,f363,f786,f740]) ).
fof(f790,plain,
( ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f787,f95]) ).
fof(f791,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f790]) ).
fof(f792,plain,
( ~ sQ53_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f96,f708]) ).
fof(f793,plain,
~ sQ53_spl,
inference(contradiction_clause,[status(thm)],[f792]) ).
fof(f828,plain,
! [X0] :
( ~ sQ34_spl
| ~ is_aligned(sk2,sk5)
| ~ is_aligned(sk2,X0)
| age(sk2,X0) != zero ),
inference(resolution,[status(thm)],[f405,f66]) ).
fof(f830,definition,
( sQ67_spl
<=> is_aligned(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f832,plain,
( sQ67_spl
| ~ is_aligned(sk2,sk5) ),
inference(component_clause,[status(thm)],[f830]) ).
fof(f833,plain,
( ~ sQ34_spl
| ~ sQ67_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f828,f701,f830,f404]) ).
fof(f835,plain,
( sQ67_spl
| hazard_of_mortality(sk2,sk5) = high
| positional_advantage(sk2,sk5)
| has_immunity(sk2,sk5)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f832,f87]) ).
fof(f841,definition,
( sQ68_spl
<=> has_immunity(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f842,plain,
( ~ sQ68_spl
| has_immunity(sk2,sk5) ),
inference(component_clause,[status(thm)],[f841]) ).
fof(f844,definition,
( sQ69_spl
<=> positional_advantage(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f845,plain,
( ~ sQ69_spl
| positional_advantage(sk2,sk5) ),
inference(component_clause,[status(thm)],[f844]) ).
fof(f847,definition,
( sQ70_spl
<=> hazard_of_mortality(sk2,sk5) = high ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f848,plain,
( ~ sQ70_spl
| hazard_of_mortality(sk2,sk5) = high ),
inference(component_clause,[status(thm)],[f847]) ).
fof(f850,plain,
( sQ67_spl
| sQ70_spl
| sQ69_spl
| sQ68_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f835,f363,f841,f844,f847,f830]) ).
fof(f864,plain,
( ~ sQ68_spl
| has_endowment(sk2)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f842,f60]) ).
fof(f869,plain,
( ~ sQ68_spl
| sQ64_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f864,f363,f786,f841]) ).
fof(f875,plain,
( ~ sQ69_spl
| ~ greater(age(sk2,sk5),sigma) ),
inference(resolution,[status(thm)],[f845,f303]) ).
fof(f881,plain,
( ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f875,f99]) ).
fof(f882,plain,
~ sQ69_spl,
inference(contradiction_clause,[status(thm)],[f881]) ).
fof(f936,plain,
( ~ greater(age(sk2,sk4),sigma)
| ~ fragile_position(sk2) ),
inference(resolution,[status(thm)],[f579,f98]) ).
fof(f939,definition,
( sQ78_spl
<=> greater(age(sk2,sk4),sigma) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f942,plain,
( ~ sQ78_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f936,f650,f939]) ).
fof(f943,definition,
( sQ79_spl
<=> smaller_or_equal(zero,sigma) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f945,plain,
( sQ79_spl
| ~ smaller_or_equal(zero,sigma) ),
inference(component_clause,[status(thm)],[f943]) ).
fof(f947,plain,
( sQ79_spl
| ~ smaller(zero,sigma) ),
inference(resolution,[status(thm)],[f945,f48]) ).
fof(f949,plain,
( sQ79_spl
| ~ greater(sigma,zero) ),
inference(resolution,[status(thm)],[f947,f54]) ).
fof(f952,plain,
( sQ79_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f949,f97]) ).
fof(f953,plain,
sQ79_spl,
inference(contradiction_clause,[status(thm)],[f952]) ).
fof(f1280,plain,
! [X0] :
( positional_advantage(sk2,X0)
| ~ smaller_or_equal(age(sk2,X0),sigma) ),
inference(resolution,[status(thm)],[f77,f94]) ).
fof(f1582,plain,
( ~ sQ58_spl
| hazard_of_mortality(sk2,sk3) = low
| ~ is_aligned(sk2,sk3)
| has_immunity(sk2,sk3) ),
inference(resolution,[status(thm)],[f744,f393]) ).
fof(f1584,definition,
( sQ115_spl
<=> hazard_of_mortality(sk2,sk3) = low ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1585,plain,
( ~ sQ115_spl
| hazard_of_mortality(sk2,sk3) = low ),
inference(component_clause,[status(thm)],[f1584]) ).
fof(f1587,plain,
( ~ sQ58_spl
| sQ115_spl
| ~ sQ56_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f1582,f740,f704,f1584,f743]) ).
fof(f1616,plain,
( positional_advantage(sk2,sk4)
| ~ fragile_position(sk2) ),
inference(resolution,[status(thm)],[f98,f77]) ).
fof(f1618,definition,
( sQ116_spl
<=> positional_advantage(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1619,plain,
( ~ sQ116_spl
| positional_advantage(sk2,sk4) ),
inference(component_clause,[status(thm)],[f1618]) ).
fof(f1621,plain,
( sQ116_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f1616,f650,f1618]) ).
fof(f1637,plain,
( positional_advantage(sk2,sk3)
| ~ smaller_or_equal(zero,sigma) ),
inference(paramodulation,[status(thm)],[f96,f1280]) ).
fof(f1638,plain,
( sQ58_spl
| ~ sQ79_spl ),
inference(split_clause,[status(thm)],[f1637,f943,f743]) ).
fof(f1641,plain,
( ~ sQ116_spl
| hazard_of_mortality(sk2,sk4) = low
| ~ is_aligned(sk2,sk4)
| has_immunity(sk2,sk4) ),
inference(resolution,[status(thm)],[f1619,f393]) ).
fof(f1643,definition,
( sQ117_spl
<=> has_immunity(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1644,plain,
( ~ sQ117_spl
| has_immunity(sk2,sk4) ),
inference(component_clause,[status(thm)],[f1643]) ).
fof(f1646,definition,
( sQ118_spl
<=> is_aligned(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1648,plain,
( sQ118_spl
| ~ is_aligned(sk2,sk4) ),
inference(component_clause,[status(thm)],[f1646]) ).
fof(f1649,definition,
( sQ119_spl
<=> hazard_of_mortality(sk2,sk4) = low ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1650,plain,
( ~ sQ119_spl
| hazard_of_mortality(sk2,sk4) = low ),
inference(component_clause,[status(thm)],[f1649]) ).
fof(f1652,plain,
( ~ sQ116_spl
| sQ119_spl
| ~ sQ118_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f1641,f1643,f1646,f1649,f1618]) ).
fof(f1658,plain,
! [X0] :
( sQ118_spl
| dissimilar(sk2,X0,sk4)
| ~ is_aligned(sk2,X0)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f1648,f69]) ).
fof(f1676,definition,
! [X0] :
( sQ124_spl
<=> ( dissimilar(sk2,X0,sk4)
| ~ is_aligned(sk2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1677,plain,
! [X0] :
( ~ sQ124_spl
| dissimilar(sk2,X0,sk4)
| ~ is_aligned(sk2,X0) ),
inference(component_clause,[status(thm)],[f1676]) ).
fof(f1679,plain,
( sQ118_spl
| sQ124_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f1658,f363,f1676,f1646]) ).
fof(f1680,plain,
( ~ sQ117_spl
| has_endowment(sk2)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f1644,f60]) ).
fof(f1681,plain,
( ~ sQ117_spl
| sQ64_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f1680,f363,f786,f1643]) ).
fof(f1693,plain,
( sQ1_spl
| ~ sQ115_spl
| hazard_of_mortality(sk2,sk4) != low ),
inference(backward_demodulation,[status(thm)],[f1585,f106]) ).
fof(f1700,plain,
( ~ sQ119_spl
| sQ1_spl
| ~ sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1650,f1693]) ).
fof(f1701,plain,
( ~ sQ119_spl
| sQ1_spl
| ~ sQ115_spl ),
inference(contradiction_clause,[status(thm)],[f1700]) ).
fof(f1703,plain,
( ~ sQ1_spl
| ~ sQ115_spl
| hazard_of_mortality(sk2,sk4) = low ),
inference(forward_demodulation,[status(thm)],[f1585,f105]) ).
fof(f1784,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ sQ115_spl
| ~ greater(hazard_of_mortality(sk2,sk5),low) ),
inference(forward_demodulation,[status(thm)],[f1703,f103]) ).
fof(f1824,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ sQ115_spl
| ~ sQ70_spl
| ~ greater(high,low) ),
inference(forward_demodulation,[status(thm)],[f848,f1784]) ).
fof(f1825,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ sQ115_spl
| ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1824,f129]) ).
fof(f1826,plain,
( sQ0_spl
| ~ sQ1_spl
| ~ sQ115_spl
| ~ sQ70_spl ),
inference(contradiction_clause,[status(thm)],[f1825]) ).
fof(f2353,plain,
! [X0] :
( ~ sQ124_spl
| greater(age(sk2,sk4),sigma)
| age(sk2,X0) != zero
| ~ is_aligned(sk2,X0) ),
inference(resolution,[status(thm)],[f1677,f138]) ).
fof(f2357,plain,
( ~ sQ124_spl
| sQ78_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f2353,f701,f939,f1676]) ).
fof(f2386,plain,
! [X0] :
( ~ sQ55_spl
| age(sk2,X0) != zero
| ~ organization(sk2)
| age(sk2,X0) != zero ),
inference(resolution,[status(thm)],[f702,f73]) ).
fof(f2400,plain,
( ~ sQ55_spl
| ~ sQ31_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f2386,f694,f363,f701]) ).
fof(f2457,plain,
( sQ56_spl
| age(sk2,sk3) != zero
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f706,f73]) ).
fof(f2462,definition,
( sQ151_spl
<=> age(sk2,sk3) = zero ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f2464,plain,
( sQ151_spl
| age(sk2,sk3) != zero ),
inference(component_clause,[status(thm)],[f2462]) ).
fof(f2465,plain,
( sQ56_spl
| ~ sQ151_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f2457,f363,f2462,f704]) ).
fof(f2469,plain,
( sQ151_spl
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f96,f2464]) ).
fof(f2470,plain,
( sQ151_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2469]) ).
fof(f2471,plain,
sQ151_spl,
inference(contradiction_clause,[status(thm)],[f2470]) ).
fof(f2472,plain,
$false,
inference(sat_refutation,[status(thm)],[f107,f374,f407,f659,f789,f791,f793,f833,f850,f869,f882,f942,f953,f1587,f1621,f1638,f1652,f1679,f1681,f1701,f1826,f2357,f2400,f2465,f2471]) ).
%------------------------------------------------------------------------------
%----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/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n015.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 01:27:35 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 1.05/0.64 % Refutation found
% 1.05/0.64 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.05/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.05/0.65 % Elapsed time: 0.280331 seconds
% 1.05/0.65 % CPU time: 1.892891 seconds
% 1.05/0.65 % Total memory used: 125.294 MB
% 1.05/0.65 % Net memory used: 122.378 MB
%------------------------------------------------------------------------------