%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM119-1 : TPTP v9.3.1. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:11:46 PM UTC 2026 % Result : Timeout 300.41s 43.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM119-1 : TPTP v9.3.1. Bugfixed v2.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.38 % Computer : n020.cluster.edu % 0.11/0.38 % Model : x86_64 x86_64 % 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.38 % Memory : 8046.5625MB % 0.11/0.38 % OS : Linux 6.8.0-71-generic % 0.11/0.38 % CPULimit : 300 % 0.11/0.38 % WCLimit : 300 % 0.11/0.38 % DateTime : Sun Sep 27 18:57:50 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 % 9.76/2.26 % (3682409)Input is clausal, will run a generic CNF schedule. % 9.76/2.26 % (3682418)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=515813025:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 9.76/2.26 % (3682417)lrs+10_1_sil=8000:sp=occurrence:random_seed=4285814237:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 9.76/2.26 % (3682415)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=15808736:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 9.76/2.26 % (3682416)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3304510043:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 9.76/2.26 % (3682414)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=558453841:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 9.76/2.26 % (3682418)Instruction limit reached! % 9.76/2.26 % (3682418)------------------------------ % 9.76/2.26 % (3682418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.26 % (3682418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.26 % (3682418)CaDiCaL version: 2.1.3 % 9.76/2.26 % (3682418)Termination reason: Instruction limit % 9.76/2.26 % (3682418)Termination phase: Saturation % 9.76/2.26 % (3682418)Time elapsed: 0.039 s % 9.76/2.26 % (3682418)Peak memory usage: 89 MB % 9.76/2.26 % (3682418)Instructions burned: 116 (million) % 9.76/2.26 % (3682420)dis-21_1_sil=8000:lcm=predicate:random_seed=3369349955:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 9.76/2.26 % (3682419)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1907180151:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 9.76/2.26 % (3682417)Instruction limit reached! % 9.76/2.26 % (3682417)------------------------------ % 9.76/2.26 % (3682417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.26 % (3682417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.26 % (3682417)CaDiCaL version: 2.1.3 % 9.76/2.26 % (3682417)Termination reason: Instruction limit % 9.76/2.26 % (3682417)Termination phase: Saturation % 9.76/2.26 % (3682417)Time elapsed: 0.068 s % 9.76/2.26 % (3682417)Peak memory usage: 89 MB % 9.76/2.26 % (3682417)Instructions burned: 107 (million) % 9.76/2.26 % (3682420)Instruction limit reached! % 9.76/2.26 % (3682420)------------------------------ % 9.76/2.26 % (3682420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.26 % (3682420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.26 % (3682420)CaDiCaL version: 2.1.3 % 9.76/2.26 % (3682420)Termination reason: Instruction limit % 9.76/2.26 % (3682420)Termination phase: Saturation % 9.76/2.26 % (3682420)Time elapsed: 0.060 s % 9.76/2.26 % (3682420)Peak memory usage: 89 MB % 9.76/2.26 % (3682420)Instructions burned: 118 (million) % 9.76/2.26 % (3682427)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=3137681972:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 9.76/2.26 % (3682427)Refutation not found, incomplete strategy % 9.76/2.26 % (3682427)------------------------------ % 9.76/2.26 % (3682427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.26 % (3682427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.26 % (3682427)CaDiCaL version: 2.1.3 % 9.76/2.26 % (3682427)Termination reason: Refutation not found, incomplete strategy % 9.76/2.26 % (3682427)Time elapsed: 0.002 s % 9.76/2.26 % (3682427)Peak memory usage: 88 MB % 9.76/2.26 % (3682427)Instructions burned: 5 (million) % 9.76/2.26 % (3682419)Instruction limit reached! % 9.76/2.26 % (3682419)------------------------------ % 9.76/2.26 % (3682419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.26 % (3682419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.26 % (3682419)CaDiCaL version: 2.1.3 % 9.76/2.26 % (3682419)Termination reason: Instruction limit % 9.76/2.26 % (3682419)Termination phase: Saturation % 9.76/2.26 % (3682419)Time elapsed: 0.138 s % 9.76/2.26 % (3682419)Peak memory usage: 91 MB % 9.76/2.26 % (3682419)Instructions burned: 181 (million) % 9.76/2.26 % (3682429)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=160623658: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) % 18.63/3.54 % (3682430)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2695569905:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 18.63/3.54 % (3682430)Refutation not found, incomplete strategy % 18.63/3.54 % (3682430)------------------------------ % 18.63/3.54 % (3682430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.54 % (3682430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.54 % (3682430)CaDiCaL version: 2.1.3 % 18.63/3.54 % (3682430)Termination reason: Refutation not found, incomplete strategy % 18.63/3.54 % (3682430)Time elapsed: 0.004 s % 18.63/3.54 % (3682430)Peak memory usage: 88 MB % 18.63/3.54 % (3682430)Instructions burned: 4 (million) % 18.63/3.54 % (3682427)------------------------------ % 18.63/3.54 % (3682427)------------------------------ % 18.63/3.54 % (3682429)Instruction limit reached! % 18.63/3.54 % (3682429)------------------------------ % 18.63/3.54 % (3682429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.54 % (3682429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.54 % (3682429)CaDiCaL version: 2.1.3 % 18.63/3.54 % (3682429)Termination reason: Instruction limit % 18.63/3.54 % (3682429)Termination phase: Saturation % 18.63/3.54 % (3682429)Time elapsed: 0.108 s % 18.63/3.54 % (3682429)Peak memory usage: 90 MB % 18.63/3.54 % (3682429)Instructions burned: 190 (million) % 18.63/3.54 % (3682432)lrs+10_64_to=lpo:sil=8000:random_seed=4179701492:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 18.63/3.54 % (3682435)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4170910341:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 18.63/3.54 % (3682432)Instruction limit reached! % 18.63/3.54 % (3682432)------------------------------ % 18.63/3.54 % (3682432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.54 % (3682432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.54 % (3682432)CaDiCaL version: 2.1.3 % 18.63/3.54 % (3682432)Termination reason: Instruction limit % 18.63/3.54 % (3682432)Termination phase: Saturation % 18.63/3.54 % (3682432)Time elapsed: 0.080 s % 18.63/3.54 % (3682432)Peak memory usage: 89 MB % 18.63/3.54 % (3682432)Instructions burned: 126 (million) % 18.63/3.54 % (3682435)Instruction limit reached! % 18.63/3.54 % (3682435)------------------------------ % 18.63/3.54 % (3682435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.54 % (3682435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.54 % (3682435)CaDiCaL version: 2.1.3 % 18.63/3.54 % (3682435)Termination reason: Instruction limit % 18.63/3.54 % (3682435)Termination phase: Saturation % 18.63/3.54 % (3682435)Time elapsed: 0.060 s % 18.63/3.54 % (3682435)Peak memory usage: 90 MB % 18.63/3.54 % (3682435)Instructions burned: 194 (million) % 18.63/3.54 % (3682437)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3621962187:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 18.63/3.54 % (3682430)------------------------------ % 18.63/3.54 % (3682430)------------------------------ % 18.63/3.54 % (3682440)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=2858507200:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 18.63/3.54 % (3682439)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1331025327:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 18.63/3.54 % (3682437)Instruction limit reached! % 18.63/3.54 % (3682437)------------------------------ % 18.63/3.54 % (3682437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.63/3.54 % (3682437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.63/3.54 % (3682437)CaDiCaL version: 2.1.3 % 18.63/3.54 % (3682437)Termination reason: Instruction limit % 18.63/3.54 % (3682437)Termination phase: Saturation % 18.63/3.54 % (3682437)Time elapsed: 0.115 s % 18.63/3.54 % (3682437)Peak memory usage: 91 MB % 18.63/3.54 % (3682437)Instructions burned: 157 (million) % 18.63/3.54 % (3682440)Instruction limit reached! % 18.63/3.54 % (3682440)------------------------------ % 18.63/3.54 % (3682440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.53/4.97 % (3682440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.53/4.97 % (3682440)CaDiCaL version: 2.1.3 % 28.53/4.97 % (3682440)Termination reason: Instruction limit % 28.53/4.97 % (3682440)Termination phase: Saturation % 28.53/4.97 % (3682440)Time elapsed: 0.035 s % 28.53/4.97 % (3682440)Peak memory usage: 89 MB % 28.53/4.97 % (3682440)Instructions burned: 106 (million) % 28.53/4.97 % (3682442)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1762407771:i=107_2993 on theBenchmark for (2993ds/107Mi) % 28.53/4.97 % (3682446)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3102830113:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi) % 28.53/4.97 % (3682442)Instruction limit reached! % 28.53/4.97 % (3682442)------------------------------ % 28.53/4.97 % (3682442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.53/4.97 % (3682442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.53/4.97 % (3682442)CaDiCaL version: 2.1.3 % 28.53/4.98 % (3682442)Termination reason: Instruction limit % 28.53/4.98 % (3682442)Termination phase: Saturation % 28.53/4.98 % (3682442)Time elapsed: 0.068 s % 28.53/4.98 % (3682442)Peak memory usage: 89 MB % 28.53/4.98 % (3682442)Instructions burned: 107 (million) % 28.53/4.98 % (3682445)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=687146828:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi) % 28.53/4.98 % (3682450)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3752823367:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi) % 28.53/4.98 % (3682445)Instruction limit reached! % 28.53/4.98 % (3682445)------------------------------ % 28.53/4.98 % (3682445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.53/4.98 % (3682445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.53/4.98 % (3682445)CaDiCaL version: 2.1.3 % 28.53/4.98 % (3682445)Termination reason: Instruction limit % 28.53/4.98 % (3682445)Termination phase: Saturation % 28.53/4.98 % (3682445)Time elapsed: 0.165 s % 28.53/4.98 % (3682445)Peak memory usage: 90 MB % 28.53/4.98 % (3682445)Instructions burned: 242 (million) % 28.53/4.98 % (3682450)Instruction limit reached! % 28.53/4.98 % (3682450)------------------------------ % 28.53/4.98 % (3682450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.53/4.98 % (3682450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.53/4.98 % (3682450)CaDiCaL version: 2.1.3 % 28.53/4.98 % (3682450)Termination reason: Instruction limit % 28.53/4.98 % (3682450)Termination phase: Saturation % 28.53/4.98 % (3682450)Time elapsed: 0.071 s % 28.53/4.98 % (3682450)Peak memory usage: 90 MB % 28.53/4.98 % (3682450)Instructions burned: 134 (million) % 28.53/4.98 % (3682452)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3320530924:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi) % 28.53/4.98 % (3682453)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=862862447:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi) % 28.53/4.98 % (3682453)Instruction limit reached! % 28.53/4.98 % (3682453)------------------------------ % 28.53/4.98 % (3682453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.53/4.98 % (3682453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.53/4.98 % (3682453)CaDiCaL version: 2.1.3 % 28.53/4.98 % (3682453)Termination reason: Instruction limit % 28.53/4.98 % (3682453)Termination phase: Saturation % 28.53/4.98 % (3682453)Time elapsed: 0.111 s % 28.53/4.98 % (3682453)Peak memory usage: 90 MB % 28.53/4.98 % (3682453)Instructions burned: 192 (million) % 28.53/4.98 % (3682456)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3682854912:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi) % 28.53/4.98 % (3682452)Instruction limit reached! % 28.53/4.98 % (3682452)------------------------------ % 28.53/4.98 % (3682452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.53/4.98 % (3682452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.53/4.98 % (3682452)CaDiCaL version: 2.1.3 % 28.53/4.98 % (3682452)Termination reason: Instruction limit % 28.53/4.98 % (3682452)Termination phase: Saturation % 28.53/4.98 % (3682452)Time elapsed: 0.299 s % 48.02/7.79 % (3682452)Peak memory usage: 96 MB % 48.02/7.79 % (3682452)Instructions burned: 500 (million) % 48.02/7.79 % (3682458)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3164995869:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi) % 48.02/7.79 % (3682456)Instruction limit reached! % 48.02/7.79 % (3682456)------------------------------ % 48.02/7.79 % (3682456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.02/7.79 % (3682456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.02/7.79 % (3682456)CaDiCaL version: 2.1.3 % 48.02/7.79 % (3682456)Termination reason: Instruction limit % 48.02/7.79 % (3682456)Termination phase: Saturation % 48.02/7.79 % (3682456)Time elapsed: 0.158 s % 48.02/7.79 % (3682456)Peak memory usage: 92 MB % 48.02/7.79 % (3682456)Instructions burned: 265 (million) % 48.02/7.79 % (3682458)Instruction limit reached! % 48.02/7.79 % (3682458)------------------------------ % 48.02/7.79 % (3682458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.02/7.79 % (3682458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.02/7.79 % (3682458)CaDiCaL version: 2.1.3 % 48.02/7.79 % (3682458)Termination reason: Instruction limit % 48.02/7.79 % (3682458)Termination phase: Saturation % 48.02/7.79 % (3682458)Time elapsed: 0.107 s % 48.02/7.79 % (3682458)Peak memory usage: 89 MB % 48.02/7.79 % (3682458)Instructions burned: 156 (million) % 48.02/7.79 % (3682460)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=3679973006:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi) % 48.02/7.79 % (3682461)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3940113564:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi) % 48.02/7.79 % (3682461)Instruction limit reached! % 48.02/7.79 % (3682461)------------------------------ % 48.02/7.79 % (3682461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.02/7.79 % (3682461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.02/7.79 % (3682461)CaDiCaL version: 2.1.3 % 48.02/7.79 % (3682461)Termination reason: Instruction limit % 48.02/7.79 % (3682461)Termination phase: Saturation % 48.02/7.79 % (3682461)Time elapsed: 0.266 s % 48.02/7.79 % (3682461)Peak memory usage: 89 MB % 48.02/7.79 % (3682461)Instructions burned: 539 (million) % 48.02/7.79 % (3682464)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=901430752:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi) % 48.02/7.79 % (3682464)Instruction limit reached! % 48.02/7.79 % (3682464)------------------------------ % 48.02/7.79 % (3682464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.02/7.79 % (3682464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.02/7.79 % (3682464)CaDiCaL version: 2.1.3 % 48.02/7.79 % (3682464)Termination reason: Instruction limit % 48.02/7.79 % (3682464)Termination phase: Saturation % 48.02/7.79 % (3682464)Time elapsed: 0.092 s % 48.02/7.79 % (3682464)Peak memory usage: 90 MB % 48.02/7.79 % (3682464)Instructions burned: 182 (million) % 48.02/7.79 % (3682466)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=3640611239:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi) % 48.02/7.79 % (3682446)Instruction limit reached! % 48.02/7.79 % (3682446)------------------------------ % 48.02/7.79 % (3682446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.02/7.79 % (3682446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.02/7.79 % (3682446)CaDiCaL version: 2.1.3 % 48.02/7.79 % (3682446)Termination reason: Instruction limit % 48.02/7.79 % (3682446)Termination phase: Saturation % 48.02/7.79 % (3682446)Time elapsed: 1.780 s % 48.02/7.79 % (3682446)Peak memory usage: 155 MB % 48.02/7.79 % (3682446)Instructions burned: 5208 (million) % 48.02/7.79 % (3682468)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=3254859730:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi) % 48.02/7.79 % (3682439)Instruction limit reached! % 48.02/7.79 % (3682439)------------------------------ % 48.02/7.79 % (3682439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.02/7.79 % (3682439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.27/10.51 % (3682439)CaDiCaL version: 2.1.3 % 67.27/10.51 % (3682439)Termination reason: Instruction limit % 67.27/10.51 % (3682439)Termination phase: Saturation % 67.27/10.51 % (3682439)Time elapsed: 2.014 s % 67.27/10.51 % (3682439)Peak memory usage: 141 MB % 67.27/10.51 % (3682439)Instructions burned: 3395 (million) % 67.27/10.51 % (3682468)Instruction limit reached! % 67.27/10.51 % (3682468)------------------------------ % 67.27/10.51 % (3682468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.27/10.51 % (3682468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.27/10.51 % (3682468)CaDiCaL version: 2.1.3 % 67.27/10.51 % (3682468)Termination reason: Instruction limit % 67.27/10.51 % (3682468)Termination phase: Saturation % 67.27/10.51 % (3682468)Time elapsed: 0.099 s % 67.27/10.51 % (3682468)Peak memory usage: 90 MB % 67.27/10.51 % (3682468)Instructions burned: 414 (million) % 67.27/10.51 % (3682470)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=1915371826:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi) % 67.27/10.51 % (3682471)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=4107472663:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2972 on theBenchmark for (2972ds/303Mi) % 67.27/10.51 % (3682471)Refutation not found, incomplete strategy % 67.27/10.51 % (3682471)------------------------------ % 67.27/10.51 % (3682471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.27/10.51 % (3682471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.27/10.51 % (3682471)CaDiCaL version: 2.1.3 % 67.27/10.51 % (3682471)Termination reason: Refutation not found, incomplete strategy % 67.27/10.51 % (3682471)Time elapsed: 0.002 s % 67.27/10.51 % (3682471)Peak memory usage: 88 MB % 67.27/10.51 % (3682471)Instructions burned: 1 (million) % 67.27/10.51 % (3682471)------------------------------ % 67.27/10.51 % (3682471)------------------------------ % 67.27/10.51 % (3682474)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3341567935:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi) % 67.27/10.51 % (3682460)Instruction limit reached! % 67.27/10.51 % (3682460)------------------------------ % 67.27/10.51 % (3682460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.27/10.51 % (3682460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.27/10.51 % (3682460)CaDiCaL version: 2.1.3 % 67.27/10.51 % (3682460)Termination reason: Instruction limit % 67.27/10.51 % (3682460)Termination phase: Saturation % 67.27/10.51 % (3682460)Time elapsed: 1.805 s % 67.27/10.51 % (3682460)Peak memory usage: 152 MB % 67.27/10.51 % (3682460)Instructions burned: 3258 (million) % 67.27/10.51 % (3682476)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3238898469:i=598:bs=on:bd=preordered:av=off:ss=axioms_2964 on theBenchmark for (2964ds/598Mi) % 67.27/10.51 % (3682474)Instruction limit reached! % 67.27/10.51 % (3682474)------------------------------ % 67.27/10.51 % (3682474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.27/10.51 % (3682474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.27/10.51 % (3682474)CaDiCaL version: 2.1.3 % 67.27/10.51 % (3682474)Termination reason: Instruction limit % 67.27/10.51 % (3682474)Termination phase: Saturation % 67.27/10.51 % (3682474)Time elapsed: 0.391 s % 67.27/10.51 % (3682474)Peak memory usage: 98 MB % 67.27/10.51 % (3682474)Instructions burned: 721 (million) % 67.27/10.51 % (3682478)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4131617239:i=2989:sd=3:ss=axioms:sgt=60_2963 on theBenchmark for (2963ds/2989Mi) % 67.27/10.51 % (3682476)Instruction limit reached! % 67.27/10.51 % (3682476)------------------------------ % 67.27/10.51 % (3682476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.27/10.51 % (3682476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.27/10.51 % (3682476)CaDiCaL version: 2.1.3 % 67.27/10.51 % (3682476)Termination reason: Instruction limit % 67.27/10.51 % (3682476)Termination phase: Saturation % 67.27/10.51 % (3682476)Time elapsed: 0.349 s % 67.27/10.51 % (3682476)Peak memory usage: 92 MB % 67.27/10.51 % (3682476)Instructions burned: 599 (million) % 67.27/10.51 % (3682480)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=2086660762:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2960 on theBenchmark for (2960ds/1997Mi) % 90.39/13.67 % (3682480)Instruction limit reached! % 90.39/13.67 % (3682480)------------------------------ % 90.39/13.67 % (3682480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.39/13.67 % (3682480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.39/13.67 % (3682480)CaDiCaL version: 2.1.3 % 90.39/13.67 % (3682480)Termination reason: Instruction limit % 90.39/13.67 % (3682480)Termination phase: Saturation % 90.39/13.67 % (3682480)Time elapsed: 1.324 s % 90.39/13.67 % (3682480)Peak memory usage: 137 MB % 90.39/13.67 % (3682480)Instructions burned: 1999 (million) % 90.39/13.67 % (3682478)Instruction limit reached! % 90.39/13.67 % (3682478)------------------------------ % 90.39/13.67 % (3682478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.39/13.67 % (3682478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.39/13.67 % (3682478)CaDiCaL version: 2.1.3 % 90.39/13.67 % (3682478)Termination reason: Instruction limit % 90.39/13.67 % (3682478)Termination phase: Saturation % 90.39/13.67 % (3682478)Time elapsed: 1.781 s % 90.39/13.67 % (3682478)Peak memory usage: 141 MB % 90.39/13.67 % (3682478)Instructions burned: 2990 (million) % 90.39/13.67 % (3682483)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=3987525201:i=2088:bd=preordered:av=off_2945 on theBenchmark for (2945ds/2088Mi) % 90.39/13.67 % (3682484)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=388201043:i=1098:nicw=on_2944 on theBenchmark for (2944ds/1098Mi) % 90.39/13.67 % (3682466)Instruction limit reached! % 90.39/13.67 % (3682466)------------------------------ % 90.39/13.67 % (3682466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.39/13.67 % (3682466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.39/13.67 % (3682466)CaDiCaL version: 2.1.3 % 90.39/13.67 % (3682466)Termination reason: Instruction limit % 90.39/13.67 % (3682466)Termination phase: Saturation % 90.39/13.67 % (3682466)Time elapsed: 3.848 s % 90.39/13.67 % (3682466)Peak memory usage: 168 MB % 90.39/13.67 % (3682466)Instructions burned: 10310 (million) % 90.39/13.67 % (3682487)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2603375431:i=433:bd=preordered_2937 on theBenchmark for (2937ds/433Mi) % 90.39/13.67 % (3682487)Refutation not found, incomplete strategy % 90.39/13.67 % (3682487)------------------------------ % 90.39/13.67 % (3682487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.39/13.67 % (3682487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.39/13.67 % (3682487)CaDiCaL version: 2.1.3 % 90.39/13.67 % (3682487)Termination reason: Refutation not found, incomplete strategy % 90.39/13.67 % (3682487)Time elapsed: 0.007 s % 90.39/13.67 % (3682487)Peak memory usage: 88 MB % 90.39/13.67 % (3682487)Instructions burned: 21 (million) % 90.39/13.67 % (3682484)Instruction limit reached! % 90.39/13.67 % (3682484)------------------------------ % 90.39/13.67 % (3682484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.39/13.67 % (3682484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.39/13.67 % (3682484)CaDiCaL version: 2.1.3 % 90.39/13.67 % (3682484)Termination reason: Instruction limit % 90.39/13.67 % (3682484)Termination phase: Saturation % 90.39/13.67 % (3682484)Time elapsed: 0.718 s % 90.39/13.67 % (3682484)Peak memory usage: 103 MB % 90.39/13.67 % (3682484)Instructions burned: 1178 (million) % 90.39/13.67 % (3682487)------------------------------ % 90.39/13.67 % (3682487)------------------------------ % 90.39/13.67 % (3682489)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2208169115:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2935 on theBenchmark for (2935ds/2942Mi) % 90.39/13.67 % (3682490)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1060579250:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2935 on theBenchmark for (2935ds/6922Mi) % 90.39/13.67 % (3682483)Instruction limit reached! % 90.39/13.67 % (3682483)------------------------------ % 90.39/13.67 % (3682483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.39/13.67 % (3682483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.69/16.63 % (3682483)CaDiCaL version: 2.1.3 % 111.69/16.63 % (3682483)Termination reason: Instruction limit % 111.69/16.63 % (3682483)Termination phase: Saturation % 111.69/16.63 % (3682483)Time elapsed: 1.345 s % 111.69/16.63 % (3682483)Peak memory usage: 137 MB % 111.69/16.63 % (3682483)Instructions burned: 2088 (million) % 111.69/16.63 % (3682470)Instruction limit reached! % 111.69/16.63 % (3682470)------------------------------ % 111.69/16.63 % (3682470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.69/16.63 % (3682470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.69/16.63 % (3682470)CaDiCaL version: 2.1.3 % 111.69/16.63 % (3682470)Termination reason: Instruction limit % 111.69/16.63 % (3682470)Termination phase: Saturation % 111.69/16.63 % (3682470)Time elapsed: 4.249 s % 111.69/16.63 % (3682470)Peak memory usage: 178 MB % 111.69/16.63 % (3682470)Instructions burned: 8481 (million) % 111.69/16.63 % (3682493)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=2641214983:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2930 on theBenchmark for (2930ds/596Mi) % 111.69/16.64 % (3682495)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=2823343637:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2929 on theBenchmark for (2929ds/4123Mi) % 111.69/16.64 % (3682493)Instruction limit reached! % 111.69/16.64 % (3682493)------------------------------ % 111.69/16.64 % (3682493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.69/16.64 % (3682493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.69/16.64 % (3682493)CaDiCaL version: 2.1.3 % 111.69/16.64 % (3682493)Termination reason: Instruction limit % 111.69/16.64 % (3682493)Termination phase: Saturation % 111.69/16.64 % (3682493)Time elapsed: 0.319 s % 111.69/16.64 % (3682493)Peak memory usage: 99 MB % 111.69/16.64 % (3682493)Instructions burned: 597 (million) % 111.69/16.64 % (3682497)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4023938690:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2926 on theBenchmark for (2926ds/16411Mi) % 111.69/16.64 % (3682489)Instruction limit reached! % 111.69/16.64 % (3682489)------------------------------ % 111.69/16.64 % (3682489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.69/16.64 % (3682489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.69/16.64 % (3682489)CaDiCaL version: 2.1.3 % 111.69/16.64 % (3682489)Termination reason: Instruction limit % 111.69/16.64 % (3682489)Termination phase: Saturation % 111.69/16.64 % (3682489)Time elapsed: 1.905 s % 111.69/16.64 % (3682489)Peak memory usage: 146 MB % 111.69/16.64 % (3682489)Instructions burned: 2943 (million) % 111.69/16.64 % (3682499)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2789530446:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2915 on theBenchmark for (2915ds/1670Mi) % 111.69/16.64 % (3682490)Instruction limit reached! % 111.69/16.64 % (3682490)------------------------------ % 111.69/16.64 % (3682490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.69/16.64 % (3682490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.69/16.64 % (3682490)CaDiCaL version: 2.1.3 % 111.69/16.64 % (3682490)Termination reason: Instruction limit % 111.69/16.64 % (3682490)Termination phase: Saturation % 111.69/16.64 % (3682490)Time elapsed: 2.169 s % 111.69/16.64 % (3682490)Peak memory usage: 171 MB % 111.69/16.64 % (3682490)Instructions burned: 6923 (million) % 111.69/16.64 % (3682501)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=3194629944:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2910 on theBenchmark for (2910ds/1722Mi) % 111.69/16.64 % (3682499)Instruction limit reached! % 111.69/16.64 % (3682499)------------------------------ % 111.69/16.64 % (3682499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.69/16.64 % (3682499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.69/16.64 % (3682499)CaDiCaL version: 2.1.3 % 111.69/16.64 % (3682499)Termination reason: Instruction limit % 111.69/16.64 % (3682499)Termination phase: Saturation % 111.69/16.64 % (3682499)Time elapsed: 1.042 s % 111.69/16.64 % (3682499)Peak memory usage: 137 MB % 111.69/16.64 % (3682499)Instructions burned: 1671 (million) % 111.69/16.64 % (3682501)Instruction limit reached! % 133.60/19.81 % (3682501)------------------------------ % 133.60/19.81 % (3682501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.81 % (3682501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.81 % (3682501)CaDiCaL version: 2.1.3 % 133.60/19.81 % (3682501)Termination reason: Instruction limit % 133.60/19.81 % (3682501)Termination phase: Saturation % 133.60/19.81 % (3682501)Time elapsed: 0.626 s % 133.60/19.81 % (3682501)Peak memory usage: 134 MB % 133.60/19.81 % (3682501)Instructions burned: 1723 (million) % 133.60/19.81 % (3682623)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=403847618:st=2:i=4495:sd=10:ss=included_2903 on theBenchmark for (2903ds/4495Mi) % 133.60/19.81 % (3682495)Instruction limit reached! % 133.60/19.81 % (3682495)------------------------------ % 133.60/19.81 % (3682495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.81 % (3682495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.81 % (3682495)CaDiCaL version: 2.1.3 % 133.60/19.81 % (3682495)Termination reason: Instruction limit % 133.60/19.81 % (3682495)Termination phase: Saturation % 133.60/19.81 % (3682495)Time elapsed: 2.547 s % 133.60/19.81 % (3682495)Peak memory usage: 156 MB % 133.60/19.81 % (3682495)Instructions burned: 4124 (million) % 133.60/19.81 % (3682622)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=4149677118:cts=off:cond=on:i=9530:bs=on:fsd=on_2903 on theBenchmark for (2903ds/9530Mi) % 133.60/19.81 % (3682626)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=1164220417:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2902 on theBenchmark for (2902ds/4920Mi) % 133.60/19.81 % (3682623)Instruction limit reached! % 133.60/19.81 % (3682623)------------------------------ % 133.60/19.81 % (3682623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.81 % (3682623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.81 % (3682623)CaDiCaL version: 2.1.3 % 133.60/19.81 % (3682623)Termination reason: Instruction limit % 133.60/19.81 % (3682623)Termination phase: Saturation % 133.60/19.81 % (3682623)Time elapsed: 1.537 s % 133.60/19.81 % (3682623)Peak memory usage: 160 MB % 133.60/19.81 % (3682623)Instructions burned: 4496 (million) % 133.60/19.81 % (3682628)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=584771518:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2887 on theBenchmark for (2887ds/2083Mi) % 133.60/19.81 % (3682628)Instruction limit reached! % 133.60/19.81 % (3682628)------------------------------ % 133.60/19.81 % (3682628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.81 % (3682628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.81 % (3682628)CaDiCaL version: 2.1.3 % 133.60/19.81 % (3682628)Termination reason: Instruction limit % 133.60/19.81 % (3682628)Termination phase: Saturation % 133.60/19.81 % (3682628)Time elapsed: 0.730 s % 133.60/19.81 % (3682628)Peak memory usage: 138 MB % 133.60/19.81 % (3682628)Instructions burned: 2085 (million) % 133.60/19.81 % (3682630)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=3637786791:i=4629:av=off:gsp=on_2878 on theBenchmark for (2878ds/4629Mi) % 133.60/19.81 % (3682630)Refutation not found, incomplete strategy % 133.60/19.81 % (3682630)------------------------------ % 133.60/19.81 % (3682630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.60/19.81 % (3682630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.60/19.81 % (3682630)CaDiCaL version: 2.1.3 % 133.60/19.81 % (3682630)Termination reason: Refutation not found, incomplete strategy % 133.60/19.81 % (3682630)Time elapsed: 0.362 s % 133.60/19.81 % (3682630)Peak memory usage: 130 MB % 133.60/19.81 % (3682630)Instructions burned: 927 (million) % 133.60/19.81 % (3682630)------------------------------ % 133.60/19.81 % (3682630)------------------------------ % 133.60/19.81 % (3682696)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=654601106:i=1258:av=off_2872 on theBenchmark for (2872ds/1258Mi) % 133.60/19.81 % (3682626)Instruction limit reached! % 133.60/19.81 % (3682626)------------------------------ % 151.90/22.39 % (3682626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.90/22.39 % (3682626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.90/22.39 % (3682626)CaDiCaL version: 2.1.3 % 151.90/22.39 % (3682626)Termination reason: Instruction limit % 151.90/22.39 % (3682626)Termination phase: Saturation % 151.90/22.39 % (3682626)Time elapsed: 2.928 s % 151.90/22.39 % (3682626)Peak memory usage: 145 MB % 151.90/22.39 % (3682626)Instructions burned: 4921 (million) % 151.90/22.39 % (3682750)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2480221567:i=7343:av=off:ss=included_2871 on theBenchmark for (2871ds/7343Mi) % 151.90/22.39 % (3682696)Instruction limit reached! % 151.90/22.39 % (3682696)------------------------------ % 151.90/22.39 % (3682696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.90/22.39 % (3682696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.90/22.39 % (3682696)CaDiCaL version: 2.1.3 % 151.90/22.39 % (3682696)Termination reason: Instruction limit % 151.90/22.39 % (3682696)Termination phase: Saturation % 151.90/22.39 % (3682696)Time elapsed: 0.345 s % 151.90/22.39 % (3682696)Peak memory usage: 95 MB % 151.90/22.39 % (3682696)Instructions burned: 1260 (million) % 151.90/22.39 % (3682867)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2162837053:i=1325:sd=2:ss=axioms:sgt=16_2868 on theBenchmark for (2868ds/1325Mi) % 151.90/22.39 % (3682867)Refutation not found, incomplete strategy % 151.90/22.39 % (3682867)------------------------------ % 151.90/22.39 % (3682867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.90/22.39 % (3682867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.90/22.39 % (3682867)CaDiCaL version: 2.1.3 % 151.90/22.39 % (3682867)Termination reason: Refutation not found, incomplete strategy % 151.90/22.39 % (3682867)Time elapsed: 0.002 s % 151.90/22.39 % (3682867)Peak memory usage: 88 MB % 151.90/22.39 % (3682867)Instructions burned: 5 (million) % 151.90/22.39 % (3682867)------------------------------ % 151.90/22.39 % (3682867)------------------------------ % 151.90/22.39 % (3682884)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=803381516:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2866 on theBenchmark for (2866ds/2646Mi) % 151.90/22.39 % (3682884)Instruction limit reached! % 151.90/22.39 % (3682884)------------------------------ % 151.90/22.39 % (3682884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.90/22.39 % (3682884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.90/22.39 % (3682884)CaDiCaL version: 2.1.3 % 151.90/22.39 % (3682884)Termination reason: Instruction limit % 151.90/22.39 % (3682884)Termination phase: Saturation % 151.90/22.39 % (3682884)Time elapsed: 1.010 s % 151.90/22.39 % (3682884)Peak memory usage: 143 MB % 151.90/22.39 % (3682884)Instructions burned: 2648 (million) % 151.90/22.39 % (3682917)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2358287985:i=1489:sd=2:ep=R:ss=axioms_2855 on theBenchmark for (2855ds/1489Mi) % 151.90/22.39 % (3682917)Instruction limit reached! % 151.90/22.39 % (3682917)------------------------------ % 151.90/22.39 % (3682917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.90/22.39 % (3682917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.90/22.39 % (3682917)CaDiCaL version: 2.1.3 % 151.90/22.39 % (3682917)Termination reason: Instruction limit % 151.90/22.39 % (3682917)Termination phase: Saturation % 151.90/22.39 % (3682917)Time elapsed: 0.514 s % 151.90/22.39 % (3682917)Peak memory usage: 135 MB % 151.90/22.39 % (3682917)Instructions burned: 1490 (million) % 151.90/22.39 % (3682919)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=3604512298:i=1503_2848 on theBenchmark for (2848ds/1503Mi) % 151.90/22.39 % (3682919)Instruction limit reached! % 151.90/22.39 % (3682919)------------------------------ % 151.90/22.39 % (3682919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.90/22.39 % (3682919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.90/22.39 % (3682919)CaDiCaL version: 2.1.3 % 151.90/22.39 % (3682919)Termination reason: Instruction limit % 151.90/22.39 % (3682919)Termination phase: Saturation % 151.90/22.39 % (3682919)Time elapsed: 0.580 s % 151.90/22.39 % (3682919)Peak memory usage: 135 MB % 151.90/22.39 % (3682919)Instructions burned: 1505 (million) % 171.49/25.12 % (3682921)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3560731455:i=13942:kws=frequency_2842 on theBenchmark for (2842ds/13942Mi) % 171.49/25.12 % (3682622)Instruction limit reached! % 171.49/25.12 % (3682622)------------------------------ % 171.49/25.12 % (3682622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.49/25.12 % (3682622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.49/25.12 % (3682622)CaDiCaL version: 2.1.3 % 171.49/25.12 % (3682622)Termination reason: Instruction limit % 171.49/25.12 % (3682622)Termination phase: Saturation % 171.49/25.12 % (3682622)Time elapsed: 6.198 s % 171.49/25.12 % (3682622)Peak memory usage: 168 MB % 171.49/25.12 % (3682622)Instructions burned: 9531 (million) % 171.49/25.12 % (3682923)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=2384269039:i=3604:fsr=off:er=filter_2840 on theBenchmark for (2840ds/3604Mi) % 171.49/25.12 % (3682750)Instruction limit reached! % 171.49/25.12 % (3682750)------------------------------ % 171.49/25.12 % (3682750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.49/25.12 % (3682750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.49/25.12 % (3682750)CaDiCaL version: 2.1.3 % 171.49/25.12 % (3682750)Termination reason: Instruction limit % 171.49/25.12 % (3682750)Termination phase: Saturation % 171.49/25.12 % (3682750)Time elapsed: 3.963 s % 171.49/25.12 % (3682750)Peak memory usage: 188 MB % 171.49/25.12 % (3682750)Instructions burned: 7344 (million) % 171.49/25.12 % (3682925)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1003609963:i=1876:sd=1:ss=included:sgt=32_2830 on theBenchmark for (2830ds/1876Mi) % 171.49/25.12 % (3682925)Refutation not found, incomplete strategy % 171.49/25.12 % (3682925)------------------------------ % 171.49/25.12 % (3682925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.49/25.12 % (3682925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.49/25.12 % (3682925)CaDiCaL version: 2.1.3 % 171.49/25.12 % (3682925)Termination reason: Refutation not found, incomplete strategy % 171.49/25.12 % (3682925)Time elapsed: 0.597 s % 171.49/25.12 % (3682925)Peak memory usage: 128 MB % 171.49/25.12 % (3682925)Instructions burned: 909 (million) % 171.49/25.12 % (3682497)Instruction limit reached! % 171.49/25.12 % (3682497)------------------------------ % 171.49/25.12 % (3682497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.49/25.12 % (3682497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.49/25.12 % (3682497)CaDiCaL version: 2.1.3 % 171.49/25.12 % (3682497)Termination reason: Instruction limit % 171.49/25.12 % (3682497)Termination phase: Saturation % 171.49/25.12 % (3682497)Time elapsed: 10.175 s % 171.49/25.12 % (3682497)Peak memory usage: 218 MB % 171.49/25.12 % (3682497)Instructions burned: 16411 (million) % 171.49/25.12 % (3682927)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1874203847:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2822 on theBenchmark for (2822ds/1932Mi) % 171.49/25.12 % (3682925)------------------------------ % 171.49/25.12 % (3682925)------------------------------ % 171.49/25.12 % (3682929)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=4182062793:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2820 on theBenchmark for (2820ds/1980Mi) % 171.49/25.12 % (3682923)Instruction limit reached! % 171.49/25.12 % (3682923)------------------------------ % 171.49/25.12 % (3682923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.49/25.12 % (3682923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.49/25.12 % (3682923)CaDiCaL version: 2.1.3 % 171.49/25.12 % (3682923)Termination reason: Instruction limit % 171.49/25.12 % (3682923)Termination phase: Saturation % 171.49/25.12 % (3682923)Time elapsed: 2.019 s % 171.49/25.12 % (3682923)Peak memory usage: 157 MB % 171.49/25.12 % (3682923)Instructions burned: 3605 (million) % 171.49/25.12 % (3682931)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=1527937752:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2818 on theBenchmark for (2818ds/3902Mi) % 171.49/25.12 % (3682927)Instruction limit reached! % 171.49/25.12 % (3682927)------------------------------ % 200.96/29.24 % (3682927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.96/29.24 % (3682927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.96/29.24 % (3682927)CaDiCaL version: 2.1.3 % 200.96/29.24 % (3682927)Termination reason: Instruction limit % 200.96/29.24 % (3682927)Termination phase: Saturation % 200.96/29.24 % (3682927)Time elapsed: 1.106 s % 200.96/29.24 % (3682927)Peak memory usage: 139 MB % 200.96/29.24 % (3682927)Instructions burned: 1933 (million) % 200.96/29.24 % (3682933)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=851450580:avsq=on:i=3916:aac=none:amm=off_2810 on theBenchmark for (2810ds/3916Mi) % 200.96/29.24 % (3682929)Instruction limit reached! % 200.96/29.24 % (3682929)------------------------------ % 200.96/29.24 % (3682929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.96/29.24 % (3682929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.96/29.24 % (3682929)CaDiCaL version: 2.1.3 % 200.96/29.24 % (3682929)Termination reason: Instruction limit % 200.96/29.24 % (3682929)Termination phase: Saturation % 200.96/29.24 % (3682929)Time elapsed: 1.254 s % 200.96/29.24 % (3682929)Peak memory usage: 138 MB % 200.96/29.24 % (3682929)Instructions burned: 1980 (million) % 200.96/29.24 % (3682935)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2473633471:cond=on:i=3940:av=off:er=known_2807 on theBenchmark for (2807ds/3940Mi) % 200.96/29.24 % (3682931)Instruction limit reached! % 200.96/29.24 % (3682931)------------------------------ % 200.96/29.24 % (3682931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.96/29.24 % (3682931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.96/29.24 % (3682931)CaDiCaL version: 2.1.3 % 200.96/29.24 % (3682931)Termination reason: Instruction limit % 200.96/29.24 % (3682931)Termination phase: Saturation % 200.96/29.24 % (3682931)Time elapsed: 2.201 s % 200.96/29.24 % (3682931)Peak memory usage: 158 MB % 200.96/29.24 % (3682931)Instructions burned: 3903 (million) % 200.96/29.24 % (3682937)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1921688831:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2795 on theBenchmark for (2795ds/3980Mi) % 200.96/29.24 % (3682921)Instruction limit reached! % 200.96/29.24 % (3682921)------------------------------ % 200.96/29.24 % (3682921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.96/29.24 % (3682921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.96/29.24 % (3682921)CaDiCaL version: 2.1.3 % 200.96/29.24 % (3682921)Termination reason: Instruction limit % 200.96/29.24 % (3682921)Termination phase: Saturation % 200.96/29.24 % (3682921)Time elapsed: 4.802 s % 200.96/29.24 % (3682921)Peak memory usage: 240 MB % 200.96/29.24 % (3682921)Instructions burned: 13943 (million) % 200.96/29.24 % (3682939)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=2278892138:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2793 on theBenchmark for (2793ds/2087Mi) % 200.96/29.24 % (3682933)Instruction limit reached! % 200.96/29.24 % (3682933)------------------------------ % 200.96/29.24 % (3682933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.96/29.24 % (3682933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.96/29.24 % (3682933)CaDiCaL version: 2.1.3 % 200.96/29.24 % (3682933)Termination reason: Instruction limit % 200.96/29.24 % (3682933)Termination phase: Saturation % 200.96/29.24 % (3682933)Time elapsed: 2.149 s % 200.96/29.24 % (3682933)Peak memory usage: 103 MB % 200.96/29.24 % (3682933)Instructions burned: 3916 (million) % 200.96/29.24 % (3682941)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=1583015581:cts=off:cond=on:i=4272:bs=on:fsd=on_2787 on theBenchmark for (2787ds/4272Mi) % 200.96/29.24 % (3682939)Instruction limit reached! % 200.96/29.24 % (3682939)------------------------------ % 200.96/29.24 % (3682939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.96/29.24 % (3682939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.96/29.24 % (3682939)CaDiCaL version: 2.1.3 % 200.96/29.24 % (3682939)Termination reason: Instruction limit % 200.96/29.24 % (3682939)Termination phase: Saturation % 243.65/35.20 % (3682939)Time elapsed: 0.766 s % 243.65/35.20 % (3682939)Peak memory usage: 139 MB % 243.65/35.20 % (3682939)Instructions burned: 2089 (million) % 243.65/35.20 % (3682943)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=221848665:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2784 on theBenchmark for (2784ds/2197Mi) % 243.65/35.20 % (3682935)Instruction limit reached! % 243.65/35.20 % (3682935)------------------------------ % 243.65/35.20 % (3682935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.65/35.20 % (3682935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.65/35.20 % (3682935)CaDiCaL version: 2.1.3 % 243.65/35.20 % (3682935)Termination reason: Instruction limit % 243.65/35.20 % (3682935)Termination phase: Saturation % 243.65/35.20 % (3682935)Time elapsed: 2.419 s % 243.65/35.20 % (3682935)Peak memory usage: 150 MB % 243.65/35.20 % (3682935)Instructions burned: 3942 (million) % 243.65/35.20 % (3682945)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2532009108:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2781 on theBenchmark for (2781ds/6508Mi) % 243.65/35.20 % (3682943)Instruction limit reached! % 243.65/35.20 % (3682943)------------------------------ % 243.65/35.20 % (3682943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.65/35.20 % (3682943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.65/35.20 % (3682943)CaDiCaL version: 2.1.3 % 243.65/35.20 % (3682943)Termination reason: Instruction limit % 243.65/35.20 % (3682943)Termination phase: Saturation % 243.65/35.20 % (3682943)Time elapsed: 0.710 s % 243.65/35.20 % (3682943)Peak memory usage: 140 MB % 243.65/35.20 % (3682943)Instructions burned: 2198 (million) % 243.65/35.20 % (3682947)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=4155358446:i=2330:fgj=on:av=off:fsr=off_2776 on theBenchmark for (2776ds/2330Mi) % 243.65/35.20 % (3682937)Instruction limit reached! % 243.65/35.20 % (3682937)------------------------------ % 243.65/35.20 % (3682937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.65/35.20 % (3682937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.65/35.20 % (3682937)CaDiCaL version: 2.1.3 % 243.65/35.20 % (3682937)Termination reason: Instruction limit % 243.65/35.20 % (3682937)Termination phase: Saturation % 243.65/35.20 % (3682937)Time elapsed: 2.507 s % 243.65/35.20 % (3682937)Peak memory usage: 157 MB % 243.65/35.20 % (3682937)Instructions burned: 3981 (million) % 243.65/35.20 % (3682947)Instruction limit reached! % 243.65/35.20 % (3682947)------------------------------ % 243.65/35.20 % (3682947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.65/35.20 % (3682947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.65/35.20 % (3682947)CaDiCaL version: 2.1.3 % 243.65/35.20 % (3682947)Termination reason: Instruction limit % 243.65/35.20 % (3682947)Termination phase: Saturation % 243.65/35.20 % (3682947)Time elapsed: 0.753 s % 243.65/35.20 % (3682947)Peak memory usage: 137 MB % 243.65/35.20 % (3682947)Instructions burned: 2331 (million) % 243.65/35.20 % (3682949)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=3760594917:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2768 on theBenchmark for (2768ds/7592Mi) % 243.65/35.20 % (3682950)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=2971833004:i=2693:kws=precedence:ins=1:av=off_2768 on theBenchmark for (2768ds/2693Mi) % 243.65/35.20 % (3682950)Instruction limit reached! % 243.65/35.20 % (3682950)------------------------------ % 243.65/35.20 % (3682950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.65/35.20 % (3682950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.65/35.20 % (3682950)CaDiCaL version: 2.1.3 % 243.65/35.20 % (3682950)Termination reason: Instruction limit % 243.65/35.20 % (3682950)Termination phase: Saturation % 243.65/35.20 % (3682950)Time elapsed: 0.959 s % 243.65/35.20 % (3682950)Peak memory usage: 139 MB % 243.65/35.20 % (3682950)Instructions burned: 2694 (million) % 243.65/35.20 % (3682941)Instruction limit reached! % 243.65/35.20 % (3682941)------------------------------ % 243.65/35.20 % (3682941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.65/35.20 % (3682941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.65/35.20 % (3682941)CaDiCaL version: 2.1.3 % 243.65/35.20 % (3682941)Termination reTerminated % 300.41/43.24 % Vampire exiting % 300.41/43.24 Terminated %------------------------------------------------------------------------------