%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT047-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 : n014.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:26 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.50s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 57
% Syntax : Number of formulae : 206 ( 24 unt; 31 def)
% Number of atoms : 488 ( 37 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 509 ( 227 ~; 251 |; 0 &)
% ( 31 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 32 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 122 ( 122 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( A = B
| smaller(A,B)
| ~ smaller_or_equal(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] :
( smaller_or_equal(A,B)
| ~ smaller(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] :
( smaller_or_equal(A,B)
| A != B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B] :
( greater_or_equal(A,B)
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B] :
( greater_or_equal(A,B)
| A != B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( greater(B,A)
| ~ smaller(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] :
( ~ greater(B,A)
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B,C] :
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] :
( greater(A,B)
| A = B
| smaller(A,B) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B] :
( ~ has_immunity(A,B)
| ~ greater(age(A,B),eta)
| ~ has_endowment(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A,B,C] :
( hazard_of_mortality(A,B) = hazard_of_mortality(A,C)
| ~ has_immunity(A,C)
| ~ has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,B,C] :
( greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B))
| has_immunity(A,C)
| ~ has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A,B,C] :
( smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B))
| ~ greater(position(A,C),position(A,B))
| ~ greater_or_equal(capability(A,C),capability(A,B))
| has_immunity(A,C)
| has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A,B,C] :
( greater(capability(A,B),capability(A,C))
| ~ smaller_or_equal(internal_friction(A,B),internal_friction(A,C))
| ~ greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A,B,C] :
( greater(position(A,B),position(A,C))
| ~ greater(external_ties(A,B),external_ties(A,C))
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [A,B,C] :
( greater(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
| ~ greater(age(A,B),age(A,C))
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A,B,C] :
( greater(external_ties(A,B),external_ties(A,C))
| ~ greater(age(A,B),age(A,C))
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A,B,C] :
( internal_friction(A,B) = internal_friction(A,C)
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
organization(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,negated_conjecture,
has_endowment(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
smaller_or_equal(age(sk2,sk3),age(sk2,sk4)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
smaller_or_equal(age(sk2,sk4),eta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
greater(age(sk2,sk5),eta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
greater(age(sk2,sk6),age(sk2,sk5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4))
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,plain,
! [X0,X1] :
( X0 = X1
| smaller(X0,X1)
| ~ smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f40,plain,
! [X0,X1] :
( smaller_or_equal(X0,X1)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f41,plain,
! [X0,X1] :
( smaller_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f43,plain,
! [X0,X1] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f44,plain,
! [X0,X1] :
( greater_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f45,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f47,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f48,plain,
! [A,C] :
( greater(A,C)
| ! [B] :
( ~ greater(B,C)
| ~ greater(A,B) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f49,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f52,plain,
! [X0,X1] :
( has_immunity(X0,X1)
| ~ smaller_or_equal(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f53,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| ~ greater(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f58,plain,
! [X0,X1,X2] :
( hazard_of_mortality(X0,X1) = hazard_of_mortality(X0,X2)
| ~ has_immunity(X0,X2)
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f59,plain,
! [X0,X1,X2] :
( greater(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1))
| has_immunity(X0,X2)
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f61,plain,
! [X0,X1,X2] :
( smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1))
| ~ greater(position(X0,X2),position(X0,X1))
| ~ greater_or_equal(capability(X0,X2),capability(X0,X1))
| has_immunity(X0,X2)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f63,plain,
! [X0,X1,X2] :
( greater(capability(X0,X1),capability(X0,X2))
| ~ smaller_or_equal(internal_friction(X0,X1),internal_friction(X0,X2))
| ~ greater(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f66,plain,
! [X0,X1,X2] :
( greater(position(X0,X1),position(X0,X2))
| ~ greater(external_ties(X0,X1),external_ties(X0,X2))
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f68,plain,
! [X0,X1,X2] :
( greater(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))
| ~ greater(age(X0,X1),age(X0,X2))
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f69,plain,
! [X0,X1,X2] :
( greater(external_ties(X0,X1),external_ties(X0,X2))
| ~ greater(age(X0,X1),age(X0,X2))
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f70,plain,
! [A] :
( ! [B,C] : internal_friction(A,B) = internal_friction(A,C)
| ~ organization(A) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f71,plain,
! [X0,X1,X2] :
( internal_friction(X0,X1) = internal_friction(X0,X2)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f72,plain,
organization(sk2),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f73,plain,
has_endowment(sk2),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f74,plain,
smaller_or_equal(age(sk2,sk3),age(sk2,sk4)),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f75,plain,
smaller_or_equal(age(sk2,sk4),eta),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f76,plain,
greater(age(sk2,sk5),eta),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f77,plain,
greater(age(sk2,sk6),age(sk2,sk5)),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f78,plain,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4))
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6)) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f79,definition,
( sQ0_spl
<=> greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f82,definition,
( sQ1_spl
<=> greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f84,plain,
( sQ1_spl
| ~ greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk4)) ),
inference(component_clause,[status(thm)],[f82]) ).
fof(f85,definition,
( sQ2_spl
<=> hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f87,plain,
( sQ2_spl
| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ),
inference(component_clause,[status(thm)],[f85]) ).
fof(f88,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f78,f79,f82,f85]) ).
fof(f89,plain,
! [X0] : smaller_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f41]) ).
fof(f90,plain,
! [X0] : greater_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f44]) ).
fof(f92,plain,
! [X0] :
( greater(X0,eta)
| ~ greater(X0,age(sk2,sk5)) ),
inference(resolution,[status(thm)],[f49,f76]) ).
fof(f93,plain,
( ~ has_immunity(sk2,sk5)
| ~ has_endowment(sk2) ),
inference(resolution,[status(thm)],[f53,f76]) ).
fof(f94,definition,
( sQ3_spl
<=> has_endowment(sk2) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f96,plain,
( sQ3_spl
| ~ has_endowment(sk2) ),
inference(component_clause,[status(thm)],[f94]) ).
fof(f97,definition,
( sQ4_spl
<=> has_immunity(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f100,plain,
( ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f93,f94,f97]) ).
fof(f101,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f96,f73]) ).
fof(f102,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f101]) ).
fof(f109,plain,
! [X0,X1] :
( greater(X1,X0)
| X0 = X1
| ~ smaller_or_equal(X0,X1) ),
inference(resolution,[status(thm)],[f39,f45]) ).
fof(f114,plain,
! [X0,X1] :
( smaller_or_equal(X0,X1)
| greater(X0,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f50,f40]) ).
fof(f120,plain,
greater(age(sk2,sk6),eta),
inference(resolution,[status(thm)],[f92,f77]) ).
fof(f121,plain,
( ~ has_immunity(sk2,sk6)
| ~ has_endowment(sk2) ),
inference(resolution,[status(thm)],[f120,f53]) ).
fof(f125,definition,
( sQ6_spl
<=> has_immunity(sk2,sk6) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f127,plain,
( sQ6_spl
| ~ has_immunity(sk2,sk6) ),
inference(component_clause,[status(thm)],[f125]) ).
fof(f128,plain,
( ~ sQ6_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f121,f94,f125]) ).
fof(f141,plain,
( greater(age(sk2,sk4),age(sk2,sk3))
| age(sk2,sk3) = age(sk2,sk4) ),
inference(resolution,[status(thm)],[f109,f74]) ).
fof(f142,plain,
( greater(eta,age(sk2,sk4))
| age(sk2,sk4) = eta ),
inference(resolution,[status(thm)],[f109,f75]) ).
fof(f153,definition,
( sQ10_spl
<=> age(sk2,sk3) = age(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f154,plain,
( ~ sQ10_spl
| age(sk2,sk3) = age(sk2,sk4) ),
inference(component_clause,[status(thm)],[f153]) ).
fof(f156,definition,
( sQ11_spl
<=> greater(age(sk2,sk4),age(sk2,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f157,plain,
( ~ sQ11_spl
| greater(age(sk2,sk4),age(sk2,sk3)) ),
inference(component_clause,[status(thm)],[f156]) ).
fof(f159,plain,
( sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f141,f153,f156]) ).
fof(f160,definition,
( sQ12_spl
<=> age(sk2,sk4) = eta ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f161,plain,
( ~ sQ12_spl
| age(sk2,sk4) = eta ),
inference(component_clause,[status(thm)],[f160]) ).
fof(f163,definition,
( sQ13_spl
<=> greater(eta,age(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f164,plain,
( ~ sQ13_spl
| greater(eta,age(sk2,sk4)) ),
inference(component_clause,[status(thm)],[f163]) ).
fof(f166,plain,
( sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f142,f160,f163]) ).
fof(f167,plain,
( ~ sQ12_spl
| smaller_or_equal(age(sk2,sk3),eta) ),
inference(backward_demodulation,[status(thm)],[f161,f74]) ).
fof(f173,definition,
( sQ15_spl
<=> has_immunity(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f174,plain,
( ~ sQ15_spl
| has_immunity(sk2,sk4) ),
inference(component_clause,[status(thm)],[f173]) ).
fof(f175,plain,
( sQ15_spl
| ~ has_immunity(sk2,sk4) ),
inference(component_clause,[status(thm)],[f173]) ).
fof(f177,plain,
( sQ15_spl
| ~ smaller_or_equal(age(sk2,sk4),eta)
| ~ has_endowment(sk2) ),
inference(resolution,[status(thm)],[f175,f52]) ).
fof(f178,definition,
( sQ16_spl
<=> smaller_or_equal(age(sk2,sk4),eta) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f180,plain,
( sQ16_spl
| ~ smaller_or_equal(age(sk2,sk4),eta) ),
inference(component_clause,[status(thm)],[f178]) ).
fof(f181,plain,
( sQ15_spl
| ~ sQ16_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f177,f94,f178,f173]) ).
fof(f231,plain,
( ~ sQ13_spl
| ~ greater(age(sk2,sk4),eta) ),
inference(resolution,[status(thm)],[f164,f47]) ).
fof(f234,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f180,f75]) ).
fof(f235,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f234]) ).
fof(f236,plain,
! [X0] :
( ~ sQ15_spl
| greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk4))
| has_immunity(sk2,X0)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f174,f59]) ).
fof(f237,plain,
! [X0] :
( ~ sQ15_spl
| hazard_of_mortality(sk2,X0) = hazard_of_mortality(sk2,sk4)
| ~ has_immunity(sk2,X0)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f174,f58]) ).
fof(f238,definition,
( sQ20_spl
<=> organization(sk2) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f240,plain,
( sQ20_spl
| ~ organization(sk2) ),
inference(component_clause,[status(thm)],[f238]) ).
fof(f241,definition,
! [X0] :
( sQ21_spl
<=> ( greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk4))
| has_immunity(sk2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f242,plain,
! [X0] :
( ~ sQ21_spl
| greater(hazard_of_mortality(sk2,X0),hazard_of_mortality(sk2,sk4))
| has_immunity(sk2,X0) ),
inference(component_clause,[status(thm)],[f241]) ).
fof(f244,plain,
( ~ sQ15_spl
| sQ21_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f236,f238,f241,f173]) ).
fof(f245,definition,
! [X0] :
( sQ22_spl
<=> ( hazard_of_mortality(sk2,X0) = hazard_of_mortality(sk2,sk4)
| ~ has_immunity(sk2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f246,plain,
! [X0] :
( ~ sQ22_spl
| hazard_of_mortality(sk2,X0) = hazard_of_mortality(sk2,sk4)
| ~ has_immunity(sk2,X0) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f248,plain,
( ~ sQ15_spl
| sQ22_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f237,f238,f245,f173]) ).
fof(f249,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f240,f72]) ).
fof(f250,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f249]) ).
fof(f292,definition,
( sQ23_spl
<=> greater(age(sk2,sk4),eta) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f294,plain,
( sQ23_spl
| ~ greater(age(sk2,sk4),eta) ),
inference(component_clause,[status(thm)],[f292]) ).
fof(f295,definition,
( sQ24_spl
<=> has_immunity(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f296,plain,
( ~ sQ24_spl
| has_immunity(sk2,sk3) ),
inference(component_clause,[status(thm)],[f295]) ).
fof(f297,plain,
( sQ24_spl
| ~ has_immunity(sk2,sk3) ),
inference(component_clause,[status(thm)],[f295]) ).
fof(f299,plain,
( sQ24_spl
| ~ smaller_or_equal(age(sk2,sk3),eta)
| ~ has_endowment(sk2) ),
inference(resolution,[status(thm)],[f297,f52]) ).
fof(f300,definition,
( sQ25_spl
<=> smaller_or_equal(age(sk2,sk3),eta) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f302,plain,
( sQ25_spl
| ~ smaller_or_equal(age(sk2,sk3),eta) ),
inference(component_clause,[status(thm)],[f300]) ).
fof(f303,plain,
( sQ24_spl
| ~ sQ25_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f299,f94,f300,f295]) ).
fof(f304,plain,
( sQ25_spl
| greater(age(sk2,sk3),eta)
| age(sk2,sk3) = eta ),
inference(resolution,[status(thm)],[f302,f114]) ).
fof(f305,definition,
( sQ26_spl
<=> age(sk2,sk3) = eta ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f306,plain,
( ~ sQ26_spl
| age(sk2,sk3) = eta ),
inference(component_clause,[status(thm)],[f305]) ).
fof(f308,definition,
( sQ27_spl
<=> greater(age(sk2,sk3),eta) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f309,plain,
( ~ sQ27_spl
| greater(age(sk2,sk3),eta) ),
inference(component_clause,[status(thm)],[f308]) ).
fof(f311,plain,
( sQ25_spl
| sQ27_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f304,f305,f308,f300]) ).
fof(f312,plain,
( sQ25_spl
| ~ sQ26_spl
| ~ smaller_or_equal(eta,eta) ),
inference(backward_demodulation,[status(thm)],[f306,f302]) ).
fof(f314,plain,
( sQ25_spl
| ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f312,f89]) ).
fof(f315,plain,
( sQ25_spl
| ~ sQ26_spl ),
inference(contradiction_clause,[status(thm)],[f314]) ).
fof(f318,plain,
! [X0] :
( ~ sQ27_spl
| greater(X0,eta)
| ~ greater(X0,age(sk2,sk3)) ),
inference(resolution,[status(thm)],[f309,f49]) ).
fof(f319,plain,
( ~ sQ27_spl
| ~ greater(eta,age(sk2,sk3)) ),
inference(resolution,[status(thm)],[f309,f47]) ).
fof(f335,plain,
! [X0,X1] : internal_friction(sk2,X0) = internal_friction(sk2,X1),
inference(resolution,[status(thm)],[f71,f72]) ).
fof(f368,plain,
( greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5))
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f68,f77]) ).
fof(f370,definition,
( sQ32_spl
<=> greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f371,plain,
( ~ sQ32_spl
| greater(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f370]) ).
fof(f373,plain,
( sQ32_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f368,f238,f370]) ).
fof(f438,plain,
( ~ sQ27_spl
| ~ sQ10_spl
| ~ greater(eta,age(sk2,sk4)) ),
inference(backward_demodulation,[status(thm)],[f154,f319]) ).
fof(f447,plain,
( ~ sQ27_spl
| ~ sQ10_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f438,f164]) ).
fof(f448,plain,
( ~ sQ27_spl
| ~ sQ10_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f447]) ).
fof(f466,plain,
( greater(external_ties(sk2,sk6),external_ties(sk2,sk5))
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f69,f77]) ).
fof(f468,definition,
( sQ39_spl
<=> greater(external_ties(sk2,sk6),external_ties(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( ~ sQ39_spl
| greater(external_ties(sk2,sk6),external_ties(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,plain,
( sQ39_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f466,f238,f468]) ).
fof(f516,plain,
( ~ sQ32_spl
| greater(capability(sk2,sk6),capability(sk2,sk5))
| ~ smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk5))
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f371,f63]) ).
fof(f521,definition,
( sQ40_spl
<=> smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( sQ40_spl
| ~ smaller_or_equal(internal_friction(sk2,sk6),internal_friction(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,definition,
( sQ41_spl
<=> greater(capability(sk2,sk6),capability(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f525,plain,
( ~ sQ41_spl
| greater(capability(sk2,sk6),capability(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f524]) ).
fof(f527,plain,
( ~ sQ32_spl
| sQ41_spl
| ~ sQ40_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f516,f238,f521,f524,f370]) ).
fof(f548,definition,
( sQ45_spl
<=> greater(capability(sk2,sk5),capability(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f549,plain,
( ~ sQ45_spl
| greater(capability(sk2,sk5),capability(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f548]) ).
fof(f563,plain,
( ~ sQ27_spl
| ~ sQ11_spl
| greater(age(sk2,sk4),eta) ),
inference(resolution,[status(thm)],[f157,f318]) ).
fof(f573,plain,
( ~ sQ27_spl
| ~ sQ11_spl
| sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f563,f294]) ).
fof(f574,plain,
( ~ sQ27_spl
| ~ sQ11_spl
| sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f573]) ).
fof(f575,plain,
( ~ sQ13_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f231,f292,f163]) ).
fof(f577,plain,
( ~ sQ12_spl
| sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f167,f302]) ).
fof(f578,plain,
( ~ sQ12_spl
| sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f577]) ).
fof(f675,plain,
( ~ sQ39_spl
| greater(position(sk2,sk6),position(sk2,sk5))
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f469,f66]) ).
fof(f680,definition,
( sQ58_spl
<=> greater(position(sk2,sk6),position(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f681,plain,
( ~ sQ58_spl
| greater(position(sk2,sk6),position(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f680]) ).
fof(f683,plain,
( ~ sQ39_spl
| sQ58_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f675,f238,f680,f468]) ).
fof(f692,plain,
! [X0] :
( sQ40_spl
| ~ smaller_or_equal(internal_friction(sk2,X0),internal_friction(sk2,sk5)) ),
inference(paramodulation,[status(thm)],[f335,f523]) ).
fof(f699,definition,
( sQ61_spl
<=> greater(internal_friction(sk2,sk6),internal_friction(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f700,plain,
( ~ sQ61_spl
| greater(internal_friction(sk2,sk6),internal_friction(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f699]) ).
fof(f711,definition,
( sQ63_spl
<=> smaller(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f712,plain,
( ~ sQ63_spl
| smaller(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f711]) ).
fof(f716,plain,
( sQ40_spl
| $false ),
inference(resolution,[status(thm)],[f692,f89]) ).
fof(f721,plain,
sQ40_spl,
inference(contradiction_clause,[status(thm)],[f716]) ).
fof(f750,plain,
( ~ sQ45_spl
| ~ greater(capability(sk2,sk5),capability(sk2,sk5)) ),
inference(resolution,[status(thm)],[f549,f47]) ).
fof(f751,definition,
( sQ68_spl
<=> greater_or_equal(position(sk2,sk5),position(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f753,plain,
( sQ68_spl
| ~ greater_or_equal(position(sk2,sk5),position(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f751]) ).
fof(f758,plain,
( ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f750,f549]) ).
fof(f759,plain,
~ sQ45_spl,
inference(contradiction_clause,[status(thm)],[f758]) ).
fof(f760,plain,
( sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f753,f90]) ).
fof(f761,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f760]) ).
fof(f792,definition,
( sQ75_spl
<=> hazard_of_mortality(sk2,sk6) = hazard_of_mortality(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f793,plain,
( ~ sQ75_spl
| hazard_of_mortality(sk2,sk6) = hazard_of_mortality(sk2,sk5) ),
inference(component_clause,[status(thm)],[f792]) ).
fof(f805,plain,
( ~ sQ58_spl
| smaller(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5))
| ~ greater_or_equal(capability(sk2,sk6),capability(sk2,sk5))
| has_immunity(sk2,sk6)
| has_immunity(sk2,sk5)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f681,f61]) ).
fof(f810,definition,
( sQ77_spl
<=> greater_or_equal(capability(sk2,sk6),capability(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f812,plain,
( sQ77_spl
| ~ greater_or_equal(capability(sk2,sk6),capability(sk2,sk5)) ),
inference(component_clause,[status(thm)],[f810]) ).
fof(f813,plain,
( ~ sQ58_spl
| sQ63_spl
| ~ sQ77_spl
| sQ6_spl
| sQ4_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f805,f238,f97,f125,f810,f711,f680]) ).
fof(f831,plain,
! [X0] :
( ~ sQ61_spl
| greater(internal_friction(sk2,X0),internal_friction(sk2,sk5)) ),
inference(paramodulation,[status(thm)],[f335,f700]) ).
fof(f849,plain,
! [X0,X1] :
( ~ sQ61_spl
| greater(internal_friction(sk2,X0),internal_friction(sk2,X1)) ),
inference(paramodulation,[status(thm)],[f335,f831]) ).
fof(f1038,plain,
( sQ77_spl
| ~ greater(capability(sk2,sk6),capability(sk2,sk5)) ),
inference(resolution,[status(thm)],[f812,f43]) ).
fof(f1039,plain,
( sQ77_spl
| ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1038,f525]) ).
fof(f1040,plain,
( sQ77_spl
| ~ sQ41_spl ),
inference(contradiction_clause,[status(thm)],[f1039]) ).
fof(f1095,plain,
! [X0,X1] :
( ~ sQ61_spl
| ~ greater(internal_friction(sk2,X0),internal_friction(sk2,X1)) ),
inference(resolution,[status(thm)],[f849,f47]) ).
fof(f1104,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1095,f849]) ).
fof(f1105,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f1104]) ).
fof(f1151,plain,
( ~ sQ63_spl
| greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6)) ),
inference(resolution,[status(thm)],[f712,f45]) ).
fof(f1152,plain,
( ~ sQ63_spl
| smaller_or_equal(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5)) ),
inference(resolution,[status(thm)],[f712,f40]) ).
fof(f1261,plain,
( ~ sQ63_spl
| greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6))
| hazard_of_mortality(sk2,sk6) = hazard_of_mortality(sk2,sk5) ),
inference(resolution,[status(thm)],[f1152,f109]) ).
fof(f1262,plain,
( ~ sQ63_spl
| sQ0_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1261,f792,f79,f711]) ).
fof(f1273,plain,
( ~ sQ63_spl
| ~ sQ75_spl
| greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk5)) ),
inference(forward_demodulation,[status(thm)],[f793,f1151]) ).
fof(f1277,plain,
( ~ sQ63_spl
| ~ sQ75_spl
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk5)) ),
inference(resolution,[status(thm)],[f1273,f47]) ).
fof(f1278,plain,
( ~ sQ63_spl
| ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1277,f1273]) ).
fof(f1279,plain,
( ~ sQ63_spl
| ~ sQ75_spl ),
inference(contradiction_clause,[status(thm)],[f1278]) ).
fof(f1406,plain,
( ~ sQ24_spl
| ~ sQ22_spl
| hazard_of_mortality(sk2,sk3) = hazard_of_mortality(sk2,sk4) ),
inference(resolution,[status(thm)],[f246,f296]) ).
fof(f1874,plain,
( ~ sQ21_spl
| sQ1_spl
| has_immunity(sk2,sk6) ),
inference(resolution,[status(thm)],[f84,f242]) ).
fof(f1878,plain,
( ~ sQ21_spl
| sQ1_spl
| sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1874,f127]) ).
fof(f1879,plain,
( ~ sQ21_spl
| sQ1_spl
| sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f1878]) ).
fof(f1880,plain,
( sQ2_spl
| ~ sQ24_spl
| ~ sQ22_spl
| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk4) ),
inference(forward_demodulation,[status(thm)],[f1406,f87]) ).
fof(f1881,plain,
( sQ2_spl
| ~ sQ24_spl
| ~ sQ22_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1880]) ).
fof(f1882,plain,
( sQ2_spl
| ~ sQ24_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f1881]) ).
fof(f1883,plain,
$false,
inference(sat_refutation,[status(thm)],[f88,f100,f102,f128,f159,f166,f181,f235,f244,f248,f250,f303,f311,f315,f373,f448,f471,f527,f574,f575,f578,f683,f721,f759,f761,f813,f1040,f1105,f1262,f1279,f1879,f1882]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT047-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n014.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 01:23:51 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.50 % Refutation found
% 0.09/0.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.51 % Elapsed time: 0.134756 seconds
% 0.09/0.51 % CPU time: 0.812007 seconds
% 0.09/0.51 % Total memory used: 92.613 MB
% 0.09/0.51 % Net memory used: 91.494 MB
%------------------------------------------------------------------------------