%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT065-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 : n001.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:32 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.52s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 44
% Syntax : Number of formulae : 144 ( 38 unt; 17 def)
% Number of atoms : 324 ( 39 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 343 ( 163 ~; 163 |; 0 &)
% ( 17 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 18 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 83 ( 83 !; 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(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(f12,axiom,
! [A] :
( organization(A)
| ~ has_endowment(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B] :
( has_immunity(A,B)
| ~ smaller_or_equal(age(A,B),eta)
| ~ has_endowment(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B] :
( ~ has_immunity(A,B)
| ~ greater(age(A,B),eta)
| ~ has_endowment(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B,C] :
( ~ is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ dissimilar(A,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A,B] :
( is_aligned(A,B)
| age(A,B) != zero
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,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(f29,axiom,
! [A,B] :
( hazard_of_mortality(A,B) = very_low
| ~ has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,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(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(f36,axiom,
greater(low,very_low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
greater(mod2,low),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
organization(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,
greater(tau,zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
greater(eta,zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,negated_conjecture,
smaller_or_equal(age(sk2,sk4),eta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,negated_conjecture,
greater(age(sk2,sk5),sigma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,negated_conjecture,
greater(age(sk2,sk5),eta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,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(f54,plain,
! [X0,X1] :
( smaller_or_equal(X0,X1)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f60,plain,
! [X0,X1] :
( smaller(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f61,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f62,plain,
! [A,C] :
( greater(A,C)
| ! [B] :
( ~ greater(B,C)
| ~ greater(A,B) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f63,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f65,plain,
! [X0] :
( organization(X0)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f66,plain,
! [X0,X1] :
( has_immunity(X0,X1)
| ~ smaller_or_equal(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f67,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| ~ greater(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f76,plain,
! [A,C] :
( ~ is_aligned(A,C)
| ! [B] :
( ~ is_aligned(A,B)
| ~ dissimilar(A,B,C) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f84,plain,
! [X0,X1] :
( is_aligned(X0,X1)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f85,plain,
! [X0,X1,X2] :
( dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f88,plain,
! [X0,X1] :
( hazard_of_mortality(X0,X1) = very_low
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f90,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)],[f31]) ).
fof(f92,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(f93,plain,
greater(high,mod1),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f94,plain,
greater(mod1,low),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f95,plain,
greater(low,very_low),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f97,plain,
greater(mod2,low),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f98,plain,
organization(sk2),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f100,plain,
has_endowment(sk2),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f101,plain,
age(sk2,sk3) = zero,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f102,plain,
greater(sigma,zero),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f103,plain,
greater(tau,zero),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f104,plain,
greater(eta,zero),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f107,plain,
smaller_or_equal(age(sk2,sk4),eta),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f108,plain,
greater(age(sk2,sk5),sigma),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f110,plain,
greater(age(sk2,sk5),eta),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f111,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)],[f52]) ).
fof(f119,definition,
( sQ2_spl
<=> greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f121,plain,
( sQ2_spl
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
inference(component_clause,[status(thm)],[f119]) ).
fof(f122,definition,
( sQ3_spl
<=> hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f124,plain,
( sQ3_spl
| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ),
inference(component_clause,[status(thm)],[f122]) ).
fof(f125,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f111,f119,f122]) ).
fof(f132,plain,
! [X0] :
( greater(X0,zero)
| ~ greater(X0,tau) ),
inference(resolution,[status(thm)],[f63,f103]) ).
fof(f136,plain,
! [X0] :
( greater(X0,low)
| ~ greater(X0,mod1) ),
inference(resolution,[status(thm)],[f94,f63]) ).
fof(f143,plain,
~ greater(low,mod2),
inference(resolution,[status(thm)],[f97,f61]) ).
fof(f155,plain,
greater(high,low),
inference(resolution,[status(thm)],[f136,f93]) ).
fof(f177,definition,
( sQ6_spl
<=> has_endowment(sk2) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f179,plain,
( sQ6_spl
| ~ has_endowment(sk2) ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f459,plain,
! [X0] :
( greater(X0,very_low)
| ~ greater(X0,low) ),
inference(resolution,[status(thm)],[f95,f63]) ).
fof(f508,plain,
! [X0] :
( greater(X0,zero)
| ~ greater(X0,sigma) ),
inference(resolution,[status(thm)],[f102,f63]) ).
fof(f572,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f179,f100]) ).
fof(f573,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f572]) ).
fof(f574,plain,
! [X0,X1] :
( ~ smaller(age(X0,X1),eta)
| has_immunity(X0,X1)
| ~ has_endowment(X0) ),
inference(resolution,[status(thm)],[f66,f54]) ).
fof(f602,definition,
( sQ54_spl
<=> organization(sk2) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( sQ54_spl
| ~ organization(sk2) ),
inference(component_clause,[status(thm)],[f602]) ).
fof(f612,definition,
( sQ57_spl
<=> has_immunity(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f616,plain,
( sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f604,f98]) ).
fof(f617,plain,
sQ54_spl,
inference(contradiction_clause,[status(thm)],[f616]) ).
fof(f625,definition,
( sQ59_spl
<=> greater(zero,sigma) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f632,definition,
( sQ61_spl
<=> has_immunity(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f633,plain,
( ~ sQ61_spl
| has_immunity(sk2,sk3) ),
inference(component_clause,[status(thm)],[f632]) ).
fof(f642,plain,
( ~ sQ61_spl
| hazard_of_mortality(sk2,sk3) = very_low
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f633,f88]) ).
fof(f643,definition,
( sQ63_spl
<=> hazard_of_mortality(sk2,sk3) = very_low ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f644,plain,
( ~ sQ63_spl
| hazard_of_mortality(sk2,sk3) = very_low ),
inference(component_clause,[status(thm)],[f643]) ).
fof(f646,plain,
( ~ sQ61_spl
| sQ63_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f642,f602,f643,f632]) ).
fof(f755,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(resolution,[status(thm)],[f85,f77]) ).
fof(f756,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f755,f84]) ).
fof(f761,plain,
( sQ3_spl
| ~ sQ63_spl
| hazard_of_mortality(sk2,sk4) != very_low ),
inference(backward_demodulation,[status(thm)],[f644,f124]) ).
fof(f960,plain,
! [X0] :
( ~ greater(zero,X0)
| ~ greater(X0,tau) ),
inference(resolution,[status(thm)],[f132,f61]) ).
fof(f1058,plain,
! [X0,X1] :
( ~ smaller_or_equal(age(X0,X1),eta)
| ~ has_endowment(X0)
| hazard_of_mortality(X0,X1) = very_low
| ~ organization(X0) ),
inference(resolution,[status(thm)],[f88,f66]) ).
fof(f1060,plain,
! [X0,X1] :
( ~ smaller_or_equal(age(X0,X1),eta)
| ~ has_endowment(X0)
| hazard_of_mortality(X0,X1) = very_low ),
inference(forward_subsumption_resolution,[status(thm)],[f1058,f65]) ).
fof(f1065,plain,
! [X0] :
( ~ greater(zero,X0)
| ~ greater(X0,sigma) ),
inference(resolution,[status(thm)],[f508,f61]) ).
fof(f1079,plain,
( ~ smaller(zero,eta)
| has_immunity(sk2,sk3)
| ~ has_endowment(sk2) ),
inference(paramodulation,[status(thm)],[f101,f574]) ).
fof(f1080,definition,
( sQ80_spl
<=> smaller(zero,eta) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f1082,plain,
( sQ80_spl
| ~ smaller(zero,eta) ),
inference(component_clause,[status(thm)],[f1080]) ).
fof(f1083,plain,
( ~ sQ80_spl
| sQ61_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1079,f177,f632,f1080]) ).
fof(f1085,plain,
( sQ80_spl
| ~ greater(eta,zero) ),
inference(resolution,[status(thm)],[f1082,f60]) ).
fof(f1088,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1085,f104]) ).
fof(f1089,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f1088]) ).
fof(f1202,definition,
( sQ91_spl
<=> hazard_of_mortality(sk2,sk4) = very_low ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f1203,plain,
( ~ sQ91_spl
| hazard_of_mortality(sk2,sk4) = very_low ),
inference(component_clause,[status(thm)],[f1202]) ).
fof(f1219,definition,
! [X0] :
( sQ93_spl
<=> age(sk2,X0) != zero ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1220,plain,
! [X0] :
( ~ sQ93_spl
| age(sk2,X0) != zero ),
inference(component_clause,[status(thm)],[f1219]) ).
fof(f1226,plain,
( ~ sQ93_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f101,f1220]) ).
fof(f1227,plain,
~ sQ93_spl,
inference(contradiction_clause,[status(thm)],[f1226]) ).
fof(f1234,plain,
( ~ greater(zero,tau)
| ~ greater(zero,tau) ),
inference(resolution,[status(thm)],[f960,f132]) ).
fof(f1236,definition,
( sQ95_spl
<=> greater(zero,tau) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f1241,plain,
~ sQ95_spl,
inference(split_clause,[status(thm)],[f1234,f1236]) ).
fof(f1418,plain,
( ~ greater(zero,sigma)
| ~ greater(zero,sigma) ),
inference(resolution,[status(thm)],[f508,f1065]) ).
fof(f1422,plain,
~ sQ59_spl,
inference(split_clause,[status(thm)],[f1418,f625]) ).
fof(f1711,plain,
( ~ has_endowment(sk2)
| hazard_of_mortality(sk2,sk4) = very_low ),
inference(resolution,[status(thm)],[f1060,f107]) ).
fof(f1714,plain,
( ~ sQ6_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f1711,f1202,f177]) ).
fof(f1733,plain,
greater(mod1,very_low),
inference(resolution,[status(thm)],[f459,f94]) ).
fof(f1734,plain,
greater(high,very_low),
inference(resolution,[status(thm)],[f459,f155]) ).
fof(f1743,definition,
( sQ113_spl
<=> mod2 = very_low ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1744,plain,
( ~ sQ113_spl
| mod2 = very_low ),
inference(component_clause,[status(thm)],[f1743]) ).
fof(f1761,plain,
( ~ sQ113_spl
| greater(low,mod2) ),
inference(backward_demodulation,[status(thm)],[f1744,f95]) ).
fof(f1769,plain,
( ~ sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1761,f143]) ).
fof(f1770,plain,
~ sQ113_spl,
inference(contradiction_clause,[status(thm)],[f1769]) ).
fof(f1831,plain,
! [X0] :
( ~ is_aligned(sk2,sk5)
| age(sk2,X0) != zero
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f756,f108]) ).
fof(f1834,definition,
( sQ119_spl
<=> is_aligned(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1836,plain,
( sQ119_spl
| ~ is_aligned(sk2,sk5) ),
inference(component_clause,[status(thm)],[f1834]) ).
fof(f1837,plain,
( ~ sQ119_spl
| sQ93_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f1831,f602,f1219,f1834]) ).
fof(f1840,plain,
( sQ119_spl
| hazard_of_mortality(sk2,sk5) = high
| positional_advantage(sk2,sk5)
| has_immunity(sk2,sk5)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f1836,f92]) ).
fof(f1841,plain,
( sQ119_spl
| hazard_of_mortality(sk2,sk5) = mod1
| ~ positional_advantage(sk2,sk5)
| has_immunity(sk2,sk5)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f1836,f90]) ).
fof(f1846,definition,
( sQ120_spl
<=> positional_advantage(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1849,definition,
( sQ121_spl
<=> hazard_of_mortality(sk2,sk5) = high ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1850,plain,
( ~ sQ121_spl
| hazard_of_mortality(sk2,sk5) = high ),
inference(component_clause,[status(thm)],[f1849]) ).
fof(f1852,plain,
( sQ119_spl
| sQ121_spl
| sQ120_spl
| sQ57_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f1840,f602,f612,f1846,f1849,f1834]) ).
fof(f1853,definition,
( sQ122_spl
<=> hazard_of_mortality(sk2,sk5) = mod1 ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1854,plain,
( ~ sQ122_spl
| hazard_of_mortality(sk2,sk5) = mod1 ),
inference(component_clause,[status(thm)],[f1853]) ).
fof(f1856,plain,
( sQ119_spl
| sQ122_spl
| ~ sQ120_spl
| sQ57_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f1841,f602,f612,f1846,f1853,f1834]) ).
fof(f2016,plain,
( sQ2_spl
| ~ sQ91_spl
| ~ greater(hazard_of_mortality(sk2,sk5),very_low) ),
inference(backward_demodulation,[status(thm)],[f1203,f121]) ).
fof(f2080,plain,
( sQ3_spl
| ~ sQ63_spl
| ~ sQ91_spl
| very_low != very_low ),
inference(forward_demodulation,[status(thm)],[f1203,f761]) ).
fof(f2081,plain,
( sQ3_spl
| ~ sQ63_spl
| ~ sQ91_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2080]) ).
fof(f2082,plain,
( sQ3_spl
| ~ sQ63_spl
| ~ sQ91_spl ),
inference(contradiction_clause,[status(thm)],[f2081]) ).
fof(f2166,plain,
( sQ2_spl
| ~ sQ91_spl
| ~ sQ121_spl
| ~ greater(high,very_low) ),
inference(backward_demodulation,[status(thm)],[f1850,f2016]) ).
fof(f2167,plain,
( sQ2_spl
| ~ sQ91_spl
| ~ sQ121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2166,f1734]) ).
fof(f2168,plain,
( sQ2_spl
| ~ sQ91_spl
| ~ sQ121_spl ),
inference(contradiction_clause,[status(thm)],[f2167]) ).
fof(f2235,plain,
( ~ has_immunity(sk2,sk5)
| ~ has_endowment(sk2) ),
inference(resolution,[status(thm)],[f67,f110]) ).
fof(f2238,plain,
( ~ sQ57_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f2235,f177,f612]) ).
fof(f2350,plain,
( sQ2_spl
| ~ sQ91_spl
| ~ sQ122_spl
| ~ greater(mod1,very_low) ),
inference(forward_demodulation,[status(thm)],[f1854,f2016]) ).
fof(f2351,plain,
( sQ2_spl
| ~ sQ91_spl
| ~ sQ122_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2350,f1733]) ).
fof(f2352,plain,
( sQ2_spl
| ~ sQ91_spl
| ~ sQ122_spl ),
inference(contradiction_clause,[status(thm)],[f2351]) ).
fof(f2353,plain,
$false,
inference(sat_refutation,[status(thm)],[f125,f573,f617,f646,f1083,f1089,f1227,f1241,f1422,f1714,f1770,f1837,f1852,f1856,f2082,f2168,f2238,f2352]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT065-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 01:29:58 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.52 % Refutation found
% 0.13/0.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.54 % Elapsed time: 0.177861 seconds
% 0.13/0.54 % CPU time: 1.127593 seconds
% 0.13/0.54 % Total memory used: 119.027 MB
% 0.13/0.54 % Net memory used: 117.089 MB
%------------------------------------------------------------------------------