%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV605-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n008.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 01:19:05 PM UTC 2026 % Result : Timeout 300.56s 43.07s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV605-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.19 % Computer : n008.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 12:01:10 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.23 Running first-order theorem proving % 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 7.37/2.00 % (2203264)Input is clausal, will run a generic CNF schedule. % 7.37/2.00 % (2203273)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=321707963:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 7.37/2.00 % (2203269)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=113719363:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 7.37/2.00 % (2203270)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=566749860:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 7.37/2.00 % (2203271)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2777812429:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 7.37/2.00 % (2203274)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3548805999:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 7.37/2.00 % (2203272)lrs+10_1_sil=8000:sp=occurrence:random_seed=2066118334:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 7.37/2.00 % (2203275)dis-21_1_sil=8000:lcm=predicate:random_seed=3288430371:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 7.37/2.00 % (2203273)Instruction limit reached! % 7.37/2.00 % (2203273)------------------------------ % 7.37/2.00 % (2203273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.37/2.00 % (2203273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/2.00 % (2203273)CaDiCaL version: 2.1.3 % 7.37/2.00 % (2203273)Termination reason: Instruction limit % 7.37/2.00 % (2203273)Termination phase: Saturation % 7.37/2.00 % (2203273)Time elapsed: 0.040 s % 7.37/2.00 % (2203273)Peak memory usage: 89 MB % 7.37/2.00 % (2203273)Instructions burned: 116 (million) % 7.37/2.00 % (2203275)Instruction limit reached! % 7.37/2.00 % (2203275)------------------------------ % 7.37/2.00 % (2203275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.37/2.00 % (2203275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/2.00 % (2203275)CaDiCaL version: 2.1.3 % 7.37/2.00 % (2203275)Termination reason: Instruction limit % 7.37/2.00 % (2203275)Termination phase: Saturation % 7.37/2.00 % (2203275)Time elapsed: 0.058 s % 7.37/2.00 % (2203275)Peak memory usage: 89 MB % 7.37/2.00 % (2203275)Instructions burned: 118 (million) % 7.37/2.00 % (2203272)Instruction limit reached! % 7.37/2.00 % (2203272)------------------------------ % 7.37/2.00 % (2203272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.37/2.00 % (2203272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/2.00 % (2203272)CaDiCaL version: 2.1.3 % 7.37/2.00 % (2203272)Termination reason: Instruction limit % 7.37/2.00 % (2203272)Termination phase: Saturation % 7.37/2.00 % (2203272)Time elapsed: 0.066 s % 7.37/2.00 % (2203272)Peak memory usage: 90 MB % 7.37/2.00 % (2203272)Instructions burned: 107 (million) % 7.37/2.00 % (2203283)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=3265909226:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 7.37/2.00 % (2203283)Refutation not found, incomplete strategy % 7.37/2.00 % (2203283)------------------------------ % 7.37/2.00 % (2203283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.37/2.00 % (2203283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/2.00 % (2203283)CaDiCaL version: 2.1.3 % 7.37/2.00 % (2203283)Termination reason: Refutation not found, incomplete strategy % 7.37/2.00 % (2203283)Time elapsed: 0.011 s % 7.37/2.00 % (2203283)Peak memory usage: 89 MB % 7.37/2.00 % (2203283)Instructions burned: 36 (million) % 7.37/2.00 % (2203274)Instruction limit reached! % 7.37/2.00 % (2203274)------------------------------ % 7.37/2.00 % (2203274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.37/2.00 % (2203274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.37/2.00 % (2203274)CaDiCaL version: 2.1.3 % 7.37/2.00 % (2203274)Termination reason: Instruction limit % 7.37/2.00 % (2203274)Termination phase: Saturation % 7.37/2.00 % (2203274)Time elapsed: 0.117 s % 7.37/2.00 % (2203274)Peak memory usage: 90 MB % 7.37/2.00 % (2203274)Instructions burned: 180 (million) % 7.37/2.00 % (2203284)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2855066026:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi) % 21.96/3.87 % (2203285)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=612431917:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 21.96/3.87 % (2203283)------------------------------ % 21.96/3.87 % (2203283)------------------------------ % 21.96/3.87 % (2203287)lrs+10_64_to=lpo:sil=8000:random_seed=2856038842:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 21.96/3.87 % (2203284)Instruction limit reached! % 21.96/3.87 % (2203284)------------------------------ % 21.96/3.87 % (2203284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.87 % (2203284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.87 % (2203284)CaDiCaL version: 2.1.3 % 21.96/3.87 % (2203284)Termination reason: Instruction limit % 21.96/3.87 % (2203284)Termination phase: Saturation % 21.96/3.87 % (2203284)Time elapsed: 0.098 s % 21.96/3.87 % (2203284)Peak memory usage: 91 MB % 21.96/3.87 % (2203284)Instructions burned: 190 (million) % 21.96/3.87 % (2203287)Instruction limit reached! % 21.96/3.87 % (2203287)------------------------------ % 21.96/3.87 % (2203287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.87 % (2203287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.87 % (2203287)CaDiCaL version: 2.1.3 % 21.96/3.87 % (2203287)Termination reason: Instruction limit % 21.96/3.87 % (2203287)Termination phase: Saturation % 21.96/3.87 % (2203287)Time elapsed: 0.074 s % 21.96/3.87 % (2203287)Peak memory usage: 90 MB % 21.96/3.87 % (2203287)Instructions burned: 127 (million) % 21.96/3.87 % (2203285)Instruction limit reached! % 21.96/3.87 % (2203285)------------------------------ % 21.96/3.87 % (2203285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.87 % (2203285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.87 % (2203285)CaDiCaL version: 2.1.3 % 21.96/3.87 % (2203285)Termination reason: Instruction limit % 21.96/3.87 % (2203285)Termination phase: Saturation % 21.96/3.87 % (2203285)Time elapsed: 0.125 s % 21.96/3.87 % (2203285)Peak memory usage: 91 MB % 21.96/3.87 % (2203285)Instructions burned: 219 (million) % 21.96/3.87 % (2203291)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3140123754:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 21.96/3.87 % (2203291)Instruction limit reached! % 21.96/3.87 % (2203291)------------------------------ % 21.96/3.87 % (2203291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.87 % (2203291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.87 % (2203291)CaDiCaL version: 2.1.3 % 21.96/3.87 % (2203291)Termination reason: Instruction limit % 21.96/3.87 % (2203291)Termination phase: Saturation % 21.96/3.87 % (2203291)Time elapsed: 0.066 s % 21.96/3.87 % (2203291)Peak memory usage: 91 MB % 21.96/3.87 % (2203291)Instructions burned: 194 (million) % 21.96/3.87 % (2203292)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=331815605:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 21.96/3.87 % (2203295)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=3656326359:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 21.96/3.87 % (2203293)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=752392946:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 21.96/3.87 % (2203296)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=999874873:i=107_2993 on theBenchmark for (2993ds/107Mi) % 21.96/3.87 % (2203292)Instruction limit reached! % 21.96/3.87 % (2203292)------------------------------ % 21.96/3.87 % (2203292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.96/3.87 % (2203292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.96/3.87 % (2203292)CaDiCaL version: 2.1.3 % 21.96/3.87 % (2203292)Termination reason: Instruction limit % 21.96/3.87 % (2203292)Termination phase: Saturation % 21.96/3.87 % (2203292)Time elapsed: 0.092 s % 21.96/3.87 % (2203292)Peak memory usage: 91 MB % 21.96/3.87 % (2203292)Instructions burned: 157 (million) % 21.96/3.87 % (2203295)Instruction limit reached! % 21.96/3.87 % (2203295)------------------------------ % 32.24/5.26 % (2203295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.24/5.26 % (2203296)Refutation not found, incomplete strategy % 32.24/5.26 % (2203296)------------------------------ % 32.24/5.26 % (2203296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.24/5.26 % (2203295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.24/5.26 % (2203296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.24/5.26 % (2203296)CaDiCaL version: 2.1.3 % 32.24/5.26 % (2203296)Termination reason: Refutation not found, incomplete strategy % 32.24/5.26 % (2203296)Time elapsed: 0.016 s % 32.24/5.26 % (2203295)CaDiCaL version: 2.1.3 % 32.24/5.26 % (2203296)Peak memory usage: 90 MB % 32.24/5.26 % (2203296)Instructions burned: 54 (million) % 32.24/5.26 % (2203295)Termination reason: Instruction limit % 32.24/5.26 % (2203295)Termination phase: Saturation % 32.24/5.26 % (2203295)Time elapsed: 0.051 s % 32.24/5.26 % (2203295)Peak memory usage: 89 MB % 32.24/5.26 % (2203295)Instructions burned: 108 (million) % 32.24/5.26 % (2203301)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3927740657:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 32.24/5.26 % (2203302)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3126788714:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi) % 32.24/5.26 % (2203296)------------------------------ % 32.24/5.26 % (2203296)------------------------------ % 32.24/5.26 % (2203305)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=752438128:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi) % 32.24/5.26 % (2203301)Instruction limit reached! % 32.24/5.26 % (2203301)------------------------------ % 32.24/5.26 % (2203301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.24/5.26 % (2203301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.24/5.26 % (2203301)CaDiCaL version: 2.1.3 % 32.24/5.26 % (2203301)Termination reason: Instruction limit % 32.24/5.26 % (2203301)Termination phase: Saturation % 32.24/5.26 % (2203301)Time elapsed: 0.140 s % 32.24/5.26 % (2203301)Peak memory usage: 91 MB % 32.24/5.26 % (2203301)Instructions burned: 243 (million) % 32.24/5.26 % (2203305)Instruction limit reached! % 32.24/5.26 % (2203305)------------------------------ % 32.24/5.26 % (2203305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.24/5.26 % (2203305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.24/5.26 % (2203305)CaDiCaL version: 2.1.3 % 32.24/5.26 % (2203305)Termination reason: Instruction limit % 32.24/5.26 % (2203305)Termination phase: Saturation % 32.24/5.26 % (2203305)Time elapsed: 0.045 s % 32.24/5.26 % (2203305)Peak memory usage: 90 MB % 32.24/5.26 % (2203305)Instructions burned: 135 (million) % 32.24/5.26 % (2203309)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=534394106:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi) % 32.24/5.26 % (2203308)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=266488711:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi) % 32.24/5.26 % (2203309)Instruction limit reached! % 32.24/5.26 % (2203309)------------------------------ % 32.24/5.26 % (2203309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.24/5.26 % (2203309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.24/5.26 % (2203309)CaDiCaL version: 2.1.3 % 32.24/5.26 % (2203309)Termination reason: Instruction limit % 32.24/5.26 % (2203309)Termination phase: Saturation % 32.24/5.26 % (2203309)Time elapsed: 0.064 s % 32.24/5.26 % (2203309)Peak memory usage: 91 MB % 32.24/5.26 % (2203309)Instructions burned: 191 (million) % 32.24/5.26 % (2203312)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2517764346:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi) % 32.24/5.26 % (2203312)Instruction limit reached! % 32.24/5.26 % (2203312)------------------------------ % 32.24/5.26 % (2203312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.24/5.26 % (2203312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.24/5.26 % (2203312)CaDiCaL version: 2.1.3 % 32.24/5.26 % (2203312)Termination reason: Instruction limit % 32.24/5.26 % (2203312)Termination phase: Saturation % 32.24/5.26 % (2203312)Time elapsed: 0.086 s % 46.91/7.37 % (2203312)Peak memory usage: 93 MB % 46.91/7.37 % (2203312)Instructions burned: 267 (million) % 46.91/7.37 % (2203308)Instruction limit reached! % 46.91/7.37 % (2203308)------------------------------ % 46.91/7.37 % (2203308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.91/7.37 % (2203308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.91/7.37 % (2203308)CaDiCaL version: 2.1.3 % 46.91/7.37 % (2203308)Termination reason: Instruction limit % 46.91/7.37 % (2203308)Termination phase: Saturation % 46.91/7.37 % (2203308)Time elapsed: 0.278 s % 46.91/7.37 % (2203308)Peak memory usage: 94 MB % 46.91/7.37 % (2203308)Instructions burned: 499 (million) % 46.91/7.37 % (2203314)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1847589313:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi) % 46.91/7.37 % (2203314)Instruction limit reached! % 46.91/7.37 % (2203314)------------------------------ % 46.91/7.37 % (2203314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.91/7.37 % (2203314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.91/7.37 % (2203314)CaDiCaL version: 2.1.3 % 46.91/7.37 % (2203314)Termination reason: Instruction limit % 46.91/7.37 % (2203314)Termination phase: Saturation % 46.91/7.37 % (2203314)Time elapsed: 0.049 s % 46.91/7.37 % (2203314)Peak memory usage: 90 MB % 46.91/7.37 % (2203314)Instructions burned: 157 (million) % 46.91/7.37 % (2203315)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=1887376281:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi) % 46.91/7.37 % (2203317)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3518377447:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi) % 46.91/7.37 % (2203317)Instruction limit reached! % 46.91/7.37 % (2203317)------------------------------ % 46.91/7.37 % (2203317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.91/7.37 % (2203317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.91/7.37 % (2203317)CaDiCaL version: 2.1.3 % 46.91/7.37 % (2203317)Termination reason: Instruction limit % 46.91/7.37 % (2203317)Termination phase: Saturation % 46.91/7.37 % (2203317)Time elapsed: 0.158 s % 46.91/7.37 % (2203317)Peak memory usage: 92 MB % 46.91/7.37 % (2203317)Instructions burned: 541 (million) % 46.91/7.37 % (2203320)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1006918222:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi) % 46.91/7.37 % (2203320)Instruction limit reached! % 46.91/7.37 % (2203320)------------------------------ % 46.91/7.37 % (2203320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.91/7.37 % (2203320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.91/7.37 % (2203320)CaDiCaL version: 2.1.3 % 46.91/7.37 % (2203320)Termination reason: Instruction limit % 46.91/7.37 % (2203320)Termination phase: Saturation % 46.91/7.37 % (2203320)Time elapsed: 0.053 s % 46.91/7.37 % (2203320)Peak memory usage: 90 MB % 46.91/7.37 % (2203320)Instructions burned: 184 (million) % 46.91/7.37 % (2203322)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=2199680199:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/10307Mi) % 46.91/7.37 % (2203293)Instruction limit reached! % 46.91/7.37 % (2203293)------------------------------ % 46.91/7.37 % (2203293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.91/7.37 % (2203293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.91/7.37 % (2203293)CaDiCaL version: 2.1.3 % 46.91/7.37 % (2203293)Termination reason: Instruction limit % 46.91/7.37 % (2203293)Termination phase: Saturation % 46.91/7.37 % (2203293)Time elapsed: 2.101 s % 46.91/7.37 % (2203293)Peak memory usage: 153 MB % 46.91/7.37 % (2203293)Instructions burned: 3395 (million) % 46.91/7.37 % (2203324)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=3114400090:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi) % 46.91/7.37 % (2203324)Instruction limit reached! % 46.91/7.37 % (2203324)------------------------------ % 46.91/7.37 % (2203324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.91/7.37 % (2203324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.87/10.73 % (2203324)CaDiCaL version: 2.1.3 % 70.87/10.73 % (2203324)Termination reason: Instruction limit % 70.87/10.73 % (2203324)Termination phase: Saturation % 70.87/10.73 % (2203324)Time elapsed: 0.313 s % 70.87/10.73 % (2203324)Peak memory usage: 93 MB % 70.87/10.73 % (2203324)Instructions burned: 563 (million) % 70.87/10.73 % (2203326)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=2473343525:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi) % 70.87/10.73 % (2203315)Instruction limit reached! % 70.87/10.73 % (2203315)------------------------------ % 70.87/10.73 % (2203315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.87/10.73 % (2203315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.87/10.73 % (2203315)CaDiCaL version: 2.1.3 % 70.87/10.73 % (2203315)Termination reason: Instruction limit % 70.87/10.73 % (2203315)Termination phase: Saturation % 70.87/10.73 % (2203315)Time elapsed: 2.021 s % 70.87/10.73 % (2203315)Peak memory usage: 150 MB % 70.87/10.73 % (2203315)Instructions burned: 3257 (million) % 70.87/10.73 % (2203328)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=769547027:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2964 on theBenchmark for (2964ds/303Mi) % 70.87/10.73 % (2203328)Instruction limit reached! % 70.87/10.73 % (2203328)------------------------------ % 70.87/10.73 % (2203328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.87/10.73 % (2203328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.87/10.73 % (2203328)CaDiCaL version: 2.1.3 % 70.87/10.73 % (2203328)Termination reason: Instruction limit % 70.87/10.73 % (2203328)Termination phase: Saturation % 70.87/10.73 % (2203328)Time elapsed: 0.173 s % 70.87/10.73 % (2203328)Peak memory usage: 92 MB % 70.87/10.73 % (2203328)Instructions burned: 304 (million) % 70.87/10.73 % (2203302)Instruction limit reached! % 70.87/10.73 % (2203302)------------------------------ % 70.87/10.73 % (2203302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.87/10.73 % (2203302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.87/10.73 % (2203302)CaDiCaL version: 2.1.3 % 70.87/10.73 % (2203302)Termination reason: Instruction limit % 70.87/10.73 % (2203302)Termination phase: Saturation % 70.87/10.73 % (2203302)Time elapsed: 3.147 s % 70.87/10.73 % (2203302)Peak memory usage: 162 MB % 70.87/10.73 % (2203302)Instructions burned: 5209 (million) % 70.87/10.73 % (2203330)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=518838700:st=4:i=720:sd=3:fsr=off:ss=axioms_2961 on theBenchmark for (2961ds/720Mi) % 70.87/10.73 % (2203332)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2252286504:i=598:bs=on:bd=preordered:av=off:ss=axioms_2959 on theBenchmark for (2959ds/598Mi) % 70.87/10.73 % (2203330)Instruction limit reached! % 70.87/10.73 % (2203330)------------------------------ % 70.87/10.73 % (2203330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.87/10.73 % (2203330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.87/10.73 % (2203330)CaDiCaL version: 2.1.3 % 70.87/10.73 % (2203330)Termination reason: Instruction limit % 70.87/10.73 % (2203330)Termination phase: Saturation % 70.87/10.73 % (2203330)Time elapsed: 0.330 s % 70.87/10.73 % (2203330)Peak memory usage: 94 MB % 70.87/10.73 % (2203330)Instructions burned: 721 (million) % 70.87/10.73 % (2203334)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2567547026:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi) % 70.87/10.73 % (2203332)Instruction limit reached! % 70.87/10.73 % (2203332)------------------------------ % 70.87/10.73 % (2203332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.87/10.73 % (2203332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.87/10.73 % (2203332)CaDiCaL version: 2.1.3 % 70.87/10.73 % (2203332)Termination reason: Instruction limit % 70.87/10.73 % (2203332)Termination phase: Saturation % 70.87/10.73 % (2203332)Time elapsed: 0.336 s % 70.87/10.73 % (2203332)Peak memory usage: 95 MB % 70.87/10.73 % (2203332)Instructions burned: 598 (million) % 70.87/10.73 % (2203336)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=1852056640:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2955 on theBenchmark for (2955ds/1997Mi) % 99.35/14.70 % (2203322)Instruction limit reached! % 99.35/14.70 % (2203322)------------------------------ % 99.35/14.70 % (2203322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.35/14.70 % (2203322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.35/14.70 % (2203322)CaDiCaL version: 2.1.3 % 99.35/14.70 % (2203322)Termination reason: Instruction limit % 99.35/14.70 % (2203322)Termination phase: Saturation % 99.35/14.70 % (2203322)Time elapsed: 3.620 s % 99.35/14.70 % (2203322)Peak memory usage: 194 MB % 99.35/14.70 % (2203322)Instructions burned: 10308 (million) % 99.35/14.70 % (2203338)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=3852205590:i=2088:bd=preordered:av=off_2944 on theBenchmark for (2944ds/2088Mi) % 99.35/14.70 % (2203336)Instruction limit reached! % 99.35/14.70 % (2203336)------------------------------ % 99.35/14.70 % (2203336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.35/14.70 % (2203336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.35/14.70 % (2203336)CaDiCaL version: 2.1.3 % 99.35/14.70 % (2203336)Termination reason: Instruction limit % 99.35/14.70 % (2203336)Termination phase: Saturation % 99.35/14.70 % (2203336)Time elapsed: 1.226 s % 99.35/14.70 % (2203336)Peak memory usage: 143 MB % 99.35/14.70 % (2203336)Instructions burned: 1999 (million) % 99.35/14.70 % (2203340)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4213891610:i=1098:nicw=on_2941 on theBenchmark for (2941ds/1098Mi) % 99.35/14.70 % (2203334)Instruction limit reached! % 99.35/14.70 % (2203334)------------------------------ % 99.35/14.70 % (2203334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.35/14.70 % (2203334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.35/14.70 % (2203334)CaDiCaL version: 2.1.3 % 99.35/14.70 % (2203334)Termination reason: Instruction limit % 99.35/14.70 % (2203334)Termination phase: Saturation % 99.35/14.70 % (2203334)Time elapsed: 1.806 s % 99.35/14.70 % (2203334)Peak memory usage: 148 MB % 99.35/14.70 % (2203334)Instructions burned: 2989 (million) % 99.35/14.70 % (2203338)Instruction limit reached! % 99.35/14.70 % (2203338)------------------------------ % 99.35/14.70 % (2203338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.35/14.70 % (2203338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.35/14.70 % (2203338)CaDiCaL version: 2.1.3 % 99.35/14.70 % (2203338)Termination reason: Instruction limit % 99.35/14.70 % (2203338)Termination phase: Saturation % 99.35/14.70 % (2203338)Time elapsed: 0.717 s % 99.35/14.70 % (2203338)Peak memory usage: 140 MB % 99.35/14.70 % (2203338)Instructions burned: 2091 (million) % 99.35/14.70 % (2203342)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3923901550:i=433:bd=preordered_2937 on theBenchmark for (2937ds/433Mi) % 99.35/14.70 % (2203342)Refutation not found, incomplete strategy % 99.35/14.70 % (2203342)------------------------------ % 99.35/14.70 % (2203342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.35/14.70 % (2203342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.35/14.70 % (2203342)CaDiCaL version: 2.1.3 % 99.35/14.70 % (2203342)Termination reason: Refutation not found, incomplete strategy % 99.35/14.70 % (2203342)Time elapsed: 0.057 s % 99.35/14.70 % (2203342)Peak memory usage: 90 MB % 99.35/14.70 % (2203342)Instructions burned: 93 (million) % 99.35/14.70 % (2203343)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2643550657:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2936 on theBenchmark for (2936ds/2942Mi) % 99.35/14.70 % (2203340)Instruction limit reached! % 99.35/14.70 % (2203340)------------------------------ % 99.35/14.70 % (2203340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.35/14.70 % (2203340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.35/14.70 % (2203340)CaDiCaL version: 2.1.3 % 99.35/14.70 % (2203340)Termination reason: Instruction limit % 99.35/14.70 % (2203340)Termination phase: Saturation % 99.35/14.70 % (2203340)Time elapsed: 0.662 s % 99.35/14.70 % (2203340)Peak memory usage: 102 MB % 99.35/14.70 % (2203340)Instructions burned: 1099 (million) % 99.35/14.70 % (2203342)------------------------------ % 99.35/14.70 % (2203342)------------------------------ % 113.22/16.79 % (2203346)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3500358899:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2933 on theBenchmark for (2933ds/6922Mi) % 113.22/16.79 % (2203347)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=1506599192:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2932 on theBenchmark for (2932ds/596Mi) % 113.22/16.79 % (2203347)Instruction limit reached! % 113.22/16.79 % (2203347)------------------------------ % 113.22/16.79 % (2203347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.22/16.79 % (2203347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.22/16.79 % (2203347)CaDiCaL version: 2.1.3 % 113.22/16.79 % (2203347)Termination reason: Instruction limit % 113.22/16.79 % (2203347)Termination phase: Saturation % 113.22/16.79 % (2203347)Time elapsed: 0.315 s % 113.22/16.79 % (2203347)Peak memory usage: 96 MB % 113.22/16.79 % (2203347)Instructions burned: 596 (million) % 113.22/16.79 % (2203350)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=2862207658:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2928 on theBenchmark for (2928ds/4123Mi) % 113.22/16.79 % (2203343)Instruction limit reached! % 113.22/16.79 % (2203343)------------------------------ % 113.22/16.79 % (2203343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.22/16.79 % (2203343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.22/16.79 % (2203343)CaDiCaL version: 2.1.3 % 113.22/16.79 % (2203343)Termination reason: Instruction limit % 113.22/16.79 % (2203343)Termination phase: Saturation % 113.22/16.79 % (2203343)Time elapsed: 1.026 s % 113.22/16.79 % (2203343)Peak memory usage: 146 MB % 113.22/16.79 % (2203343)Instructions burned: 2942 (million) % 113.22/16.79 % (2203352)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=865126806:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2924 on theBenchmark for (2924ds/16411Mi) % 113.22/16.79 % (2203326)Instruction limit reached! % 113.22/16.79 % (2203326)------------------------------ % 113.22/16.79 % (2203326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.22/16.79 % (2203326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.22/16.79 % (2203326)CaDiCaL version: 2.1.3 % 113.22/16.79 % (2203326)Termination reason: Instruction limit % 113.22/16.79 % (2203326)Termination phase: Saturation % 113.22/16.79 % (2203326)Time elapsed: 5.392 s % 113.22/16.79 % (2203326)Peak memory usage: 184 MB % 113.22/16.79 % (2203326)Instructions burned: 8479 (million) % 113.22/16.79 % (2203354)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3162170171:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2912 on theBenchmark for (2912ds/1670Mi) % 113.22/16.79 % (2203350)Instruction limit reached! % 113.22/16.79 % (2203350)------------------------------ % 113.22/16.79 % (2203350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.22/16.79 % (2203350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.22/16.79 % (2203350)CaDiCaL version: 2.1.3 % 113.22/16.79 % (2203350)Termination reason: Instruction limit % 113.22/16.79 % (2203350)Termination phase: Saturation % 113.22/16.79 % (2203350)Time elapsed: 2.459 s % 113.22/16.79 % (2203350)Peak memory usage: 159 MB % 113.22/16.79 % (2203350)Instructions burned: 4125 (million) % 113.22/16.79 % (2203356)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3997906771:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2902 on theBenchmark for (2902ds/1722Mi) % 113.22/16.79 % (2203354)Instruction limit reached! % 113.22/16.79 % (2203354)------------------------------ % 113.22/16.79 % (2203354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.22/16.79 % (2203354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.22/16.79 % (2203354)CaDiCaL version: 2.1.3 % 113.22/16.79 % (2203354)Termination reason: Instruction limit % 113.22/16.79 % (2203354)Termination phase: Saturation % 113.22/16.79 % (2203354)Time elapsed: 1.034 s % 113.22/16.79 % (2203354)Peak memory usage: 141 MB % 113.22/16.79 % (2203354)Instructions burned: 1671 (million) % 113.22/16.79 % (2203358)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1537127517:cts=off:cond=on:i=9530:bs=on:fsd=on_2900 on theBenchmark for (2900ds/9530Mi) % 131.46/19.24 % (2203346)Instruction limit reached! % 131.46/19.24 % (2203346)------------------------------ % 131.46/19.24 % (2203346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.46/19.24 % (2203346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.46/19.24 % (2203346)CaDiCaL version: 2.1.3 % 131.46/19.24 % (2203346)Termination reason: Instruction limit % 131.46/19.24 % (2203346)Termination phase: Saturation % 131.46/19.24 % (2203346)Time elapsed: 4.180 s % 131.46/19.24 % (2203346)Peak memory usage: 161 MB % 131.46/19.24 % (2203346)Instructions burned: 6923 (million) % 131.46/19.24 % (2203356)Instruction limit reached! % 131.46/19.24 % (2203356)------------------------------ % 131.46/19.24 % (2203356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.46/19.24 % (2203356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.46/19.24 % (2203356)CaDiCaL version: 2.1.3 % 131.46/19.24 % (2203356)Termination reason: Instruction limit % 131.46/19.24 % (2203356)Termination phase: Saturation % 131.46/19.24 % (2203356)Time elapsed: 1.107 s % 131.46/19.24 % (2203356)Peak memory usage: 142 MB % 131.46/19.24 % (2203356)Instructions burned: 1722 (million) % 131.46/19.24 % (2203360)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1041316540:st=2:i=4495:sd=10:ss=included_2890 on theBenchmark for (2890ds/4495Mi) % 131.46/19.24 % (2203361)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=1509632122:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2889 on theBenchmark for (2889ds/4920Mi) % 131.46/19.24 % (2203352)Instruction limit reached! % 131.46/19.24 % (2203352)------------------------------ % 131.46/19.24 % (2203352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.46/19.24 % (2203352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.46/19.24 % (2203352)CaDiCaL version: 2.1.3 % 131.46/19.24 % (2203352)Termination reason: Instruction limit % 131.46/19.24 % (2203352)Termination phase: Saturation % 131.46/19.24 % (2203352)Time elapsed: 5.599 s % 131.46/19.24 % (2203352)Peak memory usage: 219 MB % 131.46/19.24 % (2203352)Instructions burned: 16412 (million) % 131.46/19.24 % (2203364)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2638344169:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2867 on theBenchmark for (2867ds/2083Mi) % 131.46/19.24 % (2203360)Instruction limit reached! % 131.46/19.24 % (2203360)------------------------------ % 131.46/19.24 % (2203360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.46/19.24 % (2203360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.46/19.24 % (2203360)CaDiCaL version: 2.1.3 % 131.46/19.24 % (2203360)Termination reason: Instruction limit % 131.46/19.24 % (2203360)Termination phase: Saturation % 131.46/19.24 % (2203360)Time elapsed: 2.715 s % 131.46/19.24 % (2203360)Peak memory usage: 159 MB % 131.46/19.24 % (2203360)Instructions burned: 4495 (million) % 131.46/19.24 % (2203366)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=3206540526:i=4629:av=off:gsp=on_2861 on theBenchmark for (2861ds/4629Mi) % 131.46/19.24 % (2203364)Instruction limit reached! % 131.46/19.24 % (2203364)------------------------------ % 131.46/19.24 % (2203364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.46/19.24 % (2203364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.46/19.24 % (2203364)CaDiCaL version: 2.1.3 % 131.46/19.24 % (2203364)Termination reason: Instruction limit % 131.46/19.24 % (2203364)Termination phase: Saturation % 131.46/19.24 % (2203364)Time elapsed: 0.698 s % 131.46/19.24 % (2203364)Peak memory usage: 142 MB % 131.46/19.24 % (2203364)Instructions burned: 2083 (million) % 131.46/19.24 % (2203361)Instruction limit reached! % 131.46/19.24 % (2203361)------------------------------ % 131.46/19.24 % (2203361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.46/19.24 % (2203361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.46/19.24 % (2203361)CaDiCaL version: 2.1.3 % 131.46/19.24 % (2203361)Termination reason: Instruction limit % 131.46/19.24 % (2203361)Termination phase: Saturation % 153.38/22.32 % (2203361)Time elapsed: 2.908 s % 153.38/22.32 % (2203361)Peak memory usage: 164 MB % 153.38/22.32 % (2203361)Instructions burned: 4921 (million) % 153.38/22.32 % (2203368)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3180042326:i=1258:av=off_2859 on theBenchmark for (2859ds/1258Mi) % 153.38/22.32 % (2203369)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2599036367:i=7343:av=off:ss=included_2859 on theBenchmark for (2859ds/7343Mi) % 153.38/22.32 % (2203368)Instruction limit reached! % 153.38/22.32 % (2203368)------------------------------ % 153.38/22.32 % (2203368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.38/22.32 % (2203368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.38/22.32 % (2203368)CaDiCaL version: 2.1.3 % 153.38/22.32 % (2203368)Termination reason: Instruction limit % 153.38/22.32 % (2203368)Termination phase: Saturation % 153.38/22.32 % (2203368)Time elapsed: 0.374 s % 153.38/22.32 % (2203368)Peak memory usage: 95 MB % 153.38/22.32 % (2203368)Instructions burned: 1261 (million) % 153.38/22.32 % (2203372)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2631545155:i=1325:sd=2:ss=axioms:sgt=16_2855 on theBenchmark for (2855ds/1325Mi) % 153.38/22.32 % (2203366)Refutation not found, incomplete strategy % 153.38/22.32 % (2203366)------------------------------ % 153.38/22.32 % (2203366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.38/22.32 % (2203366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.38/22.32 % (2203366)CaDiCaL version: 2.1.3 % 153.38/22.32 % (2203366)Termination reason: Refutation not found, incomplete strategy % 153.38/22.32 % (2203366)Time elapsed: 0.689 s % 153.38/22.32 % (2203366)Peak memory usage: 134 MB % 153.38/22.32 % (2203366)Instructions burned: 1071 (million) % 153.38/22.32 % (2203366)------------------------------ % 153.38/22.32 % (2203366)------------------------------ % 153.38/22.32 % (2203372)Instruction limit reached! % 153.38/22.32 % (2203372)------------------------------ % 153.38/22.32 % (2203372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.38/22.32 % (2203372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.38/22.32 % (2203372)CaDiCaL version: 2.1.3 % 153.38/22.32 % (2203372)Termination reason: Instruction limit % 153.38/22.32 % (2203372)Termination phase: Saturation % 153.38/22.32 % (2203372)Time elapsed: 0.353 s % 153.38/22.32 % (2203372)Peak memory usage: 95 MB % 153.38/22.32 % (2203372)Instructions burned: 1326 (million) % 153.38/22.32 % (2203374)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=115260044:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2851 on theBenchmark for (2851ds/2646Mi) % 153.38/22.32 % (2203375)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=848721230:i=1489:sd=2:ep=R:ss=axioms_2850 on theBenchmark for (2850ds/1489Mi) % 153.38/22.32 % (2203375)Instruction limit reached! % 153.38/22.32 % (2203375)------------------------------ % 153.38/22.32 % (2203375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.38/22.32 % (2203375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.38/22.32 % (2203375)CaDiCaL version: 2.1.3 % 153.38/22.32 % (2203375)Termination reason: Instruction limit % 153.38/22.32 % (2203375)Termination phase: Saturation % 153.38/22.32 % (2203375)Time elapsed: 0.499 s % 153.38/22.32 % (2203375)Peak memory usage: 136 MB % 153.38/22.32 % (2203375)Instructions burned: 1496 (million) % 153.38/22.32 % (2203378)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=2654902526:i=1503_2844 on theBenchmark for (2844ds/1503Mi) % 153.38/22.32 % (2203358)Instruction limit reached! % 153.38/22.32 % (2203358)------------------------------ % 153.38/22.32 % (2203358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.38/22.32 % (2203358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.38/22.32 % (2203358)CaDiCaL version: 2.1.3 % 153.38/22.32 % (2203358)Termination reason: Instruction limit % 153.38/22.32 % (2203358)Termination phase: Saturation % 153.38/22.32 % (2203358)Time elapsed: 5.915 s % 153.38/22.32 % (2203358)Peak memory usage: 182 MB % 153.38/22.32 % (2203358)Instructions burned: 9530 (million) % 153.38/22.32 % (2203378)Instruction limit reached! % 153.38/22.32 % (2203378)------------------------------ % 153.38/22.32 % (2203378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.66/26.18 % (2203378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.66/26.18 % (2203378)CaDiCaL version: 2.1.3 % 180.66/26.18 % (2203378)Termination reason: Instruction limit % 180.66/26.18 % (2203378)Termination phase: Saturation % 180.66/26.18 % (2203378)Time elapsed: 0.487 s % 180.66/26.18 % (2203378)Peak memory usage: 142 MB % 180.66/26.18 % (2203378)Instructions burned: 1505 (million) % 180.66/26.18 % (2203380)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1213753111:i=13942:kws=frequency_2840 on theBenchmark for (2840ds/13942Mi) % 180.66/26.18 % (2203382)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=1693379846:i=3604:fsr=off:er=filter_2838 on theBenchmark for (2838ds/3604Mi) % 180.66/26.18 % (2203374)Instruction limit reached! % 180.66/26.18 % (2203374)------------------------------ % 180.66/26.18 % (2203374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.66/26.18 % (2203374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.66/26.18 % (2203374)CaDiCaL version: 2.1.3 % 180.66/26.18 % (2203374)Termination reason: Instruction limit % 180.66/26.18 % (2203374)Termination phase: Saturation % 180.66/26.18 % (2203374)Time elapsed: 1.668 s % 180.66/26.18 % (2203374)Peak memory usage: 146 MB % 180.66/26.18 % (2203374)Instructions burned: 2646 (million) % 180.66/26.18 % (2203384)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2979985629:i=1876:sd=1:ss=included:sgt=32_2833 on theBenchmark for (2833ds/1876Mi) % 180.66/26.18 % (2203382)Instruction limit reached! % 180.66/26.18 % (2203382)------------------------------ % 180.66/26.18 % (2203382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.66/26.18 % (2203382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.66/26.18 % (2203382)CaDiCaL version: 2.1.3 % 180.66/26.18 % (2203382)Termination reason: Instruction limit % 180.66/26.18 % (2203382)Termination phase: Saturation % 180.66/26.18 % (2203382)Time elapsed: 1.117 s % 180.66/26.18 % (2203382)Peak memory usage: 152 MB % 180.66/26.18 % (2203382)Instructions burned: 3604 (million) % 180.66/26.18 % (2203386)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2124075741:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2826 on theBenchmark for (2826ds/1932Mi) % 180.66/26.18 % (2203384)Instruction limit reached! % 180.66/26.18 % (2203384)------------------------------ % 180.66/26.18 % (2203384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.66/26.18 % (2203384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.66/26.18 % (2203384)CaDiCaL version: 2.1.3 % 180.66/26.18 % (2203384)Termination reason: Instruction limit % 180.66/26.18 % (2203384)Termination phase: Saturation % 180.66/26.18 % (2203384)Time elapsed: 1.138 s % 180.66/26.18 % (2203384)Peak memory usage: 142 MB % 180.66/26.18 % (2203384)Instructions burned: 1876 (million) % 180.66/26.18 % (2203388)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=4227398335:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2820 on theBenchmark for (2820ds/1980Mi) % 180.66/26.18 % (2203386)Instruction limit reached! % 180.66/26.18 % (2203386)------------------------------ % 180.66/26.18 % (2203386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.66/26.18 % (2203386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.66/26.18 % (2203386)CaDiCaL version: 2.1.3 % 180.66/26.18 % (2203386)Termination reason: Instruction limit % 180.66/26.18 % (2203386)Termination phase: Saturation % 180.66/26.18 % (2203386)Time elapsed: 0.656 s % 180.66/26.18 % (2203386)Peak memory usage: 139 MB % 180.66/26.18 % (2203386)Instructions burned: 1934 (million) % 180.66/26.18 % (2203390)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=3851413455:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2818 on theBenchmark for (2818ds/3902Mi) % 180.66/26.18 % (2203369)Instruction limit reached! % 180.66/26.18 % (2203369)------------------------------ % 180.66/26.18 % (2203369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.66/26.18 % (2203369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.94/28.65 % (2203369)CaDiCaL version: 2.1.3 % 196.94/28.65 % (2203369)Termination reason: Instruction limit % 196.94/28.65 % (2203369)Termination phase: Saturation % 196.94/28.65 % (2203369)Time elapsed: 4.402 s % 196.94/28.65 % (2203369)Peak memory usage: 179 MB % 196.94/28.65 % (2203369)Instructions burned: 7344 (million) % 196.94/28.65 % (2203392)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1590990218:avsq=on:i=3916:aac=none:amm=off_2814 on theBenchmark for (2814ds/3916Mi) % 196.94/28.65 % (2203388)Instruction limit reached! % 196.94/28.65 % (2203388)------------------------------ % 196.94/28.65 % (2203388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.94/28.65 % (2203388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.94/28.65 % (2203388)CaDiCaL version: 2.1.3 % 196.94/28.65 % (2203388)Termination reason: Instruction limit % 196.94/28.65 % (2203388)Termination phase: Saturation % 196.94/28.65 % (2203388)Time elapsed: 1.207 s % 196.94/28.65 % (2203388)Peak memory usage: 139 MB % 196.94/28.65 % (2203388)Instructions burned: 1980 (million) % 196.94/28.65 % (2203390)Instruction limit reached! % 196.94/28.65 % (2203390)------------------------------ % 196.94/28.65 % (2203390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.94/28.65 % (2203390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.94/28.65 % (2203390)CaDiCaL version: 2.1.3 % 196.94/28.65 % (2203390)Termination reason: Instruction limit % 196.94/28.65 % (2203390)Termination phase: Saturation % 196.94/28.65 % (2203390)Time elapsed: 1.137 s % 196.94/28.65 % (2203390)Peak memory usage: 156 MB % 196.94/28.65 % (2203390)Instructions burned: 3903 (million) % 196.94/28.65 % (2203394)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=1887344413:cond=on:i=3940:av=off:er=known_2807 on theBenchmark for (2807ds/3940Mi) % 196.94/28.65 % (2203395)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=3757975254:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2806 on theBenchmark for (2806ds/3980Mi) % 196.94/28.65 % (2203395)Instruction limit reached! % 196.94/28.65 % (2203395)------------------------------ % 196.94/28.65 % (2203395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.94/28.65 % (2203395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.94/28.65 % (2203395)CaDiCaL version: 2.1.3 % 196.94/28.65 % (2203395)Termination reason: Instruction limit % 196.94/28.65 % (2203395)Termination phase: Saturation % 196.94/28.65 % (2203395)Time elapsed: 1.306 s % 196.94/28.65 % (2203395)Peak memory usage: 155 MB % 196.94/28.65 % (2203395)Instructions burned: 3980 (million) % 196.94/28.65 % (2203398)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=3890314608:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2792 on theBenchmark for (2792ds/2087Mi) % 196.94/28.65 % (2203392)Instruction limit reached! % 196.94/28.65 % (2203392)------------------------------ % 196.94/28.65 % (2203392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.94/28.65 % (2203392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.94/28.65 % (2203392)CaDiCaL version: 2.1.3 % 196.94/28.65 % (2203392)Termination reason: Instruction limit % 196.94/28.65 % (2203392)Termination phase: Saturation % 196.94/28.65 % (2203392)Time elapsed: 2.435 s % 196.94/28.65 % (2203392)Peak memory usage: 115 MB % 196.94/28.65 % (2203392)Instructions burned: 3917 (million) % 196.94/28.65 % (2203400)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=667376336:cts=off:cond=on:i=4272:bs=on:fsd=on_2788 on theBenchmark for (2788ds/4272Mi) % 196.94/28.65 % (2203398)Instruction limit reached! % 196.94/28.65 % (2203398)------------------------------ % 196.94/28.65 % (2203398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.94/28.65 % (2203398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.94/28.65 % (2203398)CaDiCaL version: 2.1.3 % 196.94/28.65 % (2203398)Termination reason: Instruction limit % 196.94/28.65 % (2203398)Termination phase: Saturation % 196.94/28.65 % (2203398)Time elapsed: 0.742 s % 196.94/28.65 % (2203398)Peak memory usage: 142 MB % 196.94/28.65 % (2203398)Instructions burned: 2088 (million) % 196.94/28.65 % (2203402)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2514946099:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2784 on theBenchmark for (2784ds/2197Mi) % 253.49/36.48 % (2203394)Instruction limit reached! % 253.49/36.48 % (2203394)------------------------------ % 253.49/36.48 % (2203394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.49/36.48 % (2203394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.49/36.48 % (2203394)CaDiCaL version: 2.1.3 % 253.49/36.48 % (2203394)Termination reason: Instruction limit % 253.49/36.48 % (2203394)Termination phase: Saturation % 253.49/36.48 % (2203394)Time elapsed: 2.276 s % 253.49/36.48 % (2203394)Peak memory usage: 156 MB % 253.49/36.48 % (2203394)Instructions burned: 3940 (million) % 253.49/36.48 % (2203404)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1728843016:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2782 on theBenchmark for (2782ds/6508Mi) % 253.49/36.48 % (2203402)Instruction limit reached! % 253.49/36.48 % (2203402)------------------------------ % 253.49/36.48 % (2203402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.49/36.48 % (2203402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.49/36.48 % (2203402)CaDiCaL version: 2.1.3 % 253.49/36.48 % (2203402)Termination reason: Instruction limit % 253.49/36.48 % (2203402)Termination phase: Saturation % 253.49/36.48 % (2203402)Time elapsed: 0.757 s % 253.49/36.48 % (2203402)Peak memory usage: 141 MB % 253.49/36.48 % (2203402)Instructions burned: 2199 (million) % 253.49/36.48 % (2203406)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=2529024425:i=2330:fgj=on:av=off:fsr=off_2775 on theBenchmark for (2775ds/2330Mi) % 253.49/36.48 % (2203406)Instruction limit reached! % 253.49/36.48 % (2203406)------------------------------ % 253.49/36.48 % (2203406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.49/36.48 % (2203406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.49/36.48 % (2203406)CaDiCaL version: 2.1.3 % 253.49/36.48 % (2203406)Termination reason: Instruction limit % 253.49/36.48 % (2203406)Termination phase: Saturation % 253.49/36.48 % (2203406)Time elapsed: 0.774 s % 253.49/36.48 % (2203406)Peak memory usage: 142 MB % 253.49/36.48 % (2203406)Instructions burned: 2333 (million) % 253.49/36.48 % (2203408)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1716567181:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2767 on theBenchmark for (2767ds/7592Mi) % 253.49/36.48 % (2203400)Instruction limit reached! % 253.49/36.48 % (2203400)------------------------------ % 253.49/36.48 % (2203400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.49/36.48 % (2203400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.49/36.48 % (2203400)CaDiCaL version: 2.1.3 % 253.49/36.48 % (2203400)Termination reason: Instruction limit % 253.49/36.48 % (2203400)Termination phase: Saturation % 253.49/36.48 % (2203400)Time elapsed: 2.434 s % 253.49/36.48 % (2203400)Peak memory usage: 153 MB % 253.49/36.48 % (2203400)Instructions burned: 4272 (million) % 253.49/36.48 % (2203410)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=1351484067:i=2693:kws=precedence:ins=1:av=off_2762 on theBenchmark for (2762ds/2693Mi) % 253.49/36.48 % (2203380)Instruction limit reached! % 253.49/36.48 % (2203380)------------------------------ % 253.49/36.48 % (2203380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.49/36.48 % (2203380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.49/36.48 % (2203380)CaDiCaL version: 2.1.3 % 253.49/36.48 % (2203380)Termination reason: Instruction limit % 253.49/36.48 % (2203380)Termination phase: Saturation % 253.49/36.48 % (2203380)Time elapsed: 8.166 s % 253.49/36.48 % (2203380)Peak memory usage: 232 MB % 253.49/36.48 % (2203380)Instructions burned: 13942 (million) % 253.49/36.48 % (2203412)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2299012294:i=28651:sd=4:ss=included:sgt=64_2756 on theBenchmark for (2756ds/28651Mi) % 253.49/36.48 % (2203410)Instruction limit reached! % 253.49/36.48 % (2203410)------------------------------ % 253.49/36.48 % (2203410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.49/36.48 % (2203410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.49/36.48 % (2203410)CaDiCaL version: 2.1.3 % 253.49/36.48 % (2203410)Termination reason: Instruction limit % 253.49/36.48 % (2203410)Termination phase: Saturation % 253.49/36.48 % (22Terminated %------------------------------------------------------------------------------