%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM193-1 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n003.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:53 PM UTC 2026 % Result : Timeout 300.27s 43.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM193-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.37 % Computer : n003.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.09/0.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Sun Sep 27 19:11:12 UTC 2026 % 0.09/0.38 % CPUTime : % 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.41 Running first-order theorem proving % 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.80/2.28 % (866504)Input is clausal, will run a generic CNF schedule. % 9.80/2.28 % (866512)lrs+10_1_sil=8000:sp=occurrence:random_seed=1860112876:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 9.80/2.28 % (866512)Instruction limit reached! % 9.80/2.28 % (866512)------------------------------ % 9.80/2.28 % (866512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.80/2.28 % (866512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.80/2.28 % (866512)CaDiCaL version: 2.1.3 % 9.80/2.28 % (866512)Termination reason: Instruction limit % 9.80/2.28 % (866512)Termination phase: Saturation % 9.80/2.28 % (866512)Time elapsed: 0.033 s % 9.80/2.28 % (866512)Peak memory usage: 89 MB % 9.80/2.28 % (866512)Instructions burned: 110 (million) % 9.80/2.28 % (866515)dis-21_1_sil=8000:lcm=predicate:random_seed=1754051604: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.80/2.28 % (866510)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=276643215:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 9.80/2.28 % (866509)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=4085138863:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 9.80/2.28 % (866511)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1825278720:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 9.80/2.28 % (866513)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2795614765:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 9.80/2.28 % (866514)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1268704371:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 9.80/2.28 % (866513)Instruction limit reached! % 9.80/2.28 % (866513)------------------------------ % 9.80/2.28 % (866513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.80/2.28 % (866513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.80/2.28 % (866513)CaDiCaL version: 2.1.3 % 9.80/2.28 % (866513)Termination reason: Instruction limit % 9.80/2.28 % (866513)Termination phase: Saturation % 9.80/2.28 % (866513)Time elapsed: 0.069 s % 9.80/2.28 % (866513)Peak memory usage: 89 MB % 9.80/2.28 % (866513)Instructions burned: 115 (million) % 9.80/2.28 % (866515)Instruction limit reached! % 9.80/2.28 % (866515)------------------------------ % 9.80/2.28 % (866515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.80/2.28 % (866515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.80/2.28 % (866515)CaDiCaL version: 2.1.3 % 9.80/2.28 % (866515)Termination reason: Instruction limit % 9.80/2.28 % (866515)Termination phase: Saturation % 9.80/2.28 % (866515)Time elapsed: 0.071 s % 9.80/2.28 % (866515)Peak memory usage: 89 MB % 9.80/2.28 % (866515)Instructions burned: 118 (million) % 9.80/2.28 % (866523)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=1046165765:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 9.80/2.28 % (866523)Refutation not found, incomplete strategy % 9.80/2.28 % (866523)------------------------------ % 9.80/2.28 % (866523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.80/2.28 % (866523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.80/2.28 % (866523)CaDiCaL version: 2.1.3 % 9.80/2.28 % (866523)Termination reason: Refutation not found, incomplete strategy % 9.80/2.28 % (866523)Time elapsed: 0.002 s % 9.80/2.28 % (866523)Peak memory usage: 88 MB % 9.80/2.28 % (866523)Instructions burned: 5 (million) % 9.80/2.28 % (866514)Instruction limit reached! % 9.80/2.28 % (866514)------------------------------ % 9.80/2.28 % (866514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.80/2.28 % (866514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.80/2.28 % (866514)CaDiCaL version: 2.1.3 % 9.80/2.28 % (866514)Termination reason: Instruction limit % 9.80/2.28 % (866514)Termination phase: Saturation % 9.80/2.28 % (866514)Time elapsed: 0.135 s % 9.80/2.28 % (866514)Peak memory usage: 91 MB % 9.80/2.28 % (866514)Instructions burned: 180 (million) % 9.80/2.28 % (866524)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1875534417:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi) % 21.65/3.92 % (866525)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4183594458:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 21.65/3.92 % (866525)Refutation not found, incomplete strategy % 21.65/3.92 % (866525)------------------------------ % 21.65/3.92 % (866525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/3.92 % (866525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.65/3.92 % (866525)CaDiCaL version: 2.1.3 % 21.65/3.92 % (866525)Termination reason: Refutation not found, incomplete strategy % 21.65/3.92 % (866525)Time elapsed: 0.004 s % 21.65/3.92 % (866525)Peak memory usage: 88 MB % 21.65/3.92 % (866525)Instructions burned: 4 (million) % 21.65/3.92 % (866523)------------------------------ % 21.65/3.92 % (866523)------------------------------ % 21.65/3.92 % (866527)lrs+10_64_to=lpo:sil=8000:random_seed=2415372850:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 21.65/3.92 % (866524)Instruction limit reached! % 21.65/3.92 % (866524)------------------------------ % 21.65/3.92 % (866524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/3.92 % (866524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.65/3.92 % (866524)CaDiCaL version: 2.1.3 % 21.65/3.92 % (866524)Termination reason: Instruction limit % 21.65/3.92 % (866524)Termination phase: Saturation % 21.65/3.92 % (866524)Time elapsed: 0.107 s % 21.65/3.92 % (866524)Peak memory usage: 90 MB % 21.65/3.92 % (866524)Instructions burned: 189 (million) % 21.65/3.92 % (866527)Instruction limit reached! % 21.65/3.92 % (866527)------------------------------ % 21.65/3.92 % (866527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/3.92 % (866527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.65/3.92 % (866527)CaDiCaL version: 2.1.3 % 21.65/3.92 % (866527)Termination reason: Instruction limit % 21.65/3.92 % (866527)Termination phase: Saturation % 21.65/3.92 % (866527)Time elapsed: 0.083 s % 21.65/3.92 % (866527)Peak memory usage: 89 MB % 21.65/3.92 % (866527)Instructions burned: 127 (million) % 21.65/3.92 % (866530)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4222465569:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 21.65/3.92 % (866530)Instruction limit reached! % 21.65/3.92 % (866530)------------------------------ % 21.65/3.92 % (866530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/3.92 % (866530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.65/3.92 % (866530)CaDiCaL version: 2.1.3 % 21.65/3.92 % (866530)Termination reason: Instruction limit % 21.65/3.92 % (866530)Termination phase: Saturation % 21.65/3.92 % (866530)Time elapsed: 0.064 s % 21.65/3.92 % (866530)Peak memory usage: 90 MB % 21.65/3.92 % (866530)Instructions burned: 197 (million) % 21.65/3.92 % (866532)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3591967223:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 21.65/3.92 % (866525)------------------------------ % 21.65/3.92 % (866525)------------------------------ % 21.65/3.92 % (866534)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3146588816:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 21.65/3.92 % (866535)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=4244958867:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 21.65/3.92 % (866535)Instruction limit reached! % 21.65/3.92 % (866535)------------------------------ % 21.65/3.92 % (866535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/3.92 % (866535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.65/3.92 % (866535)CaDiCaL version: 2.1.3 % 21.65/3.92 % (866535)Termination reason: Instruction limit % 21.65/3.92 % (866535)Termination phase: Saturation % 21.65/3.92 % (866535)Time elapsed: 0.034 s % 21.65/3.92 % (866535)Peak memory usage: 89 MB % 21.65/3.92 % (866535)Instructions burned: 108 (million) % 21.65/3.92 % (866532)Instruction limit reached! % 21.65/3.92 % (866532)------------------------------ % 21.65/3.92 % (866532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.65/3.92 % (866532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.19/5.58 % (866532)CaDiCaL version: 2.1.3 % 33.19/5.58 % (866532)Termination reason: Instruction limit % 33.19/5.58 % (866532)Termination phase: Saturation % 33.19/5.58 % (866532)Time elapsed: 0.114 s % 33.19/5.58 % (866532)Peak memory usage: 91 MB % 33.19/5.58 % (866532)Instructions burned: 157 (million) % 33.19/5.58 % (866537)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3899013901:i=107_2993 on theBenchmark for (2993ds/107Mi) % 33.19/5.58 % (866537)Refutation not found, incomplete strategy % 33.19/5.58 % (866537)------------------------------ % 33.19/5.58 % (866537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.19/5.58 % (866537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.19/5.58 % (866537)CaDiCaL version: 2.1.3 % 33.19/5.58 % (866537)Termination reason: Refutation not found, incomplete strategy % 33.19/5.58 % (866537)Time elapsed: 0.006 s % 33.19/5.58 % (866537)Peak memory usage: 88 MB % 33.19/5.58 % (866537)Instructions burned: 11 (million) % 33.19/5.58 % (866540)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2713639555:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi) % 33.19/5.58 % (866541)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=418400293:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi) % 33.19/5.58 % (866540)Instruction limit reached! % 33.19/5.58 % (866540)------------------------------ % 33.19/5.58 % (866540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.19/5.58 % (866540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.19/5.58 % (866540)CaDiCaL version: 2.1.3 % 33.19/5.58 % (866540)Termination reason: Instruction limit % 33.19/5.58 % (866540)Termination phase: Saturation % 33.19/5.58 % (866540)Time elapsed: 0.075 s % 33.19/5.58 % (866540)Peak memory usage: 91 MB % 33.19/5.58 % (866540)Instructions burned: 243 (million) % 33.19/5.58 % (866545)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1345438305:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi) % 33.19/5.58 % (866545)Refutation not found, incomplete strategy % 33.19/5.58 % (866545)------------------------------ % 33.19/5.58 % (866545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.19/5.58 % (866545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.19/5.58 % (866545)CaDiCaL version: 2.1.3 % 33.19/5.58 % (866545)Termination reason: Refutation not found, incomplete strategy % 33.19/5.58 % (866545)Time elapsed: 0.006 s % 33.19/5.58 % (866545)Peak memory usage: 88 MB % 33.19/5.58 % (866545)Instructions burned: 16 (million) % 33.19/5.58 % (866537)------------------------------ % 33.19/5.58 % (866537)------------------------------ % 33.19/5.58 % (866545)------------------------------ % 33.19/5.58 % (866545)------------------------------ % 33.19/5.58 % (866547)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1724071719:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi) % 33.19/5.58 % (866548)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3807605498:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi) % 33.19/5.58 % (866548)Instruction limit reached! % 33.19/5.58 % (866548)------------------------------ % 33.19/5.58 % (866548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.19/5.58 % (866548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.19/5.58 % (866548)CaDiCaL version: 2.1.3 % 33.19/5.58 % (866548)Termination reason: Instruction limit % 33.19/5.58 % (866548)Termination phase: Saturation % 33.19/5.58 % (866548)Time elapsed: 0.056 s % 33.19/5.58 % (866548)Peak memory usage: 89 MB % 33.19/5.58 % (866548)Instructions burned: 193 (million) % 33.19/5.58 % (866551)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3880816876:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi) % 33.19/5.58 % (866551)Instruction limit reached! % 33.19/5.58 % (866551)------------------------------ % 33.19/5.58 % (866551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.19/5.58 % (866551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.19/5.58 % (866551)CaDiCaL version: 2.1.3 % 33.19/5.58 % (866551)Termination reason: Instruction limit % 33.19/5.58 % (866551)Termination phase: Saturation % 33.19/5.58 % (866551)Time elapsed: 0.088 s % 33.19/5.58 % (866551)Peak memory usage: 91 MB % 47.91/7.68 % (866551)Instructions burned: 265 (million) % 47.91/7.68 % (866547)Instruction limit reached! % 47.91/7.68 % (866547)------------------------------ % 47.91/7.68 % (866547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.91/7.68 % (866547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.91/7.68 % (866547)CaDiCaL version: 2.1.3 % 47.91/7.68 % (866547)Termination reason: Instruction limit % 47.91/7.68 % (866547)Termination phase: Saturation % 47.91/7.68 % (866547)Time elapsed: 0.314 s % 47.91/7.68 % (866547)Peak memory usage: 93 MB % 47.91/7.68 % (866547)Instructions burned: 500 (million) % 47.91/7.68 % (866553)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3956103794:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi) % 47.91/7.68 % (866553)Instruction limit reached! % 47.91/7.68 % (866553)------------------------------ % 47.91/7.68 % (866553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.91/7.68 % (866553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.91/7.68 % (866553)CaDiCaL version: 2.1.3 % 47.91/7.68 % (866553)Termination reason: Instruction limit % 47.91/7.68 % (866553)Termination phase: Saturation % 47.91/7.68 % (866553)Time elapsed: 0.053 s % 47.91/7.68 % (866553)Peak memory usage: 89 MB % 47.91/7.68 % (866553)Instructions burned: 156 (million) % 47.91/7.68 % (866554)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=1996553108:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi) % 47.91/7.68 % (866556)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1967955850:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi) % 47.91/7.68 % (866556)Instruction limit reached! % 47.91/7.68 % (866556)------------------------------ % 47.91/7.68 % (866556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.91/7.68 % (866556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.91/7.68 % (866556)CaDiCaL version: 2.1.3 % 47.91/7.68 % (866556)Termination reason: Instruction limit % 47.91/7.68 % (866556)Termination phase: Saturation % 47.91/7.68 % (866556)Time elapsed: 0.149 s % 47.91/7.68 % (866556)Peak memory usage: 88 MB % 47.91/7.68 % (866556)Instructions burned: 540 (million) % 47.91/7.68 % (866559)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3084501749:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi) % 47.91/7.68 % (866559)Instruction limit reached! % 47.91/7.68 % (866559)------------------------------ % 47.91/7.68 % (866559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.91/7.68 % (866559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.91/7.68 % (866559)CaDiCaL version: 2.1.3 % 47.91/7.68 % (866559)Termination reason: Instruction limit % 47.91/7.68 % (866559)Termination phase: Saturation % 47.91/7.68 % (866559)Time elapsed: 0.058 s % 47.91/7.68 % (866559)Peak memory usage: 90 MB % 47.91/7.68 % (866559)Instructions burned: 182 (million) % 47.91/7.68 % (866561)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=4112973611:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi) % 47.91/7.68 % (866534)Instruction limit reached! % 47.91/7.68 % (866534)------------------------------ % 47.91/7.68 % (866534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.91/7.68 % (866534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.91/7.68 % (866534)CaDiCaL version: 2.1.3 % 47.91/7.68 % (866534)Termination reason: Instruction limit % 47.91/7.68 % (866534)Termination phase: Saturation % 47.91/7.68 % (866534)Time elapsed: 2.118 s % 47.91/7.68 % (866534)Peak memory usage: 149 MB % 47.91/7.68 % (866534)Instructions burned: 3396 (million) % 47.91/7.68 % (866563)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=3643721125:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi) % 47.91/7.68 % (866563)Instruction limit reached! % 47.91/7.68 % (866563)------------------------------ % 47.91/7.68 % (866563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.91/7.68 % (866563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.91/7.68 % (866563)CaDiCaL version: 2.1.3 % 67.98/10.44 % (866563)Termination reason: Instruction limit % 67.98/10.44 % (866563)Termination phase: Saturation % 67.98/10.44 % (866563)Time elapsed: 0.185 s % 67.98/10.44 % (866563)Peak memory usage: 90 MB % 67.98/10.44 % (866563)Instructions burned: 412 (million) % 67.98/10.44 % (866565)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=2210067897:s2pl=no:i=8478:s2at=4:nm=6_2969 on theBenchmark for (2969ds/8478Mi) % 67.98/10.44 % (866554)Instruction limit reached! % 67.98/10.44 % (866554)------------------------------ % 67.98/10.44 % (866554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.98/10.44 % (866554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.98/10.44 % (866554)CaDiCaL version: 2.1.3 % 67.98/10.44 % (866554)Termination reason: Instruction limit % 67.98/10.44 % (866554)Termination phase: Saturation % 67.98/10.44 % (866554)Time elapsed: 1.988 s % 67.98/10.44 % (866554)Peak memory usage: 148 MB % 67.98/10.44 % (866554)Instructions burned: 3257 (million) % 67.98/10.44 % (866567)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=3093550723:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2964 on theBenchmark for (2964ds/303Mi) % 67.98/10.44 % (866567)Refutation not found, incomplete strategy % 67.98/10.44 % (866567)------------------------------ % 67.98/10.44 % (866567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.98/10.44 % (866567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.98/10.44 % (866567)CaDiCaL version: 2.1.3 % 67.98/10.44 % (866567)Termination reason: Refutation not found, incomplete strategy % 67.98/10.44 % (866567)Time elapsed: 0.002 s % 67.98/10.44 % (866567)Peak memory usage: 88 MB % 67.98/10.44 % (866567)Instructions burned: 1 (million) % 67.98/10.44 % (866567)------------------------------ % 67.98/10.44 % (866567)------------------------------ % 67.98/10.44 % (866569)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2405965107:st=4:i=720:sd=3:fsr=off:ss=axioms_2960 on theBenchmark for (2960ds/720Mi) % 67.98/10.44 % (866541)Instruction limit reached! % 67.98/10.44 % (866541)------------------------------ % 67.98/10.44 % (866541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.98/10.44 % (866541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.98/10.44 % (866541)CaDiCaL version: 2.1.3 % 67.98/10.44 % (866541)Termination reason: Instruction limit % 67.98/10.44 % (866541)Termination phase: Saturation % 67.98/10.44 % (866541)Time elapsed: 3.268 s % 67.98/10.44 % (866541)Peak memory usage: 157 MB % 67.98/10.44 % (866541)Instructions burned: 5209 (million) % 67.98/10.44 % (866571)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3659909820:i=598:bs=on:bd=preordered:av=off:ss=axioms_2958 on theBenchmark for (2958ds/598Mi) % 67.98/10.44 % (866569)Instruction limit reached! % 67.98/10.44 % (866569)------------------------------ % 67.98/10.44 % (866569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.98/10.44 % (866569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.98/10.44 % (866569)CaDiCaL version: 2.1.3 % 67.98/10.44 % (866569)Termination reason: Instruction limit % 67.98/10.44 % (866569)Termination phase: Saturation % 67.98/10.44 % (866569)Time elapsed: 0.482 s % 67.98/10.44 % (866569)Peak memory usage: 96 MB % 67.98/10.44 % (866569)Instructions burned: 721 (million) % 67.98/10.44 % (866571)Instruction limit reached! % 67.98/10.44 % (866571)------------------------------ % 67.98/10.44 % (866571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.98/10.44 % (866571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.98/10.44 % (866571)CaDiCaL version: 2.1.3 % 67.98/10.44 % (866571)Termination reason: Instruction limit % 67.98/10.44 % (866571)Termination phase: Saturation % 67.98/10.44 % (866571)Time elapsed: 0.336 s % 67.98/10.44 % (866571)Peak memory usage: 90 MB % 67.98/10.44 % (866571)Instructions burned: 600 (million) % 67.98/10.44 % (866573)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=861694782:i=2989:sd=3:ss=axioms:sgt=60_2954 on theBenchmark for (2954ds/2989Mi) % 67.98/10.44 % (866574)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=899557328:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2954 on theBenchmark for (2954ds/1997Mi) % 96.37/14.42 % (866561)Instruction limit reached! % 96.37/14.42 % (866561)------------------------------ % 96.37/14.42 % (866561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (866561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (866561)CaDiCaL version: 2.1.3 % 96.37/14.42 % (866561)Termination reason: Instruction limit % 96.37/14.42 % (866561)Termination phase: Saturation % 96.37/14.42 % (866561)Time elapsed: 3.557 s % 96.37/14.42 % (866561)Peak memory usage: 170 MB % 96.37/14.42 % (866561)Instructions burned: 10307 (million) % 96.37/14.42 % (866577)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=528195610:i=2088:bd=preordered:av=off_2943 on theBenchmark for (2943ds/2088Mi) % 96.37/14.42 % (866574)Instruction limit reached! % 96.37/14.42 % (866574)------------------------------ % 96.37/14.42 % (866574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (866574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (866574)CaDiCaL version: 2.1.3 % 96.37/14.42 % (866574)Termination reason: Instruction limit % 96.37/14.42 % (866574)Termination phase: Saturation % 96.37/14.42 % (866574)Time elapsed: 1.291 s % 96.37/14.42 % (866574)Peak memory usage: 137 MB % 96.37/14.42 % (866574)Instructions burned: 1997 (million) % 96.37/14.42 % (866579)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1396763415:i=1098:nicw=on_2939 on theBenchmark for (2939ds/1098Mi) % 96.37/14.42 % (866577)Instruction limit reached! % 96.37/14.42 % (866577)------------------------------ % 96.37/14.42 % (866577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (866577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (866577)CaDiCaL version: 2.1.3 % 96.37/14.42 % (866577)Termination reason: Instruction limit % 96.37/14.42 % (866577)Termination phase: Saturation % 96.37/14.42 % (866577)Time elapsed: 0.733 s % 96.37/14.42 % (866577)Peak memory usage: 139 MB % 96.37/14.42 % (866577)Instructions burned: 2091 (million) % 96.37/14.42 % (866581)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2586582719:i=433:bd=preordered_2935 on theBenchmark for (2935ds/433Mi) % 96.37/14.42 % (866581)Refutation not found, incomplete strategy % 96.37/14.42 % (866581)------------------------------ % 96.37/14.42 % (866581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (866581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (866581)CaDiCaL version: 2.1.3 % 96.37/14.42 % (866581)Termination reason: Refutation not found, incomplete strategy % 96.37/14.42 % (866581)Time elapsed: 0.007 s % 96.37/14.42 % (866581)Peak memory usage: 88 MB % 96.37/14.42 % (866581)Instructions burned: 20 (million) % 96.37/14.42 % (866573)Instruction limit reached! % 96.37/14.42 % (866573)------------------------------ % 96.37/14.42 % (866573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (866573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (866573)CaDiCaL version: 2.1.3 % 96.37/14.42 % (866573)Termination reason: Instruction limit % 96.37/14.42 % (866573)Termination phase: Saturation % 96.37/14.42 % (866573)Time elapsed: 1.834 s % 96.37/14.42 % (866573)Peak memory usage: 143 MB % 96.37/14.42 % (866573)Instructions burned: 2990 (million) % 96.37/14.42 % (866583)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=589196017:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2934 on theBenchmark for (2934ds/2942Mi) % 96.37/14.42 % (866581)------------------------------ % 96.37/14.42 % (866581)------------------------------ % 96.37/14.42 % (866585)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=125733205:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2933 on theBenchmark for (2933ds/6922Mi) % 96.37/14.42 % (866579)Instruction limit reached! % 96.37/14.42 % (866579)------------------------------ % 96.37/14.42 % (866579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (866579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (866579)CaDiCaL version: 2.1.3 % 96.37/14.42 % (866579)Termination reason: Instruction limit % 96.37/14.42 % (866579)Termination phase: Saturation % 111.39/16.68 % (866579)Time elapsed: 0.674 s % 111.39/16.68 % (866579)Peak memory usage: 101 MB % 111.39/16.68 % (866579)Instructions burned: 1098 (million) % 111.39/16.68 % (866587)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=2779144002:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2931 on theBenchmark for (2931ds/596Mi) % 111.39/16.68 % (866587)Instruction limit reached! % 111.39/16.68 % (866587)------------------------------ % 111.39/16.68 % (866587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.39/16.68 % (866587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.39/16.68 % (866587)CaDiCaL version: 2.1.3 % 111.39/16.68 % (866587)Termination reason: Instruction limit % 111.39/16.68 % (866587)Termination phase: Saturation % 111.39/16.68 % (866587)Time elapsed: 0.321 s % 111.39/16.68 % (866587)Peak memory usage: 99 MB % 111.39/16.68 % (866587)Instructions burned: 596 (million) % 111.39/16.68 % (866589)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=4222716990:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2927 on theBenchmark for (2927ds/4123Mi) % 111.39/16.68 % (866565)Instruction limit reached! % 111.39/16.68 % (866565)------------------------------ % 111.39/16.68 % (866565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.39/16.68 % (866565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.39/16.68 % (866565)CaDiCaL version: 2.1.3 % 111.39/16.68 % (866565)Termination reason: Instruction limit % 111.39/16.68 % (866565)Termination phase: Saturation % 111.39/16.68 % (866565)Time elapsed: 4.904 s % 111.39/16.68 % (866565)Peak memory usage: 164 MB % 111.39/16.68 % (866565)Instructions burned: 8480 (million) % 111.39/16.68 % (866591)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3235088741:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2918 on theBenchmark for (2918ds/16411Mi) % 111.39/16.68 % (866583)Instruction limit reached! % 111.39/16.68 % (866583)------------------------------ % 111.39/16.68 % (866583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.39/16.68 % (866583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.39/16.68 % (866583)CaDiCaL version: 2.1.3 % 111.39/16.68 % (866583)Termination reason: Instruction limit % 111.39/16.68 % (866583)Termination phase: Saturation % 111.39/16.68 % (866583)Time elapsed: 1.966 s % 111.39/16.68 % (866583)Peak memory usage: 142 MB % 111.39/16.68 % (866583)Instructions burned: 2943 (million) % 111.39/16.68 % (866593)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2256352570:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2913 on theBenchmark for (2913ds/1670Mi) % 111.39/16.68 % (866585)Instruction limit reached! % 111.39/16.68 % (866585)------------------------------ % 111.39/16.68 % (866585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.39/16.68 % (866585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.39/16.68 % (866585)CaDiCaL version: 2.1.3 % 111.39/16.68 % (866585)Termination reason: Instruction limit % 111.39/16.68 % (866585)Termination phase: Saturation % 111.39/16.68 % (866585)Time elapsed: 2.091 s % 111.39/16.68 % (866585)Peak memory usage: 185 MB % 111.39/16.68 % (866585)Instructions burned: 6924 (million) % 111.39/16.68 % (866595)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=1436834949:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2911 on theBenchmark for (2911ds/1722Mi) % 111.39/16.68 % (866595)Refutation not found, incomplete strategy % 111.39/16.68 % (866595)------------------------------ % 111.39/16.68 % (866595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.39/16.68 % (866595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.39/16.68 % (866595)CaDiCaL version: 2.1.3 % 111.39/16.68 % (866595)Termination reason: Refutation not found, incomplete strategy % 111.39/16.68 % (866595)Time elapsed: 0.381 s % 111.39/16.68 % (866595)Peak memory usage: 129 MB % 111.39/16.68 % (866595)Instructions burned: 929 (million) % 111.39/16.68 % (866593)Instruction limit reached! % 111.39/16.68 % (866593)------------------------------ % 111.39/16.68 % (866593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.39/16.68 % (866593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.39/16.68 % (866593)CaDiCaL version: 2.1.3 % 134.53/19.96 % (866593)Termination reason: Instruction limit % 134.53/19.96 % (866593)Termination phase: Saturation % 134.53/19.96 % (866593)Time elapsed: 0.797 s % 134.53/19.96 % (866593)Peak memory usage: 136 MB % 134.53/19.96 % (866593)Instructions burned: 1675 (million) % 134.53/19.96 % (866595)------------------------------ % 134.53/19.96 % (866595)------------------------------ % 134.53/19.96 % (866597)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=3973232265:cts=off:cond=on:i=9530:bs=on:fsd=on_2904 on theBenchmark for (2904ds/9530Mi) % 134.53/19.96 % (866598)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1027724192:st=2:i=4495:sd=10:ss=included_2904 on theBenchmark for (2904ds/4495Mi) % 134.53/19.96 % (866589)Instruction limit reached! % 134.53/19.96 % (866589)------------------------------ % 134.53/19.96 % (866589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.53/19.96 % (866589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.53/19.96 % (866589)CaDiCaL version: 2.1.3 % 134.53/19.96 % (866589)Termination reason: Instruction limit % 134.53/19.96 % (866589)Termination phase: Saturation % 134.53/19.96 % (866589)Time elapsed: 2.562 s % 134.53/19.96 % (866589)Peak memory usage: 156 MB % 134.53/19.96 % (866589)Instructions burned: 4125 (million) % 134.53/19.96 % (866601)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=2941189511:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2900 on theBenchmark for (2900ds/4920Mi) % 134.53/19.96 % (866598)Instruction limit reached! % 134.53/19.96 % (866598)------------------------------ % 134.53/19.96 % (866598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.53/19.96 % (866598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.53/19.96 % (866598)CaDiCaL version: 2.1.3 % 134.53/19.96 % (866598)Termination reason: Instruction limit % 134.53/19.96 % (866598)Termination phase: Saturation % 134.53/19.96 % (866598)Time elapsed: 2.660 s % 134.53/19.96 % (866598)Peak memory usage: 159 MB % 134.53/19.96 % (866598)Instructions burned: 4495 (million) % 134.53/19.96 % (866605)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=3033069175:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2875 on theBenchmark for (2875ds/2083Mi) % 134.53/19.96 % (866597)Instruction limit reached! % 134.53/19.96 % (866597)------------------------------ % 134.53/19.96 % (866597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.53/19.96 % (866597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.53/19.96 % (866597)CaDiCaL version: 2.1.3 % 134.53/19.96 % (866597)Termination reason: Instruction limit % 134.53/19.96 % (866597)Termination phase: Saturation % 134.53/19.96 % (866597)Time elapsed: 3.430 s % 134.53/19.96 % (866597)Peak memory usage: 169 MB % 134.53/19.96 % (866597)Instructions burned: 9530 (million) % 134.53/19.96 % (866601)Instruction limit reached! % 134.53/19.96 % (866601)------------------------------ % 134.53/19.96 % (866601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.53/19.96 % (866601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.53/19.96 % (866601)CaDiCaL version: 2.1.3 % 134.53/19.96 % (866601)Termination reason: Instruction limit % 134.53/19.96 % (866601)Termination phase: Saturation % 134.53/19.96 % (866601)Time elapsed: 3.001 s % 134.53/19.96 % (866601)Peak memory usage: 145 MB % 134.53/19.96 % (866601)Instructions burned: 4921 (million) % 134.53/19.96 % (866755)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=3725165816:i=4629:av=off:gsp=on_2868 on theBenchmark for (2868ds/4629Mi) % 134.53/19.96 % (866756)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=388281415:i=1258:av=off_2868 on theBenchmark for (2868ds/1258Mi) % 134.53/19.96 % (866755)Refutation not found, incomplete strategy % 134.53/19.96 % (866755)------------------------------ % 134.53/19.96 % (866755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.53/19.96 % (866755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.53/19.96 % (866755)CaDiCaL version: 2.1.3 % 134.53/19.96 % (866755)Termination reason: Refutation not found, incomplete strategy % 134.53/19.96 % (866755)Time elapsed: 0.355 s % 170.03/24.82 % (866755)Peak memory usage: 130 MB % 170.03/24.82 % (866755)Instructions burned: 893 (million) % 170.03/24.82 % (866755)------------------------------ % 170.03/24.82 % (866755)------------------------------ % 170.03/24.82 % (866860)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=996989691:i=7343:av=off:ss=included_2862 on theBenchmark for (2862ds/7343Mi) % 170.03/24.82 % (866605)Instruction limit reached! % 170.03/24.82 % (866605)------------------------------ % 170.03/24.82 % (866605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.03/24.82 % (866605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.03/24.82 % (866605)CaDiCaL version: 2.1.3 % 170.03/24.82 % (866605)Termination reason: Instruction limit % 170.03/24.82 % (866605)Termination phase: Saturation % 170.03/24.82 % (866605)Time elapsed: 1.297 s % 170.03/24.82 % (866605)Peak memory usage: 137 MB % 170.03/24.82 % (866605)Instructions burned: 2084 (million) % 170.03/24.82 % (866862)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1864527062:i=1325:sd=2:ss=axioms:sgt=16_2861 on theBenchmark for (2861ds/1325Mi) % 170.03/24.82 % (866756)Instruction limit reached! % 170.03/24.82 % (866756)------------------------------ % 170.03/24.82 % (866756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.03/24.82 % (866756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.03/24.82 % (866756)CaDiCaL version: 2.1.3 % 170.03/24.82 % (866756)Termination reason: Instruction limit % 170.03/24.82 % (866756)Termination phase: Saturation % 170.03/24.82 % (866756)Time elapsed: 0.742 s % 170.03/24.82 % (866756)Peak memory usage: 95 MB % 170.03/24.82 % (866756)Instructions burned: 1259 (million) % 170.03/24.82 % (866862)Refutation not found, incomplete strategy % 170.03/24.82 % (866862)------------------------------ % 170.03/24.82 % (866862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.03/24.82 % (866862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.03/24.82 % (866862)CaDiCaL version: 2.1.3 % 170.03/24.82 % (866862)Termination reason: Refutation not found, incomplete strategy % 170.03/24.82 % (866862)Time elapsed: 0.009 s % 170.03/24.82 % (866862)Peak memory usage: 88 MB % 170.03/24.82 % (866862)Instructions burned: 8 (million) % 170.03/24.82 % (866877)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=706962614:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2860 on theBenchmark for (2860ds/2646Mi) % 170.03/24.82 % (866860)Refutation not found, incomplete strategy % 170.03/24.82 % (866860)------------------------------ % 170.03/24.82 % (866860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.03/24.82 % (866860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.03/24.82 % (866860)CaDiCaL version: 2.1.3 % 170.03/24.82 % (866860)Termination reason: Refutation not found, incomplete strategy % 170.03/24.82 % (866860)Time elapsed: 0.331 s % 170.03/24.82 % (866860)Peak memory usage: 128 MB % 170.03/24.82 % (866860)Instructions burned: 902 (million) % 170.03/24.82 % (866860)------------------------------ % 170.03/24.82 % (866860)------------------------------ % 170.03/24.82 % (866862)------------------------------ % 170.03/24.82 % (866862)------------------------------ % 170.03/24.82 % (866879)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=12849068:i=1489:sd=2:ep=R:ss=axioms_2857 on theBenchmark for (2857ds/1489Mi) % 170.03/24.82 % (866880)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=2444547127:i=1503_2856 on theBenchmark for (2856ds/1503Mi) % 170.03/24.82 % (866879)Instruction limit reached! % 170.03/24.82 % (866879)------------------------------ % 170.03/24.82 % (866879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.03/24.82 % (866879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.03/24.82 % (866879)CaDiCaL version: 2.1.3 % 170.03/24.82 % (866879)Termination reason: Instruction limit % 170.03/24.82 % (866879)Termination phase: Saturation % 170.03/24.82 % (866879)Time elapsed: 0.776 s % 170.03/24.82 % (866879)Peak memory usage: 131 MB % 170.03/24.82 % (866879)Instructions burned: 1489 (million) % 170.03/24.82 % (866904)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3554587113:i=13942:kws=frequency_2848 on theBenchmark for (2848ds/13942Mi) % 170.03/24.82 % (866880)Instruction limit reached! % 170.03/24.82 % (866880)------------------------------ % 211.11/30.61 % (866880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.11/30.61 % (866880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.11/30.61 % (866880)CaDiCaL version: 2.1.3 % 211.11/30.61 % (866880)Termination reason: Instruction limit % 211.11/30.61 % (866880)Termination phase: Saturation % 211.11/30.61 % (866880)Time elapsed: 1.378 s % 211.11/30.61 % (866880)Peak memory usage: 134 MB % 211.11/30.61 % (866880)Instructions burned: 1503 (million) % 211.11/30.61 % (866919)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=1286983233:i=3604:fsr=off:er=filter_2841 on theBenchmark for (2841ds/3604Mi) % 211.11/30.61 % (866877)Instruction limit reached! % 211.11/30.61 % (866877)------------------------------ % 211.11/30.61 % (866877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.11/30.61 % (866877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.11/30.61 % (866877)CaDiCaL version: 2.1.3 % 211.11/30.61 % (866877)Termination reason: Instruction limit % 211.11/30.61 % (866877)Termination phase: Saturation % 211.11/30.61 % (866877)Time elapsed: 2.610 s % 211.11/30.61 % (866877)Peak memory usage: 144 MB % 211.11/30.61 % (866877)Instructions burned: 2646 (million) % 211.11/30.61 % (866931)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3658088476:i=1876:sd=1:ss=included:sgt=32_2832 on theBenchmark for (2832ds/1876Mi) % 211.11/30.61 % (866931)Refutation not found, incomplete strategy % 211.11/30.61 % (866931)------------------------------ % 211.11/30.61 % (866931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.11/30.61 % (866931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.11/30.61 % (866931)CaDiCaL version: 2.1.3 % 211.11/30.61 % (866931)Termination reason: Refutation not found, incomplete strategy % 211.11/30.61 % (866931)Time elapsed: 0.904 s % 211.11/30.61 % (866931)Peak memory usage: 127 MB % 211.11/30.61 % (866931)Instructions burned: 863 (million) % 211.11/30.61 % (866919)Instruction limit reached! % 211.11/30.61 % (866919)------------------------------ % 211.11/30.61 % (866919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.11/30.61 % (866919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.11/30.61 % (866919)CaDiCaL version: 2.1.3 % 211.11/30.61 % (866919)Termination reason: Instruction limit % 211.11/30.61 % (866919)Termination phase: Saturation % 211.11/30.61 % (866919)Time elapsed: 2.074 s % 211.11/30.61 % (866919)Peak memory usage: 149 MB % 211.11/30.61 % (866919)Instructions burned: 3606 (million) % 211.11/30.61 % (866931)------------------------------ % 211.11/30.61 % (866931)------------------------------ % 211.11/30.61 % (866941)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2124641467:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2819 on theBenchmark for (2819ds/1932Mi) % 211.11/30.61 % (866942)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=780236555:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2817 on theBenchmark for (2817ds/1980Mi) % 211.11/30.61 % (866941)Refutation not found, incomplete strategy % 211.11/30.61 % (866941)------------------------------ % 211.11/30.61 % (866941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.11/30.61 % (866941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.11/30.61 % (866941)CaDiCaL version: 2.1.3 % 211.11/30.61 % (866941)Termination reason: Refutation not found, incomplete strategy % 211.11/30.61 % (866941)Time elapsed: 0.517 s % 211.11/30.61 % (866941)Peak memory usage: 128 MB % 211.11/30.61 % (866941)Instructions burned: 863 (million) % 211.11/30.61 % (866941)------------------------------ % 211.11/30.61 % (866941)------------------------------ % 211.11/30.61 % (866591)Instruction limit reached! % 211.11/30.61 % (866591)------------------------------ % 211.11/30.61 % (866591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.11/30.61 % (866591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.11/30.61 % (866591)CaDiCaL version: 2.1.3 % 211.11/30.61 % (866591)Termination reason: Instruction limit % 211.11/30.61 % (866591)Termination phase: Saturation % 211.11/30.61 % (866591)Time elapsed: 10.879 s % 211.11/30.61 % (866591)Peak memory usage: 213 MB % 211.11/30.61 % (866591)Instructions burned: 16411 (million) % 245.90/35.56 % (866948)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=1322954464:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2809 on theBenchmark for (2809ds/3902Mi) % 245.90/35.56 % (866949)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=643110953:avsq=on:i=3916:aac=none:amm=off_2808 on theBenchmark for (2808ds/3916Mi) % 245.90/35.56 % (866948)Refutation not found, incomplete strategy % 245.90/35.56 % (866948)------------------------------ % 245.90/35.56 % (866948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.90/35.56 % (866948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.90/35.56 % (866948)CaDiCaL version: 2.1.3 % 245.90/35.56 % (866948)Termination reason: Refutation not found, incomplete strategy % 245.90/35.56 % (866948)Time elapsed: 0.450 s % 245.90/35.56 % (866948)Peak memory usage: 129 MB % 245.90/35.56 % (866948)Instructions burned: 916 (million) % 245.90/35.56 % (866948)------------------------------ % 245.90/35.56 % (866948)------------------------------ % 245.90/35.56 % (866956)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=655292964:cond=on:i=3940:av=off:er=known_2801 on theBenchmark for (2801ds/3940Mi) % 245.90/35.56 % (866942)Instruction limit reached! % 245.90/35.56 % (866942)------------------------------ % 245.90/35.56 % (866942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.90/35.56 % (866942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.90/35.56 % (866942)CaDiCaL version: 2.1.3 % 245.90/35.56 % (866942)Termination reason: Instruction limit % 245.90/35.56 % (866942)Termination phase: Saturation % 245.90/35.56 % (866942)Time elapsed: 2.045 s % 245.90/35.56 % (866942)Peak memory usage: 138 MB % 245.90/35.56 % (866942)Instructions burned: 1980 (million) % 245.90/35.56 % (866959)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=402294936:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2795 on theBenchmark for (2795ds/3980Mi) % 245.90/35.56 % (866949)Instruction limit reached! % 245.90/35.56 % (866949)------------------------------ % 245.90/35.56 % (866949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.90/35.56 % (866949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.90/35.56 % (866949)CaDiCaL version: 2.1.3 % 245.90/35.56 % (866949)Termination reason: Instruction limit % 245.90/35.56 % (866949)Termination phase: Saturation % 245.90/35.56 % (866949)Time elapsed: 3.478 s % 245.90/35.56 % (866949)Peak memory usage: 106 MB % 245.90/35.56 % (866949)Instructions burned: 3917 (million) % 245.90/35.56 % (866959)Instruction limit reached! % 245.90/35.56 % (866959)------------------------------ % 245.90/35.56 % (866959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.90/35.56 % (866959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.90/35.56 % (866959)CaDiCaL version: 2.1.3 % 245.90/35.56 % (866959)Termination reason: Instruction limit % 245.90/35.56 % (866959)Termination phase: Saturation % 245.90/35.56 % (866959)Time elapsed: 2.365 s % 245.90/35.56 % (866959)Peak memory usage: 154 MB % 245.90/35.56 % (866959)Instructions burned: 3981 (million) % 245.90/35.56 % (866970)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=2798415779:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2771 on theBenchmark for (2771ds/2087Mi) % 245.90/35.56 % (866972)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=4178383423:cts=off:cond=on:i=4272:bs=on:fsd=on_2770 on theBenchmark for (2770ds/4272Mi) % 245.90/35.56 % (866956)Instruction limit reached! % 245.90/35.56 % (866956)------------------------------ % 245.90/35.56 % (866956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.90/35.56 % (866956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.90/35.56 % (866956)CaDiCaL version: 2.1.3 % 245.90/35.56 % (866956)Termination reason: Instruction limit % 245.90/35.56 % (866956)Termination phase: Saturation % 245.90/35.56 % (866956)Time elapsed: 3.716 s % 245.90/35.56 % (866956)Peak memory usage: 150 MB % 245.90/35.56 % (866956)Instructions burned: 3940 (million) % 245.90/35.56 % (866975)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=320Terminated %------------------------------------------------------------------------------