%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM961_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n007.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 12:17:42 PM UTC 2026 % Result : Timeout 291.69s 42.76s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM961_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.39 % Computer : n007.cluster.edu % 0.09/0.39 % Model : x86_64 x86_64 % 0.09/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.39 % Memory : 8046.5625MB % 0.09/0.39 % OS : Linux 6.8.0-71-generic % 0.09/0.39 % CPULimit : 300 % 0.09/0.39 % WCLimit : 300 % 0.09/0.39 % DateTime : Sun Sep 27 21:46:11 UTC 2026 % 0.09/0.39 % CPUTime : % 0.09/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.43 Running first-order theorem proving % 0.09/0.43 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 % 4.81/1.71 % (1808780)Detected formulas, will run a generic FOF schedule. % 4.81/1.71 % (1808787)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=2568436264:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 4.81/1.71 % (1808787)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.81/1.71 % (1808785)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=2107208209:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 4.81/1.71 % (1808791)dis-21_1_sil=8000:lcm=predicate:random_seed=3255112113: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) % 4.81/1.71 % (1808786)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=324757440:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 4.81/1.71 % (1808789)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3511373062:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 4.81/1.71 % (1808788)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3666404316:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 4.81/1.71 % (1808790)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=634683751:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 4.81/1.71 % (1808788)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.81/1.71 % (1808788)Refutation not found, incomplete strategy % 4.81/1.71 % (1808788)------------------------------ % 4.81/1.71 % (1808788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.81/1.71 % (1808788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.81/1.71 % (1808788)CaDiCaL version: 2.1.3 % 4.81/1.71 % (1808788)Termination reason: Refutation not found, incomplete strategy % 4.81/1.71 % (1808788)Time elapsed: 0.019 s % 4.81/1.71 % (1808788)Peak memory usage: 88 MB % 4.81/1.71 % (1808788)Instructions burned: 31 (million) % 4.81/1.71 % (1808789)Instruction limit reached! % 4.81/1.71 % (1808789)------------------------------ % 4.81/1.71 % (1808789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.81/1.71 % (1808789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.81/1.71 % (1808789)CaDiCaL version: 2.1.3 % 4.81/1.71 % (1808789)Termination reason: Instruction limit % 4.81/1.71 % (1808789)Termination phase: Saturation % 4.81/1.71 % (1808789)Time elapsed: 0.062 s % 4.81/1.71 % (1808789)Peak memory usage: 88 MB % 4.81/1.71 % (1808789)Instructions burned: 120 (million) % 4.81/1.71 % (1808791)Instruction limit reached! % 4.81/1.71 % (1808791)------------------------------ % 4.81/1.71 % (1808791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.81/1.71 % (1808791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.81/1.71 % (1808791)CaDiCaL version: 2.1.3 % 4.81/1.71 % (1808791)Termination reason: Instruction limit % 4.81/1.71 % (1808791)Termination phase: Saturation % 4.81/1.71 % (1808791)Time elapsed: 0.071 s % 4.81/1.71 % (1808791)Peak memory usage: 89 MB % 4.81/1.71 % (1808791)Instructions burned: 131 (million) % 4.81/1.71 % (1808790)Instruction limit reached! % 4.81/1.71 % (1808790)------------------------------ % 4.81/1.71 % (1808790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.81/1.71 % (1808790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.81/1.71 % (1808790)CaDiCaL version: 2.1.3 % 4.81/1.71 % (1808790)Termination reason: Instruction limit % 4.81/1.71 % (1808790)Termination phase: Saturation % 4.81/1.71 % (1808790)Time elapsed: 0.083 s % 4.81/1.71 % (1808790)Peak memory usage: 90 MB % 4.81/1.71 % (1808790)Instructions burned: 139 (million) % 4.81/1.71 % (1808787)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 4.81/1.71 % (1808787)------------------------------ % 4.81/1.71 % (1808787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.81/1.71 % (1808787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.81/1.71 % (1808787)CaDiCaL version: 2.1.3 % 4.81/1.71 % (1808787)Termination reason: Unknown % 4.81/1.71 % (1808787)Termination phase: Saturation % 6.20/1.92 % (1808787)Time elapsed: 0.198 s % 6.20/1.92 % (1808787)Peak memory usage: 113 MB % 6.20/1.92 % (1808787)Instructions burned: 541 (million) % 6.20/1.92 % (1808799)lrs+10_1_sil=8000:sp=occurrence:random_seed=1299254941:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 6.20/1.92 % (1808800)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4024727125:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 6.20/1.92 % (1808801)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3889244708:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 6.20/1.92 % (1808788)------------------------------ % 6.20/1.92 % (1808788)------------------------------ % 6.20/1.92 % (1808802)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=4008697513:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 6.20/1.92 % (1808800)Instruction limit reached! % 6.20/1.92 % (1808800)------------------------------ % 6.20/1.92 % (1808800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.20/1.92 % (1808800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.20/1.92 % (1808800)CaDiCaL version: 2.1.3 % 6.20/1.92 % (1808800)Termination reason: Instruction limit % 6.20/1.92 % (1808800)Termination phase: Saturation % 6.20/1.92 % (1808800)Time elapsed: 0.089 s % 6.20/1.92 % (1808800)Peak memory usage: 90 MB % 6.20/1.92 % (1808800)Instructions burned: 159 (million) % 6.20/1.92 % (1808802)Instruction limit reached! % 6.20/1.92 % (1808802)------------------------------ % 6.20/1.92 % (1808802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.20/1.92 % (1808802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.20/1.92 % (1808802)CaDiCaL version: 2.1.3 % 6.20/1.92 % (1808802)Termination reason: Instruction limit % 6.20/1.92 % (1808802)Termination phase: Saturation % 6.20/1.92 % (1808802)Time elapsed: 0.076 s % 6.20/1.92 % (1808802)Peak memory usage: 91 MB % 6.20/1.92 % (1808802)Instructions burned: 248 (million) % 6.20/1.92 % (1808799)Instruction limit reached! % 6.20/1.92 % (1808799)------------------------------ % 6.20/1.92 % (1808799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.20/1.92 % (1808799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.20/1.92 % (1808799)CaDiCaL version: 2.1.3 % 6.20/1.92 % (1808799)Termination reason: Instruction limit % 6.20/1.92 % (1808799)Termination phase: Saturation % 6.20/1.92 % (1808799)Time elapsed: 0.156 s % 6.20/1.92 % (1808799)Peak memory usage: 91 MB % 6.20/1.92 % (1808799)Instructions burned: 285 (million) % 6.20/1.92 % (1808786)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 6.20/1.92 % (1808786)------------------------------ % 6.20/1.92 % (1808786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.20/1.92 % (1808786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.20/1.92 % (1808785)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 6.20/1.92 % (1808785)------------------------------ % 6.20/1.92 % (1808785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.20/1.92 % (1808786)CaDiCaL version: 2.1.3 % 6.20/1.92 % (1808786)Termination reason: Unknown % 6.20/1.92 % (1808786)Termination phase: Saturation % 6.20/1.92 % (1808786)Time elapsed: 0.362 s % 6.20/1.92 % (1808785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.20/1.92 % (1808786)Peak memory usage: 113 MB % 6.20/1.92 % (1808786)Instructions burned: 543 (million) % 6.20/1.92 % (1808785)CaDiCaL version: 2.1.3 % 6.20/1.92 % (1808785)Termination reason: Unknown % 6.20/1.92 % (1808785)Termination phase: Saturation % 6.20/1.92 % (1808785)Time elapsed: 0.362 s % 6.20/1.92 % (1808785)Peak memory usage: 113 MB % 6.20/1.92 % (1808785)Instructions burned: 540 (million) % 6.20/1.92 % (1808807)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=420371974:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 6.20/1.92 % (1808807)Refutation not found, incomplete strategy % 6.20/1.92 % (1808807)------------------------------ % 6.20/1.92 % (1808807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.20/1.92 % (1808807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.20/1.92 % (1808807)CaDiCaL version: 2.1.3 % 6.20/1.92 % (1808807)Termination reason: Refutation not found, incomplete strategy % 6.20/1.92 % (1808807)Time elapsed: 0.006 s % 6.20/1.92 % (1808807)Peak memory usage: 88 MB % 9.28/2.16 % (1808807)Instructions burned: 9 (million) % 9.28/2.16 % (1808801)Instruction limit reached! % 9.28/2.16 % (1808801)------------------------------ % 9.28/2.16 % (1808801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.28/2.16 % (1808801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.28/2.16 % (1808801)CaDiCaL version: 2.1.3 % 9.28/2.16 % (1808801)Termination reason: Instruction limit % 9.28/2.16 % (1808801)Termination phase: Saturation % 9.28/2.16 % (1808801)Time elapsed: 0.195 s % 9.28/2.16 % (1808801)Peak memory usage: 92 MB % 9.28/2.16 % (1808801)Instructions burned: 325 (million) % 9.28/2.16 % (1808808)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=486037146:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 9.28/2.16 % (1808809)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4129835197:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 9.28/2.16 % (1808809)Instruction limit reached! % 9.28/2.16 % (1808809)------------------------------ % 9.28/2.16 % (1808809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.28/2.16 % (1808809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.28/2.16 % (1808809)CaDiCaL version: 2.1.3 % 9.28/2.16 % (1808809)Termination reason: Instruction limit % 9.28/2.16 % (1808809)Termination phase: Saturation % 9.28/2.16 % (1808809)Time elapsed: 0.037 s % 9.28/2.16 % (1808809)Peak memory usage: 89 MB % 9.28/2.16 % (1808809)Instructions burned: 114 (million) % 9.28/2.16 % (1808810)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3944059900:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi) % 9.28/2.16 % (1808813)lrs+10_1_sil=8000:sp=occurrence:random_seed=1217632634:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 9.28/2.16 % (1808812)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1010790101:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 9.28/2.16 % (1808810)Instruction limit reached! % 9.28/2.16 % (1808810)------------------------------ % 9.28/2.16 % (1808810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.28/2.16 % (1808810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.28/2.16 % (1808810)CaDiCaL version: 2.1.3 % 9.28/2.16 % (1808810)Termination reason: Instruction limit % 9.28/2.16 % (1808810)Termination phase: Saturation % 9.28/2.16 % (1808810)Time elapsed: 0.053 s % 9.28/2.16 % (1808810)Peak memory usage: 87 MB % 9.28/2.16 % (1808810)Instructions burned: 129 (million) % 9.28/2.16 % (1808816)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4174219311:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 9.28/2.16 % (1808816)Refutation not found, incomplete strategy % 9.28/2.16 % (1808816)------------------------------ % 9.28/2.16 % (1808816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.28/2.16 % (1808816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.28/2.16 % (1808816)CaDiCaL version: 2.1.3 % 9.28/2.16 % (1808816)Termination reason: Refutation not found, incomplete strategy % 9.28/2.16 % (1808816)Time elapsed: 0.005 s % 9.28/2.16 % (1808816)Peak memory usage: 88 MB % 9.28/2.16 % (1808816)Instructions burned: 8 (million) % 9.28/2.16 % (1808812)Instruction limit reached! % 9.28/2.16 % (1808812)------------------------------ % 9.28/2.16 % (1808812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.28/2.16 % (1808812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.28/2.16 % (1808812)CaDiCaL version: 2.1.3 % 9.28/2.16 % (1808812)Termination reason: Instruction limit % 9.28/2.16 % (1808812)Termination phase: Saturation % 9.28/2.16 % (1808812)Time elapsed: 0.052 s % 9.28/2.16 % (1808812)Peak memory usage: 88 MB % 9.28/2.16 % (1808812)Instructions burned: 115 (million) % 9.28/2.16 % (1808818)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=446615085:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 9.28/2.16 % (1808807)------------------------------ % 9.28/2.16 % (1808807)------------------------------ % 9.28/2.16 % (1808822)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2449351207:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2993 on theBenchmark for (2993ds/134Mi) % 9.28/2.16 % (1808825)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2447639080:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 10.22/2.47 % (1808825)Refutation not found, incomplete strategy % 10.22/2.47 % (1808825)------------------------------ % 10.22/2.47 % (1808825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.22/2.47 % (1808825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.22/2.47 % (1808825)CaDiCaL version: 2.1.3 % 10.22/2.47 % (1808825)Termination reason: Refutation not found, incomplete strategy % 10.22/2.47 % (1808825)Time elapsed: 0.005 s % 10.22/2.47 % (1808825)Peak memory usage: 88 MB % 10.22/2.47 % (1808825)Instructions burned: 8 (million) % 10.22/2.47 % (1808822)Instruction limit reached! % 10.22/2.47 % (1808822)------------------------------ % 10.22/2.47 % (1808822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.22/2.47 % (1808822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.22/2.47 % (1808822)CaDiCaL version: 2.1.3 % 10.22/2.47 % (1808822)Termination reason: Instruction limit % 10.22/2.47 % (1808822)Termination phase: Saturation % 10.22/2.47 % (1808822)Time elapsed: 0.080 s % 10.22/2.47 % (1808822)Peak memory usage: 90 MB % 10.22/2.47 % (1808822)Instructions burned: 135 (million) % 10.22/2.47 % (1808818)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 10.22/2.47 % (1808818)------------------------------ % 10.22/2.47 % (1808818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.22/2.47 % (1808818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.22/2.47 % (1808818)CaDiCaL version: 2.1.3 % 10.22/2.47 % (1808818)Termination reason: Unknown % 10.22/2.47 % (1808818)Termination phase: Saturation % 10.22/2.47 % (1808818)Time elapsed: 0.199 s % 10.22/2.47 % (1808818)Peak memory usage: 113 MB % 10.22/2.47 % (1808818)Instructions burned: 542 (million) % 10.22/2.47 % (1808827)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3144802333:st=3:i=13193:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/13193Mi) % 10.22/2.47 % (1808808)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 10.22/2.47 % (1808808)------------------------------ % 10.22/2.47 % (1808808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.22/2.47 % (1808808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.22/2.47 % (1808808)CaDiCaL version: 2.1.3 % 10.22/2.47 % (1808808)Termination reason: Unknown % 10.22/2.47 % (1808808)Termination phase: Saturation % 10.22/2.47 % (1808808)Time elapsed: 0.366 s % 10.22/2.47 % (1808808)Peak memory usage: 113 MB % 10.22/2.47 % (1808808)Instructions burned: 540 (million) % 10.22/2.47 % (1808816)------------------------------ % 10.22/2.47 % (1808816)------------------------------ % 10.22/2.47 % (1808830)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2415218875:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 10.22/2.47 % (1808829)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=1595781662:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/125Mi) % 10.22/2.47 % (1808829)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.22/2.47 % (1808830)Instruction limit reached! % 10.22/2.47 % (1808830)------------------------------ % 10.22/2.47 % (1808830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.22/2.47 % (1808830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.22/2.47 % (1808830)CaDiCaL version: 2.1.3 % 10.22/2.47 % (1808830)Termination reason: Instruction limit % 10.22/2.47 % (1808830)Termination phase: Saturation % 10.22/2.47 % (1808830)Time elapsed: 0.040 s % 10.22/2.47 % (1808830)Peak memory usage: 90 MB % 10.22/2.47 % (1808830)Instructions burned: 134 (million) % 10.22/2.47 % (1808833)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1574824054:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/431Mi) % 10.22/2.47 % (1808832)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1784716809:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/141Mi) % 10.22/2.47 % (1808832)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.22/2.47 % (1808832)Refutation not found, incomplete strategy % 10.22/2.47 % (1808832)------------------------------ % 12.18/2.95 % (1808832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.18/2.95 % (1808832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.18/2.95 % (1808832)CaDiCaL version: 2.1.3 % 12.18/2.95 % (1808832)Termination reason: Refutation not found, incomplete strategy % 12.18/2.95 % (1808832)Time elapsed: 0.002 s % 12.18/2.95 % (1808832)Peak memory usage: 88 MB % 12.18/2.95 % (1808832)Instructions burned: 2 (million) % 12.18/2.95 % (1808829)Instruction limit reached! % 12.18/2.95 % (1808829)------------------------------ % 12.18/2.95 % (1808829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.18/2.95 % (1808829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.18/2.95 % (1808829)CaDiCaL version: 2.1.3 % 12.18/2.95 % (1808829)Termination reason: Instruction limit % 12.18/2.95 % (1808829)Termination phase: Saturation % 12.18/2.95 % (1808829)Time elapsed: 0.072 s % 12.18/2.95 % (1808829)Peak memory usage: 90 MB % 12.18/2.95 % (1808829)Instructions burned: 125 (million) % 12.18/2.95 % (1808825)------------------------------ % 12.18/2.95 % (1808825)------------------------------ % 12.18/2.95 % (1808838)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=1412980531:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 12.18/2.95 % (1808813)Instruction limit reached! % 12.18/2.95 % (1808813)------------------------------ % 12.18/2.95 % (1808813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.18/2.95 % (1808813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.18/2.95 % (1808813)CaDiCaL version: 2.1.3 % 12.18/2.95 % (1808813)Termination reason: Instruction limit % 12.18/2.95 % (1808813)Termination phase: Saturation % 12.18/2.95 % (1808813)Time elapsed: 0.526 s % 12.18/2.95 % (1808813)Peak memory usage: 99 MB % 12.18/2.95 % (1808813)Instructions burned: 907 (million) % 12.18/2.95 % (1808839)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=1504944373:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2989 on theBenchmark for (2989ds/150Mi) % 12.18/2.95 % (1808839)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 12.18/2.95 % (1808840)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4240834822:i=14155:bd=all_2988 on theBenchmark for (2988ds/14155Mi) % 12.18/2.95 % (1808833)Instruction limit reached! % 12.18/2.95 % (1808833)------------------------------ % 12.18/2.95 % (1808833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.18/2.95 % (1808833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.18/2.95 % (1808833)CaDiCaL version: 2.1.3 % 12.18/2.95 % (1808833)Termination reason: Instruction limit % 12.18/2.95 % (1808833)Termination phase: Saturation % 12.18/2.95 % (1808833)Time elapsed: 0.208 s % 12.18/2.95 % (1808833)Peak memory usage: 89 MB % 12.18/2.95 % (1808833)Instructions burned: 431 (million) % 12.18/2.95 % (1808827)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 12.18/2.95 % (1808827)------------------------------ % 12.18/2.95 % (1808827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.18/2.95 % (1808827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.18/2.95 % (1808827)CaDiCaL version: 2.1.3 % 12.18/2.95 % (1808827)Termination reason: Unknown % 12.18/2.95 % (1808827)Termination phase: Saturation % 12.18/2.95 % (1808827)Time elapsed: 0.364 s % 12.18/2.95 % (1808827)Peak memory usage: 113 MB % 12.18/2.95 % (1808827)Instructions burned: 540 (million) % 12.18/2.95 % (1808832)------------------------------ % 12.18/2.95 % (1808832)------------------------------ % 12.18/2.95 % (1808842)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4210722286:i=667:av=off:fsr=off_2988 on theBenchmark for (2988ds/667Mi) % 12.18/2.95 % (1808842)Refutation not found, incomplete strategy % 12.18/2.95 % (1808842)------------------------------ % 12.18/2.95 % (1808842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.18/2.95 % (1808842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.18/2.95 % (1808842)CaDiCaL version: 2.1.3 % 12.18/2.95 % (1808842)Termination reason: Refutation not found, incomplete strategy % 12.18/2.95 % (1808842)Time elapsed: 0.005 s % 17.30/3.36 % (1808842)Peak memory usage: 88 MB % 17.30/3.36 % (1808842)Instructions burned: 7 (million) % 17.30/3.36 % (1808839)Instruction limit reached! % 17.30/3.36 % (1808839)------------------------------ % 17.30/3.36 % (1808839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.30/3.36 % (1808839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.30/3.36 % (1808839)CaDiCaL version: 2.1.3 % 17.30/3.36 % (1808839)Termination reason: Instruction limit % 17.30/3.36 % (1808839)Termination phase: Saturation % 17.30/3.36 % (1808839)Time elapsed: 0.099 s % 17.30/3.36 % (1808839)Peak memory usage: 90 MB % 17.30/3.36 % (1808839)Instructions burned: 150 (million) % 17.30/3.36 % (1808838)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 17.30/3.36 % (1808838)------------------------------ % 17.30/3.36 % (1808838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.30/3.36 % (1808838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.30/3.36 % (1808838)CaDiCaL version: 2.1.3 % 17.30/3.36 % (1808838)Termination reason: Unknown % 17.30/3.36 % (1808838)Termination phase: Saturation % 17.30/3.36 % (1808838)Time elapsed: 0.196 s % 17.30/3.36 % (1808838)Peak memory usage: 114 MB % 17.30/3.36 % (1808838)Instructions burned: 539 (million) % 17.30/3.36 % (1808845)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=3987445550:s2a=on:i=185:s2at=1.8:fdi=4_2987 on theBenchmark for (2987ds/185Mi) % 17.30/3.36 % (1808846)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2002326144:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2987 on theBenchmark for (2987ds/193Mi) % 17.30/3.36 % (1808848)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4225247095:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2987 on theBenchmark for (2987ds/4850Mi) % 17.30/3.36 % (1808849)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=803113808:i=12111:sd=1:ss=included_2986 on theBenchmark for (2986ds/12111Mi) % 17.30/3.36 % (1808850)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2300997217:i=319:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/319Mi) % 17.30/3.36 % (1808845)Instruction limit reached! % 17.30/3.36 % (1808845)------------------------------ % 17.30/3.36 % (1808845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.30/3.36 % (1808845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.30/3.36 % (1808845)CaDiCaL version: 2.1.3 % 17.30/3.36 % (1808845)Termination reason: Instruction limit % 17.30/3.36 % (1808845)Termination phase: Saturation % 17.30/3.36 % (1808845)Time elapsed: 0.106 s % 17.30/3.36 % (1808845)Peak memory usage: 91 MB % 17.30/3.36 % (1808845)Instructions burned: 186 (million) % 17.30/3.36 % (1808846)Instruction limit reached! % 17.30/3.36 % (1808846)------------------------------ % 17.30/3.36 % (1808846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.30/3.36 % (1808846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.30/3.36 % (1808846)CaDiCaL version: 2.1.3 % 17.30/3.36 % (1808846)Termination reason: Instruction limit % 17.30/3.36 % (1808846)Termination phase: Saturation % 17.30/3.36 % (1808846)Time elapsed: 0.109 s % 17.30/3.36 % (1808846)Peak memory usage: 92 MB % 17.30/3.36 % (1808846)Instructions burned: 194 (million) % 17.30/3.36 % (1808842)------------------------------ % 17.30/3.36 % (1808842)------------------------------ % 17.30/3.36 % (1808840)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 17.30/3.36 % (1808840)------------------------------ % 17.30/3.36 % (1808840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.30/3.36 % (1808840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.30/3.36 % (1808840)CaDiCaL version: 2.1.3 % 17.30/3.36 % (1808840)Termination reason: Unknown % 17.30/3.36 % (1808840)Termination phase: Saturation % 17.30/3.36 % (1808840)Time elapsed: 0.362 s % 17.30/3.36 % (1808840)Peak memory usage: 114 MB % 17.30/3.36 % (1808840)Instructions burned: 541 (million) % 17.30/3.36 % (1808856)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3228599193:i=2064:ep=RST_2985 on theBenchmark for (2985ds/2064Mi) % 17.30/3.36 % (1808856)Refutation not found, incomplete strategy % 17.30/3.36 % (1808856)------------------------------ % 17.30/3.36 % (1808856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.48/4.17 % (1808856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.48/4.17 % (1808856)CaDiCaL version: 2.1.3 % 23.48/4.17 % (1808856)Termination reason: Refutation not found, incomplete strategy % 23.48/4.17 % (1808856)Time elapsed: 0.005 s % 23.48/4.17 % (1808856)Peak memory usage: 88 MB % 23.48/4.17 % (1808856)Instructions burned: 8 (million) % 23.48/4.17 % (1808850)Instruction limit reached! % 23.48/4.17 % (1808850)------------------------------ % 23.48/4.17 % (1808850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.48/4.17 % (1808850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.48/4.17 % (1808850)CaDiCaL version: 2.1.3 % 23.48/4.17 % (1808850)Termination reason: Instruction limit % 23.48/4.17 % (1808850)Termination phase: Saturation % 23.48/4.17 % (1808850)Time elapsed: 0.170 s % 23.48/4.17 % (1808850)Peak memory usage: 93 MB % 23.48/4.17 % (1808850)Instructions burned: 320 (million) % 23.48/4.17 % (1808857)dis-1011_128_sil=32000:random_seed=2273421078:i=3706:ep=RST:av=off_2984 on theBenchmark for (2984ds/3706Mi) % 23.48/4.17 % (1808858)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2777823288:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2984 on theBenchmark for (2984ds/757Mi) % 23.48/4.17 % (1808858)Refutation not found, incomplete strategy % 23.48/4.17 % (1808858)------------------------------ % 23.48/4.17 % (1808858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.48/4.17 % (1808858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.48/4.17 % (1808858)CaDiCaL version: 2.1.3 % 23.48/4.17 % (1808858)Termination reason: Refutation not found, incomplete strategy % 23.48/4.17 % (1808858)Time elapsed: 0.005 s % 23.48/4.17 % (1808858)Peak memory usage: 88 MB % 23.48/4.17 % (1808858)Instructions burned: 7 (million) % 23.48/4.17 % (1808860)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3648327984:i=13913:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/13913Mi) % 23.48/4.17 % (1808861)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=728783556:i=9925:aac=none_2983 on theBenchmark for (2983ds/9925Mi) % 23.48/4.17 % (1808849)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 23.48/4.17 % (1808849)------------------------------ % 23.48/4.17 % (1808849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.48/4.17 % (1808849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.48/4.17 % (1808849)CaDiCaL version: 2.1.3 % 23.48/4.17 % (1808849)Termination reason: Unknown % 23.48/4.17 % (1808849)Termination phase: Saturation % 23.48/4.17 % (1808849)Time elapsed: 0.355 s % 23.48/4.17 % (1808849)Peak memory usage: 114 MB % 23.48/4.17 % (1808849)Instructions burned: 540 (million) % 23.48/4.17 % (1808856)------------------------------ % 23.48/4.17 % (1808856)------------------------------ % 23.48/4.17 % (1808858)------------------------------ % 23.48/4.17 % (1808858)------------------------------ % 23.48/4.17 % (1808866)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1429750720:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 23.48/4.17 % (1808866)Refutation not found, incomplete strategy % 23.48/4.17 % (1808866)------------------------------ % 23.48/4.17 % (1808866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.48/4.17 % (1808866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.48/4.17 % (1808866)CaDiCaL version: 2.1.3 % 23.48/4.17 % (1808866)Termination reason: Refutation not found, incomplete strategy % 23.48/4.17 % (1808866)Time elapsed: 0.002 s % 23.48/4.17 % (1808866)Peak memory usage: 89 MB % 23.48/4.17 % (1808866)Instructions burned: 6 (million) % 23.48/4.17 % (1808867)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3140533842:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/440Mi) % 23.48/4.17 % (1808867)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 23.48/4.17 % (1808869)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4010645140:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2980 on theBenchmark for (2980ds/11145Mi) % 23.48/4.17 % (1808866)------------------------------ % 23.48/4.17 % (1808866)------------------------------ % 26.82/4.96 % (1808860)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 26.82/4.96 % (1808860)------------------------------ % 26.82/4.96 % (1808860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.82/4.96 % (1808860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.96 % (1808860)CaDiCaL version: 2.1.3 % 26.82/4.96 % (1808860)Termination reason: Unknown % 26.82/4.96 % (1808860)Termination phase: Saturation % 26.82/4.96 % (1808860)Time elapsed: 0.358 s % 26.82/4.96 % (1808860)Peak memory usage: 113 MB % 26.82/4.96 % (1808860)Instructions burned: 538 (million) % 26.82/4.96 % (1808861)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 26.82/4.96 % (1808861)------------------------------ % 26.82/4.96 % (1808861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.82/4.96 % (1808861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.96 % (1808861)CaDiCaL version: 2.1.3 % 26.82/4.96 % (1808861)Termination reason: Unknown % 26.82/4.96 % (1808861)Termination phase: Saturation % 26.82/4.96 % (1808861)Time elapsed: 0.362 s % 26.82/4.96 % (1808861)Peak memory usage: 113 MB % 26.82/4.96 % (1808861)Instructions burned: 540 (million) % 26.82/4.96 % (1808872)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=1207028926:cts=off:i=3034:av=off:er=known:fsd=on_2979 on theBenchmark for (2979ds/3034Mi) % 26.82/4.96 % (1808873)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1219548355:st=2:s2a=on:i=524:s2at=2:ss=axioms_2979 on theBenchmark for (2979ds/524Mi) % 26.82/4.96 % (1808867)Instruction limit reached! % 26.82/4.96 % (1808867)------------------------------ % 26.82/4.96 % (1808867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.82/4.96 % (1808867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.96 % (1808867)CaDiCaL version: 2.1.3 % 26.82/4.96 % (1808867)Termination reason: Instruction limit % 26.82/4.96 % (1808867)Termination phase: Saturation % 26.82/4.96 % (1808867)Time elapsed: 0.250 s % 26.82/4.96 % (1808867)Peak memory usage: 93 MB % 26.82/4.96 % (1808867)Instructions burned: 441 (million) % 26.82/4.96 % (1808874)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1802268639:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2978 on theBenchmark for (2978ds/1016Mi) % 26.82/4.96 % (1808872)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 26.82/4.96 % (1808872)------------------------------ % 26.82/4.96 % (1808872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.82/4.96 % (1808872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.96 % (1808872)CaDiCaL version: 2.1.3 % 26.82/4.96 % (1808872)Termination reason: Unknown % 26.82/4.96 % (1808872)Termination phase: Saturation % 26.82/4.96 % (1808872)Time elapsed: 0.195 s % 26.82/4.96 % (1808872)Peak memory usage: 113 MB % 26.82/4.96 % (1808872)Instructions burned: 540 (million) % 26.82/4.96 % (1808877)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2471328754:i=14123:bd=preordered:ins=4_2977 on theBenchmark for (2977ds/14123Mi) % 26.82/4.96 % (1808869)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 26.82/4.96 % (1808869)------------------------------ % 26.82/4.96 % (1808869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.82/4.96 % (1808869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.96 % (1808869)CaDiCaL version: 2.1.3 % 26.82/4.96 % (1808869)Termination reason: Unknown % 26.82/4.96 % (1808869)Termination phase: Saturation % 26.82/4.96 % (1808869)Time elapsed: 0.359 s % 26.82/4.96 % (1808869)Peak memory usage: 113 MB % 26.82/4.96 % (1808869)Instructions burned: 540 (million) % 26.82/4.96 % (1808880)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2575831829:i=5781:kws=precedence:bd=all:rawr=on_2976 on theBenchmark for (2976ds/5781Mi) % 26.82/4.96 % (1808873)Instruction limit reached! % 26.82/4.96 % (1808873)------------------------------ % 26.82/4.96 % (1808873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.82/4.96 % (1808873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.82/4.96 % (1808873)CaDiCaL version: 2.1.3 % 26.82/4.96 % (1808873)Termination reason: Instruction limit % 26.82/4.96 % (1808873)Termination phase: Saturation % 32.92/5.90 % (1808873)Time elapsed: 0.284 s % 32.92/5.90 % (1808873)Peak memory usage: 94 MB % 32.92/5.90 % (1808873)Instructions burned: 524 (million) % 32.92/5.90 % (1808881)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=2946652891:i=2448:gtgl=5:bd=preordered:gtg=all_2976 on theBenchmark for (2976ds/2448Mi) % 32.92/5.90 % (1808883)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2026873093:i=3223:kws=precedence:fgj=on:av=off_2975 on theBenchmark for (2975ds/3223Mi) % 32.92/5.90 % (1808877)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 32.92/5.90 % (1808877)------------------------------ % 32.92/5.90 % (1808877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.92/5.90 % (1808877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.92/5.90 % (1808877)CaDiCaL version: 2.1.3 % 32.92/5.90 % (1808877)Termination reason: Unknown % 32.92/5.90 % (1808877)Termination phase: Saturation % 32.92/5.90 % (1808877)Time elapsed: 0.356 s % 32.92/5.90 % (1808877)Peak memory usage: 113 MB % 32.92/5.90 % (1808877)Instructions burned: 540 (million) % 32.92/5.90 % (1808874)Instruction limit reached! % 32.92/5.90 % (1808874)------------------------------ % 32.92/5.90 % (1808874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.92/5.90 % (1808874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.92/5.90 % (1808874)CaDiCaL version: 2.1.3 % 32.92/5.90 % (1808874)Termination reason: Instruction limit % 32.92/5.90 % (1808874)Termination phase: Saturation % 32.92/5.90 % (1808874)Time elapsed: 0.558 s % 32.92/5.90 % (1808874)Peak memory usage: 100 MB % 32.92/5.90 % (1808874)Instructions burned: 1016 (million) % 32.92/5.90 % (1808886)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3041354842:st=5.6:i=2033:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/2033Mi) % 32.92/5.90 % (1808881)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 32.92/5.90 % (1808881)------------------------------ % 32.92/5.90 % (1808881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.92/5.90 % (1808881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.92/5.90 % (1808881)CaDiCaL version: 2.1.3 % 32.92/5.90 % (1808881)Termination reason: Unknown % 32.92/5.90 % (1808881)Termination phase: Saturation % 32.92/5.90 % (1808881)Time elapsed: 0.357 s % 32.92/5.90 % (1808881)Peak memory usage: 113 MB % 32.92/5.90 % (1808881)Instructions burned: 541 (million) % 32.92/5.90 % (1808887)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3703223871:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2971 on theBenchmark for (2971ds/2055Mi) % 32.92/5.90 % (1808883)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 32.92/5.90 % (1808883)------------------------------ % 32.92/5.90 % (1808883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.92/5.90 % (1808883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.92/5.90 % (1808883)CaDiCaL version: 2.1.3 % 32.92/5.90 % (1808883)Termination reason: Unknown % 32.92/5.90 % (1808883)Termination phase: Saturation % 32.92/5.90 % (1808883)Time elapsed: 0.360 s % 32.92/5.90 % (1808883)Peak memory usage: 113 MB % 32.92/5.90 % (1808883)Instructions burned: 540 (million) % 32.92/5.90 % (1808889)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=1044309018:i=21611:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/21611Mi) % 32.92/5.90 % (1808891)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2648003717:i=4835:sd=13:ss=axioms:sgt=23_2970 on theBenchmark for (2970ds/4835Mi) % 32.92/5.90 % (1808886)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 32.92/5.90 % (1808886)------------------------------ % 32.92/5.90 % (1808886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.92/5.90 % (1808886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.92/5.90 % (1808886)CaDiCaL version: 2.1.3 % 32.92/5.90 % (1808886)Termination reason: Unknown % 32.92/5.90 % (1808886)Termination phase: Saturation % 32.92/5.90 % (1808886)Time elapsed: 0.360 s % 32.92/5.90 % (1808886)Peak memory usage: 113 MB % 32.92/5.90 % (1808886)Instructions burned: 541 (million) % 32.92/5.90 % (1808887)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 37.88/7.00 % (1808887)------------------------------ % 37.88/7.00 % (1808887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.88/7.00 % (1808887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.88/7.00 % (1808887)CaDiCaL version: 2.1.3 % 37.88/7.00 % (1808887)Termination reason: Unknown % 37.88/7.00 % (1808887)Termination phase: Saturation % 37.88/7.00 % (1808887)Time elapsed: 0.359 s % 37.88/7.00 % (1808887)Peak memory usage: 113 MB % 37.88/7.00 % (1808887)Instructions burned: 540 (million) % 37.88/7.00 % (1808894)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=3665266556:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2967 on theBenchmark for (2967ds/797Mi) % 37.88/7.00 % (1808889)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 37.88/7.00 % (1808889)------------------------------ % 37.88/7.00 % (1808889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.88/7.00 % (1808889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.88/7.00 % (1808889)CaDiCaL version: 2.1.3 % 37.88/7.00 % (1808889)Termination reason: Unknown % 37.88/7.00 % (1808889)Termination phase: Saturation % 37.88/7.00 % (1808889)Time elapsed: 0.357 s % 37.88/7.00 % (1808889)Peak memory usage: 113 MB % 37.88/7.00 % (1808889)Instructions burned: 539 (million) % 37.88/7.00 % (1808895)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=835698709:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2966 on theBenchmark for (2966ds/2326Mi) % 37.88/7.00 % (1808897)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=4164360355:i=6038:nm=6_2966 on theBenchmark for (2966ds/6038Mi) % 37.88/7.00 % (1808857)Instruction limit reached! % 37.88/7.00 % (1808857)------------------------------ % 37.88/7.00 % (1808857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.88/7.00 % (1808857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.88/7.00 % (1808857)CaDiCaL version: 2.1.3 % 37.88/7.00 % (1808857)Termination reason: Instruction limit % 37.88/7.00 % (1808857)Termination phase: Saturation % 37.88/7.00 % (1808857)Time elapsed: 1.927 s % 37.88/7.00 % (1808857)Peak memory usage: 114 MB % 37.88/7.00 % (1808857)Instructions burned: 3706 (million) % 37.88/7.00 % (1808900)lrs+10_1_sil=32000:sp=occurrence:random_seed=3312391051:st=2:i=33334:sd=3:ss=included:sgt=32_2964 on theBenchmark for (2964ds/33334Mi) % 37.88/7.00 % (1808894)Instruction limit reached! % 37.88/7.00 % (1808894)------------------------------ % 37.88/7.00 % (1808894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.88/7.00 % (1808894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.88/7.00 % (1808894)CaDiCaL version: 2.1.3 % 37.88/7.00 % (1808894)Termination reason: Instruction limit % 37.88/7.00 % (1808894)Termination phase: Saturation % 37.88/7.00 % (1808894)Time elapsed: 0.430 s % 37.88/7.00 % (1808894)Peak memory usage: 97 MB % 37.88/7.00 % (1808894)Instructions burned: 799 (million) % 37.88/7.00 % (1808902)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3207752800:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2962 on theBenchmark for (2962ds/1008Mi) % 37.88/7.00 % (1808848)Instruction limit reached! % 37.88/7.00 % (1808848)------------------------------ % 37.88/7.00 % (1808848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.88/7.00 % (1808848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.88/7.00 % (1808848)CaDiCaL version: 2.1.3 % 37.88/7.00 % (1808848)Termination reason: Instruction limit % 37.88/7.00 % (1808848)Termination phase: Saturation % 37.88/7.00 % (1808848)Time elapsed: 2.570 s % 37.88/7.00 % (1808848)Peak memory usage: 149 MB % 37.88/7.00 % (1808848)Instructions burned: 4852 (million) % 37.88/7.00 % (1808880)Instruction limit reached! % 37.88/7.00 % (1808880)------------------------------ % 37.88/7.00 % (1808880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.88/7.00 % (1808880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.88/7.00 % (1808880)CaDiCaL version: 2.1.3 % 37.88/7.00 % (1808880)Termination reason: Instruction limit % 37.88/7.00 % (1808880)Termination phase: Saturation % 37.88/7.00 % (1808880)Time elapsed: 1.635 s % 37.88/7.00 % (1808880)Peak memory usage: 142 MB % 40.96/7.49 % (1808880)Instructions burned: 5781 (million) % 40.96/7.49 % (1808904)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=2615023262:i=8327:s2at=5:bd=preordered_2960 on theBenchmark for (2960ds/8327Mi) % 40.96/7.49 % (1808905)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=1295225810:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2958 on theBenchmark for (2958ds/1083Mi) % 40.96/7.49 % (1808895)Instruction limit reached! % 40.96/7.49 % (1808895)------------------------------ % 40.96/7.49 % (1808895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.96/7.49 % (1808895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.96/7.49 % (1808895)CaDiCaL version: 2.1.3 % 40.96/7.49 % (1808895)Termination reason: Instruction limit % 40.96/7.49 % (1808895)Termination phase: Saturation % 40.96/7.49 % (1808895)Time elapsed: 0.797 s % 40.96/7.49 % (1808895)Peak memory usage: 92 MB % 40.96/7.49 % (1808895)Instructions burned: 2327 (million) % 40.96/7.49 % (1808902)Instruction limit reached! % 40.96/7.49 % (1808902)------------------------------ % 40.96/7.49 % (1808902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.96/7.49 % (1808902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.96/7.49 % (1808902)CaDiCaL version: 2.1.3 % 40.96/7.49 % (1808902)Termination reason: Instruction limit % 40.96/7.49 % (1808902)Termination phase: Saturation % 40.96/7.49 % (1808902)Time elapsed: 0.456 s % 40.96/7.49 % (1808902)Peak memory usage: 95 MB % 40.96/7.49 % (1808902)Instructions burned: 1009 (million) % 40.96/7.49 % (1808908)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=446494393:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2957 on theBenchmark for (2957ds/1084Mi) % 40.96/7.49 % (1808905)Instruction limit reached! % 40.96/7.49 % (1808905)------------------------------ % 40.96/7.49 % (1808905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.96/7.49 % (1808905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.96/7.49 % (1808905)CaDiCaL version: 2.1.3 % 40.96/7.49 % (1808905)Termination reason: Instruction limit % 40.96/7.49 % (1808905)Termination phase: Saturation % 40.96/7.49 % (1808905)Time elapsed: 0.242 s % 40.96/7.49 % (1808905)Peak memory usage: 96 MB % 40.96/7.49 % (1808905)Instructions burned: 1083 (million) % 40.96/7.49 % (1808910)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3115788773:i=6995:s2at=5:gtg=all_2956 on theBenchmark for (2956ds/6995Mi) % 40.96/7.49 % (1808911)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=690745471:st=2:i=6225:sd=15:ss=axioms_2955 on theBenchmark for (2955ds/6225Mi) % 40.96/7.49 % (1808897)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 40.96/7.49 % (1808897)------------------------------ % 40.96/7.49 % (1808897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.96/7.49 % (1808897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.96/7.49 % (1808897)CaDiCaL version: 2.1.3 % 40.96/7.49 % (1808897)Termination reason: Unknown % 40.96/7.49 % (1808897)Termination phase: Saturation % 40.96/7.49 % (1808897)Time elapsed: 1.261 s % 40.96/7.49 % (1808897)Peak memory usage: 113 MB % 40.96/7.49 % (1808897)Instructions burned: 540 (million) % 40.96/7.49 % (1808914)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1611599592:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2952 on theBenchmark for (2952ds/3372Mi) % 40.96/7.49 % (1808908)Instruction limit reached! % 40.96/7.49 % (1808908)------------------------------ % 40.96/7.49 % (1808908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.96/7.49 % (1808908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.96/7.49 % (1808908)CaDiCaL version: 2.1.3 % 40.96/7.49 % (1808908)Termination reason: Instruction limit % 40.96/7.49 % (1808908)Termination phase: Saturation % 40.96/7.49 % (1808908)Time elapsed: 0.551 s % 40.96/7.49 % (1808908)Peak memory usage: 103 MB % 40.96/7.49 % (1808908)Instructions burned: 1085 (million) % 40.96/7.49 % (1808916)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1472770161:st=2.3:i=26457:sd=10:ss=included:sgt=8_2950 on theBenchmark for (2950ds/26457Mi) % 44.46/7.98 % (1808914)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 44.46/7.98 % (1808914)------------------------------ % 44.46/7.98 % (1808914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.46/7.98 % (1808914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.46/7.98 % (1808914)CaDiCaL version: 2.1.3 % 44.46/7.98 % (1808914)Termination reason: Unknown % 44.46/7.98 % (1808914)Termination phase: Saturation % 44.46/7.98 % (1808914)Time elapsed: 0.863 s % 44.46/7.98 % (1808914)Peak memory usage: 113 MB % 44.46/7.98 % (1808914)Instructions burned: 539 (million) % 44.46/7.98 % (1808910)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 44.46/7.98 % (1808910)------------------------------ % 44.46/7.98 % (1808910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.46/7.98 % (1808910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.46/7.98 % (1808910)CaDiCaL version: 2.1.3 % 44.46/7.98 % (1808910)Termination reason: Unknown % 44.46/7.98 % (1808910)Termination phase: Saturation % 44.46/7.98 % (1808910)Time elapsed: 1.277 s % 44.46/7.98 % (1808910)Peak memory usage: 113 MB % 44.46/7.98 % (1808910)Instructions burned: 545 (million) % 44.46/7.98 % (1808904)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 44.46/7.98 % (1808904)------------------------------ % 44.46/7.98 % (1808904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.46/7.98 % (1808904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.46/7.98 % (1808904)CaDiCaL version: 2.1.3 % 44.46/7.98 % (1808904)Termination reason: Unknown % 44.46/7.98 % (1808904)Termination phase: Saturation % 44.46/7.98 % (1808904)Time elapsed: 1.642 s % 44.46/7.98 % (1808904)Peak memory usage: 113 MB % 44.46/7.98 % (1808904)Instructions burned: 540 (million) % 44.46/7.98 % (1808891)Instruction limit reached! % 44.46/7.98 % (1808891)------------------------------ % 44.46/7.98 % (1808891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.46/7.98 % (1808891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.46/7.98 % (1808891)CaDiCaL version: 2.1.3 % 44.46/7.98 % (1808891)Termination reason: Instruction limit % 44.46/7.98 % (1808891)Termination phase: Saturation % 44.46/7.98 % (1808891)Time elapsed: 2.671 s % 44.46/7.98 % (1808891)Peak memory usage: 119 MB % 44.46/7.98 % (1808891)Instructions burned: 4836 (million) % 44.46/7.98 % (1808918)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=3333825977:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2942 on theBenchmark for (2942ds/13494Mi) % 44.46/7.98 % (1808920)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3086432051:i=2559:sd=1:ep=RSTC:ss=axioms_2942 on theBenchmark for (2942ds/2559Mi) % 44.46/7.98 % (1808919)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=1849163439:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2942 on theBenchmark for (2942ds/2503Mi) % 44.46/7.98 % (1808919)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 44.46/7.98 % (1808921)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1968864289:i=30753:av=off:ss=included_2941 on theBenchmark for (2941ds/30753Mi) % 44.46/7.98 % (1808911)Instruction limit reached! % 44.46/7.98 % (1808911)------------------------------ % 44.46/7.98 % (1808911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.46/7.98 % (1808911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.46/7.98 % (1808911)CaDiCaL version: 2.1.3 % 44.46/7.98 % (1808911)Termination reason: Instruction limit % 44.46/7.98 % (1808911)Termination phase: Saturation % 44.46/7.98 % (1808911)Time elapsed: 1.546 s % 44.46/7.98 % (1808911)Peak memory usage: 133 MB % 44.46/7.98 % (1808911)Instructions burned: 6225 (million) % 44.46/7.98 % (1808916)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 44.46/7.98 % (1808916)------------------------------ % 44.46/7.98 % (1808916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.46/7.98 % (1808916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.46/7.98 % (1808916)CaDiCaL version: 2.1.3 % 48.96/8.60 % (1808916)Termination reason: Unknown % 48.96/8.60 % (1808916)Termination phase: Saturation % 48.96/8.60 % (1808916)Time elapsed: 1.096 s % 48.96/8.60 % (1808916)Peak memory usage: 113 MB % 48.96/8.60 % (1808916)Instructions burned: 540 (million) % 48.96/8.60 % (1808926)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=956567364:i=26473:ep=RSTC_2939 on theBenchmark for (2939ds/26473Mi) % 48.96/8.60 % (1808927)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=2286009897:cts=off:i=2759:kws=inv_arity:fgj=on_2938 on theBenchmark for (2938ds/2759Mi) % 48.96/8.60 % (1808920)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 48.96/8.60 % (1808920)------------------------------ % 48.96/8.60 % (1808920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.96/8.60 % (1808920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.96/8.60 % (1808920)CaDiCaL version: 2.1.3 % 48.96/8.60 % (1808920)Termination reason: Unknown % 48.96/8.60 % (1808920)Termination phase: Saturation % 48.96/8.60 % (1808920)Time elapsed: 0.355 s % 48.96/8.60 % (1808920)Peak memory usage: 113 MB % 48.96/8.60 % (1808920)Instructions burned: 538 (million) % 48.96/8.60 % (1808918)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 48.96/8.60 % (1808918)------------------------------ % 48.96/8.60 % (1808918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.96/8.60 % (1808918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.96/8.60 % (1808918)CaDiCaL version: 2.1.3 % 48.96/8.60 % (1808918)Termination reason: Unknown % 48.96/8.60 % (1808918)Termination phase: Saturation % 48.96/8.60 % (1808918)Time elapsed: 0.356 s % 48.96/8.60 % (1808918)Peak memory usage: 114 MB % 48.96/8.60 % (1808918)Instructions burned: 544 (million) % 48.96/8.60 % (1808919)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 48.96/8.60 % (1808919)------------------------------ % 48.96/8.60 % (1808919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.96/8.60 % (1808919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.96/8.60 % (1808919)CaDiCaL version: 2.1.3 % 48.96/8.60 % (1808919)Termination reason: Unknown % 48.96/8.60 % (1808919)Termination phase: Saturation % 48.96/8.60 % (1808919)Time elapsed: 0.353 s % 48.96/8.60 % (1808919)Peak memory usage: 113 MB % 48.96/8.60 % (1808919)Instructions burned: 540 (million) % 48.96/8.60 % (1808921)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 48.96/8.60 % (1808921)------------------------------ % 48.96/8.60 % (1808921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.96/8.60 % (1808921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.96/8.60 % (1808921)CaDiCaL version: 2.1.3 % 48.96/8.60 % (1808921)Termination reason: Unknown % 48.96/8.60 % (1808921)Termination phase: Saturation % 48.96/8.60 % (1808921)Time elapsed: 0.356 s % 48.96/8.60 % (1808921)Peak memory usage: 113 MB % 48.96/8.60 % (1808921)Instructions burned: 541 (million) % 48.96/8.60 % (1808932)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1476942808:i=1565:sd=2:ss=axioms:sgt=32_2937 on theBenchmark for (2937ds/1565Mi) % 48.96/8.60 % (1808931)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=1735154553:i=1532:ep=RS:ss=axioms_2937 on theBenchmark for (2937ds/1532Mi) % 48.96/8.60 % (1808930)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=3198421607:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2937 on theBenchmark for (2937ds/5665Mi) % 48.96/8.60 % (1808930)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 48.96/8.60 % (1808933)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=2050388491:i=1572:fgj=on:gsp=on_2936 on theBenchmark for (2936ds/1572Mi) % 48.96/8.60 % (1808933)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 48.96/8.60 % (1808927)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.89/9.10 % (1808927)------------------------------ % 53.89/9.10 % (1808927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.89/9.10 % (1808927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.89/9.10 % (1808927)CaDiCaL version: 2.1.3 % 53.89/9.10 % (1808927)Termination reason: Unknown % 53.89/9.10 % (1808927)Termination phase: Saturation % 53.89/9.10 % (1808927)Time elapsed: 0.360 s % 53.89/9.10 % (1808927)Peak memory usage: 114 MB % 53.89/9.10 % (1808927)Instructions burned: 543 (million) % 53.89/9.10 % (1808938)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1769594768:i=6052:sd=4:ss=axioms:sgt=24_2933 on theBenchmark for (2933ds/6052Mi) % 53.89/9.10 % (1808932)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.89/9.10 % (1808932)------------------------------ % 53.89/9.10 % (1808932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.89/9.10 % (1808932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.89/9.10 % (1808932)CaDiCaL version: 2.1.3 % 53.89/9.10 % (1808932)Termination reason: Unknown % 53.89/9.10 % (1808932)Termination phase: Saturation % 53.89/9.10 % (1808932)Time elapsed: 0.356 s % 53.89/9.10 % (1808932)Peak memory usage: 113 MB % 53.89/9.10 % (1808932)Instructions burned: 539 (million) % 53.89/9.10 % (1808931)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.89/9.10 % (1808931)------------------------------ % 53.89/9.10 % (1808931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.89/9.10 % (1808931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.89/9.10 % (1808931)CaDiCaL version: 2.1.3 % 53.89/9.10 % (1808931)Termination reason: Unknown % 53.89/9.10 % (1808931)Termination phase: Saturation % 53.89/9.10 % (1808931)Time elapsed: 0.355 s % 53.89/9.10 % (1808931)Peak memory usage: 113 MB % 53.89/9.10 % (1808931)Instructions burned: 540 (million) % 53.89/9.10 % (1808930)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.89/9.10 % (1808930)------------------------------ % 53.89/9.10 % (1808930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.89/9.10 % (1808930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.89/9.10 % (1808930)CaDiCaL version: 2.1.3 % 53.89/9.10 % (1808930)Termination reason: Unknown % 53.89/9.10 % (1808930)Termination phase: Saturation % 53.89/9.10 % (1808930)Time elapsed: 0.355 s % 53.89/9.10 % (1808930)Peak memory usage: 113 MB % 53.89/9.10 % (1808930)Instructions burned: 540 (million) % 53.89/9.10 % (1808933)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.89/9.10 % (1808933)------------------------------ % 53.89/9.10 % (1808933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.89/9.10 % (1808933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.89/9.10 % (1808933)CaDiCaL version: 2.1.3 % 53.89/9.10 % (1808933)Termination reason: Unknown % 53.89/9.10 % (1808933)Termination phase: Saturation % 53.89/9.10 % (1808933)Time elapsed: 0.357 s % 53.89/9.10 % (1808933)Peak memory usage: 113 MB % 53.89/9.10 % (1808933)Instructions burned: 538 (million) % 53.89/9.10 % (1808940)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=1213515507:i=3500:sd=1:bd=preordered:sup=off:ss=included_2932 on theBenchmark for (2932ds/3500Mi) % 53.89/9.10 % (1808942)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3381943823:i=66096:add=on_2932 on theBenchmark for (2932ds/66096Mi) % 53.89/9.10 % (1808941)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=2193531969:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2932 on theBenchmark for (2932ds/1842Mi) % 53.89/9.10 % (1808941)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 53.89/9.10 % (1808943)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1447620608:i=1884:sd=1:nm=60:ss=axioms_2931 on theBenchmark for (2931ds/1884Mi) % 53.89/9.10 % (1808938)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.89/9.10 % (1808938)------------------------------ % 53.89/9.10 % (1808938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.78/9.63 % (1808938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.78/9.63 % (1808938)CaDiCaL version: 2.1.3 % 57.78/9.63 % (1808938)Termination reason: Unknown % 57.78/9.63 % (1808938)Termination phase: Saturation % 57.78/9.63 % (1808938)Time elapsed: 0.360 s % 57.78/9.63 % (1808938)Peak memory usage: 113 MB % 57.78/9.63 % (1808938)Instructions burned: 541 (million) % 57.78/9.63 % (1808948)lrs-1011_4:1_sil=16000:bsr=on:random_seed=4118063527:cts=off:i=5469:bs=on:fsr=off_2928 on theBenchmark for (2928ds/5469Mi) % 57.78/9.63 % (1808940)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 57.78/9.63 % (1808940)------------------------------ % 57.78/9.63 % (1808940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.78/9.63 % (1808940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.78/9.63 % (1808940)CaDiCaL version: 2.1.3 % 57.78/9.63 % (1808940)Termination reason: Unknown % 57.78/9.63 % (1808940)Termination phase: Saturation % 57.78/9.63 % (1808940)Time elapsed: 0.354 s % 57.78/9.63 % (1808940)Peak memory usage: 113 MB % 57.78/9.63 % (1808940)Instructions burned: 539 (million) % 57.78/9.63 % (1808941)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 57.78/9.63 % (1808941)------------------------------ % 57.78/9.63 % (1808941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.78/9.63 % (1808941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.78/9.63 % (1808941)CaDiCaL version: 2.1.3 % 57.78/9.63 % (1808941)Termination reason: Unknown % 57.78/9.63 % (1808941)Termination phase: Saturation % 57.78/9.63 % (1808941)Time elapsed: 0.355 s % 57.78/9.63 % (1808941)Peak memory usage: 113 MB % 57.78/9.63 % (1808941)Instructions burned: 541 (million) % 57.78/9.63 % (1808942)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 57.78/9.63 % (1808942)------------------------------ % 57.78/9.63 % (1808942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.78/9.63 % (1808942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.78/9.63 % (1808942)CaDiCaL version: 2.1.3 % 57.78/9.63 % (1808942)Termination reason: Unknown % 57.78/9.63 % (1808942)Termination phase: Saturation % 57.78/9.63 % (1808942)Time elapsed: 0.355 s % 57.78/9.63 % (1808942)Peak memory usage: 113 MB % 57.78/9.63 % (1808942)Instructions burned: 540 (million) % 57.78/9.63 % (1808943)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 57.78/9.63 % (1808943)------------------------------ % 57.78/9.63 % (1808943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.78/9.63 % (1808943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.78/9.63 % (1808943)CaDiCaL version: 2.1.3 % 57.78/9.63 % (1808943)Termination reason: Unknown % 57.78/9.63 % (1808943)Termination phase: Saturation % 57.78/9.63 % (1808943)Time elapsed: 0.356 s % 57.78/9.63 % (1808943)Peak memory usage: 113 MB % 57.78/9.63 % (1808943)Instructions burned: 538 (million) % 57.78/9.63 % (1808950)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=4209642607:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2927 on theBenchmark for (2927ds/2037Mi) % 57.78/9.63 % (1808951)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1448134682:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2927 on theBenchmark for (2927ds/2110Mi) % 57.78/9.63 % (1808952)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=2418146206:i=2430:add=off:aac=none:nm=16_2927 on theBenchmark for (2927ds/2430Mi) % 57.78/9.63 % (1808953)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=4190930095:cond=fast:i=4891_2926 on theBenchmark for (2926ds/4891Mi) % 57.78/9.63 % (1808952)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 57.78/9.63 % (1808952)------------------------------ % 57.78/9.63 % (1808952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.78/9.63 % (1808952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.78/9.63 % (1808952)CaDiCaL version: 2.1.3 % 57.78/9.63 % (1808952)Termination reason: Unknown % 57.78/9.63 % (1808952)Termination phase: Saturation % 61.78/10.22 % (1808952)Time elapsed: 0.353 s % 61.78/10.22 % (1808952)Peak memory usage: 113 MB % 61.78/10.22 % (1808952)Instructions burned: 540 (million) % 61.78/10.22 % (1808950)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 61.78/10.22 % (1808950)------------------------------ % 61.78/10.22 % (1808950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.78/10.22 % (1808950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.78/10.22 % (1808950)CaDiCaL version: 2.1.3 % 61.78/10.22 % (1808950)Termination reason: Unknown % 61.78/10.22 % (1808950)Termination phase: Saturation % 61.78/10.22 % (1808950)Time elapsed: 0.354 s % 61.78/10.22 % (1808950)Peak memory usage: 113 MB % 61.78/10.22 % (1808950)Instructions burned: 545 (million) % 61.78/10.22 % (1808951)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 61.78/10.22 % (1808951)------------------------------ % 61.78/10.22 % (1808951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.78/10.22 % (1808951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.78/10.22 % (1808951)CaDiCaL version: 2.1.3 % 61.78/10.22 % (1808951)Termination reason: Unknown % 61.78/10.22 % (1808951)Termination phase: Saturation % 61.78/10.22 % (1808951)Time elapsed: 0.354 s % 61.78/10.22 % (1808951)Peak memory usage: 113 MB % 61.78/10.22 % (1808951)Instructions burned: 543 (million) % 61.78/10.22 % (1808953)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 61.78/10.22 % (1808953)------------------------------ % 61.78/10.22 % (1808953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.78/10.22 % (1808953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.78/10.22 % (1808953)CaDiCaL version: 2.1.3 % 61.78/10.22 % (1808953)Termination reason: Unknown % 61.78/10.22 % (1808953)Termination phase: Saturation % 61.78/10.22 % (1808953)Time elapsed: 0.355 s % 61.78/10.22 % (1808953)Peak memory usage: 113 MB % 61.78/10.22 % (1808953)Instructions burned: 541 (million) % 61.78/10.22 % (1808960)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=3339175992:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2922 on theBenchmark for (2922ds/10353Mi) % 61.78/10.22 % (1808958)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=653994603:st=2:i=14845:sd=2:ss=included:fsd=on_2922 on theBenchmark for (2922ds/14845Mi) % 61.78/10.22 % (1808959)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=810892467:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2922 on theBenchmark for (2922ds/7534Mi) % 61.78/10.22 % (1808961)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3567838478:i=7860_2922 on theBenchmark for (2922ds/7860Mi) % 61.78/10.22 % (1808961)Refutation not found, incomplete strategy % 61.78/10.22 % (1808961)------------------------------ % 61.78/10.22 % (1808961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.78/10.22 % (1808961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.78/10.22 % (1808961)CaDiCaL version: 2.1.3 % 61.78/10.22 % (1808961)Termination reason: Refutation not found, incomplete strategy % 61.78/10.22 % (1808961)Time elapsed: 0.005 s % 61.78/10.22 % (1808961)Peak memory usage: 88 MB % 61.78/10.22 % (1808961)Instructions burned: 7 (million) % 61.78/10.22 % (1808961)------------------------------ % 61.78/10.22 % (1808961)------------------------------ % 61.78/10.22 % (1808960)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 61.78/10.22 % (1808959)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 61.78/10.22 % (1808960)------------------------------ % 61.78/10.22 % (1808960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.78/10.22 % (1808960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.78/10.22 % (1808959)------------------------------ % 61.78/10.22 % (1808959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.78/10.22 % (1808960)CaDiCaL version: 2.1.3 % 61.78/10.22 % (1808960)Termination reason: Unknown % 61.78/10.22 % (1808960)Termination phase: Saturation % 61.78/10.22 % (1808959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.78/10.22 % (1808960)Time elapsed: 0.355 s % 68.02/11.05 % (1808960)Peak memory usage: 113 MB % 68.02/11.05 % (1808960)Instructions burned: 541 (million) % 68.02/11.05 % (1808958)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 68.02/11.05 % (1808959)CaDiCaL version: 2.1.3 % 68.02/11.05 % (1808958)------------------------------ % 68.02/11.05 % (1808958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.02/11.05 % (1808959)Termination reason: Unknown % 68.02/11.05 % (1808959)Termination phase: Saturation % 68.02/11.05 % (1808959)Time elapsed: 0.355 s % 68.02/11.05 % (1808958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.02/11.05 % (1808959)Peak memory usage: 113 MB % 68.02/11.05 % (1808959)Instructions burned: 543 (million) % 68.02/11.05 % (1808958)CaDiCaL version: 2.1.3 % 68.02/11.05 % (1808958)Termination reason: Unknown % 68.02/11.05 % (1808958)Termination phase: Saturation % 68.02/11.05 % (1808958)Time elapsed: 0.355 s % 68.02/11.05 % (1808958)Peak memory usage: 114 MB % 68.02/11.05 % (1808958)Instructions burned: 540 (million) % 68.02/11.05 % (1808966)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=2846720453:i=7896:sd=2:bs=on:ss=included:sgt=20_2918 on theBenchmark for (2918ds/7896Mi) % 68.02/11.05 % (1808968)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=2439601112:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2917 on theBenchmark for (2917ds/2965Mi) % 68.02/11.05 % (1808967)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1699828299:i=5812:gtgl=2:gtg=all_2917 on theBenchmark for (2917ds/5812Mi) % 68.02/11.05 % (1808969)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2277088184:i=2967:kws=precedence:bd=preordered:av=off_2917 on theBenchmark for (2917ds/2967Mi) % 68.02/11.05 % (1808966)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 68.02/11.05 % (1808966)------------------------------ % 68.02/11.05 % (1808966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.02/11.05 % (1808966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.02/11.05 % (1808966)CaDiCaL version: 2.1.3 % 68.02/11.05 % (1808966)Termination reason: Unknown % 68.02/11.05 % (1808966)Termination phase: Saturation % 68.02/11.05 % (1808966)Time elapsed: 0.355 s % 68.02/11.05 % (1808966)Peak memory usage: 114 MB % 68.02/11.05 % (1808966)Instructions burned: 540 (million) % 68.02/11.05 % (1808968)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 68.02/11.05 % (1808969)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 68.02/11.05 % (1808968)------------------------------ % 68.02/11.05 % (1808968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.02/11.05 % (1808969)------------------------------ % 68.02/11.05 % (1808969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.02/11.05 % (1808968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.02/11.05 % (1808969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.02/11.05 % (1808968)CaDiCaL version: 2.1.3 % 68.02/11.05 % (1808969)CaDiCaL version: 2.1.3 % 68.02/11.05 % (1808968)Termination reason: Unknown % 68.02/11.05 % (1808968)Termination phase: Saturation % 68.02/11.05 % (1808969)Termination reason: Unknown % 68.02/11.05 % (1808969)Termination phase: Saturation % 68.02/11.05 % (1808968)Time elapsed: 0.354 s % 68.02/11.05 % (1808969)Time elapsed: 0.354 s % 68.02/11.05 % (1808968)Peak memory usage: 113 MB % 68.02/11.05 % (1808969)Peak memory usage: 113 MB % 68.02/11.05 % (1808968)Instructions burned: 540 (million) % 68.02/11.05 % (1808969)Instructions burned: 540 (million) % 68.02/11.05 % (1808967)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 68.02/11.05 % (1808967)------------------------------ % 68.02/11.05 % (1808967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.02/11.05 % (1808967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.02/11.05 % (1808967)CaDiCaL version: 2.1.3 % 68.02/11.05 % (1808967)Termination reason: Unknown % 68.02/11.05 % (1808967)Termination phase: Saturation % 68.02/11.05 % (1808967)Time elapsed: 0.354 s % 68.02/11.05 % (1808967)Peak memory usage: 113 MB % 68.02/11.05 % (1808967)Instructions burned: 543 (million) % 68.02/11.05 % (1808974)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=3465679889:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2913 on theBenchmark for (2913ds/3022Mi) % 70.10/11.58 % (1808976)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3021098294:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2912 on theBenchmark for (2912ds/3289Mi) % 70.10/11.58 % (1808975)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=2692667370:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2912 on theBenchmark for (2912ds/3207Mi) % 70.10/11.58 % (1808977)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1030153380:i=38569:sd=3:ss=axioms:sgt=32_2912 on theBenchmark for (2912ds/38569Mi) % 70.10/11.58 % (1808974)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.10/11.58 % (1808974)------------------------------ % 70.10/11.58 % (1808974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.10/11.58 % (1808974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.10/11.58 % (1808974)CaDiCaL version: 2.1.3 % 70.10/11.58 % (1808974)Termination reason: Unknown % 70.10/11.58 % (1808974)Termination phase: Saturation % 70.10/11.58 % (1808974)Time elapsed: 0.354 s % 70.10/11.58 % (1808974)Peak memory usage: 113 MB % 70.10/11.58 % (1808974)Instructions burned: 538 (million) % 70.10/11.58 % (1808976)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.10/11.58 % (1808976)------------------------------ % 70.10/11.58 % (1808976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.10/11.58 % (1808976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.10/11.58 % (1808976)CaDiCaL version: 2.1.3 % 70.10/11.58 % (1808975)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.10/11.58 % (1808976)Termination reason: Unknown % 70.10/11.58 % (1808976)Termination phase: Saturation % 70.10/11.58 % (1808976)Time elapsed: 0.354 s % 70.10/11.58 % (1808975)------------------------------ % 70.10/11.58 % (1808975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.10/11.58 % (1808976)Peak memory usage: 113 MB % 70.10/11.58 % (1808976)Instructions burned: 540 (million) % 70.10/11.58 % (1808975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.10/11.58 % (1808975)CaDiCaL version: 2.1.3 % 70.10/11.58 % (1808975)Termination reason: Unknown % 70.10/11.58 % (1808975)Termination phase: Saturation % 70.10/11.58 % (1808975)Time elapsed: 0.354 s % 70.10/11.58 % (1808975)Peak memory usage: 113 MB % 70.10/11.58 % (1808975)Instructions burned: 539 (million) % 70.10/11.58 % (1808977)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.10/11.58 % (1808977)------------------------------ % 70.10/11.58 % (1808977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.10/11.58 % (1808977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.10/11.58 % (1808977)CaDiCaL version: 2.1.3 % 70.10/11.58 % (1808977)Termination reason: Unknown % 70.10/11.58 % (1808977)Termination phase: Saturation % 70.10/11.58 % (1808977)Time elapsed: 0.355 s % 70.10/11.58 % (1808977)Peak memory usage: 113 MB % 70.10/11.58 % (1808977)Instructions burned: 540 (million) % 70.10/11.58 % (1808982)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2646358479:cts=off:i=3394_2908 on theBenchmark for (2908ds/3394Mi) % 70.10/11.58 % (1808984)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2948081472:i=20684:bd=all:gtg=exists_sym_2907 on theBenchmark for (2907ds/20684Mi) % 70.10/11.58 % (1808983)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=2237816014:i=33824:bd=preordered_2907 on theBenchmark for (2907ds/33824Mi) % 70.10/11.58 % (1808985)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=3806198108:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2907 on theBenchmark for (2907ds/7222Mi) % 70.10/11.58 % (1808985)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 75.86/12.21 % (1808982)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.86/12.21 % (1808982)------------------------------ % 75.86/12.21 % (1808982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.86/12.21 % (1808982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/12.21 % (1808982)CaDiCaL version: 2.1.3 % 75.86/12.21 % (1808982)Termination reason: Unknown % 75.86/12.21 % (1808982)Termination phase: Saturation % 75.86/12.21 % (1808982)Time elapsed: 0.357 s % 75.86/12.21 % (1808982)Peak memory usage: 113 MB % 75.86/12.21 % (1808982)Instructions burned: 540 (million) % 75.86/12.21 % (1808984)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.86/12.21 % (1808984)------------------------------ % 75.86/12.21 % (1808984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.86/12.21 % (1808984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/12.21 % (1808984)CaDiCaL version: 2.1.3 % 75.86/12.21 % (1808984)Termination reason: Unknown % 75.86/12.21 % (1808984)Termination phase: Saturation % 75.86/12.21 % (1808984)Time elapsed: 0.355 s % 75.86/12.21 % (1808984)Peak memory usage: 114 MB % 75.86/12.21 % (1808984)Instructions burned: 543 (million) % 75.86/12.21 % (1808983)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.86/12.21 % (1808983)------------------------------ % 75.86/12.21 % (1808983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.86/12.21 % (1808983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/12.21 % (1808983)CaDiCaL version: 2.1.3 % 75.86/12.21 % (1808983)Termination reason: Unknown % 75.86/12.21 % (1808983)Termination phase: Saturation % 75.86/12.21 % (1808983)Time elapsed: 0.353 s % 75.86/12.21 % (1808983)Peak memory usage: 114 MB % 75.86/12.21 % (1808983)Instructions burned: 540 (million) % 75.86/12.21 % (1808985)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.86/12.21 % (1808985)------------------------------ % 75.86/12.21 % (1808985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.86/12.21 % (1808985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/12.21 % (1808985)CaDiCaL version: 2.1.3 % 75.86/12.21 % (1808985)Termination reason: Unknown % 75.86/12.21 % (1808985)Termination phase: Saturation % 75.86/12.21 % (1808985)Time elapsed: 0.357 s % 75.86/12.21 % (1808985)Peak memory usage: 114 MB % 75.86/12.21 % (1808985)Instructions burned: 545 (million) % 75.86/12.21 % (1808990)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2221986278:st=4:i=7295:sd=4:ep=R:ss=axioms_2903 on theBenchmark for (2903ds/7295Mi) % 75.86/12.21 % (1808991)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=325497468:i=4036:ins=10_2903 on theBenchmark for (2903ds/4036Mi) % 75.86/12.21 % (1808992)lrs+10_1_sil=128000:lcm=predicate:random_seed=994769834:st=3:i=43697:sd=5:ss=axioms_2903 on theBenchmark for (2903ds/43697Mi) % 75.86/12.21 % (1808993)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=1015903468:i=17599:gtg=all:ss=axioms:fsd=on_2902 on theBenchmark for (2902ds/17599Mi) % 75.86/12.21 % (1808990)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.86/12.21 % (1808990)------------------------------ % 75.86/12.21 % (1808990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.86/12.21 % (1808990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/12.21 % (1808990)CaDiCaL version: 2.1.3 % 75.86/12.21 % (1808990)Termination reason: Unknown % 75.86/12.21 % (1808990)Termination phase: Saturation % 75.86/12.21 % (1808990)Time elapsed: 0.360 s % 75.86/12.21 % (1808990)Peak memory usage: 113 MB % 75.86/12.21 % (1808990)Instructions burned: 543 (million) % 75.86/12.21 % (1808991)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.86/12.21 % (1808991)------------------------------ % 75.86/12.21 % (1808991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.86/12.21 % (1808991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.86/12.21 % (1808991)CaDiCaL version: 2.1.3 % 75.86/12.21 % (1808991)Termination reason: Unknown % 75.86/12.21 % (1808991)Termination phase: Saturation % 82.88/13.19 % (1808991)Time elapsed: 0.356 s % 82.88/13.19 % (1808991)Peak memory usage: 113 MB % 82.88/13.19 % (1808991)Instructions burned: 540 (million) % 82.88/13.19 % (1808993)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.88/13.19 % (1808993)------------------------------ % 82.88/13.19 % (1808993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.88/13.19 % (1808993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.88/13.19 % (1808993)CaDiCaL version: 2.1.3 % 82.88/13.19 % (1808993)Termination reason: Unknown % 82.88/13.19 % (1808993)Termination phase: Saturation % 82.88/13.19 % (1808993)Time elapsed: 0.356 s % 82.88/13.19 % (1808993)Peak memory usage: 113 MB % 82.88/13.19 % (1808993)Instructions burned: 542 (million) % 82.88/13.19 % (1808948)Instruction limit reached! % 82.88/13.19 % (1808948)------------------------------ % 82.88/13.19 % (1808948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.88/13.19 % (1808948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.88/13.19 % (1808948)CaDiCaL version: 2.1.3 % 82.88/13.19 % (1808948)Termination reason: Instruction limit % 82.88/13.19 % (1808948)Termination phase: Saturation % 82.88/13.19 % (1808948)Time elapsed: 2.993 s % 82.88/13.19 % (1808948)Peak memory usage: 136 MB % 82.88/13.19 % (1808948)Instructions burned: 5471 (million) % 82.88/13.19 % (1808998)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=2382521646:i=4547:bd=preordered_2898 on theBenchmark for (2898ds/4547Mi) % 82.88/13.19 % (1808999)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=1248246692:i=9294:av=off_2898 on theBenchmark for (2898ds/9294Mi) % 82.88/13.19 % (1809000)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=506640195:i=32849:add=on_2897 on theBenchmark for (2897ds/32849Mi) % 82.88/13.19 % (1809001)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2892755962:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2897 on theBenchmark for (2897ds/4793Mi) % 82.88/13.19 % (1808998)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.88/13.19 % (1808998)------------------------------ % 82.88/13.19 % (1808998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.88/13.19 % (1808998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.88/13.19 % (1808998)CaDiCaL version: 2.1.3 % 82.88/13.19 % (1808998)Termination reason: Unknown % 82.88/13.19 % (1808998)Termination phase: Saturation % 82.88/13.19 % (1808998)Time elapsed: 0.358 s % 82.88/13.19 % (1808998)Peak memory usage: 114 MB % 82.88/13.19 % (1808998)Instructions burned: 540 (million) % 82.88/13.19 % (1808999)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.88/13.19 % (1808999)------------------------------ % 82.88/13.19 % (1808999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.88/13.19 % (1808999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.88/13.19 % (1808999)CaDiCaL version: 2.1.3 % 82.88/13.19 % (1808999)Termination reason: Unknown % 82.88/13.19 % (1808999)Termination phase: Saturation % 82.88/13.19 % (1808999)Time elapsed: 0.357 s % 82.88/13.19 % (1808999)Peak memory usage: 114 MB % 82.88/13.19 % (1808999)Instructions burned: 540 (million) % 82.88/13.19 % (1809000)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.88/13.19 % (1809000)------------------------------ % 82.88/13.19 % (1809000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.88/13.19 % (1809000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.88/13.19 % (1809000)CaDiCaL version: 2.1.3 % 82.88/13.19 % (1809000)Termination reason: Unknown % 82.88/13.19 % (1809000)Termination phase: Saturation % 82.88/13.19 % (1809000)Time elapsed: 0.355 s % 82.88/13.19 % (1809000)Peak memory usage: 113 MB % 82.88/13.19 % (1809000)Instructions burned: 540 (million) % 82.88/13.19 % (1809001)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.88/13.19 % (1809001)------------------------------ % 82.88/13.19 % (1809001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.88/13.19 % (1809001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.88/13.19 % (1809001)CaDiCaL version: 2.1.3 % 82.88/13.19 % (1809001)Termination reason: Unknown % 97.41/15.29 % (1809001)Termination phase: Saturation % 97.41/15.29 % (1809001)Time elapsed: 0.357 s % 97.41/15.29 % (1809001)Peak memory usage: 113 MB % 97.41/15.29 % (1809001)Instructions burned: 541 (million) % 97.41/15.29 % (1809006)dis+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:prc=on:drc=off:sims=off:sp=const_frequency:sos=on:spb=non_intro:gs=on:updr=off:newcnf=on:random_seed=1652564510:i=4840:nm=4:av=off_2893 on theBenchmark for (2893ds/4840Mi) % 97.41/15.29 % (1809007)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=1474799294:cts=off:i=5002_2893 on theBenchmark for (2893ds/5002Mi) % 97.41/15.29 % (1809008)dis+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3150329865:i=30479:sd=3:ss=axioms_2893 on theBenchmark for (2893ds/30479Mi) % 97.41/15.29 % (1809009)lrs+1011_1_anc=none:ncem=casc2026/models/loop2.pt:sil=32000:tgt=full:npcc=on:fde=unused:sas=cadical:sp=const_frequency:spb=non_intro:lsd=10:lcm=predicate:rp=on:sac=on:newcnf=on:random_seed=272190836:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2892 on theBenchmark for (2892ds/11035Mi) % 97.41/15.29 % (1809009)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 97.41/15.29 % (1809006)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 97.41/15.29 % (1809006)------------------------------ % 97.41/15.29 % (1809006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.41/15.29 % (1809006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.41/15.29 % (1809006)CaDiCaL version: 2.1.3 % 97.41/15.29 % (1809006)Termination reason: Unknown % 97.41/15.29 % (1809006)Termination phase: Saturation % 97.41/15.29 % (1809006)Time elapsed: 0.356 s % 97.41/15.29 % (1809006)Peak memory usage: 113 MB % 97.41/15.29 % (1809006)Instructions burned: 540 (million) % 97.41/15.29 % (1809007)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 97.41/15.29 % (1809007)------------------------------ % 97.41/15.29 % (1809007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.41/15.29 % (1809007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.41/15.29 % (1809007)CaDiCaL version: 2.1.3 % 97.41/15.29 % (1809007)Termination reason: Unknown % 97.41/15.29 % (1809007)Termination phase: Saturation % 97.41/15.29 % (1809007)Time elapsed: 0.355 s % 97.41/15.29 % (1809007)Peak memory usage: 113 MB % 97.41/15.29 % (1809007)Instructions burned: 539 (million) % 97.41/15.29 % (1809008)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 97.41/15.29 % (1809008)------------------------------ % 97.41/15.29 % (1809008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.41/15.29 % (1809008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.41/15.29 % (1809008)CaDiCaL version: 2.1.3 % 97.41/15.29 % (1809008)Termination reason: Unknown % 97.41/15.29 % (1809008)Termination phase: Saturation % 97.41/15.29 % (1809008)Time elapsed: 0.355 s % 97.41/15.29 % (1809008)Peak memory usage: 113 MB % 97.41/15.29 % (1809008)Instructions burned: 540 (million) % 97.41/15.29 % (1809009)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 97.41/15.29 % (1809009)------------------------------ % 97.41/15.29 % (1809009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.41/15.29 % (1809009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.41/15.29 % (1809009)CaDiCaL version: 2.1.3 % 97.41/15.29 % (1809009)Termination reason: Unknown % 97.41/15.29 % (1809009)Termination phase: Saturation % 97.41/15.29 % (1809009)Time elapsed: 0.356 s % 97.41/15.29 % (1809009)Peak memory usage: 114 MB % 97.41/15.29 % (1809009)Instructions burned: 543 (million) % 97.41/15.29 % (1809014)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=2746017724:i=5835_2889 on theBenchmark for (2889ds/5835Mi) % 97.41/15.29 % (1809015)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=1194834376:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2888 on theBenchmark for (2888ds/5890Mi) % 97.41/15.29 % (1809016)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=1178472008:cts=off:i=19910:ep=RS_2888 on theBenchmark for (2888ds/19910Mi) % 97.41/15.29 % (1809017)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=arity:fd=preordered:s2agt=16:sac=on:random_seed=489495857:i=20312:bd=preordered:fsr=off:er=filter_2887 on theBenchmark for (2887ds/20312Mi) % 115.64/17.85 % (1809014)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 115.64/17.85 % (1809014)------------------------------ % 115.64/17.85 % (1809014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.64/17.85 % (1809014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.64/17.85 % (1809014)CaDiCaL version: 2.1.3 % 115.64/17.85 % (1809014)Termination reason: Unknown % 115.64/17.85 % (1809014)Termination phase: Saturation % 115.64/17.85 % (1809014)Time elapsed: 0.357 s % 115.64/17.85 % (1809014)Peak memory usage: 113 MB % 115.64/17.85 % (1809014)Instructions burned: 540 (million) % 115.64/17.85 % (1809015)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 115.64/17.85 % (1809015)------------------------------ % 115.64/17.85 % (1809015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.64/17.85 % (1809015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.64/17.85 % (1809015)CaDiCaL version: 2.1.3 % 115.64/17.85 % (1809015)Termination reason: Unknown % 115.64/17.85 % (1809015)Termination phase: Saturation % 115.64/17.85 % (1809015)Time elapsed: 0.354 s % 115.64/17.85 % (1809015)Peak memory usage: 114 MB % 115.64/17.85 % (1809015)Instructions burned: 540 (million) % 115.64/17.85 % (1809017)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 115.64/17.85 % (1809017)------------------------------ % 115.64/17.85 % (1809017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.64/17.85 % (1809017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.64/17.85 % (1809017)CaDiCaL version: 2.1.3 % 115.64/17.85 % (1809017)Termination reason: Unknown % 115.64/17.85 % (1809017)Termination phase: Saturation % 115.64/17.85 % (1809017)Time elapsed: 0.357 s % 115.64/17.85 % (1809017)Peak memory usage: 113 MB % 115.64/17.85 % (1809017)Instructions burned: 540 (million) % 115.64/17.85 % (1809022)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal_then_units:urr=on:gs=on:sac=on:random_seed=1940881654:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2884 on theBenchmark for (2884ds/13822Mi) % 115.64/17.85 % (1809023)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=1270086100:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2883 on theBenchmark for (2883ds/7144Mi) % 115.64/17.85 % (1809024)lrs+21_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=214023448:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2882 on theBenchmark for (2882ds/15184Mi) % 115.64/17.85 % (1809022)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 115.64/17.85 % (1809022)------------------------------ % 115.64/17.85 % (1809022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.64/17.85 % (1809022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.64/17.85 % (1809022)CaDiCaL version: 2.1.3 % 115.64/17.85 % (1809022)Termination reason: Unknown % 115.64/17.85 % (1809022)Termination phase: Saturation % 115.64/17.85 % (1809022)Time elapsed: 0.355 s % 115.64/17.85 % (1809022)Peak memory usage: 114 MB % 115.64/17.85 % (1809022)Instructions burned: 540 (million) % 115.64/17.85 % (1809024)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 115.64/17.85 % (1809024)------------------------------ % 115.64/17.85 % (1809024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.64/17.85 % (1809024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.64/17.85 % (1809024)CaDiCaL version: 2.1.3 % 115.64/17.85 % (1809024)Termination reason: Unknown % 115.64/17.85 % (1809024)Termination phase: Saturation % 115.64/17.85 % (1809024)Time elapsed: 0.354 s % 115.64/17.85 % (1809024)Peak memory usage: 114 MB % 115.64/17.85 % (1809024)Instructions burned: 540 (million) % 115.64/17.85 % (1809028)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=3903113759:i=107375_2879 on theBenchmark for (2879ds/107375Mi) % 115.64/17.85 % (1809029)dis+11_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=full:npcc=on:sp=const_frequency:spb=units:lcm=predicate:fd=off:sac=on:newcnf=on:random_seed=2960454393:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2878 on theBenchmark for (2878ds/7958Mi) % 125.50/19.14 % (1809028)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 125.50/19.14 % (1809028)------------------------------ % 125.50/19.14 % (1809028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.50/19.14 % (1809028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.50/19.14 % (1809028)CaDiCaL version: 2.1.3 % 125.50/19.14 % (1809028)Termination reason: Unknown % 125.50/19.14 % (1809028)Termination phase: Saturation % 125.50/19.14 % (1809028)Time elapsed: 0.357 s % 125.50/19.14 % (1809028)Peak memory usage: 113 MB % 125.50/19.14 % (1809028)Instructions burned: 541 (million) % 125.50/19.14 % (1809029)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 125.50/19.14 % (1809029)------------------------------ % 125.50/19.14 % (1809029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.50/19.14 % (1809029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.50/19.14 % (1809029)CaDiCaL version: 2.1.3 % 125.50/19.14 % (1809029)Termination reason: Unknown % 125.50/19.14 % (1809029)Termination phase: Saturation % 125.50/19.14 % (1809029)Time elapsed: 0.357 s % 125.50/19.14 % (1809029)Peak memory usage: 114 MB % 125.50/19.14 % (1809029)Instructions burned: 540 (million) % 125.50/19.14 % (1809032)dis+10_128_sil=16000:nwc=0.7:random_seed=3551308801:i=15999:nm=2:gsp=on_2874 on theBenchmark for (2874ds/15999Mi) % 125.50/19.14 % (1809032)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 125.50/19.14 % (1809034)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=3260124788:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2873 on theBenchmark for (2873ds/8139Mi) % 125.50/19.14 % (1808926)Instruction limit reached! % 125.50/19.14 % (1808926)------------------------------ % 125.50/19.14 % (1808926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.50/19.14 % (1808926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.50/19.14 % (1808926)CaDiCaL version: 2.1.3 % 125.50/19.14 % (1808926)Termination reason: Instruction limit % 125.50/19.14 % (1808926)Termination phase: Saturation % 125.50/19.14 % (1808926)Time elapsed: 7.370 s % 125.50/19.14 % (1808926)Peak memory usage: 383 MB % 125.50/19.14 % (1808926)Instructions burned: 26474 (million) % 125.50/19.14 % (1809036)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=2084759870:st=4:i=8950:sd=5:ss=axioms_2864 on theBenchmark for (2864ds/8950Mi) % 125.50/19.14 % (1809036)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 125.50/19.14 % (1809036)------------------------------ % 125.50/19.14 % (1809036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.50/19.14 % (1809036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.50/19.14 % (1809036)CaDiCaL version: 2.1.3 % 125.50/19.14 % (1809036)Termination reason: Unknown % 125.50/19.14 % (1809036)Termination phase: Saturation % 125.50/19.14 % (1809036)Time elapsed: 0.192 s % 125.50/19.14 % (1809036)Peak memory usage: 113 MB % 125.50/19.14 % (1809036)Instructions burned: 541 (million) % 125.50/19.14 % (1809038)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=2265711740:i=9809:ins=10:av=off_2861 on theBenchmark for (2861ds/9809Mi) % 125.50/19.14 % (1809038)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 125.50/19.14 % (1809038)------------------------------ % 125.50/19.14 % (1809038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.50/19.14 % (1809038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.50/19.14 % (1809038)CaDiCaL version: 2.1.3 % 125.50/19.14 % (1809038)Termination reason: Unknown % 125.50/19.14 % (1809038)Termination phase: Saturation % 125.50/19.14 % (1809038)Time elapsed: 0.192 s % 125.50/19.14 % (1809038)Peak memory usage: 114 MB % 125.50/19.14 % (1809038)Instructions burned: 540 (million) % 125.50/19.14 % (1809040)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=1887797958:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2858 on theBenchmark for (2858ds/9885Mi) % 125.50/19.14 % (1809040)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 125.50/19.14 % (1809040)------------------------------ % 125.50/19.14 % (1809040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.50/19.14 % (1809040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.14/22.68 % (1809040)CaDiCaL version: 2.1.3 % 150.14/22.68 % (1809040)Termination reason: Unknown % 150.14/22.68 % (1809040)Termination phase: Saturation % 150.14/22.68 % (1809040)Time elapsed: 0.193 s % 150.14/22.68 % (1809040)Peak memory usage: 114 MB % 150.14/22.68 % (1809040)Instructions burned: 540 (million) % 150.14/22.68 % (1809042)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=4225099526:cond=fast:i=32078:fgj=on:av=off_2855 on theBenchmark for (2855ds/32078Mi) % 150.14/22.68 % (1809042)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 150.14/22.68 % (1809042)------------------------------ % 150.14/22.68 % (1809042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.14/22.68 % (1809042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.14/22.68 % (1809042)CaDiCaL version: 2.1.3 % 150.14/22.68 % (1809042)Termination reason: Unknown % 150.14/22.68 % (1809042)Termination phase: Saturation % 150.14/22.68 % (1809042)Time elapsed: 0.192 s % 150.14/22.68 % (1809042)Peak memory usage: 114 MB % 150.14/22.68 % (1809042)Instructions burned: 540 (million) % 150.14/22.68 % (1809044)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=4210181958:i=11101:bd=all:ss=axioms:sgt=8_2852 on theBenchmark for (2852ds/11101Mi) % 150.14/22.68 % (1809023)Instruction limit reached! % 150.14/22.68 % (1809023)------------------------------ % 150.14/22.68 % (1809023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.14/22.68 % (1809023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.14/22.68 % (1809023)CaDiCaL version: 2.1.3 % 150.14/22.68 % (1809023)Termination reason: Instruction limit % 150.14/22.68 % (1809023)Termination phase: Saturation % 150.14/22.68 % (1809023)Time elapsed: 3.721 s % 150.14/22.68 % (1809023)Peak memory usage: 152 MB % 150.14/22.68 % (1809023)Instructions burned: 7144 (million) % 150.14/22.68 % (1809046)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=1316009045:cond=on:i=13220:s2at=3:aac=none:fsd=on_2844 on theBenchmark for (2844ds/13220Mi) % 150.14/22.68 % (1809046)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 150.14/22.68 % (1809046)------------------------------ % 150.14/22.68 % (1809046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.14/22.68 % (1809046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.14/22.68 % (1809046)CaDiCaL version: 2.1.3 % 150.14/22.68 % (1809046)Termination reason: Unknown % 150.14/22.68 % (1809046)Termination phase: Saturation % 150.14/22.68 % (1809046)Time elapsed: 0.356 s % 150.14/22.68 % (1809046)Peak memory usage: 114 MB % 150.14/22.68 % (1809046)Instructions burned: 541 (million) % 150.14/22.68 % (1809048)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=2408428186:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2840 on theBenchmark for (2840ds/13528Mi) % 150.14/22.68 % (1809048)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 150.14/22.68 % (1809048)------------------------------ % 150.14/22.68 % (1809048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.14/22.68 % (1809048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.14/22.68 % (1809048)CaDiCaL version: 2.1.3 % 150.14/22.68 % (1809048)Termination reason: Unknown % 150.14/22.68 % (1809048)Termination phase: Saturation % 150.14/22.68 % (1809048)Time elapsed: 0.356 s % 150.14/22.68 % (1809048)Peak memory usage: 113 MB % 150.14/22.68 % (1809048)Instructions burned: 543 (million) % 150.14/22.68 % (1809050)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:sp=reverse_frequency:bce=on:bsr=unit_only:s2agt=32:newcnf=on:random_seed=3474298663:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2835 on theBenchmark for (2835ds/14854Mi) % 150.14/22.68 % (1809050)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 150.14/22.68 % (1809050)------------------------------ % 150.14/22.68 % (1809050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 150.14/22.68 % (1809050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 150.14/22.68 % (1809050)CaDiCaL version: 2.1.3 % 150.14/22.68 % (1809050)Termination reason: Unknown % 150.14/22.68 % (1809050)Termination phase: Saturation % 150.14/22.68 % (1809050)Time elapsed: 0.362 s % 150.14/22.68 % (1809050)Peak memory usage: 113 MB % 150.14/22.68 % (1809050)Instructions burned: 549 (million) % 157.49/23.72 % (1809052)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=960171344:i=14974:ss=axioms:sgt=16_2830 on theBenchmark for (2830ds/14974Mi) % 157.49/23.72 % (1809034)Instruction limit reached! % 157.49/23.72 % (1809034)------------------------------ % 157.49/23.72 % (1809034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.49/23.72 % (1809034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/23.72 % (1809034)CaDiCaL version: 2.1.3 % 157.49/23.72 % (1809034)Termination reason: Instruction limit % 157.49/23.72 % (1809034)Termination phase: Saturation % 157.49/23.72 % (1809034)Time elapsed: 4.456 s % 157.49/23.72 % (1809034)Peak memory usage: 153 MB % 157.49/23.72 % (1809034)Instructions burned: 8139 (million) % 157.49/23.72 % (1809054)lrs-1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:sas=cadical:sp=arity:spb=units:lsd=1:acc=on:urr=ec_only:fd=preordered:gs=on:s2agt=16:random_seed=2929193272:i=33081:aac=none:fgj=on:bd=all:fsr=off_2827 on theBenchmark for (2827ds/33081Mi) % 157.49/23.72 % (1809052)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 157.49/23.72 % (1809052)------------------------------ % 157.49/23.72 % (1809052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.49/23.72 % (1809052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/23.72 % (1809052)CaDiCaL version: 2.1.3 % 157.49/23.72 % (1809052)Termination reason: Unknown % 157.49/23.72 % (1809052)Termination phase: Saturation % 157.49/23.72 % (1809052)Time elapsed: 0.358 s % 157.49/23.72 % (1809052)Peak memory usage: 113 MB % 157.49/23.72 % (1809052)Instructions burned: 541 (million) % 157.49/23.72 % (1809056)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sims=off:sas=cadical:etr=on:spb=goal:acc=on:s2agt=60:alpa=true:random_seed=599053852:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2825 on theBenchmark for (2825ds/50856Mi) % 157.49/23.72 % (1809054)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 157.49/23.72 % (1809054)------------------------------ % 157.49/23.72 % (1809054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.49/23.72 % (1809054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/23.72 % (1809054)CaDiCaL version: 2.1.3 % 157.49/23.72 % (1809054)Termination reason: Unknown % 157.49/23.72 % (1809054)Termination phase: Saturation % 157.49/23.72 % (1809054)Time elapsed: 0.359 s % 157.49/23.72 % (1809054)Peak memory usage: 114 MB % 157.49/23.72 % (1809054)Instructions burned: 540 (million) % 157.49/23.72 % (1809058)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=535933276:i=69865_2822 on theBenchmark for (2822ds/69865Mi) % 157.49/23.72 % (1809056)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 157.49/23.72 % (1809056)------------------------------ % 157.49/23.72 % (1809056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.49/23.72 % (1809056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/23.72 % (1809056)CaDiCaL version: 2.1.3 % 157.49/23.72 % (1809056)Termination reason: Unknown % 157.49/23.72 % (1809056)Termination phase: Saturation % 157.49/23.72 % (1809056)Time elapsed: 0.358 s % 157.49/23.72 % (1809056)Peak memory usage: 114 MB % 157.49/23.72 % (1809056)Instructions burned: 540 (million) % 157.49/23.72 % (1809044)Instruction limit reached! % 157.49/23.72 % (1809044)------------------------------ % 157.49/23.72 % (1809044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.49/23.72 % (1809044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.49/23.72 % (1809044)CaDiCaL version: 2.1.3 % 157.49/23.72 % (1809044)Termination reason: Instruction limit % 157.49/23.72 % (1809044)Termination phase: Saturation % 157.49/23.72 % (1809044)Time elapsed: 3.261 s % 157.49/23.72 % (1809044)Peak memory usage: 291 MB % 157.49/23.72 % (1809044)Instructions burned: 11102 (million) % 157.49/23.72 % (1809060)lrs+1002_1_anc=none:to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:sp=arity:sos=on:spb=intro:lcm=reverse:random_seed=4287464233:cond=fast:i=17802:gtgl=3:gtg=all_2820 on theBenchmark for (2820ds/17802Mi) % 157.49/23.72 % (1809061)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3523063060:i=96644_2818 on theBenchmark for (2818ds/96644Mi) % 157.49/23.72 % (1809058)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 157.49/23.72 % (1809058)------------------------------ % 174.56/26.12 % (1809058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.56/26.12 % (1809058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.56/26.12 % (1809058)CaDiCaL version: 2.1.3 % 174.56/26.12 % (1809058)Termination reason: Unknown % 174.56/26.12 % (1809058)Termination phase: Saturation % 174.56/26.12 % (1809058)Time elapsed: 0.358 s % 174.56/26.12 % (1809058)Peak memory usage: 113 MB % 174.56/26.12 % (1809058)Instructions burned: 540 (million) % 174.56/26.12 % (1809064)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 174.56/26.12 % (1809064)dis+1011_1_to=kbo:ncem=casc2026/models/loop8.pt:tgt=ground:irw=on:drc=off:sp=unary_first:bce=on:bsr=unit_only:kmz=on:sac=on:random_seed=3060538281:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2817 on theBenchmark for (2817ds/21161Mi) % 174.56/26.12 % (1809060)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 174.56/26.12 % (1809060)------------------------------ % 174.56/26.12 % (1809060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.56/26.12 % (1809060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.56/26.12 % (1809060)CaDiCaL version: 2.1.3 % 174.56/26.12 % (1809060)Termination reason: Unknown % 174.56/26.12 % (1809060)Termination phase: Saturation % 174.56/26.12 % (1809060)Time elapsed: 0.358 s % 174.56/26.12 % (1809060)Peak memory usage: 113 MB % 174.56/26.12 % (1809060)Instructions burned: 543 (million) % 174.56/26.12 % (1809066)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=2097113212:i=22761:gtg=all:ss=axioms:fsd=on_2815 on theBenchmark for (2815ds/22761Mi) % 174.56/26.12 % (1809066)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 174.56/26.12 % (1809066)------------------------------ % 174.56/26.12 % (1809066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.56/26.12 % (1809066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.56/26.12 % (1809066)CaDiCaL version: 2.1.3 % 174.56/26.12 % (1809066)Termination reason: Unknown % 174.56/26.12 % (1809066)Termination phase: Saturation % 174.56/26.12 % (1809066)Time elapsed: 0.354 s % 174.56/26.12 % (1809066)Peak memory usage: 113 MB % 174.56/26.12 % (1809066)Instructions burned: 541 (million) % 174.56/26.12 % (1809068)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=851265342:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2810 on theBenchmark for (2810ds/23713Mi) % 174.56/26.12 % (1809032)Instruction limit reached! % 174.56/26.12 % (1809032)------------------------------ % 174.56/26.12 % (1809032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.56/26.12 % (1809032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.56/26.12 % (1809032)CaDiCaL version: 2.1.3 % 174.56/26.12 % (1809032)Termination reason: Instruction limit % 174.56/26.12 % (1809032)Termination phase: Saturation % 174.56/26.12 % (1809032)Time elapsed: 7.735 s % 174.56/26.12 % (1809032)Peak memory usage: 202 MB % 174.56/26.12 % (1809032)Instructions burned: 16001 (million) % 174.56/26.12 % (1809070)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3991996632:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2795 on theBenchmark for (2795ds/26509Mi) % 174.56/26.12 % (1809070)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 174.56/26.12 % (1809070)------------------------------ % 174.56/26.12 % (1809070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.56/26.12 % (1809070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.56/26.12 % (1809070)CaDiCaL version: 2.1.3 % 174.56/26.12 % (1809070)Termination reason: Unknown % 174.56/26.12 % (1809070)Termination phase: Saturation % 174.56/26.12 % (1809070)Time elapsed: 0.354 s % 174.56/26.12 % (1809070)Peak memory usage: 113 MB % 174.56/26.12 % (1809070)Instructions burned: 540 (million) % 174.56/26.12 % (1809072)dis+1011_1_to=kbo:ncem=casc2026/models/loop6.pt:tgt=ground:drc=off:fde=unused:sp=const_frequency:spb=units:bsr=on:sac=on:random_seed=557289281:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2790 on theBenchmark for (2790ds/28957Mi) % 174.56/26.12 % (1808900)Instruction limit reached! % 174.56/26.12 % (1808900)------------------------------ % 174.56/26.12 % (1808900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.65/28.57 % (1808900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.65/28.57 % (1808900)CaDiCaL version: 2.1.3 % 191.65/28.57 % (1808900)Termination reason: Instruction limit % 191.65/28.57 % (1808900)Termination phase: Saturation % 191.65/28.57 % (1808900)Time elapsed: 18.123 s % 191.65/28.57 % (1808900)Peak memory usage: 350 MB % 191.65/28.57 % (1808900)Instructions burned: 33334 (million) % 191.65/28.57 % (1809016)Instruction limit reached! % 191.65/28.57 % (1809016)------------------------------ % 191.65/28.57 % (1809016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.65/28.57 % (1809016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.65/28.57 % (1809016)CaDiCaL version: 2.1.3 % 191.65/28.57 % (1809016)Termination reason: Instruction limit % 191.65/28.57 % (1809016)Termination phase: Saturation % 191.65/28.57 % (1809016)Time elapsed: 10.585 s % 191.65/28.57 % (1809016)Peak memory usage: 238 MB % 191.65/28.57 % (1809016)Instructions burned: 19912 (million) % 191.65/28.57 % (1809074)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:drc=off:sp=const_max:spb=goal_then_units:lcm=predicate:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=696347900:i=29246:s2at=-1:kws=inv_arity:ins=10_2781 on theBenchmark for (2781ds/29246Mi) % 191.65/28.57 % (1809075)ott+1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:sp=weighted_frequency:urr=on:gs=on:s2agt=32:sac=on:random_seed=1838196831:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2781 on theBenchmark for (2781ds/30082Mi) % 191.65/28.57 % (1809075)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 191.65/28.57 % (1809074)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 191.65/28.57 % (1809074)------------------------------ % 191.65/28.57 % (1809074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.65/28.57 % (1809074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.65/28.57 % (1809074)CaDiCaL version: 2.1.3 % 191.65/28.57 % (1809074)Termination reason: Unknown % 191.65/28.57 % (1809074)Termination phase: Saturation % 191.65/28.57 % (1809074)Time elapsed: 0.356 s % 191.65/28.57 % (1809074)Peak memory usage: 114 MB % 191.65/28.57 % (1809074)Instructions burned: 541 (million) % 191.65/28.57 % (1809075)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 191.65/28.57 % (1809075)------------------------------ % 191.65/28.57 % (1809075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.65/28.57 % (1809075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.65/28.57 % (1809075)CaDiCaL version: 2.1.3 % 191.65/28.57 % (1809075)Termination reason: Unknown % 191.65/28.57 % (1809075)Termination phase: Saturation % 191.65/28.57 % (1809075)Time elapsed: 0.360 s % 191.65/28.57 % (1809075)Peak memory usage: 114 MB % 191.65/28.57 % (1809075)Instructions burned: 544 (million) % 191.65/28.57 % (1809078)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=29350092:i=32262:bd=preordered_2776 on theBenchmark for (2776ds/32262Mi) % 191.65/28.57 % (1809079)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=2451430562:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2776 on theBenchmark for (2776ds/32870Mi) % 191.65/28.57 % (1809078)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 191.65/28.57 % (1809078)------------------------------ % 191.65/28.57 % (1809078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.65/28.57 % (1809078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.65/28.57 % (1809078)CaDiCaL version: 2.1.3 % 191.65/28.57 % (1809078)Termination reason: Unknown % 191.65/28.57 % (1809078)Termination phase: Saturation % 191.65/28.57 % (1809078)Time elapsed: 0.358 s % 191.65/28.57 % (1809078)Peak memory usage: 113 MB % 191.65/28.57 % (1809078)Instructions burned: 540 (million) % 191.65/28.57 % (1809079)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 191.65/28.57 % (1809079)------------------------------ % 191.65/28.57 % (1809079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 191.65/28.57 % (1809079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 191.65/28.57 % (1809079)CaDiCaL version: 2.1.3 % 191.65/28.57 % (1809079)Termination reason: Unknown % 191.65/28.57 % (1809079)Termination phase: Saturation % 191.65/28.57 % (1809079)Time elapsed: 0.356 s % 191.65/28.57 % (1809079)Peak memory usage: 113 MB % 202.92/30.13 % (1809079)Instructions burned: 541 (million) % 202.92/30.13 % (1809082)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:prc=on:sp=reverse_frequency:spb=goal:acc=on:kmz=on:random_seed=1760290637:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2771 on theBenchmark for (2771ds/33295Mi) % 202.92/30.13 % (1809083)dis+11_1_anc=none:sfv=off:to=kbo:ncem=casc2026/models/loop6.pt:lma=off:bsr=unit_only:s2agt=8:kmz=on:sac=on:random_seed=2050420268:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2771 on theBenchmark for (2771ds/36826Mi) % 202.92/30.13 % (1809082)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 202.92/30.13 % (1809082)------------------------------ % 202.92/30.13 % (1809082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.92/30.13 % (1809082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.92/30.13 % (1809082)CaDiCaL version: 2.1.3 % 202.92/30.13 % (1809082)Termination reason: Unknown % 202.92/30.13 % (1809082)Termination phase: Saturation % 202.92/30.13 % (1809082)Time elapsed: 0.355 s % 202.92/30.13 % (1809082)Peak memory usage: 114 MB % 202.92/30.13 % (1809082)Instructions burned: 540 (million) % 202.92/30.13 % (1809086)lrs-1003_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:spb=goal:bsr=unit_only:gs=on:br=off:flr=on:sac=on:random_seed=3018906371:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2766 on theBenchmark for (2766ds/92981Mi) % 202.92/30.13 % (1809086)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 202.92/30.13 % (1809086)------------------------------ % 202.92/30.13 % (1809086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.92/30.13 % (1809086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.92/30.13 % (1809086)CaDiCaL version: 2.1.3 % 202.92/30.13 % (1809086)Termination reason: Unknown % 202.92/30.13 % (1809086)Termination phase: Saturation % 202.92/30.13 % (1809086)Time elapsed: 0.357 s % 202.92/30.13 % (1809086)Peak memory usage: 113 MB % 202.92/30.13 % (1809086)Instructions burned: 540 (million) % 202.92/30.13 % (1809088)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=101161335:s2pl=on:i=49423_2762 on theBenchmark for (2762ds/49423Mi) % 202.92/30.13 % (1809088)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 202.92/30.13 % (1809088)------------------------------ % 202.92/30.13 % (1809088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.92/30.13 % (1809088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.92/30.13 % (1809088)CaDiCaL version: 2.1.3 % 202.92/30.13 % (1809088)Termination reason: Unknown % 202.92/30.13 % (1809088)Termination phase: Saturation % 202.92/30.13 % (1809088)Time elapsed: 0.355 s % 202.92/30.13 % (1809088)Peak memory usage: 113 MB % 202.92/30.13 % (1809088)Instructions burned: 541 (million) % 202.92/30.13 % (1809090)lrs+1002_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:tgt=ground:npcc=on:prc=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:rp=on:updr=off:sac=on:random_seed=3999386127:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2757 on theBenchmark for (2757ds/57299Mi) % 202.92/30.13 % (1809090)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 202.92/30.13 % (1809090)------------------------------ % 202.92/30.13 % (1809090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.92/30.13 % (1809090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.92/30.13 % (1809090)CaDiCaL version: 2.1.3 % 202.92/30.13 % (1809090)Termination reason: Unknown % 202.92/30.13 % (1809090)Termination phase: Saturation % 202.92/30.13 % (1809090)Time elapsed: 0.359 s % 202.92/30.13 % (1809090)Peak memory usage: 113 MB % 202.92/30.13 % (1809090)Instructions burned: 541 (million) % 202.92/30.13 % (1809092)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=9556592:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2752 on theBenchmark for (2752ds/127679Mi) % 202.92/30.13 % (1809092)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 202.92/30.13 % (1809092)------------------------------ % 202.92/30.13 % (1809092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.92/30.13 % (1809092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.68/31.17 % (1809092)CaDiCaL version: 2.1.3 % 210.68/31.17 % (1809092)Termination reason: Unknown % 210.68/31.17 % (1809092)Termination phase: Saturation % 210.68/31.17 % (1809092)Time elapsed: 0.356 s % 210.68/31.17 % (1809092)Peak memory usage: 114 MB % 210.68/31.17 % (1809092)Instructions burned: 540 (million) % 210.68/31.17 % (1809094)lrs+31_1_anc=all:to=lpo:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_arity:fs=off:lcm=predicate:alpa=false:flr=on:random_seed=1417492757:i=69402:add=on:aac=none:fsr=off_2747 on theBenchmark for (2747ds/69402Mi) % 210.68/31.17 % (1809094)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 210.68/31.17 % (1809094)------------------------------ % 210.68/31.17 % (1809094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.68/31.17 % (1809094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.68/31.17 % (1809094)CaDiCaL version: 2.1.3 % 210.68/31.17 % (1809094)Termination reason: Unknown % 210.68/31.17 % (1809094)Termination phase: Saturation % 210.68/31.17 % (1809094)Time elapsed: 0.356 s % 210.68/31.17 % (1809094)Peak memory usage: 113 MB % 210.68/31.17 % (1809094)Instructions burned: 540 (million) % 210.68/31.17 % (1809096)lrs-2_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:drc=off:sas=cadical:sp=reverse_frequency:lcm=predicate:acc=on:bsr=unit_only:fd=preordered:sac=on:random_seed=1971545760:i=100512:doe=on:fgj=on:bd=all:fsd=on_2742 on theBenchmark for (2742ds/100512Mi) % 210.68/31.17 % (1809096)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 210.68/31.17 % (1809096)------------------------------ % 210.68/31.17 % (1809096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.68/31.17 % (1809096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.68/31.17 % (1809096)CaDiCaL version: 2.1.3 % 210.68/31.17 % (1809096)Termination reason: Unknown % 210.68/31.17 % (1809096)Termination phase: Saturation % 210.68/31.17 % (1809096)Time elapsed: 0.355 s % 210.68/31.17 % (1809096)Peak memory usage: 113 MB % 210.68/31.17 % (1809096)Instructions burned: 539 (million) % 210.68/31.17 % (1809098)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=700454961:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2737 on theBenchmark for (2737ds/138761Mi) % 210.68/31.17 % (1809098)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 210.68/31.17 % (1809098)------------------------------ % 210.68/31.17 % (1809098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.68/31.17 % (1809098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.68/31.17 % (1809098)CaDiCaL version: 2.1.3 % 210.68/31.17 % (1809098)Termination reason: Unknown % 210.68/31.17 % (1809098)Termination phase: Saturation % 210.68/31.17 % (1809098)Time elapsed: 0.356 s % 210.68/31.17 % (1809098)Peak memory usage: 114 MB % 210.68/31.17 % (1809098)Instructions burned: 540 (million) % 210.68/31.17 % (1809100)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:si=on:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2604994725:i=282386:rtra=on_2732 on theBenchmark for (2732ds/282386Mi) % 210.68/31.17 % (1809100)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 210.68/31.17 % (1809100)------------------------------ % 210.68/31.17 % (1809100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.68/31.17 % (1809100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.68/31.17 % (1809100)CaDiCaL version: 2.1.3 % 210.68/31.17 % (1809100)Termination reason: Unknown % 210.68/31.17 % (1809100)Termination phase: Saturation % 210.68/31.17 % (1809100)Time elapsed: 0.359 s % 210.68/31.17 % (1809100)Peak memory usage: 114 MB % 210.68/31.17 % (1809100)Instructions burned: 540 (million) % 210.68/31.17 % (1809102)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:si=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4194048438:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2727 on theBenchmark for (2727ds/269354Mi) % 210.68/31.17 % (1809102)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 210.68/31.17 % (1809102)------------------------------ % 210.68/31.17 % (1809102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.68/31.17 % (1809102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.46/32.77 % (1809102)CaDiCaL version: 2.1.3 % 221.46/32.77 % (1809102)Termination reason: Unknown % 221.46/32.77 % (1809102)Termination phase: Saturation % 221.46/32.77 % (1809102)Time elapsed: 0.360 s % 221.46/32.77 % (1809102)Peak memory usage: 114 MB % 221.46/32.77 % (1809102)Instructions burned: 543 (million) % 221.46/32.77 % (1809104)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:si=on:sos=all:bsr=unit_only:sac=on:random_seed=556595446:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2722 on theBenchmark for (2722ds/283390Mi) % 221.46/32.77 % (1809104)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 221.46/32.77 % (1809104)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 221.46/32.77 % (1809104)------------------------------ % 221.46/32.77 % (1809104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.46/32.77 % (1809104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.46/32.77 % (1809104)CaDiCaL version: 2.1.3 % 221.46/32.77 % (1809104)Termination reason: Unknown % 221.46/32.77 % (1809104)Termination phase: Saturation % 221.46/32.77 % (1809104)Time elapsed: 0.355 s % 221.46/32.77 % (1809104)Peak memory usage: 114 MB % 221.46/32.77 % (1809104)Instructions burned: 541 (million) % 221.46/32.77 % (1809106)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2082051530:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2718 on theBenchmark for (2718ds/218Mi) % 221.46/32.77 % (1809106)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 221.46/32.77 % (1809106)Refutation not found, incomplete strategy % 221.46/32.77 % (1809106)------------------------------ % 221.46/32.77 % (1809106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.46/32.77 % (1809106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.46/32.77 % (1809106)CaDiCaL version: 2.1.3 % 221.46/32.77 % (1809106)Termination reason: Refutation not found, incomplete strategy % 221.46/32.77 % (1809106)Time elapsed: 0.016 s % 221.46/32.77 % (1809106)Peak memory usage: 89 MB % 221.46/32.77 % (1809106)Instructions burned: 27 (million) % 221.46/32.77 % (1809106)------------------------------ % 221.46/32.77 % (1809106)------------------------------ % 221.46/32.77 % (1809108)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=372822398:i=238:av=off:rtra=on:ss=axioms_2714 on theBenchmark for (2714ds/238Mi) % 221.46/32.77 % (1809108)Instruction limit reached! % 221.46/32.77 % (1809108)------------------------------ % 221.46/32.77 % (1809108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.46/32.77 % (1809108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.46/32.77 % (1809108)CaDiCaL version: 2.1.3 % 221.46/32.77 % (1809108)Termination reason: Instruction limit % 221.46/32.77 % (1809108)Termination phase: Saturation % 221.46/32.77 % (1809108)Time elapsed: 0.124 s % 221.46/32.77 % (1809108)Peak memory usage: 90 MB % 221.46/32.77 % (1809108)Instructions burned: 240 (million) % 221.46/32.77 % (1809110)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=452338384:s2a=on:i=278:rtra=on:gtg=position_2711 on theBenchmark for (2711ds/278Mi) % 221.46/32.77 % (1809110)Instruction limit reached! % 221.46/32.77 % (1809110)------------------------------ % 221.46/32.77 % (1809110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.46/32.77 % (1809110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.46/32.77 % (1809110)CaDiCaL version: 2.1.3 % 221.46/32.77 % (1809110)Termination reason: Instruction limit % 221.46/32.77 % (1809110)Termination phase: Saturation % 221.46/32.77 % (1809110)Time elapsed: 0.167 s % 221.46/32.77 % (1809110)Peak memory usage: 91 MB % 221.46/32.77 % (1809110)Instructions burned: 280 (million) % 221.46/32.77 % (1809064)Instruction limit reached! % 221.46/32.77 % (1809064)------------------------------ % 221.46/32.77 % (1809064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.46/32.77 % (1809064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.46/32.77 % (1809064)CaDiCaL version: 2.1.3 % 221.46/32.77 % (1809064)Termination reason: Instruction limit % 221.46/32.77 % (1809064)Termination phase: Saturation % 221.46/32.77 % (1809064)Time elapsed: 10.794 s % 221.46/32.77 % (1809064)Peak memory usage: 280 MB % 221.46/32.77 % (1809064)Instructions burned: 21163 (million) % 221.46/32.77 % (1809112)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=94195654:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2708 on theBenchmark for (2708ds/258Mi) % 228.01/33.69 % (1809113)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1506422246:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2707 on theBenchmark for (2707ds/570Mi) % 228.01/33.69 % (1809112)Instruction limit reached! % 228.01/33.69 % (1809112)------------------------------ % 228.01/33.69 % (1809112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.01/33.69 % (1809112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.01/33.69 % (1809112)CaDiCaL version: 2.1.3 % 228.01/33.69 % (1809112)Termination reason: Instruction limit % 228.01/33.69 % (1809112)Termination phase: Saturation % 228.01/33.69 % (1809112)Time elapsed: 0.142 s % 228.01/33.69 % (1809112)Peak memory usage: 91 MB % 228.01/33.69 % (1809112)Instructions burned: 259 (million) % 228.01/33.69 % (1809116)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=2070555569:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2705 on theBenchmark for (2705ds/314Mi) % 228.01/33.69 % (1809113)Instruction limit reached! % 228.01/33.69 % (1809113)------------------------------ % 228.01/33.69 % (1809113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.01/33.69 % (1809113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.01/33.69 % (1809113)CaDiCaL version: 2.1.3 % 228.01/33.69 % (1809113)Termination reason: Instruction limit % 228.01/33.69 % (1809113)Termination phase: Saturation % 228.01/33.69 % (1809113)Time elapsed: 0.328 s % 228.01/33.69 % (1809113)Peak memory usage: 95 MB % 228.01/33.69 % (1809113)Instructions burned: 570 (million) % 228.01/33.69 % (1809116)Instruction limit reached! % 228.01/33.69 % (1809116)------------------------------ % 228.01/33.69 % (1809116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.01/33.69 % (1809116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.01/33.69 % (1809116)CaDiCaL version: 2.1.3 % 228.01/33.69 % (1809116)Termination reason: Instruction limit % 228.01/33.69 % (1809116)Termination phase: Saturation % 228.01/33.69 % (1809116)Time elapsed: 0.174 s % 228.01/33.69 % (1809116)Peak memory usage: 92 MB % 228.01/33.69 % (1809116)Instructions burned: 315 (million) % 228.01/33.69 % (1809118)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1525205603:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2703 on theBenchmark for (2703ds/650Mi) % 228.01/33.69 % (1809119)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:si=on:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3803120411:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2702 on theBenchmark for (2702ds/496Mi) % 228.01/33.69 % (1809119)Instruction limit reached! % 228.01/33.69 % (1809119)------------------------------ % 228.01/33.69 % (1809119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.01/33.69 % (1809119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.01/33.69 % (1809119)CaDiCaL version: 2.1.3 % 228.01/33.69 % (1809119)Termination reason: Instruction limit % 228.01/33.69 % (1809119)Termination phase: Saturation % 228.01/33.69 % (1809119)Time elapsed: 0.289 s % 228.01/33.69 % (1809119)Peak memory usage: 93 MB % 228.01/33.69 % (1809119)Instructions burned: 496 (million) % 228.01/33.69 % (1809118)Instruction limit reached! % 228.01/33.69 % (1809118)------------------------------ % 228.01/33.69 % (1809118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.01/33.69 % (1809118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.01/33.69 % (1809118)CaDiCaL version: 2.1.3 % 228.01/33.69 % (1809118)Termination reason: Instruction limit % 228.01/33.69 % (1809118)Termination phase: Saturation % 228.01/33.69 % (1809118)Time elapsed: 0.377 s % 228.01/33.69 % (1809118)Peak memory usage: 95 MB % 228.01/33.69 % (1809118)Instructions burned: 650 (million) % 228.01/33.69 % (1809122)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=3643613910:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2698 on theBenchmark for (2698ds/588Mi) % 228.01/33.69 % (1809122)Refutation not found, incomplete strategy % 228.01/33.69 % (1809122)------------------------------ % 228.01/33.69 % (1809122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.01/33.69 % (1809122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.01/33.69 % (1809122)CaDiCaL version: 2.1.3 % 228.01/33.69 % (1809122)Termination reason: Refutation not found, incomplete strategy % 228.01/33.69 % (1809122)Time elapsed: 0.006 s % 228.01/33.69 % (1809122)Peak memory usage: 88 MB % 228.01/33.69 % (1809122)Instructions burned: 9 (million) % 228.01/33.69 % (1809123)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=422457835:i=4700:rtra=on_2698 on theBenchmark for (2698ds/4700Mi) % 233.21/34.33 % (1809122)------------------------------ % 233.21/34.33 % (1809122)------------------------------ % 233.21/34.33 % (1809126)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2935302236:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2695 on theBenchmark for (2695ds/226Mi) % 233.21/34.33 % (1809123)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 233.21/34.33 % (1809123)------------------------------ % 233.21/34.33 % (1809123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.21/34.33 % (1809123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.21/34.33 % (1809123)CaDiCaL version: 2.1.3 % 233.21/34.33 % (1809123)Termination reason: Unknown % 233.21/34.33 % (1809123)Termination phase: Saturation % 233.21/34.33 % (1809123)Time elapsed: 0.361 s % 233.21/34.33 % (1809123)Peak memory usage: 114 MB % 233.21/34.33 % (1809123)Instructions burned: 541 (million) % 233.21/34.33 % (1809126)Instruction limit reached! % 233.21/34.33 % (1809126)------------------------------ % 233.21/34.33 % (1809126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.21/34.33 % (1809126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.21/34.33 % (1809126)CaDiCaL version: 2.1.3 % 233.21/34.33 % (1809126)Termination reason: Instruction limit % 233.21/34.33 % (1809126)Termination phase: Saturation % 233.21/34.33 % (1809126)Time elapsed: 0.140 s % 233.21/34.33 % (1809126)Peak memory usage: 90 MB % 233.21/34.33 % (1809126)Instructions burned: 227 (million) % 233.21/34.33 % (1809128)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=254499110:i=254:av=off:fsr=off:rtra=on:sup=off_2693 on theBenchmark for (2693ds/254Mi) % 233.21/34.33 % (1809128)Instruction limit reached! % 233.21/34.33 % (1809128)------------------------------ % 233.21/34.33 % (1809128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.21/34.33 % (1809128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.21/34.33 % (1809128)CaDiCaL version: 2.1.3 % 233.21/34.33 % (1809128)Termination reason: Instruction limit % 233.21/34.33 % (1809128)Termination phase: Saturation % 233.21/34.33 % (1809128)Time elapsed: 0.105 s % 233.21/34.33 % (1809128)Peak memory usage: 88 MB % 233.21/34.33 % (1809128)Instructions burned: 255 (million) % 233.21/34.33 % (1809129)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=3375364938:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2692 on theBenchmark for (2692ds/228Mi) % 233.21/34.33 % (1809129)Instruction limit reached! % 233.21/34.33 % (1809129)------------------------------ % 233.21/34.33 % (1809129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.21/34.33 % (1809129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.21/34.33 % (1809129)CaDiCaL version: 2.1.3 % 233.21/34.33 % (1809129)Termination reason: Instruction limit % 233.21/34.33 % (1809129)Termination phase: Saturation % 233.21/34.33 % (1809129)Time elapsed: 0.105 s % 233.21/34.33 % (1809129)Peak memory usage: 89 MB % 233.21/34.33 % (1809129)Instructions burned: 228 (million) % 233.21/34.33 % (1809131)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3476469393:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2690 on theBenchmark for (2690ds/1814Mi) % 233.21/34.33 % (1809133)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=2007045866:i=874:sd=1:aac=none:rtra=on:ss=included_2689 on theBenchmark for (2689ds/874Mi) % 233.21/34.33 % (1809133)Refutation not found, incomplete strategy % 233.21/34.33 % (1809133)------------------------------ % 233.21/34.33 % (1809133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.21/34.33 % (1809133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.21/34.33 % (1809133)CaDiCaL version: 2.1.3 % 233.21/34.33 % (1809133)Termination reason: Refutation not found, incomplete strategy % 233.21/34.33 % (1809133)Time elapsed: 0.006 s % 233.21/34.33 % (1809133)Peak memory usage: 88 MB % 233.21/34.33 % (1809133)Instructions burned: 8 (million) % 233.21/34.33 % (1809133)------------------------------ % 233.21/34.33 % (1809133)------------------------------ % 233.21/34.33 % (1809136)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=2273516588:i=10404:rtra=on:ss=axioms:sgt=16_2685 on theBenchmark for (2685ds/10404Mi) % 233.21/34.33 % (1809136)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 233.21/34.33 % (1809136)------------------------------ % 233.21/34.33 % (1809136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.71/35.02 % (1809136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.71/35.02 % (1809136)CaDiCaL version: 2.1.3 % 236.71/35.02 % (1809136)Termination reason: Unknown % 236.71/35.02 % (1809136)Termination phase: Saturation % 236.71/35.02 % (1809136)Time elapsed: 0.359 s % 236.71/35.02 % (1809136)Peak memory usage: 114 MB % 236.71/35.02 % (1809136)Instructions burned: 543 (million) % 236.71/35.02 % (1809138)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3801538561:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2680 on theBenchmark for (2680ds/268Mi) % 236.71/35.02 % (1809131)Instruction limit reached! % 236.71/35.02 % (1809131)------------------------------ % 236.71/35.02 % (1809131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.71/35.02 % (1809131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.71/35.02 % (1809131)CaDiCaL version: 2.1.3 % 236.71/35.02 % (1809131)Termination reason: Instruction limit % 236.71/35.02 % (1809131)Termination phase: Saturation % 236.71/35.02 % (1809131)Time elapsed: 1.055 s % 236.71/35.02 % (1809131)Peak memory usage: 109 MB % 236.71/35.02 % (1809131)Instructions burned: 1815 (million) % 236.71/35.02 % (1809138)Instruction limit reached! % 236.71/35.02 % (1809138)------------------------------ % 236.71/35.02 % (1809138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.71/35.02 % (1809138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.71/35.02 % (1809138)CaDiCaL version: 2.1.3 % 236.71/35.02 % (1809138)Termination reason: Instruction limit % 236.71/35.02 % (1809138)Termination phase: Saturation % 236.71/35.02 % (1809138)Time elapsed: 0.159 s % 236.71/35.02 % (1809138)Peak memory usage: 91 MB % 236.71/35.02 % (1809138)Instructions burned: 268 (million) % 236.71/35.02 % (1809140)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=3792454908:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2679 on theBenchmark for (2679ds/1184Mi) % 236.71/35.02 % (1809140)Refutation not found, incomplete strategy % 236.71/35.02 % (1809140)------------------------------ % 236.71/35.02 % (1809140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.71/35.02 % (1809140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.71/35.02 % (1809140)CaDiCaL version: 2.1.3 % 236.71/35.02 % (1809140)Termination reason: Refutation not found, incomplete strategy % 236.71/35.02 % (1809140)Time elapsed: 0.005 s % 236.71/35.02 % (1809140)Peak memory usage: 88 MB % 236.71/35.02 % (1809140)Instructions burned: 9 (million) % 236.71/35.02 % (1809141)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=2153874585:st=3:i=26386:sd=3:rtra=on:ss=axioms_2677 on theBenchmark for (2677ds/26386Mi) % 236.71/35.02 % (1809140)------------------------------ % 236.71/35.02 % (1809140)------------------------------ % 236.71/35.02 % (1809144)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:si=on:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=908315659:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2675 on theBenchmark for (2675ds/250Mi) % 236.71/35.02 % (1809144)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 236.71/35.02 % (1809141)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 236.71/35.02 % (1809141)------------------------------ % 236.71/35.02 % (1809141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.71/35.02 % (1809141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.71/35.02 % (1809141)CaDiCaL version: 2.1.3 % 236.71/35.02 % (1809141)Termination reason: Unknown % 236.71/35.02 % (1809141)Termination phase: Saturation % 236.71/35.02 % (1809141)Time elapsed: 0.359 s % 236.71/35.02 % (1809141)Peak memory usage: 114 MB % 236.71/35.02 % (1809141)Instructions burned: 541 (million) % 236.71/35.02 % (1809144)Instruction limit reached! % 236.71/35.02 % (1809144)------------------------------ % 236.71/35.02 % (1809144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.71/35.02 % (1809144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.71/35.02 % (1809144)CaDiCaL version: 2.1.3 % 236.71/35.02 % (1809144)Termination reason: Instruction limit % 236.71/35.02 % (1809144)Termination phase: Saturation % 236.71/35.02 % (1809144)Time elapsed: 0.142 s % 236.71/35.02 % (1809144)Peak memory usage: 91 MB % 236.71/35.02 % (1809144)Instructions burned: 250 (million) % 236.71/35.02 % (1809146)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3565048918:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2673 on theBenchmark for (2673ds/268Mi) % 243.04/36.02 % (1809068)Instruction limit reached! % 243.04/36.02 % (1809068)------------------------------ % 243.04/36.02 % (1809068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.04/36.02 % (1809068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/36.02 % (1809068)CaDiCaL version: 2.1.3 % 243.04/36.02 % (1809068)Termination reason: Instruction limit % 243.04/36.02 % (1809068)Termination phase: Saturation % 243.04/36.02 % (1809068)Time elapsed: 13.770 s % 243.04/36.02 % (1809068)Peak memory usage: 125 MB % 243.04/36.02 % (1809068)Instructions burned: 23714 (million) % 243.04/36.02 % (1809147)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3688296404:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2672 on theBenchmark for (2672ds/282Mi) % 243.04/36.02 % (1809147)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 243.04/36.02 % (1809147)Refutation not found, incomplete strategy % 243.04/36.02 % (1809147)------------------------------ % 243.04/36.02 % (1809147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.04/36.02 % (1809147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/36.02 % (1809147)CaDiCaL version: 2.1.3 % 243.04/36.02 % (1809147)Termination reason: Refutation not found, incomplete strategy % 243.04/36.02 % (1809147)Time elapsed: 0.002 s % 243.04/36.02 % (1809147)Peak memory usage: 88 MB % 243.04/36.02 % (1809147)Instructions burned: 3 (million) % 243.04/36.02 % (1809146)Instruction limit reached! % 243.04/36.02 % (1809146)------------------------------ % 243.04/36.02 % (1809146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.04/36.02 % (1809146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/36.02 % (1809146)CaDiCaL version: 2.1.3 % 243.04/36.02 % (1809146)Termination reason: Instruction limit % 243.04/36.02 % (1809146)Termination phase: Saturation % 243.04/36.02 % (1809146)Time elapsed: 0.148 s % 243.04/36.02 % (1809146)Peak memory usage: 91 MB % 243.04/36.02 % (1809146)Instructions burned: 268 (million) % 243.04/36.02 % (1809150)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=1802522686:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2671 on theBenchmark for (2671ds/862Mi) % 243.04/36.02 % (1809151)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:si=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=870165128:i=12120:aac=none:ins=25:rtra=on_2670 on theBenchmark for (2670ds/12120Mi) % 243.04/36.02 % (1809147)------------------------------ % 243.04/36.02 % (1809147)------------------------------ % 243.04/36.02 % (1809154)lrs+10_16_anc=all:slsqr=32,1:sil=8000:si=on: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=4035136624:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2668 on theBenchmark for (2668ds/300Mi) % 243.04/36.02 % (1809154)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 243.04/36.02 % (1809150)Instruction limit reached! % 243.04/36.02 % (1809150)------------------------------ % 243.04/36.02 % (1809150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.04/36.02 % (1809150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/36.02 % (1809150)CaDiCaL version: 2.1.3 % 243.04/36.02 % (1809150)Termination reason: Instruction limit % 243.04/36.02 % (1809150)Termination phase: Saturation % 243.04/36.02 % (1809150)Time elapsed: 0.408 s % 243.04/36.02 % (1809150)Peak memory usage: 95 MB % 243.04/36.02 % (1809150)Instructions burned: 863 (million) % 243.04/36.02 % (1809154)Instruction limit reached! % 243.04/36.02 % (1809154)------------------------------ % 243.04/36.02 % (1809154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.04/36.02 % (1809154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.04/36.02 % (1809154)CaDiCaL version: 2.1.3 % 243.04/36.02 % (1809154)Termination reason: Instruction limit % 243.04/36.02 % (1809154)Termination phase: Saturation % 243.04/36.02 % (1809154)Time elapsed: 0.194 s % 243.04/36.02 % (1809154)Peak memory usage: 93 MB % 243.04/36.02 % (1809154)Instructions burned: 301 (million) % 243.04/36.02 % (1809151)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 243.04/36.02 % (1809151)------------------------------ % 243.04/36.02 % (1809151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.37/36.88 % (1809151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.37/36.88 % (1809151)CaDiCaL version: 2.1.3 % 250.37/36.88 % (1809151)Termination reason: Unknown % 250.37/36.88 % (1809151)Termination phase: Saturation % 250.37/36.88 % (1809151)Time elapsed: 0.365 s % 250.37/36.88 % (1809151)Peak memory usage: 114 MB % 250.37/36.88 % (1809151)Instructions burned: 540 (million) % 250.37/36.88 % (1809156)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=1947390500:i=28310:bd=all:rtra=on_2665 on theBenchmark for (2665ds/28310Mi) % 250.37/36.88 % (1809157)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3407348153:i=1334:av=off:fsr=off:rtra=on_2665 on theBenchmark for (2665ds/1334Mi) % 250.37/36.88 % (1809157)Refutation not found, incomplete strategy % 250.37/36.88 % (1809157)------------------------------ % 250.37/36.88 % (1809157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.37/36.88 % (1809157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.37/36.88 % (1809157)CaDiCaL version: 2.1.3 % 250.37/36.88 % (1809157)Termination reason: Refutation not found, incomplete strategy % 250.37/36.88 % (1809157)Time elapsed: 0.005 s % 250.37/36.88 % (1809157)Peak memory usage: 89 MB % 250.37/36.88 % (1809157)Instructions burned: 7 (million) % 250.37/36.88 % (1809158)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:si=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1938561102:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2665 on theBenchmark for (2665ds/370Mi) % 250.37/36.88 % (1808992)Instruction limit reached! % 250.37/36.88 % (1808992)------------------------------ % 250.37/36.88 % (1808992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.37/36.88 % (1808992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.37/36.88 % (1808992)CaDiCaL version: 2.1.3 % 250.37/36.88 % (1808992)Termination reason: Instruction limit % 250.37/36.88 % (1808992)Termination phase: Saturation % 250.37/36.88 % (1808992)Time elapsed: 23.945 s % 250.37/36.88 % (1808992)Peak memory usage: 314 MB % 250.37/36.88 % (1808992)Instructions burned: 43698 (million) % 250.37/36.88 % (1809158)Instruction limit reached! % 250.37/36.88 % (1809158)------------------------------ % 250.37/36.88 % (1809158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.37/36.88 % (1809158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.37/36.88 % (1809158)CaDiCaL version: 2.1.3 % 250.37/36.88 % (1809158)Termination reason: Instruction limit % 250.37/36.88 % (1809158)Termination phase: Saturation % 250.37/36.88 % (1809158)Time elapsed: 0.210 s % 250.37/36.88 % (1809158)Peak memory usage: 92 MB % 250.37/36.88 % (1809158)Instructions burned: 371 (million) % 250.37/36.88 % (1809157)------------------------------ % 250.37/36.88 % (1809157)------------------------------ % 250.37/36.88 % (1809156)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 250.37/36.88 % (1809156)------------------------------ % 250.37/36.88 % (1809156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.37/36.88 % (1809156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.37/36.88 % (1809156)CaDiCaL version: 2.1.3 % 250.37/36.88 % (1809156)Termination reason: Unknown % 250.37/36.88 % (1809156)Termination phase: Saturation % 250.37/36.88 % (1809156)Time elapsed: 0.361 s % 250.37/36.88 % (1809156)Peak memory usage: 114 MB % 250.37/36.88 % (1809156)Instructions burned: 541 (million) % 250.37/36.88 % (1809163)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=571357778:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2661 on theBenchmark for (2661ds/9700Mi) % 250.37/36.88 % (1809162)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=687485533:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2661 on theBenchmark for (2661ds/386Mi) % 250.37/36.88 % (1809164)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:random_seed=1548681386:i=24222:sd=1:rtra=on:ss=included_2661 on theBenchmark for (2661ds/24222Mi) % 250.37/36.88 % (1809165)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=2674525282:i=638:kws=precedence:fsr=off:rtra=on_2661 on theBenchmark for (2661ds/638Mi) % 250.37/36.88 % (1809162)Instruction limit reached! % 250.37/36.88 % (1809162)------------------------------ % 250.37/36.88 % (1809162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.34/38.37 % (1809162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.34/38.37 % (1809162)CaDiCaL version: 2.1.3 % 261.34/38.37 % (1809162)Termination reason: Instruction limit % 261.34/38.37 % (1809162)Termination phase: Saturation % 261.34/38.37 % (1809162)Time elapsed: 0.217 s % 261.34/38.37 % (1809162)Peak memory usage: 95 MB % 261.34/38.37 % (1809162)Instructions burned: 388 (million) % 261.34/38.37 % (1809170)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1883045572:i=4128:ep=RST:rtra=on_2658 on theBenchmark for (2658ds/4128Mi) % 261.34/38.37 % (1809170)Refutation not found, incomplete strategy % 261.34/38.37 % (1809170)------------------------------ % 261.34/38.37 % (1809170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.34/38.37 % (1809170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.34/38.37 % (1809170)CaDiCaL version: 2.1.3 % 261.34/38.37 % (1809170)Termination reason: Refutation not found, incomplete strategy % 261.34/38.37 % (1809170)Time elapsed: 0.005 s % 261.34/38.37 % (1809170)Peak memory usage: 88 MB % 261.34/38.37 % (1809170)Instructions burned: 8 (million) % 261.34/38.37 % (1809164)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 261.34/38.37 % (1809164)------------------------------ % 261.34/38.37 % (1809164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.34/38.37 % (1809164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.34/38.37 % (1809164)CaDiCaL version: 2.1.3 % 261.34/38.37 % (1809164)Termination reason: Unknown % 261.34/38.37 % (1809164)Termination phase: Saturation % 261.34/38.37 % (1809164)Time elapsed: 0.358 s % 261.34/38.37 % (1809164)Peak memory usage: 114 MB % 261.34/38.37 % (1809164)Instructions burned: 541 (million) % 261.34/38.37 % (1809165)Instruction limit reached! % 261.34/38.37 % (1809165)------------------------------ % 261.34/38.37 % (1809165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.34/38.37 % (1809165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.34/38.37 % (1809165)CaDiCaL version: 2.1.3 % 261.34/38.37 % (1809165)Termination reason: Instruction limit % 261.34/38.37 % (1809165)Termination phase: Saturation % 261.34/38.37 % (1809165)Time elapsed: 0.314 s % 261.34/38.37 % (1809165)Peak memory usage: 96 MB % 261.34/38.37 % (1809165)Instructions burned: 641 (million) % 261.34/38.37 % (1809172)dis-1011_128_sil=32000:si=on:random_seed=277860590:i=7412:ep=RST:av=off:rtra=on_2656 on theBenchmark for (2656ds/7412Mi) % 261.34/38.37 % (1809173)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=608855848:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2656 on theBenchmark for (2656ds/1514Mi) % 261.34/38.37 % (1809173)Refutation not found, incomplete strategy % 261.34/38.37 % (1809173)------------------------------ % 261.34/38.37 % (1809173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.34/38.37 % (1809173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.34/38.37 % (1809173)CaDiCaL version: 2.1.3 % 261.34/38.37 % (1809173)Termination reason: Refutation not found, incomplete strategy % 261.34/38.37 % (1809173)Time elapsed: 0.005 s % 261.34/38.37 % (1809173)Peak memory usage: 89 MB % 261.34/38.37 % (1809173)Instructions burned: 7 (million) % 261.34/38.37 % (1809170)------------------------------ % 261.34/38.37 % (1809170)------------------------------ % 261.34/38.37 % (1809176)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=2297341565:i=27826:rtra=on:ss=axioms:sgt=8_2654 on theBenchmark for (2654ds/27826Mi) % 261.34/38.37 % (1809173)------------------------------ % 261.34/38.37 % (1809173)------------------------------ % 261.34/38.37 % (1809178)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=1895524023:i=19850:aac=none:rtra=on_2652 on theBenchmark for (2652ds/19850Mi) % 261.34/38.37 % (1809176)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 261.34/38.37 % (1809176)------------------------------ % 261.34/38.37 % (1809176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.34/38.37 % (1809176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.34/38.37 % (1809176)CaDiCaL version: 2.1.3 % 261.34/38.37 % (1809176)Termination reason: Unknown % 261.34/38.37 % (1809176)Termination phase: Saturation % 261.34/38.37 % (1809176)Time elapsed: 0.358 s % 261.34/38.37 % (1809176)Peak memory usage: 114 MB % 261.34/38.37 % (1809176)Instructions burned: 539 (million) % 261.34/38.37 % (1809180)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=667484084:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2649 on theBenchmark for (2649ds/4958Mi) % 269.30/39.51 % (1809180)Refutation not found, incomplete strategy % 269.30/39.51 % (1809180)------------------------------ % 269.30/39.51 % (1809180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.30/39.51 % (1809180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.30/39.51 % (1809180)CaDiCaL version: 2.1.3 % 269.30/39.51 % (1809180)Termination reason: Refutation not found, incomplete strategy % 269.30/39.51 % (1809180)Time elapsed: 0.005 s % 269.30/39.51 % (1809180)Peak memory usage: 89 MB % 269.30/39.51 % (1809180)Instructions burned: 6 (million) % 269.30/39.51 % (1809178)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 269.30/39.51 % (1809178)------------------------------ % 269.30/39.51 % (1809178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.30/39.51 % (1809178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.30/39.51 % (1809178)CaDiCaL version: 2.1.3 % 269.30/39.51 % (1809178)Termination reason: Unknown % 269.30/39.51 % (1809178)Termination phase: Saturation % 269.30/39.51 % (1809178)Time elapsed: 0.359 s % 269.30/39.51 % (1809178)Peak memory usage: 114 MB % 269.30/39.51 % (1809178)Instructions burned: 540 (million) % 269.30/39.51 % (1809182)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=99788280:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2648 on theBenchmark for (2648ds/880Mi) % 269.30/39.51 % (1809182)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 269.30/39.51 % (1809180)------------------------------ % 269.30/39.51 % (1809180)------------------------------ % 269.30/39.51 % (1809072)Instruction limit reached! % 269.30/39.51 % (1809072)------------------------------ % 269.30/39.51 % (1809072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.30/39.51 % (1809072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.30/39.51 % (1809072)CaDiCaL version: 2.1.3 % 269.30/39.51 % (1809072)Termination reason: Instruction limit % 269.30/39.51 % (1809072)Termination phase: Saturation % 269.30/39.51 % (1809072)Time elapsed: 14.441 s % 269.30/39.51 % (1809072)Peak memory usage: 320 MB % 269.30/39.51 % (1809072)Instructions burned: 28957 (million) % 269.30/39.51 % (1809184)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:si=on:erd=off:lsd=100:bsr=unit_only:random_seed=3495174120:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2645 on theBenchmark for (2645ds/22290Mi) % 269.30/39.51 % (1809185)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2412350303:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2644 on theBenchmark for (2644ds/6068Mi) % 269.30/39.51 % (1809182)Instruction limit reached! % 269.30/39.51 % (1809182)------------------------------ % 269.30/39.51 % (1809182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.30/39.51 % (1809182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.30/39.51 % (1809182)CaDiCaL version: 2.1.3 % 269.30/39.51 % (1809182)Termination reason: Instruction limit % 269.30/39.51 % (1809182)Termination phase: Saturation % 269.30/39.51 % (1809182)Time elapsed: 0.437 s % 269.30/39.51 % (1809182)Peak memory usage: 96 MB % 269.30/39.51 % (1809182)Instructions burned: 881 (million) % 269.30/39.51 % (1809184)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 269.30/39.51 % (1809184)------------------------------ % 269.30/39.51 % (1809184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.30/39.51 % (1809184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.30/39.51 % (1809184)CaDiCaL version: 2.1.3 % 269.30/39.51 % (1809184)Termination reason: Unknown % 269.30/39.51 % (1809184)Termination phase: Saturation % 269.30/39.51 % (1809184)Time elapsed: 0.359 s % 269.30/39.51 % (1809184)Peak memory usage: 114 MB % 269.30/39.51 % (1809184)Instructions burned: 540 (million) % 269.30/39.51 % (1809188)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=2386101964:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2642 on theBenchmark for (2642ds/1048Mi) % 269.30/39.51 % (1809185)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 269.30/39.51 % (1809185)------------------------------ % 269.30/39.51 % (1809185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.50/41.63 % (1809185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/41.63 % (1809185)CaDiCaL version: 2.1.3 % 284.50/41.63 % (1809185)Termination reason: Unknown % 284.50/41.63 % (1809185)Termination phase: Saturation % 284.50/41.63 % (1809185)Time elapsed: 0.360 s % 284.50/41.63 % (1809185)Peak memory usage: 113 MB % 284.50/41.63 % (1809185)Instructions burned: 541 (million) % 284.50/41.63 % (1809190)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=2384052920:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2641 on theBenchmark for (2641ds/2032Mi) % 284.50/41.63 % (1809192)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=4102189097:i=28246:bd=preordered:ins=4:rtra=on_2639 on theBenchmark for (2639ds/28246Mi) % 284.50/41.63 % (1809188)Instruction limit reached! % 284.50/41.63 % (1809188)------------------------------ % 284.50/41.63 % (1809188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.50/41.63 % (1809188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/41.63 % (1809188)CaDiCaL version: 2.1.3 % 284.50/41.63 % (1809188)Termination reason: Instruction limit % 284.50/41.63 % (1809188)Termination phase: Saturation % 284.50/41.63 % (1809188)Time elapsed: 0.571 s % 284.50/41.63 % (1809188)Peak memory usage: 99 MB % 284.50/41.63 % (1809188)Instructions burned: 1049 (million) % 284.50/41.63 % (1809192)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 284.50/41.63 % (1809192)------------------------------ % 284.50/41.63 % (1809192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.50/41.63 % (1809192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/41.63 % (1809192)CaDiCaL version: 2.1.3 % 284.50/41.63 % (1809192)Termination reason: Unknown % 284.50/41.63 % (1809192)Termination phase: Saturation % 284.50/41.63 % (1809192)Time elapsed: 0.355 s % 284.50/41.63 % (1809192)Peak memory usage: 114 MB % 284.50/41.63 % (1809192)Instructions burned: 541 (million) % 284.50/41.63 % (1809194)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2968269207:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2635 on theBenchmark for (2635ds/11562Mi) % 284.50/41.63 % (1809195)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:si=on:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=898738988:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2634 on theBenchmark for (2634ds/4896Mi) % 284.50/41.63 % (1809195)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 284.50/41.63 % (1809195)------------------------------ % 284.50/41.63 % (1809195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.50/41.63 % (1809195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/41.63 % (1809195)CaDiCaL version: 2.1.3 % 284.50/41.63 % (1809195)Termination reason: Unknown % 284.50/41.63 % (1809195)Termination phase: Saturation % 284.50/41.63 % (1809195)Time elapsed: 0.359 s % 284.50/41.63 % (1809195)Peak memory usage: 114 MB % 284.50/41.63 % (1809195)Instructions burned: 542 (million) % 284.50/41.63 % (1809198)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=771051922:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2629 on theBenchmark for (2629ds/6446Mi) % 284.50/41.63 % (1809190)Instruction limit reached! % 284.50/41.63 % (1809190)------------------------------ % 284.50/41.63 % (1809190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.50/41.63 % (1809190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.50/41.63 % (1809190)CaDiCaL version: 2.1.3 % 284.50/41.63 % (1809190)Termination reason: Instruction limit % 284.50/41.63 % (1809190)Termination phase: Saturation % 284.50/41.63 % (1809190)Time elapsed: 1.143 s % 284.50/41.63 % (1809190)Peak memory usage: 111 MB % 284.50/41.63 % (1809190)Instructions burned: 2032 (million) % 284.50/41.63 % (1809200)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=3435470364:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2628 on theBenchmark for (2628ds/4066Mi) % 284.50/41.63 % (1809198)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 284.50/41.63 % (1809198)------------------------------ % 284.50/41.63 % (1809198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.50/41.63 % (1809198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.69/42.76 % (1809198)CaDiCaL version: 2.1.3 % 291.69/42.76 % (1809198)Termination reason: Unknown % 291.69/42.76 % (1809198)Termination phase: Saturation % 291.69/42.76 % (1809198)Time elapsed: 0.358 s % 291.69/42.76 % (1809198)Peak memory usage: 114 MB % 291.69/42.76 % (1809198)Instructions burned: 541 (million) % 291.69/42.76 % (1809202)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=298418318:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2624 on theBenchmark for (2624ds/4110Mi) % 291.69/42.76 % (1809200)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 291.69/42.76 % (1809200)------------------------------ % 291.69/42.76 % (1809200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.69/42.76 % (1809200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.69/42.76 % (1809200)CaDiCaL version: 2.1.3 % 291.69/42.76 % (1809200)Termination reason: Unknown % 291.69/42.76 % (1809200)Termination phase: Saturation % 291.69/42.76 % (1809200)Time elapsed: 0.358 s % 291.69/42.76 % (1809200)Peak memory usage: 114 MB % 291.69/42.76 % (1809200)Instructions burned: 541 (million) % 291.69/42.76 % (1809204)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:si=on:sp=const_frequency:spb=goal:acc=on:random_seed=1424762237:i=43222:sd=3:rtra=on:ss=axioms_2623 on theBenchmark for (2623ds/43222Mi) % 291.69/42.76 % (1809202)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 291.69/42.76 % (1809202)------------------------------ % 291.69/42.76 % (1809202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.69/42.76 % (1809202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.69/42.76 % (1809202)CaDiCaL version: 2.1.3 % 291.69/42.76 % (1809202)Termination reason: Unknown % 291.69/42.76 % (1809202)Termination phase: Saturation % 291.69/42.76 % (1809202)Time elapsed: 0.358 s % 291.69/42.76 % (1809202)Peak memory usage: 114 MB % 291.69/42.76 % (1809202)Instructions burned: 540 (million) % 291.69/42.76 % (1809206)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=3469615382:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2620 on theBenchmark for (2620ds/9670Mi) % 291.69/42.76 % (1809204)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 291.69/42.76 % (1809204)------------------------------ % 291.69/42.76 % (1809204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.69/42.76 % (1809204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.69/42.76 % (1809204)CaDiCaL version: 2.1.3 % 291.69/42.76 % (1809204)Termination reason: Unknown % 291.69/42.76 % (1809204)Termination phase: Saturation % 291.69/42.76 % (1809204)Time elapsed: 0.357 s % 291.69/42.76 % (1809204)Peak memory usage: 114 MB % 291.69/42.76 % (1809204)Instructions burned: 539 (million) % 291.69/42.76 % (1809208)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:si=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1197509878:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2618 on theBenchmark for (2618ds/1594Mi) % 291.69/42.76 % (1809172)Instruction limit reached! % 291.69/42.76 % (1809172)------------------------------ % 291.69/42.76 % (1809172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.69/42.76 % (1809172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.69/42.76 % (1809172)CaDiCaL version: 2.1.3 % 291.69/42.76 % (1809172)Termination reason: Instruction limit % 291.69/42.76 % (1809172)Termination phase: Saturation % 291.69/42.76 % (1809172)Time elapsed: 3.822 s % 291.69/42.76 % (1809172)Peak memory usage: 130 MB % 291.69/42.76 % (1809172)Instructions burned: 7413 (million) % 291.69/42.76 % (1809210)lrs-1011_5_sil=8000:si=on:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=4081615495:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2617 on theBenchmark for (2617ds/4652Mi) % 291.69/42.76 % (1809210)Refutation not found, incomplete strategy % 291.69/42.76 % (1809210)------------------------------ % 291.69/42.76 % (1809210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.69/42.76 % (1809210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.69/42.76 % (1809210)CaDiCaL version: 2.1.3 % 291.69/42.76 % (1809210)Termination reason: Refutation not found, incomplete strategy % 291.69/42.76 % (1809210)Time elapsed: 0.007 s % 291.69/42.76 % (1809210)Peak memory usage: 89 MB % 291.69/42.76 % (1809210)Instructions burned: 10 (million) % 291.69/42.76 % (1809210)------------------------------ % 293.93/43.89 % (1809210)------------------------------ % 293.93/43.89 % (1809212)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=4235267600:i=12076:nm=6:rtra=on_2613 on theBenchmark for (2613ds/12076Mi) % 293.93/43.89 % (1809163)Instruction limit reached! % 293.93/43.89 % (1809163)------------------------------ % 293.93/43.89 % (1809163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.93/43.89 % (1809163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.93/43.89 % (1809163)CaDiCaL version: 2.1.3 % 293.93/43.89 % (1809163)Termination reason: Instruction limit % 293.93/43.89 % (1809163)Termination phase: Saturation % 293.93/43.89 % (1809163)Time elapsed: 5.163 s % 293.93/43.89 % (1809163)Peak memory usage: 214 MB % 293.93/43.89 % (1809163)Instructions burned: 9700 (million) % 293.93/43.89 % (1809212)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 293.93/43.89 % (1809212)------------------------------ % 293.93/43.89 % (1809212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.93/43.89 % (1809212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.93/43.89 % (1809212)CaDiCaL version: 2.1.3 % 293.93/43.89 % (1809212)Termination reason: Unknown % 293.93/43.89 % (1809212)Termination phase: Saturation % 293.93/43.89 % (1809212)Time elapsed: 0.357 s % 293.93/43.89 % (1809212)Peak memory usage: 113 MB % 293.93/43.89 % (1809212)Instructions burned: 540 (million) % 293.93/43.89 % (1809208)Instruction limit reached! % 293.93/43.89 % (1809208)------------------------------ % 293.93/43.89 % (1809208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.93/43.89 % (1809208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.93/43.89 % (1809208)CaDiCaL version: 2.1.3 % 293.93/43.89 % (1809208)Termination reason: Instruction limit % 293.93/43.89 % (1809208)Termination phase: Saturation % 293.93/43.89 % (1809208)Time elapsed: 0.960 s % 293.93/43.89 % (1809208)Peak memory usage: 112 MB % 293.93/43.89 % (1809208)Instructions burned: 1594 (million) % 293.93/43.89 % (1809214)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=1833874272:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2608 on theBenchmark for (2608ds/66668Mi) % 293.93/43.89 % (1809215)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=4169431745:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2608 on theBenchmark for (2608ds/2016Mi) % 293.93/43.89 % (1809216)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:si=on:sp=const_frequency:spb=intro:gs=on:random_seed=3066692402:i=16654:s2at=5:bd=preordered:rtra=on_2607 on theBenchmark for (2607ds/16654Mi) % 293.93/43.89 % (1809216)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 293.93/43.89 % (1809216)------------------------------ % 293.93/43.89 % (1809216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.93/43.89 % (1809216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.93/43.89 % (1809216)CaDiCaL version: 2.1.3 % 293.93/43.89 % (1809216)Termination reason: Unknown % 293.93/43.89 % (1809216)Termination phase: Saturation % 293.93/43.89 % (1809216)Time elapsed: 0.357 s % 293.93/43.89 % (1809216)Peak memory usage: 114 MB % 293.93/43.89 % (1809216)Instructions burned: 541 (million) % 293.93/43.89 % (1809220)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:si=on:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2473801109:s2a=on:i=2166:s2at=1.87328:slsql=off:ep=RSTC:rtra=on:fdi=16_2602 on theBenchmark for (2602ds/2166Mi) % 293.93/43.89 % (1809215)Instruction limit reached! % 293.93/43.89 % (1809215)------------------------------ % 293.93/43.89 % (1809215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.93/43.89 % (1809215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.93/43.89 % (1809215)CaDiCaL version: 2.1.3 % 293.93/43.89 % (1809215)Termination reason: Instruction limit % 293.93/43.89 % (1809215)Termination phase: Saturation % 293.93/43.89 % (1809215)Time elapsed: 0.921 s % 293.93/43.89 % (1809215)Peak memory usage: 102 MB % 293.93/43.89 % (1809215)Instructions burned: 2016 (million) % 293.93/43.89 % (1809222)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:si=on:spb=goal:fd=preordered:random_seed=856578852:i=2168:sd=1:bd=preordered:av=off:fsr=off:rtra=on:ss=axioms:sgt=14_2598 on theBenchmark for (2598ds/2168Mi) % 293.93/43.89 % (1809220)Instruction limit reacheTerminated % 300.88/43.93 % Vampire exiting % 300.88/43.93 Terminated %------------------------------------------------------------------------------