%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV421-1.405 : TPTP v9.3.1. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n013.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:12:06 PM UTC 2026 % Result : Timeout 300.10s 42.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV421-1.405 : TPTP v9.3.1. Released v3.5.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.18 % Computer : n013.cluster.edu % 0.07/0.18 % Model : x86_64 x86_64 % 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.18 % Memory : 8046.5625MB % 0.07/0.18 % OS : Linux 6.8.0-71-generic % 0.07/0.18 % CPULimit : 300 % 0.07/0.18 % WCLimit : 300 % 0.07/0.18 % DateTime : Mon Sep 28 11:00:06 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.21 Running first-order theorem proving % 0.07/0.21 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 % 10.09/2.12 % (1096415)Input is clausal, will run a generic CNF schedule. % 10.09/2.12 % (1096422)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2059469456:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 10.09/2.12 % (1096420)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=1145913640:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 10.09/2.12 % (1096421)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3081412451:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 10.09/2.12 % (1096424)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3537985113:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 10.09/2.12 % (1096423)lrs+10_1_sil=8000:sp=occurrence:random_seed=819961723:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 10.09/2.12 % (1096425)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=8648850:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 10.09/2.12 % (1096426)dis-21_1_sil=8000:lcm=predicate:random_seed=1988293397:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 10.09/2.12 % (1096423)Instruction limit reached! % 10.09/2.12 % (1096423)------------------------------ % 10.09/2.12 % (1096423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.12 % (1096423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.12 % (1096423)CaDiCaL version: 2.1.3 % 10.09/2.12 % (1096423)Termination reason: Instruction limit % 10.09/2.12 % (1096423)Termination phase: Saturation % 10.09/2.12 % (1096423)Time elapsed: 0.044 s % 10.09/2.12 % (1096423)Peak memory usage: 90 MB % 10.09/2.12 % (1096423)Instructions burned: 108 (million) % 10.09/2.12 % (1096424)Instruction limit reached! % 10.09/2.12 % (1096424)------------------------------ % 10.09/2.12 % (1096424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.12 % (1096424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.12 % (1096424)CaDiCaL version: 2.1.3 % 10.09/2.12 % (1096424)Termination reason: Instruction limit % 10.09/2.12 % (1096424)Termination phase: Saturation % 10.09/2.12 % (1096424)Time elapsed: 0.045 s % 10.09/2.12 % (1096424)Peak memory usage: 89 MB % 10.09/2.12 % (1096424)Instructions burned: 114 (million) % 10.09/2.12 % (1096426)Instruction limit reached! % 10.09/2.12 % (1096426)------------------------------ % 10.09/2.12 % (1096426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.12 % (1096426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.12 % (1096426)CaDiCaL version: 2.1.3 % 10.09/2.12 % (1096426)Termination reason: Instruction limit % 10.09/2.12 % (1096426)Termination phase: Saturation % 10.09/2.12 % (1096426)Time elapsed: 0.059 s % 10.09/2.12 % (1096426)Peak memory usage: 89 MB % 10.09/2.12 % (1096426)Instructions burned: 118 (million) % 10.09/2.12 % (1096425)Instruction limit reached! % 10.09/2.12 % (1096425)------------------------------ % 10.09/2.12 % (1096425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.09/2.12 % (1096425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.09/2.12 % (1096425)CaDiCaL version: 2.1.3 % 10.09/2.12 % (1096425)Termination reason: Instruction limit % 10.09/2.12 % (1096425)Termination phase: Saturation % 10.09/2.12 % (1096425)Time elapsed: 0.086 s % 10.09/2.12 % (1096425)Peak memory usage: 90 MB % 10.09/2.12 % (1096425)Instructions burned: 183 (million) % 10.09/2.12 % (1096434)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=909588687:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 10.09/2.12 % (1096435)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3094976100:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi) % 10.09/2.12 % (1096436)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1145256521:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 10.09/2.12 % (1096437)lrs+10_64_to=lpo:sil=8000:random_seed=2947097863:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 10.09/2.12 % (1096435)Refutation not found, incomplete strategy % 23.05/3.91 % (1096435)------------------------------ % 23.05/3.91 % (1096435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.05/3.91 % (1096435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.05/3.91 % (1096435)CaDiCaL version: 2.1.3 % 23.05/3.91 % (1096435)Termination reason: Refutation not found, incomplete strategy % 23.05/3.91 % (1096435)Time elapsed: 0.050 s % 23.05/3.91 % (1096435)Peak memory usage: 89 MB % 23.05/3.91 % (1096435)Instructions burned: 105 (million) % 23.05/3.91 % (1096434)Instruction limit reached! % 23.05/3.91 % (1096434)------------------------------ % 23.05/3.91 % (1096434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.05/3.91 % (1096434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.05/3.91 % (1096434)CaDiCaL version: 2.1.3 % 23.05/3.91 % (1096434)Termination reason: Instruction limit % 23.05/3.91 % (1096434)Termination phase: Saturation % 23.05/3.91 % (1096434)Time elapsed: 0.060 s % 23.05/3.91 % (1096434)Peak memory usage: 91 MB % 23.05/3.91 % (1096434)Instructions burned: 146 (million) % 23.05/3.91 % (1096437)Instruction limit reached! % 23.05/3.91 % (1096437)------------------------------ % 23.05/3.91 % (1096437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.05/3.91 % (1096437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.05/3.91 % (1096437)CaDiCaL version: 2.1.3 % 23.05/3.91 % (1096437)Termination reason: Instruction limit % 23.05/3.91 % (1096437)Termination phase: Saturation % 23.05/3.91 % (1096437)Time elapsed: 0.051 s % 23.05/3.91 % (1096437)Peak memory usage: 90 MB % 23.05/3.91 % (1096437)Instructions burned: 127 (million) % 23.05/3.91 % (1096436)Instruction limit reached! % 23.05/3.91 % (1096436)------------------------------ % 23.05/3.91 % (1096436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.05/3.91 % (1096436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.05/3.91 % (1096436)CaDiCaL version: 2.1.3 % 23.05/3.91 % (1096436)Termination reason: Instruction limit % 23.05/3.91 % (1096436)Termination phase: Saturation % 23.05/3.91 % (1096436)Time elapsed: 0.083 s % 23.05/3.91 % (1096436)Peak memory usage: 93 MB % 23.05/3.91 % (1096436)Instructions burned: 221 (million) % 23.05/3.91 % (1096442)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=29393310:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 23.05/3.91 % (1096443)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=724416530:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi) % 23.05/3.91 % (1096444)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1673393742:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi) % 23.05/3.91 % (1096435)------------------------------ % 23.05/3.91 % (1096435)------------------------------ % 23.05/3.91 % (1096443)Instruction limit reached! % 23.05/3.91 % (1096443)------------------------------ % 23.05/3.91 % (1096443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.05/3.91 % (1096443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.05/3.91 % (1096443)CaDiCaL version: 2.1.3 % 23.05/3.91 % (1096443)Termination reason: Instruction limit % 23.05/3.91 % (1096443)Termination phase: Saturation % 23.05/3.91 % (1096443)Time elapsed: 0.073 s % 23.05/3.91 % (1096443)Peak memory usage: 92 MB % 23.05/3.91 % (1096443)Instructions burned: 157 (million) % 23.05/3.91 % (1096442)Instruction limit reached! % 23.05/3.91 % (1096442)------------------------------ % 23.05/3.91 % (1096442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.05/3.91 % (1096442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.05/3.91 % (1096442)CaDiCaL version: 2.1.3 % 23.05/3.91 % (1096442)Termination reason: Instruction limit % 23.05/3.91 % (1096442)Termination phase: Saturation % 23.05/3.91 % (1096442)Time elapsed: 0.093 s % 23.05/3.91 % (1096442)Peak memory usage: 89 MB % 23.05/3.91 % (1096442)Instructions burned: 195 (million) % 23.05/3.91 % (1096448)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=2689958242:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 23.05/3.91 % (1096449)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3653946836:i=107_2993 on theBenchmark for (2993ds/107Mi) % 23.05/3.91 % (1096450)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=89297372:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi) % 35.61/5.72 % (1096448)Instruction limit reached! % 35.61/5.72 % (1096448)------------------------------ % 35.61/5.72 % (1096448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/5.72 % (1096448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/5.72 % (1096448)CaDiCaL version: 2.1.3 % 35.61/5.72 % (1096448)Termination reason: Instruction limit % 35.61/5.72 % (1096448)Termination phase: Saturation % 35.61/5.72 % (1096448)Time elapsed: 0.049 s % 35.61/5.72 % (1096448)Peak memory usage: 90 MB % 35.61/5.72 % (1096448)Instructions burned: 107 (million) % 35.61/5.72 % (1096449)Instruction limit reached! % 35.61/5.72 % (1096449)------------------------------ % 35.61/5.72 % (1096449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/5.72 % (1096449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/5.72 % (1096449)CaDiCaL version: 2.1.3 % 35.61/5.72 % (1096449)Termination reason: Instruction limit % 35.61/5.72 % (1096449)Termination phase: Saturation % 35.61/5.72 % (1096449)Time elapsed: 0.051 s % 35.61/5.72 % (1096449)Peak memory usage: 93 MB % 35.61/5.72 % (1096449)Instructions burned: 109 (million) % 35.61/5.72 % (1096450)Instruction limit reached! % 35.61/5.72 % (1096450)------------------------------ % 35.61/5.72 % (1096450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/5.72 % (1096450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/5.72 % (1096450)CaDiCaL version: 2.1.3 % 35.61/5.72 % (1096450)Termination reason: Instruction limit % 35.61/5.72 % (1096450)Termination phase: Saturation % 35.61/5.72 % (1096450)Time elapsed: 0.104 s % 35.61/5.72 % (1096450)Peak memory usage: 88 MB % 35.61/5.72 % (1096450)Instructions burned: 243 (million) % 35.61/5.72 % (1096454)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3710479992:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi) % 35.61/5.72 % (1096455)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2880454337:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi) % 35.61/5.72 % (1096455)Instruction limit reached! % 35.61/5.72 % (1096455)------------------------------ % 35.61/5.72 % (1096455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/5.72 % (1096455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/5.72 % (1096455)CaDiCaL version: 2.1.3 % 35.61/5.72 % (1096455)Termination reason: Instruction limit % 35.61/5.72 % (1096455)Termination phase: Saturation % 35.61/5.72 % (1096455)Time elapsed: 0.064 s % 35.61/5.72 % (1096455)Peak memory usage: 89 MB % 35.61/5.72 % (1096455)Instructions burned: 136 (million) % 35.61/5.72 % (1096456)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3204680838:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi) % 35.61/5.72 % (1096460)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3184404119:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi) % 35.61/5.72 % (1096456)Instruction limit reached! % 35.61/5.72 % (1096456)------------------------------ % 35.61/5.72 % (1096456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/5.72 % (1096456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/5.72 % (1096456)CaDiCaL version: 2.1.3 % 35.61/5.72 % (1096456)Termination reason: Instruction limit % 35.61/5.72 % (1096456)Termination phase: Saturation % 35.61/5.72 % (1096456)Time elapsed: 0.207 s % 35.61/5.72 % (1096456)Peak memory usage: 95 MB % 35.61/5.72 % (1096456)Instructions burned: 501 (million) % 35.61/5.72 % (1096460)Instruction limit reached! % 35.61/5.72 % (1096460)------------------------------ % 35.61/5.72 % (1096460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.61/5.72 % (1096460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.61/5.72 % (1096460)CaDiCaL version: 2.1.3 % 35.61/5.72 % (1096460)Termination reason: Instruction limit % 35.61/5.72 % (1096460)Termination phase: Saturation % 35.61/5.72 % (1096460)Time elapsed: 0.082 s % 35.61/5.72 % (1096460)Peak memory usage: 92 MB % 35.61/5.72 % (1096460)Instructions burned: 191 (million) % 35.61/5.72 % (1096462)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3220718787:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi) % 59.76/9.05 % (1096463)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3591681283:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi) % 59.76/9.05 % (1096463)Instruction limit reached! % 59.76/9.05 % (1096463)------------------------------ % 59.76/9.05 % (1096463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.76/9.05 % (1096463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.76/9.05 % (1096463)CaDiCaL version: 2.1.3 % 59.76/9.05 % (1096463)Termination reason: Instruction limit % 59.76/9.05 % (1096463)Termination phase: Saturation % 59.76/9.05 % (1096463)Time elapsed: 0.054 s % 59.76/9.05 % (1096463)Peak memory usage: 88 MB % 59.76/9.05 % (1096463)Instructions burned: 157 (million) % 59.76/9.05 % (1096462)Instruction limit reached! % 59.76/9.05 % (1096462)------------------------------ % 59.76/9.05 % (1096462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.76/9.05 % (1096462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.76/9.05 % (1096462)CaDiCaL version: 2.1.3 % 59.76/9.05 % (1096462)Termination reason: Instruction limit % 59.76/9.05 % (1096462)Termination phase: Saturation % 59.76/9.05 % (1096462)Time elapsed: 0.102 s % 59.76/9.05 % (1096462)Peak memory usage: 91 MB % 59.76/9.05 % (1096462)Instructions burned: 265 (million) % 59.76/9.05 % (1096467)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1473817705:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi) % 59.76/9.05 % (1096466)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=2233392871:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi) % 59.76/9.05 % (1096467)Instruction limit reached! % 59.76/9.05 % (1096467)------------------------------ % 59.76/9.05 % (1096467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.76/9.05 % (1096467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.76/9.05 % (1096467)CaDiCaL version: 2.1.3 % 59.76/9.05 % (1096467)Termination reason: Instruction limit % 59.76/9.05 % (1096467)Termination phase: Saturation % 59.76/9.05 % (1096467)Time elapsed: 0.245 s % 59.76/9.05 % (1096467)Peak memory usage: 88 MB % 59.76/9.05 % (1096467)Instructions burned: 538 (million) % 59.76/9.05 % (1096470)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3518883869:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi) % 59.76/9.05 % (1096470)Instruction limit reached! % 59.76/9.05 % (1096470)------------------------------ % 59.76/9.05 % (1096470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.76/9.05 % (1096470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.76/9.05 % (1096470)CaDiCaL version: 2.1.3 % 59.76/9.05 % (1096470)Termination reason: Instruction limit % 59.76/9.05 % (1096470)Termination phase: Saturation % 59.76/9.05 % (1096470)Time elapsed: 0.078 s % 59.76/9.05 % (1096470)Peak memory usage: 90 MB % 59.76/9.05 % (1096470)Instructions burned: 181 (million) % 59.76/9.05 % (1096472)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=2644144626:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi) % 59.76/9.05 % (1096444)Instruction limit reached! % 59.76/9.05 % (1096444)------------------------------ % 59.76/9.05 % (1096444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.76/9.05 % (1096444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.76/9.05 % (1096444)CaDiCaL version: 2.1.3 % 59.76/9.05 % (1096444)Termination reason: Instruction limit % 59.76/9.05 % (1096444)Termination phase: Saturation % 59.76/9.05 % (1096444)Time elapsed: 2.284 s % 59.76/9.05 % (1096444)Peak memory usage: 152 MB % 59.76/9.05 % (1096444)Instructions burned: 3396 (million) % 59.76/9.05 % (1096474)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=3608749948:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi) % 59.76/9.05 % (1096474)Instruction limit reached! % 59.76/9.05 % (1096474)------------------------------ % 59.76/9.05 % (1096474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.76/9.05 % (1096474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.76/9.05 % (1096474)CaDiCaL version: 2.1.3 % 81.71/12.19 % (1096474)Termination reason: Instruction limit % 81.71/12.19 % (1096474)Termination phase: Saturation % 81.71/12.19 % (1096474)Time elapsed: 0.179 s % 81.71/12.19 % (1096474)Peak memory usage: 96 MB % 81.71/12.19 % (1096474)Instructions burned: 414 (million) % 81.71/12.19 % (1096476)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=3337855699:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi) % 81.71/12.19 % (1096466)Instruction limit reached! % 81.71/12.19 % (1096466)------------------------------ % 81.71/12.19 % (1096466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.71/12.19 % (1096466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.71/12.19 % (1096466)CaDiCaL version: 2.1.3 % 81.71/12.19 % (1096466)Termination reason: Instruction limit % 81.71/12.19 % (1096466)Termination phase: Saturation % 81.71/12.19 % (1096466)Time elapsed: 1.977 s % 81.71/12.19 % (1096466)Peak memory usage: 154 MB % 81.71/12.19 % (1096466)Instructions burned: 3258 (million) % 81.71/12.19 % (1096478)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=4171389251:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2962 on theBenchmark for (2962ds/303Mi) % 81.71/12.19 % (1096478)Instruction limit reached! % 81.71/12.19 % (1096478)------------------------------ % 81.71/12.19 % (1096478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.71/12.19 % (1096478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.71/12.19 % (1096478)CaDiCaL version: 2.1.3 % 81.71/12.19 % (1096478)Termination reason: Instruction limit % 81.71/12.19 % (1096478)Termination phase: Saturation % 81.71/12.19 % (1096478)Time elapsed: 0.152 s % 81.71/12.19 % (1096478)Peak memory usage: 94 MB % 81.71/12.19 % (1096478)Instructions burned: 305 (million) % 81.71/12.19 % (1096480)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1373692640:st=4:i=720:sd=3:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/720Mi) % 81.71/12.19 % (1096480)Instruction limit reached! % 81.71/12.19 % (1096480)------------------------------ % 81.71/12.19 % (1096480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.71/12.19 % (1096480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.71/12.19 % (1096480)CaDiCaL version: 2.1.3 % 81.71/12.19 % (1096480)Termination reason: Instruction limit % 81.71/12.19 % (1096480)Termination phase: Saturation % 81.71/12.19 % (1096480)Time elapsed: 0.338 s % 81.71/12.19 % (1096480)Peak memory usage: 97 MB % 81.71/12.19 % (1096480)Instructions burned: 722 (million) % 81.71/12.19 % (1096454)Instruction limit reached! % 81.71/12.19 % (1096454)------------------------------ % 81.71/12.19 % (1096454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.71/12.19 % (1096454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.71/12.19 % (1096454)CaDiCaL version: 2.1.3 % 81.71/12.19 % (1096454)Termination reason: Instruction limit % 81.71/12.19 % (1096454)Termination phase: Saturation % 81.71/12.19 % (1096454)Time elapsed: 3.608 s % 81.71/12.19 % (1096454)Peak memory usage: 166 MB % 81.71/12.19 % (1096454)Instructions burned: 5208 (million) % 81.71/12.19 % (1096482)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=100928232:i=598:bs=on:bd=preordered:av=off:ss=axioms_2954 on theBenchmark for (2954ds/598Mi) % 81.71/12.19 % (1096483)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2989770018:i=2989:sd=3:ss=axioms:sgt=60_2953 on theBenchmark for (2953ds/2989Mi) % 81.71/12.19 % (1096482)Instruction limit reached! % 81.71/12.19 % (1096482)------------------------------ % 81.71/12.19 % (1096482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.71/12.19 % (1096482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.71/12.19 % (1096482)CaDiCaL version: 2.1.3 % 81.71/12.19 % (1096482)Termination reason: Instruction limit % 81.71/12.19 % (1096482)Termination phase: Saturation % 81.71/12.19 % (1096482)Time elapsed: 0.228 s % 81.71/12.19 % (1096482)Peak memory usage: 92 MB % 81.71/12.19 % (1096482)Instructions burned: 600 (million) % 81.71/12.19 % (1096486)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=2321432387:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2950 on theBenchmark for (2950ds/1997Mi) % 118.45/17.38 % (1096486)Instruction limit reached! % 118.45/17.38 % (1096486)------------------------------ % 118.45/17.38 % (1096486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.45/17.38 % (1096486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.45/17.38 % (1096486)CaDiCaL version: 2.1.3 % 118.45/17.38 % (1096486)Termination reason: Instruction limit % 118.45/17.38 % (1096486)Termination phase: Saturation % 118.45/17.38 % (1096486)Time elapsed: 1.278 s % 118.45/17.38 % (1096486)Peak memory usage: 134 MB % 118.45/17.38 % (1096486)Instructions burned: 2000 (million) % 118.45/17.38 % (1096488)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=202300376:i=2088:bd=preordered:av=off_2936 on theBenchmark for (2936ds/2088Mi) % 118.45/17.38 % (1096483)Instruction limit reached! % 118.45/17.38 % (1096483)------------------------------ % 118.45/17.38 % (1096483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.45/17.38 % (1096483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.45/17.38 % (1096483)CaDiCaL version: 2.1.3 % 118.45/17.38 % (1096483)Termination reason: Instruction limit % 118.45/17.38 % (1096483)Termination phase: Saturation % 118.45/17.38 % (1096483)Time elapsed: 1.969 s % 118.45/17.38 % (1096483)Peak memory usage: 145 MB % 118.45/17.38 % (1096483)Instructions burned: 2989 (million) % 118.45/17.38 % (1096490)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2403600076:i=1098:nicw=on_2932 on theBenchmark for (2932ds/1098Mi) % 118.45/17.38 % (1096490)Instruction limit reached! % 118.45/17.38 % (1096490)------------------------------ % 118.45/17.38 % (1096490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.45/17.38 % (1096490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.45/17.38 % (1096490)CaDiCaL version: 2.1.3 % 118.45/17.38 % (1096490)Termination reason: Instruction limit % 118.45/17.38 % (1096490)Termination phase: Saturation % 118.45/17.38 % (1096490)Time elapsed: 0.415 s % 118.45/17.38 % (1096490)Peak memory usage: 99 MB % 118.45/17.38 % (1096490)Instructions burned: 1099 (million) % 118.45/17.38 % (1096492)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1854251549:i=433:bd=preordered_2926 on theBenchmark for (2926ds/433Mi) % 118.45/17.38 % (1096492)Instruction limit reached! % 118.45/17.38 % (1096492)------------------------------ % 118.45/17.38 % (1096492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.45/17.38 % (1096492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.45/17.38 % (1096492)CaDiCaL version: 2.1.3 % 118.45/17.38 % (1096492)Termination reason: Instruction limit % 118.45/17.38 % (1096492)Termination phase: Saturation % 118.45/17.38 % (1096492)Time elapsed: 0.164 s % 118.45/17.38 % (1096492)Peak memory usage: 91 MB % 118.45/17.38 % (1096492)Instructions burned: 433 (million) % 118.45/17.38 % (1096488)Instruction limit reached! % 118.45/17.38 % (1096488)------------------------------ % 118.45/17.38 % (1096488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.45/17.38 % (1096488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.45/17.38 % (1096488)CaDiCaL version: 2.1.3 % 118.45/17.38 % (1096488)Termination reason: Instruction limit % 118.45/17.38 % (1096488)Termination phase: Saturation % 118.45/17.38 % (1096488)Time elapsed: 1.313 s % 118.45/17.38 % (1096488)Peak memory usage: 141 MB % 118.45/17.38 % (1096488)Instructions burned: 2089 (million) % 118.45/17.38 % (1096494)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2864257340:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2922 on theBenchmark for (2922ds/2942Mi) % 118.45/17.38 % (1096496)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1930448894:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2921 on theBenchmark for (2921ds/6922Mi) % 118.45/17.38 % (1096476)Instruction limit reached! % 118.45/17.38 % (1096476)------------------------------ % 118.45/17.38 % (1096476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.45/17.38 % (1096476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.45/17.38 % (1096476)CaDiCaL version: 2.1.3 % 118.45/17.38 % (1096476)Termination reason: Instruction limit % 118.45/17.38 % (1096476)Termination phase: Saturation % 118.45/17.38 % (1096476)Time elapsed: 4.974 s % 136.37/20.01 % (1096476)Peak memory usage: 195 MB % 136.37/20.01 % (1096476)Instructions burned: 8478 (million) % 136.37/20.01 % (1096498)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=425128097:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2915 on theBenchmark for (2915ds/596Mi) % 136.37/20.01 % (1096472)Instruction limit reached! % 136.37/20.01 % (1096472)------------------------------ % 136.37/20.01 % (1096472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.37/20.01 % (1096472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.37/20.01 % (1096472)CaDiCaL version: 2.1.3 % 136.37/20.01 % (1096472)Termination reason: Instruction limit % 136.37/20.01 % (1096472)Termination phase: Saturation % 136.37/20.01 % (1096472)Time elapsed: 6.356 s % 136.37/20.01 % (1096472)Peak memory usage: 192 MB % 136.37/20.01 % (1096472)Instructions burned: 10309 (million) % 136.37/20.01 % (1096498)Instruction limit reached! % 136.37/20.01 % (1096498)------------------------------ % 136.37/20.01 % (1096498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.37/20.01 % (1096498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.37/20.01 % (1096498)CaDiCaL version: 2.1.3 % 136.37/20.01 % (1096498)Termination reason: Instruction limit % 136.37/20.01 % (1096498)Termination phase: Saturation % 136.37/20.01 % (1096498)Time elapsed: 0.307 s % 136.37/20.01 % (1096498)Peak memory usage: 96 MB % 136.37/20.01 % (1096498)Instructions burned: 597 (million) % 136.37/20.01 % (1096500)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=3719281674:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2912 on theBenchmark for (2912ds/4123Mi) % 136.37/20.01 % (1096501)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4158653351:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2911 on theBenchmark for (2911ds/16411Mi) % 136.37/20.01 % (1096494)Instruction limit reached! % 136.37/20.01 % (1096494)------------------------------ % 136.37/20.01 % (1096494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.37/20.01 % (1096494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.37/20.01 % (1096494)CaDiCaL version: 2.1.3 % 136.37/20.01 % (1096494)Termination reason: Instruction limit % 136.37/20.01 % (1096494)Termination phase: Saturation % 136.37/20.01 % (1096494)Time elapsed: 1.818 s % 136.37/20.01 % (1096494)Peak memory usage: 147 MB % 136.37/20.01 % (1096494)Instructions burned: 2943 (million) % 136.37/20.01 % (1096504)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=869728833:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2903 on theBenchmark for (2903ds/1670Mi) % 136.37/20.01 % (1096504)Instruction limit reached! % 136.37/20.01 % (1096504)------------------------------ % 136.37/20.01 % (1096504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.37/20.01 % (1096504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.37/20.01 % (1096504)CaDiCaL version: 2.1.3 % 136.37/20.01 % (1096504)Termination reason: Instruction limit % 136.37/20.01 % (1096504)Termination phase: Saturation % 136.37/20.01 % (1096504)Time elapsed: 1.044 s % 136.37/20.01 % (1096504)Peak memory usage: 136 MB % 136.37/20.01 % (1096504)Instructions burned: 1671 (million) % 136.37/20.01 % (1096506)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=1431687918:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2891 on theBenchmark for (2891ds/1722Mi) % 136.37/20.01 % (1096500)Instruction limit reached! % 136.37/20.01 % (1096500)------------------------------ % 136.37/20.01 % (1096500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.37/20.01 % (1096500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.37/20.01 % (1096500)CaDiCaL version: 2.1.3 % 136.37/20.01 % (1096500)Termination reason: Instruction limit % 136.37/20.01 % (1096500)Termination phase: Saturation % 136.37/20.01 % (1096500)Time elapsed: 2.447 s % 136.37/20.01 % (1096500)Peak memory usage: 161 MB % 136.37/20.01 % (1096500)Instructions burned: 4124 (million) % 136.37/20.01 % (1096508)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=3317248147:cts=off:cond=on:i=9530:bs=on:fsd=on_2886 on theBenchmark for (2886ds/9530Mi) % 162.43/23.54 % (1096506)Instruction limit reached! % 162.43/23.54 % (1096506)------------------------------ % 162.43/23.54 % (1096506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.43/23.54 % (1096506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.43/23.54 % (1096506)CaDiCaL version: 2.1.3 % 162.43/23.54 % (1096506)Termination reason: Instruction limit % 162.43/23.54 % (1096506)Termination phase: Saturation % 162.43/23.54 % (1096506)Time elapsed: 1.148 s % 162.43/23.54 % (1096506)Peak memory usage: 135 MB % 162.43/23.54 % (1096506)Instructions burned: 1722 (million) % 162.43/23.54 % (1096510)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=547394445:st=2:i=4495:sd=10:ss=included_2877 on theBenchmark for (2877ds/4495Mi) % 162.43/23.54 % (1096496)Instruction limit reached! % 162.43/23.54 % (1096496)------------------------------ % 162.43/23.54 % (1096496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.43/23.54 % (1096496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.43/23.54 % (1096496)CaDiCaL version: 2.1.3 % 162.43/23.54 % (1096496)Termination reason: Instruction limit % 162.43/23.54 % (1096496)Termination phase: Saturation % 162.43/23.54 % (1096496)Time elapsed: 4.849 s % 162.43/23.54 % (1096496)Peak memory usage: 180 MB % 162.43/23.54 % (1096496)Instructions burned: 6923 (million) % 162.43/23.54 % (1096512)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=2716072166:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2871 on theBenchmark for (2871ds/4920Mi) % 162.43/23.54 % (1096508)Instruction limit reached! % 162.43/23.54 % (1096508)------------------------------ % 162.43/23.54 % (1096508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.43/23.54 % (1096508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.43/23.54 % (1096508)CaDiCaL version: 2.1.3 % 162.43/23.54 % (1096508)Termination reason: Instruction limit % 162.43/23.54 % (1096508)Termination phase: Saturation % 162.43/23.54 % (1096508)Time elapsed: 3.706 s % 162.43/23.54 % (1096508)Peak memory usage: 138 MB % 162.43/23.54 % (1096508)Instructions burned: 9532 (million) % 162.43/23.54 % (1096510)Instruction limit reached! % 162.43/23.54 % (1096510)------------------------------ % 162.43/23.54 % (1096510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.43/23.54 % (1096510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.43/23.54 % (1096510)CaDiCaL version: 2.1.3 % 162.43/23.54 % (1096510)Termination reason: Instruction limit % 162.43/23.54 % (1096510)Termination phase: Saturation % 162.43/23.54 % (1096510)Time elapsed: 3.041 s % 162.43/23.54 % (1096510)Peak memory usage: 157 MB % 162.43/23.54 % (1096510)Instructions burned: 4495 (million) % 162.43/23.54 % (1096789)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=1460853658:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2847 on theBenchmark for (2847ds/2083Mi) % 162.43/23.54 % (1096791)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=3742819233:i=4629:av=off:gsp=on_2845 on theBenchmark for (2845ds/4629Mi) % 162.43/23.54 % (1096512)Instruction limit reached! % 162.43/23.54 % (1096512)------------------------------ % 162.43/23.54 % (1096512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.43/23.54 % (1096512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.43/23.54 % (1096512)CaDiCaL version: 2.1.3 % 162.43/23.54 % (1096512)Termination reason: Instruction limit % 162.43/23.54 % (1096512)Termination phase: Saturation % 162.43/23.54 % (1096512)Time elapsed: 2.979 s % 162.43/23.54 % (1096512)Peak memory usage: 212 MB % 162.43/23.54 % (1096512)Instructions burned: 4920 (million) % 162.43/23.54 % (1096793)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1013408577:i=1258:av=off_2839 on theBenchmark for (2839ds/1258Mi) % 162.43/23.54 % (1096789)Instruction limit reached! % 162.43/23.54 % (1096789)------------------------------ % 162.43/23.54 % (1096789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.43/23.54 % (1096789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.43/23.54 % (1096789)CaDiCaL version: 2.1.3 % 162.43/23.54 % (1096789)Termination reason: Instruction limit % 162.43/23.54 % (1096789)Termination phase: Saturation % 185.46/26.81 % (1096789)Time elapsed: 1.302 s % 185.46/26.81 % (1096789)Peak memory usage: 136 MB % 185.46/26.81 % (1096789)Instructions burned: 2084 (million) % 185.46/26.81 % (1096793)Instruction limit reached! % 185.46/26.81 % (1096793)------------------------------ % 185.46/26.81 % (1096793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.46/26.81 % (1096793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.46/26.81 % (1096793)CaDiCaL version: 2.1.3 % 185.46/26.81 % (1096793)Termination reason: Instruction limit % 185.46/26.81 % (1096793)Termination phase: Saturation % 185.46/26.81 % (1096793)Time elapsed: 0.649 s % 185.46/26.81 % (1096793)Peak memory usage: 111 MB % 185.46/26.81 % (1096793)Instructions burned: 1259 (million) % 185.46/26.81 % (1096795)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4140235853:i=7343:av=off:ss=included_2832 on theBenchmark for (2832ds/7343Mi) % 185.46/26.81 % (1096796)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1051126512:i=1325:sd=2:ss=axioms:sgt=16_2831 on theBenchmark for (2831ds/1325Mi) % 185.46/26.81 % (1096796)Instruction limit reached! % 185.46/26.81 % (1096796)------------------------------ % 185.46/26.81 % (1096796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.46/26.81 % (1096796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.46/26.81 % (1096796)CaDiCaL version: 2.1.3 % 185.46/26.81 % (1096796)Termination reason: Instruction limit % 185.46/26.81 % (1096796)Termination phase: Saturation % 185.46/26.81 % (1096796)Time elapsed: 0.446 s % 185.46/26.81 % (1096796)Peak memory usage: 96 MB % 185.46/26.81 % (1096796)Instructions burned: 1327 (million) % 185.46/26.81 % (1096799)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=1689263542:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2825 on theBenchmark for (2825ds/2646Mi) % 185.46/26.81 % (1096791)Instruction limit reached! % 185.46/26.81 % (1096791)------------------------------ % 185.46/26.81 % (1096791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.46/26.81 % (1096791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.46/26.81 % (1096791)CaDiCaL version: 2.1.3 % 185.46/26.81 % (1096791)Termination reason: Instruction limit % 185.46/26.81 % (1096791)Termination phase: Saturation % 185.46/26.81 % (1096791)Time elapsed: 2.341 s % 185.46/26.81 % (1096791)Peak memory usage: 139 MB % 185.46/26.81 % (1096791)Instructions burned: 4630 (million) % 185.46/26.81 % (1096801)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3393231328:i=1489:sd=2:ep=R:ss=axioms_2820 on theBenchmark for (2820ds/1489Mi) % 185.46/26.81 % (1096501)Instruction limit reached! % 185.46/26.81 % (1096501)------------------------------ % 185.46/26.81 % (1096501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.46/26.81 % (1096501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.46/26.81 % (1096501)CaDiCaL version: 2.1.3 % 185.46/26.81 % (1096501)Termination reason: Instruction limit % 185.46/26.81 % (1096501)Termination phase: Saturation % 185.46/26.81 % (1096501)Time elapsed: 9.821 s % 185.46/26.81 % (1096501)Peak memory usage: 181 MB % 185.46/26.81 % (1096501)Instructions burned: 16412 (million) % 185.46/26.81 % (1096803)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=4280357359:i=1503_2811 on theBenchmark for (2811ds/1503Mi) % 185.46/26.81 % (1096801)Instruction limit reached! % 185.46/26.81 % (1096801)------------------------------ % 185.46/26.81 % (1096801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.46/26.81 % (1096801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 185.46/26.81 % (1096801)CaDiCaL version: 2.1.3 % 185.46/26.81 % (1096801)Termination reason: Instruction limit % 185.46/26.81 % (1096801)Termination phase: Saturation % 185.46/26.81 % (1096801)Time elapsed: 0.956 s % 185.46/26.81 % (1096801)Peak memory usage: 132 MB % 185.46/26.81 % (1096801)Instructions burned: 1489 (million) % 185.46/26.81 % (1096805)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2754933880:i=13942:kws=frequency_2809 on theBenchmark for (2809ds/13942Mi) % 185.46/26.81 % (1096799)Instruction limit reached! % 185.46/26.81 % (1096799)------------------------------ % 185.46/26.81 % (1096799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 185.46/26.81 % (1096799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.67/30.35 % (1096799)CaDiCaL version: 2.1.3 % 210.67/30.35 % (1096799)Termination reason: Instruction limit % 210.67/30.35 % (1096799)Termination phase: Saturation % 210.67/30.35 % (1096799)Time elapsed: 1.705 s % 210.67/30.35 % (1096799)Peak memory usage: 139 MB % 210.67/30.35 % (1096799)Instructions burned: 2648 (million) % 210.67/30.35 % (1096807)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=2184475747:i=3604:fsr=off:er=filter_2806 on theBenchmark for (2806ds/3604Mi) % 210.67/30.35 % (1096803)Instruction limit reached! % 210.67/30.35 % (1096803)------------------------------ % 210.67/30.35 % (1096803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.67/30.35 % (1096803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.67/30.35 % (1096803)CaDiCaL version: 2.1.3 % 210.67/30.35 % (1096803)Termination reason: Instruction limit % 210.67/30.35 % (1096803)Termination phase: Saturation % 210.67/30.35 % (1096803)Time elapsed: 0.999 s % 210.67/30.35 % (1096803)Peak memory usage: 134 MB % 210.67/30.35 % (1096803)Instructions burned: 1503 (million) % 210.67/30.35 % (1096810)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=610544312:i=1876:sd=1:ss=included:sgt=32_2799 on theBenchmark for (2799ds/1876Mi) % 210.67/30.35 % (1096810)Instruction limit reached! % 210.67/30.35 % (1096810)------------------------------ % 210.67/30.35 % (1096810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.67/30.35 % (1096810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.67/30.35 % (1096810)CaDiCaL version: 2.1.3 % 210.67/30.35 % (1096810)Termination reason: Instruction limit % 210.67/30.35 % (1096810)Termination phase: Saturation % 210.67/30.35 % (1096810)Time elapsed: 1.201 s % 210.67/30.35 % (1096810)Peak memory usage: 138 MB % 210.67/30.35 % (1096810)Instructions burned: 1877 (million) % 210.67/30.35 % (1096812)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=314059403:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2785 on theBenchmark for (2785ds/1932Mi) % 210.67/30.35 % (1096807)Instruction limit reached! % 210.67/30.35 % (1096807)------------------------------ % 210.67/30.35 % (1096807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.67/30.35 % (1096807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.67/30.35 % (1096807)CaDiCaL version: 2.1.3 % 210.67/30.35 % (1096807)Termination reason: Instruction limit % 210.67/30.35 % (1096807)Termination phase: Saturation % 210.67/30.35 % (1096807)Time elapsed: 2.415 s % 210.67/30.35 % (1096807)Peak memory usage: 156 MB % 210.67/30.35 % (1096807)Instructions burned: 3605 (million) % 210.67/30.35 % (1096795)Instruction limit reached! % 210.67/30.35 % (1096795)------------------------------ % 210.67/30.35 % (1096795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.67/30.35 % (1096795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.67/30.35 % (1096795)CaDiCaL version: 2.1.3 % 210.67/30.35 % (1096795)Termination reason: Instruction limit % 210.67/30.35 % (1096795)Termination phase: Saturation % 210.67/30.35 % (1096795)Time elapsed: 5.171 s % 210.67/30.35 % (1096795)Peak memory usage: 184 MB % 210.67/30.35 % (1096795)Instructions burned: 7344 (million) % 210.67/30.35 % (1096814)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=2808709548:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2780 on theBenchmark for (2780ds/1980Mi) % 210.67/30.35 % (1096815)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=924085070:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2779 on theBenchmark for (2779ds/3902Mi) % 210.67/30.35 % (1096812)Refutation not found, incomplete strategy % 210.67/30.35 % (1096812)------------------------------ % 210.67/30.35 % (1096812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.67/30.35 % (1096812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.67/30.35 % (1096812)CaDiCaL version: 2.1.3 % 210.67/30.35 % (1096812)Termination reason: Refutation not found, incomplete strategy % 210.67/30.35 % (1096812)Time elapsed: 1.136 s % 210.67/30.35 % (1096812)Peak memory usage: 136 MB % 210.67/30.35 % (1096812)Instructions burned: 1649 (million) % 210.67/30.35 % (1096815)Refutation not found, incomplete strategy % 240.46/34.51 % (1096815)------------------------------ % 240.46/34.51 % (1096815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.46/34.51 % (1096815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.46/34.51 % (1096815)CaDiCaL version: 2.1.3 % 240.46/34.51 % (1096815)Termination reason: Refutation not found, incomplete strategy % 240.46/34.51 % (1096815)Time elapsed: 0.626 s % 240.46/34.51 % (1096815)Peak memory usage: 130 MB % 240.46/34.51 % (1096815)Instructions burned: 977 (million) % 240.46/34.51 % (1096812)------------------------------ % 240.46/34.51 % (1096812)------------------------------ % 240.46/34.51 % (1096815)------------------------------ % 240.46/34.51 % (1096815)------------------------------ % 240.46/34.51 % (1096818)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2745027042:avsq=on:i=3916:aac=none:amm=off_2770 on theBenchmark for (2770ds/3916Mi) % 240.46/34.51 % (1096820)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=327132445:cond=on:i=3940:av=off:er=known_2768 on theBenchmark for (2768ds/3940Mi) % 240.46/34.51 % (1096814)Instruction limit reached! % 240.46/34.51 % (1096814)------------------------------ % 240.46/34.51 % (1096814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.46/34.51 % (1096814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.46/34.51 % (1096814)CaDiCaL version: 2.1.3 % 240.46/34.51 % (1096814)Termination reason: Instruction limit % 240.46/34.51 % (1096814)Termination phase: Saturation % 240.46/34.51 % (1096814)Time elapsed: 1.287 s % 240.46/34.51 % (1096814)Peak memory usage: 138 MB % 240.46/34.51 % (1096814)Instructions burned: 1980 (million) % 240.46/34.51 % (1096822)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2722174856:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2765 on theBenchmark for (2765ds/3980Mi) % 240.46/34.51 % (1096818)Instruction limit reached! % 240.46/34.51 % (1096818)------------------------------ % 240.46/34.51 % (1096818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.46/34.51 % (1096818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.46/34.51 % (1096818)CaDiCaL version: 2.1.3 % 240.46/34.51 % (1096818)Termination reason: Instruction limit % 240.46/34.51 % (1096818)Termination phase: Saturation % 240.46/34.51 % (1096818)Time elapsed: 1.652 s % 240.46/34.51 % (1096818)Peak memory usage: 99 MB % 240.46/34.51 % (1096818)Instructions burned: 3918 (million) % 240.46/34.51 % (1096824)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=2228582720:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2751 on theBenchmark for (2751ds/2087Mi) % 240.46/34.51 % (1096820)Instruction limit reached! % 240.46/34.51 % (1096820)------------------------------ % 240.46/34.51 % (1096820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.46/34.51 % (1096820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.46/34.51 % (1096820)CaDiCaL version: 2.1.3 % 240.46/34.51 % (1096820)Termination reason: Instruction limit % 240.46/34.51 % (1096820)Termination phase: Saturation % 240.46/34.51 % (1096820)Time elapsed: 2.596 s % 240.46/34.51 % (1096820)Peak memory usage: 155 MB % 240.46/34.51 % (1096820)Instructions burned: 3941 (million) % 240.46/34.51 % (1096822)Instruction limit reached! % 240.46/34.51 % (1096822)------------------------------ % 240.46/34.51 % (1096822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.46/34.51 % (1096822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.46/34.51 % (1096822)CaDiCaL version: 2.1.3 % 240.46/34.51 % (1096822)Termination reason: Instruction limit % 240.46/34.51 % (1096822)Termination phase: Saturation % 240.46/34.51 % (1096822)Time elapsed: 2.407 s % 240.46/34.51 % (1096822)Peak memory usage: 158 MB % 240.46/34.51 % (1096822)Instructions burned: 3980 (million) % 240.46/34.51 % (1096826)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=2630812356:cts=off:cond=on:i=4272:bs=on:fsd=on_2740 on theBenchmark for (2740ds/4272Mi) % 240.46/34.51 % (1096827)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3924346759:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2740 on theBenchmark for (2740ds/2197Mi) % 285.11/40.84 % (1096824)Instruction limit reached! % 285.11/40.84 % (1096824)------------------------------ % 285.11/40.84 % (1096824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.11/40.84 % (1096824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.84 % (1096824)CaDiCaL version: 2.1.3 % 285.11/40.84 % (1096824)Termination reason: Instruction limit % 285.11/40.84 % (1096824)Termination phase: Saturation % 285.11/40.84 % (1096824)Time elapsed: 1.343 s % 285.11/40.84 % (1096824)Peak memory usage: 136 MB % 285.11/40.84 % (1096824)Instructions burned: 2088 (million) % 285.11/40.84 % (1096830)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2121085183:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2736 on theBenchmark for (2736ds/6508Mi) % 285.11/40.84 % (1096827)Instruction limit reached! % 285.11/40.84 % (1096827)------------------------------ % 285.11/40.84 % (1096827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.11/40.84 % (1096827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.84 % (1096827)CaDiCaL version: 2.1.3 % 285.11/40.84 % (1096827)Termination reason: Instruction limit % 285.11/40.84 % (1096827)Termination phase: Saturation % 285.11/40.84 % (1096827)Time elapsed: 1.468 s % 285.11/40.84 % (1096827)Peak memory usage: 139 MB % 285.11/40.84 % (1096827)Instructions burned: 2197 (million) % 285.11/40.84 % (1096832)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=1170267386:i=2330:fgj=on:av=off:fsr=off_2723 on theBenchmark for (2723ds/2330Mi) % 285.11/40.84 % (1096805)Instruction limit reached! % 285.11/40.84 % (1096805)------------------------------ % 285.11/40.84 % (1096805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.11/40.84 % (1096805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.84 % (1096805)CaDiCaL version: 2.1.3 % 285.11/40.84 % (1096805)Termination reason: Instruction limit % 285.11/40.84 % (1096805)Termination phase: Saturation % 285.11/40.84 % (1096805)Time elapsed: 8.645 s % 285.11/40.84 % (1096805)Peak memory usage: 194 MB % 285.11/40.84 % (1096805)Instructions burned: 13942 (million) % 285.11/40.84 % (1096834)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=411734354:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2720 on theBenchmark for (2720ds/7592Mi) % 285.11/40.84 % (1096826)Instruction limit reached! % 285.11/40.84 % (1096826)------------------------------ % 285.11/40.84 % (1096826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.11/40.84 % (1096826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.84 % (1096826)CaDiCaL version: 2.1.3 % 285.11/40.84 % (1096826)Termination reason: Instruction limit % 285.11/40.84 % (1096826)Termination phase: Saturation % 285.11/40.84 % (1096826)Time elapsed: 2.209 s % 285.11/40.84 % (1096826)Peak memory usage: 140 MB % 285.11/40.84 % (1096826)Instructions burned: 4274 (million) % 285.11/40.84 % (1096836)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=821342771:i=2693:kws=precedence:ins=1:av=off_2717 on theBenchmark for (2717ds/2693Mi) % 285.11/40.84 % (1096832)Instruction limit reached! % 285.11/40.84 % (1096832)------------------------------ % 285.11/40.84 % (1096832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.11/40.84 % (1096832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.84 % (1096832)CaDiCaL version: 2.1.3 % 285.11/40.84 % (1096832)Termination reason: Instruction limit % 285.11/40.84 % (1096832)Termination phase: Saturation % 285.11/40.84 % (1096832)Time elapsed: 1.423 s % 285.11/40.84 % (1096832)Peak memory usage: 142 MB % 285.11/40.84 % (1096832)Instructions burned: 2331 (million) % 285.11/40.84 % (1096838)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2589028217:i=28651:sd=4:ss=included:sgt=64_2707 on theBenchmark for (2707ds/28651Mi) % 285.11/40.84 % (1096830)Instruction limit reached! % 285.11/40.84 % (1096830)------------------------------ % 285.11/40.84 % (1096830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.11/40.84 % (1096830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.11/40.84 % (1096830)CaDiCaL version: 2.1.3 % 285.11/40.84 % (1096830)Termination reason: Instruction limit % 285.11/40.84 % (1096830)Termination phase: Saturation % 285.11/40.84 % (1096830)Time elapsed: 3.221 s % 285.11/40.84 % (1096830)Peak memory usage: 113 MB % 285.11/40.84 % (1096830)InstructiTerminated %------------------------------------------------------------------------------