%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : TOP044+4 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n006.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 02:34:05 PM UTC 2026 % Result : Timeout 300.40s 44.17s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : TOP044+4 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.20 % Computer : n006.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 19:04:23 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.24 Running first-order theorem proving % 0.09/0.24 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 % 16.74/4.27 % (70413)Detected formulas, will run a generic FOF schedule. % 16.74/4.27 % (70421)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3626741435:i=109:sd=1:ins=1:gsp=on:ss=axioms_2983 on theBenchmark for (2983ds/109Mi) % 16.74/4.27 % (70420)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4266979969:i=141695:sd=1:nm=32:gsp=on:ss=included_2983 on theBenchmark for (2983ds/141695Mi) % 16.74/4.27 % (70422)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=532122458:i=119:av=off:ss=axioms_2983 on theBenchmark for (2983ds/119Mi) % 16.74/4.27 % (70419)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=874262713:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2983 on theBenchmark for (2983ds/134677Mi) % 16.74/4.27 % (70418)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=113653484:i=141193_2983 on theBenchmark for (2983ds/141193Mi) % 16.74/4.27 % (70423)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1030899829:s2a=on:i=139:gtg=position_2983 on theBenchmark for (2983ds/139Mi) % 16.74/4.27 % (70424)dis-21_1_sil=8000:lcm=predicate:random_seed=2239551597:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2983 on theBenchmark for (2983ds/129Mi) % 16.74/4.27 % (70423)Instruction limit reached! % 16.74/4.27 % (70423)------------------------------ % 16.74/4.27 % (70423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.74/4.27 % (70423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/4.27 % (70423)CaDiCaL version: 2.1.3 % 16.74/4.27 % (70423)Termination reason: Instruction limit % 16.74/4.27 % (70423)Termination phase: Property scanning % 16.74/4.27 % (70423)Time elapsed: 0.064 s % 16.74/4.27 % (70423)Peak memory usage: 172 MB % 16.74/4.27 % (70423)Instructions burned: 141 (million) % 16.74/4.27 % (70421)Instruction limit reached! % 16.74/4.27 % (70421)------------------------------ % 16.74/4.27 % (70421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.74/4.27 % (70421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/4.27 % (70421)CaDiCaL version: 2.1.3 % 16.74/4.27 % (70421)Termination reason: Instruction limit % 16.74/4.27 % (70421)Termination phase: SInE selection % 16.74/4.27 % (70421)Time elapsed: 0.080 s % 16.74/4.27 % (70421)Peak memory usage: 172 MB % 16.74/4.27 % (70421)Instructions burned: 109 (million) % 16.74/4.27 % (70422)Instruction limit reached! % 16.74/4.27 % (70422)------------------------------ % 16.74/4.27 % (70422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.74/4.27 % (70422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/4.27 % (70422)CaDiCaL version: 2.1.3 % 16.74/4.27 % (70422)Termination reason: Instruction limit % 16.74/4.27 % (70422)Termination phase: SInE selection % 16.74/4.27 % (70422)Time elapsed: 0.088 s % 16.74/4.27 % (70422)Peak memory usage: 172 MB % 16.74/4.27 % (70422)Instructions burned: 119 (million) % 16.74/4.27 % (70424)Instruction limit reached! % 16.74/4.27 % (70424)------------------------------ % 16.74/4.27 % (70424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.74/4.27 % (70424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.74/4.27 % (70424)CaDiCaL version: 2.1.3 % 16.74/4.27 % (70424)Termination reason: Instruction limit % 16.74/4.27 % (70424)Termination phase: SInE selection % 16.74/4.27 % (70424)Time elapsed: 0.099 s % 16.74/4.27 % (70424)Peak memory usage: 172 MB % 16.74/4.27 % (70424)Instructions burned: 130 (million) % 16.74/4.27 % (70432)lrs+10_1_sil=8000:sp=occurrence:random_seed=24619850:i=285:sd=3:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/285Mi) % 16.74/4.27 % (70433)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1073650192:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/157Mi) % 16.74/4.27 % (70434)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1953740790:i=325:sd=1:ss=axioms:sgt=32_2981 on theBenchmark for (2981ds/325Mi) % 16.74/4.27 % (70435)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1665099560:s2a=on:i=248:s2at=1.23:gtg=position_2980 on theBenchmark for (2980ds/248Mi) % 16.74/4.27 % (70432)Instruction limit reached! % 16.74/4.27 % (70432)------------------------------ % 16.74/4.27 % (70432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.23/6.56 % (70432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.23/6.56 % (70432)CaDiCaL version: 2.1.3 % 33.23/6.56 % (70432)Termination reason: Instruction limit % 33.23/6.56 % (70432)Termination phase: SInE selection % 33.23/6.56 % (70432)Time elapsed: 0.118 s % 33.23/6.56 % (70432)Peak memory usage: 173 MB % 33.23/6.56 % (70432)Instructions burned: 286 (million) % 33.23/6.56 % (70433)Instruction limit reached! % 33.23/6.56 % (70433)------------------------------ % 33.23/6.56 % (70433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.23/6.56 % (70433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.23/6.56 % (70433)CaDiCaL version: 2.1.3 % 33.23/6.56 % (70433)Termination reason: Instruction limit % 33.23/6.56 % (70433)Termination phase: Property scanning % 33.23/6.56 % (70433)Time elapsed: 0.074 s % 33.23/6.56 % (70433)Peak memory usage: 173 MB % 33.23/6.56 % (70433)Instructions burned: 158 (million) % 33.23/6.56 % (70435)Instruction limit reached! % 33.23/6.56 % (70435)------------------------------ % 33.23/6.56 % (70435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.23/6.56 % (70435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.23/6.56 % (70435)CaDiCaL version: 2.1.3 % 33.23/6.56 % (70435)Termination reason: Instruction limit % 33.23/6.56 % (70435)Termination phase: Property scanning % 33.23/6.56 % (70435)Time elapsed: 0.111 s % 33.23/6.56 % (70435)Peak memory usage: 173 MB % 33.23/6.56 % (70435)Instructions burned: 249 (million) % 33.23/6.56 % (70440)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3106369573:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2979 on theBenchmark for (2979ds/294Mi) % 33.23/6.56 % (70441)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2130921010:i=2350_2978 on theBenchmark for (2978ds/2350Mi) % 33.23/6.56 % (70434)Instruction limit reached! % 33.23/6.56 % (70434)------------------------------ % 33.23/6.56 % (70434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.23/6.56 % (70434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.23/6.56 % (70434)CaDiCaL version: 2.1.3 % 33.23/6.56 % (70434)Termination reason: Instruction limit % 33.23/6.56 % (70434)Termination phase: SInE selection % 33.23/6.56 % (70434)Time elapsed: 0.247 s % 33.23/6.56 % (70434)Peak memory usage: 173 MB % 33.23/6.56 % (70434)Instructions burned: 326 (million) % 33.23/6.56 % (70440)Instruction limit reached! % 33.23/6.56 % (70440)------------------------------ % 33.23/6.56 % (70440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.23/6.56 % (70440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.23/6.56 % (70440)CaDiCaL version: 2.1.3 % 33.23/6.56 % (70440)Termination reason: Instruction limit % 33.23/6.56 % (70440)Termination phase: SInE selection % 33.23/6.56 % (70440)Time elapsed: 0.117 s % 33.23/6.56 % (70440)Peak memory usage: 173 MB % 33.23/6.56 % (70440)Instructions burned: 296 (million) % 33.23/6.56 % (70442)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2096325584:cts=off:i=113:fsr=off:ss=included:sgt=4_2978 on theBenchmark for (2978ds/113Mi) % 33.23/6.56 % (70445)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=761347313:i=127:av=off:fsr=off:sup=off_2976 on theBenchmark for (2976ds/127Mi) % 33.23/6.56 % (70442)Instruction limit reached! % 33.23/6.56 % (70442)------------------------------ % 33.23/6.56 % (70442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.23/6.56 % (70442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.23/6.56 % (70442)CaDiCaL version: 2.1.3 % 33.23/6.56 % (70442)Termination reason: Instruction limit % 33.23/6.56 % (70442)Termination phase: SInE selection % 33.23/6.56 % (70442)Time elapsed: 0.092 s % 33.23/6.56 % (70442)Peak memory usage: 172 MB % 33.23/6.56 % (70442)Instructions burned: 114 (million) % 33.23/6.56 % (70446)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2283705490:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2976 on theBenchmark for (2976ds/114Mi) % 33.23/6.56 % (70446)Instruction limit reached! % 33.23/6.56 % (70446)------------------------------ % 33.23/6.56 % (70446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.23/6.56 % (70446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.23/6.56 % (70446)CaDiCaL version: 2.1.3 % 33.23/6.56 % (70446)Termination reason: Instruction limit % 33.23/6.56 % (70446)Termination phase: Property scanning % 67.24/11.31 % (70446)Time elapsed: 0.031 s % 67.24/11.31 % (70446)Peak memory usage: 173 MB % 67.24/11.31 % (70446)Instructions burned: 116 (million) % 67.24/11.31 % (70445)Instruction limit reached! % 67.24/11.31 % (70445)------------------------------ % 67.24/11.31 % (70445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/11.31 % (70445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/11.31 % (70445)CaDiCaL version: 2.1.3 % 67.24/11.31 % (70445)Termination reason: Instruction limit % 67.24/11.31 % (70445)Termination phase: Preprocessing 1 % 67.24/11.31 % (70445)Time elapsed: 0.098 s % 67.24/11.31 % (70445)Peak memory usage: 174 MB % 67.24/11.31 % (70445)Instructions burned: 128 (million) % 67.24/11.31 % (70450)lrs+10_1_sil=8000:sp=occurrence:random_seed=1548384364:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2975 on theBenchmark for (2975ds/907Mi) % 67.24/11.31 % (70451)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=743863319:i=437:sd=1:aac=none:ss=included_2975 on theBenchmark for (2975ds/437Mi) % 67.24/11.31 % (70452)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1944372597:i=5202:ss=axioms:sgt=16_2974 on theBenchmark for (2974ds/5202Mi) % 67.24/11.31 % (70451)Instruction limit reached! % 67.24/11.31 % (70451)------------------------------ % 67.24/11.31 % (70451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/11.31 % (70451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/11.31 % (70451)CaDiCaL version: 2.1.3 % 67.24/11.31 % (70451)Termination reason: Instruction limit % 67.24/11.31 % (70451)Termination phase: Clausification % 67.24/11.31 % (70451)Time elapsed: 0.200 s % 67.24/11.31 % (70451)Peak memory usage: 176 MB % 67.24/11.31 % (70451)Instructions burned: 437 (million) % 67.24/11.31 % (70456)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2574876234:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2971 on theBenchmark for (2971ds/134Mi) % 67.24/11.31 % (70456)Instruction limit reached! % 67.24/11.31 % (70456)------------------------------ % 67.24/11.31 % (70456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/11.31 % (70456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/11.31 % (70456)CaDiCaL version: 2.1.3 % 67.24/11.31 % (70456)Termination reason: Instruction limit % 67.24/11.31 % (70456)Termination phase: SInE selection % 67.24/11.31 % (70456)Time elapsed: 0.060 s % 67.24/11.31 % (70456)Peak memory usage: 172 MB % 67.24/11.31 % (70456)Instructions burned: 136 (million) % 67.24/11.31 % (70458)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2034810616:st=8:i=592:sd=3:ep=RST:ss=axioms_2969 on theBenchmark for (2969ds/592Mi) % 67.24/11.31 % (70450)Instruction limit reached! % 67.24/11.31 % (70450)------------------------------ % 67.24/11.31 % (70450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/11.31 % (70450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/11.31 % (70450)CaDiCaL version: 2.1.3 % 67.24/11.31 % (70450)Termination reason: Instruction limit % 67.24/11.31 % (70450)Termination phase: Property scanning % 67.24/11.31 % (70450)Time elapsed: 0.620 s % 67.24/11.31 % (70450)Peak memory usage: 182 MB % 67.24/11.31 % (70450)Instructions burned: 908 (million) % 67.24/11.31 % (70460)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=422693294:st=3:i=13193:sd=3:ss=axioms_2967 on theBenchmark for (2967ds/13193Mi) % 67.24/11.31 % (70458)Instruction limit reached! % 67.24/11.31 % (70458)------------------------------ % 67.24/11.31 % (70458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/11.31 % (70458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/11.31 % (70458)CaDiCaL version: 2.1.3 % 67.24/11.31 % (70458)Termination reason: Instruction limit % 67.24/11.31 % (70458)Termination phase: SInE selection % 67.24/11.31 % (70458)Time elapsed: 0.380 s % 67.24/11.31 % (70458)Peak memory usage: 174 MB % 67.24/11.31 % (70458)Instructions burned: 592 (million) % 67.24/11.31 % (70462)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1972906162:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/125Mi) % 67.24/11.31 % (70462)Instruction limit reached! % 67.24/11.31 % (70462)------------------------------ % 67.24/11.31 % (70462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/11.31 % (70462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.78/15.67 % (70462)CaDiCaL version: 2.1.3 % 97.78/15.67 % (70462)Termination reason: Instruction limit % 97.78/15.67 % (70462)Termination phase: Property scanning % 97.78/15.67 % (70462)Time elapsed: 0.060 s % 97.78/15.67 % (70462)Peak memory usage: 173 MB % 97.78/15.67 % (70462)Instructions burned: 126 (million) % 97.78/15.67 % (70441)Instruction limit reached! % 97.78/15.67 % (70441)------------------------------ % 97.78/15.67 % (70441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.78/15.67 % (70441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.78/15.67 % (70441)CaDiCaL version: 2.1.3 % 97.78/15.67 % (70441)Termination reason: Instruction limit % 97.78/15.67 % (70441)Termination phase: Preprocessing 3 % 97.78/15.67 % (70441)Time elapsed: 1.687 s % 97.78/15.67 % (70441)Peak memory usage: 276 MB % 97.78/15.67 % (70441)Instructions burned: 2351 (million) % 97.78/15.67 % (70464)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2677011788:i=134:gtgl=5:slsql=off:gtg=exists_sym_2961 on theBenchmark for (2961ds/134Mi) % 97.78/15.67 % (70464)Instruction limit reached! % 97.78/15.67 % (70464)------------------------------ % 97.78/15.67 % (70464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.78/15.67 % (70464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.78/15.67 % (70464)CaDiCaL version: 2.1.3 % 97.78/15.67 % (70464)Termination reason: Instruction limit % 97.78/15.67 % (70464)Termination phase: Property scanning % 97.78/15.67 % (70464)Time elapsed: 0.063 s % 97.78/15.67 % (70464)Peak memory usage: 173 MB % 97.78/15.67 % (70464)Instructions burned: 135 (million) % 97.78/15.67 % (70466)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1405206830:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2959 on theBenchmark for (2959ds/141Mi) % 97.78/15.67 % (70467)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3897738246:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2959 on theBenchmark for (2959ds/431Mi) % 97.78/15.67 % (70466)Instruction limit reached! % 97.78/15.67 % (70466)------------------------------ % 97.78/15.67 % (70466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.78/15.67 % (70466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.78/15.67 % (70466)CaDiCaL version: 2.1.3 % 97.78/15.67 % (70466)Termination reason: Instruction limit % 97.78/15.67 % (70466)Termination phase: SInE selection % 97.78/15.67 % (70466)Time elapsed: 0.113 s % 97.78/15.67 % (70466)Peak memory usage: 173 MB % 97.78/15.67 % (70466)Instructions burned: 141 (million) % 97.78/15.67 % (70470)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1851901822:i=6060:aac=none:ins=25_2957 on theBenchmark for (2957ds/6060Mi) % 97.78/15.67 % (70467)Instruction limit reached! % 97.78/15.67 % (70467)------------------------------ % 97.78/15.67 % (70467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.78/15.67 % (70467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.78/15.67 % (70467)CaDiCaL version: 2.1.3 % 97.78/15.67 % (70467)Termination reason: Instruction limit % 97.78/15.67 % (70467)Termination phase: Preprocessing 3 % 97.78/15.67 % (70467)Time elapsed: 0.341 s % 97.78/15.67 % (70467)Peak memory usage: 177 MB % 97.78/15.67 % (70467)Instructions burned: 431 (million) % 97.78/15.67 % (70472)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3675492144:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2954 on theBenchmark for (2954ds/150Mi) % 97.78/15.67 % (70472)Instruction limit reached! % 97.78/15.67 % (70472)------------------------------ % 97.78/15.67 % (70472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.78/15.67 % (70472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.78/15.67 % (70472)CaDiCaL version: 2.1.3 % 97.78/15.67 % (70472)Termination reason: Instruction limit % 97.78/15.67 % (70472)Termination phase: SInE selection % 97.78/15.67 % (70472)Time elapsed: 0.115 s % 97.78/15.67 % (70472)Peak memory usage: 173 MB % 97.78/15.67 % (70472)Instructions burned: 150 (million) % 97.78/15.67 % (70474)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=584263223:i=14155:bd=all_2951 on theBenchmark for (2951ds/14155Mi) % 97.78/15.67 % (70452)Instruction limit reached! % 97.78/15.67 % (70452)------------------------------ % 97.78/15.67 % (70452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.91/19.75 % (70452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/19.75 % (70452)CaDiCaL version: 2.1.3 % 126.91/19.75 % (70452)Termination reason: Instruction limit % 126.91/19.75 % (70452)Termination phase: Saturation % 126.91/19.75 % (70452)Time elapsed: 3.388 s % 126.91/19.75 % (70452)Peak memory usage: 299 MB % 126.91/19.75 % (70452)Instructions burned: 5202 (million) % 126.91/19.75 % (70476)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2843193593:i=667:av=off:fsr=off_2938 on theBenchmark for (2938ds/667Mi) % 126.91/19.75 % (70476)Instruction limit reached! % 126.91/19.75 % (70476)------------------------------ % 126.91/19.75 % (70476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.91/19.75 % (70476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/19.75 % (70476)CaDiCaL version: 2.1.3 % 126.91/19.75 % (70476)Termination reason: Instruction limit % 126.91/19.75 % (70476)Termination phase: Preprocessing 2 % 126.91/19.75 % (70476)Time elapsed: 0.586 s % 126.91/19.75 % (70476)Peak memory usage: 215 MB % 126.91/19.75 % (70476)Instructions burned: 668 (million) % 126.91/19.75 % (70478)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=749488096:s2a=on:i=185:s2at=1.8:fdi=4_2930 on theBenchmark for (2930ds/185Mi) % 126.91/19.75 % (70478)Instruction limit reached! % 126.91/19.75 % (70478)------------------------------ % 126.91/19.75 % (70478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.91/19.75 % (70478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/19.75 % (70478)CaDiCaL version: 2.1.3 % 126.91/19.75 % (70478)Termination reason: Instruction limit % 126.91/19.75 % (70478)Termination phase: SInE selection % 126.91/19.75 % (70478)Time elapsed: 0.140 s % 126.91/19.75 % (70478)Peak memory usage: 172 MB % 126.91/19.75 % (70478)Instructions burned: 185 (million) % 126.91/19.75 % (70480)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=854391859:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2927 on theBenchmark for (2927ds/193Mi) % 126.91/19.75 % (70480)Instruction limit reached! % 126.91/19.75 % (70480)------------------------------ % 126.91/19.75 % (70480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.91/19.75 % (70480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/19.75 % (70480)CaDiCaL version: 2.1.3 % 126.91/19.75 % (70480)Termination reason: Instruction limit % 126.91/19.75 % (70480)Termination phase: SInE selection % 126.91/19.75 % (70480)Time elapsed: 0.152 s % 126.91/19.75 % (70480)Peak memory usage: 172 MB % 126.91/19.75 % (70480)Instructions burned: 193 (million) % 126.91/19.75 % (70482)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1770858243:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2924 on theBenchmark for (2924ds/4850Mi) % 126.91/19.75 % (70470)Instruction limit reached! % 126.91/19.75 % (70470)------------------------------ % 126.91/19.75 % (70470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.91/19.75 % (70470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/19.75 % (70470)CaDiCaL version: 2.1.3 % 126.91/19.75 % (70470)Termination reason: Instruction limit % 126.91/19.75 % (70470)Termination phase: NewCNF % 126.91/19.75 % (70470)Time elapsed: 4.876 s % 126.91/19.75 % (70470)Peak memory usage: 330 MB % 126.91/19.75 % (70470)Instructions burned: 6060 (million) % 126.91/19.75 % (70484)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2722943219:i=12111:sd=1:ss=included_2906 on theBenchmark for (2906ds/12111Mi) % 126.91/19.75 % (70482)Instruction limit reached! % 126.91/19.75 % (70482)------------------------------ % 126.91/19.75 % (70482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.91/19.75 % (70482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.91/19.75 % (70482)CaDiCaL version: 2.1.3 % 126.91/19.75 % (70482)Termination reason: Instruction limit % 126.91/19.75 % (70482)Termination phase: Function definition elimination % 126.91/19.75 % (70482)Time elapsed: 2.712 s % 126.91/19.75 % (70482)Peak memory usage: 266 MB % 126.91/19.75 % (70482)Instructions burned: 4853 (million) % 126.91/19.75 % (70486)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=455283759:i=319:kws=precedence:fsr=off_2895 on theBenchmark for (2895ds/319Mi) % 126.91/19.75 % (70486)Instruction limit reached! % 126.91/19.75 % (70486)------------------------------ % 126.91/19.75 % (70486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.75/25.10 % (70486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.75/25.10 % (70486)CaDiCaL version: 2.1.3 % 164.75/25.10 % (70486)Termination reason: Instruction limit % 164.75/25.10 % (70486)Termination phase: Preprocessing 1 % 164.75/25.10 % (70486)Time elapsed: 0.234 s % 164.75/25.10 % (70486)Peak memory usage: 175 MB % 164.75/25.10 % (70486)Instructions burned: 321 (million) % 164.75/25.10 % (70488)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=522047868:i=2064:ep=RST_2891 on theBenchmark for (2891ds/2064Mi) % 164.75/25.10 % (70460)Instruction limit reached! % 164.75/25.10 % (70460)------------------------------ % 164.75/25.10 % (70460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.75/25.10 % (70460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.75/25.10 % (70460)CaDiCaL version: 2.1.3 % 164.75/25.10 % (70460)Termination reason: Instruction limit % 164.75/25.10 % (70460)Termination phase: Saturation % 164.75/25.10 % (70460)Time elapsed: 7.759 s % 164.75/25.10 % (70460)Peak memory usage: 545 MB % 164.75/25.10 % (70460)Instructions burned: 13194 (million) % 164.75/25.10 % (70490)dis-1011_128_sil=32000:random_seed=2324717267:i=3706:ep=RST:av=off_2887 on theBenchmark for (2887ds/3706Mi) % 164.75/25.10 % (70488)Instruction limit reached! % 164.75/25.10 % (70488)------------------------------ % 164.75/25.10 % (70488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.75/25.10 % (70488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.75/25.10 % (70488)CaDiCaL version: 2.1.3 % 164.75/25.10 % (70488)Termination reason: Instruction limit % 164.75/25.10 % (70488)Termination phase: Preprocessing 3 % 164.75/25.10 % (70488)Time elapsed: 1.433 s % 164.75/25.10 % (70488)Peak memory usage: 280 MB % 164.75/25.10 % (70488)Instructions burned: 2065 (million) % 164.75/25.10 % (70474)Instruction limit reached! % 164.75/25.10 % (70474)------------------------------ % 164.75/25.10 % (70474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.75/25.10 % (70474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.75/25.10 % (70474)CaDiCaL version: 2.1.3 % 164.75/25.10 % (70474)Termination reason: Instruction limit % 164.75/25.10 % (70474)Termination phase: Saturation % 164.75/25.10 % (70474)Time elapsed: 7.599 s % 164.75/25.10 % (70474)Peak memory usage: 804 MB % 164.75/25.10 % (70474)Instructions burned: 14155 (million) % 164.75/25.10 % (70492)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3000381623:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2874 on theBenchmark for (2874ds/757Mi) % 164.75/25.10 % (70494)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2981033159:i=13913:ss=axioms:sgt=8_2872 on theBenchmark for (2872ds/13913Mi) % 164.75/25.10 % (70492)Instruction limit reached! % 164.75/25.10 % (70492)------------------------------ % 164.75/25.10 % (70492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.75/25.10 % (70492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.75/25.10 % (70492)CaDiCaL version: 2.1.3 % 164.75/25.10 % (70492)Termination reason: Instruction limit % 164.75/25.10 % (70492)Termination phase: Saturation % 164.75/25.10 % (70492)Time elapsed: 0.604 s % 164.75/25.10 % (70492)Peak memory usage: 183 MB % 164.75/25.10 % (70492)Instructions burned: 758 (million) % 164.75/25.10 % (70496)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2220247791:i=9925:aac=none_2866 on theBenchmark for (2866ds/9925Mi) % 164.75/25.10 % (70490)Instruction limit reached! % 164.75/25.10 % (70490)------------------------------ % 164.75/25.10 % (70490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.75/25.10 % (70490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.75/25.10 % (70490)CaDiCaL version: 2.1.3 % 164.75/25.10 % (70490)Termination reason: Instruction limit % 164.75/25.10 % (70490)Termination phase: Property scanning % 164.75/25.10 % (70490)Time elapsed: 2.411 s % 164.75/25.10 % (70490)Peak memory usage: 336 MB % 164.75/25.10 % (70490)Instructions burned: 3707 (million) % 164.75/25.10 % (70498)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=640630483:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2861 on theBenchmark for (2861ds/2479Mi) % 164.75/25.10 % (70484)Instruction limit reached! % 164.75/25.10 % (70484)------------------------------ % 164.75/25.10 % (70484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.88/31.99 % (70484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.88/31.99 % (70484)CaDiCaL version: 2.1.3 % 209.88/31.99 % (70484)Termination reason: Instruction limit % 209.88/31.99 % (70484)Termination phase: Saturation % 209.88/31.99 % (70484)Time elapsed: 5.674 s % 209.88/31.99 % (70484)Peak memory usage: 249 MB % 209.88/31.99 % (70484)Instructions burned: 12115 (million) % 209.88/31.99 % (70500)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2758370587:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2847 on theBenchmark for (2847ds/440Mi) % 209.88/31.99 % (70500)Instruction limit reached! % 209.88/31.99 % (70500)------------------------------ % 209.88/31.99 % (70500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.88/31.99 % (70500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.88/31.99 % (70500)CaDiCaL version: 2.1.3 % 209.88/31.99 % (70500)Termination reason: Instruction limit % 209.88/31.99 % (70500)Termination phase: Property scanning % 209.88/31.99 % (70500)Time elapsed: 0.187 s % 209.88/31.99 % (70500)Peak memory usage: 173 MB % 209.88/31.99 % (70500)Instructions burned: 441 (million) % 209.88/31.99 % (70498)Instruction limit reached! % 209.88/31.99 % (70498)------------------------------ % 209.88/31.99 % (70498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.88/31.99 % (70498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.88/31.99 % (70498)CaDiCaL version: 2.1.3 % 209.88/31.99 % (70498)Termination reason: Instruction limit % 209.88/31.99 % (70498)Termination phase: Saturation % 209.88/31.99 % (70498)Time elapsed: 1.631 s % 209.88/31.99 % (70498)Peak memory usage: 194 MB % 209.88/31.99 % (70498)Instructions burned: 2480 (million) % 209.88/31.99 % (70502)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=339663430:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2843 on theBenchmark for (2843ds/11145Mi) % 209.88/31.99 % (70503)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3014295464:cts=off:i=3034:av=off:er=known:fsd=on_2843 on theBenchmark for (2843ds/3034Mi) % 209.88/31.99 % (70503)Instruction limit reached! % 209.88/31.99 % (70503)------------------------------ % 209.88/31.99 % (70503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.88/31.99 % (70503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.88/31.99 % (70503)CaDiCaL version: 2.1.3 % 209.88/31.99 % (70503)Termination reason: Instruction limit % 209.88/31.99 % (70503)Termination phase: Preprocessing 3 % 209.88/31.99 % (70503)Time elapsed: 2.076 s % 209.88/31.99 % (70503)Peak memory usage: 306 MB % 209.88/31.99 % (70503)Instructions burned: 3036 (million) % 209.88/31.99 % (70506)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3097109529:st=2:s2a=on:i=524:s2at=2:ss=axioms_2820 on theBenchmark for (2820ds/524Mi) % 209.88/31.99 % (70506)Instruction limit reached! % 209.88/31.99 % (70506)------------------------------ % 209.88/31.99 % (70506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.88/31.99 % (70506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.88/31.99 % (70506)CaDiCaL version: 2.1.3 % 209.88/31.99 % (70506)Termination reason: Instruction limit % 209.88/31.99 % (70506)Termination phase: SInE selection % 209.88/31.99 % (70506)Time elapsed: 0.342 s % 209.88/31.99 % (70506)Peak memory usage: 173 MB % 209.88/31.99 % (70506)Instructions burned: 525 (million) % 209.88/31.99 % (70496)Instruction limit reached! % 209.88/31.99 % (70496)------------------------------ % 209.88/31.99 % (70496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.88/31.99 % (70496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.88/31.99 % (70496)CaDiCaL version: 2.1.3 % 209.88/31.99 % (70496)Termination reason: Instruction limit % 209.88/31.99 % (70496)Termination phase: Property scanning % 209.88/31.99 % (70496)Time elapsed: 4.994 s % 209.88/31.99 % (70496)Peak memory usage: 358 MB % 209.88/31.99 % (70496)Instructions burned: 9926 (million) % 209.88/31.99 % (70508)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=889720172:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2815 on theBenchmark for (2815ds/1016Mi) % 209.88/31.99 % (70509)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3391318439:i=14123:bd=preordered:ins=4_2814 on theBenchmark for (2814ds/14123Mi) % 209.88/31.99 % (70508)Instruction limit reached! % 209.88/31.99 % (70508)------------------------------ % 209.88/31.99 % (70508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.40/39.25 % (70508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.40/39.25 % (70508)CaDiCaL version: 2.1.3 % 265.40/39.25 % (70508)Termination reason: Instruction limit % 265.40/39.25 % (70508)Termination phase: Saturation % 265.40/39.25 % (70508)Time elapsed: 0.698 s % 265.40/39.25 % (70508)Peak memory usage: 186 MB % 265.40/39.25 % (70508)Instructions burned: 1016 (million) % 265.40/39.25 % (70512)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=932191215:i=5781:kws=precedence:bd=all:rawr=on_2806 on theBenchmark for (2806ds/5781Mi) % 265.40/39.25 % (70494)Instruction limit reached! % 265.40/39.25 % (70494)------------------------------ % 265.40/39.25 % (70494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.40/39.25 % (70494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.40/39.25 % (70494)CaDiCaL version: 2.1.3 % 265.40/39.25 % (70494)Termination reason: Instruction limit % 265.40/39.25 % (70494)Termination phase: Saturation % 265.40/39.25 % (70494)Time elapsed: 9.193 s % 265.40/39.25 % (70494)Peak memory usage: 324 MB % 265.40/39.25 % (70494)Instructions burned: 13913 (million) % 265.40/39.25 % (70514)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1105482882:i=2448:gtgl=5:bd=preordered:gtg=all_2778 on theBenchmark for (2778ds/2448Mi) % 265.40/39.25 % (70502)Instruction limit reached! % 265.40/39.25 % (70502)------------------------------ % 265.40/39.25 % (70502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.40/39.25 % (70502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.40/39.25 % (70502)CaDiCaL version: 2.1.3 % 265.40/39.25 % (70502)Termination reason: Instruction limit % 265.40/39.25 % (70502)Termination phase: Saturation % 265.40/39.25 % (70502)Time elapsed: 6.965 s % 265.40/39.25 % (70502)Peak memory usage: 328 MB % 265.40/39.25 % (70502)Instructions burned: 11145 (million) % 265.40/39.25 % (70512)Instruction limit reached! % 265.40/39.25 % (70512)------------------------------ % 265.40/39.25 % (70512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.40/39.25 % (70512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.40/39.25 % (70512)CaDiCaL version: 2.1.3 % 265.40/39.25 % (70512)Termination reason: Instruction limit % 265.40/39.25 % (70512)Termination phase: Function definition elimination % 265.40/39.25 % (70512)Time elapsed: 3.334 s % 265.40/39.25 % (70512)Peak memory usage: 339 MB % 265.40/39.25 % (70512)Instructions burned: 5781 (million) % 265.40/39.25 % (70516)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=596493777:i=3223:kws=precedence:fgj=on:av=off_2772 on theBenchmark for (2772ds/3223Mi) % 265.40/39.25 % (70517)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3926120513:st=5.6:i=2033:sd=3:ss=axioms_2771 on theBenchmark for (2771ds/2033Mi) % 265.40/39.25 % (70514)Instruction limit reached! % 265.40/39.25 % (70514)------------------------------ % 265.40/39.25 % (70514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.40/39.25 % (70514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.40/39.25 % (70514)CaDiCaL version: 2.1.3 % 265.40/39.25 % (70514)Termination reason: Instruction limit % 265.40/39.25 % (70514)Termination phase: Property scanning % 265.40/39.25 % (70514)Time elapsed: 1.022 s % 265.40/39.25 % (70514)Peak memory usage: 173 MB % 265.40/39.25 % (70514)Instructions burned: 2449 (million) % 265.40/39.25 % (70520)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1100441810:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2766 on theBenchmark for (2766ds/2055Mi) % 265.40/39.25 % (70517)Instruction limit reached! % 265.40/39.25 % (70517)------------------------------ % 265.40/39.25 % (70517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.40/39.25 % (70517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.40/39.25 % (70517)CaDiCaL version: 2.1.3 % 265.40/39.25 % (70517)Termination reason: Instruction limit % 265.40/39.25 % (70517)Termination phase: Clausification % 265.40/39.25 % (70517)Time elapsed: 1.437 s % 265.40/39.25 % (70517)Peak memory usage: 218 MB % 265.40/39.25 % (70517)Instructions burned: 2033 (million) % 265.40/39.25 % (70522)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=76090537:i=21611:sd=3:ss=axioms_2755 on theBenchmark for (2755ds/21611Mi) % 300.40/44.17 % (70520)Instruction limit reached! % 300.40/44.17 % (70520)------------------------------ % 300.40/44.17 % (70520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.40/44.17 % (70520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/44.17 % (70520)CaDiCaL version: 2.1.3 % 300.40/44.17 % (70520)Termination reason: Instruction limit % 300.40/44.17 % (70520)Termination phase: Preprocessing 3 % 300.40/44.17 % (70520)Time elapsed: 1.169 s % 300.40/44.17 % (70520)Peak memory usage: 178 MB % 300.40/44.17 % (70520)Instructions burned: 2056 (million) % 300.40/44.17 % (70524)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3620911736:i=4835:sd=13:ss=axioms:sgt=23_2753 on theBenchmark for (2753ds/4835Mi) % 300.40/44.17 % (70516)Instruction limit reached! % 300.40/44.17 % (70516)------------------------------ % 300.40/44.17 % (70516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.40/44.17 % (70516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/44.17 % (70516)CaDiCaL version: 2.1.3 % 300.40/44.17 % (70516)Termination reason: Instruction limit % 300.40/44.17 % (70516)Termination phase: Preprocessing 3 % 300.40/44.17 % (70516)Time elapsed: 2.235 s % 300.40/44.17 % (70516)Peak memory usage: 311 MB % 300.40/44.17 % (70516)Instructions burned: 3224 (million) % 300.40/44.17 % (70526)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=4232183749:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2747 on theBenchmark for (2747ds/797Mi) % 300.40/44.17 % (70526)Instruction limit reached! % 300.40/44.17 % (70526)------------------------------ % 300.40/44.17 % (70526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.40/44.17 % (70526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/44.17 % (70526)CaDiCaL version: 2.1.3 % 300.40/44.17 % (70526)Termination reason: Instruction limit % 300.40/44.17 % (70526)Termination phase: SInE selection % 300.40/44.17 % (70526)Time elapsed: 0.614 s % 300.40/44.17 % (70526)Peak memory usage: 175 MB % 300.40/44.17 % (70526)Instructions burned: 797 (million) % 300.40/44.17 % (70528)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1948562047:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2739 on theBenchmark for (2739ds/2326Mi) % 300.40/44.17 % (70528)Instruction limit reached! % 300.40/44.17 % (70528)------------------------------ % 300.40/44.17 % (70528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.40/44.17 % (70528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/44.17 % (70528)CaDiCaL version: 2.1.3 % 300.40/44.17 % (70528)Termination reason: Instruction limit % 300.40/44.17 % (70528)Termination phase: Preprocessing 3 % 300.40/44.17 % (70528)Time elapsed: 1.599 s % 300.40/44.17 % (70528)Peak memory usage: 287 MB % 300.40/44.17 % (70528)Instructions burned: 2327 (million) % 300.40/44.17 % (70524)Instruction limit reached! % 300.40/44.17 % (70524)------------------------------ % 300.40/44.17 % (70524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.40/44.17 % (70524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/44.17 % (70524)CaDiCaL version: 2.1.3 % 300.40/44.17 % (70524)Termination reason: Instruction limit % 300.40/44.17 % (70524)Termination phase: Saturation % 300.40/44.17 % (70524)Time elapsed: 3.053 s % 300.40/44.17 % (70524)Peak memory usage: 223 MB % 300.40/44.17 % (70524)Instructions burned: 4835 (million) % 300.40/44.17 % (70530)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3240804858:i=6038:nm=6_2721 on theBenchmark for (2721ds/6038Mi) % 300.40/44.17 % (70531)lrs+10_1_sil=32000:sp=occurrence:random_seed=1359131165:st=2:i=33334:sd=3:ss=included:sgt=32_2720 on theBenchmark for (2720ds/33334Mi) % 300.40/44.17 % (70530)Instruction limit reached! % 300.40/44.17 % (70530)------------------------------ % 300.40/44.17 % (70530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.40/44.17 % (70530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.40/44.17 % (70530)CaDiCaL version: 2.1.3 % 300.40/44.17 % (70530)Termination reason: Instruction limit % 300.40/44.17 % (70530)Termination phase: Function definition elimination % 300.40/44.17 % (70530)Time elapsed: 3.479 s % 300.40/44.17 % (70530)Peak memory usage: 343 MB % 300.40/44.17 % (70530)Instructions burned: 6040 (million) % 300.40/44.17 % (70509)Instruction limit reached! % 300.40/44.17 % (70509)------------------------------ % 300.40/44.17 % (70509)Versio % 300.40/44.17 Terminated %------------------------------------------------------------------------------