%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW402-1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n002.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:30:16 PM UTC 2026 % Result : Timeout 300.76s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW402-1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.19 % Computer : n002.cluster.edu % 0.09/0.19 % Model : x86_64 x86_64 % 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.19 % Memory : 8046.5625MB % 0.09/0.19 % OS : Linux 6.8.0-71-generic % 0.09/0.19 % CPULimit : 300 % 0.09/0.19 % WCLimit : 300 % 0.09/0.19 % DateTime : Mon Sep 28 13:52:37 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.22 Running first-order theorem proving % 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 11.32/2.29 % (359206)Input is clausal, will run a generic CNF schedule. % 11.32/2.29 % (359211)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=3925717760:i=140167_2999 on theBenchmark for (2999ds/140167Mi) % 11.32/2.29 % (359213)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4260869293:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi) % 11.32/2.29 % (359212)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1110972709:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi) % 11.32/2.29 % (359214)lrs+10_1_sil=8000:sp=occurrence:random_seed=3279865166:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi) % 11.32/2.29 % (359217)dis-21_1_sil=8000:lcm=predicate:random_seed=2252875034:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi) % 11.32/2.29 % (359216)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3270426633:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi) % 11.32/2.29 % (359215)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4235775198:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi) % 11.32/2.29 % (359217)Refutation not found, incomplete strategy % 11.32/2.29 % (359217)------------------------------ % 11.32/2.29 % (359217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.29 % (359217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.29 % (359217)CaDiCaL version: 2.1.3 % 11.32/2.29 % (359217)Termination reason: Refutation not found, incomplete strategy % 11.32/2.29 % (359217)Time elapsed: 0.004 s % 11.32/2.29 % (359217)Peak memory usage: 88 MB % 11.32/2.29 % (359217)Instructions burned: 5 (million) % 11.32/2.29 % (359214)Instruction limit reached! % 11.32/2.29 % (359214)------------------------------ % 11.32/2.29 % (359214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.29 % (359214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.29 % (359214)CaDiCaL version: 2.1.3 % 11.32/2.29 % (359214)Termination reason: Instruction limit % 11.32/2.29 % (359214)Termination phase: Saturation % 11.32/2.29 % (359214)Time elapsed: 0.064 s % 11.32/2.29 % (359214)Peak memory usage: 89 MB % 11.32/2.29 % (359214)Instructions burned: 109 (million) % 11.32/2.29 % (359215)Instruction limit reached! % 11.32/2.29 % (359215)------------------------------ % 11.32/2.29 % (359215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.29 % (359215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.29 % (359215)CaDiCaL version: 2.1.3 % 11.32/2.29 % (359215)Termination reason: Instruction limit % 11.32/2.29 % (359215)Termination phase: Saturation % 11.32/2.29 % (359215)Time elapsed: 0.072 s % 11.32/2.29 % (359215)Peak memory usage: 89 MB % 11.32/2.29 % (359215)Instructions burned: 115 (million) % 11.32/2.29 % (359216)Instruction limit reached! % 11.32/2.29 % (359216)------------------------------ % 11.32/2.29 % (359216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.29 % (359216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.29 % (359216)CaDiCaL version: 2.1.3 % 11.32/2.29 % (359216)Termination reason: Instruction limit % 11.32/2.29 % (359216)Termination phase: Saturation % 11.32/2.29 % (359216)Time elapsed: 0.097 s % 11.32/2.29 % (359216)Peak memory usage: 89 MB % 11.32/2.29 % (359216)Instructions burned: 181 (million) % 11.32/2.29 % (359225)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=1309883358:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi) % 11.32/2.29 % (359225)Refutation not found, incomplete strategy % 11.32/2.29 % (359225)------------------------------ % 11.32/2.29 % (359225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.29 % (359225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.29 % (359225)CaDiCaL version: 2.1.3 % 11.32/2.29 % (359225)Termination reason: Refutation not found, incomplete strategy % 11.32/2.29 % (359225)Time elapsed: 0.002 s % 11.32/2.29 % (359225)Peak memory usage: 88 MB % 11.32/2.29 % (359225)Instructions burned: 1 (million) % 11.32/2.29 % (359226)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2516971132: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.63/3.81 % (359227)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2647808653:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi) % 21.63/3.81 % (359227)Refutation not found, incomplete strategy % 21.63/3.81 % (359227)------------------------------ % 21.63/3.81 % (359227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.63/3.81 % (359227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.81 % (359227)CaDiCaL version: 2.1.3 % 21.63/3.81 % (359227)Termination reason: Refutation not found, incomplete strategy % 21.63/3.81 % (359227)Time elapsed: 0.002 s % 21.63/3.81 % (359227)Peak memory usage: 88 MB % 21.63/3.81 % (359227)Instructions burned: 1 (million) % 21.63/3.81 % (359217)------------------------------ % 21.63/3.81 % (359217)------------------------------ % 21.63/3.81 % (359226)Instruction limit reached! % 21.63/3.81 % (359226)------------------------------ % 21.63/3.81 % (359226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.63/3.81 % (359226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.81 % (359226)CaDiCaL version: 2.1.3 % 21.63/3.81 % (359226)Termination reason: Instruction limit % 21.63/3.81 % (359226)Termination phase: Saturation % 21.63/3.81 % (359226)Time elapsed: 0.111 s % 21.63/3.81 % (359226)Peak memory usage: 91 MB % 21.63/3.81 % (359226)Instructions burned: 190 (million) % 21.63/3.81 % (359231)lrs+10_64_to=lpo:sil=8000:random_seed=3013528515:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi) % 21.63/3.81 % (359225)------------------------------ % 21.63/3.81 % (359225)------------------------------ % 21.63/3.81 % (359232)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1937775847:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi) % 21.63/3.81 % (359227)------------------------------ % 21.63/3.81 % (359227)------------------------------ % 21.63/3.81 % (359231)Instruction limit reached! % 21.63/3.81 % (359231)------------------------------ % 21.63/3.81 % (359231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.63/3.81 % (359231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.81 % (359231)CaDiCaL version: 2.1.3 % 21.63/3.81 % (359231)Termination reason: Instruction limit % 21.63/3.81 % (359231)Termination phase: Saturation % 21.63/3.81 % (359231)Time elapsed: 0.073 s % 21.63/3.81 % (359231)Peak memory usage: 89 MB % 21.63/3.81 % (359231)Instructions burned: 127 (million) % 21.63/3.81 % (359234)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3226324553:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi) % 21.63/3.81 % (359232)Instruction limit reached! % 21.63/3.81 % (359232)------------------------------ % 21.63/3.81 % (359232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.63/3.81 % (359232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.81 % (359232)CaDiCaL version: 2.1.3 % 21.63/3.81 % (359232)Termination reason: Instruction limit % 21.63/3.81 % (359232)Termination phase: Saturation % 21.63/3.81 % (359232)Time elapsed: 0.120 s % 21.63/3.81 % (359232)Peak memory usage: 89 MB % 21.63/3.81 % (359232)Instructions burned: 196 (million) % 21.63/3.81 % (359236)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2678358269:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi) % 21.63/3.81 % (359237)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=923846444:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi) % 21.63/3.81 % (359237)Instruction limit reached! % 21.63/3.81 % (359237)------------------------------ % 21.63/3.81 % (359237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.63/3.81 % (359237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.63/3.81 % (359237)CaDiCaL version: 2.1.3 % 21.63/3.81 % (359237)Termination reason: Instruction limit % 21.63/3.81 % (359237)Termination phase: Saturation % 21.63/3.81 % (359237)Time elapsed: 0.061 s % 21.63/3.81 % (359237)Peak memory usage: 89 MB % 21.63/3.81 % (359237)Instructions burned: 107 (million) % 21.63/3.81 % (359234)Instruction limit reached! % 21.63/3.81 % (359234)------------------------------ % 21.63/3.81 % (359234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.63/3.81 % (359234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.56 % (359234)CaDiCaL version: 2.1.3 % 34.44/5.56 % (359234)Termination reason: Instruction limit % 34.44/5.56 % (359234)Termination phase: Saturation % 34.44/5.56 % (359234)Time elapsed: 0.100 s % 34.44/5.56 % (359234)Peak memory usage: 90 MB % 34.44/5.56 % (359234)Instructions burned: 159 (million) % 34.44/5.56 % (359239)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=999834948:i=107_2992 on theBenchmark for (2992ds/107Mi) % 34.44/5.56 % (359239)Refutation not found, incomplete strategy % 34.44/5.56 % (359239)------------------------------ % 34.44/5.56 % (359239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.56 % (359239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.56 % (359239)CaDiCaL version: 2.1.3 % 34.44/5.56 % (359239)Termination reason: Refutation not found, incomplete strategy % 34.44/5.56 % (359239)Time elapsed: 0.002 s % 34.44/5.56 % (359239)Peak memory usage: 88 MB % 34.44/5.56 % (359239)Instructions burned: 1 (million) % 34.44/5.56 % (359242)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3123458279:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi) % 34.44/5.56 % (359243)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4220839117:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi) % 34.44/5.56 % (359242)Instruction limit reached! % 34.44/5.56 % (359242)------------------------------ % 34.44/5.56 % (359242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.56 % (359242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.56 % (359242)CaDiCaL version: 2.1.3 % 34.44/5.56 % (359242)Termination reason: Instruction limit % 34.44/5.56 % (359242)Termination phase: Saturation % 34.44/5.56 % (359242)Time elapsed: 0.147 s % 34.44/5.56 % (359242)Peak memory usage: 90 MB % 34.44/5.56 % (359242)Instructions burned: 242 (million) % 34.44/5.56 % (359239)------------------------------ % 34.44/5.56 % (359239)------------------------------ % 34.44/5.56 % (359247)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1881093896:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi) % 34.44/5.56 % (359248)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3191612989:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi) % 34.44/5.56 % (359247)Instruction limit reached! % 34.44/5.56 % (359247)------------------------------ % 34.44/5.56 % (359247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.56 % (359247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.56 % (359247)CaDiCaL version: 2.1.3 % 34.44/5.56 % (359247)Termination reason: Instruction limit % 34.44/5.56 % (359247)Termination phase: Saturation % 34.44/5.56 % (359247)Time elapsed: 0.076 s % 34.44/5.56 % (359247)Peak memory usage: 89 MB % 34.44/5.56 % (359247)Instructions burned: 134 (million) % 34.44/5.56 % (359251)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1014114055:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi) % 34.44/5.56 % (359248)Instruction limit reached! % 34.44/5.56 % (359248)------------------------------ % 34.44/5.56 % (359248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.56 % (359248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.56 % (359248)CaDiCaL version: 2.1.3 % 34.44/5.56 % (359248)Termination reason: Instruction limit % 34.44/5.56 % (359248)Termination phase: Saturation % 34.44/5.56 % (359248)Time elapsed: 0.283 s % 34.44/5.56 % (359248)Peak memory usage: 94 MB % 34.44/5.56 % (359248)Instructions burned: 499 (million) % 34.44/5.56 % (359251)Instruction limit reached! % 34.44/5.56 % (359251)------------------------------ % 34.44/5.56 % (359251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.44/5.56 % (359251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.44/5.56 % (359251)CaDiCaL version: 2.1.3 % 34.44/5.56 % (359251)Termination reason: Instruction limit % 34.44/5.56 % (359251)Termination phase: Saturation % 34.44/5.56 % (359251)Time elapsed: 0.122 s % 34.44/5.56 % (359251)Peak memory usage: 91 MB % 34.44/5.56 % (359251)Instructions burned: 192 (million) % 34.44/5.56 % (359253)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=298749491:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi) % 55.58/8.57 % (359254)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1347719124:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi) % 55.58/8.57 % (359254)Instruction limit reached! % 55.58/8.57 % (359254)------------------------------ % 55.58/8.57 % (359254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.58/8.57 % (359254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.58/8.57 % (359254)CaDiCaL version: 2.1.3 % 55.58/8.57 % (359254)Termination reason: Instruction limit % 55.58/8.57 % (359254)Termination phase: Saturation % 55.58/8.57 % (359254)Time elapsed: 0.091 s % 55.58/8.57 % (359254)Peak memory usage: 89 MB % 55.58/8.57 % (359254)Instructions burned: 156 (million) % 55.58/8.57 % (359253)Instruction limit reached! % 55.58/8.57 % (359253)------------------------------ % 55.58/8.57 % (359253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.58/8.57 % (359253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.58/8.57 % (359253)CaDiCaL version: 2.1.3 % 55.58/8.57 % (359253)Termination reason: Instruction limit % 55.58/8.57 % (359253)Termination phase: Saturation % 55.58/8.57 % (359253)Time elapsed: 0.140 s % 55.58/8.57 % (359253)Peak memory usage: 90 MB % 55.58/8.57 % (359253)Instructions burned: 264 (million) % 55.58/8.57 % (359257)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=2613274767:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi) % 55.58/8.57 % (359258)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2221344547:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi) % 55.58/8.57 % (359258)Instruction limit reached! % 55.58/8.57 % (359258)------------------------------ % 55.58/8.57 % (359258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.58/8.57 % (359258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.58/8.57 % (359258)CaDiCaL version: 2.1.3 % 55.58/8.57 % (359258)Termination reason: Instruction limit % 55.58/8.57 % (359258)Termination phase: Saturation % 55.58/8.57 % (359258)Time elapsed: 0.305 s % 55.58/8.57 % (359258)Peak memory usage: 90 MB % 55.58/8.57 % (359258)Instructions burned: 537 (million) % 55.58/8.57 % (359261)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2349915546:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi) % 55.58/8.57 % (359261)Instruction limit reached! % 55.58/8.57 % (359261)------------------------------ % 55.58/8.57 % (359261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.58/8.57 % (359261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.58/8.57 % (359261)CaDiCaL version: 2.1.3 % 55.58/8.57 % (359261)Termination reason: Instruction limit % 55.58/8.57 % (359261)Termination phase: Saturation % 55.58/8.57 % (359261)Time elapsed: 0.102 s % 55.58/8.57 % (359261)Peak memory usage: 90 MB % 55.58/8.57 % (359261)Instructions burned: 181 (million) % 55.58/8.57 % (359263)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=3565331694:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi) % 55.58/8.57 % (359236)Instruction limit reached! % 55.58/8.57 % (359236)------------------------------ % 55.58/8.57 % (359236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.58/8.57 % (359236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.58/8.57 % (359236)CaDiCaL version: 2.1.3 % 55.58/8.57 % (359236)Termination reason: Instruction limit % 55.58/8.57 % (359236)Termination phase: Saturation % 55.58/8.57 % (359236)Time elapsed: 2.022 s % 55.58/8.57 % (359236)Peak memory usage: 147 MB % 55.58/8.57 % (359236)Instructions burned: 3395 (million) % 55.58/8.57 % (359265)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=2589359541:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi) % 55.58/8.57 % (359265)Instruction limit reached! % 55.58/8.57 % (359265)------------------------------ % 55.58/8.57 % (359265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.58/8.57 % (359265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.58/8.57 % (359265)CaDiCaL version: 2.1.3 % 78.20/11.73 % (359265)Termination reason: Instruction limit % 78.20/11.73 % (359265)Termination phase: Saturation % 78.20/11.73 % (359265)Time elapsed: 0.253 s % 78.20/11.73 % (359265)Peak memory usage: 93 MB % 78.20/11.73 % (359265)Instructions burned: 412 (million) % 78.20/11.73 % (359267)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=2691050784:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi) % 78.20/11.73 % (359257)Instruction limit reached! % 78.20/11.73 % (359257)------------------------------ % 78.20/11.73 % (359257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.20/11.73 % (359257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.20/11.73 % (359257)CaDiCaL version: 2.1.3 % 78.20/11.73 % (359257)Termination reason: Instruction limit % 78.20/11.73 % (359257)Termination phase: Saturation % 78.20/11.73 % (359257)Time elapsed: 1.991 s % 78.20/11.73 % (359257)Peak memory usage: 147 MB % 78.20/11.73 % (359257)Instructions burned: 3257 (million) % 78.20/11.73 % (359243)Instruction limit reached! % 78.20/11.73 % (359243)------------------------------ % 78.20/11.73 % (359243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.20/11.73 % (359243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.20/11.73 % (359243)CaDiCaL version: 2.1.3 % 78.20/11.73 % (359243)Termination reason: Instruction limit % 78.20/11.73 % (359243)Termination phase: Saturation % 78.20/11.73 % (359243)Time elapsed: 3.079 s % 78.20/11.73 % (359243)Peak memory usage: 157 MB % 78.20/11.73 % (359243)Instructions burned: 5209 (million) % 78.20/11.73 % (359269)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=3897974987: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) % 78.20/11.73 % (359269)Refutation not found, incomplete strategy % 78.20/11.73 % (359269)------------------------------ % 78.20/11.73 % (359269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.20/11.73 % (359269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.20/11.73 % (359269)CaDiCaL version: 2.1.3 % 78.20/11.73 % (359269)Termination reason: Refutation not found, incomplete strategy % 78.20/11.74 % (359269)Time elapsed: 0.016 s % 78.20/11.74 % (359269)Peak memory usage: 89 MB % 78.20/11.74 % (359269)Instructions burned: 26 (million) % 78.20/11.74 % (359270)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2091796765:st=4:i=720:sd=3:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/720Mi) % 78.20/11.74 % (359269)------------------------------ % 78.20/11.74 % (359269)------------------------------ % 78.20/11.74 % (359273)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=913778750:i=598:bs=on:bd=preordered:av=off:ss=axioms_2957 on theBenchmark for (2957ds/598Mi) % 78.20/11.74 % (359270)Instruction limit reached! % 78.20/11.74 % (359270)------------------------------ % 78.20/11.74 % (359270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.20/11.74 % (359270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.20/11.74 % (359270)CaDiCaL version: 2.1.3 % 78.20/11.74 % (359270)Termination reason: Instruction limit % 78.20/11.74 % (359270)Termination phase: Saturation % 78.20/11.74 % (359270)Time elapsed: 0.453 s % 78.20/11.74 % (359270)Peak memory usage: 97 MB % 78.20/11.74 % (359270)Instructions burned: 720 (million) % 78.20/11.74 % (359275)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=929128596:i=2989:sd=3:ss=axioms:sgt=60_2953 on theBenchmark for (2953ds/2989Mi) % 78.20/11.74 % (359273)Instruction limit reached! % 78.20/11.74 % (359273)------------------------------ % 78.20/11.74 % (359273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.20/11.74 % (359273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.20/11.74 % (359273)CaDiCaL version: 2.1.3 % 78.20/11.74 % (359273)Termination reason: Instruction limit % 78.20/11.74 % (359273)Termination phase: Saturation % 78.20/11.74 % (359273)Time elapsed: 0.347 s % 78.20/11.74 % (359273)Peak memory usage: 94 MB % 78.20/11.74 % (359273)Instructions burned: 599 (million) % 78.20/11.74 % (359277)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=3495408847:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2952 on theBenchmark for (2952ds/1997Mi) % 118.20/17.33 % (359277)Instruction limit reached! % 118.20/17.33 % (359277)------------------------------ % 118.20/17.33 % (359277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.20/17.33 % (359277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/17.33 % (359277)CaDiCaL version: 2.1.3 % 118.20/17.33 % (359277)Termination reason: Instruction limit % 118.20/17.33 % (359277)Termination phase: Saturation % 118.20/17.33 % (359277)Time elapsed: 1.155 s % 118.20/17.33 % (359277)Peak memory usage: 139 MB % 118.20/17.33 % (359277)Instructions burned: 1999 (million) % 118.20/17.33 % (359279)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=291091238:i=2088:bd=preordered:av=off_2939 on theBenchmark for (2939ds/2088Mi) % 118.20/17.33 % (359275)Instruction limit reached! % 118.20/17.33 % (359275)------------------------------ % 118.20/17.33 % (359275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.20/17.33 % (359275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/17.33 % (359275)CaDiCaL version: 2.1.3 % 118.20/17.33 % (359275)Termination reason: Instruction limit % 118.20/17.33 % (359275)Termination phase: Saturation % 118.20/17.33 % (359275)Time elapsed: 1.826 s % 118.20/17.33 % (359275)Peak memory usage: 144 MB % 118.20/17.33 % (359275)Instructions burned: 2989 (million) % 118.20/17.33 % (359281)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3689193189:i=1098:nicw=on_2934 on theBenchmark for (2934ds/1098Mi) % 118.20/17.33 % (359281)Instruction limit reached! % 118.20/17.33 % (359281)------------------------------ % 118.20/17.33 % (359281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.20/17.33 % (359281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/17.33 % (359281)CaDiCaL version: 2.1.3 % 118.20/17.33 % (359281)Termination reason: Instruction limit % 118.20/17.33 % (359281)Termination phase: Saturation % 118.20/17.33 % (359281)Time elapsed: 0.649 s % 118.20/17.33 % (359281)Peak memory usage: 108 MB % 118.20/17.33 % (359281)Instructions burned: 1099 (million) % 118.20/17.33 % (359283)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1513644069:i=433:bd=preordered_2926 on theBenchmark for (2926ds/433Mi) % 118.20/17.33 % (359283)Refutation not found, incomplete strategy % 118.20/17.33 % (359283)------------------------------ % 118.20/17.33 % (359283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.20/17.33 % (359283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/17.33 % (359283)CaDiCaL version: 2.1.3 % 118.20/17.33 % (359283)Termination reason: Refutation not found, incomplete strategy % 118.20/17.33 % (359283)Time elapsed: 0.003 s % 118.20/17.33 % (359283)Peak memory usage: 88 MB % 118.20/17.33 % (359283)Instructions burned: 3 (million) % 118.20/17.33 % (359279)Instruction limit reached! % 118.20/17.33 % (359279)------------------------------ % 118.20/17.33 % (359279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.20/17.33 % (359279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/17.33 % (359279)CaDiCaL version: 2.1.3 % 118.20/17.33 % (359279)Termination reason: Instruction limit % 118.20/17.33 % (359279)Termination phase: Saturation % 118.20/17.33 % (359279)Time elapsed: 1.308 s % 118.20/17.33 % (359279)Peak memory usage: 138 MB % 118.20/17.33 % (359279)Instructions burned: 2089 (million) % 118.20/17.33 % (359285)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1324074464:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2924 on theBenchmark for (2924ds/2942Mi) % 118.20/17.33 % (359283)------------------------------ % 118.20/17.33 % (359283)------------------------------ % 118.20/17.33 % (359287)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=34301727:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2922 on theBenchmark for (2922ds/6922Mi) % 118.20/17.33 % (359263)Instruction limit reached! % 118.20/17.33 % (359263)------------------------------ % 118.20/17.33 % (359263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.20/17.33 % (359263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.20/17.33 % (359263)CaDiCaL version: 2.1.3 % 118.20/17.33 % (359263)Termination reason: Instruction limit % 118.20/17.33 % (359263)Termination phase: Saturation % 137.57/20.07 % (359263)Time elapsed: 5.332 s % 137.57/20.07 % (359263)Peak memory usage: 150 MB % 137.57/20.07 % (359263)Instructions burned: 10308 (million) % 137.57/20.07 % (359289)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=2051169769:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2920 on theBenchmark for (2920ds/596Mi) % 137.57/20.07 % (359267)Instruction limit reached! % 137.57/20.07 % (359267)------------------------------ % 137.57/20.07 % (359267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.57/20.07 % (359267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/20.07 % (359267)CaDiCaL version: 2.1.3 % 137.57/20.07 % (359267)Termination reason: Instruction limit % 137.57/20.07 % (359267)Termination phase: Saturation % 137.57/20.07 % (359267)Time elapsed: 4.991 s % 137.57/20.07 % (359267)Peak memory usage: 179 MB % 137.57/20.07 % (359267)Instructions burned: 8478 (million) % 137.57/20.07 % (359289)Instruction limit reached! % 137.57/20.07 % (359289)------------------------------ % 137.57/20.07 % (359289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.57/20.07 % (359289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/20.07 % (359289)CaDiCaL version: 2.1.3 % 137.57/20.07 % (359289)Termination reason: Instruction limit % 137.57/20.07 % (359289)Termination phase: Saturation % 137.57/20.07 % (359289)Time elapsed: 0.309 s % 137.57/20.07 % (359289)Peak memory usage: 98 MB % 137.57/20.07 % (359289)Instructions burned: 598 (million) % 137.57/20.07 % (359291)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=112577263:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2917 on theBenchmark for (2917ds/4123Mi) % 137.57/20.07 % (359292)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2526969423:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2916 on theBenchmark for (2916ds/16411Mi) % 137.57/20.07 % (359285)Instruction limit reached! % 137.57/20.07 % (359285)------------------------------ % 137.57/20.07 % (359285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.57/20.07 % (359285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/20.07 % (359285)CaDiCaL version: 2.1.3 % 137.57/20.07 % (359285)Termination reason: Instruction limit % 137.57/20.07 % (359285)Termination phase: Saturation % 137.57/20.07 % (359285)Time elapsed: 1.948 s % 137.57/20.07 % (359285)Peak memory usage: 143 MB % 137.57/20.07 % (359285)Instructions burned: 2942 (million) % 137.57/20.07 % (359295)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=145094424:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2903 on theBenchmark for (2903ds/1670Mi) % 137.57/20.07 % (359295)Instruction limit reached! % 137.57/20.07 % (359295)------------------------------ % 137.57/20.07 % (359295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.57/20.07 % (359295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/20.07 % (359295)CaDiCaL version: 2.1.3 % 137.57/20.07 % (359295)Termination reason: Instruction limit % 137.57/20.07 % (359295)Termination phase: Saturation % 137.57/20.07 % (359295)Time elapsed: 1.054 s % 137.57/20.07 % (359295)Peak memory usage: 134 MB % 137.57/20.07 % (359295)Instructions burned: 1671 (million) % 137.57/20.07 % (359291)Instruction limit reached! % 137.57/20.07 % (359291)------------------------------ % 137.57/20.07 % (359291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.57/20.07 % (359291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.57/20.07 % (359291)CaDiCaL version: 2.1.3 % 137.57/20.07 % (359291)Termination reason: Instruction limit % 137.57/20.07 % (359291)Termination phase: Saturation % 137.57/20.07 % (359291)Time elapsed: 2.537 s % 137.57/20.07 % (359291)Peak memory usage: 157 MB % 137.57/20.07 % (359291)Instructions burned: 4125 (million) % 137.57/20.07 % (359297)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=1972987363:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2891 on theBenchmark for (2891ds/1722Mi) % 137.57/20.07 % (359298)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=891971431:cts=off:cond=on:i=9530:bs=on:fsd=on_2890 on theBenchmark for (2890ds/9530Mi) % 160.02/23.29 % (359287)Instruction limit reached! % 160.02/23.29 % (359287)------------------------------ % 160.02/23.29 % (359287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.02/23.29 % (359287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.02/23.29 % (359287)CaDiCaL version: 2.1.3 % 160.02/23.29 % (359287)Termination reason: Instruction limit % 160.02/23.29 % (359287)Termination phase: Saturation % 160.02/23.29 % (359287)Time elapsed: 3.883 s % 160.02/23.29 % (359287)Peak memory usage: 166 MB % 160.02/23.29 % (359287)Instructions burned: 6922 (million) % 160.02/23.29 % (359301)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=92220900:st=2:i=4495:sd=10:ss=included_2882 on theBenchmark for (2882ds/4495Mi) % 160.02/23.29 % (359297)Instruction limit reached! % 160.02/23.29 % (359297)------------------------------ % 160.02/23.29 % (359297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.02/23.29 % (359297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.02/23.29 % (359297)CaDiCaL version: 2.1.3 % 160.02/23.29 % (359297)Termination reason: Instruction limit % 160.02/23.29 % (359297)Termination phase: Saturation % 160.02/23.29 % (359297)Time elapsed: 1.087 s % 160.02/23.29 % (359297)Peak memory usage: 135 MB % 160.02/23.29 % (359297)Instructions burned: 1722 (million) % 160.02/23.29 % (359303)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=3018659958:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2879 on theBenchmark for (2879ds/4920Mi) % 160.02/23.29 % (359301)Instruction limit reached! % 160.02/23.29 % (359301)------------------------------ % 160.02/23.29 % (359301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.02/23.29 % (359301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.02/23.29 % (359301)CaDiCaL version: 2.1.3 % 160.02/23.29 % (359301)Termination reason: Instruction limit % 160.02/23.29 % (359301)Termination phase: Saturation % 160.02/23.29 % (359301)Time elapsed: 2.551 s % 160.02/23.29 % (359301)Peak memory usage: 149 MB % 160.02/23.29 % (359301)Instructions burned: 4496 (million) % 160.02/23.29 % (359305)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=1993269679:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2855 on theBenchmark for (2855ds/2083Mi) % 160.02/23.29 % (359303)Instruction limit reached! % 160.02/23.29 % (359303)------------------------------ % 160.02/23.29 % (359303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.02/23.29 % (359303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.02/23.29 % (359303)CaDiCaL version: 2.1.3 % 160.02/23.29 % (359303)Termination reason: Instruction limit % 160.02/23.29 % (359303)Termination phase: Saturation % 160.02/23.29 % (359303)Time elapsed: 3.022 s % 160.02/23.29 % (359303)Peak memory usage: 159 MB % 160.02/23.29 % (359303)Instructions burned: 4920 (million) % 160.02/23.29 % (359307)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=1522783025:i=4629:av=off:gsp=on_2847 on theBenchmark for (2847ds/4629Mi) % 160.02/23.29 % (359305)Instruction limit reached! % 160.02/23.29 % (359305)------------------------------ % 160.02/23.29 % (359305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.02/23.29 % (359305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.02/23.29 % (359305)CaDiCaL version: 2.1.3 % 160.02/23.29 % (359305)Termination reason: Instruction limit % 160.02/23.29 % (359305)Termination phase: Saturation % 160.02/23.29 % (359305)Time elapsed: 1.313 s % 160.02/23.29 % (359305)Peak memory usage: 135 MB % 160.02/23.29 % (359305)Instructions burned: 2084 (million) % 160.02/23.29 % (359309)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1702154419:i=1258:av=off_2841 on theBenchmark for (2841ds/1258Mi) % 160.02/23.29 % (359309)Instruction limit reached! % 160.02/23.29 % (359309)------------------------------ % 160.02/23.29 % (359309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.02/23.29 % (359309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.02/23.29 % (359309)CaDiCaL version: 2.1.3 % 160.02/23.29 % (359309)Termination reason: Instruction limit % 160.02/23.29 % (359309)Termination phase: Saturation % 160.02/23.29 % (359309)Time elapsed: 0.677 s % 160.02/23.29 % (359309)Peak memory usage: 96 MB % 160.02/23.29 % (359309)Instructions burned: 1259 (million) % 190.68/27.68 % (359311)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2352089043:i=7343:av=off:ss=included_2833 on theBenchmark for (2833ds/7343Mi) % 190.68/27.68 % (359298)Instruction limit reached! % 190.68/27.68 % (359298)------------------------------ % 190.68/27.68 % (359298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.68/27.68 % (359298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.68 % (359298)CaDiCaL version: 2.1.3 % 190.68/27.68 % (359298)Termination reason: Instruction limit % 190.68/27.68 % (359298)Termination phase: Saturation % 190.68/27.68 % (359298)Time elapsed: 5.747 s % 190.68/27.68 % (359298)Peak memory usage: 204 MB % 190.68/27.68 % (359298)Instructions burned: 9531 (million) % 190.68/27.68 % (359313)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2704492930:i=1325:sd=2:ss=axioms:sgt=16_2831 on theBenchmark for (2831ds/1325Mi) % 190.68/27.68 % (359313)Refutation not found, incomplete strategy % 190.68/27.68 % (359313)------------------------------ % 190.68/27.68 % (359313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.68/27.68 % (359313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.68 % (359313)CaDiCaL version: 2.1.3 % 190.68/27.68 % (359313)Termination reason: Refutation not found, incomplete strategy % 190.68/27.68 % (359313)Time elapsed: 0.002 s % 190.68/27.68 % (359313)Peak memory usage: 88 MB % 190.68/27.68 % (359313)Instructions burned: 1 (million) % 190.68/27.68 % (359313)------------------------------ % 190.68/27.68 % (359313)------------------------------ % 190.68/27.68 % (359315)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=2462787044:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2827 on theBenchmark for (2827ds/2646Mi) % 190.68/27.68 % (359307)Instruction limit reached! % 190.68/27.68 % (359307)------------------------------ % 190.68/27.68 % (359307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.68/27.68 % (359307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.68 % (359307)CaDiCaL version: 2.1.3 % 190.68/27.68 % (359307)Termination reason: Instruction limit % 190.68/27.68 % (359307)Termination phase: Saturation % 190.68/27.68 % (359307)Time elapsed: 2.830 s % 190.68/27.68 % (359307)Peak memory usage: 154 MB % 190.68/27.68 % (359307)Instructions burned: 4630 (million) % 190.68/27.68 % (359317)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3532849064:i=1489:sd=2:ep=R:ss=axioms_2817 on theBenchmark for (2817ds/1489Mi) % 190.68/27.68 % (359315)Instruction limit reached! % 190.68/27.68 % (359315)------------------------------ % 190.68/27.68 % (359315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.68/27.68 % (359315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.68 % (359315)CaDiCaL version: 2.1.3 % 190.68/27.68 % (359315)Termination reason: Instruction limit % 190.68/27.68 % (359315)Termination phase: Saturation % 190.68/27.68 % (359315)Time elapsed: 1.627 s % 190.68/27.68 % (359315)Peak memory usage: 143 MB % 190.68/27.68 % (359315)Instructions burned: 2647 (million) % 190.68/27.68 % (359319)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=2021255725:i=1503_2809 on theBenchmark for (2809ds/1503Mi) % 190.68/27.68 % (359317)Instruction limit reached! % 190.68/27.68 % (359317)------------------------------ % 190.68/27.68 % (359317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.68/27.68 % (359317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.68 % (359317)CaDiCaL version: 2.1.3 % 190.68/27.68 % (359317)Termination reason: Instruction limit % 190.68/27.68 % (359317)Termination phase: Saturation % 190.68/27.68 % (359317)Time elapsed: 1.004 s % 190.68/27.68 % (359317)Peak memory usage: 132 MB % 190.68/27.68 % (359317)Instructions burned: 1489 (million) % 190.68/27.68 % (359292)Instruction limit reached! % 190.68/27.68 % (359292)------------------------------ % 190.68/27.68 % (359292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.68/27.68 % (359292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.68/27.68 % (359292)CaDiCaL version: 2.1.3 % 190.68/27.68 % (359292)Termination reason: Instruction limit % 190.68/27.68 % (359292)Termination phase: Saturation % 190.68/27.68 % (359292)Time elapsed: 10.926 s % 190.68/27.68 % (359292)Peak memory usage: 181 MB % 216.80/31.23 % (359292)Instructions burned: 16413 (million) % 216.80/31.23 % (359321)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3509028663:i=13942:kws=frequency_2806 on theBenchmark for (2806ds/13942Mi) % 216.80/31.23 % (359322)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=649672581:i=3604:fsr=off:er=filter_2805 on theBenchmark for (2805ds/3604Mi) % 216.80/31.23 % (359319)Instruction limit reached! % 216.80/31.23 % (359319)------------------------------ % 216.80/31.23 % (359319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.80/31.23 % (359319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.80/31.23 % (359319)CaDiCaL version: 2.1.3 % 216.80/31.23 % (359319)Termination reason: Instruction limit % 216.80/31.23 % (359319)Termination phase: Saturation % 216.80/31.23 % (359319)Time elapsed: 0.934 s % 216.80/31.23 % (359319)Peak memory usage: 134 MB % 216.80/31.23 % (359319)Instructions burned: 1503 (million) % 216.80/31.23 % (359325)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=697927919:i=1876:sd=1:ss=included:sgt=32_2799 on theBenchmark for (2799ds/1876Mi) % 216.80/31.23 % (359311)Instruction limit reached! % 216.80/31.23 % (359311)------------------------------ % 216.80/31.23 % (359311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.80/31.23 % (359311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.80/31.23 % (359311)CaDiCaL version: 2.1.3 % 216.80/31.23 % (359311)Termination reason: Instruction limit % 216.80/31.23 % (359311)Termination phase: Saturation % 216.80/31.23 % (359311)Time elapsed: 4.257 s % 216.80/31.23 % (359311)Peak memory usage: 162 MB % 216.80/31.23 % (359311)Instructions burned: 7343 (million) % 216.80/31.23 % (359327)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=523233742:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2789 on theBenchmark for (2789ds/1932Mi) % 216.80/31.23 % (359325)Instruction limit reached! % 216.80/31.23 % (359325)------------------------------ % 216.80/31.23 % (359325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.80/31.23 % (359325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.80/31.23 % (359325)CaDiCaL version: 2.1.3 % 216.80/31.23 % (359325)Termination reason: Instruction limit % 216.80/31.23 % (359325)Termination phase: Saturation % 216.80/31.23 % (359325)Time elapsed: 1.157 s % 216.80/31.23 % (359325)Peak memory usage: 136 MB % 216.80/31.23 % (359325)Instructions burned: 1877 (million) % 216.80/31.23 % (359329)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=3962788148:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2786 on theBenchmark for (2786ds/1980Mi) % 216.80/31.23 % (359322)Instruction limit reached! % 216.80/31.23 % (359322)------------------------------ % 216.80/31.23 % (359322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.80/31.23 % (359322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.80/31.23 % (359322)CaDiCaL version: 2.1.3 % 216.80/31.23 % (359322)Termination reason: Instruction limit % 216.80/31.23 % (359322)Termination phase: Saturation % 216.80/31.23 % (359322)Time elapsed: 2.215 s % 216.80/31.23 % (359322)Peak memory usage: 151 MB % 216.80/31.23 % (359322)Instructions burned: 3606 (million) % 216.80/31.23 % (359331)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=1472575137:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2782 on theBenchmark for (2782ds/3902Mi) % 216.80/31.23 % (359327)Instruction limit reached! % 216.80/31.23 % (359327)------------------------------ % 216.80/31.23 % (359327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.80/31.23 % (359327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.80/31.23 % (359327)CaDiCaL version: 2.1.3 % 216.80/31.23 % (359327)Termination reason: Instruction limit % 216.80/31.23 % (359327)Termination phase: Saturation % 216.80/31.23 % (359327)Time elapsed: 1.301 s % 216.80/31.23 % (359327)Peak memory usage: 136 MB % 216.80/31.23 % (359327)Instructions burned: 1932 (million) % 216.80/31.23 % (359333)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=840914504:avsq=on:i=3916:aac=none:amm=off_2774 on theBenchmark for (2774ds/3916Mi) % 239.88/34.58 % (359329)Instruction limit reached! % 239.88/34.58 % (359329)------------------------------ % 239.88/34.58 % (359329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.88/34.58 % (359329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.88/34.58 % (359329)CaDiCaL version: 2.1.3 % 239.88/34.58 % (359329)Termination reason: Instruction limit % 239.88/34.58 % (359329)Termination phase: Saturation % 239.88/34.58 % (359329)Time elapsed: 1.260 s % 239.88/34.58 % (359329)Peak memory usage: 137 MB % 239.88/34.58 % (359329)Instructions burned: 1980 (million) % 239.88/34.58 % (359335)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=641122990:cond=on:i=3940:av=off:er=known_2772 on theBenchmark for (2772ds/3940Mi) % 239.88/34.58 % (359331)Instruction limit reached! % 239.88/34.58 % (359331)------------------------------ % 239.88/34.58 % (359331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.88/34.58 % (359331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.88/34.58 % (359331)CaDiCaL version: 2.1.3 % 239.88/34.58 % (359331)Termination reason: Instruction limit % 239.88/34.58 % (359331)Termination phase: Saturation % 239.88/34.58 % (359331)Time elapsed: 2.545 s % 239.88/34.58 % (359331)Peak memory usage: 153 MB % 239.88/34.58 % (359331)Instructions burned: 3903 (million) % 239.88/34.58 % (359337)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2175762995:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2755 on theBenchmark for (2755ds/3980Mi) % 239.88/34.58 % (359333)Instruction limit reached! % 239.88/34.58 % (359333)------------------------------ % 239.88/34.58 % (359333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.88/34.58 % (359333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.88/34.58 % (359333)CaDiCaL version: 2.1.3 % 239.88/34.58 % (359333)Termination reason: Instruction limit % 239.88/34.58 % (359333)Termination phase: Saturation % 239.88/34.58 % (359333)Time elapsed: 2.214 s % 239.88/34.58 % (359333)Peak memory usage: 110 MB % 239.88/34.58 % (359333)Instructions burned: 3918 (million) % 239.88/34.58 % (359339)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=3589553964:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2751 on theBenchmark for (2751ds/2087Mi) % 239.88/34.58 % (359335)Instruction limit reached! % 239.88/34.58 % (359335)------------------------------ % 239.88/34.58 % (359335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.88/34.58 % (359335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.88/34.58 % (359335)CaDiCaL version: 2.1.3 % 239.88/34.58 % (359335)Termination reason: Instruction limit % 239.88/34.58 % (359335)Termination phase: Saturation % 239.88/34.58 % (359335)Time elapsed: 2.278 s % 239.88/34.58 % (359335)Peak memory usage: 153 MB % 239.88/34.58 % (359335)Instructions burned: 3940 (million) % 239.88/34.58 % (359341)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=3273254969:cts=off:cond=on:i=4272:bs=on:fsd=on_2747 on theBenchmark for (2747ds/4272Mi) % 239.88/34.58 % (359339)Instruction limit reached! % 239.88/34.58 % (359339)------------------------------ % 239.88/34.58 % (359339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.88/34.58 % (359339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.88/34.58 % (359339)CaDiCaL version: 2.1.3 % 239.88/34.58 % (359339)Termination reason: Instruction limit % 239.88/34.58 % (359339)Termination phase: Saturation % 239.88/34.58 % (359339)Time elapsed: 1.363 s % 239.88/34.58 % (359339)Peak memory usage: 138 MB % 239.88/34.58 % (359339)Instructions burned: 2090 (million) % 239.88/34.58 % (359343)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=142125819:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2736 on theBenchmark for (2736ds/2197Mi) % 239.88/34.58 % (359337)Instruction limit reached! % 239.88/34.58 % (359337)------------------------------ % 239.88/34.58 % (359337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.88/34.58 % (359337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.88/34.58 % (359337)CaDiCaL version: 2.1.3 % 239.88/34.58 % (35933Terminated %------------------------------------------------------------------------------