%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : MGT064-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.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 : Tue Sep 29 12:02:18 PM UTC 2026
% Result : Unsatisfiable 2.83s 1.31s
% Output : Refutation 3.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 50
% Syntax : Number of formulae : 213 ( 50 unt; 19 def)
% Number of atoms : 469 ( 41 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 490 ( 234 ~; 237 |; 0 &)
% ( 19 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 20 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 53 ( 0 sgn 53 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ smaller_or_equal(X0,X1)
| smaller(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_smaller_or_equal_1) ).
fof(f2,axiom,
! [X0,X1] :
( ~ smaller(X0,X1)
| smaller_or_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_smaller_or_equal_2) ).
fof(f7,axiom,
! [X0,X1] :
( ~ smaller(X0,X1)
| greater(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_smaller_7) ).
fof(f8,axiom,
! [X0,X1] :
( ~ greater(X0,X1)
| smaller(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_smaller_8) ).
fof(f9,axiom,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meaning_postulate_greater_strict_9) ).
fof(f10,axiom,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meaning_postulate_greater_transitive_10) ).
fof(f19,axiom,
! [X0,X1] :
( ~ has_immunity(X0,X1)
| has_endowment(X0)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_1_46) ).
fof(f20,axiom,
! [X2,X0,X1] :
( ~ dissimilar(X0,X1,X2)
| organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_2_47) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ dissimilar(X0,X1,X2)
| ~ is_aligned(X0,X1)
| ~ is_aligned(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_2_49) ).
fof(f24,axiom,
! [X2,X0,X1] :
( dissimilar(X0,X1,X2)
| ~ is_aligned(X0,X1)
| is_aligned(X0,X2)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_2_51) ).
fof(f27,axiom,
! [X0,X1] :
( age(X0,X1) != zero
| ~ organization(X0)
| is_aligned(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_13_54) ).
fof(f28,axiom,
! [X2,X0,X1] :
( age(X0,X1) != zero
| ~ organization(X0)
| ~ greater(age(X0,X2),sigma)
| dissimilar(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_15_55) ).
fof(f29,axiom,
! [X2,X0,X1] :
( ~ organization(X0)
| age(X0,X1) != zero
| ~ dissimilar(X0,X1,X2)
| greater(age(X0,X2),sigma) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_15_56) ).
fof(f30,axiom,
! [X0,X1] :
( ~ smaller_or_equal(age(X0,X1),tau)
| ~ robust_position(X0)
| ~ positional_advantage(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_4_57) ).
fof(f31,axiom,
! [X0,X1] :
( ~ greater(age(X0,X1),tau)
| ~ robust_position(X0)
| positional_advantage(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_4_58) ).
fof(f37,axiom,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| has_immunity(X0,X1)
| ~ is_aligned(X0,X1)
| ~ organization(X0)
| hazard_of_mortality(X0,X1) = low ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_17_64) ).
fof(f38,axiom,
! [X0,X1] :
( ~ positional_advantage(X0,X1)
| has_immunity(X0,X1)
| is_aligned(X0,X1)
| ~ organization(X0)
| hazard_of_mortality(X0,X1) = mod1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_17_65) ).
fof(f39,axiom,
! [X0,X1] :
( ~ is_aligned(X0,X1)
| has_immunity(X0,X1)
| ~ organization(X0)
| positional_advantage(X0,X1)
| hazard_of_mortality(X0,X1) = mod2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_17_66) ).
fof(f42,axiom,
greater(mod1,low),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_18b_69) ).
fof(f46,axiom,
greater(mod2,mod1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_19_73) ).
fof(f47,negated_conjecture,
organization(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_74) ).
fof(f48,negated_conjecture,
robust_position(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_75) ).
fof(f49,negated_conjecture,
~ has_endowment(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_76) ).
fof(f50,negated_conjecture,
age(sk3,sk4) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_77) ).
fof(f51,plain,
zero = age(sk3,sk4),
inference(reorient_equations,[],[f50]) ).
fof(f53,negated_conjecture,
greater(tau,zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_79) ).
fof(f54,negated_conjecture,
greater(sigma,tau),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_80) ).
fof(f55,negated_conjecture,
smaller_or_equal(age(sk3,sk5),tau),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_81) ).
fof(f56,negated_conjecture,
greater(age(sk3,sk6),tau),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_82) ).
fof(f57,negated_conjecture,
smaller_or_equal(age(sk3,sk6),sigma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_83) ).
fof(f58,negated_conjecture,
greater(age(sk3,sk7),sigma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_84) ).
fof(f59,negated_conjecture,
( ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7))
| ~ smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))
| hazard_of_mortality(sk3,sk5) != hazard_of_mortality(sk3,sk4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_10_85) ).
fof(f61,plain,
! [X2,X0,X1] :
( age(X0,X1) != zero
| ~ dissimilar(X0,X1,X2)
| greater(age(X0,X2),sigma) ),
inference(forward_subsumption_resolution,[],[f29,f20]) ).
fof(f63,definition,
( spl0_1
<=> hazard_of_mortality(sk3,sk5) = hazard_of_mortality(sk3,sk4) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f65,plain,
( hazard_of_mortality(sk3,sk5) != hazard_of_mortality(sk3,sk4)
| spl0_1 ),
inference(avatar_component_clause,[],[f63]) ).
fof(f67,definition,
( spl0_2
<=> smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f69,plain,
( ~ smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))
| spl0_2 ),
inference(avatar_component_clause,[],[f67]) ).
fof(f71,definition,
( spl0_3
<=> smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f73,plain,
( ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7))
| spl0_3 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f74,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f59,f71,f67,f63]) ).
fof(f76,plain,
smaller(zero,tau),
inference(resolution,[],[f8,f53]) ).
fof(f81,plain,
smaller(low,mod1),
inference(resolution,[],[f8,f42]) ).
fof(f84,plain,
smaller(mod1,mod2),
inference(resolution,[],[f8,f46]) ).
fof(f89,plain,
~ greater(tau,sigma),
inference(resolution,[],[f9,f54]) ).
fof(f100,plain,
smaller_or_equal(zero,tau),
inference(resolution,[],[f76,f2]) ).
fof(f103,plain,
( smaller(age(sk3,sk5),tau)
| tau = age(sk3,sk5) ),
inference(resolution,[],[f1,f55]) ).
fof(f104,plain,
( smaller(age(sk3,sk6),sigma)
| sigma = age(sk3,sk6) ),
inference(resolution,[],[f1,f57]) ).
fof(f107,definition,
( spl0_4
<=> sigma = age(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f109,plain,
( sigma = age(sk3,sk6)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f111,definition,
( spl0_5
<=> smaller(age(sk3,sk6),sigma) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f113,plain,
( smaller(age(sk3,sk6),sigma)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,plain,
( spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f104,f111,f107]) ).
fof(f116,definition,
( spl0_6
<=> tau = age(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f118,plain,
( tau = age(sk3,sk5)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f120,definition,
( spl0_7
<=> smaller(age(sk3,sk5),tau) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f122,plain,
( smaller(age(sk3,sk5),tau)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f120]) ).
fof(f123,plain,
( spl0_6
| spl0_7 ),
inference(avatar_split_clause,[],[f103,f120,f116]) ).
fof(f127,plain,
! [X0] :
( ~ greater(X0,sigma)
| greater(X0,tau) ),
inference(resolution,[],[f10,f54]) ).
fof(f144,plain,
( zero != zero
| ~ organization(sk3)
| is_aligned(sk3,sk4) ),
inference(superposition,[],[f27,f51]) ).
fof(f145,plain,
( ~ organization(sk3)
| is_aligned(sk3,sk4) ),
inference(trivial_inequality_removal,[],[f144]) ).
fof(f146,plain,
is_aligned(sk3,sk4),
inference(forward_subsumption_resolution,[],[f145,f47]) ).
fof(f147,plain,
( ~ robust_position(sk3)
| ~ positional_advantage(sk3,sk5) ),
inference(resolution,[],[f30,f55]) ).
fof(f148,plain,
( ~ smaller_or_equal(zero,tau)
| ~ robust_position(sk3)
| ~ positional_advantage(sk3,sk4) ),
inference(superposition,[],[f30,f51]) ).
fof(f149,plain,
( ~ robust_position(sk3)
| ~ positional_advantage(sk3,sk4) ),
inference(forward_subsumption_resolution,[],[f148,f100]) ).
fof(f150,plain,
~ positional_advantage(sk3,sk5),
inference(forward_subsumption_resolution,[],[f147,f48]) ).
fof(f151,plain,
~ positional_advantage(sk3,sk4),
inference(forward_subsumption_resolution,[],[f149,f48]) ).
fof(f152,plain,
( ~ robust_position(sk3)
| positional_advantage(sk3,sk6) ),
inference(resolution,[],[f31,f56]) ).
fof(f155,plain,
positional_advantage(sk3,sk6),
inference(forward_subsumption_resolution,[],[f152,f48]) ).
fof(f186,plain,
! [X0] :
( zero != zero
| ~ dissimilar(sk3,sk4,X0)
| greater(age(sk3,X0),sigma) ),
inference(superposition,[],[f61,f51]) ).
fof(f187,plain,
! [X0] :
( greater(age(sk3,X0),sigma)
| ~ dissimilar(sk3,sk4,X0) ),
inference(trivial_inequality_removal,[],[f186]) ).
fof(f207,definition,
( spl0_10
<=> is_aligned(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f208,plain,
( ~ is_aligned(sk3,sk6)
| spl0_10 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f212,plain,
! [X0] :
( zero != zero
| ~ organization(sk3)
| ~ greater(age(sk3,X0),sigma)
| dissimilar(sk3,sk4,X0) ),
inference(superposition,[],[f28,f51]) ).
fof(f214,plain,
! [X0] :
( ~ organization(sk3)
| ~ greater(age(sk3,X0),sigma)
| dissimilar(sk3,sk4,X0) ),
inference(trivial_inequality_removal,[],[f212]) ).
fof(f215,plain,
! [X0] :
( ~ greater(age(sk3,X0),sigma)
| dissimilar(sk3,sk4,X0) ),
inference(forward_subsumption_resolution,[],[f214,f47]) ).
fof(f216,plain,
( has_immunity(sk3,sk6)
| ~ is_aligned(sk3,sk6)
| ~ organization(sk3)
| low = hazard_of_mortality(sk3,sk6) ),
inference(resolution,[],[f37,f155]) ).
fof(f217,plain,
( has_immunity(sk3,sk6)
| ~ is_aligned(sk3,sk6)
| low = hazard_of_mortality(sk3,sk6) ),
inference(forward_subsumption_resolution,[],[f216,f47]) ).
fof(f219,definition,
( spl0_11
<=> low = hazard_of_mortality(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f221,plain,
( low = hazard_of_mortality(sk3,sk6)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f223,definition,
( spl0_12
<=> has_immunity(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f225,plain,
( has_immunity(sk3,sk6)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f226,plain,
( spl0_11
| ~ spl0_10
| spl0_12 ),
inference(avatar_split_clause,[],[f217,f223,f207,f219]) ).
fof(f235,plain,
( has_immunity(sk3,sk4)
| ~ organization(sk3)
| positional_advantage(sk3,sk4)
| mod2 = hazard_of_mortality(sk3,sk4) ),
inference(resolution,[],[f39,f146]) ).
fof(f237,plain,
( has_immunity(sk3,sk4)
| positional_advantage(sk3,sk4)
| mod2 = hazard_of_mortality(sk3,sk4) ),
inference(forward_subsumption_resolution,[],[f235,f47]) ).
fof(f238,plain,
( has_immunity(sk3,sk4)
| mod2 = hazard_of_mortality(sk3,sk4) ),
inference(forward_subsumption_resolution,[],[f237,f151]) ).
fof(f240,definition,
( spl0_14
<=> mod2 = hazard_of_mortality(sk3,sk4) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f244,definition,
( spl0_15
<=> has_immunity(sk3,sk4) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f246,plain,
( has_immunity(sk3,sk4)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f247,plain,
( spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f238,f244,f240]) ).
fof(f260,definition,
( spl0_17
<=> is_aligned(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f261,plain,
( ~ is_aligned(sk3,sk5)
| spl0_17 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f262,plain,
( is_aligned(sk3,sk5)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f264,definition,
( spl0_18
<=> has_immunity(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f266,plain,
( has_immunity(sk3,sk5)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f300,plain,
greater(age(sk3,sk7),tau),
inference(resolution,[],[f127,f58]) ).
fof(f310,plain,
( greater(sigma,sigma)
| ~ dissimilar(sk3,sk4,sk6)
| ~ spl0_4 ),
inference(superposition,[],[f187,f109]) ).
fof(f311,plain,
( greater(tau,sigma)
| ~ dissimilar(sk3,sk4,sk5)
| ~ spl0_6 ),
inference(superposition,[],[f187,f118]) ).
fof(f312,plain,
( ~ dissimilar(sk3,sk4,sk5)
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f311,f89]) ).
fof(f314,definition,
( spl0_22
<=> dissimilar(sk3,sk4,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f315,plain,
( dissimilar(sk3,sk4,sk6)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f316,plain,
( ~ dissimilar(sk3,sk4,sk6)
| spl0_22 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f318,definition,
( spl0_23
<=> greater(sigma,sigma) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f320,plain,
( greater(sigma,sigma)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f321,plain,
( ~ spl0_22
| spl0_23
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f310,f107,f318,f314]) ).
fof(f324,plain,
( ~ is_aligned(sk3,sk4)
| is_aligned(sk3,sk5)
| ~ organization(sk3)
| ~ spl0_6 ),
inference(resolution,[],[f312,f24]) ).
fof(f325,plain,
( is_aligned(sk3,sk5)
| ~ organization(sk3)
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f324,f146]) ).
fof(f326,plain,
( is_aligned(sk3,sk5)
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f325,f47]) ).
fof(f327,plain,
( spl0_17
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f326,f116,f260]) ).
fof(f328,plain,
dissimilar(sk3,sk4,sk7),
inference(resolution,[],[f215,f58]) ).
fof(f336,plain,
( has_immunity(sk3,sk5)
| ~ organization(sk3)
| positional_advantage(sk3,sk5)
| mod2 = hazard_of_mortality(sk3,sk5)
| ~ spl0_17 ),
inference(resolution,[],[f262,f39]) ).
fof(f337,plain,
( has_immunity(sk3,sk5)
| positional_advantage(sk3,sk5)
| mod2 = hazard_of_mortality(sk3,sk5)
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f336,f47]) ).
fof(f338,plain,
( has_immunity(sk3,sk5)
| mod2 = hazard_of_mortality(sk3,sk5)
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f337,f150]) ).
fof(f346,definition,
( spl0_25
<=> mod2 = hazard_of_mortality(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f348,plain,
( mod2 = hazard_of_mortality(sk3,sk5)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f349,plain,
( spl0_25
| spl0_18
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f338,f260,f264,f346]) ).
fof(f353,plain,
( has_endowment(sk3)
| ~ organization(sk3)
| ~ spl0_18 ),
inference(resolution,[],[f266,f19]) ).
fof(f354,plain,
( ~ organization(sk3)
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f353,f49]) ).
fof(f356,plain,
( $false
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f354,f47]) ).
fof(f357,plain,
~ spl0_18,
inference(avatar_contradiction_clause,[],[f356]) ).
fof(f358,plain,
( greater(tau,age(sk3,sk5))
| ~ spl0_7 ),
inference(resolution,[],[f122,f7]) ).
fof(f366,plain,
( ~ is_aligned(sk3,sk4)
| is_aligned(sk3,sk6)
| ~ organization(sk3)
| spl0_22 ),
inference(resolution,[],[f316,f24]) ).
fof(f373,plain,
( ~ is_aligned(sk3,sk4)
| ~ is_aligned(sk3,sk7) ),
inference(resolution,[],[f328,f22]) ).
fof(f376,plain,
~ is_aligned(sk3,sk7),
inference(forward_subsumption_resolution,[],[f373,f146]) ).
fof(f390,plain,
( ~ robust_position(sk3)
| positional_advantage(sk3,sk7) ),
inference(resolution,[],[f300,f31]) ).
fof(f395,plain,
positional_advantage(sk3,sk7),
inference(forward_subsumption_resolution,[],[f390,f48]) ).
fof(f397,plain,
( has_immunity(sk3,sk7)
| is_aligned(sk3,sk7)
| ~ organization(sk3)
| mod1 = hazard_of_mortality(sk3,sk7) ),
inference(resolution,[],[f395,f38]) ).
fof(f399,plain,
( has_immunity(sk3,sk7)
| ~ organization(sk3)
| mod1 = hazard_of_mortality(sk3,sk7) ),
inference(forward_subsumption_resolution,[],[f397,f376]) ).
fof(f400,plain,
( has_immunity(sk3,sk7)
| mod1 = hazard_of_mortality(sk3,sk7) ),
inference(forward_subsumption_resolution,[],[f399,f47]) ).
fof(f402,definition,
( spl0_26
<=> mod1 = hazard_of_mortality(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f404,plain,
( mod1 = hazard_of_mortality(sk3,sk7)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f406,definition,
( spl0_27
<=> has_immunity(sk3,sk7) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f408,plain,
( has_immunity(sk3,sk7)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f409,plain,
( spl0_26
| spl0_27 ),
inference(avatar_split_clause,[],[f400,f406,f402]) ).
fof(f413,plain,
( ! [X0] :
( greater(X0,age(sk3,sk5))
| ~ greater(X0,tau) )
| ~ spl0_7 ),
inference(resolution,[],[f358,f10]) ).
fof(f468,plain,
( ! [X0] :
( ~ greater(age(sk3,sk5),X0)
| ~ greater(X0,tau) )
| ~ spl0_7 ),
inference(resolution,[],[f413,f9]) ).
fof(f476,plain,
( ~ greater(sigma,tau)
| ~ dissimilar(sk3,sk4,sk5)
| ~ spl0_7 ),
inference(resolution,[],[f468,f187]) ).
fof(f478,plain,
( ~ dissimilar(sk3,sk4,sk5)
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f476,f54]) ).
fof(f481,plain,
( ~ is_aligned(sk3,sk4)
| is_aligned(sk3,sk5)
| ~ organization(sk3)
| ~ spl0_7 ),
inference(resolution,[],[f478,f24]) ).
fof(f482,plain,
( is_aligned(sk3,sk5)
| ~ organization(sk3)
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f481,f146]) ).
fof(f483,plain,
( ~ organization(sk3)
| ~ spl0_7
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f482,f261]) ).
fof(f484,plain,
( $false
| ~ spl0_7
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f483,f47]) ).
fof(f485,plain,
( ~ spl0_7
| spl0_17 ),
inference(avatar_contradiction_clause,[],[f484]) ).
fof(f494,plain,
( mod2 != hazard_of_mortality(sk3,sk4)
| spl0_1
| ~ spl0_25 ),
inference(superposition,[],[f65,f348]) ).
fof(f498,plain,
( ~ smaller(hazard_of_mortality(sk3,sk6),mod1)
| spl0_3
| ~ spl0_26 ),
inference(forward_demodulation,[],[f73,f404]) ).
fof(f499,plain,
( ~ smaller(low,mod1)
| spl0_3
| ~ spl0_11
| ~ spl0_26 ),
inference(forward_demodulation,[],[f498,f221]) ).
fof(f500,plain,
( $false
| spl0_3
| ~ spl0_11
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f499,f81]) ).
fof(f501,plain,
( spl0_3
| ~ spl0_11
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f500]) ).
fof(f503,plain,
( is_aligned(sk3,sk6)
| ~ organization(sk3)
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f366,f146]) ).
fof(f504,plain,
( ~ organization(sk3)
| spl0_10
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f503,f208]) ).
fof(f505,plain,
( $false
| spl0_10
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f504,f47]) ).
fof(f506,plain,
( spl0_10
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f505]) ).
fof(f507,plain,
( ~ smaller(hazard_of_mortality(sk3,sk7),mod2)
| spl0_2
| ~ spl0_25 ),
inference(forward_demodulation,[],[f69,f348]) ).
fof(f509,plain,
( ~ smaller(mod1,mod2)
| spl0_2
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_demodulation,[],[f507,f404]) ).
fof(f511,plain,
( $false
| spl0_2
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f509,f84]) ).
fof(f512,plain,
( spl0_2
| ~ spl0_25
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f511]) ).
fof(f530,plain,
( has_endowment(sk3)
| ~ organization(sk3)
| ~ spl0_27 ),
inference(resolution,[],[f408,f19]) ).
fof(f531,plain,
( ~ organization(sk3)
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f530,f49]) ).
fof(f533,plain,
( $false
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f531,f47]) ).
fof(f534,plain,
~ spl0_27,
inference(avatar_contradiction_clause,[],[f533]) ).
fof(f542,plain,
( has_endowment(sk3)
| ~ organization(sk3)
| ~ spl0_12 ),
inference(resolution,[],[f225,f19]) ).
fof(f543,plain,
( ~ organization(sk3)
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f542,f49]) ).
fof(f545,plain,
( $false
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f543,f47]) ).
fof(f546,plain,
~ spl0_12,
inference(avatar_contradiction_clause,[],[f545]) ).
fof(f548,plain,
( greater(sigma,age(sk3,sk6))
| ~ spl0_5 ),
inference(resolution,[],[f113,f7]) ).
fof(f571,plain,
( ~ greater(age(sk3,sk6),sigma)
| ~ spl0_5 ),
inference(resolution,[],[f548,f9]) ).
fof(f609,plain,
( ~ dissimilar(sk3,sk4,sk6)
| ~ spl0_5 ),
inference(resolution,[],[f571,f187]) ).
fof(f611,plain,
( $false
| ~ spl0_5
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f609,f315]) ).
fof(f612,plain,
( ~ spl0_5
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f611]) ).
fof(f614,plain,
( ~ spl0_14
| spl0_1
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f494,f346,f63,f240]) ).
fof(f652,plain,
( has_endowment(sk3)
| ~ organization(sk3)
| ~ spl0_15 ),
inference(resolution,[],[f246,f19]) ).
fof(f653,plain,
( ~ organization(sk3)
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f652,f49]) ).
fof(f655,plain,
( $false
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f653,f47]) ).
fof(f656,plain,
~ spl0_15,
inference(avatar_contradiction_clause,[],[f655]) ).
fof(f668,plain,
( ~ greater(sigma,sigma)
| ~ spl0_23 ),
inference(resolution,[],[f320,f9]) ).
fof(f672,plain,
( $false
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f668,f320]) ).
fof(f673,plain,
~ spl0_23,
inference(avatar_contradiction_clause,[],[f672]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f74]) ).
cnf(s2,plain,
( spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f114]) ).
cnf(s3,plain,
( spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f123]) ).
cnf(s6,plain,
( ~ spl0_10
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f226]) ).
cnf(s8,plain,
( spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f247]) ).
cnf(s13,plain,
( ~ spl0_4
| ~ spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f321]) ).
cnf(s14,plain,
( ~ spl0_6
| spl0_17 ),
inference(sat_conversion,[],[f327]) ).
cnf(s17,plain,
( ~ spl0_17
| spl0_18
| spl0_25 ),
inference(sat_conversion,[],[f349]) ).
cnf(s18,plain,
~ spl0_18,
inference(sat_conversion,[],[f357]) ).
cnf(s20,plain,
( spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f409]) ).
cnf(s21,plain,
( ~ spl0_7
| spl0_17 ),
inference(sat_conversion,[],[f485]) ).
cnf(s23,plain,
( spl0_3
| ~ spl0_11
| ~ spl0_26 ),
inference(sat_conversion,[],[f501]) ).
cnf(s24,plain,
( spl0_10
| spl0_22 ),
inference(sat_conversion,[],[f506]) ).
cnf(s25,plain,
( spl0_2
| ~ spl0_25
| ~ spl0_26 ),
inference(sat_conversion,[],[f512]) ).
cnf(s28,plain,
~ spl0_27,
inference(sat_conversion,[],[f534]) ).
cnf(s29,plain,
~ spl0_12,
inference(sat_conversion,[],[f546]) ).
cnf(s33,plain,
( ~ spl0_5
| ~ spl0_22 ),
inference(sat_conversion,[],[f612]) ).
cnf(s34,plain,
( spl0_1
| ~ spl0_14
| ~ spl0_25 ),
inference(sat_conversion,[],[f614]) ).
cnf(s36,plain,
~ spl0_15,
inference(sat_conversion,[],[f656]) ).
cnf(s38,plain,
~ spl0_23,
inference(sat_conversion,[],[f673]) ).
cnf(s39,plain,
spl0_26,
inference(rat,[],[s20,s28]) ).
cnf(s41,plain,
( ~ spl0_17
| spl0_25 ),
inference(rat,[],[s17,s18]) ).
cnf(s43,plain,
( ~ spl0_4
| ~ spl0_22 ),
inference(rat,[],[s13,s38]) ).
cnf(s45,plain,
spl0_14,
inference(rat,[],[s8,s36]) ).
cnf(s47,plain,
( ~ spl0_10
| spl0_11 ),
inference(rat,[],[s6,s29]) ).
cnf(s48,plain,
spl0_17,
inference(rat,[],[s3,s14,s21]) ).
cnf(s49,plain,
spl0_25,
inference(rat,[],[s41,s48]) ).
cnf(s50,plain,
spl0_2,
inference(rat,[],[s25,s39,s49]) ).
cnf(s51,plain,
spl0_1,
inference(rat,[],[s34,s45,s49]) ).
cnf(s52,plain,
~ spl0_3,
inference(rat,[],[s1,s51,s50]) ).
cnf(s53,plain,
~ spl0_11,
inference(rat,[],[s23,s39,s52]) ).
cnf(s54,plain,
~ spl0_10,
inference(rat,[],[s47,s53]) ).
cnf(s55,plain,
spl0_22,
inference(rat,[],[s24,s54]) ).
cnf(s57,plain,
~ spl0_5,
inference(rat,[],[s33,s55]) ).
cnf(s58,plain,
~ spl0_4,
inference(rat,[],[s43,s55]) ).
cnf(s59,plain,
$false,
inference(rat,[],[s2,s57,s58]) ).
fof(f674,plain,
$false,
inference(avatar_sat_refutation,[],[s59]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT064-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n013.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 17:31:06 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.83/1.31 % (440904)Input is clausal, will run a generic CNF schedule.
% 2.83/1.31 % (440915)dis-21_1_sil=8000:lcm=predicate:random_seed=3611700914:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 2.83/1.31 % (440915)Instruction limit reached!
% 2.83/1.31 % (440915)------------------------------
% 2.83/1.31 % (440915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.31 % (440915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.31 % (440915)CaDiCaL version: 2.1.3
% 2.83/1.31 % (440915)Termination reason: Instruction limit
% 2.83/1.31 % (440915)Termination phase: Saturation
% 2.83/1.31 % (440915)Time elapsed: 0.025 s
% 2.83/1.31 % (440915)Peak memory usage: 88 MB
% 2.83/1.31 % (440915)Instructions burned: 122 (million)
% 2.83/1.31 % (440912)lrs+10_1_sil=8000:sp=occurrence:random_seed=3275172677:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.83/1.31 % (440910)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2150754842:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.83/1.31 % (440909)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2142500164:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.83/1.31 % (440911)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3597010613:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.83/1.31 % (440914)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1136330539:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.83/1.31 % (440913)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1049815752:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.83/1.31 % (440912)First to succeed.
% 2.83/1.31 % (440912)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-440904"
% 2.83/1.31 % (440914)Also succeeded, but the first one will report.
% 2.83/1.31 % (440913)Instruction limit reached!
% 2.83/1.31 % (440913)------------------------------
% 2.83/1.31 % (440913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.31 % (440913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.31 % (440913)CaDiCaL version: 2.1.3
% 2.83/1.31 % (440913)Termination reason: Instruction limit
% 2.83/1.31 % (440913)Termination phase: Saturation
% 2.83/1.31 % (440913)Time elapsed: 0.075 s
% 2.83/1.31 % (440913)Peak memory usage: 89 MB
% 2.83/1.31 % (440913)Instructions burned: 114 (million)
% 2.83/1.31 % (440917)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=222913053:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.83/1.31 % (440924)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1834854973:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 2.83/1.31 % (440917)Instruction limit reached!
% 2.83/1.31 % (440917)------------------------------
% 2.83/1.31 % (440917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.83/1.31 % (440917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/1.31 % (440917)CaDiCaL version: 2.1.3
% 2.83/1.31 % (440917)Termination reason: Instruction limit
% 2.83/1.31 % (440917)Termination phase: Saturation
% 2.83/1.31 % (440917)Time elapsed: 0.099 s
% 2.83/1.31 % (440917)Peak memory usage: 89 MB
% 2.83/1.31 % (440917)Instructions burned: 143 (million)
% 2.83/1.31 % (440912)Refutation found. Thanks to Tanya!
% 2.83/1.31 % SZS status Unsatisfiable for theBenchmark
% 2.83/1.31 % SZS output start Proof for theBenchmark
% See solution above
% 3.82/1.53 % (440912)------------------------------
% 3.82/1.53 % (440912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.82/1.53 % (440912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.82/1.53 % (440912)CaDiCaL version: 2.1.3
% 3.82/1.53 % (440912)Termination reason: Refutation
% 3.82/1.53 % (440912)Time elapsed: 0.018 s
% 3.82/1.53 % (440912)Peak memory usage: 89 MB
% 3.82/1.53 % (440912)Instructions burned: 22 (million)
% 3.82/1.53 % (440912)------------------------------
% 3.82/1.53 % (440912)------------------------------
% 3.82/1.53 % (440904)Success in time 0.447 s
% 3.82/1.53 % Vampire exiting
%------------------------------------------------------------------------------