%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO029-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 09:51:15 AM UTC 2026
% Result : Unsatisfiable 5.68s 1.82s
% Output : Refutation 7.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 29
% Syntax : Number of formulae : 133 ( 36 unt; 18 def)
% Number of atoms : 305 ( 29 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 319 ( 147 ~; 156 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 17 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-5 aty)
% Number of variables : 83 ( 0 sgn 83 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : equidistant(X0,X1,X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_equidistance) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(X0,X1,X4,X5)
| ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_for_equidistance) ).
fof(f3,axiom,
! [X2,X0,X1] :
( ~ equidistant(X0,X1,X2,X2)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_for_equidistance) ).
fof(f4,axiom,
! [X2,X3,X0,X1] : between(X0,X1,extension(X0,X1,X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction1) ).
fof(f5,axiom,
! [X2,X3,X0,X1] : equidistant(X0,extension(X1,X0,X2,X3),X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction2) ).
fof(f6,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ equidistant(X1,X6,X3,X7)
| ~ equidistant(X1,X4,X3,X5)
| ~ equidistant(X0,X6,X2,X7)
| ~ equidistant(X0,X1,X2,X3)
| ~ between(X0,X1,X4)
| ~ between(X2,X3,X5)
| X0 = X1
| equidistant(X4,X6,X5,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outer_five_segment) ).
fof(f7,axiom,
! [X0,X1] :
( ~ between(X0,X1,X0)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_for_betweeness) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4] :
( between(X1,inner_pasch(X0,X1,X2,X4,X3),X3)
| ~ between(X3,X4,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inner_pasch1) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X4] :
( between(X4,inner_pasch(X0,X1,X2,X4,X3),X0)
| ~ between(X3,X4,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inner_pasch2) ).
fof(f19,axiom,
u != v,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_not_v) ).
fof(f20,negated_conjecture,
extension(u,v,u,v) != extension(u,v,v,u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_equal_extensions) ).
fof(f21,definition,
sF0 = extension(u,v,u,v),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f22,plain,
extension(u,v,u,v) = sF0,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF1 = extension(u,v,v,u),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f24,plain,
extension(u,v,v,u) = sF1,
inference(reorient_equations,[],[f23]) ).
fof(f25,plain,
sF0 != sF1,
inference(definition_folding,[],[f20,f24,f22]) ).
fof(f27,definition,
( spl2_1
<=> sF0 = sF1 ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f29,plain,
( sF0 != sF1
| spl2_1 ),
inference(avatar_component_clause,[],[f27]) ).
fof(f30,plain,
~ spl2_1,
inference(avatar_split_clause,[],[f25,f27]) ).
fof(f32,definition,
( spl2_2
<=> u = v ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f34,plain,
( u != v
| spl2_2 ),
inference(avatar_component_clause,[],[f32]) ).
fof(f35,plain,
~ spl2_2,
inference(avatar_split_clause,[],[f19,f32]) ).
fof(f52,definition,
( spl2_6
<=> extension(u,v,u,v) = sF0 ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f54,plain,
( extension(u,v,u,v) = sF0
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f52]) ).
fof(f55,plain,
spl2_6,
inference(avatar_split_clause,[],[f22,f52]) ).
fof(f57,definition,
( spl2_7
<=> extension(u,v,v,u) = sF1 ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f59,plain,
( extension(u,v,v,u) = sF1
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f57]) ).
fof(f60,plain,
spl2_7,
inference(avatar_split_clause,[],[f24,f57]) ).
fof(f62,plain,
( between(u,v,sF0)
| ~ spl2_6 ),
inference(superposition,[],[f4,f54]) ).
fof(f63,plain,
( between(u,v,sF1)
| ~ spl2_7 ),
inference(superposition,[],[f4,f59]) ).
fof(f65,definition,
( spl2_8
<=> between(u,v,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f67,plain,
( between(u,v,sF1)
| ~ spl2_8 ),
inference(avatar_component_clause,[],[f65]) ).
fof(f68,plain,
( spl2_8
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f63,f57,f65]) ).
fof(f70,definition,
( spl2_9
<=> between(u,v,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f72,plain,
( between(u,v,sF0)
| ~ spl2_9 ),
inference(avatar_component_clause,[],[f70]) ).
fof(f73,plain,
( spl2_9
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f62,f52,f70]) ).
fof(f74,plain,
! [X2,X0,X1] : extension(X1,X0,X2,X2) = X0,
inference(resolution,[],[f5,f3]) ).
fof(f87,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X1,X0) ),
inference(resolution,[],[f2,f1]) ).
fof(f88,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(X0,extension(X1,X0,X2,X3),X4,X5)
| equidistant(X4,X5,X2,X3) ),
inference(resolution,[],[f2,f5]) ).
fof(f89,plain,
! [X2,X3,X0,X1] :
( ~ between(X3,X0,X2)
| ~ between(X0,X1,X2)
| inner_pasch(X3,X0,X2,X1,X0) = X0 ),
inference(resolution,[],[f8,f7]) ).
fof(f94,plain,
! [X0,X1] : between(X1,X0,X0),
inference(superposition,[],[f4,f74]) ).
fof(f148,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ equidistant(X4,extension(X5,X0,X2,X6),X7,X6)
| ~ equidistant(X0,X1,X2,X3)
| ~ equidistant(X4,X0,X7,X2)
| ~ between(X4,X0,X1)
| ~ between(X7,X2,X3)
| X0 = X4
| equidistant(X1,extension(X5,X0,X2,X6),X3,X6) ),
inference(resolution,[],[f6,f5]) ).
fof(f163,plain,
! [X2,X3,X0,X1] : equidistant(extension(X0,X1,X2,X3),X1,X2,X3),
inference(resolution,[],[f88,f1]) ).
fof(f183,plain,
( ! [X0] :
( ~ between(v,X0,sF1)
| v = inner_pasch(u,v,sF1,X0,v) )
| ~ spl2_8 ),
inference(resolution,[],[f89,f67]) ).
fof(f233,definition,
( spl2_22
<=> equidistant(v,u,v,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_22])],[avatar_definition]) ).
fof(f234,plain,
( equidistant(v,u,v,sF1)
| ~ spl2_22 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f235,plain,
( ~ equidistant(v,u,v,sF1)
| spl2_22 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f273,definition,
( spl2_26
<=> equidistant(v,sF0,v,u) ),
introduced(definition,[new_symbols(definition,[spl2_26])],[avatar_definition]) ).
fof(f274,plain,
( equidistant(v,sF0,v,u)
| ~ spl2_26 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f275,plain,
( ~ equidistant(v,sF0,v,u)
| spl2_26 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f289,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ equidistant(X4,X0,extension(X5,X0,X2,X4),X2)
| ~ equidistant(X0,X1,X2,X3)
| ~ between(X4,X0,X1)
| ~ between(extension(X5,X0,X2,X4),X2,X3)
| X0 = X4
| equidistant(X1,extension(X5,X0,X2,X4),X3,X4) ),
inference(resolution,[],[f148,f1]) ).
fof(f330,plain,
( equidistant(sF0,v,u,v)
| ~ spl2_6 ),
inference(superposition,[],[f163,f54]) ).
fof(f331,plain,
( equidistant(sF1,v,v,u)
| ~ spl2_7 ),
inference(superposition,[],[f163,f59]) ).
fof(f334,definition,
( spl2_28
<=> equidistant(sF1,v,v,u) ),
introduced(definition,[new_symbols(definition,[spl2_28])],[avatar_definition]) ).
fof(f336,plain,
( equidistant(sF1,v,v,u)
| ~ spl2_28 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f337,plain,
( spl2_28
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f331,f57,f334]) ).
fof(f339,definition,
( spl2_29
<=> equidistant(sF0,v,u,v) ),
introduced(definition,[new_symbols(definition,[spl2_29])],[avatar_definition]) ).
fof(f341,plain,
( equidistant(sF0,v,u,v)
| ~ spl2_29 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f342,plain,
( spl2_29
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f330,f52,f339]) ).
fof(f345,plain,
( equidistant(v,u,v,sF1)
| ~ spl2_28 ),
inference(resolution,[],[f336,f87]) ).
fof(f347,plain,
( $false
| spl2_22
| ~ spl2_28 ),
inference(forward_subsumption_resolution,[],[f345,f235]) ).
fof(f348,plain,
( spl2_22
| ~ spl2_28 ),
inference(avatar_contradiction_clause,[],[f347]) ).
fof(f351,plain,
( equidistant(v,sF1,u,v)
| ~ spl2_22 ),
inference(resolution,[],[f234,f87]) ).
fof(f360,definition,
( spl2_31
<=> equidistant(v,sF1,u,v) ),
introduced(definition,[new_symbols(definition,[spl2_31])],[avatar_definition]) ).
fof(f362,plain,
( equidistant(v,sF1,u,v)
| ~ spl2_31 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f363,plain,
( spl2_31
| ~ spl2_22 ),
inference(avatar_split_clause,[],[f351,f233,f360]) ).
fof(f419,plain,
( equidistant(u,v,sF1,v)
| ~ spl2_31 ),
inference(resolution,[],[f362,f87]) ).
fof(f422,definition,
( spl2_38
<=> equidistant(u,v,sF1,v) ),
introduced(definition,[new_symbols(definition,[spl2_38])],[avatar_definition]) ).
fof(f424,plain,
( equidistant(u,v,sF1,v)
| ~ spl2_38 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f425,plain,
( spl2_38
| ~ spl2_31 ),
inference(avatar_split_clause,[],[f419,f360,f422]) ).
fof(f426,plain,
( v = inner_pasch(u,v,sF1,sF1,v)
| ~ spl2_8 ),
inference(resolution,[],[f183,f94]) ).
fof(f431,definition,
( spl2_39
<=> v = inner_pasch(u,v,sF1,sF1,v) ),
introduced(definition,[new_symbols(definition,[spl2_39])],[avatar_definition]) ).
fof(f433,plain,
( v = inner_pasch(u,v,sF1,sF1,v)
| ~ spl2_39 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f434,plain,
( spl2_39
| ~ spl2_8 ),
inference(avatar_split_clause,[],[f426,f65,f431]) ).
fof(f437,plain,
( equidistant(u,v,v,sF0)
| ~ spl2_29 ),
inference(resolution,[],[f341,f87]) ).
fof(f440,definition,
( spl2_40
<=> equidistant(u,v,v,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_40])],[avatar_definition]) ).
fof(f442,plain,
( equidistant(u,v,v,sF0)
| ~ spl2_40 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f443,plain,
( spl2_40
| ~ spl2_29 ),
inference(avatar_split_clause,[],[f437,f339,f440]) ).
fof(f459,plain,
( equidistant(v,sF0,v,u)
| ~ spl2_40 ),
inference(resolution,[],[f442,f87]) ).
fof(f461,plain,
( $false
| spl2_26
| ~ spl2_40 ),
inference(forward_subsumption_resolution,[],[f459,f275]) ).
fof(f462,plain,
( spl2_26
| ~ spl2_40 ),
inference(avatar_contradiction_clause,[],[f461]) ).
fof(f701,definition,
( spl2_55
<=> equidistant(sF0,sF1,u,u) ),
introduced(definition,[new_symbols(definition,[spl2_55])],[avatar_definition]) ).
fof(f702,plain,
( ~ equidistant(sF0,sF1,u,u)
| spl2_55 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f703,plain,
( equidistant(sF0,sF1,u,u)
| ~ spl2_55 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f760,plain,
( sF0 = sF1
| ~ spl2_55 ),
inference(resolution,[],[f703,f3]) ).
fof(f771,plain,
( $false
| spl2_1
| ~ spl2_55 ),
inference(forward_subsumption_resolution,[],[f760,f29]) ).
fof(f772,plain,
( spl2_1
| ~ spl2_55 ),
inference(avatar_contradiction_clause,[],[f771]) ).
fof(f783,plain,
( ! [X0,X1] :
( ~ equidistant(u,v,sF1,v)
| ~ equidistant(v,X0,v,X1)
| ~ between(u,v,X0)
| ~ between(sF1,v,X1)
| u = v
| equidistant(X0,sF1,X1,u) )
| ~ spl2_7 ),
inference(superposition,[],[f289,f59]) ).
fof(f785,plain,
( ! [X0,X1] :
( ~ equidistant(v,X0,v,X1)
| ~ between(u,v,X0)
| ~ between(sF1,v,X1)
| u = v
| equidistant(X0,sF1,X1,u) )
| ~ spl2_7
| ~ spl2_38 ),
inference(forward_subsumption_resolution,[],[f783,f424]) ).
fof(f786,plain,
( ! [X0,X1] :
( ~ equidistant(v,X0,v,X1)
| ~ between(u,v,X0)
| ~ between(sF1,v,X1)
| equidistant(X0,sF1,X1,u) )
| spl2_2
| ~ spl2_7
| ~ spl2_38 ),
inference(forward_subsumption_resolution,[],[f785,f34]) ).
fof(f814,plain,
( between(sF1,v,u)
| ~ between(v,sF1,sF1)
| ~ between(u,v,sF1)
| ~ spl2_39 ),
inference(superposition,[],[f9,f433]) ).
fof(f816,plain,
( between(sF1,v,u)
| ~ between(u,v,sF1)
| ~ spl2_39 ),
inference(forward_subsumption_resolution,[],[f814,f94]) ).
fof(f817,plain,
( between(sF1,v,u)
| ~ spl2_8
| ~ spl2_39 ),
inference(forward_subsumption_resolution,[],[f816,f67]) ).
fof(f819,definition,
( spl2_61
<=> between(sF1,v,u) ),
introduced(definition,[new_symbols(definition,[spl2_61])],[avatar_definition]) ).
fof(f821,plain,
( between(sF1,v,u)
| ~ spl2_61 ),
inference(avatar_component_clause,[],[f819]) ).
fof(f822,plain,
( spl2_61
| ~ spl2_8
| ~ spl2_39 ),
inference(avatar_split_clause,[],[f817,f431,f65,f819]) ).
fof(f1537,plain,
( ~ between(u,v,sF0)
| ~ between(sF1,v,u)
| equidistant(sF0,sF1,u,u)
| spl2_2
| ~ spl2_7
| ~ spl2_26
| ~ spl2_38 ),
inference(resolution,[],[f786,f274]) ).
fof(f1559,plain,
( ~ between(sF1,v,u)
| equidistant(sF0,sF1,u,u)
| spl2_2
| ~ spl2_7
| ~ spl2_9
| ~ spl2_26
| ~ spl2_38 ),
inference(forward_subsumption_resolution,[],[f1537,f72]) ).
fof(f1561,plain,
( equidistant(sF0,sF1,u,u)
| spl2_2
| ~ spl2_7
| ~ spl2_9
| ~ spl2_26
| ~ spl2_38
| ~ spl2_61 ),
inference(forward_subsumption_resolution,[],[f1559,f821]) ).
fof(f1567,plain,
( $false
| spl2_2
| ~ spl2_7
| ~ spl2_9
| ~ spl2_26
| ~ spl2_38
| spl2_55
| ~ spl2_61 ),
inference(forward_subsumption_resolution,[],[f1561,f702]) ).
fof(f1568,plain,
( spl2_2
| ~ spl2_7
| ~ spl2_9
| ~ spl2_26
| ~ spl2_38
| spl2_55
| ~ spl2_61 ),
inference(avatar_contradiction_clause,[],[f1567]) ).
cnf(s1,plain,
~ spl2_1,
inference(sat_conversion,[],[f30]) ).
cnf(s2,plain,
~ spl2_2,
inference(sat_conversion,[],[f35]) ).
cnf(s6,plain,
spl2_6,
inference(sat_conversion,[],[f55]) ).
cnf(s7,plain,
spl2_7,
inference(sat_conversion,[],[f60]) ).
cnf(s8,plain,
( ~ spl2_7
| spl2_8 ),
inference(sat_conversion,[],[f68]) ).
cnf(s9,plain,
( ~ spl2_6
| spl2_9 ),
inference(sat_conversion,[],[f73]) ).
cnf(s24,plain,
( ~ spl2_7
| spl2_28 ),
inference(sat_conversion,[],[f337]) ).
cnf(s25,plain,
( ~ spl2_6
| spl2_29 ),
inference(sat_conversion,[],[f342]) ).
cnf(s26,plain,
( spl2_22
| ~ spl2_28 ),
inference(sat_conversion,[],[f348]) ).
cnf(s28,plain,
( ~ spl2_22
| spl2_31 ),
inference(sat_conversion,[],[f363]) ).
cnf(s37,plain,
( ~ spl2_31
| spl2_38 ),
inference(sat_conversion,[],[f425]) ).
cnf(s38,plain,
( ~ spl2_8
| spl2_39 ),
inference(sat_conversion,[],[f434]) ).
cnf(s39,plain,
( ~ spl2_29
| spl2_40 ),
inference(sat_conversion,[],[f443]) ).
cnf(s41,plain,
( spl2_26
| ~ spl2_40 ),
inference(sat_conversion,[],[f462]) ).
cnf(s67,plain,
( spl2_1
| ~ spl2_55 ),
inference(sat_conversion,[],[f772]) ).
cnf(s69,plain,
( ~ spl2_8
| ~ spl2_39
| spl2_61 ),
inference(sat_conversion,[],[f822]) ).
cnf(s92,plain,
( spl2_2
| ~ spl2_7
| ~ spl2_9
| ~ spl2_26
| ~ spl2_38
| spl2_55
| ~ spl2_61 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s93,plain,
spl2_28,
inference(rat,[],[s24,s7]) ).
cnf(s95,plain,
spl2_8,
inference(rat,[],[s8,s7]) ).
cnf(s96,plain,
spl2_22,
inference(rat,[],[s26,s93]) ).
cnf(s99,plain,
spl2_39,
inference(rat,[],[s38,s95]) ).
cnf(s100,plain,
spl2_31,
inference(rat,[],[s28,s96]) ).
cnf(s102,plain,
spl2_61,
inference(rat,[],[s69,s95,s99]) ).
cnf(s103,plain,
spl2_38,
inference(rat,[],[s37,s100]) ).
cnf(s106,plain,
spl2_29,
inference(rat,[],[s25,s6]) ).
cnf(s108,plain,
spl2_9,
inference(rat,[],[s9,s6]) ).
cnf(s109,plain,
spl2_40,
inference(rat,[],[s39,s106]) ).
cnf(s113,plain,
spl2_26,
inference(rat,[],[s41,s109]) ).
cnf(s127,plain,
spl2_55,
inference(rat,[],[s92,s102,s113,s103,s108,s7,s2]) ).
cnf(s132,plain,
spl2_1,
inference(rat,[],[s67,s127]) ).
cnf(s145,plain,
$false,
inference(rat,[],[s1,s132]) ).
fof(f1569,plain,
$false,
inference(avatar_sat_refutation,[],[s145]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO029-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 % Computer : n026.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Sun Sep 27 06:39:57 UTC 2026
% 0.13/0.42 % CPUTime :
% 0.13/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.44 Running first-order theorem proving
% 0.13/0.44 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.68/1.82 % (2471492)Input is clausal, will run a generic CNF schedule.
% 5.68/1.82 % (2471500)lrs+10_1_sil=8000:sp=occurrence:random_seed=287134738:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.68/1.82 % (2471502)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3241797451:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.68/1.82 % (2471501)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2567670313:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.68/1.82 % (2471498)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2400843767:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.68/1.82 % (2471499)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1385110607:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.68/1.82 % (2471497)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=3990190672:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.68/1.82 % (2471500)Instruction limit reached!
% 5.68/1.82 % (2471500)------------------------------
% 5.68/1.82 % (2471500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471500)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471500)Termination reason: Instruction limit
% 5.68/1.82 % (2471500)Termination phase: Saturation
% 5.68/1.82 % (2471500)Time elapsed: 0.038 s
% 5.68/1.82 % (2471500)Peak memory usage: 88 MB
% 5.68/1.82 % (2471500)Instructions burned: 109 (million)
% 5.68/1.82 % (2471503)dis-21_1_sil=8000:lcm=predicate:random_seed=4126469764: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)
% 5.68/1.82 % (2471501)Instruction limit reached!
% 5.68/1.82 % (2471501)------------------------------
% 5.68/1.82 % (2471501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471501)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471501)Termination reason: Instruction limit
% 5.68/1.82 % (2471501)Termination phase: Saturation
% 5.68/1.82 % (2471501)Time elapsed: 0.069 s
% 5.68/1.82 % (2471501)Peak memory usage: 88 MB
% 5.68/1.82 % (2471501)Instructions burned: 114 (million)
% 5.68/1.82 % (2471503)Instruction limit reached!
% 5.68/1.82 % (2471503)------------------------------
% 5.68/1.82 % (2471503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471503)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471503)Termination reason: Instruction limit
% 5.68/1.82 % (2471503)Termination phase: Saturation
% 5.68/1.82 % (2471503)Time elapsed: 0.070 s
% 5.68/1.82 % (2471503)Peak memory usage: 89 MB
% 5.68/1.82 % (2471503)Instructions burned: 117 (million)
% 5.68/1.82 % (2471510)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=3063691203:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.68/1.82 % (2471510)Refutation not found, incomplete strategy
% 5.68/1.82 % (2471510)------------------------------
% 5.68/1.82 % (2471510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471510)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471510)Termination reason: Refutation not found, incomplete strategy
% 5.68/1.82 % (2471510)Time elapsed: 0.001 s
% 5.68/1.82 % (2471510)Peak memory usage: 88 MB
% 5.68/1.82 % (2471510)Instructions burned: 1 (million)
% 5.68/1.82 % (2471502)Instruction limit reached!
% 5.68/1.82 % (2471502)------------------------------
% 5.68/1.82 % (2471502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471502)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471502)Termination reason: Instruction limit
% 5.68/1.82 % (2471502)Termination phase: Saturation
% 5.68/1.82 % (2471502)Time elapsed: 0.111 s
% 5.68/1.82 % (2471502)Peak memory usage: 88 MB
% 5.68/1.82 % (2471502)Instructions burned: 181 (million)
% 5.68/1.82 % (2471513)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1061228550:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.68/1.82 % (2471512)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2658553580: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)
% 5.68/1.82 % (2471513)Refutation not found, incomplete strategy
% 5.68/1.82 % (2471513)------------------------------
% 5.68/1.82 % (2471513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471513)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471513)Termination reason: Refutation not found, incomplete strategy
% 5.68/1.82 % (2471513)Time elapsed: 0.001 s
% 5.68/1.82 % (2471513)Peak memory usage: 87 MB
% 5.68/1.82 % (2471515)lrs+10_64_to=lpo:sil=8000:random_seed=3129130183:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 5.68/1.82 % (2471510)------------------------------
% 5.68/1.82 % (2471510)------------------------------
% 5.68/1.82 % (2471515)Instruction limit reached!
% 5.68/1.82 % (2471515)------------------------------
% 5.68/1.82 % (2471515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471515)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471515)Termination reason: Instruction limit
% 5.68/1.82 % (2471515)Termination phase: Saturation
% 5.68/1.82 % (2471515)Time elapsed: 0.078 s
% 5.68/1.82 % (2471515)Peak memory usage: 88 MB
% 5.68/1.82 % (2471515)Instructions burned: 126 (million)
% 5.68/1.82 % (2471512)Instruction limit reached!
% 5.68/1.82 % (2471512)------------------------------
% 5.68/1.82 % (2471512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471512)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471512)Termination reason: Instruction limit
% 5.68/1.82 % (2471512)Termination phase: Saturation
% 5.68/1.82 % (2471512)Time elapsed: 0.114 s
% 5.68/1.82 % (2471512)Peak memory usage: 89 MB
% 5.68/1.82 % (2471512)Instructions burned: 189 (million)
% 5.68/1.82 % (2471519)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3559833397:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 5.68/1.82 % (2471519)Instruction limit reached!
% 5.68/1.82 % (2471519)------------------------------
% 5.68/1.82 % (2471519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471519)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471519)Termination reason: Instruction limit
% 5.68/1.82 % (2471519)Termination phase: Saturation
% 5.68/1.82 % (2471519)Time elapsed: 0.065 s
% 5.68/1.82 % (2471519)Peak memory usage: 89 MB
% 5.68/1.82 % (2471519)Instructions burned: 196 (million)
% 5.68/1.82 % (2471520)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2883531251:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.68/1.82 % (2471513)------------------------------
% 5.68/1.82 % (2471513)------------------------------
% 5.68/1.82 % (2471521)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3871732482:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 5.68/1.82 % (2471523)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3436218463:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 5.68/1.82 % (2471520)First to succeed.
% 5.68/1.82 % (2471520)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2471492"
% 5.68/1.82 % (2471523)Instruction limit reached!
% 5.68/1.82 % (2471523)------------------------------
% 5.68/1.82 % (2471523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471523)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471523)Termination reason: Instruction limit
% 5.68/1.82 % (2471523)Termination phase: Saturation
% 5.68/1.82 % (2471523)Time elapsed: 0.032 s
% 5.68/1.82 % (2471523)Peak memory usage: 88 MB
% 5.68/1.82 % (2471523)Instructions burned: 108 (million)
% 5.68/1.82 % (2471525)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1105991471:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 5.68/1.82 % (2471525)Refutation not found, incomplete strategy
% 5.68/1.82 % (2471525)------------------------------
% 5.68/1.82 % (2471525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471525)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471525)Termination reason: Refutation not found, incomplete strategy
% 5.68/1.82 % (2471525)Time elapsed: 0.001 s
% 5.68/1.82 % (2471525)Peak memory usage: 87 MB
% 5.68/1.82 % (2471528)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3110482303:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 5.68/1.82 % (2471498)Also succeeded, but the first one will report.
% 5.68/1.82 % (2471528)Instruction limit reached!
% 5.68/1.82 % (2471528)------------------------------
% 5.68/1.82 % (2471528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.82 % (2471528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.82 % (2471528)CaDiCaL version: 2.1.3
% 5.68/1.82 % (2471528)Termination reason: Instruction limit
% 5.68/1.82 % (2471528)Termination phase: Saturation
% 5.68/1.82 % (2471528)Time elapsed: 0.084 s
% 5.68/1.82 % (2471528)Peak memory usage: 90 MB
% 5.68/1.82 % (2471528)Instructions burned: 245 (million)
% 5.68/1.82 % (2471520)Refutation found. Thanks to Tanya!
% 5.68/1.82 % SZS status Unsatisfiable for theBenchmark
% 5.68/1.82 % SZS output start Proof for theBenchmark
% See solution above
% 7.17/2.01 % (2471520)------------------------------
% 7.17/2.01 % (2471520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.17/2.01 % (2471520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.17/2.01 % (2471520)CaDiCaL version: 2.1.3
% 7.17/2.01 % (2471520)Termination reason: Refutation
% 7.17/2.01 % (2471520)Time elapsed: 0.094 s
% 7.17/2.01 % (2471520)Peak memory usage: 91 MB
% 7.17/2.01 % (2471520)Instructions burned: 133 (million)
% 7.17/2.01 % (2471520)------------------------------
% 7.17/2.01 % (2471520)------------------------------
% 7.17/2.01 % (2471492)Success in time 0.937 s
% 7.17/2.01 % Vampire exiting
%------------------------------------------------------------------------------