%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM221-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 : n015.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:56 PM UTC 2026 % Result : Timeout 299.98s 43.14s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM221-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.14/0.42 % Computer : n015.cluster.edu % 0.14/0.42 % Model : x86_64 x86_64 % 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.42 % Memory : 8046.5625MB % 0.14/0.42 % OS : Linux 6.8.0-71-generic % 0.14/0.42 % CPULimit : 300 % 0.14/0.42 % WCLimit : 300 % 0.14/0.42 % DateTime : Sun Sep 27 19:16:16 UTC 2026 % 0.14/0.42 % CPUTime : % 0.14/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.23/0.47 Running first-order theorem proving % 0.23/0.47 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 % 19.46/3.79 % (1955550)Input is clausal, will run a generic CNF schedule. % 19.46/3.79 % (1955555)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=2028038928:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 19.46/3.79 % (1955556)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3951728637:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 19.46/3.79 % (1955560)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1430968028:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 19.46/3.79 % (1955558)lrs+10_1_sil=8000:sp=occurrence:random_seed=1193084575:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 19.46/3.79 % (1955557)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1975571418:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 19.46/3.79 % (1955559)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3063719832:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 19.46/3.79 % (1955561)dis-21_1_sil=8000:lcm=predicate:random_seed=3892393204: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) % 19.46/3.79 % (1955558)Instruction limit reached! % 19.46/3.79 % (1955558)------------------------------ % 19.46/3.79 % (1955558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.46/3.79 % (1955558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.46/3.79 % (1955558)CaDiCaL version: 2.1.3 % 19.46/3.79 % (1955558)Termination reason: Instruction limit % 19.46/3.79 % (1955558)Termination phase: Saturation % 19.46/3.79 % (1955558)Time elapsed: 0.116 s % 19.46/3.79 % (1955558)Peak memory usage: 90 MB % 19.46/3.79 % (1955558)Instructions burned: 108 (million) % 19.46/3.79 % (1955559)Instruction limit reached! % 19.46/3.79 % (1955559)------------------------------ % 19.46/3.79 % (1955559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.46/3.79 % (1955559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.46/3.79 % (1955559)CaDiCaL version: 2.1.3 % 19.46/3.79 % (1955559)Termination reason: Instruction limit % 19.46/3.79 % (1955559)Termination phase: Saturation % 19.46/3.79 % (1955559)Time elapsed: 0.117 s % 19.46/3.79 % (1955559)Peak memory usage: 89 MB % 19.46/3.79 % (1955559)Instructions burned: 115 (million) % 19.46/3.79 % (1955561)Instruction limit reached! % 19.46/3.79 % (1955561)------------------------------ % 19.46/3.79 % (1955561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.46/3.79 % (1955561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.46/3.79 % (1955561)CaDiCaL version: 2.1.3 % 19.46/3.79 % (1955561)Termination reason: Instruction limit % 19.46/3.79 % (1955561)Termination phase: Saturation % 19.46/3.79 % (1955561)Time elapsed: 0.118 s % 19.46/3.79 % (1955561)Peak memory usage: 89 MB % 19.46/3.79 % (1955561)Instructions burned: 118 (million) % 19.46/3.79 % (1955560)Instruction limit reached! % 19.46/3.79 % (1955560)------------------------------ % 19.46/3.79 % (1955560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.46/3.79 % (1955560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.46/3.79 % (1955560)CaDiCaL version: 2.1.3 % 19.46/3.79 % (1955560)Termination reason: Instruction limit % 19.46/3.79 % (1955560)Termination phase: Saturation % 19.46/3.79 % (1955560)Time elapsed: 0.204 s % 19.46/3.79 % (1955560)Peak memory usage: 90 MB % 19.46/3.79 % (1955560)Instructions burned: 180 (million) % 19.46/3.79 % (1955570)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3990155217:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi) % 19.46/3.79 % (1955569)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=3840082900:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi) % 19.46/3.79 % (1955571)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1491647028:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi) % 19.46/3.79 % (1955572)lrs+10_64_to=lpo:sil=8000:random_seed=1228686335:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 19.46/3.79 % (1955570)Instruction limit reached! % 34.23/5.95 % (1955570)------------------------------ % 34.23/5.95 % (1955570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.95 % (1955570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.95 % (1955570)CaDiCaL version: 2.1.3 % 34.23/5.95 % (1955570)Termination reason: Instruction limit % 34.23/5.95 % (1955570)Termination phase: Saturation % 34.23/5.95 % (1955570)Time elapsed: 0.152 s % 34.23/5.95 % (1955570)Peak memory usage: 90 MB % 34.23/5.95 % (1955570)Instructions burned: 190 (million) % 34.23/5.95 % (1955569)Instruction limit reached! % 34.23/5.95 % (1955569)------------------------------ % 34.23/5.95 % (1955569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.95 % (1955569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.95 % (1955569)CaDiCaL version: 2.1.3 % 34.23/5.95 % (1955569)Termination reason: Instruction limit % 34.23/5.95 % (1955569)Termination phase: Saturation % 34.23/5.95 % (1955569)Time elapsed: 0.154 s % 34.23/5.95 % (1955569)Peak memory usage: 89 MB % 34.23/5.95 % (1955569)Instructions burned: 143 (million) % 34.23/5.95 % (1955572)Instruction limit reached! % 34.23/5.95 % (1955572)------------------------------ % 34.23/5.95 % (1955572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.95 % (1955572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.95 % (1955572)CaDiCaL version: 2.1.3 % 34.23/5.95 % (1955572)Termination reason: Instruction limit % 34.23/5.95 % (1955572)Termination phase: Saturation % 34.23/5.95 % (1955572)Time elapsed: 0.124 s % 34.23/5.95 % (1955572)Peak memory usage: 89 MB % 34.23/5.95 % (1955572)Instructions burned: 126 (million) % 34.23/5.95 % (1955571)Instruction limit reached! % 34.23/5.95 % (1955571)------------------------------ % 34.23/5.95 % (1955571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.95 % (1955571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.95 % (1955571)CaDiCaL version: 2.1.3 % 34.23/5.95 % (1955571)Termination reason: Instruction limit % 34.23/5.95 % (1955571)Termination phase: Saturation % 34.23/5.95 % (1955571)Time elapsed: 0.194 s % 34.23/5.95 % (1955571)Peak memory usage: 89 MB % 34.23/5.95 % (1955571)Instructions burned: 219 (million) % 34.23/5.95 % (1955577)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2660003362:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi) % 34.23/5.95 % (1955578)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4290960607:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi) % 34.23/5.95 % (1955579)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2585355268:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi) % 34.23/5.95 % (1955578)Instruction limit reached! % 34.23/5.95 % (1955578)------------------------------ % 34.23/5.95 % (1955578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.95 % (1955578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.95 % (1955578)CaDiCaL version: 2.1.3 % 34.23/5.95 % (1955578)Termination reason: Instruction limit % 34.23/5.95 % (1955578)Termination phase: Saturation % 34.23/5.95 % (1955578)Time elapsed: 0.159 s % 34.23/5.95 % (1955578)Peak memory usage: 91 MB % 34.23/5.95 % (1955578)Instructions burned: 157 (million) % 34.23/5.95 % (1955577)Instruction limit reached! % 34.23/5.95 % (1955577)------------------------------ % 34.23/5.95 % (1955577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.95 % (1955577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.95 % (1955577)CaDiCaL version: 2.1.3 % 34.23/5.95 % (1955577)Termination reason: Instruction limit % 34.23/5.95 % (1955577)Termination phase: Saturation % 34.23/5.95 % (1955577)Time elapsed: 0.168 s % 34.23/5.95 % (1955577)Peak memory usage: 90 MB % 34.23/5.95 % (1955577)Instructions burned: 195 (million) % 34.23/5.95 % (1955580)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=1252655387:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi) % 34.23/5.95 % (1955580)Instruction limit reached! % 34.23/5.95 % (1955580)------------------------------ % 34.23/5.95 % (1955580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.23/5.95 % (1955580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.23/5.95 % (1955580)CaDiCaL version: 2.1.3 % 58.80/9.26 % (1955580)Termination reason: Instruction limit % 58.80/9.26 % (1955580)Termination phase: Saturation % 58.80/9.26 % (1955580)Time elapsed: 0.090 s % 58.80/9.26 % (1955580)Peak memory usage: 94 MB % 58.80/9.26 % (1955580)Instructions burned: 106 (million) % 58.80/9.26 % (1955584)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1707905731:i=107_2987 on theBenchmark for (2987ds/107Mi) % 58.80/9.26 % (1955586)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3928855427:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi) % 58.80/9.26 % (1955584)Instruction limit reached! % 58.80/9.26 % (1955584)------------------------------ % 58.80/9.26 % (1955584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.80/9.26 % (1955584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.80/9.26 % (1955584)CaDiCaL version: 2.1.3 % 58.80/9.26 % (1955584)Termination reason: Instruction limit % 58.80/9.26 % (1955584)Termination phase: Saturation % 58.80/9.26 % (1955584)Time elapsed: 0.117 s % 58.80/9.26 % (1955584)Peak memory usage: 89 MB % 58.80/9.26 % (1955584)Instructions burned: 107 (million) % 58.80/9.26 % (1955587)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1117212202:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi) % 58.80/9.26 % (1955586)Instruction limit reached! % 58.80/9.26 % (1955586)------------------------------ % 58.80/9.26 % (1955586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.80/9.26 % (1955586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.80/9.26 % (1955586)CaDiCaL version: 2.1.3 % 58.80/9.26 % (1955586)Termination reason: Instruction limit % 58.80/9.26 % (1955586)Termination phase: Saturation % 58.80/9.26 % (1955586)Time elapsed: 0.242 s % 58.80/9.26 % (1955586)Peak memory usage: 91 MB % 58.80/9.26 % (1955586)Instructions burned: 242 (million) % 58.80/9.26 % (1955590)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4184378868:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi) % 58.80/9.26 % (1955590)Instruction limit reached! % 58.80/9.26 % (1955590)------------------------------ % 58.80/9.26 % (1955590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.80/9.26 % (1955590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.80/9.26 % (1955590)CaDiCaL version: 2.1.3 % 58.80/9.26 % (1955590)Termination reason: Instruction limit % 58.80/9.26 % (1955590)Termination phase: Saturation % 58.80/9.26 % (1955590)Time elapsed: 0.127 s % 58.80/9.26 % (1955590)Peak memory usage: 89 MB % 58.80/9.26 % (1955590)Instructions burned: 134 (million) % 58.80/9.26 % (1955592)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1675537051:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi) % 58.80/9.26 % (1955594)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3307750943:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi) % 58.80/9.26 % (1955594)Instruction limit reached! % 58.80/9.26 % (1955594)------------------------------ % 58.80/9.26 % (1955594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.80/9.26 % (1955594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.80/9.26 % (1955594)CaDiCaL version: 2.1.3 % 58.80/9.26 % (1955594)Termination reason: Instruction limit % 58.80/9.26 % (1955594)Termination phase: Saturation % 58.80/9.26 % (1955594)Time elapsed: 0.197 s % 58.80/9.26 % (1955594)Peak memory usage: 90 MB % 58.80/9.26 % (1955594)Instructions burned: 191 (million) % 58.80/9.26 % (1955592)Instruction limit reached! % 58.80/9.26 % (1955592)------------------------------ % 58.80/9.26 % (1955592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.80/9.26 % (1955592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.80/9.26 % (1955592)CaDiCaL version: 2.1.3 % 58.80/9.26 % (1955592)Termination reason: Instruction limit % 58.80/9.26 % (1955592)Termination phase: Saturation % 58.80/9.26 % (1955592)Time elapsed: 0.487 s % 58.80/9.26 % (1955592)Peak memory usage: 94 MB % 58.80/9.26 % (1955592)Instructions burned: 499 (million) % 58.80/9.26 % (1955597)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=196370718:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi) % 58.80/9.26 % (1955598)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1177691355:cond=on:i=156:bs=on:gtg=exists_all:er=known_2974 on theBenchmark for (2974ds/156Mi) % 94.04/14.19 % (1955598)Instruction limit reached! % 94.04/14.19 % (1955598)------------------------------ % 94.04/14.19 % (1955598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.04/14.19 % (1955598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.04/14.19 % (1955598)CaDiCaL version: 2.1.3 % 94.04/14.19 % (1955598)Termination reason: Instruction limit % 94.04/14.19 % (1955598)Termination phase: Saturation % 94.04/14.19 % (1955598)Time elapsed: 0.172 s % 94.04/14.19 % (1955598)Peak memory usage: 90 MB % 94.04/14.19 % (1955598)Instructions burned: 157 (million) % 94.04/14.19 % (1955597)Instruction limit reached! % 94.04/14.19 % (1955597)------------------------------ % 94.04/14.19 % (1955597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.04/14.19 % (1955597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.04/14.19 % (1955597)CaDiCaL version: 2.1.3 % 94.04/14.19 % (1955597)Termination reason: Instruction limit % 94.04/14.19 % (1955597)Termination phase: Saturation % 94.04/14.19 % (1955597)Time elapsed: 0.273 s % 94.04/14.19 % (1955597)Peak memory usage: 92 MB % 94.04/14.19 % (1955597)Instructions burned: 264 (million) % 94.04/14.19 % (1955601)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=1142492425:i=3256:kws=precedence:bd=preordered:av=off_2970 on theBenchmark for (2970ds/3256Mi) % 94.04/14.19 % (1955602)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2636731337:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi) % 94.04/14.19 % (1955602)Instruction limit reached! % 94.04/14.19 % (1955602)------------------------------ % 94.04/14.19 % (1955602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.04/14.19 % (1955602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.04/14.19 % (1955602)CaDiCaL version: 2.1.3 % 94.04/14.19 % (1955602)Termination reason: Instruction limit % 94.04/14.19 % (1955602)Termination phase: Saturation % 94.04/14.19 % (1955602)Time elapsed: 0.398 s % 94.04/14.19 % (1955602)Peak memory usage: 91 MB % 94.04/14.19 % (1955602)Instructions burned: 538 (million) % 94.04/14.19 % (1955605)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4022858608:i=180:bd=preordered:av=off_2962 on theBenchmark for (2962ds/180Mi) % 94.04/14.19 % (1955605)Instruction limit reached! % 94.04/14.19 % (1955605)------------------------------ % 94.04/14.19 % (1955605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.04/14.19 % (1955605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.04/14.19 % (1955605)CaDiCaL version: 2.1.3 % 94.04/14.19 % (1955605)Termination reason: Instruction limit % 94.04/14.19 % (1955605)Termination phase: Saturation % 94.04/14.19 % (1955605)Time elapsed: 0.164 s % 94.04/14.19 % (1955605)Peak memory usage: 90 MB % 94.04/14.19 % (1955605)Instructions burned: 181 (million) % 94.04/14.19 % (1955579)Instruction limit reached! % 94.04/14.19 % (1955579)------------------------------ % 94.04/14.19 % (1955579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.04/14.19 % (1955579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.04/14.19 % (1955579)CaDiCaL version: 2.1.3 % 94.04/14.19 % (1955579)Termination reason: Instruction limit % 94.04/14.19 % (1955579)Termination phase: Saturation % 94.04/14.19 % (1955579)Time elapsed: 3.228 s % 94.04/14.19 % (1955579)Peak memory usage: 147 MB % 94.04/14.19 % (1955579)Instructions burned: 3395 (million) % 94.04/14.19 % (1955607)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=3790230090:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/10307Mi) % 94.04/14.19 % (1955608)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=737642429:i=412:gtgl=4:gtg=exists_all_2956 on theBenchmark for (2956ds/412Mi) % 94.04/14.19 % (1955608)Instruction limit reached! % 94.04/14.19 % (1955608)------------------------------ % 94.04/14.19 % (1955608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.04/14.19 % (1955608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.04/14.19 % (1955608)CaDiCaL version: 2.1.3 % 94.04/14.19 % (1955608)Termination reason: Instruction limit % 94.04/14.19 % (1955608)Termination phase: Saturation % 131.80/19.57 % (1955608)Time elapsed: 0.300 s % 131.80/19.57 % (1955608)Peak memory usage: 90 MB % 131.80/19.57 % (1955608)Instructions burned: 412 (million) % 131.80/19.57 % (1955611)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=2961013635:s2pl=no:i=8478:s2at=4:nm=6_2950 on theBenchmark for (2950ds/8478Mi) % 131.80/19.57 % (1955601)Instruction limit reached! % 131.80/19.57 % (1955601)------------------------------ % 131.80/19.57 % (1955601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.80/19.57 % (1955601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/19.57 % (1955601)CaDiCaL version: 2.1.3 % 131.80/19.57 % (1955601)Termination reason: Instruction limit % 131.80/19.57 % (1955601)Termination phase: Saturation % 131.80/19.57 % (1955601)Time elapsed: 3.237 s % 131.80/19.57 % (1955601)Peak memory usage: 146 MB % 131.80/19.57 % (1955601)Instructions burned: 3256 (million) % 131.80/19.57 % (1955613)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=3808303079:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2934 on theBenchmark for (2934ds/303Mi) % 131.80/19.57 % (1955613)Refutation not found, incomplete strategy % 131.80/19.57 % (1955613)------------------------------ % 131.80/19.57 % (1955613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.80/19.57 % (1955613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/19.57 % (1955613)CaDiCaL version: 2.1.3 % 131.80/19.57 % (1955613)Termination reason: Refutation not found, incomplete strategy % 131.80/19.57 % (1955613)Time elapsed: 0.004 s % 131.80/19.57 % (1955613)Peak memory usage: 89 MB % 131.80/19.57 % (1955613)Instructions burned: 2 (million) % 131.80/19.57 % (1955587)Instruction limit reached! % 131.80/19.57 % (1955587)------------------------------ % 131.80/19.57 % (1955587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.80/19.57 % (1955587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/19.57 % (1955587)CaDiCaL version: 2.1.3 % 131.80/19.57 % (1955587)Termination reason: Instruction limit % 131.80/19.57 % (1955587)Termination phase: Saturation % 131.80/19.57 % (1955587)Time elapsed: 5.235 s % 131.80/19.57 % (1955587)Peak memory usage: 162 MB % 131.80/19.57 % (1955587)Instructions burned: 5208 (million) % 131.80/19.57 % (1955615)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3653555680:st=4:i=720:sd=3:fsr=off:ss=axioms_2930 on theBenchmark for (2930ds/720Mi) % 131.80/19.57 % (1955613)------------------------------ % 131.80/19.57 % (1955613)------------------------------ % 131.80/19.57 % (1955617)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3134608154:i=598:bs=on:bd=preordered:av=off:ss=axioms_2927 on theBenchmark for (2927ds/598Mi) % 131.80/19.57 % (1955615)Instruction limit reached! % 131.80/19.57 % (1955615)------------------------------ % 131.80/19.57 % (1955615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.80/19.57 % (1955615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/19.57 % (1955615)CaDiCaL version: 2.1.3 % 131.80/19.57 % (1955615)Termination reason: Instruction limit % 131.80/19.57 % (1955615)Termination phase: Saturation % 131.80/19.57 % (1955615)Time elapsed: 0.649 s % 131.80/19.57 % (1955615)Peak memory usage: 97 MB % 131.80/19.57 % (1955615)Instructions burned: 721 (million) % 131.80/19.57 % (1955617)Instruction limit reached! % 131.80/19.57 % (1955617)------------------------------ % 131.80/19.57 % (1955617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.80/19.57 % (1955617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.80/19.57 % (1955617)CaDiCaL version: 2.1.3 % 131.80/19.57 % (1955617)Termination reason: Instruction limit % 131.80/19.57 % (1955617)Termination phase: Saturation % 131.80/19.57 % (1955617)Time elapsed: 0.565 s % 131.80/19.57 % (1955617)Peak memory usage: 94 MB % 131.80/19.57 % (1955617)Instructions burned: 599 (million) % 131.80/19.57 % (1955619)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1833639317:i=2989:sd=3:ss=axioms:sgt=60_2921 on theBenchmark for (2921ds/2989Mi) % 131.80/19.57 % (1955620)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=1608134968:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2919 on theBenchmark for (2919ds/1997Mi) % 176.91/25.87 % (1955620)Instruction limit reached! % 176.91/25.87 % (1955620)------------------------------ % 176.91/25.87 % (1955620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.91/25.87 % (1955620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.91/25.87 % (1955620)CaDiCaL version: 2.1.3 % 176.91/25.87 % (1955620)Termination reason: Instruction limit % 176.91/25.87 % (1955620)Termination phase: Saturation % 176.91/25.87 % (1955620)Time elapsed: 2.146 s % 176.91/25.87 % (1955620)Peak memory usage: 138 MB % 176.91/25.87 % (1955620)Instructions burned: 1997 (million) % 176.91/25.87 % (1955625)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=3969742193:i=2088:bd=preordered:av=off_2895 on theBenchmark for (2895ds/2088Mi) % 176.91/25.87 % (1955619)Instruction limit reached! % 176.91/25.87 % (1955619)------------------------------ % 176.91/25.87 % (1955619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.91/25.87 % (1955619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.91/25.87 % (1955619)CaDiCaL version: 2.1.3 % 176.91/25.87 % (1955619)Termination reason: Instruction limit % 176.91/25.87 % (1955619)Termination phase: Saturation % 176.91/25.87 % (1955619)Time elapsed: 2.910 s % 176.91/25.87 % (1955619)Peak memory usage: 143 MB % 176.91/25.87 % (1955619)Instructions burned: 2990 (million) % 176.91/25.87 % (1955627)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=593754069:i=1098:nicw=on_2889 on theBenchmark for (2889ds/1098Mi) % 176.91/25.87 % (1955627)Instruction limit reached! % 176.91/25.87 % (1955627)------------------------------ % 176.91/25.87 % (1955627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.91/25.87 % (1955627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.91/25.87 % (1955627)CaDiCaL version: 2.1.3 % 176.91/25.87 % (1955627)Termination reason: Instruction limit % 176.91/25.87 % (1955627)Termination phase: Saturation % 176.91/25.87 % (1955627)Time elapsed: 1.037 s % 176.91/25.87 % (1955627)Peak memory usage: 101 MB % 176.91/25.87 % (1955627)Instructions burned: 1098 (million) % 176.91/25.87 % (1955629)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=46801178:i=433:bd=preordered_2876 on theBenchmark for (2876ds/433Mi) % 176.91/25.87 % (1955625)Instruction limit reached! % 176.91/25.87 % (1955625)------------------------------ % 176.91/25.87 % (1955625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.91/25.87 % (1955625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.91/25.87 % (1955625)CaDiCaL version: 2.1.3 % 176.91/25.87 % (1955625)Termination reason: Instruction limit % 176.91/25.87 % (1955625)Termination phase: Saturation % 176.91/25.87 % (1955625)Time elapsed: 2.083 s % 176.91/25.87 % (1955625)Peak memory usage: 137 MB % 176.91/25.87 % (1955625)Instructions burned: 2088 (million) % 176.91/25.87 % (1955611)Instruction limit reached! % 176.91/25.87 % (1955611)------------------------------ % 176.91/25.87 % (1955611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.91/25.87 % (1955611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.91/25.87 % (1955611)CaDiCaL version: 2.1.3 % 176.91/25.87 % (1955611)Termination reason: Instruction limit % 176.91/25.87 % (1955611)Termination phase: Saturation % 176.91/25.87 % (1955611)Time elapsed: 7.665 s % 176.91/25.87 % (1955611)Peak memory usage: 198 MB % 176.91/25.87 % (1955611)Instructions burned: 8478 (million) % 176.91/25.87 % (1955629)Instruction limit reached! % 176.91/25.87 % (1955629)------------------------------ % 176.91/25.87 % (1955629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.91/25.87 % (1955629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.91/25.87 % (1955629)CaDiCaL version: 2.1.3 % 176.91/25.87 % (1955629)Termination reason: Instruction limit % 176.91/25.87 % (1955629)Termination phase: Saturation % 176.91/25.87 % (1955629)Time elapsed: 0.379 s % 176.91/25.87 % (1955629)Peak memory usage: 92 MB % 176.91/25.87 % (1955629)Instructions burned: 434 (million) % 176.91/25.87 % (1955631)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=97151920:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2871 on theBenchmark for (2871ds/2942Mi) % 176.91/25.87 % (1955632)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2280378829:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2870 on theBenchmark for (2870ds/6922Mi) % 201.55/29.38 % (1955633)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=383230479:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2869 on theBenchmark for (2869ds/596Mi) % 201.55/29.38 % (1955633)Instruction limit reached! % 201.55/29.38 % (1955633)------------------------------ % 201.55/29.38 % (1955633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.55/29.38 % (1955633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.55/29.38 % (1955633)CaDiCaL version: 2.1.3 % 201.55/29.38 % (1955633)Termination reason: Instruction limit % 201.55/29.38 % (1955633)Termination phase: Saturation % 201.55/29.38 % (1955633)Time elapsed: 0.510 s % 201.55/29.38 % (1955633)Peak memory usage: 99 MB % 201.55/29.38 % (1955633)Instructions burned: 597 (million) % 201.55/29.38 % (1955639)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=2077666977:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2862 on theBenchmark for (2862ds/4123Mi) % 201.55/29.38 % (1955607)Instruction limit reached! % 201.55/29.38 % (1955607)------------------------------ % 201.55/29.38 % (1955607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.55/29.38 % (1955607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.55/29.38 % (1955607)CaDiCaL version: 2.1.3 % 201.55/29.38 % (1955607)Termination reason: Instruction limit % 201.55/29.38 % (1955607)Termination phase: Saturation % 201.55/29.38 % (1955607)Time elapsed: 10.567 s % 201.55/29.38 % (1955607)Peak memory usage: 174 MB % 201.55/29.38 % (1955607)Instructions burned: 10307 (million) % 201.55/29.38 % (1955641)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3641457661:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2849 on theBenchmark for (2849ds/16411Mi) % 201.55/29.38 % (1955631)Instruction limit reached! % 201.55/29.38 % (1955631)------------------------------ % 201.55/29.38 % (1955631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.55/29.38 % (1955631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.55/29.38 % (1955631)CaDiCaL version: 2.1.3 % 201.55/29.38 % (1955631)Termination reason: Instruction limit % 201.55/29.38 % (1955631)Termination phase: Saturation % 201.55/29.38 % (1955631)Time elapsed: 3.195 s % 201.55/29.38 % (1955631)Peak memory usage: 146 MB % 201.55/29.38 % (1955631)Instructions burned: 2942 (million) % 201.55/29.38 % (1955643)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3628252604:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2836 on theBenchmark for (2836ds/1670Mi) % 201.55/29.38 % (1955643)Instruction limit reached! % 201.55/29.38 % (1955643)------------------------------ % 201.55/29.38 % (1955643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.55/29.38 % (1955643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.55/29.38 % (1955643)CaDiCaL version: 2.1.3 % 201.55/29.38 % (1955643)Termination reason: Instruction limit % 201.55/29.38 % (1955643)Termination phase: Saturation % 201.55/29.38 % (1955643)Time elapsed: 1.720 s % 201.55/29.38 % (1955643)Peak memory usage: 136 MB % 201.55/29.38 % (1955643)Instructions burned: 1670 (million) % 201.55/29.38 % (1955639)Instruction limit reached! % 201.55/29.38 % (1955639)------------------------------ % 201.55/29.38 % (1955639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.55/29.38 % (1955639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.55/29.38 % (1955639)CaDiCaL version: 2.1.3 % 201.55/29.38 % (1955639)Termination reason: Instruction limit % 201.55/29.38 % (1955639)Termination phase: Saturation % 201.55/29.38 % (1955639)Time elapsed: 4.211 s % 201.55/29.38 % (1955639)Peak memory usage: 158 MB % 201.55/29.38 % (1955639)Instructions burned: 4123 (million) % 201.55/29.38 % (1955648)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=67026576:cts=off:cond=on:i=9530:bs=on:fsd=on_2816 on theBenchmark for (2816ds/9530Mi) % 201.55/29.38 % (1955647)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=508013453:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2816 on theBenchmark for (2816ds/1722Mi) % 218.34/31.77 % (1955647)Refutation not found, incomplete strategy % 218.34/31.77 % (1955647)------------------------------ % 218.34/31.77 % (1955647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.77 % (1955647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.77 % (1955647)CaDiCaL version: 2.1.3 % 218.34/31.77 % (1955647)Termination reason: Refutation not found, incomplete strategy % 218.34/31.77 % (1955647)Time elapsed: 1.021 s % 218.34/31.77 % (1955647)Peak memory usage: 130 MB % 218.34/31.77 % (1955647)Instructions burned: 1093 (million) % 218.34/31.77 % (1955647)------------------------------ % 218.34/31.77 % (1955647)------------------------------ % 218.34/31.77 % (1955632)Instruction limit reached! % 218.34/31.77 % (1955632)------------------------------ % 218.34/31.77 % (1955632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.77 % (1955632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.77 % (1955632)CaDiCaL version: 2.1.3 % 218.34/31.77 % (1955632)Termination reason: Instruction limit % 218.34/31.77 % (1955632)Termination phase: Saturation % 218.34/31.77 % (1955632)Time elapsed: 6.674 s % 218.34/31.77 % (1955632)Peak memory usage: 178 MB % 218.34/31.77 % (1955632)Instructions burned: 6922 (million) % 218.34/31.77 % (1955653)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4229786662:st=2:i=4495:sd=10:ss=included_2801 on theBenchmark for (2801ds/4495Mi) % 218.34/31.77 % (1955654)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=2545766249:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2800 on theBenchmark for (2800ds/4920Mi) % 218.34/31.77 % (1955653)Instruction limit reached! % 218.34/31.77 % (1955653)------------------------------ % 218.34/31.77 % (1955653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.77 % (1955653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.77 % (1955653)CaDiCaL version: 2.1.3 % 218.34/31.77 % (1955653)Termination reason: Instruction limit % 218.34/31.77 % (1955653)Termination phase: Saturation % 218.34/31.77 % (1955653)Time elapsed: 2.303 s % 218.34/31.77 % (1955653)Peak memory usage: 152 MB % 218.34/31.77 % (1955653)Instructions burned: 4497 (million) % 218.34/31.77 % (1955657)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=3925384214:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2776 on theBenchmark for (2776ds/2083Mi) % 218.34/31.77 % (1955657)Instruction limit reached! % 218.34/31.77 % (1955657)------------------------------ % 218.34/31.77 % (1955657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.77 % (1955657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.77 % (1955657)CaDiCaL version: 2.1.3 % 218.34/31.77 % (1955657)Termination reason: Instruction limit % 218.34/31.77 % (1955657)Termination phase: Saturation % 218.34/31.77 % (1955657)Time elapsed: 1.127 s % 218.34/31.77 % (1955657)Peak memory usage: 139 MB % 218.34/31.77 % (1955657)Instructions burned: 2084 (million) % 218.34/31.77 % (1955659)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=2919325231:i=4629:av=off:gsp=on_2762 on theBenchmark for (2762ds/4629Mi) % 218.34/31.77 % (1955659)Refutation not found, incomplete strategy % 218.34/31.77 % (1955659)------------------------------ % 218.34/31.77 % (1955659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.77 % (1955659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.77 % (1955659)CaDiCaL version: 2.1.3 % 218.34/31.77 % (1955659)Termination reason: Refutation not found, incomplete strategy % 218.34/31.77 % (1955659)Time elapsed: 0.534 s % 218.34/31.77 % (1955659)Peak memory usage: 129 MB % 218.34/31.77 % (1955659)Instructions burned: 931 (million) % 218.34/31.77 % (1955659)------------------------------ % 218.34/31.77 % (1955659)------------------------------ % 218.34/31.77 % (1955654)Instruction limit reached! % 218.34/31.77 % (1955654)------------------------------ % 218.34/31.77 % (1955654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.77 % (1955654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.77 % (1955654)CaDiCaL version: 2.1.3 % 218.34/31.77 % (1955654)Termination reason: Instruction limit % 218.34/31.77 % (1955654)Termination phase: Saturation % 239.74/34.71 % (1955654)Time elapsed: 4.732 s % 239.74/34.71 % (1955654)Peak memory usage: 159 MB % 239.74/34.71 % (1955654)Instructions burned: 4921 (million) % 239.74/34.71 % (1955663)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2307947042:i=1258:av=off_2752 on theBenchmark for (2752ds/1258Mi) % 239.74/34.71 % (1955664)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3468358345:i=7343:av=off:ss=included_2750 on theBenchmark for (2750ds/7343Mi) % 239.74/34.71 % (1955663)Instruction limit reached! % 239.74/34.71 % (1955663)------------------------------ % 239.74/34.71 % (1955663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.74/34.71 % (1955663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.74/34.71 % (1955663)CaDiCaL version: 2.1.3 % 239.74/34.71 % (1955663)Termination reason: Instruction limit % 239.74/34.71 % (1955663)Termination phase: Saturation % 239.74/34.71 % (1955663)Time elapsed: 0.555 s % 239.74/34.71 % (1955663)Peak memory usage: 96 MB % 239.74/34.71 % (1955663)Instructions burned: 1259 (million) % 239.74/34.71 % (1955667)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1529174708:i=1325:sd=2:ss=axioms:sgt=16_2744 on theBenchmark for (2744ds/1325Mi) % 239.74/34.71 % (1955667)Refutation not found, incomplete strategy % 239.74/34.71 % (1955667)------------------------------ % 239.74/34.71 % (1955667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.74/34.71 % (1955667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.74/34.71 % (1955667)CaDiCaL version: 2.1.3 % 239.74/34.71 % (1955667)Termination reason: Refutation not found, incomplete strategy % 239.74/34.71 % (1955667)Time elapsed: 0.004 s % 239.74/34.71 % (1955667)Peak memory usage: 88 MB % 239.74/34.71 % (1955667)Instructions burned: 6 (million) % 239.74/34.71 % (1955667)------------------------------ % 239.74/34.71 % (1955667)------------------------------ % 239.74/34.71 % (1955669)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=2496632576:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2740 on theBenchmark for (2740ds/2646Mi) % 239.74/34.71 % (1955664)Instruction limit reached! % 239.74/34.71 % (1955664)------------------------------ % 239.74/34.71 % (1955664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.74/34.71 % (1955664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.74/34.71 % (1955664)CaDiCaL version: 2.1.3 % 239.74/34.71 % (1955664)Termination reason: Instruction limit % 239.74/34.71 % (1955664)Termination phase: Saturation % 239.74/34.71 % (1955664)Time elapsed: 2.776 s % 239.74/34.71 % (1955664)Peak memory usage: 190 MB % 239.74/34.71 % (1955664)Instructions burned: 7345 (million) % 239.74/34.71 % (1955669)Instruction limit reached! % 239.74/34.71 % (1955669)------------------------------ % 239.74/34.71 % (1955669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.74/34.71 % (1955669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.74/34.71 % (1955669)CaDiCaL version: 2.1.3 % 239.74/34.71 % (1955669)Termination reason: Instruction limit % 239.74/34.71 % (1955669)Termination phase: Saturation % 239.74/34.71 % (1955669)Time elapsed: 1.860 s % 239.74/34.71 % (1955669)Peak memory usage: 144 MB % 239.74/34.71 % (1955669)Instructions burned: 2647 (million) % 239.74/34.71 % (1955778)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1394016016:i=1489:sd=2:ep=R:ss=axioms_2720 on theBenchmark for (2720ds/1489Mi) % 239.74/34.71 % (1955648)Instruction limit reached! % 239.74/34.71 % (1955648)------------------------------ % 239.74/34.71 % (1955648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.74/34.71 % (1955648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.74/34.71 % (1955648)CaDiCaL version: 2.1.3 % 239.74/34.71 % (1955648)Termination reason: Instruction limit % 239.74/34.71 % (1955648)Termination phase: Saturation % 239.74/34.71 % (1955648)Time elapsed: 9.676 s % 239.74/34.71 % (1955648)Peak memory usage: 177 MB % 239.74/34.71 % (1955648)Instructions burned: 9530 (million) % 239.74/34.71 % (1955803)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=1486114062:i=1503_2718 on theBenchmark for (2718ds/1503Mi) % 239.74/34.71 % (1955829)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1946215255:i=13942:kws=frequency_2717 on theBenchmark for (2717ds/13942Mi) % 268.08/38.72 % (1955778)Instruction limit reached! % 268.08/38.72 % (1955778)------------------------------ % 268.08/38.72 % (1955778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.08/38.72 % (1955778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.08/38.72 % (1955778)CaDiCaL version: 2.1.3 % 268.08/38.72 % (1955778)Termination reason: Instruction limit % 268.08/38.72 % (1955778)Termination phase: Saturation % 268.08/38.72 % (1955778)Time elapsed: 0.510 s % 268.08/38.72 % (1955778)Peak memory usage: 135 MB % 268.08/38.72 % (1955778)Instructions burned: 1491 (million) % 268.08/38.72 % (1955832)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=2442157489:i=3604:fsr=off:er=filter_2713 on theBenchmark for (2713ds/3604Mi) % 268.08/38.72 % (1955803)Instruction limit reached! % 268.08/38.72 % (1955803)------------------------------ % 268.08/38.72 % (1955803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.08/38.72 % (1955803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.08/38.72 % (1955803)CaDiCaL version: 2.1.3 % 268.08/38.72 % (1955803)Termination reason: Instruction limit % 268.08/38.72 % (1955803)Termination phase: Saturation % 268.08/38.72 % (1955803)Time elapsed: 0.953 s % 268.08/38.72 % (1955803)Peak memory usage: 135 MB % 268.08/38.72 % (1955803)Instructions burned: 1503 (million) % 268.08/38.72 % (1955834)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2927409683:i=1876:sd=1:ss=included:sgt=32_2707 on theBenchmark for (2707ds/1876Mi) % 268.08/38.72 % (1955641)Instruction limit reached! % 268.08/38.72 % (1955641)------------------------------ % 268.08/38.72 % (1955641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.08/38.72 % (1955641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.08/38.72 % (1955641)CaDiCaL version: 2.1.3 % 268.08/38.72 % (1955641)Termination reason: Instruction limit % 268.08/38.72 % (1955641)Termination phase: Saturation % 268.08/38.72 % (1955641)Time elapsed: 14.208 s % 268.08/38.72 % (1955641)Peak memory usage: 231 MB % 268.08/38.72 % (1955641)Instructions burned: 16412 (million) % 268.08/38.72 % (1955836)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3415088061:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2704 on theBenchmark for (2704ds/1932Mi) % 268.08/38.72 % (1955832)Instruction limit reached! % 268.08/38.72 % (1955832)------------------------------ % 268.08/38.72 % (1955832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.08/38.72 % (1955832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.08/38.72 % (1955832)CaDiCaL version: 2.1.3 % 268.08/38.72 % (1955832)Termination reason: Instruction limit % 268.08/38.72 % (1955832)Termination phase: Saturation % 268.08/38.72 % (1955832)Time elapsed: 1.198 s % 268.08/38.72 % (1955832)Peak memory usage: 149 MB % 268.08/38.72 % (1955832)Instructions burned: 3606 (million) % 268.08/38.72 % (1955834)Refutation not found, incomplete strategy % 268.08/38.72 % (1955834)------------------------------ % 268.08/38.72 % (1955834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.08/38.72 % (1955834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.08/38.72 % (1955834)CaDiCaL version: 2.1.3 % 268.08/38.72 % (1955834)Termination reason: Refutation not found, incomplete strategy % 268.08/38.72 % (1955834)Time elapsed: 0.603 s % 268.08/38.72 % (1955834)Peak memory usage: 128 MB % 268.08/38.72 % (1955834)Instructions burned: 924 (million) % 268.08/38.72 % (1955838)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=579949091:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2700 on theBenchmark for (2700ds/1980Mi) % 268.08/38.72 % (1955834)------------------------------ % 268.08/38.72 % (1955834)------------------------------ % 268.08/38.72 % (1955840)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=2256258492:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2697 on theBenchmark for (2697ds/3902Mi) % 268.08/38.72 % (1955838)Instruction limit reached! % 268.08/38.72 % (1955838)------------------------------ % 268.08/38.72 % (1955838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.08/38.72 % (1955838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.98/43.14 % (1955838)CaDiCaL version: 2.1.3 % 299.98/43.14 % (1955838)Termination reason: Instruction limit % 299.98/43.14 % (1955838)Termination phase: Saturation % 299.98/43.14 % (1955838)Time elapsed: 0.700 s % 299.98/43.14 % (1955838)Peak memory usage: 137 MB % 299.98/43.14 % (1955838)Instructions burned: 1981 (million) % 299.98/43.14 % (1955836)Instruction limit reached! % 299.98/43.14 % (1955836)------------------------------ % 299.98/43.14 % (1955836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.98/43.14 % (1955836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.98/43.14 % (1955836)CaDiCaL version: 2.1.3 % 299.98/43.14 % (1955836)Termination reason: Instruction limit % 299.98/43.14 % (1955836)Termination phase: Saturation % 299.98/43.14 % (1955836)Time elapsed: 1.123 s % 299.98/43.14 % (1955836)Peak memory usage: 139 MB % 299.98/43.14 % (1955836)Instructions burned: 1934 (million) % 299.98/43.14 % (1955842)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2217660837:avsq=on:i=3916:aac=none:amm=off_2692 on theBenchmark for (2692ds/3916Mi) % 299.98/43.14 % (1955843)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=1765115394:cond=on:i=3940:av=off:er=known_2691 on theBenchmark for (2691ds/3940Mi) % 299.98/43.14 % (1955842)Instruction limit reached! % 299.98/43.14 % (1955842)------------------------------ % 299.98/43.14 % (1955842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.98/43.14 % (1955842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.98/43.14 % (1955842)CaDiCaL version: 2.1.3 % 299.98/43.14 % (1955842)Termination reason: Instruction limit % 299.98/43.14 % (1955842)Termination phase: Saturation % 299.98/43.14 % (1955842)Time elapsed: 1.187 s % 299.98/43.14 % (1955842)Peak memory usage: 100 MB % 299.98/43.14 % (1955842)Instructions burned: 3918 (million) % 299.98/43.14 % (1955846)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=678575761:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2678 on theBenchmark for (2678ds/3980Mi) % 299.98/43.14 % (1955840)Instruction limit reached! % 299.98/43.14 % (1955840)------------------------------ % 299.98/43.14 % (1955840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.98/43.14 % (1955840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.98/43.14 % (1955840)CaDiCaL version: 2.1.3 % 299.98/43.14 % (1955840)Termination reason: Instruction limit % 299.98/43.14 % (1955840)Termination phase: Saturation % 299.98/43.14 % (1955840)Time elapsed: 2.180 s % 299.98/43.14 % (1955840)Peak memory usage: 158 MB % 299.98/43.14 % (1955840)Instructions burned: 3902 (million) % 299.98/43.14 % (1955848)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=3885346097:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2674 on theBenchmark for (2674ds/2087Mi) % 299.98/43.14 % (1955843)Instruction limit reached! % 299.98/43.14 % (1955843)------------------------------ % 299.98/43.14 % (1955843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.98/43.14 % (1955843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.98/43.14 % (1955843)CaDiCaL version: 2.1.3 % 299.98/43.14 % (1955843)Termination reason: Instruction limit % 299.98/43.14 % (1955843)Termination phase: Saturation % 299.98/43.14 % (1955843)Time elapsed: 2.416 s % 299.98/43.14 % (1955843)Peak memory usage: 150 MB % 299.98/43.14 % (1955843)Instructions burned: 3940 (million) % 299.98/43.14 % (1955846)Instruction limit reached! % 299.98/43.14 % (1955846)------------------------------ % 299.98/43.14 % (1955846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.98/43.14 % (1955846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.98/43.14 % (1955846)CaDiCaL version: 2.1.3 % 299.98/43.14 % (1955846)Termination reason: Instruction limit % 299.98/43.14 % (1955846)Termination phase: Saturation % 299.98/43.14 % (1955846)Time elapsed: 1.348 s % 299.98/43.14 % (1955846)Peak memory usage: 157 MB % 299.98/43.14 % (1955846)Instructions burned: 3982 (million) % 299.98/43.14 % (1955850)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=2302950358:cts=off:cond=on:i=4272:bs=on:fsd=on_2665 on theBenchmark for (2665ds/4272Mi) % 299.98/43.14 % (195585Terminated % 300.41/43.24 % Vampire exiting % 300.41/43.24 Terminated %------------------------------------------------------------------------------