%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV514-1.050 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n018.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.92s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV514-1.050 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.18 % Computer : n018.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 11:27:55 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.22 Running first-order theorem proving % 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 7.04/1.89 % (3313136)Input is clausal, will run a generic CNF schedule. % 7.04/1.89 % (3313144)lrs+10_1_sil=8000:sp=occurrence:random_seed=3052991301:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 7.04/1.89 % (3313144)Instruction limit reached! % 7.04/1.89 % (3313144)------------------------------ % 7.04/1.89 % (3313144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.04/1.89 % (3313144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.04/1.89 % (3313144)CaDiCaL version: 2.1.3 % 7.04/1.89 % (3313144)Termination reason: Instruction limit % 7.04/1.89 % (3313144)Termination phase: Saturation % 7.04/1.89 % (3313144)Time elapsed: 0.035 s % 7.04/1.89 % (3313144)Peak memory usage: 89 MB % 7.04/1.89 % (3313144)Instructions burned: 109 (million) % 7.04/1.89 % (3313145)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1220406354:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 7.04/1.89 % (3313143)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1009857533:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 7.04/1.89 % (3313141)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=767280967:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 7.04/1.89 % (3313142)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1852573533:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 7.04/1.89 % (3313146)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2948727317:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 7.04/1.89 % (3313147)dis-21_1_sil=8000:lcm=predicate:random_seed=3699424796: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) % 7.04/1.89 % (3313147)Refutation not found, incomplete strategy % 7.04/1.89 % (3313147)------------------------------ % 7.04/1.89 % (3313147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.04/1.89 % (3313147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.04/1.89 % (3313147)CaDiCaL version: 2.1.3 % 7.04/1.89 % (3313147)Termination reason: Refutation not found, incomplete strategy % 7.04/1.89 % (3313147)Time elapsed: 0.003 s % 7.04/1.89 % (3313147)Peak memory usage: 88 MB % 7.04/1.89 % (3313147)Instructions burned: 3 (million) % 7.04/1.89 % (3313145)Instruction limit reached! % 7.04/1.89 % (3313145)------------------------------ % 7.04/1.89 % (3313145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.04/1.89 % (3313145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.04/1.89 % (3313145)CaDiCaL version: 2.1.3 % 7.04/1.89 % (3313145)Termination reason: Instruction limit % 7.04/1.89 % (3313145)Termination phase: Saturation % 7.04/1.89 % (3313145)Time elapsed: 0.065 s % 7.04/1.89 % (3313145)Peak memory usage: 89 MB % 7.04/1.89 % (3313145)Instructions burned: 115 (million) % 7.04/1.89 % (3313149)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=3977611748:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 7.04/1.89 % (3313146)Instruction limit reached! % 7.04/1.89 % (3313146)------------------------------ % 7.04/1.89 % (3313146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.04/1.89 % (3313146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.04/1.89 % (3313146)CaDiCaL version: 2.1.3 % 7.04/1.89 % (3313146)Termination reason: Instruction limit % 7.04/1.89 % (3313146)Termination phase: Saturation % 7.04/1.89 % (3313146)Time elapsed: 0.102 s % 7.04/1.89 % (3313146)Peak memory usage: 89 MB % 7.04/1.89 % (3313146)Instructions burned: 180 (million) % 7.04/1.89 % (3313149)Instruction limit reached! % 7.04/1.89 % (3313149)------------------------------ % 7.04/1.89 % (3313149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.04/1.89 % (3313149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.04/1.89 % (3313149)CaDiCaL version: 2.1.3 % 7.04/1.89 % (3313149)Termination reason: Instruction limit % 7.04/1.89 % (3313149)Termination phase: Saturation % 7.04/1.89 % (3313149)Time elapsed: 0.048 s % 7.04/1.89 % (3313149)Peak memory usage: 90 MB % 7.04/1.89 % (3313149)Instructions burned: 144 (million) % 7.04/1.89 % (3313156)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1008321402: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) % 15.05/3.02 % (3313159)lrs+10_64_to=lpo:sil=8000:random_seed=1009727476:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 15.05/3.02 % (3313158)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2165680870:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 15.05/3.02 % (3313159)Instruction limit reached! % 15.05/3.02 % (3313159)------------------------------ % 15.05/3.02 % (3313159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/3.02 % (3313159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/3.02 % (3313159)CaDiCaL version: 2.1.3 % 15.05/3.02 % (3313159)Termination reason: Instruction limit % 15.05/3.02 % (3313159)Termination phase: Saturation % 15.05/3.02 % (3313159)Time elapsed: 0.030 s % 15.05/3.02 % (3313159)Peak memory usage: 88 MB % 15.05/3.02 % (3313159)Instructions burned: 128 (million) % 15.05/3.02 % (3313147)------------------------------ % 15.05/3.02 % (3313147)------------------------------ % 15.05/3.02 % (3313156)Instruction limit reached! % 15.05/3.02 % (3313156)------------------------------ % 15.05/3.02 % (3313156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/3.02 % (3313156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/3.02 % (3313156)CaDiCaL version: 2.1.3 % 15.05/3.02 % (3313156)Termination reason: Instruction limit % 15.05/3.02 % (3313156)Termination phase: Saturation % 15.05/3.02 % (3313156)Time elapsed: 0.087 s % 15.05/3.02 % (3313156)Peak memory usage: 91 MB % 15.05/3.02 % (3313156)Instructions burned: 189 (million) % 15.05/3.02 % (3313163)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=787657056:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi) % 15.05/3.02 % (3313158)Instruction limit reached! % 15.05/3.02 % (3313158)------------------------------ % 15.05/3.02 % (3313158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/3.02 % (3313158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/3.02 % (3313158)CaDiCaL version: 2.1.3 % 15.05/3.02 % (3313158)Termination reason: Instruction limit % 15.05/3.02 % (3313158)Termination phase: Saturation % 15.05/3.02 % (3313158)Time elapsed: 0.112 s % 15.05/3.02 % (3313158)Peak memory usage: 90 MB % 15.05/3.02 % (3313158)Instructions burned: 219 (million) % 15.05/3.02 % (3313163)Instruction limit reached! % 15.05/3.02 % (3313163)------------------------------ % 15.05/3.02 % (3313163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/3.02 % (3313163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/3.02 % (3313163)CaDiCaL version: 2.1.3 % 15.05/3.02 % (3313163)Termination reason: Instruction limit % 15.05/3.02 % (3313163)Termination phase: Saturation % 15.05/3.02 % (3313163)Time elapsed: 0.059 s % 15.05/3.02 % (3313163)Peak memory usage: 90 MB % 15.05/3.02 % (3313163)Instructions burned: 195 (million) % 15.05/3.02 % (3313164)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3808509708:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 15.05/3.02 % (3313165)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=830488707:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi) % 15.05/3.02 % (3313168)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3222709689:i=107_2994 on theBenchmark for (2994ds/107Mi) % 15.05/3.02 % (3313167)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=1765058814:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 15.05/3.02 % (3313164)Instruction limit reached! % 15.05/3.02 % (3313164)------------------------------ % 15.05/3.02 % (3313164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.05/3.02 % (3313164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.05/3.02 % (3313164)CaDiCaL version: 2.1.3 % 15.05/3.02 % (3313164)Termination reason: Instruction limit % 15.05/3.02 % (3313164)Termination phase: Saturation % 15.05/3.02 % (3313164)Time elapsed: 0.093 s % 15.05/3.02 % (3313164)Peak memory usage: 91 MB % 15.05/3.02 % (3313164)Instructions burned: 157 (million) % 15.05/3.02 % (3313168)Instruction limit reached! % 15.05/3.02 % (3313168)------------------------------ % 29.27/4.89 % (3313168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.27/4.89 % (3313168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.27/4.89 % (3313168)CaDiCaL version: 2.1.3 % 29.27/4.89 % (3313168)Termination reason: Instruction limit % 29.27/4.89 % (3313168)Termination phase: Saturation % 29.27/4.89 % (3313168)Time elapsed: 0.034 s % 29.27/4.89 % (3313168)Peak memory usage: 89 MB % 29.27/4.89 % (3313168)Instructions burned: 109 (million) % 29.27/4.89 % (3313167)Instruction limit reached! % 29.27/4.89 % (3313167)------------------------------ % 29.27/4.89 % (3313167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.27/4.89 % (3313167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.27/4.89 % (3313167)CaDiCaL version: 2.1.3 % 29.27/4.89 % (3313167)Termination reason: Instruction limit % 29.27/4.89 % (3313167)Termination phase: Saturation % 29.27/4.89 % (3313167)Time elapsed: 0.048 s % 29.27/4.89 % (3313167)Peak memory usage: 90 MB % 29.27/4.89 % (3313167)Instructions burned: 108 (million) % 29.27/4.89 % (3313174)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=556686362:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi) % 29.27/4.89 % (3313173)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3231129758:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi) % 29.27/4.89 % (3313175)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2586023773:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi) % 29.27/4.89 % (3313175)Instruction limit reached! % 29.27/4.89 % (3313175)------------------------------ % 29.27/4.89 % (3313175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.27/4.89 % (3313175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.27/4.89 % (3313175)CaDiCaL version: 2.1.3 % 29.27/4.89 % (3313175)Termination reason: Instruction limit % 29.27/4.89 % (3313175)Termination phase: Saturation % 29.27/4.89 % (3313175)Time elapsed: 0.076 s % 29.27/4.89 % (3313175)Peak memory usage: 90 MB % 29.27/4.89 % (3313175)Instructions burned: 134 (million) % 29.27/4.89 % (3313173)Instruction limit reached! % 29.27/4.89 % (3313173)------------------------------ % 29.27/4.89 % (3313173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.27/4.89 % (3313173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.27/4.89 % (3313173)CaDiCaL version: 2.1.3 % 29.27/4.89 % (3313173)Termination reason: Instruction limit % 29.27/4.89 % (3313173)Termination phase: Saturation % 29.27/4.89 % (3313173)Time elapsed: 0.131 s % 29.27/4.89 % (3313173)Peak memory usage: 91 MB % 29.27/4.89 % (3313173)Instructions burned: 245 (million) % 29.27/4.89 % (3313180)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=144313233:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi) % 29.27/4.89 % (3313179)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2599721715:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi) % 29.27/4.89 % (3313180)Instruction limit reached! % 29.27/4.89 % (3313180)------------------------------ % 29.27/4.89 % (3313180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.27/4.89 % (3313180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.27/4.89 % (3313180)CaDiCaL version: 2.1.3 % 29.27/4.89 % (3313180)Termination reason: Instruction limit % 29.27/4.89 % (3313180)Termination phase: Saturation % 29.27/4.89 % (3313180)Time elapsed: 0.108 s % 29.27/4.89 % (3313180)Peak memory usage: 91 MB % 29.27/4.89 % (3313180)Instructions burned: 192 (million) % 29.27/4.89 % (3313179)Instruction limit reached! % 29.27/4.89 % (3313179)------------------------------ % 29.27/4.89 % (3313179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.27/4.89 % (3313179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.27/4.89 % (3313179)CaDiCaL version: 2.1.3 % 29.27/4.89 % (3313179)Termination reason: Instruction limit % 29.27/4.89 % (3313179)Termination phase: Saturation % 29.27/4.89 % (3313179)Time elapsed: 0.212 s % 29.27/4.89 % (3313179)Peak memory usage: 92 MB % 29.27/4.89 % (3313179)Instructions burned: 501 (million) % 29.27/4.89 % (3313183)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=206642618:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi) % 43.32/6.92 % (3313184)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3924650645:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi) % 43.32/6.92 % (3313183)Instruction limit reached! % 43.32/6.92 % (3313183)------------------------------ % 43.32/6.92 % (3313183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.32/6.92 % (3313183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.32/6.92 % (3313183)CaDiCaL version: 2.1.3 % 43.32/6.92 % (3313183)Termination reason: Instruction limit % 43.32/6.92 % (3313183)Termination phase: Saturation % 43.32/6.92 % (3313183)Time elapsed: 0.140 s % 43.32/6.92 % (3313183)Peak memory usage: 92 MB % 43.32/6.92 % (3313183)Instructions burned: 265 (million) % 43.32/6.92 % (3313184)Instruction limit reached! % 43.32/6.92 % (3313184)------------------------------ % 43.32/6.92 % (3313184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.32/6.92 % (3313184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.32/6.92 % (3313184)CaDiCaL version: 2.1.3 % 43.32/6.92 % (3313184)Termination reason: Instruction limit % 43.32/6.92 % (3313184)Termination phase: Saturation % 43.32/6.92 % (3313184)Time elapsed: 0.084 s % 43.32/6.92 % (3313184)Peak memory usage: 89 MB % 43.32/6.92 % (3313184)Instructions burned: 157 (million) % 43.32/6.92 % (3313187)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=2432002832:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi) % 43.32/6.92 % (3313188)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2669646204:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi) % 43.32/6.92 % (3313188)Instruction limit reached! % 43.32/6.92 % (3313188)------------------------------ % 43.32/6.92 % (3313188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.32/6.92 % (3313188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.32/6.92 % (3313188)CaDiCaL version: 2.1.3 % 43.32/6.92 % (3313188)Termination reason: Instruction limit % 43.32/6.92 % (3313188)Termination phase: Saturation % 43.32/6.92 % (3313188)Time elapsed: 0.283 s % 43.32/6.92 % (3313188)Peak memory usage: 93 MB % 43.32/6.92 % (3313188)Instructions burned: 537 (million) % 43.32/6.92 % (3313191)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2749289203:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi) % 43.32/6.92 % (3313174)Instruction limit reached! % 43.32/6.92 % (3313174)------------------------------ % 43.32/6.92 % (3313174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.32/6.92 % (3313174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.32/6.92 % (3313174)CaDiCaL version: 2.1.3 % 43.32/6.92 % (3313174)Termination reason: Instruction limit % 43.32/6.92 % (3313174)Termination phase: Saturation % 43.32/6.92 % (3313174)Time elapsed: 1.286 s % 43.32/6.92 % (3313174)Peak memory usage: 145 MB % 43.32/6.92 % (3313174)Instructions burned: 5213 (million) % 43.32/6.92 % (3313191)Instruction limit reached! % 43.32/6.92 % (3313191)------------------------------ % 43.32/6.92 % (3313191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.32/6.92 % (3313191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.32/6.92 % (3313191)CaDiCaL version: 2.1.3 % 43.32/6.92 % (3313191)Termination reason: Instruction limit % 43.32/6.92 % (3313191)Termination phase: Saturation % 43.32/6.92 % (3313191)Time elapsed: 0.075 s % 43.32/6.92 % (3313191)Peak memory usage: 88 MB % 43.32/6.92 % (3313191)Instructions burned: 180 (million) % 43.32/6.92 % (3313193)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=2926912681:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/10307Mi) % 43.32/6.92 % (3313194)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=1972774549:i=412:gtgl=4:gtg=exists_all_2979 on theBenchmark for (2979ds/412Mi) % 43.32/6.92 % (3313194)Instruction limit reached! % 43.32/6.92 % (3313194)------------------------------ % 43.32/6.92 % (3313194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.32/6.92 % (3313194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.32/6.92 % (3313194)CaDiCaL version: 2.1.3 % 61.56/9.30 % (3313194)Termination reason: Instruction limit % 61.56/9.30 % (3313194)Termination phase: Saturation % 61.56/9.30 % (3313194)Time elapsed: 0.177 s % 61.56/9.30 % (3313194)Peak memory usage: 91 MB % 61.56/9.30 % (3313194)Instructions burned: 412 (million) % 61.56/9.30 % (3313197)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=4079865633:s2pl=no:i=8478:s2at=4:nm=6_2976 on theBenchmark for (2976ds/8478Mi) % 61.56/9.30 % (3313165)Instruction limit reached! % 61.56/9.30 % (3313165)------------------------------ % 61.56/9.30 % (3313165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.56/9.30 % (3313165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.56/9.30 % (3313165)CaDiCaL version: 2.1.3 % 61.56/9.30 % (3313165)Termination reason: Instruction limit % 61.56/9.30 % (3313165)Termination phase: Saturation % 61.56/9.30 % (3313165)Time elapsed: 2.291 s % 61.56/9.30 % (3313165)Peak memory usage: 150 MB % 61.56/9.30 % (3313165)Instructions burned: 3394 (million) % 61.56/9.30 % (3313199)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=3408727244:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2971 on theBenchmark for (2971ds/303Mi) % 61.56/9.30 % (3313199)Refutation not found, incomplete strategy % 61.56/9.30 % (3313199)------------------------------ % 61.56/9.30 % (3313199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.56/9.30 % (3313199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.56/9.30 % (3313199)CaDiCaL version: 2.1.3 % 61.56/9.30 % (3313199)Termination reason: Refutation not found, incomplete strategy % 61.56/9.30 % (3313199)Time elapsed: 0.008 s % 61.56/9.30 % (3313199)Peak memory usage: 89 MB % 61.56/9.30 % (3313199)Instructions burned: 15 (million) % 61.56/9.30 % (3313199)------------------------------ % 61.56/9.30 % (3313199)------------------------------ % 61.56/9.30 % (3313201)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3079142952:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi) % 61.56/9.30 % (3313187)Instruction limit reached! % 61.56/9.30 % (3313187)------------------------------ % 61.56/9.30 % (3313187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.56/9.30 % (3313187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.56/9.30 % (3313187)CaDiCaL version: 2.1.3 % 61.56/9.30 % (3313187)Termination reason: Instruction limit % 61.56/9.30 % (3313187)Termination phase: Saturation % 61.56/9.30 % (3313187)Time elapsed: 2.150 s % 61.56/9.30 % (3313187)Peak memory usage: 150 MB % 61.56/9.30 % (3313187)Instructions burned: 3257 (million) % 61.56/9.30 % (3313201)Instruction limit reached! % 61.56/9.30 % (3313201)------------------------------ % 61.56/9.30 % (3313201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.56/9.30 % (3313201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.56/9.30 % (3313201)CaDiCaL version: 2.1.3 % 61.56/9.30 % (3313201)Termination reason: Instruction limit % 61.56/9.30 % (3313201)Termination phase: Saturation % 61.56/9.30 % (3313201)Time elapsed: 0.317 s % 61.56/9.30 % (3313201)Peak memory usage: 92 MB % 61.56/9.30 % (3313201)Instructions burned: 723 (million) % 61.56/9.30 % (3313203)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=943673796:i=598:bs=on:bd=preordered:av=off:ss=axioms_2963 on theBenchmark for (2963ds/598Mi) % 61.56/9.30 % (3313204)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2961583904:i=2989:sd=3:ss=axioms:sgt=60_2963 on theBenchmark for (2963ds/2989Mi) % 61.56/9.30 % (3313203)Instruction limit reached! % 61.56/9.30 % (3313203)------------------------------ % 61.56/9.30 % (3313203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.56/9.30 % (3313203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.56/9.30 % (3313203)CaDiCaL version: 2.1.3 % 61.56/9.30 % (3313203)Termination reason: Instruction limit % 61.56/9.30 % (3313203)Termination phase: Saturation % 61.56/9.30 % (3313203)Time elapsed: 0.302 s % 61.56/9.30 % (3313203)Peak memory usage: 93 MB % 61.56/9.30 % (3313203)Instructions burned: 599 (million) % 61.56/9.30 % (3313207)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=1355236627:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2958 on theBenchmark for (2958ds/1997Mi) % 98.48/14.55 % (3313193)Instruction limit reached! % 98.48/14.55 % (3313193)------------------------------ % 98.48/14.55 % (3313193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.48/14.55 % (3313193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.48/14.55 % (3313193)CaDiCaL version: 2.1.3 % 98.48/14.55 % (3313193)Termination reason: Instruction limit % 98.48/14.55 % (3313193)Termination phase: Saturation % 98.48/14.55 % (3313193)Time elapsed: 2.815 s % 98.48/14.55 % (3313193)Peak memory usage: 155 MB % 98.48/14.55 % (3313193)Instructions burned: 10308 (million) % 98.48/14.55 % (3313209)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=3037114451:i=2088:bd=preordered:av=off_2950 on theBenchmark for (2950ds/2088Mi) % 98.48/14.55 % (3313207)Instruction limit reached! % 98.48/14.55 % (3313207)------------------------------ % 98.48/14.55 % (3313207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.48/14.55 % (3313207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.48/14.55 % (3313207)CaDiCaL version: 2.1.3 % 98.48/14.55 % (3313207)Termination reason: Instruction limit % 98.48/14.55 % (3313207)Termination phase: Saturation % 98.48/14.55 % (3313207)Time elapsed: 1.323 s % 98.48/14.55 % (3313207)Peak memory usage: 139 MB % 98.48/14.55 % (3313207)Instructions burned: 1999 (million) % 98.48/14.55 % (3313211)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2751446757:i=1098:nicw=on_2944 on theBenchmark for (2944ds/1098Mi) % 98.48/14.55 % (3313209)Instruction limit reached! % 98.48/14.55 % (3313209)------------------------------ % 98.48/14.55 % (3313209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.48/14.55 % (3313209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.48/14.55 % (3313209)CaDiCaL version: 2.1.3 % 98.48/14.55 % (3313209)Termination reason: Instruction limit % 98.48/14.55 % (3313209)Termination phase: Saturation % 98.48/14.55 % (3313209)Time elapsed: 0.704 s % 98.48/14.55 % (3313209)Peak memory usage: 137 MB % 98.48/14.55 % (3313209)Instructions burned: 2089 (million) % 98.48/14.55 % (3313213)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1835774654:i=433:bd=preordered_2942 on theBenchmark for (2942ds/433Mi) % 98.48/14.55 % (3313213)Instruction limit reached! % 98.48/14.55 % (3313213)------------------------------ % 98.48/14.55 % (3313213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.48/14.55 % (3313213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.48/14.55 % (3313213)CaDiCaL version: 2.1.3 % 98.48/14.55 % (3313213)Termination reason: Instruction limit % 98.48/14.55 % (3313213)Termination phase: Saturation % 98.48/14.55 % (3313213)Time elapsed: 0.104 s % 98.48/14.55 % (3313213)Peak memory usage: 91 MB % 98.48/14.55 % (3313213)Instructions burned: 435 (million) % 98.48/14.55 % (3313204)Instruction limit reached! % 98.48/14.55 % (3313204)------------------------------ % 98.48/14.55 % (3313204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.48/14.55 % (3313204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.48/14.55 % (3313204)CaDiCaL version: 2.1.3 % 98.48/14.55 % (3313204)Termination reason: Instruction limit % 98.48/14.55 % (3313204)Termination phase: Saturation % 98.48/14.55 % (3313204)Time elapsed: 2.113 s % 98.48/14.55 % (3313204)Peak memory usage: 145 MB % 98.48/14.55 % (3313204)Instructions burned: 2990 (million) % 98.48/14.55 % (3313215)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3237130787:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2940 on theBenchmark for (2940ds/2942Mi) % 98.48/14.55 % (3313216)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=4172934690:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2940 on theBenchmark for (2940ds/6922Mi) % 98.48/14.55 % (3313211)Instruction limit reached! % 98.48/14.55 % (3313211)------------------------------ % 98.48/14.55 % (3313211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.48/14.55 % (3313211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.48/14.55 % (3313211)CaDiCaL version: 2.1.3 % 98.48/14.55 % (3313211)Termination reason: Instruction limit % 113.07/16.65 % (3313211)Termination phase: Saturation % 113.07/16.65 % (3313211)Time elapsed: 0.580 s % 113.07/16.65 % (3313211)Peak memory usage: 104 MB % 113.07/16.65 % (3313211)Instructions burned: 1098 (million) % 113.07/16.65 % (3313219)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=2061306131:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2937 on theBenchmark for (2937ds/596Mi) % 113.07/16.65 % (3313219)Refutation not found, incomplete strategy % 113.07/16.65 % (3313219)------------------------------ % 113.07/16.65 % (3313219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.65 % (3313219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.65 % (3313219)CaDiCaL version: 2.1.3 % 113.07/16.65 % (3313219)Termination reason: Refutation not found, incomplete strategy % 113.07/16.65 % (3313219)Time elapsed: 0.003 s % 113.07/16.65 % (3313219)Peak memory usage: 88 MB % 113.07/16.65 % (3313219)Instructions burned: 11 (million) % 113.07/16.65 % (3313219)------------------------------ % 113.07/16.65 % (3313219)------------------------------ % 113.07/16.65 % (3313221)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=1529218837:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2934 on theBenchmark for (2934ds/4123Mi) % 113.07/16.65 % (3313215)Instruction limit reached! % 113.07/16.65 % (3313215)------------------------------ % 113.07/16.65 % (3313215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.65 % (3313215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.65 % (3313215)CaDiCaL version: 2.1.3 % 113.07/16.65 % (3313215)Termination reason: Instruction limit % 113.07/16.65 % (3313215)Termination phase: Saturation % 113.07/16.65 % (3313215)Time elapsed: 1.810 s % 113.07/16.65 % (3313215)Peak memory usage: 145 MB % 113.07/16.65 % (3313215)Instructions burned: 2942 (million) % 113.07/16.65 % (3313221)Instruction limit reached! % 113.07/16.65 % (3313221)------------------------------ % 113.07/16.65 % (3313221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.65 % (3313221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.65 % (3313221)CaDiCaL version: 2.1.3 % 113.07/16.65 % (3313221)Termination reason: Instruction limit % 113.07/16.65 % (3313221)Termination phase: Saturation % 113.07/16.65 % (3313221)Time elapsed: 1.242 s % 113.07/16.65 % (3313221)Peak memory usage: 151 MB % 113.07/16.65 % (3313221)Instructions burned: 4124 (million) % 113.07/16.65 % (3313224)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2439142774:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2921 on theBenchmark for (2921ds/1670Mi) % 113.07/16.65 % (3313223)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1907149409:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2921 on theBenchmark for (2921ds/16411Mi) % 113.07/16.65 % (3313197)Instruction limit reached! % 113.07/16.65 % (3313197)------------------------------ % 113.07/16.65 % (3313197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.65 % (3313197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.65 % (3313197)CaDiCaL version: 2.1.3 % 113.07/16.65 % (3313197)Termination reason: Instruction limit % 113.07/16.65 % (3313197)Termination phase: Saturation % 113.07/16.65 % (3313197)Time elapsed: 5.760 s % 113.07/16.65 % (3313197)Peak memory usage: 193 MB % 113.07/16.65 % (3313197)Instructions burned: 8479 (million) % 113.07/16.65 % (3313227)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=1634151170:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2917 on theBenchmark for (2917ds/1722Mi) % 113.07/16.65 % (3313224)Instruction limit reached! % 113.07/16.65 % (3313224)------------------------------ % 113.07/16.65 % (3313224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.07/16.65 % (3313224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.07/16.65 % (3313224)CaDiCaL version: 2.1.3 % 113.07/16.65 % (3313224)Termination reason: Instruction limit % 113.07/16.65 % (3313224)Termination phase: Saturation % 113.07/16.65 % (3313224)Time elapsed: 0.609 s % 113.07/16.65 % (3313224)Peak memory usage: 135 MB % 113.07/16.65 % (3313224)Instructions burned: 1671 (million) % 113.07/16.65 % (3313229)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=2680450179:cts=off:cond=on:i=9530:bs=on:fsd=on_2914 on theBenchmark for (2914ds/9530Mi) % 134.30/19.63 % (3313227)Instruction limit reached! % 134.30/19.63 % (3313227)------------------------------ % 134.30/19.63 % (3313227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.30/19.63 % (3313227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.30/19.63 % (3313227)CaDiCaL version: 2.1.3 % 134.30/19.63 % (3313227)Termination reason: Instruction limit % 134.30/19.63 % (3313227)Termination phase: Saturation % 134.30/19.63 % (3313227)Time elapsed: 1.135 s % 134.30/19.63 % (3313227)Peak memory usage: 134 MB % 134.30/19.63 % (3313227)Instructions burned: 1722 (million) % 134.30/19.63 % (3313231)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1328587580:st=2:i=4495:sd=10:ss=included_2904 on theBenchmark for (2904ds/4495Mi) % 134.30/19.63 % (3313216)Instruction limit reached! % 134.30/19.63 % (3313216)------------------------------ % 134.30/19.63 % (3313216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.30/19.63 % (3313216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.30/19.63 % (3313216)CaDiCaL version: 2.1.3 % 134.30/19.63 % (3313216)Termination reason: Instruction limit % 134.30/19.63 % (3313216)Termination phase: Saturation % 134.30/19.63 % (3313216)Time elapsed: 4.469 s % 134.30/19.63 % (3313216)Peak memory usage: 174 MB % 134.30/19.63 % (3313216)Instructions burned: 6922 (million) % 134.30/19.63 % (3313233)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=78394510:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2894 on theBenchmark for (2894ds/4920Mi) % 134.30/19.63 % (3313231)Instruction limit reached! % 134.30/19.63 % (3313231)------------------------------ % 134.30/19.63 % (3313231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.30/19.63 % (3313231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.30/19.63 % (3313231)CaDiCaL version: 2.1.3 % 134.30/19.63 % (3313231)Termination reason: Instruction limit % 134.30/19.63 % (3313231)Termination phase: Saturation % 134.30/19.63 % (3313231)Time elapsed: 1.979 s % 134.30/19.63 % (3313231)Peak memory usage: 159 MB % 134.30/19.63 % (3313231)Instructions burned: 4502 (million) % 134.30/19.63 % (3313235)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=3333358482:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2883 on theBenchmark for (2883ds/2083Mi) % 134.30/19.63 % (3313235)Instruction limit reached! % 134.30/19.63 % (3313235)------------------------------ % 134.30/19.63 % (3313235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.30/19.63 % (3313235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.30/19.63 % (3313235)CaDiCaL version: 2.1.3 % 134.30/19.63 % (3313235)Termination reason: Instruction limit % 134.30/19.63 % (3313235)Termination phase: Saturation % 134.30/19.63 % (3313235)Time elapsed: 0.726 s % 134.30/19.63 % (3313235)Peak memory usage: 138 MB % 134.30/19.63 % (3313235)Instructions burned: 2087 (million) % 134.30/19.63 % (3313237)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=2735634717:i=4629:av=off:gsp=on_2875 on theBenchmark for (2875ds/4629Mi) % 134.30/19.63 % (3313229)Instruction limit reached! % 134.30/19.63 % (3313229)------------------------------ % 134.30/19.63 % (3313229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.30/19.63 % (3313229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.30/19.63 % (3313229)CaDiCaL version: 2.1.3 % 134.30/19.63 % (3313229)Termination reason: Instruction limit % 134.30/19.63 % (3313229)Termination phase: Saturation % 134.30/19.63 % (3313229)Time elapsed: 4.628 s % 134.30/19.63 % (3313229)Peak memory usage: 162 MB % 134.30/19.63 % (3313229)Instructions burned: 9531 (million) % 134.30/19.63 % (3313239)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3173158614:i=1258:av=off_2867 on theBenchmark for (2867ds/1258Mi) % 134.30/19.63 % (3313237)Instruction limit reached! % 134.30/19.63 % (3313237)------------------------------ % 134.30/19.63 % (3313237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.30/19.63 % (3313237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.94/22.71 % (3313237)CaDiCaL version: 2.1.3 % 155.94/22.71 % (3313237)Termination reason: Instruction limit % 155.94/22.71 % (3313237)Termination phase: Saturation % 155.94/22.71 % (3313237)Time elapsed: 1.296 s % 155.94/22.71 % (3313237)Peak memory usage: 149 MB % 155.94/22.71 % (3313237)Instructions burned: 4631 (million) % 155.94/22.71 % (3313241)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3528669598:i=7343:av=off:ss=included_2860 on theBenchmark for (2860ds/7343Mi) % 155.94/22.71 % (3313233)Instruction limit reached! % 155.94/22.71 % (3313233)------------------------------ % 155.94/22.71 % (3313233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.94/22.71 % (3313233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.94/22.71 % (3313233)CaDiCaL version: 2.1.3 % 155.94/22.71 % (3313233)Termination reason: Instruction limit % 155.94/22.71 % (3313233)Termination phase: Saturation % 155.94/22.71 % (3313233)Time elapsed: 3.291 s % 155.94/22.71 % (3313233)Peak memory usage: 161 MB % 155.94/22.71 % (3313233)Instructions burned: 4921 (million) % 155.94/22.71 % (3313239)Instruction limit reached! % 155.94/22.71 % (3313239)------------------------------ % 155.94/22.71 % (3313239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.94/22.71 % (3313239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.94/22.71 % (3313239)CaDiCaL version: 2.1.3 % 155.94/22.71 % (3313239)Termination reason: Instruction limit % 155.94/22.71 % (3313239)Termination phase: Saturation % 155.94/22.71 % (3313239)Time elapsed: 0.651 s % 155.94/22.71 % (3313239)Peak memory usage: 98 MB % 155.94/22.71 % (3313239)Instructions burned: 1259 (million) % 155.94/22.71 % (3313243)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=383327498:i=1325:sd=2:ss=axioms:sgt=16_2859 on theBenchmark for (2859ds/1325Mi) % 155.94/22.71 % (3313244)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=2534629550:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2859 on theBenchmark for (2859ds/2646Mi) % 155.94/22.71 % (3313243)Instruction limit reached! % 155.94/22.71 % (3313243)------------------------------ % 155.94/22.71 % (3313243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.94/22.71 % (3313243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.94/22.71 % (3313243)CaDiCaL version: 2.1.3 % 155.94/22.71 % (3313243)Termination reason: Instruction limit % 155.94/22.71 % (3313243)Termination phase: Saturation % 155.94/22.71 % (3313243)Time elapsed: 0.570 s % 155.94/22.71 % (3313243)Peak memory usage: 96 MB % 155.94/22.71 % (3313243)Instructions burned: 1326 (million) % 155.94/22.71 % (3313247)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2024832062:i=1489:sd=2:ep=R:ss=axioms_2852 on theBenchmark for (2852ds/1489Mi) % 155.94/22.71 % (3313247)Refutation not found, incomplete strategy % 155.94/22.71 % (3313247)------------------------------ % 155.94/22.71 % (3313247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.94/22.71 % (3313247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.94/22.71 % (3313247)CaDiCaL version: 2.1.3 % 155.94/22.71 % (3313247)Termination reason: Refutation not found, incomplete strategy % 155.94/22.71 % (3313247)Time elapsed: 0.608 s % 155.94/22.71 % (3313247)Peak memory usage: 129 MB % 155.94/22.71 % (3313247)Instructions burned: 942 (million) % 155.94/22.71 % (3313247)------------------------------ % 155.94/22.71 % (3313247)------------------------------ % 155.94/22.71 % (3313249)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=1054532552:i=1503_2842 on theBenchmark for (2842ds/1503Mi) % 155.94/22.71 % (3313244)Instruction limit reached! % 155.94/22.71 % (3313244)------------------------------ % 155.94/22.71 % (3313244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.94/22.71 % (3313244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.94/22.71 % (3313244)CaDiCaL version: 2.1.3 % 155.94/22.71 % (3313244)Termination reason: Instruction limit % 155.94/22.71 % (3313244)Termination phase: Saturation % 155.94/22.71 % (3313244)Time elapsed: 1.674 s % 155.94/22.71 % (3313244)Peak memory usage: 141 MB % 155.94/22.71 % (3313244)Instructions burned: 2647 (million) % 155.94/22.71 % (3313251)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1175964035:i=13942:kws=frequency_2841 on theBenchmark for (2841ds/13942Mi) % 176.45/25.51 % (3313241)Instruction limit reached! % 176.45/25.51 % (3313241)------------------------------ % 176.45/25.51 % (3313241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.45/25.51 % (3313241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.45/25.51 % (3313241)CaDiCaL version: 2.1.3 % 176.45/25.51 % (3313241)Termination reason: Instruction limit % 176.45/25.51 % (3313241)Termination phase: Saturation % 176.45/25.51 % (3313241)Time elapsed: 2.497 s % 176.45/25.51 % (3313241)Peak memory usage: 169 MB % 176.45/25.51 % (3313241)Instructions burned: 7345 (million) % 176.45/25.51 % (3313253)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=3447682900:i=3604:fsr=off:er=filter_2834 on theBenchmark for (2834ds/3604Mi) % 176.45/25.51 % (3313249)Instruction limit reached! % 176.45/25.51 % (3313249)------------------------------ % 176.45/25.51 % (3313249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.45/25.51 % (3313249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.45/25.51 % (3313249)CaDiCaL version: 2.1.3 % 176.45/25.51 % (3313249)Termination reason: Instruction limit % 176.45/25.51 % (3313249)Termination phase: Saturation % 176.45/25.51 % (3313249)Time elapsed: 1.015 s % 176.45/25.51 % (3313249)Peak memory usage: 134 MB % 176.45/25.51 % (3313249)Instructions burned: 1504 (million) % 176.45/25.51 % (3313255)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2935085051:i=1876:sd=1:ss=included:sgt=32_2831 on theBenchmark for (2831ds/1876Mi) % 176.45/25.51 % (3313255)Instruction limit reached! % 176.45/25.51 % (3313255)------------------------------ % 176.45/25.51 % (3313255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.45/25.51 % (3313255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.45/25.51 % (3313255)CaDiCaL version: 2.1.3 % 176.45/25.51 % (3313255)Termination reason: Instruction limit % 176.45/25.51 % (3313255)Termination phase: Saturation % 176.45/25.51 % (3313255)Time elapsed: 1.230 s % 176.45/25.51 % (3313255)Peak memory usage: 137 MB % 176.45/25.51 % (3313255)Instructions burned: 1877 (million) % 176.45/25.51 % (3313257)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2030791567:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2817 on theBenchmark for (2817ds/1932Mi) % 176.45/25.51 % (3313253)Instruction limit reached! % 176.45/25.51 % (3313253)------------------------------ % 176.45/25.51 % (3313253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.45/25.51 % (3313253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.45/25.51 % (3313253)CaDiCaL version: 2.1.3 % 176.45/25.51 % (3313253)Termination reason: Instruction limit % 176.45/25.51 % (3313253)Termination phase: Saturation % 176.45/25.51 % (3313253)Time elapsed: 1.986 s % 176.45/25.51 % (3313253)Peak memory usage: 144 MB % 176.45/25.51 % (3313253)Instructions burned: 3604 (million) % 176.45/25.51 % (3313259)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=4153511162:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2813 on theBenchmark for (2813ds/1980Mi) % 176.45/25.51 % (3313223)Instruction limit reached! % 176.45/25.51 % (3313223)------------------------------ % 176.45/25.51 % (3313223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.45/25.51 % (3313223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.45/25.51 % (3313223)CaDiCaL version: 2.1.3 % 176.45/25.51 % (3313223)Termination reason: Instruction limit % 176.45/25.51 % (3313223)Termination phase: Saturation % 176.45/25.51 % (3313223)Time elapsed: 10.955 s % 176.45/25.51 % (3313223)Peak memory usage: 291 MB % 176.45/25.51 % (3313223)Instructions burned: 16411 (million) % 176.45/25.51 % (3313257)Refutation not found, incomplete strategy % 176.45/25.51 % (3313257)------------------------------ % 176.45/25.51 % (3313257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.45/25.51 % (3313257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.45/25.51 % (3313257)CaDiCaL version: 2.1.3 % 176.45/25.51 % (3313257)Termination reason: Refutation not found, incomplete strategy % 176.45/25.51 % (3313257)Time elapsed: 0.619 s % 176.45/25.51 % (3313257)Peak memory usage: 129 MB % 176.45/25.51 % (3313257)Instructions burned: 945 (million) % 212.63/30.60 % (3313261)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=1230736891:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2810 on theBenchmark for (2810ds/3902Mi) % 212.63/30.60 % (3313257)------------------------------ % 212.63/30.60 % (3313257)------------------------------ % 212.63/30.60 % (3313263)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2714046997:avsq=on:i=3916:aac=none:amm=off_2807 on theBenchmark for (2807ds/3916Mi) % 212.63/30.60 % (3313259)Instruction limit reached! % 212.63/30.60 % (3313259)------------------------------ % 212.63/30.60 % (3313259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.63/30.60 % (3313259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.63/30.60 % (3313259)CaDiCaL version: 2.1.3 % 212.63/30.60 % (3313259)Termination reason: Instruction limit % 212.63/30.60 % (3313259)Termination phase: Saturation % 212.63/30.60 % (3313259)Time elapsed: 1.323 s % 212.63/30.60 % (3313259)Peak memory usage: 137 MB % 212.63/30.60 % (3313259)Instructions burned: 1981 (million) % 212.63/30.60 % (3313265)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2061656864:cond=on:i=3940:av=off:er=known_2799 on theBenchmark for (2799ds/3940Mi) % 212.63/30.60 % (3313251)Instruction limit reached! % 212.63/30.60 % (3313251)------------------------------ % 212.63/30.60 % (3313251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.63/30.60 % (3313251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.63/30.60 % (3313251)CaDiCaL version: 2.1.3 % 212.63/30.60 % (3313251)Termination reason: Instruction limit % 212.63/30.60 % (3313251)Termination phase: Saturation % 212.63/30.60 % (3313251)Time elapsed: 4.480 s % 212.63/30.60 % (3313251)Peak memory usage: 225 MB % 212.63/30.60 % (3313251)Instructions burned: 13944 (million) % 212.63/30.60 % (3313267)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=4275015531:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2795 on theBenchmark for (2795ds/3980Mi) % 212.63/30.60 % (3313263)Instruction limit reached! % 212.63/30.60 % (3313263)------------------------------ % 212.63/30.60 % (3313263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.63/30.60 % (3313263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.63/30.60 % (3313263)CaDiCaL version: 2.1.3 % 212.63/30.60 % (3313263)Termination reason: Instruction limit % 212.63/30.60 % (3313263)Termination phase: Saturation % 212.63/30.60 % (3313263)Time elapsed: 2.368 s % 212.63/30.60 % (3313263)Peak memory usage: 109 MB % 212.63/30.60 % (3313263)Instructions burned: 3917 (million) % 212.63/30.60 % (3313261)Instruction limit reached! % 212.63/30.60 % (3313261)------------------------------ % 212.63/30.60 % (3313261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.63/30.60 % (3313261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.63/30.60 % (3313261)CaDiCaL version: 2.1.3 % 212.63/30.60 % (3313261)Termination reason: Instruction limit % 212.63/30.60 % (3313261)Termination phase: Saturation % 212.63/30.60 % (3313261)Time elapsed: 2.691 s % 212.63/30.60 % (3313261)Peak memory usage: 153 MB % 212.63/30.60 % (3313261)Instructions burned: 3903 (million) % 212.63/30.60 % (3313269)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=2783881461:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2782 on theBenchmark for (2782ds/2087Mi) % 212.63/30.60 % (3313270)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=107732829:cts=off:cond=on:i=4272:bs=on:fsd=on_2782 on theBenchmark for (2782ds/4272Mi) % 212.63/30.60 % (3313267)Instruction limit reached! % 212.63/30.60 % (3313267)------------------------------ % 212.63/30.60 % (3313267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.63/30.60 % (3313267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.63/30.60 % (3313267)CaDiCaL version: 2.1.3 % 212.63/30.60 % (3313267)Termination reason: Instruction limit % 212.63/30.60 % (3313267)Termination phase: Saturation % 212.63/30.60 % (3313267)Time elapsed: 1.389 s % 212.63/30.60 % (3313267)Peak memory usage: 155 MB % 212.63/30.60 % (3313267)Instructions burned: 3983 (million) % 212.63/30.60 % (3313273)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3266518888:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2780 on theBenchmark for (2780ds/2197Mi) % 260.85/37.44 % (3313265)Instruction limit reached! % 260.85/37.44 % (3313265)------------------------------ % 260.85/37.44 % (3313265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.85/37.44 % (3313265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.85/37.44 % (3313265)CaDiCaL version: 2.1.3 % 260.85/37.44 % (3313265)Termination reason: Instruction limit % 260.85/37.44 % (3313265)Termination phase: Saturation % 260.85/37.44 % (3313265)Time elapsed: 1.947 s % 260.85/37.44 % (3313265)Peak memory usage: 140 MB % 260.85/37.44 % (3313265)Instructions burned: 3943 (million) % 260.85/37.44 % (3313275)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2148264004:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2778 on theBenchmark for (2778ds/6508Mi) % 260.85/37.44 % (3313273)Instruction limit reached! % 260.85/37.44 % (3313273)------------------------------ % 260.85/37.44 % (3313273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.85/37.44 % (3313273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.85/37.44 % (3313273)CaDiCaL version: 2.1.3 % 260.85/37.44 % (3313273)Termination reason: Instruction limit % 260.85/37.44 % (3313273)Termination phase: Saturation % 260.85/37.44 % (3313273)Time elapsed: 0.791 s % 260.85/37.44 % (3313273)Peak memory usage: 139 MB % 260.85/37.44 % (3313273)Instructions burned: 2198 (million) % 260.85/37.44 % (3313277)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3882794266:i=2330:fgj=on:av=off:fsr=off_2771 on theBenchmark for (2771ds/2330Mi) % 260.85/37.44 % (3313269)Instruction limit reached! % 260.85/37.44 % (3313269)------------------------------ % 260.85/37.44 % (3313269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.85/37.44 % (3313269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.85/37.44 % (3313269)CaDiCaL version: 2.1.3 % 260.85/37.44 % (3313269)Termination reason: Instruction limit % 260.85/37.44 % (3313269)Termination phase: Saturation % 260.85/37.44 % (3313269)Time elapsed: 1.389 s % 260.85/37.44 % (3313269)Peak memory usage: 141 MB % 260.85/37.44 % (3313269)Instructions burned: 2088 (million) % 260.85/37.44 % (3313279)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1649154149:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2767 on theBenchmark for (2767ds/7592Mi) % 260.85/37.44 % (3313277)Instruction limit reached! % 260.85/37.44 % (3313277)------------------------------ % 260.85/37.44 % (3313277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.85/37.44 % (3313277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.85/37.44 % (3313277)CaDiCaL version: 2.1.3 % 260.85/37.44 % (3313277)Termination reason: Instruction limit % 260.85/37.44 % (3313277)Termination phase: Saturation % 260.85/37.44 % (3313277)Time elapsed: 0.869 s % 260.85/37.44 % (3313277)Peak memory usage: 139 MB % 260.85/37.44 % (3313277)Instructions burned: 2332 (million) % 260.85/37.44 % (3313281)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=1396800253:i=2693:kws=precedence:ins=1:av=off_2761 on theBenchmark for (2761ds/2693Mi) % 260.85/37.44 % (3313281)Instruction limit reached! % 260.85/37.44 % (3313281)------------------------------ % 260.85/37.44 % (3313281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.85/37.44 % (3313281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.85/37.44 % (3313281)CaDiCaL version: 2.1.3 % 260.85/37.44 % (3313281)Termination reason: Instruction limit % 260.85/37.44 % (3313281)Termination phase: Saturation % 260.85/37.44 % (3313281)Time elapsed: 0.886 s % 260.85/37.44 % (3313281)Peak memory usage: 144 MB % 260.85/37.44 % (3313281)Instructions burned: 2693 (million) % 260.85/37.44 % (3313270)Instruction limit reached! % 260.85/37.44 % (3313270)------------------------------ % 260.85/37.44 % (3313270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.85/37.44 % (3313270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.85/37.44 % (3313270)CaDiCaL version: 2.1.3 % 260.85/37.44 % (3313270)Termination reason: Instruction limit % 260.85/37.44 % (3313270)Termination phase: Saturation % 260.85/37.44 % (3313270)Time elapsed: 2.985 s % 260.85/37.44 % (3313270)Peak memory usage: 149 MB % 260.85/37.44 % (3313270)InstruTerminated %------------------------------------------------------------------------------