%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM112-1 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:11:46 PM UTC 2026 % Result : Timeout 294.29s 42.31s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM112-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.38 % Computer : n014.cluster.edu % 0.10/0.38 % Model : x86_64 x86_64 % 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.38 % Memory : 8046.5625MB % 0.10/0.38 % OS : Linux 6.8.0-71-generic % 0.10/0.38 % CPULimit : 300 % 0.10/0.38 % WCLimit : 300 % 0.10/0.38 % DateTime : Sun Sep 27 18:54:47 UTC 2026 % 0.10/0.38 % CPUTime : % 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.42 Running first-order theorem proving % 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.27/2.20 % (1102683)Input is clausal, will run a generic CNF schedule. % 9.27/2.20 % (1102694)dis-21_1_sil=8000:lcm=predicate:random_seed=1144839187:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 9.27/2.20 % (1102694)Instruction limit reached! % 9.27/2.20 % (1102694)------------------------------ % 9.27/2.20 % (1102694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.27/2.20 % (1102694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.27/2.20 % (1102694)CaDiCaL version: 2.1.3 % 9.27/2.20 % (1102694)Termination reason: Instruction limit % 9.27/2.20 % (1102694)Termination phase: Saturation % 9.27/2.20 % (1102694)Time elapsed: 0.033 s % 9.27/2.20 % (1102694)Peak memory usage: 89 MB % 9.27/2.20 % (1102694)Instructions burned: 123 (million) % 9.27/2.20 % (1102691)lrs+10_1_sil=8000:sp=occurrence:random_seed=1665826633:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 9.27/2.20 % (1102689)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3094829149:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 9.27/2.20 % (1102692)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3496701818:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 9.27/2.20 % (1102690)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=290828798:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 9.27/2.20 % (1102688)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=2011723644:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 9.27/2.20 % (1102693)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1377711274:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 9.27/2.20 % (1102691)Instruction limit reached! % 9.27/2.20 % (1102691)------------------------------ % 9.27/2.20 % (1102691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.27/2.20 % (1102691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.27/2.20 % (1102691)CaDiCaL version: 2.1.3 % 9.27/2.20 % (1102691)Termination reason: Instruction limit % 9.27/2.20 % (1102691)Termination phase: Saturation % 9.27/2.20 % (1102691)Time elapsed: 0.042 s % 9.27/2.20 % (1102691)Peak memory usage: 88 MB % 9.27/2.20 % (1102691)Instructions burned: 110 (million) % 9.27/2.20 % (1102692)Instruction limit reached! % 9.27/2.20 % (1102692)------------------------------ % 9.27/2.20 % (1102692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.27/2.20 % (1102692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.27/2.20 % (1102692)CaDiCaL version: 2.1.3 % 9.27/2.20 % (1102692)Termination reason: Instruction limit % 9.27/2.20 % (1102692)Termination phase: Saturation % 9.27/2.20 % (1102692)Time elapsed: 0.070 s % 9.27/2.20 % (1102692)Peak memory usage: 89 MB % 9.27/2.20 % (1102692)Instructions burned: 114 (million) % 9.27/2.20 % (1102696)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=1820952529:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 9.27/2.20 % (1102696)Refutation not found, incomplete strategy % 9.27/2.20 % (1102696)------------------------------ % 9.27/2.20 % (1102696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.27/2.20 % (1102696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.27/2.20 % (1102696)CaDiCaL version: 2.1.3 % 9.27/2.20 % (1102696)Termination reason: Refutation not found, incomplete strategy % 9.27/2.20 % (1102696)Time elapsed: 0.002 s % 9.27/2.20 % (1102696)Peak memory usage: 88 MB % 9.27/2.20 % (1102696)Instructions burned: 4 (million) % 9.27/2.20 % (1102693)Instruction limit reached! % 9.27/2.20 % (1102693)------------------------------ % 9.27/2.20 % (1102693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.27/2.20 % (1102693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.27/2.20 % (1102693)CaDiCaL version: 2.1.3 % 9.27/2.20 % (1102693)Termination reason: Instruction limit % 9.27/2.20 % (1102693)Termination phase: Saturation % 9.27/2.20 % (1102693)Time elapsed: 0.139 s % 9.27/2.20 % (1102693)Peak memory usage: 90 MB % 9.27/2.20 % (1102693)Instructions burned: 180 (million) % 9.27/2.20 % (1102703)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3996963925:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi) % 19.78/3.64 % (1102704)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1023055653:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 19.78/3.64 % (1102696)------------------------------ % 19.78/3.64 % (1102696)------------------------------ % 19.78/3.64 % (1102703)Instruction limit reached! % 19.78/3.64 % (1102703)------------------------------ % 19.78/3.64 % (1102703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.78/3.64 % (1102703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.78/3.64 % (1102703)CaDiCaL version: 2.1.3 % 19.78/3.64 % (1102703)Termination reason: Instruction limit % 19.78/3.64 % (1102703)Termination phase: Saturation % 19.78/3.64 % (1102703)Time elapsed: 0.104 s % 19.78/3.64 % (1102703)Peak memory usage: 90 MB % 19.78/3.64 % (1102703)Instructions burned: 189 (million) % 19.78/3.64 % (1102706)lrs+10_64_to=lpo:sil=8000:random_seed=4280234286:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 19.78/3.64 % (1102709)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2432160971:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi) % 19.78/3.64 % (1102704)Instruction limit reached! % 19.78/3.64 % (1102704)------------------------------ % 19.78/3.64 % (1102704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.78/3.64 % (1102704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.78/3.64 % (1102704)CaDiCaL version: 2.1.3 % 19.78/3.64 % (1102704)Termination reason: Instruction limit % 19.78/3.64 % (1102704)Termination phase: Saturation % 19.78/3.64 % (1102704)Time elapsed: 0.147 s % 19.78/3.64 % (1102704)Peak memory usage: 90 MB % 19.78/3.64 % (1102704)Instructions burned: 220 (million) % 19.78/3.64 % (1102706)Instruction limit reached! % 19.78/3.64 % (1102706)------------------------------ % 19.78/3.64 % (1102706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.78/3.64 % (1102706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.78/3.64 % (1102706)CaDiCaL version: 2.1.3 % 19.78/3.64 % (1102706)Termination reason: Instruction limit % 19.78/3.64 % (1102706)Termination phase: Saturation % 19.78/3.64 % (1102706)Time elapsed: 0.081 s % 19.78/3.64 % (1102706)Peak memory usage: 89 MB % 19.78/3.64 % (1102706)Instructions burned: 126 (million) % 19.78/3.64 % (1102709)Instruction limit reached! % 19.78/3.64 % (1102709)------------------------------ % 19.78/3.64 % (1102709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.78/3.64 % (1102709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.78/3.64 % (1102709)CaDiCaL version: 2.1.3 % 19.78/3.64 % (1102709)Termination reason: Instruction limit % 19.78/3.64 % (1102709)Termination phase: Saturation % 19.78/3.64 % (1102709)Time elapsed: 0.061 s % 19.78/3.64 % (1102709)Peak memory usage: 90 MB % 19.78/3.64 % (1102709)Instructions burned: 195 (million) % 19.78/3.64 % (1102710)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2953324930:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 19.78/3.64 % (1102715)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2592667877:i=107_2994 on theBenchmark for (2994ds/107Mi) % 19.78/3.64 % (1102715)Refutation not found, incomplete strategy % 19.78/3.64 % (1102715)------------------------------ % 19.78/3.64 % (1102715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.78/3.64 % (1102715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.78/3.64 % (1102715)CaDiCaL version: 2.1.3 % 19.78/3.64 % (1102715)Termination reason: Refutation not found, incomplete strategy % 19.78/3.64 % (1102715)Time elapsed: 0.004 s % 19.78/3.64 % (1102715)Peak memory usage: 88 MB % 19.78/3.64 % (1102715)Instructions burned: 11 (million) % 19.78/3.64 % (1102713)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=999447861:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 19.78/3.64 % (1102714)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=3079964951:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 19.78/3.64 % (1102710)Instruction limit reached! % 19.78/3.64 % (1102710)------------------------------ % 26.59/4.64 % (1102710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.64 % (1102710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.64 % (1102710)CaDiCaL version: 2.1.3 % 26.59/4.64 % (1102710)Termination reason: Instruction limit % 26.59/4.64 % (1102710)Termination phase: Saturation % 26.59/4.64 % (1102710)Time elapsed: 0.111 s % 26.59/4.64 % (1102710)Peak memory usage: 91 MB % 26.59/4.64 % (1102710)Instructions burned: 157 (million) % 26.59/4.64 % (1102714)Instruction limit reached! % 26.59/4.64 % (1102714)------------------------------ % 26.59/4.64 % (1102714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.64 % (1102714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.64 % (1102714)CaDiCaL version: 2.1.3 % 26.59/4.64 % (1102714)Termination reason: Instruction limit % 26.59/4.64 % (1102714)Termination phase: Saturation % 26.59/4.64 % (1102714)Time elapsed: 0.064 s % 26.59/4.64 % (1102714)Peak memory usage: 89 MB % 26.59/4.64 % (1102714)Instructions burned: 106 (million) % 26.59/4.64 % (1102715)------------------------------ % 26.59/4.64 % (1102715)------------------------------ % 26.59/4.64 % (1102720)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1583375171:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi) % 26.59/4.64 % (1102721)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2941945886:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi) % 26.59/4.64 % (1102722)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=239837421:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi) % 26.59/4.64 % (1102722)Refutation not found, incomplete strategy % 26.59/4.64 % (1102722)------------------------------ % 26.59/4.64 % (1102722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.64 % (1102722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.64 % (1102722)CaDiCaL version: 2.1.3 % 26.59/4.64 % (1102722)Termination reason: Refutation not found, incomplete strategy % 26.59/4.64 % (1102722)Time elapsed: 0.005 s % 26.59/4.64 % (1102722)Peak memory usage: 88 MB % 26.59/4.64 % (1102722)Instructions burned: 12 (million) % 26.59/4.64 % (1102720)Instruction limit reached! % 26.59/4.64 % (1102720)------------------------------ % 26.59/4.64 % (1102720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.64 % (1102720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.64 % (1102720)CaDiCaL version: 2.1.3 % 26.59/4.64 % (1102720)Termination reason: Instruction limit % 26.59/4.64 % (1102720)Termination phase: Saturation % 26.59/4.64 % (1102720)Time elapsed: 0.140 s % 26.59/4.64 % (1102720)Peak memory usage: 91 MB % 26.59/4.64 % (1102720)Instructions burned: 242 (million) % 26.59/4.64 % (1102722)------------------------------ % 26.59/4.64 % (1102722)------------------------------ % 26.59/4.64 % (1102726)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4238362274:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi) % 26.59/4.64 % (1102727)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1493028887:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi) % 26.59/4.64 % (1102727)Instruction limit reached! % 26.59/4.64 % (1102727)------------------------------ % 26.59/4.64 % (1102727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.64 % (1102727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.64 % (1102727)CaDiCaL version: 2.1.3 % 26.59/4.64 % (1102727)Termination reason: Instruction limit % 26.59/4.64 % (1102727)Termination phase: Saturation % 26.59/4.64 % (1102727)Time elapsed: 0.056 s % 26.59/4.64 % (1102727)Peak memory usage: 89 MB % 26.59/4.64 % (1102727)Instructions burned: 192 (million) % 26.59/4.64 % (1102730)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3018993526:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi) % 26.59/4.64 % (1102730)Instruction limit reached! % 26.59/4.64 % (1102730)------------------------------ % 26.59/4.64 % (1102730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.59/4.64 % (1102730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.59/4.64 % (1102730)CaDiCaL version: 2.1.3 % 26.59/4.64 % (1102730)Termination reason: Instruction limit % 48.77/7.78 % (1102730)Termination phase: Saturation % 48.77/7.78 % (1102730)Time elapsed: 0.093 s % 48.77/7.78 % (1102730)Peak memory usage: 92 MB % 48.77/7.78 % (1102730)Instructions burned: 274 (million) % 48.77/7.78 % (1102726)Instruction limit reached! % 48.77/7.78 % (1102726)------------------------------ % 48.77/7.78 % (1102726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.77/7.78 % (1102726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.77/7.78 % (1102726)CaDiCaL version: 2.1.3 % 48.77/7.78 % (1102726)Termination reason: Instruction limit % 48.77/7.78 % (1102726)Termination phase: Saturation % 48.77/7.78 % (1102726)Time elapsed: 0.303 s % 48.77/7.78 % (1102726)Peak memory usage: 92 MB % 48.77/7.78 % (1102726)Instructions burned: 499 (million) % 48.77/7.78 % (1102732)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3723214809:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi) % 48.77/7.78 % (1102733)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=583803868:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi) % 48.77/7.78 % (1102732)Instruction limit reached! % 48.77/7.78 % (1102732)------------------------------ % 48.77/7.78 % (1102732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.77/7.78 % (1102732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.77/7.78 % (1102732)CaDiCaL version: 2.1.3 % 48.77/7.78 % (1102732)Termination reason: Instruction limit % 48.77/7.78 % (1102732)Termination phase: Saturation % 48.77/7.78 % (1102732)Time elapsed: 0.093 s % 48.77/7.78 % (1102732)Peak memory usage: 89 MB % 48.77/7.78 % (1102732)Instructions burned: 157 (million) % 48.77/7.78 % (1102736)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1293895484:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi) % 48.77/7.78 % (1102736)Instruction limit reached! % 48.77/7.78 % (1102736)------------------------------ % 48.77/7.78 % (1102736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.77/7.78 % (1102736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.77/7.78 % (1102736)CaDiCaL version: 2.1.3 % 48.77/7.78 % (1102736)Termination reason: Instruction limit % 48.77/7.78 % (1102736)Termination phase: Saturation % 48.77/7.78 % (1102736)Time elapsed: 0.188 s % 48.77/7.78 % (1102736)Peak memory usage: 87 MB % 48.77/7.78 % (1102736)Instructions burned: 538 (million) % 48.77/7.78 % (1102738)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2371779834:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi) % 48.77/7.78 % (1102738)Instruction limit reached! % 48.77/7.78 % (1102738)------------------------------ % 48.77/7.78 % (1102738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.77/7.78 % (1102738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.77/7.78 % (1102738)CaDiCaL version: 2.1.3 % 48.77/7.78 % (1102738)Termination reason: Instruction limit % 48.77/7.78 % (1102738)Termination phase: Saturation % 48.77/7.78 % (1102738)Time elapsed: 0.094 s % 48.77/7.78 % (1102738)Peak memory usage: 90 MB % 48.77/7.78 % (1102738)Instructions burned: 180 (million) % 48.77/7.78 % (1102740)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=2040396273:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/10307Mi) % 48.77/7.78 % (1102721)Instruction limit reached! % 48.77/7.78 % (1102721)------------------------------ % 48.77/7.78 % (1102721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.77/7.78 % (1102721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.77/7.78 % (1102721)CaDiCaL version: 2.1.3 % 48.77/7.78 % (1102721)Termination reason: Instruction limit % 48.77/7.78 % (1102721)Termination phase: Saturation % 48.77/7.78 % (1102721)Time elapsed: 1.906 s % 48.77/7.78 % (1102721)Peak memory usage: 147 MB % 48.77/7.78 % (1102721)Instructions burned: 5209 (million) % 48.77/7.78 % (1102713)Instruction limit reached! % 48.77/7.78 % (1102713)------------------------------ % 48.77/7.78 % (1102713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.77/7.78 % (1102713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.77/7.78 % (1102713)CaDiCaL version: 2.1.3 % 48.77/7.78 % (1102713)Termination reason: Instruction limit % 48.77/7.78 % (1102713)Termination phase: Saturation % 65.35/10.09 % (1102713)Time elapsed: 2.157 s % 65.35/10.09 % (1102713)Peak memory usage: 147 MB % 65.35/10.09 % (1102713)Instructions burned: 3394 (million) % 65.35/10.09 % (1102742)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=1120266923:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi) % 65.35/10.09 % (1102743)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=766730921:s2pl=no:i=8478:s2at=4:nm=6_2972 on theBenchmark for (2972ds/8478Mi) % 65.35/10.09 % (1102742)Instruction limit reached! % 65.35/10.09 % (1102742)------------------------------ % 65.35/10.09 % (1102742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.35/10.09 % (1102742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.35/10.09 % (1102742)CaDiCaL version: 2.1.3 % 65.35/10.09 % (1102742)Termination reason: Instruction limit % 65.35/10.09 % (1102742)Termination phase: Saturation % 65.35/10.09 % (1102742)Time elapsed: 0.100 s % 65.35/10.09 % (1102742)Peak memory usage: 90 MB % 65.35/10.09 % (1102742)Instructions burned: 415 (million) % 65.35/10.09 % (1102746)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=2511875610:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi) % 65.35/10.09 % (1102746)Instruction limit reached! % 65.35/10.09 % (1102746)------------------------------ % 65.35/10.09 % (1102746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.35/10.09 % (1102746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.35/10.09 % (1102746)CaDiCaL version: 2.1.3 % 65.35/10.09 % (1102746)Termination reason: Instruction limit % 65.35/10.09 % (1102746)Termination phase: Saturation % 65.35/10.09 % (1102746)Time elapsed: 0.060 s % 65.35/10.09 % (1102746)Peak memory usage: 88 MB % 65.35/10.09 % (1102746)Instructions burned: 308 (million) % 65.35/10.09 % (1102748)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3048057276:st=4:i=720:sd=3:fsr=off:ss=axioms_2969 on theBenchmark for (2969ds/720Mi) % 65.35/10.09 % (1102748)Instruction limit reached! % 65.35/10.09 % (1102748)------------------------------ % 65.35/10.09 % (1102748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.35/10.09 % (1102748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.35/10.09 % (1102748)CaDiCaL version: 2.1.3 % 65.35/10.09 % (1102748)Termination reason: Instruction limit % 65.35/10.09 % (1102748)Termination phase: Saturation % 65.35/10.09 % (1102748)Time elapsed: 0.263 s % 65.35/10.09 % (1102748)Peak memory usage: 96 MB % 65.35/10.09 % (1102748)Instructions burned: 722 (million) % 65.35/10.09 % (1102733)Instruction limit reached! % 65.35/10.09 % (1102733)------------------------------ % 65.35/10.09 % (1102733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.35/10.09 % (1102733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.35/10.09 % (1102733)CaDiCaL version: 2.1.3 % 65.35/10.09 % (1102733)Termination reason: Instruction limit % 65.35/10.09 % (1102733)Termination phase: Saturation % 65.35/10.09 % (1102733)Time elapsed: 2.003 s % 65.35/10.09 % (1102733)Peak memory usage: 147 MB % 65.35/10.09 % (1102733)Instructions burned: 3258 (million) % 65.35/10.10 % (1102750)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3830649141:i=598:bs=on:bd=preordered:av=off:ss=axioms_2965 on theBenchmark for (2965ds/598Mi) % 65.35/10.10 % (1102751)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1065624853:i=2989:sd=3:ss=axioms:sgt=60_2964 on theBenchmark for (2964ds/2989Mi) % 65.35/10.10 % (1102750)Instruction limit reached! % 65.35/10.10 % (1102750)------------------------------ % 65.35/10.10 % (1102750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.35/10.10 % (1102750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.35/10.10 % (1102750)CaDiCaL version: 2.1.3 % 65.35/10.10 % (1102750)Termination reason: Instruction limit % 65.35/10.10 % (1102750)Termination phase: Saturation % 65.35/10.10 % (1102750)Time elapsed: 0.184 s % 65.35/10.10 % (1102750)Peak memory usage: 90 MB % 65.35/10.10 % (1102750)Instructions burned: 600 (million) % 65.35/10.10 % (1102754)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=2413420289:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2963 on theBenchmark for (2963ds/1997Mi) % 97.75/14.65 % (1102754)Instruction limit reached! % 97.75/14.65 % (1102754)------------------------------ % 97.75/14.65 % (1102754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.75/14.65 % (1102754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.75/14.65 % (1102754)CaDiCaL version: 2.1.3 % 97.75/14.65 % (1102754)Termination reason: Instruction limit % 97.75/14.65 % (1102754)Termination phase: Saturation % 97.75/14.65 % (1102754)Time elapsed: 0.739 s % 97.75/14.65 % (1102754)Peak memory usage: 138 MB % 97.75/14.65 % (1102754)Instructions burned: 1998 (million) % 97.75/14.65 % (1102756)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=2087712107:i=2088:bd=preordered:av=off_2954 on theBenchmark for (2954ds/2088Mi) % 97.75/14.65 % (1102756)Instruction limit reached! % 97.75/14.65 % (1102756)------------------------------ % 97.75/14.65 % (1102756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.75/14.65 % (1102756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.75/14.65 % (1102756)CaDiCaL version: 2.1.3 % 97.75/14.65 % (1102756)Termination reason: Instruction limit % 97.75/14.65 % (1102756)Termination phase: Saturation % 97.75/14.65 % (1102756)Time elapsed: 0.725 s % 97.75/14.65 % (1102756)Peak memory usage: 139 MB % 97.75/14.65 % (1102756)Instructions burned: 2090 (million) % 97.75/14.65 % (1102758)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1025480243:i=1098:nicw=on_2946 on theBenchmark for (2946ds/1098Mi) % 97.75/14.65 % (1102751)Instruction limit reached! % 97.75/14.65 % (1102751)------------------------------ % 97.75/14.65 % (1102751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.75/14.65 % (1102751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.75/14.65 % (1102751)CaDiCaL version: 2.1.3 % 97.75/14.65 % (1102751)Termination reason: Instruction limit % 97.75/14.65 % (1102751)Termination phase: Saturation % 97.75/14.65 % (1102751)Time elapsed: 1.946 s % 97.75/14.65 % (1102751)Peak memory usage: 146 MB % 97.75/14.65 % (1102751)Instructions burned: 2990 (million) % 97.75/14.65 % (1102760)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2990387494:i=433:bd=preordered_2944 on theBenchmark for (2944ds/433Mi) % 97.75/14.65 % (1102760)Refutation not found, incomplete strategy % 97.75/14.65 % (1102760)------------------------------ % 97.75/14.65 % (1102760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.75/14.65 % (1102760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.75/14.65 % (1102760)CaDiCaL version: 2.1.3 % 97.75/14.65 % (1102760)Termination reason: Refutation not found, incomplete strategy % 97.75/14.65 % (1102760)Time elapsed: 0.012 s % 97.75/14.65 % (1102760)Peak memory usage: 88 MB % 97.75/14.65 % (1102760)Instructions burned: 19 (million) % 97.75/14.65 % (1102758)Instruction limit reached! % 97.75/14.65 % (1102758)------------------------------ % 97.75/14.65 % (1102758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.75/14.65 % (1102758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.75/14.65 % (1102758)CaDiCaL version: 2.1.3 % 97.75/14.65 % (1102758)Termination reason: Instruction limit % 97.75/14.65 % (1102758)Termination phase: Saturation % 97.75/14.65 % (1102758)Time elapsed: 0.363 s % 97.75/14.65 % (1102758)Peak memory usage: 101 MB % 97.75/14.65 % (1102758)Instructions burned: 1101 (million) % 97.75/14.65 % (1102762)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4130962140:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2942 on theBenchmark for (2942ds/2942Mi) % 97.75/14.65 % (1102760)------------------------------ % 97.75/14.65 % (1102760)------------------------------ % 97.75/14.65 % (1102764)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=666280774:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2940 on theBenchmark for (2940ds/6922Mi) % 97.75/14.65 % (1102762)Instruction limit reached! % 97.75/14.65 % (1102762)------------------------------ % 97.75/14.65 % (1102762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.46/15.90 % (1102762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.46/15.90 % (1102762)CaDiCaL version: 2.1.3 % 105.46/15.90 % (1102762)Termination reason: Instruction limit % 105.46/15.90 % (1102762)Termination phase: Saturation % 105.46/15.90 % (1102762)Time elapsed: 1.030 s % 105.46/15.90 % (1102762)Peak memory usage: 147 MB % 105.46/15.90 % (1102762)Instructions burned: 2944 (million) % 105.46/15.90 % (1102766)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=3037032097:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2930 on theBenchmark for (2930ds/596Mi) % 105.46/15.90 % (1102766)Instruction limit reached! % 105.46/15.90 % (1102766)------------------------------ % 105.46/15.90 % (1102766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.46/15.90 % (1102766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.46/15.90 % (1102766)CaDiCaL version: 2.1.3 % 105.46/15.90 % (1102766)Termination reason: Instruction limit % 105.46/15.90 % (1102766)Termination phase: Saturation % 105.46/15.90 % (1102766)Time elapsed: 0.177 s % 105.46/15.90 % (1102766)Peak memory usage: 99 MB % 105.46/15.90 % (1102766)Instructions burned: 600 (million) % 105.46/15.90 % (1102768)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=717303705:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2928 on theBenchmark for (2928ds/4123Mi) % 105.46/15.90 % (1102743)Instruction limit reached! % 105.46/15.90 % (1102743)------------------------------ % 105.46/15.90 % (1102743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.46/15.90 % (1102743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.46/15.90 % (1102743)CaDiCaL version: 2.1.3 % 105.46/15.90 % (1102743)Termination reason: Instruction limit % 105.46/15.90 % (1102743)Termination phase: Saturation % 105.46/15.90 % (1102743)Time elapsed: 4.968 s % 105.46/15.90 % (1102743)Peak memory usage: 164 MB % 105.46/15.90 % (1102743)Instructions burned: 8479 (million) % 105.46/15.90 % (1102770)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2308393448:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2921 on theBenchmark for (2921ds/16411Mi) % 105.46/15.90 % (1102740)Instruction limit reached! % 105.46/15.90 % (1102740)------------------------------ % 105.46/15.90 % (1102740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.46/15.90 % (1102740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.46/15.90 % (1102740)CaDiCaL version: 2.1.3 % 105.46/15.90 % (1102740)Termination reason: Instruction limit % 105.46/15.90 % (1102740)Termination phase: Saturation % 105.46/15.90 % (1102740)Time elapsed: 6.387 s % 105.46/15.90 % (1102740)Peak memory usage: 170 MB % 105.46/15.90 % (1102740)Instructions burned: 10308 (million) % 105.46/15.90 % (1102768)Instruction limit reached! % 105.46/15.90 % (1102768)------------------------------ % 105.46/15.90 % (1102768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.46/15.90 % (1102768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.46/15.90 % (1102768)CaDiCaL version: 2.1.3 % 105.46/15.90 % (1102768)Termination reason: Instruction limit % 105.46/15.90 % (1102768)Termination phase: Saturation % 105.46/15.90 % (1102768)Time elapsed: 1.391 s % 105.46/15.90 % (1102768)Peak memory usage: 155 MB % 105.46/15.90 % (1102768)Instructions burned: 4126 (million) % 105.46/15.90 % (1102773)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=2709817428:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2913 on theBenchmark for (2913ds/1722Mi) % 105.46/15.90 % (1102772)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2385789883:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2913 on theBenchmark for (2913ds/1670Mi) % 105.46/15.90 % (1102773)Refutation not found, incomplete strategy % 105.46/15.90 % (1102773)------------------------------ % 105.46/15.90 % (1102773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.46/15.90 % (1102773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.46/15.90 % (1102773)CaDiCaL version: 2.1.3 % 105.46/15.90 % (1102773)Termination reason: Refutation not found, incomplete strategy % 105.46/15.90 % (1102773)Time elapsed: 0.331 s % 105.46/15.90 % (1102773)Peak memory usage: 129 MB % 105.46/15.90 % (1102773)Instructions burned: 926 (million) % 105.46/15.90 % (1102773)------------------------------ % 120.48/17.96 % (1102773)------------------------------ % 120.48/17.96 % (1102776)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=3019406034:cts=off:cond=on:i=9530:bs=on:fsd=on_2907 on theBenchmark for (2907ds/9530Mi) % 120.48/17.96 % (1102772)Instruction limit reached! % 120.48/17.96 % (1102772)------------------------------ % 120.48/17.96 % (1102772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.48/17.96 % (1102772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.48/17.96 % (1102772)CaDiCaL version: 2.1.3 % 120.48/17.96 % (1102772)Termination reason: Instruction limit % 120.48/17.96 % (1102772)Termination phase: Saturation % 120.48/17.96 % (1102772)Time elapsed: 1.031 s % 120.48/17.96 % (1102772)Peak memory usage: 136 MB % 120.48/17.96 % (1102772)Instructions burned: 1671 (million) % 120.48/17.96 % (1102764)Instruction limit reached! % 120.48/17.96 % (1102764)------------------------------ % 120.48/17.96 % (1102764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.48/17.97 % (1102764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.48/17.97 % (1102764)CaDiCaL version: 2.1.3 % 120.48/17.97 % (1102764)Termination reason: Instruction limit % 120.48/17.97 % (1102764)Termination phase: Saturation % 120.48/17.97 % (1102764)Time elapsed: 3.738 s % 120.48/17.97 % (1102764)Peak memory usage: 181 MB % 120.48/17.97 % (1102764)Instructions burned: 6923 (million) % 120.48/17.97 % (1102778)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2927290795:st=2:i=4495:sd=10:ss=included_2901 on theBenchmark for (2901ds/4495Mi) % 120.48/17.97 % (1102779)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=2830890796:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2901 on theBenchmark for (2901ds/4920Mi) % 120.48/17.97 % (1102778)Instruction limit reached! % 120.48/17.97 % (1102778)------------------------------ % 120.48/17.97 % (1102778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.48/17.97 % (1102778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.48/17.97 % (1102778)CaDiCaL version: 2.1.3 % 120.48/17.97 % (1102778)Termination reason: Instruction limit % 120.48/17.97 % (1102778)Termination phase: Saturation % 120.48/17.97 % (1102778)Time elapsed: 2.606 s % 120.48/17.97 % (1102778)Peak memory usage: 164 MB % 120.48/17.97 % (1102778)Instructions burned: 4496 (million) % 120.48/17.97 % (1102782)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=2562380457:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2874 on theBenchmark for (2874ds/2083Mi) % 120.48/17.97 % (1102776)Instruction limit reached! % 120.48/17.97 % (1102776)------------------------------ % 120.48/17.97 % (1102776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.48/17.97 % (1102776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.48/17.97 % (1102776)CaDiCaL version: 2.1.3 % 120.48/17.97 % (1102776)Termination reason: Instruction limit % 120.48/17.97 % (1102776)Termination phase: Saturation % 120.48/17.97 % (1102776)Time elapsed: 3.532 s % 120.48/17.97 % (1102776)Peak memory usage: 180 MB % 120.48/17.97 % (1102776)Instructions burned: 9533 (million) % 120.48/17.97 % (1102779)Instruction limit reached! % 120.48/17.97 % (1102779)------------------------------ % 120.48/17.97 % (1102779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.48/17.97 % (1102779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.48/17.97 % (1102779)CaDiCaL version: 2.1.3 % 120.48/17.97 % (1102779)Termination reason: Instruction limit % 120.48/17.97 % (1102779)Termination phase: Saturation % 120.48/17.97 % (1102779)Time elapsed: 2.922 s % 120.48/17.97 % (1102779)Peak memory usage: 153 MB % 120.48/17.97 % (1102779)Instructions burned: 4921 (million) % 120.48/17.97 % (1102784)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=3063861610:i=4629:av=off:gsp=on_2871 on theBenchmark for (2871ds/4629Mi) % 120.48/17.97 % (1102785)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1965737375:i=1258:av=off_2870 on theBenchmark for (2870ds/1258Mi) % 120.48/17.97 % (1102785)Instruction limit reached! % 120.48/17.97 % (1102785)------------------------------ % 146.32/21.57 % (1102785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.32/21.57 % (1102785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.32/21.57 % (1102785)CaDiCaL version: 2.1.3 % 146.32/21.57 % (1102785)Termination reason: Instruction limit % 146.32/21.57 % (1102785)Termination phase: Saturation % 146.32/21.57 % (1102785)Time elapsed: 0.706 s % 146.32/21.57 % (1102785)Peak memory usage: 94 MB % 146.32/21.57 % (1102785)Instructions burned: 1259 (million) % 146.32/21.57 % (1102788)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4097905223:i=7343:av=off:ss=included_2862 on theBenchmark for (2862ds/7343Mi) % 146.32/21.57 % (1102782)Instruction limit reached! % 146.32/21.57 % (1102782)------------------------------ % 146.32/21.57 % (1102782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.32/21.57 % (1102782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.32/21.57 % (1102782)CaDiCaL version: 2.1.3 % 146.32/21.57 % (1102782)Termination reason: Instruction limit % 146.32/21.57 % (1102782)Termination phase: Saturation % 146.32/21.58 % (1102782)Time elapsed: 1.301 s % 146.32/21.58 % (1102782)Peak memory usage: 138 MB % 146.32/21.58 % (1102782)Instructions burned: 2084 (million) % 146.32/21.58 % (1102790)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2721862304:i=1325:sd=2:ss=axioms:sgt=16_2860 on theBenchmark for (2860ds/1325Mi) % 146.32/21.58 % (1102790)Refutation not found, incomplete strategy % 146.32/21.58 % (1102790)------------------------------ % 146.32/21.58 % (1102790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.32/21.58 % (1102790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.32/21.58 % (1102790)CaDiCaL version: 2.1.3 % 146.32/21.58 % (1102790)Termination reason: Refutation not found, incomplete strategy % 146.32/21.58 % (1102790)Time elapsed: 0.043 s % 146.32/21.58 % (1102790)Peak memory usage: 89 MB % 146.32/21.58 % (1102790)Instructions burned: 66 (million) % 146.32/21.58 % (1102790)------------------------------ % 146.32/21.58 % (1102790)------------------------------ % 146.32/21.58 % (1102784)Instruction limit reached! % 146.32/21.58 % (1102784)------------------------------ % 146.32/21.58 % (1102784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.32/21.58 % (1102784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.32/21.58 % (1102784)CaDiCaL version: 2.1.3 % 146.32/21.58 % (1102784)Termination reason: Instruction limit % 146.32/21.58 % (1102784)Termination phase: Saturation % 146.32/21.58 % (1102784)Time elapsed: 1.457 s % 146.32/21.58 % (1102784)Peak memory usage: 147 MB % 146.32/21.58 % (1102784)Instructions burned: 4631 (million) % 146.32/21.58 % (1102793)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=4147388806:i=1489:sd=2:ep=R:ss=axioms_2855 on theBenchmark for (2855ds/1489Mi) % 146.32/21.58 % (1102788)Refutation not found, incomplete strategy % 146.32/21.58 % (1102788)------------------------------ % 146.32/21.58 % (1102788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.32/21.58 % (1102788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.32/21.58 % (1102788)CaDiCaL version: 2.1.3 % 146.32/21.58 % (1102788)Termination reason: Refutation not found, incomplete strategy % 146.32/21.58 % (1102788)Time elapsed: 0.598 s % 146.32/21.58 % (1102788)Peak memory usage: 127 MB % 146.32/21.58 % (1102788)Instructions burned: 900 (million) % 146.32/21.58 % (1102792)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=3214691186:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2855 on theBenchmark for (2855ds/2646Mi) % 146.32/21.58 % (1102788)------------------------------ % 146.32/21.58 % (1102788)------------------------------ % 146.32/21.58 % (1102796)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=1883467608:i=1503_2852 on theBenchmark for (2852ds/1503Mi) % 146.32/21.58 % (1102793)Instruction limit reached! % 146.32/21.58 % (1102793)------------------------------ % 146.32/21.58 % (1102793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.32/21.58 % (1102793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.32/21.58 % (1102793)CaDiCaL version: 2.1.3 % 146.32/21.58 % (1102793)Termination reason: Instruction limit % 146.32/21.58 % (1102793)Termination phase: Saturation % 146.32/21.58 % (1102793)Time elapsed: 0.539 s % 174.34/25.50 % (1102793)Peak memory usage: 135 MB % 174.34/25.50 % (1102793)Instructions burned: 1492 (million) % 174.34/25.50 % (1102798)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1580760714:i=13942:kws=frequency_2849 on theBenchmark for (2849ds/13942Mi) % 174.34/25.50 % (1102792)Instruction limit reached! % 174.34/25.50 % (1102792)------------------------------ % 174.34/25.50 % (1102792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.34/25.50 % (1102792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.34/25.50 % (1102792)CaDiCaL version: 2.1.3 % 174.34/25.50 % (1102792)Termination reason: Instruction limit % 174.34/25.50 % (1102792)Termination phase: Saturation % 174.34/25.50 % (1102792)Time elapsed: 1.122 s % 174.34/25.50 % (1102792)Peak memory usage: 141 MB % 174.34/25.50 % (1102792)Instructions burned: 2647 (million) % 174.34/25.50 % (1102800)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=3852974444:i=3604:fsr=off:er=filter_2843 on theBenchmark for (2843ds/3604Mi) % 174.34/25.50 % (1102796)Instruction limit reached! % 174.34/25.50 % (1102796)------------------------------ % 174.34/25.50 % (1102796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.34/25.50 % (1102796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.34/25.50 % (1102796)CaDiCaL version: 2.1.3 % 174.34/25.50 % (1102796)Termination reason: Instruction limit % 174.34/25.50 % (1102796)Termination phase: Saturation % 174.34/25.50 % (1102796)Time elapsed: 0.992 s % 174.34/25.50 % (1102796)Peak memory usage: 134 MB % 174.34/25.50 % (1102796)Instructions burned: 1503 (million) % 174.34/25.50 % (1102802)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1930285423:i=1876:sd=1:ss=included:sgt=32_2841 on theBenchmark for (2841ds/1876Mi) % 174.34/25.50 % (1102770)Instruction limit reached! % 174.34/25.50 % (1102770)------------------------------ % 174.34/25.50 % (1102770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.34/25.50 % (1102770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.34/25.50 % (1102770)CaDiCaL version: 2.1.3 % 174.34/25.50 % (1102770)Termination reason: Instruction limit % 174.34/25.50 % (1102770)Termination phase: Saturation % 174.34/25.50 % (1102770)Time elapsed: 8.552 s % 174.34/25.50 % (1102770)Peak memory usage: 179 MB % 174.34/25.50 % (1102770)Instructions burned: 16413 (million) % 174.34/25.50 % (1102802)Refutation not found, incomplete strategy % 174.34/25.50 % (1102802)------------------------------ % 174.34/25.50 % (1102802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.34/25.50 % (1102802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.34/25.50 % (1102802)CaDiCaL version: 2.1.3 % 174.34/25.50 % (1102802)Termination reason: Refutation not found, incomplete strategy % 174.34/25.50 % (1102802)Time elapsed: 0.570 s % 174.34/25.50 % (1102802)Peak memory usage: 127 MB % 174.34/25.50 % (1102802)Instructions burned: 868 (million) % 174.34/25.50 % (1102804)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3211754551:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2834 on theBenchmark for (2834ds/1932Mi) % 174.34/25.50 % (1102802)------------------------------ % 174.34/25.50 % (1102802)------------------------------ % 174.34/25.50 % (1102806)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=3700369757:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2831 on theBenchmark for (2831ds/1980Mi) % 174.34/25.50 % (1102800)Instruction limit reached! % 174.34/25.50 % (1102800)------------------------------ % 174.34/25.50 % (1102800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.34/25.50 % (1102800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.34/25.50 % (1102800)CaDiCaL version: 2.1.3 % 174.34/25.50 % (1102800)Termination reason: Instruction limit % 174.34/25.50 % (1102800)Termination phase: Saturation % 174.34/25.50 % (1102800)Time elapsed: 1.254 s % 174.34/25.50 % (1102800)Peak memory usage: 151 MB % 174.34/25.50 % (1102800)Instructions burned: 3606 (million) % 174.34/25.50 % (1102808)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=1611047812:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2829 on theBenchmark for (2829ds/3902Mi) % 191.27/27.82 % (1102804)Instruction limit reached! % 191.27/27.82 % (1102804)------------------------------ % 191.27/27.82 % (1102804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.27/27.82 % (1102804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.27/27.82 % (1102804)CaDiCaL version: 2.1.3 % 191.27/27.82 % (1102804)Termination reason: Instruction limit % 191.27/27.82 % (1102804)Termination phase: Saturation % 191.27/27.82 % (1102804)Time elapsed: 1.202 s % 191.27/27.82 % (1102804)Peak memory usage: 134 MB % 191.27/27.82 % (1102804)Instructions burned: 1932 (million) % 191.27/27.82 % (1102810)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=3377508118:avsq=on:i=3916:aac=none:amm=off_2820 on theBenchmark for (2820ds/3916Mi) % 191.27/27.82 % (1102806)Instruction limit reached! % 191.27/27.82 % (1102806)------------------------------ % 191.27/27.82 % (1102806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.27/27.82 % (1102806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.27/27.82 % (1102806)CaDiCaL version: 2.1.3 % 191.27/27.82 % (1102806)Termination reason: Instruction limit % 191.27/27.82 % (1102806)Termination phase: Saturation % 191.27/27.82 % (1102806)Time elapsed: 1.273 s % 191.27/27.82 % (1102806)Peak memory usage: 138 MB % 191.27/27.82 % (1102806)Instructions burned: 1981 (million) % 191.27/27.82 % (1102812)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=597141191:cond=on:i=3940:av=off:er=known_2817 on theBenchmark for (2817ds/3940Mi) % 191.27/27.82 % (1102808)Instruction limit reached! % 191.27/27.82 % (1102808)------------------------------ % 191.27/27.82 % (1102808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.27/27.82 % (1102808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.27/27.82 % (1102808)CaDiCaL version: 2.1.3 % 191.27/27.82 % (1102808)Termination reason: Instruction limit % 191.27/27.82 % (1102808)Termination phase: Saturation % 191.27/27.82 % (1102808)Time elapsed: 1.367 s % 191.27/27.82 % (1102808)Peak memory usage: 154 MB % 191.27/27.82 % (1102808)Instructions burned: 3903 (million) % 191.27/27.82 % (1102814)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=3519712242:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2815 on theBenchmark for (2815ds/3980Mi) % 191.27/27.82 % (1102812)Instruction limit reached! % 191.27/27.82 % (1102812)------------------------------ % 191.27/27.82 % (1102812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.27/27.82 % (1102812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.27/27.82 % (1102812)CaDiCaL version: 2.1.3 % 191.27/27.82 % (1102812)Termination reason: Instruction limit % 191.27/27.82 % (1102812)Termination phase: Saturation % 191.27/27.82 % (1102812)Time elapsed: 1.490 s % 191.27/27.82 % (1102812)Peak memory usage: 150 MB % 191.27/27.82 % (1102812)Instructions burned: 3945 (million) % 191.27/27.82 % (1102816)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=3303810220:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2801 on theBenchmark for (2801ds/2087Mi) % 191.27/27.82 % (1102810)Instruction limit reached! % 191.27/27.82 % (1102810)------------------------------ % 191.27/27.82 % (1102810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.27/27.82 % (1102810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.27/27.82 % (1102810)CaDiCaL version: 2.1.3 % 191.27/27.82 % (1102810)Termination reason: Instruction limit % 191.27/27.82 % (1102810)Termination phase: Saturation % 191.27/27.82 % (1102810)Time elapsed: 2.215 s % 191.27/27.82 % (1102810)Peak memory usage: 106 MB % 191.27/27.82 % (1102810)Instructions burned: 3916 (million) % 191.27/27.82 % (1102818)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=310354150:cts=off:cond=on:i=4272:bs=on:fsd=on_2797 on theBenchmark for (2797ds/4272Mi) % 191.27/27.82 % (1102816)Instruction limit reached! % 191.27/27.82 % (1102816)------------------------------ % 191.27/27.82 % (1102816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.27/27.82 % (1102816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.27/27.82 % (1102816)CaDiCaL version: 2.1.3 % 255.95/36.99 % (1102816)Termination reason: Instruction limit % 255.95/36.99 % (1102816)Termination phase: Saturation % 255.95/36.99 % (1102816)Time elapsed: 0.751 s % 255.95/36.99 % (1102816)Peak memory usage: 140 MB % 255.95/36.99 % (1102816)Instructions burned: 2088 (million) % 255.95/36.99 % (1102820)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2301196525:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2792 on theBenchmark for (2792ds/2197Mi) % 255.95/36.99 % (1102814)Instruction limit reached! % 255.95/36.99 % (1102814)------------------------------ % 255.95/36.99 % (1102814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.95/36.99 % (1102814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.95/36.99 % (1102814)CaDiCaL version: 2.1.3 % 255.95/36.99 % (1102814)Termination reason: Instruction limit % 255.95/36.99 % (1102814)Termination phase: Saturation % 255.95/36.99 % (1102814)Time elapsed: 2.287 s % 255.95/36.99 % (1102814)Peak memory usage: 155 MB % 255.95/36.99 % (1102814)Instructions burned: 3981 (million) % 255.95/36.99 % (1102822)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2526839727:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2791 on theBenchmark for (2791ds/6508Mi) % 255.95/36.99 % (1102820)Instruction limit reached! % 255.95/36.99 % (1102820)------------------------------ % 255.95/36.99 % (1102820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.95/36.99 % (1102820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.95/36.99 % (1102820)CaDiCaL version: 2.1.3 % 255.95/36.99 % (1102820)Termination reason: Instruction limit % 255.95/36.99 % (1102820)Termination phase: Saturation % 255.95/36.99 % (1102820)Time elapsed: 0.731 s % 255.95/36.99 % (1102820)Peak memory usage: 140 MB % 255.95/36.99 % (1102820)Instructions burned: 2202 (million) % 255.95/36.99 % (1102824)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=4115983673:i=2330:fgj=on:av=off:fsr=off_2784 on theBenchmark for (2784ds/2330Mi) % 255.95/36.99 % (1102824)Instruction limit reached! % 255.95/36.99 % (1102824)------------------------------ % 255.95/36.99 % (1102824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.95/36.99 % (1102824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.95/36.99 % (1102824)CaDiCaL version: 2.1.3 % 255.95/36.99 % (1102824)Termination reason: Instruction limit % 255.95/36.99 % (1102824)Termination phase: Saturation % 255.95/36.99 % (1102824)Time elapsed: 0.770 s % 255.95/36.99 % (1102824)Peak memory usage: 140 MB % 255.95/36.99 % (1102824)Instructions burned: 2331 (million) % 255.95/36.99 % (1102826)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1577024061:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2775 on theBenchmark for (2775ds/7592Mi) % 255.95/36.99 % (1102818)Instruction limit reached! % 255.95/36.99 % (1102818)------------------------------ % 255.95/36.99 % (1102818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.95/36.99 % (1102818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.95/36.99 % (1102818)CaDiCaL version: 2.1.3 % 255.95/36.99 % (1102818)Termination reason: Instruction limit % 255.95/36.99 % (1102818)Termination phase: Saturation % 255.95/36.99 % (1102818)Time elapsed: 2.746 s % 255.95/36.99 % (1102818)Peak memory usage: 149 MB % 255.95/36.99 % (1102818)Instructions burned: 4273 (million) % 255.95/36.99 % (1102828)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=685395885:i=2693:kws=precedence:ins=1:av=off_2768 on theBenchmark for (2768ds/2693Mi) % 255.95/36.99 % (1102798)Instruction limit reached! % 255.95/36.99 % (1102798)------------------------------ % 255.95/36.99 % (1102798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.95/36.99 % (1102798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.95/36.99 % (1102798)CaDiCaL version: 2.1.3 % 255.95/36.99 % (1102798)Termination reason: Instruction limit % 255.95/36.99 % (1102798)Termination phase: Saturation % 255.95/36.99 % (1102798)Time elapsed: 8.707 s % 255.95/36.99 % (1102798)Peak memory usage: 237 MB % 255.95/36.99 % (1102798)Instructions burned: 13944 (million) % 255.95/36.99 % (1102830)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=634606721:i=28651:sd=4:ss=included:sgt=64_2760 on theBenchmark for (2760ds/28651Mi) % 255.95/36.99 % (1102826)Instruction limit reached! % 255.95/36.99 % (1102826)------------------------------ % 255.95/36.99 % (1102826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.29/42.31 % (1102826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.29/42.31 % (1102826)CaDiCaL version: 2.1.3 % 294.29/42.31 % (1102826)Termination reason: Instruction limit % 294.29/42.31 % (1102826)Termination phase: Saturation % 294.29/42.31 % (1102826)Time elapsed: 2.146 s % 294.29/42.31 % (1102826)Peak memory usage: 125 MB % 294.29/42.31 % (1102826)Instructions burned: 7595 (million) % 294.29/42.31 % (1102822)Instruction limit reached! % 294.29/42.31 % (1102822)------------------------------ % 294.29/42.31 % (1102822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.29/42.31 % (1102822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.29/42.31 % (1102822)CaDiCaL version: 2.1.3 % 294.29/42.31 % (1102822)Termination reason: Instruction limit % 294.29/42.31 % (1102822)Termination phase: Saturation % 294.29/42.31 % (1102822)Time elapsed: 3.724 s % 294.29/42.31 % (1102822)Peak memory usage: 130 MB % 294.29/42.31 % (1102822)Instructions burned: 6508 (million) % 294.29/42.31 % (1102832)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=3363728954:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2753 on theBenchmark for (2753ds/2700Mi) % 294.29/42.31 % (1102833)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=3505737259:i=3196:nm=4_2752 on theBenchmark for (2752ds/3196Mi) % 294.29/42.31 % (1102828)Instruction limit reached! % 294.29/42.31 % (1102828)------------------------------ % 294.29/42.31 % (1102828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.29/42.31 % (1102828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.29/42.31 % (1102828)CaDiCaL version: 2.1.3 % 294.29/42.31 % (1102828)Termination reason: Instruction limit % 294.29/42.31 % (1102828)Termination phase: Saturation % 294.29/42.31 % (1102828)Time elapsed: 1.721 s % 294.29/42.31 % (1102828)Peak memory usage: 146 MB % 294.29/42.31 % (1102828)Instructions burned: 2694 (million) % 294.29/42.31 % (1102836)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=3742913934:cts=off:i=3254:av=off_2749 on theBenchmark for (2749ds/3254Mi) % 294.29/42.31 % (1102832)Instruction limit reached! % 294.29/42.31 % (1102832)------------------------------ % 294.29/42.31 % (1102832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.29/42.31 % (1102832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.29/42.31 % (1102832)CaDiCaL version: 2.1.3 % 294.29/42.31 % (1102832)Termination reason: Instruction limit % 294.29/42.31 % (1102832)Termination phase: Saturation % 294.29/42.31 % (1102832)Time elapsed: 0.922 s % 294.29/42.31 % (1102832)Peak memory usage: 141 MB % 294.29/42.31 % (1102832)Instructions burned: 2702 (million) % 294.29/42.31 % (1102838)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=40416402:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2743 on theBenchmark for (2743ds/3264Mi) % 294.29/42.31 % (1102833)Instruction limit reached! % 294.29/42.31 % (1102833)------------------------------ % 294.29/42.31 % (1102833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.29/42.31 % (1102833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.29/42.31 % (1102833)CaDiCaL version: 2.1.3 % 294.29/42.31 % (1102833)Termination reason: Instruction limit % 294.29/42.31 % (1102833)Termination phase: Saturation % 294.29/42.31 % (1102833)Time elapsed: 1.983 s % 294.29/42.31 % (1102833)Peak memory usage: 147 MB % 294.29/42.31 % (1102833)Instructions burned: 3196 (million) % 294.29/42.31 % (1102838)Instruction limit reached! % 294.29/42.31 % (1102838)------------------------------ % 294.29/42.31 % (1102838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.29/42.31 % (1102838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.29/42.31 % (1102838)CaDiCaL version: 2.1.3 % 294.29/42.31 % (1102838)Termination reason: Instruction limit % 294.29/42.31 % (1102838)Termination phase: Saturation % 294.29/42.31 % (1102838)Time elapsed: 1.202 s % 294.29/42.31 % (1102838)Peak memory usage: 145 MB % 294.29/42.31 % (1102838)Instructions burned: 3266 (million) % 294.29/42.31 % (1102840)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=2703705014:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2731 on theBenchmark for (2731ds/9708Mi) % 300.24/43.17 % (1102841)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=656994483:i=21997:s2at=5:gtg=all_2730 on theBenchmark for (2730ds/21997Mi) % 300.24/43.17 % (1102836)Instruction limit reached! % 300.24/43.17 % (1102836)------------------------------ % 300.24/43.17 % (1102836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.17 % (1102836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.17 % (1102836)CaDiCaL version: 2.1.3 % 300.24/43.17 % (1102836)Termination reason: Instruction limit % 300.24/43.17 % (1102836)Termination phase: Saturation % 300.24/43.17 % (1102836)Time elapsed: 2.002 s % 300.24/43.17 % (1102836)Peak memory usage: 147 MB % 300.24/43.17 % (1102836)Instructions burned: 3254 (million) % 300.24/43.17 % (1102844)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=285563201:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2728 on theBenchmark for (2728ds/7551Mi) % 300.24/43.17 % (1102844)Instruction limit reached! % 300.24/43.17 % (1102844)------------------------------ % 300.24/43.17 % (1102844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.17 % (1102844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.17 % (1102844)CaDiCaL version: 2.1.3 % 300.24/43.17 % (1102844)Termination reason: Instruction limit % 300.24/43.17 % (1102844)Termination phase: Saturation % 300.24/43.17 % (1102844)Time elapsed: 4.382 s % 300.24/43.17 % (1102844)Peak memory usage: 136 MB % 300.24/43.17 % (1102844)Instructions burned: 7551 (million) % 300.24/43.17 % (1102846)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=924103185:i=8924:sd=1:ss=included_2683 on theBenchmark for (2683ds/8924Mi) % 300.24/43.17 % (1102840)Instruction limit reached! % 300.24/43.17 % (1102840)------------------------------ % 300.24/43.17 % (1102840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.17 % (1102840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.17 % (1102840)CaDiCaL version: 2.1.3 % 300.24/43.17 % (1102840)Termination reason: Instruction limit % 300.24/43.17 % (1102840)Termination phase: Saturation % 300.24/43.17 % (1102840)Time elapsed: 6.132 s % 300.24/43.17 % (1102840)Peak memory usage: 197 MB % 300.24/43.17 % (1102840)Instructions burned: 9708 (million) % 300.24/43.17 % (1102841)Instruction limit reached! % 300.24/43.17 % (1102841)------------------------------ % 300.24/43.17 % (1102841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.17 % (1102841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.17 % (1102841)CaDiCaL version: 2.1.3 % 300.24/43.17 % (1102841)Termination reason: Instruction limit % 300.24/43.17 % (1102841)Termination phase: Saturation % 300.24/43.17 % (1102841)Time elapsed: 6.182 s % 300.24/43.17 % (1102841)Peak memory usage: 182 MB % 300.24/43.17 % (1102841)Instructions burned: 22000 (million) % 300.24/43.17 % (1102850)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=1529125020:i=9638:kws=frequency:bd=preordered_2668 on theBenchmark for (2668ds/9638Mi) % 300.24/43.17 % (1102852)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:prc=on:drc=off:sp=const_min:sos=on:lcm=predicate:s2agt=20:br=off:flr=on:random_seed=419262768:i=5177:s2at=1.5:bd=preordered:ins=10:fdi=128_2667 on theBenchmark for (2667ds/5177Mi) % 300.24/43.17 % (1102852)Refutation not found, incomplete strategy % 300.24/43.17 % (1102852)------------------------------ % 300.24/43.17 % (1102852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.24/43.17 % (1102852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.24/43.17 % (1102852)CaDiCaL version: 2.1.3 % 300.24/43.17 % (1102852)Termination reason: Refutation not found, incomplete strategy % 300.24/43.17 % (1102852)Time elapsed: 0.337 s % 300.24/43.17 % (1102852)Peak memory usage: 128 MB % 300.24/43.17 % (1102852)Instructions burned: 897 (million) % 300.24/43.17 % (1102852)------------------------------ % 300.24/43.17 % (1102852)------------------------------ % 300.24/43.17 % (1102854)lrs-1011_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:sas=cadical:sp=unary_first:acc=on:alpa=false:random_seed=2918173180:i=6464:aac=none:ins=10_2661 on theBenchmark for (2661ds/6464Mi) % 300.24/43.17 % (1102854)Instruction limit reached! % 300.24/43.17 % (1102854)------------------------------ % 300.24/43.17 % (1102854)Version: Vampire 5.0.1 (Release build, commit ea89 % 300.24/43.18 Terminated %------------------------------------------------------------------------------