%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT062-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 : n002.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:31 PM UTC 2026
% Result : Unsatisfiable 5.42s 1.28s
% Output : CNFRefutation 5.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 55
% Syntax : Number of formulae : 203 ( 32 unt; 29 def)
% Number of atoms : 491 ( 63 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 543 ( 255 ~; 259 |; 0 &)
% ( 29 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 30 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 122 ( 122 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A,B] :
( smaller_or_equal(A,B)
| ~ smaller(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( greater(B,A)
| ~ 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(f11,axiom,
! [A,B] :
( greater(A,B)
| A = B
| smaller(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),tau)
| ~ robust_position(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A,B] :
( positional_advantage(A,B)
| ~ greater(age(A,B),tau)
| ~ robust_position(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(f32,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(f34,axiom,
greater(mod2,mod1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
organization(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
robust_position(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
~ has_endowment(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
age(sk2,sk3) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
greater(sigma,zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
sigma = tau,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
smaller_or_equal(age(sk2,sk4),sigma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
greater(age(sk2,sk5),sigma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,plain,
! [X0,X1] :
( smaller_or_equal(X0,X1)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f51,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f52,plain,
! [X0,X1] :
( smaller(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f53,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f56,plain,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f57,plain,
! [A] :
( ! [B] : ~ has_immunity(A,B)
| has_endowment(A)
| ~ organization(A) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f58,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| has_endowment(X0)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
! [A] :
( organization(A)
| ! [B,C] : ~ dissimilar(A,B,C) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f60,plain,
! [X0,X1,X2] :
( organization(X0)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f63,plain,
! [A,C] :
( ~ is_aligned(A,C)
| ! [B] :
( ~ is_aligned(A,B)
| ~ dissimilar(A,B,C) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f67,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(f71,plain,
! [X0,X1] :
( is_aligned(X0,X1)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f72,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(f73,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(f74,plain,
! [X0,X1,X2] :
( greater(age(X0,X2),sigma)
| ~ dissimilar(X0,X1,X2)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f75,plain,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| ~ smaller_or_equal(age(X0,X1),tau)
| ~ robust_position(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f76,plain,
! [X0,X1] :
( positional_advantage(X0,X1)
| ~ greater(age(X0,X1),tau)
| ~ robust_position(X0) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f83,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(f84,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)],[f32]) ).
fof(f86,plain,
greater(mod2,mod1),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f87,plain,
organization(sk2),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f88,plain,
robust_position(sk2),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f89,plain,
~ has_endowment(sk2),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f90,plain,
age(sk2,sk3) = zero,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f91,plain,
greater(sigma,zero),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f93,plain,
sigma = tau,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f94,plain,
smaller_or_equal(age(sk2,sk4),sigma),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f95,plain,
greater(age(sk2,sk5),sigma),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f96,plain,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f97,definition,
( sQ0_spl
<=> smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f99,plain,
( sQ0_spl
| ~ smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
inference(component_clause,[status(thm)],[f97]) ).
fof(f100,definition,
( sQ1_spl
<=> hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f101,plain,
( ~ sQ1_spl
| hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3) ),
inference(component_clause,[status(thm)],[f100]) ).
fof(f102,plain,
( sQ1_spl
| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ),
inference(component_clause,[status(thm)],[f100]) ).
fof(f103,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f96,f97,f100]) ).
fof(f106,plain,
greater(tau,zero),
inference(forward_demodulation,[status(thm)],[f93,f91]) ).
fof(f108,plain,
~ greater(zero,tau),
inference(resolution,[status(thm)],[f53,f106]) ).
fof(f115,plain,
! [X0,X1] :
( greater(X1,X0)
| greater(X0,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f56,f51]) ).
fof(f116,plain,
smaller_or_equal(age(sk2,sk4),tau),
inference(forward_demodulation,[status(thm)],[f93,f94]) ).
fof(f117,plain,
greater(age(sk2,sk5),tau),
inference(forward_demodulation,[status(thm)],[f93,f95]) ).
fof(f119,plain,
~ greater(tau,age(sk2,sk5)),
inference(resolution,[status(thm)],[f117,f53]) ).
fof(f148,plain,
( greater(age(sk2,sk5),tau)
| age(sk2,sk5) = tau ),
inference(resolution,[status(thm)],[f115,f119]) ).
fof(f151,plain,
( greater(tau,zero)
| tau = zero ),
inference(resolution,[status(thm)],[f115,f108]) ).
fof(f156,definition,
( sQ7_spl
<=> age(sk2,sk5) = tau ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f157,plain,
( ~ sQ7_spl
| age(sk2,sk5) = tau ),
inference(component_clause,[status(thm)],[f156]) ).
fof(f159,definition,
( sQ8_spl
<=> greater(age(sk2,sk5),tau) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f160,plain,
( ~ sQ8_spl
| greater(age(sk2,sk5),tau) ),
inference(component_clause,[status(thm)],[f159]) ).
fof(f162,plain,
( sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f148,f156,f159]) ).
fof(f177,definition,
( sQ13_spl
<=> tau = zero ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f178,plain,
( ~ sQ13_spl
| tau = zero ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f180,definition,
( sQ14_spl
<=> greater(tau,zero) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f183,plain,
( sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f151,f177,f180]) ).
fof(f188,plain,
( ~ sQ13_spl
| greater(tau,tau) ),
inference(backward_demodulation,[status(thm)],[f178,f106]) ).
fof(f197,definition,
( sQ16_spl
<=> greater(tau,tau) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f198,plain,
( ~ sQ16_spl
| greater(tau,tau) ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f199,plain,
( sQ16_spl
| ~ greater(tau,tau) ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f212,plain,
( ~ sQ16_spl
| ~ greater(tau,tau) ),
inference(resolution,[status(thm)],[f198,f53]) ).
fof(f213,plain,
( ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f212,f198]) ).
fof(f214,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f213]) ).
fof(f215,plain,
! [X0,X1,X2] :
( dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),tau)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(forward_demodulation,[status(thm)],[f93,f72]) ).
fof(f236,plain,
( ~ sQ13_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f188,f197,f177]) ).
fof(f237,plain,
! [X0,X1,X2] :
( greater(age(X0,X2),tau)
| ~ dissimilar(X0,X1,X2)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(forward_demodulation,[status(thm)],[f93,f74]) ).
fof(f238,plain,
! [X0,X1,X2] :
( greater(age(X0,X2),tau)
| ~ dissimilar(X0,X1,X2)
| age(X0,X1) != zero ),
inference(forward_subsumption_resolution,[status(thm)],[f237,f60]) ).
fof(f242,plain,
( ~ sQ7_spl
| greater(tau,tau) ),
inference(forward_demodulation,[status(thm)],[f157,f117]) ).
fof(f243,plain,
( ~ sQ7_spl
| sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f242,f199]) ).
fof(f244,plain,
( ~ sQ7_spl
| sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f243]) ).
fof(f431,plain,
! [X0,X1] :
( ~ greater(age(X0,X1),tau)
| ~ robust_position(X0)
| ~ smaller_or_equal(age(X0,X1),tau)
| ~ robust_position(X0) ),
inference(resolution,[status(thm)],[f75,f76]) ).
fof(f433,plain,
! [X0,X1] :
( ~ greater(age(X0,X1),tau)
| ~ smaller_or_equal(age(X0,X1),tau)
| ~ robust_position(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f431]) ).
fof(f532,definition,
( sQ33_spl
<=> organization(sk2) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f534,plain,
( sQ33_spl
| ~ organization(sk2) ),
inference(component_clause,[status(thm)],[f532]) ).
fof(f547,plain,
! [X0] :
( ~ positional_advantage(sk2,X0)
| ~ smaller_or_equal(age(sk2,X0),tau) ),
inference(resolution,[status(thm)],[f75,f88]) ).
fof(f569,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f534,f87]) ).
fof(f570,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f569]) ).
fof(f585,definition,
! [X0] :
( sQ37_spl
<=> age(sk2,X0) != zero ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f586,plain,
! [X0] :
( ~ sQ37_spl
| age(sk2,X0) != zero ),
inference(component_clause,[status(thm)],[f585]) ).
fof(f592,plain,
( ~ sQ37_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f90,f586]) ).
fof(f593,plain,
~ sQ37_spl,
inference(contradiction_clause,[status(thm)],[f592]) ).
fof(f763,definition,
! [X0] :
( sQ43_spl
<=> ( age(sk2,X0) != zero
| age(sk2,X0) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f764,plain,
! [X0] :
( ~ sQ43_spl
| age(sk2,X0) != zero
| age(sk2,X0) != zero ),
inference(component_clause,[status(thm)],[f763]) ).
fof(f770,definition,
! [X0] :
( sQ45_spl
<=> ( ~ is_aligned(sk2,X0)
| age(sk2,X0) != zero ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f771,plain,
! [X0] :
( ~ sQ45_spl
| ~ is_aligned(sk2,X0)
| age(sk2,X0) != zero ),
inference(component_clause,[status(thm)],[f770]) ).
fof(f774,plain,
! [X0] :
( ~ sQ43_spl
| age(sk2,X0) != zero ),
inference(duplicate_literals_removal,[status(thm)],[f764]) ).
fof(f775,plain,
( ~ sQ43_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f90,f774]) ).
fof(f776,plain,
~ sQ43_spl,
inference(contradiction_clause,[status(thm)],[f775]) ).
fof(f996,definition,
( sQ50_spl
<=> robust_position(sk2) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f998,plain,
( sQ50_spl
| ~ robust_position(sk2) ),
inference(component_clause,[status(thm)],[f996]) ).
fof(f1003,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f998,f88]) ).
fof(f1004,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f1003]) ).
fof(f1134,plain,
! [X0] :
( positional_advantage(sk2,X0)
| ~ greater(age(sk2,X0),tau) ),
inference(resolution,[status(thm)],[f76,f88]) ).
fof(f1164,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ greater(age(X0,X2),tau)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(resolution,[status(thm)],[f215,f64]) ).
fof(f1165,plain,
! [X0,X1,X2] :
( ~ is_aligned(X0,X2)
| ~ greater(age(X0,X2),tau)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1164,f71]) ).
fof(f1705,definition,
( sQ60_spl
<=> is_aligned(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f1707,plain,
( sQ60_spl
| ~ is_aligned(sk2,sk3) ),
inference(component_clause,[status(thm)],[f1705]) ).
fof(f1805,definition,
( sQ62_spl
<=> greater(age(sk2,sk4),tau) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1829,definition,
( sQ64_spl
<=> is_aligned(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1831,plain,
( sQ64_spl
| ~ is_aligned(sk2,sk5) ),
inference(component_clause,[status(thm)],[f1829]) ).
fof(f1833,plain,
! [X0] :
( ~ sQ45_spl
| age(sk2,X0) != zero
| ~ organization(sk2)
| age(sk2,X0) != zero ),
inference(resolution,[status(thm)],[f771,f71]) ).
fof(f1839,plain,
( ~ sQ45_spl
| ~ sQ33_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f1833,f763,f532,f770]) ).
fof(f1858,plain,
( sQ64_spl
| hazard_of_mortality(sk2,sk5) = mod1
| ~ positional_advantage(sk2,sk5)
| has_immunity(sk2,sk5)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f1831,f83]) ).
fof(f1863,definition,
( sQ69_spl
<=> has_immunity(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1864,plain,
( ~ sQ69_spl
| has_immunity(sk2,sk5) ),
inference(component_clause,[status(thm)],[f1863]) ).
fof(f1866,definition,
( sQ70_spl
<=> positional_advantage(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1873,definition,
( sQ72_spl
<=> hazard_of_mortality(sk2,sk5) = mod1 ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1874,plain,
( ~ sQ72_spl
| hazard_of_mortality(sk2,sk5) = mod1 ),
inference(component_clause,[status(thm)],[f1873]) ).
fof(f1876,plain,
( sQ64_spl
| sQ72_spl
| ~ sQ70_spl
| sQ69_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1858,f532,f1863,f1866,f1873,f1829]) ).
fof(f1886,plain,
( ~ sQ69_spl
| has_endowment(sk2)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f1864,f58]) ).
fof(f1891,definition,
( sQ76_spl
<=> has_endowment(sk2) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1892,plain,
( ~ sQ76_spl
| has_endowment(sk2) ),
inference(component_clause,[status(thm)],[f1891]) ).
fof(f1894,plain,
( ~ sQ69_spl
| sQ76_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f1886,f532,f1891,f1863]) ).
fof(f1898,plain,
( ~ sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1892,f89]) ).
fof(f1899,plain,
~ sQ76_spl,
inference(contradiction_clause,[status(thm)],[f1898]) ).
fof(f1900,plain,
( ~ greater(age(sk2,sk4),tau)
| ~ robust_position(sk2) ),
inference(resolution,[status(thm)],[f116,f433]) ).
fof(f1902,plain,
( ~ sQ62_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1900,f996,f1805]) ).
fof(f1910,plain,
( sQ0_spl
| ~ sQ72_spl
| ~ smaller(mod1,hazard_of_mortality(sk2,sk4)) ),
inference(backward_demodulation,[status(thm)],[f1874,f99]) ).
fof(f2020,definition,
( sQ88_spl
<=> positional_advantage(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f2021,plain,
( ~ sQ88_spl
| positional_advantage(sk2,sk3) ),
inference(component_clause,[status(thm)],[f2020]) ).
fof(f2025,plain,
( ~ sQ88_spl
| ~ smaller_or_equal(age(sk2,sk3),tau)
| ~ robust_position(sk2) ),
inference(resolution,[status(thm)],[f2021,f75]) ).
fof(f2028,definition,
( sQ89_spl
<=> smaller_or_equal(age(sk2,sk3),tau) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2030,plain,
( sQ89_spl
| ~ smaller_or_equal(age(sk2,sk3),tau) ),
inference(component_clause,[status(thm)],[f2028]) ).
fof(f2031,plain,
( ~ sQ88_spl
| ~ sQ89_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f2025,f996,f2028,f2020]) ).
fof(f2032,definition,
( sQ90_spl
<=> has_immunity(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2033,plain,
( ~ sQ90_spl
| has_immunity(sk2,sk3) ),
inference(component_clause,[status(thm)],[f2032]) ).
fof(f2034,plain,
( sQ90_spl
| ~ has_immunity(sk2,sk3) ),
inference(component_clause,[status(thm)],[f2032]) ).
fof(f2039,plain,
( sQ89_spl
| ~ smaller_or_equal(zero,tau) ),
inference(forward_demodulation,[status(thm)],[f90,f2030]) ).
fof(f2041,plain,
( sQ60_spl
| age(sk2,sk3) != zero
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f1707,f71]) ).
fof(f2050,definition,
( sQ93_spl
<=> age(sk2,sk3) = zero ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f2052,plain,
( sQ93_spl
| age(sk2,sk3) != zero ),
inference(component_clause,[status(thm)],[f2050]) ).
fof(f2053,plain,
( sQ60_spl
| ~ sQ93_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f2041,f532,f2050,f1705]) ).
fof(f2066,plain,
( sQ93_spl
| zero != zero ),
inference(forward_demodulation,[status(thm)],[f90,f2052]) ).
fof(f2067,plain,
( sQ93_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2066]) ).
fof(f2068,plain,
sQ93_spl,
inference(contradiction_clause,[status(thm)],[f2067]) ).
fof(f2069,plain,
( sQ89_spl
| ~ smaller(zero,tau) ),
inference(resolution,[status(thm)],[f2039,f46]) ).
fof(f2071,plain,
( ~ sQ90_spl
| has_endowment(sk2)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f2033,f58]) ).
fof(f2076,plain,
( ~ sQ90_spl
| sQ76_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f2071,f532,f1891,f2032]) ).
fof(f2079,plain,
( sQ89_spl
| ~ greater(tau,zero) ),
inference(resolution,[status(thm)],[f2069,f52]) ).
fof(f2082,plain,
( sQ89_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f2079,f180,f2028]) ).
fof(f2092,definition,
( sQ98_spl
<=> hazard_of_mortality(sk2,sk3) = mod2 ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f2093,plain,
( ~ sQ98_spl
| hazard_of_mortality(sk2,sk3) = mod2 ),
inference(component_clause,[status(thm)],[f2092]) ).
fof(f2384,definition,
( sQ111_spl
<=> has_immunity(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f2385,plain,
( ~ sQ111_spl
| has_immunity(sk2,sk4) ),
inference(component_clause,[status(thm)],[f2384]) ).
fof(f2386,plain,
( sQ111_spl
| ~ has_immunity(sk2,sk4) ),
inference(component_clause,[status(thm)],[f2384]) ).
fof(f2387,definition,
( sQ112_spl
<=> is_aligned(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f2389,plain,
( sQ112_spl
| ~ is_aligned(sk2,sk4) ),
inference(component_clause,[status(thm)],[f2387]) ).
fof(f2390,definition,
( sQ113_spl
<=> positional_advantage(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f2391,plain,
( ~ sQ113_spl
| positional_advantage(sk2,sk4) ),
inference(component_clause,[status(thm)],[f2390]) ).
fof(f2438,plain,
( ~ sQ8_spl
| positional_advantage(sk2,sk5) ),
inference(resolution,[status(thm)],[f1134,f160]) ).
fof(f2441,plain,
( ~ sQ8_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f2438,f1866,f159]) ).
fof(f2450,plain,
( sQ1_spl
| ~ sQ98_spl
| hazard_of_mortality(sk2,sk4) != mod2 ),
inference(forward_demodulation,[status(thm)],[f2093,f102]) ).
fof(f2487,plain,
! [X0] :
( sQ112_spl
| dissimilar(sk2,X0,sk4)
| ~ is_aligned(sk2,X0)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f2389,f67]) ).
fof(f2499,definition,
! [X0] :
( sQ117_spl
<=> ( dissimilar(sk2,X0,sk4)
| ~ is_aligned(sk2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f2500,plain,
! [X0] :
( ~ sQ117_spl
| dissimilar(sk2,X0,sk4)
| ~ is_aligned(sk2,X0) ),
inference(component_clause,[status(thm)],[f2499]) ).
fof(f2502,plain,
( sQ112_spl
| sQ117_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f2487,f532,f2499,f2387]) ).
fof(f2503,plain,
( ~ sQ111_spl
| has_endowment(sk2)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f2385,f58]) ).
fof(f2504,plain,
( ~ sQ111_spl
| sQ76_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f2503,f532,f1891,f2384]) ).
fof(f2546,plain,
! [X0] :
( hazard_of_mortality(sk2,X0) = mod2
| positional_advantage(sk2,X0)
| ~ is_aligned(sk2,X0)
| has_immunity(sk2,X0) ),
inference(resolution,[status(thm)],[f84,f87]) ).
fof(f2676,definition,
( sQ121_spl
<=> mod2 = hazard_of_mortality(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f2677,plain,
( ~ sQ121_spl
| mod2 = hazard_of_mortality(sk2,sk4) ),
inference(component_clause,[status(thm)],[f2676]) ).
fof(f2687,plain,
( ~ sQ121_spl
| sQ1_spl
| ~ sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2677,f2450]) ).
fof(f2688,plain,
( ~ sQ121_spl
| sQ1_spl
| ~ sQ98_spl ),
inference(contradiction_clause,[status(thm)],[f2687]) ).
fof(f3844,plain,
( sQ111_spl
| hazard_of_mortality(sk2,sk4) = mod2
| positional_advantage(sk2,sk4)
| ~ is_aligned(sk2,sk4) ),
inference(resolution,[status(thm)],[f2546,f2386]) ).
fof(f3845,plain,
( sQ90_spl
| hazard_of_mortality(sk2,sk3) = mod2
| positional_advantage(sk2,sk3)
| ~ is_aligned(sk2,sk3) ),
inference(resolution,[status(thm)],[f2546,f2034]) ).
fof(f3849,plain,
( sQ111_spl
| sQ121_spl
| sQ113_spl
| ~ sQ112_spl ),
inference(split_clause,[status(thm)],[f3844,f2387,f2390,f2676,f2384]) ).
fof(f3850,plain,
( sQ90_spl
| sQ98_spl
| sQ88_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f3845,f1705,f2020,f2092,f2032]) ).
fof(f3895,plain,
( ~ sQ113_spl
| ~ smaller_or_equal(age(sk2,sk4),tau) ),
inference(resolution,[status(thm)],[f2391,f547]) ).
fof(f3896,plain,
( ~ sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3895,f116]) ).
fof(f3897,plain,
~ sQ113_spl,
inference(contradiction_clause,[status(thm)],[f3896]) ).
fof(f3921,plain,
( ~ sQ1_spl
| ~ sQ98_spl
| hazard_of_mortality(sk2,sk4) = mod2 ),
inference(forward_demodulation,[status(thm)],[f2093,f101]) ).
fof(f4027,plain,
( sQ0_spl
| ~ sQ72_spl
| ~ sQ1_spl
| ~ sQ98_spl
| ~ smaller(mod1,mod2) ),
inference(backward_demodulation,[status(thm)],[f3921,f1910]) ).
fof(f4056,plain,
( sQ0_spl
| ~ sQ72_spl
| ~ sQ1_spl
| ~ sQ98_spl
| ~ greater(mod2,mod1) ),
inference(resolution,[status(thm)],[f4027,f52]) ).
fof(f4062,plain,
( sQ0_spl
| ~ sQ72_spl
| ~ sQ1_spl
| ~ sQ98_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4056,f86]) ).
fof(f4063,plain,
( sQ0_spl
| ~ sQ72_spl
| ~ sQ1_spl
| ~ sQ98_spl ),
inference(contradiction_clause,[status(thm)],[f4062]) ).
fof(f4672,plain,
! [X0] :
( ~ sQ8_spl
| ~ is_aligned(sk2,sk5)
| age(sk2,X0) != zero
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[f160,f1165]) ).
fof(f4680,plain,
( ~ sQ8_spl
| ~ sQ64_spl
| sQ37_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f4672,f532,f585,f1829,f159]) ).
fof(f4823,plain,
! [X0] :
( ~ sQ117_spl
| greater(age(sk2,sk4),tau)
| age(sk2,X0) != zero
| ~ is_aligned(sk2,X0) ),
inference(resolution,[status(thm)],[f2500,f238]) ).
fof(f4827,plain,
( ~ sQ117_spl
| sQ62_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f4823,f770,f1805,f2499]) ).
fof(f4830,plain,
$false,
inference(sat_refutation,[status(thm)],[f103,f162,f183,f214,f236,f244,f570,f593,f776,f1004,f1839,f1876,f1894,f1899,f1902,f2031,f2053,f2068,f2076,f2082,f2441,f2502,f2504,f2688,f3849,f3850,f3897,f4063,f4680,f4827]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT062-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n002.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:27:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 5.42/1.28 % Refutation found
% 5.42/1.28 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.42/1.28 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.79/1.31 % Elapsed time: 0.927736 seconds
% 0.79/1.31 % CPU time: 7.035915 seconds
% 0.79/1.31 % Total memory used: 152.837 MB
% 0.79/1.31 % Net memory used: 144.447 MB
%------------------------------------------------------------------------------