%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV871-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:41 PM UTC 2026 % Result : Timeout 300.66s 43.07s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV871-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.18 % Computer : n003.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 12:48:42 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.22 Running first-order theorem proving % 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.88/2.09 % (1559072)Input is clausal, will run a generic CNF schedule. % 9.88/2.09 % (1559083)dis-21_1_sil=8000:lcm=predicate:random_seed=3301382038: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) % 9.88/2.09 % (1559083)Instruction limit reached! % 9.88/2.09 % (1559083)------------------------------ % 9.88/2.09 % (1559083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.88/2.09 % (1559083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.88/2.09 % (1559083)CaDiCaL version: 2.1.3 % 9.88/2.09 % (1559083)Termination reason: Instruction limit % 9.88/2.09 % (1559083)Termination phase: Saturation % 9.88/2.09 % (1559083)Time elapsed: 0.028 s % 9.88/2.09 % (1559083)Peak memory usage: 89 MB % 9.88/2.09 % (1559083)Instructions burned: 123 (million) % 9.88/2.09 % (1559080)lrs+10_1_sil=8000:sp=occurrence:random_seed=3126254207:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 9.88/2.09 % (1559077)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=799804461:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 9.88/2.09 % (1559082)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2294444456:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 9.88/2.09 % (1559078)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2593088074:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 9.88/2.09 % (1559079)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1778526579:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 9.88/2.09 % (1559081)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=59283027:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 9.88/2.09 % (1559081)Instruction limit reached! % 9.88/2.09 % (1559081)------------------------------ % 9.88/2.09 % (1559081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.88/2.09 % (1559081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.88/2.09 % (1559081)CaDiCaL version: 2.1.3 % 9.88/2.09 % (1559081)Termination reason: Instruction limit % 9.88/2.09 % (1559081)Termination phase: Saturation % 9.88/2.09 % (1559081)Time elapsed: 0.052 s % 9.88/2.09 % (1559081)Peak memory usage: 88 MB % 9.88/2.09 % (1559081)Instructions burned: 115 (million) % 9.88/2.09 % (1559080)Instruction limit reached! % 9.88/2.09 % (1559080)------------------------------ % 9.88/2.09 % (1559080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.88/2.09 % (1559080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.88/2.09 % (1559080)CaDiCaL version: 2.1.3 % 9.88/2.09 % (1559080)Termination reason: Instruction limit % 9.88/2.09 % (1559080)Termination phase: Saturation % 9.88/2.09 % (1559080)Time elapsed: 0.069 s % 9.88/2.09 % (1559080)Peak memory usage: 89 MB % 9.88/2.09 % (1559080)Instructions burned: 107 (million) % 9.88/2.09 % (1559082)Instruction limit reached! % 9.88/2.09 % (1559082)------------------------------ % 9.88/2.09 % (1559082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.88/2.09 % (1559082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.88/2.09 % (1559082)CaDiCaL version: 2.1.3 % 9.88/2.09 % (1559082)Termination reason: Instruction limit % 9.88/2.09 % (1559082)Termination phase: Saturation % 9.88/2.09 % (1559082)Time elapsed: 0.080 s % 9.88/2.09 % (1559082)Peak memory usage: 89 MB % 9.88/2.09 % (1559082)Instructions burned: 181 (million) % 9.88/2.09 % (1559085)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=438073399:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi) % 9.88/2.09 % (1559085)Instruction limit reached! % 9.88/2.09 % (1559085)------------------------------ % 9.88/2.09 % (1559085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.88/2.09 % (1559085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.88/2.09 % (1559085)CaDiCaL version: 2.1.3 % 9.88/2.09 % (1559085)Termination reason: Instruction limit % 9.88/2.09 % (1559085)Termination phase: Saturation % 9.88/2.09 % (1559085)Time elapsed: 0.047 s % 9.88/2.09 % (1559085)Peak memory usage: 90 MB % 9.88/2.09 % (1559085)Instructions burned: 145 (million) % 9.88/2.09 % (1559092)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3559191934: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) % 19.47/3.44 % (1559093)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2052232734:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 19.47/3.44 % (1559094)lrs+10_64_to=lpo:sil=8000:random_seed=3161299102:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi) % 19.47/3.44 % (1559096)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=201330719:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi) % 19.47/3.44 % (1559092)Instruction limit reached! % 19.47/3.44 % (1559092)------------------------------ % 19.47/3.44 % (1559092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.44 % (1559092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.44 % (1559092)CaDiCaL version: 2.1.3 % 19.47/3.44 % (1559092)Termination reason: Instruction limit % 19.47/3.44 % (1559092)Termination phase: Saturation % 19.47/3.44 % (1559092)Time elapsed: 0.109 s % 19.47/3.44 % (1559092)Peak memory usage: 90 MB % 19.47/3.44 % (1559092)Instructions burned: 189 (million) % 19.47/3.44 % (1559094)Instruction limit reached! % 19.47/3.44 % (1559094)------------------------------ % 19.47/3.44 % (1559094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.44 % (1559094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.44 % (1559094)CaDiCaL version: 2.1.3 % 19.47/3.44 % (1559094)Termination reason: Instruction limit % 19.47/3.44 % (1559094)Termination phase: Saturation % 19.47/3.44 % (1559094)Time elapsed: 0.077 s % 19.47/3.44 % (1559094)Peak memory usage: 91 MB % 19.47/3.44 % (1559094)Instructions burned: 126 (million) % 19.47/3.44 % (1559093)Instruction limit reached! % 19.47/3.44 % (1559093)------------------------------ % 19.47/3.44 % (1559093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.44 % (1559093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.44 % (1559093)CaDiCaL version: 2.1.3 % 19.47/3.44 % (1559093)Termination reason: Instruction limit % 19.47/3.44 % (1559093)Termination phase: Saturation % 19.47/3.44 % (1559093)Time elapsed: 0.127 s % 19.47/3.44 % (1559093)Peak memory usage: 91 MB % 19.47/3.44 % (1559093)Instructions burned: 220 (million) % 19.47/3.44 % (1559096)Instruction limit reached! % 19.47/3.44 % (1559096)------------------------------ % 19.47/3.44 % (1559096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.44 % (1559096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.44 % (1559096)CaDiCaL version: 2.1.3 % 19.47/3.44 % (1559096)Termination reason: Instruction limit % 19.47/3.44 % (1559096)Termination phase: Saturation % 19.47/3.44 % (1559096)Time elapsed: 0.055 s % 19.47/3.44 % (1559096)Peak memory usage: 90 MB % 19.47/3.44 % (1559096)Instructions burned: 199 (million) % 19.47/3.44 % (1559102)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1725559505:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi) % 19.47/3.44 % (1559101)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=357710742:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 19.47/3.44 % (1559104)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3685561847:i=107_2994 on theBenchmark for (2994ds/107Mi) % 19.47/3.44 % (1559103)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=2108047202:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi) % 19.47/3.44 % (1559104)Instruction limit reached! % 19.47/3.44 % (1559104)------------------------------ % 19.47/3.44 % (1559104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.47/3.44 % (1559104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.47/3.44 % (1559104)CaDiCaL version: 2.1.3 % 19.47/3.44 % (1559104)Termination reason: Instruction limit % 19.47/3.44 % (1559104)Termination phase: Saturation % 19.47/3.44 % (1559104)Time elapsed: 0.034 s % 19.47/3.44 % (1559104)Peak memory usage: 90 MB % 19.47/3.44 % (1559104)Instructions burned: 110 (million) % 19.47/3.44 % (1559101)Instruction limit reached! % 19.47/3.44 % (1559101)------------------------------ % 19.47/3.44 % (1559101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.79/6.48 % (1559101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.79/6.48 % (1559101)CaDiCaL version: 2.1.3 % 40.79/6.48 % (1559101)Termination reason: Instruction limit % 40.79/6.48 % (1559101)Termination phase: Saturation % 40.79/6.48 % (1559101)Time elapsed: 0.098 s % 40.79/6.48 % (1559101)Peak memory usage: 90 MB % 40.79/6.48 % (1559101)Instructions burned: 157 (million) % 40.79/6.48 % (1559103)Instruction limit reached! % 40.79/6.48 % (1559103)------------------------------ % 40.79/6.48 % (1559103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.79/6.48 % (1559103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.79/6.48 % (1559103)CaDiCaL version: 2.1.3 % 40.79/6.48 % (1559103)Termination reason: Instruction limit % 40.79/6.48 % (1559103)Termination phase: Saturation % 40.79/6.48 % (1559103)Time elapsed: 0.059 s % 40.79/6.48 % (1559103)Peak memory usage: 90 MB % 40.79/6.48 % (1559103)Instructions burned: 107 (million) % 40.79/6.48 % (1559109)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=751814825:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 40.79/6.48 % (1559110)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1255886806:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi) % 40.79/6.48 % (1559109)Instruction limit reached! % 40.79/6.48 % (1559109)------------------------------ % 40.79/6.48 % (1559109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.79/6.48 % (1559109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.79/6.48 % (1559109)CaDiCaL version: 2.1.3 % 40.79/6.48 % (1559109)Termination reason: Instruction limit % 40.79/6.48 % (1559109)Termination phase: Saturation % 40.79/6.48 % (1559109)Time elapsed: 0.074 s % 40.79/6.48 % (1559109)Peak memory usage: 90 MB % 40.79/6.48 % (1559109)Instructions burned: 242 (million) % 40.79/6.48 % (1559111)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2765950749:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi) % 40.79/6.48 % (1559111)Instruction limit reached! % 40.79/6.48 % (1559111)------------------------------ % 40.79/6.48 % (1559111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.79/6.48 % (1559111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.79/6.48 % (1559111)CaDiCaL version: 2.1.3 % 40.79/6.48 % (1559111)Termination reason: Instruction limit % 40.79/6.48 % (1559111)Termination phase: Saturation % 40.79/6.48 % (1559111)Time elapsed: 0.057 s % 40.79/6.48 % (1559111)Peak memory usage: 89 MB % 40.79/6.48 % (1559111)Instructions burned: 136 (million) % 40.79/6.48 % (1559114)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2383896851:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi) % 40.79/6.48 % (1559116)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1945049301:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi) % 40.79/6.48 % (1559114)Instruction limit reached! % 40.79/6.48 % (1559114)------------------------------ % 40.79/6.48 % (1559114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.79/6.48 % (1559114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.79/6.48 % (1559114)CaDiCaL version: 2.1.3 % 40.79/6.48 % (1559114)Termination reason: Instruction limit % 40.79/6.48 % (1559114)Termination phase: Saturation % 40.79/6.48 % (1559114)Time elapsed: 0.173 s % 40.79/6.48 % (1559114)Peak memory usage: 95 MB % 40.79/6.48 % (1559114)Instructions burned: 499 (million) % 40.79/6.48 % (1559116)Instruction limit reached! % 40.79/6.48 % (1559116)------------------------------ % 40.79/6.48 % (1559116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.79/6.48 % (1559116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.79/6.48 % (1559116)CaDiCaL version: 2.1.3 % 40.79/6.48 % (1559116)Termination reason: Instruction limit % 40.79/6.48 % (1559116)Termination phase: Saturation % 40.79/6.48 % (1559116)Time elapsed: 0.125 s % 40.79/6.48 % (1559116)Peak memory usage: 91 MB % 40.79/6.48 % (1559116)Instructions burned: 192 (million) % 40.79/6.48 % (1559119)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=984388303:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi) % 40.79/6.48 % (1559119)Instruction limit reached! % 40.79/6.48 % (1559119)------------------------------ % 50.21/7.95 % (1559119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.21/7.95 % (1559119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.21/7.95 % (1559119)CaDiCaL version: 2.1.3 % 50.21/7.95 % (1559119)Termination reason: Instruction limit % 50.21/7.95 % (1559119)Termination phase: Saturation % 50.21/7.95 % (1559119)Time elapsed: 0.069 s % 50.21/7.95 % (1559119)Peak memory usage: 90 MB % 50.21/7.95 % (1559119)Instructions burned: 273 (million) % 50.21/7.95 % (1559120)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3210862636:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi) % 50.21/7.95 % (1559120)Instruction limit reached! % 50.21/7.95 % (1559120)------------------------------ % 50.21/7.95 % (1559120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.21/7.95 % (1559120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.21/7.95 % (1559120)CaDiCaL version: 2.1.3 % 50.21/7.95 % (1559120)Termination reason: Instruction limit % 50.21/7.95 % (1559120)Termination phase: Saturation % 50.21/7.95 % (1559120)Time elapsed: 0.094 s % 50.21/7.95 % (1559120)Peak memory usage: 90 MB % 50.21/7.95 % (1559120)Instructions burned: 156 (million) % 50.21/7.95 % (1559122)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=3157813326:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi) % 50.21/7.95 % (1559124)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1555302525:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi) % 50.21/7.95 % (1559124)Instruction limit reached! % 50.21/7.95 % (1559124)------------------------------ % 50.21/7.95 % (1559124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.21/7.95 % (1559124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.21/7.95 % (1559124)CaDiCaL version: 2.1.3 % 50.21/7.95 % (1559124)Termination reason: Instruction limit % 50.21/7.95 % (1559124)Termination phase: Saturation % 50.21/7.95 % (1559124)Time elapsed: 0.229 s % 50.21/7.95 % (1559124)Peak memory usage: 90 MB % 50.21/7.95 % (1559124)Instructions burned: 539 (million) % 50.21/7.95 % (1559127)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2279073920:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi) % 50.21/7.95 % (1559127)Instruction limit reached! % 50.21/7.95 % (1559127)------------------------------ % 50.21/7.95 % (1559127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.21/7.95 % (1559127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.21/7.95 % (1559127)CaDiCaL version: 2.1.3 % 50.21/7.95 % (1559127)Termination reason: Instruction limit % 50.21/7.95 % (1559127)Termination phase: Saturation % 50.21/7.95 % (1559127)Time elapsed: 0.094 s % 50.21/7.95 % (1559127)Peak memory usage: 91 MB % 50.21/7.95 % (1559127)Instructions burned: 182 (million) % 50.21/7.95 % (1559129)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=1066159107:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi) % 50.21/7.95 % (1559122)Instruction limit reached! % 50.21/7.95 % (1559122)------------------------------ % 50.21/7.95 % (1559122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.21/7.95 % (1559122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.21/7.95 % (1559122)CaDiCaL version: 2.1.3 % 50.21/7.95 % (1559122)Termination reason: Instruction limit % 50.21/7.95 % (1559122)Termination phase: Saturation % 50.21/7.95 % (1559122)Time elapsed: 1.081 s % 50.21/7.95 % (1559122)Peak memory usage: 153 MB % 50.21/7.95 % (1559122)Instructions burned: 3256 (million) % 50.21/7.95 % (1559102)Instruction limit reached! % 50.21/7.95 % (1559102)------------------------------ % 50.21/7.95 % (1559102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.21/7.95 % (1559102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.21/7.95 % (1559102)CaDiCaL version: 2.1.3 % 50.21/7.95 % (1559102)Termination reason: Instruction limit % 50.21/7.95 % (1559102)Termination phase: Saturation % 50.21/7.95 % (1559102)Time elapsed: 2.106 s % 50.21/7.95 % (1559102)Peak memory usage: 150 MB % 50.21/7.95 % (1559102)Instructions burned: 3395 (million) % 50.21/7.95 % (1559131)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=1445617070:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi) % 68.75/10.46 % (1559131)Instruction limit reached! % 68.75/10.46 % (1559131)------------------------------ % 68.75/10.46 % (1559131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.75/10.46 % (1559131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.75/10.46 % (1559131)CaDiCaL version: 2.1.3 % 68.75/10.46 % (1559131)Termination reason: Instruction limit % 68.75/10.46 % (1559131)Termination phase: Saturation % 68.75/10.46 % (1559131)Time elapsed: 0.128 s % 68.75/10.46 % (1559131)Peak memory usage: 93 MB % 68.75/10.46 % (1559131)Instructions burned: 415 (million) % 68.75/10.46 % (1559132)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=2234265408:s2pl=no:i=8478:s2at=4:nm=6_2972 on theBenchmark for (2972ds/8478Mi) % 68.75/10.46 % (1559134)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=214928815:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi) % 68.75/10.46 % (1559134)Instruction limit reached! % 68.75/10.46 % (1559134)------------------------------ % 68.75/10.46 % (1559134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.75/10.46 % (1559134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.75/10.46 % (1559134)CaDiCaL version: 2.1.3 % 68.75/10.46 % (1559134)Termination reason: Instruction limit % 68.75/10.46 % (1559134)Termination phase: Saturation % 68.75/10.46 % (1559134)Time elapsed: 0.148 s % 68.75/10.46 % (1559134)Peak memory usage: 90 MB % 68.75/10.46 % (1559134)Instructions burned: 303 (million) % 68.75/10.46 % (1559137)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1954218530:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi) % 68.75/10.46 % (1559137)Instruction limit reached! % 68.75/10.46 % (1559137)------------------------------ % 68.75/10.46 % (1559137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.75/10.46 % (1559137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.75/10.46 % (1559137)CaDiCaL version: 2.1.3 % 68.75/10.46 % (1559137)Termination reason: Instruction limit % 68.75/10.46 % (1559137)Termination phase: Saturation % 68.75/10.46 % (1559137)Time elapsed: 0.427 s % 68.75/10.46 % (1559137)Peak memory usage: 94 MB % 68.75/10.46 % (1559137)Instructions burned: 721 (million) % 68.75/10.46 % (1559139)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2003360771:i=598:bs=on:bd=preordered:av=off:ss=axioms_2961 on theBenchmark for (2961ds/598Mi) % 68.75/10.46 % (1559110)Instruction limit reached! % 68.75/10.46 % (1559110)------------------------------ % 68.75/10.46 % (1559110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.75/10.46 % (1559110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.75/10.46 % (1559110)CaDiCaL version: 2.1.3 % 68.75/10.46 % (1559110)Termination reason: Instruction limit % 68.75/10.46 % (1559110)Termination phase: Saturation % 68.75/10.46 % (1559110)Time elapsed: 3.162 s % 68.75/10.46 % (1559110)Peak memory usage: 166 MB % 68.75/10.46 % (1559110)Instructions burned: 5209 (million) % 68.75/10.46 % (1559141)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4017454898:i=2989:sd=3:ss=axioms:sgt=60_2959 on theBenchmark for (2959ds/2989Mi) % 68.75/10.46 % (1559139)Instruction limit reached! % 68.75/10.46 % (1559139)------------------------------ % 68.75/10.46 % (1559139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.75/10.46 % (1559139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.75/10.46 % (1559139)CaDiCaL version: 2.1.3 % 68.75/10.46 % (1559139)Termination reason: Instruction limit % 68.75/10.46 % (1559139)Termination phase: Saturation % 68.75/10.46 % (1559139)Time elapsed: 0.377 s % 68.75/10.46 % (1559139)Peak memory usage: 95 MB % 68.75/10.46 % (1559139)Instructions burned: 598 (million) % 68.75/10.46 % (1559143)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=1345851625:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2956 on theBenchmark for (2956ds/1997Mi) % 68.75/10.46 % (1559143)Instruction limit reached! % 68.75/10.46 % (1559143)------------------------------ % 100.68/14.93 % (1559143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.68/14.93 % (1559143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.68/14.93 % (1559143)CaDiCaL version: 2.1.3 % 100.68/14.93 % (1559143)Termination reason: Instruction limit % 100.68/14.93 % (1559143)Termination phase: Saturation % 100.68/14.93 % (1559143)Time elapsed: 1.277 s % 100.68/14.93 % (1559143)Peak memory usage: 139 MB % 100.68/14.93 % (1559143)Instructions burned: 1997 (million) % 100.68/14.93 % (1559145)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=4126981613:i=2088:bd=preordered:av=off_2941 on theBenchmark for (2941ds/2088Mi) % 100.68/14.93 % (1559141)Instruction limit reached! % 100.68/14.93 % (1559141)------------------------------ % 100.68/14.93 % (1559141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.68/14.93 % (1559141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.68/14.93 % (1559141)CaDiCaL version: 2.1.3 % 100.68/14.93 % (1559141)Termination reason: Instruction limit % 100.68/14.93 % (1559141)Termination phase: Saturation % 100.68/14.93 % (1559141)Time elapsed: 1.776 s % 100.68/14.93 % (1559141)Peak memory usage: 146 MB % 100.68/14.93 % (1559141)Instructions burned: 2990 (million) % 100.68/14.93 % (1559129)Instruction limit reached! % 100.68/14.93 % (1559129)------------------------------ % 100.68/14.93 % (1559129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.68/14.93 % (1559129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.68/14.93 % (1559129)CaDiCaL version: 2.1.3 % 100.68/14.93 % (1559129)Termination reason: Instruction limit % 100.68/14.93 % (1559129)Termination phase: Saturation % 100.68/14.93 % (1559129)Time elapsed: 3.702 s % 100.68/14.93 % (1559129)Peak memory usage: 176 MB % 100.68/14.93 % (1559129)Instructions burned: 10308 (million) % 100.68/14.93 % (1559147)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2784803212:i=1098:nicw=on_2939 on theBenchmark for (2939ds/1098Mi) % 100.68/14.93 % (1559148)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=613154279:i=433:bd=preordered_2938 on theBenchmark for (2938ds/433Mi) % 100.68/14.93 % (1559148)Instruction limit reached! % 100.68/14.93 % (1559148)------------------------------ % 100.68/14.93 % (1559148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.68/14.93 % (1559148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.68/14.93 % (1559148)CaDiCaL version: 2.1.3 % 100.68/14.93 % (1559148)Termination reason: Instruction limit % 100.68/14.93 % (1559148)Termination phase: Saturation % 100.68/14.93 % (1559148)Time elapsed: 0.139 s % 100.68/14.93 % (1559148)Peak memory usage: 93 MB % 100.68/14.93 % (1559148)Instructions burned: 436 (million) % 100.68/14.93 % (1559151)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=564536488:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2936 on theBenchmark for (2936ds/2942Mi) % 100.68/14.93 % (1559147)Instruction limit reached! % 100.68/14.93 % (1559147)------------------------------ % 100.68/14.93 % (1559147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.68/14.93 % (1559147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.68/14.93 % (1559147)CaDiCaL version: 2.1.3 % 100.68/14.93 % (1559147)Termination reason: Instruction limit % 100.68/14.93 % (1559147)Termination phase: Saturation % 100.68/14.93 % (1559147)Time elapsed: 0.669 s % 100.68/14.93 % (1559147)Peak memory usage: 99 MB % 100.68/14.93 % (1559147)Instructions burned: 1099 (million) % 100.68/14.93 % (1559153)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3601127493:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2931 on theBenchmark for (2931ds/6922Mi) % 100.68/14.93 % (1559145)Instruction limit reached! % 100.68/14.93 % (1559145)------------------------------ % 100.68/14.93 % (1559145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.68/14.93 % (1559145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.68/14.93 % (1559145)CaDiCaL version: 2.1.3 % 100.68/14.93 % (1559145)Termination reason: Instruction limit % 100.68/14.93 % (1559145)Termination phase: Saturation % 100.68/14.93 % (1559145)Time elapsed: 1.288 s % 100.68/14.93 % (1559145)Peak memory usage: 141 MB % 100.68/14.93 % (1559145)Instructions burned: 2088 (million) % 117.20/17.23 % (1559155)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=972673701:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2927 on theBenchmark for (2927ds/596Mi) % 117.20/17.23 % (1559151)Instruction limit reached! % 117.20/17.23 % (1559151)------------------------------ % 117.20/17.23 % (1559151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.20/17.23 % (1559151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.20/17.23 % (1559151)CaDiCaL version: 2.1.3 % 117.20/17.23 % (1559151)Termination reason: Instruction limit % 117.20/17.23 % (1559151)Termination phase: Saturation % 117.20/17.23 % (1559151)Time elapsed: 1.005 s % 117.20/17.23 % (1559151)Peak memory usage: 144 MB % 117.20/17.23 % (1559151)Instructions burned: 2944 (million) % 117.20/17.23 % (1559157)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=3712734994:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2924 on theBenchmark for (2924ds/4123Mi) % 117.20/17.23 % (1559155)Instruction limit reached! % 117.20/17.23 % (1559155)------------------------------ % 117.20/17.23 % (1559155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.20/17.23 % (1559155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.20/17.23 % (1559155)CaDiCaL version: 2.1.3 % 117.20/17.23 % (1559155)Termination reason: Instruction limit % 117.20/17.23 % (1559155)Termination phase: Saturation % 117.20/17.23 % (1559155)Time elapsed: 0.354 s % 117.20/17.23 % (1559155)Peak memory usage: 96 MB % 117.20/17.23 % (1559155)Instructions burned: 597 (million) % 117.20/17.23 % (1559159)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1345060808:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2921 on theBenchmark for (2921ds/16411Mi) % 117.20/17.23 % (1559132)Instruction limit reached! % 117.20/17.23 % (1559132)------------------------------ % 117.20/17.23 % (1559132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.20/17.23 % (1559132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.20/17.23 % (1559132)CaDiCaL version: 2.1.3 % 117.20/17.23 % (1559132)Termination reason: Instruction limit % 117.20/17.23 % (1559132)Termination phase: Saturation % 117.20/17.23 % (1559132)Time elapsed: 5.214 s % 117.20/17.23 % (1559132)Peak memory usage: 197 MB % 117.20/17.23 % (1559132)Instructions burned: 8478 (million) % 117.20/17.23 % (1559161)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3538506875:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2918 on theBenchmark for (2918ds/1670Mi) % 117.20/17.23 % (1559157)Instruction limit reached! % 117.20/17.23 % (1559157)------------------------------ % 117.20/17.23 % (1559157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.20/17.23 % (1559157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.20/17.23 % (1559157)CaDiCaL version: 2.1.3 % 117.20/17.23 % (1559157)Termination reason: Instruction limit % 117.20/17.23 % (1559157)Termination phase: Saturation % 117.20/17.23 % (1559157)Time elapsed: 1.377 s % 117.20/17.23 % (1559157)Peak memory usage: 160 MB % 117.20/17.23 % (1559157)Instructions burned: 4124 (million) % 117.20/17.23 % (1559163)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=452328747:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2909 on theBenchmark for (2909ds/1722Mi) % 117.20/17.23 % (1559161)Instruction limit reached! % 117.20/17.23 % (1559161)------------------------------ % 117.20/17.23 % (1559161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.20/17.23 % (1559161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.20/17.23 % (1559161)CaDiCaL version: 2.1.3 % 117.20/17.23 % (1559161)Termination reason: Instruction limit % 117.20/17.23 % (1559161)Termination phase: Saturation % 117.20/17.23 % (1559161)Time elapsed: 1.007 s % 117.20/17.23 % (1559161)Peak memory usage: 138 MB % 117.20/17.23 % (1559161)Instructions burned: 1670 (million) % 117.20/17.23 % (1559165)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=4093781935:cts=off:cond=on:i=9530:bs=on:fsd=on_2906 on theBenchmark for (2906ds/9530Mi) % 117.20/17.23 % (1559163)Instruction limit reached! % 117.20/17.23 % (1559163)------------------------------ % 138.56/20.20 % (1559163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.56/20.20 % (1559163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.56/20.20 % (1559163)CaDiCaL version: 2.1.3 % 138.56/20.20 % (1559163)Termination reason: Instruction limit % 138.56/20.20 % (1559163)Termination phase: Saturation % 138.56/20.20 % (1559163)Time elapsed: 0.608 s % 138.56/20.20 % (1559163)Peak memory usage: 145 MB % 138.56/20.20 % (1559163)Instructions burned: 1725 (million) % 138.56/20.20 % (1559167)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=514153742:st=2:i=4495:sd=10:ss=included_2901 on theBenchmark for (2901ds/4495Mi) % 138.56/20.20 % (1559153)Instruction limit reached! % 138.56/20.20 % (1559153)------------------------------ % 138.56/20.20 % (1559153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.56/20.20 % (1559153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.56/20.20 % (1559153)CaDiCaL version: 2.1.3 % 138.56/20.20 % (1559153)Termination reason: Instruction limit % 138.56/20.20 % (1559153)Termination phase: Saturation % 138.56/20.20 % (1559153)Time elapsed: 4.062 s % 138.56/20.20 % (1559153)Peak memory usage: 184 MB % 138.56/20.20 % (1559153)Instructions burned: 6924 (million) % 138.56/20.20 % (1559169)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=3691007610:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2889 on theBenchmark for (2889ds/4920Mi) % 138.56/20.20 % (1559167)Instruction limit reached! % 138.56/20.20 % (1559167)------------------------------ % 138.56/20.20 % (1559167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.56/20.20 % (1559167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.56/20.20 % (1559167)CaDiCaL version: 2.1.3 % 138.56/20.20 % (1559167)Termination reason: Instruction limit % 138.56/20.20 % (1559167)Termination phase: Saturation % 138.56/20.20 % (1559167)Time elapsed: 1.485 s % 138.56/20.20 % (1559167)Peak memory usage: 158 MB % 138.56/20.20 % (1559167)Instructions burned: 4496 (million) % 138.56/20.20 % (1559171)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=1752909675:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2885 on theBenchmark for (2885ds/2083Mi) % 138.56/20.20 % (1559171)Instruction limit reached! % 138.56/20.20 % (1559171)------------------------------ % 138.56/20.20 % (1559171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.56/20.20 % (1559171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.56/20.20 % (1559171)CaDiCaL version: 2.1.3 % 138.56/20.20 % (1559171)Termination reason: Instruction limit % 138.56/20.20 % (1559171)Termination phase: Saturation % 138.56/20.20 % (1559171)Time elapsed: 0.712 s % 138.56/20.20 % (1559171)Peak memory usage: 139 MB % 138.56/20.20 % (1559171)Instructions burned: 2086 (million) % 138.56/20.20 % (1559173)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=1452078927:i=4629:av=off:gsp=on_2877 on theBenchmark for (2877ds/4629Mi) % 138.56/20.20 % (1559173)Instruction limit reached! % 138.56/20.20 % (1559173)------------------------------ % 138.56/20.20 % (1559173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.56/20.20 % (1559173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.56/20.20 % (1559173)CaDiCaL version: 2.1.3 % 138.56/20.20 % (1559173)Termination reason: Instruction limit % 138.56/20.20 % (1559173)Termination phase: Saturation % 138.56/20.20 % (1559173)Time elapsed: 1.407 s % 138.56/20.20 % (1559173)Peak memory usage: 145 MB % 138.56/20.20 % (1559173)Instructions burned: 4632 (million) % 138.56/20.20 % (1559175)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3183659437:i=1258:av=off_2861 on theBenchmark for (2861ds/1258Mi) % 138.56/20.20 % (1559169)Instruction limit reached! % 138.56/20.20 % (1559169)------------------------------ % 138.56/20.20 % (1559169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.56/20.20 % (1559169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.56/20.20 % (1559169)CaDiCaL version: 2.1.3 % 138.56/20.20 % (1559169)Termination reason: Instruction limit % 138.56/20.20 % (1559169)Termination phase: Saturation % 138.56/20.20 % (1559169)Time elapsed: 3.011 s % 138.56/20.20 % (1559169)Peak memory usage: 164 MB % 161.34/23.47 % (1559169)Instructions burned: 4922 (million) % 161.34/23.47 % (1559175)Instruction limit reached! % 161.34/23.47 % (1559175)------------------------------ % 161.34/23.47 % (1559175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.34/23.47 % (1559175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.34/23.47 % (1559175)CaDiCaL version: 2.1.3 % 161.34/23.47 % (1559175)Termination reason: Instruction limit % 161.34/23.47 % (1559175)Termination phase: Saturation % 161.34/23.47 % (1559175)Time elapsed: 0.401 s % 161.34/23.47 % (1559175)Peak memory usage: 99 MB % 161.34/23.47 % (1559175)Instructions burned: 1258 (million) % 161.34/23.47 % (1559177)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3961017855:i=7343:av=off:ss=included_2857 on theBenchmark for (2857ds/7343Mi) % 161.34/23.47 % (1559178)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2426321762:i=1325:sd=2:ss=axioms:sgt=16_2856 on theBenchmark for (2856ds/1325Mi) % 161.34/23.47 % (1559178)Instruction limit reached! % 161.34/23.47 % (1559178)------------------------------ % 161.34/23.47 % (1559178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.34/23.47 % (1559178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.34/23.47 % (1559178)CaDiCaL version: 2.1.3 % 161.34/23.47 % (1559178)Termination reason: Instruction limit % 161.34/23.47 % (1559178)Termination phase: Saturation % 161.34/23.47 % (1559178)Time elapsed: 0.405 s % 161.34/23.47 % (1559178)Peak memory usage: 97 MB % 161.34/23.47 % (1559178)Instructions burned: 1327 (million) % 161.34/23.47 % (1559181)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=68947864:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2851 on theBenchmark for (2851ds/2646Mi) % 161.34/23.47 % (1559165)Instruction limit reached! % 161.34/23.47 % (1559165)------------------------------ % 161.34/23.47 % (1559165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.34/23.47 % (1559165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.34/23.47 % (1559165)CaDiCaL version: 2.1.3 % 161.34/23.47 % (1559165)Termination reason: Instruction limit % 161.34/23.47 % (1559165)Termination phase: Saturation % 161.34/23.47 % (1559165)Time elapsed: 5.705 s % 161.34/23.47 % (1559165)Peak memory usage: 177 MB % 161.34/23.47 % (1559165)Instructions burned: 9531 (million) % 161.34/23.47 % (1559183)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1947336596:i=1489:sd=2:ep=R:ss=axioms_2847 on theBenchmark for (2847ds/1489Mi) % 161.34/23.47 % (1559181)Instruction limit reached! % 161.34/23.47 % (1559181)------------------------------ % 161.34/23.47 % (1559181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.34/23.47 % (1559181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.34/23.47 % (1559181)CaDiCaL version: 2.1.3 % 161.34/23.47 % (1559181)Termination reason: Instruction limit % 161.34/23.47 % (1559181)Termination phase: Saturation % 161.34/23.47 % (1559181)Time elapsed: 0.902 s % 161.34/23.47 % (1559181)Peak memory usage: 144 MB % 161.34/23.47 % (1559181)Instructions burned: 2649 (million) % 161.34/23.47 % (1559186)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=511989882:i=1503_2840 on theBenchmark for (2840ds/1503Mi) % 161.34/23.47 % (1559183)Instruction limit reached! % 161.34/23.47 % (1559183)------------------------------ % 161.34/23.47 % (1559183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.34/23.47 % (1559183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.34/23.47 % (1559183)CaDiCaL version: 2.1.3 % 161.34/23.47 % (1559183)Termination reason: Instruction limit % 161.34/23.47 % (1559183)Termination phase: Saturation % 161.34/23.47 % (1559183)Time elapsed: 0.961 s % 161.34/23.47 % (1559183)Peak memory usage: 133 MB % 161.34/23.47 % (1559183)Instructions burned: 1490 (million) % 161.34/23.47 % (1559188)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1008488501:i=13942:kws=frequency_2836 on theBenchmark for (2836ds/13942Mi) % 161.34/23.47 % (1559186)Instruction limit reached! % 161.34/23.47 % (1559186)------------------------------ % 161.34/23.47 % (1559186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.34/23.47 % (1559186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.34/23.47 % (1559186)CaDiCaL version: 2.1.3 % 188.31/27.20 % (1559186)Termination reason: Instruction limit % 188.31/27.20 % (1559186)Termination phase: Saturation % 188.31/27.20 % (1559186)Time elapsed: 0.518 s % 188.31/27.20 % (1559186)Peak memory usage: 143 MB % 188.31/27.20 % (1559186)Instructions burned: 1503 (million) % 188.31/27.20 % (1559190)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=2121296362:i=3604:fsr=off:er=filter_2834 on theBenchmark for (2834ds/3604Mi) % 188.31/27.20 % (1559190)Instruction limit reached! % 188.31/27.20 % (1559190)------------------------------ % 188.31/27.20 % (1559190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.31/27.20 % (1559190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.31/27.20 % (1559190)CaDiCaL version: 2.1.3 % 188.31/27.20 % (1559190)Termination reason: Instruction limit % 188.31/27.20 % (1559190)Termination phase: Saturation % 188.31/27.20 % (1559190)Time elapsed: 1.144 s % 188.31/27.20 % (1559190)Peak memory usage: 148 MB % 188.31/27.20 % (1559190)Instructions burned: 3607 (million) % 188.31/27.20 % (1559192)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2080004755:i=1876:sd=1:ss=included:sgt=32_2821 on theBenchmark for (2821ds/1876Mi) % 188.31/27.20 % (1559159)Instruction limit reached! % 188.31/27.20 % (1559159)------------------------------ % 188.31/27.20 % (1559159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.31/27.20 % (1559159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.31/27.20 % (1559159)CaDiCaL version: 2.1.3 % 188.31/27.20 % (1559159)Termination reason: Instruction limit % 188.31/27.20 % (1559159)Termination phase: Saturation % 188.31/27.20 % (1559159)Time elapsed: 10.226 s % 188.31/27.20 % (1559159)Peak memory usage: 186 MB % 188.31/27.20 % (1559159)Instructions burned: 16411 (million) % 188.31/27.20 % (1559194)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=180824392:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2817 on theBenchmark for (2817ds/1932Mi) % 188.31/27.20 % (1559192)Instruction limit reached! % 188.31/27.20 % (1559192)------------------------------ % 188.31/27.20 % (1559192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.31/27.20 % (1559192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.31/27.20 % (1559192)CaDiCaL version: 2.1.3 % 188.31/27.20 % (1559192)Termination reason: Instruction limit % 188.31/27.20 % (1559192)Termination phase: Saturation % 188.31/27.20 % (1559192)Time elapsed: 0.664 s % 188.31/27.20 % (1559192)Peak memory usage: 143 MB % 188.31/27.20 % (1559192)Instructions burned: 1877 (million) % 188.31/27.20 % (1559196)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=949699971:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2813 on theBenchmark for (2813ds/1980Mi) % 188.31/27.20 % (1559177)Instruction limit reached! % 188.31/27.20 % (1559177)------------------------------ % 188.31/27.20 % (1559177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.31/27.20 % (1559177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.31/27.20 % (1559177)CaDiCaL version: 2.1.3 % 188.31/27.20 % (1559177)Termination reason: Instruction limit % 188.31/27.20 % (1559177)Termination phase: Saturation % 188.31/27.20 % (1559177)Time elapsed: 4.499 s % 188.31/27.20 % (1559177)Peak memory usage: 184 MB % 188.31/27.20 % (1559177)Instructions burned: 7345 (million) % 188.31/27.20 % (1559198)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=2162209743:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2810 on theBenchmark for (2810ds/3902Mi) % 188.31/27.20 % (1559196)Instruction limit reached! % 188.31/27.20 % (1559196)------------------------------ % 188.31/27.20 % (1559196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.31/27.20 % (1559196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.31/27.20 % (1559196)CaDiCaL version: 2.1.3 % 188.31/27.20 % (1559196)Termination reason: Instruction limit % 188.31/27.20 % (1559196)Termination phase: Saturation % 188.31/27.20 % (1559196)Time elapsed: 0.667 s % 188.31/27.20 % (1559196)Peak memory usage: 144 MB % 188.31/27.20 % (1559196)Instructions burned: 1982 (million) % 188.31/27.20 % (1559194)Instruction limit reached! % 188.31/27.20 % (1559194)------------------------------ % 188.31/27.20 % (1559194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.25/29.54 % (1559194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.54 % (1559194)CaDiCaL version: 2.1.3 % 204.25/29.54 % (1559194)Termination reason: Instruction limit % 204.25/29.54 % (1559194)Termination phase: Saturation % 204.25/29.54 % (1559194)Time elapsed: 1.134 s % 204.25/29.54 % (1559194)Peak memory usage: 139 MB % 204.25/29.54 % (1559194)Instructions burned: 1934 (million) % 204.25/29.54 % (1559200)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2817453158:avsq=on:i=3916:aac=none:amm=off_2805 on theBenchmark for (2805ds/3916Mi) % 204.25/29.54 % (1559201)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=4276070526:cond=on:i=3940:av=off:er=known_2804 on theBenchmark for (2804ds/3940Mi) % 204.25/29.54 % (1559200)Instruction limit reached! % 204.25/29.54 % (1559200)------------------------------ % 204.25/29.54 % (1559200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.25/29.54 % (1559200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.54 % (1559200)CaDiCaL version: 2.1.3 % 204.25/29.54 % (1559200)Termination reason: Instruction limit % 204.25/29.54 % (1559200)Termination phase: Saturation % 204.25/29.54 % (1559200)Time elapsed: 1.333 s % 204.25/29.54 % (1559200)Peak memory usage: 132 MB % 204.25/29.54 % (1559200)Instructions burned: 3919 (million) % 204.25/29.54 % (1559204)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1599035871:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2790 on theBenchmark for (2790ds/3980Mi) % 204.25/29.54 % (1559198)Instruction limit reached! % 204.25/29.54 % (1559198)------------------------------ % 204.25/29.54 % (1559198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.25/29.54 % (1559198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.54 % (1559198)CaDiCaL version: 2.1.3 % 204.25/29.54 % (1559198)Termination reason: Instruction limit % 204.25/29.54 % (1559198)Termination phase: Saturation % 204.25/29.54 % (1559198)Time elapsed: 2.197 s % 204.25/29.54 % (1559198)Peak memory usage: 152 MB % 204.25/29.54 % (1559198)Instructions burned: 3903 (million) % 204.25/29.54 % (1559206)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=485972076:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2786 on theBenchmark for (2786ds/2087Mi) % 204.25/29.54 % (1559201)Instruction limit reached! % 204.25/29.54 % (1559201)------------------------------ % 204.25/29.54 % (1559201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.25/29.54 % (1559201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.54 % (1559201)CaDiCaL version: 2.1.3 % 204.25/29.54 % (1559201)Termination reason: Instruction limit % 204.25/29.54 % (1559201)Termination phase: Saturation % 204.25/29.54 % (1559201)Time elapsed: 2.130 s % 204.25/29.54 % (1559201)Peak memory usage: 159 MB % 204.25/29.54 % (1559201)Instructions burned: 3941 (million) % 204.25/29.54 % (1559208)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=2918098122:cts=off:cond=on:i=4272:bs=on:fsd=on_2781 on theBenchmark for (2781ds/4272Mi) % 204.25/29.54 % (1559204)Instruction limit reached! % 204.25/29.54 % (1559204)------------------------------ % 204.25/29.54 % (1559204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.25/29.54 % (1559204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 204.25/29.54 % (1559204)CaDiCaL version: 2.1.3 % 204.25/29.54 % (1559204)Termination reason: Instruction limit % 204.25/29.54 % (1559204)Termination phase: Saturation % 204.25/29.54 % (1559204)Time elapsed: 1.243 s % 204.25/29.54 % (1559204)Peak memory usage: 158 MB % 204.25/29.54 % (1559204)Instructions burned: 3981 (million) % 204.25/29.54 % (1559210)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=42045414:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2776 on theBenchmark for (2776ds/2197Mi) % 204.25/29.54 % (1559206)Instruction limit reached! % 204.25/29.54 % (1559206)------------------------------ % 204.25/29.54 % (1559206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 204.25/29.54 % (1559206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.39/40.11 % (1559206)CaDiCaL version: 2.1.3 % 279.39/40.11 % (1559206)Termination reason: Instruction limit % 279.39/40.11 % (1559206)Termination phase: Saturation % 279.39/40.11 % (1559206)Time elapsed: 1.335 s % 279.39/40.11 % (1559206)Peak memory usage: 143 MB % 279.39/40.11 % (1559206)Instructions burned: 2088 (million) % 279.39/40.11 % (1559212)dis+21_1_sil=8000:spb=goal_then_units:random_seed=4098972477:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2771 on theBenchmark for (2771ds/6508Mi) % 279.39/40.11 % (1559210)Instruction limit reached! % 279.39/40.11 % (1559210)------------------------------ % 279.39/40.11 % (1559210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.39/40.11 % (1559210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.39/40.11 % (1559210)CaDiCaL version: 2.1.3 % 279.39/40.11 % (1559210)Termination reason: Instruction limit % 279.39/40.11 % (1559210)Termination phase: Saturation % 279.39/40.11 % (1559210)Time elapsed: 0.712 s % 279.39/40.11 % (1559210)Peak memory usage: 142 MB % 279.39/40.11 % (1559210)Instructions burned: 2201 (million) % 279.39/40.11 % (1559214)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=2368809152:i=2330:fgj=on:av=off:fsr=off_2768 on theBenchmark for (2768ds/2330Mi) % 279.39/40.11 % (1559214)Instruction limit reached! % 279.39/40.11 % (1559214)------------------------------ % 279.39/40.11 % (1559214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.39/40.11 % (1559214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.39/40.11 % (1559214)CaDiCaL version: 2.1.3 % 279.39/40.11 % (1559214)Termination reason: Instruction limit % 279.39/40.11 % (1559214)Termination phase: Saturation % 279.39/40.11 % (1559214)Time elapsed: 0.773 s % 279.39/40.11 % (1559214)Peak memory usage: 143 MB % 279.39/40.11 % (1559214)Instructions burned: 2332 (million) % 279.39/40.11 % (1559216)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1746004907:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2759 on theBenchmark for (2759ds/7592Mi) % 279.39/40.11 % (1559208)Instruction limit reached! % 279.39/40.11 % (1559208)------------------------------ % 279.39/40.11 % (1559208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.39/40.11 % (1559208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.39/40.11 % (1559208)CaDiCaL version: 2.1.3 % 279.39/40.11 % (1559208)Termination reason: Instruction limit % 279.39/40.11 % (1559208)Termination phase: Saturation % 279.39/40.11 % (1559208)Time elapsed: 2.651 s % 279.39/40.11 % (1559208)Peak memory usage: 154 MB % 279.39/40.11 % (1559208)Instructions burned: 4274 (million) % 279.39/40.11 % (1559219)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=2540883943:i=2693:kws=precedence:ins=1:av=off_2753 on theBenchmark for (2753ds/2693Mi) % 279.39/40.11 % (1559188)Instruction limit reached! % 279.39/40.11 % (1559188)------------------------------ % 279.39/40.11 % (1559188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.39/40.11 % (1559188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.39/40.11 % (1559188)CaDiCaL version: 2.1.3 % 279.39/40.11 % (1559188)Termination reason: Instruction limit % 279.39/40.11 % (1559188)Termination phase: Saturation % 279.39/40.11 % (1559188)Time elapsed: 8.427 s % 279.39/40.11 % (1559188)Peak memory usage: 239 MB % 279.39/40.11 % (1559188)Instructions burned: 13943 (million) % 279.39/40.11 % (1559221)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2096592611:i=28651:sd=4:ss=included:sgt=64_2750 on theBenchmark for (2750ds/28651Mi) % 279.39/40.11 % (1559216)Instruction limit reached! % 279.39/40.11 % (1559216)------------------------------ % 279.39/40.11 % (1559216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.39/40.11 % (1559216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.39/40.11 % (1559216)CaDiCaL version: 2.1.3 % 279.39/40.11 % (1559216)Termination reason: Instruction limit % 279.39/40.11 % (1559216)Termination phase: Saturation % 279.39/40.11 % (1559216)Time elapsed: 2.315 s % 279.39/40.11 % (1559216)Peak memory usage: 133 MB % 279.39/40.11 % (1559216)Instructions burned: 7594 (million) % 279.39/40.11 % (1559219)Instruction limit reached! % 279.39/40.11 % (1559219)------------------------------ % 279.39/40.11 % (1559219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.39/40.11 % (1559219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559219)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559219)Termination reason: Instruction limit % 300.66/43.07 % (1559219)Termination phase: Saturation % 300.66/43.07 % (1559219)Time elapsed: 1.694 s % 300.66/43.07 % (1559219)Peak memory usage: 148 MB % 300.66/43.07 % (1559219)Instructions burned: 2693 (million) % 300.66/43.07 % (1559212)Instruction limit reached! % 300.66/43.07 % (1559212)------------------------------ % 300.66/43.07 % (1559212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559212)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559212)Termination reason: Instruction limit % 300.66/43.07 % (1559212)Termination phase: Saturation % 300.66/43.07 % (1559212)Time elapsed: 3.590 s % 300.66/43.07 % (1559212)Peak memory usage: 114 MB % 300.66/43.07 % (1559212)Instructions burned: 6508 (million) % 300.66/43.07 % (1559223)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1285994485:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2734 on theBenchmark for (2734ds/2700Mi) % 300.66/43.07 % (1559224)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=157756052:i=3196:nm=4_2734 on theBenchmark for (2734ds/3196Mi) % 300.66/43.07 % (1559225)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=3712936889:cts=off:i=3254:av=off_2734 on theBenchmark for (2734ds/3254Mi) % 300.66/43.07 % (1559223)Instruction limit reached! % 300.66/43.07 % (1559223)------------------------------ % 300.66/43.07 % (1559223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559223)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559223)Termination reason: Instruction limit % 300.66/43.07 % (1559223)Termination phase: Saturation % 300.66/43.07 % (1559223)Time elapsed: 0.939 s % 300.66/43.07 % (1559223)Peak memory usage: 146 MB % 300.66/43.07 % (1559223)Instructions burned: 2701 (million) % 300.66/43.07 % (1559229)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=4028838795:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2724 on theBenchmark for (2724ds/3264Mi) % 300.66/43.07 % (1559224)Instruction limit reached! % 300.66/43.07 % (1559224)------------------------------ % 300.66/43.07 % (1559224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559224)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559224)Termination reason: Instruction limit % 300.66/43.07 % (1559224)Termination phase: Saturation % 300.66/43.07 % (1559224)Time elapsed: 1.859 s % 300.66/43.07 % (1559224)Peak memory usage: 146 MB % 300.66/43.07 % (1559224)Instructions burned: 3197 (million) % 300.66/43.07 % (1559225)Instruction limit reached! % 300.66/43.07 % (1559225)------------------------------ % 300.66/43.07 % (1559225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559225)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559225)Termination reason: Instruction limit % 300.66/43.07 % (1559225)Termination phase: Saturation % 300.66/43.07 % (1559225)Time elapsed: 1.981 s % 300.66/43.07 % (1559225)Peak memory usage: 149 MB % 300.66/43.07 % (1559225)Instructions burned: 3255 (million) % 300.66/43.07 % (1559231)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=3054601193:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2714 on theBenchmark for (2714ds/9708Mi) % 300.66/43.07 % (1559229)Instruction limit reached! % 300.66/43.07 % (1559229)------------------------------ % 300.66/43.07 % (1559229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559229)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559229)Termination reason: Instruction limit % 300.66/43.07 % (1559229)Termination phase: Saturation % 300.66/43.07 % (1559229)Time elapsed: 1.166 s % 300.66/43.07 % (1559229)Peak memory usage: 148 MB % 300.66/43.07 % (1559229)Instructions burned: 3264 (million) % 300.66/43.07 % (1559232)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2350888094:i=21997:s2at=5:gtg=all_2712 on theBenchmark for (2712ds/21997Mi) % 300.66/43.07 % (1559234)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3416150230:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2711 on theBenchmark for (2711ds/7551Mi) % 300.66/43.07 % (1559234)Instruction limit reached! % 300.66/43.07 % (1559234)------------------------------ % 300.66/43.07 % (1559234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559234)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559234)Termination reason: Instruction limit % 300.66/43.07 % (1559234)Termination phase: Saturation % 300.66/43.07 % (1559234)Time elapsed: 2.197 s % 300.66/43.07 % (1559234)Peak memory usage: 124 MB % 300.66/43.07 % (1559234)Instructions burned: 7551 (million) % 300.66/43.07 % (1559389)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3895622524:i=8924:sd=1:ss=included_2688 on theBenchmark for (2688ds/8924Mi) % 300.66/43.07 % (1559389)Instruction limit reached! % 300.66/43.07 % (1559389)------------------------------ % 300.66/43.07 % (1559389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559389)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559389)Termination reason: Instruction limit % 300.66/43.07 % (1559389)Termination phase: Saturation % 300.66/43.07 % (1559389)Time elapsed: 2.703 s % 300.66/43.07 % (1559389)Peak memory usage: 202 MB % 300.66/43.07 % (1559389)Instructions burned: 8927 (million) % 300.66/43.07 % (1559391)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=2510621925:i=9638:kws=frequency:bd=preordered_2659 on theBenchmark for (2659ds/9638Mi) % 300.66/43.07 % (1559231)Instruction limit reached! % 300.66/43.07 % (1559231)------------------------------ % 300.66/43.07 % (1559231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559231)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559231)Termination reason: Instruction limit % 300.66/43.07 % (1559231)Termination phase: Saturation % 300.66/43.07 % (1559231)Time elapsed: 5.504 s % 300.66/43.07 % (1559231)Peak memory usage: 201 MB % 300.66/43.07 % (1559231)Instructions burned: 9708 (million) % 300.66/43.07 % (1559393)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:prc=on:drc=off:sp=const_min:sos=on:lcm=predicate:s2agt=20:br=off:flr=on:random_seed=2906023949:i=5177:s2at=1.5:bd=preordered:ins=10:fdi=128_2657 on theBenchmark for (2657ds/5177Mi) % 300.66/43.07 % (1559393)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 300.66/43.07 % (1559393)------------------------------ % 300.66/43.07 % (1559393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559393)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559393)Termination reason: Unknown % 300.66/43.07 % (1559393)Termination phase: Saturation % 300.66/43.07 % (1559393)Time elapsed: 0.783 s % 300.66/43.07 % (1559393)Peak memory usage: 134 MB % 300.66/43.07 % (1559393)Instructions burned: 1276 (million) % 300.66/43.07 % (1559395)lrs-1011_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:sas=cadical:sp=unary_first:acc=on:alpa=false:random_seed=2972941727:i=6464:aac=none:ins=10_2648 on theBenchmark for (2648ds/6464Mi) % 300.66/43.07 % (1559391)Instruction limit reached! % 300.66/43.07 % (1559391)------------------------------ % 300.66/43.07 % (1559391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.07 % (1559391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.07 % (1559391)CaDiCaL version: 2.1.3 % 300.66/43.07 % (1559391)Termination reason: Instruction limit % 300.66/43.07 % (1559391)Termination phase: Saturation % 300.66/43.07 % (1559391)Time elapsed: 3.219 s % 300.66/43.07 % (1559391)Peak memory usage: 202 MB % 300.66/43.07 % (1559391)Instructions burned: 9640 (million) % 300.66/43.07 % (1559397)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:erd=off:urr=on:bsr=on:fd=preordered:random_seed=1253365728:i=19192:av=off_2626 on theBenchmark for (2626ds/19192Mi) % 300.66/43.07 % (1559395)Instruction limit reached! % 300.66/43.07 % (1559395)------------------------------ % 300.66/43.07 % (1559395)Version: Vampire 5.0.1 (Relea % 300.66/43.08 Terminated %------------------------------------------------------------------------------