%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV525-1.040 : 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 : n007.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:42 PM UTC 2026 % Result : Timeout 297.27s 42.67s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV525-1.040 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.18 % Computer : n007.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 11:29:10 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.22 Running first-order theorem proving % 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.69/2.15 % (2333177)Input is clausal, will run a generic CNF schedule. % 10.69/2.15 % (2333184)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=531054385:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 10.69/2.15 % (2333186)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=718696780:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 10.69/2.15 % (2333188)dis-21_1_sil=8000:lcm=predicate:random_seed=2105672241: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) % 10.69/2.15 % (2333183)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=970723708:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 10.69/2.15 % (2333185)lrs+10_1_sil=8000:sp=occurrence:random_seed=3141596425:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 10.69/2.15 % (2333182)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=541436764:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 10.69/2.15 % (2333188)Refutation not found, incomplete strategy % 10.69/2.15 % (2333188)------------------------------ % 10.69/2.15 % (2333188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.15 % (2333188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.15 % (2333188)CaDiCaL version: 2.1.3 % 10.69/2.15 % (2333188)Termination reason: Refutation not found, incomplete strategy % 10.69/2.15 % (2333188)Time elapsed: 0.002 s % 10.69/2.15 % (2333188)Peak memory usage: 88 MB % 10.69/2.15 % (2333188)Instructions burned: 3 (million) % 10.69/2.15 % (2333187)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2156378216:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 10.69/2.15 % (2333186)Instruction limit reached! % 10.69/2.15 % (2333186)------------------------------ % 10.69/2.15 % (2333186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.15 % (2333186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.15 % (2333186)CaDiCaL version: 2.1.3 % 10.69/2.15 % (2333186)Termination reason: Instruction limit % 10.69/2.15 % (2333186)Termination phase: Saturation % 10.69/2.15 % (2333186)Time elapsed: 0.056 s % 10.69/2.15 % (2333186)Peak memory usage: 88 MB % 10.69/2.15 % (2333186)Instructions burned: 115 (million) % 10.69/2.15 % (2333185)Instruction limit reached! % 10.69/2.15 % (2333185)------------------------------ % 10.69/2.15 % (2333185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.15 % (2333185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.15 % (2333185)CaDiCaL version: 2.1.3 % 10.69/2.15 % (2333185)Termination reason: Instruction limit % 10.69/2.15 % (2333185)Termination phase: Saturation % 10.69/2.15 % (2333185)Time elapsed: 0.062 s % 10.69/2.15 % (2333185)Peak memory usage: 89 MB % 10.69/2.15 % (2333185)Instructions burned: 107 (million) % 10.69/2.15 % (2333187)Instruction limit reached! % 10.69/2.15 % (2333187)------------------------------ % 10.69/2.15 % (2333187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.15 % (2333187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.69/2.15 % (2333187)CaDiCaL version: 2.1.3 % 10.69/2.15 % (2333187)Termination reason: Instruction limit % 10.69/2.15 % (2333187)Termination phase: Saturation % 10.69/2.15 % (2333187)Time elapsed: 0.102 s % 10.69/2.15 % (2333187)Peak memory usage: 89 MB % 10.69/2.15 % (2333187)Instructions burned: 180 (million) % 10.69/2.15 % (2333196)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=3471392721:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 10.69/2.15 % (2333197)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3443759134: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) % 10.69/2.15 % (2333188)------------------------------ % 10.69/2.15 % (2333188)------------------------------ % 10.69/2.15 % (2333196)Instruction limit reached! % 10.69/2.15 % (2333196)------------------------------ % 10.69/2.15 % (2333196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.69/2.15 % (2333196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.20/3.05 % (2333196)CaDiCaL version: 2.1.3 % 17.20/3.05 % (2333196)Termination reason: Instruction limit % 17.20/3.05 % (2333196)Termination phase: Saturation % 17.20/3.05 % (2333196)Time elapsed: 0.059 s % 17.20/3.05 % (2333196)Peak memory usage: 89 MB % 17.20/3.05 % (2333196)Instructions burned: 145 (million) % 17.20/3.05 % (2333198)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=776387740:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 17.20/3.05 % (2333197)Instruction limit reached! % 17.20/3.05 % (2333197)------------------------------ % 17.20/3.05 % (2333197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.20/3.05 % (2333197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.20/3.05 % (2333197)CaDiCaL version: 2.1.3 % 17.20/3.05 % (2333197)Termination reason: Instruction limit % 17.20/3.05 % (2333197)Termination phase: Saturation % 17.20/3.05 % (2333197)Time elapsed: 0.076 s % 17.20/3.05 % (2333197)Peak memory usage: 89 MB % 17.20/3.05 % (2333197)Instructions burned: 189 (million) % 17.20/3.05 % (2333202)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1866978395:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 17.20/3.05 % (2333198)Instruction limit reached! % 17.20/3.05 % (2333198)------------------------------ % 17.20/3.05 % (2333198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.20/3.05 % (2333198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.20/3.05 % (2333198)CaDiCaL version: 2.1.3 % 17.20/3.05 % (2333198)Termination reason: Instruction limit % 17.20/3.05 % (2333198)Termination phase: Saturation % 17.20/3.05 % (2333198)Time elapsed: 0.088 s % 17.20/3.05 % (2333198)Peak memory usage: 89 MB % 17.20/3.05 % (2333198)Instructions burned: 219 (million) % 17.20/3.05 % (2333201)lrs+10_64_to=lpo:sil=8000:random_seed=1173143266:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 17.20/3.05 % (2333202)Instruction limit reached! % 17.20/3.05 % (2333202)------------------------------ % 17.20/3.05 % (2333202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.20/3.05 % (2333202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.20/3.05 % (2333202)CaDiCaL version: 2.1.3 % 17.20/3.05 % (2333202)Termination reason: Instruction limit % 17.20/3.05 % (2333202)Termination phase: Saturation % 17.20/3.05 % (2333202)Time elapsed: 0.055 s % 17.20/3.05 % (2333202)Peak memory usage: 90 MB % 17.20/3.05 % (2333202)Instructions burned: 197 (million) % 17.20/3.05 % (2333201)Instruction limit reached! % 17.20/3.05 % (2333201)------------------------------ % 17.20/3.05 % (2333201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.20/3.05 % (2333201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.20/3.05 % (2333201)CaDiCaL version: 2.1.3 % 17.20/3.05 % (2333201)Termination reason: Instruction limit % 17.20/3.05 % (2333201)Termination phase: Saturation % 17.20/3.05 % (2333201)Time elapsed: 0.071 s % 17.20/3.05 % (2333201)Peak memory usage: 89 MB % 17.20/3.05 % (2333201)Instructions burned: 127 (million) % 17.20/3.05 % (2333204)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=279733322:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 17.20/3.05 % (2333207)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1428677291:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 17.20/3.05 % (2333208)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=3648710606:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 17.20/3.05 % (2333204)Instruction limit reached! % 17.20/3.05 % (2333204)------------------------------ % 17.20/3.05 % (2333204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.20/3.05 % (2333204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.20/3.05 % (2333204)CaDiCaL version: 2.1.3 % 17.20/3.05 % (2333204)Termination reason: Instruction limit % 17.20/3.05 % (2333204)Termination phase: Saturation % 17.20/3.05 % (2333204)Time elapsed: 0.086 s % 17.20/3.05 % (2333204)Peak memory usage: 91 MB % 17.20/3.05 % (2333204)Instructions burned: 158 (million) % 17.20/3.05 % (2333208)Instruction limit reached! % 17.20/3.05 % (2333208)------------------------------ % 17.20/3.05 % (2333208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.20/3.05 % (2333208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.00/5.18 % (2333208)CaDiCaL version: 2.1.3 % 32.00/5.18 % (2333208)Termination reason: Instruction limit % 32.00/5.18 % (2333208)Termination phase: Saturation % 32.00/5.18 % (2333208)Time elapsed: 0.025 s % 32.00/5.18 % (2333208)Peak memory usage: 89 MB % 32.00/5.18 % (2333208)Instructions burned: 107 (million) % 32.00/5.18 % (2333209)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2462245041:i=107_2993 on theBenchmark for (2993ds/107Mi) % 32.00/5.18 % (2333209)Instruction limit reached! % 32.00/5.18 % (2333209)------------------------------ % 32.00/5.18 % (2333209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.00/5.18 % (2333209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.00/5.18 % (2333209)CaDiCaL version: 2.1.3 % 32.00/5.18 % (2333209)Termination reason: Instruction limit % 32.00/5.18 % (2333209)Termination phase: Saturation % 32.00/5.18 % (2333209)Time elapsed: 0.044 s % 32.00/5.18 % (2333209)Peak memory usage: 88 MB % 32.00/5.18 % (2333209)Instructions burned: 108 (million) % 32.00/5.18 % (2333214)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3272433765:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi) % 32.00/5.18 % (2333213)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1597455185:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 32.00/5.18 % (2333216)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1787854068:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi) % 32.00/5.18 % (2333213)Instruction limit reached! % 32.00/5.18 % (2333213)------------------------------ % 32.00/5.18 % (2333213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.00/5.18 % (2333213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.00/5.18 % (2333213)CaDiCaL version: 2.1.3 % 32.00/5.18 % (2333213)Termination reason: Instruction limit % 32.00/5.18 % (2333213)Termination phase: Saturation % 32.00/5.18 % (2333213)Time elapsed: 0.129 s % 32.00/5.18 % (2333213)Peak memory usage: 91 MB % 32.00/5.18 % (2333213)Instructions burned: 244 (million) % 32.00/5.18 % (2333216)Instruction limit reached! % 32.00/5.18 % (2333216)------------------------------ % 32.00/5.18 % (2333216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.00/5.18 % (2333216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.00/5.18 % (2333216)CaDiCaL version: 2.1.3 % 32.00/5.18 % (2333216)Termination reason: Instruction limit % 32.00/5.18 % (2333216)Termination phase: Saturation % 32.00/5.18 % (2333216)Time elapsed: 0.079 s % 32.00/5.18 % (2333216)Peak memory usage: 89 MB % 32.00/5.18 % (2333216)Instructions burned: 135 (million) % 32.00/5.18 % (2333220)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=681952832:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi) % 32.00/5.18 % (2333221)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1605991506:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi) % 32.00/5.18 % (2333221)Instruction limit reached! % 32.00/5.18 % (2333221)------------------------------ % 32.00/5.18 % (2333221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.00/5.18 % (2333221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.00/5.18 % (2333221)CaDiCaL version: 2.1.3 % 32.00/5.18 % (2333221)Termination reason: Instruction limit % 32.00/5.18 % (2333221)Termination phase: Saturation % 32.00/5.18 % (2333221)Time elapsed: 0.108 s % 32.00/5.18 % (2333221)Peak memory usage: 90 MB % 32.00/5.18 % (2333221)Instructions burned: 193 (million) % 32.00/5.18 % (2333220)Instruction limit reached! % 32.00/5.18 % (2333220)------------------------------ % 32.00/5.18 % (2333220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.00/5.18 % (2333220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.00/5.18 % (2333220)CaDiCaL version: 2.1.3 % 32.00/5.18 % (2333220)Termination reason: Instruction limit % 32.00/5.18 % (2333220)Termination phase: Saturation % 32.00/5.18 % (2333220)Time elapsed: 0.188 s % 32.00/5.18 % (2333220)Peak memory usage: 91 MB % 32.00/5.18 % (2333220)Instructions burned: 499 (million) % 32.00/5.18 % (2333224)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2602934417:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi) % 46.16/7.16 % (2333225)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=678837952:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi) % 46.16/7.16 % (2333225)Instruction limit reached! % 46.16/7.16 % (2333225)------------------------------ % 46.16/7.16 % (2333225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.16/7.16 % (2333225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.16/7.16 % (2333225)CaDiCaL version: 2.1.3 % 46.16/7.16 % (2333225)Termination reason: Instruction limit % 46.16/7.16 % (2333225)Termination phase: Saturation % 46.16/7.16 % (2333225)Time elapsed: 0.093 s % 46.16/7.16 % (2333225)Peak memory usage: 89 MB % 46.16/7.16 % (2333225)Instructions burned: 156 (million) % 46.16/7.16 % (2333224)Instruction limit reached! % 46.16/7.16 % (2333224)------------------------------ % 46.16/7.16 % (2333224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.16/7.16 % (2333224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.16/7.16 % (2333224)CaDiCaL version: 2.1.3 % 46.16/7.16 % (2333224)Termination reason: Instruction limit % 46.16/7.16 % (2333224)Termination phase: Saturation % 46.16/7.16 % (2333224)Time elapsed: 0.154 s % 46.16/7.16 % (2333224)Peak memory usage: 91 MB % 46.16/7.16 % (2333224)Instructions burned: 266 (million) % 46.16/7.16 % (2333228)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=952836776:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi) % 46.16/7.16 % (2333229)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2145436532:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi) % 46.16/7.16 % (2333207)Instruction limit reached! % 46.16/7.16 % (2333207)------------------------------ % 46.16/7.16 % (2333207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.16/7.16 % (2333207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.16/7.16 % (2333207)CaDiCaL version: 2.1.3 % 46.16/7.16 % (2333207)Termination reason: Instruction limit % 46.16/7.16 % (2333207)Termination phase: Saturation % 46.16/7.16 % (2333207)Time elapsed: 1.242 s % 46.16/7.16 % (2333207)Peak memory usage: 145 MB % 46.16/7.16 % (2333207)Instructions burned: 3398 (million) % 46.16/7.16 % (2333232)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1960167282:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi) % 46.16/7.16 % (2333229)Instruction limit reached! % 46.16/7.16 % (2333229)------------------------------ % 46.16/7.16 % (2333229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.16/7.16 % (2333229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.16/7.16 % (2333229)CaDiCaL version: 2.1.3 % 46.16/7.16 % (2333229)Termination reason: Instruction limit % 46.16/7.16 % (2333229)Termination phase: Saturation % 46.16/7.16 % (2333229)Time elapsed: 0.286 s % 46.16/7.16 % (2333229)Peak memory usage: 93 MB % 46.16/7.16 % (2333229)Instructions burned: 537 (million) % 46.16/7.16 % (2333232)Instruction limit reached! % 46.16/7.16 % (2333232)------------------------------ % 46.16/7.16 % (2333232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.16/7.16 % (2333232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.16/7.16 % (2333232)CaDiCaL version: 2.1.3 % 46.16/7.16 % (2333232)Termination reason: Instruction limit % 46.16/7.16 % (2333232)Termination phase: Saturation % 46.16/7.16 % (2333232)Time elapsed: 0.052 s % 46.16/7.16 % (2333232)Peak memory usage: 89 MB % 46.16/7.16 % (2333232)Instructions burned: 181 (million) % 46.16/7.16 % (2333234)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=2328797597:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/10307Mi) % 46.16/7.16 % (2333235)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=2235116495:i=412:gtgl=4:gtg=exists_all_2978 on theBenchmark for (2978ds/412Mi) % 46.16/7.16 % (2333235)Instruction limit reached! % 46.16/7.16 % (2333235)------------------------------ % 46.16/7.16 % (2333235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.16/7.16 % (2333235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.16/7.16 % (2333235)CaDiCaL version: 2.1.3 % 64.30/9.70 % (2333235)Termination reason: Instruction limit % 64.30/9.70 % (2333235)Termination phase: Saturation % 64.30/9.70 % (2333235)Time elapsed: 0.129 s % 64.30/9.70 % (2333235)Peak memory usage: 95 MB % 64.30/9.70 % (2333235)Instructions burned: 412 (million) % 64.30/9.70 % (2333239)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=3319981258:s2pl=no:i=8478:s2at=4:nm=6_2976 on theBenchmark for (2976ds/8478Mi) % 64.30/9.70 % (2333228)Instruction limit reached! % 64.30/9.70 % (2333228)------------------------------ % 64.30/9.70 % (2333228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.30/9.70 % (2333228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.30/9.70 % (2333228)CaDiCaL version: 2.1.3 % 64.30/9.70 % (2333228)Termination reason: Instruction limit % 64.30/9.70 % (2333228)Termination phase: Saturation % 64.30/9.70 % (2333228)Time elapsed: 1.667 s % 64.30/9.70 % (2333228)Peak memory usage: 148 MB % 64.30/9.70 % (2333228)Instructions burned: 3258 (million) % 64.30/9.70 % (2333241)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=181106041:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2965 on theBenchmark for (2965ds/303Mi) % 64.30/9.70 % (2333241)Refutation not found, incomplete strategy % 64.30/9.70 % (2333241)------------------------------ % 64.30/9.70 % (2333241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.30/9.70 % (2333241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.30/9.70 % (2333241)CaDiCaL version: 2.1.3 % 64.30/9.70 % (2333241)Termination reason: Refutation not found, incomplete strategy % 64.30/9.70 % (2333241)Time elapsed: 0.008 s % 64.30/9.70 % (2333241)Peak memory usage: 88 MB % 64.30/9.70 % (2333241)Instructions burned: 15 (million) % 64.30/9.70 % (2333214)Instruction limit reached! % 64.30/9.70 % (2333214)------------------------------ % 64.30/9.70 % (2333214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.30/9.70 % (2333214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.30/9.70 % (2333214)CaDiCaL version: 2.1.3 % 64.30/9.70 % (2333214)Termination reason: Instruction limit % 64.30/9.70 % (2333214)Termination phase: Saturation % 64.30/9.70 % (2333214)Time elapsed: 2.775 s % 64.30/9.70 % (2333214)Peak memory usage: 168 MB % 64.30/9.70 % (2333214)Instructions burned: 5209 (million) % 64.30/9.70 % (2333243)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2984399418:st=4:i=720:sd=3:fsr=off:ss=axioms_2963 on theBenchmark for (2963ds/720Mi) % 64.30/9.70 % (2333241)------------------------------ % 64.30/9.70 % (2333241)------------------------------ % 64.30/9.70 % (2333245)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1755390125:i=598:bs=on:bd=preordered:av=off:ss=axioms_2961 on theBenchmark for (2961ds/598Mi) % 64.30/9.70 % (2333243)Instruction limit reached! % 64.30/9.70 % (2333243)------------------------------ % 64.30/9.70 % (2333243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.30/9.70 % (2333243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.30/9.70 % (2333243)CaDiCaL version: 2.1.3 % 64.30/9.70 % (2333243)Termination reason: Instruction limit % 64.30/9.70 % (2333243)Termination phase: Saturation % 64.30/9.70 % (2333243)Time elapsed: 0.264 s % 64.30/9.70 % (2333243)Peak memory usage: 90 MB % 64.30/9.70 % (2333243)Instructions burned: 722 (million) % 64.30/9.70 % (2333247)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1709925152:i=2989:sd=3:ss=axioms:sgt=60_2958 on theBenchmark for (2958ds/2989Mi) % 64.30/9.70 % (2333245)Instruction limit reached! % 64.30/9.70 % (2333245)------------------------------ % 64.30/9.70 % (2333245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.30/9.70 % (2333245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.30/9.70 % (2333245)CaDiCaL version: 2.1.3 % 64.30/9.70 % (2333245)Termination reason: Instruction limit % 64.30/9.70 % (2333245)Termination phase: Saturation % 64.30/9.70 % (2333245)Time elapsed: 0.334 s % 64.30/9.70 % (2333245)Peak memory usage: 98 MB % 64.30/9.70 % (2333245)Instructions burned: 598 (million) % 64.30/9.70 % (2333249)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=515618838:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2956 on theBenchmark for (2956ds/1997Mi) % 95.91/14.15 % (2333239)Instruction limit reached! % 95.91/14.15 % (2333239)------------------------------ % 95.91/14.15 % (2333239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.91/14.15 % (2333239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.91/14.15 % (2333239)CaDiCaL version: 2.1.3 % 95.91/14.15 % (2333239)Termination reason: Instruction limit % 95.91/14.15 % (2333239)Termination phase: Saturation % 95.91/14.15 % (2333239)Time elapsed: 3.151 s % 95.91/14.15 % (2333239)Peak memory usage: 187 MB % 95.91/14.15 % (2333239)Instructions burned: 8481 (million) % 95.91/14.15 % (2333249)Instruction limit reached! % 95.91/14.15 % (2333249)------------------------------ % 95.91/14.15 % (2333249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.91/14.15 % (2333249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.91/14.15 % (2333249)CaDiCaL version: 2.1.3 % 95.91/14.15 % (2333249)Termination reason: Instruction limit % 95.91/14.15 % (2333249)Termination phase: Saturation % 95.91/14.15 % (2333249)Time elapsed: 1.272 s % 95.91/14.15 % (2333249)Peak memory usage: 138 MB % 95.91/14.15 % (2333249)Instructions burned: 1997 (million) % 95.91/14.15 % (2333251)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=1986575482:i=2088:bd=preordered:av=off_2943 on theBenchmark for (2943ds/2088Mi) % 95.91/14.15 % (2333247)Instruction limit reached! % 95.91/14.15 % (2333247)------------------------------ % 95.91/14.15 % (2333247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.91/14.15 % (2333247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.91/14.15 % (2333247)CaDiCaL version: 2.1.3 % 95.91/14.15 % (2333247)Termination reason: Instruction limit % 95.91/14.15 % (2333247)Termination phase: Saturation % 95.91/14.15 % (2333247)Time elapsed: 1.662 s % 95.91/14.15 % (2333247)Peak memory usage: 144 MB % 95.91/14.15 % (2333247)Instructions burned: 2989 (million) % 95.91/14.15 % (2333253)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1967425563:i=1098:nicw=on_2942 on theBenchmark for (2942ds/1098Mi) % 95.91/14.15 % (2333254)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2497872855:i=433:bd=preordered_2940 on theBenchmark for (2940ds/433Mi) % 95.91/14.15 % (2333254)Refutation not found, incomplete strategy % 95.91/14.15 % (2333254)------------------------------ % 95.91/14.15 % (2333254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.91/14.15 % (2333254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.91/14.15 % (2333254)CaDiCaL version: 2.1.3 % 95.91/14.15 % (2333254)Termination reason: Refutation not found, incomplete strategy % 95.91/14.15 % (2333254)Time elapsed: 0.004 s % 95.91/14.15 % (2333254)Peak memory usage: 88 MB % 95.91/14.15 % (2333254)Instructions burned: 7 (million) % 95.91/14.15 % (2333254)------------------------------ % 95.91/14.15 % (2333254)------------------------------ % 95.91/14.15 % (2333253)Instruction limit reached! % 95.91/14.15 % (2333253)------------------------------ % 95.91/14.15 % (2333253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.91/14.15 % (2333253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.91/14.15 % (2333253)CaDiCaL version: 2.1.3 % 95.91/14.15 % (2333253)Termination reason: Instruction limit % 95.91/14.15 % (2333253)Termination phase: Saturation % 95.91/14.15 % (2333253)Time elapsed: 0.500 s % 95.91/14.15 % (2333253)Peak memory usage: 103 MB % 95.91/14.15 % (2333253)Instructions burned: 1100 (million) % 95.91/14.15 % (2333251)Instruction limit reached! % 95.91/14.15 % (2333251)------------------------------ % 95.91/14.15 % (2333251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.91/14.15 % (2333251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.91/14.15 % (2333251)CaDiCaL version: 2.1.3 % 95.91/14.15 % (2333251)Termination reason: Instruction limit % 95.91/14.15 % (2333251)Termination phase: Saturation % 95.91/14.15 % (2333251)Time elapsed: 0.687 s % 95.91/14.15 % (2333251)Peak memory usage: 139 MB % 95.91/14.15 % (2333251)Instructions burned: 2092 (million) % 95.91/14.15 % (2333257)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3122553932:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2936 on theBenchmark for (2936ds/2942Mi) % 106.66/15.74 % (2333258)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=127637978:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2935 on theBenchmark for (2935ds/6922Mi) % 106.66/15.74 % (2333259)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=725519004:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2935 on theBenchmark for (2935ds/596Mi) % 106.66/15.74 % (2333259)Refutation not found, incomplete strategy % 106.66/15.74 % (2333259)------------------------------ % 106.66/15.74 % (2333259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.66/15.74 % (2333259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.66/15.74 % (2333259)CaDiCaL version: 2.1.3 % 106.66/15.74 % (2333259)Termination reason: Refutation not found, incomplete strategy % 106.66/15.74 % (2333259)Time elapsed: 0.004 s % 106.66/15.74 % (2333259)Peak memory usage: 88 MB % 106.66/15.74 % (2333259)Instructions burned: 7 (million) % 106.66/15.74 % (2333259)------------------------------ % 106.66/15.74 % (2333259)------------------------------ % 106.66/15.74 % (2333263)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=2628637066:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2931 on theBenchmark for (2931ds/4123Mi) % 106.66/15.74 % (2333234)Instruction limit reached! % 106.66/15.74 % (2333234)------------------------------ % 106.66/15.74 % (2333234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.66/15.74 % (2333234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.66/15.74 % (2333234)CaDiCaL version: 2.1.3 % 106.66/15.74 % (2333234)Termination reason: Instruction limit % 106.66/15.74 % (2333234)Termination phase: Saturation % 106.66/15.74 % (2333234)Time elapsed: 4.722 s % 106.66/15.74 % (2333234)Peak memory usage: 148 MB % 106.66/15.74 % (2333234)Instructions burned: 10308 (million) % 106.66/15.74 % (2333265)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3414881679:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2930 on theBenchmark for (2930ds/16411Mi) % 106.66/15.74 % (2333263)Instruction limit reached! % 106.66/15.74 % (2333263)------------------------------ % 106.66/15.74 % (2333263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.66/15.74 % (2333263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.66/15.74 % (2333263)CaDiCaL version: 2.1.3 % 106.66/15.74 % (2333263)Termination reason: Instruction limit % 106.66/15.74 % (2333263)Termination phase: Saturation % 106.66/15.74 % (2333263)Time elapsed: 1.127 s % 106.66/15.74 % (2333263)Peak memory usage: 142 MB % 106.66/15.74 % (2333263)Instructions burned: 4129 (million) % 106.66/15.74 % (2333267)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3711107828:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2919 on theBenchmark for (2919ds/1670Mi) % 106.66/15.74 % (2333257)Instruction limit reached! % 106.66/15.74 % (2333257)------------------------------ % 106.66/15.74 % (2333257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.66/15.74 % (2333257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.66/15.74 % (2333257)CaDiCaL version: 2.1.3 % 106.66/15.74 % (2333257)Termination reason: Instruction limit % 106.66/15.74 % (2333257)Termination phase: Saturation % 106.66/15.74 % (2333257)Time elapsed: 1.729 s % 106.66/15.74 % (2333257)Peak memory usage: 144 MB % 106.66/15.74 % (2333257)Instructions burned: 2942 (million) % 106.66/15.74 % (2333269)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=3962640484:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2917 on theBenchmark for (2917ds/1722Mi) % 106.66/15.74 % (2333267)Instruction limit reached! % 106.66/15.74 % (2333267)------------------------------ % 106.66/15.74 % (2333267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.66/15.74 % (2333267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.66/15.74 % (2333267)CaDiCaL version: 2.1.3 % 106.66/15.74 % (2333267)Termination reason: Instruction limit % 106.66/15.74 % (2333267)Termination phase: Saturation % 106.66/15.74 % (2333267)Time elapsed: 0.677 s % 106.66/15.74 % (2333267)Peak memory usage: 134 MB % 106.66/15.74 % (2333267)Instructions burned: 1672 (million) % 106.66/15.74 % (2333271)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=3017241512:cts=off:cond=on:i=9530:bs=on:fsd=on_2911 on theBenchmark for (2911ds/9530Mi) % 126.40/18.54 % (2333269)Instruction limit reached! % 126.40/18.54 % (2333269)------------------------------ % 126.40/18.54 % (2333269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.40/18.54 % (2333269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.40/18.54 % (2333269)CaDiCaL version: 2.1.3 % 126.40/18.54 % (2333269)Termination reason: Instruction limit % 126.40/18.54 % (2333269)Termination phase: Saturation % 126.40/18.54 % (2333269)Time elapsed: 0.944 s % 126.40/18.54 % (2333269)Peak memory usage: 129 MB % 126.40/18.54 % (2333269)Instructions burned: 1722 (million) % 126.40/18.54 % (2333273)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=988382848:st=2:i=4495:sd=10:ss=included_2906 on theBenchmark for (2906ds/4495Mi) % 126.40/18.54 % (2333258)Instruction limit reached! % 126.40/18.54 % (2333258)------------------------------ % 126.40/18.54 % (2333258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.40/18.54 % (2333258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.40/18.54 % (2333258)CaDiCaL version: 2.1.3 % 126.40/18.54 % (2333258)Termination reason: Instruction limit % 126.40/18.54 % (2333258)Termination phase: Saturation % 126.40/18.54 % (2333258)Time elapsed: 3.468 s % 126.40/18.54 % (2333258)Peak memory usage: 162 MB % 126.40/18.54 % (2333258)Instructions burned: 6923 (million) % 126.40/18.54 % (2333275)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=3638013390:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2899 on theBenchmark for (2899ds/4920Mi) % 126.40/18.54 % (2333273)Instruction limit reached! % 126.40/18.54 % (2333273)------------------------------ % 126.40/18.54 % (2333273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.40/18.54 % (2333273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.40/18.54 % (2333273)CaDiCaL version: 2.1.3 % 126.40/18.54 % (2333273)Termination reason: Instruction limit % 126.40/18.54 % (2333273)Termination phase: Saturation % 126.40/18.54 % (2333273)Time elapsed: 2.559 s % 126.40/18.54 % (2333273)Peak memory usage: 159 MB % 126.40/18.54 % (2333273)Instructions burned: 4495 (million) % 126.40/18.54 % (2333277)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=259177813:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2878 on theBenchmark for (2878ds/2083Mi) % 126.40/18.54 % (2333271)Instruction limit reached! % 126.40/18.54 % (2333271)------------------------------ % 126.40/18.54 % (2333271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.40/18.54 % (2333271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.40/18.54 % (2333271)CaDiCaL version: 2.1.3 % 126.40/18.54 % (2333271)Termination reason: Instruction limit % 126.40/18.54 % (2333271)Termination phase: Saturation % 126.40/18.54 % (2333271)Time elapsed: 3.378 s % 126.40/18.54 % (2333271)Peak memory usage: 181 MB % 126.40/18.54 % (2333271)Instructions burned: 9531 (million) % 126.40/18.54 % (2333279)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=2315361944:i=4629:av=off:gsp=on_2875 on theBenchmark for (2875ds/4629Mi) % 126.40/18.54 % (2333275)Instruction limit reached! % 126.40/18.54 % (2333275)------------------------------ % 126.40/18.54 % (2333275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.40/18.54 % (2333275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.40/18.54 % (2333275)CaDiCaL version: 2.1.3 % 126.40/18.54 % (2333275)Termination reason: Instruction limit % 126.40/18.54 % (2333275)Termination phase: Saturation % 126.40/18.54 % (2333275)Time elapsed: 2.605 s % 126.40/18.54 % (2333275)Peak memory usage: 162 MB % 126.40/18.54 % (2333275)Instructions burned: 4922 (million) % 126.40/18.54 % (2333281)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=963595092:i=1258:av=off_2871 on theBenchmark for (2871ds/1258Mi) % 126.40/18.54 % (2333277)Instruction limit reached! % 126.40/18.54 % (2333277)------------------------------ % 126.40/18.54 % (2333277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.50/21.69 % (2333277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.50/21.69 % (2333277)CaDiCaL version: 2.1.3 % 148.50/21.69 % (2333277)Termination reason: Instruction limit % 148.50/21.69 % (2333277)Termination phase: Saturation % 148.50/21.69 % (2333277)Time elapsed: 1.214 s % 148.50/21.69 % (2333277)Peak memory usage: 134 MB % 148.50/21.69 % (2333277)Instructions burned: 2084 (million) % 148.50/21.69 % (2333279)Instruction limit reached! % 148.50/21.69 % (2333279)------------------------------ % 148.50/21.69 % (2333279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.50/21.69 % (2333279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.50/21.69 % (2333279)CaDiCaL version: 2.1.3 % 148.50/21.69 % (2333279)Termination reason: Instruction limit % 148.50/21.69 % (2333279)Termination phase: Saturation % 148.50/21.69 % (2333279)Time elapsed: 1.063 s % 148.50/21.69 % (2333279)Peak memory usage: 142 MB % 148.50/21.69 % (2333279)Instructions burned: 4632 (million) % 148.50/21.69 % (2333283)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1815984238:i=7343:av=off:ss=included_2865 on theBenchmark for (2865ds/7343Mi) % 148.50/21.69 % (2333281)Instruction limit reached! % 148.50/21.69 % (2333281)------------------------------ % 148.50/21.69 % (2333281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.50/21.69 % (2333281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.50/21.69 % (2333281)CaDiCaL version: 2.1.3 % 148.50/21.69 % (2333281)Termination reason: Instruction limit % 148.50/21.69 % (2333281)Termination phase: Saturation % 148.50/21.69 % (2333281)Time elapsed: 0.687 s % 148.50/21.69 % (2333281)Peak memory usage: 100 MB % 148.50/21.69 % (2333281)Instructions burned: 1259 (million) % 148.50/21.69 % (2333285)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=4214941884:i=1325:sd=2:ss=axioms:sgt=16_2863 on theBenchmark for (2863ds/1325Mi) % 148.50/21.69 % (2333288)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=4244804261:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2862 on theBenchmark for (2862ds/2646Mi) % 148.50/21.69 % (2333285)Instruction limit reached! % 148.50/21.69 % (2333285)------------------------------ % 148.50/21.69 % (2333285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.50/21.69 % (2333285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.50/21.69 % (2333285)CaDiCaL version: 2.1.3 % 148.50/21.69 % (2333285)Termination reason: Instruction limit % 148.50/21.69 % (2333285)Termination phase: Saturation % 148.50/21.69 % (2333285)Time elapsed: 0.275 s % 148.50/21.69 % (2333285)Peak memory usage: 92 MB % 148.50/21.69 % (2333285)Instructions burned: 1327 (million) % 148.50/21.69 % (2333290)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2957868469:i=1489:sd=2:ep=R:ss=axioms_2859 on theBenchmark for (2859ds/1489Mi) % 148.50/21.69 % (2333290)Refutation not found, incomplete strategy % 148.50/21.69 % (2333290)------------------------------ % 148.50/21.69 % (2333290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.50/21.69 % (2333290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.50/21.69 % (2333290)CaDiCaL version: 2.1.3 % 148.50/21.69 % (2333290)Termination reason: Refutation not found, incomplete strategy % 148.50/21.69 % (2333290)Time elapsed: 0.369 s % 148.50/21.69 % (2333290)Peak memory usage: 128 MB % 148.50/21.69 % (2333290)Instructions burned: 915 (million) % 148.50/21.69 % (2333290)------------------------------ % 148.50/21.69 % (2333290)------------------------------ % 148.50/21.69 % (2333292)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=1276717689:i=1503_2852 on theBenchmark for (2852ds/1503Mi) % 148.50/21.69 % (2333288)Instruction limit reached! % 148.50/21.69 % (2333288)------------------------------ % 148.50/21.69 % (2333288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.50/21.69 % (2333288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.50/21.69 % (2333288)CaDiCaL version: 2.1.3 % 148.50/21.69 % (2333288)Termination reason: Instruction limit % 148.50/21.69 % (2333288)Termination phase: Saturation % 148.50/21.69 % (2333288)Time elapsed: 1.031 s % 148.50/21.69 % (2333288)Peak memory usage: 136 MB % 148.50/21.69 % (2333288)Instructions burned: 2650 (million) % 148.50/21.69 % (2333294)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1231486230:i=13942:kws=frequency_2850 on theBenchmark for (2850ds/13942Mi) % 169.66/24.69 % (2333292)Instruction limit reached! % 169.66/24.69 % (2333292)------------------------------ % 169.66/24.69 % (2333292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.66/24.69 % (2333292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.66/24.69 % (2333292)CaDiCaL version: 2.1.3 % 169.66/24.69 % (2333292)Termination reason: Instruction limit % 169.66/24.69 % (2333292)Termination phase: Saturation % 169.66/24.69 % (2333292)Time elapsed: 0.894 s % 169.66/24.69 % (2333292)Peak memory usage: 135 MB % 169.66/24.69 % (2333292)Instructions burned: 1503 (million) % 169.66/24.69 % (2333296)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=363340241:i=3604:fsr=off:er=filter_2841 on theBenchmark for (2841ds/3604Mi) % 169.66/24.69 % (2333265)Instruction limit reached! % 169.66/24.69 % (2333265)------------------------------ % 169.66/24.69 % (2333265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.66/24.69 % (2333265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.66/24.69 % (2333265)CaDiCaL version: 2.1.3 % 169.66/24.69 % (2333265)Termination reason: Instruction limit % 169.66/24.69 % (2333265)Termination phase: Saturation % 169.66/24.69 % (2333265)Time elapsed: 8.923 s % 169.66/24.69 % (2333265)Peak memory usage: 269 MB % 169.66/24.69 % (2333265)Instructions burned: 16413 (million) % 169.66/24.69 % (2333298)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1069713926:i=1876:sd=1:ss=included:sgt=32_2839 on theBenchmark for (2839ds/1876Mi) % 169.66/24.69 % (2333283)Instruction limit reached! % 169.66/24.69 % (2333283)------------------------------ % 169.66/24.69 % (2333283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.66/24.69 % (2333283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.66/24.69 % (2333283)CaDiCaL version: 2.1.3 % 169.66/24.69 % (2333283)Termination reason: Instruction limit % 169.66/24.69 % (2333283)Termination phase: Saturation % 169.66/24.69 % (2333283)Time elapsed: 3.443 s % 169.66/24.69 % (2333283)Peak memory usage: 173 MB % 169.66/24.69 % (2333283)Instructions burned: 7345 (million) % 169.66/24.69 % (2333300)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1414025449:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2828 on theBenchmark for (2828ds/1932Mi) % 169.66/24.69 % (2333298)Instruction limit reached! % 169.66/24.69 % (2333298)------------------------------ % 169.66/24.69 % (2333298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.66/24.69 % (2333298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.66/24.69 % (2333298)CaDiCaL version: 2.1.3 % 169.66/24.69 % (2333298)Termination reason: Instruction limit % 169.66/24.69 % (2333298)Termination phase: Saturation % 169.66/24.69 % (2333298)Time elapsed: 1.107 s % 169.66/24.69 % (2333298)Peak memory usage: 136 MB % 169.66/24.69 % (2333298)Instructions burned: 1877 (million) % 169.66/24.69 % (2333302)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=2999690063:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2826 on theBenchmark for (2826ds/1980Mi) % 169.66/24.69 % (2333300)Refutation not found, incomplete strategy % 169.66/24.69 % (2333300)------------------------------ % 169.66/24.69 % (2333300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.66/24.69 % (2333300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.66/24.69 % (2333300)CaDiCaL version: 2.1.3 % 169.66/24.69 % (2333300)Termination reason: Refutation not found, incomplete strategy % 169.66/24.69 % (2333300)Time elapsed: 0.585 s % 169.66/24.69 % (2333300)Peak memory usage: 128 MB % 169.66/24.69 % (2333300)Instructions burned: 891 (million) % 169.66/24.69 % (2333296)Instruction limit reached! % 169.66/24.69 % (2333296)------------------------------ % 169.66/24.69 % (2333296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.66/24.69 % (2333296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.66/24.69 % (2333296)CaDiCaL version: 2.1.3 % 169.66/24.69 % (2333296)Termination reason: Instruction limit % 169.66/24.69 % (2333296)Termination phase: Saturation % 169.66/24.69 % (2333296)Time elapsed: 1.886 s % 169.66/24.69 % (2333296)Peak memory usage: 132 MB % 188.01/27.18 % (2333296)Instructions burned: 3605 (million) % 188.01/27.18 % (2333304)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=3665746680:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2821 on theBenchmark for (2821ds/3902Mi) % 188.01/27.18 % (2333300)------------------------------ % 188.01/27.18 % (2333300)------------------------------ % 188.01/27.18 % (2333306)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1532060931:avsq=on:i=3916:aac=none:amm=off_2818 on theBenchmark for (2818ds/3916Mi) % 188.01/27.18 % (2333302)Instruction limit reached! % 188.01/27.18 % (2333302)------------------------------ % 188.01/27.18 % (2333302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.01/27.18 % (2333302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.01/27.18 % (2333302)CaDiCaL version: 2.1.3 % 188.01/27.18 % (2333302)Termination reason: Instruction limit % 188.01/27.18 % (2333302)Termination phase: Saturation % 188.01/27.18 % (2333302)Time elapsed: 1.158 s % 188.01/27.18 % (2333302)Peak memory usage: 137 MB % 188.01/27.18 % (2333302)Instructions burned: 1982 (million) % 188.01/27.18 % (2333308)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=611026903:cond=on:i=3940:av=off:er=known_2813 on theBenchmark for (2813ds/3940Mi) % 188.01/27.18 % (2333294)Instruction limit reached! % 188.01/27.18 % (2333294)------------------------------ % 188.01/27.18 % (2333294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.01/27.18 % (2333294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.01/27.18 % (2333294)CaDiCaL version: 2.1.3 % 188.01/27.18 % (2333294)Termination reason: Instruction limit % 188.01/27.18 % (2333294)Termination phase: Saturation % 188.01/27.18 % (2333294)Time elapsed: 4.574 s % 188.01/27.18 % (2333294)Peak memory usage: 239 MB % 188.01/27.18 % (2333294)Instructions burned: 13943 (million) % 188.01/27.18 % (2333310)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=919879610:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2803 on theBenchmark for (2803ds/3980Mi) % 188.01/27.18 % (2333304)Instruction limit reached! % 188.01/27.18 % (2333304)------------------------------ % 188.01/27.18 % (2333304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.01/27.18 % (2333304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.01/27.18 % (2333304)CaDiCaL version: 2.1.3 % 188.01/27.18 % (2333304)Termination reason: Instruction limit % 188.01/27.18 % (2333304)Termination phase: Saturation % 188.01/27.18 % (2333304)Time elapsed: 2.136 s % 188.01/27.18 % (2333304)Peak memory usage: 148 MB % 188.01/27.18 % (2333304)Instructions burned: 3904 (million) % 188.01/27.18 % (2333312)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=1054076668:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2797 on theBenchmark for (2797ds/2087Mi) % 188.01/27.18 % (2333306)Instruction limit reached! % 188.01/27.18 % (2333306)------------------------------ % 188.01/27.18 % (2333306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.01/27.18 % (2333306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.01/27.18 % (2333306)CaDiCaL version: 2.1.3 % 188.01/27.18 % (2333306)Termination reason: Instruction limit % 188.01/27.18 % (2333306)Termination phase: Saturation % 188.01/27.18 % (2333306)Time elapsed: 2.296 s % 188.01/27.18 % (2333306)Peak memory usage: 121 MB % 188.01/27.18 % (2333306)Instructions burned: 3916 (million) % 188.01/27.18 % (2333314)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=491205108:cts=off:cond=on:i=4272:bs=on:fsd=on_2794 on theBenchmark for (2794ds/4272Mi) % 188.01/27.18 % (2333310)Instruction limit reached! % 188.01/27.18 % (2333310)------------------------------ % 188.01/27.18 % (2333310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.01/27.18 % (2333310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.01/27.18 % (2333310)CaDiCaL version: 2.1.3 % 188.01/27.18 % (2333310)Termination reason: Instruction limit % 188.01/27.18 % (2333310)Termination phase: Saturation % 188.01/27.18 % (2333310)Time elapsed: 1.234 s % 188.01/27.18 % (2333310)Peak memory usage: 158 MB % 256.55/36.89 % (2333310)Instructions burned: 3981 (million) % 256.55/36.89 % (2333308)Instruction limit reached! % 256.55/36.89 % (2333308)------------------------------ % 256.55/36.89 % (2333308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.55/36.89 % (2333308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.55/36.89 % (2333308)CaDiCaL version: 2.1.3 % 256.55/36.89 % (2333308)Termination reason: Instruction limit % 256.55/36.89 % (2333308)Termination phase: Saturation % 256.55/36.89 % (2333308)Time elapsed: 2.289 s % 256.55/36.89 % (2333308)Peak memory usage: 153 MB % 256.55/36.89 % (2333308)Instructions burned: 3941 (million) % 256.55/36.89 % (2333316)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2637911131:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2789 on theBenchmark for (2789ds/2197Mi) % 256.55/36.89 % (2333317)dis+21_1_sil=8000:spb=goal_then_units:random_seed=3855225238:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2788 on theBenchmark for (2788ds/6508Mi) % 256.55/36.89 % (2333312)Instruction limit reached! % 256.55/36.89 % (2333312)------------------------------ % 256.55/36.89 % (2333312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.55/36.89 % (2333312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.55/36.89 % (2333312)CaDiCaL version: 2.1.3 % 256.55/36.89 % (2333312)Termination reason: Instruction limit % 256.55/36.89 % (2333312)Termination phase: Saturation % 256.55/36.89 % (2333312)Time elapsed: 1.296 s % 256.55/36.89 % (2333312)Peak memory usage: 138 MB % 256.55/36.89 % (2333312)Instructions burned: 2089 (million) % 256.55/36.89 % (2333316)Instruction limit reached! % 256.55/36.89 % (2333316)------------------------------ % 256.55/36.89 % (2333316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.55/36.89 % (2333316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.55/36.89 % (2333316)CaDiCaL version: 2.1.3 % 256.55/36.89 % (2333316)Termination reason: Instruction limit % 256.55/36.89 % (2333316)Termination phase: Saturation % 256.55/36.89 % (2333316)Time elapsed: 0.649 s % 256.55/36.89 % (2333316)Peak memory usage: 166 MB % 256.55/36.89 % (2333316)Instructions burned: 2203 (million) % 256.55/36.89 % (2333320)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=822992773:i=2330:fgj=on:av=off:fsr=off_2783 on theBenchmark for (2783ds/2330Mi) % 256.55/36.89 % (2333321)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=4150554760:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2781 on theBenchmark for (2781ds/7592Mi) % 256.55/36.89 % (2333320)Instruction limit reached! % 256.55/36.89 % (2333320)------------------------------ % 256.55/36.89 % (2333320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.55/36.89 % (2333320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.55/36.89 % (2333320)CaDiCaL version: 2.1.3 % 256.55/36.89 % (2333320)Termination reason: Instruction limit % 256.55/36.89 % (2333320)Termination phase: Saturation % 256.55/36.89 % (2333320)Time elapsed: 1.340 s % 256.55/36.89 % (2333320)Peak memory usage: 139 MB % 256.55/36.89 % (2333320)Instructions burned: 2331 (million) % 256.55/36.89 % (2333324)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=1830050333:i=2693:kws=precedence:ins=1:av=off_2767 on theBenchmark for (2767ds/2693Mi) % 256.55/36.89 % (2333314)Instruction limit reached! % 256.55/36.89 % (2333314)------------------------------ % 256.55/36.89 % (2333314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.55/36.89 % (2333314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.55/36.89 % (2333314)CaDiCaL version: 2.1.3 % 256.55/36.89 % (2333314)Termination reason: Instruction limit % 256.55/36.89 % (2333314)Termination phase: Saturation % 256.55/36.89 % (2333314)Time elapsed: 2.685 s % 256.55/36.89 % (2333314)Peak memory usage: 142 MB % 256.55/36.89 % (2333314)Instructions burned: 4273 (million) % 256.55/36.89 % (2333326)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=1480968329:i=28651:sd=4:ss=included:sgt=64_2765 on theBenchmark for (2765ds/28651Mi) % 256.55/36.89 % (2333321)Instruction limit reached! % 256.55/36.89 % (2333321)------------------------------ % 256.55/36.89 % (2333321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.55/36.89 % (2333321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.67 % (2333321)CaDiCaL version: 2.1.3 % 297.27/42.67 % (2333321)Termination reason: Instruction limit % 297.27/42.67 % (2333321)Termination phase: Saturation % 297.27/42.67 % (2333321)Time elapsed: 2.096 s % 297.27/42.67 % (2333321)Peak memory usage: 131 MB % 297.27/42.67 % (2333321)Instructions burned: 7593 (million) % 297.27/42.67 % (2333317)Instruction limit reached! % 297.27/42.67 % (2333317)------------------------------ % 297.27/42.67 % (2333317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.67 % (2333317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.67 % (2333317)CaDiCaL version: 2.1.3 % 297.27/42.67 % (2333317)Termination reason: Instruction limit % 297.27/42.67 % (2333317)Termination phase: Saturation % 297.27/42.67 % (2333317)Time elapsed: 2.835 s % 297.27/42.67 % (2333317)Peak memory usage: 107 MB % 297.27/42.67 % (2333317)Instructions burned: 6508 (million) % 297.27/42.67 % (2333328)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=3179854853:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2759 on theBenchmark for (2759ds/2700Mi) % 297.27/42.67 % (2333329)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=1853347176:i=3196:nm=4_2758 on theBenchmark for (2758ds/3196Mi) % 297.27/42.67 % (2333324)Instruction limit reached! % 297.27/42.67 % (2333324)------------------------------ % 297.27/42.67 % (2333324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.67 % (2333324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.67 % (2333324)CaDiCaL version: 2.1.3 % 297.27/42.67 % (2333324)Termination reason: Instruction limit % 297.27/42.67 % (2333324)Termination phase: Saturation % 297.27/42.67 % (2333324)Time elapsed: 1.624 s % 297.27/42.67 % (2333324)Peak memory usage: 148 MB % 297.27/42.67 % (2333324)Instructions burned: 2695 (million) % 297.27/42.67 % (2333328)Instruction limit reached! % 297.27/42.67 % (2333328)------------------------------ % 297.27/42.67 % (2333328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.67 % (2333328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.67 % (2333328)CaDiCaL version: 2.1.3 % 297.27/42.67 % (2333328)Termination reason: Instruction limit % 297.27/42.67 % (2333328)Termination phase: Saturation % 297.27/42.67 % (2333328)Time elapsed: 0.928 s % 297.27/42.67 % (2333328)Peak memory usage: 141 MB % 297.27/42.67 % (2333328)Instructions burned: 2704 (million) % 297.27/42.67 % (2333332)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=1008560730:cts=off:i=3254:av=off_2749 on theBenchmark for (2749ds/3254Mi) % 297.27/42.67 % (2333333)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=1119917282:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2749 on theBenchmark for (2749ds/3264Mi) % 297.27/42.67 % (2333329)Instruction limit reached! % 297.27/42.67 % (2333329)------------------------------ % 297.27/42.67 % (2333329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.67 % (2333329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.67 % (2333329)CaDiCaL version: 2.1.3 % 297.27/42.67 % (2333329)Termination reason: Instruction limit % 297.27/42.67 % (2333329)Termination phase: Saturation % 297.27/42.67 % (2333329)Time elapsed: 1.782 s % 297.27/42.67 % (2333329)Peak memory usage: 148 MB % 297.27/42.67 % (2333329)Instructions burned: 3197 (million) % 297.27/42.67 % (2333336)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=1890202785:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2738 on theBenchmark for (2738ds/9708Mi) % 297.27/42.67 % (2333333)Instruction limit reached! % 297.27/42.67 % (2333333)------------------------------ % 297.27/42.67 % (2333333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.27/42.67 % (2333333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.27/42.67 % (2333333)CaDiCaL version: 2.1.3 % 297.27/42.67 % (2333333)Termination reason: Instruction limit % 297.27/42.67 % (2333333)Termination phase: Saturation % 297.27/42.67 % (2333333)Time elapsed: 1.167 s % 297.27/42.67 % (2333333)Peak memory usage: 146 MB % 297.27/42.67 % (2333333)Instructions burned: 3264 (million) % 297.27/42.67 % (2333338)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3188409026:i=21997:Terminated %------------------------------------------------------------------------------