%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : MGT051-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 : n003.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:14 PM UTC 2026
% Result : Unsatisfiable 3.11s 1.39s
% Output : Refutation 4.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 46
% Syntax : Number of formulae : 214 ( 40 unt; 19 def)
% Number of atoms : 528 ( 46 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 570 ( 256 ~; 295 |; 0 &)
% ( 19 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 20 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 99 ( 0 sgn 99 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( smaller(X0,X1)
| ~ smaller_or_equal(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(f3,axiom,
! [X0,X1] :
( X0 != X1
| smaller_or_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_smaller_or_equal_3) ).
fof(f6,axiom,
! [X0,X1] :
( X0 != X1
| greater_or_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_greater_or_equal_6) ).
fof(f7,axiom,
! [X0,X1] :
( greater(X1,X0)
| ~ smaller(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_smaller_7) ).
fof(f8,axiom,
! [X0,X1] :
( smaller(X1,X0)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_smaller_8) ).
fof(f9,axiom,
! [X0,X1] :
( ~ greater(X0,X1)
| ~ greater(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meaning_postulate_greater_strict_9) ).
fof(f10,axiom,
! [X2,X0,X1] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meaning_postulate_greater_transitive_10) ).
fof(f11,axiom,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| smaller(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meaning_postulate_greater_comparable_11) ).
fof(f12,axiom,
! [X0] :
( organization(X0)
| ~ has_endowment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_1_41) ).
fof(f13,axiom,
! [X0,X1] :
( has_immunity(X0,X1)
| ~ smaller_or_equal(age(X0,X1),eta)
| ~ has_endowment(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_1_42) ).
fof(f14,axiom,
! [X0,X1] :
( ~ has_endowment(X0)
| ~ greater(age(X0,X1),eta)
| ~ has_immunity(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_1_43) ).
fof(f19,axiom,
! [X2,X0,X1] :
( ~ has_immunity(X0,X1)
| ~ organization(X0)
| ~ has_immunity(X0,X2)
| hazard_of_mortality(X0,X1) = hazard_of_mortality(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_2_48) ).
fof(f20,axiom,
! [X2,X0,X1] :
( greater(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1))
| ~ has_immunity(X0,X1)
| has_immunity(X0,X2)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_3_49) ).
fof(f21,axiom,
! [X2,X0,X1] :
( smaller(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1))
| has_immunity(X0,X1)
| has_immunity(X0,X2)
| ~ greater(capability(X0,X2),capability(X0,X1))
| ~ greater_or_equal(position(X0,X2),position(X0,X1))
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_4_50) ).
fof(f26,axiom,
! [X2,X0,X1] :
( smaller(capability(X0,X1),capability(X0,X2))
| ~ smaller_or_equal(stock_of_knowledge(X0,X1),stock_of_knowledge(X0,X2))
| ~ greater(internal_friction(X0,X1),internal_friction(X0,X2))
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_5_54) ).
fof(f30,axiom,
! [X2,X0,X1] :
( ~ organization(X0)
| external_ties(X0,X1) != external_ties(X0,X2)
| position(X0,X1) = position(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_6_57) ).
fof(f31,plain,
! [X2,X0,X1] :
( ~ organization(X0)
| external_ties(X0,X1) != external_ties(X0,X2)
| position(X0,X2) = position(X0,X1) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,axiom,
! [X2,X0,X1] :
( stock_of_knowledge(X0,X1) = stock_of_knowledge(X0,X2)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_10_58) ).
fof(f33,axiom,
! [X2,X0,X1] :
( external_ties(X0,X1) = external_ties(X0,X2)
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_11_59) ).
fof(f34,axiom,
! [X2,X0,X1] :
( greater(internal_friction(X0,X1),internal_friction(X0,X2))
| ~ greater(age(X0,X1),age(X0,X2))
| ~ organization(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_12_60) ).
fof(f35,negated_conjecture,
organization(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_61) ).
fof(f36,negated_conjecture,
has_endowment(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_62) ).
fof(f37,negated_conjecture,
smaller_or_equal(age(sk2,sk3),age(sk2,sk4)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_63) ).
fof(f38,negated_conjecture,
smaller_or_equal(age(sk2,sk4),eta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_64) ).
fof(f39,negated_conjecture,
greater(age(sk2,sk5),eta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_65) ).
fof(f40,negated_conjecture,
greater(age(sk2,sk6),age(sk2,sk5)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_66) ).
fof(f41,negated_conjecture,
( ~ greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5))
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_4_67) ).
fof(f42,plain,
! [X1] : smaller_or_equal(X1,X1),
inference(equality_resolution,[],[f3]) ).
fof(f43,plain,
! [X1] : greater_or_equal(X1,X1),
inference(equality_resolution,[],[f6]) ).
fof(f45,definition,
( spl0_1
<=> hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f47,plain,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| spl0_1 ),
inference(avatar_component_clause,[],[f45]) ).
fof(f49,definition,
( spl0_2
<=> greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f51,plain,
( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
| spl0_2 ),
inference(avatar_component_clause,[],[f49]) ).
fof(f53,definition,
( spl0_3
<=> greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f55,plain,
( ~ greater(hazard_of_mortality(sk2,sk6),hazard_of_mortality(sk2,sk5))
| spl0_3 ),
inference(avatar_component_clause,[],[f53]) ).
fof(f56,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f41,f53,f49,f45]) ).
fof(f57,plain,
! [X0,X1] :
( smaller_or_equal(X1,X0)
| ~ greater(X0,X1) ),
inference(resolution,[],[f8,f2]) ).
fof(f58,plain,
~ greater(eta,age(sk2,sk5)),
inference(resolution,[],[f9,f39]) ).
fof(f60,plain,
! [X0,X1] :
( ~ smaller(X0,X1)
| ~ greater(X0,X1) ),
inference(resolution,[],[f9,f7]) ).
fof(f61,plain,
! [X0] : ~ greater(X0,X0),
inference(factoring,[],[f9]) ).
fof(f83,plain,
! [X0] :
( ~ greater(eta,X0)
| ~ greater(X0,age(sk2,sk5)) ),
inference(resolution,[],[f10,f58]) ).
fof(f116,plain,
! [X0] :
( ~ has_immunity(sk2,X0)
| ~ greater(age(sk2,X0),eta) ),
inference(resolution,[],[f14,f36]) ).
fof(f143,plain,
! [X2,X0,X1] :
( ~ organization(X0)
| ~ has_immunity(X0,X1)
| hazard_of_mortality(X0,X1) = hazard_of_mortality(X0,X2)
| ~ smaller_or_equal(age(X0,X2),eta)
| ~ has_endowment(X0) ),
inference(resolution,[],[f19,f13]) ).
fof(f145,plain,
! [X2,X0,X1] :
( ~ has_endowment(X0)
| hazard_of_mortality(X0,X1) = hazard_of_mortality(X0,X2)
| ~ smaller_or_equal(age(X0,X2),eta)
| ~ has_immunity(X0,X1) ),
inference(forward_subsumption_resolution,[],[f143,f12]) ).
fof(f159,plain,
! [X2,X0,X1] :
( ~ organization(X0)
| position(X0,X2) = position(X0,X1) ),
inference(forward_subsumption_resolution,[],[f31,f33]) ).
fof(f160,plain,
! [X0,X1] : position(sk2,X0) = position(sk2,X1),
inference(resolution,[],[f159,f35]) ).
fof(f181,plain,
! [X0] :
( ~ greater(age(sk2,X0),eta)
| ~ smaller_or_equal(age(sk2,X0),eta)
| ~ has_endowment(sk2) ),
inference(resolution,[],[f116,f13]) ).
fof(f182,plain,
! [X0] :
( ~ smaller_or_equal(age(sk2,X0),eta)
| ~ greater(age(sk2,X0),eta) ),
inference(forward_subsumption_resolution,[],[f181,f36]) ).
fof(f184,plain,
! [X0] :
( ~ greater(X0,age(sk2,sk5))
| eta = X0
| smaller(eta,X0) ),
inference(resolution,[],[f83,f11]) ).
fof(f198,plain,
~ greater(age(sk2,sk4),eta),
inference(resolution,[],[f182,f38]) ).
fof(f211,plain,
! [X0] :
( ~ greater(X0,eta)
| ~ greater(age(sk2,sk4),X0) ),
inference(resolution,[],[f198,f10]) ).
fof(f238,plain,
! [X0,X1] :
( ~ smaller_or_equal(X0,X1)
| ~ greater(X0,X1)
| X0 = X1 ),
inference(resolution,[],[f60,f1]) ).
fof(f277,definition,
( spl0_16
<=> eta = age(sk2,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f278,plain,
( eta != age(sk2,sk3)
| spl0_16 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f279,plain,
( eta = age(sk2,sk3)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f302,plain,
! [X0,X1] :
( ~ has_immunity(sk2,X0)
| ~ smaller_or_equal(age(sk2,X1),eta)
| hazard_of_mortality(sk2,X0) = hazard_of_mortality(sk2,X1) ),
inference(resolution,[],[f145,f36]) ).
fof(f403,plain,
! [X0,X1] :
( ~ smaller_or_equal(age(sk2,X0),eta)
| hazard_of_mortality(sk2,X0) = hazard_of_mortality(sk2,X1)
| ~ smaller_or_equal(age(sk2,X1),eta)
| ~ has_endowment(sk2) ),
inference(resolution,[],[f302,f13]) ).
fof(f404,plain,
! [X0,X1] :
( ~ smaller_or_equal(age(sk2,X0),eta)
| hazard_of_mortality(sk2,X0) = hazard_of_mortality(sk2,X1)
| ~ smaller_or_equal(age(sk2,X1),eta) ),
inference(forward_subsumption_resolution,[],[f403,f36]) ).
fof(f430,plain,
( ~ greater(age(sk2,sk3),age(sk2,sk4))
| age(sk2,sk3) = age(sk2,sk4) ),
inference(resolution,[],[f238,f37]) ).
fof(f500,plain,
( eta = age(sk2,sk6)
| smaller(eta,age(sk2,sk6)) ),
inference(resolution,[],[f184,f40]) ).
fof(f502,definition,
( spl0_25
<=> smaller(eta,age(sk2,sk6)) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f504,plain,
( smaller(eta,age(sk2,sk6))
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f502]) ).
fof(f506,definition,
( spl0_26
<=> eta = age(sk2,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f507,plain,
( eta != age(sk2,sk6)
| spl0_26 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f508,plain,
( eta = age(sk2,sk6)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f509,plain,
( spl0_25
| spl0_26 ),
inference(avatar_split_clause,[],[f500,f506,f502]) ).
fof(f512,plain,
( ~ greater(eta,age(sk2,sk6))
| ~ spl0_25 ),
inference(resolution,[],[f504,f60]) ).
fof(f518,plain,
( ~ smaller(age(sk2,sk6),eta)
| ~ spl0_25 ),
inference(resolution,[],[f512,f7]) ).
fof(f542,plain,
( greater(eta,age(sk2,sk5))
| ~ spl0_26 ),
inference(superposition,[],[f40,f508]) ).
fof(f570,plain,
( $false
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f542,f58]) ).
fof(f571,plain,
~ spl0_26,
inference(avatar_contradiction_clause,[],[f570]) ).
fof(f724,plain,
! [X0] :
( ~ smaller_or_equal(age(sk2,X0),eta)
| hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,X0) ),
inference(resolution,[],[f404,f38]) ).
fof(f739,plain,
( ~ smaller_or_equal(eta,eta)
| hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3)
| ~ spl0_16 ),
inference(superposition,[],[f724,f279]) ).
fof(f740,plain,
( hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3)
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f739,f42]) ).
fof(f743,plain,
( $false
| spl0_1
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f740,f47]) ).
fof(f744,plain,
( spl0_1
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f743]) ).
fof(f746,definition,
( spl0_30
<=> age(sk2,sk3) = age(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f748,plain,
( age(sk2,sk3) = age(sk2,sk4)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f750,definition,
( spl0_31
<=> greater(age(sk2,sk3),age(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f752,plain,
( ~ greater(age(sk2,sk3),age(sk2,sk4))
| spl0_31 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f753,plain,
( spl0_30
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f430,f750,f746]) ).
fof(f755,definition,
( spl0_32
<=> ! [X0] :
( ~ greater(X0,eta)
| ~ greater(age(sk2,sk4),X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f756,plain,
( ! [X0] :
( ~ greater(age(sk2,sk4),X0)
| ~ greater(X0,eta) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f781,definition,
( spl0_33
<=> smaller_or_equal(age(sk2,sk3),eta) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f782,plain,
( smaller_or_equal(age(sk2,sk3),eta)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f783,plain,
( ~ smaller_or_equal(age(sk2,sk3),eta)
| spl0_33 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f837,plain,
( ~ has_immunity(sk2,sk4)
| has_immunity(sk2,sk5)
| ~ organization(sk2)
| spl0_2 ),
inference(resolution,[],[f51,f20]) ).
fof(f856,plain,
( ~ has_immunity(sk2,sk4)
| has_immunity(sk2,sk5)
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f837,f35]) ).
fof(f858,definition,
( spl0_50
<=> has_immunity(sk2,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f859,plain,
( ~ has_immunity(sk2,sk5)
| spl0_50 ),
inference(avatar_component_clause,[],[f858]) ).
fof(f860,plain,
( has_immunity(sk2,sk5)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f858]) ).
fof(f862,definition,
( spl0_51
<=> has_immunity(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f864,plain,
( ~ has_immunity(sk2,sk4)
| spl0_51 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f865,plain,
( spl0_50
| ~ spl0_51
| spl0_2 ),
inference(avatar_split_clause,[],[f856,f49,f862,f858]) ).
fof(f948,definition,
( spl0_54
<=> greater_or_equal(position(sk2,sk5),position(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f949,plain,
( greater_or_equal(position(sk2,sk5),position(sk2,sk4))
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f950,plain,
( ~ greater_or_equal(position(sk2,sk5),position(sk2,sk4))
| spl0_54 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f983,plain,
( ~ greater(eta,age(sk2,sk3))
| spl0_33 ),
inference(resolution,[],[f783,f57]) ).
fof(f993,plain,
( eta = age(sk2,sk3)
| smaller(eta,age(sk2,sk3))
| spl0_33 ),
inference(resolution,[],[f983,f11]) ).
fof(f998,plain,
( smaller(eta,age(sk2,sk3))
| spl0_16
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f993,f278]) ).
fof(f1000,plain,
( ! [X0] : ~ greater_or_equal(position(sk2,X0),position(sk2,sk4))
| spl0_54 ),
inference(superposition,[],[f950,f160]) ).
fof(f1044,definition,
( spl0_61
<=> greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f1045,plain,
( greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4))
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f1044]) ).
fof(f1046,plain,
( ~ greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4))
| spl0_61 ),
inference(avatar_component_clause,[],[f1044]) ).
fof(f1076,plain,
( ~ smaller_or_equal(age(sk2,sk4),eta)
| ~ has_endowment(sk2)
| spl0_51 ),
inference(resolution,[],[f864,f13]) ).
fof(f1077,plain,
( ~ has_endowment(sk2)
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f1076,f38]) ).
fof(f1078,plain,
( $false
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f1077,f36]) ).
fof(f1079,plain,
spl0_51,
inference(avatar_contradiction_clause,[],[f1078]) ).
fof(f1093,plain,
( age(sk2,sk3) = age(sk2,sk4)
| smaller(age(sk2,sk3),age(sk2,sk4))
| spl0_31 ),
inference(resolution,[],[f752,f11]) ).
fof(f1103,definition,
( spl0_64
<=> smaller(age(sk2,sk3),age(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f1105,plain,
( smaller(age(sk2,sk3),age(sk2,sk4))
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f1103]) ).
fof(f1106,plain,
( spl0_64
| spl0_30
| spl0_31 ),
inference(avatar_split_clause,[],[f1093,f750,f746,f1103]) ).
fof(f1108,plain,
( $false
| spl0_54 ),
inference(resolution,[],[f1000,f43]) ).
fof(f1114,plain,
spl0_54,
inference(avatar_contradiction_clause,[],[f1108]) ).
fof(f1119,plain,
( ! [X0] : greater_or_equal(position(sk2,sk5),position(sk2,X0))
| ~ spl0_54 ),
inference(superposition,[],[f949,f160]) ).
fof(f1204,plain,
( ~ smaller(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,sk5))
| spl0_61 ),
inference(resolution,[],[f1046,f7]) ).
fof(f1214,definition,
( spl0_69
<=> stock_of_knowledge(sk2,sk5) = stock_of_knowledge(sk2,sk4) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f1216,plain,
( stock_of_knowledge(sk2,sk5) = stock_of_knowledge(sk2,sk4)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f1214]) ).
fof(f1223,definition,
( spl0_71
<=> smaller(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f1224,plain,
( ~ smaller(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4))
| spl0_71 ),
inference(avatar_component_clause,[],[f1223]) ).
fof(f1225,plain,
( smaller(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4))
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f1223]) ).
fof(f1359,plain,
( ! [X0] :
( ~ smaller(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,X0))
| ~ organization(sk2) )
| spl0_61 ),
inference(superposition,[],[f1204,f32]) ).
fof(f1360,plain,
( ! [X0] : ~ smaller(stock_of_knowledge(sk2,sk4),stock_of_knowledge(sk2,X0))
| spl0_61 ),
inference(forward_subsumption_resolution,[],[f1359,f35]) ).
fof(f1596,plain,
( ! [X0,X1] :
( ~ smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))
| ~ organization(sk2) )
| spl0_61 ),
inference(superposition,[],[f1360,f32]) ).
fof(f1600,plain,
( ! [X0,X1] : ~ smaller(stock_of_knowledge(sk2,X0),stock_of_knowledge(sk2,X1))
| spl0_61 ),
inference(forward_subsumption_resolution,[],[f1596,f35]) ).
fof(f1633,plain,
spl0_32,
inference(avatar_split_clause,[],[f211,f755]) ).
fof(f2136,plain,
( ! [X0] :
( ~ smaller(X0,age(sk2,sk4))
| ~ greater(X0,eta) )
| ~ spl0_32 ),
inference(resolution,[],[f756,f7]) ).
fof(f2152,plain,
( ~ greater(age(sk2,sk3),eta)
| ~ spl0_32
| ~ spl0_64 ),
inference(resolution,[],[f2136,f1105]) ).
fof(f2158,plain,
( ~ smaller(eta,age(sk2,sk3))
| ~ spl0_32
| ~ spl0_64 ),
inference(resolution,[],[f2152,f7]) ).
fof(f2159,plain,
( $false
| spl0_16
| ~ spl0_32
| spl0_33
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f2158,f998]) ).
fof(f2160,plain,
( spl0_16
| ~ spl0_32
| spl0_33
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f2159]) ).
fof(f2274,plain,
( ~ smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk6))
| spl0_3 ),
inference(resolution,[],[f55,f7]) ).
fof(f2363,definition,
( spl0_115
<=> has_immunity(sk2,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f2364,plain,
( ~ has_immunity(sk2,sk6)
| spl0_115 ),
inference(avatar_component_clause,[],[f2363]) ).
fof(f2365,plain,
( has_immunity(sk2,sk6)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f2363]) ).
fof(f2431,plain,
( hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3)
| ~ spl0_33 ),
inference(resolution,[],[f782,f724]) ).
fof(f2560,definition,
( spl0_131
<=> smaller_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f2561,plain,
( smaller_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4))
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f2560]) ).
fof(f2562,plain,
( ~ smaller_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4))
| spl0_131 ),
inference(avatar_component_clause,[],[f2560]) ).
fof(f2603,plain,
( ~ greater(age(sk2,sk6),eta)
| ~ spl0_115 ),
inference(resolution,[],[f2365,f116]) ).
fof(f2610,plain,
( eta = age(sk2,sk6)
| smaller(age(sk2,sk6),eta)
| ~ spl0_115 ),
inference(resolution,[],[f2603,f11]) ).
fof(f2617,plain,
( smaller(age(sk2,sk6),eta)
| spl0_26
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f2610,f507]) ).
fof(f2618,plain,
( $false
| ~ spl0_25
| spl0_26
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f2617,f518]) ).
fof(f2619,plain,
( ~ spl0_25
| spl0_26
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f2618]) ).
fof(f2695,plain,
( spl0_1
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f2431,f781,f45]) ).
fof(f2703,plain,
( ~ greater(age(sk2,sk5),eta)
| ~ spl0_50 ),
inference(resolution,[],[f860,f116]) ).
fof(f2710,plain,
( $false
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f2703,f39]) ).
fof(f2711,plain,
~ spl0_50,
inference(avatar_contradiction_clause,[],[f2710]) ).
fof(f2908,plain,
( ~ smaller_or_equal(age(sk2,sk4),eta)
| hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3)
| ~ spl0_30 ),
inference(superposition,[],[f724,f748]) ).
fof(f2919,plain,
( hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3)
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f2908,f38]) ).
fof(f2933,plain,
( $false
| spl0_1
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f2919,f47]) ).
fof(f2934,plain,
( spl0_1
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f2933]) ).
fof(f3017,plain,
( has_immunity(sk2,sk6)
| has_immunity(sk2,sk5)
| ~ greater(capability(sk2,sk5),capability(sk2,sk6))
| ~ greater_or_equal(position(sk2,sk5),position(sk2,sk6))
| ~ organization(sk2)
| spl0_3 ),
inference(resolution,[],[f2274,f21]) ).
fof(f3023,plain,
( has_immunity(sk2,sk5)
| ~ greater(capability(sk2,sk5),capability(sk2,sk6))
| ~ greater_or_equal(position(sk2,sk5),position(sk2,sk6))
| ~ organization(sk2)
| spl0_3
| spl0_115 ),
inference(forward_subsumption_resolution,[],[f3017,f2364]) ).
fof(f3026,plain,
( ~ greater(capability(sk2,sk5),capability(sk2,sk6))
| ~ greater_or_equal(position(sk2,sk5),position(sk2,sk6))
| ~ organization(sk2)
| spl0_3
| spl0_50
| spl0_115 ),
inference(forward_subsumption_resolution,[],[f3023,f859]) ).
fof(f3027,plain,
( ~ greater(capability(sk2,sk5),capability(sk2,sk6))
| ~ organization(sk2)
| spl0_3
| spl0_50
| ~ spl0_54
| spl0_115 ),
inference(forward_subsumption_resolution,[],[f3026,f1119]) ).
fof(f3028,plain,
( ~ greater(capability(sk2,sk5),capability(sk2,sk6))
| spl0_3
| spl0_50
| ~ spl0_54
| spl0_115 ),
inference(forward_subsumption_resolution,[],[f3027,f35]) ).
fof(f3112,plain,
( ~ smaller(capability(sk2,sk6),capability(sk2,sk5))
| spl0_3
| spl0_50
| ~ spl0_54
| spl0_115 ),
inference(resolution,[],[f3028,f7]) ).
fof(f3217,plain,
( ! [X0] :
( ~ smaller_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,X0))
| ~ organization(sk2) )
| spl0_131 ),
inference(superposition,[],[f2562,f32]) ).
fof(f3218,plain,
( ! [X0] : ~ smaller_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,X0))
| spl0_131 ),
inference(forward_subsumption_resolution,[],[f3217,f35]) ).
fof(f3374,plain,
( $false
| spl0_131 ),
inference(resolution,[],[f3218,f42]) ).
fof(f3382,plain,
spl0_131,
inference(avatar_contradiction_clause,[],[f3374]) ).
fof(f3418,plain,
( $false
| spl0_61
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f1225,f1600]) ).
fof(f3419,plain,
( spl0_61
| ~ spl0_71 ),
inference(avatar_contradiction_clause,[],[f3418]) ).
fof(f3456,plain,
( ! [X0] :
( greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,X0))
| ~ organization(sk2) )
| ~ spl0_61 ),
inference(superposition,[],[f1045,f32]) ).
fof(f3457,plain,
( ! [X0] : greater(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,X0))
| ~ spl0_61 ),
inference(forward_subsumption_resolution,[],[f3456,f35]) ).
fof(f3601,plain,
( $false
| ~ spl0_61 ),
inference(resolution,[],[f3457,f61]) ).
fof(f3612,plain,
~ spl0_61,
inference(avatar_contradiction_clause,[],[f3601]) ).
fof(f3631,plain,
( stock_of_knowledge(sk2,sk5) = stock_of_knowledge(sk2,sk4)
| smaller(stock_of_knowledge(sk2,sk5),stock_of_knowledge(sk2,sk4))
| spl0_61 ),
inference(resolution,[],[f1046,f11]) ).
fof(f3644,plain,
( stock_of_knowledge(sk2,sk5) = stock_of_knowledge(sk2,sk4)
| spl0_61
| spl0_71 ),
inference(forward_subsumption_resolution,[],[f3631,f1224]) ).
fof(f3646,plain,
( spl0_69
| spl0_61
| spl0_71 ),
inference(avatar_split_clause,[],[f3644,f1223,f1044,f1214]) ).
fof(f4149,plain,
( ~ smaller_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5))
| ~ greater(internal_friction(sk2,sk6),internal_friction(sk2,sk5))
| ~ organization(sk2)
| spl0_3
| spl0_50
| ~ spl0_54
| spl0_115 ),
inference(resolution,[],[f3112,f26]) ).
fof(f4162,plain,
( ~ smaller_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk5))
| ~ greater(internal_friction(sk2,sk6),internal_friction(sk2,sk5))
| spl0_3
| spl0_50
| ~ spl0_54
| spl0_115 ),
inference(forward_subsumption_resolution,[],[f4149,f35]) ).
fof(f4163,plain,
( ~ smaller_or_equal(stock_of_knowledge(sk2,sk6),stock_of_knowledge(sk2,sk4))
| ~ greater(internal_friction(sk2,sk6),internal_friction(sk2,sk5))
| spl0_3
| spl0_50
| ~ spl0_54
| ~ spl0_69
| spl0_115 ),
inference(forward_demodulation,[],[f4162,f1216]) ).
fof(f4164,plain,
( ~ greater(internal_friction(sk2,sk6),internal_friction(sk2,sk5))
| spl0_3
| spl0_50
| ~ spl0_54
| ~ spl0_69
| spl0_115
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f4163,f2561]) ).
fof(f4392,plain,
( ~ greater(age(sk2,sk6),age(sk2,sk5))
| ~ organization(sk2)
| spl0_3
| spl0_50
| ~ spl0_54
| ~ spl0_69
| spl0_115
| ~ spl0_131 ),
inference(resolution,[],[f4164,f34]) ).
fof(f4402,plain,
( ~ organization(sk2)
| spl0_3
| spl0_50
| ~ spl0_54
| ~ spl0_69
| spl0_115
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f4392,f40]) ).
fof(f4403,plain,
( $false
| spl0_3
| spl0_50
| ~ spl0_54
| ~ spl0_69
| spl0_115
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f4402,f35]) ).
fof(f4404,plain,
( spl0_3
| spl0_50
| ~ spl0_54
| ~ spl0_69
| spl0_115
| ~ spl0_131 ),
inference(avatar_contradiction_clause,[],[f4403]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f56]) ).
cnf(s28,plain,
( spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f509]) ).
cnf(s38,plain,
~ spl0_26,
inference(sat_conversion,[],[f571]) ).
cnf(s42,plain,
( spl0_1
| ~ spl0_16 ),
inference(sat_conversion,[],[f744]) ).
cnf(s43,plain,
( spl0_30
| ~ spl0_31 ),
inference(sat_conversion,[],[f753]) ).
cnf(s59,plain,
( spl0_2
| spl0_50
| ~ spl0_51 ),
inference(sat_conversion,[],[f865]) ).
cnf(s83,plain,
spl0_51,
inference(sat_conversion,[],[f1079]) ).
cnf(s86,plain,
( spl0_30
| spl0_31
| spl0_64 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s87,plain,
spl0_54,
inference(sat_conversion,[],[f1114]) ).
cnf(s108,plain,
spl0_32,
inference(sat_conversion,[],[f1633]) ).
cnf(s147,plain,
( spl0_16
| ~ spl0_32
| spl0_33
| ~ spl0_64 ),
inference(sat_conversion,[],[f2160]) ).
cnf(s215,plain,
( ~ spl0_25
| spl0_26
| ~ spl0_115 ),
inference(sat_conversion,[],[f2619]) ).
cnf(s238,plain,
( spl0_1
| ~ spl0_33 ),
inference(sat_conversion,[],[f2695]) ).
cnf(s247,plain,
~ spl0_50,
inference(sat_conversion,[],[f2711]) ).
cnf(s281,plain,
( spl0_1
| ~ spl0_30 ),
inference(sat_conversion,[],[f2934]) ).
cnf(s351,plain,
spl0_131,
inference(sat_conversion,[],[f3382]) ).
cnf(s356,plain,
( spl0_61
| ~ spl0_71 ),
inference(sat_conversion,[],[f3419]) ).
cnf(s377,plain,
~ spl0_61,
inference(sat_conversion,[],[f3612]) ).
cnf(s386,plain,
( spl0_61
| spl0_69
| spl0_71 ),
inference(sat_conversion,[],[f3646]) ).
cnf(s487,plain,
( spl0_3
| spl0_50
| ~ spl0_54
| ~ spl0_69
| spl0_115
| ~ spl0_131 ),
inference(sat_conversion,[],[f4404]) ).
cnf(s492,plain,
~ spl0_71,
inference(rat,[],[s356,s377]) ).
cnf(s493,plain,
spl0_69,
inference(rat,[],[s386,s377,s492]) ).
cnf(s519,plain,
spl0_2,
inference(rat,[],[s59,s83,s247]) ).
cnf(s529,plain,
spl0_25,
inference(rat,[],[s28,s38]) ).
cnf(s530,plain,
~ spl0_115,
inference(rat,[],[s215,s38,s529]) ).
cnf(s535,plain,
spl0_3,
inference(rat,[],[s487,s351,s87,s493,s247,s530]) ).
cnf(s546,plain,
~ spl0_1,
inference(rat,[],[s1,s535,s519]) ).
cnf(s547,plain,
~ spl0_30,
inference(rat,[],[s281,s546]) ).
cnf(s548,plain,
~ spl0_33,
inference(rat,[],[s238,s546]) ).
cnf(s550,plain,
~ spl0_16,
inference(rat,[],[s42,s546]) ).
cnf(s552,plain,
~ spl0_31,
inference(rat,[],[s43,s547]) ).
cnf(s559,plain,
~ spl0_64,
inference(rat,[],[s147,s548,s108,s550]) ).
cnf(s566,plain,
$false,
inference(rat,[],[s86,s547,s559,s552]) ).
fof(f4405,plain,
$false,
inference(avatar_sat_refutation,[],[s566]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT051-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.35 % Computer : n003.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 27 17:29:56 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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
% 3.11/1.39 % (809970)Input is clausal, will run a generic CNF schedule.
% 3.11/1.39 % (809979)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3859219469:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.11/1.39 % (809979)Instruction limit reached!
% 3.11/1.39 % (809979)------------------------------
% 3.11/1.39 % (809979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.11/1.39 % (809979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/1.39 % (809979)CaDiCaL version: 2.1.3
% 3.11/1.39 % (809979)Termination reason: Instruction limit
% 3.11/1.39 % (809979)Termination phase: Saturation
% 3.11/1.39 % (809979)Time elapsed: 0.042 s
% 3.11/1.39 % (809979)Peak memory usage: 89 MB
% 3.11/1.39 % (809979)Instructions burned: 118 (million)
% 3.11/1.39 % (809978)lrs+10_1_sil=8000:sp=occurrence:random_seed=161318961:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.11/1.39 % (809975)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=2308412949:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.11/1.39 % (809981)dis-21_1_sil=8000:lcm=predicate:random_seed=3998834030: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)
% 3.11/1.39 % (809977)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1587322802:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.11/1.39 % (809976)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2566215887:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.11/1.39 % (809980)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1465008128:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.11/1.39 % (809981)Instruction limit reached!
% 3.11/1.39 % (809981)------------------------------
% 3.11/1.39 % (809981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.11/1.39 % (809981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/1.39 % (809981)CaDiCaL version: 2.1.3
% 3.11/1.39 % (809981)Termination reason: Instruction limit
% 3.11/1.39 % (809981)Termination phase: Saturation
% 3.11/1.39 % (809981)Time elapsed: 0.067 s
% 3.11/1.39 % (809981)Peak memory usage: 88 MB
% 3.11/1.39 % (809981)Instructions burned: 117 (million)
% 3.11/1.39 % (809978)Instruction limit reached!
% 3.11/1.39 % (809978)------------------------------
% 3.11/1.39 % (809978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.11/1.39 % (809978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/1.39 % (809978)CaDiCaL version: 2.1.3
% 3.11/1.39 % (809978)Termination reason: Instruction limit
% 3.11/1.39 % (809978)Termination phase: Saturation
% 3.11/1.39 % (809978)Time elapsed: 0.072 s
% 3.11/1.39 % (809978)Peak memory usage: 89 MB
% 3.11/1.39 % (809978)Instructions burned: 109 (million)
% 3.11/1.39 % (809983)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=474549323:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.11/1.39 % (809980)First to succeed.
% 3.11/1.39 % (809980)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-809970"
% 3.11/1.39 % (809983)Instruction limit reached!
% 3.11/1.39 % (809983)------------------------------
% 3.11/1.39 % (809983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.11/1.39 % (809983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/1.39 % (809983)CaDiCaL version: 2.1.3
% 3.11/1.39 % (809983)Termination reason: Instruction limit
% 3.11/1.39 % (809983)Termination phase: Saturation
% 3.11/1.39 % (809983)Time elapsed: 0.054 s
% 3.11/1.39 % (809983)Peak memory usage: 89 MB
% 3.11/1.39 % (809983)Instructions burned: 144 (million)
% 3.11/1.39 % (809990)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1551476636: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)
% 3.11/1.39 % (809991)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3373049640:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.11/1.39 % (809990)Refutation not found, incomplete strategy
% 3.11/1.39 % (809990)------------------------------
% 3.11/1.39 % (809990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.11/1.39 % (809990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/1.39 % (809990)CaDiCaL version: 2.1.3
% 3.11/1.39 % (809990)Termination reason: Refutation not found, incomplete strategy
% 3.11/1.39 % (809990)Time elapsed: 0.013 s
% 3.11/1.39 % (809990)Peak memory usage: 88 MB
% 3.11/1.39 % (809990)Instructions burned: 19 (million)
% 3.11/1.39 % (809993)lrs+10_64_to=lpo:sil=8000:random_seed=1816651280:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 3.11/1.39 % (809993)Instruction limit reached!
% 3.11/1.39 % (809993)------------------------------
% 3.11/1.39 % (809993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.11/1.39 % (809993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/1.39 % (809993)CaDiCaL version: 2.1.3
% 3.11/1.39 % (809993)Termination reason: Instruction limit
% 3.11/1.39 % (809993)Termination phase: Saturation
% 3.11/1.39 % (809993)Time elapsed: 0.037 s
% 3.11/1.39 % (809993)Peak memory usage: 88 MB
% 3.11/1.39 % (809993)Instructions burned: 127 (million)
% 3.11/1.39 % (809991)Instruction limit reached!
% 3.11/1.39 % (809991)------------------------------
% 3.11/1.39 % (809991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.11/1.39 % (809991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.11/1.39 % (809991)CaDiCaL version: 2.1.3
% 3.11/1.39 % (809991)Termination reason: Instruction limit
% 3.11/1.39 % (809991)Termination phase: Saturation
% 3.11/1.39 % (809991)Time elapsed: 0.127 s
% 3.11/1.39 % (809991)Peak memory usage: 89 MB
% 3.11/1.39 % (809991)Instructions burned: 220 (million)
% 3.11/1.39 % (809980)Refutation found. Thanks to Tanya!
% 3.11/1.39 % SZS status Unsatisfiable for theBenchmark
% 3.11/1.39 % SZS output start Proof for theBenchmark
% See solution above
% 4.44/1.58 % (809980)------------------------------
% 4.44/1.58 % (809980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.58 % (809980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.58 % (809980)CaDiCaL version: 2.1.3
% 4.44/1.58 % (809980)Termination reason: Refutation
% 4.44/1.58 % (809980)Time elapsed: 0.117 s
% 4.44/1.58 % (809980)Peak memory usage: 91 MB
% 4.44/1.58 % (809980)Instructions burned: 166 (million)
% 4.44/1.58 % (809980)------------------------------
% 4.44/1.58 % (809980)------------------------------
% 4.44/1.58 % (809970)Success in time 0.552 s
% 4.44/1.58 % Vampire exiting
%------------------------------------------------------------------------------