%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC157-1 : TPTP v9.3.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:02:42 PM UTC 2026 % Result : Timeout 300.05s 43.33s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWC157-1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.16/0.44 % Computer : n014.cluster.edu % 0.16/0.44 % Model : x86_64 x86_64 % 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.44 % Memory : 8046.5625MB % 0.16/0.44 % OS : Linux 6.8.0-71-generic % 0.16/0.44 % CPULimit : 300 % 0.16/0.44 % WCLimit : 300 % 0.16/0.44 % DateTime : Mon Sep 28 08:12:16 UTC 2026 % 0.16/0.44 % CPUTime : % 0.16/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.24/0.50 Running first-order theorem proving % 0.24/0.50 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 % 18.75/3.79 % (1624399)Input is clausal, will run a generic CNF schedule. % 18.75/3.79 % (1624410)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=476727584:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 18.75/3.79 % (1624414)dis-21_1_sil=8000:lcm=predicate:random_seed=1675276664: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) % 18.75/3.79 % (1624414)Instruction limit reached! % 18.75/3.79 % (1624414)------------------------------ % 18.75/3.79 % (1624414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.75/3.79 % (1624414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.75/3.79 % (1624414)CaDiCaL version: 2.1.3 % 18.75/3.79 % (1624414)Termination reason: Instruction limit % 18.75/3.79 % (1624414)Termination phase: Saturation % 18.75/3.79 % (1624414)Time elapsed: 0.065 s % 18.75/3.79 % (1624414)Peak memory usage: 89 MB % 18.75/3.79 % (1624414)Instructions burned: 118 (million) % 18.75/3.79 % (1624411)lrs+10_1_sil=8000:sp=occurrence:random_seed=864905268:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 18.75/3.79 % (1624413)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1616154403:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 18.75/3.79 % (1624412)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3909441704:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 18.75/3.79 % (1624409)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=22341566:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 18.75/3.79 % (1624408)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=4257346226:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 18.75/3.79 % (1624411)Instruction limit reached! % 18.75/3.79 % (1624411)------------------------------ % 18.75/3.79 % (1624411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.75/3.79 % (1624411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.75/3.79 % (1624411)CaDiCaL version: 2.1.3 % 18.75/3.79 % (1624411)Termination reason: Instruction limit % 18.75/3.79 % (1624411)Termination phase: Saturation % 18.75/3.79 % (1624411)Time elapsed: 0.093 s % 18.75/3.79 % (1624411)Peak memory usage: 90 MB % 18.75/3.79 % (1624411)Instructions burned: 107 (million) % 18.75/3.79 % (1624412)Instruction limit reached! % 18.75/3.79 % (1624412)------------------------------ % 18.75/3.79 % (1624412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.75/3.79 % (1624412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.75/3.79 % (1624412)CaDiCaL version: 2.1.3 % 18.75/3.79 % (1624412)Termination reason: Instruction limit % 18.75/3.79 % (1624412)Termination phase: Saturation % 18.75/3.79 % (1624412)Time elapsed: 0.113 s % 18.75/3.79 % (1624412)Peak memory usage: 89 MB % 18.75/3.79 % (1624412)Instructions burned: 114 (million) % 18.75/3.79 % (1624413)Instruction limit reached! % 18.75/3.79 % (1624413)------------------------------ % 18.75/3.79 % (1624413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.75/3.79 % (1624413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.75/3.79 % (1624413)CaDiCaL version: 2.1.3 % 18.75/3.79 % (1624413)Termination reason: Instruction limit % 18.75/3.79 % (1624413)Termination phase: Saturation % 18.75/3.79 % (1624413)Time elapsed: 0.197 s % 18.75/3.79 % (1624413)Peak memory usage: 90 MB % 18.75/3.79 % (1624413)Instructions burned: 181 (million) % 18.75/3.79 % (1624418)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=367838972:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 18.75/3.79 % (1624424)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1192370652:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi) % 18.75/3.79 % (1624426)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2597537842:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi) % 18.75/3.79 % (1624418)Instruction limit reached! % 18.75/3.79 % (1624418)------------------------------ % 18.75/3.79 % (1624418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.59/6.36 % (1624418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.59/6.36 % (1624418)CaDiCaL version: 2.1.3 % 37.59/6.36 % (1624418)Termination reason: Instruction limit % 37.59/6.36 % (1624418)Termination phase: Saturation % 37.59/6.36 % (1624418)Time elapsed: 0.151 s % 37.59/6.36 % (1624418)Peak memory usage: 90 MB % 37.59/6.36 % (1624418)Instructions burned: 144 (million) % 37.59/6.36 % (1624428)lrs+10_64_to=lpo:sil=8000:random_seed=3096901410:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 37.59/6.36 % (1624424)Instruction limit reached! % 37.59/6.36 % (1624424)------------------------------ % 37.59/6.36 % (1624424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.59/6.36 % (1624424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.59/6.36 % (1624424)CaDiCaL version: 2.1.3 % 37.59/6.36 % (1624424)Termination reason: Instruction limit % 37.59/6.36 % (1624424)Termination phase: Saturation % 37.59/6.36 % (1624424)Time elapsed: 0.177 s % 37.59/6.36 % (1624424)Peak memory usage: 91 MB % 37.59/6.36 % (1624424)Instructions burned: 189 (million) % 37.59/6.36 % (1624428)Instruction limit reached! % 37.59/6.36 % (1624428)------------------------------ % 37.59/6.36 % (1624428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.59/6.36 % (1624428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.59/6.36 % (1624428)CaDiCaL version: 2.1.3 % 37.59/6.36 % (1624428)Termination reason: Instruction limit % 37.59/6.36 % (1624428)Termination phase: Saturation % 37.59/6.36 % (1624428)Time elapsed: 0.113 s % 37.59/6.36 % (1624428)Peak memory usage: 90 MB % 37.59/6.36 % (1624428)Instructions burned: 126 (million) % 37.59/6.36 % (1624433)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2362175304:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi) % 37.59/6.36 % (1624426)Instruction limit reached! % 37.59/6.36 % (1624426)------------------------------ % 37.59/6.36 % (1624426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.59/6.36 % (1624426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.59/6.36 % (1624426)CaDiCaL version: 2.1.3 % 37.59/6.36 % (1624426)Termination reason: Instruction limit % 37.59/6.36 % (1624426)Termination phase: Saturation % 37.59/6.36 % (1624426)Time elapsed: 0.239 s % 37.59/6.36 % (1624426)Peak memory usage: 90 MB % 37.59/6.36 % (1624426)Instructions burned: 220 (million) % 37.59/6.36 % (1624435)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=290763582:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi) % 37.59/6.36 % (1624436)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1701658975:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi) % 37.59/6.36 % (1624433)Instruction limit reached! % 37.59/6.36 % (1624433)------------------------------ % 37.59/6.36 % (1624433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.59/6.36 % (1624433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.59/6.36 % (1624433)CaDiCaL version: 2.1.3 % 37.59/6.36 % (1624433)Termination reason: Instruction limit % 37.59/6.36 % (1624433)Termination phase: Saturation % 37.59/6.36 % (1624433)Time elapsed: 0.202 s % 37.59/6.36 % (1624433)Peak memory usage: 90 MB % 37.59/6.36 % (1624433)Instructions burned: 195 (million) % 37.59/6.36 % (1624438)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=2243370676:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi) % 37.59/6.36 % (1624435)Instruction limit reached! % 37.59/6.36 % (1624435)------------------------------ % 37.59/6.36 % (1624435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.59/6.36 % (1624435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.59/6.36 % (1624435)CaDiCaL version: 2.1.3 % 37.59/6.36 % (1624435)Termination reason: Instruction limit % 37.59/6.36 % (1624435)Termination phase: Saturation % 37.59/6.36 % (1624435)Time elapsed: 0.158 s % 37.59/6.36 % (1624435)Peak memory usage: 91 MB % 37.59/6.36 % (1624435)Instructions burned: 159 (million) % 37.59/6.36 % (1624438)Instruction limit reached! % 37.59/6.36 % (1624438)------------------------------ % 37.59/6.36 % (1624438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.59/6.36 % (1624438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.59/6.36 % (1624438)CaDiCaL version: 2.1.3 % 73.86/11.40 % (1624438)Termination reason: Instruction limit % 73.86/11.40 % (1624438)Termination phase: Saturation % 73.86/11.40 % (1624438)Time elapsed: 0.091 s % 73.86/11.40 % (1624438)Peak memory usage: 90 MB % 73.86/11.40 % (1624438)Instructions burned: 107 (million) % 73.86/11.40 % (1624441)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1788608152:i=107_2988 on theBenchmark for (2988ds/107Mi) % 73.86/11.40 % (1624444)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1960992723:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi) % 73.86/11.40 % (1624441)Instruction limit reached! % 73.86/11.40 % (1624441)------------------------------ % 73.86/11.40 % (1624441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.86/11.40 % (1624441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.86/11.40 % (1624441)CaDiCaL version: 2.1.3 % 73.86/11.40 % (1624441)Termination reason: Instruction limit % 73.86/11.40 % (1624441)Termination phase: Saturation % 73.86/11.40 % (1624441)Time elapsed: 0.106 s % 73.86/11.40 % (1624441)Peak memory usage: 90 MB % 73.86/11.40 % (1624441)Instructions burned: 108 (million) % 73.86/11.40 % (1624445)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1559190138:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi) % 73.86/11.40 % (1624444)Instruction limit reached! % 73.86/11.40 % (1624444)------------------------------ % 73.86/11.40 % (1624444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.86/11.40 % (1624444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.86/11.40 % (1624444)CaDiCaL version: 2.1.3 % 73.86/11.40 % (1624444)Termination reason: Instruction limit % 73.86/11.40 % (1624444)Termination phase: Saturation % 73.86/11.40 % (1624444)Time elapsed: 0.248 s % 73.86/11.40 % (1624444)Peak memory usage: 90 MB % 73.86/11.40 % (1624444)Instructions burned: 242 (million) % 73.86/11.40 % (1624449)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3662072575:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi) % 73.86/11.40 % (1624449)Instruction limit reached! % 73.86/11.40 % (1624449)------------------------------ % 73.86/11.40 % (1624449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.86/11.40 % (1624449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.86/11.40 % (1624449)CaDiCaL version: 2.1.3 % 73.86/11.40 % (1624449)Termination reason: Instruction limit % 73.86/11.40 % (1624449)Termination phase: Saturation % 73.86/11.40 % (1624449)Time elapsed: 0.096 s % 73.86/11.40 % (1624449)Peak memory usage: 89 MB % 73.86/11.40 % (1624449)Instructions burned: 134 (million) % 73.86/11.40 % (1624451)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4231444054:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi) % 73.86/11.40 % (1624453)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2124733566:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi) % 73.86/11.40 % (1624453)Instruction limit reached! % 73.86/11.40 % (1624453)------------------------------ % 73.86/11.40 % (1624453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.86/11.40 % (1624453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.86/11.40 % (1624453)CaDiCaL version: 2.1.3 % 73.86/11.40 % (1624453)Termination reason: Instruction limit % 73.86/11.40 % (1624453)Termination phase: Saturation % 73.86/11.40 % (1624453)Time elapsed: 0.188 s % 73.86/11.40 % (1624453)Peak memory usage: 93 MB % 73.86/11.40 % (1624453)Instructions burned: 191 (million) % 73.86/11.40 % (1624451)Instruction limit reached! % 73.86/11.40 % (1624451)------------------------------ % 73.86/11.40 % (1624451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.86/11.40 % (1624451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.86/11.40 % (1624451)CaDiCaL version: 2.1.3 % 73.86/11.40 % (1624451)Termination reason: Instruction limit % 73.86/11.40 % (1624451)Termination phase: Saturation % 73.86/11.40 % (1624451)Time elapsed: 0.438 s % 73.86/11.40 % (1624451)Peak memory usage: 102 MB % 73.86/11.40 % (1624451)Instructions burned: 499 (million) % 73.86/11.40 % (1624457)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1766204245:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi) % 73.86/11.40 % (1624458)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=928991144:cond=on:i=156:bs=on:gtg=exists_all:er=known_2975 on theBenchmark for (2975ds/156Mi) % 93.33/14.17 % (1624457)Instruction limit reached! % 93.33/14.17 % (1624457)------------------------------ % 93.33/14.17 % (1624457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.33/14.17 % (1624457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.33/14.17 % (1624457)CaDiCaL version: 2.1.3 % 93.33/14.17 % (1624457)Termination reason: Instruction limit % 93.33/14.17 % (1624457)Termination phase: Saturation % 93.33/14.17 % (1624457)Time elapsed: 0.235 s % 93.33/14.17 % (1624457)Peak memory usage: 92 MB % 93.33/14.17 % (1624457)Instructions burned: 264 (million) % 93.33/14.17 % (1624458)Instruction limit reached! % 93.33/14.17 % (1624458)------------------------------ % 93.33/14.17 % (1624458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.33/14.17 % (1624458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.33/14.17 % (1624458)CaDiCaL version: 2.1.3 % 93.33/14.17 % (1624458)Termination reason: Instruction limit % 93.33/14.17 % (1624458)Termination phase: Saturation % 93.33/14.17 % (1624458)Time elapsed: 0.162 s % 93.33/14.17 % (1624458)Peak memory usage: 90 MB % 93.33/14.17 % (1624458)Instructions burned: 156 (million) % 93.33/14.17 % (1624464)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=789715778:i=537:av=off:ss=included_2971 on theBenchmark for (2971ds/537Mi) % 93.33/14.17 % (1624463)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=2925412101:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi) % 93.33/14.17 % (1624464)Instruction limit reached! % 93.33/14.17 % (1624464)------------------------------ % 93.33/14.17 % (1624464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.33/14.17 % (1624464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.33/14.17 % (1624464)CaDiCaL version: 2.1.3 % 93.33/14.17 % (1624464)Termination reason: Instruction limit % 93.33/14.17 % (1624464)Termination phase: Saturation % 93.33/14.17 % (1624464)Time elapsed: 0.478 s % 93.33/14.17 % (1624464)Peak memory usage: 92 MB % 93.33/14.17 % (1624464)Instructions burned: 537 (million) % 93.33/14.17 % (1624471)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=823930473:i=180:bd=preordered:av=off_2963 on theBenchmark for (2963ds/180Mi) % 93.33/14.17 % (1624471)Instruction limit reached! % 93.33/14.17 % (1624471)------------------------------ % 93.33/14.17 % (1624471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.33/14.17 % (1624471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.33/14.17 % (1624471)CaDiCaL version: 2.1.3 % 93.33/14.17 % (1624471)Termination reason: Instruction limit % 93.33/14.17 % (1624471)Termination phase: Saturation % 93.33/14.17 % (1624471)Time elapsed: 0.164 s % 93.33/14.17 % (1624471)Peak memory usage: 91 MB % 93.33/14.17 % (1624471)Instructions burned: 181 (million) % 93.33/14.17 % (1624473)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=617582146:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2958 on theBenchmark for (2958ds/10307Mi) % 93.33/14.17 % (1624436)Instruction limit reached! % 93.33/14.17 % (1624436)------------------------------ % 93.33/14.17 % (1624436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.33/14.17 % (1624436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.33/14.17 % (1624436)CaDiCaL version: 2.1.3 % 93.33/14.17 % (1624436)Termination reason: Instruction limit % 93.33/14.17 % (1624436)Termination phase: Saturation % 93.33/14.17 % (1624436)Time elapsed: 3.534 s % 93.33/14.17 % (1624436)Peak memory usage: 153 MB % 93.33/14.17 % (1624436)Instructions burned: 3395 (million) % 93.33/14.17 % (1624475)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=3180461964:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi) % 93.33/14.17 % (1624475)Instruction limit reached! % 93.33/14.17 % (1624475)------------------------------ % 93.33/14.17 % (1624475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.33/14.17 % (1624475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.33/14.17 % (1624475)CaDiCaL version: 2.1.3 % 93.33/14.17 % (1624475)Termination reason: Instruction limit % 93.33/14.17 % (1624475)Termination phase: Saturation % 126.43/18.83 % (1624475)Time elapsed: 0.361 s % 126.43/18.83 % (1624475)Peak memory usage: 91 MB % 126.43/18.83 % (1624475)Instructions burned: 413 (million) % 126.43/18.83 % (1624477)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=1462475561:s2pl=no:i=8478:s2at=4:nm=6_2946 on theBenchmark for (2946ds/8478Mi) % 126.43/18.83 % (1624463)Instruction limit reached! % 126.43/18.83 % (1624463)------------------------------ % 126.43/18.83 % (1624463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.43/18.83 % (1624463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.43/18.83 % (1624463)CaDiCaL version: 2.1.3 % 126.43/18.83 % (1624463)Termination reason: Instruction limit % 126.43/18.83 % (1624463)Termination phase: Saturation % 126.43/18.83 % (1624463)Time elapsed: 3.246 s % 126.43/18.83 % (1624463)Peak memory usage: 150 MB % 126.43/18.83 % (1624463)Instructions burned: 3257 (million) % 126.43/18.83 % (1624479)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=1760150807:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2935 on theBenchmark for (2935ds/303Mi) % 126.43/18.83 % (1624445)Instruction limit reached! % 126.43/18.83 % (1624445)------------------------------ % 126.43/18.83 % (1624445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.43/18.83 % (1624445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.43/18.83 % (1624445)CaDiCaL version: 2.1.3 % 126.43/18.83 % (1624445)Termination reason: Instruction limit % 126.43/18.83 % (1624445)Termination phase: Saturation % 126.43/18.83 % (1624445)Time elapsed: 5.126 s % 126.43/18.83 % (1624445)Peak memory usage: 160 MB % 126.43/18.83 % (1624445)Instructions burned: 5208 (million) % 126.43/18.83 % (1624479)Instruction limit reached! % 126.43/18.83 % (1624479)------------------------------ % 126.43/18.83 % (1624479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.43/18.83 % (1624479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.43/18.83 % (1624479)CaDiCaL version: 2.1.3 % 126.43/18.83 % (1624479)Termination reason: Instruction limit % 126.43/18.83 % (1624479)Termination phase: Saturation % 126.43/18.83 % (1624479)Time elapsed: 0.281 s % 126.43/18.83 % (1624479)Peak memory usage: 95 MB % 126.43/18.83 % (1624479)Instructions burned: 304 (million) % 126.43/18.83 % (1624482)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4145434386:st=4:i=720:sd=3:fsr=off:ss=axioms_2932 on theBenchmark for (2932ds/720Mi) % 126.43/18.83 % (1624484)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3332362223:i=598:bs=on:bd=preordered:av=off:ss=axioms_2930 on theBenchmark for (2930ds/598Mi) % 126.43/18.83 % (1624482)Instruction limit reached! % 126.43/18.83 % (1624482)------------------------------ % 126.43/18.83 % (1624482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.43/18.83 % (1624482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.43/18.83 % (1624482)CaDiCaL version: 2.1.3 % 126.43/18.83 % (1624482)Termination reason: Instruction limit % 126.43/18.83 % (1624482)Termination phase: Saturation % 126.43/18.83 % (1624482)Time elapsed: 0.630 s % 126.43/18.83 % (1624482)Peak memory usage: 100 MB % 126.43/18.83 % (1624482)Instructions burned: 720 (million) % 126.43/18.83 % (1624484)Instruction limit reached! % 126.43/18.83 % (1624484)------------------------------ % 126.43/18.83 % (1624484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.43/18.83 % (1624484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.43/18.83 % (1624484)CaDiCaL version: 2.1.3 % 126.43/18.83 % (1624484)Termination reason: Instruction limit % 126.43/18.83 % (1624484)Termination phase: Saturation % 126.43/18.83 % (1624484)Time elapsed: 0.562 s % 126.43/18.83 % (1624484)Peak memory usage: 96 MB % 126.43/18.83 % (1624484)Instructions burned: 598 (million) % 126.43/18.83 % (1624489)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2341900050:i=2989:sd=3:ss=axioms:sgt=60_2923 on theBenchmark for (2923ds/2989Mi) % 126.43/18.83 % (1624490)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=3973689348:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2921 on theBenchmark for (2921ds/1997Mi) % 126.43/18.83 % (1624490)Instruction limit reached! % 126.43/18.83 % (1624490)------------------------------ % 174.66/25.60 % (1624490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.66/25.60 % (1624490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.66/25.60 % (1624490)CaDiCaL version: 2.1.3 % 174.66/25.60 % (1624490)Termination reason: Instruction limit % 174.66/25.60 % (1624490)Termination phase: Saturation % 174.66/25.60 % (1624490)Time elapsed: 2.211 s % 174.66/25.60 % (1624490)Peak memory usage: 138 MB % 174.66/25.60 % (1624490)Instructions burned: 1997 (million) % 174.66/25.60 % (1624499)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=1933181767:i=2088:bd=preordered:av=off_2896 on theBenchmark for (2896ds/2088Mi) % 174.66/25.60 % (1624489)Instruction limit reached! % 174.66/25.60 % (1624489)------------------------------ % 174.66/25.60 % (1624489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.66/25.60 % (1624489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.66/25.60 % (1624489)CaDiCaL version: 2.1.3 % 174.66/25.60 % (1624489)Termination reason: Instruction limit % 174.66/25.60 % (1624489)Termination phase: Saturation % 174.66/25.60 % (1624489)Time elapsed: 3.180 s % 174.66/25.60 % (1624489)Peak memory usage: 148 MB % 174.66/25.60 % (1624489)Instructions burned: 2990 (million) % 174.66/25.60 % (1624501)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=42808143:i=1098:nicw=on_2888 on theBenchmark for (2888ds/1098Mi) % 174.66/25.60 % (1624501)Instruction limit reached! % 174.66/25.60 % (1624501)------------------------------ % 174.66/25.60 % (1624501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.66/25.60 % (1624501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.66/25.60 % (1624501)CaDiCaL version: 2.1.3 % 174.66/25.60 % (1624501)Termination reason: Instruction limit % 174.66/25.60 % (1624501)Termination phase: Saturation % 174.66/25.60 % (1624501)Time elapsed: 0.935 s % 174.66/25.60 % (1624501)Peak memory usage: 123 MB % 174.66/25.60 % (1624501)Instructions burned: 1099 (million) % 174.66/25.60 % (1624477)Instruction limit reached! % 174.66/25.60 % (1624477)------------------------------ % 174.66/25.60 % (1624477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.66/25.60 % (1624477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.66/25.60 % (1624477)CaDiCaL version: 2.1.3 % 174.66/25.60 % (1624477)Termination reason: Instruction limit % 174.66/25.60 % (1624477)Termination phase: Saturation % 174.66/25.60 % (1624477)Time elapsed: 6.772 s % 174.66/25.60 % (1624477)Peak memory usage: 189 MB % 174.66/25.60 % (1624477)Instructions burned: 8478 (million) % 174.66/25.60 % (1624506)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3140671312:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2876 on theBenchmark for (2876ds/2942Mi) % 174.66/25.60 % (1624505)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1715514403:i=433:bd=preordered_2876 on theBenchmark for (2876ds/433Mi) % 174.66/25.60 % (1624499)Instruction limit reached! % 174.66/25.60 % (1624499)------------------------------ % 174.66/25.60 % (1624499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.66/25.60 % (1624499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.66/25.60 % (1624499)CaDiCaL version: 2.1.3 % 174.66/25.60 % (1624499)Termination reason: Instruction limit % 174.66/25.60 % (1624499)Termination phase: Saturation % 174.66/25.60 % (1624499)Time elapsed: 2.106 s % 174.66/25.60 % (1624499)Peak memory usage: 138 MB % 174.66/25.60 % (1624499)Instructions burned: 2088 (million) % 174.66/25.60 % (1624511)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=69429637:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2872 on theBenchmark for (2872ds/6922Mi) % 174.66/25.60 % (1624505)Instruction limit reached! % 174.66/25.60 % (1624505)------------------------------ % 174.66/25.60 % (1624505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.66/25.60 % (1624505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.66/25.60 % (1624505)CaDiCaL version: 2.1.3 % 174.66/25.60 % (1624505)Termination reason: Instruction limit % 174.66/25.60 % (1624505)Termination phase: Saturation % 174.66/25.60 % (1624505)Time elapsed: 0.436 s % 174.66/25.60 % (1624505)Peak memory usage: 93 MB % 174.66/25.60 % (1624505)Instructions burned: 433 (million) % 199.07/29.13 % (1624473)Instruction limit reached! % 199.07/29.13 % (1624473)------------------------------ % 199.07/29.13 % (1624473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.07/29.13 % (1624473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.07/29.13 % (1624473)CaDiCaL version: 2.1.3 % 199.07/29.13 % (1624473)Termination reason: Instruction limit % 199.07/29.13 % (1624473)Termination phase: Saturation % 199.07/29.13 % (1624473)Time elapsed: 8.789 s % 199.07/29.13 % (1624473)Peak memory usage: 149 MB % 199.07/29.13 % (1624473)Instructions burned: 10307 (million) % 199.07/29.13 % (1624514)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=2050835971:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2867 on theBenchmark for (2867ds/4123Mi) % 199.07/29.13 % (1624513)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=918501641:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2868 on theBenchmark for (2868ds/596Mi) % 199.07/29.13 % (1624513)Instruction limit reached! % 199.07/29.13 % (1624513)------------------------------ % 199.07/29.13 % (1624513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.07/29.13 % (1624513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.07/29.13 % (1624513)CaDiCaL version: 2.1.3 % 199.07/29.13 % (1624513)Termination reason: Instruction limit % 199.07/29.13 % (1624513)Termination phase: Saturation % 199.07/29.13 % (1624513)Time elapsed: 0.505 s % 199.07/29.13 % (1624513)Peak memory usage: 109 MB % 199.07/29.13 % (1624513)Instructions burned: 596 (million) % 199.07/29.13 % (1624519)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=962834107:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2861 on theBenchmark for (2861ds/16411Mi) % 199.07/29.13 % (1624514)Instruction limit reached! % 199.07/29.13 % (1624514)------------------------------ % 199.07/29.13 % (1624514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.07/29.13 % (1624514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.07/29.13 % (1624514)CaDiCaL version: 2.1.3 % 199.07/29.13 % (1624514)Termination reason: Instruction limit % 199.07/29.13 % (1624514)Termination phase: Saturation % 199.07/29.13 % (1624514)Time elapsed: 2.054 s % 199.07/29.13 % (1624514)Peak memory usage: 166 MB % 199.07/29.13 % (1624514)Instructions burned: 4125 (million) % 199.07/29.13 % (1624506)Instruction limit reached! % 199.07/29.13 % (1624506)------------------------------ % 199.07/29.13 % (1624506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.07/29.13 % (1624506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.07/29.13 % (1624506)CaDiCaL version: 2.1.3 % 199.07/29.13 % (1624506)Termination reason: Instruction limit % 199.07/29.13 % (1624506)Termination phase: Saturation % 199.07/29.13 % (1624506)Time elapsed: 3.026 s % 199.07/29.13 % (1624506)Peak memory usage: 146 MB % 199.07/29.13 % (1624506)Instructions burned: 2942 (million) % 199.07/29.13 % (1624525)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2062520245:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2845 on theBenchmark for (2845ds/1670Mi) % 199.07/29.13 % (1624527)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=3869259712:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2843 on theBenchmark for (2843ds/1722Mi) % 199.07/29.13 % (1624525)Instruction limit reached! % 199.07/29.13 % (1624525)------------------------------ % 199.07/29.13 % (1624525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.07/29.13 % (1624525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.07/29.13 % (1624525)CaDiCaL version: 2.1.3 % 199.07/29.13 % (1624525)Termination reason: Instruction limit % 199.07/29.13 % (1624525)Termination phase: Saturation % 199.07/29.13 % (1624525)Time elapsed: 0.951 s % 199.07/29.13 % (1624525)Peak memory usage: 137 MB % 199.07/29.13 % (1624525)Instructions burned: 1671 (million) % 199.07/29.13 % (1624532)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=1331849337:cts=off:cond=on:i=9530:bs=on:fsd=on_2833 on theBenchmark for (2833ds/9530Mi) % 199.07/29.13 % (1624527)Instruction limit reached! % 199.07/29.13 % (1624527)------------------------------ % 234.60/34.09 % (1624527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.60/34.09 % (1624527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.60/34.09 % (1624527)CaDiCaL version: 2.1.3 % 234.60/34.09 % (1624527)Termination reason: Instruction limit % 234.60/34.09 % (1624527)Termination phase: Saturation % 234.60/34.09 % (1624527)Time elapsed: 1.784 s % 234.60/34.09 % (1624527)Peak memory usage: 133 MB % 234.60/34.09 % (1624527)Instructions burned: 1723 (million) % 234.60/34.09 % (1624536)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2568499340:st=2:i=4495:sd=10:ss=included_2822 on theBenchmark for (2822ds/4495Mi) % 234.60/34.09 % (1624511)Instruction limit reached! % 234.60/34.09 % (1624511)------------------------------ % 234.60/34.09 % (1624511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.60/34.09 % (1624511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.60/34.09 % (1624511)CaDiCaL version: 2.1.3 % 234.60/34.09 % (1624511)Termination reason: Instruction limit % 234.60/34.09 % (1624511)Termination phase: Saturation % 234.60/34.09 % (1624511)Time elapsed: 6.432 s % 234.60/34.09 % (1624511)Peak memory usage: 195 MB % 234.60/34.09 % (1624511)Instructions burned: 6923 (million) % 234.60/34.09 % (1624541)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=3244208979:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2805 on theBenchmark for (2805ds/4920Mi) % 234.60/34.09 % (1624532)Instruction limit reached! % 234.60/34.09 % (1624532)------------------------------ % 234.60/34.09 % (1624532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.60/34.09 % (1624532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.60/34.09 % (1624532)CaDiCaL version: 2.1.3 % 234.60/34.09 % (1624532)Termination reason: Instruction limit % 234.60/34.09 % (1624532)Termination phase: Saturation % 234.60/34.09 % (1624532)Time elapsed: 4.402 s % 234.60/34.09 % (1624532)Peak memory usage: 152 MB % 234.60/34.09 % (1624532)Instructions burned: 9532 (million) % 234.60/34.09 % (1624544)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=2883276885:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2787 on theBenchmark for (2787ds/2083Mi) % 234.60/34.09 % (1624536)Instruction limit reached! % 234.60/34.09 % (1624536)------------------------------ % 234.60/34.09 % (1624536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.60/34.09 % (1624536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.60/34.09 % (1624536)CaDiCaL version: 2.1.3 % 234.60/34.09 % (1624536)Termination reason: Instruction limit % 234.60/34.09 % (1624536)Termination phase: Saturation % 234.60/34.09 % (1624536)Time elapsed: 4.558 s % 234.60/34.09 % (1624536)Peak memory usage: 163 MB % 234.60/34.09 % (1624536)Instructions burned: 4497 (million) % 234.60/34.09 % (1624546)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=3437854344:i=4629:av=off:gsp=on_2773 on theBenchmark for (2773ds/4629Mi) % 234.60/34.09 % (1624544)Instruction limit reached! % 234.60/34.09 % (1624544)------------------------------ % 234.60/34.09 % (1624544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.60/34.09 % (1624544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.60/34.09 % (1624544)CaDiCaL version: 2.1.3 % 234.60/34.09 % (1624544)Termination reason: Instruction limit % 234.60/34.09 % (1624544)Termination phase: Saturation % 234.60/34.09 % (1624544)Time elapsed: 1.571 s % 234.60/34.09 % (1624544)Peak memory usage: 139 MB % 234.60/34.09 % (1624544)Instructions burned: 2085 (million) % 234.60/34.09 % (1624549)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1088054072:i=1258:av=off_2769 on theBenchmark for (2769ds/1258Mi) % 234.60/34.09 % (1624549)Instruction limit reached! % 234.60/34.09 % (1624549)------------------------------ % 234.60/34.09 % (1624549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.60/34.09 % (1624549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.60/34.09 % (1624549)CaDiCaL version: 2.1.3 % 234.60/34.09 % (1624549)Termination reason: Instruction limit % 234.60/34.09 % (1624549)Termination phase: Saturation % 234.60/34.09 % (1624549)Time elapsed: 1.156 s % 234.60/34.09 % (1624549)Peak memory usage: 111 MB % 258.02/37.47 % (1624549)Instructions burned: 1259 (million) % 258.02/37.47 % (1624541)Instruction limit reached! % 258.02/37.47 % (1624541)------------------------------ % 258.02/37.47 % (1624541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.02/37.47 % (1624541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.02/37.47 % (1624541)CaDiCaL version: 2.1.3 % 258.02/37.47 % (1624541)Termination reason: Instruction limit % 258.02/37.47 % (1624541)Termination phase: Saturation % 258.02/37.47 % (1624541)Time elapsed: 4.832 s % 258.02/37.47 % (1624541)Peak memory usage: 159 MB % 258.02/37.47 % (1624541)Instructions burned: 4921 (million) % 258.02/37.47 % (1624556)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2042537922:i=7343:av=off:ss=included_2754 on theBenchmark for (2754ds/7343Mi) % 258.02/37.47 % (1624558)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3754039152:i=1325:sd=2:ss=axioms:sgt=16_2753 on theBenchmark for (2753ds/1325Mi) % 258.02/37.47 % (1624546)Instruction limit reached! % 258.02/37.47 % (1624546)------------------------------ % 258.02/37.47 % (1624546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.02/37.47 % (1624546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.02/37.47 % (1624546)CaDiCaL version: 2.1.3 % 258.02/37.47 % (1624546)Termination reason: Instruction limit % 258.02/37.47 % (1624546)Termination phase: Saturation % 258.02/37.47 % (1624546)Time elapsed: 2.431 s % 258.02/37.47 % (1624546)Peak memory usage: 164 MB % 258.02/37.47 % (1624546)Instructions burned: 4630 (million) % 258.02/37.47 % (1624564)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=2107885802:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2746 on theBenchmark for (2746ds/2646Mi) % 258.02/37.47 % (1624558)Instruction limit reached! % 258.02/37.47 % (1624558)------------------------------ % 258.02/37.47 % (1624558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.02/37.47 % (1624558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.02/37.47 % (1624558)CaDiCaL version: 2.1.3 % 258.02/37.47 % (1624558)Termination reason: Instruction limit % 258.02/37.47 % (1624558)Termination phase: Saturation % 258.02/37.47 % (1624558)Time elapsed: 1.142 s % 258.02/37.47 % (1624558)Peak memory usage: 99 MB % 258.02/37.47 % (1624558)Instructions burned: 1325 (million) % 258.02/37.47 % (1624568)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2430782056:i=1489:sd=2:ep=R:ss=axioms_2739 on theBenchmark for (2739ds/1489Mi) % 258.02/37.47 % (1624564)Instruction limit reached! % 258.02/37.47 % (1624564)------------------------------ % 258.02/37.47 % (1624564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.02/37.47 % (1624564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.02/37.47 % (1624564)CaDiCaL version: 2.1.3 % 258.02/37.47 % (1624564)Termination reason: Instruction limit % 258.02/37.47 % (1624564)Termination phase: Saturation % 258.02/37.47 % (1624564)Time elapsed: 1.487 s % 258.02/37.47 % (1624564)Peak memory usage: 142 MB % 258.02/37.47 % (1624564)Instructions burned: 2647 (million) % 258.02/37.47 % (1624570)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=3122981336:i=1503_2729 on theBenchmark for (2729ds/1503Mi) % 258.02/37.47 % (1624568)Instruction limit reached! % 258.02/37.47 % (1624568)------------------------------ % 258.02/37.47 % (1624568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.02/37.47 % (1624568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.02/37.47 % (1624568)CaDiCaL version: 2.1.3 % 258.02/37.47 % (1624568)Termination reason: Instruction limit % 258.02/37.47 % (1624568)Termination phase: Saturation % 258.02/37.47 % (1624568)Time elapsed: 1.533 s % 258.02/37.47 % (1624568)Peak memory usage: 136 MB % 258.02/37.47 % (1624568)Instructions burned: 1489 (million) % 258.02/37.47 % (1624570)Instruction limit reached! % 258.02/37.47 % (1624570)------------------------------ % 258.02/37.47 % (1624570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 258.02/37.47 % (1624570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 258.02/37.47 % (1624570)CaDiCaL version: 2.1.3 % 258.02/37.47 % (1624570)Termination reason: Instruction limit % 258.02/37.47 % (1624570)Termination phase: Saturation % 258.02/37.47 % (1624570)Time elapsed: 0.824 s % 258.02/37.47 % (1624570)Peak memory usage: 145 MB % 279.44/40.47 % (1624570)Instructions burned: 1504 (million) % 279.44/40.47 % (1624572)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1202498125:i=13942:kws=frequency_2721 on theBenchmark for (2721ds/13942Mi) % 279.44/40.47 % (1624573)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=2817355360:i=3604:fsr=off:er=filter_2719 on theBenchmark for (2719ds/3604Mi) % 279.44/40.47 % (1624573)Instruction limit reached! % 279.44/40.47 % (1624573)------------------------------ % 279.44/40.47 % (1624573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.44/40.47 % (1624573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.44/40.47 % (1624573)CaDiCaL version: 2.1.3 % 279.44/40.47 % (1624573)Termination reason: Instruction limit % 279.44/40.47 % (1624573)Termination phase: Saturation % 279.44/40.47 % (1624573)Time elapsed: 1.902 s % 279.44/40.47 % (1624573)Peak memory usage: 160 MB % 279.44/40.47 % (1624573)Instructions burned: 3606 (million) % 279.44/40.47 % (1624578)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1391535113:i=1876:sd=1:ss=included:sgt=32_2697 on theBenchmark for (2697ds/1876Mi) % 279.44/40.47 % (1624519)Instruction limit reached! % 279.44/40.47 % (1624519)------------------------------ % 279.44/40.47 % (1624519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.44/40.47 % (1624519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.44/40.47 % (1624519)CaDiCaL version: 2.1.3 % 279.44/40.47 % (1624519)Termination reason: Instruction limit % 279.44/40.47 % (1624519)Termination phase: Saturation % 279.44/40.47 % (1624519)Time elapsed: 17.137 s % 279.44/40.47 % (1624519)Peak memory usage: 223 MB % 279.44/40.47 % (1624519)Instructions burned: 16411 (million) % 279.44/40.47 % (1624578)Instruction limit reached! % 279.44/40.47 % (1624578)------------------------------ % 279.44/40.47 % (1624578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.44/40.47 % (1624578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.44/40.47 % (1624578)CaDiCaL version: 2.1.3 % 279.44/40.47 % (1624578)Termination reason: Instruction limit % 279.44/40.47 % (1624578)Termination phase: Saturation % 279.44/40.47 % (1624578)Time elapsed: 0.962 s % 279.44/40.47 % (1624578)Peak memory usage: 139 MB % 279.44/40.47 % (1624578)Instructions burned: 1877 (million) % 279.44/40.47 % (1624585)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=3032675674:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2685 on theBenchmark for (2685ds/1980Mi) % 279.44/40.47 % (1624584)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3326900456:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2686 on theBenchmark for (2686ds/1932Mi) % 279.44/40.47 % (1624556)Instruction limit reached! % 279.44/40.47 % (1624556)------------------------------ % 279.44/40.47 % (1624556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.44/40.47 % (1624556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.44/40.47 % (1624556)CaDiCaL version: 2.1.3 % 279.44/40.47 % (1624556)Termination reason: Instruction limit % 279.44/40.47 % (1624556)Termination phase: Saturation % 279.44/40.47 % (1624556)Time elapsed: 7.248 s % 279.44/40.47 % (1624556)Peak memory usage: 192 MB % 279.44/40.47 % (1624556)Instructions burned: 7343 (million) % 279.44/40.47 % (1624588)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=735201464:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2678 on theBenchmark for (2678ds/3902Mi) % 279.44/40.47 % (1624585)Instruction limit reached! % 279.44/40.47 % (1624585)------------------------------ % 279.44/40.47 % (1624585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.44/40.47 % (1624585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.44/40.47 % (1624585)CaDiCaL version: 2.1.3 % 279.44/40.47 % (1624585)Termination reason: Instruction limit % 279.44/40.47 % (1624585)Termination phase: Saturation % 279.44/40.47 % (1624585)Time elapsed: 1.163 s % 279.44/40.47 % (1624585)Peak memory usage: 138 MB % 279.44/40.47 % (1624585)Instructions burned: 1981 (million) % 279.44/40.47 % (1624591)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=387296432:avsq=on:i=3916:aac=none:amm=off_2672 on theBenchmark for (2672ds/3916Mi) % 300.05/43.33 % (1624584)Instruction limit reached! % 300.05/43.33 % (1624584)------------------------------ % 300.05/43.33 % (1624584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.05/43.33 % (1624584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/43.33 % (1624584)CaDiCaL version: 2.1.3 % 300.05/43.33 % (1624584)Termination reason: Instruction limit % 300.05/43.33 % (1624584)Termination phase: Saturation % 300.05/43.33 % (1624584)Time elapsed: 1.866 s % 300.05/43.33 % (1624584)Peak memory usage: 141 MB % 300.05/43.33 % (1624584)Instructions burned: 1933 (million) % 300.05/43.33 % (1624594)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=1016807597:cond=on:i=3940:av=off:er=known_2664 on theBenchmark for (2664ds/3940Mi) % 300.05/43.33 % (1624591)Instruction limit reached! % 300.05/43.33 % (1624591)------------------------------ % 300.05/43.33 % (1624591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.05/43.33 % (1624591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/43.33 % (1624591)CaDiCaL version: 2.1.3 % 300.05/43.33 % (1624591)Termination reason: Instruction limit % 300.05/43.33 % (1624591)Termination phase: Saturation % 300.05/43.33 % (1624591)Time elapsed: 1.330 s % 300.05/43.33 % (1624591)Peak memory usage: 126 MB % 300.05/43.33 % (1624591)Instructions burned: 3920 (million) % 300.05/43.33 % (1624749)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=595479580:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2656 on theBenchmark for (2656ds/3980Mi) % 300.05/43.33 % (1624588)Instruction limit reached! % 300.05/43.33 % (1624588)------------------------------ % 300.05/43.33 % (1624588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.05/43.33 % (1624588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/43.33 % (1624588)CaDiCaL version: 2.1.3 % 300.05/43.33 % (1624588)Termination reason: Instruction limit % 300.05/43.33 % (1624588)Termination phase: Saturation % 300.05/43.33 % (1624588)Time elapsed: 2.438 s % 300.05/43.33 % (1624588)Peak memory usage: 164 MB % 300.05/43.33 % (1624588)Instructions burned: 3903 (million) % 300.05/43.33 % (1624751)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=1145802251:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2651 on theBenchmark for (2651ds/2087Mi) % 300.05/43.33 % (1624749)Instruction limit reached! % 300.05/43.33 % (1624749)------------------------------ % 300.05/43.33 % (1624749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.05/43.33 % (1624749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/43.33 % (1624749)CaDiCaL version: 2.1.3 % 300.05/43.33 % (1624749)Termination reason: Instruction limit % 300.05/43.33 % (1624749)Termination phase: Saturation % 300.05/43.33 % (1624749)Time elapsed: 1.393 s % 300.05/43.33 % (1624749)Peak memory usage: 158 MB % 300.05/43.33 % (1624749)Instructions burned: 3983 (million) % 300.05/43.33 % (1624753)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=3383683006:cts=off:cond=on:i=4272:bs=on:fsd=on_2641 on theBenchmark for (2641ds/4272Mi) % 300.05/43.33 % (1624594)Instruction limit reached! % 300.05/43.33 % (1624594)------------------------------ % 300.05/43.33 % (1624594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.05/43.33 % (1624594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.05/43.33 % (1624594)CaDiCaL version: 2.1.3 % 300.05/43.33 % (1624594)Termination reason: Instruction limit % 300.05/43.33 % (1624594)Termination phase: Saturation % 300.05/43.33 % (1624594)Time elapsed: 2.457 s % 300.05/43.33 % (1624594)Peak memory usage: 155 MB % 300.05/43.33 % (1624594)Instructions burned: 3941 (million) % 300.05/43.33 % (1624755)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=550432646:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2638 on theBenchmark for (2638ds/2197Mi) % 300.05/43.33 % (1624751)Instruction limit reached! % 300.05/43.33 % (1624751)------------------------------ % 300.05/43.33 % (1624751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.05/43.33 % (1624751)Li % 300.05/43.34 Terminated %------------------------------------------------------------------------------