%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV526-1.040 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:16:42 PM UTC 2026 % Result : Timeout 300.37s 42.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV526-1.040 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n008.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 11:33:55 UTC 2026 % 0.08/0.19 % CPUTime : % 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.22 Running first-order theorem proving % 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 7.14/1.53 % (2188728)Input is clausal, will run a generic CNF schedule. % 7.14/1.53 % (2188738)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2964259738:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 7.14/1.53 % (2188733)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=1290406029:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 7.14/1.53 % (2188735)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=54538810:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 7.14/1.53 % (2188734)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2779257616:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 7.14/1.53 % (2188736)lrs+10_1_sil=8000:sp=occurrence:random_seed=1130762368:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 7.14/1.53 % (2188737)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1364386754:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 7.14/1.53 % (2188739)dis-21_1_sil=8000:lcm=predicate:random_seed=161689379:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 7.14/1.53 % (2188739)Refutation not found, incomplete strategy % 7.14/1.53 % (2188739)------------------------------ % 7.14/1.53 % (2188739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.14/1.53 % (2188739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.53 % (2188739)CaDiCaL version: 2.1.3 % 7.14/1.53 % (2188739)Termination reason: Refutation not found, incomplete strategy % 7.14/1.53 % (2188739)Time elapsed: 0.002 s % 7.14/1.53 % (2188739)Peak memory usage: 88 MB % 7.14/1.53 % (2188739)Instructions burned: 3 (million) % 7.14/1.53 % (2188738)Instruction limit reached! % 7.14/1.53 % (2188738)------------------------------ % 7.14/1.53 % (2188738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.14/1.53 % (2188738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.53 % (2188738)CaDiCaL version: 2.1.3 % 7.14/1.53 % (2188738)Termination reason: Instruction limit % 7.14/1.53 % (2188738)Termination phase: Saturation % 7.14/1.53 % (2188738)Time elapsed: 0.054 s % 7.14/1.53 % (2188738)Peak memory usage: 89 MB % 7.14/1.53 % (2188738)Instructions burned: 181 (million) % 7.14/1.53 % (2188737)Instruction limit reached! % 7.14/1.53 % (2188737)------------------------------ % 7.14/1.53 % (2188737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.14/1.53 % (2188737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.53 % (2188737)CaDiCaL version: 2.1.3 % 7.14/1.53 % (2188737)Termination reason: Instruction limit % 7.14/1.53 % (2188737)Termination phase: Saturation % 7.14/1.53 % (2188737)Time elapsed: 0.057 s % 7.14/1.53 % (2188737)Peak memory usage: 88 MB % 7.14/1.53 % (2188737)Instructions burned: 114 (million) % 7.14/1.53 % (2188736)Instruction limit reached! % 7.14/1.53 % (2188736)------------------------------ % 7.14/1.53 % (2188736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.14/1.53 % (2188736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.53 % (2188736)CaDiCaL version: 2.1.3 % 7.14/1.53 % (2188736)Termination reason: Instruction limit % 7.14/1.53 % (2188736)Termination phase: Saturation % 7.14/1.53 % (2188736)Time elapsed: 0.062 s % 7.14/1.53 % (2188736)Peak memory usage: 89 MB % 7.14/1.53 % (2188736)Instructions burned: 108 (million) % 7.14/1.53 % (2188747)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=3680478249:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 7.14/1.53 % (2188747)Instruction limit reached! % 7.14/1.53 % (2188747)------------------------------ % 7.14/1.53 % (2188747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.14/1.53 % (2188747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.14/1.53 % (2188747)CaDiCaL version: 2.1.3 % 7.14/1.53 % (2188747)Termination reason: Instruction limit % 7.14/1.53 % (2188747)Termination phase: Saturation % 7.14/1.53 % (2188747)Time elapsed: 0.031 s % 7.14/1.53 % (2188747)Peak memory usage: 89 MB % 7.14/1.53 % (2188747)Instructions burned: 145 (million) % 7.14/1.53 % (2188748)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1371479962:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi) % 15.94/2.79 % (2188749)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3327718107:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 15.94/2.79 % (2188751)lrs+10_64_to=lpo:sil=8000:random_seed=1423305170:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 15.94/2.79 % (2188739)------------------------------ % 15.94/2.79 % (2188739)------------------------------ % 15.94/2.79 % (2188751)Instruction limit reached! % 15.94/2.79 % (2188751)------------------------------ % 15.94/2.79 % (2188751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.94/2.79 % (2188751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.94/2.79 % (2188751)CaDiCaL version: 2.1.3 % 15.94/2.79 % (2188751)Termination reason: Instruction limit % 15.94/2.79 % (2188751)Termination phase: Saturation % 15.94/2.79 % (2188751)Time elapsed: 0.038 s % 15.94/2.79 % (2188751)Peak memory usage: 89 MB % 15.94/2.79 % (2188751)Instructions burned: 130 (million) % 15.94/2.79 % (2188748)Instruction limit reached! % 15.94/2.79 % (2188748)------------------------------ % 15.94/2.79 % (2188748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.94/2.79 % (2188748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.94/2.79 % (2188748)CaDiCaL version: 2.1.3 % 15.94/2.79 % (2188748)Termination reason: Instruction limit % 15.94/2.79 % (2188748)Termination phase: Saturation % 15.94/2.79 % (2188748)Time elapsed: 0.075 s % 15.94/2.79 % (2188748)Peak memory usage: 89 MB % 15.94/2.79 % (2188748)Instructions burned: 190 (million) % 15.94/2.79 % (2188749)Instruction limit reached! % 15.94/2.79 % (2188749)------------------------------ % 15.94/2.79 % (2188749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.94/2.79 % (2188749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.94/2.79 % (2188749)CaDiCaL version: 2.1.3 % 15.94/2.79 % (2188749)Termination reason: Instruction limit % 15.94/2.79 % (2188749)Termination phase: Saturation % 15.94/2.79 % (2188749)Time elapsed: 0.088 s % 15.94/2.79 % (2188749)Peak memory usage: 89 MB % 15.94/2.79 % (2188749)Instructions burned: 220 (million) % 15.94/2.79 % (2188756)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4135611988:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 15.94/2.79 % (2188755)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=599034745:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi) % 15.94/2.79 % (2188756)Instruction limit reached! % 15.94/2.79 % (2188756)------------------------------ % 15.94/2.79 % (2188756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.94/2.79 % (2188756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.94/2.79 % (2188756)CaDiCaL version: 2.1.3 % 15.94/2.79 % (2188756)Termination reason: Instruction limit % 15.94/2.79 % (2188756)Termination phase: Saturation % 15.94/2.79 % (2188756)Time elapsed: 0.046 s % 15.94/2.79 % (2188756)Peak memory usage: 91 MB % 15.94/2.79 % (2188756)Instructions burned: 157 (million) % 15.94/2.79 % (2188757)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2705968749:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi) % 15.94/2.79 % (2188758)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=1645456381:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi) % 15.94/2.79 % (2188758)Instruction limit reached! % 15.94/2.79 % (2188758)------------------------------ % 15.94/2.79 % (2188758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.94/2.79 % (2188758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.94/2.79 % (2188758)CaDiCaL version: 2.1.3 % 15.94/2.79 % (2188758)Termination reason: Instruction limit % 15.94/2.79 % (2188758)Termination phase: Saturation % 15.94/2.79 % (2188758)Time elapsed: 0.046 s % 15.94/2.79 % (2188758)Peak memory usage: 89 MB % 15.94/2.79 % (2188758)Instructions burned: 107 (million) % 15.94/2.79 % (2188762)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3649288360:i=107_2994 on theBenchmark for (2994ds/107Mi) % 15.94/2.79 % (2188755)Instruction limit reached! % 15.94/2.79 % (2188755)------------------------------ % 27.37/4.32 % (2188755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.37/4.32 % (2188755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.37/4.32 % (2188755)CaDiCaL version: 2.1.3 % 27.37/4.32 % (2188755)Termination reason: Instruction limit % 27.37/4.32 % (2188755)Termination phase: Saturation % 27.37/4.32 % (2188755)Time elapsed: 0.103 s % 27.37/4.32 % (2188755)Peak memory usage: 90 MB % 27.37/4.32 % (2188755)Instructions burned: 195 (million) % 27.37/4.32 % (2188762)Instruction limit reached! % 27.37/4.32 % (2188762)------------------------------ % 27.37/4.32 % (2188762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.37/4.32 % (2188762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.37/4.32 % (2188762)CaDiCaL version: 2.1.3 % 27.37/4.32 % (2188762)Termination reason: Instruction limit % 27.37/4.32 % (2188762)Termination phase: Saturation % 27.37/4.32 % (2188762)Time elapsed: 0.024 s % 27.37/4.32 % (2188762)Peak memory usage: 88 MB % 27.37/4.32 % (2188762)Instructions burned: 108 (million) % 27.37/4.32 % (2188767)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1065415285:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi) % 27.37/4.32 % (2188764)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3435757748:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi) % 27.37/4.32 % (2188766)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=13547497:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi) % 27.37/4.32 % (2188767)Instruction limit reached! % 27.37/4.32 % (2188767)------------------------------ % 27.37/4.32 % (2188767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.37/4.32 % (2188767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.37/4.32 % (2188767)CaDiCaL version: 2.1.3 % 27.37/4.32 % (2188767)Termination reason: Instruction limit % 27.37/4.32 % (2188767)Termination phase: Saturation % 27.37/4.32 % (2188767)Time elapsed: 0.043 s % 27.37/4.32 % (2188767)Peak memory usage: 90 MB % 27.37/4.32 % (2188767)Instructions burned: 136 (million) % 27.37/4.32 % (2188771)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1183601576:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi) % 27.37/4.32 % (2188764)Instruction limit reached! % 27.37/4.32 % (2188764)------------------------------ % 27.37/4.32 % (2188764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.37/4.32 % (2188764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.37/4.32 % (2188764)CaDiCaL version: 2.1.3 % 27.37/4.32 % (2188764)Termination reason: Instruction limit % 27.37/4.32 % (2188764)Termination phase: Saturation % 27.37/4.32 % (2188764)Time elapsed: 0.130 s % 27.37/4.32 % (2188764)Peak memory usage: 91 MB % 27.37/4.32 % (2188764)Instructions burned: 243 (million) % 27.37/4.32 % (2188771)Instruction limit reached! % 27.37/4.32 % (2188771)------------------------------ % 27.37/4.32 % (2188771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.37/4.32 % (2188771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.37/4.32 % (2188771)CaDiCaL version: 2.1.3 % 27.37/4.32 % (2188771)Termination reason: Instruction limit % 27.37/4.32 % (2188771)Termination phase: Saturation % 27.37/4.32 % (2188771)Time elapsed: 0.101 s % 27.37/4.32 % (2188771)Peak memory usage: 91 MB % 27.37/4.32 % (2188771)Instructions burned: 501 (million) % 27.37/4.32 % (2188773)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1264342442:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi) % 27.37/4.32 % (2188774)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1583364254:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi) % 27.37/4.32 % (2188773)Instruction limit reached! % 27.37/4.32 % (2188773)------------------------------ % 27.37/4.32 % (2188773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.37/4.32 % (2188773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.37/4.32 % (2188773)CaDiCaL version: 2.1.3 % 27.37/4.32 % (2188773)Termination reason: Instruction limit % 27.37/4.32 % (2188773)Termination phase: Saturation % 27.37/4.32 % (2188773)Time elapsed: 0.109 s % 27.37/4.32 % (2188773)Peak memory usage: 90 MB % 27.37/4.32 % (2188773)Instructions burned: 191 (million) % 45.03/6.97 % (2188774)Instruction limit reached! % 45.03/6.97 % (2188774)------------------------------ % 45.03/6.97 % (2188774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.03/6.97 % (2188774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.03/6.97 % (2188774)CaDiCaL version: 2.1.3 % 45.03/6.97 % (2188774)Termination reason: Instruction limit % 45.03/6.97 % (2188774)Termination phase: Saturation % 45.03/6.97 % (2188774)Time elapsed: 0.083 s % 45.03/6.97 % (2188774)Peak memory usage: 91 MB % 45.03/6.97 % (2188774)Instructions burned: 267 (million) % 45.03/6.97 % (2188778)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=1333140862:i=3256:kws=precedence:bd=preordered:av=off_2988 on theBenchmark for (2988ds/3256Mi) % 45.03/6.97 % (2188777)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3920628474:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi) % 45.03/6.97 % (2188777)Instruction limit reached! % 45.03/6.97 % (2188777)------------------------------ % 45.03/6.97 % (2188777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.03/6.97 % (2188777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.03/6.97 % (2188777)CaDiCaL version: 2.1.3 % 45.03/6.97 % (2188777)Termination reason: Instruction limit % 45.03/6.97 % (2188777)Termination phase: Saturation % 45.03/6.97 % (2188777)Time elapsed: 0.094 s % 45.03/6.97 % (2188777)Peak memory usage: 89 MB % 45.03/6.97 % (2188777)Instructions burned: 157 (million) % 45.03/6.97 % (2188781)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2115273144:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi) % 45.03/6.97 % (2188781)Instruction limit reached! % 45.03/6.97 % (2188781)------------------------------ % 45.03/6.97 % (2188781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.03/6.97 % (2188781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.03/6.97 % (2188781)CaDiCaL version: 2.1.3 % 45.03/6.97 % (2188781)Termination reason: Instruction limit % 45.03/6.97 % (2188781)Termination phase: Saturation % 45.03/6.97 % (2188781)Time elapsed: 0.281 s % 45.03/6.97 % (2188781)Peak memory usage: 93 MB % 45.03/6.97 % (2188781)Instructions burned: 537 (million) % 45.03/6.97 % (2188783)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3620378785:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi) % 45.03/6.97 % (2188783)Instruction limit reached! % 45.03/6.97 % (2188783)------------------------------ % 45.03/6.97 % (2188783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.03/6.97 % (2188783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.03/6.97 % (2188783)CaDiCaL version: 2.1.3 % 45.03/6.97 % (2188783)Termination reason: Instruction limit % 45.03/6.97 % (2188783)Termination phase: Saturation % 45.03/6.97 % (2188783)Time elapsed: 0.097 s % 45.03/6.97 % (2188783)Peak memory usage: 89 MB % 45.03/6.97 % (2188783)Instructions burned: 181 (million) % 45.03/6.97 % (2188785)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=701626122:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi) % 45.03/6.97 % (2188778)Instruction limit reached! % 45.03/6.97 % (2188778)------------------------------ % 45.03/6.97 % (2188778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.03/6.97 % (2188778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.03/6.97 % (2188778)CaDiCaL version: 2.1.3 % 45.03/6.97 % (2188778)Termination reason: Instruction limit % 45.03/6.97 % (2188778)Termination phase: Saturation % 45.03/6.97 % (2188778)Time elapsed: 0.944 s % 45.03/6.97 % (2188778)Peak memory usage: 149 MB % 45.03/6.97 % (2188778)Instructions burned: 3259 (million) % 45.03/6.97 % (2188787)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=544265425:i=412:gtgl=4:gtg=exists_all_2978 on theBenchmark for (2978ds/412Mi) % 45.03/6.97 % (2188787)Instruction limit reached! % 45.03/6.97 % (2188787)------------------------------ % 45.03/6.97 % (2188787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.03/6.97 % (2188787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.03/6.97 % (2188787)CaDiCaL version: 2.1.3 % 57.96/8.67 % (2188787)Termination reason: Instruction limit % 57.96/8.67 % (2188787)Termination phase: Saturation % 57.96/8.67 % (2188787)Time elapsed: 0.129 s % 57.96/8.67 % (2188787)Peak memory usage: 95 MB % 57.96/8.67 % (2188787)Instructions burned: 415 (million) % 57.96/8.67 % (2188757)Instruction limit reached! % 57.96/8.67 % (2188757)------------------------------ % 57.96/8.67 % (2188757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.96/8.67 % (2188757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.96/8.67 % (2188757)CaDiCaL version: 2.1.3 % 57.96/8.67 % (2188757)Termination reason: Instruction limit % 57.96/8.67 % (2188757)Termination phase: Saturation % 57.96/8.67 % (2188757)Time elapsed: 1.841 s % 57.96/8.67 % (2188757)Peak memory usage: 144 MB % 57.96/8.67 % (2188757)Instructions burned: 3394 (million) % 57.96/8.67 % (2188789)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=2880920548:s2pl=no:i=8478:s2at=4:nm=6_2976 on theBenchmark for (2976ds/8478Mi) % 57.96/8.67 % (2188790)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=229612570:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2976 on theBenchmark for (2976ds/303Mi) % 57.96/8.67 % (2188790)Refutation not found, incomplete strategy % 57.96/8.67 % (2188790)------------------------------ % 57.96/8.67 % (2188790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.96/8.67 % (2188790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.96/8.67 % (2188790)CaDiCaL version: 2.1.3 % 57.96/8.67 % (2188790)Termination reason: Refutation not found, incomplete strategy % 57.96/8.67 % (2188790)Time elapsed: 0.007 s % 57.96/8.67 % (2188790)Peak memory usage: 88 MB % 57.96/8.67 % (2188790)Instructions burned: 14 (million) % 57.96/8.67 % (2188790)------------------------------ % 57.96/8.67 % (2188790)------------------------------ % 57.96/8.67 % (2188793)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=707558361:st=4:i=720:sd=3:fsr=off:ss=axioms_2972 on theBenchmark for (2972ds/720Mi) % 57.96/8.67 % (2188793)Instruction limit reached! % 57.96/8.67 % (2188793)------------------------------ % 57.96/8.67 % (2188793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.96/8.67 % (2188793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.96/8.67 % (2188793)CaDiCaL version: 2.1.3 % 57.96/8.67 % (2188793)Termination reason: Instruction limit % 57.96/8.67 % (2188793)Termination phase: Saturation % 57.96/8.67 % (2188793)Time elapsed: 0.263 s % 57.96/8.67 % (2188793)Peak memory usage: 90 MB % 57.96/8.67 % (2188793)Instructions burned: 721 (million) % 57.96/8.67 % (2188795)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=192903806:i=598:bs=on:bd=preordered:av=off:ss=axioms_2968 on theBenchmark for (2968ds/598Mi) % 57.96/8.67 % (2188795)Instruction limit reached! % 57.96/8.67 % (2188795)------------------------------ % 57.96/8.67 % (2188795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.96/8.67 % (2188795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.96/8.67 % (2188795)CaDiCaL version: 2.1.3 % 57.96/8.67 % (2188795)Termination reason: Instruction limit % 57.96/8.67 % (2188795)Termination phase: Saturation % 57.96/8.67 % (2188795)Time elapsed: 0.338 s % 57.96/8.67 % (2188795)Peak memory usage: 98 MB % 57.96/8.67 % (2188795)Instructions burned: 600 (million) % 57.96/8.67 % (2188766)Instruction limit reached! % 57.96/8.67 % (2188766)------------------------------ % 57.96/8.67 % (2188766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.96/8.67 % (2188766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.96/8.67 % (2188766)CaDiCaL version: 2.1.3 % 57.96/8.67 % (2188766)Termination reason: Instruction limit % 57.96/8.67 % (2188766)Termination phase: Saturation % 57.96/8.67 % (2188766)Time elapsed: 3.009 s % 57.96/8.67 % (2188766)Peak memory usage: 168 MB % 57.96/8.67 % (2188766)Instructions burned: 5210 (million) % 57.96/8.67 % (2188797)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=166151715:i=2989:sd=3:ss=axioms:sgt=60_2963 on theBenchmark for (2963ds/2989Mi) % 57.96/8.67 % (2188799)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=2915521044:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2962 on theBenchmark for (2962ds/1997Mi) % 87.50/12.81 % (2188799)Instruction limit reached! % 87.50/12.81 % (2188799)------------------------------ % 87.50/12.81 % (2188799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.50/12.81 % (2188799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.50/12.81 % (2188799)CaDiCaL version: 2.1.3 % 87.50/12.81 % (2188799)Termination reason: Instruction limit % 87.50/12.81 % (2188799)Termination phase: Saturation % 87.50/12.81 % (2188799)Time elapsed: 1.274 s % 87.50/12.81 % (2188799)Peak memory usage: 138 MB % 87.50/12.81 % (2188799)Instructions burned: 1998 (million) % 87.50/12.81 % (2188801)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=824575653:i=2088:bd=preordered:av=off_2948 on theBenchmark for (2948ds/2088Mi) % 87.50/12.81 % (2188797)Instruction limit reached! % 87.50/12.81 % (2188797)------------------------------ % 87.50/12.81 % (2188797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.50/12.81 % (2188797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.50/12.81 % (2188797)CaDiCaL version: 2.1.3 % 87.50/12.81 % (2188797)Termination reason: Instruction limit % 87.50/12.81 % (2188797)Termination phase: Saturation % 87.50/12.81 % (2188797)Time elapsed: 1.660 s % 87.50/12.81 % (2188797)Peak memory usage: 144 MB % 87.50/12.81 % (2188797)Instructions burned: 2990 (million) % 87.50/12.81 % (2188789)Instruction limit reached! % 87.50/12.81 % (2188789)------------------------------ % 87.50/12.81 % (2188789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.50/12.81 % (2188789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.50/12.81 % (2188789)CaDiCaL version: 2.1.3 % 87.50/12.81 % (2188789)Termination reason: Instruction limit % 87.50/12.81 % (2188789)Termination phase: Saturation % 87.50/12.81 % (2188789)Time elapsed: 3.048 s % 87.50/12.81 % (2188789)Peak memory usage: 188 MB % 87.50/12.81 % (2188789)Instructions burned: 8480 (million) % 87.50/12.81 % (2188803)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2560862410:i=1098:nicw=on_2945 on theBenchmark for (2945ds/1098Mi) % 87.50/12.81 % (2188804)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1129556995:i=433:bd=preordered_2944 on theBenchmark for (2944ds/433Mi) % 87.50/12.81 % (2188804)Refutation not found, incomplete strategy % 87.50/12.81 % (2188804)------------------------------ % 87.50/12.81 % (2188804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.50/12.81 % (2188804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.50/12.81 % (2188804)CaDiCaL version: 2.1.3 % 87.50/12.81 % (2188804)Termination reason: Refutation not found, incomplete strategy % 87.50/12.81 % (2188804)Time elapsed: 0.002 s % 87.50/12.81 % (2188804)Peak memory usage: 88 MB % 87.50/12.81 % (2188804)Instructions burned: 7 (million) % 87.50/12.81 % (2188804)------------------------------ % 87.50/12.81 % (2188804)------------------------------ % 87.50/12.81 % (2188807)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1210311326:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2942 on theBenchmark for (2942ds/2942Mi) % 87.50/12.81 % (2188803)Instruction limit reached! % 87.50/12.81 % (2188803)------------------------------ % 87.50/12.81 % (2188803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.50/12.81 % (2188803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.50/12.81 % (2188803)CaDiCaL version: 2.1.3 % 87.50/12.81 % (2188803)Termination reason: Instruction limit % 87.50/12.81 % (2188803)Termination phase: Saturation % 87.50/12.81 % (2188803)Time elapsed: 0.501 s % 87.50/12.81 % (2188803)Peak memory usage: 103 MB % 87.50/12.81 % (2188803)Instructions burned: 1100 (million) % 87.50/12.81 % (2188809)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=4264726886:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2939 on theBenchmark for (2939ds/6922Mi) % 87.50/12.81 % (2188801)Instruction limit reached! % 87.50/12.81 % (2188801)------------------------------ % 87.50/12.81 % (2188801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.50/12.81 % (2188801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.91 % (2188801)CaDiCaL version: 2.1.3 % 102.48/14.91 % (2188801)Termination reason: Instruction limit % 102.48/14.91 % (2188801)Termination phase: Saturation % 102.48/14.91 % (2188801)Time elapsed: 1.233 s % 102.48/14.91 % (2188801)Peak memory usage: 139 MB % 102.48/14.91 % (2188801)Instructions burned: 2089 (million) % 102.48/14.91 % (2188811)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=2315731959:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2934 on theBenchmark for (2934ds/596Mi) % 102.48/14.91 % (2188811)Refutation not found, incomplete strategy % 102.48/14.91 % (2188811)------------------------------ % 102.48/14.91 % (2188811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/14.91 % (2188811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.91 % (2188811)CaDiCaL version: 2.1.3 % 102.48/14.91 % (2188811)Termination reason: Refutation not found, incomplete strategy % 102.48/14.91 % (2188811)Time elapsed: 0.004 s % 102.48/14.91 % (2188811)Peak memory usage: 88 MB % 102.48/14.91 % (2188811)Instructions burned: 7 (million) % 102.48/14.91 % (2188807)Instruction limit reached! % 102.48/14.91 % (2188807)------------------------------ % 102.48/14.91 % (2188807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/14.91 % (2188807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.91 % (2188807)CaDiCaL version: 2.1.3 % 102.48/14.91 % (2188807)Termination reason: Instruction limit % 102.48/14.91 % (2188807)Termination phase: Saturation % 102.48/14.91 % (2188807)Time elapsed: 0.960 s % 102.48/14.91 % (2188807)Peak memory usage: 144 MB % 102.48/14.91 % (2188807)Instructions burned: 2944 (million) % 102.48/14.91 % (2188785)Instruction limit reached! % 102.48/14.91 % (2188785)------------------------------ % 102.48/14.91 % (2188785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/14.91 % (2188785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.91 % (2188785)CaDiCaL version: 2.1.3 % 102.48/14.91 % (2188785)Termination reason: Instruction limit % 102.48/14.91 % (2188785)Termination phase: Saturation % 102.48/14.91 % (2188785)Time elapsed: 4.752 s % 102.48/14.91 % (2188785)Peak memory usage: 148 MB % 102.48/14.91 % (2188785)Instructions burned: 10310 (million) % 102.48/14.91 % (2188813)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=3284898809:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2931 on theBenchmark for (2931ds/4123Mi) % 102.48/14.91 % (2188811)------------------------------ % 102.48/14.91 % (2188811)------------------------------ % 102.48/14.91 % (2188814)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=226224749:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2931 on theBenchmark for (2931ds/16411Mi) % 102.48/14.91 % (2188816)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3209284820:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2930 on theBenchmark for (2930ds/1670Mi) % 102.48/14.91 % (2188813)Instruction limit reached! % 102.48/14.91 % (2188813)------------------------------ % 102.48/14.91 % (2188813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/14.91 % (2188813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.91 % (2188813)CaDiCaL version: 2.1.3 % 102.48/14.91 % (2188813)Termination reason: Instruction limit % 102.48/14.91 % (2188813)Termination phase: Saturation % 102.48/14.91 % (2188813)Time elapsed: 1.114 s % 102.48/14.91 % (2188813)Peak memory usage: 141 MB % 102.48/14.91 % (2188813)Instructions burned: 4128 (million) % 102.48/14.91 % (2188819)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=2547348357:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2919 on theBenchmark for (2919ds/1722Mi) % 102.48/14.91 % (2188816)Instruction limit reached! % 102.48/14.91 % (2188816)------------------------------ % 102.48/14.91 % (2188816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/14.91 % (2188816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/14.91 % (2188816)CaDiCaL version: 2.1.3 % 102.48/14.91 % (2188816)Termination reason: Instruction limit % 102.48/14.91 % (2188816)Termination phase: Saturation % 102.48/14.91 % (2188816)Time elapsed: 1.042 s % 102.48/14.91 % (2188816)Peak memory usage: 134 MB % 102.48/14.91 % (2188816)Instructions burned: 1671 (million) % 102.48/14.91 % (2188821)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=2938260887:cts=off:cond=on:i=9530:bs=on:fsd=on_2918 on theBenchmark for (2918ds/9530Mi) % 125.82/18.18 % (2188819)Instruction limit reached! % 125.82/18.18 % (2188819)------------------------------ % 125.82/18.18 % (2188819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.82/18.18 % (2188819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.82/18.18 % (2188819)CaDiCaL version: 2.1.3 % 125.82/18.18 % (2188819)Termination reason: Instruction limit % 125.82/18.18 % (2188819)Termination phase: Saturation % 125.82/18.18 % (2188819)Time elapsed: 0.565 s % 125.82/18.18 % (2188819)Peak memory usage: 129 MB % 125.82/18.18 % (2188819)Instructions burned: 1724 (million) % 125.82/18.18 % (2188823)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2749871161:st=2:i=4495:sd=10:ss=included_2913 on theBenchmark for (2913ds/4495Mi) % 125.82/18.18 % (2188809)Instruction limit reached! % 125.82/18.18 % (2188809)------------------------------ % 125.82/18.18 % (2188809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.82/18.18 % (2188809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.82/18.18 % (2188809)CaDiCaL version: 2.1.3 % 125.82/18.18 % (2188809)Termination reason: Instruction limit % 125.82/18.18 % (2188809)Termination phase: Saturation % 125.82/18.18 % (2188809)Time elapsed: 3.570 s % 125.82/18.18 % (2188809)Peak memory usage: 177 MB % 125.82/18.18 % (2188809)Instructions burned: 6922 (million) % 125.82/18.18 % (2188825)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=2197954087:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2902 on theBenchmark for (2902ds/4920Mi) % 125.82/18.18 % (2188823)Instruction limit reached! % 125.82/18.18 % (2188823)------------------------------ % 125.82/18.18 % (2188823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.82/18.18 % (2188823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.82/18.18 % (2188823)CaDiCaL version: 2.1.3 % 125.82/18.18 % (2188823)Termination reason: Instruction limit % 125.82/18.18 % (2188823)Termination phase: Saturation % 125.82/18.18 % (2188823)Time elapsed: 1.368 s % 125.82/18.18 % (2188823)Peak memory usage: 159 MB % 125.82/18.18 % (2188823)Instructions burned: 4498 (million) % 125.82/18.18 % (2188827)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=1769946627:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2898 on theBenchmark for (2898ds/2083Mi) % 125.82/18.18 % (2188827)Instruction limit reached! % 125.82/18.18 % (2188827)------------------------------ % 125.82/18.18 % (2188827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.82/18.18 % (2188827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.82/18.18 % (2188827)CaDiCaL version: 2.1.3 % 125.82/18.18 % (2188827)Termination reason: Instruction limit % 125.82/18.18 % (2188827)Termination phase: Saturation % 125.82/18.18 % (2188827)Time elapsed: 0.648 s % 125.82/18.18 % (2188827)Peak memory usage: 134 MB % 125.82/18.18 % (2188827)Instructions burned: 2086 (million) % 125.82/18.18 % (2188829)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=2922229572:i=4629:av=off:gsp=on_2891 on theBenchmark for (2891ds/4629Mi) % 125.82/18.18 % (2188825)Instruction limit reached! % 125.82/18.18 % (2188825)------------------------------ % 125.82/18.18 % (2188825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.82/18.18 % (2188825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.82/18.18 % (2188825)CaDiCaL version: 2.1.3 % 125.82/18.18 % (2188825)Termination reason: Instruction limit % 125.82/18.18 % (2188825)Termination phase: Saturation % 125.82/18.18 % (2188825)Time elapsed: 2.007 s % 125.82/18.18 % (2188825)Peak memory usage: 162 MB % 125.82/18.18 % (2188825)Instructions burned: 4922 (million) % 125.82/18.18 % (2188831)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=578715097:i=1258:av=off_2880 on theBenchmark for (2880ds/1258Mi) % 125.82/18.18 % (2188831)Instruction limit reached! % 125.82/18.18 % (2188831)------------------------------ % 125.82/18.18 % (2188831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.33/24.50 % (2188831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.33/24.50 % (2188831)CaDiCaL version: 2.1.3 % 170.33/24.50 % (2188831)Termination reason: Instruction limit % 170.33/24.50 % (2188831)Termination phase: Saturation % 170.33/24.50 % (2188831)Time elapsed: 0.380 s % 170.33/24.50 % (2188831)Peak memory usage: 100 MB % 170.33/24.50 % (2188831)Instructions burned: 1261 (million) % 170.33/24.50 % (2188833)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2933843147:i=7343:av=off:ss=included_2876 on theBenchmark for (2876ds/7343Mi) % 170.33/24.50 % (2188829)Instruction limit reached! % 170.33/24.50 % (2188829)------------------------------ % 170.33/24.50 % (2188829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.33/24.50 % (2188829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.33/24.50 % (2188829)CaDiCaL version: 2.1.3 % 170.33/24.50 % (2188829)Termination reason: Instruction limit % 170.33/24.50 % (2188829)Termination phase: Saturation % 170.33/24.50 % (2188829)Time elapsed: 1.748 s % 170.33/24.50 % (2188829)Peak memory usage: 142 MB % 170.33/24.50 % (2188829)Instructions burned: 4630 (million) % 170.33/24.50 % (2188835)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3500496592:i=1325:sd=2:ss=axioms:sgt=16_2872 on theBenchmark for (2872ds/1325Mi) % 170.33/24.50 % (2188821)Instruction limit reached! % 170.33/24.50 % (2188821)------------------------------ % 170.33/24.50 % (2188821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.33/24.50 % (2188821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.33/24.50 % (2188821)CaDiCaL version: 2.1.3 % 170.33/24.50 % (2188821)Termination reason: Instruction limit % 170.33/24.50 % (2188821)Termination phase: Saturation % 170.33/24.50 % (2188821)Time elapsed: 4.810 s % 170.33/24.50 % (2188821)Peak memory usage: 145 MB % 170.33/24.50 % (2188821)Instructions burned: 9532 (million) % 170.33/24.50 % (2188848)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=233213909:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2869 on theBenchmark for (2869ds/2646Mi) % 170.33/24.50 % (2188835)Instruction limit reached! % 170.33/24.50 % (2188835)------------------------------ % 170.33/24.50 % (2188835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.33/24.50 % (2188835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.33/24.50 % (2188835)CaDiCaL version: 2.1.3 % 170.33/24.50 % (2188835)Termination reason: Instruction limit % 170.33/24.50 % (2188835)Termination phase: Saturation % 170.33/24.50 % (2188835)Time elapsed: 0.536 s % 170.33/24.50 % (2188835)Peak memory usage: 92 MB % 170.33/24.50 % (2188835)Instructions burned: 1326 (million) % 170.33/24.50 % (2188965)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3800740581:i=1489:sd=2:ep=R:ss=axioms_2866 on theBenchmark for (2866ds/1489Mi) % 170.33/24.50 % (2188965)Refutation not found, incomplete strategy % 170.33/24.50 % (2188965)------------------------------ % 170.33/24.50 % (2188965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.33/24.50 % (2188965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.33/24.50 % (2188965)CaDiCaL version: 2.1.3 % 170.33/24.50 % (2188965)Termination reason: Refutation not found, incomplete strategy % 170.33/24.50 % (2188965)Time elapsed: 0.614 s % 170.33/24.50 % (2188965)Peak memory usage: 128 MB % 170.33/24.50 % (2188965)Instructions burned: 916 (million) % 170.33/24.50 % (2188833)Instruction limit reached! % 170.33/24.50 % (2188833)------------------------------ % 170.33/24.50 % (2188833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.33/24.50 % (2188833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.33/24.50 % (2188833)CaDiCaL version: 2.1.3 % 170.33/24.50 % (2188833)Termination reason: Instruction limit % 170.33/24.50 % (2188833)Termination phase: Saturation % 170.33/24.50 % (2188833)Time elapsed: 1.734 s % 170.33/24.50 % (2188833)Peak memory usage: 142 MB % 170.33/24.50 % (2188833)Instructions burned: 7348 (million) % 170.33/24.50 % (2189095)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=4110902184:i=1503_2857 on theBenchmark for (2857ds/1503Mi) % 170.33/24.50 % (2188965)------------------------------ % 170.33/24.50 % (2188965)------------------------------ % 170.33/24.50 % (2189106)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2728315842:i=13942:kws=frequency_2856 on theBenchmark for (2856ds/13942Mi) % 213.69/30.57 % (2188848)Instruction limit reached! % 213.69/30.57 % (2188848)------------------------------ % 213.69/30.57 % (2188848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.69/30.57 % (2188848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.69/30.57 % (2188848)CaDiCaL version: 2.1.3 % 213.69/30.57 % (2188848)Termination reason: Instruction limit % 213.69/30.57 % (2188848)Termination phase: Saturation % 213.69/30.57 % (2188848)Time elapsed: 1.483 s % 213.69/30.57 % (2188848)Peak memory usage: 136 MB % 213.69/30.57 % (2188848)Instructions burned: 2646 (million) % 213.69/30.57 % (2189095)Instruction limit reached! % 213.69/30.57 % (2189095)------------------------------ % 213.69/30.57 % (2189095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.69/30.57 % (2189095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.69/30.57 % (2189095)CaDiCaL version: 2.1.3 % 213.69/30.57 % (2189095)Termination reason: Instruction limit % 213.69/30.57 % (2189095)Termination phase: Saturation % 213.69/30.57 % (2189095)Time elapsed: 0.484 s % 213.69/30.57 % (2189095)Peak memory usage: 135 MB % 213.69/30.57 % (2189095)Instructions burned: 1503 (million) % 213.69/30.57 % (2189108)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=2675203533:i=3604:fsr=off:er=filter_2853 on theBenchmark for (2853ds/3604Mi) % 213.69/30.57 % (2189109)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2634931947:i=1876:sd=1:ss=included:sgt=32_2851 on theBenchmark for (2851ds/1876Mi) % 213.69/30.57 % (2189109)Instruction limit reached! % 213.69/30.57 % (2189109)------------------------------ % 213.69/30.57 % (2189109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.69/30.57 % (2189109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.69/30.57 % (2189109)CaDiCaL version: 2.1.3 % 213.69/30.57 % (2189109)Termination reason: Instruction limit % 213.69/30.57 % (2189109)Termination phase: Saturation % 213.69/30.57 % (2189109)Time elapsed: 0.898 s % 213.69/30.57 % (2189109)Peak memory usage: 136 MB % 213.69/30.57 % (2189109)Instructions burned: 1878 (million) % 213.69/30.57 % (2189137)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1350392823:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2841 on theBenchmark for (2841ds/1932Mi) % 213.69/30.57 % (2189137)Refutation not found, incomplete strategy % 213.69/30.57 % (2189137)------------------------------ % 213.69/30.57 % (2189137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.69/30.57 % (2189137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.69/30.57 % (2189137)CaDiCaL version: 2.1.3 % 213.69/30.57 % (2189137)Termination reason: Refutation not found, incomplete strategy % 213.69/30.57 % (2189137)Time elapsed: 0.535 s % 213.69/30.57 % (2189137)Peak memory usage: 128 MB % 213.69/30.57 % (2189137)Instructions burned: 888 (million) % 213.69/30.57 % (2188814)Instruction limit reached! % 213.69/30.57 % (2188814)------------------------------ % 213.69/30.57 % (2188814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.69/30.57 % (2188814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.69/30.57 % (2188814)CaDiCaL version: 2.1.3 % 213.69/30.57 % (2188814)Termination reason: Instruction limit % 213.69/30.57 % (2188814)Termination phase: Saturation % 213.69/30.57 % (2188814)Time elapsed: 9.470 s % 213.69/30.57 % (2188814)Peak memory usage: 269 MB % 213.69/30.57 % (2188814)Instructions burned: 16411 (million) % 213.69/30.57 % (2189150)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=2228999700:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2834 on theBenchmark for (2834ds/1980Mi) % 213.69/30.57 % (2189137)------------------------------ % 213.69/30.57 % (2189137)------------------------------ % 213.69/30.57 % (2189156)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=2824480619:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2831 on theBenchmark for (2831ds/3902Mi) % 213.69/30.57 % (2189108)Instruction limit reached! % 213.69/30.57 % (2189108)------------------------------ % 213.69/30.57 % (2189108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.76/37.34 % (2189108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.76/37.34 % (2189108)CaDiCaL version: 2.1.3 % 261.76/37.34 % (2189108)Termination reason: Instruction limit % 261.76/37.34 % (2189108)Termination phase: Saturation % 261.76/37.34 % (2189108)Time elapsed: 2.956 s % 261.76/37.34 % (2189108)Peak memory usage: 132 MB % 261.76/37.34 % (2189108)Instructions burned: 3604 (million) % 261.76/37.34 % (2189167)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1761270546:avsq=on:i=3916:aac=none:amm=off_2822 on theBenchmark for (2822ds/3916Mi) % 261.76/37.34 % (2189150)Instruction limit reached! % 261.76/37.34 % (2189150)------------------------------ % 261.76/37.34 % (2189150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.76/37.34 % (2189150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.76/37.34 % (2189150)CaDiCaL version: 2.1.3 % 261.76/37.34 % (2189150)Termination reason: Instruction limit % 261.76/37.34 % (2189150)Termination phase: Saturation % 261.76/37.34 % (2189150)Time elapsed: 1.857 s % 261.76/37.34 % (2189150)Peak memory usage: 137 MB % 261.76/37.34 % (2189150)Instructions burned: 1980 (million) % 261.76/37.34 % (2189171)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=6248279:cond=on:i=3940:av=off:er=known_2814 on theBenchmark for (2814ds/3940Mi) % 261.76/37.34 % (2189156)Instruction limit reached! % 261.76/37.34 % (2189156)------------------------------ % 261.76/37.34 % (2189156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.76/37.34 % (2189156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.76/37.34 % (2189156)CaDiCaL version: 2.1.3 % 261.76/37.34 % (2189156)Termination reason: Instruction limit % 261.76/37.34 % (2189156)Termination phase: Saturation % 261.76/37.34 % (2189156)Time elapsed: 3.592 s % 261.76/37.34 % (2189156)Peak memory usage: 149 MB % 261.76/37.34 % (2189156)Instructions burned: 3902 (million) % 261.76/37.34 % (2189185)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2114162337:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2793 on theBenchmark for (2793ds/3980Mi) % 261.76/37.34 % (2189167)Instruction limit reached! % 261.76/37.34 % (2189167)------------------------------ % 261.76/37.34 % (2189167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.76/37.34 % (2189167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.76/37.34 % (2189167)CaDiCaL version: 2.1.3 % 261.76/37.34 % (2189167)Termination reason: Instruction limit % 261.76/37.34 % (2189167)Termination phase: Saturation % 261.76/37.34 % (2189167)Time elapsed: 3.693 s % 261.76/37.34 % (2189167)Peak memory usage: 118 MB % 261.76/37.34 % (2189167)Instructions burned: 3916 (million) % 261.76/37.34 % (2189191)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=3657794720:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2782 on theBenchmark for (2782ds/2087Mi) % 261.76/37.34 % (2189171)Instruction limit reached! % 261.76/37.34 % (2189171)------------------------------ % 261.76/37.34 % (2189171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.76/37.34 % (2189171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.76/37.34 % (2189171)CaDiCaL version: 2.1.3 % 261.76/37.34 % (2189171)Termination reason: Instruction limit % 261.76/37.34 % (2189171)Termination phase: Saturation % 261.76/37.34 % (2189171)Time elapsed: 3.897 s % 261.76/37.34 % (2189171)Peak memory usage: 152 MB % 261.76/37.34 % (2189171)Instructions burned: 3940 (million) % 261.76/37.34 % (2189195)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=2611410642:cts=off:cond=on:i=4272:bs=on:fsd=on_2772 on theBenchmark for (2772ds/4272Mi) % 261.76/37.34 % (2189191)Instruction limit reached! % 261.76/37.34 % (2189191)------------------------------ % 261.76/37.34 % (2189191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.76/37.34 % (2189191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.76/37.34 % (2189191)CaDiCaL version: 2.1.3 % 261.76/37.34 % (2189191)Termination reason: Instruction limit % 261.76/37.34 % (2189191)Termination phase: Saturation % 261.76/37.34 % (2189191)Time elapsed: 2.154 s % 261.76/37.34 % (2189191)Peak memorTerminated %------------------------------------------------------------------------------