%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW468-1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/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 01:30:23 PM UTC 2026 % Result : Timeout 300.69s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW468-1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.18 % Computer : n015.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 14:03:46 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.22 Running first-order theorem proving % 0.09/0.22 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 % 11.29/2.23 % (2641465)Input is clausal, will run a generic CNF schedule. % 11.29/2.23 % (2641472)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3044266831:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 11.29/2.23 % (2641475)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=941556711:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 11.29/2.23 % (2641471)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3565184723:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 11.29/2.23 % (2641470)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=1245541757:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 11.29/2.23 % (2641473)lrs+10_1_sil=8000:sp=occurrence:random_seed=3137865347:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 11.29/2.23 % (2641474)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3043465914:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 11.29/2.23 % (2641476)dis-21_1_sil=8000:lcm=predicate:random_seed=3454603677:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 11.29/2.23 % (2641476)Refutation not found, incomplete strategy % 11.29/2.23 % (2641476)------------------------------ % 11.29/2.23 % (2641476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.29/2.23 % (2641476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.29/2.23 % (2641476)CaDiCaL version: 2.1.3 % 11.29/2.23 % (2641476)Termination reason: Refutation not found, incomplete strategy % 11.29/2.23 % (2641476)Time elapsed: 0.001 s % 11.29/2.23 % (2641476)Peak memory usage: 88 MB % 11.29/2.23 % (2641476)Instructions burned: 1 (million) % 11.29/2.23 % (2641473)Instruction limit reached! % 11.29/2.23 % (2641473)------------------------------ % 11.29/2.23 % (2641473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.29/2.23 % (2641473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.29/2.23 % (2641473)CaDiCaL version: 2.1.3 % 11.29/2.23 % (2641473)Termination reason: Instruction limit % 11.29/2.23 % (2641473)Termination phase: Saturation % 11.29/2.23 % (2641473)Time elapsed: 0.062 s % 11.29/2.23 % (2641473)Peak memory usage: 88 MB % 11.29/2.23 % (2641473)Instructions burned: 107 (million) % 11.29/2.23 % (2641474)Instruction limit reached! % 11.29/2.23 % (2641474)------------------------------ % 11.29/2.23 % (2641474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.29/2.23 % (2641474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.29/2.23 % (2641474)CaDiCaL version: 2.1.3 % 11.29/2.23 % (2641474)Termination reason: Instruction limit % 11.29/2.23 % (2641474)Termination phase: Saturation % 11.29/2.23 % (2641474)Time elapsed: 0.066 s % 11.29/2.23 % (2641474)Peak memory usage: 89 MB % 11.29/2.23 % (2641474)Instructions burned: 115 (million) % 11.29/2.23 % (2641475)Instruction limit reached! % 11.29/2.23 % (2641475)------------------------------ % 11.29/2.23 % (2641475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.29/2.23 % (2641475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.29/2.23 % (2641475)CaDiCaL version: 2.1.3 % 11.29/2.23 % (2641475)Termination reason: Instruction limit % 11.29/2.23 % (2641475)Termination phase: Saturation % 11.29/2.23 % (2641475)Time elapsed: 0.104 s % 11.29/2.23 % (2641475)Peak memory usage: 89 MB % 11.29/2.23 % (2641475)Instructions burned: 182 (million) % 11.29/2.23 % (2641485)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1104615672:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi) % 11.29/2.23 % (2641484)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=1336645008:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 11.29/2.23 % (2641484)Refutation not found, incomplete strategy % 11.29/2.23 % (2641484)------------------------------ % 11.29/2.23 % (2641484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.29/2.23 % (2641484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.29/2.23 % (2641484)CaDiCaL version: 2.1.3 % 19.54/3.48 % (2641484)Termination reason: Refutation not found, incomplete strategy % 19.54/3.48 % (2641484)Time elapsed: 0.004 s % 19.54/3.48 % (2641484)Peak memory usage: 88 MB % 19.54/3.48 % (2641484)Instructions burned: 7 (million) % 19.54/3.48 % (2641485)Refutation not found, incomplete strategy % 19.54/3.48 % (2641485)------------------------------ % 19.54/3.48 % (2641485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.54/3.48 % (2641485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.54/3.48 % (2641485)CaDiCaL version: 2.1.3 % 19.54/3.48 % (2641485)Termination reason: Refutation not found, incomplete strategy % 19.54/3.48 % (2641485)Time elapsed: 0.005 s % 19.54/3.48 % (2641485)Peak memory usage: 88 MB % 19.54/3.48 % (2641485)Instructions burned: 8 (million) % 19.54/3.48 % (2641486)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2487961726:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 19.54/3.48 % (2641486)Refutation not found, incomplete strategy % 19.54/3.48 % (2641486)------------------------------ % 19.54/3.48 % (2641486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.54/3.48 % (2641486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.54/3.48 % (2641486)CaDiCaL version: 2.1.3 % 19.54/3.48 % (2641486)Termination reason: Refutation not found, incomplete strategy % 19.54/3.48 % (2641486)Time elapsed: 0.004 s % 19.54/3.48 % (2641486)Peak memory usage: 88 MB % 19.54/3.48 % (2641486)Instructions burned: 7 (million) % 19.54/3.48 % (2641476)------------------------------ % 19.54/3.48 % (2641476)------------------------------ % 19.54/3.48 % (2641490)lrs+10_64_to=lpo:sil=8000:random_seed=893853981:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 19.54/3.48 % (2641484)------------------------------ % 19.54/3.48 % (2641484)------------------------------ % 19.54/3.48 % (2641485)------------------------------ % 19.54/3.48 % (2641485)------------------------------ % 19.54/3.48 % (2641490)Instruction limit reached! % 19.54/3.48 % (2641490)------------------------------ % 19.54/3.48 % (2641490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.54/3.48 % (2641490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.54/3.48 % (2641490)CaDiCaL version: 2.1.3 % 19.54/3.48 % (2641490)Termination reason: Instruction limit % 19.54/3.48 % (2641490)Termination phase: Saturation % 19.54/3.48 % (2641490)Time elapsed: 0.072 s % 19.54/3.48 % (2641490)Peak memory usage: 89 MB % 19.54/3.48 % (2641490)Instructions burned: 128 (million) % 19.54/3.48 % (2641486)------------------------------ % 19.54/3.48 % (2641486)------------------------------ % 19.54/3.48 % (2641493)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2150812193:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 19.54/3.48 % (2641492)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=811389143:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi) % 19.54/3.48 % (2641495)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=3730172076:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 19.54/3.48 % (2641494)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1948056920:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi) % 19.54/3.48 % (2641495)Instruction limit reached! % 19.54/3.48 % (2641495)------------------------------ % 19.54/3.48 % (2641495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.54/3.48 % (2641495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.54/3.48 % (2641495)CaDiCaL version: 2.1.3 % 19.54/3.48 % (2641495)Termination reason: Instruction limit % 19.54/3.48 % (2641495)Termination phase: Saturation % 19.54/3.48 % (2641495)Time elapsed: 0.061 s % 19.54/3.48 % (2641495)Peak memory usage: 89 MB % 19.54/3.48 % (2641495)Instructions burned: 108 (million) % 19.54/3.48 % (2641493)Instruction limit reached! % 19.54/3.48 % (2641493)------------------------------ % 19.54/3.48 % (2641493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.54/3.48 % (2641493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.54/3.48 % (2641493)CaDiCaL version: 2.1.3 % 19.54/3.48 % (2641493)Termination reason: Instruction limit % 19.54/3.48 % (2641493)Termination phase: Saturation % 19.54/3.48 % (2641493)Time elapsed: 0.095 s % 19.54/3.48 % (2641493)Peak memory usage: 91 MB % 19.54/3.48 % (2641493)Instructions burned: 157 (million) % 31.43/5.07 % (2641492)Instruction limit reached! % 31.43/5.07 % (2641492)------------------------------ % 31.43/5.07 % (2641492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.43/5.07 % (2641492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.43/5.07 % (2641492)CaDiCaL version: 2.1.3 % 31.43/5.07 % (2641492)Termination reason: Instruction limit % 31.43/5.07 % (2641492)Termination phase: Saturation % 31.43/5.07 % (2641492)Time elapsed: 0.097 s % 31.43/5.07 % (2641492)Peak memory usage: 89 MB % 31.43/5.07 % (2641492)Instructions burned: 195 (million) % 31.43/5.07 % (2641500)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4240706195:i=107_2991 on theBenchmark for (2991ds/107Mi) % 31.43/5.07 % (2641500)Refutation not found, incomplete strategy % 31.43/5.07 % (2641500)------------------------------ % 31.43/5.07 % (2641500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.43/5.07 % (2641500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.43/5.07 % (2641500)CaDiCaL version: 2.1.3 % 31.43/5.07 % (2641500)Termination reason: Refutation not found, incomplete strategy % 31.43/5.07 % (2641500)Time elapsed: 0.004 s % 31.43/5.07 % (2641500)Peak memory usage: 87 MB % 31.43/5.07 % (2641500)Instructions burned: 7 (million) % 31.43/5.07 % (2641502)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3501518709:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi) % 31.43/5.07 % (2641501)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3912290190:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi) % 31.43/5.07 % (2641501)Instruction limit reached! % 31.43/5.07 % (2641501)------------------------------ % 31.43/5.07 % (2641501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.43/5.07 % (2641501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.43/5.07 % (2641501)CaDiCaL version: 2.1.3 % 31.43/5.07 % (2641501)Termination reason: Instruction limit % 31.43/5.07 % (2641501)Termination phase: Saturation % 31.43/5.07 % (2641501)Time elapsed: 0.147 s % 31.43/5.07 % (2641501)Peak memory usage: 91 MB % 31.43/5.07 % (2641501)Instructions burned: 242 (million) % 31.43/5.07 % (2641500)------------------------------ % 31.43/5.07 % (2641500)------------------------------ % 31.43/5.07 % (2641506)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2514788435:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi) % 31.43/5.07 % (2641506)Instruction limit reached! % 31.43/5.07 % (2641506)------------------------------ % 31.43/5.07 % (2641506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.43/5.07 % (2641506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.43/5.07 % (2641506)CaDiCaL version: 2.1.3 % 31.43/5.07 % (2641506)Termination reason: Instruction limit % 31.43/5.07 % (2641506)Termination phase: Saturation % 31.43/5.07 % (2641506)Time elapsed: 0.071 s % 31.43/5.07 % (2641506)Peak memory usage: 89 MB % 31.43/5.07 % (2641506)Instructions burned: 134 (million) % 31.43/5.07 % (2641507)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2730436652:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi) % 31.43/5.07 % (2641510)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=118429974:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi) % 31.43/5.07 % (2641510)Instruction limit reached! % 31.43/5.07 % (2641510)------------------------------ % 31.43/5.07 % (2641510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.43/5.07 % (2641510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.43/5.07 % (2641510)CaDiCaL version: 2.1.3 % 31.43/5.07 % (2641510)Termination reason: Instruction limit % 31.43/5.07 % (2641510)Termination phase: Saturation % 31.43/5.07 % (2641510)Time elapsed: 0.119 s % 31.43/5.07 % (2641510)Peak memory usage: 90 MB % 31.43/5.07 % (2641510)Instructions burned: 191 (million) % 31.43/5.07 % (2641507)Instruction limit reached! % 31.43/5.07 % (2641507)------------------------------ % 31.43/5.07 % (2641507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.43/5.07 % (2641507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.43/5.07 % (2641507)CaDiCaL version: 2.1.3 % 31.43/5.07 % (2641507)Termination reason: Instruction limit % 49.97/7.77 % (2641507)Termination phase: Saturation % 49.97/7.77 % (2641507)Time elapsed: 0.269 s % 49.97/7.77 % (2641507)Peak memory usage: 90 MB % 49.97/7.77 % (2641507)Instructions burned: 500 (million) % 49.97/7.77 % (2641512)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1895695257:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi) % 49.97/7.77 % (2641513)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4203867167:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi) % 49.97/7.77 % (2641513)Instruction limit reached! % 49.97/7.77 % (2641513)------------------------------ % 49.97/7.77 % (2641513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.97/7.77 % (2641513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.97/7.77 % (2641513)CaDiCaL version: 2.1.3 % 49.97/7.77 % (2641513)Termination reason: Instruction limit % 49.97/7.77 % (2641513)Termination phase: Saturation % 49.97/7.77 % (2641513)Time elapsed: 0.077 s % 49.97/7.77 % (2641513)Peak memory usage: 88 MB % 49.97/7.77 % (2641513)Instructions burned: 157 (million) % 49.97/7.77 % (2641512)Instruction limit reached! % 49.97/7.77 % (2641512)------------------------------ % 49.97/7.77 % (2641512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.97/7.77 % (2641512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.97/7.77 % (2641512)CaDiCaL version: 2.1.3 % 49.97/7.77 % (2641512)Termination reason: Instruction limit % 49.97/7.77 % (2641512)Termination phase: Saturation % 49.97/7.77 % (2641512)Time elapsed: 0.142 s % 49.97/7.77 % (2641512)Peak memory usage: 90 MB % 49.97/7.77 % (2641512)Instructions burned: 266 (million) % 49.97/7.77 % (2641516)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=2474210714:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi) % 49.97/7.77 % (2641517)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3598334277:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi) % 49.97/7.77 % (2641517)Instruction limit reached! % 49.97/7.77 % (2641517)------------------------------ % 49.97/7.77 % (2641517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.97/7.77 % (2641517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.97/7.77 % (2641517)CaDiCaL version: 2.1.3 % 49.97/7.77 % (2641517)Termination reason: Instruction limit % 49.97/7.77 % (2641517)Termination phase: Saturation % 49.97/7.77 % (2641517)Time elapsed: 0.303 s % 49.97/7.77 % (2641517)Peak memory usage: 91 MB % 49.97/7.77 % (2641517)Instructions burned: 537 (million) % 49.97/7.77 % (2641520)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2546962706:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi) % 49.97/7.77 % (2641520)Instruction limit reached! % 49.97/7.77 % (2641520)------------------------------ % 49.97/7.77 % (2641520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.97/7.77 % (2641520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.97/7.77 % (2641520)CaDiCaL version: 2.1.3 % 49.97/7.77 % (2641520)Termination reason: Instruction limit % 49.97/7.77 % (2641520)Termination phase: Saturation % 49.97/7.77 % (2641520)Time elapsed: 0.099 s % 49.97/7.77 % (2641520)Peak memory usage: 89 MB % 49.97/7.77 % (2641520)Instructions burned: 182 (million) % 49.97/7.77 % (2641522)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=1168863457:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi) % 49.97/7.77 % (2641494)Instruction limit reached! % 49.97/7.77 % (2641494)------------------------------ % 49.97/7.77 % (2641494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 49.97/7.77 % (2641494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 49.97/7.77 % (2641494)CaDiCaL version: 2.1.3 % 49.97/7.77 % (2641494)Termination reason: Instruction limit % 49.97/7.77 % (2641494)Termination phase: Saturation % 49.97/7.77 % (2641494)Time elapsed: 1.951 s % 49.97/7.77 % (2641494)Peak memory usage: 144 MB % 49.97/7.77 % (2641494)Instructions burned: 3394 (million) % 49.97/7.77 % (2641524)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=4137006243:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi) % 72.73/10.97 % (2641524)Instruction limit reached! % 72.73/10.97 % (2641524)------------------------------ % 72.73/10.97 % (2641524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.73/10.97 % (2641524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.97 % (2641524)CaDiCaL version: 2.1.3 % 72.73/10.97 % (2641524)Termination reason: Instruction limit % 72.73/10.97 % (2641524)Termination phase: Saturation % 72.73/10.97 % (2641524)Time elapsed: 0.234 s % 72.73/10.97 % (2641524)Peak memory usage: 94 MB % 72.73/10.97 % (2641524)Instructions burned: 412 (million) % 72.73/10.97 % (2641526)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=1248097103:s2pl=no:i=8478:s2at=4:nm=6_2969 on theBenchmark for (2969ds/8478Mi) % 72.73/10.97 % (2641502)Instruction limit reached! % 72.73/10.97 % (2641502)------------------------------ % 72.73/10.97 % (2641502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.73/10.97 % (2641502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.97 % (2641502)CaDiCaL version: 2.1.3 % 72.73/10.97 % (2641502)Termination reason: Instruction limit % 72.73/10.97 % (2641502)Termination phase: Saturation % 72.73/10.97 % (2641502)Time elapsed: 2.650 s % 72.73/10.97 % (2641502)Peak memory usage: 147 MB % 72.73/10.97 % (2641502)Instructions burned: 5209 (million) % 72.73/10.97 % (2641516)Instruction limit reached! % 72.73/10.97 % (2641516)------------------------------ % 72.73/10.97 % (2641516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.73/10.97 % (2641516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.97 % (2641516)CaDiCaL version: 2.1.3 % 72.73/10.97 % (2641516)Termination reason: Instruction limit % 72.73/10.97 % (2641516)Termination phase: Saturation % 72.73/10.97 % (2641516)Time elapsed: 1.789 s % 72.73/10.97 % (2641516)Peak memory usage: 141 MB % 72.73/10.97 % (2641516)Instructions burned: 3257 (million) % 72.73/10.97 % (2641528)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=4261996388:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2964 on theBenchmark for (2964ds/303Mi) % 72.73/10.97 % (2641528)Refutation not found, incomplete strategy % 72.73/10.97 % (2641528)------------------------------ % 72.73/10.97 % (2641528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.73/10.97 % (2641528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.97 % (2641528)CaDiCaL version: 2.1.3 % 72.73/10.97 % (2641528)Termination reason: Refutation not found, incomplete strategy % 72.73/10.97 % (2641528)Time elapsed: 0.002 s % 72.73/10.97 % (2641528)Peak memory usage: 88 MB % 72.73/10.97 % (2641528)Instructions burned: 1 (million) % 72.73/10.97 % (2641529)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=589636981:st=4:i=720:sd=3:fsr=off:ss=axioms_2962 on theBenchmark for (2962ds/720Mi) % 72.73/10.97 % (2641529)Refutation not found, incomplete strategy % 72.73/10.97 % (2641529)------------------------------ % 72.73/10.97 % (2641529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.73/10.97 % (2641529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.73/10.97 % (2641529)CaDiCaL version: 2.1.3 % 72.73/10.97 % (2641529)Termination reason: Refutation not found, incomplete strategy % 72.73/10.97 % (2641529)Time elapsed: 0.004 s % 72.73/10.97 % (2641529)Peak memory usage: 88 MB % 72.73/10.97 % (2641529)Instructions burned: 7 (million) % 72.73/10.97 % (2641528)------------------------------ % 72.73/10.97 % (2641528)------------------------------ % 72.73/10.97 % (2641529)------------------------------ % 72.73/10.97 % (2641529)------------------------------ % 72.73/10.97 % (2641532)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=303616831:i=598:bs=on:bd=preordered:av=off:ss=axioms_2960 on theBenchmark for (2960ds/598Mi) % 72.73/10.97 % (2641533)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4220639543:i=2989:sd=3:ss=axioms:sgt=60_2958 on theBenchmark for (2958ds/2989Mi) % 72.73/10.97 % (2641532)Instruction limit reached! % 72.73/10.97 % (2641532)------------------------------ % 72.73/10.97 % (2641532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.73/10.97 % (2641532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.21/15.32 % (2641532)CaDiCaL version: 2.1.3 % 104.21/15.32 % (2641532)Termination reason: Instruction limit % 104.21/15.32 % (2641532)Termination phase: Saturation % 104.21/15.32 % (2641532)Time elapsed: 0.294 s % 104.21/15.32 % (2641532)Peak memory usage: 93 MB % 104.21/15.32 % (2641532)Instructions burned: 598 (million) % 104.21/15.32 % (2641536)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=974689976:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2955 on theBenchmark for (2955ds/1997Mi) % 104.21/15.32 % (2641536)Instruction limit reached! % 104.21/15.32 % (2641536)------------------------------ % 104.21/15.32 % (2641536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.21/15.32 % (2641536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.21/15.32 % (2641536)CaDiCaL version: 2.1.3 % 104.21/15.32 % (2641536)Termination reason: Instruction limit % 104.21/15.32 % (2641536)Termination phase: Saturation % 104.21/15.32 % (2641536)Time elapsed: 1.209 s % 104.21/15.32 % (2641536)Peak memory usage: 139 MB % 104.21/15.32 % (2641536)Instructions burned: 1997 (million) % 104.21/15.32 % (2641538)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=915124419:i=2088:bd=preordered:av=off_2942 on theBenchmark for (2942ds/2088Mi) % 104.21/15.32 % (2641533)Instruction limit reached! % 104.21/15.32 % (2641533)------------------------------ % 104.21/15.32 % (2641533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.21/15.32 % (2641533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.21/15.32 % (2641533)CaDiCaL version: 2.1.3 % 104.21/15.32 % (2641533)Termination reason: Instruction limit % 104.21/15.32 % (2641533)Termination phase: Saturation % 104.21/15.32 % (2641533)Time elapsed: 1.746 s % 104.21/15.32 % (2641533)Peak memory usage: 146 MB % 104.21/15.32 % (2641533)Instructions burned: 2991 (million) % 104.21/15.32 % (2641540)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1837343922:i=1098:nicw=on_2940 on theBenchmark for (2940ds/1098Mi) % 104.21/15.32 % (2641540)Instruction limit reached! % 104.21/15.32 % (2641540)------------------------------ % 104.21/15.32 % (2641540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.21/15.32 % (2641540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.21/15.32 % (2641540)CaDiCaL version: 2.1.3 % 104.21/15.32 % (2641540)Termination reason: Instruction limit % 104.21/15.32 % (2641540)Termination phase: Saturation % 104.21/15.32 % (2641540)Time elapsed: 0.559 s % 104.21/15.32 % (2641540)Peak memory usage: 93 MB % 104.21/15.32 % (2641540)Instructions burned: 1099 (million) % 104.21/15.32 % (2641542)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2984295649:i=433:bd=preordered_2933 on theBenchmark for (2933ds/433Mi) % 104.21/15.32 % (2641542)Refutation not found, incomplete strategy % 104.21/15.32 % (2641542)------------------------------ % 104.21/15.32 % (2641542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.21/15.32 % (2641542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.21/15.32 % (2641542)CaDiCaL version: 2.1.3 % 104.21/15.32 % (2641542)Termination reason: Refutation not found, incomplete strategy % 104.21/15.32 % (2641542)Time elapsed: 0.006 s % 104.21/15.32 % (2641542)Peak memory usage: 88 MB % 104.21/15.32 % (2641542)Instructions burned: 11 (million) % 104.21/15.32 % (2641542)------------------------------ % 104.21/15.32 % (2641542)------------------------------ % 104.21/15.32 % (2641526)Instruction limit reached! % 104.21/15.32 % (2641526)------------------------------ % 104.21/15.32 % (2641526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.21/15.32 % (2641526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.21/15.32 % (2641526)CaDiCaL version: 2.1.3 % 104.21/15.32 % (2641526)Termination reason: Instruction limit % 104.21/15.32 % (2641526)Termination phase: Saturation % 104.21/15.32 % (2641526)Time elapsed: 3.895 s % 104.21/15.32 % (2641526)Peak memory usage: 148 MB % 104.21/15.32 % (2641526)Instructions burned: 8480 (million) % 104.21/15.32 % (2641538)Instruction limit reached! % 104.21/15.32 % (2641538)------------------------------ % 104.21/15.32 % (2641538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.21/15.32 % (2641538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.21/15.32 % (2641538)CaDiCaL version: 2.1.3 % 104.21/15.32 % (2641538)Termination reason: Instruction limit % 129.67/19.00 % (2641538)Termination phase: Saturation % 129.67/19.00 % (2641538)Time elapsed: 1.210 s % 129.67/19.00 % (2641538)Peak memory usage: 139 MB % 129.67/19.00 % (2641538)Instructions burned: 2089 (million) % 129.67/19.00 % (2641544)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4079720051:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2929 on theBenchmark for (2929ds/2942Mi) % 129.67/19.00 % (2641545)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2490060899:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2929 on theBenchmark for (2929ds/6922Mi) % 129.67/19.00 % (2641546)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=95330480:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2928 on theBenchmark for (2928ds/596Mi) % 129.67/19.00 % (2641546)Refutation not found, incomplete strategy % 129.67/19.00 % (2641546)------------------------------ % 129.67/19.00 % (2641546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 129.67/19.00 % (2641546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.67/19.00 % (2641546)CaDiCaL version: 2.1.3 % 129.67/19.00 % (2641546)Termination reason: Refutation not found, incomplete strategy % 129.67/19.00 % (2641546)Time elapsed: 0.003 s % 129.67/19.00 % (2641546)Peak memory usage: 88 MB % 129.67/19.00 % (2641546)Instructions burned: 4 (million) % 129.67/19.00 % (2641546)------------------------------ % 129.67/19.00 % (2641546)------------------------------ % 129.67/19.00 % (2641550)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=3019937256:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2925 on theBenchmark for (2925ds/4123Mi) % 129.67/19.00 % (2641522)Instruction limit reached! % 129.67/19.00 % (2641522)------------------------------ % 129.67/19.00 % (2641522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 129.67/19.00 % (2641522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.67/19.00 % (2641522)CaDiCaL version: 2.1.3 % 129.67/19.00 % (2641522)Termination reason: Instruction limit % 129.67/19.00 % (2641522)Termination phase: Saturation % 129.67/19.00 % (2641522)Time elapsed: 6.017 s % 129.67/19.00 % (2641522)Peak memory usage: 172 MB % 129.67/19.00 % (2641522)Instructions burned: 10308 (million) % 129.67/19.00 % (2641552)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1344056751:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2913 on theBenchmark for (2913ds/16411Mi) % 129.67/19.00 % (2641544)Instruction limit reached! % 129.67/19.00 % (2641544)------------------------------ % 129.67/19.00 % (2641544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 129.67/19.00 % (2641544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.67/19.00 % (2641544)CaDiCaL version: 2.1.3 % 129.67/19.00 % (2641544)Termination reason: Instruction limit % 129.67/19.00 % (2641544)Termination phase: Saturation % 129.67/19.00 % (2641544)Time elapsed: 1.918 s % 129.67/19.00 % (2641544)Peak memory usage: 142 MB % 129.67/19.00 % (2641544)Instructions burned: 2942 (million) % 129.67/19.00 % (2641554)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3464933592:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2908 on theBenchmark for (2908ds/1670Mi) % 129.67/19.00 % (2641550)Instruction limit reached! % 129.67/19.00 % (2641550)------------------------------ % 129.67/19.00 % (2641550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 129.67/19.00 % (2641550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.67/19.00 % (2641550)CaDiCaL version: 2.1.3 % 129.67/19.00 % (2641550)Termination reason: Instruction limit % 129.67/19.00 % (2641550)Termination phase: Saturation % 129.67/19.00 % (2641550)Time elapsed: 2.309 s % 129.67/19.00 % (2641550)Peak memory usage: 160 MB % 129.67/19.00 % (2641550)Instructions burned: 4125 (million) % 129.67/19.00 % (2641556)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=3464888198:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2900 on theBenchmark for (2900ds/1722Mi) % 129.67/19.00 % (2641554)Instruction limit reached! % 129.67/19.00 % (2641554)------------------------------ % 129.67/19.00 % (2641554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.99/22.11 % (2641554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.99/22.11 % (2641554)CaDiCaL version: 2.1.3 % 151.99/22.11 % (2641554)Termination reason: Instruction limit % 151.99/22.11 % (2641554)Termination phase: Saturation % 151.99/22.11 % (2641554)Time elapsed: 1.074 s % 151.99/22.11 % (2641554)Peak memory usage: 135 MB % 151.99/22.11 % (2641554)Instructions burned: 1670 (million) % 151.99/22.11 % (2641558)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=3847548604:cts=off:cond=on:i=9530:bs=on:fsd=on_2896 on theBenchmark for (2896ds/9530Mi) % 151.99/22.11 % (2641545)Instruction limit reached! % 151.99/22.11 % (2641545)------------------------------ % 151.99/22.11 % (2641545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.99/22.11 % (2641545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.99/22.11 % (2641545)CaDiCaL version: 2.1.3 % 151.99/22.11 % (2641545)Termination reason: Instruction limit % 151.99/22.11 % (2641545)Termination phase: Saturation % 151.99/22.11 % (2641545)Time elapsed: 3.384 s % 151.99/22.11 % (2641545)Peak memory usage: 135 MB % 151.99/22.11 % (2641545)Instructions burned: 6922 (million) % 151.99/22.11 % (2641560)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3950683008:st=2:i=4495:sd=10:ss=included_2893 on theBenchmark for (2893ds/4495Mi) % 151.99/22.11 % (2641556)Instruction limit reached! % 151.99/22.11 % (2641556)------------------------------ % 151.99/22.11 % (2641556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.99/22.11 % (2641556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.99/22.11 % (2641556)CaDiCaL version: 2.1.3 % 151.99/22.11 % (2641556)Termination reason: Instruction limit % 151.99/22.11 % (2641556)Termination phase: Saturation % 151.99/22.11 % (2641556)Time elapsed: 1.040 s % 151.99/22.11 % (2641556)Peak memory usage: 134 MB % 151.99/22.11 % (2641556)Instructions burned: 1723 (million) % 151.99/22.11 % (2641562)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=898079111:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2888 on theBenchmark for (2888ds/4920Mi) % 151.99/22.11 % (2641560)Instruction limit reached! % 151.99/22.11 % (2641560)------------------------------ % 151.99/22.11 % (2641560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.99/22.11 % (2641560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.99/22.11 % (2641560)CaDiCaL version: 2.1.3 % 151.99/22.11 % (2641560)Termination reason: Instruction limit % 151.99/22.11 % (2641560)Termination phase: Saturation % 151.99/22.11 % (2641560)Time elapsed: 2.459 s % 151.99/22.11 % (2641560)Peak memory usage: 149 MB % 151.99/22.11 % (2641560)Instructions burned: 4497 (million) % 151.99/22.11 % (2641564)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=2044508919:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2868 on theBenchmark for (2868ds/2083Mi) % 151.99/22.11 % (2641562)Instruction limit reached! % 151.99/22.11 % (2641562)------------------------------ % 151.99/22.11 % (2641562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.99/22.11 % (2641562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.99/22.11 % (2641562)CaDiCaL version: 2.1.3 % 151.99/22.11 % (2641562)Termination reason: Instruction limit % 151.99/22.11 % (2641562)Termination phase: Saturation % 151.99/22.11 % (2641562)Time elapsed: 2.883 s % 151.99/22.11 % (2641562)Peak memory usage: 160 MB % 151.99/22.11 % (2641562)Instructions burned: 4921 (million) % 151.99/22.11 % (2641566)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=2190206935:i=4629:av=off:gsp=on_2858 on theBenchmark for (2858ds/4629Mi) % 151.99/22.11 % (2641564)Instruction limit reached! % 151.99/22.11 % (2641564)------------------------------ % 151.99/22.11 % (2641564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.99/22.11 % (2641564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.99/22.11 % (2641564)CaDiCaL version: 2.1.3 % 151.99/22.11 % (2641564)Termination reason: Instruction limit % 151.99/22.11 % (2641564)Termination phase: Saturation % 151.99/22.11 % (2641564)Time elapsed: 1.325 s % 151.99/22.11 % (2641564)Peak memory usage: 136 MB % 176.93/25.62 % (2641564)Instructions burned: 2083 (million) % 176.93/25.62 % (2641569)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=4064894979:i=1258:av=off_2853 on theBenchmark for (2853ds/1258Mi) % 176.93/25.62 % (2641569)Instruction limit reached! % 176.93/25.62 % (2641569)------------------------------ % 176.93/25.62 % (2641569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.93/25.62 % (2641569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.62 % (2641569)CaDiCaL version: 2.1.3 % 176.93/25.62 % (2641569)Termination reason: Instruction limit % 176.93/25.62 % (2641569)Termination phase: Saturation % 176.93/25.62 % (2641569)Time elapsed: 0.688 s % 176.93/25.62 % (2641569)Peak memory usage: 97 MB % 176.93/25.62 % (2641569)Instructions burned: 1258 (million) % 176.93/25.62 % (2641571)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2513927523:i=7343:av=off:ss=included_2845 on theBenchmark for (2845ds/7343Mi) % 176.93/25.62 % (2641558)Instruction limit reached! % 176.93/25.62 % (2641558)------------------------------ % 176.93/25.62 % (2641558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.93/25.62 % (2641558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.62 % (2641558)CaDiCaL version: 2.1.3 % 176.93/25.62 % (2641558)Termination reason: Instruction limit % 176.93/25.62 % (2641558)Termination phase: Saturation % 176.93/25.62 % (2641558)Time elapsed: 5.743 s % 176.93/25.62 % (2641558)Peak memory usage: 199 MB % 176.93/25.62 % (2641558)Instructions burned: 9530 (million) % 176.93/25.62 % (2641573)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=326752489:i=1325:sd=2:ss=axioms:sgt=16_2837 on theBenchmark for (2837ds/1325Mi) % 176.93/25.62 % (2641573)Refutation not found, incomplete strategy % 176.93/25.62 % (2641573)------------------------------ % 176.93/25.62 % (2641573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.93/25.62 % (2641573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.62 % (2641573)CaDiCaL version: 2.1.3 % 176.93/25.62 % (2641573)Termination reason: Refutation not found, incomplete strategy % 176.93/25.62 % (2641573)Time elapsed: 0.004 s % 176.93/25.62 % (2641573)Peak memory usage: 88 MB % 176.93/25.62 % (2641573)Instructions burned: 5 (million) % 176.93/25.62 % (2641573)------------------------------ % 176.93/25.62 % (2641573)------------------------------ % 176.93/25.62 % (2641575)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=1210778551:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2834 on theBenchmark for (2834ds/2646Mi) % 176.93/25.62 % (2641566)Instruction limit reached! % 176.93/25.62 % (2641566)------------------------------ % 176.93/25.62 % (2641566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.93/25.62 % (2641566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.62 % (2641566)CaDiCaL version: 2.1.3 % 176.93/25.62 % (2641566)Termination reason: Instruction limit % 176.93/25.62 % (2641566)Termination phase: Saturation % 176.93/25.62 % (2641566)Time elapsed: 2.844 s % 176.93/25.62 % (2641566)Peak memory usage: 150 MB % 176.93/25.62 % (2641566)Instructions burned: 4629 (million) % 176.93/25.62 % (2641577)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1053319419:i=1489:sd=2:ep=R:ss=axioms_2828 on theBenchmark for (2828ds/1489Mi) % 176.93/25.62 % (2641577)Refutation not found, incomplete strategy % 176.93/25.62 % (2641577)------------------------------ % 176.93/25.62 % (2641577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.93/25.62 % (2641577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.93/25.62 % (2641577)CaDiCaL version: 2.1.3 % 176.93/25.62 % (2641577)Termination reason: Refutation not found, incomplete strategy % 176.93/25.62 % (2641577)Time elapsed: 0.591 s % 176.93/25.62 % (2641577)Peak memory usage: 128 MB % 176.93/25.62 % (2641577)Instructions burned: 897 (million) % 176.93/25.62 % (2641577)------------------------------ % 176.93/25.62 % (2641577)------------------------------ % 176.93/25.62 % (2641579)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=2601076636:i=1503_2818 on theBenchmark for (2818ds/1503Mi) % 176.93/25.62 % (2641575)Instruction limit reached! % 176.93/25.62 % (2641575)------------------------------ % 176.93/25.62 % (2641575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.42 % (2641575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.42 % (2641575)CaDiCaL version: 2.1.3 % 197.03/28.42 % (2641575)Termination reason: Instruction limit % 197.03/28.42 % (2641575)Termination phase: Saturation % 197.03/28.42 % (2641575)Time elapsed: 1.624 s % 197.03/28.42 % (2641575)Peak memory usage: 142 MB % 197.03/28.42 % (2641575)Instructions burned: 2647 (million) % 197.03/28.42 % (2641581)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2503307707:i=13942:kws=frequency_2816 on theBenchmark for (2816ds/13942Mi) % 197.03/28.42 % (2641579)Refutation not found, incomplete strategy % 197.03/28.42 % (2641579)------------------------------ % 197.03/28.42 % (2641579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.42 % (2641579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.42 % (2641579)CaDiCaL version: 2.1.3 % 197.03/28.42 % (2641579)Termination reason: Refutation not found, incomplete strategy % 197.03/28.42 % (2641579)Time elapsed: 0.588 s % 197.03/28.42 % (2641579)Peak memory usage: 128 MB % 197.03/28.42 % (2641579)Instructions burned: 896 (million) % 197.03/28.42 % (2641579)------------------------------ % 197.03/28.42 % (2641579)------------------------------ % 197.03/28.42 % (2641583)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=3587699872:i=3604:fsr=off:er=filter_2809 on theBenchmark for (2809ds/3604Mi) % 197.03/28.42 % (2641571)Instruction limit reached! % 197.03/28.42 % (2641571)------------------------------ % 197.03/28.42 % (2641571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.42 % (2641571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.42 % (2641571)CaDiCaL version: 2.1.3 % 197.03/28.42 % (2641571)Termination reason: Instruction limit % 197.03/28.42 % (2641571)Termination phase: Saturation % 197.03/28.42 % (2641571)Time elapsed: 3.703 s % 197.03/28.42 % (2641571)Peak memory usage: 161 MB % 197.03/28.42 % (2641571)Instructions burned: 7344 (million) % 197.03/28.42 % (2641586)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=388269196:i=1876:sd=1:ss=included:sgt=32_2806 on theBenchmark for (2806ds/1876Mi) % 197.03/28.42 % (2641586)Instruction limit reached! % 197.03/28.42 % (2641586)------------------------------ % 197.03/28.42 % (2641586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.42 % (2641586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.42 % (2641586)CaDiCaL version: 2.1.3 % 197.03/28.42 % (2641586)Termination reason: Instruction limit % 197.03/28.42 % (2641586)Termination phase: Saturation % 197.03/28.42 % (2641586)Time elapsed: 1.139 s % 197.03/28.42 % (2641586)Peak memory usage: 135 MB % 197.03/28.42 % (2641586)Instructions burned: 1876 (million) % 197.03/28.42 % (2641588)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2723660606:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2794 on theBenchmark for (2794ds/1932Mi) % 197.03/28.42 % (2641583)Instruction limit reached! % 197.03/28.42 % (2641583)------------------------------ % 197.03/28.42 % (2641583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.42 % (2641583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.42 % (2641583)CaDiCaL version: 2.1.3 % 197.03/28.42 % (2641583)Termination reason: Instruction limit % 197.03/28.42 % (2641583)Termination phase: Saturation % 197.03/28.42 % (2641583)Time elapsed: 2.076 s % 197.03/28.42 % (2641583)Peak memory usage: 145 MB % 197.03/28.42 % (2641583)Instructions burned: 3605 (million) % 197.03/28.42 % (2641588)Refutation not found, incomplete strategy % 197.03/28.42 % (2641588)------------------------------ % 197.03/28.42 % (2641588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.42 % (2641588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.42 % (2641588)CaDiCaL version: 2.1.3 % 197.03/28.42 % (2641588)Termination reason: Refutation not found, incomplete strategy % 197.03/28.42 % (2641588)Time elapsed: 0.592 s % 197.03/28.42 % (2641588)Peak memory usage: 128 MB % 197.03/28.42 % (2641588)Instructions burned: 898 (million) % 197.03/28.42 % (2641590)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=3140469591:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2786 on theBenchmark for (2786ds/1980Mi) % 218.34/31.54 % (2641588)------------------------------ % 218.34/31.54 % (2641588)------------------------------ % 218.34/31.54 % (2641592)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=2987777768:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2784 on theBenchmark for (2784ds/3902Mi) % 218.34/31.54 % (2641552)Instruction limit reached! % 218.34/31.54 % (2641552)------------------------------ % 218.34/31.54 % (2641552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.54 % (2641552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.54 % (2641552)CaDiCaL version: 2.1.3 % 218.34/31.54 % (2641552)Termination reason: Instruction limit % 218.34/31.54 % (2641552)Termination phase: Saturation % 218.34/31.54 % (2641552)Time elapsed: 13.469 s % 218.34/31.54 % (2641552)Peak memory usage: 169 MB % 218.34/31.54 % (2641552)Instructions burned: 16412 (million) % 218.34/31.54 % (2641592)Refutation not found, incomplete strategy % 218.34/31.54 % (2641592)------------------------------ % 218.34/31.54 % (2641592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.54 % (2641592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.54 % (2641592)CaDiCaL version: 2.1.3 % 218.34/31.54 % (2641592)Termination reason: Refutation not found, incomplete strategy % 218.34/31.54 % (2641592)Time elapsed: 0.594 s % 218.34/31.54 % (2641592)Peak memory usage: 128 MB % 218.34/31.54 % (2641592)Instructions burned: 905 (million) % 218.34/31.54 % (2641594)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1785504032:avsq=on:i=3916:aac=none:amm=off_2777 on theBenchmark for (2777ds/3916Mi) % 218.34/31.54 % (2641592)------------------------------ % 218.34/31.54 % (2641592)------------------------------ % 218.34/31.54 % (2641590)Instruction limit reached! % 218.34/31.54 % (2641590)------------------------------ % 218.34/31.54 % (2641590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.54 % (2641590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.54 % (2641590)CaDiCaL version: 2.1.3 % 218.34/31.54 % (2641590)Termination reason: Instruction limit % 218.34/31.54 % (2641590)Termination phase: Saturation % 218.34/31.54 % (2641590)Time elapsed: 1.192 s % 218.34/31.54 % (2641590)Peak memory usage: 140 MB % 218.34/31.54 % (2641590)Instructions burned: 1981 (million) % 218.34/31.54 % (2641596)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3964459925:cond=on:i=3940:av=off:er=known_2774 on theBenchmark for (2774ds/3940Mi) % 218.34/31.54 % (2641597)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1197201359:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2773 on theBenchmark for (2773ds/3980Mi) % 218.34/31.54 % (2641594)Instruction limit reached! % 218.34/31.54 % (2641594)------------------------------ % 218.34/31.54 % (2641594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.54 % (2641594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.54 % (2641594)CaDiCaL version: 2.1.3 % 218.34/31.54 % (2641594)Termination reason: Instruction limit % 218.34/31.54 % (2641594)Termination phase: Saturation % 218.34/31.54 % (2641594)Time elapsed: 2.258 s % 218.34/31.54 % (2641594)Peak memory usage: 130 MB % 218.34/31.54 % (2641594)Instructions burned: 3918 (million) % 218.34/31.54 % (2641600)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=264680143:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2753 on theBenchmark for (2753ds/2087Mi) % 218.34/31.54 % (2641596)Instruction limit reached! % 218.34/31.54 % (2641596)------------------------------ % 218.34/31.54 % (2641596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.34/31.54 % (2641596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.34/31.54 % (2641596)CaDiCaL version: 2.1.3 % 218.34/31.54 % (2641596)Termination reason: Instruction limit % 218.34/31.54 % (2641596)Termination phase: Saturation % 218.34/31.54 % (2641596)Time elapsed: 2.132 s % 218.34/31.54 % (2641596)Peak memory usage: 153 MB % 218.34/31.54 % (2641596)Instructions burned: 3940 (million) % 218.34/31.54 % (2641602)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=3538090907:cts=off:cond=on:i=4272:bs=on:fsd=on_2751 on theBenchmark for (2751ds/4272Mi) % 276.29/39.69 % (2641597)Instruction limit reached! % 276.29/39.69 % (2641597)------------------------------ % 276.29/39.69 % (2641597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.69 % (2641597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.69 % (2641597)CaDiCaL version: 2.1.3 % 276.29/39.69 % (2641597)Termination reason: Instruction limit % 276.29/39.69 % (2641597)Termination phase: Saturation % 276.29/39.69 % (2641597)Time elapsed: 2.579 s % 276.29/39.69 % (2641597)Peak memory usage: 153 MB % 276.29/39.69 % (2641597)Instructions burned: 3981 (million) % 276.29/39.69 % (2641604)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2024502603:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2746 on theBenchmark for (2746ds/2197Mi) % 276.29/39.69 % (2641581)Instruction limit reached! % 276.29/39.69 % (2641581)------------------------------ % 276.29/39.69 % (2641581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.69 % (2641581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.69 % (2641581)CaDiCaL version: 2.1.3 % 276.29/39.69 % (2641581)Termination reason: Instruction limit % 276.29/39.69 % (2641581)Termination phase: Saturation % 276.29/39.69 % (2641581)Time elapsed: 7.316 s % 276.29/39.69 % (2641581)Peak memory usage: 181 MB % 276.29/39.69 % (2641581)Instructions burned: 13943 (million) % 276.29/39.69 % (2641606)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2042275306:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2741 on theBenchmark for (2741ds/6508Mi) % 276.29/39.69 % (2641600)Instruction limit reached! % 276.29/39.69 % (2641600)------------------------------ % 276.29/39.69 % (2641600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.69 % (2641600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.69 % (2641600)CaDiCaL version: 2.1.3 % 276.29/39.69 % (2641600)Termination reason: Instruction limit % 276.29/39.69 % (2641600)Termination phase: Saturation % 276.29/39.69 % (2641600)Time elapsed: 1.245 s % 276.29/39.69 % (2641600)Peak memory usage: 140 MB % 276.29/39.69 % (2641600)Instructions burned: 2089 (million) % 276.29/39.69 % (2641608)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=127747646:i=2330:fgj=on:av=off:fsr=off_2739 on theBenchmark for (2739ds/2330Mi) % 276.29/39.69 % (2641604)Instruction limit reached! % 276.29/39.69 % (2641604)------------------------------ % 276.29/39.69 % (2641604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.69 % (2641604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.69 % (2641604)CaDiCaL version: 2.1.3 % 276.29/39.69 % (2641604)Termination reason: Instruction limit % 276.29/39.69 % (2641604)Termination phase: Saturation % 276.29/39.69 % (2641604)Time elapsed: 1.309 s % 276.29/39.69 % (2641604)Peak memory usage: 142 MB % 276.29/39.69 % (2641604)Instructions burned: 2197 (million) % 276.29/39.69 % (2641610)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=3723997745:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2731 on theBenchmark for (2731ds/7592Mi) % 276.29/39.69 % (2641608)Instruction limit reached! % 276.29/39.69 % (2641608)------------------------------ % 276.29/39.69 % (2641608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.69 % (2641608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.69 % (2641608)CaDiCaL version: 2.1.3 % 276.29/39.69 % (2641608)Termination reason: Instruction limit % 276.29/39.69 % (2641608)Termination phase: Saturation % 276.29/39.69 % (2641608)Time elapsed: 1.463 s % 276.29/39.69 % (2641608)Peak memory usage: 138 MB % 276.29/39.69 % (2641608)Instructions burned: 2330 (million) % 276.29/39.69 % (2641602)Instruction limit reached! % 276.29/39.69 % (2641602)------------------------------ % 276.29/39.69 % (2641602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.69 % (2641602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.69 % (2641602)CaDiCaL version: 2.1.3 % 276.29/39.69 % (2641602)Termination reason: Instruction limit % 276.29/39.69 % (2641602)Termination phase: Saturation % 276.29/39.69 % (2641602)Time elapsed: 2.700 s % 276.29/39.69 % (2641602)Peak memory usage: 153 MB % 276.29/39.69 % (2641602)Instructions burned: 4272 (million) % 276.29/39.69 % (2641612)lrs-1002_1_ncem=casc2026/models/loop6.pt:silTerminated % 300.69/43.08 % Vampire exiting % 300.69/43.08 Terminated %------------------------------------------------------------------------------