%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO009-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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:10 AM UTC 2026
% Result : Unsatisfiable 94.28s 24.84s
% Output : Refutation 170.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 28
% Syntax : Number of formulae : 163 ( 39 unt; 14 def)
% Number of atoms : 403 ( 49 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 454 ( 214 ~; 226 |; 0 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 15 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-5 aty)
% Number of variables : 197 ( 0 sgn 197 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ between(X0,X1,X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_for_betweeness) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( ~ between(X1,X3,X2)
| ~ between(X0,X1,X2)
| between(X0,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_for_betweeness) ).
fof(f3,axiom,
! [X2,X3,X0,X1] :
( ~ between(X0,X1,X3)
| ~ between(X0,X1,X2)
| X0 = X1
| between(X0,X2,X3)
| between(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',connectivity_for_betweeness) ).
fof(f4,axiom,
! [X0,X1] : equidistant(X0,X1,X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_for_equidistance) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ equidistant(X0,X1,X2,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_for_equidistance) ).
fof(f6,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/sandbox2/benchmark/theBenchmark.p',transitivity_for_equidistance) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X4] :
( between(X0,outer_pasch(X1,X0,X3,X4,X2),X3)
| ~ between(X3,X2,X4)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outer_pasch1) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4] :
( between(X4,X1,outer_pasch(X1,X0,X3,X4,X2))
| ~ between(X3,X2,X4)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outer_pasch2) ).
fof(f13,axiom,
! [X2,X3,X0,X1] : between(X0,X1,extension(X0,X1,X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',segment_construction1) ).
fof(f14,axiom,
! [X2,X3,X0,X1] : equidistant(X0,extension(X1,X0,X2,X3),X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',segment_construction2) ).
fof(f21,axiom,
between(a,c,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_between_a_and_e) ).
fof(f22,axiom,
between(a,d,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_between_a_and_e) ).
fof(f23,axiom,
~ between(a,c,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_between_a_and_d) ).
fof(f24,negated_conjecture,
~ between(a,d,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_d_between_a_and_c) ).
fof(f26,plain,
! [X2,X0,X1] : extension(X1,X0,X2,X2) = X0,
inference(resolution,[],[f14,f5]) ).
fof(f28,plain,
! [X0,X1] : between(X1,X0,X0),
inference(superposition,[],[f13,f26]) ).
fof(f29,plain,
! [X0] :
( between(X0,a,c)
| ~ between(X0,a,e) ),
inference(resolution,[],[f2,f21]) ).
fof(f34,plain,
! [X2,X3,X0,X1] :
( ~ equidistant(X0,X1,X2,X3)
| equidistant(X2,X3,X1,X0) ),
inference(resolution,[],[f6,f4]) ).
fof(f38,plain,
! [X2,X3,X0,X1] :
( ~ between(X0,X3,X1)
| ~ between(X0,X1,X2)
| outer_pasch(X3,X0,X0,X2,X1) = X0 ),
inference(resolution,[],[f7,f1]) ).
fof(f39,plain,
! [X2,X3,X0,X1,X4,X5] :
( between(X5,X3,outer_pasch(X4,X3,X0,X2,X1))
| ~ between(X3,X4,X1)
| ~ between(X5,X3,X0)
| ~ between(X0,X1,X2) ),
inference(resolution,[],[f7,f2]) ).
fof(f51,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ between(X5,X2,outer_pasch(X4,X3,X0,X2,X1))
| ~ between(X3,X4,X1)
| ~ between(X0,X1,X2)
| between(X5,X2,X4) ),
inference(resolution,[],[f8,f2]) ).
fof(f55,definition,
( spl0_3
<=> a = d ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f57,plain,
( a = d
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f55]) ).
fof(f64,plain,
! [X0] :
( ~ between(a,d,X0)
| a = d
| between(a,X0,e)
| between(a,e,X0) ),
inference(resolution,[],[f3,f22]) ).
fof(f72,definition,
( spl0_5
<=> ! [X0] :
( ~ between(a,d,X0)
| between(a,e,X0)
| between(a,X0,e) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f73,plain,
( ! [X0] :
( ~ between(a,d,X0)
| between(a,e,X0)
| between(a,X0,e) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f72]) ).
fof(f74,plain,
( spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f64,f72,f55]) ).
fof(f82,plain,
( between(a,a,e)
| ~ spl0_3 ),
inference(superposition,[],[f22,f57]) ).
fof(f83,plain,
( ~ between(a,a,c)
| ~ spl0_3 ),
inference(superposition,[],[f24,f57]) ).
fof(f89,plain,
( ~ between(a,a,e)
| ~ spl0_3 ),
inference(resolution,[],[f83,f29]) ).
fof(f95,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f82,f89]) ).
fof(f96,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f95]) ).
fof(f98,plain,
( ! [X0,X1] :
( between(a,extension(a,d,X0,X1),e)
| between(a,e,extension(a,d,X0,X1)) )
| ~ spl0_5 ),
inference(resolution,[],[f73,f13]) ).
fof(f103,plain,
! [X2,X3,X0,X1] : equidistant(X0,X1,extension(X2,X3,X0,X1),X3),
inference(resolution,[],[f34,f14]) ).
fof(f1535,definition,
( spl0_36
<=> between(a,e,d) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f1537,plain,
( between(a,e,d)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f1535]) ).
fof(f2177,plain,
( ! [X2,X0,X1] :
( ~ between(a,e,X0)
| a = outer_pasch(extension(a,d,X1,X2),a,a,X0,e)
| between(a,e,extension(a,d,X1,X2)) )
| ~ spl0_5 ),
inference(resolution,[],[f38,f98]) ).
fof(f2189,plain,
! [X0] :
( ~ between(a,e,X0)
| a = outer_pasch(c,a,a,X0,e) ),
inference(resolution,[],[f38,f21]) ).
fof(f2190,plain,
! [X0] :
( ~ between(a,e,X0)
| a = outer_pasch(d,a,a,X0,e) ),
inference(resolution,[],[f38,f22]) ).
fof(f2197,plain,
( ! [X0] :
( ~ between(a,d,X0)
| a = outer_pasch(e,a,a,X0,d) )
| ~ spl0_36 ),
inference(resolution,[],[f38,f1537]) ).
fof(f2198,plain,
! [X2,X0,X1] :
( ~ between(X0,X1,X2)
| outer_pasch(X1,X0,X0,X2,X1) = X0 ),
inference(resolution,[],[f38,f28]) ).
fof(f2214,plain,
( a = outer_pasch(e,a,a,d,d)
| ~ spl0_36 ),
inference(resolution,[],[f2197,f28]) ).
fof(f2258,plain,
( ! [X2,X3,X0,X1] :
( between(a,e,extension(a,d,X0,X1))
| a = outer_pasch(extension(a,d,X0,X1),a,a,extension(a,e,X2,X3),e) )
| ~ spl0_5 ),
inference(resolution,[],[f2177,f13]) ).
fof(f2278,plain,
( between(d,e,a)
| ~ between(a,d,d)
| ~ between(a,e,d)
| ~ spl0_36 ),
inference(superposition,[],[f8,f2214]) ).
fof(f2280,plain,
( between(d,e,a)
| ~ between(a,e,d)
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f2278,f28]) ).
fof(f2281,plain,
( between(d,e,a)
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f2280,f1537]) ).
fof(f2297,definition,
( spl0_48
<=> e = d ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f2298,plain,
( e != d
| spl0_48 ),
inference(avatar_component_clause,[],[f2297]) ).
fof(f2299,plain,
( e = d
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f2297]) ).
fof(f2321,plain,
( ~ between(a,c,e)
| ~ spl0_48 ),
inference(superposition,[],[f23,f2299]) ).
fof(f2425,plain,
( $false
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f2321,f21]) ).
fof(f2426,plain,
~ spl0_48,
inference(avatar_contradiction_clause,[],[f2425]) ).
fof(f2569,definition,
( spl0_53
<=> a = outer_pasch(c,a,a,e,e) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f2571,plain,
( a = outer_pasch(c,a,a,e,e)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f2569]) ).
fof(f2574,definition,
( spl0_54
<=> ! [X2,X1] : a = outer_pasch(c,a,a,extension(a,e,X1,X2),e) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f2575,plain,
( ! [X2,X1] : a = outer_pasch(c,a,a,extension(a,e,X1,X2),e)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f2574]) ).
fof(f2595,plain,
( ! [X2,X1] :
( between(a,e,d)
| a = outer_pasch(d,a,a,extension(a,e,X1,X2),e) )
| ~ spl0_5 ),
inference(superposition,[],[f2258,f26]) ).
fof(f3014,definition,
( spl0_57
<=> a = outer_pasch(d,a,a,e,e) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f3016,plain,
( a = outer_pasch(d,a,a,e,e)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f3014]) ).
fof(f3019,definition,
( spl0_58
<=> ! [X2,X1] : a = outer_pasch(d,a,a,extension(a,e,X1,X2),e) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f3020,plain,
( ! [X2,X1] : a = outer_pasch(d,a,a,extension(a,e,X1,X2),e)
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f3019]) ).
fof(f3021,plain,
( spl0_58
| spl0_36
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f2595,f72,f1535,f3019]) ).
fof(f3422,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X0,X1,X2)
| ~ between(X3,X2,X0)
| between(X4,X0,X1)
| ~ between(X0,X1,X2)
| ~ between(X4,X0,X3)
| ~ between(X3,X2,X0) ),
inference(resolution,[],[f51,f39]) ).
fof(f3425,plain,
( ! [X0] :
( ~ between(X0,e,a)
| ~ between(a,c,e)
| ~ between(a,e,e)
| between(X0,e,c) )
| ~ spl0_53 ),
inference(superposition,[],[f51,f2571]) ).
fof(f3428,plain,
! [X2,X3,X0,X1,X4] :
( ~ between(X4,X0,X3)
| ~ between(X3,X2,X0)
| between(X4,X0,X1)
| ~ between(X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f3422]) ).
fof(f3430,plain,
( ! [X0] :
( ~ between(X0,e,a)
| ~ between(a,e,e)
| between(X0,e,c) )
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f3425,f21]) ).
fof(f3431,plain,
( ! [X0] :
( between(X0,e,c)
| ~ between(X0,e,a) )
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f3430,f28]) ).
fof(f4236,plain,
( ! [X0,X1] :
( between(extension(a,e,X0,X1),c,a)
| ~ between(a,e,extension(a,e,X0,X1))
| ~ between(a,c,e) )
| ~ spl0_54 ),
inference(superposition,[],[f8,f2575]) ).
fof(f4238,plain,
( ! [X0,X1] :
( between(extension(a,e,X0,X1),c,a)
| ~ between(a,e,extension(a,e,X0,X1)) )
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f4236,f21]) ).
fof(f4240,plain,
( ! [X0,X1] : between(extension(a,e,X0,X1),c,a)
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f4238,f13]) ).
fof(f5878,plain,
( ! [X0] :
( ~ between(X0,e,a)
| ~ between(a,d,e)
| ~ between(a,e,e)
| between(X0,e,d) )
| ~ spl0_57 ),
inference(superposition,[],[f51,f3016]) ).
fof(f5883,plain,
( ! [X0] :
( ~ between(X0,e,a)
| ~ between(a,e,e)
| between(X0,e,d) )
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f5878,f22]) ).
fof(f5886,plain,
( ! [X0] :
( between(X0,e,d)
| ~ between(X0,e,a) )
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f5883,f28]) ).
fof(f5943,plain,
( ~ between(d,e,a)
| e = d
| ~ spl0_57 ),
inference(resolution,[],[f5886,f1]) ).
fof(f5945,plain,
( ! [X0,X1] :
( ~ between(X0,e,X1)
| ~ between(X0,e,a)
| e = X0
| between(X0,X1,d)
| between(X0,d,X1) )
| ~ spl0_57 ),
inference(resolution,[],[f5886,f3]) ).
fof(f6025,plain,
( ~ between(d,e,a)
| spl0_48
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f5943,f2298]) ).
fof(f6030,definition,
( spl0_68
<=> between(d,e,a) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f6032,plain,
( ~ between(d,e,a)
| spl0_68 ),
inference(avatar_component_clause,[],[f6030]) ).
fof(f6038,plain,
( ~ spl0_68
| spl0_48
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f6025,f3014,f2297,f6030]) ).
fof(f6173,plain,
( ! [X0,X1] :
( between(extension(a,e,X0,X1),d,a)
| ~ between(a,e,extension(a,e,X0,X1))
| ~ between(a,d,e) )
| ~ spl0_58 ),
inference(superposition,[],[f8,f3020]) ).
fof(f6175,plain,
( ! [X0,X1] :
( between(extension(a,e,X0,X1),d,a)
| ~ between(a,e,extension(a,e,X0,X1)) )
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f6173,f22]) ).
fof(f6178,plain,
( ! [X0,X1] : between(extension(a,e,X0,X1),d,a)
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f6175,f13]) ).
fof(f6843,plain,
a = outer_pasch(c,a,a,e,e),
inference(resolution,[],[f2189,f28]) ).
fof(f6848,plain,
! [X0,X1] : a = outer_pasch(c,a,a,extension(a,e,X0,X1),e),
inference(resolution,[],[f2189,f13]) ).
fof(f6849,plain,
spl0_54,
inference(avatar_split_clause,[],[f6848,f2574]) ).
fof(f6879,plain,
spl0_53,
inference(avatar_split_clause,[],[f6843,f2569]) ).
fof(f7660,plain,
a = outer_pasch(d,a,a,e,e),
inference(resolution,[],[f2190,f28]) ).
fof(f8400,plain,
! [X2,X3,X0,X1] : outer_pasch(X0,X1,X1,extension(X1,X0,X2,X3),X0) = X1,
inference(resolution,[],[f2198,f13]) ).
fof(f8412,plain,
( ! [X0,X1] : extension(a,e,X0,X1) = outer_pasch(d,extension(a,e,X0,X1),extension(a,e,X0,X1),a,d)
| ~ spl0_58 ),
inference(resolution,[],[f2198,f6178]) ).
fof(f8414,plain,
( ! [X0,X1] : extension(a,e,X0,X1) = outer_pasch(c,extension(a,e,X0,X1),extension(a,e,X0,X1),a,c)
| ~ spl0_54 ),
inference(resolution,[],[f2198,f4240]) ).
fof(f9666,definition,
( spl0_92
<=> c = d ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f9667,plain,
( c != d
| spl0_92 ),
inference(avatar_component_clause,[],[f9666]) ).
fof(f9668,plain,
( c = d
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f9666]) ).
fof(f9729,plain,
( ~ between(a,c,c)
| ~ spl0_92 ),
inference(superposition,[],[f23,f9668]) ).
fof(f9906,plain,
( $false
| ~ spl0_92 ),
inference(forward_subsumption_resolution,[],[f9729,f28]) ).
fof(f9907,plain,
~ spl0_92,
inference(avatar_contradiction_clause,[],[f9906]) ).
fof(f10881,plain,
( ! [X0] :
( ~ between(X0,e,a)
| e = X0
| between(X0,c,d)
| between(X0,d,c)
| ~ between(X0,e,a) )
| ~ spl0_53
| ~ spl0_57 ),
inference(resolution,[],[f5945,f3431]) ).
fof(f10925,plain,
( ! [X0] :
( between(X0,d,c)
| e = X0
| between(X0,c,d)
| ~ between(X0,e,a) )
| ~ spl0_53
| ~ spl0_57 ),
inference(duplicate_literal_removal,[],[f10881]) ).
fof(f11436,plain,
( ! [X0,X1] :
( between(a,d,extension(a,e,X0,X1))
| ~ between(extension(a,e,X0,X1),d,a)
| ~ between(extension(a,e,X0,X1),d,d) )
| ~ spl0_58 ),
inference(superposition,[],[f8,f8412]) ).
fof(f11438,plain,
( ! [X0,X1] :
( between(a,d,extension(a,e,X0,X1))
| ~ between(extension(a,e,X0,X1),d,d) )
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f11436,f6178]) ).
fof(f11441,plain,
( ! [X0,X1] : between(a,d,extension(a,e,X0,X1))
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f11438,f28]) ).
fof(f11815,plain,
( ! [X0,X1] :
( between(a,c,extension(a,e,X0,X1))
| ~ between(extension(a,e,X0,X1),c,a)
| ~ between(extension(a,e,X0,X1),c,c) )
| ~ spl0_54 ),
inference(superposition,[],[f8,f8414]) ).
fof(f11817,plain,
( ! [X0,X1] :
( between(a,c,extension(a,e,X0,X1))
| ~ between(extension(a,e,X0,X1),c,c) )
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f11815,f4240]) ).
fof(f11820,plain,
( ! [X0,X1] : between(a,c,extension(a,e,X0,X1))
| ~ spl0_54 ),
inference(forward_subsumption_resolution,[],[f11817,f28]) ).
fof(f15840,plain,
! [X2,X3,X0,X1] :
( between(extension(X0,X1,X2,X3),X1,X0)
| ~ between(X0,X1,extension(X0,X1,X2,X3))
| ~ between(X0,X1,X1) ),
inference(superposition,[],[f8,f8400]) ).
fof(f15936,plain,
! [X2,X3,X0,X1] :
( between(extension(X0,X1,X2,X3),X1,X0)
| ~ between(X0,X1,X1) ),
inference(forward_subsumption_resolution,[],[f15840,f13]) ).
fof(f15954,plain,
! [X2,X3,X0,X1] : between(extension(X0,X1,X2,X3),X1,X0),
inference(forward_subsumption_resolution,[],[f15936,f28]) ).
fof(f24739,plain,
( ! [X2,X3,X0,X1] :
( ~ between(extension(a,e,X0,X1),X2,c)
| between(a,c,X3)
| ~ between(c,X3,X2) )
| ~ spl0_54 ),
inference(resolution,[],[f3428,f11820]) ).
fof(f24740,plain,
( ! [X2,X3,X0,X1] :
( ~ between(extension(a,e,X0,X1),X2,d)
| between(a,d,X3)
| ~ between(d,X3,X2) )
| ~ spl0_58 ),
inference(resolution,[],[f3428,f11441]) ).
fof(f34354,plain,
( ! [X2,X0,X1] :
( between(a,c,X0)
| ~ between(c,X0,d)
| e = extension(a,e,X1,X2)
| between(extension(a,e,X1,X2),c,d)
| ~ between(extension(a,e,X1,X2),e,a) )
| ~ spl0_53
| ~ spl0_54
| ~ spl0_57 ),
inference(resolution,[],[f24739,f10925]) ).
fof(f34356,plain,
( ! [X2,X0,X1] :
( between(a,c,X0)
| ~ between(c,X0,d)
| e = extension(a,e,X1,X2)
| between(extension(a,e,X1,X2),c,d) )
| ~ spl0_53
| ~ spl0_54
| ~ spl0_57 ),
inference(forward_subsumption_resolution,[],[f34354,f15954]) ).
fof(f34374,definition,
( spl0_292
<=> ! [X2,X1] :
( e = extension(a,e,X1,X2)
| between(extension(a,e,X1,X2),c,d) ) ),
introduced(definition,[new_symbols(definition,[spl0_292])],[avatar_definition]) ).
fof(f34375,plain,
( ! [X2,X1] :
( between(extension(a,e,X1,X2),c,d)
| e = extension(a,e,X1,X2) )
| ~ spl0_292 ),
inference(avatar_component_clause,[],[f34374]) ).
fof(f34377,definition,
( spl0_293
<=> ! [X0] :
( between(a,c,X0)
| ~ between(c,X0,d) ) ),
introduced(definition,[new_symbols(definition,[spl0_293])],[avatar_definition]) ).
fof(f34378,plain,
( ! [X0] :
( ~ between(c,X0,d)
| between(a,c,X0) )
| ~ spl0_293 ),
inference(avatar_component_clause,[],[f34377]) ).
fof(f34379,plain,
( spl0_292
| spl0_293
| ~ spl0_53
| ~ spl0_54
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f34356,f3014,f2574,f2569,f34377,f34374]) ).
fof(f35064,plain,
( ! [X2,X0,X1] :
( between(a,d,X0)
| ~ between(d,X0,c)
| e = extension(a,e,X1,X2) )
| ~ spl0_58
| ~ spl0_292 ),
inference(resolution,[],[f24740,f34375]) ).
fof(f35098,definition,
( spl0_295
<=> ! [X2,X1] : e = extension(a,e,X1,X2) ),
introduced(definition,[new_symbols(definition,[spl0_295])],[avatar_definition]) ).
fof(f35099,plain,
( ! [X2,X1] : e = extension(a,e,X1,X2)
| ~ spl0_295 ),
inference(avatar_component_clause,[],[f35098]) ).
fof(f35101,definition,
( spl0_296
<=> ! [X0] :
( between(a,d,X0)
| ~ between(d,X0,c) ) ),
introduced(definition,[new_symbols(definition,[spl0_296])],[avatar_definition]) ).
fof(f35102,plain,
( ! [X0] :
( ~ between(d,X0,c)
| between(a,d,X0) )
| ~ spl0_296 ),
inference(avatar_component_clause,[],[f35101]) ).
fof(f35162,plain,
( between(a,c,d)
| ~ spl0_293 ),
inference(resolution,[],[f34378,f28]) ).
fof(f35180,plain,
( $false
| ~ spl0_293 ),
inference(forward_subsumption_resolution,[],[f35162,f23]) ).
fof(f35181,plain,
~ spl0_293,
inference(avatar_contradiction_clause,[],[f35180]) ).
fof(f35183,plain,
( spl0_295
| spl0_296
| ~ spl0_58
| ~ spl0_292 ),
inference(avatar_split_clause,[],[f35064,f34374,f3019,f35101,f35098]) ).
fof(f35710,plain,
( ! [X0,X1] : equidistant(X0,X1,e,e)
| ~ spl0_295 ),
inference(superposition,[],[f103,f35099]) ).
fof(f35923,plain,
( ! [X0,X1] : X0 = X1
| ~ spl0_295 ),
inference(resolution,[],[f35710,f5]) ).
fof(f39484,plain,
( ! [X0] : c != X0
| spl0_92
| ~ spl0_295 ),
inference(superposition,[],[f9667,f35923]) ).
fof(f43689,plain,
( $false
| spl0_92
| ~ spl0_295 ),
inference(forward_subsumption_resolution,[],[f39484,f35923]) ).
fof(f43690,plain,
( spl0_92
| ~ spl0_295 ),
inference(avatar_contradiction_clause,[],[f43689]) ).
fof(f44038,plain,
( between(a,d,c)
| ~ spl0_296 ),
inference(resolution,[],[f35102,f28]) ).
fof(f44054,plain,
( $false
| ~ spl0_296 ),
inference(forward_subsumption_resolution,[],[f44038,f24]) ).
fof(f44055,plain,
~ spl0_296,
inference(avatar_contradiction_clause,[],[f44054]) ).
fof(f44066,plain,
( $false
| ~ spl0_36
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f2281,f6032]) ).
fof(f44067,plain,
( ~ spl0_36
| spl0_68 ),
inference(avatar_contradiction_clause,[],[f44066]) ).
fof(f44074,plain,
spl0_57,
inference(avatar_split_clause,[],[f7660,f3014]) ).
cnf(s3,plain,
( spl0_3
| spl0_5 ),
inference(sat_conversion,[],[f74]) ).
cnf(s5,plain,
~ spl0_3,
inference(sat_conversion,[],[f96]) ).
cnf(s42,plain,
~ spl0_48,
inference(sat_conversion,[],[f2426]) ).
cnf(s53,plain,
( ~ spl0_5
| spl0_36
| spl0_58 ),
inference(sat_conversion,[],[f3021]) ).
cnf(s69,plain,
( spl0_48
| ~ spl0_57
| ~ spl0_68 ),
inference(sat_conversion,[],[f6038]) ).
cnf(s78,plain,
spl0_54,
inference(sat_conversion,[],[f6849]) ).
cnf(s90,plain,
spl0_53,
inference(sat_conversion,[],[f6879]) ).
cnf(s119,plain,
~ spl0_92,
inference(sat_conversion,[],[f9907]) ).
cnf(s325,plain,
( ~ spl0_53
| ~ spl0_54
| ~ spl0_57
| spl0_292
| spl0_293 ),
inference(sat_conversion,[],[f34379]) ).
cnf(s331,plain,
~ spl0_293,
inference(sat_conversion,[],[f35181]) ).
cnf(s333,plain,
( ~ spl0_58
| ~ spl0_292
| spl0_295
| spl0_296 ),
inference(sat_conversion,[],[f35183]) ).
cnf(s465,plain,
( spl0_92
| ~ spl0_295 ),
inference(sat_conversion,[],[f43690]) ).
cnf(s631,plain,
~ spl0_296,
inference(sat_conversion,[],[f44055]) ).
cnf(s633,plain,
( ~ spl0_36
| spl0_68 ),
inference(sat_conversion,[],[f44067]) ).
cnf(s638,plain,
spl0_57,
inference(sat_conversion,[],[f44074]) ).
cnf(s808,plain,
( ~ spl0_58
| ~ spl0_292
| spl0_295 ),
inference(rat,[],[s333,s631]) ).
cnf(s813,plain,
( ~ spl0_53
| ~ spl0_54
| spl0_292 ),
inference(rat,[],[s325,s331,s638]) ).
cnf(s833,plain,
~ spl0_295,
inference(rat,[],[s465,s119]) ).
cnf(s841,plain,
spl0_292,
inference(rat,[],[s813,s90,s78]) ).
cnf(s843,plain,
~ spl0_58,
inference(rat,[],[s808,s833,s841]) ).
cnf(s848,plain,
( spl0_48
| ~ spl0_68 ),
inference(rat,[],[s69,s638]) ).
cnf(s860,plain,
( ~ spl0_5
| spl0_36 ),
inference(rat,[],[s53,s843]) ).
cnf(s863,plain,
~ spl0_68,
inference(rat,[],[s848,s42]) ).
cnf(s864,plain,
~ spl0_36,
inference(rat,[],[s633,s863]) ).
cnf(s865,plain,
~ spl0_5,
inference(rat,[],[s860,s864]) ).
cnf(s926,plain,
$false,
inference(rat,[],[s3,s865,s5]) ).
fof(f44559,plain,
$false,
inference(avatar_sat_refutation,[],[s926]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO009-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 06:33:11 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.41 Running first-order theorem proving
% 0.15/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
% 9.80/2.21 % (2468399)Input is clausal, will run a generic CNF schedule.
% 9.80/2.21 % (2468406)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3866430078:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.80/2.21 % (2468407)lrs+10_1_sil=8000:sp=occurrence:random_seed=3898310442:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.80/2.21 % (2468409)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=587370668:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.80/2.21 % (2468405)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=641138364:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.80/2.21 % (2468410)dis-21_1_sil=8000:lcm=predicate:random_seed=812057845: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)
% 9.80/2.21 % (2468404)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=1004074859:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.80/2.21 % (2468408)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4292012146:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.80/2.21 % (2468407)Refutation not found, incomplete strategy
% 9.80/2.21 % (2468407)------------------------------
% 9.80/2.21 % (2468407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.21 % (2468407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.21 % (2468407)CaDiCaL version: 2.1.3
% 9.80/2.21 % (2468407)Termination reason: Refutation not found, incomplete strategy
% 9.80/2.21 % (2468407)Time elapsed: 0.001 s
% 9.80/2.21 % (2468407)Peak memory usage: 87 MB
% 9.80/2.21 % (2468408)Instruction limit reached!
% 9.80/2.21 % (2468408)------------------------------
% 9.80/2.21 % (2468408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.21 % (2468408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.21 % (2468408)CaDiCaL version: 2.1.3
% 9.80/2.21 % (2468408)Termination reason: Instruction limit
% 9.80/2.21 % (2468408)Termination phase: Saturation
% 9.80/2.21 % (2468408)Time elapsed: 0.043 s
% 9.80/2.21 % (2468408)Peak memory usage: 87 MB
% 9.80/2.21 % (2468408)Instructions burned: 114 (million)
% 9.80/2.21 % (2468410)Instruction limit reached!
% 9.80/2.21 % (2468410)------------------------------
% 9.80/2.21 % (2468410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.21 % (2468410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.21 % (2468410)CaDiCaL version: 2.1.3
% 9.80/2.21 % (2468410)Termination reason: Instruction limit
% 9.80/2.21 % (2468410)Termination phase: Saturation
% 9.80/2.21 % (2468410)Time elapsed: 0.070 s
% 9.80/2.21 % (2468410)Peak memory usage: 88 MB
% 9.80/2.21 % (2468410)Instructions burned: 117 (million)
% 9.80/2.21 % (2468409)Instruction limit reached!
% 9.80/2.21 % (2468409)------------------------------
% 9.80/2.21 % (2468409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.21 % (2468409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.21 % (2468409)CaDiCaL version: 2.1.3
% 9.80/2.21 % (2468409)Termination reason: Instruction limit
% 9.80/2.21 % (2468409)Termination phase: Saturation
% 9.80/2.21 % (2468409)Time elapsed: 0.121 s
% 9.80/2.21 % (2468409)Peak memory usage: 89 MB
% 9.80/2.21 % (2468409)Instructions burned: 181 (million)
% 9.80/2.21 % (2468418)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=2707782470:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.80/2.21 % (2468418)Refutation not found, incomplete strategy
% 9.80/2.21 % (2468418)------------------------------
% 9.80/2.21 % (2468418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.80/2.21 % (2468418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.80/2.21 % (2468418)CaDiCaL version: 2.1.3
% 9.80/2.21 % (2468418)Termination reason: Refutation not found, incomplete strategy
% 9.80/2.21 % (2468418)Time elapsed: 0.001 s
% 9.80/2.21 % (2468418)Peak memory usage: 87 MB
% 9.80/2.21 % (2468419)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4142012750: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)
% 22.96/4.07 % (2468407)------------------------------
% 22.96/4.07 % (2468407)------------------------------
% 22.96/4.07 % (2468420)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3497222266:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 22.96/4.07 % (2468419)Instruction limit reached!
% 22.96/4.07 % (2468419)------------------------------
% 22.96/4.07 % (2468419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.96/4.07 % (2468419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.96/4.07 % (2468419)CaDiCaL version: 2.1.3
% 22.96/4.07 % (2468419)Termination reason: Instruction limit
% 22.96/4.07 % (2468419)Termination phase: Saturation
% 22.96/4.07 % (2468419)Time elapsed: 0.107 s
% 22.96/4.07 % (2468419)Peak memory usage: 89 MB
% 22.96/4.07 % (2468419)Instructions burned: 189 (million)
% 22.96/4.07 % (2468423)lrs+10_64_to=lpo:sil=8000:random_seed=1187111874:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 22.96/4.07 % (2468420)Instruction limit reached!
% 22.96/4.07 % (2468420)------------------------------
% 22.96/4.07 % (2468420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.96/4.07 % (2468420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.96/4.07 % (2468420)CaDiCaL version: 2.1.3
% 22.96/4.07 % (2468420)Termination reason: Instruction limit
% 22.96/4.07 % (2468420)Termination phase: Saturation
% 22.96/4.07 % (2468420)Time elapsed: 0.135 s
% 22.96/4.07 % (2468420)Peak memory usage: 89 MB
% 22.96/4.07 % (2468420)Instructions burned: 219 (million)
% 22.96/4.07 % (2468425)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3841613097:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 22.96/4.07 % (2468418)------------------------------
% 22.96/4.07 % (2468418)------------------------------
% 22.96/4.07 % (2468423)Instruction limit reached!
% 22.96/4.07 % (2468423)------------------------------
% 22.96/4.07 % (2468423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.96/4.07 % (2468423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.96/4.07 % (2468423)CaDiCaL version: 2.1.3
% 22.96/4.07 % (2468423)Termination reason: Instruction limit
% 22.96/4.07 % (2468423)Termination phase: Saturation
% 22.96/4.07 % (2468423)Time elapsed: 0.078 s
% 22.96/4.07 % (2468423)Peak memory usage: 88 MB
% 22.96/4.07 % (2468423)Instructions burned: 127 (million)
% 22.96/4.07 % (2468425)Instruction limit reached!
% 22.96/4.07 % (2468425)------------------------------
% 22.96/4.07 % (2468425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.96/4.07 % (2468425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.96/4.07 % (2468425)CaDiCaL version: 2.1.3
% 22.96/4.07 % (2468425)Termination reason: Instruction limit
% 22.96/4.07 % (2468425)Termination phase: Saturation
% 22.96/4.07 % (2468425)Time elapsed: 0.065 s
% 22.96/4.07 % (2468425)Peak memory usage: 88 MB
% 22.96/4.07 % (2468425)Instructions burned: 197 (million)
% 22.96/4.07 % (2468427)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4164887519:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 22.96/4.07 % (2468429)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1678459720:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 22.96/4.07 % (2468430)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=3716735805:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 22.96/4.07 % (2468430)Refutation not found, incomplete strategy
% 22.96/4.07 % (2468430)------------------------------
% 22.96/4.07 % (2468430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.96/4.07 % (2468430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.96/4.07 % (2468430)CaDiCaL version: 2.1.3
% 22.96/4.07 % (2468430)Termination reason: Refutation not found, incomplete strategy
% 22.96/4.07 % (2468430)Time elapsed: 0.001 s
% 22.96/4.07 % (2468430)Peak memory usage: 87 MB
% 22.96/4.07 % (2468431)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=150244818:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 22.96/4.07 % (2468431)Instruction limit reached!
% 22.96/4.07 % (2468431)------------------------------
% 22.96/4.07 % (2468431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.46 % (2468431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.46 % (2468431)CaDiCaL version: 2.1.3
% 32.22/5.46 % (2468431)Termination reason: Instruction limit
% 32.22/5.46 % (2468431)Termination phase: Saturation
% 32.22/5.46 % (2468431)Time elapsed: 0.035 s
% 32.22/5.46 % (2468431)Peak memory usage: 88 MB
% 32.22/5.46 % (2468431)Instructions burned: 108 (million)
% 32.22/5.46 % (2468427)Instruction limit reached!
% 32.22/5.46 % (2468427)------------------------------
% 32.22/5.46 % (2468427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.46 % (2468427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.46 % (2468427)CaDiCaL version: 2.1.3
% 32.22/5.46 % (2468427)Termination reason: Instruction limit
% 32.22/5.46 % (2468427)Termination phase: Saturation
% 32.22/5.46 % (2468427)Time elapsed: 0.101 s
% 32.22/5.46 % (2468427)Peak memory usage: 89 MB
% 32.22/5.46 % (2468427)Instructions burned: 157 (million)
% 32.22/5.46 % (2468436)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1063381667:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 32.22/5.46 % (2468437)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3454799855:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 32.22/5.46 % (2468436)Instruction limit reached!
% 32.22/5.46 % (2468436)------------------------------
% 32.22/5.46 % (2468436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.46 % (2468436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.46 % (2468436)CaDiCaL version: 2.1.3
% 32.22/5.46 % (2468436)Termination reason: Instruction limit
% 32.22/5.46 % (2468436)Termination phase: Saturation
% 32.22/5.46 % (2468436)Time elapsed: 0.083 s
% 32.22/5.46 % (2468436)Peak memory usage: 89 MB
% 32.22/5.46 % (2468436)Instructions burned: 245 (million)
% 32.22/5.46 % (2468430)------------------------------
% 32.22/5.46 % (2468430)------------------------------
% 32.22/5.46 % (2468440)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1623328678:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 32.22/5.46 % (2468440)Instruction limit reached!
% 32.22/5.46 % (2468440)------------------------------
% 32.22/5.46 % (2468440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.46 % (2468440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.46 % (2468440)CaDiCaL version: 2.1.3
% 32.22/5.46 % (2468440)Termination reason: Instruction limit
% 32.22/5.46 % (2468440)Termination phase: Saturation
% 32.22/5.46 % (2468440)Time elapsed: 0.026 s
% 32.22/5.46 % (2468440)Peak memory usage: 87 MB
% 32.22/5.46 % (2468440)Instructions burned: 140 (million)
% 32.22/5.46 % (2468441)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1247330654:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 32.22/5.46 % (2468443)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1593571741:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 32.22/5.46 % (2468443)Instruction limit reached!
% 32.22/5.46 % (2468443)------------------------------
% 32.22/5.46 % (2468443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.46 % (2468443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.46 % (2468443)CaDiCaL version: 2.1.3
% 32.22/5.46 % (2468443)Termination reason: Instruction limit
% 32.22/5.46 % (2468443)Termination phase: Saturation
% 32.22/5.46 % (2468443)Time elapsed: 0.063 s
% 32.22/5.46 % (2468443)Peak memory usage: 89 MB
% 32.22/5.46 % (2468443)Instructions burned: 192 (million)
% 32.22/5.46 % (2468446)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=805914673:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 32.22/5.46 % (2468446)Instruction limit reached!
% 32.22/5.46 % (2468446)------------------------------
% 32.22/5.46 % (2468446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.22/5.46 % (2468446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.22/5.46 % (2468446)CaDiCaL version: 2.1.3
% 32.22/5.46 % (2468446)Termination reason: Instruction limit
% 32.22/5.46 % (2468446)Termination phase: Saturation
% 32.22/5.46 % (2468446)Time elapsed: 0.087 s
% 32.22/5.46 % (2468446)Peak memory usage: 90 MB
% 32.22/5.46 % (2468446)Instructions burned: 265 (million)
% 45.97/7.36 % (2468441)Instruction limit reached!
% 45.97/7.36 % (2468441)------------------------------
% 45.97/7.36 % (2468441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.97/7.36 % (2468441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.97/7.36 % (2468441)CaDiCaL version: 2.1.3
% 45.97/7.36 % (2468441)Termination reason: Instruction limit
% 45.97/7.36 % (2468441)Termination phase: Saturation
% 45.97/7.36 % (2468441)Time elapsed: 0.287 s
% 45.97/7.36 % (2468441)Peak memory usage: 93 MB
% 45.97/7.36 % (2468441)Instructions burned: 499 (million)
% 45.97/7.36 % (2468448)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=450451133:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 45.97/7.36 % (2468449)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2414169161:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 45.97/7.36 % (2468448)Instruction limit reached!
% 45.97/7.36 % (2468448)------------------------------
% 45.97/7.36 % (2468448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.97/7.36 % (2468448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.97/7.36 % (2468448)CaDiCaL version: 2.1.3
% 45.97/7.36 % (2468448)Termination reason: Instruction limit
% 45.97/7.36 % (2468448)Termination phase: Saturation
% 45.97/7.36 % (2468448)Time elapsed: 0.056 s
% 45.97/7.36 % (2468448)Peak memory usage: 88 MB
% 45.97/7.36 % (2468448)Instructions burned: 157 (million)
% 45.97/7.36 % (2468452)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2041265625:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi)
% 45.97/7.36 % (2468452)Instruction limit reached!
% 45.97/7.36 % (2468452)------------------------------
% 45.97/7.36 % (2468452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.97/7.36 % (2468452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.97/7.36 % (2468452)CaDiCaL version: 2.1.3
% 45.97/7.36 % (2468452)Termination reason: Instruction limit
% 45.97/7.36 % (2468452)Termination phase: Saturation
% 45.97/7.36 % (2468452)Time elapsed: 0.096 s
% 45.97/7.36 % (2468452)Peak memory usage: 87 MB
% 45.97/7.36 % (2468452)Instructions burned: 541 (million)
% 45.97/7.36 % (2468454)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4225158257:i=180:bd=preordered:av=off_2983 on theBenchmark for (2983ds/180Mi)
% 45.97/7.36 % (2468454)Instruction limit reached!
% 45.97/7.36 % (2468454)------------------------------
% 45.97/7.36 % (2468454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.97/7.36 % (2468454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.97/7.36 % (2468454)CaDiCaL version: 2.1.3
% 45.97/7.36 % (2468454)Termination reason: Instruction limit
% 45.97/7.36 % (2468454)Termination phase: Saturation
% 45.97/7.36 % (2468454)Time elapsed: 0.058 s
% 45.97/7.36 % (2468454)Peak memory usage: 88 MB
% 45.97/7.36 % (2468454)Instructions burned: 183 (million)
% 45.97/7.36 % (2468456)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2884677713:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/10307Mi)
% 45.97/7.36 % (2468429)Instruction limit reached!
% 45.97/7.36 % (2468429)------------------------------
% 45.97/7.36 % (2468429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.97/7.36 % (2468429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.97/7.36 % (2468429)CaDiCaL version: 2.1.3
% 45.97/7.36 % (2468429)Termination reason: Instruction limit
% 45.97/7.36 % (2468429)Termination phase: Saturation
% 45.97/7.36 % (2468429)Time elapsed: 2.189 s
% 45.97/7.36 % (2468429)Peak memory usage: 145 MB
% 45.97/7.36 % (2468429)Instructions burned: 3395 (million)
% 45.97/7.36 % (2468458)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3543765718:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 45.97/7.36 % (2468458)Instruction limit reached!
% 45.97/7.36 % (2468458)------------------------------
% 45.97/7.36 % (2468458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.97/7.36 % (2468458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.14 % (2468458)CaDiCaL version: 2.1.3
% 66.05/10.14 % (2468458)Termination reason: Instruction limit
% 66.05/10.14 % (2468458)Termination phase: Saturation
% 66.05/10.14 % (2468458)Time elapsed: 0.190 s
% 66.05/10.14 % (2468458)Peak memory usage: 90 MB
% 66.05/10.14 % (2468458)Instructions burned: 414 (million)
% 66.05/10.14 % (2468460)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=4137593628:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi)
% 66.05/10.14 % (2468449)Instruction limit reached!
% 66.05/10.14 % (2468449)------------------------------
% 66.05/10.14 % (2468449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.14 % (2468449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.14 % (2468449)CaDiCaL version: 2.1.3
% 66.05/10.14 % (2468449)Termination reason: Instruction limit
% 66.05/10.14 % (2468449)Termination phase: Saturation
% 66.05/10.14 % (2468449)Time elapsed: 1.895 s
% 66.05/10.14 % (2468449)Peak memory usage: 148 MB
% 66.05/10.14 % (2468449)Instructions burned: 3256 (million)
% 66.05/10.14 % (2468462)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3466972378:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2965 on theBenchmark for (2965ds/303Mi)
% 66.05/10.14 % (2468462)Instruction limit reached!
% 66.05/10.14 % (2468462)------------------------------
% 66.05/10.14 % (2468462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.14 % (2468462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.14 % (2468462)CaDiCaL version: 2.1.3
% 66.05/10.14 % (2468462)Termination reason: Instruction limit
% 66.05/10.14 % (2468462)Termination phase: Saturation
% 66.05/10.14 % (2468462)Time elapsed: 0.110 s
% 66.05/10.14 % (2468462)Peak memory usage: 88 MB
% 66.05/10.14 % (2468462)Instructions burned: 305 (million)
% 66.05/10.14 % (2468464)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=232084298:st=4:i=720:sd=3:fsr=off:ss=axioms_2963 on theBenchmark for (2963ds/720Mi)
% 66.05/10.14 % (2468437)Instruction limit reached!
% 66.05/10.14 % (2468437)------------------------------
% 66.05/10.14 % (2468437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.14 % (2468437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.14 % (2468437)CaDiCaL version: 2.1.3
% 66.05/10.14 % (2468437)Termination reason: Instruction limit
% 66.05/10.14 % (2468437)Termination phase: Saturation
% 66.05/10.14 % (2468437)Time elapsed: 3.144 s
% 66.05/10.14 % (2468437)Peak memory usage: 148 MB
% 66.05/10.14 % (2468437)Instructions burned: 5209 (million)
% 66.05/10.14 % (2468466)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=901387912:i=598:bs=on:bd=preordered:av=off:ss=axioms_2959 on theBenchmark for (2959ds/598Mi)
% 66.05/10.14 % (2468464)Instruction limit reached!
% 66.05/10.14 % (2468464)------------------------------
% 66.05/10.14 % (2468464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.14 % (2468464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.14 % (2468464)CaDiCaL version: 2.1.3
% 66.05/10.14 % (2468464)Termination reason: Instruction limit
% 66.05/10.14 % (2468464)Termination phase: Saturation
% 66.05/10.14 % (2468464)Time elapsed: 0.408 s
% 66.05/10.14 % (2468464)Peak memory usage: 95 MB
% 66.05/10.14 % (2468464)Instructions burned: 721 (million)
% 66.05/10.14 % (2468468)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=517757222:i=2989:sd=3:ss=axioms:sgt=60_2958 on theBenchmark for (2958ds/2989Mi)
% 66.05/10.14 % (2468466)Instruction limit reached!
% 66.05/10.14 % (2468466)------------------------------
% 66.05/10.14 % (2468466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.14 % (2468466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.14 % (2468466)CaDiCaL version: 2.1.3
% 66.05/10.14 % (2468466)Termination reason: Instruction limit
% 66.05/10.14 % (2468466)Termination phase: Saturation
% 66.05/10.14 % (2468466)Time elapsed: 0.312 s
% 66.05/10.14 % (2468466)Peak memory usage: 88 MB
% 66.05/10.14 % (2468466)Instructions burned: 600 (million)
% 66.05/10.14 % (2468470)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=2548083798:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2955 on theBenchmark for (2955ds/1997Mi)
% 88.63/13.37 % (2468456)Instruction limit reached!
% 88.63/13.37 % (2468456)------------------------------
% 88.63/13.37 % (2468456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.63/13.37 % (2468456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.63/13.37 % (2468456)CaDiCaL version: 2.1.3
% 88.63/13.37 % (2468456)Termination reason: Instruction limit
% 88.63/13.37 % (2468456)Termination phase: Saturation
% 88.63/13.37 % (2468456)Time elapsed: 3.314 s
% 88.63/13.37 % (2468456)Peak memory usage: 161 MB
% 88.63/13.37 % (2468456)Instructions burned: 10310 (million)
% 88.63/13.37 % (2468472)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2977872888:i=2088:bd=preordered:av=off_2947 on theBenchmark for (2947ds/2088Mi)
% 88.63/13.37 % (2468468)Instruction limit reached!
% 88.63/13.37 % (2468468)------------------------------
% 88.63/13.37 % (2468468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.63/13.37 % (2468468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.63/13.37 % (2468468)CaDiCaL version: 2.1.3
% 88.63/13.37 % (2468468)Termination reason: Instruction limit
% 88.63/13.37 % (2468468)Termination phase: Saturation
% 88.63/13.37 % (2468468)Time elapsed: 1.466 s
% 88.63/13.37 % (2468468)Peak memory usage: 130 MB
% 88.63/13.37 % (2468468)Instructions burned: 2989 (million)
% 88.63/13.37 % (2468474)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1305197555:i=1098:nicw=on_2942 on theBenchmark for (2942ds/1098Mi)
% 88.63/13.37 % (2468470)Instruction limit reached!
% 88.63/13.37 % (2468470)------------------------------
% 88.63/13.37 % (2468470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.63/13.37 % (2468470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.63/13.37 % (2468470)CaDiCaL version: 2.1.3
% 88.63/13.37 % (2468470)Termination reason: Instruction limit
% 88.63/13.37 % (2468470)Termination phase: Saturation
% 88.63/13.37 % (2468470)Time elapsed: 1.309 s
% 88.63/13.37 % (2468470)Peak memory usage: 134 MB
% 88.63/13.37 % (2468470)Instructions burned: 1997 (million)
% 88.63/13.37 % (2468476)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3575474946:i=433:bd=preordered_2940 on theBenchmark for (2940ds/433Mi)
% 88.63/13.37 % (2468472)Instruction limit reached!
% 88.63/13.37 % (2468472)------------------------------
% 88.63/13.37 % (2468472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.63/13.37 % (2468472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.63/13.37 % (2468472)CaDiCaL version: 2.1.3
% 88.63/13.37 % (2468472)Termination reason: Instruction limit
% 88.63/13.37 % (2468472)Termination phase: Saturation
% 88.63/13.37 % (2468472)Time elapsed: 0.728 s
% 88.63/13.37 % (2468472)Peak memory usage: 135 MB
% 88.63/13.37 % (2468472)Instructions burned: 2089 (million)
% 88.63/13.37 % (2468478)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1272276809:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2939 on theBenchmark for (2939ds/2942Mi)
% 88.63/13.37 % (2468476)Instruction limit reached!
% 88.63/13.37 % (2468476)------------------------------
% 88.63/13.37 % (2468476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.63/13.37 % (2468476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.63/13.37 % (2468476)CaDiCaL version: 2.1.3
% 88.63/13.37 % (2468476)Termination reason: Instruction limit
% 88.63/13.37 % (2468476)Termination phase: Saturation
% 88.63/13.37 % (2468476)Time elapsed: 0.255 s
% 88.63/13.37 % (2468476)Peak memory usage: 91 MB
% 88.63/13.37 % (2468476)Instructions burned: 433 (million)
% 88.63/13.37 % (2468480)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1163674995:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2936 on theBenchmark for (2936ds/6922Mi)
% 88.63/13.37 % (2468474)Instruction limit reached!
% 88.63/13.37 % (2468474)------------------------------
% 88.63/13.37 % (2468474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.63/13.37 % (2468474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.63/13.37 % (2468474)CaDiCaL version: 2.1.3
% 88.63/13.37 % (2468474)Termination reason: Instruction limit
% 88.63/13.37 % (2468474)Termination phase: Saturation
% 102.11/15.27 % (2468474)Time elapsed: 0.602 s
% 102.11/15.27 % (2468474)Peak memory usage: 101 MB
% 102.11/15.27 % (2468474)Instructions burned: 1099 (million)
% 102.11/15.27 % (2468482)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=170028569:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2934 on theBenchmark for (2934ds/596Mi)
% 102.11/15.27 % (2468482)Instruction limit reached!
% 102.11/15.27 % (2468482)------------------------------
% 102.11/15.27 % (2468482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.11/15.27 % (2468482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.11/15.27 % (2468482)CaDiCaL version: 2.1.3
% 102.11/15.27 % (2468482)Termination reason: Instruction limit
% 102.11/15.27 % (2468482)Termination phase: Saturation
% 102.11/15.27 % (2468482)Time elapsed: 0.306 s
% 102.11/15.27 % (2468482)Peak memory usage: 92 MB
% 102.11/15.27 % (2468482)Instructions burned: 597 (million)
% 102.11/15.27 % (2468484)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3843263693:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2930 on theBenchmark for (2930ds/4123Mi)
% 102.11/15.27 % (2468478)Instruction limit reached!
% 102.11/15.27 % (2468478)------------------------------
% 102.11/15.27 % (2468478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.11/15.27 % (2468478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.11/15.27 % (2468478)CaDiCaL version: 2.1.3
% 102.11/15.27 % (2468478)Termination reason: Instruction limit
% 102.11/15.27 % (2468478)Termination phase: Saturation
% 102.11/15.27 % (2468478)Time elapsed: 0.983 s
% 102.11/15.27 % (2468478)Peak memory usage: 138 MB
% 102.11/15.27 % (2468478)Instructions burned: 2945 (million)
% 102.11/15.27 % (2468486)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1829785153:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2928 on theBenchmark for (2928ds/16411Mi)
% 102.11/15.27 % (2468460)Instruction limit reached!
% 102.11/15.27 % (2468460)------------------------------
% 102.11/15.27 % (2468460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.11/15.27 % (2468460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.11/15.27 % (2468460)CaDiCaL version: 2.1.3
% 102.11/15.27 % (2468460)Termination reason: Instruction limit
% 102.11/15.27 % (2468460)Termination phase: Saturation
% 102.11/15.27 % (2468460)Time elapsed: 4.611 s
% 102.11/15.27 % (2468460)Peak memory usage: 201 MB
% 102.11/15.27 % (2468460)Instructions burned: 8479 (million)
% 102.11/15.27 % (2468488)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3299504928:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2920 on theBenchmark for (2920ds/1670Mi)
% 102.11/15.27 % (2468480)Instruction limit reached!
% 102.11/15.27 % (2468480)------------------------------
% 102.11/15.27 % (2468480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.11/15.27 % (2468480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.11/15.27 % (2468480)CaDiCaL version: 2.1.3
% 102.11/15.27 % (2468480)Termination reason: Instruction limit
% 102.11/15.27 % (2468480)Termination phase: Saturation
% 102.11/15.27 % (2468480)Time elapsed: 2.325 s
% 102.11/15.27 % (2468480)Peak memory usage: 187 MB
% 102.11/15.27 % (2468480)Instructions burned: 6931 (million)
% 102.11/15.27 % (2468490)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3991019499:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2912 on theBenchmark for (2912ds/1722Mi)
% 102.11/15.27 % (2468488)Instruction limit reached!
% 102.11/15.27 % (2468488)------------------------------
% 102.11/15.27 % (2468488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.11/15.27 % (2468488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.11/15.27 % (2468488)CaDiCaL version: 2.1.3
% 102.11/15.27 % (2468488)Termination reason: Instruction limit
% 102.11/15.27 % (2468488)Termination phase: Saturation
% 102.11/15.27 % (2468488)Time elapsed: 1.056 s
% 102.11/15.27 % (2468488)Peak memory usage: 135 MB
% 102.11/15.27 % (2468488)Instructions burned: 1670 (million)
% 102.11/15.27 % (2468492)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=4198806834:cts=off:cond=on:i=9530:bs=on:fsd=on_2908 on theBenchmark for (2908ds/9530Mi)
% 124.47/18.44 % (2468484)Instruction limit reached!
% 124.47/18.44 % (2468484)------------------------------
% 124.47/18.44 % (2468484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.47/18.44 % (2468484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.47/18.44 % (2468484)CaDiCaL version: 2.1.3
% 124.47/18.44 % (2468484)Termination reason: Instruction limit
% 124.47/18.44 % (2468484)Termination phase: Saturation
% 124.47/18.44 % (2468484)Time elapsed: 2.281 s
% 124.47/18.44 % (2468484)Peak memory usage: 157 MB
% 124.47/18.44 % (2468484)Instructions burned: 4123 (million)
% 124.47/18.44 % (2468490)Instruction limit reached!
% 124.47/18.44 % (2468490)------------------------------
% 124.47/18.44 % (2468490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.47/18.44 % (2468490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.47/18.44 % (2468490)CaDiCaL version: 2.1.3
% 124.47/18.44 % (2468490)Termination reason: Instruction limit
% 124.47/18.44 % (2468490)Termination phase: Saturation
% 124.47/18.44 % (2468490)Time elapsed: 0.577 s
% 124.47/18.44 % (2468490)Peak memory usage: 130 MB
% 124.47/18.44 % (2468490)Instructions burned: 1725 (million)
% 124.47/18.44 % (2468494)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=205416246:st=2:i=4495:sd=10:ss=included_2906 on theBenchmark for (2906ds/4495Mi)
% 124.47/18.44 % (2468495)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=3480019186:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2905 on theBenchmark for (2905ds/4920Mi)
% 124.47/18.44 % (2468494)Refutation not found, incomplete strategy
% 124.47/18.44 % (2468494)------------------------------
% 124.47/18.44 % (2468494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.47/18.44 % (2468494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.47/18.44 % (2468494)CaDiCaL version: 2.1.3
% 124.47/18.44 % (2468494)Termination reason: Refutation not found, incomplete strategy
% 124.47/18.44 % (2468494)Time elapsed: 0.586 s
% 124.47/18.44 % (2468494)Peak memory usage: 127 MB
% 124.47/18.44 % (2468494)Instructions burned: 894 (million)
% 124.47/18.44 % (2468494)------------------------------
% 124.47/18.44 % (2468494)------------------------------
% 124.47/18.44 % (2468498)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=3636828926:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2896 on theBenchmark for (2896ds/2083Mi)
% 124.47/18.44 % (2468495)Instruction limit reached!
% 124.47/18.44 % (2468495)------------------------------
% 124.47/18.44 % (2468495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.47/18.44 % (2468495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.47/18.44 % (2468495)CaDiCaL version: 2.1.3
% 124.47/18.44 % (2468495)Termination reason: Instruction limit
% 124.47/18.44 % (2468495)Termination phase: Saturation
% 124.47/18.44 % (2468495)Time elapsed: 1.468 s
% 124.47/18.44 % (2468495)Peak memory usage: 142 MB
% 124.47/18.44 % (2468495)Instructions burned: 4922 (million)
% 124.47/18.44 % (2468500)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2586575076:i=4629:av=off:gsp=on_2890 on theBenchmark for (2890ds/4629Mi)
% 124.47/18.44 % (2468498)Instruction limit reached!
% 124.47/18.44 % (2468498)------------------------------
% 124.47/18.44 % (2468498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.47/18.44 % (2468498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.47/18.44 % (2468498)CaDiCaL version: 2.1.3
% 124.47/18.44 % (2468498)Termination reason: Instruction limit
% 124.47/18.44 % (2468498)Termination phase: Saturation
% 124.47/18.44 % (2468498)Time elapsed: 1.265 s
% 124.47/18.44 % (2468498)Peak memory usage: 132 MB
% 124.47/18.44 % (2468498)Instructions burned: 2084 (million)
% 124.47/18.44 % (2468502)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2620361150:i=1258:av=off_2882 on theBenchmark for (2882ds/1258Mi)
% 124.47/18.44 % (2468502)Instruction limit reached!
% 124.47/18.44 % (2468502)------------------------------
% 124.47/18.44 % (2468502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 124.47/18.44 % (2468502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 124.47/18.44 % (2468502)CaDiCaL version: 2.1.3
% 141.82/20.88 % (2468502)Termination reason: Instruction limit
% 141.82/20.88 % (2468502)Termination phase: Saturation
% 141.82/20.88 % (2468502)Time elapsed: 0.677 s
% 141.82/20.88 % (2468502)Peak memory usage: 98 MB
% 141.82/20.88 % (2468502)Instructions burned: 1259 (million)
% 141.82/20.88 % (2468500)Instruction limit reached!
% 141.82/20.88 % (2468500)------------------------------
% 141.82/20.88 % (2468500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.82/20.88 % (2468500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.82/20.88 % (2468500)CaDiCaL version: 2.1.3
% 141.82/20.88 % (2468500)Termination reason: Instruction limit
% 141.82/20.88 % (2468500)Termination phase: Saturation
% 141.82/20.88 % (2468500)Time elapsed: 1.471 s
% 141.82/20.88 % (2468500)Peak memory usage: 149 MB
% 141.82/20.88 % (2468500)Instructions burned: 4631 (million)
% 141.82/20.88 % (2468505)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=782655506:i=1325:sd=2:ss=axioms:sgt=16_2874 on theBenchmark for (2874ds/1325Mi)
% 141.82/20.88 % (2468504)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4178669548:i=7343:av=off:ss=included_2874 on theBenchmark for (2874ds/7343Mi)
% 141.82/20.88 % (2468505)Instruction limit reached!
% 141.82/20.88 % (2468505)------------------------------
% 141.82/20.88 % (2468505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.82/20.88 % (2468505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.82/20.88 % (2468505)CaDiCaL version: 2.1.3
% 141.82/20.88 % (2468505)Termination reason: Instruction limit
% 141.82/20.88 % (2468505)Termination phase: Saturation
% 141.82/20.88 % (2468505)Time elapsed: 0.234 s
% 141.82/20.88 % (2468505)Peak memory usage: 87 MB
% 141.82/20.88 % (2468505)Instructions burned: 1327 (million)
% 141.82/20.88 % (2468508)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=256613633:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2871 on theBenchmark for (2871ds/2646Mi)
% 141.82/20.88 % (2468504)Refutation not found, incomplete strategy
% 141.82/20.88 % (2468504)------------------------------
% 141.82/20.88 % (2468504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.82/20.88 % (2468504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.82/20.88 % (2468504)CaDiCaL version: 2.1.3
% 141.82/20.88 % (2468504)Termination reason: Refutation not found, incomplete strategy
% 141.82/20.88 % (2468504)Time elapsed: 0.591 s
% 141.82/20.88 % (2468504)Peak memory usage: 127 MB
% 141.82/20.88 % (2468504)Instructions burned: 894 (million)
% 141.82/20.88 % (2468504)------------------------------
% 141.82/20.88 % (2468504)------------------------------
% 141.82/20.88 % (2468510)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3409686481:i=1489:sd=2:ep=R:ss=axioms_2865 on theBenchmark for (2865ds/1489Mi)
% 141.82/20.88 % (2468508)Instruction limit reached!
% 141.82/20.88 % (2468508)------------------------------
% 141.82/20.88 % (2468508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.82/20.88 % (2468508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.82/20.88 % (2468508)CaDiCaL version: 2.1.3
% 141.82/20.88 % (2468508)Termination reason: Instruction limit
% 141.82/20.88 % (2468508)Termination phase: Saturation
% 141.82/20.88 % (2468508)Time elapsed: 0.835 s
% 141.82/20.88 % (2468508)Peak memory usage: 131 MB
% 141.82/20.88 % (2468508)Instructions burned: 2649 (million)
% 141.82/20.88 % (2468512)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=331729361:i=1503_2862 on theBenchmark for (2862ds/1503Mi)
% 141.82/20.88 % (2468512)Instruction limit reached!
% 141.82/20.88 % (2468512)------------------------------
% 141.82/20.88 % (2468512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.82/20.88 % (2468512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.82/20.88 % (2468512)CaDiCaL version: 2.1.3
% 141.82/20.88 % (2468512)Termination reason: Instruction limit
% 141.82/20.88 % (2468512)Termination phase: Saturation
% 141.82/20.88 % (2468512)Time elapsed: 0.509 s
% 141.82/20.88 % (2468512)Peak memory usage: 133 MB
% 141.82/20.88 % (2468512)Instructions burned: 1505 (million)
% 141.82/20.88 % (2468510)Instruction limit reached!
% 141.82/20.88 % (2468510)------------------------------
% 141.82/20.88 % (2468510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.82/20.88 % (2468510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.65/23.12 % (2468510)CaDiCaL version: 2.1.3
% 157.65/23.12 % (2468510)Termination reason: Instruction limit
% 157.65/23.12 % (2468510)Termination phase: Saturation
% 157.65/23.12 % (2468510)Time elapsed: 0.804 s
% 157.65/23.12 % (2468510)Peak memory usage: 127 MB
% 157.65/23.12 % (2468510)Instructions burned: 1491 (million)
% 157.65/23.12 % (2468515)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2105936149:i=13942:kws=frequency_2856 on theBenchmark for (2856ds/13942Mi)
% 157.65/23.12 % (2468516)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=3387246331:i=3604:fsr=off:er=filter_2855 on theBenchmark for (2855ds/3604Mi)
% 157.65/23.12 % (2468492)Instruction limit reached!
% 157.65/23.12 % (2468492)------------------------------
% 157.65/23.12 % (2468492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.65/23.12 % (2468492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.65/23.12 % (2468492)CaDiCaL version: 2.1.3
% 157.65/23.12 % (2468492)Termination reason: Instruction limit
% 157.65/23.12 % (2468492)Termination phase: Saturation
% 157.65/23.12 % (2468492)Time elapsed: 5.569 s
% 157.65/23.12 % (2468492)Peak memory usage: 159 MB
% 157.65/23.12 % (2468492)Instructions burned: 9530 (million)
% 157.65/23.12 % (2468519)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3350714810:i=1876:sd=1:ss=included:sgt=32_2851 on theBenchmark for (2851ds/1876Mi)
% 157.65/23.12 % (2468519)Instruction limit reached!
% 157.65/23.12 % (2468519)------------------------------
% 157.65/23.12 % (2468519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.65/23.12 % (2468519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.65/23.12 % (2468519)CaDiCaL version: 2.1.3
% 157.65/23.12 % (2468519)Termination reason: Instruction limit
% 157.65/23.12 % (2468519)Termination phase: Saturation
% 157.65/23.12 % (2468519)Time elapsed: 1.234 s
% 157.65/23.12 % (2468519)Peak memory usage: 135 MB
% 157.65/23.12 % (2468519)Instructions burned: 1876 (million)
% 157.65/23.12 % (2468521)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3301509171:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2837 on theBenchmark for (2837ds/1932Mi)
% 157.65/23.12 % (2468516)Instruction limit reached!
% 157.65/23.12 % (2468516)------------------------------
% 157.65/23.12 % (2468516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.65/23.12 % (2468516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.65/23.12 % (2468516)CaDiCaL version: 2.1.3
% 157.65/23.12 % (2468516)Termination reason: Instruction limit
% 157.65/23.12 % (2468516)Termination phase: Saturation
% 157.65/23.12 % (2468516)Time elapsed: 2.071 s
% 157.65/23.12 % (2468516)Peak memory usage: 157 MB
% 157.65/23.12 % (2468516)Instructions burned: 3604 (million)
% 157.65/23.12 % (2468523)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=2281676500:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2833 on theBenchmark for (2833ds/1980Mi)
% 157.65/23.12 % (2468521)Refutation not found, incomplete strategy
% 157.65/23.12 % (2468521)------------------------------
% 157.65/23.12 % (2468521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.65/23.12 % (2468521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.65/23.12 % (2468521)CaDiCaL version: 2.1.3
% 157.65/23.12 % (2468521)Termination reason: Refutation not found, incomplete strategy
% 157.65/23.12 % (2468521)Time elapsed: 0.591 s
% 157.65/23.12 % (2468521)Peak memory usage: 127 MB
% 157.65/23.12 % (2468521)Instructions burned: 894 (million)
% 157.65/23.12 % (2468521)------------------------------
% 157.65/23.12 % (2468521)------------------------------
% 157.65/23.12 % (2468525)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=225935766:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2827 on theBenchmark for (2827ds/3902Mi)
% 157.65/23.12 % (2468486)Instruction limit reached!
% 157.65/23.12 % (2468486)------------------------------
% 157.65/23.12 % (2468486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.65/23.12 % (2468486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468486)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468486)Termination reason: Instruction limit
% 94.28/24.84 % (2468486)Termination phase: Saturation
% 94.28/24.84 % (2468486)Time elapsed: 10.329 s
% 94.28/24.84 % (2468486)Peak memory usage: 202 MB
% 94.28/24.84 % (2468486)Instructions burned: 16412 (million)
% 94.28/24.84 % (2468527)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2174420523:avsq=on:i=3916:aac=none:amm=off_2823 on theBenchmark for (2823ds/3916Mi)
% 94.28/24.84 % (2468525)Refutation not found, incomplete strategy
% 94.28/24.84 % (2468525)------------------------------
% 94.28/24.84 % (2468525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468525)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468525)Termination reason: Refutation not found, incomplete strategy
% 94.28/24.84 % (2468525)Time elapsed: 0.580 s
% 94.28/24.84 % (2468525)Peak memory usage: 127 MB
% 94.28/24.84 % (2468525)Instructions burned: 888 (million)
% 94.28/24.84 % (2468523)Instruction limit reached!
% 94.28/24.84 % (2468523)------------------------------
% 94.28/24.84 % (2468523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468523)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468523)Termination reason: Instruction limit
% 94.28/24.84 % (2468523)Termination phase: Saturation
% 94.28/24.84 % (2468523)Time elapsed: 1.276 s
% 94.28/24.84 % (2468523)Peak memory usage: 135 MB
% 94.28/24.84 % (2468523)Instructions burned: 1980 (million)
% 94.28/24.84 % (2468525)------------------------------
% 94.28/24.84 % (2468525)------------------------------
% 94.28/24.84 % (2468529)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3231490530:cond=on:i=3940:av=off:er=known_2819 on theBenchmark for (2819ds/3940Mi)
% 94.28/24.84 % (2468531)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2563358281:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2818 on theBenchmark for (2818ds/3980Mi)
% 94.28/24.84 % (2468515)Instruction limit reached!
% 94.28/24.84 % (2468515)------------------------------
% 94.28/24.84 % (2468515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468515)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468515)Termination reason: Instruction limit
% 94.28/24.84 % (2468515)Termination phase: Saturation
% 94.28/24.84 % (2468515)Time elapsed: 4.624 s
% 94.28/24.84 % (2468515)Peak memory usage: 210 MB
% 94.28/24.84 % (2468515)Instructions burned: 13947 (million)
% 94.28/24.84 % (2468533)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=1889509515:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2808 on theBenchmark for (2808ds/2087Mi)
% 94.28/24.84 % (2468533)Instruction limit reached!
% 94.28/24.84 % (2468533)------------------------------
% 94.28/24.84 % (2468533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468533)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468533)Termination reason: Instruction limit
% 94.28/24.84 % (2468533)Termination phase: Saturation
% 94.28/24.84 % (2468533)Time elapsed: 0.752 s
% 94.28/24.84 % (2468533)Peak memory usage: 137 MB
% 94.28/24.84 % (2468533)Instructions burned: 2090 (million)
% 94.28/24.84 % (2468527)Instruction limit reached!
% 94.28/24.84 % (2468527)------------------------------
% 94.28/24.84 % (2468527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468527)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468527)Termination reason: Instruction limit
% 94.28/24.84 % (2468527)Termination phase: Saturation
% 94.28/24.84 % (2468527)Time elapsed: 2.209 s
% 94.28/24.84 % (2468527)Peak memory usage: 107 MB
% 94.28/24.84 % (2468527)Instructions burned: 3919 (million)
% 94.28/24.84 % (2468535)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1953528000:cts=off:cond=on:i=4272:bs=on:fsd=on_2800 on theBenchmark for (2800ds/4272Mi)
% 94.28/24.84 % (2468536)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=777712354:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2800 on theBenchmark for (2800ds/2197Mi)
% 94.28/24.84 % (2468529)Instruction limit reached!
% 94.28/24.84 % (2468529)------------------------------
% 94.28/24.84 % (2468529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468529)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468529)Termination reason: Instruction limit
% 94.28/24.84 % (2468529)Termination phase: Saturation
% 94.28/24.84 % (2468529)Time elapsed: 2.299 s
% 94.28/24.84 % (2468529)Peak memory usage: 150 MB
% 94.28/24.84 % (2468529)Instructions burned: 3941 (million)
% 94.28/24.84 % (2468539)dis+21_1_sil=8000:spb=goal_then_units:random_seed=26135425:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2795 on theBenchmark for (2795ds/6508Mi)
% 94.28/24.84 % (2468531)Instruction limit reached!
% 94.28/24.84 % (2468531)------------------------------
% 94.28/24.84 % (2468531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468531)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468531)Termination reason: Instruction limit
% 94.28/24.84 % (2468531)Termination phase: Saturation
% 94.28/24.84 % (2468531)Time elapsed: 2.464 s
% 94.28/24.84 % (2468531)Peak memory usage: 152 MB
% 94.28/24.84 % (2468531)Instructions burned: 3981 (million)
% 94.28/24.84 % (2468541)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=682206027:i=2330:fgj=on:av=off:fsr=off_2792 on theBenchmark for (2792ds/2330Mi)
% 94.28/24.84 % (2468536)Instruction limit reached!
% 94.28/24.84 % (2468536)------------------------------
% 94.28/24.84 % (2468536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468536)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468536)Termination reason: Instruction limit
% 94.28/24.84 % (2468536)Termination phase: Saturation
% 94.28/24.84 % (2468536)Time elapsed: 1.268 s
% 94.28/24.84 % (2468536)Peak memory usage: 139 MB
% 94.28/24.84 % (2468536)Instructions burned: 2197 (million)
% 94.28/24.84 % (2468535)Instruction limit reached!
% 94.28/24.84 % (2468535)------------------------------
% 94.28/24.84 % (2468535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468535)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468535)Termination reason: Instruction limit
% 94.28/24.84 % (2468535)Termination phase: Saturation
% 94.28/24.84 % (2468535)Time elapsed: 1.450 s
% 94.28/24.84 % (2468535)Peak memory usage: 143 MB
% 94.28/24.84 % (2468535)Instructions burned: 4272 (million)
% 94.28/24.84 % (2468543)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=221698840:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2786 on theBenchmark for (2786ds/7592Mi)
% 94.28/24.84 % (2468544)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=764052970:i=2693:kws=precedence:ins=1:av=off_2785 on theBenchmark for (2785ds/2693Mi)
% 94.28/24.84 % (2468541)Instruction limit reached!
% 94.28/24.84 % (2468541)------------------------------
% 94.28/24.84 % (2468541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468541)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468541)Termination reason: Instruction limit
% 94.28/24.84 % (2468541)Termination phase: Saturation
% 94.28/24.84 % (2468541)Time elapsed: 1.298 s
% 94.28/24.84 % (2468541)Peak memory usage: 132 MB
% 94.28/24.84 % (2468541)Instructions burned: 2333 (million)
% 94.28/24.84 % (2468544)Instruction limit reached!
% 94.28/24.84 % (2468544)------------------------------
% 94.28/24.84 % (2468544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468544)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468544)Termination reason: Instruction limit
% 94.28/24.84 % (2468544)Termination phase: Saturation
% 94.28/24.84 % (2468544)Time elapsed: 0.700 s
% 94.28/24.84 % (2468544)Peak memory usage: 130 MB
% 94.28/24.84 % (2468544)Instructions burned: 2695 (million)
% 94.28/24.84 % (2468547)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2503307689:i=28651:sd=4:ss=included:sgt=64_2777 on theBenchmark for (2777ds/28651Mi)
% 94.28/24.84 % (2468548)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=2577737522:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2777 on theBenchmark for (2777ds/2700Mi)
% 94.28/24.84 % (2468548)Instruction limit reached!
% 94.28/24.84 % (2468548)------------------------------
% 94.28/24.84 % (2468548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.28/24.84 % (2468548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.28/24.84 % (2468548)CaDiCaL version: 2.1.3
% 94.28/24.84 % (2468548)Termination reason: Instruction limit
% 94.28/24.84 % (2468548)Termination phase: Saturation
% 94.28/24.84 % (2468548)Time elapsed: 0.980 s
% 94.28/24.84 % (2468548)Peak memory usage: 137 MB
% 94.28/24.84 % (2468548)Instructions burned: 2701 (million)
% 94.28/24.84 % (2468551)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=3652428290:i=3196:nm=4_2766 on theBenchmark for (2766ds/3196Mi)
% 94.28/24.84 % (2468539)First to succeed.
% 94.28/24.84 % (2468539)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2468399"
% 94.28/24.84 % (2468539)Refutation found. Thanks to Tanya!
% 94.28/24.84 % SZS status Unsatisfiable for theBenchmark
% 94.28/24.84 % SZS output start Proof for theBenchmark
% See solution above
% 170.34/24.96 % (2468539)------------------------------
% 170.34/24.96 % (2468539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 170.34/24.96 % (2468539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.34/24.96 % (2468539)CaDiCaL version: 2.1.3
% 170.34/24.96 % (2468539)Termination reason: Refutation
% 170.34/24.96 % (2468539)Time elapsed: 3.075 s
% 170.34/24.96 % (2468539)Peak memory usage: 112 MB
% 170.34/24.96 % (2468539)Instructions burned: 5352 (million)
% 170.34/24.96 % (2468539)------------------------------
% 170.34/24.96 % (2468539)------------------------------
% 170.34/24.96 % (2468399)Success in time 23.994 s
% 170.34/24.96 % Vampire exiting
%------------------------------------------------------------------------------