%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM075-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:11:42 PM UTC 2026
% Result : Unsatisfiable 116.62s 17.40s
% Output : Refutation 117.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 21
% Syntax : Number of formulae : 70 ( 11 unt; 3 def)
% Number of atoms : 165 ( 21 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 178 ( 83 ~; 92 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 4 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-3 aty)
% Number of variables : 63 ( 0 sgn 63 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ member(X2,X0)
| member(X2,X1)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product2) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( member(ordered_pair(X0,X2),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product3) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f125,axiom,
! [X0,X1] :
( ~ connected(X0,X1)
| subclass(cross_product(X1,X1),union(identity_relation,symmetrization_of(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',connected1) ).
fof(f126,axiom,
! [X0,X1] :
( connected(X1,X0)
| ~ subclass(cross_product(X0,X0),union(identity_relation,symmetrization_of(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',connected2) ).
fof(f134,axiom,
! [X0,X1] :
( ~ well_ordering(X0,X1)
| connected(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_ordering1) ).
fof(f135,axiom,
! [X2,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| X2 = null_class
| member(least(X0,X2),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_ordering2) ).
fof(f136,plain,
! [X2,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| null_class = X2
| member(least(X0,X2),X2) ),
inference(reorient_equations,[],[f135]) ).
fof(f138,axiom,
! [X2,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| segment(X0,X2,least(X0,X2)) = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_ordering4) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| null_class = segment(X0,X2,least(X0,X2)) ),
inference(reorient_equations,[],[f138]) ).
fof(f141,axiom,
! [X0,X1] :
( ~ connected(X0,X1)
| not_well_ordering(X0,X1) != null_class
| well_ordering(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_ordering6) ).
fof(f142,plain,
! [X0,X1] :
( well_ordering(X0,X1)
| null_class != not_well_ordering(X0,X1)
| ~ connected(X0,X1) ),
inference(reorient_equations,[],[f141]) ).
fof(f143,axiom,
! [X0,X1] :
( well_ordering(X0,X1)
| subclass(not_well_ordering(X0,X1),X1)
| ~ connected(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_ordering7) ).
fof(f144,axiom,
! [X2,X0,X1] :
( ~ member(X0,not_well_ordering(X1,X2))
| segment(X1,not_well_ordering(X1,X2),X0) != null_class
| ~ connected(X1,X2)
| well_ordering(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_ordering8) ).
fof(f145,plain,
! [X2,X0,X1] :
( well_ordering(X1,X2)
| null_class != segment(X1,not_well_ordering(X1,X2),X0)
| ~ connected(X1,X2)
| ~ member(X0,not_well_ordering(X1,X2)) ),
inference(reorient_equations,[],[f144]) ).
fof(f176,negated_conjecture,
well_ordering(xr,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_well_ordering_property6_1) ).
fof(f177,negated_conjecture,
subclass(z,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_well_ordering_property6_2) ).
fof(f178,negated_conjecture,
~ well_ordering(xr,z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_well_ordering_property6_3) ).
fof(f192,plain,
! [X0] :
( ~ subclass(X0,y)
| null_class = segment(xr,X0,least(xr,X0)) ),
inference(resolution,[],[f176,f139]) ).
fof(f194,plain,
! [X0] :
( member(least(xr,X0),X0)
| null_class = X0
| ~ subclass(X0,y) ),
inference(resolution,[],[f176,f136]) ).
fof(f195,plain,
connected(xr,y),
inference(resolution,[],[f176,f134]) ).
fof(f196,plain,
! [X0] :
( null_class != segment(xr,not_well_ordering(xr,z),X0)
| ~ connected(xr,z)
| ~ member(X0,not_well_ordering(xr,z)) ),
inference(resolution,[],[f178,f145]) ).
fof(f198,plain,
( null_class != not_well_ordering(xr,z)
| ~ connected(xr,z) ),
inference(resolution,[],[f178,f142]) ).
fof(f201,definition,
( spl0_1
<=> connected(xr,z) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f202,plain,
( connected(xr,z)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f203,plain,
( ~ connected(xr,z)
| spl0_1 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f205,definition,
( spl0_2
<=> ! [X0] :
( null_class != segment(xr,not_well_ordering(xr,z),X0)
| ~ member(X0,not_well_ordering(xr,z)) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f206,plain,
( ! [X0] :
( ~ member(X0,not_well_ordering(xr,z))
| null_class != segment(xr,not_well_ordering(xr,z),X0) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f207,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f196,f205,f201]) ).
fof(f210,plain,
( ~ subclass(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))
| spl0_1 ),
inference(resolution,[],[f203,f126]) ).
fof(f213,plain,
( ~ member(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr))),union(identity_relation,symmetrization_of(xr)))
| spl0_1 ),
inference(unit_resulting_resolution,[],[f3,f210]) ).
fof(f214,plain,
( member(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr))),cross_product(z,z))
| spl0_1 ),
inference(unit_resulting_resolution,[],[f2,f210]) ).
fof(f228,plain,
( not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr))) = ordered_pair(first(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),second(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))))
| spl0_1 ),
inference(resolution,[],[f214,f17]) ).
fof(f242,plain,
subclass(cross_product(y,y),union(identity_relation,symmetrization_of(xr))),
inference(resolution,[],[f195,f125]) ).
fof(f276,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr))),cross_product(X0,X1))
| member(first(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),X0) )
| spl0_1 ),
inference(superposition,[],[f14,f228]) ).
fof(f277,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr))),cross_product(X0,X1))
| member(second(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),X1) )
| spl0_1 ),
inference(superposition,[],[f15,f228]) ).
fof(f278,plain,
( ! [X0,X1] :
( member(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr))),cross_product(X0,X1))
| ~ member(second(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),X1)
| ~ member(first(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),X0) )
| spl0_1 ),
inference(superposition,[],[f16,f228]) ).
fof(f329,plain,
( ~ member(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr))),cross_product(y,y))
| spl0_1 ),
inference(unit_resulting_resolution,[],[f1,f213,f242]) ).
fof(f392,definition,
( spl0_5
<=> null_class = not_well_ordering(xr,z) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f394,plain,
( null_class != not_well_ordering(xr,z)
| spl0_5 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f395,plain,
( ~ spl0_1
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f198,f392,f201]) ).
fof(f416,plain,
( member(second(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),z)
| spl0_1 ),
inference(resolution,[],[f277,f214]) ).
fof(f421,plain,
( member(second(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),y)
| spl0_1 ),
inference(unit_resulting_resolution,[],[f1,f177,f416]) ).
fof(f477,plain,
( ~ member(first(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),y)
| spl0_1 ),
inference(unit_resulting_resolution,[],[f278,f329,f421]) ).
fof(f552,plain,
( member(first(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),z)
| spl0_1 ),
inference(resolution,[],[f276,f214]) ).
fof(f559,plain,
( member(first(not_subclass_element(cross_product(z,z),union(identity_relation,symmetrization_of(xr)))),y)
| spl0_1 ),
inference(unit_resulting_resolution,[],[f1,f177,f552]) ).
fof(f590,plain,
( $false
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f559,f477]) ).
fof(f591,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f590]) ).
fof(f599,plain,
( null_class != segment(xr,not_well_ordering(xr,z),least(xr,not_well_ordering(xr,z)))
| null_class = not_well_ordering(xr,z)
| ~ subclass(not_well_ordering(xr,z),y)
| ~ spl0_2 ),
inference(resolution,[],[f206,f194]) ).
fof(f602,plain,
( null_class = not_well_ordering(xr,z)
| ~ subclass(not_well_ordering(xr,z),y)
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f599,f192]) ).
fof(f606,plain,
( ~ subclass(not_well_ordering(xr,z),y)
| ~ spl0_2
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f602,f394]) ).
fof(f607,plain,
( subclass(not_well_ordering(xr,z),z)
| ~ spl0_1 ),
inference(unit_resulting_resolution,[],[f143,f178,f202]) ).
fof(f612,plain,
( ~ member(not_subclass_element(not_well_ordering(xr,z),y),y)
| ~ spl0_2
| spl0_5 ),
inference(unit_resulting_resolution,[],[f3,f606]) ).
fof(f613,plain,
( member(not_subclass_element(not_well_ordering(xr,z),y),not_well_ordering(xr,z))
| ~ spl0_2
| spl0_5 ),
inference(unit_resulting_resolution,[],[f2,f606]) ).
fof(f629,plain,
( ~ member(not_subclass_element(not_well_ordering(xr,z),y),z)
| ~ spl0_2
| spl0_5 ),
inference(unit_resulting_resolution,[],[f1,f177,f612]) ).
fof(f651,plain,
( member(not_subclass_element(not_well_ordering(xr,z),y),z)
| ~ spl0_1
| ~ spl0_2
| spl0_5 ),
inference(unit_resulting_resolution,[],[f1,f607,f613]) ).
fof(f669,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f651,f629]) ).
fof(f670,plain,
( ~ spl0_1
| ~ spl0_2
| spl0_5 ),
inference(avatar_contradiction_clause,[],[f669]) ).
cnf(s1,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f207]) ).
cnf(s3,plain,
( ~ spl0_1
| ~ spl0_5 ),
inference(sat_conversion,[],[f395]) ).
cnf(s4,plain,
spl0_1,
inference(sat_conversion,[],[f591]) ).
cnf(s5,plain,
( ~ spl0_1
| ~ spl0_2
| spl0_5 ),
inference(sat_conversion,[],[f670]) ).
cnf(s6,plain,
~ spl0_5,
inference(rat,[],[s3,s4]) ).
cnf(s7,plain,
~ spl0_2,
inference(rat,[],[s5,s4,s6]) ).
cnf(s8,plain,
$false,
inference(rat,[],[s1,s7,s4]) ).
fof(f671,plain,
$false,
inference(avatar_sat_refutation,[],[s8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM075-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 18:49:09 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 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
% 9.59/2.17 % (2665207)Input is clausal, will run a generic CNF schedule.
% 9.59/2.17 % (2665215)lrs+10_1_sil=8000:sp=occurrence:random_seed=2456128580:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.59/2.17 % (2665215)Refutation not found, incomplete strategy
% 9.59/2.17 % (2665215)------------------------------
% 9.59/2.17 % (2665215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.17 % (2665215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.17 % (2665215)CaDiCaL version: 2.1.3
% 9.59/2.17 % (2665215)Termination reason: Refutation not found, incomplete strategy
% 9.59/2.17 % (2665215)Time elapsed: 0.001 s
% 9.59/2.17 % (2665215)Peak memory usage: 88 MB
% 9.59/2.17 % (2665215)Instructions burned: 1 (million)
% 9.59/2.17 % (2665217)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=188501391:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.59/2.17 % (2665213)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=392309410:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.59/2.17 % (2665212)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=3256989889:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.59/2.17 % (2665214)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3248472051:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.59/2.17 % (2665218)dis-21_1_sil=8000:lcm=predicate:random_seed=1971239398: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.59/2.17 % (2665216)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3479914105:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.59/2.17 % (2665216)Refutation not found, incomplete strategy
% 9.59/2.17 % (2665216)------------------------------
% 9.59/2.17 % (2665216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.17 % (2665216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.17 % (2665216)CaDiCaL version: 2.1.3
% 9.59/2.17 % (2665216)Termination reason: Refutation not found, incomplete strategy
% 9.59/2.17 % (2665216)Time elapsed: 0.002 s
% 9.59/2.17 % (2665216)Peak memory usage: 88 MB
% 9.59/2.17 % (2665216)Instructions burned: 1 (million)
% 9.59/2.17 % (2665218)Instruction limit reached!
% 9.59/2.17 % (2665218)------------------------------
% 9.59/2.17 % (2665218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.17 % (2665218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.17 % (2665218)CaDiCaL version: 2.1.3
% 9.59/2.17 % (2665218)Termination reason: Instruction limit
% 9.59/2.17 % (2665218)Termination phase: Saturation
% 9.59/2.17 % (2665218)Time elapsed: 0.054 s
% 9.59/2.17 % (2665218)Peak memory usage: 89 MB
% 9.59/2.17 % (2665218)Instructions burned: 118 (million)
% 9.59/2.17 % (2665215)------------------------------
% 9.59/2.17 % (2665215)------------------------------
% 9.59/2.17 % (2665217)Instruction limit reached!
% 9.59/2.17 % (2665217)------------------------------
% 9.59/2.17 % (2665217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.17 % (2665217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.17 % (2665217)CaDiCaL version: 2.1.3
% 9.59/2.17 % (2665217)Termination reason: Instruction limit
% 9.59/2.17 % (2665217)Termination phase: Saturation
% 9.59/2.17 % (2665217)Time elapsed: 0.143 s
% 9.59/2.17 % (2665217)Peak memory usage: 90 MB
% 9.59/2.17 % (2665217)Instructions burned: 180 (million)
% 9.59/2.17 % (2665226)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=1561930876:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.59/2.17 % (2665226)Refutation not found, incomplete strategy
% 9.59/2.17 % (2665226)------------------------------
% 9.59/2.17 % (2665226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.59/2.17 % (2665226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.59/2.17 % (2665226)CaDiCaL version: 2.1.3
% 9.59/2.17 % (2665226)Termination reason: Refutation not found, incomplete strategy
% 9.59/2.17 % (2665226)Time elapsed: 0.003 s
% 9.59/2.17 % (2665226)Peak memory usage: 88 MB
% 18.82/3.55 % (2665226)Instructions burned: 2 (million)
% 18.82/3.55 % (2665227)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2756257747: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)
% 18.82/3.55 % (2665216)------------------------------
% 18.82/3.55 % (2665216)------------------------------
% 18.82/3.55 % (2665227)Instruction limit reached!
% 18.82/3.55 % (2665227)------------------------------
% 18.82/3.55 % (2665227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.55 % (2665227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.55 % (2665227)CaDiCaL version: 2.1.3
% 18.82/3.55 % (2665227)Termination reason: Instruction limit
% 18.82/3.55 % (2665227)Termination phase: Saturation
% 18.82/3.55 % (2665227)Time elapsed: 0.053 s
% 18.82/3.55 % (2665227)Peak memory usage: 91 MB
% 18.82/3.55 % (2665227)Instructions burned: 192 (million)
% 18.82/3.55 % (2665228)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2753907141:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 18.82/3.55 % (2665228)Refutation not found, incomplete strategy
% 18.82/3.55 % (2665228)------------------------------
% 18.82/3.55 % (2665228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.55 % (2665228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.55 % (2665228)CaDiCaL version: 2.1.3
% 18.82/3.55 % (2665228)Termination reason: Refutation not found, incomplete strategy
% 18.82/3.55 % (2665228)Time elapsed: 0.004 s
% 18.82/3.55 % (2665228)Peak memory usage: 88 MB
% 18.82/3.55 % (2665228)Instructions burned: 4 (million)
% 18.82/3.55 % (2665233)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2113198456:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.82/3.55 % (2665231)lrs+10_64_to=lpo:sil=8000:random_seed=2554287843:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 18.82/3.55 % (2665226)------------------------------
% 18.82/3.55 % (2665226)------------------------------
% 18.82/3.55 % (2665233)Instruction limit reached!
% 18.82/3.55 % (2665233)------------------------------
% 18.82/3.55 % (2665233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.55 % (2665233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.55 % (2665233)CaDiCaL version: 2.1.3
% 18.82/3.55 % (2665233)Termination reason: Instruction limit
% 18.82/3.55 % (2665233)Termination phase: Saturation
% 18.82/3.55 % (2665233)Time elapsed: 0.070 s
% 18.82/3.55 % (2665233)Peak memory usage: 90 MB
% 18.82/3.55 % (2665233)Instructions burned: 195 (million)
% 18.82/3.55 % (2665231)Instruction limit reached!
% 18.82/3.55 % (2665231)------------------------------
% 18.82/3.55 % (2665231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.55 % (2665231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.55 % (2665231)CaDiCaL version: 2.1.3
% 18.82/3.55 % (2665231)Termination reason: Instruction limit
% 18.82/3.55 % (2665231)Termination phase: Saturation
% 18.82/3.55 % (2665231)Time elapsed: 0.080 s
% 18.82/3.55 % (2665231)Peak memory usage: 89 MB
% 18.82/3.55 % (2665231)Instructions burned: 127 (million)
% 18.82/3.55 % (2665237)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2218679092:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 18.82/3.55 % (2665228)------------------------------
% 18.82/3.55 % (2665228)------------------------------
% 18.82/3.55 % (2665236)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=524488803:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 18.82/3.55 % (2665238)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=2716829738:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 18.82/3.55 % (2665240)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3628384951:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 18.82/3.55 % (2665236)Instruction limit reached!
% 18.82/3.55 % (2665236)------------------------------
% 18.82/3.55 % (2665236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.82/3.55 % (2665236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.82/3.55 % (2665236)CaDiCaL version: 2.1.3
% 18.82/3.55 % (2665236)Termination reason: Instruction limit
% 30.09/5.09 % (2665236)Termination phase: Saturation
% 30.09/5.09 % (2665236)Time elapsed: 0.113 s
% 30.09/5.09 % (2665236)Peak memory usage: 91 MB
% 30.09/5.09 % (2665236)Instructions burned: 157 (million)
% 30.09/5.09 % (2665238)Instruction limit reached!
% 30.09/5.09 % (2665238)------------------------------
% 30.09/5.09 % (2665238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.09/5.09 % (2665238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.09/5.09 % (2665238)CaDiCaL version: 2.1.3
% 30.09/5.09 % (2665238)Termination reason: Instruction limit
% 30.09/5.09 % (2665238)Termination phase: Saturation
% 30.09/5.09 % (2665238)Time elapsed: 0.064 s
% 30.09/5.09 % (2665238)Peak memory usage: 89 MB
% 30.09/5.09 % (2665238)Instructions burned: 107 (million)
% 30.09/5.09 % (2665240)Instruction limit reached!
% 30.09/5.09 % (2665240)------------------------------
% 30.09/5.09 % (2665240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.09/5.09 % (2665240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.09/5.09 % (2665240)CaDiCaL version: 2.1.3
% 30.09/5.09 % (2665240)Termination reason: Instruction limit
% 30.09/5.09 % (2665240)Termination phase: Saturation
% 30.09/5.09 % (2665240)Time elapsed: 0.075 s
% 30.09/5.09 % (2665240)Peak memory usage: 89 MB
% 30.09/5.09 % (2665240)Instructions burned: 107 (million)
% 30.09/5.09 % (2665244)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3829786982:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 30.09/5.09 % (2665245)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2020263119:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 30.09/5.09 % (2665246)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4218315669:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 30.09/5.09 % (2665246)Instruction limit reached!
% 30.09/5.09 % (2665246)------------------------------
% 30.09/5.09 % (2665246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.09/5.09 % (2665246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.09/5.09 % (2665246)CaDiCaL version: 2.1.3
% 30.09/5.09 % (2665246)Termination reason: Instruction limit
% 30.09/5.09 % (2665246)Termination phase: Saturation
% 30.09/5.09 % (2665246)Time elapsed: 0.052 s
% 30.09/5.09 % (2665246)Peak memory usage: 88 MB
% 30.09/5.09 % (2665246)Instructions burned: 135 (million)
% 30.09/5.09 % (2665244)Instruction limit reached!
% 30.09/5.09 % (2665244)------------------------------
% 30.09/5.09 % (2665244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.09/5.09 % (2665244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.09/5.09 % (2665244)CaDiCaL version: 2.1.3
% 30.09/5.09 % (2665244)Termination reason: Instruction limit
% 30.09/5.09 % (2665244)Termination phase: Saturation
% 30.09/5.09 % (2665244)Time elapsed: 0.159 s
% 30.09/5.09 % (2665244)Peak memory usage: 90 MB
% 30.09/5.09 % (2665244)Instructions burned: 242 (million)
% 30.09/5.09 % (2665250)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1099626877:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 30.09/5.09 % (2665251)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2738710768:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 30.09/5.09 % (2665250)Instruction limit reached!
% 30.09/5.09 % (2665250)------------------------------
% 30.09/5.09 % (2665250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.09/5.09 % (2665250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.09/5.09 % (2665250)CaDiCaL version: 2.1.3
% 30.09/5.09 % (2665250)Termination reason: Instruction limit
% 30.09/5.09 % (2665250)Termination phase: Saturation
% 30.09/5.09 % (2665250)Time elapsed: 0.191 s
% 30.09/5.09 % (2665250)Peak memory usage: 95 MB
% 30.09/5.09 % (2665250)Instructions burned: 501 (million)
% 30.09/5.09 % (2665251)Instruction limit reached!
% 30.09/5.09 % (2665251)------------------------------
% 30.09/5.09 % (2665251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.09/5.09 % (2665251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.09/5.09 % (2665251)CaDiCaL version: 2.1.3
% 30.09/5.09 % (2665251)Termination reason: Instruction limit
% 30.09/5.09 % (2665251)Termination phase: Saturation
% 30.09/5.09 % (2665251)Time elapsed: 0.109 s
% 46.06/7.39 % (2665251)Peak memory usage: 89 MB
% 46.06/7.39 % (2665251)Instructions burned: 192 (million)
% 46.06/7.39 % (2665255)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1512193740:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 46.06/7.39 % (2665254)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1455358195:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 46.06/7.39 % (2665255)Instruction limit reached!
% 46.06/7.39 % (2665255)------------------------------
% 46.06/7.39 % (2665255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.06/7.39 % (2665255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.06/7.39 % (2665255)CaDiCaL version: 2.1.3
% 46.06/7.39 % (2665255)Termination reason: Instruction limit
% 46.06/7.39 % (2665255)Termination phase: Saturation
% 46.06/7.39 % (2665255)Time elapsed: 0.060 s
% 46.06/7.39 % (2665255)Peak memory usage: 89 MB
% 46.06/7.39 % (2665255)Instructions burned: 158 (million)
% 46.06/7.39 % (2665258)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=889205072:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 46.06/7.39 % (2665254)Instruction limit reached!
% 46.06/7.39 % (2665254)------------------------------
% 46.06/7.39 % (2665254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.06/7.39 % (2665254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.06/7.39 % (2665254)CaDiCaL version: 2.1.3
% 46.06/7.39 % (2665254)Termination reason: Instruction limit
% 46.06/7.39 % (2665254)Termination phase: Saturation
% 46.06/7.39 % (2665254)Time elapsed: 0.176 s
% 46.06/7.39 % (2665254)Peak memory usage: 91 MB
% 46.06/7.39 % (2665254)Instructions burned: 265 (million)
% 46.06/7.39 % (2665260)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2429164520:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 46.06/7.39 % (2665260)Refutation not found, incomplete strategy
% 46.06/7.39 % (2665260)------------------------------
% 46.06/7.39 % (2665260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.06/7.39 % (2665260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.06/7.39 % (2665260)CaDiCaL version: 2.1.3
% 46.06/7.39 % (2665260)Termination reason: Refutation not found, incomplete strategy
% 46.06/7.39 % (2665260)Time elapsed: 0.001 s
% 46.06/7.39 % (2665260)Peak memory usage: 87 MB
% 46.06/7.39 % (2665260)Instructions burned: 1 (million)
% 46.06/7.39 % (2665260)------------------------------
% 46.06/7.39 % (2665260)------------------------------
% 46.06/7.39 % (2665262)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3009941132:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 46.06/7.39 % (2665262)Instruction limit reached!
% 46.06/7.39 % (2665262)------------------------------
% 46.06/7.39 % (2665262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.06/7.39 % (2665262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.06/7.39 % (2665262)CaDiCaL version: 2.1.3
% 46.06/7.39 % (2665262)Termination reason: Instruction limit
% 46.06/7.39 % (2665262)Termination phase: Saturation
% 46.06/7.39 % (2665262)Time elapsed: 0.103 s
% 46.06/7.39 % (2665262)Peak memory usage: 90 MB
% 46.06/7.39 % (2665262)Instructions burned: 181 (million)
% 46.06/7.39 % (2665264)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=2044914226:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi)
% 46.06/7.39 % (2665237)Instruction limit reached!
% 46.06/7.39 % (2665237)------------------------------
% 46.06/7.39 % (2665237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.06/7.39 % (2665237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.06/7.39 % (2665237)CaDiCaL version: 2.1.3
% 46.06/7.39 % (2665237)Termination reason: Instruction limit
% 46.06/7.39 % (2665237)Termination phase: Saturation
% 46.06/7.39 % (2665237)Time elapsed: 2.005 s
% 46.06/7.39 % (2665237)Peak memory usage: 150 MB
% 46.06/7.39 % (2665237)Instructions burned: 3394 (million)
% 46.06/7.39 % (2665258)Instruction limit reached!
% 46.06/7.39 % (2665258)------------------------------
% 46.06/7.39 % (2665258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.06/7.39 % (2665258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.31/10.96 % (2665258)CaDiCaL version: 2.1.3
% 71.31/10.96 % (2665258)Termination reason: Instruction limit
% 71.31/10.96 % (2665258)Termination phase: Saturation
% 71.31/10.96 % (2665258)Time elapsed: 1.130 s
% 71.31/10.96 % (2665258)Peak memory usage: 147 MB
% 71.31/10.96 % (2665258)Instructions burned: 3259 (million)
% 71.31/10.96 % (2665267)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=21263144:s2pl=no:i=8478:s2at=4:nm=6_2972 on theBenchmark for (2972ds/8478Mi)
% 71.31/10.96 % (2665266)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=2798066315:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 71.31/10.96 % (2665266)Instruction limit reached!
% 71.31/10.96 % (2665266)------------------------------
% 71.31/10.96 % (2665266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.31/10.96 % (2665266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.31/10.96 % (2665266)CaDiCaL version: 2.1.3
% 71.31/10.96 % (2665266)Termination reason: Instruction limit
% 71.31/10.96 % (2665266)Termination phase: Saturation
% 71.31/10.96 % (2665266)Time elapsed: 0.188 s
% 71.31/10.96 % (2665266)Peak memory usage: 90 MB
% 71.31/10.96 % (2665266)Instructions burned: 414 (million)
% 71.31/10.96 % (2665270)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=1041612006:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2969 on theBenchmark for (2969ds/303Mi)
% 71.31/10.96 % (2665270)Refutation not found, incomplete strategy
% 71.31/10.96 % (2665270)------------------------------
% 71.31/10.96 % (2665270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.31/10.96 % (2665270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.31/10.96 % (2665270)CaDiCaL version: 2.1.3
% 71.31/10.96 % (2665270)Termination reason: Refutation not found, incomplete strategy
% 71.31/10.96 % (2665270)Time elapsed: 0.002 s
% 71.31/10.96 % (2665270)Peak memory usage: 88 MB
% 71.31/10.96 % (2665270)Instructions burned: 1 (million)
% 71.31/10.96 % (2665270)------------------------------
% 71.31/10.96 % (2665270)------------------------------
% 71.31/10.96 % (2665272)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3122792097:st=4:i=720:sd=3:fsr=off:ss=axioms_2966 on theBenchmark for (2966ds/720Mi)
% 71.31/10.96 % (2665272)Instruction limit reached!
% 71.31/10.96 % (2665272)------------------------------
% 71.31/10.96 % (2665272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.31/10.96 % (2665272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.31/10.96 % (2665272)CaDiCaL version: 2.1.3
% 71.31/10.96 % (2665272)Termination reason: Instruction limit
% 71.31/10.96 % (2665272)Termination phase: Saturation
% 71.31/10.96 % (2665272)Time elapsed: 0.410 s
% 71.31/10.96 % (2665272)Peak memory usage: 96 MB
% 71.31/10.96 % (2665272)Instructions burned: 721 (million)
% 71.31/10.96 % (2665274)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2279915829:i=598:bs=on:bd=preordered:av=off:ss=axioms_2960 on theBenchmark for (2960ds/598Mi)
% 71.31/10.96 % (2665274)Refutation not found, incomplete strategy
% 71.31/10.96 % (2665274)------------------------------
% 71.31/10.96 % (2665274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.31/10.96 % (2665274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.31/10.96 % (2665274)CaDiCaL version: 2.1.3
% 71.31/10.96 % (2665274)Termination reason: Refutation not found, incomplete strategy
% 71.31/10.96 % (2665274)Time elapsed: 0.002 s
% 71.31/10.96 % (2665274)Peak memory usage: 87 MB
% 71.31/10.96 % (2665274)Instructions burned: 1 (million)
% 71.31/10.96 % (2665245)Instruction limit reached!
% 71.31/10.96 % (2665245)------------------------------
% 71.31/10.96 % (2665245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.31/10.96 % (2665245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.31/10.96 % (2665245)CaDiCaL version: 2.1.3
% 71.31/10.96 % (2665245)Termination reason: Instruction limit
% 71.31/10.96 % (2665245)Termination phase: Saturation
% 71.31/10.96 % (2665245)Time elapsed: 3.158 s
% 71.31/10.96 % (2665245)Peak memory usage: 153 MB
% 71.31/10.96 % (2665245)Instructions burned: 5209 (million)
% 71.31/10.96 % (2665276)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1287913078:i=2989:sd=3:ss=axioms:sgt=60_2958 on theBenchmark for (2958ds/2989Mi)
% 100.98/15.08 % (2665274)------------------------------
% 100.98/15.08 % (2665274)------------------------------
% 100.98/15.08 % (2665278)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=1919277686:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2957 on theBenchmark for (2957ds/1997Mi)
% 100.98/15.08 % (2665267)Instruction limit reached!
% 100.98/15.08 % (2665267)------------------------------
% 100.98/15.08 % (2665267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2665267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2665267)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2665267)Termination reason: Instruction limit
% 100.98/15.08 % (2665267)Termination phase: Saturation
% 100.98/15.08 % (2665267)Time elapsed: 2.693 s
% 100.98/15.08 % (2665267)Peak memory usage: 167 MB
% 100.98/15.08 % (2665267)Instructions burned: 8480 (million)
% 100.98/15.08 % (2665280)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=3185899101:i=2088:bd=preordered:av=off_2944 on theBenchmark for (2944ds/2088Mi)
% 100.98/15.08 % (2665278)Instruction limit reached!
% 100.98/15.08 % (2665278)------------------------------
% 100.98/15.08 % (2665278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2665278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2665278)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2665278)Termination reason: Instruction limit
% 100.98/15.08 % (2665278)Termination phase: Saturation
% 100.98/15.08 % (2665278)Time elapsed: 1.321 s
% 100.98/15.08 % (2665278)Peak memory usage: 137 MB
% 100.98/15.08 % (2665278)Instructions burned: 1997 (million)
% 100.98/15.08 % (2665282)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1914128692:i=1098:nicw=on_2942 on theBenchmark for (2942ds/1098Mi)
% 100.98/15.08 % (2665276)Instruction limit reached!
% 100.98/15.08 % (2665276)------------------------------
% 100.98/15.08 % (2665276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2665276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2665276)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2665276)Termination reason: Instruction limit
% 100.98/15.08 % (2665276)Termination phase: Saturation
% 100.98/15.08 % (2665276)Time elapsed: 1.856 s
% 100.98/15.08 % (2665276)Peak memory usage: 145 MB
% 100.98/15.08 % (2665276)Instructions burned: 2989 (million)
% 100.98/15.08 % (2665284)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1401249365:i=433:bd=preordered_2938 on theBenchmark for (2938ds/433Mi)
% 100.98/15.08 % (2665280)Instruction limit reached!
% 100.98/15.08 % (2665280)------------------------------
% 100.98/15.08 % (2665280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.08 % (2665280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.08 % (2665280)CaDiCaL version: 2.1.3
% 100.98/15.08 % (2665280)Termination reason: Instruction limit
% 100.98/15.08 % (2665280)Termination phase: Saturation
% 100.98/15.08 % (2665280)Time elapsed: 0.750 s
% 100.98/15.08 % (2665280)Peak memory usage: 139 MB
% 100.98/15.09 % (2665280)Instructions burned: 2090 (million)
% 100.98/15.09 % (2665286)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1077504093:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2936 on theBenchmark for (2936ds/2942Mi)
% 100.98/15.09 % (2665284)Instruction limit reached!
% 100.98/15.09 % (2665284)------------------------------
% 100.98/15.09 % (2665284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.98/15.09 % (2665284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.98/15.09 % (2665284)CaDiCaL version: 2.1.3
% 100.98/15.09 % (2665284)Termination reason: Instruction limit
% 100.98/15.09 % (2665284)Termination phase: Saturation
% 100.98/15.09 % (2665284)Time elapsed: 0.264 s
% 100.98/15.09 % (2665284)Peak memory usage: 92 MB
% 100.98/15.09 % (2665284)Instructions burned: 433 (million)
% 100.98/15.09 % (2665282)Instruction limit reached!
% 100.98/15.09 % (2665282)------------------------------
% 100.98/15.09 % (2665282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.55/16.80 % (2665282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.55/16.80 % (2665282)CaDiCaL version: 2.1.3
% 112.55/16.80 % (2665282)Termination reason: Instruction limit
% 112.55/16.80 % (2665282)Termination phase: Saturation
% 112.55/16.80 % (2665282)Time elapsed: 0.667 s
% 112.55/16.80 % (2665282)Peak memory usage: 101 MB
% 112.55/16.80 % (2665282)Instructions burned: 1099 (million)
% 112.55/16.80 % (2665288)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1695532034:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2934 on theBenchmark for (2934ds/6922Mi)
% 112.55/16.80 % (2665289)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=1315240828:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2934 on theBenchmark for (2934ds/596Mi)
% 112.55/16.80 % (2665289)Instruction limit reached!
% 112.55/16.80 % (2665289)------------------------------
% 112.55/16.80 % (2665289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.55/16.80 % (2665289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.55/16.80 % (2665289)CaDiCaL version: 2.1.3
% 112.55/16.80 % (2665289)Termination reason: Instruction limit
% 112.55/16.80 % (2665289)Termination phase: Saturation
% 112.55/16.80 % (2665289)Time elapsed: 0.321 s
% 112.55/16.80 % (2665289)Peak memory usage: 99 MB
% 112.55/16.80 % (2665289)Instructions burned: 596 (million)
% 112.55/16.80 % (2665292)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=4277992855:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2929 on theBenchmark for (2929ds/4123Mi)
% 112.55/16.80 % (2665286)Instruction limit reached!
% 112.55/16.80 % (2665286)------------------------------
% 112.55/16.80 % (2665286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.55/16.80 % (2665286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.55/16.80 % (2665286)CaDiCaL version: 2.1.3
% 112.55/16.80 % (2665286)Termination reason: Instruction limit
% 112.55/16.80 % (2665286)Termination phase: Saturation
% 112.55/16.80 % (2665286)Time elapsed: 1.123 s
% 112.55/16.80 % (2665286)Peak memory usage: 145 MB
% 112.55/16.80 % (2665286)Instructions burned: 2943 (million)
% 112.55/16.80 % (2665294)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1110430460:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2923 on theBenchmark for (2923ds/16411Mi)
% 112.55/16.80 % (2665264)Instruction limit reached!
% 112.55/16.80 % (2665264)------------------------------
% 112.55/16.80 % (2665264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.55/16.80 % (2665264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.55/16.80 % (2665264)CaDiCaL version: 2.1.3
% 112.55/16.80 % (2665264)Termination reason: Instruction limit
% 112.55/16.80 % (2665264)Termination phase: Saturation
% 112.55/16.80 % (2665264)Time elapsed: 6.544 s
% 112.55/16.80 % (2665264)Peak memory usage: 160 MB
% 112.55/16.80 % (2665264)Instructions burned: 10307 (million)
% 112.55/16.80 % (2665296)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2884956521:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2910 on theBenchmark for (2910ds/1670Mi)
% 112.55/16.80 % (2665292)Instruction limit reached!
% 112.55/16.80 % (2665292)------------------------------
% 112.55/16.80 % (2665292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.55/16.80 % (2665292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.55/16.80 % (2665292)CaDiCaL version: 2.1.3
% 112.55/16.80 % (2665292)Termination reason: Instruction limit
% 112.55/16.80 % (2665292)Termination phase: Saturation
% 112.55/16.80 % (2665292)Time elapsed: 2.587 s
% 112.55/16.80 % (2665292)Peak memory usage: 158 MB
% 112.55/16.80 % (2665292)Instructions burned: 4125 (million)
% 112.55/16.80 % (2665298)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=1352407586:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2902 on theBenchmark for (2902ds/1722Mi)
% 112.55/16.80 % (2665296)Instruction limit reached!
% 112.55/16.80 % (2665296)------------------------------
% 112.55/16.80 % (2665296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.55/16.80 % (2665296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.55/16.80 % (2665296)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665296)Termination reason: Instruction limit
% 116.62/17.40 % (2665296)Termination phase: Saturation
% 116.62/17.40 % (2665296)Time elapsed: 1.051 s
% 116.62/17.40 % (2665296)Peak memory usage: 136 MB
% 116.62/17.40 % (2665296)Instructions burned: 1670 (million)
% 116.62/17.40 % (2665300)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=136284903:cts=off:cond=on:i=9530:bs=on:fsd=on_2898 on theBenchmark for (2898ds/9530Mi)
% 116.62/17.40 % (2665288)Instruction limit reached!
% 116.62/17.40 % (2665288)------------------------------
% 116.62/17.40 % (2665288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665288)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665288)Termination reason: Instruction limit
% 116.62/17.40 % (2665288)Termination phase: Saturation
% 116.62/17.40 % (2665288)Time elapsed: 3.814 s
% 116.62/17.40 % (2665288)Peak memory usage: 184 MB
% 116.62/17.40 % (2665288)Instructions burned: 6923 (million)
% 116.62/17.40 % (2665302)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2280350547:st=2:i=4495:sd=10:ss=included_2895 on theBenchmark for (2895ds/4495Mi)
% 116.62/17.40 % (2665298)Instruction limit reached!
% 116.62/17.40 % (2665298)------------------------------
% 116.62/17.40 % (2665298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665298)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665298)Termination reason: Instruction limit
% 116.62/17.40 % (2665298)Termination phase: Saturation
% 116.62/17.40 % (2665298)Time elapsed: 1.144 s
% 116.62/17.40 % (2665298)Peak memory usage: 134 MB
% 116.62/17.40 % (2665298)Instructions burned: 1722 (million)
% 116.62/17.40 % (2665304)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=2522392719:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2890 on theBenchmark for (2890ds/4920Mi)
% 116.62/17.40 % (2665302)Instruction limit reached!
% 116.62/17.40 % (2665302)------------------------------
% 116.62/17.40 % (2665302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665302)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665302)Termination reason: Instruction limit
% 116.62/17.40 % (2665302)Termination phase: Saturation
% 116.62/17.40 % (2665302)Time elapsed: 2.590 s
% 116.62/17.40 % (2665302)Peak memory usage: 162 MB
% 116.62/17.40 % (2665302)Instructions burned: 4495 (million)
% 116.62/17.40 % (2665306)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=269830939:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2868 on theBenchmark for (2868ds/2083Mi)
% 116.62/17.40 % (2665294)Instruction limit reached!
% 116.62/17.40 % (2665294)------------------------------
% 116.62/17.40 % (2665294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665294)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665294)Termination reason: Instruction limit
% 116.62/17.40 % (2665294)Termination phase: Saturation
% 116.62/17.40 % (2665294)Time elapsed: 5.805 s
% 116.62/17.40 % (2665294)Peak memory usage: 215 MB
% 116.62/17.40 % (2665294)Instructions burned: 16411 (million)
% 116.62/17.40 % (2665308)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=3593185236:i=4629:av=off:gsp=on_2864 on theBenchmark for (2864ds/4629Mi)
% 116.62/17.40 % (2665304)Instruction limit reached!
% 116.62/17.40 % (2665304)------------------------------
% 116.62/17.40 % (2665304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665304)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665304)Termination reason: Instruction limit
% 116.62/17.40 % (2665304)Termination phase: Saturation
% 116.62/17.40 % (2665304)Time elapsed: 2.986 s
% 116.62/17.40 % (2665304)Peak memory usage: 152 MB
% 116.62/17.40 % (2665304)Instructions burned: 4921 (million)
% 116.62/17.40 % (2665310)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=791041907:i=1258:av=off_2858 on theBenchmark for (2858ds/1258Mi)
% 116.62/17.40 % (2665306)Instruction limit reached!
% 116.62/17.40 % (2665306)------------------------------
% 116.62/17.40 % (2665306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665306)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665306)Termination reason: Instruction limit
% 116.62/17.40 % (2665306)Termination phase: Saturation
% 116.62/17.40 % (2665306)Time elapsed: 1.314 s
% 116.62/17.40 % (2665306)Peak memory usage: 137 MB
% 116.62/17.40 % (2665306)Instructions burned: 2084 (million)
% 116.62/17.40 % (2665312)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=267194412:i=7343:av=off:ss=included_2853 on theBenchmark for (2853ds/7343Mi)
% 116.62/17.40 % (2665310)Instruction limit reached!
% 116.62/17.40 % (2665310)------------------------------
% 116.62/17.40 % (2665310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665310)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665310)Termination reason: Instruction limit
% 116.62/17.40 % (2665310)Termination phase: Saturation
% 116.62/17.40 % (2665310)Time elapsed: 0.691 s
% 116.62/17.40 % (2665310)Peak memory usage: 94 MB
% 116.62/17.40 % (2665310)Instructions burned: 1258 (million)
% 116.62/17.40 % (2665314)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=4054167782:i=1325:sd=2:ss=axioms:sgt=16_2850 on theBenchmark for (2850ds/1325Mi)
% 116.62/17.40 % (2665308)Instruction limit reached!
% 116.62/17.40 % (2665308)------------------------------
% 116.62/17.40 % (2665308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665314)Refutation not found, incomplete strategy
% 116.62/17.40 % (2665314)------------------------------
% 116.62/17.40 % (2665314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665308)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665308)Termination reason: Instruction limit
% 116.62/17.40 % (2665308)Termination phase: Saturation
% 116.62/17.40 % (2665308)Time elapsed: 1.480 s
% 116.62/17.40 % (2665308)Peak memory usage: 158 MB
% 116.62/17.40 % (2665314)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665308)Instructions burned: 4630 (million)
% 116.62/17.40 % (2665314)Termination reason: Refutation not found, incomplete strategy
% 116.62/17.40 % (2665314)Time elapsed: 0.002 s
% 116.62/17.40 % (2665314)Peak memory usage: 88 MB
% 116.62/17.40 % (2665314)Instructions burned: 2 (million)
% 116.62/17.40 % (2665316)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=3041495356:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2849 on theBenchmark for (2849ds/2646Mi)
% 116.62/17.40 % (2665314)------------------------------
% 116.62/17.40 % (2665314)------------------------------
% 116.62/17.40 % (2665312)Refutation not found, incomplete strategy
% 116.62/17.40 % (2665312)------------------------------
% 116.62/17.40 % (2665312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665312)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665312)Termination reason: Refutation not found, incomplete strategy
% 116.62/17.40 % (2665312)Time elapsed: 0.594 s
% 116.62/17.40 % (2665312)Peak memory usage: 127 MB
% 116.62/17.40 % (2665312)Instructions burned: 897 (million)
% 116.62/17.40 % (2665318)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1994448241:i=1489:sd=2:ep=R:ss=axioms_2846 on theBenchmark for (2846ds/1489Mi)
% 116.62/17.40 % (2665312)------------------------------
% 116.62/17.40 % (2665312)------------------------------
% 116.62/17.40 % (2665320)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=225262293:i=1503_2843 on theBenchmark for (2843ds/1503Mi)
% 116.62/17.40 % (2665300)Instruction limit reached!
% 116.62/17.40 % (2665300)------------------------------
% 116.62/17.40 % (2665300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665300)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665300)Termination reason: Instruction limit
% 116.62/17.40 % (2665300)Termination phase: Saturation
% 116.62/17.40 % (2665300)Time elapsed: 5.695 s
% 116.62/17.40 % (2665300)Peak memory usage: 164 MB
% 116.62/17.40 % (2665300)Instructions burned: 9531 (million)
% 116.62/17.40 % (2665318)Refutation not found, incomplete strategy
% 116.62/17.40 % (2665318)------------------------------
% 116.62/17.40 % (2665318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665318)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665318)Termination reason: Refutation not found, incomplete strategy
% 116.62/17.40 % (2665318)Time elapsed: 0.567 s
% 116.62/17.40 % (2665318)Peak memory usage: 127 MB
% 116.62/17.40 % (2665318)Instructions burned: 858 (million)
% 116.62/17.40 % (2665322)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3295322638:i=13942:kws=frequency_2840 on theBenchmark for (2840ds/13942Mi)
% 116.62/17.40 % (2665316)Instruction limit reached!
% 116.62/17.40 % (2665316)------------------------------
% 116.62/17.40 % (2665316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.62/17.40 % (2665316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.62/17.40 % (2665316)CaDiCaL version: 2.1.3
% 116.62/17.40 % (2665316)Termination reason: Instruction limit
% 116.62/17.40 % (2665316)Termination phase: Saturation
% 116.62/17.40 % (2665316)Time elapsed: 1.018 s
% 116.62/17.40 % (2665316)Peak memory usage: 142 MB
% 116.62/17.40 % (2665316)Instructions burned: 2646 (million)
% 116.62/17.40 % (2665318)------------------------------
% 116.62/17.40 % (2665318)------------------------------
% 116.62/17.40 % (2665324)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=3393833554:i=3604:fsr=off:er=filter_2838 on theBenchmark for (2838ds/3604Mi)
% 116.62/17.40 % (2665320)First to succeed.
% 116.62/17.40 % (2665320)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2665207"
% 116.62/17.40 % (2665325)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3038185498:i=1876:sd=1:ss=included:sgt=32_2837 on theBenchmark for (2837ds/1876Mi)
% 116.62/17.40 % (2665320)Refutation found. Thanks to Tanya!
% 116.62/17.40 % SZS status Unsatisfiable for theBenchmark
% 116.62/17.40 % SZS output start Proof for theBenchmark
% See solution above
% 117.60/17.49 % (2665320)------------------------------
% 117.60/17.49 % (2665320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.60/17.49 % (2665320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.60/17.49 % (2665320)CaDiCaL version: 2.1.3
% 117.60/17.49 % (2665320)Termination reason: Refutation
% 117.60/17.49 % (2665320)Time elapsed: 0.607 s
% 117.60/17.49 % (2665320)Peak memory usage: 131 MB
% 117.60/17.49 % (2665320)Instructions burned: 1045 (million)
% 117.60/17.49 % (2665320)------------------------------
% 117.60/17.49 % (2665320)------------------------------
% 117.60/17.49 % (2665207)Success in time 16.561 s
% 117.60/17.49 % Vampire exiting
%------------------------------------------------------------------------------