%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV700-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:18 PM UTC 2026 % Result : Timeout 300.34s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV700-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.21 % Computer : n008.cluster.edu % 0.09/0.21 % Model : x86_64 x86_64 % 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.21 % Memory : 8046.5625MB % 0.09/0.21 % OS : Linux 6.8.0-71-generic % 0.09/0.21 % CPULimit : 300 % 0.09/0.21 % WCLimit : 300 % 0.09/0.21 % DateTime : Mon Sep 28 12:19:39 UTC 2026 % 0.09/0.21 % CPUTime : % 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.25 Running first-order theorem proving % 0.09/0.25 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 % 10.64/2.26 % (2214455)Input is clausal, will run a generic CNF schedule. % 10.64/2.26 % (2214460)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=4156383736:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 10.64/2.26 % (2214464)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2890299678:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 10.64/2.26 % (2214461)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=955946406:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 10.64/2.26 % (2214462)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2845508808:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 10.64/2.26 % (2214463)lrs+10_1_sil=8000:sp=occurrence:random_seed=4262302919:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 10.64/2.26 % (2214465)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1986283799:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 10.64/2.26 % (2214466)dis-21_1_sil=8000:lcm=predicate:random_seed=1249239586:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 10.64/2.26 % (2214464)Instruction limit reached! % 10.64/2.26 % (2214464)------------------------------ % 10.64/2.26 % (2214464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.64/2.26 % (2214464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.64/2.26 % (2214464)CaDiCaL version: 2.1.3 % 10.64/2.26 % (2214464)Termination reason: Instruction limit % 10.64/2.26 % (2214464)Termination phase: Saturation % 10.64/2.26 % (2214464)Time elapsed: 0.069 s % 10.64/2.26 % (2214464)Peak memory usage: 90 MB % 10.64/2.26 % (2214464)Instructions burned: 115 (million) % 10.64/2.26 % (2214463)Instruction limit reached! % 10.64/2.26 % (2214463)------------------------------ % 10.64/2.26 % (2214463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.64/2.26 % (2214463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.64/2.26 % (2214463)CaDiCaL version: 2.1.3 % 10.64/2.26 % (2214463)Termination reason: Instruction limit % 10.64/2.26 % (2214463)Termination phase: Saturation % 10.64/2.26 % (2214463)Time elapsed: 0.065 s % 10.64/2.26 % (2214463)Peak memory usage: 90 MB % 10.64/2.26 % (2214463)Instructions burned: 108 (million) % 10.64/2.26 % (2214466)Instruction limit reached! % 10.64/2.26 % (2214466)------------------------------ % 10.64/2.26 % (2214466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.64/2.26 % (2214466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.64/2.26 % (2214466)CaDiCaL version: 2.1.3 % 10.64/2.26 % (2214466)Termination reason: Instruction limit % 10.64/2.26 % (2214466)Termination phase: Saturation % 10.64/2.26 % (2214466)Time elapsed: 0.060 s % 10.64/2.26 % (2214466)Peak memory usage: 90 MB % 10.64/2.26 % (2214466)Instructions burned: 118 (million) % 10.64/2.26 % (2214465)Instruction limit reached! % 10.64/2.26 % (2214465)------------------------------ % 10.64/2.26 % (2214465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.64/2.26 % (2214465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.64/2.26 % (2214465)CaDiCaL version: 2.1.3 % 10.64/2.26 % (2214465)Termination reason: Instruction limit % 10.64/2.26 % (2214465)Termination phase: Saturation % 10.64/2.26 % (2214465)Time elapsed: 0.104 s % 10.64/2.26 % (2214465)Peak memory usage: 90 MB % 10.64/2.26 % (2214465)Instructions burned: 181 (million) % 10.64/2.26 % (2214474)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=3833242351:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 10.64/2.26 % (2214474)Refutation not found, incomplete strategy % 10.64/2.26 % (2214474)------------------------------ % 10.64/2.26 % (2214474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.64/2.26 % (2214474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.64/2.26 % (2214474)CaDiCaL version: 2.1.3 % 10.64/2.26 % (2214474)Termination reason: Refutation not found, incomplete strategy % 10.64/2.26 % (2214474)Time elapsed: 0.011 s % 10.64/2.26 % (2214474)Peak memory usage: 89 MB % 10.64/2.26 % (2214474)Instructions burned: 16 (million) % 10.64/2.26 % (2214476)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1608508689:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 21.10/3.87 % (2214475)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=867152557: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.10/3.87 % (2214476)Refutation not found, incomplete strategy % 21.10/3.87 % (2214476)------------------------------ % 21.10/3.87 % (2214476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.87 % (2214476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.87 % (2214476)CaDiCaL version: 2.1.3 % 21.10/3.87 % (2214476)Termination reason: Refutation not found, incomplete strategy % 21.10/3.87 % (2214476)Time elapsed: 0.039 s % 21.10/3.87 % (2214476)Peak memory usage: 90 MB % 21.10/3.87 % (2214476)Instructions burned: 70 (million) % 21.10/3.87 % (2214477)lrs+10_64_to=lpo:sil=8000:random_seed=409424852:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi) % 21.10/3.87 % (2214475)Instruction limit reached! % 21.10/3.87 % (2214475)------------------------------ % 21.10/3.87 % (2214475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.87 % (2214475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.87 % (2214475)CaDiCaL version: 2.1.3 % 21.10/3.87 % (2214475)Termination reason: Instruction limit % 21.10/3.87 % (2214475)Termination phase: Saturation % 21.10/3.87 % (2214475)Time elapsed: 0.094 s % 21.10/3.87 % (2214475)Peak memory usage: 91 MB % 21.10/3.87 % (2214475)Instructions burned: 194 (million) % 21.10/3.87 % (2214477)Instruction limit reached! % 21.10/3.87 % (2214477)------------------------------ % 21.10/3.87 % (2214477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.87 % (2214477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.87 % (2214477)CaDiCaL version: 2.1.3 % 21.10/3.87 % (2214477)Termination reason: Instruction limit % 21.10/3.87 % (2214477)Termination phase: Saturation % 21.10/3.87 % (2214477)Time elapsed: 0.072 s % 21.10/3.87 % (2214477)Peak memory usage: 90 MB % 21.10/3.87 % (2214477)Instructions burned: 126 (million) % 21.10/3.87 % (2214482)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3535870398:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi) % 21.10/3.87 % (2214474)------------------------------ % 21.10/3.87 % (2214474)------------------------------ % 21.10/3.87 % (2214483)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2950438794:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 21.10/3.87 % (2214476)------------------------------ % 21.10/3.87 % (2214476)------------------------------ % 21.10/3.87 % (2214482)Instruction limit reached! % 21.10/3.87 % (2214482)------------------------------ % 21.10/3.87 % (2214482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.87 % (2214482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.87 % (2214482)CaDiCaL version: 2.1.3 % 21.10/3.87 % (2214482)Termination reason: Instruction limit % 21.10/3.87 % (2214482)Termination phase: Saturation % 21.10/3.87 % (2214482)Time elapsed: 0.118 s % 21.10/3.87 % (2214482)Peak memory usage: 91 MB % 21.10/3.87 % (2214482)Instructions burned: 196 (million) % 21.10/3.87 % (2214483)Instruction limit reached! % 21.10/3.87 % (2214483)------------------------------ % 21.10/3.87 % (2214483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.10/3.87 % (2214483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.10/3.87 % (2214483)CaDiCaL version: 2.1.3 % 21.10/3.87 % (2214483)Termination reason: Instruction limit % 21.10/3.87 % (2214483)Termination phase: Saturation % 21.10/3.87 % (2214483)Time elapsed: 0.084 s % 21.10/3.87 % (2214483)Peak memory usage: 91 MB % 21.10/3.87 % (2214483)Instructions burned: 158 (million) % 21.10/3.87 % (2214485)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3990543900:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi) % 21.10/3.87 % (2214487)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=768363502:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 21.10/3.87 % (2214487)Instruction limit reached! % 21.10/3.87 % (2214487)------------------------------ % 21.10/3.87 % (2214487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.45 % (2214487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.45 % (2214487)CaDiCaL version: 2.1.3 % 33.22/5.45 % (2214487)Termination reason: Instruction limit % 33.22/5.45 % (2214487)Termination phase: Saturation % 33.22/5.45 % (2214487)Time elapsed: 0.060 s % 33.22/5.45 % (2214487)Peak memory usage: 90 MB % 33.22/5.45 % (2214487)Instructions burned: 106 (million) % 33.22/5.45 % (2214488)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=858851987:i=107_2992 on theBenchmark for (2992ds/107Mi) % 33.22/5.45 % (2214489)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1880329799:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi) % 33.22/5.45 % (2214488)Refutation not found, incomplete strategy % 33.22/5.45 % (2214488)------------------------------ % 33.22/5.45 % (2214488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.45 % (2214488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.45 % (2214488)CaDiCaL version: 2.1.3 % 33.22/5.45 % (2214488)Termination reason: Refutation not found, incomplete strategy % 33.22/5.45 % (2214488)Time elapsed: 0.039 s % 33.22/5.45 % (2214488)Peak memory usage: 90 MB % 33.22/5.45 % (2214488)Instructions burned: 70 (million) % 33.22/5.45 % (2214493)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2001680140:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi) % 33.22/5.45 % (2214489)Instruction limit reached! % 33.22/5.45 % (2214489)------------------------------ % 33.22/5.45 % (2214489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.45 % (2214489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.45 % (2214489)CaDiCaL version: 2.1.3 % 33.22/5.45 % (2214489)Termination reason: Instruction limit % 33.22/5.45 % (2214489)Termination phase: Saturation % 33.22/5.45 % (2214489)Time elapsed: 0.128 s % 33.22/5.45 % (2214489)Peak memory usage: 90 MB % 33.22/5.45 % (2214489)Instructions burned: 242 (million) % 33.22/5.45 % (2214496)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2368443435:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi) % 33.22/5.45 % (2214488)------------------------------ % 33.22/5.45 % (2214488)------------------------------ % 33.22/5.45 % (2214496)Instruction limit reached! % 33.22/5.45 % (2214496)------------------------------ % 33.22/5.45 % (2214496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.45 % (2214496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.45 % (2214496)CaDiCaL version: 2.1.3 % 33.22/5.45 % (2214496)Termination reason: Instruction limit % 33.22/5.45 % (2214496)Termination phase: Saturation % 33.22/5.45 % (2214496)Time elapsed: 0.085 s % 33.22/5.45 % (2214496)Peak memory usage: 90 MB % 33.22/5.45 % (2214496)Instructions burned: 134 (million) % 33.22/5.45 % (2214498)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1785501568:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi) % 33.22/5.45 % (2214499)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1754490029:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi) % 33.22/5.45 % (2214499)Instruction limit reached! % 33.22/5.45 % (2214499)------------------------------ % 33.22/5.45 % (2214499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.45 % (2214499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.45 % (2214499)CaDiCaL version: 2.1.3 % 33.22/5.45 % (2214499)Termination reason: Instruction limit % 33.22/5.45 % (2214499)Termination phase: Saturation % 33.22/5.45 % (2214499)Time elapsed: 0.117 s % 33.22/5.45 % (2214499)Peak memory usage: 92 MB % 33.22/5.45 % (2214499)Instructions burned: 192 (million) % 33.22/5.45 % (2214498)Instruction limit reached! % 33.22/5.45 % (2214498)------------------------------ % 33.22/5.45 % (2214498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.22/5.45 % (2214498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.22/5.45 % (2214498)CaDiCaL version: 2.1.3 % 33.22/5.45 % (2214498)Termination reason: Instruction limit % 33.22/5.45 % (2214498)Termination phase: Saturation % 33.22/5.45 % (2214498)Time elapsed: 0.280 s % 33.22/5.45 % (2214498)Peak memory usage: 94 MB % 33.22/5.45 % (2214498)Instructions burned: 499 (million) % 60.25/9.26 % (2214502)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2332770962:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi) % 60.25/9.26 % (2214503)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3753075388:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi) % 60.25/9.26 % (2214502)Instruction limit reached! % 60.25/9.26 % (2214502)------------------------------ % 60.25/9.26 % (2214502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.25/9.26 % (2214502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.25/9.26 % (2214502)CaDiCaL version: 2.1.3 % 60.25/9.26 % (2214502)Termination reason: Instruction limit % 60.25/9.26 % (2214502)Termination phase: Saturation % 60.25/9.26 % (2214502)Time elapsed: 0.154 s % 60.25/9.26 % (2214502)Peak memory usage: 93 MB % 60.25/9.26 % (2214502)Instructions burned: 264 (million) % 60.25/9.26 % (2214503)Instruction limit reached! % 60.25/9.26 % (2214503)------------------------------ % 60.25/9.26 % (2214503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.25/9.26 % (2214503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.25/9.26 % (2214503)CaDiCaL version: 2.1.3 % 60.25/9.26 % (2214503)Termination reason: Instruction limit % 60.25/9.26 % (2214503)Termination phase: Saturation % 60.25/9.26 % (2214503)Time elapsed: 0.084 s % 60.25/9.26 % (2214503)Peak memory usage: 90 MB % 60.25/9.26 % (2214503)Instructions burned: 156 (million) % 60.25/9.26 % (2214506)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=152179132:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi) % 60.25/9.26 % (2214507)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4257735713:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi) % 60.25/9.26 % (2214507)Instruction limit reached! % 60.25/9.26 % (2214507)------------------------------ % 60.25/9.26 % (2214507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.25/9.26 % (2214507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.25/9.26 % (2214507)CaDiCaL version: 2.1.3 % 60.25/9.26 % (2214507)Termination reason: Instruction limit % 60.25/9.26 % (2214507)Termination phase: Saturation % 60.25/9.26 % (2214507)Time elapsed: 0.310 s % 60.25/9.26 % (2214507)Peak memory usage: 92 MB % 60.25/9.26 % (2214507)Instructions burned: 538 (million) % 60.25/9.26 % (2214510)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2340060255:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi) % 60.25/9.26 % (2214510)Instruction limit reached! % 60.25/9.26 % (2214510)------------------------------ % 60.25/9.26 % (2214510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.25/9.26 % (2214510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.25/9.26 % (2214510)CaDiCaL version: 2.1.3 % 60.25/9.26 % (2214510)Termination reason: Instruction limit % 60.25/9.26 % (2214510)Termination phase: Saturation % 60.25/9.26 % (2214510)Time elapsed: 0.101 s % 60.25/9.26 % (2214510)Peak memory usage: 91 MB % 60.25/9.26 % (2214510)Instructions burned: 180 (million) % 60.25/9.26 % (2214512)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=180931913:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi) % 60.25/9.26 % (2214485)Instruction limit reached! % 60.25/9.26 % (2214485)------------------------------ % 60.25/9.26 % (2214485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.25/9.26 % (2214485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.25/9.26 % (2214485)CaDiCaL version: 2.1.3 % 60.25/9.26 % (2214485)Termination reason: Instruction limit % 60.25/9.26 % (2214485)Termination phase: Saturation % 60.25/9.26 % (2214485)Time elapsed: 2.043 s % 60.25/9.26 % (2214485)Peak memory usage: 151 MB % 60.25/9.26 % (2214485)Instructions burned: 3395 (million) % 60.25/9.26 % (2214514)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=2800656743:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi) % 60.25/9.26 % (2214514)Instruction limit reached! % 60.25/9.26 % (2214514)------------------------------ % 60.25/9.26 % (2214514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.59/12.55 % (2214514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.59/12.55 % (2214514)CaDiCaL version: 2.1.3 % 83.59/12.55 % (2214514)Termination reason: Instruction limit % 83.59/12.55 % (2214514)Termination phase: Saturation % 83.59/12.55 % (2214514)Time elapsed: 0.223 s % 83.59/12.55 % (2214514)Peak memory usage: 93 MB % 83.59/12.55 % (2214514)Instructions burned: 412 (million) % 83.59/12.55 % (2214516)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=2412855643:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi) % 83.59/12.55 % (2214506)Instruction limit reached! % 83.59/12.55 % (2214506)------------------------------ % 83.59/12.55 % (2214506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.59/12.55 % (2214506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.59/12.55 % (2214506)CaDiCaL version: 2.1.3 % 83.59/12.55 % (2214506)Termination reason: Instruction limit % 83.59/12.55 % (2214506)Termination phase: Saturation % 83.59/12.55 % (2214506)Time elapsed: 1.974 s % 83.59/12.55 % (2214506)Peak memory usage: 151 MB % 83.59/12.55 % (2214506)Instructions burned: 3257 (million) % 83.59/12.55 % (2214518)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=1502221058:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2961 on theBenchmark for (2961ds/303Mi) % 83.59/12.55 % (2214493)Instruction limit reached! % 83.59/12.55 % (2214493)------------------------------ % 83.59/12.55 % (2214493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.59/12.55 % (2214493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.59/12.55 % (2214493)CaDiCaL version: 2.1.3 % 83.59/12.55 % (2214493)Termination reason: Instruction limit % 83.59/12.55 % (2214493)Termination phase: Saturation % 83.59/12.55 % (2214493)Time elapsed: 3.127 s % 83.59/12.55 % (2214493)Peak memory usage: 168 MB % 83.59/12.55 % (2214493)Instructions burned: 5208 (million) % 83.59/12.55 % (2214518)Instruction limit reached! % 83.59/12.55 % (2214518)------------------------------ % 83.59/12.55 % (2214518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.59/12.55 % (2214518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.59/12.55 % (2214518)CaDiCaL version: 2.1.3 % 83.59/12.55 % (2214518)Termination reason: Instruction limit % 83.59/12.55 % (2214518)Termination phase: Saturation % 83.59/12.55 % (2214518)Time elapsed: 0.173 s % 83.59/12.55 % (2214518)Peak memory usage: 91 MB % 83.59/12.55 % (2214518)Instructions burned: 305 (million) % 83.59/12.55 % (2214520)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3933898424:st=4:i=720:sd=3:fsr=off:ss=axioms_2958 on theBenchmark for (2958ds/720Mi) % 83.59/12.55 % (2214521)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=525228517:i=598:bs=on:bd=preordered:av=off:ss=axioms_2958 on theBenchmark for (2958ds/598Mi) % 83.59/12.55 % (2214520)Instruction limit reached! % 83.59/12.55 % (2214520)------------------------------ % 83.59/12.55 % (2214520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.59/12.55 % (2214520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.59/12.55 % (2214520)CaDiCaL version: 2.1.3 % 83.59/12.55 % (2214520)Termination reason: Instruction limit % 83.59/12.55 % (2214520)Termination phase: Saturation % 83.59/12.55 % (2214520)Time elapsed: 0.309 s % 83.59/12.55 % (2214520)Peak memory usage: 91 MB % 83.59/12.55 % (2214520)Instructions burned: 721 (million) % 83.59/12.55 % (2214521)Instruction limit reached! % 83.59/12.55 % (2214521)------------------------------ % 83.59/12.55 % (2214521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.59/12.55 % (2214521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.59/12.55 % (2214521)CaDiCaL version: 2.1.3 % 83.59/12.55 % (2214521)Termination reason: Instruction limit % 83.59/12.55 % (2214521)Termination phase: Saturation % 83.59/12.55 % (2214521)Time elapsed: 0.324 s % 83.59/12.55 % (2214521)Peak memory usage: 94 MB % 83.59/12.55 % (2214521)Instructions burned: 599 (million) % 83.59/12.55 % (2214524)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=718263231:i=2989:sd=3:ss=axioms:sgt=60_2953 on theBenchmark for (2953ds/2989Mi) % 83.59/12.55 % (2214525)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=242955314:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2953 on theBenchmark for (2953ds/1997Mi) % 121.13/17.96 % (2214525)Instruction limit reached! % 121.13/17.96 % (2214525)------------------------------ % 121.13/17.96 % (2214525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.13/17.96 % (2214525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.13/17.96 % (2214525)CaDiCaL version: 2.1.3 % 121.13/17.96 % (2214525)Termination reason: Instruction limit % 121.13/17.96 % (2214525)Termination phase: Saturation % 121.13/17.96 % (2214525)Time elapsed: 1.270 s % 121.13/17.96 % (2214525)Peak memory usage: 141 MB % 121.13/17.96 % (2214525)Instructions burned: 1997 (million) % 121.13/17.96 % (2214528)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=3831204232:i=2088:bd=preordered:av=off_2939 on theBenchmark for (2939ds/2088Mi) % 121.13/17.96 % (2214524)Instruction limit reached! % 121.13/17.96 % (2214524)------------------------------ % 121.13/17.96 % (2214524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.13/17.96 % (2214524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.13/17.96 % (2214524)CaDiCaL version: 2.1.3 % 121.13/17.96 % (2214524)Termination reason: Instruction limit % 121.13/17.96 % (2214524)Termination phase: Saturation % 121.13/17.96 % (2214524)Time elapsed: 1.782 s % 121.13/17.96 % (2214524)Peak memory usage: 145 MB % 121.13/17.96 % (2214524)Instructions burned: 2990 (million) % 121.13/17.96 % (2214530)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3116268612:i=1098:nicw=on_2934 on theBenchmark for (2934ds/1098Mi) % 121.13/17.96 % (2214530)Instruction limit reached! % 121.13/17.96 % (2214530)------------------------------ % 121.13/17.96 % (2214530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.13/17.96 % (2214530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.13/17.96 % (2214530)CaDiCaL version: 2.1.3 % 121.13/17.96 % (2214530)Termination reason: Instruction limit % 121.13/17.96 % (2214530)Termination phase: Saturation % 121.13/17.96 % (2214530)Time elapsed: 0.703 s % 121.13/17.96 % (2214530)Peak memory usage: 102 MB % 121.13/17.96 % (2214530)Instructions burned: 1100 (million) % 121.13/17.96 % (2214528)Instruction limit reached! % 121.13/17.96 % (2214528)------------------------------ % 121.13/17.96 % (2214528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.13/17.96 % (2214528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.13/17.96 % (2214528)CaDiCaL version: 2.1.3 % 121.13/17.96 % (2214528)Termination reason: Instruction limit % 121.13/17.96 % (2214528)Termination phase: Saturation % 121.13/17.96 % (2214528)Time elapsed: 1.276 s % 121.13/17.96 % (2214528)Peak memory usage: 144 MB % 121.13/17.96 % (2214528)Instructions burned: 2088 (million) % 121.13/17.96 % (2214532)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=16938269:i=433:bd=preordered_2926 on theBenchmark for (2926ds/433Mi) % 121.13/17.96 % (2214533)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3153833255:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2925 on theBenchmark for (2925ds/2942Mi) % 121.13/17.96 % (2214532)Refutation not found, incomplete strategy % 121.13/17.96 % (2214532)------------------------------ % 121.13/17.96 % (2214532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.13/17.96 % (2214532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.13/17.96 % (2214532)CaDiCaL version: 2.1.3 % 121.13/17.96 % (2214532)Termination reason: Refutation not found, incomplete strategy % 121.13/17.96 % (2214532)Time elapsed: 0.083 s % 121.13/17.96 % (2214532)Peak memory usage: 91 MB % 121.13/17.96 % (2214532)Instructions burned: 136 (million) % 121.13/17.96 % (2214532)------------------------------ % 121.13/17.96 % (2214532)------------------------------ % 121.13/17.96 % (2214536)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=362852364:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2921 on theBenchmark for (2921ds/6922Mi) % 121.13/17.96 % (2214516)Instruction limit reached! % 121.13/17.96 % (2214516)------------------------------ % 121.13/17.96 % (2214516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.13/17.96 % (2214516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.14/20.07 % (2214516)CaDiCaL version: 2.1.3 % 137.14/20.07 % (2214516)Termination reason: Instruction limit % 137.14/20.07 % (2214516)Termination phase: Saturation % 137.14/20.07 % (2214516)Time elapsed: 5.263 s % 137.14/20.07 % (2214516)Peak memory usage: 186 MB % 137.14/20.07 % (2214516)Instructions burned: 8478 (million) % 137.14/20.07 % (2214538)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=1920247349:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2914 on theBenchmark for (2914ds/596Mi) % 137.14/20.07 % (2214512)Instruction limit reached! % 137.14/20.07 % (2214512)------------------------------ % 137.14/20.07 % (2214512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.14/20.07 % (2214512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.14/20.07 % (2214512)CaDiCaL version: 2.1.3 % 137.14/20.07 % (2214512)Termination reason: Instruction limit % 137.14/20.07 % (2214512)Termination phase: Saturation % 137.14/20.07 % (2214512)Time elapsed: 6.417 s % 137.14/20.07 % (2214512)Peak memory usage: 204 MB % 137.14/20.07 % (2214512)Instructions burned: 10308 (million) % 137.14/20.07 % (2214538)Instruction limit reached! % 137.14/20.07 % (2214538)------------------------------ % 137.14/20.07 % (2214538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.14/20.07 % (2214538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.14/20.07 % (2214538)CaDiCaL version: 2.1.3 % 137.14/20.07 % (2214538)Termination reason: Instruction limit % 137.14/20.07 % (2214538)Termination phase: Saturation % 137.14/20.07 % (2214538)Time elapsed: 0.312 s % 137.14/20.07 % (2214538)Peak memory usage: 93 MB % 137.14/20.07 % (2214538)Instructions burned: 597 (million) % 137.14/20.07 % (2214540)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=124276375:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2909 on theBenchmark for (2909ds/4123Mi) % 137.14/20.07 % (2214541)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=715616274:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2909 on theBenchmark for (2909ds/16411Mi) % 137.14/20.07 % (2214533)Instruction limit reached! % 137.14/20.07 % (2214533)------------------------------ % 137.14/20.07 % (2214533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.14/20.07 % (2214533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.14/20.07 % (2214533)CaDiCaL version: 2.1.3 % 137.14/20.07 % (2214533)Termination reason: Instruction limit % 137.14/20.07 % (2214533)Termination phase: Saturation % 137.14/20.07 % (2214533)Time elapsed: 1.975 s % 137.14/20.07 % (2214533)Peak memory usage: 145 MB % 137.14/20.07 % (2214533)Instructions burned: 2942 (million) % 137.14/20.07 % (2214544)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2157674205:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2904 on theBenchmark for (2904ds/1670Mi) % 137.14/20.07 % (2214544)Instruction limit reached! % 137.14/20.07 % (2214544)------------------------------ % 137.14/20.07 % (2214544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.14/20.07 % (2214544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.14/20.07 % (2214544)CaDiCaL version: 2.1.3 % 137.14/20.07 % (2214544)Termination reason: Instruction limit % 137.14/20.07 % (2214544)Termination phase: Saturation % 137.14/20.07 % (2214544)Time elapsed: 1.027 s % 137.14/20.07 % (2214544)Peak memory usage: 145 MB % 137.14/20.07 % (2214544)Instructions burned: 1671 (million) % 137.14/20.07 % (2214546)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=546482198:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2892 on theBenchmark for (2892ds/1722Mi) % 137.14/20.07 % (2214540)Instruction limit reached! % 137.14/20.07 % (2214540)------------------------------ % 137.14/20.07 % (2214540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.14/20.07 % (2214540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.14/20.07 % (2214540)CaDiCaL version: 2.1.3 % 137.14/20.07 % (2214540)Termination reason: Instruction limit % 137.14/20.07 % (2214540)Termination phase: Saturation % 137.14/20.07 % (2214540)Time elapsed: 2.566 s % 137.14/20.07 % (2214540)Peak memory usage: 166 MB % 137.14/20.07 % (2214540)Instructions burned: 4124 (million) % 137.14/20.07 % (2214548)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=1003344142:cts=off:cond=on:i=9530:bs=on:fsd=on_2882 on theBenchmark for (2882ds/9530Mi) % 159.08/23.14 % (2214546)Instruction limit reached! % 159.08/23.14 % (2214546)------------------------------ % 159.08/23.14 % (2214546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.08/23.14 % (2214546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.08/23.14 % (2214546)CaDiCaL version: 2.1.3 % 159.08/23.14 % (2214546)Termination reason: Instruction limit % 159.08/23.14 % (2214546)Termination phase: Saturation % 159.08/23.14 % (2214546)Time elapsed: 1.078 s % 159.08/23.14 % (2214546)Peak memory usage: 155 MB % 159.08/23.14 % (2214546)Instructions burned: 1722 (million) % 159.08/23.14 % (2214536)Instruction limit reached! % 159.08/23.14 % (2214536)------------------------------ % 159.08/23.14 % (2214536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.08/23.14 % (2214536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.08/23.14 % (2214536)CaDiCaL version: 2.1.3 % 159.08/23.14 % (2214536)Termination reason: Instruction limit % 159.08/23.14 % (2214536)Termination phase: Saturation % 159.08/23.14 % (2214536)Time elapsed: 4.049 s % 159.08/23.14 % (2214536)Peak memory usage: 174 MB % 159.08/23.14 % (2214536)Instructions burned: 6922 (million) % 159.08/23.14 % (2214550)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=859344541:st=2:i=4495:sd=10:ss=included_2880 on theBenchmark for (2880ds/4495Mi) % 159.08/23.14 % (2214551)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=257287697:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2879 on theBenchmark for (2879ds/4920Mi) % 159.08/23.14 % (2214550)Instruction limit reached! % 159.08/23.14 % (2214550)------------------------------ % 159.08/23.14 % (2214550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.08/23.14 % (2214550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.08/23.14 % (2214550)CaDiCaL version: 2.1.3 % 159.08/23.14 % (2214550)Termination reason: Instruction limit % 159.08/23.14 % (2214550)Termination phase: Saturation % 159.08/23.14 % (2214550)Time elapsed: 2.859 s % 159.08/23.14 % (2214550)Peak memory usage: 155 MB % 159.08/23.14 % (2214550)Instructions burned: 4496 (million) % 159.08/23.14 % (2214554)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=760749169:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2850 on theBenchmark for (2850ds/2083Mi) % 159.08/23.14 % (2214551)Instruction limit reached! % 159.08/23.14 % (2214551)------------------------------ % 159.08/23.14 % (2214551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.08/23.14 % (2214551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.08/23.14 % (2214551)CaDiCaL version: 2.1.3 % 159.08/23.14 % (2214551)Termination reason: Instruction limit % 159.08/23.14 % (2214551)Termination phase: Saturation % 159.08/23.14 % (2214551)Time elapsed: 3.088 s % 159.08/23.14 % (2214551)Peak memory usage: 153 MB % 159.08/23.14 % (2214551)Instructions burned: 4921 (million) % 159.08/23.14 % (2214556)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=3084490333:i=4629:av=off:gsp=on_2847 on theBenchmark for (2847ds/4629Mi) % 159.08/23.14 % (2214554)Instruction limit reached! % 159.08/23.14 % (2214554)------------------------------ % 159.08/23.14 % (2214554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.08/23.14 % (2214554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.08/23.14 % (2214554)CaDiCaL version: 2.1.3 % 159.08/23.14 % (2214554)Termination reason: Instruction limit % 159.08/23.14 % (2214554)Termination phase: Saturation % 159.08/23.14 % (2214554)Time elapsed: 1.290 s % 159.08/23.14 % (2214554)Peak memory usage: 140 MB % 159.08/23.14 % (2214554)Instructions burned: 2083 (million) % 159.08/23.14 % (2214558)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=978383874:i=1258:av=off_2836 on theBenchmark for (2836ds/1258Mi) % 159.08/23.14 % (2214558)Instruction limit reached! % 159.08/23.14 % (2214558)------------------------------ % 159.08/23.14 % (2214558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.90/26.99 % (2214558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.90/26.99 % (2214558)CaDiCaL version: 2.1.3 % 184.90/26.99 % (2214558)Termination reason: Instruction limit % 184.90/26.99 % (2214558)Termination phase: Saturation % 184.90/26.99 % (2214558)Time elapsed: 0.762 s % 184.90/26.99 % (2214558)Peak memory usage: 100 MB % 184.90/26.99 % (2214558)Instructions burned: 1258 (million) % 184.90/26.99 % (2214560)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3755901683:i=7343:av=off:ss=included_2827 on theBenchmark for (2827ds/7343Mi) % 184.90/26.99 % (2214556)Instruction limit reached! % 184.90/26.99 % (2214556)------------------------------ % 184.90/26.99 % (2214556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.90/26.99 % (2214556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.90/26.99 % (2214556)CaDiCaL version: 2.1.3 % 184.90/26.99 % (2214556)Termination reason: Instruction limit % 184.90/26.99 % (2214556)Termination phase: Saturation % 184.90/26.99 % (2214556)Time elapsed: 2.405 s % 184.90/26.99 % (2214556)Peak memory usage: 148 MB % 184.90/26.99 % (2214556)Instructions burned: 4630 (million) % 184.90/26.99 % (2214548)Instruction limit reached! % 184.90/26.99 % (2214548)------------------------------ % 184.90/26.99 % (2214548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.90/26.99 % (2214548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.90/26.99 % (2214548)CaDiCaL version: 2.1.3 % 184.90/26.99 % (2214548)Termination reason: Instruction limit % 184.90/26.99 % (2214548)Termination phase: Saturation % 184.90/26.99 % (2214548)Time elapsed: 5.996 s % 184.90/26.99 % (2214548)Peak memory usage: 185 MB % 184.90/26.99 % (2214548)Instructions burned: 9531 (million) % 184.90/26.99 % (2214562)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2937944169:i=1325:sd=2:ss=axioms:sgt=16_2821 on theBenchmark for (2821ds/1325Mi) % 184.90/26.99 % (2214562)Refutation not found, incomplete strategy % 184.90/26.99 % (2214562)------------------------------ % 184.90/26.99 % (2214562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.90/26.99 % (2214562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.90/26.99 % (2214562)CaDiCaL version: 2.1.3 % 184.90/26.99 % (2214562)Termination reason: Refutation not found, incomplete strategy % 184.90/26.99 % (2214562)Time elapsed: 0.014 s % 184.90/26.99 % (2214562)Peak memory usage: 89 MB % 184.90/26.99 % (2214562)Instructions burned: 22 (million) % 184.90/26.99 % (2214563)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=2833500542:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2821 on theBenchmark for (2821ds/2646Mi) % 184.90/26.99 % (2214562)------------------------------ % 184.90/26.99 % (2214562)------------------------------ % 184.90/26.99 % (2214566)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2367908761:i=1489:sd=2:ep=R:ss=axioms_2817 on theBenchmark for (2817ds/1489Mi) % 184.90/26.99 % (2214541)Instruction limit reached! % 184.90/26.99 % (2214541)------------------------------ % 184.90/26.99 % (2214541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.90/26.99 % (2214541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.90/26.99 % (2214541)CaDiCaL version: 2.1.3 % 184.90/26.99 % (2214541)Termination reason: Instruction limit % 184.90/26.99 % (2214541)Termination phase: Saturation % 184.90/26.99 % (2214541)Time elapsed: 9.583 s % 184.90/26.99 % (2214541)Peak memory usage: 234 MB % 184.90/26.99 % (2214541)Instructions burned: 16413 (million) % 184.90/26.99 % (2214568)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=230528112:i=1503_2812 on theBenchmark for (2812ds/1503Mi) % 184.90/26.99 % (2214566)Instruction limit reached! % 184.90/26.99 % (2214566)------------------------------ % 184.90/26.99 % (2214566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.90/26.99 % (2214566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.90/26.99 % (2214566)CaDiCaL version: 2.1.3 % 184.90/26.99 % (2214566)Termination reason: Instruction limit % 184.90/26.99 % (2214566)Termination phase: Saturation % 184.90/26.99 % (2214566)Time elapsed: 0.911 s % 184.90/26.99 % (2214566)Peak memory usage: 136 MB % 184.90/26.99 % (2214566)Instructions burned: 1491 (million) % 184.90/26.99 % (2214570)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1975065168:i=13942:kws=frequency_2807 on theBenchmark for (2807ds/13942Mi) % 212.06/30.66 % (2214563)Instruction limit reached! % 212.06/30.66 % (2214563)------------------------------ % 212.06/30.66 % (2214563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.06/30.66 % (2214563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.06/30.66 % (2214563)CaDiCaL version: 2.1.3 % 212.06/30.66 % (2214563)Termination reason: Instruction limit % 212.06/30.66 % (2214563)Termination phase: Saturation % 212.06/30.66 % (2214563)Time elapsed: 1.685 s % 212.06/30.66 % (2214563)Peak memory usage: 144 MB % 212.06/30.66 % (2214563)Instructions burned: 2647 (million) % 212.06/30.66 % (2214568)Instruction limit reached! % 212.06/30.66 % (2214568)------------------------------ % 212.06/30.66 % (2214568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.06/30.66 % (2214568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.06/30.66 % (2214568)CaDiCaL version: 2.1.3 % 212.06/30.66 % (2214568)Termination reason: Instruction limit % 212.06/30.66 % (2214568)Termination phase: Saturation % 212.06/30.66 % (2214568)Time elapsed: 0.882 s % 212.06/30.66 % (2214568)Peak memory usage: 137 MB % 212.06/30.66 % (2214568)Instructions burned: 1505 (million) % 212.06/30.66 % (2214572)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=1871861767:i=3604:fsr=off:er=filter_2803 on theBenchmark for (2803ds/3604Mi) % 212.06/30.66 % (2214573)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=724126137:i=1876:sd=1:ss=included:sgt=32_2801 on theBenchmark for (2801ds/1876Mi) % 212.06/30.66 % (2214573)Instruction limit reached! % 212.06/30.66 % (2214573)------------------------------ % 212.06/30.66 % (2214573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.06/30.66 % (2214573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.06/30.66 % (2214573)CaDiCaL version: 2.1.3 % 212.06/30.66 % (2214573)Termination reason: Instruction limit % 212.06/30.66 % (2214573)Termination phase: Saturation % 212.06/30.66 % (2214573)Time elapsed: 1.168 s % 212.06/30.66 % (2214573)Peak memory usage: 145 MB % 212.06/30.66 % (2214573)Instructions burned: 1877 (million) % 212.06/30.66 % (2214576)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=275417567:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2788 on theBenchmark for (2788ds/1932Mi) % 212.06/30.66 % (2214560)Instruction limit reached! % 212.06/30.66 % (2214560)------------------------------ % 212.06/30.66 % (2214560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.06/30.66 % (2214560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.06/30.66 % (2214560)CaDiCaL version: 2.1.3 % 212.06/30.66 % (2214560)Termination reason: Instruction limit % 212.06/30.66 % (2214560)Termination phase: Saturation % 212.06/30.66 % (2214560)Time elapsed: 4.154 s % 212.06/30.66 % (2214560)Peak memory usage: 163 MB % 212.06/30.66 % (2214560)Instructions burned: 7344 (million) % 212.06/30.66 % (2214578)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=1894729295:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2784 on theBenchmark for (2784ds/1980Mi) % 212.06/30.66 % (2214572)Instruction limit reached! % 212.06/30.66 % (2214572)------------------------------ % 212.06/30.66 % (2214572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.06/30.66 % (2214572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.06/30.66 % (2214572)CaDiCaL version: 2.1.3 % 212.06/30.66 % (2214572)Termination reason: Instruction limit % 212.06/30.66 % (2214572)Termination phase: Saturation % 212.06/30.66 % (2214572)Time elapsed: 1.944 s % 212.06/30.66 % (2214572)Peak memory usage: 160 MB % 212.06/30.66 % (2214572)Instructions burned: 3605 (million) % 212.06/30.66 % (2214580)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=308049532:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2782 on theBenchmark for (2782ds/3902Mi) % 212.06/30.66 % (2214576)Instruction limit reached! % 212.06/30.66 % (2214576)------------------------------ % 212.06/30.66 % (2214576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.06/30.66 % (2214576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.33/34.92 % (2214576)CaDiCaL version: 2.1.3 % 242.33/34.92 % (2214576)Termination reason: Instruction limit % 242.33/34.92 % (2214576)Termination phase: Saturation % 242.33/34.92 % (2214576)Time elapsed: 1.204 s % 242.33/34.92 % (2214576)Peak memory usage: 141 MB % 242.33/34.92 % (2214576)Instructions burned: 1933 (million) % 242.33/34.92 % (2214582)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1076535421:avsq=on:i=3916:aac=none:amm=off_2775 on theBenchmark for (2775ds/3916Mi) % 242.33/34.92 % (2214578)Instruction limit reached! % 242.33/34.92 % (2214578)------------------------------ % 242.33/34.92 % (2214578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.33/34.92 % (2214578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.33/34.92 % (2214578)CaDiCaL version: 2.1.3 % 242.33/34.92 % (2214578)Termination reason: Instruction limit % 242.33/34.92 % (2214578)Termination phase: Saturation % 242.33/34.92 % (2214578)Time elapsed: 1.186 s % 242.33/34.92 % (2214578)Peak memory usage: 149 MB % 242.33/34.92 % (2214578)Instructions burned: 1981 (million) % 242.33/34.92 % (2214584)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3067175955:cond=on:i=3940:av=off:er=known_2770 on theBenchmark for (2770ds/3940Mi) % 242.33/34.92 % (2214580)Instruction limit reached! % 242.33/34.92 % (2214580)------------------------------ % 242.33/34.92 % (2214580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.33/34.92 % (2214580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.33/34.92 % (2214580)CaDiCaL version: 2.1.3 % 242.33/34.92 % (2214580)Termination reason: Instruction limit % 242.33/34.92 % (2214580)Termination phase: Saturation % 242.33/34.92 % (2214580)Time elapsed: 1.895 s % 242.33/34.92 % (2214580)Peak memory usage: 138 MB % 242.33/34.92 % (2214580)Instructions burned: 3903 (million) % 242.33/34.92 % (2214586)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1573010425:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2761 on theBenchmark for (2761ds/3980Mi) % 242.33/34.92 % (2214582)Instruction limit reached! % 242.33/34.92 % (2214582)------------------------------ % 242.33/34.92 % (2214582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.33/34.92 % (2214582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.33/34.92 % (2214582)CaDiCaL version: 2.1.3 % 242.33/34.92 % (2214582)Termination reason: Instruction limit % 242.33/34.92 % (2214582)Termination phase: Saturation % 242.33/34.92 % (2214582)Time elapsed: 2.128 s % 242.33/34.92 % (2214582)Peak memory usage: 111 MB % 242.33/34.92 % (2214582)Instructions burned: 3918 (million) % 242.33/34.92 % (2214588)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=2559519995:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2752 on theBenchmark for (2752ds/2087Mi) % 242.33/34.92 % (2214584)Instruction limit reached! % 242.33/34.92 % (2214584)------------------------------ % 242.33/34.92 % (2214584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.33/34.92 % (2214584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.33/34.92 % (2214584)CaDiCaL version: 2.1.3 % 242.33/34.92 % (2214584)Termination reason: Instruction limit % 242.33/34.92 % (2214584)Termination phase: Saturation % 242.33/34.92 % (2214584)Time elapsed: 2.253 s % 242.33/34.92 % (2214584)Peak memory usage: 151 MB % 242.33/34.92 % (2214584)Instructions burned: 3941 (million) % 242.33/34.92 % (2214590)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=1899999940:cts=off:cond=on:i=4272:bs=on:fsd=on_2746 on theBenchmark for (2746ds/4272Mi) % 242.33/34.92 % (2214588)Instruction limit reached! % 242.33/34.92 % (2214588)------------------------------ % 242.33/34.92 % (2214588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 242.33/34.92 % (2214588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 242.33/34.92 % (2214588)CaDiCaL version: 2.1.3 % 242.33/34.92 % (2214588)Termination reason: Instruction limit % 242.33/34.92 % (2214588)Termination phase: Saturation % 242.33/34.92 % (2214588)Time elapsed: 1.329 s % 242.33/34.92 % (2214588)Peak memory usage: 145 MB % 242.33/34.92 % (2214588)Instructions burned: 2088 (million) % 242.33/34.92 % (2214592)lrs-30_1Terminated %------------------------------------------------------------------------------