%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV946-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n002.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:19:50 PM UTC 2026 % Result : Timeout 290.01s 41.83s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV946-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.26 % Computer : n002.cluster.edu % 0.10/0.26 % Model : x86_64 x86_64 % 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.26 % Memory : 8046.5625MB % 0.10/0.26 % OS : Linux 6.8.0-71-generic % 0.10/0.26 % CPULimit : 300 % 0.10/0.26 % WCLimit : 300 % 0.10/0.26 % DateTime : Mon Sep 28 13:01:37 UTC 2026 % 0.10/0.27 % CPUTime : % 0.10/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.26/0.32 Running first-order theorem proving % 0.26/0.32 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 % 17.11/3.39 % (333537)Input is clausal, will run a generic CNF schedule. % 17.11/3.39 % (333545)lrs+10_1_sil=8000:sp=occurrence:random_seed=296226785:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 17.11/3.39 % (333548)dis-21_1_sil=8000:lcm=predicate:random_seed=3157038042: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) % 17.11/3.39 % (333545)Instruction limit reached! % 17.11/3.39 % (333545)------------------------------ % 17.11/3.39 % (333545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.11/3.39 % (333545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.11/3.39 % (333545)CaDiCaL version: 2.1.3 % 17.11/3.39 % (333545)Termination reason: Instruction limit % 17.11/3.39 % (333545)Termination phase: Saturation % 17.11/3.39 % (333545)Time elapsed: 0.052 s % 17.11/3.39 % (333545)Peak memory usage: 89 MB % 17.11/3.39 % (333545)Instructions burned: 107 (million) % 17.11/3.39 % (333548)Instruction limit reached! % 17.11/3.39 % (333548)------------------------------ % 17.11/3.39 % (333548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.11/3.39 % (333548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.11/3.39 % (333548)CaDiCaL version: 2.1.3 % 17.11/3.39 % (333548)Termination reason: Instruction limit % 17.11/3.39 % (333548)Termination phase: Saturation % 17.11/3.39 % (333548)Time elapsed: 0.070 s % 17.11/3.39 % (333548)Peak memory usage: 88 MB % 17.11/3.39 % (333548)Instructions burned: 117 (million) % 17.11/3.39 % (333542)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=3584662199:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 17.11/3.39 % (333547)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2741619135:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 17.11/3.39 % (333546)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2689887671:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 17.11/3.39 % (333543)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3554087217:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 17.11/3.39 % (333544)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=235099763:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 17.11/3.39 % (333546)Instruction limit reached! % 17.11/3.39 % (333546)------------------------------ % 17.11/3.39 % (333546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.11/3.39 % (333546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.11/3.39 % (333546)CaDiCaL version: 2.1.3 % 17.11/3.39 % (333546)Termination reason: Instruction limit % 17.11/3.39 % (333546)Termination phase: Saturation % 17.11/3.39 % (333546)Time elapsed: 0.098 s % 17.11/3.39 % (333546)Peak memory usage: 88 MB % 17.11/3.39 % (333546)Instructions burned: 114 (million) % 17.11/3.39 % (333547)Instruction limit reached! % 17.11/3.39 % (333547)------------------------------ % 17.11/3.39 % (333547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.11/3.39 % (333547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.11/3.39 % (333547)CaDiCaL version: 2.1.3 % 17.11/3.39 % (333547)Termination reason: Instruction limit % 17.11/3.39 % (333547)Termination phase: Saturation % 17.11/3.39 % (333547)Time elapsed: 0.170 s % 17.11/3.39 % (333547)Peak memory usage: 90 MB % 17.11/3.39 % (333547)Instructions burned: 181 (million) % 17.11/3.39 % (333552)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2710735282: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) % 17.11/3.39 % (333551)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=3333260947:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 17.11/3.39 % (333551)Refutation not found, incomplete strategy % 17.11/3.39 % (333551)------------------------------ % 17.11/3.39 % (333551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.11/3.39 % (333551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.11/3.39 % (333551)CaDiCaL version: 2.1.3 % 17.11/3.39 % (333551)Termination reason: Refutation not found, incomplete strategy % 30.82/5.25 % (333551)Time elapsed: 0.004 s % 30.82/5.25 % (333551)Peak memory usage: 88 MB % 30.82/5.25 % (333551)Instructions burned: 6 (million) % 30.82/5.25 % (333559)lrs+10_64_to=lpo:sil=8000:random_seed=737228781:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 30.82/5.25 % (333558)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2629641813:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi) % 30.82/5.25 % (333552)Instruction limit reached! % 30.82/5.25 % (333552)------------------------------ % 30.82/5.25 % (333552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.82/5.25 % (333552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/5.25 % (333552)CaDiCaL version: 2.1.3 % 30.82/5.25 % (333552)Termination reason: Instruction limit % 30.82/5.25 % (333552)Termination phase: Saturation % 30.82/5.25 % (333552)Time elapsed: 0.174 s % 30.82/5.25 % (333552)Peak memory usage: 91 MB % 30.82/5.25 % (333552)Instructions burned: 189 (million) % 30.82/5.25 % (333551)------------------------------ % 30.82/5.25 % (333551)------------------------------ % 30.82/5.25 % (333559)Instruction limit reached! % 30.82/5.25 % (333559)------------------------------ % 30.82/5.25 % (333559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.82/5.25 % (333559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/5.25 % (333559)CaDiCaL version: 2.1.3 % 30.82/5.25 % (333559)Termination reason: Instruction limit % 30.82/5.25 % (333559)Termination phase: Saturation % 30.82/5.25 % (333559)Time elapsed: 0.123 s % 30.82/5.25 % (333559)Peak memory usage: 89 MB % 30.82/5.25 % (333559)Instructions burned: 127 (million) % 30.82/5.25 % (333558)Instruction limit reached! % 30.82/5.25 % (333558)------------------------------ % 30.82/5.25 % (333558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.82/5.25 % (333558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/5.25 % (333558)CaDiCaL version: 2.1.3 % 30.82/5.25 % (333558)Termination reason: Instruction limit % 30.82/5.25 % (333558)Termination phase: Saturation % 30.82/5.25 % (333558)Time elapsed: 0.199 s % 30.82/5.25 % (333558)Peak memory usage: 89 MB % 30.82/5.25 % (333558)Instructions burned: 219 (million) % 30.82/5.25 % (333564)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4223584781:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi) % 30.82/5.25 % (333564)Instruction limit reached! % 30.82/5.25 % (333564)------------------------------ % 30.82/5.25 % (333564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.82/5.25 % (333564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/5.25 % (333564)CaDiCaL version: 2.1.3 % 30.82/5.25 % (333564)Termination reason: Instruction limit % 30.82/5.25 % (333564)Termination phase: Saturation % 30.82/5.25 % (333564)Time elapsed: 0.116 s % 30.82/5.25 % (333564)Peak memory usage: 90 MB % 30.82/5.25 % (333564)Instructions burned: 195 (million) % 30.82/5.25 % (333565)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2227853986:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi) % 30.82/5.25 % (333566)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2166289549:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi) % 30.82/5.25 % (333568)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=4168301995:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi) % 30.82/5.25 % (333565)Instruction limit reached! % 30.82/5.25 % (333565)------------------------------ % 30.82/5.25 % (333565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.82/5.25 % (333565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.82/5.25 % (333565)CaDiCaL version: 2.1.3 % 30.82/5.25 % (333565)Termination reason: Instruction limit % 30.82/5.25 % (333565)Termination phase: Saturation % 30.82/5.25 % (333565)Time elapsed: 0.157 s % 30.82/5.25 % (333565)Peak memory usage: 91 MB % 30.82/5.25 % (333565)Instructions burned: 157 (million) % 30.82/5.25 % (333569)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=875626154:i=107_2990 on theBenchmark for (2990ds/107Mi) % 30.82/5.25 % (333569)Refutation not found, incomplete strategy % 30.82/5.25 % (333569)------------------------------ % 30.82/5.25 % (333569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.63/8.20 % (333569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.63/8.20 % (333569)CaDiCaL version: 2.1.3 % 51.63/8.20 % (333569)Termination reason: Refutation not found, incomplete strategy % 51.63/8.20 % (333569)Time elapsed: 0.007 s % 51.63/8.20 % (333569)Peak memory usage: 88 MB % 51.63/8.20 % (333569)Instructions burned: 11 (million) % 51.63/8.20 % (333568)Instruction limit reached! % 51.63/8.20 % (333568)------------------------------ % 51.63/8.20 % (333568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.63/8.20 % (333568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.63/8.20 % (333568)CaDiCaL version: 2.1.3 % 51.63/8.20 % (333568)Termination reason: Instruction limit % 51.63/8.20 % (333568)Termination phase: Saturation % 51.63/8.20 % (333568)Time elapsed: 0.090 s % 51.63/8.20 % (333568)Peak memory usage: 89 MB % 51.63/8.20 % (333568)Instructions burned: 106 (million) % 51.63/8.20 % (333573)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2863861176:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi) % 51.63/8.20 % (333569)------------------------------ % 51.63/8.20 % (333569)------------------------------ % 51.63/8.20 % (333575)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3474692744:cond=fast:i=5208:av=off_2988 on theBenchmark for (2988ds/5208Mi) % 51.63/8.20 % (333573)Instruction limit reached! % 51.63/8.20 % (333573)------------------------------ % 51.63/8.20 % (333573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.63/8.20 % (333573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.63/8.20 % (333573)CaDiCaL version: 2.1.3 % 51.63/8.20 % (333573)Termination reason: Instruction limit % 51.63/8.20 % (333573)Termination phase: Saturation % 51.63/8.20 % (333573)Time elapsed: 0.165 s % 51.63/8.20 % (333573)Peak memory usage: 91 MB % 51.63/8.20 % (333573)Instructions burned: 242 (million) % 51.63/8.20 % (333577)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=998975982:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi) % 51.63/8.20 % (333579)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=631088668:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi) % 51.63/8.20 % (333577)Instruction limit reached! % 51.63/8.20 % (333577)------------------------------ % 51.63/8.20 % (333577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.63/8.20 % (333577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.63/8.20 % (333577)CaDiCaL version: 2.1.3 % 51.63/8.20 % (333577)Termination reason: Instruction limit % 51.63/8.20 % (333577)Termination phase: Saturation % 51.63/8.20 % (333577)Time elapsed: 0.096 s % 51.63/8.20 % (333577)Peak memory usage: 88 MB % 51.63/8.20 % (333577)Instructions burned: 135 (million) % 51.63/8.20 % (333582)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=672225895:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi) % 51.63/8.20 % (333579)Instruction limit reached! % 51.63/8.20 % (333579)------------------------------ % 51.63/8.20 % (333579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.63/8.20 % (333579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.63/8.20 % (333579)CaDiCaL version: 2.1.3 % 51.63/8.20 % (333579)Termination reason: Instruction limit % 51.63/8.20 % (333579)Termination phase: Saturation % 51.63/8.20 % (333579)Time elapsed: 0.443 s % 51.63/8.20 % (333579)Peak memory usage: 94 MB % 51.63/8.20 % (333579)Instructions burned: 499 (million) % 51.63/8.20 % (333582)Instruction limit reached! % 51.63/8.20 % (333582)------------------------------ % 51.63/8.20 % (333582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.63/8.20 % (333582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.63/8.20 % (333582)CaDiCaL version: 2.1.3 % 51.63/8.20 % (333582)Termination reason: Instruction limit % 51.63/8.20 % (333582)Termination phase: Saturation % 51.63/8.20 % (333582)Time elapsed: 0.171 s % 51.63/8.20 % (333582)Peak memory usage: 90 MB % 51.63/8.20 % (333582)Instructions burned: 192 (million) % 51.63/8.20 % (333588)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2459839835:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi) % 51.63/8.20 % (333591)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2827917825:cond=on:i=156:bs=on:gtg=exists_all:er=known_2977 on theBenchmark for (2977ds/156Mi) % 78.19/12.05 % (333591)Instruction limit reached! % 78.19/12.05 % (333591)------------------------------ % 78.19/12.05 % (333591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.19/12.05 % (333591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.19/12.05 % (333591)CaDiCaL version: 2.1.3 % 78.19/12.05 % (333591)Termination reason: Instruction limit % 78.19/12.05 % (333591)Termination phase: Saturation % 78.19/12.05 % (333591)Time elapsed: 0.089 s % 78.19/12.05 % (333591)Peak memory usage: 88 MB % 78.19/12.05 % (333591)Instructions burned: 157 (million) % 78.19/12.05 % (333588)Instruction limit reached! % 78.19/12.05 % (333588)------------------------------ % 78.19/12.05 % (333588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.19/12.05 % (333588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.19/12.05 % (333588)CaDiCaL version: 2.1.3 % 78.19/12.05 % (333588)Termination reason: Instruction limit % 78.19/12.05 % (333588)Termination phase: Saturation % 78.19/12.05 % (333588)Time elapsed: 0.181 s % 78.19/12.05 % (333588)Peak memory usage: 88 MB % 78.19/12.05 % (333588)Instructions burned: 265 (million) % 78.19/12.05 % (333600)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=4196164892:i=3256:kws=precedence:bd=preordered:av=off_2974 on theBenchmark for (2974ds/3256Mi) % 78.19/12.05 % (333601)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3086876211:i=537:av=off:ss=included_2973 on theBenchmark for (2973ds/537Mi) % 78.19/12.05 % (333601)Instruction limit reached! % 78.19/12.05 % (333601)------------------------------ % 78.19/12.05 % (333601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.19/12.05 % (333601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.19/12.05 % (333601)CaDiCaL version: 2.1.3 % 78.19/12.05 % (333601)Termination reason: Instruction limit % 78.19/12.05 % (333601)Termination phase: Saturation % 78.19/12.05 % (333601)Time elapsed: 0.390 s % 78.19/12.05 % (333601)Peak memory usage: 88 MB % 78.19/12.05 % (333601)Instructions burned: 537 (million) % 78.19/12.05 % (333604)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1038439963:i=180:bd=preordered:av=off_2966 on theBenchmark for (2966ds/180Mi) % 78.19/12.05 % (333604)Instruction limit reached! % 78.19/12.05 % (333604)------------------------------ % 78.19/12.05 % (333604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.19/12.05 % (333604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.19/12.05 % (333604)CaDiCaL version: 2.1.3 % 78.19/12.05 % (333604)Termination reason: Instruction limit % 78.19/12.05 % (333604)Termination phase: Saturation % 78.19/12.05 % (333604)Time elapsed: 0.147 s % 78.19/12.05 % (333604)Peak memory usage: 90 MB % 78.19/12.05 % (333604)Instructions burned: 180 (million) % 78.19/12.05 % (333575)Instruction limit reached! % 78.19/12.05 % (333575)------------------------------ % 78.19/12.05 % (333575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.19/12.05 % (333575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.19/12.05 % (333575)CaDiCaL version: 2.1.3 % 78.19/12.05 % (333575)Termination reason: Instruction limit % 78.19/12.05 % (333575)Termination phase: Saturation % 78.19/12.05 % (333575)Time elapsed: 2.452 s % 78.19/12.05 % (333575)Peak memory usage: 165 MB % 78.19/12.05 % (333575)Instructions burned: 5212 (million) % 78.19/12.05 % (333609)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=3976649257:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2963 on theBenchmark for (2963ds/10307Mi) % 78.19/12.05 % (333610)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=3855744210:i=412:gtgl=4:gtg=exists_all_2960 on theBenchmark for (2960ds/412Mi) % 78.19/12.05 % (333566)Instruction limit reached! % 78.19/12.05 % (333566)------------------------------ % 78.19/12.05 % (333566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.19/12.05 % (333566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.19/12.05 % (333566)CaDiCaL version: 2.1.3 % 78.19/12.05 % (333566)Termination reason: Instruction limit % 78.19/12.05 % (333566)Termination phase: Saturation % 78.19/12.05 % (333566)Time elapsed: 3.317 s % 78.19/12.05 % (333566)Peak memory usage: 151 MB % 103.92/15.67 % (333566)Instructions burned: 3394 (million) % 103.92/15.67 % (333610)Instruction limit reached! % 103.92/15.67 % (333610)------------------------------ % 103.92/15.67 % (333610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.92/15.67 % (333610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.92/15.67 % (333610)CaDiCaL version: 2.1.3 % 103.92/15.67 % (333610)Termination reason: Instruction limit % 103.92/15.67 % (333610)Termination phase: Saturation % 103.92/15.67 % (333610)Time elapsed: 0.356 s % 103.92/15.67 % (333610)Peak memory usage: 92 MB % 103.92/15.67 % (333610)Instructions burned: 412 (million) % 103.92/15.67 % (333613)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=1660859075:s2pl=no:i=8478:s2at=4:nm=6_2956 on theBenchmark for (2956ds/8478Mi) % 103.92/15.67 % (333614)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=274641655:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2954 on theBenchmark for (2954ds/303Mi) % 103.92/15.67 % (333600)Instruction limit reached! % 103.92/15.67 % (333600)------------------------------ % 103.92/15.67 % (333600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.92/15.67 % (333600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.92/15.67 % (333600)CaDiCaL version: 2.1.3 % 103.92/15.67 % (333600)Termination reason: Instruction limit % 103.92/15.67 % (333600)Termination phase: Saturation % 103.92/15.67 % (333600)Time elapsed: 2.097 s % 103.92/15.67 % (333600)Peak memory usage: 152 MB % 103.92/15.67 % (333600)Instructions burned: 3258 (million) % 103.92/15.67 % (333614)Instruction limit reached! % 103.92/15.67 % (333614)------------------------------ % 103.92/15.67 % (333614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.92/15.67 % (333614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.92/15.67 % (333614)CaDiCaL version: 2.1.3 % 103.92/15.67 % (333614)Termination reason: Instruction limit % 103.92/15.67 % (333614)Termination phase: Saturation % 103.92/15.67 % (333614)Time elapsed: 0.269 s % 103.92/15.67 % (333614)Peak memory usage: 91 MB % 103.92/15.67 % (333614)Instructions burned: 303 (million) % 103.92/15.67 % (333617)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3494289962:st=4:i=720:sd=3:fsr=off:ss=axioms_2950 on theBenchmark for (2950ds/720Mi) % 103.92/15.67 % (333618)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=390830433:i=598:bs=on:bd=preordered:av=off:ss=axioms_2949 on theBenchmark for (2949ds/598Mi) % 103.92/15.67 % (333618)Instruction limit reached! % 103.92/15.67 % (333618)------------------------------ % 103.92/15.67 % (333618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.92/15.67 % (333618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.92/15.67 % (333618)CaDiCaL version: 2.1.3 % 103.92/15.67 % (333618)Termination reason: Instruction limit % 103.92/15.67 % (333618)Termination phase: Saturation % 103.92/15.67 % (333618)Time elapsed: 0.247 s % 103.92/15.67 % (333618)Peak memory usage: 93 MB % 103.92/15.67 % (333618)Instructions burned: 598 (million) % 103.92/15.67 % (333621)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2792856047:i=2989:sd=3:ss=axioms:sgt=60_2944 on theBenchmark for (2944ds/2989Mi) % 103.92/15.67 % (333617)Instruction limit reached! % 103.92/15.67 % (333617)------------------------------ % 103.92/15.67 % (333617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.92/15.67 % (333617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.92/15.67 % (333617)CaDiCaL version: 2.1.3 % 103.92/15.67 % (333617)Termination reason: Instruction limit % 103.92/15.67 % (333617)Termination phase: Saturation % 103.92/15.67 % (333617)Time elapsed: 0.640 s % 103.92/15.67 % (333617)Peak memory usage: 100 MB % 103.92/15.67 % (333617)Instructions burned: 720 (million) % 103.92/15.67 % (333623)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=3086931973:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2942 on theBenchmark for (2942ds/1997Mi) % 103.92/15.67 % (333621)Instruction limit reached! % 103.92/15.67 % (333621)------------------------------ % 103.92/15.67 % (333621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.92/15.67 % (333621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.29/19.70 % (333621)CaDiCaL version: 2.1.3 % 133.29/19.70 % (333621)Termination reason: Instruction limit % 133.29/19.70 % (333621)Termination phase: Saturation % 133.29/19.70 % (333621)Time elapsed: 1.533 s % 133.29/19.70 % (333621)Peak memory usage: 144 MB % 133.29/19.70 % (333621)Instructions burned: 2990 (million) % 133.29/19.70 % (333625)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=975926985:i=2088:bd=preordered:av=off_2927 on theBenchmark for (2927ds/2088Mi) % 133.29/19.70 % (333623)Instruction limit reached! % 133.29/19.70 % (333623)------------------------------ % 133.29/19.70 % (333623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.29/19.70 % (333623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.29/19.70 % (333623)CaDiCaL version: 2.1.3 % 133.29/19.70 % (333623)Termination reason: Instruction limit % 133.29/19.70 % (333623)Termination phase: Saturation % 133.29/19.70 % (333623)Time elapsed: 2.005 s % 133.29/19.70 % (333623)Peak memory usage: 138 MB % 133.29/19.70 % (333623)Instructions burned: 1997 (million) % 133.29/19.70 % (333627)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2957308349:i=1098:nicw=on_2918 on theBenchmark for (2918ds/1098Mi) % 133.29/19.70 % (333625)Instruction limit reached! % 133.29/19.70 % (333625)------------------------------ % 133.29/19.70 % (333625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.29/19.70 % (333625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.29/19.70 % (333625)CaDiCaL version: 2.1.3 % 133.29/19.70 % (333625)Termination reason: Instruction limit % 133.29/19.70 % (333625)Termination phase: Saturation % 133.29/19.70 % (333625)Time elapsed: 1.259 s % 133.29/19.70 % (333625)Peak memory usage: 138 MB % 133.29/19.70 % (333625)Instructions burned: 2088 (million) % 133.29/19.70 % (333629)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=587085779:i=433:bd=preordered_2912 on theBenchmark for (2912ds/433Mi) % 133.29/19.70 % (333629)Instruction limit reached! % 133.29/19.70 % (333629)------------------------------ % 133.29/19.70 % (333629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.29/19.70 % (333629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.29/19.70 % (333629)CaDiCaL version: 2.1.3 % 133.29/19.70 % (333629)Termination reason: Instruction limit % 133.29/19.70 % (333629)Termination phase: Saturation % 133.29/19.70 % (333629)Time elapsed: 0.207 s % 133.29/19.70 % (333629)Peak memory usage: 92 MB % 133.29/19.70 % (333629)Instructions burned: 433 (million) % 133.29/19.70 % (333627)Instruction limit reached! % 133.29/19.70 % (333627)------------------------------ % 133.29/19.70 % (333627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.29/19.70 % (333627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.29/19.70 % (333627)CaDiCaL version: 2.1.3 % 133.29/19.70 % (333627)Termination reason: Instruction limit % 133.29/19.70 % (333627)Termination phase: Saturation % 133.29/19.70 % (333627)Time elapsed: 0.953 s % 133.29/19.70 % (333627)Peak memory usage: 105 MB % 133.29/19.70 % (333627)Instructions burned: 1098 (million) % 133.29/19.70 % (333631)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3645713945:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2907 on theBenchmark for (2907ds/2942Mi) % 133.29/19.70 % (333634)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2716020646:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2906 on theBenchmark for (2906ds/6922Mi) % 133.29/19.70 % (333631)Instruction limit reached! % 133.29/19.70 % (333631)------------------------------ % 133.29/19.70 % (333631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.29/19.70 % (333631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.29/19.70 % (333631)CaDiCaL version: 2.1.3 % 133.29/19.70 % (333631)Termination reason: Instruction limit % 133.29/19.70 % (333631)Termination phase: Saturation % 133.29/19.70 % (333631)Time elapsed: 1.482 s % 133.29/19.70 % (333631)Peak memory usage: 151 MB % 133.29/19.70 % (333631)Instructions burned: 2944 (million) % 133.29/19.70 % (333637)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=331268364:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2890 on theBenchmark for (2890ds/596Mi) % 145.40/21.47 % (333637)Instruction limit reached! % 145.40/21.47 % (333637)------------------------------ % 145.40/21.47 % (333637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.40/21.47 % (333637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.40/21.47 % (333637)CaDiCaL version: 2.1.3 % 145.40/21.47 % (333637)Termination reason: Instruction limit % 145.40/21.47 % (333637)Termination phase: Saturation % 145.40/21.47 % (333637)Time elapsed: 0.258 s % 145.40/21.47 % (333637)Peak memory usage: 95 MB % 145.40/21.47 % (333637)Instructions burned: 598 (million) % 145.40/21.47 % (333639)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=3709686244:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2886 on theBenchmark for (2886ds/4123Mi) % 145.40/21.47 % (333613)Instruction limit reached! % 145.40/21.47 % (333613)------------------------------ % 145.40/21.47 % (333613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.40/21.47 % (333613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.40/21.47 % (333613)CaDiCaL version: 2.1.3 % 145.40/21.47 % (333613)Termination reason: Instruction limit % 145.40/21.47 % (333613)Termination phase: Saturation % 145.40/21.47 % (333613)Time elapsed: 7.532 s % 145.40/21.47 % (333613)Peak memory usage: 196 MB % 145.40/21.47 % (333613)Instructions burned: 8479 (million) % 145.40/21.47 % (333641)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4238739572:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2878 on theBenchmark for (2878ds/16411Mi) % 145.40/21.47 % (333609)Instruction limit reached! % 145.40/21.47 % (333609)------------------------------ % 145.40/21.47 % (333609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.40/21.47 % (333609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.40/21.47 % (333609)CaDiCaL version: 2.1.3 % 145.40/21.47 % (333609)Termination reason: Instruction limit % 145.40/21.47 % (333609)Termination phase: Saturation % 145.40/21.47 % (333609)Time elapsed: 9.518 s % 145.40/21.47 % (333609)Peak memory usage: 211 MB % 145.40/21.47 % (333609)Instructions burned: 10309 (million) % 145.40/21.47 % (333644)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=331269556:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2864 on theBenchmark for (2864ds/1670Mi) % 145.40/21.47 % (333639)Instruction limit reached! % 145.40/21.47 % (333639)------------------------------ % 145.40/21.47 % (333639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.40/21.47 % (333639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.40/21.47 % (333639)CaDiCaL version: 2.1.3 % 145.40/21.47 % (333639)Termination reason: Instruction limit % 145.40/21.47 % (333639)Termination phase: Saturation % 145.40/21.47 % (333639)Time elapsed: 2.110 s % 145.40/21.47 % (333639)Peak memory usage: 158 MB % 145.40/21.47 % (333639)Instructions burned: 4125 (million) % 145.40/21.47 % (333646)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=1763598775:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2862 on theBenchmark for (2862ds/1722Mi) % 145.40/21.47 % (333634)Instruction limit reached! % 145.40/21.47 % (333634)------------------------------ % 145.40/21.47 % (333634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.40/21.47 % (333634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.40/21.47 % (333634)CaDiCaL version: 2.1.3 % 145.40/21.47 % (333634)Termination reason: Instruction limit % 145.40/21.47 % (333634)Termination phase: Saturation % 145.40/21.47 % (333634)Time elapsed: 4.555 s % 145.40/21.47 % (333634)Peak memory usage: 181 MB % 145.40/21.47 % (333634)Instructions burned: 6923 (million) % 145.40/21.47 % (333687)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=2640260260:cts=off:cond=on:i=9530:bs=on:fsd=on_2858 on theBenchmark for (2858ds/9530Mi) % 145.40/21.47 % (333644)Instruction limit reached! % 145.40/21.47 % (333644)------------------------------ % 145.40/21.47 % (333644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.40/21.47 % (333644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.40/21.47 % (333644)CaDiCaL version: 2.1.3 % 145.40/21.47 % (333644)Termination reason: Instruction limit % 165.95/24.33 % (333644)Termination phase: Saturation % 165.95/24.33 % (333644)Time elapsed: 1.058 s % 165.95/24.33 % (333644)Peak memory usage: 136 MB % 165.95/24.33 % (333644)Instructions burned: 1671 (million) % 165.95/24.33 % (333689)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=511495250:st=2:i=4495:sd=10:ss=included_2852 on theBenchmark for (2852ds/4495Mi) % 165.95/24.33 % (333646)Instruction limit reached! % 165.95/24.33 % (333646)------------------------------ % 165.95/24.33 % (333646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.95/24.33 % (333646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.95/24.33 % (333646)CaDiCaL version: 2.1.3 % 165.95/24.33 % (333646)Termination reason: Instruction limit % 165.95/24.33 % (333646)Termination phase: Saturation % 165.95/24.33 % (333646)Time elapsed: 1.040 s % 165.95/24.33 % (333646)Peak memory usage: 137 MB % 165.95/24.33 % (333646)Instructions burned: 1723 (million) % 165.95/24.33 % (333691)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=2754230588:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2850 on theBenchmark for (2850ds/4920Mi) % 165.95/24.33 % (333641)Instruction limit reached! % 165.95/24.33 % (333641)------------------------------ % 165.95/24.33 % (333641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.95/24.33 % (333641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.95/24.33 % (333641)CaDiCaL version: 2.1.3 % 165.95/24.33 % (333641)Termination reason: Instruction limit % 165.95/24.33 % (333641)Termination phase: Saturation % 165.95/24.33 % (333641)Time elapsed: 4.986 s % 165.95/24.33 % (333641)Peak memory usage: 261 MB % 165.95/24.33 % (333641)Instructions burned: 16413 (million) % 165.95/24.33 % (333689)Instruction limit reached! % 165.95/24.33 % (333689)------------------------------ % 165.95/24.33 % (333689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.95/24.33 % (333689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.95/24.33 % (333689)CaDiCaL version: 2.1.3 % 165.95/24.33 % (333689)Termination reason: Instruction limit % 165.95/24.33 % (333689)Termination phase: Saturation % 165.95/24.33 % (333689)Time elapsed: 2.411 s % 165.95/24.33 % (333689)Peak memory usage: 159 MB % 165.95/24.33 % (333689)Instructions burned: 4497 (million) % 165.95/24.33 % (333693)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=292308901:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2826 on theBenchmark for (2826ds/2083Mi) % 165.95/24.33 % (333694)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=3787820010:i=4629:av=off:gsp=on_2826 on theBenchmark for (2826ds/4629Mi) % 165.95/24.33 % (333691)Instruction limit reached! % 165.95/24.33 % (333691)------------------------------ % 165.95/24.33 % (333691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.95/24.33 % (333691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.95/24.33 % (333691)CaDiCaL version: 2.1.3 % 165.95/24.33 % (333691)Termination reason: Instruction limit % 165.95/24.33 % (333691)Termination phase: Saturation % 165.95/24.33 % (333691)Time elapsed: 2.749 s % 165.95/24.33 % (333691)Peak memory usage: 170 MB % 165.95/24.33 % (333691)Instructions burned: 4921 (million) % 165.95/24.33 % (333697)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=371953877:i=1258:av=off_2821 on theBenchmark for (2821ds/1258Mi) % 165.95/24.33 % (333697)Instruction limit reached! % 165.95/24.33 % (333697)------------------------------ % 165.95/24.33 % (333697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.95/24.33 % (333697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.95/24.33 % (333697)CaDiCaL version: 2.1.3 % 165.95/24.33 % (333697)Termination reason: Instruction limit % 165.95/24.33 % (333697)Termination phase: Saturation % 165.95/24.33 % (333697)Time elapsed: 0.602 s % 165.95/24.33 % (333697)Peak memory usage: 98 MB % 165.95/24.33 % (333697)Instructions burned: 1258 (million) % 165.95/24.33 % (333693)Instruction limit reached! % 165.95/24.33 % (333693)------------------------------ % 165.95/24.33 % (333693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 165.95/24.33 % (333693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 165.95/24.33 % (333693)CaDiCaL version: 2.1.3 % 189.36/27.65 % (333693)Termination reason: Instruction limit % 189.36/27.65 % (333693)Termination phase: Saturation % 189.36/27.65 % (333693)Time elapsed: 1.320 s % 189.36/27.65 % (333693)Peak memory usage: 137 MB % 189.36/27.65 % (333693)Instructions burned: 2083 (million) % 189.36/27.65 % (333699)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=234048556:i=7343:av=off:ss=included_2813 on theBenchmark for (2813ds/7343Mi) % 189.36/27.65 % (333700)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1657913396:i=1325:sd=2:ss=axioms:sgt=16_2812 on theBenchmark for (2812ds/1325Mi) % 189.36/27.65 % (333687)Instruction limit reached! % 189.36/27.65 % (333687)------------------------------ % 189.36/27.65 % (333687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.36/27.65 % (333687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.65 % (333687)CaDiCaL version: 2.1.3 % 189.36/27.65 % (333687)Termination reason: Instruction limit % 189.36/27.65 % (333687)Termination phase: Saturation % 189.36/27.65 % (333687)Time elapsed: 4.636 s % 189.36/27.65 % (333687)Peak memory usage: 165 MB % 189.36/27.65 % (333687)Instructions burned: 9533 (million) % 189.36/27.65 % (333703)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=758978221:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2810 on theBenchmark for (2810ds/2646Mi) % 189.36/27.65 % (333700)Instruction limit reached! % 189.36/27.65 % (333700)------------------------------ % 189.36/27.65 % (333700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.36/27.65 % (333700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.65 % (333700)CaDiCaL version: 2.1.3 % 189.36/27.65 % (333700)Termination reason: Instruction limit % 189.36/27.65 % (333700)Termination phase: Saturation % 189.36/27.65 % (333700)Time elapsed: 0.721 s % 189.36/27.65 % (333700)Peak memory usage: 93 MB % 189.36/27.65 % (333700)Instructions burned: 1326 (million) % 189.36/27.65 % (333703)Instruction limit reached! % 189.36/27.65 % (333703)------------------------------ % 189.36/27.65 % (333703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.36/27.65 % (333703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.65 % (333703)CaDiCaL version: 2.1.3 % 189.36/27.65 % (333703)Termination reason: Instruction limit % 189.36/27.65 % (333703)Termination phase: Saturation % 189.36/27.65 % (333703)Time elapsed: 0.706 s % 189.36/27.65 % (333703)Peak memory usage: 133 MB % 189.36/27.65 % (333703)Instructions burned: 2652 (million) % 189.36/27.65 % (333705)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=4175992532:i=1489:sd=2:ep=R:ss=axioms_2803 on theBenchmark for (2803ds/1489Mi) % 189.36/27.65 % (333706)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=2690204260:i=1503_2801 on theBenchmark for (2801ds/1503Mi) % 189.36/27.65 % (333694)Instruction limit reached! % 189.36/27.65 % (333694)------------------------------ % 189.36/27.65 % (333694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.36/27.65 % (333694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.65 % (333694)CaDiCaL version: 2.1.3 % 189.36/27.65 % (333694)Termination reason: Instruction limit % 189.36/27.65 % (333694)Termination phase: Saturation % 189.36/27.65 % (333694)Time elapsed: 2.469 s % 189.36/27.65 % (333694)Peak memory usage: 137 MB % 189.36/27.65 % (333694)Instructions burned: 4630 (million) % 189.36/27.65 % (333709)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=973899515:i=13942:kws=frequency_2800 on theBenchmark for (2800ds/13942Mi) % 189.36/27.65 % (333706)Instruction limit reached! % 189.36/27.65 % (333706)------------------------------ % 189.36/27.65 % (333706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 189.36/27.65 % (333706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 189.36/27.65 % (333706)CaDiCaL version: 2.1.3 % 189.36/27.65 % (333706)Termination reason: Instruction limit % 189.36/27.65 % (333706)Termination phase: Saturation % 189.36/27.65 % (333706)Time elapsed: 0.508 s % 189.36/27.65 % (333706)Peak memory usage: 136 MB % 189.36/27.65 % (333706)Instructions burned: 1503 (million) % 189.36/27.65 % (333711)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=4257168157:i=3604:fsr=off:er=filter_2795 on theBenchmark for (2795ds/3604Mi) % 210.63/30.67 % (333705)Instruction limit reached! % 210.63/30.67 % (333705)------------------------------ % 210.63/30.67 % (333705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.63/30.67 % (333705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/30.67 % (333705)CaDiCaL version: 2.1.3 % 210.63/30.67 % (333705)Termination reason: Instruction limit % 210.63/30.67 % (333705)Termination phase: Saturation % 210.63/30.67 % (333705)Time elapsed: 0.959 s % 210.63/30.67 % (333705)Peak memory usage: 130 MB % 210.63/30.67 % (333705)Instructions burned: 1489 (million) % 210.63/30.67 % (333713)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1598813171:i=1876:sd=1:ss=included:sgt=32_2791 on theBenchmark for (2791ds/1876Mi) % 210.63/30.67 % (333711)Instruction limit reached! % 210.63/30.67 % (333711)------------------------------ % 210.63/30.67 % (333711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.63/30.67 % (333711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/30.67 % (333711)CaDiCaL version: 2.1.3 % 210.63/30.67 % (333711)Termination reason: Instruction limit % 210.63/30.67 % (333711)Termination phase: Saturation % 210.63/30.67 % (333711)Time elapsed: 1.028 s % 210.63/30.67 % (333711)Peak memory usage: 154 MB % 210.63/30.67 % (333711)Instructions burned: 3606 (million) % 210.63/30.67 % (333715)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=764644878:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2784 on theBenchmark for (2784ds/1932Mi) % 210.63/30.67 % (333713)Instruction limit reached! % 210.63/30.67 % (333713)------------------------------ % 210.63/30.67 % (333713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.63/30.67 % (333713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/30.67 % (333713)CaDiCaL version: 2.1.3 % 210.63/30.67 % (333713)Termination reason: Instruction limit % 210.63/30.67 % (333713)Termination phase: Saturation % 210.63/30.67 % (333713)Time elapsed: 1.124 s % 210.63/30.67 % (333713)Peak memory usage: 137 MB % 210.63/30.67 % (333713)Instructions burned: 1882 (million) % 210.63/30.67 % (333717)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=3771069145:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2778 on theBenchmark for (2778ds/1980Mi) % 210.63/30.67 % (333715)Instruction limit reached! % 210.63/30.67 % (333715)------------------------------ % 210.63/30.67 % (333715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.63/30.67 % (333715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/30.67 % (333715)CaDiCaL version: 2.1.3 % 210.63/30.67 % (333715)Termination reason: Instruction limit % 210.63/30.67 % (333715)Termination phase: Saturation % 210.63/30.67 % (333715)Time elapsed: 0.635 s % 210.63/30.67 % (333715)Peak memory usage: 138 MB % 210.63/30.67 % (333715)Instructions burned: 1937 (million) % 210.63/30.67 % (333719)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=4069644043:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2776 on theBenchmark for (2776ds/3902Mi) % 210.63/30.67 % (333699)Instruction limit reached! % 210.63/30.67 % (333699)------------------------------ % 210.63/30.67 % (333699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.63/30.67 % (333699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/30.67 % (333699)CaDiCaL version: 2.1.3 % 210.63/30.67 % (333699)Termination reason: Instruction limit % 210.63/30.67 % (333699)Termination phase: Saturation % 210.63/30.67 % (333699)Time elapsed: 3.784 s % 210.63/30.67 % (333699)Peak memory usage: 185 MB % 210.63/30.67 % (333699)Instructions burned: 7344 (million) % 210.63/30.67 % (333721)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2522423018:avsq=on:i=3916:aac=none:amm=off_2773 on theBenchmark for (2773ds/3916Mi) % 210.63/30.67 % (333717)Instruction limit reached! % 210.63/30.67 % (333717)------------------------------ % 210.63/30.67 % (333717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.63/30.67 % (333717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/30.67 % (333717)CaDiCaL version: 2.1.3 % 210.63/30.67 % (333717)Termination reason: Instruction limit % 227.87/33.11 % (333717)Termination phase: Saturation % 227.87/33.11 % (333717)Time elapsed: 1.158 s % 227.87/33.11 % (333717)Peak memory usage: 137 MB % 227.87/33.11 % (333717)Instructions burned: 1982 (million) % 227.87/33.11 % (333723)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3488285445:cond=on:i=3940:av=off:er=known_2765 on theBenchmark for (2765ds/3940Mi) % 227.87/33.11 % (333719)Instruction limit reached! % 227.87/33.11 % (333719)------------------------------ % 227.87/33.11 % (333719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.87/33.11 % (333719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.87/33.11 % (333719)CaDiCaL version: 2.1.3 % 227.87/33.11 % (333719)Termination reason: Instruction limit % 227.87/33.11 % (333719)Termination phase: Saturation % 227.87/33.11 % (333719)Time elapsed: 1.330 s % 227.87/33.11 % (333719)Peak memory usage: 153 MB % 227.87/33.11 % (333719)Instructions burned: 3905 (million) % 227.87/33.11 % (333725)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2361013391:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2761 on theBenchmark for (2761ds/3980Mi) % 227.87/33.11 % (333721)Instruction limit reached! % 227.87/33.11 % (333721)------------------------------ % 227.87/33.11 % (333721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.87/33.11 % (333721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.87/33.11 % (333721)CaDiCaL version: 2.1.3 % 227.87/33.11 % (333721)Termination reason: Instruction limit % 227.87/33.11 % (333721)Termination phase: Saturation % 227.87/33.11 % (333721)Time elapsed: 1.820 s % 227.87/33.11 % (333721)Peak memory usage: 117 MB % 227.87/33.11 % (333721)Instructions burned: 3918 (million) % 227.87/33.11 % (333727)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=2577909520:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2753 on theBenchmark for (2753ds/2087Mi) % 227.87/33.11 % (333725)Instruction limit reached! % 227.87/33.11 % (333725)------------------------------ % 227.87/33.11 % (333725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.87/33.11 % (333725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.87/33.11 % (333725)CaDiCaL version: 2.1.3 % 227.87/33.11 % (333725)Termination reason: Instruction limit % 227.87/33.11 % (333725)Termination phase: Saturation % 227.87/33.11 % (333725)Time elapsed: 1.158 s % 227.87/33.11 % (333725)Peak memory usage: 157 MB % 227.87/33.11 % (333725)Instructions burned: 3987 (million) % 227.87/33.11 % (333729)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=2134072357:cts=off:cond=on:i=4272:bs=on:fsd=on_2749 on theBenchmark for (2749ds/4272Mi) % 227.87/33.11 % (333723)Instruction limit reached! % 227.87/33.11 % (333723)------------------------------ % 227.87/33.11 % (333723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.87/33.11 % (333723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.87/33.11 % (333723)CaDiCaL version: 2.1.3 % 227.87/33.11 % (333723)Termination reason: Instruction limit % 227.87/33.11 % (333723)Termination phase: Saturation % 227.87/33.11 % (333723)Time elapsed: 2.114 s % 227.87/33.11 % (333723)Peak memory usage: 152 MB % 227.87/33.11 % (333723)Instructions burned: 3940 (million) % 227.87/33.11 % (333731)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3966803967:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2742 on theBenchmark for (2742ds/2197Mi) % 227.87/33.11 % (333727)Instruction limit reached! % 227.87/33.11 % (333727)------------------------------ % 227.87/33.11 % (333727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.87/33.11 % (333727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.87/33.11 % (333727)CaDiCaL version: 2.1.3 % 227.87/33.11 % (333727)Termination reason: Instruction limit % 227.87/33.11 % (333727)Termination phase: Saturation % 227.87/33.11 % (333727)Time elapsed: 1.239 s % 227.87/33.11 % (333727)Peak memory usage: 140 MB % 227.87/33.11 % (333727)Instructions burned: 2088 (million) % 227.87/33.11 % (333733)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2360392696:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2739 on theBenchmark for (2739ds/6508Mi) % 227.87/33.11 % (333729)Instruction limit reached! % 290.01/41.83 % (333729)------------------------------ % 290.01/41.83 % (333729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.01/41.83 % (333729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.01/41.83 % (333729)CaDiCaL version: 2.1.3 % 290.01/41.83 % (333729)Termination reason: Instruction limit % 290.01/41.83 % (333729)Termination phase: Saturation % 290.01/41.83 % (333729)Time elapsed: 1.522 s % 290.01/41.83 % (333729)Peak memory usage: 146 MB % 290.01/41.83 % (333729)Instructions burned: 4274 (million) % 290.01/41.83 % (333735)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=2429074287:i=2330:fgj=on:av=off:fsr=off_2732 on theBenchmark for (2732ds/2330Mi) % 290.01/41.83 % (333731)Instruction limit reached! % 290.01/41.83 % (333731)------------------------------ % 290.01/41.83 % (333731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.01/41.83 % (333731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.01/41.83 % (333731)CaDiCaL version: 2.1.3 % 290.01/41.83 % (333731)Termination reason: Instruction limit % 290.01/41.83 % (333731)Termination phase: Saturation % 290.01/41.83 % (333731)Time elapsed: 1.218 s % 290.01/41.83 % (333731)Peak memory usage: 141 MB % 290.01/41.83 % (333731)Instructions burned: 2198 (million) % 290.01/41.83 % (333737)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=637812422:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2729 on theBenchmark for (2729ds/7592Mi) % 290.01/41.83 % (333709)Instruction limit reached! % 290.01/41.83 % (333709)------------------------------ % 290.01/41.83 % (333709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.01/41.83 % (333709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.01/41.83 % (333709)CaDiCaL version: 2.1.3 % 290.01/41.83 % (333709)Termination reason: Instruction limit % 290.01/41.83 % (333709)Termination phase: Saturation % 290.01/41.83 % (333709)Time elapsed: 7.320 s % 290.01/41.83 % (333709)Peak memory usage: 241 MB % 290.01/41.83 % (333709)Instructions burned: 13943 (million) % 290.01/41.83 % (333739)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=1963591294:i=2693:kws=precedence:ins=1:av=off_2725 on theBenchmark for (2725ds/2693Mi) % 290.01/41.83 % (333735)Instruction limit reached! % 290.01/41.83 % (333735)------------------------------ % 290.01/41.83 % (333735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.01/41.83 % (333735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.01/41.83 % (333735)CaDiCaL version: 2.1.3 % 290.01/41.83 % (333735)Termination reason: Instruction limit % 290.01/41.83 % (333735)Termination phase: Saturation % 290.01/41.83 % (333735)Time elapsed: 0.862 s % 290.01/41.83 % (333735)Peak memory usage: 229 MB % 290.01/41.83 % (333735)Instructions burned: 2332 (million) % 290.01/41.83 % (333741)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=733263375:i=28651:sd=4:ss=included:sgt=64_2722 on theBenchmark for (2722ds/28651Mi) % 290.01/41.83 % (333739)Instruction limit reached! % 290.01/41.83 % (333739)------------------------------ % 290.01/41.83 % (333739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.01/41.83 % (333739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.01/41.83 % (333739)CaDiCaL version: 2.1.3 % 290.01/41.83 % (333739)Termination reason: Instruction limit % 290.01/41.83 % (333739)Termination phase: Saturation % 290.01/41.83 % (333739)Time elapsed: 1.096 s % 290.01/41.83 % (333739)Peak memory usage: 149 MB % 290.01/41.83 % (333739)Instructions burned: 2696 (million) % 290.01/41.83 % (333743)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=2855022620:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2712 on theBenchmark for (2712ds/2700Mi) % 290.01/41.83 % (333733)Instruction limit reached! % 290.01/41.83 % (333733)------------------------------ % 290.01/41.83 % (333733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.01/41.83 % (333733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.01/41.83 % (333733)CaDiCaL version: 2.1.3 % 290.01/41.83 % (333733)Termination reason: Instruction limit % 290.01/41.83 % (333733)Termination phase: Saturation % 290.01/41.83 % (333733)Time elapsed: 3.479 s % 290.01/41.83 % (333733)Peak memory usage: 137 MB % 290.01/41.83 % (333733)Instructions burned: 6510 (million) % 290.01/41.83 % (333743)Instruction limit reached! % 290.01/41.83 % (333743)------------------------------ % 300.04/43.24 % (333743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.04/43.24 % (333743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.04/43.24 % (333743)CaDiCaL version: 2.1.3 % 300.04/43.24 % (333743)Termination reason: Instruction limit % 300.04/43.24 % (333743)Termination phase: Saturation % 300.04/43.24 % (333743)Time elapsed: 0.878 s % 300.04/43.24 % (333743)Peak memory usage: 147 MB % 300.04/43.24 % (333743)Instructions burned: 2701 (million) % 300.04/43.24 % (333745)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=1526680592:i=3196:nm=4_2703 on theBenchmark for (2703ds/3196Mi) % 300.04/43.24 % (333746)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=2752361071:cts=off:i=3254:av=off_2702 on theBenchmark for (2702ds/3254Mi) % 300.04/43.24 % (333746)Instruction limit reached! % 300.04/43.24 % (333746)------------------------------ % 300.04/43.24 % (333746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.04/43.24 % (333746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.04/43.24 % (333746)CaDiCaL version: 2.1.3 % 300.04/43.24 % (333746)Termination reason: Instruction limit % 300.04/43.24 % (333746)Termination phase: Saturation % 300.04/43.24 % (333746)Time elapsed: 1.077 s % 300.04/43.24 % (333746)Peak memory usage: 145 MB % 300.04/43.24 % (333746)Instructions burned: 3254 (million) % 300.04/43.24 % (333751)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=3992084894:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2690 on theBenchmark for (2690ds/3264Mi) % 300.04/43.24 % (333737)Instruction limit reached! % 300.04/43.24 % (333737)------------------------------ % 300.04/43.24 % (333737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.04/43.24 % (333737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.04/43.24 % (333737)CaDiCaL version: 2.1.3 % 300.04/43.24 % (333737)Termination reason: Instruction limit % 300.04/43.24 % (333737)Termination phase: Saturation % 300.04/43.24 % (333737)Time elapsed: 4.059 s % 300.04/43.24 % (333737)Peak memory usage: 148 MB % 300.04/43.24 % (333737)Instructions burned: 7592 (million) % 300.04/43.24 % (333753)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=3422129174:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2686 on theBenchmark for (2686ds/9708Mi) % 300.04/43.24 % (333745)Instruction limit reached! % 300.04/43.24 % (333745)------------------------------ % 300.04/43.24 % (333745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.04/43.24 % (333745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.04/43.24 % (333745)CaDiCaL version: 2.1.3 % 300.04/43.24 % (333745)Termination reason: Instruction limit % 300.04/43.24 % (333745)Termination phase: Saturation % 300.04/43.24 % (333745)Time elapsed: 1.771 s % 300.04/43.24 % (333745)Peak memory usage: 151 MB % 300.04/43.24 % (333745)Instructions burned: 3198 (million) % 300.04/43.24 % (333755)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4028900453:i=21997:s2at=5:gtg=all_2684 on theBenchmark for (2684ds/21997Mi) % 300.04/43.24 % (333751)Instruction limit reached! % 300.04/43.24 % (333751)------------------------------ % 300.04/43.24 % (333751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.04/43.24 % (333751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.04/43.24 % (333751)CaDiCaL version: 2.1.3 % 300.04/43.24 % (333751)Termination reason: Instruction limit % 300.04/43.24 % (333751)Termination phase: Saturation % 300.04/43.24 % (333751)Time elapsed: 0.988 s % 300.04/43.24 % (333751)Peak memory usage: 147 MB % 300.04/43.24 % (333751)Instructions burned: 3268 (million) % 300.04/43.24 % (333753)Refutation not found, incomplete strategy % 300.04/43.24 % (333753)------------------------------ % 300.04/43.24 % (333753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.04/43.24 % (333753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.04/43.24 % (333753)CaDiCaL version: 2.1.3 % 300.04/43.24 % (333753)Termination reason: Refutation not found, incomplete strategy % 300.04/43.24 % (333753)Time elapsed: 0.611 s % 300.04/43.24 % (333753)Peak memory usage: 135 MB % 300.04/43.24 % (333753)Instructions burned: 937 (million) % 300.04/43.24 % (333757)dis+10_14_to=lpo:sil=8000: % 300.04/43.25 Terminated %------------------------------------------------------------------------------