%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT050-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 : n026.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:27 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.40s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 25
% Syntax : Number of formulae : 89 ( 16 unt; 11 def)
% Number of atoms : 200 ( 23 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 206 ( 95 ~; 100 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 12 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 76 ( 76 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A,B] :
( smaller_or_equal(A,B)
| A != B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B] :
( greater_or_equal(A,B)
| 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(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] :
( smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B))
| ~ greater_or_equal(position(A,C),position(A,B))
| ~ greater(capability(A,C),capability(A,B))
| has_immunity(A,C)
| has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A,B,C] :
( smaller(capability(A,B),capability(A,C))
| ~ greater(internal_friction(A,B),internal_friction(A,C))
| ~ smaller_or_equal(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,B,C] :
( position(A,B) = position(A,C)
| external_ties(A,B) != external_ties(A,C)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A,B,C] :
( stock_of_knowledge(A,B) = stock_of_knowledge(A,C)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A,B,C] :
( external_ties(A,B) = external_ties(A,C)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A,B,C] :
( greater(internal_friction(A,B),internal_friction(A,C))
| ~ greater(age(A,B),age(A,C))
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
organization(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
~ has_endowment(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
greater(age(sk1,sk3),age(sk1,sk2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,plain,
! [X0,X1] :
( smaller_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f33,plain,
! [X0,X1] :
( greater_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f34,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f40,plain,
! [A] :
( ! [B] : ~ has_immunity(A,B)
| has_endowment(A)
| ~ organization(A) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f41,plain,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| has_endowment(X0)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f42,plain,
! [X0,X1,X2] :
( smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1))
| ~ greater_or_equal(position(X0,X2),position(X0,X1))
| ~ greater(capability(X0,X2),capability(X0,X1))
| has_immunity(X0,X2)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f46,plain,
! [X0,X1,X2] :
( smaller(capability(X0,X1),capability(X0,X2))
| ~ greater(internal_friction(X0,X1),internal_friction(X0,X2))
| ~ smaller_or_equal(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f49,plain,
! [X0,X1,X2] :
( position(X0,X1) = position(X0,X2)
| external_ties(X0,X1) != external_ties(X0,X2)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f50,plain,
! [A] :
( ! [B,C] : stock_of_knowledge(A,B) = stock_of_knowledge(A,C)
| ~ organization(A) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f51,plain,
! [X0,X1,X2] :
( stock_of_knowledge(X0,X1) = stock_of_knowledge(X0,X2)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
! [A] :
( ! [B,C] : external_ties(A,B) = external_ties(A,C)
| ~ organization(A) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f53,plain,
! [X0,X1,X2] :
( external_ties(X0,X1) = external_ties(X0,X2)
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f54,plain,
! [X0,X1,X2] :
( greater(internal_friction(X0,X1),internal_friction(X0,X2))
| ~ greater(age(X0,X1),age(X0,X2))
| ~ organization(X0) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f55,plain,
organization(sk1),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f56,plain,
~ has_endowment(sk1),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f57,plain,
greater(age(sk1,sk3),age(sk1,sk2)),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f58,plain,
~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f59,plain,
! [X0] : smaller_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f30]) ).
fof(f60,plain,
! [X0] : greater_or_equal(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f33]) ).
fof(f63,plain,
( greater(internal_friction(sk1,sk3),internal_friction(sk1,sk2))
| ~ organization(sk1) ),
inference(resolution,[status(thm)],[f54,f57]) ).
fof(f64,definition,
( sQ0_spl
<=> organization(sk1) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f66,plain,
( sQ0_spl
| ~ organization(sk1) ),
inference(component_clause,[status(thm)],[f64]) ).
fof(f67,definition,
( sQ1_spl
<=> greater(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f68,plain,
( ~ sQ1_spl
| greater(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) ),
inference(component_clause,[status(thm)],[f67]) ).
fof(f70,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f63,f64,f67]) ).
fof(f71,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f66,f55]) ).
fof(f72,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f71]) ).
fof(f251,definition,
( sQ19_spl
<=> has_immunity(sk1,sk2) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f252,plain,
( ~ sQ19_spl
| has_immunity(sk1,sk2) ),
inference(component_clause,[status(thm)],[f251]) ).
fof(f317,plain,
! [X0,X1] :
( smaller(capability(sk1,X0),capability(sk1,X1))
| ~ greater(internal_friction(sk1,X0),internal_friction(sk1,X1))
| ~ smaller_or_equal(stock_of_knowledge(sk1,X0),stock_of_knowledge(sk1,X1)) ),
inference(resolution,[status(thm)],[f46,f55]) ).
fof(f353,definition,
( sQ28_spl
<=> stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f354,plain,
( ~ sQ28_spl
| stock_of_knowledge(sk1,sk2) = stock_of_knowledge(sk1,sk3) ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f355,plain,
( sQ28_spl
| stock_of_knowledge(sk1,sk2) != stock_of_knowledge(sk1,sk3) ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f362,plain,
! [X0] :
( ~ sQ28_spl
| stock_of_knowledge(sk1,X0) = stock_of_knowledge(sk1,sk3)
| ~ organization(sk1) ),
inference(paramodulation,[status(thm)],[f354,f51]) ).
fof(f364,definition,
! [X0] :
( sQ30_spl
<=> stock_of_knowledge(sk1,X0) = stock_of_knowledge(sk1,sk3) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f365,plain,
! [X0] :
( ~ sQ30_spl
| stock_of_knowledge(sk1,X0) = stock_of_knowledge(sk1,sk3) ),
inference(component_clause,[status(thm)],[f364]) ).
fof(f367,plain,
( ~ sQ28_spl
| sQ30_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f362,f64,f364,f353]) ).
fof(f369,plain,
! [X0,X1] :
( ~ sQ30_spl
| stock_of_knowledge(sk1,X0) = stock_of_knowledge(sk1,X1) ),
inference(paramodulation,[status(thm)],[f365,f365]) ).
fof(f398,definition,
( sQ32_spl
<=> has_immunity(sk1,sk3) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( ~ sQ32_spl
| has_immunity(sk1,sk3) ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f401,definition,
( sQ33_spl
<=> greater_or_equal(position(sk1,sk2),position(sk1,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( sQ33_spl
| ~ greater_or_equal(position(sk1,sk2),position(sk1,sk3)) ),
inference(component_clause,[status(thm)],[f401]) ).
fof(f404,definition,
( sQ34_spl
<=> smaller(hazard_of_mortality(sk1,sk2),hazard_of_mortality(sk1,sk3)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f405,plain,
( ~ sQ34_spl
| smaller(hazard_of_mortality(sk1,sk2),hazard_of_mortality(sk1,sk3)) ),
inference(component_clause,[status(thm)],[f404]) ).
fof(f408,plain,
( ~ sQ19_spl
| has_endowment(sk1)
| ~ organization(sk1) ),
inference(resolution,[status(thm)],[f252,f41]) ).
fof(f409,definition,
( sQ35_spl
<=> has_endowment(sk1) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f410,plain,
( ~ sQ35_spl
| has_endowment(sk1) ),
inference(component_clause,[status(thm)],[f409]) ).
fof(f412,plain,
( ~ sQ19_spl
| sQ35_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f408,f64,f409,f251]) ).
fof(f413,plain,
( ~ sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f410,f56]) ).
fof(f414,plain,
~ sQ35_spl,
inference(contradiction_clause,[status(thm)],[f413]) ).
fof(f451,plain,
( ~ sQ1_spl
| smaller(capability(sk1,sk3),capability(sk1,sk2))
| ~ smaller_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ),
inference(resolution,[status(thm)],[f317,f68]) ).
fof(f458,definition,
( sQ39_spl
<=> smaller_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( sQ39_spl
| ~ smaller_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,definition,
( sQ40_spl
<=> smaller(capability(sk1,sk3),capability(sk1,sk2)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f462,plain,
( ~ sQ40_spl
| smaller(capability(sk1,sk3),capability(sk1,sk2)) ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,plain,
( ~ sQ1_spl
| sQ40_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f451,f458,f461,f67]) ).
fof(f483,plain,
( ~ sQ34_spl
| greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) ),
inference(resolution,[status(thm)],[f405,f34]) ).
fof(f485,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f483,f58]) ).
fof(f486,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f485]) ).
fof(f488,plain,
! [X0] :
( ~ sQ30_spl
| sQ39_spl
| ~ smaller_or_equal(stock_of_knowledge(sk1,X0),stock_of_knowledge(sk1,sk2)) ),
inference(paramodulation,[status(thm)],[f369,f460]) ).
fof(f507,plain,
( sQ28_spl
| ~ organization(sk1) ),
inference(resolution,[status(thm)],[f355,f51]) ).
fof(f509,plain,
( sQ28_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f507,f64,f353]) ).
fof(f511,plain,
( ~ sQ32_spl
| has_endowment(sk1)
| ~ organization(sk1) ),
inference(resolution,[status(thm)],[f399,f41]) ).
fof(f512,plain,
( ~ sQ32_spl
| sQ35_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f511,f64,f409,f398]) ).
fof(f527,plain,
! [X0,X1,X2] :
( position(X0,X1) = position(X0,X2)
| ~ organization(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f49,f53]) ).
fof(f528,plain,
! [X0,X1] : position(sk1,X0) = position(sk1,X1),
inference(resolution,[status(thm)],[f527,f55]) ).
fof(f548,plain,
( ~ sQ40_spl
| greater(capability(sk1,sk2),capability(sk1,sk3)) ),
inference(resolution,[status(thm)],[f462,f34]) ).
fof(f601,plain,
! [X0] :
( sQ33_spl
| ~ greater_or_equal(position(sk1,X0),position(sk1,sk3)) ),
inference(paramodulation,[status(thm)],[f528,f403]) ).
fof(f606,plain,
( sQ33_spl
| $false ),
inference(resolution,[status(thm)],[f601,f60]) ).
fof(f611,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f606]) ).
fof(f612,plain,
( ~ sQ40_spl
| smaller(hazard_of_mortality(sk1,sk2),hazard_of_mortality(sk1,sk3))
| ~ greater_or_equal(position(sk1,sk2),position(sk1,sk3))
| has_immunity(sk1,sk2)
| has_immunity(sk1,sk3)
| ~ organization(sk1) ),
inference(resolution,[status(thm)],[f548,f42]) ).
fof(f617,plain,
( ~ sQ40_spl
| sQ34_spl
| ~ sQ33_spl
| sQ19_spl
| sQ32_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f612,f64,f398,f251,f401,f404,f461]) ).
fof(f619,plain,
( ~ sQ30_spl
| sQ39_spl
| $false ),
inference(resolution,[status(thm)],[f488,f59]) ).
fof(f624,plain,
( ~ sQ30_spl
| sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f619]) ).
fof(f625,plain,
$false,
inference(sat_refutation,[status(thm)],[f70,f72,f367,f412,f414,f464,f486,f509,f512,f611,f617,f624]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT050-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.35 % Computer : n026.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 01:27:06 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.14/0.36 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.42 % Elapsed time: 0.063222 seconds
% 0.14/0.42 % CPU time: 0.265362 seconds
% 0.14/0.42 % Total memory used: 76.057 MB
% 0.14/0.42 % Net memory used: 75.733 MB
%------------------------------------------------------------------------------