%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV061-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 10:36:44 AM UTC 2026
% Result : Unsatisfiable 94.11s 18.29s
% Output : Refutation 110.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 26
% Syntax : Number of formulae : 88 ( 19 unt; 11 def)
% Number of atoms : 289 ( 0 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 391 ( 190 ~; 190 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 16 prp; 0-3 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 119 ( 0 sgn 119 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3655,axiom,
! [X2,X0,X1] :
( ~ esk19874_3(X0,X1,X2)
| esk16547_3(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_3655) ).
fof(f19944,axiom,
! [X2,X0,X1] :
( ~ p(X0)
| esk7964_0
| ~ esk19874_3(X1,X2,X0)
| ~ p(X2)
| p(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_19944) ).
fof(f21820,axiom,
esk2_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_21820) ).
fof(f29308,axiom,
! [X2,X0,X1] :
( ~ p(X0)
| esk1_0
| ~ p(X1)
| ~ p(X2)
| ~ esk27895_3(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_29308) ).
fof(f30917,axiom,
! [X2,X0,X1] :
( ~ esk16607_3(X0,X1,X2)
| esk27895_3(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_30917) ).
fof(f37328,axiom,
! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| esk28025_3(X0,X2,X1)
| ~ esk2_0
| ~ p(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_37328) ).
fof(f40244,axiom,
! [X2,X0,X1] :
( ~ esk19874_3(X0,X1,X2)
| ~ p(X1)
| ~ p(X2)
| ~ p(X0)
| esk7968_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_40244) ).
fof(f42909,axiom,
! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ esk7968_0
| ~ p(X2)
| esk19874_3(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_42909) ).
fof(f46490,axiom,
! [X2,X0,X1] :
( ~ esk16547_3(X0,X1,X2)
| esk16607_3(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_46490) ).
fof(f49597,axiom,
~ esk1_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_49597) ).
fof(f54419,axiom,
! [X2,X0,X1] :
( ~ esk17875_3(X0,X1,X2)
| esk19874_3(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_54419) ).
fof(f69287,axiom,
! [X2,X0,X1] :
( ~ esk28025_3(X0,X1,X2)
| esk17935_3(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_69287) ).
fof(f71200,axiom,
! [X2,X0,X1] :
( ~ p(X0)
| ~ esk7964_0
| esk19874_3(X1,X2,X0)
| ~ p(X2)
| p(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_71200) ).
fof(f83158,axiom,
! [X2,X0,X1] :
( ~ esk17935_3(X0,X1,X2)
| esk17875_3(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',i_0_83158) ).
fof(f89005,axiom,
p(true),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_true) ).
fof(f89028,definition,
( spl0_6
<=> esk1_0 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f89517,definition,
( spl0_128
<=> esk2_0 ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f149676,definition,
( spl0_15165
<=> esk7964_0 ),
introduced(definition,[new_symbols(definition,[spl0_15165])],[avatar_definition]) ).
fof(f149680,definition,
( spl0_15166
<=> ! [X2,X0,X1] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| esk19874_3(X1,X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_15166])],[avatar_definition]) ).
fof(f149681,plain,
( ! [X2,X0,X1] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| esk19874_3(X1,X2,X0) )
| ~ spl0_15166 ),
inference(avatar_component_clause,[],[f149680]) ).
fof(f149682,plain,
( ~ spl0_15165
| spl0_15166 ),
inference(avatar_split_clause,[],[f71200,f149680,f149676]) ).
fof(f194202,definition,
( spl0_26284
<=> esk7968_0 ),
introduced(definition,[new_symbols(definition,[spl0_26284])],[avatar_definition]) ).
fof(f207904,plain,
~ spl0_6,
inference(avatar_split_clause,[],[f49597,f89028]) ).
fof(f223354,definition,
( spl0_33552
<=> ! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| esk19874_3(X1,X2,X0)
| ~ p(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_33552])],[avatar_definition]) ).
fof(f223355,plain,
( ! [X2,X0,X1] :
( esk19874_3(X1,X2,X0)
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) )
| ~ spl0_33552 ),
inference(avatar_component_clause,[],[f223354]) ).
fof(f223356,plain,
( ~ spl0_26284
| spl0_33552 ),
inference(avatar_split_clause,[],[f42909,f223354,f194202]) ).
fof(f229577,definition,
( spl0_35102
<=> ! [X2,X0,X1] :
( ~ esk19874_3(X0,X1,X2)
| ~ p(X0)
| ~ p(X2)
| ~ p(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_35102])],[avatar_definition]) ).
fof(f229578,plain,
( ! [X2,X0,X1] :
( ~ esk19874_3(X0,X1,X2)
| ~ p(X0)
| ~ p(X2)
| ~ p(X1) )
| ~ spl0_35102 ),
inference(avatar_component_clause,[],[f229577]) ).
fof(f229579,plain,
( spl0_26284
| spl0_35102 ),
inference(avatar_split_clause,[],[f40244,f229577,f194202]) ).
fof(f236229,definition,
( spl0_36761
<=> ! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X2)
| esk28025_3(X0,X2,X1)
| ~ p(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_36761])],[avatar_definition]) ).
fof(f236230,plain,
( ! [X2,X0,X1] :
( esk28025_3(X0,X2,X1)
| ~ p(X2)
| ~ p(X0)
| ~ p(X1) )
| ~ spl0_36761 ),
inference(avatar_component_clause,[],[f236229]) ).
fof(f236231,plain,
( ~ spl0_128
| spl0_36761 ),
inference(avatar_split_clause,[],[f37328,f236229,f89517]) ).
fof(f254117,definition,
( spl0_41215
<=> ! [X2,X0,X1] :
( ~ p(X0)
| ~ esk27895_3(X0,X2,X1)
| ~ p(X2)
| ~ p(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_41215])],[avatar_definition]) ).
fof(f254118,plain,
( ! [X2,X0,X1] :
( ~ esk27895_3(X0,X2,X1)
| ~ p(X0)
| ~ p(X2)
| ~ p(X1) )
| ~ spl0_41215 ),
inference(avatar_component_clause,[],[f254117]) ).
fof(f254119,plain,
( spl0_6
| spl0_41215 ),
inference(avatar_split_clause,[],[f29308,f254117,f89028]) ).
fof(f270199,plain,
spl0_128,
inference(avatar_split_clause,[],[f21820,f89517]) ).
fof(f274192,definition,
( spl0_46208
<=> ! [X2,X0,X1] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| ~ esk19874_3(X1,X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_46208])],[avatar_definition]) ).
fof(f274193,plain,
( ! [X2,X0,X1] :
( ~ p(X0)
| p(X1)
| ~ p(X2)
| ~ esk19874_3(X1,X2,X0) )
| ~ spl0_46208 ),
inference(avatar_component_clause,[],[f274192]) ).
fof(f274194,plain,
( spl0_15165
| spl0_46208 ),
inference(avatar_split_clause,[],[f19944,f274192,f149676]) ).
fof(f326599,definition,
( spl0_56631
<=> ! [X1] : ~ p(X1) ),
introduced(definition,[new_symbols(definition,[spl0_56631])],[avatar_definition]) ).
fof(f326600,plain,
( ! [X1] : ~ p(X1)
| ~ spl0_56631 ),
inference(avatar_component_clause,[],[f326599]) ).
fof(f327796,plain,
( ! [X2,X0,X1] :
( ~ esk19874_3(X0,X1,X2)
| ~ p(X2)
| ~ p(X1) )
| ~ spl0_35102
| ~ spl0_46208 ),
inference(forward_subsumption_resolution,[],[f229578,f274193]) ).
fof(f327907,plain,
( ! [X2,X0,X1] :
( esk17935_3(X1,X0,X2)
| ~ p(X1)
| ~ p(X2)
| ~ p(X0) )
| ~ spl0_36761 ),
inference(resolution,[],[f236230,f69287]) ).
fof(f327909,plain,
( ! [X2,X0,X1] :
( esk17875_3(X0,X2,X1)
| ~ p(X1)
| ~ p(X2)
| ~ p(X0) )
| ~ spl0_36761 ),
inference(resolution,[],[f327907,f83158]) ).
fof(f327910,plain,
( ! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| esk19874_3(X2,X1,X0) )
| ~ spl0_36761 ),
inference(resolution,[],[f327909,f54419]) ).
fof(f327951,plain,
( ! [X2,X0,X1] :
( esk16547_3(X0,X2,X1)
| ~ p(X1)
| ~ p(X2)
| ~ p(X0) )
| ~ spl0_33552 ),
inference(resolution,[],[f223355,f3655]) ).
fof(f327964,plain,
( ! [X2,X0,X1] :
( esk16607_3(X2,X1,X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X0) )
| ~ spl0_33552 ),
inference(resolution,[],[f327951,f46490]) ).
fof(f327965,plain,
( ! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| esk27895_3(X1,X0,X2) )
| ~ spl0_33552 ),
inference(resolution,[],[f327964,f30917]) ).
fof(f327967,plain,
( ! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2) )
| ~ spl0_33552
| ~ spl0_41215 ),
inference(forward_subsumption_resolution,[],[f327965,f254118]) ).
fof(f327968,plain,
( spl0_56631
| spl0_56631
| spl0_56631
| ~ spl0_33552
| ~ spl0_41215 ),
inference(avatar_split_clause,[],[f327967,f254117,f223354,f326599,f326599,f326599]) ).
fof(f327971,plain,
( ! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2) )
| ~ spl0_35102
| ~ spl0_36761
| ~ spl0_46208 ),
inference(forward_subsumption_resolution,[],[f327910,f327796]) ).
fof(f327973,plain,
( spl0_56631
| spl0_56631
| spl0_56631
| ~ spl0_35102
| ~ spl0_36761
| ~ spl0_46208 ),
inference(avatar_split_clause,[],[f327971,f274192,f236229,f229577,f326599,f326599,f326599]) ).
fof(f327974,plain,
( $false
| ~ spl0_56631 ),
inference(resolution,[],[f326600,f89005]) ).
fof(f327975,plain,
~ spl0_56631,
inference(avatar_contradiction_clause,[],[f327974]) ).
fof(f328075,plain,
( ! [X2,X0,X1] :
( esk19874_3(X2,X1,X0)
| ~ p(X1)
| ~ p(X0) )
| ~ spl0_15166
| ~ spl0_36761 ),
inference(forward_subsumption_resolution,[],[f327910,f149681]) ).
fof(f328078,plain,
( ! [X2,X0,X1] :
( esk16547_3(X2,X0,X1)
| ~ p(X1)
| ~ p(X0) )
| ~ spl0_15166
| ~ spl0_36761 ),
inference(resolution,[],[f328075,f3655]) ).
fof(f328089,plain,
( ! [X2,X0,X1] :
( esk16607_3(X2,X1,X0)
| ~ p(X1)
| ~ p(X0) )
| ~ spl0_15166
| ~ spl0_36761 ),
inference(resolution,[],[f328078,f46490]) ).
fof(f328090,plain,
( ! [X2,X0,X1] :
( esk27895_3(X2,X0,X1)
| ~ p(X1)
| ~ p(X0) )
| ~ spl0_15166
| ~ spl0_36761 ),
inference(resolution,[],[f328089,f30917]) ).
fof(f328103,plain,
( ! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) )
| ~ spl0_15166
| ~ spl0_36761
| ~ spl0_41215 ),
inference(resolution,[],[f328090,f254118]) ).
fof(f328105,plain,
( ! [X2,X0,X1] :
( ~ p(X0)
| ~ p(X1)
| ~ p(X2) )
| ~ spl0_15166
| ~ spl0_36761
| ~ spl0_41215 ),
inference(duplicate_literal_removal,[],[f328103]) ).
fof(f328106,plain,
( spl0_56631
| spl0_56631
| spl0_56631
| ~ spl0_15166
| ~ spl0_36761
| ~ spl0_41215 ),
inference(avatar_split_clause,[],[f328105,f254117,f236229,f149680,f326599,f326599,f326599]) ).
cnf(s9208,plain,
( ~ spl0_15165
| spl0_15166 ),
inference(sat_conversion,[],[f149682]) ).
cnf(s20495,plain,
~ spl0_6,
inference(sat_conversion,[],[f207904]) ).
cnf(s23946,plain,
( ~ spl0_26284
| spl0_33552 ),
inference(sat_conversion,[],[f223356]) ).
cnf(s25358,plain,
( spl0_26284
| spl0_35102 ),
inference(sat_conversion,[],[f229579]) ).
cnf(s26888,plain,
( ~ spl0_128
| spl0_36761 ),
inference(sat_conversion,[],[f236231]) ).
cnf(s31158,plain,
( spl0_6
| spl0_41215 ),
inference(sat_conversion,[],[f254119]) ).
cnf(s35076,plain,
spl0_128,
inference(sat_conversion,[],[f270199]) ).
cnf(s36068,plain,
( spl0_15165
| spl0_46208 ),
inference(sat_conversion,[],[f274194]) ).
cnf(s46539,plain,
( spl0_56631
| spl0_56631
| ~ spl0_33552
| ~ spl0_41215
| spl0_56631 ),
inference(sat_conversion,[],[f327968]) ).
cnf(s46540,plain,
( ~ spl0_33552
| ~ spl0_41215
| spl0_56631 ),
inference(rat,[],[s46539]) ).
cnf(s46541,plain,
( spl0_56631
| spl0_56631
| ~ spl0_46208
| ~ spl0_35102
| ~ spl0_36761
| spl0_56631 ),
inference(sat_conversion,[],[f327973]) ).
cnf(s46542,plain,
( ~ spl0_35102
| ~ spl0_36761
| ~ spl0_46208
| spl0_56631 ),
inference(rat,[],[s46541]) ).
cnf(s46543,plain,
~ spl0_56631,
inference(sat_conversion,[],[f327975]) ).
cnf(s46551,plain,
( spl0_56631
| spl0_56631
| ~ spl0_41215
| ~ spl0_15166
| ~ spl0_36761
| spl0_56631 ),
inference(sat_conversion,[],[f328106]) ).
cnf(s46552,plain,
( ~ spl0_15166
| ~ spl0_36761
| ~ spl0_41215
| spl0_56631 ),
inference(rat,[],[s46551]) ).
cnf(s46554,plain,
( ~ spl0_35102
| ~ spl0_36761
| ~ spl0_46208 ),
inference(rat,[],[s46542,s46543]) ).
cnf(s46555,plain,
( ~ spl0_33552
| ~ spl0_41215 ),
inference(rat,[],[s46540,s46543]) ).
cnf(s46683,plain,
spl0_36761,
inference(rat,[],[s26888,s35076]) ).
cnf(s47585,plain,
spl0_41215,
inference(rat,[],[s31158,s20495]) ).
cnf(s48186,plain,
~ spl0_33552,
inference(rat,[],[s46555,s47585]) ).
cnf(s48188,plain,
~ spl0_15166,
inference(rat,[],[s46552,s46543,s46683,s47585]) ).
cnf(s48192,plain,
~ spl0_26284,
inference(rat,[],[s23946,s48186]) ).
cnf(s48195,plain,
spl0_35102,
inference(rat,[],[s25358,s48192]) ).
cnf(s48198,plain,
~ spl0_46208,
inference(rat,[],[s46554,s46683,s48195]) ).
cnf(s48200,plain,
spl0_15165,
inference(rat,[],[s36068,s48198]) ).
cnf(s48967,plain,
$false,
inference(rat,[],[s9208,s48188,s48200]) ).
fof(f328107,plain,
$false,
inference(avatar_sat_refutation,[],[s48967]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV061-1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n014.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 11:18:47 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.46 Running first-order theorem proving
% 0.20/0.46 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
% 20.36/5.73 % (644889)Input is clausal, will run a generic CNF schedule.
% 20.36/5.73 % (644936)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=1352756699:i=140167_2977 on theBenchmark for (2977ds/140167Mi)
% 20.36/5.73 % (644941)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1667482036:s2a=on:i=180:gtg=position_2977 on theBenchmark for (2977ds/180Mi)
% 20.36/5.73 % (644937)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2108111700:i=132376:av=off_2977 on theBenchmark for (2977ds/132376Mi)
% 20.36/5.73 % (644940)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=646924372:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2977 on theBenchmark for (2977ds/114Mi)
% 20.36/5.73 % (644938)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2937856140:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2977 on theBenchmark for (2977ds/137899Mi)
% 20.36/5.73 % (644939)lrs+10_1_sil=8000:sp=occurrence:random_seed=4246930423:i=107:sd=3:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/107Mi)
% 20.36/5.73 % (644942)dis-21_1_sil=8000:lcm=predicate:random_seed=156835004:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2977 on theBenchmark for (2977ds/117Mi)
% 20.36/5.73 % (644940)Instruction limit reached!
% 20.36/5.73 % (644940)------------------------------
% 20.36/5.73 % (644940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.36/5.73 % (644940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/5.73 % (644940)CaDiCaL version: 2.1.3
% 20.36/5.73 % (644940)Termination reason: Instruction limit
% 20.36/5.73 % (644940)Termination phase: SInE selection
% 20.36/5.73 % (644940)Time elapsed: 0.091 s
% 20.36/5.73 % (644940)Peak memory usage: 156 MB
% 20.36/5.73 % (644940)Instructions burned: 114 (million)
% 20.36/5.73 % (644939)Instruction limit reached!
% 20.36/5.73 % (644939)------------------------------
% 20.36/5.73 % (644939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.36/5.73 % (644939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/5.73 % (644939)CaDiCaL version: 2.1.3
% 20.36/5.73 % (644939)Termination reason: Instruction limit
% 20.36/5.73 % (644939)Termination phase: SInE selection
% 20.36/5.73 % (644939)Time elapsed: 0.129 s
% 20.36/5.73 % (644939)Peak memory usage: 156 MB
% 20.36/5.73 % (644939)Instructions burned: 107 (million)
% 20.36/5.73 % (644941)Instruction limit reached!
% 20.36/5.73 % (644941)------------------------------
% 20.36/5.73 % (644941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.36/5.73 % (644941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/5.73 % (644941)CaDiCaL version: 2.1.3
% 20.36/5.73 % (644941)Termination reason: Instruction limit
% 20.36/5.73 % (644941)Termination phase: Property scanning
% 20.36/5.73 % (644941)Time elapsed: 0.189 s
% 20.36/5.73 % (644941)Peak memory usage: 155 MB
% 20.36/5.73 % (644941)Instructions burned: 181 (million)
% 20.36/5.73 % (644942)Instruction limit reached!
% 20.36/5.73 % (644942)------------------------------
% 20.36/5.73 % (644942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.36/5.73 % (644942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.36/5.73 % (644942)CaDiCaL version: 2.1.3
% 20.36/5.73 % (644942)Termination reason: Instruction limit
% 20.36/5.73 % (644942)Termination phase: SInE selection
% 20.36/5.73 % (644942)Time elapsed: 0.156 s
% 20.36/5.73 % (644942)Peak memory usage: 160 MB
% 20.36/5.73 % (644942)Instructions burned: 117 (million)
% 20.36/5.73 % (644952)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=1613910362:i=143:sd=2:aac=none:ss=axioms:sgt=16_2974 on theBenchmark for (2974ds/143Mi)
% 20.36/5.73 % (644955)lrs+10_64_to=lpo:sil=8000:random_seed=2170453614:i=126:bd=preordered_2973 on theBenchmark for (2973ds/126Mi)
% 20.36/5.73 % (644953)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2954174651:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2973 on theBenchmark for (2973ds/189Mi)
% 20.36/5.73 % (644954)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2081318443:st=4:i=219:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/219Mi)
% 20.36/5.73 % (644952)Instruction limit reached!
% 20.36/5.73 % (644952)------------------------------
% 45.33/9.25 % (644952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.33/9.25 % (644952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.33/9.25 % (644952)CaDiCaL version: 2.1.3
% 45.33/9.25 % (644952)Termination reason: Instruction limit
% 45.33/9.25 % (644952)Termination phase: SInE selection
% 45.33/9.25 % (644952)Time elapsed: 0.177 s
% 45.33/9.25 % (644952)Peak memory usage: 157 MB
% 45.33/9.25 % (644952)Instructions burned: 144 (million)
% 45.33/9.25 % (644953)Instruction limit reached!
% 45.33/9.25 % (644953)------------------------------
% 45.33/9.25 % (644953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.33/9.25 % (644953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.33/9.25 % (644953)CaDiCaL version: 2.1.3
% 45.33/9.25 % (644953)Termination reason: Instruction limit
% 45.33/9.25 % (644953)Termination phase: SInE selection
% 45.33/9.25 % (644953)Time elapsed: 0.206 s
% 45.33/9.25 % (644953)Peak memory usage: 157 MB
% 45.33/9.25 % (644953)Instructions burned: 189 (million)
% 45.33/9.25 % (644955)Instruction limit reached!
% 45.33/9.25 % (644955)------------------------------
% 45.33/9.25 % (644955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.33/9.25 % (644955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.33/9.25 % (644955)CaDiCaL version: 2.1.3
% 45.33/9.25 % (644955)Termination reason: Instruction limit
% 45.33/9.25 % (644955)Termination phase: Saturation
% 45.33/9.25 % (644955)Time elapsed: 0.233 s
% 45.33/9.25 % (644955)Peak memory usage: 175 MB
% 45.33/9.25 % (644955)Instructions burned: 127 (million)
% 45.33/9.25 % (644954)Instruction limit reached!
% 45.33/9.25 % (644954)------------------------------
% 45.33/9.25 % (644954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.33/9.25 % (644954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.33/9.25 % (644954)CaDiCaL version: 2.1.3
% 45.33/9.25 % (644954)Termination reason: Instruction limit
% 45.33/9.25 % (644954)Termination phase: SInE selection
% 45.33/9.25 % (644954)Time elapsed: 0.234 s
% 45.33/9.25 % (644954)Peak memory usage: 157 MB
% 45.33/9.25 % (644954)Instructions burned: 219 (million)
% 45.33/9.25 % (644961)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=259972011:avsq=on:i=194:fgj=on:bd=preordered_2970 on theBenchmark for (2970ds/194Mi)
% 45.33/9.25 % (644962)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2106374269:i=157:gtg=all_2969 on theBenchmark for (2969ds/157Mi)
% 45.33/9.25 % (644963)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=706181761:i=3394:sd=4:ss=included:sgt=64_2969 on theBenchmark for (2969ds/3394Mi)
% 45.33/9.25 % (644964)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=1051467513:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2968 on theBenchmark for (2968ds/106Mi)
% 45.33/9.25 % (644961)Instruction limit reached!
% 45.33/9.25 % (644961)------------------------------
% 45.33/9.25 % (644961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.33/9.25 % (644961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.33/9.25 % (644961)CaDiCaL version: 2.1.3
% 45.33/9.25 % (644961)Termination reason: Instruction limit
% 45.33/9.25 % (644961)Termination phase: Saturation
% 45.33/9.25 % (644961)Time elapsed: 0.331 s
% 45.33/9.25 % (644961)Peak memory usage: 175 MB
% 45.33/9.25 % (644961)Instructions burned: 194 (million)
% 45.33/9.25 % (644962)Instruction limit reached!
% 45.33/9.25 % (644962)------------------------------
% 45.33/9.25 % (644962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.33/9.25 % (644962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.33/9.25 % (644962)CaDiCaL version: 2.1.3
% 45.33/9.25 % (644962)Termination reason: Instruction limit
% 45.33/9.25 % (644962)Termination phase: Property scanning
% 45.33/9.25 % (644962)Time elapsed: 0.173 s
% 45.33/9.25 % (644962)Peak memory usage: 155 MB
% 45.33/9.25 % (644962)Instructions burned: 157 (million)
% 45.33/9.25 % (644964)Instruction limit reached!
% 45.33/9.25 % (644964)------------------------------
% 45.33/9.25 % (644964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.33/9.25 % (644964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.33/9.25 % (644964)CaDiCaL version: 2.1.3
% 45.33/9.25 % (644964)Termination reason: Instruction limit
% 45.33/9.25 % (644964)Termination phase: SInE selection
% 67.46/12.31 % (644964)Time elapsed: 0.134 s
% 67.46/12.31 % (644964)Peak memory usage: 156 MB
% 67.46/12.31 % (644964)Instructions burned: 106 (million)
% 67.46/12.31 % (644969)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3402869160:i=107_2965 on theBenchmark for (2965ds/107Mi)
% 67.46/12.31 % (644970)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3901181034:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2965 on theBenchmark for (2965ds/242Mi)
% 67.46/12.31 % (644971)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3083505651:cond=fast:i=5208:av=off_2964 on theBenchmark for (2964ds/5208Mi)
% 67.46/12.31 % (644969)Instruction limit reached!
% 67.46/12.31 % (644969)------------------------------
% 67.46/12.31 % (644969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.46/12.31 % (644969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.46/12.31 % (644969)CaDiCaL version: 2.1.3
% 67.46/12.32 % (644969)Termination reason: Instruction limit
% 67.46/12.32 % (644969)Termination phase: Saturation
% 67.46/12.32 % (644969)Time elapsed: 0.165 s
% 67.46/12.32 % (644969)Peak memory usage: 175 MB
% 67.46/12.32 % (644969)Instructions burned: 107 (million)
% 67.46/12.32 % (644970)Instruction limit reached!
% 67.46/12.32 % (644970)------------------------------
% 67.46/12.32 % (644970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.46/12.32 % (644970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.46/12.32 % (644970)CaDiCaL version: 2.1.3
% 67.46/12.32 % (644970)Termination reason: Instruction limit
% 67.46/12.32 % (644970)Termination phase: Property scanning
% 67.46/12.32 % (644970)Time elapsed: 0.254 s
% 67.46/12.32 % (644970)Peak memory usage: 155 MB
% 67.46/12.32 % (644970)Instructions burned: 242 (million)
% 67.46/12.32 % (644975)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4173709686:i=134:sd=2:doe=on:ss=axioms:sgt=14_2961 on theBenchmark for (2961ds/134Mi)
% 67.46/12.32 % (644975)Instruction limit reached!
% 67.46/12.32 % (644975)------------------------------
% 67.46/12.32 % (644975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.46/12.32 % (644975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.46/12.32 % (644975)CaDiCaL version: 2.1.3
% 67.46/12.32 % (644975)Termination reason: Instruction limit
% 67.46/12.32 % (644975)Termination phase: SInE selection
% 67.46/12.32 % (644975)Time elapsed: 0.168 s
% 67.46/12.32 % (644975)Peak memory usage: 157 MB
% 67.46/12.32 % (644975)Instructions burned: 134 (million)
% 67.46/12.32 % (644976)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=461052884:i=499:bd=all_2960 on theBenchmark for (2960ds/499Mi)
% 67.46/12.32 % (644980)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1601964170:i=191:fgj=on:bd=all_2958 on theBenchmark for (2958ds/191Mi)
% 67.46/12.32 % (644980)Instruction limit reached!
% 67.46/12.32 % (644980)------------------------------
% 67.46/12.32 % (644980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.46/12.32 % (644980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.46/12.32 % (644980)CaDiCaL version: 2.1.3
% 67.46/12.32 % (644980)Termination reason: Instruction limit
% 67.46/12.32 % (644980)Termination phase: Saturation
% 67.46/12.32 % (644980)Time elapsed: 0.222 s
% 67.46/12.32 % (644980)Peak memory usage: 176 MB
% 67.46/12.32 % (644980)Instructions burned: 192 (million)
% 67.46/12.32 % (644976)Instruction limit reached!
% 67.46/12.32 % (644976)------------------------------
% 67.46/12.32 % (644976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.46/12.32 % (644976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.46/12.32 % (644976)CaDiCaL version: 2.1.3
% 67.46/12.32 % (644976)Termination reason: Instruction limit
% 67.46/12.32 % (644976)Termination phase: Saturation
% 67.46/12.32 % (644976)Time elapsed: 0.476 s
% 67.46/12.32 % (644976)Peak memory usage: 187 MB
% 67.46/12.32 % (644976)Instructions burned: 500 (million)
% 67.46/12.32 % (644983)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=403189661:i=264:kws=precedence:fsr=off_2953 on theBenchmark for (2953ds/264Mi)
% 67.46/12.32 % (644984)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2821019912:cond=on:i=156:bs=on:gtg=exists_all:er=known_2953 on theBenchmark for (2953ds/156Mi)
% 71.75/12.95 % (644984)Instruction limit reached!
% 71.75/12.95 % (644984)------------------------------
% 71.75/12.95 % (644984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.75/12.95 % (644984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.75/12.95 % (644984)CaDiCaL version: 2.1.3
% 71.75/12.95 % (644984)Termination reason: Instruction limit
% 71.75/12.95 % (644984)Termination phase: Property scanning
% 71.75/12.95 % (644984)Time elapsed: 0.107 s
% 71.75/12.95 % (644984)Peak memory usage: 155 MB
% 71.75/12.95 % (644984)Instructions burned: 157 (million)
% 71.75/12.95 % (644987)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=2631192922:i=3256:kws=precedence:bd=preordered:av=off_2950 on theBenchmark for (2950ds/3256Mi)
% 71.75/12.95 % (644983)Instruction limit reached!
% 71.75/12.95 % (644983)------------------------------
% 71.75/12.95 % (644983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.75/12.95 % (644983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.75/12.95 % (644983)CaDiCaL version: 2.1.3
% 71.75/12.95 % (644983)Termination reason: Instruction limit
% 71.75/12.95 % (644983)Termination phase: Saturation
% 71.75/12.95 % (644983)Time elapsed: 0.329 s
% 71.75/12.95 % (644983)Peak memory usage: 176 MB
% 71.75/12.95 % (644983)Instructions burned: 264 (million)
% 71.75/12.95 % (644989)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3555697952:i=537:av=off:ss=included_2948 on theBenchmark for (2948ds/537Mi)
% 71.75/12.95 % (644989)Instruction limit reached!
% 71.75/12.95 % (644989)------------------------------
% 71.75/12.95 % (644989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.75/12.95 % (644989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.75/12.95 % (644989)CaDiCaL version: 2.1.3
% 71.75/12.95 % (644989)Termination reason: Instruction limit
% 71.75/12.95 % (644989)Termination phase: Property scanning
% 71.75/12.95 % (644989)Time elapsed: 0.471 s
% 71.75/12.95 % (644989)Peak memory usage: 174 MB
% 71.75/12.95 % (644989)Instructions burned: 538 (million)
% 71.75/12.95 % (644991)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3374749725:i=180:bd=preordered:av=off_2942 on theBenchmark for (2942ds/180Mi)
% 71.75/12.95 % (644991)Instruction limit reached!
% 71.75/12.95 % (644991)------------------------------
% 71.75/12.95 % (644991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.75/12.95 % (644991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.75/12.95 % (644991)CaDiCaL version: 2.1.3
% 71.75/12.95 % (644991)Termination reason: Instruction limit
% 71.75/12.95 % (644991)Termination phase: Saturation
% 71.75/12.95 % (644991)Time elapsed: 0.252 s
% 71.75/12.95 % (644991)Peak memory usage: 175 MB
% 71.75/12.95 % (644991)Instructions burned: 182 (million)
% 71.75/12.95 % (644993)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=861293772:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2938 on theBenchmark for (2938ds/10307Mi)
% 71.75/12.95 % (644963)Instruction limit reached!
% 71.75/12.95 % (644963)------------------------------
% 71.75/12.95 % (644963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.75/12.95 % (644963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.75/12.95 % (644963)CaDiCaL version: 2.1.3
% 71.75/12.95 % (644963)Termination reason: Instruction limit
% 71.75/12.95 % (644963)Termination phase: Saturation
% 71.75/12.95 % (644963)Time elapsed: 4.375 s
% 71.75/12.95 % (644963)Peak memory usage: 614 MB
% 71.75/12.95 % (644963)Instructions burned: 3394 (million)
% 71.75/12.95 % (645035)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=1706599278:i=412:gtgl=4:gtg=exists_all_2922 on theBenchmark for (2922ds/412Mi)
% 71.75/12.95 % (645035)Instruction limit reached!
% 71.75/12.95 % (645035)------------------------------
% 71.75/12.95 % (645035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.75/12.95 % (645035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.75/12.95 % (645035)CaDiCaL version: 2.1.3
% 71.75/12.95 % (645035)Termination reason: Instruction limit
% 71.75/12.95 % (645035)Termination phase: Initialization
% 71.75/12.95 % (645035)Time elapsed: 0.254 s
% 71.75/12.95 % (645035)Peak memory usage: 156 MB
% 71.75/12.95 % (645035)Instructions burned: 413 (million)
% 71.75/12.95 % (645037)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=3342559376:s2pl=no:i=8478:s2at=4:nm=6_2918 on theBenchmark for (2918ds/8478Mi)
% 93.98/16.06 % (644987)Instruction limit reached!
% 93.98/16.06 % (644987)------------------------------
% 93.98/16.06 % (644987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.98/16.06 % (644987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.98/16.06 % (644987)CaDiCaL version: 2.1.3
% 93.98/16.06 % (644987)Termination reason: Instruction limit
% 93.98/16.06 % (644987)Termination phase: Saturation
% 93.98/16.06 % (644987)Time elapsed: 3.898 s
% 93.98/16.06 % (644987)Peak memory usage: 604 MB
% 93.98/16.06 % (644987)Instructions burned: 3258 (million)
% 93.98/16.06 % (645039)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=3158057104:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2909 on theBenchmark for (2909ds/303Mi)
% 93.98/16.06 % (645039)Instruction limit reached!
% 93.98/16.06 % (645039)------------------------------
% 93.98/16.06 % (645039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.98/16.06 % (645039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.98/16.06 % (645039)CaDiCaL version: 2.1.3
% 93.98/16.06 % (645039)Termination reason: Instruction limit
% 93.98/16.06 % (645039)Termination phase: SInE selection
% 93.98/16.06 % (645039)Time elapsed: 0.269 s
% 93.98/16.06 % (645039)Peak memory usage: 163 MB
% 93.98/16.06 % (645039)Instructions burned: 303 (million)
% 93.98/16.06 % (645041)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3613280269:st=4:i=720:sd=3:fsr=off:ss=axioms_2905 on theBenchmark for (2905ds/720Mi)
% 93.98/16.06 % (645041)Refutation not found, incomplete strategy
% 93.98/16.06 % (645041)------------------------------
% 93.98/16.06 % (645041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.98/16.06 % (645041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.98/16.06 % (645041)CaDiCaL version: 2.1.3
% 93.98/16.06 % (645041)Termination reason: Refutation not found, incomplete strategy
% 93.98/16.06 % (645041)Time elapsed: 0.280 s
% 93.98/16.06 % (645041)Peak memory usage: 175 MB
% 93.98/16.06 % (645041)Instructions burned: 322 (million)
% 93.98/16.06 % (645041)------------------------------
% 93.98/16.06 % (645041)------------------------------
% 93.98/16.06 % (645043)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1062040864:i=598:bs=on:bd=preordered:av=off:ss=axioms_2898 on theBenchmark for (2898ds/598Mi)
% 93.98/16.06 % (644971)Instruction limit reached!
% 93.98/16.06 % (644971)------------------------------
% 93.98/16.06 % (644971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.98/16.06 % (644971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.98/16.06 % (644971)CaDiCaL version: 2.1.3
% 93.98/16.06 % (644971)Termination reason: Instruction limit
% 93.98/16.06 % (644971)Termination phase: Saturation
% 93.98/16.06 % (644971)Time elapsed: 6.699 s
% 93.98/16.06 % (644971)Peak memory usage: 609 MB
% 93.98/16.06 % (644971)Instructions burned: 5211 (million)
% 93.98/16.06 % (645043)Refutation not found, incomplete strategy
% 93.98/16.06 % (645043)------------------------------
% 93.98/16.06 % (645043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.98/16.06 % (645043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.98/16.06 % (645043)CaDiCaL version: 2.1.3
% 93.98/16.06 % (645043)Termination reason: Refutation not found, incomplete strategy
% 93.98/16.06 % (645043)Time elapsed: 0.245 s
% 93.98/16.06 % (645043)Peak memory usage: 175 MB
% 93.98/16.06 % (645043)Instructions burned: 242 (million)
% 93.98/16.06 % (645045)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2443228457:i=2989:sd=3:ss=axioms:sgt=60_2894 on theBenchmark for (2894ds/2989Mi)
% 93.98/16.06 % (645043)------------------------------
% 93.98/16.06 % (645043)------------------------------
% 93.98/16.06 % (645047)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=2138918093:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2891 on theBenchmark for (2891ds/1997Mi)
% 93.98/16.06 [W927 11:18:59.794148887 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794182454 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794239914 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794252504 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794280681 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794291661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794383511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794401878 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794428945 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794439581 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794466575 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 [W927 11:18:59.794477688 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.57/16.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.57/16.46 % (645045)Refutation not found, incomplete strategy
% 96.57/16.46 % (645045)------------------------------
% 96.57/16.46 % (645045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.57/16.46 % (645045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.57/16.46 % (645045)CaDiCaL version: 2.1.3
% 96.57/16.46 % (645045)Termination reason: Refutation not found, incomplete strategy
% 96.57/16.46 % (645045)Time elapsed: 1.402 s
% 96.57/16.46 % (645045)Peak memory usage: 240 MB
% 103.80/17.51 % (645045)Instructions burned: 1808 (million)
% 103.80/17.51 % (645047)Instruction limit reached!
% 103.80/17.51 % (645047)------------------------------
% 103.80/17.51 % (645047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.80/17.51 % (645047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.80/17.51 % (645047)CaDiCaL version: 2.1.3
% 103.80/17.51 % (645047)Termination reason: Instruction limit
% 103.80/17.51 % (645047)Termination phase: Saturation
% 103.80/17.51 % (645047)Time elapsed: 1.280 s
% 103.80/17.51 % (645047)Peak memory usage: 187 MB
% 103.80/17.51 % (645047)Instructions burned: 1999 (million)
% 103.80/17.51 % (645045)------------------------------
% 103.80/17.51 % (645045)------------------------------
% 103.80/17.51 % (645049)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=2031871309:i=2088:bd=preordered:av=off_2876 on theBenchmark for (2876ds/2088Mi)
% 103.80/17.51 % (645050)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4494699:i=1098:nicw=on_2876 on theBenchmark for (2876ds/1098Mi)
% 103.80/17.51 % (645050)Instruction limit reached!
% 103.80/17.51 % (645050)------------------------------
% 103.80/17.51 % (645050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.80/17.51 % (645050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.80/17.51 % (645050)CaDiCaL version: 2.1.3
% 103.80/17.51 % (645050)Termination reason: Instruction limit
% 103.80/17.51 % (645050)Termination phase: Saturation
% 103.80/17.51 % (645050)Time elapsed: 0.753 s
% 103.80/17.51 % (645050)Peak memory usage: 187 MB
% 103.80/17.51 % (645050)Instructions burned: 1099 (million)
% 103.80/17.51 % (645166)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2152588628:i=433:bd=preordered_2867 on theBenchmark for (2867ds/433Mi)
% 103.80/17.51 % (645166)Instruction limit reached!
% 103.80/17.51 % (645166)------------------------------
% 103.80/17.51 % (645166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.80/17.51 % (645166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.80/17.51 % (645166)CaDiCaL version: 2.1.3
% 103.80/17.51 % (645166)Termination reason: Instruction limit
% 103.80/17.51 % (645166)Termination phase: Saturation
% 103.80/17.51 % (645166)Time elapsed: 0.341 s
% 103.80/17.51 % (645166)Peak memory usage: 175 MB
% 103.80/17.51 % (645166)Instructions burned: 433 (million)
% 103.80/17.51 % (645168)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2227586854:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2862 on theBenchmark for (2862ds/2942Mi)
% 103.80/17.51 % (645049)Instruction limit reached!
% 103.80/17.51 % (645049)------------------------------
% 103.80/17.51 % (645049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.80/17.51 % (645049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.80/17.51 % (645049)CaDiCaL version: 2.1.3
% 103.80/17.51 % (645049)Termination reason: Instruction limit
% 103.80/17.51 % (645049)Termination phase: Saturation
% 103.80/17.51 % (645049)Time elapsed: 2.033 s
% 103.80/17.51 % (645049)Peak memory usage: 439 MB
% 103.80/17.51 % (645049)Instructions burned: 2088 (million)
% 103.80/17.51 % (645170)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1153538859:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2854 on theBenchmark for (2854ds/6922Mi)
% 103.80/17.51 [W927 11:19:03.542047044 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.80/17.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.80/17.51 [W927 11:19:03.542081831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.80/17.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.80/17.51 [W927 11:19:03.542124517 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.80/17.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.542137651 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.542171488 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.542181708 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.542207518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.542217924 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.542242168 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.542252188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.542277188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.542287061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940437118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940480094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940523671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940546488 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940573231 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940583551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940610018 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940620128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940645261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940655495 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940691565 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 [W927 11:19:03.940701792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 94.11/18.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 94.11/18.29 % (645168)Refutation not found, incomplete strategy
% 94.11/18.29 % (645168)------------------------------
% 94.11/18.29 % (645168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.11/18.29 % (645168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.11/18.29 % (645168)CaDiCaL version: 2.1.3
% 94.11/18.29 % (645168)Termination reason: Refutation not found, incomplete strategy
% 94.11/18.29 % (645168)Time elapsed: 1.889 s
% 94.11/18.29 % (645168)Peak memory usage: 262 MB
% 94.11/18.29 % (645168)Instructions burned: 2519 (million)
% 94.11/18.29 % (645168)------------------------------
% 94.11/18.29 % (645168)------------------------------
% 94.11/18.29 % (645170)Refutation not found, incomplete strategy
% 94.11/18.29 % (645170)------------------------------
% 94.11/18.29 % (645170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.11/18.29 % (645170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.11/18.29 % (645170)CaDiCaL version: 2.1.3
% 94.11/18.29 % (645170)Termination reason: Refutation not found, incomplete strategy
% 94.11/18.29 % (645170)Time elapsed: 1.496 s
% 94.11/18.29 % (645170)Peak memory usage: 257 MB
% 94.11/18.29 % (645170)Instructions burned: 1943 (million)
% 94.11/18.29 % (645172)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=1102681176:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2839 on theBenchmark for (2839ds/596Mi)
% 94.11/18.29 % (645170)------------------------------
% 94.11/18.29 % (645170)------------------------------
% 94.11/18.29 % (645172)Instruction limit reached!
% 94.11/18.29 % (645172)------------------------------
% 94.11/18.29 % (645172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.11/18.29 % (645172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.11/18.29 % (645172)CaDiCaL version: 2.1.3
% 94.11/18.29 % (645172)Termination reason: Instruction limit
% 94.11/18.29 % (645172)Termination phase: Property scanning
% 94.11/18.29 % (645172)Time elapsed: 0.354 s
% 94.11/18.29 % (645172)Peak memory usage: 156 MB
% 94.11/18.29 % (645172)Instructions burned: 597 (million)
% 94.11/18.29 % (645174)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=2141150441:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2835 on theBenchmark for (2835ds/4123Mi)
% 94.11/18.29 % (645176)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2164103130:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2833 on theBenchmark for (2833ds/16411Mi)
% 94.11/18.29 % (644936)First to succeed.
% 94.11/18.29 % (644936)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-644889"
% 94.11/18.29 % (644936)Refutation found. Thanks to Tanya!
% 94.11/18.29 % SZS status Unsatisfiable for theBenchmark
% 94.11/18.29 % SZS output start Proof for theBenchmark
% See solution above
% 110.00/18.55 % (644936)------------------------------
% 110.00/18.55 % (644936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.00/18.55 % (644936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.00/18.55 % (644936)CaDiCaL version: 2.1.3
% 110.00/18.55 % (644936)Termination reason: Refutation
% 110.00/18.55 % (644936)Time elapsed: 14.671 s
% 110.00/18.55 % (644936)Peak memory usage: 812 MB
% 110.00/18.55 % (644936)Instructions burned: 26480 (million)
% 110.00/18.55 % (644936)------------------------------
% 110.00/18.55 % (644936)------------------------------
% 110.00/18.55 % (644889)Success in time 17.386 s
% 110.00/18.55 % Vampire exiting
%------------------------------------------------------------------------------