%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC215-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 : n001.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:58 PM UTC 2026 % Result : Timeout 300.08s 43.17s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC215-1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.37 % Computer : n001.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.09/0.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Mon Sep 28 08:37:38 UTC 2026 % 0.09/0.37 % CPUTime : % 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.41 Running first-order theorem proving % 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 11.58/2.57 % (216970)Input is clausal, will run a generic CNF schedule. % 11.58/2.57 % (216977)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3837499783:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 11.58/2.57 % (216979)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=464342507:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 11.58/2.57 % (216975)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=2166245231:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 11.58/2.57 % (216976)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=219046129:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 11.58/2.57 % (216980)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4207120321:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 11.58/2.57 % (216978)lrs+10_1_sil=8000:sp=occurrence:random_seed=4000107045:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 11.58/2.57 % (216981)dis-21_1_sil=8000:lcm=predicate:random_seed=251932849: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.58/2.57 % (216981)Instruction limit reached! % 11.58/2.57 % (216981)------------------------------ % 11.58/2.57 % (216981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.58/2.57 % (216981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.58/2.57 % (216981)CaDiCaL version: 2.1.3 % 11.58/2.57 % (216981)Termination reason: Instruction limit % 11.58/2.57 % (216981)Termination phase: Saturation % 11.58/2.57 % (216981)Time elapsed: 0.053 s % 11.58/2.57 % (216981)Peak memory usage: 90 MB % 11.58/2.57 % (216981)Instructions burned: 117 (million) % 11.58/2.57 % (216978)Instruction limit reached! % 11.58/2.57 % (216978)------------------------------ % 11.58/2.57 % (216978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.58/2.57 % (216978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.58/2.57 % (216978)CaDiCaL version: 2.1.3 % 11.58/2.57 % (216978)Termination reason: Instruction limit % 11.58/2.57 % (216978)Termination phase: Saturation % 11.58/2.57 % (216978)Time elapsed: 0.064 s % 11.58/2.57 % (216978)Peak memory usage: 89 MB % 11.58/2.57 % (216978)Instructions burned: 107 (million) % 11.58/2.57 % (216979)Instruction limit reached! % 11.58/2.57 % (216979)------------------------------ % 11.58/2.57 % (216979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.58/2.57 % (216979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.58/2.57 % (216979)CaDiCaL version: 2.1.3 % 11.58/2.57 % (216979)Termination reason: Instruction limit % 11.58/2.57 % (216979)Termination phase: Saturation % 11.58/2.57 % (216979)Time elapsed: 0.066 s % 11.58/2.57 % (216979)Peak memory usage: 89 MB % 11.58/2.57 % (216979)Instructions burned: 114 (million) % 11.58/2.57 % (216980)Instruction limit reached! % 11.58/2.57 % (216980)------------------------------ % 11.58/2.57 % (216980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.58/2.57 % (216980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.58/2.57 % (216980)CaDiCaL version: 2.1.3 % 11.58/2.57 % (216980)Termination reason: Instruction limit % 11.58/2.57 % (216980)Termination phase: Saturation % 11.58/2.57 % (216980)Time elapsed: 0.122 s % 11.58/2.57 % (216980)Peak memory usage: 90 MB % 11.58/2.57 % (216980)Instructions burned: 181 (million) % 11.58/2.57 % (216989)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=2660538093:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 11.58/2.57 % (216990)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1415363330: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) % 11.58/2.57 % (216991)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4181122323:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 11.58/2.57 % (216989)Instruction limit reached! % 11.58/2.57 % (216989)------------------------------ % 11.58/2.57 % (216989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.58/2.57 % (216989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.87/4.25 % (216989)CaDiCaL version: 2.1.3 % 23.87/4.25 % (216989)Termination reason: Instruction limit % 23.87/4.25 % (216989)Termination phase: Saturation % 23.87/4.25 % (216989)Time elapsed: 0.075 s % 23.87/4.25 % (216989)Peak memory usage: 89 MB % 23.87/4.25 % (216989)Instructions burned: 145 (million) % 23.87/4.25 % (216993)lrs+10_64_to=lpo:sil=8000:random_seed=1683180557:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 23.87/4.25 % (216990)Instruction limit reached! % 23.87/4.25 % (216990)------------------------------ % 23.87/4.25 % (216990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.87/4.25 % (216990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.87/4.25 % (216990)CaDiCaL version: 2.1.3 % 23.87/4.25 % (216990)Termination reason: Instruction limit % 23.87/4.25 % (216990)Termination phase: Saturation % 23.87/4.25 % (216990)Time elapsed: 0.099 s % 23.87/4.25 % (216990)Peak memory usage: 90 MB % 23.87/4.25 % (216990)Instructions burned: 191 (million) % 23.87/4.25 % (216993)Instruction limit reached! % 23.87/4.25 % (216993)------------------------------ % 23.87/4.25 % (216993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.87/4.25 % (216993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.87/4.25 % (216993)CaDiCaL version: 2.1.3 % 23.87/4.25 % (216993)Termination reason: Instruction limit % 23.87/4.25 % (216993)Termination phase: Saturation % 23.87/4.25 % (216993)Time elapsed: 0.058 s % 23.87/4.25 % (216993)Peak memory usage: 89 MB % 23.87/4.25 % (216993)Instructions burned: 127 (million) % 23.87/4.25 % (216991)Instruction limit reached! % 23.87/4.25 % (216991)------------------------------ % 23.87/4.25 % (216991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.87/4.25 % (216991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.87/4.25 % (216991)CaDiCaL version: 2.1.3 % 23.87/4.25 % (216991)Termination reason: Instruction limit % 23.87/4.25 % (216991)Termination phase: Saturation % 23.87/4.25 % (216991)Time elapsed: 0.127 s % 23.87/4.25 % (216991)Peak memory usage: 90 MB % 23.87/4.25 % (216991)Instructions burned: 220 (million) % 23.87/4.25 % (216998)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3909554168:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 23.87/4.25 % (216999)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1982668803:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 23.87/4.25 % (217000)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4237746819:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 23.87/4.25 % (217001)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=1844152356:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 23.87/4.25 % (216998)Instruction limit reached! % 23.87/4.25 % (216998)------------------------------ % 23.87/4.25 % (216998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.87/4.25 % (216998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.87/4.25 % (216998)CaDiCaL version: 2.1.3 % 23.87/4.25 % (216998)Termination reason: Instruction limit % 23.87/4.25 % (216998)Termination phase: Saturation % 23.87/4.25 % (216998)Time elapsed: 0.122 s % 23.87/4.25 % (216998)Peak memory usage: 90 MB % 23.87/4.25 % (216998)Instructions burned: 194 (million) % 23.87/4.25 % (217001)Instruction limit reached! % 23.87/4.25 % (217001)------------------------------ % 23.87/4.25 % (217001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.87/4.25 % (217001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.87/4.25 % (217001)CaDiCaL version: 2.1.3 % 23.87/4.25 % (217001)Termination reason: Instruction limit % 23.87/4.25 % (217001)Termination phase: Saturation % 23.87/4.25 % (217001)Time elapsed: 0.054 s % 23.87/4.25 % (217001)Peak memory usage: 89 MB % 23.87/4.25 % (217001)Instructions burned: 107 (million) % 23.87/4.25 % (216999)Instruction limit reached! % 23.87/4.25 % (216999)------------------------------ % 23.87/4.25 % (216999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.87/4.25 % (216999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.87/4.25 % (216999)CaDiCaL version: 2.1.3 % 23.87/4.25 % (216999)Termination reason: Instruction limit % 23.87/4.25 % (216999)Termination phase: Saturation % 23.87/4.25 % (216999)Time elapsed: 0.096 s % 35.02/6.03 % (216999)Peak memory usage: 91 MB % 35.02/6.03 % (216999)Instructions burned: 158 (million) % 35.02/6.03 % (217006)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=494618488:i=107_2992 on theBenchmark for (2992ds/107Mi) % 35.02/6.03 % (217007)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4245860430:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 35.02/6.03 % (217008)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2074546440:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi) % 35.02/6.03 % (217006)Instruction limit reached! % 35.02/6.03 % (217006)------------------------------ % 35.02/6.03 % (217006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.02/6.03 % (217006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.02/6.03 % (217006)CaDiCaL version: 2.1.3 % 35.02/6.03 % (217006)Termination reason: Instruction limit % 35.02/6.03 % (217006)Termination phase: Saturation % 35.02/6.03 % (217006)Time elapsed: 0.066 s % 35.02/6.03 % (217006)Peak memory usage: 89 MB % 35.02/6.03 % (217006)Instructions burned: 107 (million) % 35.02/6.03 % (217007)Instruction limit reached! % 35.02/6.03 % (217007)------------------------------ % 35.02/6.03 % (217007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.02/6.03 % (217007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.02/6.03 % (217007)CaDiCaL version: 2.1.3 % 35.02/6.03 % (217007)Termination reason: Instruction limit % 35.02/6.03 % (217007)Termination phase: Saturation % 35.02/6.03 % (217007)Time elapsed: 0.152 s % 35.02/6.03 % (217007)Peak memory usage: 89 MB % 35.02/6.03 % (217007)Instructions burned: 243 (million) % 35.02/6.03 % (217012)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1580833735:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi) % 35.02/6.03 % (217012)Instruction limit reached! % 35.02/6.03 % (217012)------------------------------ % 35.02/6.03 % (217012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.02/6.03 % (217012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.02/6.03 % (217012)CaDiCaL version: 2.1.3 % 35.02/6.03 % (217012)Termination reason: Instruction limit % 35.02/6.03 % (217012)Termination phase: Saturation % 35.02/6.03 % (217012)Time elapsed: 0.076 s % 35.02/6.03 % (217012)Peak memory usage: 89 MB % 35.02/6.03 % (217012)Instructions burned: 136 (million) % 35.02/6.03 % (217013)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2349704766:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi) % 35.02/6.03 % (217015)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2438406930:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi) % 35.02/6.03 % (217013)Instruction limit reached! % 35.02/6.03 % (217013)------------------------------ % 35.02/6.03 % (217013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.02/6.03 % (217013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.02/6.03 % (217013)CaDiCaL version: 2.1.3 % 35.02/6.03 % (217013)Termination reason: Instruction limit % 35.02/6.03 % (217013)Termination phase: Saturation % 35.02/6.03 % (217013)Time elapsed: 0.253 s % 35.02/6.03 % (217013)Peak memory usage: 97 MB % 35.02/6.03 % (217013)Instructions burned: 500 (million) % 35.02/6.03 % (217015)Instruction limit reached! % 35.02/6.03 % (217015)------------------------------ % 35.02/6.03 % (217015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.02/6.03 % (217015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.02/6.03 % (217015)CaDiCaL version: 2.1.3 % 35.02/6.03 % (217015)Termination reason: Instruction limit % 35.02/6.03 % (217015)Termination phase: Saturation % 35.02/6.03 % (217015)Time elapsed: 0.099 s % 35.02/6.03 % (217015)Peak memory usage: 91 MB % 35.02/6.03 % (217015)Instructions burned: 191 (million) % 35.02/6.03 % (217019)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1548387776:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi) % 35.02/6.03 % (217018)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=504715363:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi) % 35.02/6.03 % (217019)Instruction limit reached! % 35.02/6.03 % (217019)------------------------------ % 48.20/7.88 % (217019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.20/7.88 % (217019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.20/7.88 % (217019)CaDiCaL version: 2.1.3 % 48.20/7.88 % (217019)Termination reason: Instruction limit % 48.20/7.88 % (217019)Termination phase: Saturation % 48.20/7.88 % (217019)Time elapsed: 0.090 s % 48.20/7.88 % (217019)Peak memory usage: 90 MB % 48.20/7.88 % (217019)Instructions burned: 157 (million) % 48.20/7.88 % (217018)Instruction limit reached! % 48.20/7.88 % (217018)------------------------------ % 48.20/7.88 % (217018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.20/7.88 % (217018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.20/7.88 % (217018)CaDiCaL version: 2.1.3 % 48.20/7.88 % (217018)Termination reason: Instruction limit % 48.20/7.88 % (217018)Termination phase: Saturation % 48.20/7.88 % (217018)Time elapsed: 0.137 s % 48.20/7.88 % (217018)Peak memory usage: 89 MB % 48.20/7.88 % (217018)Instructions burned: 266 (million) % 48.20/7.88 % (217022)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=1637508089:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi) % 48.20/7.88 % (217023)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1099446095:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi) % 48.20/7.88 % (217023)Instruction limit reached! % 48.20/7.88 % (217023)------------------------------ % 48.20/7.88 % (217023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.20/7.88 % (217023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.20/7.88 % (217023)CaDiCaL version: 2.1.3 % 48.20/7.88 % (217023)Termination reason: Instruction limit % 48.20/7.88 % (217023)Termination phase: Saturation % 48.20/7.88 % (217023)Time elapsed: 0.126 s % 48.20/7.88 % (217023)Peak memory usage: 88 MB % 48.20/7.88 % (217023)Instructions burned: 544 (million) % 48.20/7.88 % (217027)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1272228541:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi) % 48.20/7.88 % (217027)Instruction limit reached! % 48.20/7.88 % (217027)------------------------------ % 48.20/7.88 % (217027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.20/7.88 % (217027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.20/7.88 % (217027)CaDiCaL version: 2.1.3 % 48.20/7.88 % (217027)Termination reason: Instruction limit % 48.20/7.88 % (217027)Termination phase: Saturation % 48.20/7.88 % (217027)Time elapsed: 0.050 s % 48.20/7.88 % (217027)Peak memory usage: 91 MB % 48.20/7.88 % (217027)Instructions burned: 183 (million) % 48.20/7.88 % (217029)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=3406111446:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi) % 48.20/7.88 % (217000)Instruction limit reached! % 48.20/7.88 % (217000)------------------------------ % 48.20/7.88 % (217000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.20/7.88 % (217000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.20/7.88 % (217000)CaDiCaL version: 2.1.3 % 48.20/7.88 % (217000)Termination reason: Instruction limit % 48.20/7.88 % (217000)Termination phase: Saturation % 48.20/7.88 % (217000)Time elapsed: 2.149 s % 48.20/7.88 % (217000)Peak memory usage: 152 MB % 48.20/7.88 % (217000)Instructions burned: 3395 (million) % 48.20/7.88 % (217031)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=3589523577:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi) % 48.20/7.88 % (217031)Instruction limit reached! % 48.20/7.88 % (217031)------------------------------ % 48.20/7.88 % (217031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.20/7.88 % (217031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.20/7.88 % (217031)CaDiCaL version: 2.1.3 % 48.20/7.88 % (217031)Termination reason: Instruction limit % 48.20/7.88 % (217031)Termination phase: Saturation % 48.20/7.88 % (217031)Time elapsed: 0.216 s % 48.20/7.88 % (217031)Peak memory usage: 91 MB % 48.20/7.88 % (217031)Instructions burned: 412 (million) % 48.20/7.88 % (217033)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=3238052548:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi) % 70.90/10.96 % (217022)Instruction limit reached! % 70.90/10.96 % (217022)------------------------------ % 70.90/10.96 % (217022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.90/10.96 % (217022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.90/10.96 % (217022)CaDiCaL version: 2.1.3 % 70.90/10.96 % (217022)Termination reason: Instruction limit % 70.90/10.96 % (217022)Termination phase: Saturation % 70.90/10.96 % (217022)Time elapsed: 1.889 s % 70.90/10.96 % (217022)Peak memory usage: 153 MB % 70.90/10.96 % (217022)Instructions burned: 3257 (million) % 70.90/10.96 % (217008)Instruction limit reached! % 70.90/10.96 % (217008)------------------------------ % 70.90/10.96 % (217008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.90/10.96 % (217008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.90/10.96 % (217008)CaDiCaL version: 2.1.3 % 70.90/10.96 % (217008)Termination reason: Instruction limit % 70.90/10.96 % (217008)Termination phase: Saturation % 70.90/10.96 % (217008)Time elapsed: 2.988 s % 70.90/10.96 % (217008)Peak memory usage: 150 MB % 70.90/10.96 % (217008)Instructions burned: 5208 (million) % 70.90/10.96 % (217035)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=2610476496: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) % 70.90/10.96 % (217036)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1178097505:st=4:i=720:sd=3:fsr=off:ss=axioms_2960 on theBenchmark for (2960ds/720Mi) % 70.90/10.96 % (217035)Instruction limit reached! % 70.90/10.96 % (217035)------------------------------ % 70.90/10.96 % (217035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.90/10.96 % (217035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.90/10.96 % (217035)CaDiCaL version: 2.1.3 % 70.90/10.96 % (217035)Termination reason: Instruction limit % 70.90/10.96 % (217035)Termination phase: Saturation % 70.90/10.96 % (217035)Time elapsed: 0.191 s % 70.90/10.96 % (217035)Peak memory usage: 91 MB % 70.90/10.96 % (217035)Instructions burned: 303 (million) % 70.90/10.96 % (217039)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1512275696:i=598:bs=on:bd=preordered:av=off:ss=axioms_2958 on theBenchmark for (2958ds/598Mi) % 70.90/10.96 % (217036)Instruction limit reached! % 70.90/10.96 % (217036)------------------------------ % 70.90/10.96 % (217036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.90/10.96 % (217036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.90/10.96 % (217036)CaDiCaL version: 2.1.3 % 70.90/10.96 % (217036)Termination reason: Instruction limit % 70.90/10.96 % (217036)Termination phase: Saturation % 70.90/10.96 % (217036)Time elapsed: 0.353 s % 70.90/10.96 % (217036)Peak memory usage: 99 MB % 70.90/10.96 % (217036)Instructions burned: 722 (million) % 70.90/10.96 % (217041)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2706706033:i=2989:sd=3:ss=axioms:sgt=60_2955 on theBenchmark for (2955ds/2989Mi) % 70.90/10.96 % (217039)Instruction limit reached! % 70.90/10.96 % (217039)------------------------------ % 70.90/10.96 % (217039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.90/10.96 % (217039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.90/10.96 % (217039)CaDiCaL version: 2.1.3 % 70.90/10.96 % (217039)Termination reason: Instruction limit % 70.90/10.96 % (217039)Termination phase: Saturation % 70.90/10.96 % (217039)Time elapsed: 0.317 s % 70.90/10.96 % (217039)Peak memory usage: 93 MB % 70.90/10.96 % (217039)Instructions burned: 598 (million) % 70.90/10.96 % (217043)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=3288171201:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2953 on theBenchmark for (2953ds/1997Mi) % 70.90/10.96 % (217029)Instruction limit reached! % 70.90/10.96 % (217029)------------------------------ % 70.90/10.96 % (217029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.90/10.96 % (217029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.90/10.96 % (217029)CaDiCaL version: 2.1.3 % 70.90/10.96 % (217029)Termination reason: Instruction limit % 96.47/14.60 % (217029)Termination phase: Saturation % 96.47/14.60 % (217029)Time elapsed: 2.785 s % 96.47/14.60 % (217029)Peak memory usage: 155 MB % 96.47/14.60 % (217029)Instructions burned: 10307 (million) % 96.47/14.60 % (217045)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=2286855538:i=2088:bd=preordered:av=off_2948 on theBenchmark for (2948ds/2088Mi) % 96.47/14.60 % (217043)Instruction limit reached! % 96.47/14.60 % (217043)------------------------------ % 96.47/14.60 % (217043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.47/14.60 % (217043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.47/14.60 % (217043)CaDiCaL version: 2.1.3 % 96.47/14.60 % (217043)Termination reason: Instruction limit % 96.47/14.60 % (217043)Termination phase: Saturation % 96.47/14.60 % (217043)Time elapsed: 0.936 s % 96.47/14.60 % (217043)Peak memory usage: 137 MB % 96.47/14.60 % (217043)Instructions burned: 2000 (million) % 96.47/14.60 % (217047)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1919573855:i=1098:nicw=on_2942 on theBenchmark for (2942ds/1098Mi) % 96.47/14.60 % (217047)Instruction limit reached! % 96.47/14.60 % (217047)------------------------------ % 96.47/14.60 % (217047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.47/14.60 % (217047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.47/14.60 % (217047)CaDiCaL version: 2.1.3 % 96.47/14.60 % (217047)Termination reason: Instruction limit % 96.47/14.60 % (217047)Termination phase: Saturation % 96.47/14.60 % (217047)Time elapsed: 0.283 s % 96.47/14.60 % (217047)Peak memory usage: 119 MB % 96.47/14.60 % (217047)Instructions burned: 1101 (million) % 96.47/14.60 % (217049)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3757817108:i=433:bd=preordered_2938 on theBenchmark for (2938ds/433Mi) % 96.47/14.60 % (217049)Instruction limit reached! % 96.47/14.60 % (217049)------------------------------ % 96.47/14.60 % (217049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.47/14.60 % (217049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.47/14.60 % (217049)CaDiCaL version: 2.1.3 % 96.47/14.60 % (217049)Termination reason: Instruction limit % 96.47/14.60 % (217049)Termination phase: Saturation % 96.47/14.60 % (217049)Time elapsed: 0.143 s % 96.47/14.60 % (217049)Peak memory usage: 91 MB % 96.47/14.60 % (217049)Instructions burned: 434 (million) % 96.47/14.60 % (217041)Instruction limit reached! % 96.47/14.60 % (217041)------------------------------ % 96.47/14.60 % (217041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.47/14.60 % (217041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.47/14.60 % (217041)CaDiCaL version: 2.1.3 % 96.47/14.60 % (217041)Termination reason: Instruction limit % 96.47/14.60 % (217041)Termination phase: Saturation % 96.47/14.60 % (217041)Time elapsed: 1.894 s % 96.47/14.60 % (217041)Peak memory usage: 145 MB % 96.47/14.60 % (217041)Instructions burned: 2990 (million) % 96.47/14.60 % (217051)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1625828851: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) % 96.47/14.60 % (217045)Instruction limit reached! % 96.47/14.60 % (217045)------------------------------ % 96.47/14.60 % (217045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.47/14.60 % (217045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.47/14.60 % (217045)CaDiCaL version: 2.1.3 % 96.47/14.60 % (217045)Termination reason: Instruction limit % 96.47/14.60 % (217045)Termination phase: Saturation % 96.47/14.60 % (217045)Time elapsed: 1.273 s % 96.47/14.60 % (217045)Peak memory usage: 137 MB % 96.47/14.60 % (217045)Instructions burned: 2088 (million) % 96.47/14.60 % (217052)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3297777144:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2934 on theBenchmark for (2934ds/6922Mi) % 96.47/14.60 % (217054)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=3575421638:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2934 on theBenchmark for (2934ds/596Mi) % 96.47/14.60 % (217054)Instruction limit reached! % 96.47/14.60 % (217054)------------------------------ % 96.47/14.60 % (217054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.23/16.92 % (217054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.23/16.92 % (217054)CaDiCaL version: 2.1.3 % 113.23/16.92 % (217054)Termination reason: Instruction limit % 113.23/16.92 % (217054)Termination phase: Saturation % 113.23/16.92 % (217054)Time elapsed: 0.288 s % 113.23/16.92 % (217054)Peak memory usage: 108 MB % 113.23/16.92 % (217054)Instructions burned: 598 (million) % 113.23/16.92 % (217057)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=3584535298:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2929 on theBenchmark for (2929ds/4123Mi) % 113.23/16.92 % (217051)Instruction limit reached! % 113.23/16.92 % (217051)------------------------------ % 113.23/16.92 % (217051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.23/16.92 % (217051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.23/16.92 % (217051)CaDiCaL version: 2.1.3 % 113.23/16.92 % (217051)Termination reason: Instruction limit % 113.23/16.92 % (217051)Termination phase: Saturation % 113.23/16.92 % (217051)Time elapsed: 0.980 s % 113.23/16.92 % (217051)Peak memory usage: 141 MB % 113.23/16.92 % (217051)Instructions burned: 2945 (million) % 113.23/16.92 % (217059)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3802603169:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2924 on theBenchmark for (2924ds/16411Mi) % 113.23/16.92 % (217033)Instruction limit reached! % 113.23/16.92 % (217033)------------------------------ % 113.23/16.92 % (217033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.23/16.92 % (217033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.23/16.92 % (217033)CaDiCaL version: 2.1.3 % 113.23/16.92 % (217033)Termination reason: Instruction limit % 113.23/16.92 % (217033)Termination phase: Saturation % 113.23/16.92 % (217033)Time elapsed: 4.277 s % 113.23/16.92 % (217033)Peak memory usage: 198 MB % 113.23/16.92 % (217033)Instructions burned: 8481 (million) % 113.23/16.92 % (217061)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3556146277:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2923 on theBenchmark for (2923ds/1670Mi) % 113.23/16.92 % (217061)Instruction limit reached! % 113.23/16.92 % (217061)------------------------------ % 113.23/16.92 % (217061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.23/16.92 % (217061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.23/16.92 % (217061)CaDiCaL version: 2.1.3 % 113.23/16.92 % (217061)Termination reason: Instruction limit % 113.23/16.92 % (217061)Termination phase: Saturation % 113.23/16.92 % (217061)Time elapsed: 1.042 s % 113.23/16.92 % (217061)Peak memory usage: 136 MB % 113.23/16.92 % (217061)Instructions burned: 1672 (million) % 113.23/16.92 % (217063)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=3142348346:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2911 on theBenchmark for (2911ds/1722Mi) % 113.23/16.92 % (217057)Instruction limit reached! % 113.23/16.92 % (217057)------------------------------ % 113.23/16.92 % (217057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.23/16.92 % (217057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.23/16.92 % (217057)CaDiCaL version: 2.1.3 % 113.23/16.92 % (217057)Termination reason: Instruction limit % 113.23/16.92 % (217057)Termination phase: Saturation % 113.23/16.92 % (217057)Time elapsed: 2.282 s % 113.23/16.92 % (217057)Peak memory usage: 164 MB % 113.23/16.92 % (217057)Instructions burned: 4124 (million) % 113.23/16.92 % (217065)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=3766477292:cts=off:cond=on:i=9530:bs=on:fsd=on_2905 on theBenchmark for (2905ds/9530Mi) % 113.23/16.92 % (217063)Instruction limit reached! % 113.23/16.92 % (217063)------------------------------ % 113.23/16.92 % (217063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.23/16.92 % (217063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.23/16.92 % (217063)CaDiCaL version: 2.1.3 % 113.23/16.92 % (217063)Termination reason: Instruction limit % 113.23/16.92 % (217063)Termination phase: Saturation % 113.23/16.92 % (217063)Time elapsed: 1.052 s % 113.23/16.92 % (217063)Peak memory usage: 132 MB % 133.13/19.65 % (217063)Instructions burned: 1722 (million) % 133.13/19.65 % (217067)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3711520438:st=2:i=4495:sd=10:ss=included_2898 on theBenchmark for (2898ds/4495Mi) % 133.13/19.65 % (217052)Instruction limit reached! % 133.13/19.65 % (217052)------------------------------ % 133.13/19.65 % (217052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.13/19.65 % (217052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.13/19.65 % (217052)CaDiCaL version: 2.1.3 % 133.13/19.65 % (217052)Termination reason: Instruction limit % 133.13/19.65 % (217052)Termination phase: Saturation % 133.13/19.65 % (217052)Time elapsed: 3.636 s % 133.13/19.65 % (217052)Peak memory usage: 195 MB % 133.13/19.65 % (217052)Instructions burned: 6923 (million) % 133.13/19.65 % (217069)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=4283266565:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2896 on theBenchmark for (2896ds/4920Mi) % 133.13/19.65 % (217059)Instruction limit reached! % 133.13/19.65 % (217059)------------------------------ % 133.13/19.65 % (217059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.13/19.65 % (217059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.13/19.65 % (217059)CaDiCaL version: 2.1.3 % 133.13/19.65 % (217059)Termination reason: Instruction limit % 133.13/19.65 % (217059)Termination phase: Saturation % 133.13/19.65 % (217059)Time elapsed: 4.749 s % 133.13/19.65 % (217059)Peak memory usage: 200 MB % 133.13/19.65 % (217059)Instructions burned: 16414 (million) % 133.13/19.65 % (217071)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=2043439186:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2875 on theBenchmark for (2875ds/2083Mi) % 133.13/19.65 % (217067)Instruction limit reached! % 133.13/19.65 % (217067)------------------------------ % 133.13/19.65 % (217067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.13/19.65 % (217067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.13/19.65 % (217067)CaDiCaL version: 2.1.3 % 133.13/19.65 % (217067)Termination reason: Instruction limit % 133.13/19.65 % (217067)Termination phase: Saturation % 133.13/19.65 % (217067)Time elapsed: 2.809 s % 133.13/19.65 % (217067)Peak memory usage: 161 MB % 133.13/19.65 % (217067)Instructions burned: 4495 (million) % 133.13/19.65 % (217071)Instruction limit reached! % 133.13/19.65 % (217071)------------------------------ % 133.13/19.65 % (217071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.13/19.65 % (217071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.13/19.65 % (217071)CaDiCaL version: 2.1.3 % 133.13/19.65 % (217071)Termination reason: Instruction limit % 133.13/19.65 % (217071)Termination phase: Saturation % 133.13/19.65 % (217071)Time elapsed: 0.705 s % 133.13/19.65 % (217071)Peak memory usage: 138 MB % 133.13/19.65 % (217071)Instructions burned: 2085 (million) % 133.13/19.65 % (217073)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=4174281841:i=4629:av=off:gsp=on_2869 on theBenchmark for (2869ds/4629Mi) % 133.13/19.65 % (217075)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2011606215:i=1258:av=off_2867 on theBenchmark for (2867ds/1258Mi) % 133.13/19.65 % (217069)Instruction limit reached! % 133.13/19.65 % (217069)------------------------------ % 133.13/19.65 % (217069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.13/19.65 % (217069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.13/19.65 % (217069)CaDiCaL version: 2.1.3 % 133.13/19.65 % (217069)Termination reason: Instruction limit % 133.13/19.65 % (217069)Termination phase: Saturation % 133.13/19.65 % (217069)Time elapsed: 2.955 s % 133.13/19.65 % (217069)Peak memory usage: 150 MB % 133.13/19.65 % (217069)Instructions burned: 4921 (million) % 133.13/19.65 % (217077)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3799992414:i=7343:av=off:ss=included_2865 on theBenchmark for (2865ds/7343Mi) % 133.13/19.65 % (217075)Instruction limit reached! % 133.13/19.65 % (217075)------------------------------ % 133.13/19.65 % (217075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.13/19.65 % (217075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.54/22.55 % (217075)CaDiCaL version: 2.1.3 % 153.54/22.55 % (217075)Termination reason: Instruction limit % 153.54/22.55 % (217075)Termination phase: Saturation % 153.54/22.55 % (217075)Time elapsed: 0.351 s % 153.54/22.55 % (217075)Peak memory usage: 103 MB % 153.54/22.55 % (217075)Instructions burned: 1261 (million) % 153.54/22.55 % (217079)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=4119273360:i=1325:sd=2:ss=axioms:sgt=16_2862 on theBenchmark for (2862ds/1325Mi) % 153.54/22.55 % (217079)Instruction limit reached! % 153.54/22.55 % (217079)------------------------------ % 153.54/22.55 % (217079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.54/22.55 % (217079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.54/22.55 % (217079)CaDiCaL version: 2.1.3 % 153.54/22.55 % (217079)Termination reason: Instruction limit % 153.54/22.55 % (217079)Termination phase: Saturation % 153.54/22.55 % (217079)Time elapsed: 0.251 s % 153.54/22.55 % (217079)Peak memory usage: 90 MB % 153.54/22.55 % (217079)Instructions burned: 1327 (million) % 153.54/22.55 % (217081)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=1010008581:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2858 on theBenchmark for (2858ds/2646Mi) % 153.54/22.55 % (217065)Instruction limit reached! % 153.54/22.55 % (217065)------------------------------ % 153.54/22.55 % (217065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.54/22.55 % (217065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.54/22.55 % (217065)CaDiCaL version: 2.1.3 % 153.54/22.55 % (217065)Termination reason: Instruction limit % 153.54/22.55 % (217065)Termination phase: Saturation % 153.54/22.55 % (217065)Time elapsed: 4.858 s % 153.54/22.55 % (217065)Peak memory usage: 148 MB % 153.54/22.55 % (217065)Instructions burned: 9532 (million) % 153.54/22.55 % (217083)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1669046605:i=1489:sd=2:ep=R:ss=axioms_2855 on theBenchmark for (2855ds/1489Mi) % 153.54/22.55 % (217081)Instruction limit reached! % 153.54/22.55 % (217081)------------------------------ % 153.54/22.55 % (217081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.54/22.55 % (217081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.54/22.55 % (217081)CaDiCaL version: 2.1.3 % 153.54/22.55 % (217081)Termination reason: Instruction limit % 153.54/22.55 % (217081)Termination phase: Saturation % 153.54/22.55 % (217081)Time elapsed: 0.845 s % 153.54/22.55 % (217081)Peak memory usage: 137 MB % 153.54/22.55 % (217081)Instructions burned: 2647 (million) % 153.54/22.55 % (217085)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=156998230:i=1503_2849 on theBenchmark for (2849ds/1503Mi) % 153.54/22.55 % (217083)Instruction limit reached! % 153.54/22.55 % (217083)------------------------------ % 153.54/22.55 % (217083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.54/22.55 % (217083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.54/22.55 % (217083)CaDiCaL version: 2.1.3 % 153.54/22.55 % (217083)Termination reason: Instruction limit % 153.54/22.55 % (217083)Termination phase: Saturation % 153.54/22.55 % (217083)Time elapsed: 0.886 s % 153.54/22.55 % (217083)Peak memory usage: 136 MB % 153.54/22.55 % (217083)Instructions burned: 1490 (million) % 153.54/22.55 % (217087)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3540564443:i=13942:kws=frequency_2844 on theBenchmark for (2844ds/13942Mi) % 153.54/22.55 % (217085)Instruction limit reached! % 153.54/22.55 % (217085)------------------------------ % 153.54/22.55 % (217085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.54/22.55 % (217085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.54/22.55 % (217085)CaDiCaL version: 2.1.3 % 153.54/22.55 % (217085)Termination reason: Instruction limit % 153.54/22.55 % (217085)Termination phase: Saturation % 153.54/22.55 % (217085)Time elapsed: 0.505 s % 153.54/22.55 % (217085)Peak memory usage: 143 MB % 153.54/22.55 % (217085)Instructions burned: 1507 (million) % 153.54/22.55 % (217089)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=194045350:i=3604:fsr=off:er=filter_2842 on theBenchmark for (2842ds/3604Mi) % 153.54/22.55 % (217073)Instruction limit reached! % 153.54/22.55 % (217073)------------------------------ % 182.84/26.79 % (217073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.84/26.79 % (217073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.84/26.79 % (217073)CaDiCaL version: 2.1.3 % 182.84/26.79 % (217073)Termination reason: Instruction limit % 182.84/26.79 % (217073)Termination phase: Saturation % 182.84/26.79 % (217073)Time elapsed: 2.803 s % 182.84/26.79 % (217073)Peak memory usage: 161 MB % 182.84/26.79 % (217073)Instructions burned: 4630 (million) % 182.84/26.79 % (217091)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1269449147:i=1876:sd=1:ss=included:sgt=32_2839 on theBenchmark for (2839ds/1876Mi) % 182.84/26.79 % (217089)Instruction limit reached! % 182.84/26.79 % (217089)------------------------------ % 182.84/26.79 % (217089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.84/26.79 % (217089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.84/26.79 % (217089)CaDiCaL version: 2.1.3 % 182.84/26.79 % (217089)Termination reason: Instruction limit % 182.84/26.79 % (217089)Termination phase: Saturation % 182.84/26.79 % (217089)Time elapsed: 1.057 s % 182.84/26.79 % (217089)Peak memory usage: 161 MB % 182.84/26.79 % (217089)Instructions burned: 3605 (million) % 182.84/26.79 % (217093)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3610332765:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2830 on theBenchmark for (2830ds/1932Mi) % 182.84/26.79 % (217091)Instruction limit reached! % 182.84/26.79 % (217091)------------------------------ % 182.84/26.79 % (217091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.84/26.79 % (217091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.84/26.79 % (217091)CaDiCaL version: 2.1.3 % 182.84/26.79 % (217091)Termination reason: Instruction limit % 182.84/26.79 % (217091)Termination phase: Saturation % 182.84/26.79 % (217091)Time elapsed: 1.182 s % 182.84/26.79 % (217091)Peak memory usage: 133 MB % 182.84/26.79 % (217091)Instructions burned: 1876 (million) % 182.84/26.79 % (217095)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=535200244:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2825 on theBenchmark for (2825ds/1980Mi) % 182.84/26.79 % (217093)Instruction limit reached! % 182.84/26.79 % (217093)------------------------------ % 182.84/26.79 % (217093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.84/26.79 % (217093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.84/26.79 % (217093)CaDiCaL version: 2.1.3 % 182.84/26.79 % (217093)Termination reason: Instruction limit % 182.84/26.79 % (217093)Termination phase: Saturation % 182.84/26.79 % (217093)Time elapsed: 0.579 s % 182.84/26.79 % (217093)Peak memory usage: 135 MB % 182.84/26.79 % (217093)Instructions burned: 1935 (million) % 182.84/26.79 % (217097)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=3244131528:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2823 on theBenchmark for (2823ds/3902Mi) % 182.84/26.79 % (217077)Instruction limit reached! % 182.84/26.79 % (217077)------------------------------ % 182.84/26.79 % (217077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.84/26.79 % (217077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.84/26.79 % (217077)CaDiCaL version: 2.1.3 % 182.84/26.79 % (217077)Termination reason: Instruction limit % 182.84/26.79 % (217077)Termination phase: Saturation % 182.84/26.79 % (217077)Time elapsed: 4.229 s % 182.84/26.79 % (217077)Peak memory usage: 167 MB % 182.84/26.79 % (217077)Instructions burned: 7343 (million) % 182.84/26.79 % (217099)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=638212137:avsq=on:i=3916:aac=none:amm=off_2821 on theBenchmark for (2821ds/3916Mi) % 182.84/26.79 % (217097)Instruction limit reached! % 182.84/26.79 % (217097)------------------------------ % 182.84/26.79 % (217097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.84/26.79 % (217097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.84/26.79 % (217097)CaDiCaL version: 2.1.3 % 182.84/26.79 % (217097)Termination reason: Instruction limit % 182.84/26.79 % (217097)Termination phase: Saturation % 182.84/26.79 % (217097)Time elapsed: 1.041 s % 182.84/26.79 % (217097)Peak memory usage: 156 MB % 182.84/26.79 % (217097)Instructions burned: 3904 (million) % 227.48/32.95 % (217095)Instruction limit reached! % 227.48/32.95 % (217095)------------------------------ % 227.48/32.95 % (217095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.48/32.95 % (217095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.48/32.95 % (217095)CaDiCaL version: 2.1.3 % 227.48/32.95 % (217095)Termination reason: Instruction limit % 227.48/32.95 % (217095)Termination phase: Saturation % 227.48/32.95 % (217095)Time elapsed: 1.271 s % 227.48/32.95 % (217095)Peak memory usage: 137 MB % 227.48/32.95 % (217095)Instructions burned: 1981 (million) % 227.48/32.95 % (217101)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=1659004246:cond=on:i=3940:av=off:er=known_2812 on theBenchmark for (2812ds/3940Mi) % 227.48/32.95 % (217102)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=981069871:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2811 on theBenchmark for (2811ds/3980Mi) % 227.48/32.95 % (217099)Instruction limit reached! % 227.48/32.95 % (217099)------------------------------ % 227.48/32.95 % (217099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.48/32.95 % (217099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.48/32.95 % (217099)CaDiCaL version: 2.1.3 % 227.48/32.95 % (217099)Termination reason: Instruction limit % 227.48/32.95 % (217099)Termination phase: Saturation % 227.48/32.95 % (217099)Time elapsed: 2.150 s % 227.48/32.95 % (217099)Peak memory usage: 120 MB % 227.48/32.95 % (217099)Instructions burned: 3917 (million) % 227.48/32.95 % (217101)Instruction limit reached! % 227.48/32.95 % (217101)------------------------------ % 227.48/32.95 % (217101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.48/32.95 % (217101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.48/32.95 % (217101)CaDiCaL version: 2.1.3 % 227.48/32.95 % (217101)Termination reason: Instruction limit % 227.48/32.95 % (217101)Termination phase: Saturation % 227.48/32.95 % (217101)Time elapsed: 1.317 s % 227.48/32.95 % (217101)Peak memory usage: 152 MB % 227.48/32.95 % (217101)Instructions burned: 3944 (million) % 227.48/32.95 % (217105)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=4167716573:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2798 on theBenchmark for (2798ds/2087Mi) % 227.48/32.95 % (217106)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=1537705696:cts=off:cond=on:i=4272:bs=on:fsd=on_2797 on theBenchmark for (2797ds/4272Mi) % 227.48/32.95 % (217102)Instruction limit reached! % 227.48/32.95 % (217102)------------------------------ % 227.48/32.95 % (217102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.48/32.95 % (217102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.48/32.95 % (217102)CaDiCaL version: 2.1.3 % 227.48/32.95 % (217102)Termination reason: Instruction limit % 227.48/32.95 % (217102)Termination phase: Saturation % 227.48/32.95 % (217102)Time elapsed: 2.426 s % 227.48/32.95 % (217102)Peak memory usage: 159 MB % 227.48/32.95 % (217102)Instructions burned: 3981 (million) % 227.48/32.95 % (217109)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1933209533:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2785 on theBenchmark for (2785ds/2197Mi) % 227.48/32.95 % (217105)Instruction limit reached! % 227.48/32.95 % (217105)------------------------------ % 227.48/32.95 % (217105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.48/32.95 % (217105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.48/32.95 % (217105)CaDiCaL version: 2.1.3 % 227.48/32.95 % (217105)Termination reason: Instruction limit % 227.48/32.95 % (217105)Termination phase: Saturation % 227.48/32.95 % (217105)Time elapsed: 1.334 s % 227.48/32.95 % (217105)Peak memory usage: 141 MB % 227.48/32.95 % (217105)Instructions burned: 2087 (million) % 227.48/32.95 % (217106)Instruction limit reached! % 227.48/32.95 % (217106)------------------------------ % 227.48/32.95 % (217106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.48/32.95 % (217106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.48/32.95 % (217106)CaDiCaL version: 2.1.3 % 227.48/32.95 % (217106)Termination reason: Instruction limit % 263.91/38.10 % (217106)Termination phase: Saturation % 263.91/38.10 % (217106)Time elapsed: 1.314 s % 263.91/38.10 % (217106)Peak memory usage: 144 MB % 263.91/38.10 % (217106)Instructions burned: 4275 (million) % 263.91/38.10 % (217111)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1152475290:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2783 on theBenchmark for (2783ds/6508Mi) % 263.91/38.10 % (217112)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=1025254167:i=2330:fgj=on:av=off:fsr=off_2783 on theBenchmark for (2783ds/2330Mi) % 263.91/38.10 % (217109)Instruction limit reached! % 263.91/38.10 % (217109)------------------------------ % 263.91/38.10 % (217109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.91/38.10 % (217109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.91/38.10 % (217109)CaDiCaL version: 2.1.3 % 263.91/38.10 % (217109)Termination reason: Instruction limit % 263.91/38.10 % (217109)Termination phase: Saturation % 263.91/38.10 % (217109)Time elapsed: 1.256 s % 263.91/38.10 % (217109)Peak memory usage: 144 MB % 263.91/38.10 % (217109)Instructions burned: 2198 (million) % 263.91/38.10 % (217115)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1378111492:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2771 on theBenchmark for (2771ds/7592Mi) % 263.91/38.10 % (217112)Instruction limit reached! % 263.91/38.10 % (217112)------------------------------ % 263.91/38.10 % (217112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.91/38.10 % (217112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.91/38.10 % (217112)CaDiCaL version: 2.1.3 % 263.91/38.10 % (217112)Termination reason: Instruction limit % 263.91/38.10 % (217112)Termination phase: Saturation % 263.91/38.10 % (217112)Time elapsed: 1.454 s % 263.91/38.10 % (217112)Peak memory usage: 140 MB % 263.91/38.10 % (217112)Instructions burned: 2330 (million) % 263.91/38.10 % (217117)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=3107909294:i=2693:kws=precedence:ins=1:av=off_2766 on theBenchmark for (2766ds/2693Mi) % 263.91/38.10 % (217111)Instruction limit reached! % 263.91/38.10 % (217111)------------------------------ % 263.91/38.10 % (217111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.91/38.10 % (217111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.91/38.10 % (217111)CaDiCaL version: 2.1.3 % 263.91/38.10 % (217111)Termination reason: Instruction limit % 263.91/38.10 % (217111)Termination phase: Saturation % 263.91/38.10 % (217111)Time elapsed: 1.802 s % 263.91/38.10 % (217111)Peak memory usage: 147 MB % 263.91/38.10 % (217111)Instructions burned: 6510 (million) % 263.91/38.10 % (217119)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2314288080:i=28651:sd=4:ss=included:sgt=64_2763 on theBenchmark for (2763ds/28651Mi) % 263.91/38.10 % (217087)Instruction limit reached! % 263.91/38.10 % (217087)------------------------------ % 263.91/38.10 % (217087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.91/38.10 % (217087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.91/38.10 % (217087)CaDiCaL version: 2.1.3 % 263.91/38.10 % (217087)Termination reason: Instruction limit % 263.91/38.10 % (217087)Termination phase: Saturation % 263.91/38.10 % (217087)Time elapsed: 8.337 s % 263.91/38.10 % (217087)Peak memory usage: 258 MB % 263.91/38.10 % (217087)Instructions burned: 13943 (million) % 263.91/38.10 % (217121)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1295195355:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2759 on theBenchmark for (2759ds/2700Mi) % 263.91/38.10 % (217117)Instruction limit reached! % 263.91/38.10 % (217117)------------------------------ % 263.91/38.10 % (217117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 263.91/38.10 % (217117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 263.91/38.10 % (217117)CaDiCaL version: 2.1.3 % 263.91/38.10 % (217117)Termination reason: Instruction limit % 263.91/38.10 % (217117)Termination phase: Saturation % 263.91/38.10 % (217117)Time elapsed: 1.680 s % 263.91/38.10 % (217117)Peak memory usage: 141 MB % 263.91/38.10 % (217117)Instructions burned: 2693 (million) % 263.91/38.10 % (217123)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=4292295933:i=3196:nm=4_2748 on theBenchmark for (2748ds/3196Mi) % 263.91/38.10 % (217121Terminated %------------------------------------------------------------------------------