%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC064-1 : TPTP v9.3.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n006.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:16 PM UTC 2026 % Result : Timeout 300.29s 43.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC064-1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.39 % Computer : n006.cluster.edu % 0.11/0.39 % Model : x86_64 x86_64 % 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.39 % Memory : 8046.5625MB % 0.11/0.39 % OS : Linux 6.8.0-71-generic % 0.11/0.39 % CPULimit : 300 % 0.11/0.39 % WCLimit : 300 % 0.11/0.39 % DateTime : Mon Sep 28 07:41:40 UTC 2026 % 0.11/0.39 % CPUTime : % 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.42 Running first-order theorem proving % 0.11/0.42 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 % 11.73/2.51 % (3803494)Input is clausal, will run a generic CNF schedule. % 11.73/2.51 % (3803500)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2924154680:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 11.73/2.51 % (3803502)lrs+10_1_sil=8000:sp=occurrence:random_seed=1120394302:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 11.73/2.51 % (3803503)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1735831801:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 11.73/2.51 % (3803499)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=3158294383:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 11.73/2.51 % (3803501)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1017060569:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 11.73/2.51 % (3803504)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2962397335:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 11.73/2.51 % (3803505)dis-21_1_sil=8000:lcm=predicate:random_seed=4036113053: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) % 11.73/2.51 % (3803503)Instruction limit reached! % 11.73/2.51 % (3803503)------------------------------ % 11.73/2.51 % (3803503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.73/2.51 % (3803503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.73/2.51 % (3803503)CaDiCaL version: 2.1.3 % 11.73/2.51 % (3803503)Termination reason: Instruction limit % 11.73/2.51 % (3803503)Termination phase: Saturation % 11.73/2.51 % (3803503)Time elapsed: 0.055 s % 11.73/2.51 % (3803503)Peak memory usage: 88 MB % 11.73/2.51 % (3803503)Instructions burned: 116 (million) % 11.73/2.51 % (3803502)Instruction limit reached! % 11.73/2.51 % (3803502)------------------------------ % 11.73/2.51 % (3803502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.73/2.51 % (3803502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.73/2.51 % (3803502)CaDiCaL version: 2.1.3 % 11.73/2.51 % (3803502)Termination reason: Instruction limit % 11.73/2.51 % (3803502)Termination phase: Saturation % 11.73/2.51 % (3803502)Time elapsed: 0.065 s % 11.73/2.51 % (3803502)Peak memory usage: 89 MB % 11.73/2.51 % (3803502)Instructions burned: 108 (million) % 11.73/2.51 % (3803505)Instruction limit reached! % 11.73/2.51 % (3803505)------------------------------ % 11.73/2.51 % (3803505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.73/2.51 % (3803505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.73/2.51 % (3803505)CaDiCaL version: 2.1.3 % 11.73/2.51 % (3803505)Termination reason: Instruction limit % 11.73/2.51 % (3803505)Termination phase: Saturation % 11.73/2.51 % (3803505)Time elapsed: 0.057 s % 11.73/2.51 % (3803505)Peak memory usage: 89 MB % 11.73/2.51 % (3803505)Instructions burned: 117 (million) % 11.73/2.51 % (3803504)Instruction limit reached! % 11.73/2.51 % (3803504)------------------------------ % 11.73/2.51 % (3803504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.73/2.51 % (3803504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.73/2.51 % (3803504)CaDiCaL version: 2.1.3 % 11.73/2.51 % (3803504)Termination reason: Instruction limit % 11.73/2.51 % (3803504)Termination phase: Saturation % 11.73/2.51 % (3803504)Time elapsed: 0.117 s % 11.73/2.51 % (3803504)Peak memory usage: 89 MB % 11.73/2.51 % (3803504)Instructions burned: 181 (million) % 11.73/2.51 % (3803513)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=2666493744:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 11.73/2.51 % (3803513)Refutation not found, incomplete strategy % 11.73/2.51 % (3803513)------------------------------ % 11.73/2.51 % (3803513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.73/2.51 % (3803513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.73/2.51 % (3803513)CaDiCaL version: 2.1.3 % 11.73/2.51 % (3803513)Termination reason: Refutation not found, incomplete strategy % 11.73/2.51 % (3803513)Time elapsed: 0.003 s % 11.73/2.51 % (3803513)Peak memory usage: 89 MB % 11.73/2.51 % (3803513)Instructions burned: 2 (million) % 11.73/2.51 % (3803514)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2566992063: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) % 22.90/4.10 % (3803515)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2876688678:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 22.90/4.10 % (3803516)lrs+10_64_to=lpo:sil=8000:random_seed=3982212770:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 22.90/4.10 % (3803515)Instruction limit reached! % 22.90/4.10 % (3803515)------------------------------ % 22.90/4.10 % (3803515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.90/4.10 % (3803515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.90/4.10 % (3803515)CaDiCaL version: 2.1.3 % 22.90/4.10 % (3803515)Termination reason: Instruction limit % 22.90/4.10 % (3803515)Termination phase: Saturation % 22.90/4.10 % (3803515)Time elapsed: 0.091 s % 22.90/4.10 % (3803515)Peak memory usage: 88 MB % 22.90/4.10 % (3803515)Instructions burned: 221 (million) % 22.90/4.10 % (3803514)Instruction limit reached! % 22.90/4.10 % (3803514)------------------------------ % 22.90/4.10 % (3803514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.90/4.10 % (3803514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.90/4.10 % (3803514)CaDiCaL version: 2.1.3 % 22.90/4.10 % (3803514)Termination reason: Instruction limit % 22.90/4.10 % (3803514)Termination phase: Saturation % 22.90/4.10 % (3803514)Time elapsed: 0.107 s % 22.90/4.10 % (3803514)Peak memory usage: 90 MB % 22.90/4.10 % (3803514)Instructions burned: 189 (million) % 22.90/4.10 % (3803516)Instruction limit reached! % 22.90/4.10 % (3803516)------------------------------ % 22.90/4.10 % (3803516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.90/4.10 % (3803516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.90/4.10 % (3803516)CaDiCaL version: 2.1.3 % 22.90/4.10 % (3803516)Termination reason: Instruction limit % 22.90/4.10 % (3803516)Termination phase: Saturation % 22.90/4.10 % (3803516)Time elapsed: 0.069 s % 22.90/4.10 % (3803516)Peak memory usage: 90 MB % 22.90/4.10 % (3803516)Instructions burned: 126 (million) % 22.90/4.10 % (3803513)------------------------------ % 22.90/4.10 % (3803513)------------------------------ % 22.90/4.10 % (3803521)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1666788077:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 22.90/4.10 % (3803522)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=241602192:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 22.90/4.10 % (3803523)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=65868458:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 22.90/4.10 % (3803522)Instruction limit reached! % 22.90/4.10 % (3803522)------------------------------ % 22.90/4.10 % (3803522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.90/4.10 % (3803522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.90/4.10 % (3803522)CaDiCaL version: 2.1.3 % 22.90/4.10 % (3803522)Termination reason: Instruction limit % 22.90/4.10 % (3803522)Termination phase: Saturation % 22.90/4.10 % (3803522)Time elapsed: 0.094 s % 22.90/4.10 % (3803522)Peak memory usage: 91 MB % 22.90/4.10 % (3803522)Instructions burned: 158 (million) % 22.90/4.10 % (3803521)Instruction limit reached! % 22.90/4.10 % (3803521)------------------------------ % 22.90/4.10 % (3803521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.90/4.10 % (3803521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.90/4.10 % (3803521)CaDiCaL version: 2.1.3 % 22.90/4.10 % (3803521)Termination reason: Instruction limit % 22.90/4.10 % (3803521)Termination phase: Saturation % 22.90/4.10 % (3803521)Time elapsed: 0.129 s % 22.90/4.10 % (3803521)Peak memory usage: 90 MB % 22.90/4.10 % (3803521)Instructions burned: 194 (million) % 22.90/4.10 % (3803524)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=656331652:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 22.90/4.10 % (3803524)Instruction limit reached! % 22.90/4.10 % (3803524)------------------------------ % 22.90/4.10 % (3803524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.90/4.10 % (3803524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.11/5.57 % (3803524)CaDiCaL version: 2.1.3 % 33.11/5.57 % (3803524)Termination reason: Instruction limit % 33.11/5.57 % (3803524)Termination phase: Saturation % 33.11/5.57 % (3803524)Time elapsed: 0.059 s % 33.11/5.57 % (3803524)Peak memory usage: 91 MB % 33.11/5.57 % (3803524)Instructions burned: 107 (million) % 33.11/5.57 % (3803528)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1377399658:i=107_2992 on theBenchmark for (2992ds/107Mi) % 33.11/5.57 % (3803529)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3804917316:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 33.11/5.57 % (3803528)Instruction limit reached! % 33.11/5.57 % (3803528)------------------------------ % 33.11/5.57 % (3803528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.11/5.57 % (3803528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.11/5.57 % (3803528)CaDiCaL version: 2.1.3 % 33.11/5.57 % (3803528)Termination reason: Instruction limit % 33.11/5.57 % (3803528)Termination phase: Saturation % 33.11/5.57 % (3803528)Time elapsed: 0.065 s % 33.11/5.57 % (3803528)Peak memory usage: 90 MB % 33.11/5.57 % (3803528)Instructions burned: 107 (million) % 33.11/5.57 % (3803531)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2448982039:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi) % 33.11/5.57 % (3803529)Instruction limit reached! % 33.11/5.57 % (3803529)------------------------------ % 33.11/5.57 % (3803529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.11/5.57 % (3803529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.11/5.57 % (3803529)CaDiCaL version: 2.1.3 % 33.11/5.57 % (3803529)Termination reason: Instruction limit % 33.11/5.57 % (3803529)Termination phase: Saturation % 33.11/5.57 % (3803529)Time elapsed: 0.147 s % 33.11/5.57 % (3803529)Peak memory usage: 89 MB % 33.11/5.57 % (3803529)Instructions burned: 243 (million) % 33.11/5.57 % (3803534)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3982453056:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi) % 33.11/5.57 % (3803534)Instruction limit reached! % 33.11/5.57 % (3803534)------------------------------ % 33.11/5.57 % (3803534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.11/5.57 % (3803534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.11/5.57 % (3803534)CaDiCaL version: 2.1.3 % 33.11/5.57 % (3803534)Termination reason: Instruction limit % 33.11/5.57 % (3803534)Termination phase: Saturation % 33.11/5.57 % (3803534)Time elapsed: 0.087 s % 33.11/5.57 % (3803534)Peak memory usage: 90 MB % 33.11/5.57 % (3803534)Instructions burned: 134 (million) % 33.11/5.57 % (3803536)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4072730644:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi) % 33.11/5.57 % (3803538)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3361649689:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi) % 33.11/5.57 % (3803536)Instruction limit reached! % 33.11/5.57 % (3803536)------------------------------ % 33.11/5.57 % (3803536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.11/5.57 % (3803536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.11/5.57 % (3803536)CaDiCaL version: 2.1.3 % 33.11/5.57 % (3803536)Termination reason: Instruction limit % 33.11/5.57 % (3803536)Termination phase: Saturation % 33.11/5.57 % (3803536)Time elapsed: 0.257 s % 33.11/5.57 % (3803536)Peak memory usage: 98 MB % 33.11/5.57 % (3803536)Instructions burned: 500 (million) % 33.11/5.57 % (3803538)Instruction limit reached! % 33.11/5.57 % (3803538)------------------------------ % 33.11/5.57 % (3803538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.11/5.57 % (3803538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.11/5.57 % (3803538)CaDiCaL version: 2.1.3 % 33.11/5.57 % (3803538)Termination reason: Instruction limit % 33.11/5.57 % (3803538)Termination phase: Saturation % 33.11/5.57 % (3803538)Time elapsed: 0.120 s % 33.11/5.57 % (3803538)Peak memory usage: 90 MB % 33.11/5.57 % (3803538)Instructions burned: 192 (million) % 33.11/5.57 % (3803541)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3536100121:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi) % 53.27/8.45 % (3803542)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=401141103:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi) % 53.27/8.45 % (3803542)Instruction limit reached! % 53.27/8.45 % (3803542)------------------------------ % 53.27/8.45 % (3803542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.45 % (3803542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.45 % (3803542)CaDiCaL version: 2.1.3 % 53.27/8.45 % (3803542)Termination reason: Instruction limit % 53.27/8.45 % (3803542)Termination phase: Saturation % 53.27/8.45 % (3803542)Time elapsed: 0.091 s % 53.27/8.45 % (3803542)Peak memory usage: 90 MB % 53.27/8.45 % (3803542)Instructions burned: 156 (million) % 53.27/8.45 % (3803541)Instruction limit reached! % 53.27/8.45 % (3803541)------------------------------ % 53.27/8.45 % (3803541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.45 % (3803541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.45 % (3803541)CaDiCaL version: 2.1.3 % 53.27/8.45 % (3803541)Termination reason: Instruction limit % 53.27/8.45 % (3803541)Termination phase: Saturation % 53.27/8.45 % (3803541)Time elapsed: 0.132 s % 53.27/8.45 % (3803541)Peak memory usage: 92 MB % 53.27/8.45 % (3803541)Instructions burned: 266 (million) % 53.27/8.45 % (3803545)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=4002685094:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi) % 53.27/8.45 % (3803546)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2597501383:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi) % 53.27/8.45 % (3803546)Instruction limit reached! % 53.27/8.45 % (3803546)------------------------------ % 53.27/8.45 % (3803546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.45 % (3803546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.45 % (3803546)CaDiCaL version: 2.1.3 % 53.27/8.45 % (3803546)Termination reason: Instruction limit % 53.27/8.45 % (3803546)Termination phase: Saturation % 53.27/8.45 % (3803546)Time elapsed: 0.264 s % 53.27/8.45 % (3803546)Peak memory usage: 93 MB % 53.27/8.45 % (3803546)Instructions burned: 537 (million) % 53.27/8.45 % (3803550)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3059132160:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi) % 53.27/8.45 % (3803550)Instruction limit reached! % 53.27/8.45 % (3803550)------------------------------ % 53.27/8.45 % (3803550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.45 % (3803550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.45 % (3803550)CaDiCaL version: 2.1.3 % 53.27/8.45 % (3803550)Termination reason: Instruction limit % 53.27/8.45 % (3803550)Termination phase: Saturation % 53.27/8.45 % (3803550)Time elapsed: 0.092 s % 53.27/8.45 % (3803550)Peak memory usage: 91 MB % 53.27/8.45 % (3803550)Instructions burned: 180 (million) % 53.27/8.45 % (3803552)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=2660956872:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi) % 53.27/8.45 % (3803523)Instruction limit reached! % 53.27/8.45 % (3803523)------------------------------ % 53.27/8.45 % (3803523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.45 % (3803523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.45 % (3803523)CaDiCaL version: 2.1.3 % 53.27/8.45 % (3803523)Termination reason: Instruction limit % 53.27/8.45 % (3803523)Termination phase: Saturation % 53.27/8.45 % (3803523)Time elapsed: 2.169 s % 53.27/8.45 % (3803523)Peak memory usage: 152 MB % 53.27/8.45 % (3803523)Instructions burned: 3396 (million) % 53.27/8.45 % (3803554)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=2266968397:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi) % 53.27/8.45 % (3803554)Instruction limit reached! % 53.27/8.45 % (3803554)------------------------------ % 53.27/8.45 % (3803554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.45 % (3803554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.45 % (3803554)CaDiCaL version: 2.1.3 % 75.70/11.52 % (3803554)Termination reason: Instruction limit % 75.70/11.52 % (3803554)Termination phase: Saturation % 75.70/11.52 % (3803554)Time elapsed: 0.214 s % 75.70/11.52 % (3803554)Peak memory usage: 91 MB % 75.70/11.52 % (3803554)Instructions burned: 412 (million) % 75.70/11.52 % (3803556)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=23402490:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi) % 75.70/11.52 % (3803545)Instruction limit reached! % 75.70/11.52 % (3803545)------------------------------ % 75.70/11.52 % (3803545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.70/11.52 % (3803545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.70/11.52 % (3803545)CaDiCaL version: 2.1.3 % 75.70/11.52 % (3803545)Termination reason: Instruction limit % 75.70/11.52 % (3803545)Termination phase: Saturation % 75.70/11.52 % (3803545)Time elapsed: 1.825 s % 75.70/11.52 % (3803545)Peak memory usage: 153 MB % 75.70/11.52 % (3803545)Instructions burned: 3256 (million) % 75.70/11.52 % (3803558)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=1833653126:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2962 on theBenchmark for (2962ds/303Mi) % 75.70/11.52 % (3803558)Instruction limit reached! % 75.70/11.52 % (3803558)------------------------------ % 75.70/11.52 % (3803558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.70/11.52 % (3803558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.70/11.52 % (3803558)CaDiCaL version: 2.1.3 % 75.70/11.52 % (3803558)Termination reason: Instruction limit % 75.70/11.52 % (3803558)Termination phase: Saturation % 75.70/11.52 % (3803558)Time elapsed: 0.149 s % 75.70/11.52 % (3803558)Peak memory usage: 98 MB % 75.70/11.52 % (3803558)Instructions burned: 304 (million) % 75.70/11.52 % (3803531)Instruction limit reached! % 75.70/11.52 % (3803531)------------------------------ % 75.70/11.52 % (3803531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.70/11.52 % (3803531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.70/11.52 % (3803531)CaDiCaL version: 2.1.3 % 75.70/11.52 % (3803531)Termination reason: Instruction limit % 75.70/11.52 % (3803531)Termination phase: Saturation % 75.70/11.52 % (3803531)Time elapsed: 3.069 s % 75.70/11.52 % (3803531)Peak memory usage: 147 MB % 75.70/11.52 % (3803531)Instructions burned: 5209 (million) % 75.70/11.52 % (3803560)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3737784288:st=4:i=720:sd=3:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/720Mi) % 75.70/11.52 % (3803561)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3893472686:i=598:bs=on:bd=preordered:av=off:ss=axioms_2958 on theBenchmark for (2958ds/598Mi) % 75.70/11.52 % (3803560)Instruction limit reached! % 75.70/11.52 % (3803560)------------------------------ % 75.70/11.52 % (3803560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.70/11.52 % (3803560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.70/11.52 % (3803560)CaDiCaL version: 2.1.3 % 75.70/11.52 % (3803560)Termination reason: Instruction limit % 75.70/11.52 % (3803560)Termination phase: Saturation % 75.70/11.52 % (3803560)Time elapsed: 0.348 s % 75.70/11.52 % (3803560)Peak memory usage: 98 MB % 75.70/11.52 % (3803560)Instructions burned: 721 (million) % 75.70/11.52 % (3803561)Instruction limit reached! % 75.70/11.52 % (3803561)------------------------------ % 75.70/11.52 % (3803561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.70/11.52 % (3803561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.70/11.52 % (3803561)CaDiCaL version: 2.1.3 % 75.70/11.52 % (3803561)Termination reason: Instruction limit % 75.70/11.52 % (3803561)Termination phase: Saturation % 75.70/11.52 % (3803561)Time elapsed: 0.294 s % 75.70/11.52 % (3803561)Peak memory usage: 93 MB % 75.70/11.52 % (3803561)Instructions burned: 598 (million) % 75.70/11.52 % (3803564)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4055872819:i=2989:sd=3:ss=axioms:sgt=60_2954 on theBenchmark for (2954ds/2989Mi) % 75.70/11.52 % (3803565)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=3087163653:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2954 on theBenchmark for (2954ds/1997Mi) % 105.67/16.02 % (3803565)Instruction limit reached! % 105.67/16.02 % (3803565)------------------------------ % 105.67/16.02 % (3803565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.67/16.02 % (3803565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.67/16.02 % (3803565)CaDiCaL version: 2.1.3 % 105.67/16.02 % (3803565)Termination reason: Instruction limit % 105.67/16.02 % (3803565)Termination phase: Saturation % 105.67/16.02 % (3803565)Time elapsed: 1.230 s % 105.67/16.02 % (3803565)Peak memory usage: 138 MB % 105.67/16.02 % (3803565)Instructions burned: 2000 (million) % 105.67/16.02 % (3803568)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=3372152077:i=2088:bd=preordered:av=off_2940 on theBenchmark for (2940ds/2088Mi) % 105.67/16.02 % (3803564)Instruction limit reached! % 105.67/16.02 % (3803564)------------------------------ % 105.67/16.02 % (3803564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.67/16.02 % (3803564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.67/16.02 % (3803564)CaDiCaL version: 2.1.3 % 105.67/16.02 % (3803564)Termination reason: Instruction limit % 105.67/16.02 % (3803564)Termination phase: Saturation % 105.67/16.02 % (3803564)Time elapsed: 1.959 s % 105.67/16.02 % (3803564)Peak memory usage: 146 MB % 105.67/16.02 % (3803564)Instructions burned: 2989 (million) % 105.67/16.02 % (3803570)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2066744018:i=1098:nicw=on_2933 on theBenchmark for (2933ds/1098Mi) % 105.67/16.02 % (3803556)Instruction limit reached! % 105.67/16.02 % (3803556)------------------------------ % 105.67/16.02 % (3803556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.67/16.02 % (3803556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.67/16.02 % (3803556)CaDiCaL version: 2.1.3 % 105.67/16.02 % (3803556)Termination reason: Instruction limit % 105.67/16.02 % (3803556)Termination phase: Saturation % 105.67/16.02 % (3803556)Time elapsed: 3.811 s % 105.67/16.02 % (3803556)Peak memory usage: 193 MB % 105.67/16.02 % (3803556)Instructions burned: 8480 (million) % 105.67/16.02 % (3803570)Instruction limit reached! % 105.67/16.02 % (3803570)------------------------------ % 105.67/16.02 % (3803570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.67/16.02 % (3803570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.67/16.02 % (3803570)CaDiCaL version: 2.1.3 % 105.67/16.02 % (3803570)Termination reason: Instruction limit % 105.67/16.02 % (3803570)Termination phase: Saturation % 105.67/16.02 % (3803570)Time elapsed: 0.518 s % 105.67/16.02 % (3803570)Peak memory usage: 120 MB % 105.67/16.02 % (3803570)Instructions burned: 1099 (million) % 105.67/16.02 % (3803572)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2714271719:i=433:bd=preordered_2927 on theBenchmark for (2927ds/433Mi) % 105.67/16.02 % (3803568)Instruction limit reached! % 105.67/16.02 % (3803568)------------------------------ % 105.67/16.02 % (3803568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.67/16.02 % (3803568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.67/16.02 % (3803568)CaDiCaL version: 2.1.3 % 105.67/16.02 % (3803568)Termination reason: Instruction limit % 105.67/16.02 % (3803568)Termination phase: Saturation % 105.67/16.02 % (3803568)Time elapsed: 1.296 s % 105.67/16.02 % (3803568)Peak memory usage: 138 MB % 105.67/16.02 % (3803568)Instructions burned: 2090 (million) % 105.67/16.02 % (3803573)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3096168719:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2926 on theBenchmark for (2926ds/2942Mi) % 105.67/16.02 % (3803575)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=4017358225:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2925 on theBenchmark for (2925ds/6922Mi) % 105.67/16.02 % (3803552)Instruction limit reached! % 105.67/16.02 % (3803552)------------------------------ % 105.67/16.02 % (3803552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.67/16.02 % (3803552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.67/16.02 % (3803552)CaDiCaL version: 2.1.3 % 105.67/16.02 % (3803552)Termination reason: Instruction limit % 105.67/16.02 % (3803552)Termination phase: Saturation % 105.67/16.02 % (3803552)Time elapsed: 4.970 s % 120.45/17.85 % (3803552)Peak memory usage: 148 MB % 120.45/17.85 % (3803552)Instructions burned: 10308 (million) % 120.45/17.85 % (3803572)Instruction limit reached! % 120.45/17.85 % (3803572)------------------------------ % 120.45/17.85 % (3803572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.45/17.85 % (3803572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.85 % (3803572)CaDiCaL version: 2.1.3 % 120.45/17.85 % (3803572)Termination reason: Instruction limit % 120.45/17.85 % (3803572)Termination phase: Saturation % 120.45/17.85 % (3803572)Time elapsed: 0.261 s % 120.45/17.85 % (3803572)Peak memory usage: 93 MB % 120.45/17.85 % (3803572)Instructions burned: 435 (million) % 120.45/17.85 % (3803578)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=4089872188:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2923 on theBenchmark for (2923ds/596Mi) % 120.45/17.85 % (3803579)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=1301541948:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2923 on theBenchmark for (2923ds/4123Mi) % 120.45/17.85 % (3803578)Instruction limit reached! % 120.45/17.85 % (3803578)------------------------------ % 120.45/17.85 % (3803578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.45/17.85 % (3803578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.85 % (3803578)CaDiCaL version: 2.1.3 % 120.45/17.85 % (3803578)Termination reason: Instruction limit % 120.45/17.85 % (3803578)Termination phase: Saturation % 120.45/17.85 % (3803578)Time elapsed: 0.293 s % 120.45/17.85 % (3803578)Peak memory usage: 108 MB % 120.45/17.85 % (3803578)Instructions burned: 598 (million) % 120.45/17.85 % (3803582)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3837335027:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2919 on theBenchmark for (2919ds/16411Mi) % 120.45/17.85 % (3803573)Instruction limit reached! % 120.45/17.85 % (3803573)------------------------------ % 120.45/17.85 % (3803573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.45/17.85 % (3803573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.85 % (3803573)CaDiCaL version: 2.1.3 % 120.45/17.85 % (3803573)Termination reason: Instruction limit % 120.45/17.85 % (3803573)Termination phase: Saturation % 120.45/17.85 % (3803573)Time elapsed: 1.854 s % 120.45/17.85 % (3803573)Peak memory usage: 144 MB % 120.45/17.85 % (3803573)Instructions burned: 2942 (million) % 120.45/17.85 % (3803584)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2356223425:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2906 on theBenchmark for (2906ds/1670Mi) % 120.45/17.85 % (3803579)Instruction limit reached! % 120.45/17.85 % (3803579)------------------------------ % 120.45/17.85 % (3803579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.45/17.85 % (3803579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.85 % (3803579)CaDiCaL version: 2.1.3 % 120.45/17.85 % (3803579)Termination reason: Instruction limit % 120.45/17.85 % (3803579)Termination phase: Saturation % 120.45/17.85 % (3803579)Time elapsed: 2.275 s % 120.45/17.85 % (3803579)Peak memory usage: 164 MB % 120.45/17.85 % (3803579)Instructions burned: 4123 (million) % 120.45/17.85 % (3803586)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=2247477904:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2898 on theBenchmark for (2898ds/1722Mi) % 120.45/17.85 % (3803584)Instruction limit reached! % 120.45/17.85 % (3803584)------------------------------ % 120.45/17.85 % (3803584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.45/17.85 % (3803584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.45/17.85 % (3803584)CaDiCaL version: 2.1.3 % 120.45/17.85 % (3803584)Termination reason: Instruction limit % 120.45/17.85 % (3803584)Termination phase: Saturation % 120.45/17.85 % (3803584)Time elapsed: 1.003 s % 120.45/17.85 % (3803584)Peak memory usage: 137 MB % 120.45/17.85 % (3803584)Instructions burned: 1670 (million) % 120.45/17.85 % (3803588)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=496553050:cts=off:cond=on:i=9530:bs=on:fsd=on_2894 on theBenchmark for (2894ds/9530Mi) % 136.35/20.09 % (3803575)Instruction limit reached! % 136.35/20.09 % (3803575)------------------------------ % 136.35/20.09 % (3803575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.35/20.09 % (3803575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.35/20.09 % (3803575)CaDiCaL version: 2.1.3 % 136.35/20.09 % (3803575)Termination reason: Instruction limit % 136.35/20.09 % (3803575)Termination phase: Saturation % 136.35/20.09 % (3803575)Time elapsed: 3.587 s % 136.35/20.09 % (3803575)Peak memory usage: 186 MB % 136.35/20.09 % (3803575)Instructions burned: 6924 (million) % 136.35/20.09 % (3803586)Instruction limit reached! % 136.35/20.09 % (3803586)------------------------------ % 136.35/20.09 % (3803586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.35/20.09 % (3803586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.35/20.09 % (3803586)CaDiCaL version: 2.1.3 % 136.35/20.09 % (3803586)Termination reason: Instruction limit % 136.35/20.09 % (3803586)Termination phase: Saturation % 136.35/20.09 % (3803586)Time elapsed: 1.031 s % 136.35/20.09 % (3803586)Peak memory usage: 133 MB % 136.35/20.09 % (3803586)Instructions burned: 1722 (million) % 136.35/20.09 % (3803590)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1570810386:st=2:i=4495:sd=10:ss=included_2888 on theBenchmark for (2888ds/4495Mi) % 136.35/20.09 % (3803591)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=3914479616:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2886 on theBenchmark for (2886ds/4920Mi) % 136.35/20.09 % (3803590)Instruction limit reached! % 136.35/20.09 % (3803590)------------------------------ % 136.35/20.09 % (3803590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.35/20.09 % (3803590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.35/20.09 % (3803590)CaDiCaL version: 2.1.3 % 136.35/20.09 % (3803590)Termination reason: Instruction limit % 136.35/20.09 % (3803590)Termination phase: Saturation % 136.35/20.09 % (3803590)Time elapsed: 2.664 s % 136.35/20.09 % (3803590)Peak memory usage: 151 MB % 136.35/20.09 % (3803590)Instructions burned: 4496 (million) % 136.35/20.09 % (3803594)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=2914693903:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2859 on theBenchmark for (2859ds/2083Mi) % 136.35/20.09 % (3803582)Instruction limit reached! % 136.35/20.09 % (3803582)------------------------------ % 136.35/20.09 % (3803582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.35/20.09 % (3803582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.35/20.09 % (3803582)CaDiCaL version: 2.1.3 % 136.35/20.09 % (3803582)Termination reason: Instruction limit % 136.35/20.09 % (3803582)Termination phase: Saturation % 136.35/20.09 % (3803582)Time elapsed: 6.065 s % 136.35/20.09 % (3803582)Peak memory usage: 253 MB % 136.35/20.09 % (3803582)Instructions burned: 16414 (million) % 136.35/20.09 % (3803591)Instruction limit reached! % 136.35/20.09 % (3803591)------------------------------ % 136.35/20.09 % (3803591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.35/20.09 % (3803591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.35/20.09 % (3803591)CaDiCaL version: 2.1.3 % 136.35/20.09 % (3803591)Termination reason: Instruction limit % 136.35/20.09 % (3803591)Termination phase: Saturation % 136.35/20.09 % (3803591)Time elapsed: 2.929 s % 136.35/20.09 % (3803591)Peak memory usage: 154 MB % 136.35/20.09 % (3803591)Instructions burned: 4921 (million) % 136.35/20.09 % (3803596)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=307806648:i=4629:av=off:gsp=on_2857 on theBenchmark for (2857ds/4629Mi) % 136.35/20.09 % (3803597)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2595282086:i=1258:av=off_2855 on theBenchmark for (2855ds/1258Mi) % 136.35/20.09 % (3803597)Instruction limit reached! % 136.35/20.09 % (3803597)------------------------------ % 136.35/20.09 % (3803597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.35/20.09 % (3803597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.35/20.09 % (3803597)CaDiCaL version: 2.1.3 % 136.35/20.09 % (3803597)Termination reason: Instruction limit % 136.35/20.09 % (3803597)Termination phase: Saturation % 159.86/23.49 % (3803597)Time elapsed: 0.601 s % 159.86/23.49 % (3803597)Peak memory usage: 102 MB % 159.86/23.49 % (3803597)Instructions burned: 1258 (million) % 159.86/23.49 % (3803600)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3952519839:i=7343:av=off:ss=included_2848 on theBenchmark for (2848ds/7343Mi) % 159.86/23.49 % (3803588)Instruction limit reached! % 159.86/23.49 % (3803588)------------------------------ % 159.86/23.49 % (3803588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.86/23.49 % (3803588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.86/23.49 % (3803588)CaDiCaL version: 2.1.3 % 159.86/23.49 % (3803588)Termination reason: Instruction limit % 159.86/23.49 % (3803588)Termination phase: Saturation % 159.86/23.49 % (3803588)Time elapsed: 4.680 s % 159.86/23.49 % (3803588)Peak memory usage: 155 MB % 159.86/23.49 % (3803588)Instructions burned: 9532 (million) % 159.86/23.49 % (3803594)Instruction limit reached! % 159.86/23.49 % (3803594)------------------------------ % 159.86/23.49 % (3803594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.86/23.49 % (3803594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.86/23.49 % (3803594)CaDiCaL version: 2.1.3 % 159.86/23.49 % (3803594)Termination reason: Instruction limit % 159.86/23.49 % (3803594)Termination phase: Saturation % 159.86/23.49 % (3803594)Time elapsed: 1.283 s % 159.86/23.49 % (3803594)Peak memory usage: 139 MB % 159.86/23.49 % (3803594)Instructions burned: 2083 (million) % 159.86/23.49 % (3803602)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=736661781:i=1325:sd=2:ss=axioms:sgt=16_2846 on theBenchmark for (2846ds/1325Mi) % 159.86/23.49 % (3803603)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=3596200556:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2845 on theBenchmark for (2845ds/2646Mi) % 159.86/23.49 % (3803596)Instruction limit reached! % 159.86/23.49 % (3803596)------------------------------ % 159.86/23.49 % (3803596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.86/23.49 % (3803596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.86/23.49 % (3803596)CaDiCaL version: 2.1.3 % 159.86/23.49 % (3803596)Termination reason: Instruction limit % 159.86/23.49 % (3803596)Termination phase: Saturation % 159.86/23.49 % (3803596)Time elapsed: 1.420 s % 159.86/23.49 % (3803596)Peak memory usage: 166 MB % 159.86/23.49 % (3803596)Instructions burned: 4630 (million) % 159.86/23.49 % (3803602)Instruction limit reached! % 159.86/23.49 % (3803602)------------------------------ % 159.86/23.49 % (3803602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.86/23.49 % (3803602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.86/23.49 % (3803602)CaDiCaL version: 2.1.3 % 159.86/23.49 % (3803602)Termination reason: Instruction limit % 159.86/23.49 % (3803602)Termination phase: Saturation % 159.86/23.49 % (3803602)Time elapsed: 0.444 s % 159.86/23.49 % (3803602)Peak memory usage: 88 MB % 159.86/23.49 % (3803602)Instructions burned: 1325 (million) % 159.86/23.49 % (3803606)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2885363546:i=1489:sd=2:ep=R:ss=axioms_2841 on theBenchmark for (2841ds/1489Mi) % 159.86/23.49 % (3803607)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=3162743600:i=1503_2840 on theBenchmark for (2840ds/1503Mi) % 159.86/23.49 % (3803606)Instruction limit reached! % 159.86/23.49 % (3803606)------------------------------ % 159.86/23.49 % (3803606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.86/23.49 % (3803606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.86/23.49 % (3803606)CaDiCaL version: 2.1.3 % 159.86/23.49 % (3803606)Termination reason: Instruction limit % 159.86/23.49 % (3803606)Termination phase: Saturation % 159.86/23.49 % (3803606)Time elapsed: 0.883 s % 159.86/23.49 % (3803606)Peak memory usage: 136 MB % 159.86/23.49 % (3803606)Instructions burned: 1489 (million) % 159.86/23.49 % (3803607)Instruction limit reached! % 159.86/23.49 % (3803607)------------------------------ % 159.86/23.49 % (3803607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.86/23.49 % (3803607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.86/23.49 % (3803607)CaDiCaL version: 2.1.3 % 159.86/23.49 % (3803607)Termination reason: Instruction limit % 159.86/23.49 % (3803607)Termination phase: Saturation % 186.01/27.11 % (3803607)Time elapsed: 0.884 s % 186.01/27.11 % (3803607)Peak memory usage: 145 MB % 186.01/27.11 % (3803607)Instructions burned: 1504 (million) % 186.01/27.11 % (3803610)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=4222656183:i=13942:kws=frequency_2831 on theBenchmark for (2831ds/13942Mi) % 186.01/27.11 % (3803611)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=3261394336:i=3604:fsr=off:er=filter_2829 on theBenchmark for (2829ds/3604Mi) % 186.01/27.11 % (3803603)Instruction limit reached! % 186.01/27.11 % (3803603)------------------------------ % 186.01/27.11 % (3803603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.01/27.11 % (3803603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.01/27.11 % (3803603)CaDiCaL version: 2.1.3 % 186.01/27.11 % (3803603)Termination reason: Instruction limit % 186.01/27.11 % (3803603)Termination phase: Saturation % 186.01/27.11 % (3803603)Time elapsed: 1.602 s % 186.01/27.11 % (3803603)Peak memory usage: 138 MB % 186.01/27.11 % (3803603)Instructions burned: 2647 (million) % 186.01/27.11 % (3803614)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=670703108:i=1876:sd=1:ss=included:sgt=32_2827 on theBenchmark for (2827ds/1876Mi) % 186.01/27.11 % (3803600)Instruction limit reached! % 186.01/27.11 % (3803600)------------------------------ % 186.01/27.11 % (3803600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.01/27.11 % (3803600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.01/27.11 % (3803600)CaDiCaL version: 2.1.3 % 186.01/27.11 % (3803600)Termination reason: Instruction limit % 186.01/27.11 % (3803600)Termination phase: Saturation % 186.01/27.11 % (3803600)Time elapsed: 2.607 s % 186.01/27.11 % (3803600)Peak memory usage: 184 MB % 186.01/27.11 % (3803600)Instructions burned: 7344 (million) % 186.01/27.11 % (3803616)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2598515341:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2820 on theBenchmark for (2820ds/1932Mi) % 186.01/27.11 % (3803614)Instruction limit reached! % 186.01/27.11 % (3803614)------------------------------ % 186.01/27.11 % (3803614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.01/27.11 % (3803614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.01/27.11 % (3803614)CaDiCaL version: 2.1.3 % 186.01/27.11 % (3803614)Termination reason: Instruction limit % 186.01/27.11 % (3803614)Termination phase: Saturation % 186.01/27.11 % (3803614)Time elapsed: 1.223 s % 186.01/27.11 % (3803614)Peak memory usage: 136 MB % 186.01/27.11 % (3803614)Instructions burned: 1876 (million) % 186.01/27.11 % (3803616)Instruction limit reached! % 186.01/27.11 % (3803616)------------------------------ % 186.01/27.11 % (3803616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.01/27.11 % (3803616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.01/27.11 % (3803616)CaDiCaL version: 2.1.3 % 186.01/27.11 % (3803616)Termination reason: Instruction limit % 186.01/27.11 % (3803616)Termination phase: Saturation % 186.01/27.11 % (3803616)Time elapsed: 0.594 s % 186.01/27.11 % (3803616)Peak memory usage: 139 MB % 186.01/27.11 % (3803616)Instructions burned: 1932 (million) % 186.01/27.11 % (3803619)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=2927734003:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2813 on theBenchmark for (2813ds/3902Mi) % 186.01/27.11 % (3803618)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=644321776:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2813 on theBenchmark for (2813ds/1980Mi) % 186.01/27.11 % (3803611)Instruction limit reached! % 186.01/27.11 % (3803611)------------------------------ % 186.01/27.11 % (3803611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 186.01/27.11 % (3803611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 186.01/27.11 % (3803611)CaDiCaL version: 2.1.3 % 186.01/27.11 % (3803611)Termination reason: Instruction limit % 186.01/27.11 % (3803611)Termination phase: Saturation % 186.01/27.11 % (3803611)Time elapsed: 2.068 s % 186.01/27.11 % (3803611)Peak memory usage: 158 MB % 186.01/27.11 % (3803611)Instructions burned: 3605 (million) % 202.65/29.45 % (3803622)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=3838636198:avsq=on:i=3916:aac=none:amm=off_2807 on theBenchmark for (2807ds/3916Mi) % 202.65/29.45 % (3803619)Instruction limit reached! % 202.65/29.45 % (3803619)------------------------------ % 202.65/29.45 % (3803619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.65/29.45 % (3803619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.65/29.45 % (3803619)CaDiCaL version: 2.1.3 % 202.65/29.45 % (3803619)Termination reason: Instruction limit % 202.65/29.45 % (3803619)Termination phase: Saturation % 202.65/29.45 % (3803619)Time elapsed: 1.161 s % 202.65/29.45 % (3803619)Peak memory usage: 162 MB % 202.65/29.45 % (3803619)Instructions burned: 3904 (million) % 202.65/29.45 % (3803618)Instruction limit reached! % 202.65/29.45 % (3803618)------------------------------ % 202.65/29.45 % (3803618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.65/29.45 % (3803618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.65/29.45 % (3803618)CaDiCaL version: 2.1.3 % 202.65/29.45 % (3803618)Termination reason: Instruction limit % 202.65/29.45 % (3803618)Termination phase: Saturation % 202.65/29.45 % (3803618)Time elapsed: 1.270 s % 202.65/29.45 % (3803618)Peak memory usage: 138 MB % 202.65/29.45 % (3803618)Instructions burned: 1980 (million) % 202.65/29.45 % (3803624)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3366028167:cond=on:i=3940:av=off:er=known_2800 on theBenchmark for (2800ds/3940Mi) % 202.65/29.45 % (3803625)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=3873828596:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2799 on theBenchmark for (2799ds/3980Mi) % 202.65/29.45 % (3803624)Instruction limit reached! % 202.65/29.45 % (3803624)------------------------------ % 202.65/29.45 % (3803624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.65/29.45 % (3803624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.65/29.45 % (3803624)CaDiCaL version: 2.1.3 % 202.65/29.45 % (3803624)Termination reason: Instruction limit % 202.65/29.45 % (3803624)Termination phase: Saturation % 202.65/29.45 % (3803624)Time elapsed: 1.270 s % 202.65/29.45 % (3803624)Peak memory usage: 151 MB % 202.65/29.45 % (3803624)Instructions burned: 3940 (million) % 202.65/29.45 % (3803628)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=2375776543:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2786 on theBenchmark for (2786ds/2087Mi) % 202.65/29.45 % (3803622)Instruction limit reached! % 202.65/29.45 % (3803622)------------------------------ % 202.65/29.45 % (3803622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.65/29.45 % (3803622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.65/29.45 % (3803622)CaDiCaL version: 2.1.3 % 202.65/29.45 % (3803622)Termination reason: Instruction limit % 202.65/29.45 % (3803622)Termination phase: Saturation % 202.65/29.45 % (3803622)Time elapsed: 2.311 s % 202.65/29.45 % (3803622)Peak memory usage: 119 MB % 202.65/29.45 % (3803622)Instructions burned: 3916 (million) % 202.65/29.45 % (3803630)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=412872277:cts=off:cond=on:i=4272:bs=on:fsd=on_2782 on theBenchmark for (2782ds/4272Mi) % 202.65/29.45 % (3803628)Instruction limit reached! % 202.65/29.45 % (3803628)------------------------------ % 202.65/29.45 % (3803628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.65/29.45 % (3803628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.65/29.45 % (3803628)CaDiCaL version: 2.1.3 % 202.65/29.45 % (3803628)Termination reason: Instruction limit % 202.65/29.45 % (3803628)Termination phase: Saturation % 202.65/29.45 % (3803628)Time elapsed: 0.722 s % 202.65/29.45 % (3803628)Peak memory usage: 141 MB % 202.65/29.45 % (3803628)Instructions burned: 2090 (million) % 202.65/29.45 % (3803632)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=417496268:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2778 on theBenchmark for (2778ds/2197Mi) % 202.65/29.45 % (3803625)Instruction limit reached! % 202.65/29.45 % (3803625)------------------------------ % 202.65/29.45 % (3803625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.32/40.09 % (3803625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.32/40.09 % (3803625)CaDiCaL version: 2.1.3 % 278.32/40.09 % (3803625)Termination reason: Instruction limit % 278.32/40.09 % (3803625)Termination phase: Saturation % 278.32/40.09 % (3803625)Time elapsed: 2.428 s % 278.32/40.09 % (3803625)Peak memory usage: 159 MB % 278.32/40.09 % (3803625)Instructions burned: 3981 (million) % 278.32/40.09 % (3803634)dis+21_1_sil=8000:spb=goal_then_units:random_seed=982575235:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2773 on theBenchmark for (2773ds/6508Mi) % 278.32/40.09 % (3803632)Instruction limit reached! % 278.32/40.09 % (3803632)------------------------------ % 278.32/40.09 % (3803632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.32/40.09 % (3803632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.32/40.09 % (3803632)CaDiCaL version: 2.1.3 % 278.32/40.09 % (3803632)Termination reason: Instruction limit % 278.32/40.09 % (3803632)Termination phase: Saturation % 278.32/40.09 % (3803632)Time elapsed: 0.699 s % 278.32/40.09 % (3803632)Peak memory usage: 144 MB % 278.32/40.09 % (3803632)Instructions burned: 2198 (million) % 278.32/40.09 % (3803636)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3739639686:i=2330:fgj=on:av=off:fsr=off_2769 on theBenchmark for (2769ds/2330Mi) % 278.32/40.09 % (3803636)Instruction limit reached! % 278.32/40.09 % (3803636)------------------------------ % 278.32/40.09 % (3803636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.32/40.09 % (3803636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.32/40.09 % (3803636)CaDiCaL version: 2.1.3 % 278.32/40.09 % (3803636)Termination reason: Instruction limit % 278.32/40.09 % (3803636)Termination phase: Saturation % 278.32/40.09 % (3803636)Time elapsed: 0.768 s % 278.32/40.09 % (3803636)Peak memory usage: 139 MB % 278.32/40.09 % (3803636)Instructions burned: 2333 (million) % 278.32/40.09 % (3803638)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2122419036:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2760 on theBenchmark for (2760ds/7592Mi) % 278.32/40.09 % (3803630)Instruction limit reached! % 278.32/40.09 % (3803630)------------------------------ % 278.32/40.09 % (3803630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.32/40.09 % (3803630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.32/40.09 % (3803630)CaDiCaL version: 2.1.3 % 278.32/40.09 % (3803630)Termination reason: Instruction limit % 278.32/40.09 % (3803630)Termination phase: Saturation % 278.32/40.09 % (3803630)Time elapsed: 2.515 s % 278.32/40.09 % (3803630)Peak memory usage: 148 MB % 278.32/40.09 % (3803630)Instructions burned: 4273 (million) % 278.32/40.09 % (3803640)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=2387765991:i=2693:kws=precedence:ins=1:av=off_2755 on theBenchmark for (2755ds/2693Mi) % 278.32/40.09 % (3803610)Instruction limit reached! % 278.32/40.09 % (3803610)------------------------------ % 278.32/40.09 % (3803610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.32/40.09 % (3803610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.32/40.09 % (3803610)CaDiCaL version: 2.1.3 % 278.32/40.09 % (3803610)Termination reason: Instruction limit % 278.32/40.09 % (3803610)Termination phase: Saturation % 278.32/40.09 % (3803610)Time elapsed: 8.261 s % 278.32/40.09 % (3803610)Peak memory usage: 259 MB % 278.32/40.09 % (3803610)Instructions burned: 13943 (million) % 278.32/40.09 % (3803642)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2768469811:i=28651:sd=4:ss=included:sgt=64_2746 on theBenchmark for (2746ds/28651Mi) % 278.32/40.09 % (3803634)Instruction limit reached! % 278.32/40.09 % (3803634)------------------------------ % 278.32/40.09 % (3803634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.32/40.09 % (3803634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.32/40.09 % (3803634)CaDiCaL version: 2.1.3 % 278.32/40.09 % (3803634)Termination reason: Instruction limit % 278.32/40.09 % (3803634)Termination phase: Saturation % 278.32/40.09 % (3803634)Time elapsed: 3.288 s % 278.32/40.09 % (3803634)Peak memory usage: 149 MB % 278.32/40.09 % (3803634)Instructions burned: 6509 (million) % 278.32/40.09 % (3803640)Instruction limit reached! % 278.32/40.09 % (3803640)------------------------------ % 278.32/40.09 % (3803640)Version: Vampire 5.0.1 (Release buiTerminated %------------------------------------------------------------------------------