%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX220-1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n018.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:46:13 PM UTC 2026 % Result : Timeout 300.83s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWX220-1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.19 % Computer : n018.cluster.edu % 0.08/0.19 % Model : x86_64 x86_64 % 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.19 % Memory : 8046.5625MB % 0.08/0.19 % OS : Linux 6.8.0-71-generic % 0.08/0.19 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 15:15:10 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.23 Running first-order theorem proving % 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.81/2.30 % (3473677)Input is clausal, will run a generic CNF schedule. % 11.81/2.30 % (3473684)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3122610387:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 11.81/2.30 % (3473687)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=41359391:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 11.81/2.30 % (3473685)lrs+10_1_sil=8000:sp=occurrence:random_seed=1525521736:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 11.81/2.30 % (3473686)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2429576556:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 11.81/2.30 % (3473683)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2858466910:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 11.81/2.30 % (3473688)dis-21_1_sil=8000:lcm=predicate:random_seed=2679544564: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) % 11.81/2.30 % (3473682)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=974912975:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 11.81/2.30 % (3473688)Refutation not found, incomplete strategy % 11.81/2.30 % (3473688)------------------------------ % 11.81/2.30 % (3473688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.81/2.30 % (3473688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.81/2.30 % (3473688)CaDiCaL version: 2.1.3 % 11.81/2.30 % (3473688)Termination reason: Refutation not found, incomplete strategy % 11.81/2.30 % (3473688)Time elapsed: 0.002 s % 11.81/2.30 % (3473688)Peak memory usage: 88 MB % 11.81/2.30 % (3473688)Instructions burned: 2 (million) % 11.81/2.30 % (3473686)Instruction limit reached! % 11.81/2.30 % (3473686)------------------------------ % 11.81/2.30 % (3473686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.81/2.30 % (3473686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.81/2.30 % (3473686)CaDiCaL version: 2.1.3 % 11.81/2.30 % (3473686)Termination reason: Instruction limit % 11.81/2.30 % (3473686)Termination phase: Saturation % 11.81/2.30 % (3473686)Time elapsed: 0.063 s % 11.81/2.30 % (3473686)Peak memory usage: 88 MB % 11.81/2.30 % (3473686)Instructions burned: 114 (million) % 11.81/2.30 % (3473685)Instruction limit reached! % 11.81/2.30 % (3473685)------------------------------ % 11.81/2.30 % (3473685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.81/2.30 % (3473685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.81/2.30 % (3473685)CaDiCaL version: 2.1.3 % 11.81/2.30 % (3473685)Termination reason: Instruction limit % 11.81/2.30 % (3473685)Termination phase: Saturation % 11.81/2.30 % (3473685)Time elapsed: 0.065 s % 11.81/2.30 % (3473685)Peak memory usage: 89 MB % 11.81/2.30 % (3473685)Instructions burned: 107 (million) % 11.81/2.30 % (3473687)Instruction limit reached! % 11.81/2.30 % (3473687)------------------------------ % 11.81/2.30 % (3473687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.81/2.30 % (3473687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.81/2.30 % (3473687)CaDiCaL version: 2.1.3 % 11.81/2.30 % (3473687)Termination reason: Instruction limit % 11.81/2.30 % (3473687)Termination phase: Saturation % 11.81/2.30 % (3473687)Time elapsed: 0.104 s % 11.81/2.30 % (3473687)Peak memory usage: 90 MB % 11.81/2.30 % (3473687)Instructions burned: 181 (million) % 11.81/2.30 % (3473696)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=1110647529:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 11.81/2.30 % (3473696)Refutation not found, incomplete strategy % 11.81/2.30 % (3473696)------------------------------ % 11.81/2.30 % (3473696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.81/2.30 % (3473696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.81/2.30 % (3473696)CaDiCaL version: 2.1.3 % 11.81/2.30 % (3473696)Termination reason: Refutation not found, incomplete strategy % 11.81/2.30 % (3473696)Time elapsed: 0.002 s % 11.81/2.30 % (3473696)Peak memory usage: 88 MB % 11.81/2.30 % (3473696)Instructions burned: 2 (million) % 11.81/2.30 % (3473697)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4070272651: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) % 21.27/3.78 % (3473697)Refutation not found, incomplete strategy % 21.27/3.78 % (3473697)------------------------------ % 21.27/3.78 % (3473697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.27/3.78 % (3473697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.27/3.78 % (3473697)CaDiCaL version: 2.1.3 % 21.27/3.78 % (3473697)Termination reason: Refutation not found, incomplete strategy % 21.27/3.78 % (3473697)Time elapsed: 0.004 s % 21.27/3.78 % (3473697)Peak memory usage: 88 MB % 21.27/3.78 % (3473697)Instructions burned: 5 (million) % 21.27/3.78 % (3473698)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2188963490:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 21.27/3.78 % (3473688)------------------------------ % 21.27/3.78 % (3473688)------------------------------ % 21.27/3.78 % (3473698)Refutation not found, incomplete strategy % 21.27/3.78 % (3473698)------------------------------ % 21.27/3.78 % (3473698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.27/3.78 % (3473698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.27/3.78 % (3473698)CaDiCaL version: 2.1.3 % 21.27/3.78 % (3473698)Termination reason: Refutation not found, incomplete strategy % 21.27/3.78 % (3473698)Time elapsed: 0.003 s % 21.27/3.78 % (3473698)Peak memory usage: 88 MB % 21.27/3.78 % (3473698)Instructions burned: 3 (million) % 21.27/3.78 % (3473702)lrs+10_64_to=lpo:sil=8000:random_seed=2482483492:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 21.27/3.78 % (3473696)------------------------------ % 21.27/3.78 % (3473696)------------------------------ % 21.27/3.78 % (3473697)------------------------------ % 21.27/3.78 % (3473697)------------------------------ % 21.27/3.78 % (3473702)Instruction limit reached! % 21.27/3.78 % (3473702)------------------------------ % 21.27/3.78 % (3473702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.27/3.78 % (3473702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.27/3.78 % (3473702)CaDiCaL version: 2.1.3 % 21.27/3.78 % (3473702)Termination reason: Instruction limit % 21.27/3.78 % (3473702)Termination phase: Saturation % 21.27/3.78 % (3473702)Time elapsed: 0.077 s % 21.27/3.78 % (3473702)Peak memory usage: 89 MB % 21.27/3.78 % (3473702)Instructions burned: 128 (million) % 21.27/3.78 % (3473698)------------------------------ % 21.27/3.78 % (3473698)------------------------------ % 21.27/3.78 % (3473704)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1148975267:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi) % 21.27/3.78 % (3473705)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4207555429:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 21.27/3.78 % (3473706)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3746782136:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 21.27/3.78 % (3473707)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=2947531361:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 21.27/3.78 % (3473704)Instruction limit reached! % 21.27/3.78 % (3473704)------------------------------ % 21.27/3.78 % (3473704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.27/3.78 % (3473704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.27/3.78 % (3473704)CaDiCaL version: 2.1.3 % 21.27/3.78 % (3473704)Termination reason: Instruction limit % 21.27/3.78 % (3473704)Termination phase: Saturation % 21.27/3.78 % (3473704)Time elapsed: 0.111 s % 21.27/3.78 % (3473704)Peak memory usage: 89 MB % 21.27/3.78 % (3473704)Instructions burned: 195 (million) % 21.27/3.78 % (3473705)Instruction limit reached! % 21.27/3.78 % (3473705)------------------------------ % 21.27/3.78 % (3473705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.27/3.78 % (3473705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.27/3.78 % (3473705)CaDiCaL version: 2.1.3 % 21.27/3.78 % (3473705)Termination reason: Instruction limit % 21.27/3.78 % (3473705)Termination phase: Saturation % 21.27/3.78 % (3473705)Time elapsed: 0.109 s % 21.27/3.78 % (3473705)Peak memory usage: 90 MB % 21.27/3.78 % (3473705)Instructions burned: 157 (million) % 34.53/5.63 % (3473707)Instruction limit reached! % 34.53/5.63 % (3473707)------------------------------ % 34.53/5.63 % (3473707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.53/5.63 % (3473707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.53/5.63 % (3473707)CaDiCaL version: 2.1.3 % 34.53/5.63 % (3473707)Termination reason: Instruction limit % 34.53/5.63 % (3473707)Termination phase: Saturation % 34.53/5.63 % (3473707)Time elapsed: 0.072 s % 34.53/5.63 % (3473707)Peak memory usage: 90 MB % 34.53/5.63 % (3473707)Instructions burned: 107 (million) % 34.53/5.63 % (3473712)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3503891694:i=107_2991 on theBenchmark for (2991ds/107Mi) % 34.53/5.63 % (3473712)Refutation not found, incomplete strategy % 34.53/5.63 % (3473712)------------------------------ % 34.53/5.63 % (3473712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.53/5.63 % (3473712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.53/5.63 % (3473712)CaDiCaL version: 2.1.3 % 34.53/5.63 % (3473712)Termination reason: Refutation not found, incomplete strategy % 34.53/5.63 % (3473712)Time elapsed: 0.002 s % 34.53/5.63 % (3473712)Peak memory usage: 88 MB % 34.53/5.63 % (3473712)Instructions burned: 2 (million) % 34.53/5.63 % (3473714)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4068196404:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi) % 34.53/5.63 % (3473713)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3831037179:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi) % 34.53/5.63 % (3473713)Instruction limit reached! % 34.53/5.63 % (3473713)------------------------------ % 34.53/5.63 % (3473713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.53/5.63 % (3473713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.53/5.63 % (3473713)CaDiCaL version: 2.1.3 % 34.53/5.63 % (3473713)Termination reason: Instruction limit % 34.53/5.63 % (3473713)Termination phase: Saturation % 34.53/5.63 % (3473713)Time elapsed: 0.138 s % 34.53/5.63 % (3473713)Peak memory usage: 90 MB % 34.53/5.63 % (3473713)Instructions burned: 242 (million) % 34.53/5.63 % (3473712)------------------------------ % 34.53/5.63 % (3473712)------------------------------ % 34.53/5.63 % (3473718)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=744891306:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi) % 34.53/5.63 % (3473718)Instruction limit reached! % 34.53/5.63 % (3473718)------------------------------ % 34.53/5.63 % (3473718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.53/5.63 % (3473718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.53/5.63 % (3473718)CaDiCaL version: 2.1.3 % 34.53/5.63 % (3473718)Termination reason: Instruction limit % 34.53/5.63 % (3473718)Termination phase: Saturation % 34.53/5.63 % (3473718)Time elapsed: 0.074 s % 34.53/5.63 % (3473718)Peak memory usage: 90 MB % 34.53/5.63 % (3473718)Instructions burned: 135 (million) % 34.53/5.63 % (3473719)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3972396450:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi) % 34.53/5.63 % (3473722)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1829623175:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi) % 34.53/5.63 % (3473722)Instruction limit reached! % 34.53/5.63 % (3473722)------------------------------ % 34.53/5.63 % (3473722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.53/5.63 % (3473722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.53/5.63 % (3473722)CaDiCaL version: 2.1.3 % 34.53/5.63 % (3473722)Termination reason: Instruction limit % 34.53/5.63 % (3473722)Termination phase: Saturation % 34.53/5.63 % (3473722)Time elapsed: 0.105 s % 34.53/5.63 % (3473722)Peak memory usage: 89 MB % 34.53/5.63 % (3473722)Instructions burned: 191 (million) % 34.53/5.63 % (3473719)Instruction limit reached! % 34.53/5.63 % (3473719)------------------------------ % 34.53/5.63 % (3473719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.53/5.63 % (3473719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.53/5.63 % (3473719)CaDiCaL version: 2.1.3 % 34.53/5.63 % (3473719)Termination reason: Instruction limit % 57.03/8.76 % (3473719)Termination phase: Saturation % 57.03/8.76 % (3473719)Time elapsed: 0.319 s % 57.03/8.76 % (3473719)Peak memory usage: 94 MB % 57.03/8.76 % (3473719)Instructions burned: 502 (million) % 57.03/8.76 % (3473725)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3515163511:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi) % 57.03/8.76 % (3473726)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2356540943:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi) % 57.03/8.76 % (3473725)Instruction limit reached! % 57.03/8.76 % (3473725)------------------------------ % 57.03/8.76 % (3473725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.03/8.76 % (3473725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.03/8.76 % (3473725)CaDiCaL version: 2.1.3 % 57.03/8.76 % (3473725)Termination reason: Instruction limit % 57.03/8.76 % (3473725)Termination phase: Saturation % 57.03/8.76 % (3473725)Time elapsed: 0.148 s % 57.03/8.76 % (3473725)Peak memory usage: 91 MB % 57.03/8.76 % (3473725)Instructions burned: 264 (million) % 57.03/8.76 % (3473726)Instruction limit reached! % 57.03/8.76 % (3473726)------------------------------ % 57.03/8.76 % (3473726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.03/8.76 % (3473726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.03/8.76 % (3473726)CaDiCaL version: 2.1.3 % 57.03/8.76 % (3473726)Termination reason: Instruction limit % 57.03/8.76 % (3473726)Termination phase: Saturation % 57.03/8.76 % (3473726)Time elapsed: 0.096 s % 57.03/8.76 % (3473726)Peak memory usage: 89 MB % 57.03/8.76 % (3473726)Instructions burned: 156 (million) % 57.03/8.76 % (3473729)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=3535930855:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi) % 57.03/8.76 % (3473730)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2211191194:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi) % 57.03/8.76 % (3473730)Instruction limit reached! % 57.03/8.76 % (3473730)------------------------------ % 57.03/8.76 % (3473730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.03/8.76 % (3473730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.03/8.76 % (3473730)CaDiCaL version: 2.1.3 % 57.03/8.76 % (3473730)Termination reason: Instruction limit % 57.03/8.76 % (3473730)Termination phase: Saturation % 57.03/8.76 % (3473730)Time elapsed: 0.279 s % 57.03/8.76 % (3473730)Peak memory usage: 91 MB % 57.03/8.76 % (3473730)Instructions burned: 538 (million) % 57.03/8.76 % (3473733)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1515627127:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi) % 57.03/8.76 % (3473733)Instruction limit reached! % 57.03/8.76 % (3473733)------------------------------ % 57.03/8.76 % (3473733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.03/8.76 % (3473733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.03/8.76 % (3473733)CaDiCaL version: 2.1.3 % 57.03/8.76 % (3473733)Termination reason: Instruction limit % 57.03/8.76 % (3473733)Termination phase: Saturation % 57.03/8.76 % (3473733)Time elapsed: 0.107 s % 57.03/8.76 % (3473733)Peak memory usage: 89 MB % 57.03/8.76 % (3473733)Instructions burned: 180 (million) % 57.03/8.76 % (3473735)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=4038352099:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi) % 57.03/8.76 % (3473706)Instruction limit reached! % 57.03/8.76 % (3473706)------------------------------ % 57.03/8.76 % (3473706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.03/8.76 % (3473706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.03/8.76 % (3473706)CaDiCaL version: 2.1.3 % 57.03/8.76 % (3473706)Termination reason: Instruction limit % 57.03/8.76 % (3473706)Termination phase: Saturation % 57.03/8.76 % (3473706)Time elapsed: 2.259 s % 57.03/8.76 % (3473706)Peak memory usage: 145 MB % 57.03/8.76 % (3473706)Instructions burned: 3395 (million) % 57.03/8.76 % (3473737)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=1737186893:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi) % 80.90/12.08 % (3473737)Instruction limit reached! % 80.90/12.08 % (3473737)------------------------------ % 80.90/12.08 % (3473737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.90/12.08 % (3473737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.90/12.08 % (3473737)CaDiCaL version: 2.1.3 % 80.90/12.08 % (3473737)Termination reason: Instruction limit % 80.90/12.08 % (3473737)Termination phase: Saturation % 80.90/12.08 % (3473737)Time elapsed: 0.227 s % 80.90/12.08 % (3473737)Peak memory usage: 96 MB % 80.90/12.08 % (3473737)Instructions burned: 412 (million) % 80.90/12.08 % (3473739)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=1135705535:s2pl=no:i=8478:s2at=4:nm=6_2966 on theBenchmark for (2966ds/8478Mi) % 80.90/12.08 % (3473729)Instruction limit reached! % 80.90/12.08 % (3473729)------------------------------ % 80.90/12.08 % (3473729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.90/12.08 % (3473729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.90/12.08 % (3473729)CaDiCaL version: 2.1.3 % 80.90/12.08 % (3473729)Termination reason: Instruction limit % 80.90/12.08 % (3473729)Termination phase: Saturation % 80.90/12.08 % (3473729)Time elapsed: 2.125 s % 80.90/12.08 % (3473729)Peak memory usage: 145 MB % 80.90/12.08 % (3473729)Instructions burned: 3256 (million) % 80.90/12.08 % (3473741)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=533630730:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2959 on theBenchmark for (2959ds/303Mi) % 80.90/12.08 % (3473714)Instruction limit reached! % 80.90/12.08 % (3473714)------------------------------ % 80.90/12.08 % (3473714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.90/12.08 % (3473714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.90/12.08 % (3473714)CaDiCaL version: 2.1.3 % 80.90/12.08 % (3473714)Termination reason: Instruction limit % 80.90/12.08 % (3473714)Termination phase: Saturation % 80.90/12.08 % (3473714)Time elapsed: 3.246 s % 80.90/12.08 % (3473714)Peak memory usage: 164 MB % 80.90/12.08 % (3473714)Instructions burned: 5209 (million) % 80.90/12.08 % (3473741)Refutation not found, incomplete strategy % 80.90/12.08 % (3473741)------------------------------ % 80.90/12.08 % (3473741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.90/12.08 % (3473741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.90/12.08 % (3473741)CaDiCaL version: 2.1.3 % 80.90/12.08 % (3473741)Termination reason: Refutation not found, incomplete strategy % 80.90/12.08 % (3473741)Time elapsed: 0.037 s % 80.90/12.08 % (3473741)Peak memory usage: 89 MB % 80.90/12.08 % (3473741)Instructions burned: 60 (million) % 80.90/12.08 % (3473743)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=832839133:st=4:i=720:sd=3:fsr=off:ss=axioms_2957 on theBenchmark for (2957ds/720Mi) % 80.90/12.08 % (3473743)Refutation not found, incomplete strategy % 80.90/12.08 % (3473743)------------------------------ % 80.90/12.08 % (3473743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.90/12.08 % (3473743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.90/12.08 % (3473743)CaDiCaL version: 2.1.3 % 80.90/12.08 % (3473743)Termination reason: Refutation not found, incomplete strategy % 80.90/12.08 % (3473743)Time elapsed: 0.003 s % 80.90/12.08 % (3473743)Peak memory usage: 88 MB % 80.90/12.08 % (3473743)Instructions burned: 4 (million) % 80.90/12.08 % (3473741)------------------------------ % 80.90/12.08 % (3473741)------------------------------ % 80.90/12.08 % (3473743)------------------------------ % 80.90/12.08 % (3473743)------------------------------ % 80.90/12.08 % (3473745)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2306032316:i=598:bs=on:bd=preordered:av=off:ss=axioms_2955 on theBenchmark for (2955ds/598Mi) % 80.90/12.08 % (3473746)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4102062859:i=2989:sd=3:ss=axioms:sgt=60_2954 on theBenchmark for (2954ds/2989Mi) % 80.90/12.08 % (3473745)Instruction limit reached! % 80.90/12.08 % (3473745)------------------------------ % 80.90/12.08 % (3473745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.90/12.08 % (3473745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.48/16.98 % (3473745)CaDiCaL version: 2.1.3 % 114.48/16.98 % (3473745)Termination reason: Instruction limit % 114.48/16.98 % (3473745)Termination phase: Saturation % 114.48/16.98 % (3473745)Time elapsed: 0.339 s % 114.48/16.98 % (3473745)Peak memory usage: 91 MB % 114.48/16.98 % (3473745)Instructions burned: 598 (million) % 114.48/16.98 % (3473749)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=1232596568:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2950 on theBenchmark for (2950ds/1997Mi) % 114.48/16.98 % (3473749)Instruction limit reached! % 114.48/16.98 % (3473749)------------------------------ % 114.48/16.98 % (3473749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.48/16.98 % (3473749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.48/16.98 % (3473749)CaDiCaL version: 2.1.3 % 114.48/16.98 % (3473749)Termination reason: Instruction limit % 114.48/16.98 % (3473749)Termination phase: Saturation % 114.48/16.98 % (3473749)Time elapsed: 1.337 s % 114.48/16.98 % (3473749)Peak memory usage: 137 MB % 114.48/16.98 % (3473749)Instructions burned: 1998 (million) % 114.48/16.98 % (3473751)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=380247153:i=2088:bd=preordered:av=off_2935 on theBenchmark for (2935ds/2088Mi) % 114.48/16.98 % (3473746)Instruction limit reached! % 114.48/16.98 % (3473746)------------------------------ % 114.48/16.98 % (3473746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.48/16.98 % (3473746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.48/16.98 % (3473746)CaDiCaL version: 2.1.3 % 114.48/16.98 % (3473746)Termination reason: Instruction limit % 114.48/16.98 % (3473746)Termination phase: Saturation % 114.48/16.98 % (3473746)Time elapsed: 1.948 s % 114.48/16.98 % (3473746)Peak memory usage: 141 MB % 114.48/16.98 % (3473746)Instructions burned: 2990 (million) % 114.48/16.98 % (3473753)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4066330581:i=1098:nicw=on_2933 on theBenchmark for (2933ds/1098Mi) % 114.48/16.98 % (3473753)Instruction limit reached! % 114.48/16.98 % (3473753)------------------------------ % 114.48/16.98 % (3473753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.48/16.98 % (3473753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.48/16.98 % (3473753)CaDiCaL version: 2.1.3 % 114.48/16.98 % (3473753)Termination reason: Instruction limit % 114.48/16.98 % (3473753)Termination phase: Saturation % 114.48/16.98 % (3473753)Time elapsed: 0.657 s % 114.48/16.98 % (3473753)Peak memory usage: 106 MB % 114.48/16.98 % (3473753)Instructions burned: 1098 (million) % 114.48/16.98 % (3473755)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3992688088:i=433:bd=preordered_2925 on theBenchmark for (2925ds/433Mi) % 114.48/16.98 % (3473755)Instruction limit reached! % 114.48/16.98 % (3473755)------------------------------ % 114.48/16.98 % (3473755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.48/16.98 % (3473755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.48/16.98 % (3473755)CaDiCaL version: 2.1.3 % 114.48/16.98 % (3473755)Termination reason: Instruction limit % 114.48/16.98 % (3473755)Termination phase: Saturation % 114.48/16.98 % (3473755)Time elapsed: 0.235 s % 114.48/16.98 % (3473755)Peak memory usage: 93 MB % 114.48/16.98 % (3473755)Instructions burned: 434 (million) % 114.48/16.98 % (3473751)Instruction limit reached! % 114.48/16.98 % (3473751)------------------------------ % 114.48/16.98 % (3473751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.48/16.98 % (3473751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.48/16.98 % (3473751)CaDiCaL version: 2.1.3 % 114.48/16.98 % (3473751)Termination reason: Instruction limit % 114.48/16.98 % (3473751)Termination phase: Saturation % 114.48/16.98 % (3473751)Time elapsed: 1.381 s % 114.48/16.98 % (3473751)Peak memory usage: 138 MB % 114.48/16.98 % (3473751)Instructions burned: 2088 (million) % 114.48/16.98 % (3473757)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=466266901:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2921 on theBenchmark for (2921ds/2942Mi) % 114.48/16.98 % (3473758)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=800778864:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2920 on theBenchmark for (2920ds/6922Mi) % 134.25/19.69 % (3473739)Instruction limit reached! % 134.25/19.69 % (3473739)------------------------------ % 134.25/19.69 % (3473739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.25/19.69 % (3473739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.25/19.69 % (3473739)CaDiCaL version: 2.1.3 % 134.25/19.69 % (3473739)Termination reason: Instruction limit % 134.25/19.69 % (3473739)Termination phase: Saturation % 134.25/19.69 % (3473739)Time elapsed: 4.821 s % 134.25/19.69 % (3473739)Peak memory usage: 193 MB % 134.25/19.69 % (3473739)Instructions burned: 8479 (million) % 134.25/19.69 % (3473761)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=2473978013:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2917 on theBenchmark for (2917ds/596Mi) % 134.25/19.69 % (3473761)Instruction limit reached! % 134.25/19.69 % (3473761)------------------------------ % 134.25/19.69 % (3473761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.25/19.69 % (3473761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.25/19.69 % (3473761)CaDiCaL version: 2.1.3 % 134.25/19.69 % (3473761)Termination reason: Instruction limit % 134.25/19.69 % (3473761)Termination phase: Saturation % 134.25/19.69 % (3473761)Time elapsed: 0.337 s % 134.25/19.69 % (3473761)Peak memory usage: 95 MB % 134.25/19.69 % (3473761)Instructions burned: 596 (million) % 134.25/19.69 % (3473763)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=3393411310:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2912 on theBenchmark for (2912ds/4123Mi) % 134.25/19.69 % (3473735)Instruction limit reached! % 134.25/19.69 % (3473735)------------------------------ % 134.25/19.69 % (3473735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.25/19.69 % (3473735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.25/19.69 % (3473735)CaDiCaL version: 2.1.3 % 134.25/19.69 % (3473735)Termination reason: Instruction limit % 134.25/19.69 % (3473735)Termination phase: Saturation % 134.25/19.69 % (3473735)Time elapsed: 6.804 s % 134.25/19.69 % (3473735)Peak memory usage: 184 MB % 134.25/19.69 % (3473735)Instructions burned: 10307 (million) % 134.25/19.69 % (3473765)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1684821821:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2905 on theBenchmark for (2905ds/16411Mi) % 134.25/19.69 % (3473757)Instruction limit reached! % 134.25/19.69 % (3473757)------------------------------ % 134.25/19.69 % (3473757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.25/19.69 % (3473757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.25/19.69 % (3473757)CaDiCaL version: 2.1.3 % 134.25/19.69 % (3473757)Termination reason: Instruction limit % 134.25/19.69 % (3473757)Termination phase: Saturation % 134.25/19.69 % (3473757)Time elapsed: 1.859 s % 134.25/19.69 % (3473757)Peak memory usage: 153 MB % 134.25/19.69 % (3473757)Instructions burned: 2943 (million) % 134.25/19.69 % (3473767)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2118225025:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2901 on theBenchmark for (2901ds/1670Mi) % 134.25/19.69 % (3473767)Instruction limit reached! % 134.25/19.69 % (3473767)------------------------------ % 134.25/19.69 % (3473767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.25/19.69 % (3473767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.25/19.69 % (3473767)CaDiCaL version: 2.1.3 % 134.25/19.69 % (3473767)Termination reason: Instruction limit % 134.25/19.69 % (3473767)Termination phase: Saturation % 134.25/19.69 % (3473767)Time elapsed: 1.047 s % 134.25/19.69 % (3473767)Peak memory usage: 134 MB % 134.25/19.69 % (3473767)Instructions burned: 1671 (million) % 134.25/19.69 % (3473769)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=2839600146:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2889 on theBenchmark for (2889ds/1722Mi) % 134.25/19.69 % (3473763)Instruction limit reached! % 134.25/19.69 % (3473763)------------------------------ % 134.25/19.69 % (3473763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.25/19.69 % (3473763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.25/19.69 % (3473763)CaDiCaL version: 2.1.3 % 152.95/22.24 % (3473763)Termination reason: Instruction limit % 152.95/22.24 % (3473763)Termination phase: Saturation % 152.95/22.24 % (3473763)Time elapsed: 2.510 s % 152.95/22.24 % (3473763)Peak memory usage: 157 MB % 152.95/22.24 % (3473763)Instructions burned: 4123 (million) % 152.95/22.24 % (3473771)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=965586130:cts=off:cond=on:i=9530:bs=on:fsd=on_2885 on theBenchmark for (2885ds/9530Mi) % 152.95/22.24 % (3473769)Refutation not found, incomplete strategy % 152.95/22.24 % (3473769)------------------------------ % 152.95/22.24 % (3473769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.95/22.24 % (3473769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.95/22.24 % (3473769)CaDiCaL version: 2.1.3 % 152.95/22.24 % (3473769)Termination reason: Refutation not found, incomplete strategy % 152.95/22.24 % (3473769)Time elapsed: 0.605 s % 152.95/22.24 % (3473769)Peak memory usage: 129 MB % 152.95/22.24 % (3473769)Instructions burned: 920 (million) % 152.95/22.24 % (3473769)------------------------------ % 152.95/22.24 % (3473769)------------------------------ % 152.95/22.24 % (3473773)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3190064810:st=2:i=4495:sd=10:ss=included_2879 on theBenchmark for (2879ds/4495Mi) % 152.95/22.24 % (3473758)Instruction limit reached! % 152.95/22.24 % (3473758)------------------------------ % 152.95/22.24 % (3473758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.95/22.24 % (3473758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.95/22.24 % (3473758)CaDiCaL version: 2.1.3 % 152.95/22.24 % (3473758)Termination reason: Instruction limit % 152.95/22.24 % (3473758)Termination phase: Saturation % 152.95/22.24 % (3473758)Time elapsed: 4.274 s % 152.95/22.24 % (3473758)Peak memory usage: 167 MB % 152.95/22.24 % (3473758)Instructions burned: 6923 (million) % 152.95/22.24 % (3473775)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=3588842524:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2876 on theBenchmark for (2876ds/4920Mi) % 152.95/22.24 % (3473773)Instruction limit reached! % 152.95/22.24 % (3473773)------------------------------ % 152.95/22.24 % (3473773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.95/22.24 % (3473773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.95/22.24 % (3473773)CaDiCaL version: 2.1.3 % 152.95/22.24 % (3473773)Termination reason: Instruction limit % 152.95/22.24 % (3473773)Termination phase: Saturation % 152.95/22.24 % (3473773)Time elapsed: 2.957 s % 152.95/22.24 % (3473773)Peak memory usage: 152 MB % 152.95/22.24 % (3473773)Instructions burned: 4496 (million) % 152.95/22.24 % (3473777)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=2392599002:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2848 on theBenchmark for (2848ds/2083Mi) % 152.95/22.24 % (3473775)Instruction limit reached! % 152.95/22.24 % (3473775)------------------------------ % 152.95/22.24 % (3473775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.95/22.24 % (3473775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.95/22.24 % (3473775)CaDiCaL version: 2.1.3 % 152.95/22.24 % (3473775)Termination reason: Instruction limit % 152.95/22.24 % (3473775)Termination phase: Saturation % 152.95/22.24 % (3473775)Time elapsed: 2.812 s % 152.95/22.24 % (3473775)Peak memory usage: 162 MB % 152.95/22.24 % (3473775)Instructions burned: 4920 (million) % 152.95/22.24 % (3473779)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=84364751:i=4629:av=off:gsp=on_2846 on theBenchmark for (2846ds/4629Mi) % 152.95/22.24 % (3473779)Refutation not found, incomplete strategy % 152.95/22.24 % (3473779)------------------------------ % 152.95/22.24 % (3473779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.95/22.24 % (3473779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.95/22.24 % (3473779)CaDiCaL version: 2.1.3 % 152.95/22.24 % (3473779)Termination reason: Refutation not found, incomplete strategy % 152.95/22.24 % (3473779)Time elapsed: 0.602 s % 152.95/22.24 % (3473779)Peak memory usage: 128 MB % 152.95/22.24 % (3473779)Instructions burned: 909 (million) % 152.95/22.24 % (3473779)------------------------------ % 180.16/26.12 % (3473779)------------------------------ % 180.16/26.12 % (3473781)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3722288275:i=1258:av=off_2836 on theBenchmark for (2836ds/1258Mi) % 180.16/26.12 % (3473781)Refutation not found, incomplete strategy % 180.16/26.12 % (3473781)------------------------------ % 180.16/26.12 % (3473781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.16/26.12 % (3473781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.16/26.12 % (3473781)CaDiCaL version: 2.1.3 % 180.16/26.12 % (3473781)Termination reason: Refutation not found, incomplete strategy % 180.16/26.12 % (3473781)Time elapsed: 0.024 s % 180.16/26.12 % (3473781)Peak memory usage: 88 MB % 180.16/26.12 % (3473781)Instructions burned: 40 (million) % 180.16/26.12 % (3473777)Instruction limit reached! % 180.16/26.12 % (3473777)------------------------------ % 180.16/26.12 % (3473777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.16/26.12 % (3473777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.16/26.12 % (3473777)CaDiCaL version: 2.1.3 % 180.16/26.12 % (3473777)Termination reason: Instruction limit % 180.16/26.12 % (3473777)Termination phase: Saturation % 180.16/26.12 % (3473777)Time elapsed: 1.399 s % 180.16/26.12 % (3473777)Peak memory usage: 137 MB % 180.16/26.12 % (3473777)Instructions burned: 2083 (million) % 180.16/26.12 % (3473781)------------------------------ % 180.16/26.12 % (3473781)------------------------------ % 180.16/26.12 % (3473783)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=944191192:i=7343:av=off:ss=included_2833 on theBenchmark for (2833ds/7343Mi) % 180.16/26.12 % (3473784)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2486885430:i=1325:sd=2:ss=axioms:sgt=16_2832 on theBenchmark for (2832ds/1325Mi) % 180.16/26.12 % (3473784)Instruction limit reached! % 180.16/26.12 % (3473784)------------------------------ % 180.16/26.12 % (3473784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.16/26.12 % (3473784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.16/26.12 % (3473784)CaDiCaL version: 2.1.3 % 180.16/26.12 % (3473784)Termination reason: Instruction limit % 180.16/26.12 % (3473784)Termination phase: Saturation % 180.16/26.12 % (3473784)Time elapsed: 0.700 s % 180.16/26.12 % (3473784)Peak memory usage: 93 MB % 180.16/26.12 % (3473784)Instructions burned: 1327 (million) % 180.16/26.12 % (3473771)Instruction limit reached! % 180.16/26.12 % (3473771)------------------------------ % 180.16/26.12 % (3473771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.16/26.12 % (3473771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.16/26.12 % (3473771)CaDiCaL version: 2.1.3 % 180.16/26.12 % (3473771)Termination reason: Instruction limit % 180.16/26.12 % (3473771)Termination phase: Saturation % 180.16/26.12 % (3473771)Time elapsed: 6.139 s % 180.16/26.12 % (3473771)Peak memory usage: 182 MB % 180.16/26.12 % (3473771)Instructions burned: 9530 (million) % 180.16/26.12 % (3473787)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=2788544461:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2824 on theBenchmark for (2824ds/2646Mi) % 180.16/26.12 % (3473789)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=4140341954:i=1489:sd=2:ep=R:ss=axioms_2823 on theBenchmark for (2823ds/1489Mi) % 180.16/26.12 % (3473789)Refutation not found, incomplete strategy % 180.16/26.12 % (3473789)------------------------------ % 180.16/26.12 % (3473789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.16/26.12 % (3473789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.16/26.12 % (3473789)CaDiCaL version: 2.1.3 % 180.16/26.12 % (3473789)Termination reason: Refutation not found, incomplete strategy % 180.16/26.12 % (3473789)Time elapsed: 0.581 s % 180.16/26.12 % (3473789)Peak memory usage: 127 MB % 180.16/26.12 % (3473789)Instructions burned: 860 (million) % 180.16/26.12 % (3473789)------------------------------ % 180.16/26.12 % (3473789)------------------------------ % 180.16/26.12 % (3473791)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=175019653:i=1503_2813 on theBenchmark for (2813ds/1503Mi) % 180.16/26.12 % (3473765)Instruction limit reached! % 180.16/26.12 % (3473765)------------------------------ % 180.16/26.12 % (3473765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.57/29.27 % (3473765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.57/29.27 % (3473765)CaDiCaL version: 2.1.3 % 202.57/29.27 % (3473765)Termination reason: Instruction limit % 202.57/29.27 % (3473765)Termination phase: Saturation % 202.57/29.27 % (3473765)Time elapsed: 9.443 s % 202.57/29.27 % (3473765)Peak memory usage: 239 MB % 202.57/29.27 % (3473765)Instructions burned: 16411 (million) % 202.57/29.27 % (3473793)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=251397986:i=13942:kws=frequency_2809 on theBenchmark for (2809ds/13942Mi) % 202.57/29.27 % (3473791)Refutation not found, incomplete strategy % 202.57/29.27 % (3473791)------------------------------ % 202.57/29.27 % (3473791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.57/29.27 % (3473791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.57/29.27 % (3473791)CaDiCaL version: 2.1.3 % 202.57/29.27 % (3473791)Termination reason: Refutation not found, incomplete strategy % 202.57/29.27 % (3473791)Time elapsed: 0.573 s % 202.57/29.27 % (3473791)Peak memory usage: 128 MB % 202.57/29.27 % (3473791)Instructions burned: 858 (million) % 202.57/29.27 % (3473787)Instruction limit reached! % 202.57/29.27 % (3473787)------------------------------ % 202.57/29.27 % (3473787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.57/29.27 % (3473787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.57/29.27 % (3473787)CaDiCaL version: 2.1.3 % 202.57/29.27 % (3473787)Termination reason: Instruction limit % 202.57/29.27 % (3473787)Termination phase: Saturation % 202.57/29.27 % (3473787)Time elapsed: 1.660 s % 202.57/29.27 % (3473787)Peak memory usage: 142 MB % 202.57/29.27 % (3473787)Instructions burned: 2646 (million) % 202.57/29.27 % (3473795)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=4288803994:i=3604:fsr=off:er=filter_2806 on theBenchmark for (2806ds/3604Mi) % 202.57/29.27 % (3473791)------------------------------ % 202.57/29.27 % (3473791)------------------------------ % 202.57/29.27 % (3473797)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1610677844:i=1876:sd=1:ss=included:sgt=32_2804 on theBenchmark for (2804ds/1876Mi) % 202.57/29.27 % (3473797)Instruction limit reached! % 202.57/29.27 % (3473797)------------------------------ % 202.57/29.27 % (3473797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.57/29.27 % (3473797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.57/29.27 % (3473797)CaDiCaL version: 2.1.3 % 202.57/29.27 % (3473797)Termination reason: Instruction limit % 202.57/29.27 % (3473797)Termination phase: Saturation % 202.57/29.27 % (3473797)Time elapsed: 1.245 s % 202.57/29.27 % (3473797)Peak memory usage: 136 MB % 202.57/29.27 % (3473797)Instructions burned: 1877 (million) % 202.57/29.27 % (3473799)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=476114191:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2790 on theBenchmark for (2790ds/1932Mi) % 202.57/29.27 % (3473783)Instruction limit reached! % 202.57/29.27 % (3473783)------------------------------ % 202.57/29.27 % (3473783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.57/29.27 % (3473783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.57/29.27 % (3473783)CaDiCaL version: 2.1.3 % 202.57/29.27 % (3473783)Termination reason: Instruction limit % 202.57/29.27 % (3473783)Termination phase: Saturation % 202.57/29.27 % (3473783)Time elapsed: 4.466 s % 202.57/29.27 % (3473783)Peak memory usage: 172 MB % 202.57/29.27 % (3473783)Instructions burned: 7344 (million) % 202.57/29.27 % (3473801)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=3741298803:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2787 on theBenchmark for (2787ds/1980Mi) % 202.57/29.27 % (3473795)Instruction limit reached! % 202.57/29.27 % (3473795)------------------------------ % 202.57/29.27 % (3473795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.57/29.27 % (3473795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.57/29.27 % (3473795)CaDiCaL version: 2.1.3 % 202.57/29.27 % (3473795)Termination reason: Instruction limit % 202.57/29.27 % (3473795)Termination phase: Saturation % 229.83/33.04 % (3473795)Time elapsed: 2.089 s % 229.83/33.04 % (3473795)Peak memory usage: 142 MB % 229.83/33.04 % (3473795)Instructions burned: 3605 (million) % 229.83/33.04 % (3473803)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=1278637403:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2784 on theBenchmark for (2784ds/3902Mi) % 229.83/33.04 % (3473803)Refutation not found, incomplete strategy % 229.83/33.04 % (3473803)------------------------------ % 229.83/33.04 % (3473803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.83/33.04 % (3473803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.83/33.04 % (3473803)CaDiCaL version: 2.1.3 % 229.83/33.04 % (3473803)Termination reason: Refutation not found, incomplete strategy % 229.83/33.04 % (3473803)Time elapsed: 0.601 s % 229.83/33.04 % (3473803)Peak memory usage: 128 MB % 229.83/33.04 % (3473803)Instructions burned: 905 (million) % 229.83/33.04 % (3473799)Instruction limit reached! % 229.83/33.04 % (3473799)------------------------------ % 229.83/33.04 % (3473799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.83/33.04 % (3473799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.83/33.04 % (3473799)CaDiCaL version: 2.1.3 % 229.83/33.04 % (3473799)Termination reason: Instruction limit % 229.83/33.04 % (3473799)Termination phase: Saturation % 229.83/33.04 % (3473799)Time elapsed: 1.291 s % 229.83/33.04 % (3473799)Peak memory usage: 134 MB % 229.83/33.04 % (3473799)Instructions burned: 1932 (million) % 229.83/33.04 % (3473805)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2003481332:avsq=on:i=3916:aac=none:amm=off_2775 on theBenchmark for (2775ds/3916Mi) % 229.83/33.04 % (3473803)------------------------------ % 229.83/33.04 % (3473803)------------------------------ % 229.83/33.04 % (3473801)Instruction limit reached! % 229.83/33.04 % (3473801)------------------------------ % 229.83/33.04 % (3473801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.83/33.04 % (3473801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.83/33.04 % (3473801)CaDiCaL version: 2.1.3 % 229.83/33.04 % (3473801)Termination reason: Instruction limit % 229.83/33.04 % (3473801)Termination phase: Saturation % 229.83/33.04 % (3473801)Time elapsed: 1.265 s % 229.83/33.04 % (3473801)Peak memory usage: 137 MB % 229.83/33.04 % (3473801)Instructions burned: 1980 (million) % 229.83/33.04 % (3473807)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2334076488:cond=on:i=3940:av=off:er=known_2774 on theBenchmark for (2774ds/3940Mi) % 229.83/33.04 % (3473808)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=3486326731:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2773 on theBenchmark for (2773ds/3980Mi) % 229.83/33.04 % (3473805)Instruction limit reached! % 229.83/33.04 % (3473805)------------------------------ % 229.83/33.04 % (3473805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.83/33.04 % (3473805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.83/33.04 % (3473805)CaDiCaL version: 2.1.3 % 229.83/33.04 % (3473805)Termination reason: Instruction limit % 229.83/33.04 % (3473805)Termination phase: Saturation % 229.83/33.04 % (3473805)Time elapsed: 2.080 s % 229.83/33.04 % (3473805)Peak memory usage: 139 MB % 229.83/33.04 % (3473805)Instructions burned: 3918 (million) % 229.83/33.04 % (3473811)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=2700051200:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2753 on theBenchmark for (2753ds/2087Mi) % 229.83/33.04 % (3473807)Instruction limit reached! % 229.83/33.04 % (3473807)------------------------------ % 229.83/33.04 % (3473807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.83/33.04 % (3473807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.83/33.04 % (3473807)CaDiCaL version: 2.1.3 % 229.83/33.04 % (3473807)Termination reason: Instruction limit % 229.83/33.04 % (3473807)Termination phase: Saturation % 229.83/33.04 % (3473807)Time elapsed: 2.621 s % 229.83/33.04 % (3473807)Peak memory usage: 151 MB % 229.83/33.04 % (3473807)Instructions burned: 3942 (million) % 229.83/33.04 % (3473808)Instruction limit reached! % 229.83/33.04 % (3473808)------------------------------ % 229.83/33.04 % (3473808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.83/33.04 % (3473808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.67/40.30 % (3473808)CaDiCaL version: 2.1.3 % 280.67/40.30 % (3473808)Termination reason: Instruction limit % 280.67/40.30 % (3473808)Termination phase: Saturation % 280.67/40.30 % (3473808)Time elapsed: 2.629 s % 280.67/40.30 % (3473808)Peak memory usage: 147 MB % 280.67/40.30 % (3473808)Instructions burned: 3980 (million) % 280.67/40.30 % (3473813)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=1951258636:cts=off:cond=on:i=4272:bs=on:fsd=on_2746 on theBenchmark for (2746ds/4272Mi) % 280.67/40.30 % (3473814)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1119808507:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2745 on theBenchmark for (2745ds/2197Mi) % 280.67/40.30 % (3473811)Instruction limit reached! % 280.67/40.30 % (3473811)------------------------------ % 280.67/40.30 % (3473811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.67/40.30 % (3473811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.67/40.30 % (3473811)CaDiCaL version: 2.1.3 % 280.67/40.30 % (3473811)Termination reason: Instruction limit % 280.67/40.30 % (3473811)Termination phase: Saturation % 280.67/40.30 % (3473811)Time elapsed: 1.415 s % 280.67/40.30 % (3473811)Peak memory usage: 140 MB % 280.67/40.30 % (3473811)Instructions burned: 2088 (million) % 280.67/40.30 % (3473817)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2571246516:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2738 on theBenchmark for (2738ds/6508Mi) % 280.67/40.30 % (3473814)Instruction limit reached! % 280.67/40.30 % (3473814)------------------------------ % 280.67/40.30 % (3473814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.67/40.30 % (3473814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.67/40.30 % (3473814)CaDiCaL version: 2.1.3 % 280.67/40.30 % (3473814)Termination reason: Instruction limit % 280.67/40.30 % (3473814)Termination phase: Saturation % 280.67/40.30 % (3473814)Time elapsed: 1.388 s % 280.67/40.30 % (3473814)Peak memory usage: 138 MB % 280.67/40.30 % (3473814)Instructions burned: 2197 (million) % 280.67/40.30 % (3473819)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=827221479:i=2330:fgj=on:av=off:fsr=off_2730 on theBenchmark for (2730ds/2330Mi) % 280.67/40.30 % (3473793)Instruction limit reached! % 280.67/40.30 % (3473793)------------------------------ % 280.67/40.30 % (3473793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.67/40.30 % (3473793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.67/40.30 % (3473793)CaDiCaL version: 2.1.3 % 280.67/40.30 % (3473793)Termination reason: Instruction limit % 280.67/40.30 % (3473793)Termination phase: Saturation % 280.67/40.30 % (3473793)Time elapsed: 8.382 s % 280.67/40.30 % (3473793)Peak memory usage: 218 MB % 280.67/40.30 % (3473793)Instructions burned: 13943 (million) % 280.67/40.30 % (3473821)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2682721555:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2724 on theBenchmark for (2724ds/7592Mi) % 280.67/40.30 % (3473813)Instruction limit reached! % 280.67/40.30 % (3473813)------------------------------ % 280.67/40.30 % (3473813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.67/40.30 % (3473813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.67/40.30 % (3473813)CaDiCaL version: 2.1.3 % 280.67/40.30 % (3473813)Termination reason: Instruction limit % 280.67/40.30 % (3473813)Termination phase: Saturation % 280.67/40.30 % (3473813)Time elapsed: 2.999 s % 280.67/40.30 % (3473813)Peak memory usage: 152 MB % 280.67/40.30 % (3473813)Instructions burned: 4273 (million) % 280.67/40.30 % (3473819)Instruction limit reached! % 280.67/40.30 % (3473819)------------------------------ % 280.67/40.30 % (3473819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.67/40.30 % (3473819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.67/40.30 % (3473819)CaDiCaL version: 2.1.3 % 280.67/40.30 % (3473819)Termination reason: Instruction limit % 280.67/40.30 % (3473819)Termination phase: Saturation % 280.67/40.30 % (3473819)Time elapsed: 1.387 s % 280.67/40.30 % (3473819)Peak memory usage: 141 MB % 280.67/40.30 % (3473819)Instructions burned: 2331 (million) % 280.67/40.30 % (3473823)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_unTerminated %------------------------------------------------------------------------------