%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC278-1 : TPTP v9.3.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n016.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:03:15 PM UTC 2026 % Result : Timeout 300.92s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWC278-1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.18 % Computer : n016.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 08:55:33 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.22 Running first-order theorem proving % 0.09/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 % 6.61/1.79 % (3488794)Input is clausal, will run a generic CNF schedule. % 6.61/1.79 % (3488805)dis-21_1_sil=8000:lcm=predicate:random_seed=3952161914: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) % 6.61/1.79 % (3488805)Instruction limit reached! % 6.61/1.79 % (3488805)------------------------------ % 6.61/1.79 % (3488805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.79 % (3488805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.79 % (3488805)CaDiCaL version: 2.1.3 % 6.61/1.79 % (3488805)Termination reason: Instruction limit % 6.61/1.79 % (3488805)Termination phase: Saturation % 6.61/1.79 % (3488805)Time elapsed: 0.030 s % 6.61/1.79 % (3488805)Peak memory usage: 89 MB % 6.61/1.79 % (3488805)Instructions burned: 120 (million) % 6.61/1.79 % (3488800)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=430793237:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 6.61/1.79 % (3488803)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=449303643:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 6.61/1.79 % (3488802)lrs+10_1_sil=8000:sp=occurrence:random_seed=2699197487:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 6.61/1.79 % (3488801)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3265842764:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 6.61/1.79 % (3488804)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2773505363:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 6.61/1.79 % (3488799)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=1972581298:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 6.61/1.79 % (3488802)Instruction limit reached! % 6.61/1.79 % (3488802)------------------------------ % 6.61/1.79 % (3488802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.79 % (3488802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.79 % (3488802)CaDiCaL version: 2.1.3 % 6.61/1.79 % (3488802)Termination reason: Instruction limit % 6.61/1.79 % (3488802)Termination phase: Saturation % 6.61/1.79 % (3488802)Time elapsed: 0.065 s % 6.61/1.79 % (3488802)Peak memory usage: 90 MB % 6.61/1.79 % (3488802)Instructions burned: 108 (million) % 6.61/1.79 % (3488803)Instruction limit reached! % 6.61/1.79 % (3488803)------------------------------ % 6.61/1.79 % (3488803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.79 % (3488803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.79 % (3488803)CaDiCaL version: 2.1.3 % 6.61/1.79 % (3488803)Termination reason: Instruction limit % 6.61/1.79 % (3488803)Termination phase: Saturation % 6.61/1.79 % (3488803)Time elapsed: 0.069 s % 6.61/1.79 % (3488803)Peak memory usage: 89 MB % 6.61/1.79 % (3488803)Instructions burned: 114 (million) % 6.61/1.79 % (3488807)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=3069719549:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 6.61/1.79 % (3488804)Instruction limit reached! % 6.61/1.79 % (3488804)------------------------------ % 6.61/1.79 % (3488804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.79 % (3488804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.79 % (3488804)CaDiCaL version: 2.1.3 % 6.61/1.79 % (3488804)Termination reason: Instruction limit % 6.61/1.79 % (3488804)Termination phase: Saturation % 6.61/1.79 % (3488804)Time elapsed: 0.121 s % 6.61/1.79 % (3488804)Peak memory usage: 90 MB % 6.61/1.79 % (3488804)Instructions burned: 180 (million) % 6.61/1.79 % (3488807)Instruction limit reached! % 6.61/1.79 % (3488807)------------------------------ % 6.61/1.79 % (3488807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.61/1.79 % (3488807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.61/1.79 % (3488807)CaDiCaL version: 2.1.3 % 6.61/1.79 % (3488807)Termination reason: Instruction limit % 6.61/1.79 % (3488807)Termination phase: Saturation % 6.61/1.79 % (3488807)Time elapsed: 0.051 s % 6.61/1.79 % (3488807)Peak memory usage: 90 MB % 6.61/1.79 % (3488807)Instructions burned: 144 (million) % 6.61/1.79 % (3488814)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3160751876:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi) % 20.95/3.66 % (3488815)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3318493547:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 20.95/3.66 % (3488818)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4029223416:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi) % 20.95/3.66 % (3488817)lrs+10_64_to=lpo:sil=8000:random_seed=2472329309:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 20.95/3.66 % (3488814)Instruction limit reached! % 20.95/3.66 % (3488814)------------------------------ % 20.95/3.66 % (3488814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.95/3.66 % (3488814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.66 % (3488814)CaDiCaL version: 2.1.3 % 20.95/3.66 % (3488814)Termination reason: Instruction limit % 20.95/3.66 % (3488814)Termination phase: Saturation % 20.95/3.66 % (3488814)Time elapsed: 0.101 s % 20.95/3.66 % (3488814)Peak memory usage: 91 MB % 20.95/3.66 % (3488814)Instructions burned: 189 (million) % 20.95/3.66 % (3488818)Instruction limit reached! % 20.95/3.66 % (3488818)------------------------------ % 20.95/3.66 % (3488818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.95/3.66 % (3488818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.66 % (3488818)CaDiCaL version: 2.1.3 % 20.95/3.66 % (3488818)Termination reason: Instruction limit % 20.95/3.66 % (3488818)Termination phase: Saturation % 20.95/3.66 % (3488818)Time elapsed: 0.064 s % 20.95/3.66 % (3488818)Peak memory usage: 90 MB % 20.95/3.66 % (3488818)Instructions burned: 196 (million) % 20.95/3.66 % (3488817)Instruction limit reached! % 20.95/3.66 % (3488817)------------------------------ % 20.95/3.66 % (3488817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.95/3.66 % (3488817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.66 % (3488817)CaDiCaL version: 2.1.3 % 20.95/3.66 % (3488817)Termination reason: Instruction limit % 20.95/3.66 % (3488817)Termination phase: Saturation % 20.95/3.66 % (3488817)Time elapsed: 0.066 s % 20.95/3.66 % (3488817)Peak memory usage: 90 MB % 20.95/3.66 % (3488817)Instructions burned: 127 (million) % 20.95/3.66 % (3488815)Instruction limit reached! % 20.95/3.66 % (3488815)------------------------------ % 20.95/3.66 % (3488815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.95/3.66 % (3488815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.66 % (3488815)CaDiCaL version: 2.1.3 % 20.95/3.66 % (3488815)Termination reason: Instruction limit % 20.95/3.66 % (3488815)Termination phase: Saturation % 20.95/3.66 % (3488815)Time elapsed: 0.131 s % 20.95/3.66 % (3488815)Peak memory usage: 90 MB % 20.95/3.66 % (3488815)Instructions burned: 219 (million) % 20.95/3.66 % (3488823)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1342619109:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 20.95/3.66 % (3488824)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=261511976:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi) % 20.95/3.66 % (3488823)Instruction limit reached! % 20.95/3.66 % (3488823)------------------------------ % 20.95/3.66 % (3488823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.95/3.66 % (3488823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.95/3.66 % (3488823)CaDiCaL version: 2.1.3 % 20.95/3.66 % (3488823)Termination reason: Instruction limit % 20.95/3.66 % (3488823)Termination phase: Saturation % 20.95/3.66 % (3488823)Time elapsed: 0.053 s % 20.95/3.66 % (3488823)Peak memory usage: 91 MB % 20.95/3.66 % (3488823)Instructions burned: 158 (million) % 20.95/3.66 % (3488825)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=3700096492:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi) % 20.95/3.66 % (3488826)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=373755096:i=107_2995 on theBenchmark for (2995ds/107Mi) % 20.95/3.66 % (3488825)Instruction limit reached! % 20.95/3.66 % (3488825)------------------------------ % 20.95/3.66 % (3488825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.41/5.09 % (3488825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.41/5.09 % (3488825)CaDiCaL version: 2.1.3 % 31.41/5.09 % (3488825)Termination reason: Instruction limit % 31.41/5.09 % (3488825)Termination phase: Saturation % 31.41/5.09 % (3488825)Time elapsed: 0.057 s % 31.41/5.09 % (3488825)Peak memory usage: 90 MB % 31.41/5.09 % (3488825)Instructions burned: 107 (million) % 31.41/5.09 % (3488829)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=980118032:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi) % 31.41/5.09 % (3488826)Instruction limit reached! % 31.41/5.09 % (3488826)------------------------------ % 31.41/5.09 % (3488826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.41/5.09 % (3488826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.41/5.09 % (3488826)CaDiCaL version: 2.1.3 % 31.41/5.09 % (3488826)Termination reason: Instruction limit % 31.41/5.09 % (3488826)Termination phase: Saturation % 31.41/5.09 % (3488826)Time elapsed: 0.068 s % 31.41/5.09 % (3488826)Peak memory usage: 90 MB % 31.41/5.09 % (3488826)Instructions burned: 107 (million) % 31.41/5.09 % (3488829)Instruction limit reached! % 31.41/5.09 % (3488829)------------------------------ % 31.41/5.09 % (3488829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.41/5.09 % (3488829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.41/5.09 % (3488829)CaDiCaL version: 2.1.3 % 31.41/5.09 % (3488829)Termination reason: Instruction limit % 31.41/5.09 % (3488829)Termination phase: Saturation % 31.41/5.09 % (3488829)Time elapsed: 0.083 s % 31.41/5.09 % (3488829)Peak memory usage: 89 MB % 31.41/5.09 % (3488829)Instructions burned: 243 (million) % 31.41/5.09 % (3488832)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2707483442:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi) % 31.41/5.09 % (3488834)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1724029871:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi) % 31.41/5.09 % (3488835)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1699280232:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi) % 31.41/5.09 % (3488834)Instruction limit reached! % 31.41/5.09 % (3488834)------------------------------ % 31.41/5.09 % (3488834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.41/5.09 % (3488834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.41/5.09 % (3488834)CaDiCaL version: 2.1.3 % 31.41/5.09 % (3488834)Termination reason: Instruction limit % 31.41/5.09 % (3488834)Termination phase: Saturation % 31.41/5.09 % (3488834)Time elapsed: 0.088 s % 31.41/5.09 % (3488834)Peak memory usage: 90 MB % 31.41/5.09 % (3488834)Instructions burned: 136 (million) % 31.41/5.09 % (3488835)Instruction limit reached! % 31.41/5.09 % (3488835)------------------------------ % 31.41/5.09 % (3488835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.41/5.09 % (3488835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.41/5.09 % (3488835)CaDiCaL version: 2.1.3 % 31.41/5.09 % (3488835)Termination reason: Instruction limit % 31.41/5.09 % (3488835)Termination phase: Saturation % 31.41/5.09 % (3488835)Time elapsed: 0.119 s % 31.41/5.09 % (3488835)Peak memory usage: 94 MB % 31.41/5.09 % (3488835)Instructions burned: 500 (million) % 31.41/5.09 % (3488839)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3836537847:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi) % 31.41/5.09 % (3488840)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1145974960:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi) % 31.41/5.09 % (3488840)Instruction limit reached! % 31.41/5.09 % (3488840)------------------------------ % 31.41/5.09 % (3488840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.41/5.09 % (3488840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.41/5.09 % (3488840)CaDiCaL version: 2.1.3 % 31.41/5.09 % (3488840)Termination reason: Instruction limit % 31.41/5.09 % (3488840)Termination phase: Saturation % 31.41/5.09 % (3488840)Time elapsed: 0.077 s % 31.41/5.09 % (3488840)Peak memory usage: 91 MB % 31.41/5.09 % (3488840)Instructions burned: 267 (million) % 31.41/5.09 % (3488839)Instruction limit reached! % 31.41/5.09 % (3488839)------------------------------ % 41.54/6.59 % (3488839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.59 % (3488839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.59 % (3488839)CaDiCaL version: 2.1.3 % 41.54/6.59 % (3488839)Termination reason: Instruction limit % 41.54/6.59 % (3488839)Termination phase: Saturation % 41.54/6.59 % (3488839)Time elapsed: 0.108 s % 41.54/6.59 % (3488839)Peak memory usage: 92 MB % 41.54/6.59 % (3488839)Instructions burned: 191 (million) % 41.54/6.59 % (3488843)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1487305500:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi) % 41.54/6.59 % (3488843)Instruction limit reached! % 41.54/6.59 % (3488843)------------------------------ % 41.54/6.59 % (3488843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.59 % (3488843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.59 % (3488843)CaDiCaL version: 2.1.3 % 41.54/6.59 % (3488843)Termination reason: Instruction limit % 41.54/6.59 % (3488843)Termination phase: Saturation % 41.54/6.59 % (3488843)Time elapsed: 0.051 s % 41.54/6.59 % (3488843)Peak memory usage: 90 MB % 41.54/6.59 % (3488843)Instructions burned: 156 (million) % 41.54/6.59 % (3488844)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=4276284009:i=3256:kws=precedence:bd=preordered:av=off_2988 on theBenchmark for (2988ds/3256Mi) % 41.54/6.59 % (3488846)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=715406150:i=537:av=off:ss=included_2987 on theBenchmark for (2987ds/537Mi) % 41.54/6.59 % (3488846)Instruction limit reached! % 41.54/6.59 % (3488846)------------------------------ % 41.54/6.59 % (3488846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.59 % (3488846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.59 % (3488846)CaDiCaL version: 2.1.3 % 41.54/6.59 % (3488846)Termination reason: Instruction limit % 41.54/6.59 % (3488846)Termination phase: Saturation % 41.54/6.59 % (3488846)Time elapsed: 0.138 s % 41.54/6.59 % (3488846)Peak memory usage: 93 MB % 41.54/6.59 % (3488846)Instructions burned: 538 (million) % 41.54/6.59 % (3488849)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1338228048:i=180:bd=preordered:av=off_2985 on theBenchmark for (2985ds/180Mi) % 41.54/6.59 % (3488849)Instruction limit reached! % 41.54/6.59 % (3488849)------------------------------ % 41.54/6.59 % (3488849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.59 % (3488849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.59 % (3488849)CaDiCaL version: 2.1.3 % 41.54/6.59 % (3488849)Termination reason: Instruction limit % 41.54/6.59 % (3488849)Termination phase: Saturation % 41.54/6.59 % (3488849)Time elapsed: 0.066 s % 41.54/6.59 % (3488849)Peak memory usage: 90 MB % 41.54/6.59 % (3488849)Instructions burned: 181 (million) % 41.54/6.59 % (3488851)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=4141026775:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2983 on theBenchmark for (2983ds/10307Mi) % 41.54/6.59 % (3488824)Instruction limit reached! % 41.54/6.59 % (3488824)------------------------------ % 41.54/6.59 % (3488824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.59 % (3488824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.59 % (3488824)CaDiCaL version: 2.1.3 % 41.54/6.59 % (3488824)Termination reason: Instruction limit % 41.54/6.59 % (3488824)Termination phase: Saturation % 41.54/6.59 % (3488824)Time elapsed: 2.065 s % 41.54/6.59 % (3488824)Peak memory usage: 153 MB % 41.54/6.59 % (3488824)Instructions burned: 3395 (million) % 41.54/6.59 % (3488853)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=4043624605:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi) % 41.54/6.59 % (3488853)Instruction limit reached! % 41.54/6.59 % (3488853)------------------------------ % 41.54/6.59 % (3488853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.54/6.59 % (3488853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.54/6.59 % (3488853)CaDiCaL version: 2.1.3 % 41.54/6.59 % (3488853)Termination reason: Instruction limit % 41.54/6.59 % (3488853)Termination phase: Saturation % 63.80/9.74 % (3488853)Time elapsed: 0.218 s % 63.80/9.74 % (3488853)Peak memory usage: 91 MB % 63.80/9.74 % (3488853)Instructions burned: 413 (million) % 63.80/9.74 % (3488844)Instruction limit reached! % 63.80/9.74 % (3488844)------------------------------ % 63.80/9.74 % (3488844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.80/9.74 % (3488844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.80/9.74 % (3488844)CaDiCaL version: 2.1.3 % 63.80/9.74 % (3488844)Termination reason: Instruction limit % 63.80/9.74 % (3488844)Termination phase: Saturation % 63.80/9.74 % (3488844)Time elapsed: 1.860 s % 63.80/9.74 % (3488844)Peak memory usage: 154 MB % 63.80/9.74 % (3488844)Instructions burned: 3257 (million) % 63.80/9.74 % (3488855)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=3398315410:s2pl=no:i=8478:s2at=4:nm=6_2969 on theBenchmark for (2969ds/8478Mi) % 63.80/9.74 % (3488857)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=672862021:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2968 on theBenchmark for (2968ds/303Mi) % 63.80/9.74 % (3488857)Instruction limit reached! % 63.80/9.74 % (3488857)------------------------------ % 63.80/9.74 % (3488857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.80/9.74 % (3488857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.80/9.74 % (3488857)CaDiCaL version: 2.1.3 % 63.80/9.74 % (3488857)Termination reason: Instruction limit % 63.80/9.74 % (3488857)Termination phase: Saturation % 63.80/9.74 % (3488857)Time elapsed: 0.153 s % 63.80/9.74 % (3488857)Peak memory usage: 97 MB % 63.80/9.74 % (3488857)Instructions burned: 303 (million) % 63.80/9.74 % (3488859)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4144246637:st=4:i=720:sd=3:fsr=off:ss=axioms_2965 on theBenchmark for (2965ds/720Mi) % 63.80/9.74 % (3488859)Instruction limit reached! % 63.80/9.74 % (3488859)------------------------------ % 63.80/9.74 % (3488859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.80/9.74 % (3488859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.80/9.74 % (3488859)CaDiCaL version: 2.1.3 % 63.80/9.74 % (3488859)Termination reason: Instruction limit % 63.80/9.74 % (3488859)Termination phase: Saturation % 63.80/9.74 % (3488859)Time elapsed: 0.350 s % 63.80/9.74 % (3488859)Peak memory usage: 97 MB % 63.80/9.74 % (3488859)Instructions burned: 720 (million) % 63.80/9.74 % (3488832)Instruction limit reached! % 63.80/9.74 % (3488832)------------------------------ % 63.80/9.74 % (3488832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.80/9.74 % (3488832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.80/9.74 % (3488832)CaDiCaL version: 2.1.3 % 63.80/9.74 % (3488832)Termination reason: Instruction limit % 63.80/9.74 % (3488832)Termination phase: Saturation % 63.80/9.74 % (3488832)Time elapsed: 3.138 s % 63.80/9.74 % (3488832)Peak memory usage: 155 MB % 63.80/9.74 % (3488832)Instructions burned: 5209 (million) % 63.80/9.74 % (3488861)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=57630407:i=598:bs=on:bd=preordered:av=off:ss=axioms_2960 on theBenchmark for (2960ds/598Mi) % 63.80/9.74 % (3488862)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4204128170:i=2989:sd=3:ss=axioms:sgt=60_2960 on theBenchmark for (2960ds/2989Mi) % 63.80/9.74 % (3488861)Instruction limit reached! % 63.80/9.74 % (3488861)------------------------------ % 63.80/9.74 % (3488861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.80/9.74 % (3488861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.80/9.74 % (3488861)CaDiCaL version: 2.1.3 % 63.80/9.74 % (3488861)Termination reason: Instruction limit % 63.80/9.74 % (3488861)Termination phase: Saturation % 63.80/9.74 % (3488861)Time elapsed: 0.302 s % 63.80/9.74 % (3488861)Peak memory usage: 94 MB % 63.80/9.74 % (3488861)Instructions burned: 599 (million) % 63.80/9.74 % (3488851)Instruction limit reached! % 63.80/9.74 % (3488851)------------------------------ % 63.80/9.74 % (3488851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.80/9.74 % (3488851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.80/9.74 % (3488851)CaDiCaL version: 2.1.3 % 63.80/9.74 % (3488851)Termination reason: Instruction limit % 88.13/13.09 % (3488851)Termination phase: Saturation % 88.13/13.09 % (3488851)Time elapsed: 2.659 s % 88.13/13.09 % (3488851)Peak memory usage: 149 MB % 88.13/13.09 % (3488851)Instructions burned: 10309 (million) % 88.13/13.09 % (3488865)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=2896641254:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2956 on theBenchmark for (2956ds/1997Mi) % 88.13/13.09 % (3488866)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=2162444704:i=2088:bd=preordered:av=off_2955 on theBenchmark for (2955ds/2088Mi) % 88.13/13.09 % (3488866)Instruction limit reached! % 88.13/13.09 % (3488866)------------------------------ % 88.13/13.09 % (3488866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.13/13.09 % (3488866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.13/13.09 % (3488866)CaDiCaL version: 2.1.3 % 88.13/13.09 % (3488866)Termination reason: Instruction limit % 88.13/13.09 % (3488866)Termination phase: Saturation % 88.13/13.09 % (3488866)Time elapsed: 0.709 s % 88.13/13.09 % (3488866)Peak memory usage: 139 MB % 88.13/13.09 % (3488866)Instructions burned: 2092 (million) % 88.13/13.09 % (3488869)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1136418757:i=1098:nicw=on_2947 on theBenchmark for (2947ds/1098Mi) % 88.13/13.09 % (3488869)Instruction limit reached! % 88.13/13.09 % (3488869)------------------------------ % 88.13/13.09 % (3488869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.13/13.09 % (3488869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.13/13.09 % (3488869)CaDiCaL version: 2.1.3 % 88.13/13.09 % (3488869)Termination reason: Instruction limit % 88.13/13.09 % (3488869)Termination phase: Saturation % 88.13/13.09 % (3488869)Time elapsed: 0.279 s % 88.13/13.09 % (3488869)Peak memory usage: 111 MB % 88.13/13.09 % (3488869)Instructions burned: 1100 (million) % 88.13/13.09 % (3488871)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=470701555:i=433:bd=preordered_2943 on theBenchmark for (2943ds/433Mi) % 88.13/13.09 % (3488865)Instruction limit reached! % 88.13/13.09 % (3488865)------------------------------ % 88.13/13.09 % (3488865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.13/13.09 % (3488865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.13/13.09 % (3488865)CaDiCaL version: 2.1.3 % 88.13/13.09 % (3488865)Termination reason: Instruction limit % 88.13/13.09 % (3488865)Termination phase: Saturation % 88.13/13.09 % (3488865)Time elapsed: 1.313 s % 88.13/13.09 % (3488865)Peak memory usage: 138 MB % 88.13/13.09 % (3488865)Instructions burned: 1997 (million) % 88.13/13.09 % (3488871)Instruction limit reached! % 88.13/13.09 % (3488871)------------------------------ % 88.13/13.09 % (3488871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.13/13.09 % (3488871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.13/13.09 % (3488871)CaDiCaL version: 2.1.3 % 88.13/13.09 % (3488871)Termination reason: Instruction limit % 88.13/13.09 % (3488871)Termination phase: Saturation % 88.13/13.09 % (3488871)Time elapsed: 0.147 s % 88.13/13.09 % (3488871)Peak memory usage: 92 MB % 88.13/13.09 % (3488871)Instructions burned: 436 (million) % 88.13/13.09 % (3488873)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1518253705: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) % 88.13/13.09 % (3488862)Instruction limit reached! % 88.13/13.09 % (3488862)------------------------------ % 88.13/13.09 % (3488862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.13/13.09 % (3488862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.13/13.09 % (3488862)CaDiCaL version: 2.1.3 % 88.13/13.09 % (3488862)Termination reason: Instruction limit % 88.13/13.09 % (3488862)Termination phase: Saturation % 88.13/13.09 % (3488862)Time elapsed: 1.877 s % 88.13/13.09 % (3488862)Peak memory usage: 147 MB % 88.13/13.09 % (3488862)Instructions burned: 2989 (million) % 88.13/13.09 % (3488874)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3069683948:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2941 on theBenchmark for (2941ds/6922Mi) % 104.79/15.46 % (3488876)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=2888061811:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2940 on theBenchmark for (2940ds/596Mi) % 104.79/15.46 % (3488876)Instruction limit reached! % 104.79/15.46 % (3488876)------------------------------ % 104.79/15.46 % (3488876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.79/15.46 % (3488876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.79/15.46 % (3488876)CaDiCaL version: 2.1.3 % 104.79/15.46 % (3488876)Termination reason: Instruction limit % 104.79/15.46 % (3488876)Termination phase: Saturation % 104.79/15.46 % (3488876)Time elapsed: 0.266 s % 104.79/15.46 % (3488876)Peak memory usage: 101 MB % 104.79/15.46 % (3488876)Instructions burned: 598 (million) % 104.79/15.46 % (3488879)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=480191384:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2936 on theBenchmark for (2936ds/4123Mi) % 104.79/15.46 % (3488855)Instruction limit reached! % 104.79/15.46 % (3488855)------------------------------ % 104.79/15.46 % (3488855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.79/15.46 % (3488855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.79/15.46 % (3488855)CaDiCaL version: 2.1.3 % 104.79/15.46 % (3488855)Termination reason: Instruction limit % 104.79/15.46 % (3488855)Termination phase: Saturation % 104.79/15.46 % (3488855)Time elapsed: 3.997 s % 104.79/15.46 % (3488855)Peak memory usage: 183 MB % 104.79/15.46 % (3488855)Instructions burned: 8479 (million) % 104.79/15.46 % (3488881)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3300515001:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2928 on theBenchmark for (2928ds/16411Mi) % 104.79/15.46 % (3488879)Instruction limit reached! % 104.79/15.46 % (3488879)------------------------------ % 104.79/15.46 % (3488879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.79/15.46 % (3488879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.79/15.46 % (3488879)CaDiCaL version: 2.1.3 % 104.79/15.46 % (3488879)Termination reason: Instruction limit % 104.79/15.46 % (3488879)Termination phase: Saturation % 104.79/15.46 % (3488879)Time elapsed: 1.223 s % 104.79/15.46 % (3488879)Peak memory usage: 165 MB % 104.79/15.46 % (3488879)Instructions burned: 4123 (million) % 104.79/15.46 % (3488883)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=218851144:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2923 on theBenchmark for (2923ds/1670Mi) % 104.79/15.46 % (3488873)Instruction limit reached! % 104.79/15.46 % (3488873)------------------------------ % 104.79/15.46 % (3488873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.79/15.46 % (3488873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.79/15.46 % (3488873)CaDiCaL version: 2.1.3 % 104.79/15.46 % (3488873)Termination reason: Instruction limit % 104.79/15.46 % (3488873)Termination phase: Saturation % 104.79/15.46 % (3488873)Time elapsed: 2.008 s % 104.79/15.46 % (3488873)Peak memory usage: 142 MB % 104.79/15.46 % (3488873)Instructions burned: 2942 (million) % 104.79/15.46 % (3488885)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=2796488056:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2920 on theBenchmark for (2920ds/1722Mi) % 104.79/15.46 % (3488883)Instruction limit reached! % 104.79/15.46 % (3488883)------------------------------ % 104.79/15.46 % (3488883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.79/15.46 % (3488883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.79/15.46 % (3488883)CaDiCaL version: 2.1.3 % 104.79/15.46 % (3488883)Termination reason: Instruction limit % 104.79/15.46 % (3488883)Termination phase: Saturation % 104.79/15.46 % (3488883)Time elapsed: 0.603 s % 104.79/15.46 % (3488883)Peak memory usage: 136 MB % 104.79/15.46 % (3488883)Instructions burned: 1673 (million) % 104.79/15.46 % (3488887)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=3531603755:cts=off:cond=on:i=9530:bs=on:fsd=on_2916 on theBenchmark for (2916ds/9530Mi) % 104.79/15.46 % (3488885)Instruction limit reached! % 124.31/18.19 % (3488885)------------------------------ % 124.31/18.19 % (3488885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.31/18.19 % (3488885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.31/18.19 % (3488885)CaDiCaL version: 2.1.3 % 124.31/18.19 % (3488885)Termination reason: Instruction limit % 124.31/18.19 % (3488885)Termination phase: Saturation % 124.31/18.19 % (3488885)Time elapsed: 1.048 s % 124.31/18.19 % (3488885)Peak memory usage: 132 MB % 124.31/18.19 % (3488885)Instructions burned: 1722 (million) % 124.31/18.19 % (3488889)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1892909615:st=2:i=4495:sd=10:ss=included_2909 on theBenchmark for (2909ds/4495Mi) % 124.31/18.19 % (3488874)Instruction limit reached! % 124.31/18.19 % (3488874)------------------------------ % 124.31/18.19 % (3488874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.31/18.19 % (3488874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.31/18.19 % (3488874)CaDiCaL version: 2.1.3 % 124.31/18.19 % (3488874)Termination reason: Instruction limit % 124.31/18.19 % (3488874)Termination phase: Saturation % 124.31/18.19 % (3488874)Time elapsed: 3.420 s % 124.31/18.19 % (3488874)Peak memory usage: 191 MB % 124.31/18.19 % (3488874)Instructions burned: 6923 (million) % 124.31/18.19 % (3488891)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=1801543298:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2906 on theBenchmark for (2906ds/4920Mi) % 124.31/18.19 % (3488887)Instruction limit reached! % 124.31/18.19 % (3488887)------------------------------ % 124.31/18.19 % (3488887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.31/18.19 % (3488887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.31/18.19 % (3488887)CaDiCaL version: 2.1.3 % 124.31/18.19 % (3488887)Termination reason: Instruction limit % 124.31/18.19 % (3488887)Termination phase: Saturation % 124.31/18.19 % (3488887)Time elapsed: 2.472 s % 124.31/18.19 % (3488887)Peak memory usage: 149 MB % 124.31/18.19 % (3488887)Instructions burned: 9533 (million) % 124.31/18.19 % (3488893)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=1841521466:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2890 on theBenchmark for (2890ds/2083Mi) % 124.31/18.19 % (3488893)Instruction limit reached! % 124.31/18.19 % (3488893)------------------------------ % 124.31/18.19 % (3488893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.31/18.19 % (3488893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.31/18.19 % (3488893)CaDiCaL version: 2.1.3 % 124.31/18.19 % (3488893)Termination reason: Instruction limit % 124.31/18.19 % (3488893)Termination phase: Saturation % 124.31/18.19 % (3488893)Time elapsed: 0.723 s % 124.31/18.19 % (3488893)Peak memory usage: 139 MB % 124.31/18.19 % (3488893)Instructions burned: 2086 (million) % 124.31/18.19 % (3488895)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=749384163:i=4629:av=off:gsp=on_2882 on theBenchmark for (2882ds/4629Mi) % 124.31/18.19 % (3488889)Instruction limit reached! % 124.31/18.19 % (3488889)------------------------------ % 124.31/18.19 % (3488889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.31/18.19 % (3488889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.31/18.19 % (3488889)CaDiCaL version: 2.1.3 % 124.31/18.19 % (3488889)Termination reason: Instruction limit % 124.31/18.19 % (3488889)Termination phase: Saturation % 124.31/18.19 % (3488889)Time elapsed: 2.655 s % 124.31/18.19 % (3488889)Peak memory usage: 166 MB % 124.31/18.19 % (3488889)Instructions burned: 4495 (million) % 124.31/18.19 % (3488897)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3020478221:i=1258:av=off_2881 on theBenchmark for (2881ds/1258Mi) % 124.31/18.19 % (3488891)Instruction limit reached! % 124.31/18.19 % (3488891)------------------------------ % 124.31/18.19 % (3488891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.31/18.19 % (3488891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.31/18.19 % (3488891)CaDiCaL version: 2.1.3 % 124.31/18.19 % (3488891)Termination reason: Instruction limit % 124.31/18.19 % (3488891)Termination phase: Saturation % 124.31/18.19 % (3488891)Time elapsed: 2.945 s % 124.31/18.19 % (3488891)Peak memory usage: 156 MB % 147.45/21.47 % (3488891)Instructions burned: 4920 (million) % 147.45/21.47 % (3488899)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3865502760:i=7343:av=off:ss=included_2875 on theBenchmark for (2875ds/7343Mi) % 147.45/21.47 % (3488897)Instruction limit reached! % 147.45/21.47 % (3488897)------------------------------ % 147.45/21.47 % (3488897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.45/21.47 % (3488897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.45/21.47 % (3488897)CaDiCaL version: 2.1.3 % 147.45/21.47 % (3488897)Termination reason: Instruction limit % 147.45/21.47 % (3488897)Termination phase: Saturation % 147.45/21.47 % (3488897)Time elapsed: 0.710 s % 147.45/21.47 % (3488897)Peak memory usage: 111 MB % 147.45/21.47 % (3488897)Instructions burned: 1258 (million) % 147.45/21.47 % (3488901)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2925854621:i=1325:sd=2:ss=axioms:sgt=16_2872 on theBenchmark for (2872ds/1325Mi) % 147.45/21.47 % (3488895)Instruction limit reached! % 147.45/21.47 % (3488895)------------------------------ % 147.45/21.47 % (3488895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.45/21.47 % (3488895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.45/21.47 % (3488895)CaDiCaL version: 2.1.3 % 147.45/21.47 % (3488895)Termination reason: Instruction limit % 147.45/21.47 % (3488895)Termination phase: Saturation % 147.45/21.47 % (3488895)Time elapsed: 1.430 s % 147.45/21.47 % (3488895)Peak memory usage: 166 MB % 147.45/21.47 % (3488895)Instructions burned: 4630 (million) % 147.45/21.47 % (3488903)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=2755721476:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2867 on theBenchmark for (2867ds/2646Mi) % 147.45/21.47 % (3488901)Instruction limit reached! % 147.45/21.47 % (3488901)------------------------------ % 147.45/21.47 % (3488901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.45/21.47 % (3488901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.45/21.47 % (3488901)CaDiCaL version: 2.1.3 % 147.45/21.47 % (3488901)Termination reason: Instruction limit % 147.45/21.47 % (3488901)Termination phase: Saturation % 147.45/21.47 % (3488901)Time elapsed: 0.744 s % 147.45/21.47 % (3488901)Peak memory usage: 99 MB % 147.45/21.47 % (3488901)Instructions burned: 1326 (million) % 147.45/21.47 % (3488905)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=4099112627:i=1489:sd=2:ep=R:ss=axioms_2863 on theBenchmark for (2863ds/1489Mi) % 147.45/21.47 % (3488903)Instruction limit reached! % 147.45/21.47 % (3488903)------------------------------ % 147.45/21.47 % (3488903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.45/21.47 % (3488903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.45/21.47 % (3488903)CaDiCaL version: 2.1.3 % 147.45/21.47 % (3488903)Termination reason: Instruction limit % 147.45/21.47 % (3488903)Termination phase: Saturation % 147.45/21.47 % (3488903)Time elapsed: 0.885 s % 147.45/21.47 % (3488903)Peak memory usage: 139 MB % 147.45/21.47 % (3488903)Instructions burned: 2648 (million) % 147.45/21.47 % (3488907)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=2403703751:i=1503_2857 on theBenchmark for (2857ds/1503Mi) % 147.45/21.47 % (3488905)Instruction limit reached! % 147.45/21.47 % (3488905)------------------------------ % 147.45/21.47 % (3488905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.45/21.47 % (3488905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.45/21.47 % (3488905)CaDiCaL version: 2.1.3 % 147.45/21.47 % (3488905)Termination reason: Instruction limit % 147.45/21.47 % (3488905)Termination phase: Saturation % 147.45/21.47 % (3488905)Time elapsed: 0.888 s % 147.45/21.47 % (3488905)Peak memory usage: 137 MB % 147.45/21.47 % (3488905)Instructions burned: 1490 (million) % 147.45/21.47 % (3488909)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2489432570:i=13942:kws=frequency_2853 on theBenchmark for (2853ds/13942Mi) % 147.45/21.47 % (3488907)Instruction limit reached! % 147.45/21.47 % (3488907)------------------------------ % 147.45/21.47 % (3488907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.45/21.47 % (3488907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.45/21.47 % (3488907)CaDiCaL version: 2.1.3 % 167.31/24.29 % (3488907)Termination reason: Instruction limit % 167.31/24.29 % (3488907)Termination phase: Saturation % 167.31/24.29 % (3488907)Time elapsed: 0.499 s % 167.31/24.29 % (3488907)Peak memory usage: 138 MB % 167.31/24.29 % (3488907)Instructions burned: 1505 (million) % 167.31/24.29 % (3488911)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=1112900082:i=3604:fsr=off:er=filter_2851 on theBenchmark for (2851ds/3604Mi) % 167.31/24.29 % (3488911)Instruction limit reached! % 167.31/24.29 % (3488911)------------------------------ % 167.31/24.29 % (3488911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.31/24.29 % (3488911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.31/24.29 % (3488911)CaDiCaL version: 2.1.3 % 167.31/24.29 % (3488911)Termination reason: Instruction limit % 167.31/24.29 % (3488911)Termination phase: Saturation % 167.31/24.29 % (3488911)Time elapsed: 1.087 s % 167.31/24.29 % (3488911)Peak memory usage: 160 MB % 167.31/24.29 % (3488911)Instructions burned: 3607 (million) % 167.31/24.29 % (3488913)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1156625334:i=1876:sd=1:ss=included:sgt=32_2839 on theBenchmark for (2839ds/1876Mi) % 167.31/24.29 % (3488913)Instruction limit reached! % 167.31/24.29 % (3488913)------------------------------ % 167.31/24.29 % (3488913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.31/24.29 % (3488913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.31/24.29 % (3488913)CaDiCaL version: 2.1.3 % 167.31/24.29 % (3488913)Termination reason: Instruction limit % 167.31/24.29 % (3488913)Termination phase: Saturation % 167.31/24.29 % (3488913)Time elapsed: 0.631 s % 167.31/24.29 % (3488913)Peak memory usage: 138 MB % 167.31/24.29 % (3488913)Instructions burned: 1878 (million) % 167.31/24.29 % (3488915)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1295421095:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2832 on theBenchmark for (2832ds/1932Mi) % 167.31/24.29 % (3488899)Instruction limit reached! % 167.31/24.29 % (3488899)------------------------------ % 167.31/24.29 % (3488899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.31/24.29 % (3488899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.31/24.29 % (3488899)CaDiCaL version: 2.1.3 % 167.31/24.29 % (3488899)Termination reason: Instruction limit % 167.31/24.29 % (3488899)Termination phase: Saturation % 167.31/24.29 % (3488899)Time elapsed: 4.337 s % 167.31/24.29 % (3488899)Peak memory usage: 190 MB % 167.31/24.29 % (3488899)Instructions burned: 7344 (million) % 167.31/24.29 % (3488917)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=4213188681:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2830 on theBenchmark for (2830ds/1980Mi) % 167.31/24.29 % (3488881)Instruction limit reached! % 167.31/24.29 % (3488881)------------------------------ % 167.31/24.29 % (3488881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.31/24.29 % (3488881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.31/24.29 % (3488881)CaDiCaL version: 2.1.3 % 167.31/24.29 % (3488881)Termination reason: Instruction limit % 167.31/24.29 % (3488881)Termination phase: Saturation % 167.31/24.29 % (3488881)Time elapsed: 9.831 s % 167.31/24.29 % (3488881)Peak memory usage: 227 MB % 167.31/24.29 % (3488881)Instructions burned: 16411 (million) % 167.31/24.29 % (3488919)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=3507558666:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2828 on theBenchmark for (2828ds/3902Mi) % 167.31/24.29 % (3488915)Instruction limit reached! % 167.31/24.29 % (3488915)------------------------------ % 167.31/24.29 % (3488915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 167.31/24.29 % (3488915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 167.31/24.29 % (3488915)CaDiCaL version: 2.1.3 % 167.31/24.29 % (3488915)Termination reason: Instruction limit % 167.31/24.29 % (3488915)Termination phase: Saturation % 167.31/24.29 % (3488915)Time elapsed: 0.623 s % 167.31/24.29 % (3488915)Peak memory usage: 141 MB % 167.31/24.29 % (3488915)Instructions burned: 1933 (million) % 167.31/24.29 % (3488921)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1157225922:avsq=on:i=3916:aac=none:amm=off_2825 on theBenchmark for (2825ds/3916Mi) % 190.90/27.67 % (3488917)Instruction limit reached! % 190.90/27.67 % (3488917)------------------------------ % 190.90/27.67 % (3488917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.90/27.67 % (3488917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.90/27.67 % (3488917)CaDiCaL version: 2.1.3 % 190.90/27.67 % (3488917)Termination reason: Instruction limit % 190.90/27.67 % (3488917)Termination phase: Saturation % 190.90/27.67 % (3488917)Time elapsed: 1.268 s % 190.90/27.67 % (3488917)Peak memory usage: 138 MB % 190.90/27.67 % (3488917)Instructions burned: 1980 (million) % 190.90/27.67 % (3488923)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3936976028:cond=on:i=3940:av=off:er=known_2816 on theBenchmark for (2816ds/3940Mi) % 190.90/27.67 % (3488921)Instruction limit reached! % 190.90/27.67 % (3488921)------------------------------ % 190.90/27.67 % (3488921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.90/27.67 % (3488921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.90/27.67 % (3488921)CaDiCaL version: 2.1.3 % 190.90/27.67 % (3488921)Termination reason: Instruction limit % 190.90/27.67 % (3488921)Termination phase: Saturation % 190.90/27.67 % (3488921)Time elapsed: 1.215 s % 190.90/27.67 % (3488921)Peak memory usage: 124 MB % 190.90/27.67 % (3488921)Instructions burned: 3917 (million) % 190.90/27.67 % (3488925)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2058787315:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2812 on theBenchmark for (2812ds/3980Mi) % 190.90/27.67 % (3488919)Instruction limit reached! % 190.90/27.67 % (3488919)------------------------------ % 190.90/27.67 % (3488919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.90/27.67 % (3488919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.90/27.67 % (3488919)CaDiCaL version: 2.1.3 % 190.90/27.67 % (3488919)Termination reason: Instruction limit % 190.90/27.67 % (3488919)Termination phase: Saturation % 190.90/27.67 % (3488919)Time elapsed: 2.082 s % 190.90/27.67 % (3488919)Peak memory usage: 163 MB % 190.90/27.67 % (3488919)Instructions burned: 3902 (million) % 190.90/27.67 % (3488928)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=3026852865:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2806 on theBenchmark for (2806ds/2087Mi) % 190.90/27.67 % (3488925)Instruction limit reached! % 190.90/27.67 % (3488925)------------------------------ % 190.90/27.67 % (3488925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.90/27.67 % (3488925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.90/27.67 % (3488925)CaDiCaL version: 2.1.3 % 190.90/27.67 % (3488925)Termination reason: Instruction limit % 190.90/27.67 % (3488925)Termination phase: Saturation % 190.90/27.67 % (3488925)Time elapsed: 1.377 s % 190.90/27.67 % (3488925)Peak memory usage: 160 MB % 190.90/27.67 % (3488925)Instructions burned: 3983 (million) % 190.90/27.67 % (3488930)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=1312166992:cts=off:cond=on:i=4272:bs=on:fsd=on_2797 on theBenchmark for (2797ds/4272Mi) % 190.90/27.67 % (3488923)Instruction limit reached! % 190.90/27.67 % (3488923)------------------------------ % 190.90/27.67 % (3488923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.90/27.67 % (3488923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.90/27.67 % (3488923)CaDiCaL version: 2.1.3 % 190.90/27.67 % (3488923)Termination reason: Instruction limit % 190.90/27.67 % (3488923)Termination phase: Saturation % 190.90/27.67 % (3488923)Time elapsed: 2.340 s % 190.90/27.67 % (3488923)Peak memory usage: 154 MB % 190.90/27.67 % (3488923)Instructions burned: 3940 (million) % 190.90/27.67 % (3488928)Instruction limit reached! % 190.90/27.67 % (3488928)------------------------------ % 190.90/27.67 % (3488928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.90/27.67 % (3488928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.90/27.67 % (3488928)CaDiCaL version: 2.1.3 % 190.90/27.67 % (3488928)Termination reason: Instruction limit % 190.90/27.67 % (3488928)Termination phase: Saturation % 190.90/27.67 % (3488928)Time elapsed: 1.347 s % 260.23/37.39 % (3488928)Peak memory usage: 140 MB % 260.23/37.39 % (3488928)Instructions burned: 2089 (million) % 260.23/37.39 % (3488932)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4073228707:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2791 on theBenchmark for (2791ds/2197Mi) % 260.23/37.39 % (3488933)dis+21_1_sil=8000:spb=goal_then_units:random_seed=367499969:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2791 on theBenchmark for (2791ds/6508Mi) % 260.23/37.39 % (3488930)Instruction limit reached! % 260.23/37.39 % (3488930)------------------------------ % 260.23/37.39 % (3488930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.23/37.39 % (3488930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/37.39 % (3488930)CaDiCaL version: 2.1.3 % 260.23/37.39 % (3488930)Termination reason: Instruction limit % 260.23/37.39 % (3488930)Termination phase: Saturation % 260.23/37.39 % (3488930)Time elapsed: 1.300 s % 260.23/37.39 % (3488930)Peak memory usage: 144 MB % 260.23/37.39 % (3488930)Instructions burned: 4273 (million) % 260.23/37.39 % (3488936)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=2090775881:i=2330:fgj=on:av=off:fsr=off_2783 on theBenchmark for (2783ds/2330Mi) % 260.23/37.39 % (3488932)Instruction limit reached! % 260.23/37.39 % (3488932)------------------------------ % 260.23/37.39 % (3488932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.23/37.39 % (3488932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/37.39 % (3488932)CaDiCaL version: 2.1.3 % 260.23/37.39 % (3488932)Termination reason: Instruction limit % 260.23/37.39 % (3488932)Termination phase: Saturation % 260.23/37.39 % (3488932)Time elapsed: 1.217 s % 260.23/37.39 % (3488932)Peak memory usage: 144 MB % 260.23/37.39 % (3488932)Instructions burned: 2199 (million) % 260.23/37.39 % (3488938)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=747083216:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2778 on theBenchmark for (2778ds/7592Mi) % 260.23/37.39 % (3488936)Instruction limit reached! % 260.23/37.39 % (3488936)------------------------------ % 260.23/37.39 % (3488936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.23/37.39 % (3488936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/37.39 % (3488936)CaDiCaL version: 2.1.3 % 260.23/37.39 % (3488936)Termination reason: Instruction limit % 260.23/37.39 % (3488936)Termination phase: Saturation % 260.23/37.39 % (3488936)Time elapsed: 0.783 s % 260.23/37.39 % (3488936)Peak memory usage: 140 MB % 260.23/37.39 % (3488936)Instructions burned: 2333 (million) % 260.23/37.39 % (3488940)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=173370712:i=2693:kws=precedence:ins=1:av=off_2774 on theBenchmark for (2774ds/2693Mi) % 260.23/37.39 % (3488909)Instruction limit reached! % 260.23/37.39 % (3488909)------------------------------ % 260.23/37.39 % (3488909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.23/37.39 % (3488909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/37.39 % (3488909)CaDiCaL version: 2.1.3 % 260.23/37.39 % (3488909)Termination reason: Instruction limit % 260.23/37.39 % (3488909)Termination phase: Saturation % 260.23/37.39 % (3488909)Time elapsed: 8.070 s % 260.23/37.39 % (3488909)Peak memory usage: 257 MB % 260.23/37.39 % (3488909)Instructions burned: 13944 (million) % 260.23/37.39 % (3488942)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=3976083283:i=28651:sd=4:ss=included:sgt=64_2771 on theBenchmark for (2771ds/28651Mi) % 260.23/37.39 % (3488940)Instruction limit reached! % 260.23/37.39 % (3488940)------------------------------ % 260.23/37.39 % (3488940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 260.23/37.39 % (3488940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 260.23/37.39 % (3488940)CaDiCaL version: 2.1.3 % 260.23/37.39 % (3488940)Termination reason: Instruction limit % 260.23/37.39 % (3488940)Termination phase: Saturation % 260.23/37.39 % (3488940)Time elapsed: 0.962 s % 260.23/37.39 % (3488940)Peak memory usage: 144 MB % 260.23/37.39 % (3488940)Instructions burned: 2696 (million) % 260.23/37.39 % (3488944)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1708736003:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2764 on theBenchmark for (2764ds/2700Terminated %------------------------------------------------------------------------------