%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV516-1.050 : 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 : 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:16:38 PM UTC 2026 % Result : Timeout 300.26s 43.17s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV516-1.050 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.23 % Computer : n015.cluster.edu % 0.09/0.23 % Model : x86_64 x86_64 % 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.23 % Memory : 8046.5625MB % 0.09/0.23 % OS : Linux 6.8.0-71-generic % 0.09/0.23 % CPULimit : 300 % 0.09/0.23 % WCLimit : 300 % 0.09/0.23 % DateTime : Mon Sep 28 11:30:32 UTC 2026 % 0.09/0.24 % CPUTime : % 0.09/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.28 Running first-order theorem proving % 0.09/0.28 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 % 19.23/3.58 % (2561444)Input is clausal, will run a generic CNF schedule. % 19.23/3.58 % (2561455)dis-21_1_sil=8000:lcm=predicate:random_seed=3002878477:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 19.23/3.58 % (2561455)Refutation not found, incomplete strategy % 19.23/3.58 % (2561455)------------------------------ % 19.23/3.58 % (2561455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.23/3.58 % (2561455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.23/3.58 % (2561455)CaDiCaL version: 2.1.3 % 19.23/3.58 % (2561455)Termination reason: Refutation not found, incomplete strategy % 19.23/3.58 % (2561455)Time elapsed: 0.038 s % 19.23/3.58 % (2561455)Peak memory usage: 89 MB % 19.23/3.58 % (2561455)Instructions burned: 64 (million) % 19.23/3.58 % (2561453)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2520121731:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 19.23/3.58 % (2561449)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=3188718838:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 19.23/3.58 % (2561450)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=813409636:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 19.23/3.58 % (2561452)lrs+10_1_sil=8000:sp=occurrence:random_seed=553406709:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 19.23/3.58 % (2561454)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1000161067:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 19.23/3.58 % (2561451)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=789518485:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 19.23/3.58 % (2561453)Instruction limit reached! % 19.23/3.58 % (2561453)------------------------------ % 19.23/3.58 % (2561453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.23/3.58 % (2561453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.23/3.58 % (2561453)CaDiCaL version: 2.1.3 % 19.23/3.58 % (2561453)Termination reason: Instruction limit % 19.23/3.58 % (2561453)Termination phase: Saturation % 19.23/3.58 % (2561453)Time elapsed: 0.094 s % 19.23/3.58 % (2561453)Peak memory usage: 89 MB % 19.23/3.58 % (2561453)Instructions burned: 114 (million) % 19.23/3.58 % (2561452)Instruction limit reached! % 19.23/3.58 % (2561452)------------------------------ % 19.23/3.58 % (2561452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.23/3.58 % (2561452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.23/3.58 % (2561452)CaDiCaL version: 2.1.3 % 19.23/3.58 % (2561452)Termination reason: Instruction limit % 19.23/3.58 % (2561452)Termination phase: Saturation % 19.23/3.58 % (2561452)Time elapsed: 0.097 s % 19.23/3.58 % (2561452)Peak memory usage: 89 MB % 19.23/3.58 % (2561452)Instructions burned: 107 (million) % 19.23/3.58 % (2561454)Instruction limit reached! % 19.23/3.58 % (2561454)------------------------------ % 19.23/3.58 % (2561454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.23/3.58 % (2561454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.23/3.58 % (2561454)CaDiCaL version: 2.1.3 % 19.23/3.58 % (2561454)Termination reason: Instruction limit % 19.23/3.58 % (2561454)Termination phase: Saturation % 19.23/3.58 % (2561454)Time elapsed: 0.167 s % 19.23/3.58 % (2561454)Peak memory usage: 89 MB % 19.23/3.58 % (2561454)Instructions burned: 181 (million) % 19.23/3.58 % (2561455)------------------------------ % 19.23/3.58 % (2561455)------------------------------ % 19.23/3.58 % (2561467)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=1133276376:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi) % 19.23/3.58 % (2561468)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4246024337:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi) % 19.23/3.58 % (2561467)Refutation not found, incomplete strategy % 19.23/3.58 % (2561467)------------------------------ % 19.23/3.58 % (2561467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.23/3.58 % (2561467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.44/5.93 % (2561467)CaDiCaL version: 2.1.3 % 35.44/5.93 % (2561467)Termination reason: Refutation not found, incomplete strategy % 35.44/5.93 % (2561467)Time elapsed: 0.050 s % 35.44/5.93 % (2561467)Peak memory usage: 89 MB % 35.44/5.93 % (2561467)Instructions burned: 56 (million) % 35.44/5.93 % (2561470)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3081429966:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi) % 35.44/5.93 % (2561470)Refutation not found, incomplete strategy % 35.44/5.93 % (2561470)------------------------------ % 35.44/5.93 % (2561470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.44/5.93 % (2561470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.44/5.93 % (2561470)CaDiCaL version: 2.1.3 % 35.44/5.93 % (2561470)Termination reason: Refutation not found, incomplete strategy % 35.44/5.93 % (2561470)Time elapsed: 0.036 s % 35.44/5.93 % (2561470)Peak memory usage: 88 MB % 35.44/5.93 % (2561470)Instructions burned: 43 (million) % 35.44/5.93 % (2561468)Instruction limit reached! % 35.44/5.93 % (2561468)------------------------------ % 35.44/5.93 % (2561468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.44/5.93 % (2561468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.44/5.93 % (2561468)CaDiCaL version: 2.1.3 % 35.44/5.93 % (2561468)Termination reason: Instruction limit % 35.44/5.93 % (2561468)Termination phase: Saturation % 35.44/5.93 % (2561468)Time elapsed: 0.187 s % 35.44/5.93 % (2561468)Peak memory usage: 91 MB % 35.44/5.93 % (2561468)Instructions burned: 189 (million) % 35.44/5.93 % (2561471)lrs+10_64_to=lpo:sil=8000:random_seed=3275323153:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi) % 35.44/5.93 % (2561471)Instruction limit reached! % 35.44/5.93 % (2561471)------------------------------ % 35.44/5.93 % (2561471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.44/5.93 % (2561471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.44/5.93 % (2561471)CaDiCaL version: 2.1.3 % 35.44/5.93 % (2561471)Termination reason: Instruction limit % 35.44/5.93 % (2561471)Termination phase: Saturation % 35.44/5.93 % (2561471)Time elapsed: 0.117 s % 35.44/5.93 % (2561471)Peak memory usage: 89 MB % 35.44/5.93 % (2561471)Instructions burned: 126 (million) % 35.44/5.93 % (2561467)------------------------------ % 35.44/5.93 % (2561467)------------------------------ % 35.44/5.93 % (2561477)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1406659759:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi) % 35.44/5.93 % (2561470)------------------------------ % 35.44/5.93 % (2561470)------------------------------ % 35.44/5.93 % (2561479)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4292800396:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi) % 35.44/5.93 % (2561477)Instruction limit reached! % 35.44/5.93 % (2561477)------------------------------ % 35.44/5.93 % (2561477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.44/5.93 % (2561477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.44/5.93 % (2561477)CaDiCaL version: 2.1.3 % 35.44/5.93 % (2561477)Termination reason: Instruction limit % 35.44/5.93 % (2561477)Termination phase: Saturation % 35.44/5.93 % (2561477)Time elapsed: 0.178 s % 35.44/5.93 % (2561477)Peak memory usage: 91 MB % 35.44/5.93 % (2561477)Instructions burned: 194 (million) % 35.44/5.93 % (2561480)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4156286679:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi) % 35.44/5.93 % (2561479)Instruction limit reached! % 35.44/5.93 % (2561479)------------------------------ % 35.44/5.93 % (2561479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.44/5.93 % (2561479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.44/5.93 % (2561479)CaDiCaL version: 2.1.3 % 35.44/5.93 % (2561479)Termination reason: Instruction limit % 35.44/5.93 % (2561479)Termination phase: Saturation % 35.44/5.93 % (2561479)Time elapsed: 0.136 s % 35.44/5.93 % (2561479)Peak memory usage: 93 MB % 35.44/5.93 % (2561479)Instructions burned: 158 (million) % 35.44/5.93 % (2561483)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=3690655831:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi) % 35.44/5.93 % (2561483)Instruction limit reached! % 35.44/5.93 % (2561483)------------------------------ % 59.80/9.27 % (2561483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.80/9.27 % (2561483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.80/9.27 % (2561483)CaDiCaL version: 2.1.3 % 59.80/9.27 % (2561483)Termination reason: Instruction limit % 59.80/9.27 % (2561483)Termination phase: Saturation % 59.80/9.27 % (2561483)Time elapsed: 0.098 s % 59.80/9.27 % (2561483)Peak memory usage: 90 MB % 59.80/9.27 % (2561483)Instructions burned: 106 (million) % 59.80/9.27 % (2561485)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4130389537:i=107_2986 on theBenchmark for (2986ds/107Mi) % 59.80/9.27 % (2561485)Refutation not found, incomplete strategy % 59.80/9.27 % (2561485)------------------------------ % 59.80/9.27 % (2561485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.80/9.27 % (2561485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.80/9.27 % (2561485)CaDiCaL version: 2.1.3 % 59.80/9.27 % (2561485)Termination reason: Refutation not found, incomplete strategy % 59.80/9.27 % (2561485)Time elapsed: 0.031 s % 59.80/9.27 % (2561485)Peak memory usage: 88 MB % 59.80/9.27 % (2561485)Instructions burned: 36 (million) % 59.80/9.27 % (2561487)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1411578336:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi) % 59.80/9.27 % (2561489)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2584364962:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi) % 59.80/9.27 % (2561487)Instruction limit reached! % 59.80/9.27 % (2561487)------------------------------ % 59.80/9.27 % (2561487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.80/9.27 % (2561487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.80/9.27 % (2561487)CaDiCaL version: 2.1.3 % 59.80/9.27 % (2561487)Termination reason: Instruction limit % 59.80/9.27 % (2561487)Termination phase: Saturation % 59.80/9.27 % (2561487)Time elapsed: 0.219 s % 59.80/9.27 % (2561487)Peak memory usage: 91 MB % 59.80/9.27 % (2561487)Instructions burned: 242 (million) % 59.80/9.27 % (2561485)------------------------------ % 59.80/9.27 % (2561485)------------------------------ % 59.80/9.27 % (2561493)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2589134698:i=134:sd=2:doe=on:ss=axioms:sgt=14_2981 on theBenchmark for (2981ds/134Mi) % 59.80/9.27 % (2561493)Instruction limit reached! % 59.80/9.27 % (2561493)------------------------------ % 59.80/9.27 % (2561493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.80/9.27 % (2561493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.80/9.27 % (2561493)CaDiCaL version: 2.1.3 % 59.80/9.27 % (2561493)Termination reason: Instruction limit % 59.80/9.27 % (2561493)Termination phase: Saturation % 59.80/9.27 % (2561493)Time elapsed: 0.124 s % 59.80/9.27 % (2561493)Peak memory usage: 90 MB % 59.80/9.27 % (2561493)Instructions burned: 134 (million) % 59.80/9.27 % (2561495)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=660490278:i=499:bd=all_2979 on theBenchmark for (2979ds/499Mi) % 59.80/9.27 % (2561498)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1335223553:i=191:fgj=on:bd=all_2976 on theBenchmark for (2976ds/191Mi) % 59.80/9.27 % (2561495)Instruction limit reached! % 59.80/9.27 % (2561495)------------------------------ % 59.80/9.27 % (2561495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.80/9.27 % (2561495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.80/9.27 % (2561495)CaDiCaL version: 2.1.3 % 59.80/9.27 % (2561495)Termination reason: Instruction limit % 59.80/9.27 % (2561495)Termination phase: Saturation % 59.80/9.27 % (2561495)Time elapsed: 0.434 s % 59.80/9.27 % (2561495)Peak memory usage: 94 MB % 59.80/9.27 % (2561495)Instructions burned: 499 (million) % 59.80/9.27 % (2561498)Instruction limit reached! % 59.80/9.27 % (2561498)------------------------------ % 59.80/9.27 % (2561498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.80/9.27 % (2561498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.80/9.27 % (2561498)CaDiCaL version: 2.1.3 % 59.80/9.27 % (2561498)Termination reason: Instruction limit % 59.80/9.27 % (2561498)Termination phase: Saturation % 59.80/9.27 % (2561498)Time elapsed: 0.181 s % 94.50/14.12 % (2561498)Peak memory usage: 91 MB % 94.50/14.12 % (2561498)Instructions burned: 191 (million) % 94.50/14.12 % (2561502)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2259386042:i=264:kws=precedence:fsr=off_2972 on theBenchmark for (2972ds/264Mi) % 94.50/14.12 % (2561503)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=582696403:cond=on:i=156:bs=on:gtg=exists_all:er=known_2972 on theBenchmark for (2972ds/156Mi) % 94.50/14.12 % (2561503)Instruction limit reached! % 94.50/14.12 % (2561503)------------------------------ % 94.50/14.12 % (2561503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.50/14.12 % (2561503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.50/14.12 % (2561503)CaDiCaL version: 2.1.3 % 94.50/14.12 % (2561503)Termination reason: Instruction limit % 94.50/14.12 % (2561503)Termination phase: Saturation % 94.50/14.12 % (2561503)Time elapsed: 0.148 s % 94.50/14.12 % (2561503)Peak memory usage: 90 MB % 94.50/14.12 % (2561503)Instructions burned: 156 (million) % 94.50/14.12 % (2561502)Instruction limit reached! % 94.50/14.12 % (2561502)------------------------------ % 94.50/14.13 % (2561502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.50/14.13 % (2561502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.50/14.13 % (2561502)CaDiCaL version: 2.1.3 % 94.50/14.13 % (2561502)Termination reason: Instruction limit % 94.50/14.13 % (2561502)Termination phase: Saturation % 94.50/14.13 % (2561502)Time elapsed: 0.199 s % 94.50/14.13 % (2561502)Peak memory usage: 92 MB % 94.50/14.13 % (2561502)Instructions burned: 264 (million) % 94.50/14.13 % (2561508)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3765115880:i=537:av=off:ss=included_2967 on theBenchmark for (2967ds/537Mi) % 94.50/14.13 % (2561507)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=1121993099:i=3256:kws=precedence:bd=preordered:av=off_2967 on theBenchmark for (2967ds/3256Mi) % 94.50/14.13 % (2561508)Instruction limit reached! % 94.50/14.13 % (2561508)------------------------------ % 94.50/14.13 % (2561508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.50/14.13 % (2561508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.50/14.13 % (2561508)CaDiCaL version: 2.1.3 % 94.50/14.13 % (2561508)Termination reason: Instruction limit % 94.50/14.13 % (2561508)Termination phase: Saturation % 94.50/14.13 % (2561508)Time elapsed: 0.506 s % 94.50/14.13 % (2561508)Peak memory usage: 95 MB % 94.50/14.13 % (2561508)Instructions burned: 538 (million) % 94.50/14.13 % (2561514)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=380918629:i=180:bd=preordered:av=off_2959 on theBenchmark for (2959ds/180Mi) % 94.50/14.13 % (2561480)Instruction limit reached! % 94.50/14.13 % (2561480)------------------------------ % 94.50/14.13 % (2561480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.50/14.13 % (2561480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.50/14.13 % (2561480)CaDiCaL version: 2.1.3 % 94.50/14.13 % (2561480)Termination reason: Instruction limit % 94.50/14.13 % (2561480)Termination phase: Saturation % 94.50/14.13 % (2561480)Time elapsed: 3.101 s % 94.50/14.13 % (2561480)Peak memory usage: 154 MB % 94.50/14.13 % (2561480)Instructions burned: 3394 (million) % 94.50/14.13 % (2561514)Instruction limit reached! % 94.50/14.13 % (2561514)------------------------------ % 94.50/14.13 % (2561514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.50/14.13 % (2561514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.50/14.13 % (2561514)CaDiCaL version: 2.1.3 % 94.50/14.13 % (2561514)Termination reason: Instruction limit % 94.50/14.13 % (2561514)Termination phase: Saturation % 94.50/14.13 % (2561514)Time elapsed: 0.154 s % 94.50/14.13 % (2561514)Peak memory usage: 91 MB % 94.50/14.13 % (2561514)Instructions burned: 181 (million) % 94.50/14.13 % (2561516)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=986363826:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2955 on theBenchmark for (2955ds/10307Mi) % 94.50/14.13 % (2561517)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=42309736:i=412:gtgl=4:gtg=exists_all_2955 on theBenchmark for (2955ds/412Mi) % 94.50/14.13 % (2561517)Instruction limit reached! % 94.50/14.13 % (2561517)------------------------------ % 135.39/19.89 % (2561517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.39/19.89 % (2561517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.39/19.89 % (2561517)CaDiCaL version: 2.1.3 % 135.39/19.89 % (2561517)Termination reason: Instruction limit % 135.39/19.89 % (2561517)Termination phase: Saturation % 135.39/19.89 % (2561517)Time elapsed: 0.377 s % 135.39/19.89 % (2561517)Peak memory usage: 97 MB % 135.39/19.89 % (2561517)Instructions burned: 413 (million) % 135.39/19.89 % (2561522)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=1214219772:s2pl=no:i=8478:s2at=4:nm=6_2948 on theBenchmark for (2948ds/8478Mi) % 135.39/19.89 % (2561507)Instruction limit reached! % 135.39/19.89 % (2561507)------------------------------ % 135.39/19.89 % (2561507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.39/19.89 % (2561507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.39/19.89 % (2561507)CaDiCaL version: 2.1.3 % 135.39/19.89 % (2561507)Termination reason: Instruction limit % 135.39/19.89 % (2561507)Termination phase: Saturation % 135.39/19.89 % (2561507)Time elapsed: 3.534 s % 135.39/19.89 % (2561507)Peak memory usage: 152 MB % 135.39/19.89 % (2561507)Instructions burned: 3257 (million) % 135.39/19.89 % (2561489)Instruction limit reached! % 135.39/19.89 % (2561489)------------------------------ % 135.39/19.89 % (2561489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.39/19.89 % (2561489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.39/19.89 % (2561489)CaDiCaL version: 2.1.3 % 135.39/19.89 % (2561489)Termination reason: Instruction limit % 135.39/19.89 % (2561489)Termination phase: Saturation % 135.39/19.89 % (2561489)Time elapsed: 5.240 s % 135.39/19.89 % (2561489)Peak memory usage: 172 MB % 135.39/19.89 % (2561489)Instructions burned: 5210 (million) % 135.39/19.89 % (2561528)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=1378402115:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2929 on theBenchmark for (2929ds/303Mi) % 135.39/19.89 % (2561529)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2176084265:st=4:i=720:sd=3:fsr=off:ss=axioms_2928 on theBenchmark for (2928ds/720Mi) % 135.39/19.89 % (2561528)Instruction limit reached! % 135.39/19.89 % (2561528)------------------------------ % 135.39/19.89 % (2561528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.39/19.89 % (2561528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.39/19.89 % (2561528)CaDiCaL version: 2.1.3 % 135.39/19.89 % (2561528)Termination reason: Instruction limit % 135.39/19.89 % (2561528)Termination phase: Saturation % 135.39/19.89 % (2561528)Time elapsed: 0.213 s % 135.39/19.89 % (2561528)Peak memory usage: 91 MB % 135.39/19.89 % (2561528)Instructions burned: 303 (million) % 135.39/19.89 % (2561534)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2596049557:i=598:bs=on:bd=preordered:av=off:ss=axioms_2924 on theBenchmark for (2924ds/598Mi) % 135.39/19.89 % (2561534)Refutation not found, incomplete strategy % 135.39/19.89 % (2561534)------------------------------ % 135.39/19.89 % (2561534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.39/19.89 % (2561534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.39/19.89 % (2561534)CaDiCaL version: 2.1.3 % 135.39/19.89 % (2561534)Termination reason: Refutation not found, incomplete strategy % 135.39/19.89 % (2561534)Time elapsed: 0.070 s % 135.39/19.89 % (2561534)Peak memory usage: 89 MB % 135.39/19.89 % (2561534)Instructions burned: 82 (million) % 135.39/19.89 % (2561529)Instruction limit reached! % 135.39/19.89 % (2561529)------------------------------ % 135.39/19.89 % (2561529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.39/19.89 % (2561529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.39/19.89 % (2561529)CaDiCaL version: 2.1.3 % 135.39/19.89 % (2561529)Termination reason: Instruction limit % 135.39/19.89 % (2561529)Termination phase: Saturation % 135.39/19.89 % (2561529)Time elapsed: 0.777 s % 135.39/19.89 % (2561529)Peak memory usage: 97 MB % 135.39/19.89 % (2561529)Instructions burned: 720 (million) % 135.39/19.89 % (2561534)------------------------------ % 135.39/19.89 % (2561534)------------------------------ % 135.39/19.89 % (2561536)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1681163060:i=2989:sd=3:ss=axioms:sgt=60_2917 on theBenchmark for (2917ds/2989Mi) % 192.93/27.95 % (2561537)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=1662920910:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2917 on theBenchmark for (2917ds/1997Mi) % 192.93/27.95 % (2561537)Instruction limit reached! % 192.93/27.95 % (2561537)------------------------------ % 192.93/27.95 % (2561537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.93/27.95 % (2561537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.93/27.95 % (2561537)CaDiCaL version: 2.1.3 % 192.93/27.95 % (2561537)Termination reason: Instruction limit % 192.93/27.95 % (2561537)Termination phase: Saturation % 192.93/27.95 % (2561537)Time elapsed: 2.101 s % 192.93/27.95 % (2561537)Peak memory usage: 141 MB % 192.93/27.95 % (2561537)Instructions burned: 1998 (million) % 192.93/27.95 % (2561546)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=1202532273:i=2088:bd=preordered:av=off_2893 on theBenchmark for (2893ds/2088Mi) % 192.93/27.95 % (2561536)Instruction limit reached! % 192.93/27.95 % (2561536)------------------------------ % 192.93/27.95 % (2561536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.93/27.95 % (2561536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.93/27.95 % (2561536)CaDiCaL version: 2.1.3 % 192.93/27.95 % (2561536)Termination reason: Instruction limit % 192.93/27.95 % (2561536)Termination phase: Saturation % 192.93/27.95 % (2561536)Time elapsed: 2.841 s % 192.93/27.95 % (2561536)Peak memory usage: 146 MB % 192.93/27.95 % (2561536)Instructions burned: 2989 (million) % 192.93/27.95 % (2561548)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2929267906:i=1098:nicw=on_2886 on theBenchmark for (2886ds/1098Mi) % 192.93/27.95 % (2561548)Instruction limit reached! % 192.93/27.95 % (2561548)------------------------------ % 192.93/27.95 % (2561548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.93/27.95 % (2561548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.93/27.95 % (2561548)CaDiCaL version: 2.1.3 % 192.93/27.95 % (2561548)Termination reason: Instruction limit % 192.93/27.95 % (2561548)Termination phase: Saturation % 192.93/27.95 % (2561548)Time elapsed: 0.874 s % 192.93/27.95 % (2561548)Peak memory usage: 102 MB % 192.93/27.95 % (2561548)Instructions burned: 1099 (million) % 192.93/27.95 % (2561554)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=798313248:i=433:bd=preordered_2874 on theBenchmark for (2874ds/433Mi) % 192.93/27.95 % (2561554)Refutation not found, incomplete strategy % 192.93/27.95 % (2561554)------------------------------ % 192.93/27.95 % (2561554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.93/27.95 % (2561554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.93/27.95 % (2561554)CaDiCaL version: 2.1.3 % 192.93/27.95 % (2561554)Termination reason: Refutation not found, incomplete strategy % 192.93/27.95 % (2561554)Time elapsed: 0.077 s % 192.93/27.95 % (2561554)Peak memory usage: 92 MB % 192.93/27.95 % (2561554)Instructions burned: 83 (million) % 192.93/27.95 % (2561546)Instruction limit reached! % 192.93/27.95 % (2561546)------------------------------ % 192.93/27.95 % (2561546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.93/27.95 % (2561546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.93/27.95 % (2561546)CaDiCaL version: 2.1.3 % 192.93/27.95 % (2561546)Termination reason: Instruction limit % 192.93/27.95 % (2561546)Termination phase: Saturation % 192.93/27.95 % (2561546)Time elapsed: 2.074 s % 192.93/27.95 % (2561546)Peak memory usage: 142 MB % 192.93/27.95 % (2561546)Instructions burned: 2088 (million) % 192.93/27.95 % (2561554)------------------------------ % 192.93/27.95 % (2561554)------------------------------ % 192.93/27.95 % (2561556)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=325912224:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2869 on theBenchmark for (2869ds/2942Mi) % 192.93/27.95 % (2561516)Instruction limit reached! % 192.93/27.95 % (2561516)------------------------------ % 192.93/27.95 % (2561516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.93/27.95 % (2561516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.49/29.89 % (2561516)CaDiCaL version: 2.1.3 % 206.49/29.89 % (2561516)Termination reason: Instruction limit % 206.49/29.89 % (2561516)Termination phase: Saturation % 206.49/29.89 % (2561516)Time elapsed: 8.568 s % 206.49/29.89 % (2561516)Peak memory usage: 152 MB % 206.49/29.89 % (2561516)Instructions burned: 10308 (million) % 206.49/29.89 % (2561558)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2434952655:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2867 on theBenchmark for (2867ds/6922Mi) % 206.49/29.89 % (2561561)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=3834021284:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2866 on theBenchmark for (2866ds/596Mi) % 206.49/29.89 % (2561561)Refutation not found, incomplete strategy % 206.49/29.89 % (2561561)------------------------------ % 206.49/29.89 % (2561561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.49/29.89 % (2561561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.49/29.89 % (2561561)CaDiCaL version: 2.1.3 % 206.49/29.89 % (2561561)Termination reason: Refutation not found, incomplete strategy % 206.49/29.89 % (2561561)Time elapsed: 0.210 s % 206.49/29.89 % (2561561)Peak memory usage: 91 MB % 206.49/29.89 % (2561561)Instructions burned: 234 (million) % 206.49/29.89 % (2561561)------------------------------ % 206.49/29.89 % (2561561)------------------------------ % 206.49/29.89 % (2561522)Instruction limit reached! % 206.49/29.89 % (2561522)------------------------------ % 206.49/29.89 % (2561522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.49/29.89 % (2561522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.49/29.89 % (2561522)CaDiCaL version: 2.1.3 % 206.49/29.89 % (2561522)Termination reason: Instruction limit % 206.49/29.89 % (2561522)Termination phase: Saturation % 206.49/29.89 % (2561522)Time elapsed: 9.092 s % 206.49/29.89 % (2561522)Peak memory usage: 204 MB % 206.49/29.89 % (2561522)Instructions burned: 8478 (million) % 206.49/29.89 % (2561564)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=3714620542:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2857 on theBenchmark for (2857ds/4123Mi) % 206.49/29.89 % (2561567)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3943248183:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2854 on theBenchmark for (2854ds/16411Mi) % 206.49/29.89 % (2561556)Instruction limit reached! % 206.49/29.89 % (2561556)------------------------------ % 206.49/29.89 % (2561556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.49/29.89 % (2561556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.49/29.89 % (2561556)CaDiCaL version: 2.1.3 % 206.49/29.89 % (2561556)Termination reason: Instruction limit % 206.49/29.89 % (2561556)Termination phase: Saturation % 206.49/29.89 % (2561556)Time elapsed: 2.907 s % 206.49/29.89 % (2561556)Peak memory usage: 145 MB % 206.49/29.89 % (2561556)Instructions burned: 2942 (million) % 206.49/29.89 % (2561574)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1234031938:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2837 on theBenchmark for (2837ds/1670Mi) % 206.49/29.89 % (2561574)Instruction limit reached! % 206.49/29.89 % (2561574)------------------------------ % 206.49/29.89 % (2561574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.49/29.89 % (2561574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.49/29.89 % (2561574)CaDiCaL version: 2.1.3 % 206.49/29.89 % (2561574)Termination reason: Instruction limit % 206.49/29.89 % (2561574)Termination phase: Saturation % 206.49/29.89 % (2561574)Time elapsed: 1.482 s % 206.49/29.89 % (2561574)Peak memory usage: 139 MB % 206.49/29.89 % (2561574)Instructions burned: 1670 (million) % 206.49/29.89 % (2561578)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=2673609869:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2819 on theBenchmark for (2819ds/1722Mi) % 206.49/29.89 % (2561564)Instruction limit reached! % 206.49/29.89 % (2561564)------------------------------ % 206.49/29.89 % (2561564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 206.49/29.89 % (2561564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 206.49/29.89 % (2561564)CaDiCaL version: 2.1.3 % 230.39/33.39 % (2561564)Termination reason: Instruction limit % 230.39/33.39 % (2561564)Termination phase: Saturation % 230.39/33.39 % (2561564)Time elapsed: 4.552 s % 230.39/33.39 % (2561564)Peak memory usage: 159 MB % 230.39/33.39 % (2561564)Instructions burned: 4123 (million) % 230.39/33.39 % (2561583)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=3440087931:cts=off:cond=on:i=9530:bs=on:fsd=on_2808 on theBenchmark for (2808ds/9530Mi) % 230.39/33.39 % (2561578)Instruction limit reached! % 230.39/33.39 % (2561578)------------------------------ % 230.39/33.39 % (2561578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.39/33.39 % (2561578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.39/33.39 % (2561578)CaDiCaL version: 2.1.3 % 230.39/33.39 % (2561578)Termination reason: Instruction limit % 230.39/33.39 % (2561578)Termination phase: Saturation % 230.39/33.39 % (2561578)Time elapsed: 1.565 s % 230.39/33.39 % (2561578)Peak memory usage: 136 MB % 230.39/33.39 % (2561578)Instructions burned: 1723 (million) % 230.39/33.39 % (2561586)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1734860086:st=2:i=4495:sd=10:ss=included_2801 on theBenchmark for (2801ds/4495Mi) % 230.39/33.39 % (2561558)Instruction limit reached! % 230.39/33.39 % (2561558)------------------------------ % 230.39/33.39 % (2561558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.39/33.39 % (2561558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.39/33.39 % (2561558)CaDiCaL version: 2.1.3 % 230.39/33.39 % (2561558)Termination reason: Instruction limit % 230.39/33.39 % (2561558)Termination phase: Saturation % 230.39/33.39 % (2561558)Time elapsed: 6.724 s % 230.39/33.39 % (2561558)Peak memory usage: 220 MB % 230.39/33.39 % (2561558)Instructions burned: 6923 (million) % 230.39/33.39 % (2561588)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=1102107377:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2796 on theBenchmark for (2796ds/4920Mi) % 230.39/33.39 % (2561586)Instruction limit reached! % 230.39/33.39 % (2561586)------------------------------ % 230.39/33.39 % (2561586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.39/33.39 % (2561586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.39/33.39 % (2561586)CaDiCaL version: 2.1.3 % 230.39/33.39 % (2561586)Termination reason: Instruction limit % 230.39/33.39 % (2561586)Termination phase: Saturation % 230.39/33.39 % (2561586)Time elapsed: 4.330 s % 230.39/33.39 % (2561586)Peak memory usage: 165 MB % 230.39/33.39 % (2561586)Instructions burned: 4496 (million) % 230.39/33.39 % (2561594)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=2675496339:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2755 on theBenchmark for (2755ds/2083Mi) % 230.39/33.39 % (2561588)Instruction limit reached! % 230.39/33.39 % (2561588)------------------------------ % 230.39/33.39 % (2561588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.39/33.39 % (2561588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.39/33.39 % (2561588)CaDiCaL version: 2.1.3 % 230.39/33.39 % (2561588)Termination reason: Instruction limit % 230.39/33.39 % (2561588)Termination phase: Saturation % 230.39/33.39 % (2561588)Time elapsed: 5.132 s % 230.39/33.39 % (2561588)Peak memory usage: 163 MB % 230.39/33.39 % (2561588)Instructions burned: 4920 (million) % 230.39/33.39 % (2561596)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=1684201763:i=4629:av=off:gsp=on_2742 on theBenchmark for (2742ds/4629Mi) % 230.39/33.39 % (2561594)Instruction limit reached! % 230.39/33.39 % (2561594)------------------------------ % 230.39/33.39 % (2561594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.39/33.39 % (2561594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.39/33.39 % (2561594)CaDiCaL version: 2.1.3 % 230.39/33.39 % (2561594)Termination reason: Instruction limit % 230.39/33.39 % (2561594)Termination phase: Saturation % 230.39/33.39 % (2561594)Time elapsed: 2.150 s % 230.39/33.39 % (2561594)Peak memory usage: 141 MB % 230.39/33.39 % (2561594)Instructions burned: 2083 (million) % 230.39/33.39 % (2561598)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=4035187057:i=1258:av=off_2730 on theBenchmark for (2730ds/1258Mi) % 250.61/36.14 % (2561596)Refutation not found, incomplete strategy % 250.61/36.14 % (2561596)------------------------------ % 250.61/36.14 % (2561596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.61/36.14 % (2561596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.61/36.14 % (2561596)CaDiCaL version: 2.1.3 % 250.61/36.14 % (2561596)Termination reason: Refutation not found, incomplete strategy % 250.61/36.14 % (2561596)Time elapsed: 1.192 s % 250.61/36.14 % (2561596)Peak memory usage: 138 MB % 250.61/36.14 % (2561596)Instructions burned: 1164 (million) % 250.61/36.14 % (2561596)------------------------------ % 250.61/36.14 % (2561596)------------------------------ % 250.61/36.14 % (2561583)Instruction limit reached! % 250.61/36.14 % (2561583)------------------------------ % 250.61/36.14 % (2561583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.61/36.14 % (2561583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.61/36.14 % (2561583)CaDiCaL version: 2.1.3 % 250.61/36.14 % (2561583)Termination reason: Instruction limit % 250.61/36.14 % (2561583)Termination phase: Saturation % 250.61/36.14 % (2561583)Time elapsed: 8.277 s % 250.61/36.14 % (2561583)Peak memory usage: 156 MB % 250.61/36.14 % (2561583)Instructions burned: 9531 (million) % 250.61/36.14 % (2561600)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=785184160:i=7343:av=off:ss=included_2724 on theBenchmark for (2724ds/7343Mi) % 250.61/36.14 % (2561618)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2571028352:i=1325:sd=2:ss=axioms:sgt=16_2722 on theBenchmark for (2722ds/1325Mi) % 250.61/36.14 % (2561618)Refutation not found, incomplete strategy % 250.61/36.14 % (2561618)------------------------------ % 250.61/36.14 % (2561618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.61/36.14 % (2561618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.61/36.14 % (2561618)CaDiCaL version: 2.1.3 % 250.61/36.14 % (2561618)Termination reason: Refutation not found, incomplete strategy % 250.61/36.14 % (2561618)Time elapsed: 0.019 s % 250.61/36.14 % (2561618)Peak memory usage: 88 MB % 250.61/36.14 % (2561618)Instructions burned: 43 (million) % 250.61/36.14 % (2561598)Instruction limit reached! % 250.61/36.14 % (2561598)------------------------------ % 250.61/36.14 % (2561598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.61/36.14 % (2561598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.61/36.14 % (2561598)CaDiCaL version: 2.1.3 % 250.61/36.14 % (2561598)Termination reason: Instruction limit % 250.61/36.14 % (2561598)Termination phase: Saturation % 250.61/36.14 % (2561598)Time elapsed: 0.850 s % 250.61/36.14 % (2561598)Peak memory usage: 104 MB % 250.61/36.14 % (2561598)Instructions burned: 1259 (million) % 250.61/36.14 % (2561618)------------------------------ % 250.61/36.14 % (2561618)------------------------------ % 250.61/36.14 % (2561676)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=2877083998:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2719 on theBenchmark for (2719ds/2646Mi) % 250.61/36.14 % (2561694)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2011726429:i=1489:sd=2:ep=R:ss=axioms_2718 on theBenchmark for (2718ds/1489Mi) % 250.61/36.14 % (2561694)Refutation not found, incomplete strategy % 250.61/36.14 % (2561694)------------------------------ % 250.61/36.14 % (2561694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.61/36.14 % (2561694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.61/36.14 % (2561694)CaDiCaL version: 2.1.3 % 250.61/36.14 % (2561694)Termination reason: Refutation not found, incomplete strategy % 250.61/36.14 % (2561694)Time elapsed: 0.707 s % 250.61/36.14 % (2561694)Peak memory usage: 136 MB % 250.61/36.14 % (2561694)Instructions burned: 1128 (million) % 250.61/36.14 % (2561567)Instruction limit reached! % 250.61/36.14 % (2561567)------------------------------ % 250.61/36.14 % (2561567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.61/36.14 % (2561567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.61/36.14 % (2561567)CaDiCaL version: 2.1.3 % 250.61/36.14 % (2561567)Termination reason: Instruction limit % 250.61/36.14 % (2561567)Termination phase: Saturation % 250.61/36.14 % (2561567)Time elapsed: 14.224 s % 250.61/36.14 % (2561567)Peak memory usage: 282 MB % 273.04/39.32 % (2561567)Instructions burned: 16411 (million) % 273.04/39.32 % (2561694)------------------------------ % 273.04/39.32 % (2561694)------------------------------ % 273.04/39.32 % (2561761)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=2249420467:i=1503_2708 on theBenchmark for (2708ds/1503Mi) % 273.04/39.32 % (2561762)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=85286465:i=13942:kws=frequency_2707 on theBenchmark for (2707ds/13942Mi) % 273.04/39.32 % (2561676)Instruction limit reached! % 273.04/39.32 % (2561676)------------------------------ % 273.04/39.32 % (2561676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.04/39.32 % (2561676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.04/39.32 % (2561676)CaDiCaL version: 2.1.3 % 273.04/39.32 % (2561676)Termination reason: Instruction limit % 273.04/39.32 % (2561676)Termination phase: Saturation % 273.04/39.32 % (2561676)Time elapsed: 1.469 s % 273.04/39.32 % (2561676)Peak memory usage: 139 MB % 273.04/39.32 % (2561676)Instructions burned: 2648 (million) % 273.04/39.32 % (2561765)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=957480608:i=3604:fsr=off:er=filter_2703 on theBenchmark for (2703ds/3604Mi) % 273.04/39.32 % (2561761)Instruction limit reached! % 273.04/39.32 % (2561761)------------------------------ % 273.04/39.32 % (2561761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.04/39.32 % (2561761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.04/39.32 % (2561761)CaDiCaL version: 2.1.3 % 273.04/39.32 % (2561761)Termination reason: Instruction limit % 273.04/39.32 % (2561761)Termination phase: Saturation % 273.04/39.32 % (2561761)Time elapsed: 0.975 s % 273.04/39.32 % (2561761)Peak memory usage: 137 MB % 273.04/39.32 % (2561761)Instructions burned: 1504 (million) % 273.04/39.32 % (2561767)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=999277339:i=1876:sd=1:ss=included:sgt=32_2697 on theBenchmark for (2697ds/1876Mi) % 273.04/39.32 % (2561767)Instruction limit reached! % 273.04/39.32 % (2561767)------------------------------ % 273.04/39.32 % (2561767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.04/39.32 % (2561767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.04/39.32 % (2561767)CaDiCaL version: 2.1.3 % 273.04/39.32 % (2561767)Termination reason: Instruction limit % 273.04/39.32 % (2561767)Termination phase: Saturation % 273.04/39.32 % (2561767)Time elapsed: 1.098 s % 273.04/39.32 % (2561767)Peak memory usage: 139 MB % 273.04/39.32 % (2561767)Instructions burned: 1877 (million) % 273.04/39.32 % (2561769)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3960188977:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2684 on theBenchmark for (2684ds/1932Mi) % 273.04/39.32 % (2561600)Instruction limit reached! % 273.04/39.32 % (2561600)------------------------------ % 273.04/39.32 % (2561600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.04/39.32 % (2561600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.04/39.32 % (2561600)CaDiCaL version: 2.1.3 % 273.04/39.32 % (2561600)Termination reason: Instruction limit % 273.04/39.32 % (2561600)Termination phase: Saturation % 273.04/39.32 % (2561600)Time elapsed: 4.464 s % 273.04/39.32 % (2561600)Peak memory usage: 187 MB % 273.04/39.32 % (2561600)Instructions burned: 7345 (million) % 273.04/39.32 % (2561765)Instruction limit reached! % 273.04/39.32 % (2561765)------------------------------ % 273.04/39.32 % (2561765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.04/39.32 % (2561765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.04/39.32 % (2561765)CaDiCaL version: 2.1.3 % 273.04/39.32 % (2561765)Termination reason: Instruction limit % 273.04/39.32 % (2561765)Termination phase: Saturation % 273.04/39.32 % (2561765)Time elapsed: 2.568 s % 273.04/39.32 % (2561765)Peak memory usage: 150 MB % 273.04/39.32 % (2561765)Instructions burned: 3604 (million) % 273.04/39.32 % (2561772)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=1417230964:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2675 on theBenchmark for (2675ds/3902Mi) % 273.04/39.32 % (2561771)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_Terminated %------------------------------------------------------------------------------