%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM257-2 : 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 : n012.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:12:00 PM UTC 2026 % Result : Timeout 300.43s 43.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : NUM257-2 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.04/0.30 % Computer : n012.cluster.edu % 0.04/0.30 % Model : x86_64 x86_64 % 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.04/0.30 % Memory : 8046.5625MB % 0.04/0.30 % OS : Linux 6.8.0-71-generic % 0.04/0.31 % CPULimit : 300 % 0.04/0.31 % WCLimit : 300 % 0.04/0.31 % DateTime : Sun Sep 27 19:21:34 UTC 2026 % 0.04/0.31 % CPUTime : % 0.04/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.33 Running first-order theorem proving % 0.07/0.33 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 % 6.96/1.69 % (2682777)Input is clausal, will run a generic CNF schedule. % 6.96/1.69 % (2682786)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4182006297:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 6.96/1.69 % (2682785)lrs+10_1_sil=8000:sp=occurrence:random_seed=2558530717:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 6.96/1.69 % (2682783)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=759832974:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 6.96/1.69 % (2682787)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3490907353:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 6.96/1.69 % (2682788)dis-21_1_sil=8000:lcm=predicate:random_seed=1610452350: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) % 6.96/1.69 % (2682784)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=544772874:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 6.96/1.69 % (2682782)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=457478989:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 6.96/1.69 % (2682788)Instruction limit reached! % 6.96/1.69 % (2682788)------------------------------ % 6.96/1.69 % (2682788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.96/1.69 % (2682788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.69 % (2682788)CaDiCaL version: 2.1.3 % 6.96/1.69 % (2682788)Termination reason: Instruction limit % 6.96/1.69 % (2682788)Termination phase: Saturation % 6.96/1.69 % (2682788)Time elapsed: 0.030 s % 6.96/1.69 % (2682788)Peak memory usage: 89 MB % 6.96/1.69 % (2682788)Instructions burned: 119 (million) % 6.96/1.69 % (2682785)Instruction limit reached! % 6.96/1.69 % (2682785)------------------------------ % 6.96/1.69 % (2682785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.96/1.69 % (2682785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.69 % (2682785)CaDiCaL version: 2.1.3 % 6.96/1.69 % (2682785)Termination reason: Instruction limit % 6.96/1.69 % (2682785)Termination phase: Saturation % 6.96/1.69 % (2682785)Time elapsed: 0.037 s % 6.96/1.69 % (2682785)Peak memory usage: 89 MB % 6.96/1.69 % (2682785)Instructions burned: 108 (million) % 6.96/1.69 % (2682786)Instruction limit reached! % 6.96/1.69 % (2682786)------------------------------ % 6.96/1.69 % (2682786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.96/1.69 % (2682786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.69 % (2682786)CaDiCaL version: 2.1.3 % 6.96/1.69 % (2682786)Termination reason: Instruction limit % 6.96/1.69 % (2682786)Termination phase: Saturation % 6.96/1.69 % (2682786)Time elapsed: 0.040 s % 6.96/1.69 % (2682786)Peak memory usage: 89 MB % 6.96/1.69 % (2682786)Instructions burned: 115 (million) % 6.96/1.69 % (2682787)Instruction limit reached! % 6.96/1.69 % (2682787)------------------------------ % 6.96/1.69 % (2682787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.96/1.69 % (2682787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.96/1.69 % (2682787)CaDiCaL version: 2.1.3 % 6.96/1.69 % (2682787)Termination reason: Instruction limit % 6.96/1.69 % (2682787)Termination phase: Saturation % 6.96/1.69 % (2682787)Time elapsed: 0.074 s % 6.96/1.69 % (2682787)Peak memory usage: 90 MB % 6.96/1.69 % (2682787)Instructions burned: 181 (million) % 6.96/1.69 % (2682796)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=2208572668:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 6.96/1.69 % (2682797)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2364559366: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) % 6.96/1.69 % (2682798)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1823391836:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi) % 6.96/1.69 % (2682796)Instruction limit reached! % 6.96/1.69 % (2682796)------------------------------ % 6.96/1.69 % (2682796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.75/2.40 % (2682796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.75/2.40 % (2682796)CaDiCaL version: 2.1.3 % 12.75/2.40 % (2682796)Termination reason: Instruction limit % 12.75/2.40 % (2682796)Termination phase: Saturation % 12.75/2.40 % (2682796)Time elapsed: 0.056 s % 12.75/2.40 % (2682796)Peak memory usage: 89 MB % 12.75/2.40 % (2682796)Instructions burned: 144 (million) % 12.75/2.40 % (2682799)lrs+10_64_to=lpo:sil=8000:random_seed=2051079338:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 12.75/2.40 % (2682797)Instruction limit reached! % 12.75/2.40 % (2682797)------------------------------ % 12.75/2.40 % (2682797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.75/2.40 % (2682797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.75/2.40 % (2682797)CaDiCaL version: 2.1.3 % 12.75/2.40 % (2682797)Termination reason: Instruction limit % 12.75/2.40 % (2682797)Termination phase: Saturation % 12.75/2.40 % (2682797)Time elapsed: 0.058 s % 12.75/2.40 % (2682797)Peak memory usage: 90 MB % 12.75/2.40 % (2682797)Instructions burned: 191 (million) % 12.75/2.40 % (2682798)Instruction limit reached! % 12.75/2.40 % (2682798)------------------------------ % 12.75/2.40 % (2682798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.75/2.40 % (2682798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.75/2.40 % (2682798)CaDiCaL version: 2.1.3 % 12.75/2.40 % (2682798)Termination reason: Instruction limit % 12.75/2.40 % (2682798)Termination phase: Saturation % 12.75/2.40 % (2682798)Time elapsed: 0.072 s % 12.75/2.40 % (2682798)Peak memory usage: 89 MB % 12.75/2.40 % (2682798)Instructions burned: 219 (million) % 12.75/2.40 % (2682799)Instruction limit reached! % 12.75/2.40 % (2682799)------------------------------ % 12.75/2.40 % (2682799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.75/2.40 % (2682799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.75/2.40 % (2682799)CaDiCaL version: 2.1.3 % 12.75/2.40 % (2682799)Termination reason: Instruction limit % 12.75/2.40 % (2682799)Termination phase: Saturation % 12.75/2.40 % (2682799)Time elapsed: 0.044 s % 12.75/2.40 % (2682799)Peak memory usage: 89 MB % 12.75/2.40 % (2682799)Instructions burned: 129 (million) % 12.75/2.40 % (2682803)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=558990524:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi) % 12.75/2.40 % (2682805)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3947244736:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi) % 12.75/2.40 % (2682806)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3462491234:i=3394:sd=4:ss=included:sgt=64_2996 on theBenchmark for (2996ds/3394Mi) % 12.75/2.40 % (2682807)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=596498851:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2996 on theBenchmark for (2996ds/106Mi) % 12.75/2.40 % (2682803)Instruction limit reached! % 12.75/2.40 % (2682803)------------------------------ % 12.75/2.40 % (2682803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.75/2.40 % (2682803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.75/2.40 % (2682803)CaDiCaL version: 2.1.3 % 12.75/2.40 % (2682803)Termination reason: Instruction limit % 12.75/2.40 % (2682803)Termination phase: Saturation % 12.75/2.40 % (2682803)Time elapsed: 0.062 s % 12.75/2.40 % (2682803)Peak memory usage: 90 MB % 12.75/2.40 % (2682803)Instructions burned: 194 (million) % 12.75/2.40 % (2682805)Instruction limit reached! % 12.75/2.40 % (2682805)------------------------------ % 12.75/2.40 % (2682805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.75/2.40 % (2682805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.75/2.40 % (2682805)CaDiCaL version: 2.1.3 % 12.75/2.40 % (2682805)Termination reason: Instruction limit % 12.75/2.40 % (2682805)Termination phase: Saturation % 12.75/2.40 % (2682805)Time elapsed: 0.054 s % 12.75/2.40 % (2682805)Peak memory usage: 91 MB % 12.75/2.40 % (2682805)Instructions burned: 159 (million) % 12.75/2.40 % (2682807)Instruction limit reached! % 12.75/2.40 % (2682807)------------------------------ % 12.75/2.40 % (2682807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.75/2.40 % (2682807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.75/2.40 % (2682807)CaDiCaL version: 2.1.3 % 25.85/4.20 % (2682807)Termination reason: Instruction limit % 25.85/4.20 % (2682807)Termination phase: Saturation % 25.85/4.20 % (2682807)Time elapsed: 0.029 s % 25.85/4.20 % (2682807)Peak memory usage: 95 MB % 25.85/4.20 % (2682807)Instructions burned: 109 (million) % 25.85/4.20 % (2682813)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3007613161:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi) % 25.85/4.20 % (2682812)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2256319922:i=107_2994 on theBenchmark for (2994ds/107Mi) % 25.85/4.20 % (2682814)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=950377669:cond=fast:i=5208:av=off_2994 on theBenchmark for (2994ds/5208Mi) % 25.85/4.20 % (2682812)Instruction limit reached! % 25.85/4.20 % (2682812)------------------------------ % 25.85/4.20 % (2682812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.85/4.20 % (2682812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.85/4.20 % (2682812)CaDiCaL version: 2.1.3 % 25.85/4.20 % (2682812)Termination reason: Instruction limit % 25.85/4.20 % (2682812)Termination phase: Saturation % 25.85/4.20 % (2682812)Time elapsed: 0.040 s % 25.85/4.20 % (2682812)Peak memory usage: 89 MB % 25.85/4.20 % (2682812)Instructions burned: 109 (million) % 25.85/4.20 % (2682813)Instruction limit reached! % 25.85/4.20 % (2682813)------------------------------ % 25.85/4.20 % (2682813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.85/4.20 % (2682813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.85/4.20 % (2682813)CaDiCaL version: 2.1.3 % 25.85/4.20 % (2682813)Termination reason: Instruction limit % 25.85/4.20 % (2682813)Termination phase: Saturation % 25.85/4.20 % (2682813)Time elapsed: 0.091 s % 25.85/4.20 % (2682813)Peak memory usage: 90 MB % 25.85/4.20 % (2682813)Instructions burned: 243 (million) % 25.85/4.20 % (2682818)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4215442411:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi) % 25.85/4.20 % (2682818)Instruction limit reached! % 25.85/4.20 % (2682818)------------------------------ % 25.85/4.20 % (2682818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.85/4.20 % (2682818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.85/4.20 % (2682818)CaDiCaL version: 2.1.3 % 25.85/4.20 % (2682818)Termination reason: Instruction limit % 25.85/4.20 % (2682818)Termination phase: Saturation % 25.85/4.20 % (2682818)Time elapsed: 0.050 s % 25.85/4.20 % (2682818)Peak memory usage: 90 MB % 25.85/4.20 % (2682818)Instructions burned: 134 (million) % 25.85/4.20 % (2682819)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=153866092:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi) % 25.85/4.20 % (2682822)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=209176215:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi) % 25.85/4.20 % (2682819)Instruction limit reached! % 25.85/4.20 % (2682819)------------------------------ % 25.85/4.20 % (2682819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.85/4.20 % (2682819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.85/4.20 % (2682819)CaDiCaL version: 2.1.3 % 25.85/4.20 % (2682819)Termination reason: Instruction limit % 25.85/4.20 % (2682819)Termination phase: Saturation % 25.85/4.20 % (2682819)Time elapsed: 0.157 s % 25.85/4.20 % (2682819)Peak memory usage: 94 MB % 25.85/4.20 % (2682819)Instructions burned: 502 (million) % 25.85/4.20 % (2682822)Instruction limit reached! % 25.85/4.20 % (2682822)------------------------------ % 25.85/4.20 % (2682822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.85/4.20 % (2682822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.85/4.20 % (2682822)CaDiCaL version: 2.1.3 % 25.85/4.20 % (2682822)Termination reason: Instruction limit % 25.85/4.20 % (2682822)Termination phase: Saturation % 25.85/4.20 % (2682822)Time elapsed: 0.063 s % 25.85/4.20 % (2682822)Peak memory usage: 90 MB % 25.85/4.20 % (2682822)Instructions burned: 191 (million) % 25.85/4.20 % (2682824)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3379147037:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi) % 25.85/4.20 % (2682825)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1153435280:cond=on:i=156:bs=on:gtg=exists_all:er=known_2989 on theBenchmark for (2989ds/156Mi) % 32.62/5.22 % (2682824)Instruction limit reached! % 32.62/5.22 % (2682824)------------------------------ % 32.62/5.22 % (2682824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.22 % (2682824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.22 % (2682824)CaDiCaL version: 2.1.3 % 32.62/5.22 % (2682824)Termination reason: Instruction limit % 32.62/5.22 % (2682824)Termination phase: Saturation % 32.62/5.22 % (2682824)Time elapsed: 0.091 s % 32.62/5.22 % (2682824)Peak memory usage: 92 MB % 32.62/5.22 % (2682824)Instructions burned: 264 (million) % 32.62/5.22 % (2682825)Instruction limit reached! % 32.62/5.22 % (2682825)------------------------------ % 32.62/5.22 % (2682825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.22 % (2682825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.22 % (2682825)CaDiCaL version: 2.1.3 % 32.62/5.22 % (2682825)Termination reason: Instruction limit % 32.62/5.22 % (2682825)Termination phase: Saturation % 32.62/5.22 % (2682825)Time elapsed: 0.059 s % 32.62/5.22 % (2682825)Peak memory usage: 90 MB % 32.62/5.22 % (2682825)Instructions burned: 157 (million) % 32.62/5.22 % (2682828)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=1625512312:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi) % 32.62/5.22 % (2682829)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2762876030:i=537:av=off:ss=included_2987 on theBenchmark for (2987ds/537Mi) % 32.62/5.22 % (2682829)Instruction limit reached! % 32.62/5.22 % (2682829)------------------------------ % 32.62/5.22 % (2682829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.22 % (2682829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.22 % (2682829)CaDiCaL version: 2.1.3 % 32.62/5.22 % (2682829)Termination reason: Instruction limit % 32.62/5.22 % (2682829)Termination phase: Saturation % 32.62/5.22 % (2682829)Time elapsed: 0.117 s % 32.62/5.22 % (2682829)Peak memory usage: 88 MB % 32.62/5.22 % (2682829)Instructions burned: 538 (million) % 32.62/5.22 % (2682832)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2690763604:i=180:bd=preordered:av=off_2985 on theBenchmark for (2985ds/180Mi) % 32.62/5.22 % (2682806)Instruction limit reached! % 32.62/5.22 % (2682806)------------------------------ % 32.62/5.22 % (2682806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.22 % (2682806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.22 % (2682806)CaDiCaL version: 2.1.3 % 32.62/5.22 % (2682806)Termination reason: Instruction limit % 32.62/5.22 % (2682806)Termination phase: Saturation % 32.62/5.22 % (2682806)Time elapsed: 1.143 s % 32.62/5.22 % (2682806)Peak memory usage: 148 MB % 32.62/5.22 % (2682806)Instructions burned: 3394 (million) % 32.62/5.22 % (2682832)Instruction limit reached! % 32.62/5.22 % (2682832)------------------------------ % 32.62/5.22 % (2682832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.22 % (2682832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.22 % (2682832)CaDiCaL version: 2.1.3 % 32.62/5.22 % (2682832)Termination reason: Instruction limit % 32.62/5.22 % (2682832)Termination phase: Saturation % 32.62/5.22 % (2682832)Time elapsed: 0.052 s % 32.62/5.22 % (2682832)Peak memory usage: 90 MB % 32.62/5.22 % (2682832)Instructions burned: 184 (million) % 32.62/5.22 % (2682834)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=905658418:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2983 on theBenchmark for (2983ds/10307Mi) % 32.62/5.22 % (2682835)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=1262565916:i=412:gtgl=4:gtg=exists_all_2983 on theBenchmark for (2983ds/412Mi) % 32.62/5.22 % (2682835)Instruction limit reached! % 32.62/5.22 % (2682835)------------------------------ % 32.62/5.22 % (2682835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.62/5.22 % (2682835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.62/5.22 % (2682835)CaDiCaL version: 2.1.3 % 32.62/5.22 % (2682835)Termination reason: Instruction limit % 32.62/5.22 % (2682835)Termination phase: Saturation % 46.99/7.23 % (2682835)Time elapsed: 0.107 s % 46.99/7.23 % (2682835)Peak memory usage: 91 MB % 46.99/7.23 % (2682835)Instructions burned: 414 (million) % 46.99/7.23 % (2682840)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=2467104486:s2pl=no:i=8478:s2at=4:nm=6_2981 on theBenchmark for (2981ds/8478Mi) % 46.99/7.23 % (2682828)Instruction limit reached! % 46.99/7.23 % (2682828)------------------------------ % 46.99/7.23 % (2682828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.99/7.23 % (2682828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.99/7.23 % (2682828)CaDiCaL version: 2.1.3 % 46.99/7.23 % (2682828)Termination reason: Instruction limit % 46.99/7.23 % (2682828)Termination phase: Saturation % 46.99/7.23 % (2682828)Time elapsed: 0.971 s % 46.99/7.23 % (2682828)Peak memory usage: 150 MB % 46.99/7.23 % (2682828)Instructions burned: 3260 (million) % 46.99/7.23 % (2682814)Instruction limit reached! % 46.99/7.23 % (2682814)------------------------------ % 46.99/7.23 % (2682814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.99/7.23 % (2682814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.99/7.23 % (2682814)CaDiCaL version: 2.1.3 % 46.99/7.23 % (2682814)Termination reason: Instruction limit % 46.99/7.23 % (2682814)Termination phase: Saturation % 46.99/7.23 % (2682814)Time elapsed: 1.709 s % 46.99/7.23 % (2682814)Peak memory usage: 161 MB % 46.99/7.23 % (2682814)Instructions burned: 5208 (million) % 46.99/7.23 % (2682842)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=706371445:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2976 on theBenchmark for (2976ds/303Mi) % 46.99/7.23 % (2682843)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=243434727:st=4:i=720:sd=3:fsr=off:ss=axioms_2976 on theBenchmark for (2976ds/720Mi) % 46.99/7.23 % (2682842)Instruction limit reached! % 46.99/7.23 % (2682842)------------------------------ % 46.99/7.23 % (2682842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.99/7.23 % (2682842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.99/7.23 % (2682842)CaDiCaL version: 2.1.3 % 46.99/7.23 % (2682842)Termination reason: Instruction limit % 46.99/7.23 % (2682842)Termination phase: Saturation % 46.99/7.23 % (2682842)Time elapsed: 0.094 s % 46.99/7.23 % (2682842)Peak memory usage: 93 MB % 46.99/7.23 % (2682842)Instructions burned: 305 (million) % 46.99/7.23 % (2682846)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=944609962:i=598:bs=on:bd=preordered:av=off:ss=axioms_2974 on theBenchmark for (2974ds/598Mi) % 46.99/7.23 % (2682843)Instruction limit reached! % 46.99/7.23 % (2682843)------------------------------ % 46.99/7.23 % (2682843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.99/7.23 % (2682843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.99/7.23 % (2682843)CaDiCaL version: 2.1.3 % 46.99/7.23 % (2682843)Termination reason: Instruction limit % 46.99/7.23 % (2682843)Termination phase: Saturation % 46.99/7.23 % (2682843)Time elapsed: 0.216 s % 46.99/7.23 % (2682843)Peak memory usage: 98 MB % 46.99/7.23 % (2682843)Instructions burned: 723 (million) % 46.99/7.23 % (2682846)Instruction limit reached! % 46.99/7.23 % (2682846)------------------------------ % 46.99/7.23 % (2682846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.99/7.23 % (2682846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.99/7.23 % (2682846)CaDiCaL version: 2.1.3 % 46.99/7.23 % (2682846)Termination reason: Instruction limit % 46.99/7.23 % (2682846)Termination phase: Saturation % 46.99/7.23 % (2682846)Time elapsed: 0.185 s % 46.99/7.23 % (2682846)Peak memory usage: 94 MB % 46.99/7.23 % (2682846)Instructions burned: 598 (million) % 46.99/7.23 % (2682848)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3651718243:i=2989:sd=3:ss=axioms:sgt=60_2972 on theBenchmark for (2972ds/2989Mi) % 46.99/7.23 % (2682849)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=1694541285:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2971 on theBenchmark for (2971ds/1997Mi) % 46.99/7.23 % (2682849)Instruction limit reached! % 46.99/7.23 % (2682849)------------------------------ % 68.09/10.27 % (2682849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.09/10.27 % (2682849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.09/10.27 % (2682849)CaDiCaL version: 2.1.3 % 68.09/10.27 % (2682849)Termination reason: Instruction limit % 68.09/10.27 % (2682849)Termination phase: Saturation % 68.09/10.27 % (2682849)Time elapsed: 0.682 s % 68.09/10.27 % (2682849)Peak memory usage: 138 MB % 68.09/10.27 % (2682849)Instructions burned: 2000 (million) % 68.09/10.27 % (2682852)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=3262611971:i=2088:bd=preordered:av=off_2963 on theBenchmark for (2963ds/2088Mi) % 68.09/10.27 % (2682848)Instruction limit reached! % 68.09/10.27 % (2682848)------------------------------ % 68.09/10.27 % (2682848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.09/10.27 % (2682848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.09/10.27 % (2682848)CaDiCaL version: 2.1.3 % 68.09/10.27 % (2682848)Termination reason: Instruction limit % 68.09/10.27 % (2682848)Termination phase: Saturation % 68.09/10.27 % (2682848)Time elapsed: 0.984 s % 68.09/10.27 % (2682848)Peak memory usage: 144 MB % 68.09/10.27 % (2682848)Instructions burned: 2991 (million) % 68.09/10.27 % (2682854)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1115057587:i=1098:nicw=on_2961 on theBenchmark for (2961ds/1098Mi) % 68.09/10.27 % (2682854)Instruction limit reached! % 68.09/10.27 % (2682854)------------------------------ % 68.09/10.27 % (2682854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.09/10.27 % (2682854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.09/10.27 % (2682854)CaDiCaL version: 2.1.3 % 68.09/10.27 % (2682854)Termination reason: Instruction limit % 68.09/10.27 % (2682854)Termination phase: Saturation % 68.09/10.27 % (2682854)Time elapsed: 0.368 s % 68.09/10.27 % (2682854)Peak memory usage: 103 MB % 68.09/10.27 % (2682854)Instructions burned: 1098 (million) % 68.09/10.27 % (2682856)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=4276931618:i=433:bd=preordered_2956 on theBenchmark for (2956ds/433Mi) % 68.09/10.27 % (2682852)Instruction limit reached! % 68.09/10.27 % (2682852)------------------------------ % 68.09/10.27 % (2682852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.09/10.27 % (2682852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.09/10.27 % (2682852)CaDiCaL version: 2.1.3 % 68.09/10.27 % (2682852)Termination reason: Instruction limit % 68.09/10.27 % (2682852)Termination phase: Saturation % 68.09/10.27 % (2682852)Time elapsed: 0.704 s % 68.09/10.27 % (2682852)Peak memory usage: 139 MB % 68.09/10.27 % (2682852)Instructions burned: 2091 (million) % 68.09/10.27 % (2682840)Instruction limit reached! % 68.09/10.27 % (2682840)------------------------------ % 68.09/10.27 % (2682840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.09/10.27 % (2682840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.09/10.27 % (2682840)CaDiCaL version: 2.1.3 % 68.09/10.27 % (2682840)Termination reason: Instruction limit % 68.09/10.27 % (2682840)Termination phase: Saturation % 68.09/10.27 % (2682840)Time elapsed: 2.568 s % 68.09/10.27 % (2682840)Peak memory usage: 200 MB % 68.09/10.27 % (2682840)Instructions burned: 8482 (million) % 68.09/10.27 % (2682856)Instruction limit reached! % 68.09/10.27 % (2682856)------------------------------ % 68.09/10.27 % (2682856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.09/10.27 % (2682856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.09/10.27 % (2682856)CaDiCaL version: 2.1.3 % 68.09/10.27 % (2682856)Termination reason: Instruction limit % 68.09/10.27 % (2682856)Termination phase: Saturation % 68.09/10.27 % (2682856)Time elapsed: 0.126 s % 68.09/10.27 % (2682856)Peak memory usage: 91 MB % 68.09/10.27 % (2682856)Instructions burned: 436 (million) % 68.09/10.27 % (2682858)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2189952200:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2954 on theBenchmark for (2954ds/2942Mi) % 68.09/10.27 % (2682859)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1131953466:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2954 on theBenchmark for (2954ds/6922Mi) % 80.91/12.06 % (2682860)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=557515120:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2953 on theBenchmark for (2953ds/596Mi) % 80.91/12.06 % (2682860)Instruction limit reached! % 80.91/12.06 % (2682860)------------------------------ % 80.91/12.06 % (2682860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.91/12.06 % (2682860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.91/12.06 % (2682860)CaDiCaL version: 2.1.3 % 80.91/12.06 % (2682860)Termination reason: Instruction limit % 80.91/12.06 % (2682860)Termination phase: Saturation % 80.91/12.06 % (2682860)Time elapsed: 0.175 s % 80.91/12.06 % (2682860)Peak memory usage: 99 MB % 80.91/12.06 % (2682860)Instructions burned: 600 (million) % 80.91/12.06 % (2682864)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=2062357470:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2950 on theBenchmark for (2950ds/4123Mi) % 80.91/12.06 % (2682834)Instruction limit reached! % 80.91/12.06 % (2682834)------------------------------ % 80.91/12.06 % (2682834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.91/12.06 % (2682834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.91/12.06 % (2682834)CaDiCaL version: 2.1.3 % 80.91/12.06 % (2682834)Termination reason: Instruction limit % 80.91/12.06 % (2682834)Termination phase: Saturation % 80.91/12.06 % (2682834)Time elapsed: 3.510 s % 80.91/12.06 % (2682834)Peak memory usage: 170 MB % 80.91/12.06 % (2682834)Instructions burned: 10309 (million) % 80.91/12.06 % (2682866)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2791424329:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2947 on theBenchmark for (2947ds/16411Mi) % 80.91/12.06 % (2682858)Instruction limit reached! % 80.91/12.06 % (2682858)------------------------------ % 80.91/12.06 % (2682858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.91/12.06 % (2682858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.91/12.06 % (2682858)CaDiCaL version: 2.1.3 % 80.91/12.06 % (2682858)Termination reason: Instruction limit % 80.91/12.06 % (2682858)Termination phase: Saturation % 80.91/12.06 % (2682858)Time elapsed: 1.065 s % 80.91/12.06 % (2682858)Peak memory usage: 144 MB % 80.91/12.06 % (2682858)Instructions burned: 2942 (million) % 80.91/12.06 % (2682868)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3524418699:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2942 on theBenchmark for (2942ds/1670Mi) % 80.91/12.06 % (2682864)Instruction limit reached! % 80.91/12.06 % (2682864)------------------------------ % 80.91/12.06 % (2682864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.91/12.06 % (2682864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.91/12.06 % (2682864)CaDiCaL version: 2.1.3 % 80.91/12.06 % (2682864)Termination reason: Instruction limit % 80.91/12.06 % (2682864)Termination phase: Saturation % 80.91/12.06 % (2682864)Time elapsed: 1.191 s % 80.91/12.06 % (2682864)Peak memory usage: 156 MB % 80.91/12.06 % (2682864)Instructions burned: 4124 (million) % 80.91/12.06 % (2682870)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=3402922755:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2937 on theBenchmark for (2937ds/1722Mi) % 80.91/12.06 % (2682868)Instruction limit reached! % 80.91/12.06 % (2682868)------------------------------ % 80.91/12.06 % (2682868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.91/12.06 % (2682868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.91/12.06 % (2682868)CaDiCaL version: 2.1.3 % 80.91/12.06 % (2682868)Termination reason: Instruction limit % 80.91/12.06 % (2682868)Termination phase: Saturation % 80.91/12.06 % (2682868)Time elapsed: 0.579 s % 80.91/12.06 % (2682868)Peak memory usage: 137 MB % 80.91/12.06 % (2682868)Instructions burned: 1670 (million) % 80.91/12.06 % (2682872)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=659977313:cts=off:cond=on:i=9530:bs=on:fsd=on_2935 on theBenchmark for (2935ds/9530Mi) % 80.91/12.06 % (2682859)Instruction limit reached! % 80.91/12.06 % (2682859)------------------------------ % 90.45/13.45 % (2682859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.45/13.45 % (2682859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.45/13.45 % (2682859)CaDiCaL version: 2.1.3 % 90.45/13.45 % (2682859)Termination reason: Instruction limit % 90.45/13.45 % (2682859)Termination phase: Saturation % 90.45/13.45 % (2682859)Time elapsed: 2.007 s % 90.45/13.45 % (2682859)Peak memory usage: 186 MB % 90.45/13.45 % (2682859)Instructions burned: 6926 (million) % 90.45/13.45 % (2682874)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=272867811:st=2:i=4495:sd=10:ss=included_2932 on theBenchmark for (2932ds/4495Mi) % 90.45/13.45 % (2682870)Instruction limit reached! % 90.45/13.45 % (2682870)------------------------------ % 90.45/13.45 % (2682870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.45/13.45 % (2682870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.45/13.45 % (2682870)CaDiCaL version: 2.1.3 % 90.45/13.45 % (2682870)Termination reason: Instruction limit % 90.45/13.45 % (2682870)Termination phase: Saturation % 90.45/13.45 % (2682870)Time elapsed: 0.629 s % 90.45/13.45 % (2682870)Peak memory usage: 134 MB % 90.45/13.45 % (2682870)Instructions burned: 1722 (million) % 90.45/13.45 % (2682876)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=526594210:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2929 on theBenchmark for (2929ds/4920Mi) % 90.45/13.45 % (2682874)Instruction limit reached! % 90.45/13.45 % (2682874)------------------------------ % 90.45/13.45 % (2682874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.45/13.45 % (2682874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.45/13.45 % (2682874)CaDiCaL version: 2.1.3 % 90.45/13.45 % (2682874)Termination reason: Instruction limit % 90.45/13.45 % (2682874)Termination phase: Saturation % 90.45/13.45 % (2682874)Time elapsed: 1.512 s % 90.45/13.45 % (2682874)Peak memory usage: 156 MB % 90.45/13.45 % (2682874)Instructions burned: 4497 (million) % 90.45/13.45 % (2682878)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=1052064229:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2916 on theBenchmark for (2916ds/2083Mi) % 90.45/13.45 % (2682876)Instruction limit reached! % 90.45/13.45 % (2682876)------------------------------ % 90.45/13.45 % (2682876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.45/13.45 % (2682876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.45/13.45 % (2682876)CaDiCaL version: 2.1.3 % 90.45/13.45 % (2682876)Termination reason: Instruction limit % 90.45/13.45 % (2682876)Termination phase: Saturation % 90.45/13.45 % (2682876)Time elapsed: 1.627 s % 90.45/13.45 % (2682876)Peak memory usage: 162 MB % 90.45/13.45 % (2682876)Instructions burned: 4923 (million) % 90.45/13.45 % (2682880)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=1814958596:i=4629:av=off:gsp=on_2912 on theBenchmark for (2912ds/4629Mi) % 90.45/13.45 % (2682878)Instruction limit reached! % 90.45/13.45 % (2682878)------------------------------ % 90.45/13.45 % (2682878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.45/13.45 % (2682878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.45/13.45 % (2682878)CaDiCaL version: 2.1.3 % 90.45/13.45 % (2682878)Termination reason: Instruction limit % 90.45/13.45 % (2682878)Termination phase: Saturation % 90.45/13.45 % (2682878)Time elapsed: 0.724 s % 90.45/13.45 % (2682878)Peak memory usage: 138 MB % 90.45/13.45 % (2682878)Instructions burned: 2083 (million) % 90.45/13.45 % (2682882)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3908194058:i=1258:av=off_2907 on theBenchmark for (2907ds/1258Mi) % 90.45/13.45 % (2682882)Instruction limit reached! % 90.45/13.45 % (2682882)------------------------------ % 90.45/13.45 % (2682882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.45/13.45 % (2682882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.45/13.45 % (2682882)CaDiCaL version: 2.1.3 % 90.45/13.45 % (2682882)Termination reason: Instruction limit % 90.45/13.45 % (2682882)Termination phase: Saturation % 90.45/13.45 % (2682882)Time elapsed: 0.384 s % 90.45/13.45 % (2682882)Peak memory usage: 98 MB % 90.45/13.45 % (2682882)Instructions burned: 1259 (million) % 109.01/16.07 % (2682884)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1377728189:i=7343:av=off:ss=included_2902 on theBenchmark for (2902ds/7343Mi) % 109.01/16.07 % (2682872)Instruction limit reached! % 109.01/16.07 % (2682872)------------------------------ % 109.01/16.07 % (2682872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.01/16.07 % (2682872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.01/16.07 % (2682872)CaDiCaL version: 2.1.3 % 109.01/16.07 % (2682872)Termination reason: Instruction limit % 109.01/16.07 % (2682872)Termination phase: Saturation % 109.01/16.07 % (2682872)Time elapsed: 3.311 s % 109.01/16.07 % (2682872)Peak memory usage: 165 MB % 109.01/16.07 % (2682872)Instructions burned: 9532 (million) % 109.01/16.07 % (2682886)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=275301658:i=1325:sd=2:ss=axioms:sgt=16_2901 on theBenchmark for (2901ds/1325Mi) % 109.01/16.07 % (2682880)Instruction limit reached! % 109.01/16.07 % (2682880)------------------------------ % 109.01/16.07 % (2682880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.01/16.07 % (2682880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.01/16.07 % (2682880)CaDiCaL version: 2.1.3 % 109.01/16.07 % (2682880)Termination reason: Instruction limit % 109.01/16.07 % (2682880)Termination phase: Saturation % 109.01/16.07 % (2682880)Time elapsed: 1.469 s % 109.01/16.07 % (2682880)Peak memory usage: 157 MB % 109.01/16.07 % (2682880)Instructions burned: 4631 (million) % 109.01/16.07 % (2682886)Instruction limit reached! % 109.01/16.07 % (2682886)------------------------------ % 109.01/16.07 % (2682886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.01/16.07 % (2682886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.01/16.07 % (2682886)CaDiCaL version: 2.1.3 % 109.01/16.07 % (2682886)Termination reason: Instruction limit % 109.01/16.07 % (2682886)Termination phase: Saturation % 109.01/16.07 % (2682886)Time elapsed: 0.371 s % 109.01/16.07 % (2682886)Peak memory usage: 98 MB % 109.01/16.07 % (2682886)Instructions burned: 1326 (million) % 109.01/16.07 % (2682888)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=2206479269:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2896 on theBenchmark for (2896ds/2646Mi) % 109.01/16.07 % (2682889)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=947105304:i=1489:sd=2:ep=R:ss=axioms_2895 on theBenchmark for (2895ds/1489Mi) % 109.01/16.07 % (2682866)Instruction limit reached! % 109.01/16.07 % (2682866)------------------------------ % 109.01/16.07 % (2682866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.01/16.07 % (2682866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.01/16.07 % (2682866)CaDiCaL version: 2.1.3 % 109.01/16.07 % (2682866)Termination reason: Instruction limit % 109.01/16.07 % (2682866)Termination phase: Saturation % 109.01/16.07 % (2682866)Time elapsed: 5.554 s % 109.01/16.07 % (2682866)Peak memory usage: 234 MB % 109.01/16.07 % (2682866)Instructions burned: 16413 (million) % 109.01/16.07 % (2682889)Instruction limit reached! % 109.01/16.07 % (2682889)------------------------------ % 109.01/16.07 % (2682889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.01/16.07 % (2682889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.01/16.07 % (2682889)CaDiCaL version: 2.1.3 % 109.01/16.07 % (2682889)Termination reason: Instruction limit % 109.01/16.07 % (2682889)Termination phase: Saturation % 109.01/16.07 % (2682889)Time elapsed: 0.500 s % 109.01/16.07 % (2682889)Peak memory usage: 134 MB % 109.01/16.07 % (2682889)Instructions burned: 1490 (million) % 109.01/16.07 % (2682892)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=1847145180:i=1503_2890 on theBenchmark for (2890ds/1503Mi) % 109.01/16.07 % (2682893)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2989278446:i=13942:kws=frequency_2889 on theBenchmark for (2889ds/13942Mi) % 109.01/16.07 % (2682888)Instruction limit reached! % 109.01/16.07 % (2682888)------------------------------ % 109.01/16.07 % (2682888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.01/16.07 % (2682888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.01/16.07 % (2682888)CaDiCaL version: 2.1.3 % 124.39/18.25 % (2682888)Termination reason: Instruction limit % 124.39/18.25 % (2682888)Termination phase: Saturation % 124.39/18.25 % (2682888)Time elapsed: 1.025 s % 124.39/18.25 % (2682888)Peak memory usage: 141 MB % 124.39/18.25 % (2682888)Instructions burned: 2647 (million) % 124.39/18.25 % (2682892)Instruction limit reached! % 124.39/18.25 % (2682892)------------------------------ % 124.39/18.25 % (2682892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.39/18.25 % (2682892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.39/18.25 % (2682892)CaDiCaL version: 2.1.3 % 124.39/18.25 % (2682892)Termination reason: Instruction limit % 124.39/18.25 % (2682892)Termination phase: Saturation % 124.39/18.25 % (2682892)Time elapsed: 0.519 s % 124.39/18.25 % (2682892)Peak memory usage: 134 MB % 124.39/18.25 % (2682892)Instructions burned: 1505 (million) % 124.39/18.25 % (2682896)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=2748932565:i=3604:fsr=off:er=filter_2884 on theBenchmark for (2884ds/3604Mi) % 124.39/18.25 % (2682897)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=4013994456:i=1876:sd=1:ss=included:sgt=32_2883 on theBenchmark for (2883ds/1876Mi) % 124.39/18.25 % (2682884)Instruction limit reached! % 124.39/18.25 % (2682884)------------------------------ % 124.39/18.25 % (2682884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.39/18.25 % (2682884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.39/18.25 % (2682884)CaDiCaL version: 2.1.3 % 124.39/18.25 % (2682884)Termination reason: Instruction limit % 124.39/18.25 % (2682884)Termination phase: Saturation % 124.39/18.25 % (2682884)Time elapsed: 2.140 s % 124.39/18.25 % (2682884)Peak memory usage: 187 MB % 124.39/18.25 % (2682884)Instructions burned: 7344 (million) % 124.39/18.25 % (2682900)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1104956256:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2879 on theBenchmark for (2879ds/1932Mi) % 124.39/18.25 % (2682897)Instruction limit reached! % 124.39/18.25 % (2682897)------------------------------ % 124.39/18.25 % (2682897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.39/18.25 % (2682897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.39/18.25 % (2682897)CaDiCaL version: 2.1.3 % 124.39/18.25 % (2682897)Termination reason: Instruction limit % 124.39/18.25 % (2682897)Termination phase: Saturation % 124.39/18.25 % (2682897)Time elapsed: 0.648 s % 124.39/18.25 % (2682897)Peak memory usage: 135 MB % 124.39/18.25 % (2682897)Instructions burned: 1879 (million) % 124.39/18.25 % (2682902)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=3076306233:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2876 on theBenchmark for (2876ds/1980Mi) % 124.39/18.25 % (2682900)Instruction limit reached! % 124.39/18.25 % (2682900)------------------------------ % 124.39/18.25 % (2682900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.39/18.25 % (2682900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.39/18.25 % (2682900)CaDiCaL version: 2.1.3 % 124.39/18.25 % (2682900)Termination reason: Instruction limit % 124.39/18.25 % (2682900)Termination phase: Saturation % 124.39/18.25 % (2682900)Time elapsed: 0.597 s % 124.39/18.25 % (2682900)Peak memory usage: 137 MB % 124.39/18.25 % (2682900)Instructions burned: 1935 (million) % 124.39/18.25 % (2682896)Instruction limit reached! % 124.39/18.25 % (2682896)------------------------------ % 124.39/18.25 % (2682896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.39/18.25 % (2682896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.39/18.25 % (2682896)CaDiCaL version: 2.1.3 % 124.39/18.25 % (2682896)Termination reason: Instruction limit % 124.39/18.25 % (2682896)Termination phase: Saturation % 124.39/18.25 % (2682896)Time elapsed: 1.105 s % 124.39/18.25 % (2682896)Peak memory usage: 153 MB % 124.39/18.25 % (2682896)Instructions burned: 3606 (million) % 124.39/18.25 % (2682904)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=416517597:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2872 on theBenchmark for (2872ds/3902Mi) % 124.39/18.25 % (2682905)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=449243371:avsq=on:i=3916:aac=none:amm=off_2872 on theBenchmark for (2872ds/3916Mi) % 139.79/20.46 % (2682902)Instruction limit reached! % 139.79/20.46 % (2682902)------------------------------ % 139.79/20.46 % (2682902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.79/20.46 % (2682902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.79/20.46 % (2682902)CaDiCaL version: 2.1.3 % 139.79/20.46 % (2682902)Termination reason: Instruction limit % 139.79/20.46 % (2682902)Termination phase: Saturation % 139.79/20.46 % (2682902)Time elapsed: 0.702 s % 139.79/20.46 % (2682902)Peak memory usage: 138 MB % 139.79/20.46 % (2682902)Instructions burned: 1982 (million) % 139.79/20.46 % (2682908)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2145885370:cond=on:i=3940:av=off:er=known_2867 on theBenchmark for (2867ds/3940Mi) % 139.79/20.46 % (2682904)Instruction limit reached! % 139.79/20.46 % (2682904)------------------------------ % 139.79/20.46 % (2682904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.79/20.46 % (2682904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.79/20.46 % (2682904)CaDiCaL version: 2.1.3 % 139.79/20.46 % (2682904)Termination reason: Instruction limit % 139.79/20.46 % (2682904)Termination phase: Saturation % 139.79/20.46 % (2682904)Time elapsed: 1.131 s % 139.79/20.46 % (2682904)Peak memory usage: 156 MB % 139.79/20.46 % (2682904)Instructions burned: 3903 (million) % 139.79/20.46 % (2682905)Instruction limit reached! % 139.79/20.46 % (2682905)------------------------------ % 139.79/20.46 % (2682905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.79/20.46 % (2682905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.79/20.46 % (2682905)CaDiCaL version: 2.1.3 % 139.79/20.46 % (2682905)Termination reason: Instruction limit % 139.79/20.46 % (2682905)Termination phase: Saturation % 139.79/20.46 % (2682905)Time elapsed: 1.159 s % 139.79/20.46 % (2682905)Peak memory usage: 107 MB % 139.79/20.46 % (2682905)Instructions burned: 3918 (million) % 139.79/20.46 % (2683077)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2480599090:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2859 on theBenchmark for (2859ds/3980Mi) % 139.79/20.46 % (2683104)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=1620609292:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2859 on theBenchmark for (2859ds/2087Mi) % 139.79/20.46 % (2682908)Instruction limit reached! % 139.79/20.46 % (2682908)------------------------------ % 139.79/20.46 % (2682908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.79/20.46 % (2682908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.79/20.46 % (2682908)CaDiCaL version: 2.1.3 % 139.79/20.46 % (2682908)Termination reason: Instruction limit % 139.79/20.46 % (2682908)Termination phase: Saturation % 139.79/20.46 % (2682908)Time elapsed: 1.346 s % 139.79/20.46 % (2682908)Peak memory usage: 154 MB % 139.79/20.46 % (2682908)Instructions burned: 3941 (million) % 139.79/20.46 % (2683175)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=3295260585:cts=off:cond=on:i=4272:bs=on:fsd=on_2852 on theBenchmark for (2852ds/4272Mi) % 139.79/20.47 % (2683104)Instruction limit reached! % 139.79/20.47 % (2683104)------------------------------ % 139.79/20.47 % (2683104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.79/20.47 % (2683104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.79/20.47 % (2683104)CaDiCaL version: 2.1.3 % 139.79/20.47 % (2683104)Termination reason: Instruction limit % 139.79/20.47 % (2683104)Termination phase: Saturation % 139.79/20.47 % (2683104)Time elapsed: 0.748 s % 139.79/20.47 % (2683104)Peak memory usage: 140 MB % 139.79/20.47 % (2683104)Instructions burned: 2088 (million) % 139.79/20.47 % (2683177)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4279389281:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2850 on theBenchmark for (2850ds/2197Mi) % 139.79/20.47 % (2683077)Instruction limit reached! % 139.79/20.47 % (2683077)------------------------------ % 139.79/20.47 % (2683077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.79/20.47 % (2683077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.19 % (2683077)CaDiCaL version: 2.1.3 % 180.19/26.19 % (2683077)Termination reason: Instruction limit % 180.19/26.19 % (2683077)Termination phase: Saturation % 180.19/26.19 % (2683077)Time elapsed: 1.398 s % 180.19/26.19 % (2683077)Peak memory usage: 157 MB % 180.19/26.19 % (2683077)Instructions burned: 3980 (million) % 180.19/26.19 % (2683179)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2103826284:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2844 on theBenchmark for (2844ds/6508Mi) % 180.19/26.19 % (2683177)Instruction limit reached! % 180.19/26.19 % (2683177)------------------------------ % 180.19/26.19 % (2683177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.19/26.19 % (2683177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.19 % (2683177)CaDiCaL version: 2.1.3 % 180.19/26.19 % (2683177)Termination reason: Instruction limit % 180.19/26.19 % (2683177)Termination phase: Saturation % 180.19/26.19 % (2683177)Time elapsed: 0.668 s % 180.19/26.19 % (2683177)Peak memory usage: 140 MB % 180.19/26.19 % (2683177)Instructions burned: 2201 (million) % 180.19/26.19 % (2683181)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=273073328:i=2330:fgj=on:av=off:fsr=off_2842 on theBenchmark for (2842ds/2330Mi) % 180.19/26.19 % (2682893)Instruction limit reached! % 180.19/26.19 % (2682893)------------------------------ % 180.19/26.19 % (2682893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.19/26.19 % (2682893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.19 % (2682893)CaDiCaL version: 2.1.3 % 180.19/26.19 % (2682893)Termination reason: Instruction limit % 180.19/26.19 % (2682893)Termination phase: Saturation % 180.19/26.19 % (2682893)Time elapsed: 5.190 s % 180.19/26.19 % (2682893)Peak memory usage: 236 MB % 180.19/26.19 % (2682893)Instructions burned: 13942 (million) % 180.19/26.19 % (2683175)Instruction limit reached! % 180.19/26.19 % (2683175)------------------------------ % 180.19/26.19 % (2683175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.19/26.19 % (2683175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.19 % (2683175)CaDiCaL version: 2.1.3 % 180.19/26.19 % (2683175)Termination reason: Instruction limit % 180.19/26.19 % (2683175)Termination phase: Saturation % 180.19/26.19 % (2683175)Time elapsed: 1.519 s % 180.19/26.19 % (2683175)Peak memory usage: 150 MB % 180.19/26.19 % (2683175)Instructions burned: 4272 (million) % 180.19/26.19 % (2683183)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2321814058:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2836 on theBenchmark for (2836ds/7592Mi) % 180.19/26.19 % (2683184)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=825902494:i=2693:kws=precedence:ins=1:av=off_2836 on theBenchmark for (2836ds/2693Mi) % 180.19/26.19 % (2683181)Instruction limit reached! % 180.19/26.19 % (2683181)------------------------------ % 180.19/26.19 % (2683181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.19/26.19 % (2683181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.19 % (2683181)CaDiCaL version: 2.1.3 % 180.19/26.19 % (2683181)Termination reason: Instruction limit % 180.19/26.19 % (2683181)Termination phase: Saturation % 180.19/26.19 % (2683181)Time elapsed: 0.784 s % 180.19/26.19 % (2683181)Peak memory usage: 139 MB % 180.19/26.19 % (2683181)Instructions burned: 2330 (million) % 180.19/26.19 % (2683187)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=3427662032:i=28651:sd=4:ss=included:sgt=64_2833 on theBenchmark for (2833ds/28651Mi) % 180.19/26.19 % (2683184)Instruction limit reached! % 180.19/26.19 % (2683184)------------------------------ % 180.19/26.19 % (2683184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.19/26.19 % (2683184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.19/26.19 % (2683184)CaDiCaL version: 2.1.3 % 180.19/26.19 % (2683184)Termination reason: Instruction limit % 180.19/26.19 % (2683184)Termination phase: Saturation % 180.19/26.19 % (2683184)Time elapsed: 0.930 s % 180.19/26.19 % (2683184)Peak memory usage: 146 MB % 180.19/26.19 % (2683184)Instructions burned: 2695 (million) % 180.19/26.19 % (2683189)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1627814264:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2825 on theBenchmark for (2825ds/2700Mi) % 180.19/26.19 % (2683179)Instruction limit reached! % 208.37/30.15 % (2683179)------------------------------ % 208.37/30.15 % (2683179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.37/30.15 % (2683179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/30.15 % (2683179)CaDiCaL version: 2.1.3 % 208.37/30.15 % (2683179)Termination reason: Instruction limit % 208.37/30.15 % (2683179)Termination phase: Saturation % 208.37/30.15 % (2683179)Time elapsed: 2.039 s % 208.37/30.15 % (2683179)Peak memory usage: 130 MB % 208.37/30.15 % (2683179)Instructions burned: 6508 (million) % 208.37/30.15 % (2683191)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=3168989207:i=3196:nm=4_2822 on theBenchmark for (2822ds/3196Mi) % 208.37/30.15 % (2683189)Instruction limit reached! % 208.37/30.15 % (2683189)------------------------------ % 208.37/30.15 % (2683189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.37/30.15 % (2683189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/30.15 % (2683189)CaDiCaL version: 2.1.3 % 208.37/30.15 % (2683189)Termination reason: Instruction limit % 208.37/30.15 % (2683189)Termination phase: Saturation % 208.37/30.15 % (2683189)Time elapsed: 0.937 s % 208.37/30.15 % (2683189)Peak memory usage: 142 MB % 208.37/30.15 % (2683189)Instructions burned: 2701 (million) % 208.37/30.15 % (2683183)Instruction limit reached! % 208.37/30.15 % (2683183)------------------------------ % 208.37/30.15 % (2683183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.37/30.15 % (2683183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/30.15 % (2683183)CaDiCaL version: 2.1.3 % 208.37/30.15 % (2683183)Termination reason: Instruction limit % 208.37/30.15 % (2683183)Termination phase: Saturation % 208.37/30.15 % (2683183)Time elapsed: 2.085 s % 208.37/30.15 % (2683183)Peak memory usage: 150 MB % 208.37/30.15 % (2683183)Instructions burned: 7595 (million) % 208.37/30.15 % (2683193)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=1505819193:cts=off:i=3254:av=off_2814 on theBenchmark for (2814ds/3254Mi) % 208.37/30.15 % (2683194)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=2910116048:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2814 on theBenchmark for (2814ds/3264Mi) % 208.37/30.15 % (2683191)Instruction limit reached! % 208.37/30.15 % (2683191)------------------------------ % 208.37/30.15 % (2683191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.37/30.15 % (2683191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/30.15 % (2683191)CaDiCaL version: 2.1.3 % 208.37/30.15 % (2683191)Termination reason: Instruction limit % 208.37/30.15 % (2683191)Termination phase: Saturation % 208.37/30.15 % (2683191)Time elapsed: 1.016 s % 208.37/30.15 % (2683191)Peak memory usage: 151 MB % 208.37/30.15 % (2683191)Instructions burned: 3197 (million) % 208.37/30.15 % (2683197)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=2371571965:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2811 on theBenchmark for (2811ds/9708Mi) % 208.37/30.15 % (2683193)Instruction limit reached! % 208.37/30.15 % (2683193)------------------------------ % 208.37/30.15 % (2683193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.37/30.15 % (2683193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/30.15 % (2683193)CaDiCaL version: 2.1.3 % 208.37/30.15 % (2683193)Termination reason: Instruction limit % 208.37/30.15 % (2683193)Termination phase: Saturation % 208.37/30.15 % (2683193)Time elapsed: 1.104 s % 208.37/30.15 % (2683193)Peak memory usage: 148 MB % 208.37/30.15 % (2683193)Instructions burned: 3255 (million) % 208.37/30.15 % (2683199)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=633256275:i=21997:s2at=5:gtg=all_2802 on theBenchmark for (2802ds/21997Mi) % 208.37/30.15 % (2683194)Instruction limit reached! % 208.37/30.15 % (2683194)------------------------------ % 208.37/30.15 % (2683194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 208.37/30.15 % (2683194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 208.37/30.15 % (2683194)CaDiCaL version: 2.1.3 % 208.37/30.15 % (2683194)Termination reason: Instruction limit % 208.37/30.15 % (2683194)Termination phase: Saturation % 208.37/30.15 % (2683194)Time elapsed: 1.227 s % 252.33/36.45 % (2683194)Peak memory usage: 146 MB % 252.33/36.45 % (2683194)Instructions burned: 3265 (million) % 252.33/36.45 % (2683201)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2196995552:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2800 on theBenchmark for (2800ds/7551Mi) % 252.33/36.45 % (2683197)Instruction limit reached! % 252.33/36.45 % (2683197)------------------------------ % 252.33/36.45 % (2683197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.33/36.45 % (2683197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.33/36.45 % (2683197)CaDiCaL version: 2.1.3 % 252.33/36.45 % (2683197)Termination reason: Instruction limit % 252.33/36.45 % (2683197)Termination phase: Saturation % 252.33/36.45 % (2683197)Time elapsed: 2.963 s % 252.33/36.45 % (2683197)Peak memory usage: 217 MB % 252.33/36.45 % (2683197)Instructions burned: 9710 (million) % 252.33/36.45 % (2683203)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=261911711:i=8924:sd=1:ss=included_2779 on theBenchmark for (2779ds/8924Mi) % 252.33/36.45 % (2683201)Instruction limit reached! % 252.33/36.45 % (2683201)------------------------------ % 252.33/36.45 % (2683201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.33/36.45 % (2683201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.33/36.45 % (2683201)CaDiCaL version: 2.1.3 % 252.33/36.45 % (2683201)Termination reason: Instruction limit % 252.33/36.45 % (2683201)Termination phase: Saturation % 252.33/36.45 % (2683201)Time elapsed: 2.369 s % 252.33/36.45 % (2683201)Peak memory usage: 133 MB % 252.33/36.45 % (2683201)Instructions burned: 7554 (million) % 252.33/36.45 % (2683205)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=474455107:i=9638:kws=frequency:bd=preordered_2775 on theBenchmark for (2775ds/9638Mi) % 252.33/36.45 % (2683187)Instruction limit reached! % 252.33/36.45 % (2683187)------------------------------ % 252.33/36.45 % (2683187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.33/36.45 % (2683187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.33/36.45 % (2683187)CaDiCaL version: 2.1.3 % 252.33/36.45 % (2683187)Termination reason: Instruction limit % 252.33/36.45 % (2683187)Termination phase: Saturation % 252.33/36.45 % (2683187)Time elapsed: 7.324 s % 252.33/36.45 % (2683187)Peak memory usage: 290 MB % 252.33/36.45 % (2683187)Instructions burned: 28653 (million) % 252.33/36.45 % (2683207)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=1546987358:i=5177:s2at=1.5:bd=preordered:ins=10:fdi=128_2758 on theBenchmark for (2758ds/5177Mi) % 252.33/36.45 % (2683207)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 252.33/36.45 % (2683207)------------------------------ % 252.33/36.45 % (2683207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.33/36.45 % (2683207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.33/36.45 % (2683207)CaDiCaL version: 2.1.3 % 252.33/36.45 % (2683207)Termination reason: Unknown % 252.33/36.45 % (2683207)Termination phase: Saturation % 252.33/36.45 % (2683207)Time elapsed: 0.331 s % 252.33/36.45 % (2683207)Peak memory usage: 130 MB % 252.33/36.45 % (2683207)Instructions burned: 921 (million) % 252.33/36.45 % (2683203)Instruction limit reached! % 252.33/36.45 % (2683203)------------------------------ % 252.33/36.45 % (2683203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.33/36.45 % (2683203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.33/36.45 % (2683203)CaDiCaL version: 2.1.3 % 252.33/36.45 % (2683203)Termination reason: Instruction limit % 252.33/36.45 % (2683203)Termination phase: Saturation % 252.33/36.45 % (2683203)Time elapsed: 2.618 s % 252.33/36.45 % (2683203)Peak memory usage: 258 MB % 252.33/36.45 % (2683203)Instructions burned: 8926 (million) % 252.33/36.45 % (2683209)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=2132506459:i=6464:aac=none:ins=10_2753 on theBenchmark for (2753ds/6464Mi) % 252.33/36.45 % (2683211)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:erd=off:urr=on:bsr=on:fd=preordered:random_seed=295775312:i=19192:av=off_2752 on theBenchmark for (2752ds/19192Mi) % 252.33/36.45 % (2683205)Instruction limit reached! % 252.33/36.45 % (2683205)------------------------------ % 252.33/36.45 % (2683205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.09/40.67 % (2683205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.09/40.67 % (2683205)CaDiCaL version: 2.1.3 % 282.09/40.67 % (2683205)Termination reason: Instruction limit % 282.09/40.67 % (2683205)Termination phase: Saturation % 282.09/40.67 % (2683205)Time elapsed: 3.067 s % 282.09/40.67 % (2683205)Peak memory usage: 164 MB % 282.09/40.67 % (2683205)Instructions burned: 9642 (million) % 282.09/40.67 % (2683213)lrs+10_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=8000:npcc=on:prc=on:fde=unused:sp=const_min:random_seed=1743043239:i=7136:fgj=on:bd=preordered:ins=3:ss=included_2743 on theBenchmark for (2743ds/7136Mi) % 282.09/40.67 % (2683199)Instruction limit reached! % 282.09/40.67 % (2683199)------------------------------ % 282.09/40.67 % (2683199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.09/40.67 % (2683199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.09/40.67 % (2683199)CaDiCaL version: 2.1.3 % 282.09/40.67 % (2683199)Termination reason: Instruction limit % 282.09/40.67 % (2683199)Termination phase: Saturation % 282.09/40.67 % (2683199)Time elapsed: 6.411 s % 282.09/40.67 % (2683199)Peak memory usage: 247 MB % 282.09/40.67 % (2683199)Instructions burned: 21998 (million) % 282.09/40.67 % (2683215)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop6.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=2224541269:cts=off:cond=on:i=7540:bs=on:fsd=on_2737 on theBenchmark for (2737ds/7540Mi) % 282.09/40.67 % (2683209)Instruction limit reached! % 282.09/40.67 % (2683209)------------------------------ % 282.09/40.67 % (2683209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.09/40.67 % (2683209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.09/40.67 % (2683209)CaDiCaL version: 2.1.3 % 282.09/40.67 % (2683209)Termination reason: Instruction limit % 282.09/40.67 % (2683209)Termination phase: Saturation % 282.09/40.67 % (2683209)Time elapsed: 2.310 s % 282.09/40.67 % (2683209)Peak memory usage: 176 MB % 282.09/40.67 % (2683209)Instructions burned: 6467 (million) % 282.09/40.67 % (2683217)ott+1011_1_to=lpo:ncem=casc2026/models/loop5.pt:sil=64000:tgt=ground:npcc=on:drc=off:sp=const_frequency:random_seed=3465497301:i=15570:s2at=5:gtgl=4:gtg=exists_sym_2729 on theBenchmark for (2729ds/15570Mi) % 282.09/40.67 % (2683213)Instruction limit reached! % 282.09/40.67 % (2683213)------------------------------ % 282.09/40.67 % (2683213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.09/40.67 % (2683213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.09/40.67 % (2683213)CaDiCaL version: 2.1.3 % 282.09/40.67 % (2683213)Termination reason: Instruction limit % 282.09/40.67 % (2683213)Termination phase: Saturation % 282.09/40.67 % (2683213)Time elapsed: 2.589 s % 282.09/40.67 % (2683213)Peak memory usage: 173 MB % 282.09/40.67 % (2683213)Instructions burned: 7139 (million) % 282.09/40.67 % (2683219)lrs+1011_1_anc=none:to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lsd=20:bce=on:bsr=on:fd=preordered:gs=on:random_seed=1280569335:i=15957:add=on:fgj=on_2716 on theBenchmark for (2716ds/15957Mi) % 282.09/40.67 % (2683215)Instruction limit reached! % 282.09/40.67 % (2683215)------------------------------ % 282.09/40.67 % (2683215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.09/40.67 % (2683215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.09/40.67 % (2683215)CaDiCaL version: 2.1.3 % 282.09/40.67 % (2683215)Termination reason: Instruction limit % 282.09/40.67 % (2683215)Termination phase: Saturation % 282.09/40.67 % (2683215)Time elapsed: 2.522 s % 282.09/40.67 % (2683215)Peak memory usage: 160 MB % 282.09/40.67 % (2683215)Instructions burned: 7540 (million) % 282.09/40.67 % (2683221)lrs+1010_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=32000:tgt=full:npcc=on:prc=on:drc=ordering:fde=none:sp=arity:spb=intro:urr=ec_only:s2agt=40:random_seed=1698830101:cond=on:i=8289:erml=3:bd=preordered:er=filter:proc=on_2710 on theBenchmark for (2710ds/8289Mi) % 282.09/40.67 % (2683211)Instruction limit reached! % 282.09/40.67 % (2683211)------------------------------ % 282.09/40.67 % (2683211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.09/40.67 % (2683211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.09/40.67 % (2683211)CaDiCaL version: 2.1.3 % 282.09/40.67 % (2683211)Termination reason: Instruction limit % 282.09/40.67 % (2683211)TerminTerminated % 300.43/43.24 % Vampire exiting %------------------------------------------------------------------------------