%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV870-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 : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:41 PM UTC 2026 % Result : Timeout 300.27s 43.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV870-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.09/0.21 % Computer : n015.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 12:50:17 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.27 Running first-order theorem proving % 0.09/0.27 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 % 13.91/2.99 % (2608565)Input is clausal, will run a generic CNF schedule. % 13.91/2.99 % (2608586)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1609681285:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 13.91/2.99 % (2608581)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=2403873407:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 13.91/2.99 % (2608586)Instruction limit reached! % 13.91/2.99 % (2608586)------------------------------ % 13.91/2.99 % (2608586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.91/2.99 % (2608586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.91/2.99 % (2608586)CaDiCaL version: 2.1.3 % 13.91/2.99 % (2608586)Termination reason: Instruction limit % 13.91/2.99 % (2608586)Termination phase: Saturation % 13.91/2.99 % (2608586)Time elapsed: 0.054 s % 13.91/2.99 % (2608586)Peak memory usage: 89 MB % 13.91/2.99 % (2608586)Instructions burned: 183 (million) % 13.91/2.99 % (2608582)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3779975769:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 13.91/2.99 % (2608587)dis-21_1_sil=8000:lcm=predicate:random_seed=3983728743: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) % 13.91/2.99 % (2608584)lrs+10_1_sil=8000:sp=occurrence:random_seed=2334436374:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 13.91/2.99 % (2608583)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2924600192:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 13.91/2.99 % (2608585)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2070817549:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 13.91/2.99 % (2608587)Instruction limit reached! % 13.91/2.99 % (2608587)------------------------------ % 13.91/2.99 % (2608587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.91/2.99 % (2608587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.91/2.99 % (2608587)CaDiCaL version: 2.1.3 % 13.91/2.99 % (2608587)Termination reason: Instruction limit % 13.91/2.99 % (2608587)Termination phase: Saturation % 13.91/2.99 % (2608587)Time elapsed: 0.082 s % 13.91/2.99 % (2608587)Peak memory usage: 88 MB % 13.91/2.99 % (2608587)Instructions burned: 118 (million) % 13.91/2.99 % (2608585)Instruction limit reached! % 13.91/2.99 % (2608585)------------------------------ % 13.91/2.99 % (2608585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.91/2.99 % (2608585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.91/2.99 % (2608585)CaDiCaL version: 2.1.3 % 13.91/2.99 % (2608585)Termination reason: Instruction limit % 13.91/2.99 % (2608585)Termination phase: Saturation % 13.91/2.99 % (2608585)Time elapsed: 0.084 s % 13.91/2.99 % (2608585)Peak memory usage: 88 MB % 13.91/2.99 % (2608585)Instructions burned: 115 (million) % 13.91/2.99 % (2608584)Instruction limit reached! % 13.91/2.99 % (2608584)------------------------------ % 13.91/2.99 % (2608584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.91/2.99 % (2608584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.91/2.99 % (2608584)CaDiCaL version: 2.1.3 % 13.91/2.99 % (2608584)Termination reason: Instruction limit % 13.91/2.99 % (2608584)Termination phase: Saturation % 13.91/2.99 % (2608584)Time elapsed: 0.119 s % 13.91/2.99 % (2608584)Peak memory usage: 89 MB % 13.91/2.99 % (2608584)Instructions burned: 107 (million) % 13.91/2.99 % (2608593)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=2647655737:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 13.91/2.99 % (2608593)Instruction limit reached! % 13.91/2.99 % (2608593)------------------------------ % 13.91/2.99 % (2608593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.91/2.99 % (2608593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.91/2.99 % (2608593)CaDiCaL version: 2.1.3 % 13.91/2.99 % (2608593)Termination reason: Instruction limit % 13.91/2.99 % (2608593)Termination phase: Saturation % 13.91/2.99 % (2608593)Time elapsed: 0.074 s % 13.91/2.99 % (2608593)Peak memory usage: 89 MB % 13.91/2.99 % (2608593)Instructions burned: 144 (million) % 31.66/5.37 % (2608598)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3538295722:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi) % 31.66/5.37 % (2608599)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2824806017:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi) % 31.66/5.37 % (2608602)lrs+10_64_to=lpo:sil=8000:random_seed=3029235646:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 31.66/5.37 % (2608605)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3175990057:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 31.66/5.37 % (2608598)Instruction limit reached! % 31.66/5.37 % (2608598)------------------------------ % 31.66/5.37 % (2608598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.66/5.37 % (2608598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.66/5.37 % (2608598)CaDiCaL version: 2.1.3 % 31.66/5.37 % (2608598)Termination reason: Instruction limit % 31.66/5.37 % (2608598)Termination phase: Saturation % 31.66/5.37 % (2608598)Time elapsed: 0.175 s % 31.66/5.37 % (2608598)Peak memory usage: 90 MB % 31.66/5.37 % (2608598)Instructions burned: 190 (million) % 31.66/5.37 % (2608605)Instruction limit reached! % 31.66/5.37 % (2608605)------------------------------ % 31.66/5.37 % (2608605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.66/5.37 % (2608605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.66/5.37 % (2608605)CaDiCaL version: 2.1.3 % 31.66/5.37 % (2608605)Termination reason: Instruction limit % 31.66/5.37 % (2608605)Termination phase: Saturation % 31.66/5.37 % (2608605)Time elapsed: 0.099 s % 31.66/5.37 % (2608605)Peak memory usage: 90 MB % 31.66/5.37 % (2608605)Instructions burned: 195 (million) % 31.66/5.37 % (2608602)Instruction limit reached! % 31.66/5.37 % (2608602)------------------------------ % 31.66/5.37 % (2608602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.66/5.37 % (2608602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.66/5.37 % (2608602)CaDiCaL version: 2.1.3 % 31.66/5.37 % (2608602)Termination reason: Instruction limit % 31.66/5.37 % (2608602)Termination phase: Saturation % 31.66/5.37 % (2608602)Time elapsed: 0.132 s % 31.66/5.37 % (2608602)Peak memory usage: 89 MB % 31.66/5.37 % (2608602)Instructions burned: 126 (million) % 31.66/5.37 % (2608599)Instruction limit reached! % 31.66/5.37 % (2608599)------------------------------ % 31.66/5.37 % (2608599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.66/5.37 % (2608599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.66/5.37 % (2608599)CaDiCaL version: 2.1.3 % 31.66/5.37 % (2608599)Termination reason: Instruction limit % 31.66/5.37 % (2608599)Termination phase: Saturation % 31.66/5.37 % (2608599)Time elapsed: 0.206 s % 31.66/5.37 % (2608599)Peak memory usage: 90 MB % 31.66/5.37 % (2608599)Instructions burned: 219 (million) % 31.66/5.37 % (2608613)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1484807197:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi) % 31.66/5.37 % (2608615)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4138339817:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi) % 31.66/5.37 % (2608616)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=1288520305:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi) % 31.66/5.37 % (2608617)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4283258036:i=107_2992 on theBenchmark for (2992ds/107Mi) % 31.66/5.37 % (2608617)Refutation not found, incomplete strategy % 31.66/5.37 % (2608617)------------------------------ % 31.66/5.37 % (2608617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.66/5.37 % (2608617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.66/5.37 % (2608617)CaDiCaL version: 2.1.3 % 31.66/5.37 % (2608617)Termination reason: Refutation not found, incomplete strategy % 31.66/5.37 % (2608617)Time elapsed: 0.046 s % 31.66/5.37 % (2608617)Peak memory usage: 89 MB % 31.66/5.37 % (2608617)Instructions burned: 45 (million) % 31.66/5.37 % (2608616)Instruction limit reached! % 31.66/5.37 % (2608616)------------------------------ % 31.66/5.37 % (2608616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.45/8.67 % (2608616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.45/8.67 % (2608616)CaDiCaL version: 2.1.3 % 54.45/8.67 % (2608616)Termination reason: Instruction limit % 54.45/8.67 % (2608616)Termination phase: Saturation % 54.45/8.67 % (2608616)Time elapsed: 0.091 s % 54.45/8.67 % (2608616)Peak memory usage: 89 MB % 54.45/8.67 % (2608616)Instructions burned: 106 (million) % 54.45/8.67 % (2608613)Instruction limit reached! % 54.45/8.67 % (2608613)------------------------------ % 54.45/8.67 % (2608613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.45/8.67 % (2608613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.45/8.67 % (2608613)CaDiCaL version: 2.1.3 % 54.45/8.67 % (2608613)Termination reason: Instruction limit % 54.45/8.67 % (2608613)Termination phase: Saturation % 54.45/8.67 % (2608613)Time elapsed: 0.162 s % 54.45/8.67 % (2608613)Peak memory usage: 90 MB % 54.45/8.67 % (2608613)Instructions burned: 158 (million) % 54.45/8.67 % (2608624)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2795478748:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi) % 54.45/8.67 % (2608625)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3466395329:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi) % 54.45/8.67 % (2608617)------------------------------ % 54.45/8.67 % (2608617)------------------------------ % 54.45/8.67 % (2608624)Instruction limit reached! % 54.45/8.67 % (2608624)------------------------------ % 54.45/8.67 % (2608624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.45/8.67 % (2608624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.45/8.67 % (2608624)CaDiCaL version: 2.1.3 % 54.45/8.67 % (2608624)Termination reason: Instruction limit % 54.45/8.67 % (2608624)Termination phase: Saturation % 54.45/8.67 % (2608624)Time elapsed: 0.244 s % 54.45/8.67 % (2608624)Peak memory usage: 90 MB % 54.45/8.67 % (2608624)Instructions burned: 242 (million) % 54.45/8.67 % (2608630)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1839352975:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi) % 54.45/8.67 % (2608630)Instruction limit reached! % 54.45/8.67 % (2608630)------------------------------ % 54.45/8.67 % (2608630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.45/8.67 % (2608630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.45/8.67 % (2608630)CaDiCaL version: 2.1.3 % 54.45/8.67 % (2608630)Termination reason: Instruction limit % 54.45/8.67 % (2608630)Termination phase: Saturation % 54.45/8.67 % (2608630)Time elapsed: 0.050 s % 54.45/8.67 % (2608630)Peak memory usage: 88 MB % 54.45/8.67 % (2608630)Instructions burned: 136 (million) % 54.45/8.67 % (2608632)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3245139153:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi) % 54.45/8.67 % (2608635)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3939870803:i=191:fgj=on:bd=all_2984 on theBenchmark for (2984ds/191Mi) % 54.45/8.67 % (2608635)Instruction limit reached! % 54.45/8.67 % (2608635)------------------------------ % 54.45/8.67 % (2608635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.45/8.67 % (2608635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.45/8.67 % (2608635)CaDiCaL version: 2.1.3 % 54.45/8.67 % (2608635)Termination reason: Instruction limit % 54.45/8.67 % (2608635)Termination phase: Saturation % 54.45/8.67 % (2608635)Time elapsed: 0.131 s % 54.45/8.67 % (2608635)Peak memory usage: 91 MB % 54.45/8.67 % (2608635)Instructions burned: 192 (million) % 54.45/8.67 % (2608638)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3965803569:i=264:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/264Mi) % 54.45/8.67 % (2608638)Instruction limit reached! % 54.45/8.67 % (2608638)------------------------------ % 54.45/8.67 % (2608638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.45/8.67 % (2608638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.45/8.67 % (2608638)CaDiCaL version: 2.1.3 % 54.45/8.67 % (2608638)Termination reason: Instruction limit % 54.45/8.67 % (2608638)Termination phase: Saturation % 54.45/8.67 % (2608638)Time elapsed: 0.111 s % 54.45/8.67 % (2608638)Peak memory usage: 90 MB % 54.45/8.67 % (2608638)Instructions burned: 266 (million) % 79.56/12.11 % (2608632)Instruction limit reached! % 79.56/12.11 % (2608632)------------------------------ % 79.56/12.11 % (2608632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.56/12.11 % (2608632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.56/12.11 % (2608632)CaDiCaL version: 2.1.3 % 79.56/12.11 % (2608632)Termination reason: Instruction limit % 79.56/12.11 % (2608632)Termination phase: Saturation % 79.56/12.11 % (2608632)Time elapsed: 0.530 s % 79.56/12.11 % (2608632)Peak memory usage: 95 MB % 79.56/12.11 % (2608632)Instructions burned: 499 (million) % 79.56/12.11 % (2608640)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4067556041:cond=on:i=156:bs=on:gtg=exists_all:er=known_2978 on theBenchmark for (2978ds/156Mi) % 79.56/12.11 % (2608640)Instruction limit reached! % 79.56/12.11 % (2608640)------------------------------ % 79.56/12.11 % (2608640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.56/12.11 % (2608640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.56/12.11 % (2608640)CaDiCaL version: 2.1.3 % 79.56/12.11 % (2608640)Termination reason: Instruction limit % 79.56/12.11 % (2608640)Termination phase: Saturation % 79.56/12.11 % (2608640)Time elapsed: 0.086 s % 79.56/12.11 % (2608640)Peak memory usage: 90 MB % 79.56/12.11 % (2608640)Instructions burned: 156 (million) % 79.56/12.11 % (2608641)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=4637778:i=3256:kws=precedence:bd=preordered:av=off_2978 on theBenchmark for (2978ds/3256Mi) % 79.56/12.11 % (2608644)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1161716982:i=537:av=off:ss=included_2976 on theBenchmark for (2976ds/537Mi) % 79.56/12.11 % (2608644)Instruction limit reached! % 79.56/12.11 % (2608644)------------------------------ % 79.56/12.11 % (2608644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.56/12.11 % (2608644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.56/12.11 % (2608644)CaDiCaL version: 2.1.3 % 79.56/12.11 % (2608644)Termination reason: Instruction limit % 79.56/12.11 % (2608644)Termination phase: Saturation % 79.56/12.11 % (2608644)Time elapsed: 0.201 s % 79.56/12.11 % (2608644)Peak memory usage: 89 MB % 79.56/12.11 % (2608644)Instructions burned: 537 (million) % 79.56/12.11 % (2608650)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2802266890:i=180:bd=preordered:av=off_2972 on theBenchmark for (2972ds/180Mi) % 79.56/12.11 % (2608650)Instruction limit reached! % 79.56/12.11 % (2608650)------------------------------ % 79.56/12.11 % (2608650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.56/12.11 % (2608650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.56/12.11 % (2608650)CaDiCaL version: 2.1.3 % 79.56/12.11 % (2608650)Termination reason: Instruction limit % 79.56/12.11 % (2608650)Termination phase: Saturation % 79.56/12.11 % (2608650)Time elapsed: 0.090 s % 79.56/12.11 % (2608650)Peak memory usage: 91 MB % 79.56/12.11 % (2608650)Instructions burned: 182 (million) % 79.56/12.11 % (2608652)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=3879088145:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2970 on theBenchmark for (2970ds/10307Mi) % 79.56/12.11 % (2608615)Instruction limit reached! % 79.56/12.11 % (2608615)------------------------------ % 79.56/12.11 % (2608615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.56/12.11 % (2608615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.56/12.11 % (2608615)CaDiCaL version: 2.1.3 % 79.56/12.11 % (2608615)Termination reason: Instruction limit % 79.56/12.11 % (2608615)Termination phase: Saturation % 79.56/12.11 % (2608615)Time elapsed: 3.028 s % 79.56/12.11 % (2608615)Peak memory usage: 148 MB % 79.56/12.11 % (2608615)Instructions burned: 3394 (million) % 79.56/12.11 % (2608656)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=1444747790:i=412:gtgl=4:gtg=exists_all_2961 on theBenchmark for (2961ds/412Mi) % 79.56/12.11 % (2608656)Instruction limit reached! % 79.56/12.11 % (2608656)------------------------------ % 79.56/12.11 % (2608656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.56/12.11 % (2608656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.56/12.11 % (2608656)CaDiCaL version: 2.1.3 % 109.65/16.34 % (2608656)Termination reason: Instruction limit % 109.65/16.34 % (2608656)Termination phase: Saturation % 109.65/16.34 % (2608656)Time elapsed: 0.369 s % 109.65/16.34 % (2608656)Peak memory usage: 92 MB % 109.65/16.34 % (2608656)Instructions burned: 413 (million) % 109.65/16.34 % (2608658)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=3872566652:s2pl=no:i=8478:s2at=4:nm=6_2955 on theBenchmark for (2955ds/8478Mi) % 109.65/16.34 % (2608641)Instruction limit reached! % 109.65/16.34 % (2608641)------------------------------ % 109.65/16.34 % (2608641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.65/16.34 % (2608641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.65/16.34 % (2608641)CaDiCaL version: 2.1.3 % 109.65/16.34 % (2608641)Termination reason: Instruction limit % 109.65/16.34 % (2608641)Termination phase: Saturation % 109.65/16.34 % (2608641)Time elapsed: 3.321 s % 109.65/16.34 % (2608641)Peak memory usage: 149 MB % 109.65/16.34 % (2608641)Instructions burned: 3256 (million) % 109.65/16.34 % (2608662)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=3904764207:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2942 on theBenchmark for (2942ds/303Mi) % 109.65/16.35 % (2608662)Instruction limit reached! % 109.65/16.35 % (2608662)------------------------------ % 109.65/16.35 % (2608662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.65/16.35 % (2608662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.65/16.35 % (2608662)CaDiCaL version: 2.1.3 % 109.65/16.35 % (2608662)Termination reason: Instruction limit % 109.65/16.35 % (2608662)Termination phase: Saturation % 109.65/16.35 % (2608662)Time elapsed: 0.307 s % 109.65/16.35 % (2608662)Peak memory usage: 92 MB % 109.65/16.35 % (2608662)Instructions burned: 303 (million) % 109.65/16.35 % (2608664)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1014127120:st=4:i=720:sd=3:fsr=off:ss=axioms_2937 on theBenchmark for (2937ds/720Mi) % 109.65/16.35 % (2608625)Instruction limit reached! % 109.65/16.35 % (2608625)------------------------------ % 109.65/16.35 % (2608625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.65/16.35 % (2608625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.65/16.35 % (2608625)CaDiCaL version: 2.1.3 % 109.65/16.35 % (2608625)Termination reason: Instruction limit % 109.65/16.35 % (2608625)Termination phase: Saturation % 109.65/16.35 % (2608625)Time elapsed: 5.441 s % 109.65/16.35 % (2608625)Peak memory usage: 153 MB % 109.65/16.35 % (2608625)Instructions burned: 5208 (million) % 109.65/16.35 % (2608666)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1046055030:i=598:bs=on:bd=preordered:av=off:ss=axioms_2933 on theBenchmark for (2933ds/598Mi) % 109.65/16.35 % (2608664)Instruction limit reached! % 109.65/16.35 % (2608664)------------------------------ % 109.65/16.35 % (2608664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.65/16.35 % (2608664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.65/16.35 % (2608664)CaDiCaL version: 2.1.3 % 109.65/16.35 % (2608664)Termination reason: Instruction limit % 109.65/16.35 % (2608664)Termination phase: Saturation % 109.65/16.35 % (2608664)Time elapsed: 0.676 s % 109.65/16.35 % (2608664)Peak memory usage: 95 MB % 109.65/16.35 % (2608664)Instructions burned: 720 (million) % 109.65/16.35 % (2608668)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=86612089:i=2989:sd=3:ss=axioms:sgt=60_2928 on theBenchmark for (2928ds/2989Mi) % 109.65/16.35 % (2608666)Instruction limit reached! % 109.65/16.35 % (2608666)------------------------------ % 109.65/16.35 % (2608666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.65/16.35 % (2608666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.65/16.35 % (2608666)CaDiCaL version: 2.1.3 % 109.65/16.35 % (2608666)Termination reason: Instruction limit % 109.65/16.35 % (2608666)Termination phase: Saturation % 109.65/16.35 % (2608666)Time elapsed: 0.662 s % 109.65/16.35 % (2608666)Peak memory usage: 94 MB % 109.65/16.35 % (2608666)Instructions burned: 598 (million) % 109.65/16.35 % (2608670)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=3691969253:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2924 on theBenchmark for (2924ds/1997Mi) % 176.63/25.76 % (2608652)Instruction limit reached! % 176.63/25.76 % (2608652)------------------------------ % 176.63/25.76 % (2608652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.63/25.76 % (2608652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.63/25.76 % (2608652)CaDiCaL version: 2.1.3 % 176.63/25.76 % (2608652)Termination reason: Instruction limit % 176.63/25.76 % (2608652)Termination phase: Saturation % 176.63/25.76 % (2608652)Time elapsed: 6.103 s % 176.63/25.76 % (2608652)Peak memory usage: 185 MB % 176.63/25.76 % (2608652)Instructions burned: 10308 (million) % 176.63/25.76 % (2608676)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=1080079394:i=2088:bd=preordered:av=off_2907 on theBenchmark for (2907ds/2088Mi) % 176.63/25.76 % (2608670)Instruction limit reached! % 176.63/25.76 % (2608670)------------------------------ % 176.63/25.76 % (2608670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.63/25.76 % (2608670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.63/25.76 % (2608670)CaDiCaL version: 2.1.3 % 176.63/25.76 % (2608670)Termination reason: Instruction limit % 176.63/25.76 % (2608670)Termination phase: Saturation % 176.63/25.76 % (2608670)Time elapsed: 2.183 s % 176.63/25.76 % (2608670)Peak memory usage: 138 MB % 176.63/25.76 % (2608670)Instructions burned: 1997 (million) % 176.63/25.76 % (2608678)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=436968595:i=1098:nicw=on_2900 on theBenchmark for (2900ds/1098Mi) % 176.63/25.76 % (2608668)Instruction limit reached! % 176.63/25.76 % (2608668)------------------------------ % 176.63/25.76 % (2608668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.63/25.76 % (2608668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.63/25.76 % (2608668)CaDiCaL version: 2.1.3 % 176.63/25.76 % (2608668)Termination reason: Instruction limit % 176.63/25.76 % (2608668)Termination phase: Saturation % 176.63/25.76 % (2608668)Time elapsed: 3.044 s % 176.63/25.76 % (2608668)Peak memory usage: 144 MB % 176.63/25.76 % (2608668)Instructions burned: 2990 (million) % 176.63/25.76 % (2608680)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3240040486:i=433:bd=preordered_2895 on theBenchmark for (2895ds/433Mi) % 176.63/25.76 % (2608678)Instruction limit reached! % 176.63/25.76 % (2608678)------------------------------ % 176.63/25.76 % (2608678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.63/25.76 % (2608678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.63/25.76 % (2608678)CaDiCaL version: 2.1.3 % 176.63/25.76 % (2608678)Termination reason: Instruction limit % 176.63/25.76 % (2608678)Termination phase: Saturation % 176.63/25.76 % (2608678)Time elapsed: 0.589 s % 176.63/25.76 % (2608678)Peak memory usage: 100 MB % 176.63/25.76 % (2608678)Instructions burned: 1098 (million) % 176.63/25.76 % (2608682)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3591802212:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2892 on theBenchmark for (2892ds/2942Mi) % 176.63/25.76 % (2608680)Instruction limit reached! % 176.63/25.76 % (2608680)------------------------------ % 176.63/25.76 % (2608680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.63/25.76 % (2608680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.63/25.76 % (2608680)CaDiCaL version: 2.1.3 % 176.63/25.76 % (2608680)Termination reason: Instruction limit % 176.63/25.76 % (2608680)Termination phase: Saturation % 176.63/25.76 % (2608680)Time elapsed: 0.420 s % 176.63/25.76 % (2608680)Peak memory usage: 92 MB % 176.63/25.76 % (2608680)Instructions burned: 433 (million) % 176.63/25.76 % (2608676)Instruction limit reached! % 176.63/25.76 % (2608676)------------------------------ % 176.63/25.76 % (2608676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.63/25.76 % (2608676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.63/25.76 % (2608676)CaDiCaL version: 2.1.3 % 176.63/25.76 % (2608676)Termination reason: Instruction limit % 176.63/25.76 % (2608676)Termination phase: Saturation % 176.63/25.76 % (2608676)Time elapsed: 1.826 s % 176.63/25.76 % (2608676)Peak memory usage: 139 MB % 176.63/25.76 % (2608676)Instructions burned: 2089 (million) % 176.63/25.76 % (2608684)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=407399117:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2889 on theBenchmark for (2889ds/6922Mi) % 214.62/31.08 % (2608688)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=3734910092:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2887 on theBenchmark for (2887ds/596Mi) % 214.62/31.08 % (2608688)Instruction limit reached! % 214.62/31.08 % (2608688)------------------------------ % 214.62/31.08 % (2608688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.62/31.08 % (2608688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.62/31.08 % (2608688)CaDiCaL version: 2.1.3 % 214.62/31.08 % (2608688)Termination reason: Instruction limit % 214.62/31.08 % (2608688)Termination phase: Saturation % 214.62/31.08 % (2608688)Time elapsed: 0.572 s % 214.62/31.08 % (2608688)Peak memory usage: 96 MB % 214.62/31.08 % (2608688)Instructions burned: 596 (million) % 214.62/31.08 % (2608692)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=261555148:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2879 on theBenchmark for (2879ds/4123Mi) % 214.62/31.08 % (2608682)Instruction limit reached! % 214.62/31.08 % (2608682)------------------------------ % 214.62/31.08 % (2608682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.62/31.08 % (2608682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.62/31.08 % (2608682)CaDiCaL version: 2.1.3 % 214.62/31.08 % (2608682)Termination reason: Instruction limit % 214.62/31.08 % (2608682)Termination phase: Saturation % 214.62/31.08 % (2608682)Time elapsed: 1.682 s % 214.62/31.08 % (2608682)Peak memory usage: 145 MB % 214.62/31.08 % (2608682)Instructions burned: 2942 (million) % 214.62/31.08 % (2608694)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2081029821:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2874 on theBenchmark for (2874ds/16411Mi) % 214.62/31.08 % (2608658)Instruction limit reached! % 214.62/31.08 % (2608658)------------------------------ % 214.62/31.08 % (2608658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.62/31.08 % (2608658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.62/31.08 % (2608658)CaDiCaL version: 2.1.3 % 214.62/31.08 % (2608658)Termination reason: Instruction limit % 214.62/31.08 % (2608658)Termination phase: Saturation % 214.62/31.08 % (2608658)Time elapsed: 8.485 s % 214.62/31.08 % (2608658)Peak memory usage: 189 MB % 214.62/31.08 % (2608658)Instructions burned: 8478 (million) % 214.62/31.08 % (2608696)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=4074783385:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2867 on theBenchmark for (2867ds/1670Mi) % 214.62/31.08 % (2608692)Instruction limit reached! % 214.62/31.08 % (2608692)------------------------------ % 214.62/31.08 % (2608692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.62/31.08 % (2608692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.62/31.08 % (2608692)CaDiCaL version: 2.1.3 % 214.62/31.08 % (2608692)Termination reason: Instruction limit % 214.62/31.08 % (2608692)Termination phase: Saturation % 214.62/31.08 % (2608692)Time elapsed: 2.589 s % 214.62/31.08 % (2608692)Peak memory usage: 158 MB % 214.62/31.08 % (2608692)Instructions burned: 4123 (million) % 214.62/31.08 % (2608698)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=2307983093:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2851 on theBenchmark for (2851ds/1722Mi) % 214.62/31.08 % (2608696)Instruction limit reached! % 214.62/31.08 % (2608696)------------------------------ % 214.62/31.08 % (2608696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.62/31.08 % (2608696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.62/31.08 % (2608696)CaDiCaL version: 2.1.3 % 214.62/31.08 % (2608696)Termination reason: Instruction limit % 214.62/31.08 % (2608696)Termination phase: Saturation % 214.62/31.08 % (2608696)Time elapsed: 1.731 s % 214.62/31.08 % (2608696)Peak memory usage: 137 MB % 214.62/31.08 % (2608696)Instructions burned: 1670 (million) % 214.62/31.08 % (2608700)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=262202487:cts=off:cond=on:i=9530:bs=on:fsd=on_2847 on theBenchmark for (2847ds/9530Mi) % 245.18/35.82 % (2608698)Instruction limit reached! % 245.18/35.82 % (2608698)------------------------------ % 245.18/35.82 % (2608698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.18/35.82 % (2608698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.18/35.82 % (2608698)CaDiCaL version: 2.1.3 % 245.18/35.82 % (2608698)Termination reason: Instruction limit % 245.18/35.82 % (2608698)Termination phase: Saturation % 245.18/35.82 % (2608698)Time elapsed: 0.997 s % 245.18/35.82 % (2608698)Peak memory usage: 136 MB % 245.18/35.82 % (2608698)Instructions burned: 1723 (million) % 245.18/35.82 % (2608703)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1036461643:st=2:i=4495:sd=10:ss=included_2839 on theBenchmark for (2839ds/4495Mi) % 245.18/35.82 % (2608684)Instruction limit reached! % 245.18/35.82 % (2608684)------------------------------ % 245.18/35.82 % (2608684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.18/35.82 % (2608684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.18/35.82 % (2608684)CaDiCaL version: 2.1.3 % 245.18/35.82 % (2608684)Termination reason: Instruction limit % 245.18/35.82 % (2608684)Termination phase: Saturation % 245.18/35.82 % (2608684)Time elapsed: 7.036 s % 245.18/35.82 % (2608684)Peak memory usage: 181 MB % 245.18/35.82 % (2608684)Instructions burned: 6922 (million) % 245.18/35.82 % (2608708)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=1001530304:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2817 on theBenchmark for (2817ds/4920Mi) % 245.18/35.82 % (2608703)Instruction limit reached! % 245.18/35.82 % (2608703)------------------------------ % 245.18/35.82 % (2608703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.18/35.82 % (2608703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.18/35.82 % (2608703)CaDiCaL version: 2.1.3 % 245.18/35.82 % (2608703)Termination reason: Instruction limit % 245.18/35.82 % (2608703)Termination phase: Saturation % 245.18/35.82 % (2608703)Time elapsed: 4.697 s % 245.18/35.82 % (2608703)Peak memory usage: 158 MB % 245.18/35.82 % (2608703)Instructions burned: 4496 (million) % 245.18/35.82 % (2608710)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=2975673794:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2791 on theBenchmark for (2791ds/2083Mi) % 245.18/35.82 % (2608710)Instruction limit reached! % 245.18/35.82 % (2608710)------------------------------ % 245.18/35.82 % (2608710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.18/35.82 % (2608710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.18/35.82 % (2608710)CaDiCaL version: 2.1.3 % 245.18/35.82 % (2608710)Termination reason: Instruction limit % 245.18/35.82 % (2608710)Termination phase: Saturation % 245.18/35.82 % (2608710)Time elapsed: 2.271 s % 245.18/35.82 % (2608710)Peak memory usage: 139 MB % 245.18/35.82 % (2608710)Instructions burned: 2084 (million) % 245.18/35.82 % (2608708)Instruction limit reached! % 245.18/35.82 % (2608708)------------------------------ % 245.18/35.82 % (2608708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.18/35.82 % (2608708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.18/35.82 % (2608708)CaDiCaL version: 2.1.3 % 245.18/35.82 % (2608708)Termination reason: Instruction limit % 245.18/35.82 % (2608708)Termination phase: Saturation % 245.18/35.82 % (2608708)Time elapsed: 4.902 s % 245.18/35.82 % (2608708)Peak memory usage: 161 MB % 245.18/35.82 % (2608708)Instructions burned: 4920 (million) % 245.18/35.82 % (2608715)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2793096819:i=1258:av=off_2765 on theBenchmark for (2765ds/1258Mi) % 245.18/35.82 % (2608714)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=3169357618:i=4629:av=off:gsp=on_2765 on theBenchmark for (2765ds/4629Mi) % 245.18/35.82 % (2608715)Instruction limit reached! % 245.18/35.82 % (2608715)------------------------------ % 245.18/35.82 % (2608715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 245.18/35.82 % (2608715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 245.18/35.82 % (2608715)CaDiCaL version: 2.1.3 % 245.18/35.82 % (2608715)Termination reason: Instruction limit % 245.18/35.82 % (2608715)Termination phTerminated %------------------------------------------------------------------------------