%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWB052+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 : 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:00:19 PM UTC 2026 % Result : Timeout 288.35s 41.56s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWB052+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.38 % Computer : n008.cluster.edu % 0.11/0.38 % Model : x86_64 x86_64 % 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.38 % Memory : 8046.5625MB % 0.11/0.38 % OS : Linux 6.8.0-71-generic % 0.11/0.38 % CPULimit : 300 % 0.11/0.38 % WCLimit : 300 % 0.11/0.38 % DateTime : Mon Sep 28 07:12:09 UTC 2026 % 0.11/0.38 % CPUTime : % 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.14/0.42 Running first-order theorem proving % 0.14/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.64/2.20 % (2071530)Detected formulas, will run a generic FOF schedule. % 9.64/2.20 % (2071535)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=3594277371:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 9.64/2.20 % (2071538)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=475589009:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 9.64/2.20 % (2071539)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2170653482:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 9.64/2.20 % (2071541)dis-21_1_sil=8000:lcm=predicate:random_seed=3055677864:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 9.64/2.20 % (2071536)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3247675531:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 9.64/2.20 % (2071537)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=457181510:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 9.64/2.20 % (2071538)Refutation not found, incomplete strategy % 9.64/2.20 % (2071538)------------------------------ % 9.64/2.20 % (2071538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.64/2.20 % (2071538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.64/2.20 % (2071538)CaDiCaL version: 2.1.3 % 9.64/2.20 % (2071538)Termination reason: Refutation not found, incomplete strategy % 9.64/2.20 % (2071538)Time elapsed: 0.002 s % 9.64/2.20 % (2071538)Peak memory usage: 88 MB % 9.64/2.20 % (2071538)Instructions burned: 2 (million) % 9.64/2.20 % (2071540)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3565976248:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 9.64/2.20 % (2071539)Instruction limit reached! % 9.64/2.20 % (2071539)------------------------------ % 9.64/2.20 % (2071539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.64/2.20 % (2071539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.64/2.20 % (2071539)CaDiCaL version: 2.1.3 % 9.64/2.20 % (2071539)Termination reason: Instruction limit % 9.64/2.20 % (2071539)Termination phase: Saturation % 9.64/2.20 % (2071539)Time elapsed: 0.068 s % 9.64/2.20 % (2071539)Peak memory usage: 88 MB % 9.64/2.20 % (2071539)Instructions burned: 121 (million) % 9.64/2.20 % (2071541)Instruction limit reached! % 9.64/2.20 % (2071541)------------------------------ % 9.64/2.20 % (2071541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.64/2.20 % (2071541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.64/2.20 % (2071541)CaDiCaL version: 2.1.3 % 9.64/2.20 % (2071541)Termination reason: Instruction limit % 9.64/2.20 % (2071541)Termination phase: Saturation % 9.64/2.20 % (2071541)Time elapsed: 0.068 s % 9.64/2.20 % (2071541)Peak memory usage: 91 MB % 9.64/2.20 % (2071541)Instructions burned: 130 (million) % 9.64/2.20 % (2071540)Instruction limit reached! % 9.64/2.20 % (2071540)------------------------------ % 9.64/2.20 % (2071540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.64/2.20 % (2071540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.64/2.20 % (2071540)CaDiCaL version: 2.1.3 % 9.64/2.20 % (2071540)Termination reason: Instruction limit % 9.64/2.20 % (2071540)Termination phase: Saturation % 9.64/2.20 % (2071540)Time elapsed: 0.081 s % 9.64/2.20 % (2071540)Peak memory usage: 91 MB % 9.64/2.20 % (2071540)Instructions burned: 140 (million) % 9.64/2.20 % (2071549)lrs+10_1_sil=8000:sp=occurrence:random_seed=927776687:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 9.64/2.20 % (2071550)lrs+10_1_sil=32000:urr=on:br=off:random_seed=891034921:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 9.64/2.20 % (2071550)Refutation not found, incomplete strategy % 9.64/2.20 % (2071550)------------------------------ % 9.64/2.20 % (2071550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.64/2.20 % (2071550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.64/2.20 % (2071550)CaDiCaL version: 2.1.3 % 9.64/2.20 % (2071550)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2071550)Time elapsed: 0.004 s % 16.29/3.17 % (2071550)Peak memory usage: 88 MB % 16.29/3.17 % (2071550)Instructions burned: 5 (million) % 16.29/3.17 % (2071549)Refutation not found, incomplete strategy % 16.29/3.17 % (2071549)------------------------------ % 16.29/3.17 % (2071549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2071549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2071549)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2071549)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2071549)Time elapsed: 0.016 s % 16.29/3.17 % (2071549)Peak memory usage: 89 MB % 16.29/3.17 % (2071549)Instructions burned: 24 (million) % 16.29/3.17 % (2071551)lrs+1011_1_sil=32000:sp=occurrence:random_seed=115428417:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 16.29/3.17 % (2071551)Refutation not found, incomplete strategy % 16.29/3.17 % (2071551)------------------------------ % 16.29/3.17 % (2071551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2071551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2071551)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2071551)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2071551)Time elapsed: 0.003 s % 16.29/3.17 % (2071551)Peak memory usage: 88 MB % 16.29/3.17 % (2071551)Instructions burned: 3 (million) % 16.29/3.17 % (2071538)------------------------------ % 16.29/3.17 % (2071538)------------------------------ % 16.29/3.17 % (2071555)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1016415404:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 16.29/3.17 % (2071550)------------------------------ % 16.29/3.17 % (2071550)------------------------------ % 16.29/3.17 % (2071549)------------------------------ % 16.29/3.17 % (2071549)------------------------------ % 16.29/3.17 % (2071551)------------------------------ % 16.29/3.17 % (2071551)------------------------------ % 16.29/3.17 % (2071555)Instruction limit reached! % 16.29/3.17 % (2071555)------------------------------ % 16.29/3.17 % (2071555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2071555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2071555)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2071555)Termination reason: Instruction limit % 16.29/3.17 % (2071555)Termination phase: Saturation % 16.29/3.17 % (2071555)Time elapsed: 0.134 s % 16.29/3.17 % (2071555)Peak memory usage: 92 MB % 16.29/3.17 % (2071555)Instructions burned: 248 (million) % 16.29/3.17 % (2071557)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3771029040:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 16.29/3.17 % (2071557)Refutation not found, incomplete strategy % 16.29/3.17 % (2071557)------------------------------ % 16.29/3.17 % (2071557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2071557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2071557)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2071557)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2071557)Time elapsed: 0.005 s % 16.29/3.17 % (2071557)Peak memory usage: 89 MB % 16.29/3.17 % (2071557)Instructions burned: 6 (million) % 16.29/3.17 % (2071536)Refutation not found, incomplete strategy % 16.29/3.17 % (2071536)------------------------------ % 16.29/3.17 % (2071536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2071536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2071536)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2071536)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2071536)Time elapsed: 0.618 s % 16.29/3.17 % (2071536)Peak memory usage: 128 MB % 16.29/3.17 % (2071536)Instructions burned: 918 (million) % 16.29/3.17 % (2071558)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=569041535:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 16.29/3.17 % (2071559)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=576850444:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 16.29/3.17 % (2071559)Refutation not found, incomplete strategy % 16.29/3.17 % (2071559)------------------------------ % 16.29/3.17 % (2071559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2071559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.85/4.26 % (2071559)CaDiCaL version: 2.1.3 % 23.85/4.26 % (2071559)Termination reason: Refutation not found, incomplete strategy % 23.85/4.26 % (2071559)Time elapsed: 0.003 s % 23.85/4.26 % (2071559)Peak memory usage: 89 MB % 23.85/4.26 % (2071559)Instructions burned: 2 (million) % 23.85/4.26 % (2071560)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3595615682:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 23.85/4.26 % (2071560)Instruction limit reached! % 23.85/4.26 % (2071560)------------------------------ % 23.85/4.26 % (2071560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.85/4.26 % (2071560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.85/4.26 % (2071560)CaDiCaL version: 2.1.3 % 23.85/4.26 % (2071560)Termination reason: Instruction limit % 23.85/4.26 % (2071560)Termination phase: Saturation % 23.85/4.26 % (2071560)Time elapsed: 0.065 s % 23.85/4.26 % (2071560)Peak memory usage: 90 MB % 23.85/4.26 % (2071560)Instructions burned: 128 (million) % 23.85/4.26 % (2071557)------------------------------ % 23.85/4.26 % (2071557)------------------------------ % 23.85/4.26 % (2071536)------------------------------ % 23.85/4.26 % (2071536)------------------------------ % 23.85/4.26 % (2071559)------------------------------ % 23.85/4.26 % (2071559)------------------------------ % 23.85/4.26 % (2071565)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2259901534:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi) % 23.85/4.26 % (2071565)Instruction limit reached! % 23.85/4.26 % (2071565)------------------------------ % 23.85/4.26 % (2071565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.85/4.26 % (2071565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.85/4.26 % (2071565)CaDiCaL version: 2.1.3 % 23.85/4.26 % (2071565)Termination reason: Instruction limit % 23.85/4.26 % (2071565)Termination phase: Saturation % 23.85/4.26 % (2071565)Time elapsed: 0.062 s % 23.85/4.26 % (2071565)Peak memory usage: 89 MB % 23.85/4.26 % (2071565)Instructions burned: 114 (million) % 23.85/4.26 % (2071566)lrs+10_1_sil=8000:sp=occurrence:random_seed=3849849683:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi) % 23.85/4.26 % (2071566)Refutation not found, incomplete strategy % 23.85/4.26 % (2071566)------------------------------ % 23.85/4.26 % (2071566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.85/4.26 % (2071566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.85/4.26 % (2071566)CaDiCaL version: 2.1.3 % 23.85/4.26 % (2071566)Termination reason: Refutation not found, incomplete strategy % 23.85/4.26 % (2071566)Time elapsed: 0.017 s % 23.85/4.26 % (2071566)Peak memory usage: 89 MB % 23.85/4.26 % (2071566)Instructions burned: 24 (million) % 23.85/4.26 % (2071567)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1824800471:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 23.85/4.26 % (2071568)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2048909343:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi) % 23.85/4.26 % (2071567)Refutation not found, incomplete strategy % 23.85/4.26 % (2071567)------------------------------ % 23.85/4.26 % (2071567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.85/4.26 % (2071567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.85/4.26 % (2071567)CaDiCaL version: 2.1.3 % 23.85/4.26 % (2071567)Termination reason: Refutation not found, incomplete strategy % 23.85/4.26 % (2071567)Time elapsed: 0.003 s % 23.85/4.26 % (2071567)Peak memory usage: 88 MB % 23.85/4.26 % (2071567)Instructions burned: 2 (million) % 23.85/4.26 % (2071571)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=433870524:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 23.85/4.26 % (2071571)Refutation not found, incomplete strategy % 23.85/4.26 % (2071571)------------------------------ % 23.85/4.26 % (2071571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.85/4.26 % (2071571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.85/4.26 % (2071571)CaDiCaL version: 2.1.3 % 23.85/4.26 % (2071571)Termination reason: Refutation not found, incomplete strategy % 23.85/4.26 % (2071571)Time elapsed: 0.004 s % 23.85/4.26 % (2071571)Peak memory usage: 89 MB % 23.85/4.26 % (2071571)Instructions burned: 3 (million) % 41.76/6.93 % (2071567)------------------------------ % 41.76/6.93 % (2071567)------------------------------ % 41.76/6.93 % (2071566)------------------------------ % 41.76/6.93 % (2071566)------------------------------ % 41.76/6.93 % (2071571)------------------------------ % 41.76/6.93 % (2071571)------------------------------ % 41.76/6.93 % (2071576)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2409528268:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi) % 41.76/6.93 % (2071575)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3334968742:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi) % 41.76/6.93 % (2071577)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=4108530833:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi) % 41.76/6.93 % (2071577)Refutation not found, incomplete strategy % 41.76/6.93 % (2071577)------------------------------ % 41.76/6.93 % (2071577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.76/6.93 % (2071577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.76/6.93 % (2071577)CaDiCaL version: 2.1.3 % 41.76/6.93 % (2071577)Termination reason: Refutation not found, incomplete strategy % 41.76/6.93 % (2071577)Time elapsed: 0.008 s % 41.76/6.93 % (2071577)Peak memory usage: 89 MB % 41.76/6.93 % (2071577)Instructions burned: 11 (million) % 41.76/6.93 % (2071575)Instruction limit reached! % 41.76/6.93 % (2071575)------------------------------ % 41.76/6.93 % (2071575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.76/6.93 % (2071575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.76/6.93 % (2071575)CaDiCaL version: 2.1.3 % 41.76/6.93 % (2071575)Termination reason: Instruction limit % 41.76/6.93 % (2071575)Termination phase: Saturation % 41.76/6.93 % (2071575)Time elapsed: 0.296 s % 41.76/6.93 % (2071575)Peak memory usage: 96 MB % 41.76/6.93 % (2071575)Instructions burned: 593 (million) % 41.76/6.93 % (2071577)------------------------------ % 41.76/6.93 % (2071577)------------------------------ % 41.76/6.93 % (2071581)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1005246113:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi) % 41.76/6.93 % (2071581)Instruction limit reached! % 41.76/6.93 % (2071581)------------------------------ % 41.76/6.93 % (2071581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.76/6.93 % (2071581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.76/6.93 % (2071581)CaDiCaL version: 2.1.3 % 41.76/6.93 % (2071581)Termination reason: Instruction limit % 41.76/6.93 % (2071581)Termination phase: Saturation % 41.76/6.93 % (2071581)Time elapsed: 0.071 s % 41.76/6.93 % (2071581)Peak memory usage: 91 MB % 41.76/6.93 % (2071581)Instructions burned: 137 (million) % 41.76/6.93 % (2071582)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=599093992:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi) % 41.76/6.93 % (2071582)Refutation not found, incomplete strategy % 41.76/6.93 % (2071582)------------------------------ % 41.76/6.93 % (2071582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.76/6.93 % (2071582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.76/6.93 % (2071582)CaDiCaL version: 2.1.3 % 41.76/6.93 % (2071582)Termination reason: Refutation not found, incomplete strategy % 41.76/6.93 % (2071582)Time elapsed: 0.003 s % 41.76/6.93 % (2071582)Peak memory usage: 88 MB % 41.76/6.93 % (2071582)Instructions burned: 2 (million) % 41.76/6.93 % (2071558)Instruction limit reached! % 41.76/6.93 % (2071558)------------------------------ % 41.76/6.93 % (2071558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.76/6.93 % (2071558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.76/6.93 % (2071558)CaDiCaL version: 2.1.3 % 41.76/6.93 % (2071558)Termination reason: Instruction limit % 41.76/6.93 % (2071558)Termination phase: Saturation % 41.76/6.93 % (2071558)Time elapsed: 1.450 s % 41.76/6.93 % (2071558)Peak memory usage: 146 MB % 41.76/6.93 % (2071558)Instructions burned: 2350 (million) % 41.76/6.93 % (2071584)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3983268400:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi) % 41.76/6.93 % (2071584)Refutation not found, incomplete strategy % 41.76/6.93 % (2071584)------------------------------ % 65.30/10.06 % (2071584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.30/10.06 % (2071584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.30/10.06 % (2071584)CaDiCaL version: 2.1.3 % 65.30/10.06 % (2071584)Termination reason: Refutation not found, incomplete strategy % 65.30/10.06 % (2071584)Time elapsed: 0.003 s % 65.30/10.06 % (2071584)Peak memory usage: 88 MB % 65.30/10.06 % (2071584)Instructions burned: 2 (million) % 65.30/10.06 % (2071582)------------------------------ % 65.30/10.06 % (2071582)------------------------------ % 65.30/10.06 % (2071586)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3353772841:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi) % 65.30/10.06 % (2071584)------------------------------ % 65.30/10.06 % (2071584)------------------------------ % 65.30/10.06 % (2071588)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=641187970:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi) % 65.30/10.06 % (2071588)Instruction limit reached! % 65.30/10.06 % (2071588)------------------------------ % 65.30/10.06 % (2071588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.30/10.06 % (2071588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.30/10.06 % (2071588)CaDiCaL version: 2.1.3 % 65.30/10.06 % (2071588)Termination reason: Instruction limit % 65.30/10.06 % (2071588)Termination phase: Saturation % 65.30/10.06 % (2071588)Time elapsed: 0.080 s % 65.30/10.06 % (2071588)Peak memory usage: 92 MB % 65.30/10.06 % (2071588)Instructions burned: 151 (million) % 65.30/10.06 % (2071590)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1634657317:i=14155:bd=all_2974 on theBenchmark for (2974ds/14155Mi) % 65.30/10.06 % (2071592)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=246614172:i=667:av=off:fsr=off_2973 on theBenchmark for (2973ds/667Mi) % 65.30/10.06 % (2071592)Instruction limit reached! % 65.30/10.06 % (2071592)------------------------------ % 65.30/10.06 % (2071592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.30/10.06 % (2071592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.30/10.06 % (2071592)CaDiCaL version: 2.1.3 % 65.30/10.06 % (2071592)Termination reason: Instruction limit % 65.30/10.06 % (2071592)Termination phase: Saturation % 65.30/10.06 % (2071592)Time elapsed: 0.282 s % 65.30/10.06 % (2071592)Peak memory usage: 91 MB % 65.30/10.06 % (2071592)Instructions burned: 670 (million) % 65.30/10.06 % (2071568)Instruction limit reached! % 65.30/10.06 % (2071568)------------------------------ % 65.30/10.06 % (2071568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.30/10.06 % (2071568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.30/10.06 % (2071568)CaDiCaL version: 2.1.3 % 65.30/10.06 % (2071568)Termination reason: Instruction limit % 65.30/10.06 % (2071568)Termination phase: Saturation % 65.30/10.06 % (2071568)Time elapsed: 2.028 s % 65.30/10.06 % (2071568)Peak memory usage: 129 MB % 65.30/10.06 % (2071568)Instructions burned: 5203 (million) % 65.30/10.06 % (2071595)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2525918613:s2a=on:i=185:s2at=1.8:fdi=4_2968 on theBenchmark for (2968ds/185Mi) % 65.30/10.07 % (2071595)Instruction limit reached! % 65.30/10.07 % (2071595)------------------------------ % 65.30/10.07 % (2071595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.30/10.07 % (2071595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.30/10.07 % (2071595)CaDiCaL version: 2.1.3 % 65.30/10.07 % (2071595)Termination reason: Instruction limit % 65.30/10.07 % (2071595)Termination phase: Saturation % 65.30/10.07 % (2071595)Time elapsed: 0.104 s % 65.30/10.07 % (2071595)Peak memory usage: 92 MB % 65.30/10.07 % (2071595)Instructions burned: 185 (million) % 65.30/10.07 % (2071596)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2911582742:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2967 on theBenchmark for (2967ds/193Mi) % 65.30/10.07 % (2071596)Refutation not found, incomplete strategy % 65.30/10.07 % (2071596)------------------------------ % 65.30/10.07 % (2071596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.55/12.95 % (2071596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.55/12.95 % (2071596)CaDiCaL version: 2.1.3 % 85.55/12.95 % (2071596)Termination reason: Refutation not found, incomplete strategy % 85.55/12.95 % (2071596)Time elapsed: 0.008 s % 85.55/12.95 % (2071596)Peak memory usage: 89 MB % 85.55/12.95 % (2071596)Instructions burned: 9 (million) % 85.55/12.95 % (2071598)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1514375678:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2966 on theBenchmark for (2966ds/4850Mi) % 85.55/12.95 % (2071596)------------------------------ % 85.55/12.95 % (2071596)------------------------------ % 85.55/12.95 % (2071601)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2914403065:i=12111:sd=1:ss=included_2963 on theBenchmark for (2963ds/12111Mi) % 85.55/12.95 % (2071601)Refutation not found, incomplete strategy % 85.55/12.95 % (2071601)------------------------------ % 85.55/12.95 % (2071601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.55/12.95 % (2071601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.55/12.95 % (2071601)CaDiCaL version: 2.1.3 % 85.55/12.95 % (2071601)Termination reason: Refutation not found, incomplete strategy % 85.55/12.95 % (2071601)Time elapsed: 0.604 s % 85.55/12.95 % (2071601)Peak memory usage: 129 MB % 85.55/12.95 % (2071601)Instructions burned: 915 (million) % 85.55/12.95 % (2071601)------------------------------ % 85.55/12.95 % (2071601)------------------------------ % 85.55/12.95 % (2071603)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=983180508:i=319:kws=precedence:fsr=off_2953 on theBenchmark for (2953ds/319Mi) % 85.55/12.95 % (2071603)Instruction limit reached! % 85.55/12.95 % (2071603)------------------------------ % 85.55/12.95 % (2071603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.55/12.95 % (2071603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.55/12.95 % (2071603)CaDiCaL version: 2.1.3 % 85.55/12.95 % (2071603)Termination reason: Instruction limit % 85.55/12.95 % (2071603)Termination phase: Saturation % 85.55/12.95 % (2071603)Time elapsed: 0.136 s % 85.55/12.95 % (2071603)Peak memory usage: 94 MB % 85.55/12.95 % (2071603)Instructions burned: 320 (million) % 85.55/12.95 % (2071605)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=324740599:i=2064:ep=RST_2950 on theBenchmark for (2950ds/2064Mi) % 85.55/12.95 % (2071586)Instruction limit reached! % 85.55/12.95 % (2071586)------------------------------ % 85.55/12.95 % (2071586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.55/12.95 % (2071586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.55/12.95 % (2071586)CaDiCaL version: 2.1.3 % 85.55/12.95 % (2071586)Termination reason: Instruction limit % 85.55/12.95 % (2071586)Termination phase: Saturation % 85.55/12.95 % (2071586)Time elapsed: 3.444 s % 85.55/12.95 % (2071586)Peak memory usage: 163 MB % 85.55/12.95 % (2071586)Instructions burned: 6062 (million) % 85.55/12.95 % (2071598)Instruction limit reached! % 85.55/12.95 % (2071598)------------------------------ % 85.55/12.95 % (2071598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.55/12.95 % (2071598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.55/12.95 % (2071598)CaDiCaL version: 2.1.3 % 85.55/12.95 % (2071598)Termination reason: Instruction limit % 85.55/12.95 % (2071598)Termination phase: Saturation % 85.55/12.95 % (2071598)Time elapsed: 2.385 s % 85.55/12.95 % (2071598)Peak memory usage: 105 MB % 85.55/12.95 % (2071598)Instructions burned: 4851 (million) % 85.55/12.95 % (2071605)Instruction limit reached! % 85.55/12.95 % (2071605)------------------------------ % 85.55/12.95 % (2071605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.55/12.95 % (2071605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.55/12.95 % (2071605)CaDiCaL version: 2.1.3 % 85.55/12.95 % (2071605)Termination reason: Instruction limit % 85.55/12.95 % (2071605)Termination phase: Saturation % 85.55/12.95 % (2071605)Time elapsed: 0.925 s % 85.55/12.95 % (2071605)Peak memory usage: 95 MB % 85.55/12.95 % (2071605)Instructions burned: 2064 (million) % 85.55/12.95 % (2071607)dis-1011_128_sil=32000:random_seed=2365898779:i=3706:ep=RST:av=off_2941 on theBenchmark for (2941ds/3706Mi) % 85.55/12.95 % (2071608)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2530648305:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2940 on theBenchmark for (2940ds/757Mi) % 102.48/15.30 % (2071608)Refutation not found, incomplete strategy % 102.48/15.30 % (2071608)------------------------------ % 102.48/15.30 % (2071608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/15.30 % (2071608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/15.30 % (2071608)CaDiCaL version: 2.1.3 % 102.48/15.30 % (2071608)Termination reason: Refutation not found, incomplete strategy % 102.48/15.30 % (2071608)Time elapsed: 0.009 s % 102.48/15.30 % (2071608)Peak memory usage: 89 MB % 102.48/15.30 % (2071608)Instructions burned: 15 (million) % 102.48/15.30 % (2071609)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2375532821:i=13913:ss=axioms:sgt=8_2939 on theBenchmark for (2939ds/13913Mi) % 102.48/15.30 % (2071608)------------------------------ % 102.48/15.30 % (2071608)------------------------------ % 102.48/15.30 % (2071613)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=312569385:i=9925:aac=none_2936 on theBenchmark for (2936ds/9925Mi) % 102.48/15.30 % (2071609)Refutation not found, incomplete strategy % 102.48/15.30 % (2071609)------------------------------ % 102.48/15.30 % (2071609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/15.30 % (2071609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/15.30 % (2071609)CaDiCaL version: 2.1.3 % 102.48/15.30 % (2071609)Termination reason: Refutation not found, incomplete strategy % 102.48/15.30 % (2071609)Time elapsed: 0.612 s % 102.48/15.30 % (2071609)Peak memory usage: 129 MB % 102.48/15.30 % (2071609)Instructions burned: 923 (million) % 102.48/15.30 % (2071609)------------------------------ % 102.48/15.30 % (2071609)------------------------------ % 102.48/15.30 % (2071615)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1159668609:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2929 on theBenchmark for (2929ds/2479Mi) % 102.48/15.30 % (2071615)Refutation not found, incomplete strategy % 102.48/15.30 % (2071615)------------------------------ % 102.48/15.30 % (2071615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/15.30 % (2071615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/15.30 % (2071615)CaDiCaL version: 2.1.3 % 102.48/15.30 % (2071615)Termination reason: Refutation not found, incomplete strategy % 102.48/15.30 % (2071615)Time elapsed: 0.004 s % 102.48/15.30 % (2071615)Peak memory usage: 89 MB % 102.48/15.30 % (2071615)Instructions burned: 4 (million) % 102.48/15.30 % (2071615)------------------------------ % 102.48/15.30 % (2071615)------------------------------ % 102.48/15.30 % (2071617)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3752919287:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2925 on theBenchmark for (2925ds/440Mi) % 102.48/15.30 % (2071607)Instruction limit reached! % 102.48/15.30 % (2071607)------------------------------ % 102.48/15.30 % (2071607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/15.30 % (2071607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/15.30 % (2071607)CaDiCaL version: 2.1.3 % 102.48/15.30 % (2071607)Termination reason: Instruction limit % 102.48/15.30 % (2071607)Termination phase: Saturation % 102.48/15.30 % (2071607)Time elapsed: 1.805 s % 102.48/15.30 % (2071607)Peak memory usage: 111 MB % 102.48/15.30 % (2071607)Instructions burned: 3709 (million) % 102.48/15.30 % (2071617)Instruction limit reached! % 102.48/15.30 % (2071617)------------------------------ % 102.48/15.30 % (2071617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.48/15.30 % (2071617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.48/15.30 % (2071617)CaDiCaL version: 2.1.3 % 102.48/15.30 % (2071617)Termination reason: Instruction limit % 102.48/15.30 % (2071617)Termination phase: Saturation % 102.48/15.30 % (2071617)Time elapsed: 0.226 s % 102.48/15.30 % (2071617)Peak memory usage: 94 MB % 102.48/15.30 % (2071617)Instructions burned: 441 (million) % 102.48/15.30 % (2071619)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=608247528:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2921 on theBenchmark for (2921ds/11145Mi) % 102.48/15.30 % (2071620)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1513452222:cts=off:i=3034:av=off:er=known:fsd=on_2921 on theBenchmark for (2921ds/3034Mi) % 102.48/15.30 % (2071576)Instruction limit reached! % 102.48/15.30 % (2071576)------------------------------ % 102.48/15.30 % (2071576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.84/17.64 % (2071576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.84/17.64 % (2071576)CaDiCaL version: 2.1.3 % 118.84/17.64 % (2071576)Termination reason: Instruction limit % 118.84/17.64 % (2071576)Termination phase: Saturation % 118.84/17.64 % (2071576)Time elapsed: 7.600 s % 118.84/17.64 % (2071576)Peak memory usage: 202 MB % 118.84/17.64 % (2071576)Instructions burned: 13194 (million) % 118.84/17.64 % (2071623)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=464234840:st=2:s2a=on:i=524:s2at=2:ss=axioms_2907 on theBenchmark for (2907ds/524Mi) % 118.84/17.64 % (2071623)Instruction limit reached! % 118.84/17.64 % (2071623)------------------------------ % 118.84/17.64 % (2071623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.84/17.64 % (2071623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.84/17.64 % (2071623)CaDiCaL version: 2.1.3 % 118.84/17.64 % (2071623)Termination reason: Instruction limit % 118.84/17.64 % (2071623)Termination phase: Saturation % 118.84/17.64 % (2071623)Time elapsed: 0.250 s % 118.84/17.64 % (2071623)Peak memory usage: 96 MB % 118.84/17.64 % (2071623)Instructions burned: 525 (million) % 118.84/17.64 % (2071620)Instruction limit reached! % 118.84/17.64 % (2071620)------------------------------ % 118.84/17.64 % (2071620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.84/17.64 % (2071620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.84/17.64 % (2071620)CaDiCaL version: 2.1.3 % 118.84/17.64 % (2071620)Termination reason: Instruction limit % 118.84/17.64 % (2071620)Termination phase: Saturation % 118.84/17.64 % (2071620)Time elapsed: 1.730 s % 118.84/17.64 % (2071620)Peak memory usage: 145 MB % 118.84/17.64 % (2071620)Instructions burned: 3034 (million) % 118.84/17.64 % (2071625)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3432586576:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2903 on theBenchmark for (2903ds/1016Mi) % 118.84/17.64 % (2071625)Refutation not found, incomplete strategy % 118.84/17.64 % (2071625)------------------------------ % 118.84/17.64 % (2071625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.84/17.64 % (2071625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.84/17.64 % (2071625)CaDiCaL version: 2.1.3 % 118.84/17.64 % (2071625)Termination reason: Refutation not found, incomplete strategy % 118.84/17.64 % (2071625)Time elapsed: 0.003 s % 118.84/17.64 % (2071625)Peak memory usage: 89 MB % 118.84/17.64 % (2071625)Instructions burned: 2 (million) % 118.84/17.64 % (2071626)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2137098459:i=14123:bd=preordered:ins=4_2902 on theBenchmark for (2902ds/14123Mi) % 118.84/17.64 % (2071625)------------------------------ % 118.84/17.64 % (2071625)------------------------------ % 118.84/17.64 % (2071629)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=212821825:i=5781:kws=precedence:bd=all:rawr=on_2899 on theBenchmark for (2899ds/5781Mi) % 118.84/17.64 % (2071590)Instruction limit reached! % 118.84/17.64 % (2071590)------------------------------ % 118.84/17.64 % (2071590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.84/17.64 % (2071590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.84/17.64 % (2071590)CaDiCaL version: 2.1.3 % 118.84/17.64 % (2071590)Termination reason: Instruction limit % 118.84/17.64 % (2071590)Termination phase: Saturation % 118.84/17.64 % (2071590)Time elapsed: 7.784 s % 118.84/17.64 % (2071590)Peak memory usage: 208 MB % 118.84/17.64 % (2071590)Instructions burned: 14155 (million) % 118.84/17.64 % (2071631)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2644298696:i=2448:gtgl=5:bd=preordered:gtg=all_2894 on theBenchmark for (2894ds/2448Mi) % 118.84/17.64 % (2071613)Instruction limit reached! % 118.84/17.64 % (2071613)------------------------------ % 118.84/17.64 % (2071613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.84/17.64 % (2071613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.84/17.64 % (2071613)CaDiCaL version: 2.1.3 % 118.84/17.64 % (2071613)Termination reason: Instruction limit % 118.84/17.64 % (2071613)Termination phase: Saturation % 118.84/17.64 % (2071613)Time elapsed: 5.427 s % 118.84/17.64 % (2071613)Peak memory usage: 200 MB % 118.84/17.64 % (2071613)Instructions burned: 9927 (million) % 118.84/17.64 % (2071633)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3597376646:i=3223:kws=precedence:fgj=on:av=off_2880 on theBenchmark for (2880ds/3223Mi) % 133.48/19.71 % (2071631)Instruction limit reached! % 133.48/19.71 % (2071631)------------------------------ % 133.48/19.71 % (2071631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.48/19.71 % (2071631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.48/19.71 % (2071631)CaDiCaL version: 2.1.3 % 133.48/19.71 % (2071631)Termination reason: Instruction limit % 133.48/19.71 % (2071631)Termination phase: Saturation % 133.48/19.71 % (2071631)Time elapsed: 1.496 s % 133.48/19.71 % (2071631)Peak memory usage: 144 MB % 133.48/19.71 % (2071631)Instructions burned: 2450 (million) % 133.48/19.71 % (2071635)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1474755505:st=5.6:i=2033:sd=3:ss=axioms_2878 on theBenchmark for (2878ds/2033Mi) % 133.48/19.71 % (2071635)Instruction limit reached! % 133.48/19.71 % (2071635)------------------------------ % 133.48/19.71 % (2071635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.48/19.71 % (2071635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.48/19.71 % (2071635)CaDiCaL version: 2.1.3 % 133.48/19.71 % (2071635)Termination reason: Instruction limit % 133.48/19.71 % (2071635)Termination phase: Saturation % 133.48/19.71 % (2071635)Time elapsed: 1.145 s % 133.48/19.71 % (2071635)Peak memory usage: 142 MB % 133.48/19.71 % (2071635)Instructions burned: 2034 (million) % 133.48/19.71 % (2071629)Instruction limit reached! % 133.48/19.71 % (2071629)------------------------------ % 133.48/19.71 % (2071629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.48/19.71 % (2071629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.48/19.71 % (2071629)CaDiCaL version: 2.1.3 % 133.48/19.71 % (2071629)Termination reason: Instruction limit % 133.48/19.71 % (2071629)Termination phase: Saturation % 133.48/19.71 % (2071629)Time elapsed: 3.338 s % 133.48/19.71 % (2071629)Peak memory usage: 149 MB % 133.48/19.71 % (2071629)Instructions burned: 5781 (million) % 133.48/19.71 % (2071637)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2223096496:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2865 on theBenchmark for (2865ds/2055Mi) % 133.48/19.71 % (2071638)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=2900344484:i=21611:sd=3:ss=axioms_2864 on theBenchmark for (2864ds/21611Mi) % 133.48/19.71 % (2071619)Instruction limit reached! % 133.48/19.71 % (2071619)------------------------------ % 133.48/19.71 % (2071619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.48/19.71 % (2071619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.48/19.71 % (2071619)CaDiCaL version: 2.1.3 % 133.48/19.71 % (2071619)Termination reason: Instruction limit % 133.48/19.71 % (2071619)Termination phase: Saturation % 133.48/19.71 % (2071619)Time elapsed: 6.081 s % 133.48/19.71 % (2071619)Peak memory usage: 159 MB % 133.48/19.71 % (2071619)Instructions burned: 11147 (million) % 133.48/19.71 % (2071641)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1685444495:i=4835:sd=13:ss=axioms:sgt=23_2858 on theBenchmark for (2858ds/4835Mi) % 133.48/19.71 % (2071633)Instruction limit reached! % 133.48/19.71 % (2071633)------------------------------ % 133.48/19.71 % (2071633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.48/19.71 % (2071633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.48/19.71 % (2071633)CaDiCaL version: 2.1.3 % 133.48/19.71 % (2071633)Termination reason: Instruction limit % 133.48/19.71 % (2071633)Termination phase: Saturation % 133.48/19.71 % (2071633)Time elapsed: 2.186 s % 133.48/19.71 % (2071633)Peak memory usage: 149 MB % 133.48/19.71 % (2071633)Instructions burned: 3224 (million) % 133.48/19.71 % (2071638)Refutation not found, incomplete strategy % 133.48/19.71 % (2071638)------------------------------ % 133.48/19.71 % (2071638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.48/19.71 % (2071638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.48/19.71 % (2071638)CaDiCaL version: 2.1.3 % 133.48/19.71 % (2071638)Termination reason: Refutation not found, incomplete strategy % 133.48/19.71 % (2071638)Time elapsed: 0.612 s % 133.48/19.71 % (2071638)Peak memory usage: 129 MB % 133.48/19.71 % (2071638)Instructions burned: 921 (million) % 133.48/19.71 % (2071643)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1320243109:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2857 on theBenchmark for (2857ds/797Mi) % 169.22/24.77 % (2071638)------------------------------ % 169.22/24.77 % (2071638)------------------------------ % 169.22/24.77 % (2071637)Instruction limit reached! % 169.22/24.77 % (2071637)------------------------------ % 169.22/24.77 % (2071637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.22/24.77 % (2071637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.22/24.77 % (2071637)CaDiCaL version: 2.1.3 % 169.22/24.77 % (2071637)Termination reason: Instruction limit % 169.22/24.77 % (2071637)Termination phase: Saturation % 169.22/24.77 % (2071637)Time elapsed: 1.014 s % 169.22/24.77 % (2071637)Peak memory usage: 129 MB % 169.22/24.77 % (2071637)Instructions burned: 2055 (million) % 169.22/24.77 % (2071645)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3072841214:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2854 on theBenchmark for (2854ds/2326Mi) % 169.22/24.77 % (2071646)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=487931778:i=6038:nm=6_2853 on theBenchmark for (2853ds/6038Mi) % 169.22/24.78 % (2071643)Instruction limit reached! % 169.22/24.78 % (2071643)------------------------------ % 169.22/24.78 % (2071643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.22/24.78 % (2071643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.22/24.78 % (2071643)CaDiCaL version: 2.1.3 % 169.22/24.78 % (2071643)Termination reason: Instruction limit % 169.22/24.78 % (2071643)Termination phase: Saturation % 169.22/24.78 % (2071643)Time elapsed: 0.434 s % 169.22/24.78 % (2071643)Peak memory usage: 96 MB % 169.22/24.78 % (2071643)Instructions burned: 798 (million) % 169.22/24.78 % (2071649)lrs+10_1_sil=32000:sp=occurrence:random_seed=4224429241:st=2:i=33334:sd=3:ss=included:sgt=32_2851 on theBenchmark for (2851ds/33334Mi) % 169.22/24.78 % (2071641)Instruction limit reached! % 169.22/24.78 % (2071641)------------------------------ % 169.22/24.78 % (2071641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.22/24.78 % (2071641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.22/24.78 % (2071641)CaDiCaL version: 2.1.3 % 169.22/24.78 % (2071641)Termination reason: Instruction limit % 169.22/24.78 % (2071641)Termination phase: Saturation % 169.22/24.78 % (2071641)Time elapsed: 1.730 s % 169.22/24.78 % (2071641)Peak memory usage: 91 MB % 169.22/24.78 % (2071641)Instructions burned: 4837 (million) % 169.22/24.78 % (2071645)Instruction limit reached! % 169.22/24.78 % (2071645)------------------------------ % 169.22/24.78 % (2071645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.22/24.78 % (2071645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.22/24.78 % (2071645)CaDiCaL version: 2.1.3 % 169.22/24.78 % (2071645)Termination reason: Instruction limit % 169.22/24.78 % (2071645)Termination phase: Saturation % 169.22/24.78 % (2071645)Time elapsed: 1.399 s % 169.22/24.78 % (2071645)Peak memory usage: 102 MB % 169.22/24.78 % (2071645)Instructions burned: 2326 (million) % 169.22/24.78 % (2071651)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3374708604:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2839 on theBenchmark for (2839ds/1008Mi) % 169.22/24.78 % (2071652)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=2188127777:i=8327:s2at=5:bd=preordered_2838 on theBenchmark for (2838ds/8327Mi) % 169.22/24.78 % (2071651)Instruction limit reached! % 169.22/24.78 % (2071651)------------------------------ % 169.22/24.78 % (2071651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.22/24.78 % (2071651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.22/24.78 % (2071651)CaDiCaL version: 2.1.3 % 169.22/24.78 % (2071651)Termination reason: Instruction limit % 169.22/24.78 % (2071651)Termination phase: Saturation % 169.22/24.78 % (2071651)Time elapsed: 0.472 s % 169.22/24.78 % (2071651)Peak memory usage: 96 MB % 169.22/24.78 % (2071651)Instructions burned: 1008 (million) % 169.22/24.78 % (2071655)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2512171057:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2833 on theBenchmark for (2833ds/1083Mi) % 210.12/30.54 % (2071655)Instruction limit reached! % 210.12/30.54 % (2071655)------------------------------ % 210.12/30.54 % (2071655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.12/30.54 % (2071655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.12/30.54 % (2071655)CaDiCaL version: 2.1.3 % 210.12/30.54 % (2071655)Termination reason: Instruction limit % 210.12/30.54 % (2071655)Termination phase: Saturation % 210.12/30.54 % (2071655)Time elapsed: 0.518 s % 210.12/30.54 % (2071655)Peak memory usage: 94 MB % 210.12/30.54 % (2071655)Instructions burned: 1084 (million) % 210.12/30.54 % (2071657)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=156072066:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2826 on theBenchmark for (2826ds/1084Mi) % 210.12/30.54 % (2071657)Refutation not found, incomplete strategy % 210.12/30.54 % (2071657)------------------------------ % 210.12/30.54 % (2071657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.12/30.54 % (2071657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.12/30.54 % (2071657)CaDiCaL version: 2.1.3 % 210.12/30.54 % (2071657)Termination reason: Refutation not found, incomplete strategy % 210.12/30.54 % (2071657)Time elapsed: 0.003 s % 210.12/30.54 % (2071657)Peak memory usage: 88 MB % 210.12/30.54 % (2071657)Instructions burned: 2 (million) % 210.12/30.54 % (2071657)------------------------------ % 210.12/30.54 % (2071657)------------------------------ % 210.12/30.54 % (2071659)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3053017049:i=6995:s2at=5:gtg=all_2822 on theBenchmark for (2822ds/6995Mi) % 210.12/30.54 % (2071626)Instruction limit reached! % 210.12/30.54 % (2071626)------------------------------ % 210.12/30.54 % (2071626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.12/30.54 % (2071626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.12/30.54 % (2071626)CaDiCaL version: 2.1.3 % 210.12/30.54 % (2071626)Termination reason: Instruction limit % 210.12/30.54 % (2071626)Termination phase: Saturation % 210.12/30.54 % (2071626)Time elapsed: 8.089 s % 210.12/30.54 % (2071626)Peak memory usage: 201 MB % 210.12/30.54 % (2071626)Instructions burned: 14124 (million) % 210.12/30.54 % (2071646)Instruction limit reached! % 210.12/30.54 % (2071646)------------------------------ % 210.12/30.54 % (2071646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.12/30.54 % (2071646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.12/30.54 % (2071646)CaDiCaL version: 2.1.3 % 210.12/30.54 % (2071646)Termination reason: Instruction limit % 210.12/30.54 % (2071646)Termination phase: Saturation % 210.12/30.54 % (2071646)Time elapsed: 3.244 s % 210.12/30.54 % (2071646)Peak memory usage: 230 MB % 210.12/30.54 % (2071646)Instructions burned: 6039 (million) % 210.12/30.54 % (2071661)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=625728114:st=2:i=6225:sd=15:ss=axioms_2819 on theBenchmark for (2819ds/6225Mi) % 210.12/30.54 % (2071661)Refutation not found, incomplete strategy % 210.12/30.54 % (2071661)------------------------------ % 210.12/30.54 % (2071661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.12/30.54 % (2071661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.12/30.54 % (2071661)CaDiCaL version: 2.1.3 % 210.12/30.54 % (2071661)Termination reason: Refutation not found, incomplete strategy % 210.12/30.54 % (2071661)Time elapsed: 0.015 s % 210.12/30.54 % (2071661)Peak memory usage: 89 MB % 210.12/30.54 % (2071661)Instructions burned: 24 (million) % 210.12/30.54 % (2071662)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=508899920:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2819 on theBenchmark for (2819ds/3372Mi) % 210.12/30.54 % (2071661)------------------------------ % 210.12/30.54 % (2071661)------------------------------ % 210.12/30.54 % (2071665)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1067049534:st=2.3:i=26457:sd=10:ss=included:sgt=8_2815 on theBenchmark for (2815ds/26457Mi) % 210.12/30.54 % (2071662)Refutation not found, incomplete strategy % 210.12/30.54 % (2071662)------------------------------ % 210.12/30.54 % (2071662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.12/30.54 % (2071662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.12/30.54 % (2071662)CaDiCaL version: 2.1.3 % 210.12/30.54 % (2071662)Termination reason: Refutation not found, incomplete strategy % 226.26/32.94 % (2071662)Time elapsed: 0.598 s % 226.26/32.94 % (2071662)Peak memory usage: 129 MB % 226.26/32.94 % (2071662)Instructions burned: 901 (million) % 226.26/32.94 % (2071662)------------------------------ % 226.26/32.94 % (2071662)------------------------------ % 226.26/32.94 % (2071667)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=1275812602:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2809 on theBenchmark for (2809ds/13494Mi) % 226.26/32.94 % (2071652)Instruction limit reached! % 226.26/32.94 % (2071652)------------------------------ % 226.26/32.94 % (2071652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.26/32.94 % (2071652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.26/32.94 % (2071652)CaDiCaL version: 2.1.3 % 226.26/32.94 % (2071652)Termination reason: Instruction limit % 226.26/32.94 % (2071652)Termination phase: Saturation % 226.26/32.94 % (2071652)Time elapsed: 4.955 s % 226.26/32.94 % (2071652)Peak memory usage: 171 MB % 226.26/32.94 % (2071652)Instructions burned: 8327 (million) % 226.26/32.94 % (2071669)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=2922330131:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2787 on theBenchmark for (2787ds/2503Mi) % 226.26/32.94 % (2071659)Instruction limit reached! % 226.26/32.94 % (2071659)------------------------------ % 226.26/32.94 % (2071659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.26/32.94 % (2071659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.26/32.94 % (2071659)CaDiCaL version: 2.1.3 % 226.26/32.94 % (2071659)Termination reason: Instruction limit % 226.26/32.94 % (2071659)Termination phase: Saturation % 226.26/32.94 % (2071659)Time elapsed: 4.145 s % 226.26/32.94 % (2071659)Peak memory usage: 167 MB % 226.26/32.94 % (2071659)Instructions burned: 6995 (million) % 226.26/32.94 % (2071671)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1716758198:i=2559:sd=1:ep=RSTC:ss=axioms_2779 on theBenchmark for (2779ds/2559Mi) % 226.26/32.94 % (2071669)Instruction limit reached! % 226.26/32.94 % (2071669)------------------------------ % 226.26/32.94 % (2071669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.26/32.94 % (2071669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.26/32.94 % (2071669)CaDiCaL version: 2.1.3 % 226.26/32.94 % (2071669)Termination reason: Instruction limit % 226.26/32.94 % (2071669)Termination phase: Saturation % 226.26/32.94 % (2071669)Time elapsed: 1.258 s % 226.26/32.94 % (2071669)Peak memory usage: 130 MB % 226.26/32.94 % (2071669)Instructions burned: 2504 (million) % 226.26/32.94 % (2071671)Refutation not found, incomplete strategy % 226.26/32.94 % (2071671)------------------------------ % 226.26/32.94 % (2071671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.26/32.94 % (2071671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.26/32.94 % (2071671)CaDiCaL version: 2.1.3 % 226.26/32.94 % (2071671)Termination reason: Refutation not found, incomplete strategy % 226.26/32.94 % (2071671)Time elapsed: 0.594 s % 226.26/32.94 % (2071671)Peak memory usage: 128 MB % 226.26/32.94 % (2071671)Instructions burned: 894 (million) % 226.26/32.94 % (2071673)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2804952123:i=30753:av=off:ss=included_2772 on theBenchmark for (2772ds/30753Mi) % 226.26/32.94 % (2071671)------------------------------ % 226.26/32.94 % (2071671)------------------------------ % 226.26/32.94 % (2071675)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=900757264:i=26473:ep=RSTC_2769 on theBenchmark for (2769ds/26473Mi) % 226.26/32.94 % (2071673)Refutation not found, incomplete strategy % 226.26/32.94 % (2071673)------------------------------ % 226.26/32.94 % (2071673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.26/32.94 % (2071673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.26/32.94 % (2071673)CaDiCaL version: 2.1.3 % 226.26/32.94 % (2071673)Termination reason: Refutation not found, incomplete strategy % 226.26/32.94 % (2071673)Time elapsed: 0.642 s % 226.26/32.94 % (2071673)Peak memory usage: 128 MB % 226.26/32.94 % (2071673)Instructions burned: 921 (million) % 226.26/32.94 % (2071673)------------------------------ % 226.26/32.94 % (2071673)------------------------------ % 226.26/32.94 % (2071677)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=2880243502:cts=off:i=2759:kws=inv_arity:fgj=on_2762 on theBenchmark for (2762ds/2759Mi) % 252.14/36.40 % (2071677)Instruction limit reached! % 252.14/36.40 % (2071677)------------------------------ % 252.14/36.40 % (2071677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.14/36.40 % (2071677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.14/36.40 % (2071677)CaDiCaL version: 2.1.3 % 252.14/36.40 % (2071677)Termination reason: Instruction limit % 252.14/36.40 % (2071677)Termination phase: Saturation % 252.14/36.40 % (2071677)Time elapsed: 1.769 s % 252.14/36.40 % (2071677)Peak memory usage: 149 MB % 252.14/36.40 % (2071677)Instructions burned: 2759 (million) % 252.14/36.40 % (2071679)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=3142128489:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2743 on theBenchmark for (2743ds/5665Mi) % 252.14/36.40 % (2071667)Instruction limit reached! % 252.14/36.40 % (2071667)------------------------------ % 252.14/36.40 % (2071667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.14/36.40 % (2071667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.14/36.40 % (2071667)CaDiCaL version: 2.1.3 % 252.14/36.40 % (2071667)Termination reason: Instruction limit % 252.14/36.40 % (2071667)Termination phase: Saturation % 252.14/36.40 % (2071667)Time elapsed: 7.765 s % 252.14/36.40 % (2071667)Peak memory usage: 246 MB % 252.14/36.40 % (2071667)Instructions burned: 13495 (million) % 252.14/36.40 % (2071681)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=2581253318:i=1532:ep=RS:ss=axioms_2729 on theBenchmark for (2729ds/1532Mi) % 252.14/36.40 % (2071681)Refutation not found, incomplete strategy % 252.14/36.40 % (2071681)------------------------------ % 252.14/36.40 % (2071681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.14/36.40 % (2071681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.14/36.40 % (2071681)CaDiCaL version: 2.1.3 % 252.14/36.40 % (2071681)Termination reason: Refutation not found, incomplete strategy % 252.14/36.40 % (2071681)Time elapsed: 0.589 s % 252.14/36.40 % (2071681)Peak memory usage: 129 MB % 252.14/36.40 % (2071681)Instructions burned: 891 (million) % 252.14/36.40 % (2071681)------------------------------ % 252.14/36.40 % (2071681)------------------------------ % 252.14/36.40 % (2071683)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3513658272:i=1565:sd=2:ss=axioms:sgt=32_2719 on theBenchmark for (2719ds/1565Mi) % 252.14/36.40 % (2071679)Instruction limit reached! % 252.14/36.40 % (2071679)------------------------------ % 252.14/36.40 % (2071679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.14/36.40 % (2071679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.14/36.40 % (2071679)CaDiCaL version: 2.1.3 % 252.14/36.40 % (2071679)Termination reason: Instruction limit % 252.14/36.40 % (2071679)Termination phase: Saturation % 252.14/36.40 % (2071679)Time elapsed: 2.676 s % 252.14/36.40 % (2071679)Peak memory usage: 136 MB % 252.14/36.40 % (2071679)Instructions burned: 5667 (million) % 252.14/36.40 % (2071685)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=463649618:i=1572:fgj=on:gsp=on_2714 on theBenchmark for (2714ds/1572Mi) % 252.14/36.40 % (2071683)Instruction limit reached! % 252.14/36.40 % (2071683)------------------------------ % 252.14/36.40 % (2071683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.14/36.40 % (2071683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.14/36.40 % (2071683)CaDiCaL version: 2.1.3 % 252.14/36.40 % (2071683)Termination reason: Instruction limit % 252.14/36.40 % (2071683)Termination phase: Saturation % 252.14/36.40 % (2071683)Time elapsed: 1.069 s % 252.14/36.40 % (2071683)Peak memory usage: 136 MB % 252.14/36.40 % (2071683)Instructions burned: 1566 (million) % 252.14/36.40 % (2071687)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2348798927:i=6052:sd=4:ss=axioms:sgt=24_2707 on theBenchmark for (2707ds/6052Mi) % 252.14/36.40 % (2071685)Instruction limit reached! % 252.14/36.40 % (2071685)------------------------------ % 252.14/36.40 % (2071685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.40/38.48 % (2071685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.40/38.48 % (2071685)CaDiCaL version: 2.1.3 % 266.40/38.48 % (2071685)Termination reason: Instruction limit % 266.40/38.48 % (2071685)Termination phase: Saturation % 266.40/38.48 % (2071685)Time elapsed: 0.979 s % 266.40/38.48 % (2071685)Peak memory usage: 152 MB % 266.40/38.48 % (2071685)Instructions burned: 1573 (million) % 266.40/38.48 % (2071689)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=3482546198:i=3500:sd=1:bd=preordered:sup=off:ss=included_2703 on theBenchmark for (2703ds/3500Mi) % 266.40/38.48 % (2071687)Refutation not found, incomplete strategy % 266.40/38.48 % (2071687)------------------------------ % 266.40/38.48 % (2071687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.40/38.48 % (2071687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.40/38.48 % (2071687)CaDiCaL version: 2.1.3 % 266.40/38.48 % (2071687)Termination reason: Refutation not found, incomplete strategy % 266.40/38.48 % (2071687)Time elapsed: 0.595 s % 266.40/38.48 % (2071687)Peak memory usage: 129 MB % 266.40/38.48 % (2071687)Instructions burned: 901 (million) % 266.40/38.48 % (2071687)------------------------------ % 266.40/38.48 % (2071687)------------------------------ % 266.40/38.48 % (2071691)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=3792817144:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2697 on theBenchmark for (2697ds/1842Mi) % 266.40/38.48 % (2071689)Refutation not found, incomplete strategy % 266.40/38.48 % (2071689)------------------------------ % 266.40/38.48 % (2071689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.40/38.48 % (2071689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.40/38.48 % (2071689)CaDiCaL version: 2.1.3 % 266.40/38.48 % (2071689)Termination reason: Refutation not found, incomplete strategy % 266.40/38.48 % (2071689)Time elapsed: 0.621 s % 266.40/38.48 % (2071689)Peak memory usage: 128 MB % 266.40/38.48 % (2071689)Instructions burned: 891 (million) % 266.40/38.48 % (2071689)------------------------------ % 266.40/38.48 % (2071689)------------------------------ % 266.40/38.48 % (2071693)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1018580257:i=66096:add=on_2692 on theBenchmark for (2692ds/66096Mi) % 266.40/38.48 % (2071691)Refutation not found, incomplete strategy % 266.40/38.48 % (2071691)------------------------------ % 266.40/38.48 % (2071691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.40/38.48 % (2071691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.40/38.48 % (2071691)CaDiCaL version: 2.1.3 % 266.40/38.48 % (2071691)Termination reason: Refutation not found, incomplete strategy % 266.40/38.48 % (2071691)Time elapsed: 0.620 s % 266.40/38.48 % (2071691)Peak memory usage: 129 MB % 266.40/38.48 % (2071691)Instructions burned: 933 (million) % 266.40/38.48 % (2071691)------------------------------ % 266.40/38.48 % (2071691)------------------------------ % 266.40/38.48 % (2071649)Instruction limit reached! % 266.40/38.48 % (2071649)------------------------------ % 266.40/38.48 % (2071649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.40/38.48 % (2071649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.40/38.48 % (2071649)CaDiCaL version: 2.1.3 % 266.40/38.48 % (2071649)Termination reason: Instruction limit % 266.40/38.48 % (2071649)Termination phase: Saturation % 266.40/38.48 % (2071649)Time elapsed: 16.443 s % 266.40/38.48 % (2071649)Peak memory usage: 342 MB % 266.40/38.48 % (2071649)Instructions burned: 33338 (million) % 266.40/38.48 % (2071695)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=322002212:i=1884:sd=1:nm=60:ss=axioms_2686 on theBenchmark for (2686ds/1884Mi) % 266.40/38.48 % (2071697)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1067236635:cts=off:i=5469:bs=on:fsr=off_2684 on theBenchmark for (2684ds/5469Mi) % 266.40/38.48 % (2071695)Refutation not found, incomplete strategy % 266.40/38.48 % (2071695)------------------------------ % 266.40/38.48 % (2071695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.40/38.48 % (2071695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.40/38.48 % (2071695)CaDiCaL version: 2.1.3 % 266.40/38.48 % (2071695)Termination reason: Refutation not found, incomplete strategy % 288.35/41.56 % (2071695)Time elapsed: 0.595 s % 288.35/41.56 % (2071695)Peak memory usage: 129 MB % 288.35/41.56 % (2071695)Instructions burned: 898 (million) % 288.35/41.56 % (2071695)------------------------------ % 288.35/41.56 % (2071695)------------------------------ % 288.35/41.56 % (2071699)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=1395913998:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2676 on theBenchmark for (2676ds/2037Mi) % 288.35/41.56 % (2071665)Instruction limit reached! % 288.35/41.56 % (2071665)------------------------------ % 288.35/41.56 % (2071665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.56 % (2071665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.56 % (2071665)CaDiCaL version: 2.1.3 % 288.35/41.56 % (2071665)Termination reason: Instruction limit % 288.35/41.56 % (2071665)Termination phase: Saturation % 288.35/41.56 % (2071665)Time elapsed: 15.005 s % 288.35/41.56 % (2071665)Peak memory usage: 258 MB % 288.35/41.56 % (2071665)Instructions burned: 26458 (million) % 288.35/41.56 % (2071699)Instruction limit reached! % 288.35/41.56 % (2071699)------------------------------ % 288.35/41.56 % (2071699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.56 % (2071699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.56 % (2071699)CaDiCaL version: 2.1.3 % 288.35/41.56 % (2071699)Termination reason: Instruction limit % 288.35/41.56 % (2071699)Termination phase: Saturation % 288.35/41.56 % (2071699)Time elapsed: 1.251 s % 288.35/41.56 % (2071699)Peak memory usage: 145 MB % 288.35/41.56 % (2071699)Instructions burned: 2037 (million) % 288.35/41.56 % (2071701)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=111717450:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2663 on theBenchmark for (2663ds/2110Mi) % 288.35/41.56 % (2071702)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=3424573075:i=2430:add=off:aac=none:nm=16_2662 on theBenchmark for (2662ds/2430Mi) % 288.35/41.56 % (2071697)Instruction limit reached! % 288.35/41.56 % (2071697)------------------------------ % 288.35/41.56 % (2071697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.56 % (2071697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.56 % (2071697)CaDiCaL version: 2.1.3 % 288.35/41.56 % (2071697)Termination reason: Instruction limit % 288.35/41.56 % (2071697)Termination phase: Saturation % 288.35/41.56 % (2071697)Time elapsed: 2.710 s % 288.35/41.56 % (2071697)Peak memory usage: 103 MB % 288.35/41.56 % (2071697)Instructions burned: 5469 (million) % 288.35/41.56 % (2071705)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=408320878:cond=fast:i=4891_2656 on theBenchmark for (2656ds/4891Mi) % 288.35/41.56 % (2071701)Instruction limit reached! % 288.35/41.56 % (2071701)------------------------------ % 288.35/41.56 % (2071701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.56 % (2071701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.56 % (2071701)CaDiCaL version: 2.1.3 % 288.35/41.56 % (2071701)Termination reason: Instruction limit % 288.35/41.56 % (2071701)Termination phase: Saturation % 288.35/41.56 % (2071701)Time elapsed: 1.283 s % 288.35/41.56 % (2071701)Peak memory usage: 146 MB % 288.35/41.56 % (2071701)Instructions burned: 2111 (million) % 288.35/41.56 % (2071707)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=3125877321:st=2:i=14845:sd=2:ss=included:fsd=on_2648 on theBenchmark for (2648ds/14845Mi) % 288.35/41.56 % (2071702)Instruction limit reached! % 288.35/41.56 % (2071702)------------------------------ % 288.35/41.56 % (2071702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 288.35/41.56 % (2071702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 288.35/41.56 % (2071702)CaDiCaL version: 2.1.3 % 288.35/41.56 % (2071702)Termination reason: Instruction limit % 288.35/41.56 % (2071702)Termination phase: Saturation % 288.35/41.56 % (2071702)Time elapsed: 1.443 s % 288.35/41.56 % (2071702)Peak memory usage: 144 MB % 288.35/41.56 % (2071702)Instructions burned: 2430 (million) % 288.35/41.56 % (2071709)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:nTerminated %------------------------------------------------------------------------------