%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV548-1.004 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n013.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:17:57 PM UTC 2026 % Result : Timeout 301.35s 43.05s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWV548-1.004 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.26 % Computer : n013.cluster.edu % 0.10/0.26 % Model : x86_64 x86_64 % 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.26 % Memory : 8046.5625MB % 0.10/0.26 % OS : Linux 6.8.0-71-generic % 0.10/0.26 % CPULimit : 300 % 0.10/0.26 % WCLimit : 300 % 0.10/0.26 % DateTime : Mon Sep 28 11:43:21 UTC 2026 % 0.10/0.26 % CPUTime : % 0.10/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.25/0.31 Running first-order theorem proving % 0.25/0.31 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.16/2.94 % (1120438)Input is clausal, will run a generic CNF schedule. % 16.16/2.94 % (1120451)dis-21_1_sil=8000:lcm=predicate:random_seed=239618819: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) % 16.16/2.94 % (1120451)Refutation not found, incomplete strategy % 16.16/2.94 % (1120451)------------------------------ % 16.16/2.94 % (1120451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.16/2.94 % (1120451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.16/2.94 % (1120451)CaDiCaL version: 2.1.3 % 16.16/2.94 % (1120451)Termination reason: Refutation not found, incomplete strategy % 16.16/2.94 % (1120451)Time elapsed: 0.001 s % 16.16/2.94 % (1120451)Peak memory usage: 88 MB % 16.16/2.94 % (1120451)Instructions burned: 1 (million) % 16.16/2.94 % (1120445)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=3585258093:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 16.16/2.94 % (1120448)lrs+10_1_sil=8000:sp=occurrence:random_seed=2915993507:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 16.16/2.94 % (1120449)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2904174214:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 16.16/2.94 % (1120447)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4039315010:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 16.16/2.94 % (1120450)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1715054192:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 16.16/2.94 % (1120446)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1487210910:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 16.16/2.94 % (1120448)Instruction limit reached! % 16.16/2.94 % (1120448)------------------------------ % 16.16/2.94 % (1120448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.16/2.94 % (1120448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.16/2.94 % (1120448)CaDiCaL version: 2.1.3 % 16.16/2.94 % (1120448)Termination reason: Instruction limit % 16.16/2.94 % (1120448)Termination phase: Saturation % 16.16/2.94 % (1120448)Time elapsed: 0.101 s % 16.16/2.94 % (1120448)Peak memory usage: 89 MB % 16.16/2.94 % (1120448)Instructions burned: 107 (million) % 16.16/2.94 % (1120449)Instruction limit reached! % 16.16/2.94 % (1120449)------------------------------ % 16.16/2.94 % (1120449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.16/2.94 % (1120449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.16/2.94 % (1120449)CaDiCaL version: 2.1.3 % 16.16/2.94 % (1120449)Termination reason: Instruction limit % 16.16/2.94 % (1120449)Termination phase: Saturation % 16.16/2.94 % (1120449)Time elapsed: 0.102 s % 16.16/2.94 % (1120449)Peak memory usage: 88 MB % 16.16/2.94 % (1120449)Instructions burned: 115 (million) % 16.16/2.94 % (1120450)Instruction limit reached! % 16.16/2.94 % (1120450)------------------------------ % 16.16/2.94 % (1120450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.16/2.94 % (1120450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.16/2.94 % (1120450)CaDiCaL version: 2.1.3 % 16.16/2.94 % (1120450)Termination reason: Instruction limit % 16.16/2.94 % (1120450)Termination phase: Saturation % 16.16/2.94 % (1120450)Time elapsed: 0.172 s % 16.16/2.94 % (1120450)Peak memory usage: 89 MB % 16.16/2.94 % (1120450)Instructions burned: 180 (million) % 16.16/2.94 % (1120451)------------------------------ % 16.16/2.94 % (1120451)------------------------------ % 16.16/2.94 % (1120460)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=4051533203:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi) % 16.16/2.94 % (1120461)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3478476419: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) % 16.16/2.94 % (1120463)lrs+10_64_to=lpo:sil=8000:random_seed=4261553837:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 16.16/2.94 % (1120462)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=445419818:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi) % 33.22/5.39 % (1120463)Instruction limit reached! % 33.22/5.39 % (1120463)------------------------------ % 33.22/5.39 % (1120463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.39 % (1120463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.39 % (1120463)CaDiCaL version: 2.1.3 % 33.22/5.39 % (1120463)Termination reason: Instruction limit % 33.22/5.39 % (1120463)Termination phase: Saturation % 33.22/5.39 % (1120463)Time elapsed: 0.058 s % 33.22/5.39 % (1120463)Peak memory usage: 88 MB % 33.22/5.39 % (1120463)Instructions burned: 126 (million) % 33.22/5.39 % (1120460)Instruction limit reached! % 33.22/5.39 % (1120460)------------------------------ % 33.22/5.39 % (1120460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.39 % (1120460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.39 % (1120460)CaDiCaL version: 2.1.3 % 33.22/5.39 % (1120460)Termination reason: Instruction limit % 33.22/5.39 % (1120460)Termination phase: Saturation % 33.22/5.39 % (1120460)Time elapsed: 0.144 s % 33.22/5.39 % (1120460)Peak memory usage: 89 MB % 33.22/5.39 % (1120460)Instructions burned: 143 (million) % 33.22/5.39 % (1120461)Instruction limit reached! % 33.22/5.39 % (1120461)------------------------------ % 33.22/5.39 % (1120461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.39 % (1120461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.39 % (1120461)CaDiCaL version: 2.1.3 % 33.22/5.39 % (1120461)Termination reason: Instruction limit % 33.22/5.39 % (1120461)Termination phase: Saturation % 33.22/5.39 % (1120461)Time elapsed: 0.160 s % 33.22/5.39 % (1120461)Peak memory usage: 89 MB % 33.22/5.39 % (1120461)Instructions burned: 190 (million) % 33.22/5.39 % (1120462)Instruction limit reached! % 33.22/5.39 % (1120462)------------------------------ % 33.22/5.39 % (1120462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.39 % (1120462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.39 % (1120462)CaDiCaL version: 2.1.3 % 33.22/5.39 % (1120462)Termination reason: Instruction limit % 33.22/5.39 % (1120462)Termination phase: Saturation % 33.22/5.39 % (1120462)Time elapsed: 0.188 s % 33.22/5.39 % (1120462)Peak memory usage: 89 MB % 33.22/5.39 % (1120462)Instructions burned: 219 (million) % 33.22/5.39 % (1120468)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1711458941:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi) % 33.22/5.39 % (1120469)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2967514700:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi) % 33.22/5.39 % (1120470)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=640776290:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi) % 33.22/5.39 % (1120469)Instruction limit reached! % 33.22/5.39 % (1120469)------------------------------ % 33.22/5.39 % (1120469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.39 % (1120469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.39 % (1120469)CaDiCaL version: 2.1.3 % 33.22/5.39 % (1120469)Termination reason: Instruction limit % 33.22/5.39 % (1120469)Termination phase: Saturation % 33.22/5.39 % (1120469)Time elapsed: 0.085 s % 33.22/5.39 % (1120469)Peak memory usage: 90 MB % 33.22/5.39 % (1120469)Instructions burned: 158 (million) % 33.22/5.39 % (1120471)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=2835843792:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi) % 33.22/5.39 % (1120468)Instruction limit reached! % 33.22/5.39 % (1120468)------------------------------ % 33.22/5.39 % (1120468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.39 % (1120468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.39 % (1120468)CaDiCaL version: 2.1.3 % 33.22/5.39 % (1120468)Termination reason: Instruction limit % 33.22/5.39 % (1120468)Termination phase: Saturation % 33.22/5.39 % (1120468)Time elapsed: 0.189 s % 33.22/5.39 % (1120468)Peak memory usage: 90 MB % 33.22/5.39 % (1120468)Instructions burned: 194 (million) % 33.22/5.39 % (1120471)Instruction limit reached! % 33.22/5.39 % (1120471)------------------------------ % 33.22/5.39 % (1120471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.39 % (1120471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.44/7.86 % (1120471)CaDiCaL version: 2.1.3 % 50.44/7.86 % (1120471)Termination reason: Instruction limit % 50.44/7.86 % (1120471)Termination phase: Saturation % 50.44/7.86 % (1120471)Time elapsed: 0.099 s % 50.44/7.86 % (1120471)Peak memory usage: 89 MB % 50.44/7.86 % (1120471)Instructions burned: 106 (million) % 50.44/7.86 % (1120475)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3723852020:i=107_2989 on theBenchmark for (2989ds/107Mi) % 50.44/7.86 % (1120475)Instruction limit reached! % 50.44/7.86 % (1120475)------------------------------ % 50.44/7.86 % (1120475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.44/7.86 % (1120475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.44/7.86 % (1120475)CaDiCaL version: 2.1.3 % 50.44/7.86 % (1120475)Termination reason: Instruction limit % 50.44/7.86 % (1120475)Termination phase: Saturation % 50.44/7.86 % (1120475)Time elapsed: 0.058 s % 50.44/7.86 % (1120475)Peak memory usage: 89 MB % 50.44/7.86 % (1120475)Instructions burned: 107 (million) % 50.44/7.86 % (1120477)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3207246848:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi) % 50.44/7.86 % (1120478)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1243832942:cond=fast:i=5208:av=off_2988 on theBenchmark for (2988ds/5208Mi) % 50.44/7.86 % (1120480)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3705478790:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi) % 50.44/7.86 % (1120480)Instruction limit reached! % 50.44/7.86 % (1120480)------------------------------ % 50.44/7.86 % (1120480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.44/7.86 % (1120480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.44/7.86 % (1120480)CaDiCaL version: 2.1.3 % 50.44/7.86 % (1120480)Termination reason: Instruction limit % 50.44/7.86 % (1120480)Termination phase: Saturation % 50.44/7.86 % (1120480)Time elapsed: 0.070 s % 50.44/7.86 % (1120480)Peak memory usage: 89 MB % 50.44/7.86 % (1120480)Instructions burned: 135 (million) % 50.44/7.86 % (1120477)Instruction limit reached! % 50.44/7.86 % (1120477)------------------------------ % 50.44/7.86 % (1120477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.44/7.86 % (1120477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.44/7.86 % (1120477)CaDiCaL version: 2.1.3 % 50.44/7.86 % (1120477)Termination reason: Instruction limit % 50.44/7.86 % (1120477)Termination phase: Saturation % 50.44/7.86 % (1120477)Time elapsed: 0.217 s % 50.44/7.86 % (1120477)Peak memory usage: 90 MB % 50.44/7.86 % (1120477)Instructions burned: 242 (million) % 50.44/7.86 % (1120484)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=246484555:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi) % 50.44/7.86 % (1120485)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1795955169:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi) % 50.44/7.86 % (1120484)Instruction limit reached! % 50.44/7.86 % (1120484)------------------------------ % 50.44/7.86 % (1120484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.44/7.86 % (1120484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.44/7.86 % (1120484)CaDiCaL version: 2.1.3 % 50.44/7.86 % (1120484)Termination reason: Instruction limit % 50.44/7.86 % (1120484)Termination phase: Saturation % 50.44/7.86 % (1120484)Time elapsed: 0.258 s % 50.44/7.86 % (1120484)Peak memory usage: 93 MB % 50.44/7.86 % (1120484)Instructions burned: 500 (million) % 50.44/7.86 % (1120485)Instruction limit reached! % 50.44/7.86 % (1120485)------------------------------ % 50.44/7.86 % (1120485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.44/7.86 % (1120485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.44/7.86 % (1120485)CaDiCaL version: 2.1.3 % 50.44/7.86 % (1120485)Termination reason: Instruction limit % 50.44/7.86 % (1120485)Termination phase: Saturation % 50.44/7.86 % (1120485)Time elapsed: 0.195 s % 50.44/7.86 % (1120485)Peak memory usage: 89 MB % 50.44/7.86 % (1120485)Instructions burned: 191 (million) % 50.44/7.86 % (1120488)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=81595317:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi) % 89.21/13.17 % (1120489)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2116862753:cond=on:i=156:bs=on:gtg=exists_all:er=known_2978 on theBenchmark for (2978ds/156Mi) % 89.21/13.17 % (1120488)Instruction limit reached! % 89.21/13.17 % (1120488)------------------------------ % 89.21/13.17 % (1120488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.21/13.17 % (1120488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.21/13.17 % (1120488)CaDiCaL version: 2.1.3 % 89.21/13.17 % (1120488)Termination reason: Instruction limit % 89.21/13.17 % (1120488)Termination phase: Saturation % 89.21/13.17 % (1120488)Time elapsed: 0.135 s % 89.21/13.17 % (1120488)Peak memory usage: 91 MB % 89.21/13.17 % (1120488)Instructions burned: 265 (million) % 89.21/13.17 % (1120489)Instruction limit reached! % 89.21/13.17 % (1120489)------------------------------ % 89.21/13.17 % (1120489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.21/13.17 % (1120489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.21/13.17 % (1120489)CaDiCaL version: 2.1.3 % 89.21/13.17 % (1120489)Termination reason: Instruction limit % 89.21/13.17 % (1120489)Termination phase: Saturation % 89.21/13.17 % (1120489)Time elapsed: 0.172 s % 89.21/13.17 % (1120489)Peak memory usage: 90 MB % 89.21/13.17 % (1120489)Instructions burned: 156 (million) % 89.21/13.17 % (1120492)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=3865449896:i=3256:kws=precedence:bd=preordered:av=off_2975 on theBenchmark for (2975ds/3256Mi) % 89.21/13.17 % (1120493)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3792764457:i=537:av=off:ss=included_2973 on theBenchmark for (2973ds/537Mi) % 89.21/13.17 % (1120493)Instruction limit reached! % 89.21/13.17 % (1120493)------------------------------ % 89.21/13.17 % (1120493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.21/13.17 % (1120493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.21/13.17 % (1120493)CaDiCaL version: 2.1.3 % 89.21/13.17 % (1120493)Termination reason: Instruction limit % 89.21/13.17 % (1120493)Termination phase: Saturation % 89.21/13.17 % (1120493)Time elapsed: 0.426 s % 89.21/13.17 % (1120493)Peak memory usage: 89 MB % 89.21/13.17 % (1120493)Instructions burned: 538 (million) % 89.21/13.17 % (1120496)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2477792449:i=180:bd=preordered:av=off_2966 on theBenchmark for (2966ds/180Mi) % 89.21/13.17 % (1120496)Instruction limit reached! % 89.21/13.17 % (1120496)------------------------------ % 89.21/13.17 % (1120496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.21/13.17 % (1120496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.21/13.17 % (1120496)CaDiCaL version: 2.1.3 % 89.21/13.17 % (1120496)Termination reason: Instruction limit % 89.21/13.17 % (1120496)Termination phase: Saturation % 89.21/13.17 % (1120496)Time elapsed: 0.173 s % 89.21/13.17 % (1120496)Peak memory usage: 89 MB % 89.21/13.17 % (1120496)Instructions burned: 181 (million) % 89.21/13.17 % (1120498)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=3894256325:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2961 on theBenchmark for (2961ds/10307Mi) % 89.21/13.17 % (1120492)Instruction limit reached! % 89.21/13.17 % (1120492)------------------------------ % 89.21/13.17 % (1120492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.21/13.17 % (1120492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.21/13.17 % (1120492)CaDiCaL version: 2.1.3 % 89.21/13.17 % (1120492)Termination reason: Instruction limit % 89.21/13.17 % (1120492)Termination phase: Saturation % 89.21/13.17 % (1120492)Time elapsed: 1.838 s % 89.21/13.17 % (1120492)Peak memory usage: 151 MB % 89.21/13.17 % (1120492)Instructions burned: 3257 (million) % 89.21/13.17 % (1120470)Instruction limit reached! % 89.21/13.17 % (1120470)------------------------------ % 89.21/13.17 % (1120470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.21/13.17 % (1120470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.21/13.17 % (1120470)CaDiCaL version: 2.1.3 % 89.21/13.17 % (1120470)Termination reason: Instruction limit % 89.21/13.17 % (1120470)Termination phase: Saturation % 89.21/13.17 % (1120470)Time elapsed: 3.493 s % 89.21/13.17 % (1120470)Peak memory usage: 150 MB % 89.21/13.17 % (1120470)Instructions burned: 3394 (million) % 89.21/13.17 % (1120503)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=1886243673:i=412:gtgl=4:gtg=exists_all_2954 on theBenchmark for (2954ds/412Mi) % 111.41/16.36 % (1120504)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=1311383933:s2pl=no:i=8478:s2at=4:nm=6_2954 on theBenchmark for (2954ds/8478Mi) % 111.41/16.36 % (1120503)Instruction limit reached! % 111.41/16.36 % (1120503)------------------------------ % 111.41/16.36 % (1120503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.41/16.36 % (1120503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.41/16.36 % (1120503)CaDiCaL version: 2.1.3 % 111.41/16.36 % (1120503)Termination reason: Instruction limit % 111.41/16.36 % (1120503)Termination phase: Saturation % 111.41/16.36 % (1120503)Time elapsed: 0.226 s % 111.41/16.36 % (1120503)Peak memory usage: 93 MB % 111.41/16.36 % (1120503)Instructions burned: 414 (million) % 111.41/16.36 % (1120508)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=635967637:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2950 on theBenchmark for (2950ds/303Mi) % 111.41/16.36 % (1120508)Refutation not found, incomplete strategy % 111.41/16.36 % (1120508)------------------------------ % 111.41/16.36 % (1120508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.41/16.36 % (1120508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.41/16.36 % (1120508)CaDiCaL version: 2.1.3 % 111.41/16.36 % (1120508)Termination reason: Refutation not found, incomplete strategy % 111.41/16.36 % (1120508)Time elapsed: 0.002 s % 111.41/16.36 % (1120508)Peak memory usage: 88 MB % 111.41/16.36 % (1120508)Instructions burned: 2 (million) % 111.41/16.36 % (1120508)------------------------------ % 111.41/16.36 % (1120508)------------------------------ % 111.41/16.36 % (1120510)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=308554317:st=4:i=720:sd=3:fsr=off:ss=axioms_2945 on theBenchmark for (2945ds/720Mi) % 111.41/16.36 % (1120510)Instruction limit reached! % 111.41/16.36 % (1120510)------------------------------ % 111.41/16.36 % (1120510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.41/16.36 % (1120510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.41/16.36 % (1120510)CaDiCaL version: 2.1.3 % 111.41/16.36 % (1120510)Termination reason: Instruction limit % 111.41/16.36 % (1120510)Termination phase: Saturation % 111.41/16.36 % (1120510)Time elapsed: 0.296 s % 111.41/16.36 % (1120510)Peak memory usage: 92 MB % 111.41/16.36 % (1120510)Instructions burned: 720 (million) % 111.41/16.36 % (1120512)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2844030257:i=598:bs=on:bd=preordered:av=off:ss=axioms_2940 on theBenchmark for (2940ds/598Mi) % 111.41/16.36 % (1120512)Instruction limit reached! % 111.41/16.36 % (1120512)------------------------------ % 111.41/16.36 % (1120512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.41/16.36 % (1120512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.41/16.36 % (1120512)CaDiCaL version: 2.1.3 % 111.41/16.36 % (1120512)Termination reason: Instruction limit % 111.41/16.36 % (1120512)Termination phase: Saturation % 111.41/16.36 % (1120512)Time elapsed: 0.322 s % 111.41/16.36 % (1120512)Peak memory usage: 95 MB % 111.41/16.36 % (1120512)Instructions burned: 600 (million) % 111.41/16.36 % (1120516)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1486674672:i=2989:sd=3:ss=axioms:sgt=60_2934 on theBenchmark for (2934ds/2989Mi) % 111.41/16.36 % (1120478)Instruction limit reached! % 111.41/16.36 % (1120478)------------------------------ % 111.41/16.36 % (1120478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.41/16.36 % (1120478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.41/16.36 % (1120478)CaDiCaL version: 2.1.3 % 111.41/16.36 % (1120478)Termination reason: Instruction limit % 111.41/16.36 % (1120478)Termination phase: Saturation % 111.41/16.36 % (1120478)Time elapsed: 5.447 s % 111.41/16.36 % (1120478)Peak memory usage: 161 MB % 111.41/16.36 % (1120478)Instructions burned: 5208 (million) % 111.41/16.36 % (1120518)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=3788954646:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2930 on theBenchmark for (2930ds/1997Mi) % 164.88/23.81 % (1120516)Instruction limit reached! % 164.88/23.81 % (1120516)------------------------------ % 164.88/23.81 % (1120516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.88/23.81 % (1120516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.88/23.81 % (1120516)CaDiCaL version: 2.1.3 % 164.88/23.81 % (1120516)Termination reason: Instruction limit % 164.88/23.81 % (1120516)Termination phase: Saturation % 164.88/23.81 % (1120516)Time elapsed: 1.736 s % 164.88/23.81 % (1120516)Peak memory usage: 145 MB % 164.88/23.81 % (1120516)Instructions burned: 2990 (million) % 164.88/23.81 % (1120526)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=883749327:i=2088:bd=preordered:av=off_2914 on theBenchmark for (2914ds/2088Mi) % 164.88/23.81 % (1120518)Instruction limit reached! % 164.88/23.81 % (1120518)------------------------------ % 164.88/23.81 % (1120518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.88/23.81 % (1120518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.88/23.81 % (1120518)CaDiCaL version: 2.1.3 % 164.88/23.81 % (1120518)Termination reason: Instruction limit % 164.88/23.81 % (1120518)Termination phase: Saturation % 164.88/23.81 % (1120518)Time elapsed: 2.121 s % 164.88/23.81 % (1120518)Peak memory usage: 137 MB % 164.88/23.81 % (1120518)Instructions burned: 1997 (million) % 164.88/23.81 % (1120530)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2422015370:i=1098:nicw=on_2906 on theBenchmark for (2906ds/1098Mi) % 164.88/23.81 % (1120526)Instruction limit reached! % 164.88/23.81 % (1120526)------------------------------ % 164.88/23.81 % (1120526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.88/23.81 % (1120526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.88/23.81 % (1120526)CaDiCaL version: 2.1.3 % 164.88/23.81 % (1120526)Termination reason: Instruction limit % 164.88/23.81 % (1120526)Termination phase: Saturation % 164.88/23.81 % (1120526)Time elapsed: 1.175 s % 164.88/23.81 % (1120526)Peak memory usage: 139 MB % 164.88/23.81 % (1120526)Instructions burned: 2089 (million) % 164.88/23.81 % (1120534)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2522042031:i=433:bd=preordered_2900 on theBenchmark for (2900ds/433Mi) % 164.88/23.81 % (1120534)Instruction limit reached! % 164.88/23.81 % (1120534)------------------------------ % 164.88/23.81 % (1120534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.88/23.81 % (1120534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.88/23.81 % (1120534)CaDiCaL version: 2.1.3 % 164.88/23.81 % (1120534)Termination reason: Instruction limit % 164.88/23.81 % (1120534)Termination phase: Saturation % 164.88/23.81 % (1120534)Time elapsed: 0.193 s % 164.88/23.81 % (1120534)Peak memory usage: 91 MB % 164.88/23.81 % (1120534)Instructions burned: 434 (million) % 164.88/23.81 % (1120536)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1161035265:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2896 on theBenchmark for (2896ds/2942Mi) % 164.88/23.81 % (1120530)Instruction limit reached! % 164.88/23.81 % (1120530)------------------------------ % 164.88/23.81 % (1120530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.88/23.81 % (1120530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.88/23.81 % (1120530)CaDiCaL version: 2.1.3 % 164.88/23.81 % (1120530)Termination reason: Instruction limit % 164.88/23.81 % (1120530)Termination phase: Saturation % 164.88/23.81 % (1120530)Time elapsed: 1.042 s % 164.88/23.81 % (1120530)Peak memory usage: 105 MB % 164.88/23.81 % (1120530)Instructions burned: 1098 (million) % 164.88/23.81 % (1120539)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3508028337:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2892 on theBenchmark for (2892ds/6922Mi) % 164.88/23.81 % (1120498)Instruction limit reached! % 164.88/23.81 % (1120498)------------------------------ % 164.88/23.81 % (1120498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.88/23.81 % (1120498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.88/23.81 % (1120498)CaDiCaL version: 2.1.3 % 164.88/23.81 % (1120498)Termination reason: Instruction limit % 188.95/27.25 % (1120498)Termination phase: Saturation % 188.95/27.25 % (1120498)Time elapsed: 8.392 s % 188.95/27.25 % (1120498)Peak memory usage: 145 MB % 188.95/27.25 % (1120498)Instructions burned: 10307 (million) % 188.95/27.25 % (1120548)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=4022154765:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2874 on theBenchmark for (2874ds/596Mi) % 188.95/27.25 % (1120548)Refutation not found, incomplete strategy % 188.95/27.25 % (1120548)------------------------------ % 188.95/27.25 % (1120548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.95/27.25 % (1120548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.95/27.25 % (1120548)CaDiCaL version: 2.1.3 % 188.95/27.25 % (1120548)Termination reason: Refutation not found, incomplete strategy % 188.95/27.25 % (1120548)Time elapsed: 0.002 s % 188.95/27.25 % (1120548)Peak memory usage: 88 MB % 188.95/27.25 % (1120548)Instructions burned: 3 (million) % 188.95/27.25 % (1120548)------------------------------ % 188.95/27.25 % (1120548)------------------------------ % 188.95/27.25 % (1120504)Instruction limit reached! % 188.95/27.25 % (1120504)------------------------------ % 188.95/27.25 % (1120504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.95/27.25 % (1120504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.95/27.25 % (1120504)CaDiCaL version: 2.1.3 % 188.95/27.25 % (1120504)Termination reason: Instruction limit % 188.95/27.25 % (1120504)Termination phase: Saturation % 188.95/27.25 % (1120504)Time elapsed: 8.289 s % 188.95/27.25 % (1120504)Peak memory usage: 195 MB % 188.95/27.25 % (1120504)Instructions burned: 8478 (million) % 188.95/27.25 % (1120550)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=693897259:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2869 on theBenchmark for (2869ds/4123Mi) % 188.95/27.25 % (1120551)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3840151834:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2868 on theBenchmark for (2868ds/16411Mi) % 188.95/27.25 % (1120536)Instruction limit reached! % 188.95/27.25 % (1120536)------------------------------ % 188.95/27.25 % (1120536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.95/27.25 % (1120536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.95/27.25 % (1120536)CaDiCaL version: 2.1.3 % 188.95/27.25 % (1120536)Termination reason: Instruction limit % 188.95/27.25 % (1120536)Termination phase: Saturation % 188.95/27.25 % (1120536)Time elapsed: 2.976 s % 188.95/27.25 % (1120536)Peak memory usage: 146 MB % 188.95/27.25 % (1120536)Instructions burned: 2942 (million) % 188.95/27.25 % (1120555)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=879000875:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2864 on theBenchmark for (2864ds/1670Mi) % 188.95/27.25 % (1120555)Instruction limit reached! % 188.95/27.25 % (1120555)------------------------------ % 188.95/27.25 % (1120555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.95/27.25 % (1120555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.95/27.25 % (1120555)CaDiCaL version: 2.1.3 % 188.95/27.25 % (1120555)Termination reason: Instruction limit % 188.95/27.25 % (1120555)Termination phase: Saturation % 188.95/27.25 % (1120555)Time elapsed: 1.702 s % 188.95/27.25 % (1120555)Peak memory usage: 134 MB % 188.95/27.25 % (1120555)Instructions burned: 1670 (million) % 188.95/27.25 % (1120550)Instruction limit reached! % 188.95/27.25 % (1120550)------------------------------ % 188.95/27.25 % (1120550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.95/27.25 % (1120550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.95/27.25 % (1120550)CaDiCaL version: 2.1.3 % 188.95/27.25 % (1120550)Termination reason: Instruction limit % 188.95/27.25 % (1120550)Termination phase: Saturation % 188.95/27.25 % (1120550)Time elapsed: 2.306 s % 188.95/27.25 % (1120550)Peak memory usage: 160 MB % 188.95/27.25 % (1120550)Instructions burned: 4124 (million) % 188.95/27.25 % (1120564)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=1137461572:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2844 on theBenchmark for (2844ds/1722Mi) % 188.95/27.25 % (1120565)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=2870417502:cts=off:cond=on:i=9530:bs=on:fsd=on_2844 on theBenchmark for (2844ds/9530Mi) % 228.74/32.81 % (1120539)Instruction limit reached! % 228.74/32.81 % (1120539)------------------------------ % 228.74/32.81 % (1120539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.74/32.81 % (1120539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.74/32.81 % (1120539)CaDiCaL version: 2.1.3 % 228.74/32.81 % (1120539)Termination reason: Instruction limit % 228.74/32.81 % (1120539)Termination phase: Saturation % 228.74/32.81 % (1120539)Time elapsed: 5.680 s % 228.74/32.81 % (1120539)Peak memory usage: 187 MB % 228.74/32.81 % (1120539)Instructions burned: 6922 (million) % 228.74/32.81 % (1120564)Instruction limit reached! % 228.74/32.81 % (1120564)------------------------------ % 228.74/32.81 % (1120564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.74/32.81 % (1120564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.74/32.81 % (1120564)CaDiCaL version: 2.1.3 % 228.74/32.81 % (1120564)Termination reason: Instruction limit % 228.74/32.81 % (1120564)Termination phase: Saturation % 228.74/32.81 % (1120564)Time elapsed: 0.965 s % 228.74/32.81 % (1120564)Peak memory usage: 131 MB % 228.74/32.81 % (1120564)Instructions burned: 1722 (million) % 228.74/32.81 % (1120569)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4093851276:st=2:i=4495:sd=10:ss=included_2833 on theBenchmark for (2833ds/4495Mi) % 228.74/32.81 % (1120570)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=1447976805:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2833 on theBenchmark for (2833ds/4920Mi) % 228.74/32.81 % (1120569)Instruction limit reached! % 228.74/32.81 % (1120569)------------------------------ % 228.74/32.81 % (1120569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.74/32.81 % (1120569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.74/32.81 % (1120569)CaDiCaL version: 2.1.3 % 228.74/32.81 % (1120569)Termination reason: Instruction limit % 228.74/32.81 % (1120569)Termination phase: Saturation % 228.74/32.81 % (1120569)Time elapsed: 2.540 s % 228.74/32.81 % (1120569)Peak memory usage: 162 MB % 228.74/32.81 % (1120569)Instructions burned: 4495 (million) % 228.74/32.81 % (1120578)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=1066456053:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2806 on theBenchmark for (2806ds/2083Mi) % 228.74/32.81 % (1120578)Instruction limit reached! % 228.74/32.81 % (1120578)------------------------------ % 228.74/32.81 % (1120578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.74/32.81 % (1120578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.74/32.81 % (1120578)CaDiCaL version: 2.1.3 % 228.74/32.81 % (1120578)Termination reason: Instruction limit % 228.74/32.81 % (1120578)Termination phase: Saturation % 228.74/32.81 % (1120578)Time elapsed: 1.223 s % 228.74/32.81 % (1120578)Peak memory usage: 138 MB % 228.74/32.81 % (1120578)Instructions burned: 2085 (million) % 228.74/32.81 % (1120584)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=602769406:i=4629:av=off:gsp=on_2791 on theBenchmark for (2791ds/4629Mi) % 228.74/32.81 % (1120570)Instruction limit reached! % 228.74/32.81 % (1120570)------------------------------ % 228.74/32.81 % (1120570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.74/32.81 % (1120570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.74/32.81 % (1120570)CaDiCaL version: 2.1.3 % 228.74/32.81 % (1120570)Termination reason: Instruction limit % 228.74/32.81 % (1120570)Termination phase: Saturation % 228.74/32.81 % (1120570)Time elapsed: 4.750 s % 228.74/32.81 % (1120570)Peak memory usage: 147 MB % 228.74/32.81 % (1120570)Instructions burned: 4920 (million) % 228.74/32.81 % (1120587)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=886301811:i=1258:av=off_2782 on theBenchmark for (2782ds/1258Mi) % 228.74/32.81 % (1120587)Instruction limit reached! % 228.74/32.81 % (1120587)------------------------------ % 228.74/32.81 % (1120587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.74/32.81 % (1120587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.80/36.82 % (1120587)CaDiCaL version: 2.1.3 % 255.80/36.82 % (1120587)Termination reason: Instruction limit % 255.80/36.82 % (1120587)Termination phase: Saturation % 255.80/36.82 % (1120587)Time elapsed: 1.121 s % 255.80/36.82 % (1120587)Peak memory usage: 96 MB % 255.80/36.82 % (1120587)Instructions burned: 1259 (million) % 255.80/36.82 % (1120565)Instruction limit reached! % 255.80/36.82 % (1120565)------------------------------ % 255.80/36.82 % (1120565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.80/36.82 % (1120565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.80/36.82 % (1120565)CaDiCaL version: 2.1.3 % 255.80/36.82 % (1120565)Termination reason: Instruction limit % 255.80/36.82 % (1120565)Termination phase: Saturation % 255.80/36.82 % (1120565)Time elapsed: 7.633 s % 255.80/36.82 % (1120565)Peak memory usage: 140 MB % 255.80/36.82 % (1120565)Instructions burned: 9530 (million) % 255.80/36.82 % (1120592)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1576521139:i=7343:av=off:ss=included_2768 on theBenchmark for (2768ds/7343Mi) % 255.80/36.82 % (1120593)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2349435506:i=1325:sd=2:ss=axioms:sgt=16_2766 on theBenchmark for (2766ds/1325Mi) % 255.80/36.82 % (1120584)Instruction limit reached! % 255.80/36.82 % (1120584)------------------------------ % 255.80/36.82 % (1120584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.80/36.82 % (1120584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.80/36.82 % (1120584)CaDiCaL version: 2.1.3 % 255.80/36.82 % (1120584)Termination reason: Instruction limit % 255.80/36.82 % (1120584)Termination phase: Saturation % 255.80/36.82 % (1120584)Time elapsed: 2.613 s % 255.80/36.82 % (1120584)Peak memory usage: 150 MB % 255.80/36.82 % (1120584)Instructions burned: 4631 (million) % 255.80/36.82 % (1120597)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=28787541:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2762 on theBenchmark for (2762ds/2646Mi) % 255.80/36.82 % (1120593)Instruction limit reached! % 255.80/36.82 % (1120593)------------------------------ % 255.80/36.82 % (1120593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.80/36.82 % (1120593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.80/36.82 % (1120593)CaDiCaL version: 2.1.3 % 255.80/36.82 % (1120593)Termination reason: Instruction limit % 255.80/36.82 % (1120593)Termination phase: Saturation % 255.80/36.82 % (1120593)Time elapsed: 0.685 s % 255.80/36.82 % (1120593)Peak memory usage: 97 MB % 255.80/36.82 % (1120593)Instructions burned: 1325 (million) % 255.80/36.82 % (1120601)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1766298288:i=1489:sd=2:ep=R:ss=axioms_2756 on theBenchmark for (2756ds/1489Mi) % 255.80/36.82 % (1120601)Refutation not found, incomplete strategy % 255.80/36.82 % (1120601)------------------------------ % 255.80/36.82 % (1120601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.80/36.82 % (1120601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.80/36.82 % (1120601)CaDiCaL version: 2.1.3 % 255.80/36.82 % (1120601)Termination reason: Refutation not found, incomplete strategy % 255.80/36.82 % (1120601)Time elapsed: 0.569 s % 255.80/36.82 % (1120601)Peak memory usage: 128 MB % 255.80/36.82 % (1120601)Instructions burned: 900 (million) % 255.80/36.82 % (1120601)------------------------------ % 255.80/36.82 % (1120601)------------------------------ % 255.80/36.82 % (1120606)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=814443270:i=1503_2746 on theBenchmark for (2746ds/1503Mi) % 255.80/36.82 % (1120606)Instruction limit reached! % 255.80/36.82 % (1120606)------------------------------ % 255.80/36.82 % (1120606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.80/36.82 % (1120606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.80/36.82 % (1120606)CaDiCaL version: 2.1.3 % 255.80/36.82 % (1120606)Termination reason: Instruction limit % 255.80/36.82 % (1120606)Termination phase: Saturation % 255.80/36.82 % (1120606)Time elapsed: 0.909 s % 255.80/36.82 % (1120606)Peak memory usage: 134 MB % 255.80/36.82 % (1120606)Instructions burned: 1503 (million) % 255.80/36.82 % (1120597)Instruction limit reached! % 255.80/36.82 % (1120597)------------------------------ % 255.80/36.82 % (1120597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.28/39.51 % (1120597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.28/39.51 % (1120597)CaDiCaL version: 2.1.3 % 276.28/39.51 % (1120597)Termination reason: Instruction limit % 276.28/39.51 % (1120597)Termination phase: Saturation % 276.28/39.51 % (1120597)Time elapsed: 2.602 s % 276.28/39.51 % (1120597)Peak memory usage: 139 MB % 276.28/39.51 % (1120597)Instructions burned: 2647 (million) % 276.28/39.51 % (1120609)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=456544399:i=13942:kws=frequency_2735 on theBenchmark for (2735ds/13942Mi) % 276.28/39.51 % (1120611)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=3022218967:i=3604:fsr=off:er=filter_2733 on theBenchmark for (2733ds/3604Mi) % 276.28/39.51 % (1120611)Instruction limit reached! % 276.28/39.51 % (1120611)------------------------------ % 276.28/39.51 % (1120611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.28/39.51 % (1120611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.28/39.51 % (1120611)CaDiCaL version: 2.1.3 % 276.28/39.51 % (1120611)Termination reason: Instruction limit % 276.28/39.51 % (1120611)Termination phase: Saturation % 276.28/39.51 % (1120611)Time elapsed: 3.134 s % 276.28/39.51 % (1120611)Peak memory usage: 136 MB % 276.28/39.51 % (1120611)Instructions burned: 3605 (million) % 276.28/39.51 % (1120617)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1407763599:i=1876:sd=1:ss=included:sgt=32_2699 on theBenchmark for (2699ds/1876Mi) % 276.28/39.51 % (1120592)Instruction limit reached! % 276.28/39.51 % (1120592)------------------------------ % 276.28/39.51 % (1120592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.28/39.51 % (1120592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.28/39.51 % (1120592)CaDiCaL version: 2.1.3 % 276.28/39.51 % (1120592)Termination reason: Instruction limit % 276.28/39.51 % (1120592)Termination phase: Saturation % 276.28/39.51 % (1120592)Time elapsed: 7.168 s % 276.28/39.51 % (1120592)Peak memory usage: 182 MB % 276.28/39.51 % (1120592)Instructions burned: 7343 (million) % 276.28/39.51 % (1120551)Instruction limit reached! % 276.28/39.51 % (1120551)------------------------------ % 276.28/39.51 % (1120551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.28/39.51 % (1120551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.28/39.51 % (1120551)CaDiCaL version: 2.1.3 % 276.28/39.51 % (1120551)Termination reason: Instruction limit % 276.28/39.51 % (1120551)Termination phase: Saturation % 276.28/39.51 % (1120551)Time elapsed: 17.229 s % 276.28/39.51 % (1120551)Peak memory usage: 271 MB % 276.28/39.51 % (1120551)Instructions burned: 16412 (million) % 276.28/39.51 % (1120620)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3615746152:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2694 on theBenchmark for (2694ds/1932Mi) % 276.28/39.51 % (1120621)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=284137699:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2692 on theBenchmark for (2692ds/1980Mi) % 276.28/39.51 % (1120620)Refutation not found, incomplete strategy % 276.28/39.51 % (1120620)------------------------------ % 276.28/39.51 % (1120620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.28/39.51 % (1120620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.28/39.51 % (1120620)CaDiCaL version: 2.1.3 % 276.28/39.51 % (1120620)Termination reason: Refutation not found, incomplete strategy % 276.28/39.51 % (1120620)Time elapsed: 0.877 s % 276.28/39.51 % (1120620)Peak memory usage: 128 MB % 276.28/39.51 % (1120620)Instructions burned: 898 (million) % 276.28/39.51 % (1120620)------------------------------ % 276.28/39.51 % (1120620)------------------------------ % 276.28/39.51 % (1120617)Instruction limit reached! % 276.28/39.51 % (1120617)------------------------------ % 276.28/39.51 % (1120617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.28/39.51 % (1120617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.28/39.51 % (1120617)CaDiCaL version: 2.1.3 % 276.28/39.51 % (1120617)Termination reason: Instruction limit % 276.28/39.51 % (1120617)Termination phase: Saturation % 276.28/39.51 % (1120617)Time elapsed: 1.935 s % 301.35/43.05 % (1120617)Peak memory usage: 136 MB % 301.35/43.05 % (1120617)Instructions burned: 1877 (million) % 301.35/43.05 % (1120626)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=79157011:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2679 on theBenchmark for (2679ds/3902Mi) % 301.35/43.05 % (1120627)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=3129878220:avsq=on:i=3916:aac=none:amm=off_2678 on theBenchmark for (2678ds/3916Mi) % 301.35/43.05 % (1120621)Instruction limit reached! % 301.35/43.05 % (1120621)------------------------------ % 301.35/43.05 % (1120621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 301.35/43.05 % (1120621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/43.05 % (1120621)CaDiCaL version: 2.1.3 % 301.35/43.05 % (1120621)Termination reason: Instruction limit % 301.35/43.05 % (1120621)Termination phase: Saturation % 301.35/43.05 % (1120621)Time elapsed: 2.082 s % 301.35/43.05 % (1120621)Peak memory usage: 137 MB % 301.35/43.05 % (1120621)Instructions burned: 1980 (million) % 301.35/43.05 % (1120634)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3709413312:cond=on:i=3940:av=off:er=known_2669 on theBenchmark for (2669ds/3940Mi) % 301.35/43.05 % (1120609)Instruction limit reached! % 301.35/43.05 % (1120609)------------------------------ % 301.35/43.05 % (1120609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 301.35/43.05 % (1120609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/43.05 % (1120609)CaDiCaL version: 2.1.3 % 301.35/43.05 % (1120609)Termination reason: Instruction limit % 301.35/43.05 % (1120609)Termination phase: Saturation % 301.35/43.05 % (1120609)Time elapsed: 7.681 s % 301.35/43.05 % (1120609)Peak memory usage: 251 MB % 301.35/43.05 % (1120609)Instructions burned: 13942 (million) % 301.35/43.05 % (1120638)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=408935900:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2655 on theBenchmark for (2655ds/3980Mi) % 301.35/43.05 % (1120627)Instruction limit reached! % 301.35/43.05 % (1120627)------------------------------ % 301.35/43.05 % (1120627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 301.35/43.05 % (1120627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/43.05 % (1120627)CaDiCaL version: 2.1.3 % 301.35/43.05 % (1120627)Termination reason: Instruction limit % 301.35/43.05 % (1120627)Termination phase: Saturation % 301.35/43.05 % (1120627)Time elapsed: 3.093 s % 301.35/43.05 % (1120627)Peak memory usage: 119 MB % 301.35/43.05 % (1120627)Instructions burned: 3917 (million) % 301.35/43.05 % (1120626)Instruction limit reached! % 301.35/43.05 % (1120626)------------------------------ % 301.35/43.05 % (1120626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 301.35/43.05 % (1120626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/43.05 % (1120626)CaDiCaL version: 2.1.3 % 301.35/43.05 % (1120626)Termination reason: Instruction limit % 301.35/43.05 % (1120626)Termination phase: Saturation % 301.35/43.05 % (1120626)Time elapsed: 3.224 s % 301.35/43.05 % (1120626)Peak memory usage: 157 MB % 301.35/43.05 % (1120626)Instructions burned: 3902 (million) % 301.35/43.05 % (1120753)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=2165971483:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2644 on theBenchmark for (2644ds/2087Mi) % 301.35/43.05 % (1120777)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=3263862140:cts=off:cond=on:i=4272:bs=on:fsd=on_2644 on theBenchmark for (2644ds/4272Mi) % 301.35/43.05 % (1120638)Instruction limit reached! % 301.35/43.05 % (1120638)------------------------------ % 301.35/43.05 % (1120638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 301.35/43.05 % (1120638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 301.35/43.05 % (1120638)CaDiCaL version: 2.1.3 % 301.35/43.05 % (1120638)Termination reason: Instruction limit % 301.35/43.05 % (1120638)Termination phase: Saturation % 301.35/43.05 % (1120638)Time elapsed: 1.412 s % 301.35/43.05 % (1120638)Peak memory usage: 155 MB % 301.35/43.05 % (1120638)Instructions burned: 3981 (million) % 301.35/43.05 % (1120799)lrs-30_Terminated %------------------------------------------------------------------------------