%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM956_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 : n006.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:41 PM UTC 2026 % Result : Timeout 293.51s 42.34s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM956_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.43 % Computer : n006.cluster.edu % 0.17/0.43 % Model : x86_64 x86_64 % 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.43 % Memory : 8046.5625MB % 0.17/0.43 % OS : Linux 6.8.0-71-generic % 0.17/0.43 % CPULimit : 300 % 0.17/0.43 % WCLimit : 300 % 0.17/0.43 % DateTime : Sun Sep 27 21:47:40 UTC 2026 % 0.17/0.43 % CPUTime : % 0.17/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.22/0.48 Running first-order theorem proving % 0.22/0.48 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.65/2.31 % (3349793)Detected formulas, will run a generic FOF schedule. % 9.65/2.31 % (3349798)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=545500041:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 9.65/2.31 % (3349804)dis-21_1_sil=8000:lcm=predicate:random_seed=2147876241:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 9.65/2.31 % (3349801)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1808076233:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 9.65/2.31 % (3349802)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=533772799:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 9.65/2.31 % (3349803)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3448181634:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 9.65/2.31 % (3349800)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=1287682708:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 9.65/2.31 % (3349799)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=2306956421:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 9.65/2.31 % (3349801)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 9.65/2.31 % (3349800)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 9.65/2.31 % (3349801)Refutation not found, incomplete strategy % 9.65/2.31 % (3349801)------------------------------ % 9.65/2.31 % (3349801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.31 % (3349801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.31 % (3349801)CaDiCaL version: 2.1.3 % 9.65/2.31 % (3349801)Termination reason: Refutation not found, incomplete strategy % 9.65/2.31 % (3349801)Time elapsed: 0.008 s % 9.65/2.31 % (3349801)Peak memory usage: 89 MB % 9.65/2.31 % (3349801)Instructions burned: 6 (million) % 9.65/2.31 % (3349804)Instruction limit reached! % 9.65/2.31 % (3349804)------------------------------ % 9.65/2.31 % (3349804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.31 % (3349804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.31 % (3349804)CaDiCaL version: 2.1.3 % 9.65/2.31 % (3349804)Termination reason: Instruction limit % 9.65/2.31 % (3349804)Termination phase: Saturation % 9.65/2.31 % (3349804)Time elapsed: 0.108 s % 9.65/2.31 % (3349804)Peak memory usage: 89 MB % 9.65/2.31 % (3349804)Instructions burned: 130 (million) % 9.65/2.31 % (3349802)Instruction limit reached! % 9.65/2.31 % (3349802)------------------------------ % 9.65/2.31 % (3349802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.31 % (3349802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.31 % (3349802)CaDiCaL version: 2.1.3 % 9.65/2.31 % (3349802)Termination reason: Instruction limit % 9.65/2.31 % (3349802)Termination phase: Saturation % 9.65/2.31 % (3349802)Time elapsed: 0.110 s % 9.65/2.31 % (3349802)Peak memory usage: 88 MB % 9.65/2.31 % (3349802)Instructions burned: 120 (million) % 9.65/2.31 % (3349803)Instruction limit reached! % 9.65/2.31 % (3349803)------------------------------ % 9.65/2.31 % (3349803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.31 % (3349803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.31 % (3349803)CaDiCaL version: 2.1.3 % 9.65/2.31 % (3349803)Termination reason: Instruction limit % 9.65/2.31 % (3349803)Termination phase: Saturation % 9.65/2.31 % (3349803)Time elapsed: 0.146 s % 9.65/2.31 % (3349803)Peak memory usage: 89 MB % 9.65/2.31 % (3349803)Instructions burned: 139 (million) % 9.65/2.31 % (3349798)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 9.65/2.31 % (3349798)------------------------------ % 9.65/2.31 % (3349798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.65/2.31 % (3349798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.65/2.31 % (3349798)CaDiCaL version: 2.1.3 % 9.65/2.31 % (3349798)Termination reason: Unknown % 9.65/2.31 % (3349798)Termination phase: Saturation % 11.61/2.91 % (3349798)Time elapsed: 0.322 s % 11.61/2.91 % (3349798)Peak memory usage: 114 MB % 11.61/2.91 % (3349798)Instructions burned: 541 (million) % 11.61/2.91 % (3349812)lrs+10_1_sil=8000:sp=occurrence:random_seed=3233832082:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 11.61/2.91 % (3349813)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2176069727:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 11.61/2.91 % (3349801)------------------------------ % 11.61/2.91 % (3349801)------------------------------ % 11.61/2.91 % (3349816)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3701823561:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 11.61/2.91 % (3349817)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=2104745781:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi) % 11.61/2.91 % (3349813)Instruction limit reached! % 11.61/2.91 % (3349813)------------------------------ % 11.61/2.91 % (3349813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.61/2.91 % (3349813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.61/2.91 % (3349813)CaDiCaL version: 2.1.3 % 11.61/2.91 % (3349813)Termination reason: Instruction limit % 11.61/2.91 % (3349813)Termination phase: Saturation % 11.61/2.91 % (3349813)Time elapsed: 0.148 s % 11.61/2.91 % (3349813)Peak memory usage: 89 MB % 11.61/2.91 % (3349813)Instructions burned: 158 (million) % 11.61/2.91 % (3349820)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2064863795:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 11.61/2.91 % (3349800)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 11.61/2.91 % (3349799)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 11.61/2.91 % (3349799)------------------------------ % 11.61/2.91 % (3349799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.61/2.91 % (3349800)------------------------------ % 11.61/2.91 % (3349800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.61/2.91 % (3349799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.61/2.91 % (3349800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.61/2.91 % (3349800)CaDiCaL version: 2.1.3 % 11.61/2.91 % (3349799)CaDiCaL version: 2.1.3 % 11.61/2.91 % (3349799)Termination reason: Unknown % 11.61/2.91 % (3349799)Termination phase: Saturation % 11.61/2.91 % (3349800)Termination reason: Unknown % 11.61/2.91 % (3349800)Termination phase: Saturation % 11.61/2.91 % (3349799)Time elapsed: 0.588 s % 11.61/2.91 % (3349800)Time elapsed: 0.588 s % 11.61/2.91 % (3349800)Peak memory usage: 113 MB % 11.61/2.91 % (3349799)Peak memory usage: 113 MB % 11.61/2.91 % (3349800)Instructions burned: 541 (million) % 11.61/2.91 % (3349799)Instructions burned: 544 (million) % 11.61/2.91 % (3349820)Refutation not found, incomplete strategy % 11.61/2.91 % (3349820)------------------------------ % 11.61/2.91 % (3349820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.61/2.91 % (3349820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.61/2.91 % (3349820)CaDiCaL version: 2.1.3 % 11.61/2.91 % (3349820)Termination reason: Refutation not found, incomplete strategy % 11.61/2.91 % (3349820)Time elapsed: 0.007 s % 11.61/2.91 % (3349820)Peak memory usage: 88 MB % 11.61/2.91 % (3349820)Instructions burned: 10 (million) % 11.61/2.91 % (3349812)Instruction limit reached! % 11.61/2.91 % (3349812)------------------------------ % 11.61/2.91 % (3349812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.61/2.91 % (3349812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.61/2.91 % (3349812)CaDiCaL version: 2.1.3 % 11.61/2.91 % (3349812)Termination reason: Instruction limit % 11.61/2.91 % (3349812)Termination phase: Saturation % 11.61/2.91 % (3349812)Time elapsed: 0.255 s % 11.61/2.91 % (3349812)Peak memory usage: 91 MB % 11.61/2.91 % (3349812)Instructions burned: 286 (million) % 11.61/2.91 % (3349817)Instruction limit reached! % 11.61/2.91 % (3349817)------------------------------ % 11.61/2.91 % (3349817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.61/2.91 % (3349817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.61/2.91 % (3349817)CaDiCaL version: 2.1.3 % 11.61/2.91 % (3349817)Termination reason: Instruction limit % 11.61/2.91 % (3349817)Termination phase: Saturation % 11.61/2.91 % (3349817)Time elapsed: 0.241 s % 11.61/2.91 % (3349817)Peak memory usage: 91 MB % 16.61/3.33 % (3349817)Instructions burned: 249 (million) % 16.61/3.33 % (3349823)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2539028836:i=2350_2991 on theBenchmark for (2991ds/2350Mi) % 16.61/3.33 % (3349816)Instruction limit reached! % 16.61/3.33 % (3349816)------------------------------ % 16.61/3.33 % (3349816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.61/3.33 % (3349816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.61/3.33 % (3349816)CaDiCaL version: 2.1.3 % 16.61/3.33 % (3349816)Termination reason: Instruction limit % 16.61/3.33 % (3349816)Termination phase: Saturation % 16.61/3.33 % (3349816)Time elapsed: 0.320 s % 16.61/3.33 % (3349816)Peak memory usage: 91 MB % 16.61/3.33 % (3349816)Instructions burned: 325 (million) % 16.61/3.33 % (3349827)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=595413970:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 16.61/3.33 % (3349825)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1812537895:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi) % 16.61/3.33 % (3349826)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2422712759:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi) % 16.61/3.33 % (3349827)Instruction limit reached! % 16.61/3.33 % (3349827)------------------------------ % 16.61/3.33 % (3349827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.61/3.33 % (3349827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.61/3.33 % (3349827)CaDiCaL version: 2.1.3 % 16.61/3.33 % (3349827)Termination reason: Instruction limit % 16.61/3.33 % (3349827)Termination phase: Saturation % 16.61/3.33 % (3349827)Time elapsed: 0.091 s % 16.61/3.33 % (3349827)Peak memory usage: 89 MB % 16.61/3.33 % (3349827)Instructions burned: 115 (million) % 16.61/3.33 % (3349826)Instruction limit reached! % 16.61/3.33 % (3349826)------------------------------ % 16.61/3.33 % (3349826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.61/3.33 % (3349826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.61/3.33 % (3349826)CaDiCaL version: 2.1.3 % 16.61/3.33 % (3349826)Termination reason: Instruction limit % 16.61/3.33 % (3349826)Termination phase: Saturation % 16.61/3.33 % (3349826)Time elapsed: 0.105 s % 16.61/3.33 % (3349826)Peak memory usage: 88 MB % 16.61/3.33 % (3349826)Instructions burned: 128 (million) % 16.61/3.33 % (3349820)------------------------------ % 16.61/3.33 % (3349820)------------------------------ % 16.61/3.33 % (3349825)Instruction limit reached! % 16.61/3.33 % (3349825)------------------------------ % 16.61/3.33 % (3349825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.61/3.33 % (3349825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.61/3.33 % (3349825)CaDiCaL version: 2.1.3 % 16.61/3.33 % (3349825)Termination reason: Instruction limit % 16.61/3.33 % (3349825)Termination phase: Saturation % 16.61/3.33 % (3349825)Time elapsed: 0.121 s % 16.61/3.33 % (3349825)Peak memory usage: 89 MB % 16.61/3.33 % (3349825)Instructions burned: 114 (million) % 16.61/3.33 % (3349829)lrs+10_1_sil=8000:sp=occurrence:random_seed=924623460:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi) % 16.61/3.33 % (3349830)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3882341489:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 16.61/3.33 % (3349830)Refutation not found, incomplete strategy % 16.61/3.33 % (3349830)------------------------------ % 16.61/3.33 % (3349830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.61/3.33 % (3349830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.61/3.33 % (3349830)CaDiCaL version: 2.1.3 % 16.61/3.33 % (3349830)Termination reason: Refutation not found, incomplete strategy % 16.61/3.33 % (3349830)Time elapsed: 0.009 s % 16.61/3.33 % (3349830)Peak memory usage: 88 MB % 16.61/3.33 % (3349830)Instructions burned: 8 (million) % 16.61/3.33 % (3349823)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 16.61/3.33 % (3349823)------------------------------ % 16.61/3.33 % (3349823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.61/3.33 % (3349823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.61/3.33 % (3349823)CaDiCaL version: 2.1.3 % 16.61/3.33 % (3349823)Termination reason: Unknown % 17.73/3.78 % (3349823)Termination phase: Saturation % 17.73/3.78 % (3349823)Time elapsed: 0.325 s % 17.73/3.78 % (3349823)Peak memory usage: 114 MB % 17.73/3.78 % (3349823)Instructions burned: 541 (million) % 17.73/3.78 % (3349834)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2091666512:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi) % 17.73/3.78 % (3349837)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4179410276:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi) % 17.73/3.78 % (3349836)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3660393117:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi) % 17.73/3.78 % (3349835)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2640534002:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi) % 17.73/3.78 % (3349836)Refutation not found, incomplete strategy % 17.73/3.78 % (3349836)------------------------------ % 17.73/3.78 % (3349836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.73/3.78 % (3349836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.73/3.78 % (3349836)CaDiCaL version: 2.1.3 % 17.73/3.78 % (3349836)Termination reason: Refutation not found, incomplete strategy % 17.73/3.78 % (3349836)Time elapsed: 0.010 s % 17.73/3.78 % (3349836)Peak memory usage: 88 MB % 17.73/3.78 % (3349836)Instructions burned: 10 (million) % 17.73/3.78 % (3349840)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=578598107:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi) % 17.73/3.78 % (3349840)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.73/3.78 % (3349840)Instruction limit reached! % 17.73/3.78 % (3349840)------------------------------ % 17.73/3.78 % (3349840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.73/3.78 % (3349840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.73/3.78 % (3349840)CaDiCaL version: 2.1.3 % 17.73/3.78 % (3349840)Termination reason: Instruction limit % 17.73/3.78 % (3349840)Termination phase: Saturation % 17.73/3.78 % (3349840)Time elapsed: 0.063 s % 17.73/3.78 % (3349840)Peak memory usage: 90 MB % 17.73/3.78 % (3349840)Instructions burned: 127 (million) % 17.73/3.78 % (3349835)Instruction limit reached! % 17.73/3.78 % (3349835)------------------------------ % 17.73/3.78 % (3349835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.73/3.78 % (3349835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.73/3.78 % (3349835)CaDiCaL version: 2.1.3 % 17.73/3.78 % (3349835)Termination reason: Instruction limit % 17.73/3.78 % (3349835)Termination phase: Saturation % 17.73/3.78 % (3349835)Time elapsed: 0.135 s % 17.73/3.78 % (3349835)Peak memory usage: 90 MB % 17.73/3.78 % (3349835)Instructions burned: 135 (million) % 17.73/3.78 % (3349830)------------------------------ % 17.73/3.78 % (3349830)------------------------------ % 17.73/3.78 % (3349846)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4201023364:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi) % 17.73/3.78 % (3349846)Instruction limit reached! % 17.73/3.78 % (3349846)------------------------------ % 17.73/3.78 % (3349846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.73/3.78 % (3349846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.73/3.78 % (3349846)CaDiCaL version: 2.1.3 % 17.73/3.78 % (3349846)Termination reason: Instruction limit % 17.73/3.78 % (3349846)Termination phase: Saturation % 17.73/3.78 % (3349846)Time elapsed: 0.070 s % 17.73/3.78 % (3349846)Peak memory usage: 90 MB % 17.73/3.78 % (3349846)Instructions burned: 135 (million) % 17.73/3.78 % (3349836)------------------------------ % 17.73/3.78 % (3349836)------------------------------ % 17.73/3.78 % (3349847)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2968223653:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi) % 17.73/3.78 % (3349847)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.73/3.78 % (3349847)Refutation not found, incomplete strategy % 17.73/3.78 % (3349847)------------------------------ % 17.73/3.78 % (3349847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.22/4.44 % (3349847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.22/4.44 % (3349847)CaDiCaL version: 2.1.3 % 24.22/4.44 % (3349847)Termination reason: Refutation not found, incomplete strategy % 24.22/4.44 % (3349847)Time elapsed: 0.005 s % 24.22/4.44 % (3349847)Peak memory usage: 88 MB % 24.22/4.44 % (3349847)Instructions burned: 3 (million) % 24.22/4.44 % (3349848)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1054609618:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/431Mi) % 24.22/4.44 % (3349848)Refutation not found, incomplete strategy % 24.22/4.44 % (3349848)------------------------------ % 24.22/4.44 % (3349848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.22/4.44 % (3349848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.22/4.44 % (3349848)CaDiCaL version: 2.1.3 % 24.22/4.44 % (3349848)Termination reason: Refutation not found, incomplete strategy % 24.22/4.44 % (3349848)Time elapsed: 0.009 s % 24.22/4.44 % (3349848)Peak memory usage: 89 MB % 24.22/4.44 % (3349848)Instructions burned: 8 (million) % 24.22/4.44 % (3349834)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 24.22/4.44 % (3349834)------------------------------ % 24.22/4.44 % (3349834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.22/4.44 % (3349834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.22/4.44 % (3349834)CaDiCaL version: 2.1.3 % 24.22/4.44 % (3349834)Termination reason: Unknown % 24.22/4.44 % (3349834)Termination phase: Saturation % 24.22/4.44 % (3349834)Time elapsed: 0.552 s % 24.22/4.44 % (3349834)Peak memory usage: 113 MB % 24.22/4.44 % (3349834)Instructions burned: 542 (million) % 24.22/4.44 % (3349850)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=382510843:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi) % 24.22/4.44 % (3349837)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 24.22/4.44 % (3349837)------------------------------ % 24.22/4.44 % (3349837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.22/4.44 % (3349837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.22/4.44 % (3349837)CaDiCaL version: 2.1.3 % 24.22/4.44 % (3349837)Termination reason: Unknown % 24.22/4.44 % (3349837)Termination phase: Saturation % 24.22/4.44 % (3349837)Time elapsed: 0.596 s % 24.22/4.44 % (3349837)Peak memory usage: 114 MB % 24.22/4.44 % (3349837)Instructions burned: 541 (million) % 24.22/4.44 % (3349855)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2691354216:i=14155:bd=all_2980 on theBenchmark for (2980ds/14155Mi) % 24.22/4.44 % (3349829)Instruction limit reached! % 24.22/4.44 % (3349829)------------------------------ % 24.22/4.44 % (3349829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.22/4.44 % (3349829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.22/4.44 % (3349829)CaDiCaL version: 2.1.3 % 24.22/4.44 % (3349829)Termination reason: Instruction limit % 24.22/4.44 % (3349829)Termination phase: Saturation % 24.22/4.44 % (3349829)Time elapsed: 0.896 s % 24.22/4.44 % (3349829)Peak memory usage: 95 MB % 24.22/4.44 % (3349829)Instructions burned: 907 (million) % 24.22/4.44 % (3349851)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=717141394:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi) % 24.22/4.44 % (3349851)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 24.22/4.44 % (3349847)------------------------------ % 24.22/4.44 % (3349847)------------------------------ % 24.22/4.44 % (3349851)Instruction limit reached! % 24.22/4.44 % (3349851)------------------------------ % 24.22/4.44 % (3349851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.22/4.44 % (3349851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.22/4.44 % (3349851)CaDiCaL version: 2.1.3 % 24.22/4.44 % (3349851)Termination reason: Instruction limit % 24.22/4.44 % (3349851)Termination phase: Saturation % 24.22/4.44 % (3349851)Time elapsed: 0.146 s % 24.22/4.44 % (3349851)Peak memory usage: 90 MB % 24.22/4.44 % (3349851)Instructions burned: 150 (million) % 24.22/4.44 % (3349848)------------------------------ % 24.22/4.44 % (3349848)------------------------------ % 30.75/5.34 % (3349860)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1237614356:i=667:av=off:fsr=off_2978 on theBenchmark for (2978ds/667Mi) % 30.75/5.34 % (3349860)Refutation not found, incomplete strategy % 30.75/5.34 % (3349860)------------------------------ % 30.75/5.34 % (3349860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.75/5.34 % (3349860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/5.34 % (3349860)CaDiCaL version: 2.1.3 % 30.75/5.34 % (3349860)Termination reason: Refutation not found, incomplete strategy % 30.75/5.34 % (3349860)Time elapsed: 0.010 s % 30.75/5.34 % (3349860)Peak memory usage: 88 MB % 30.75/5.34 % (3349860)Instructions burned: 9 (million) % 30.75/5.34 % (3349855)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 30.75/5.34 % (3349855)------------------------------ % 30.75/5.34 % (3349855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.75/5.34 % (3349855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/5.34 % (3349855)CaDiCaL version: 2.1.3 % 30.75/5.34 % (3349855)Termination reason: Unknown % 30.75/5.34 % (3349855)Termination phase: Saturation % 30.75/5.34 % (3349855)Time elapsed: 0.288 s % 30.75/5.34 % (3349855)Peak memory usage: 114 MB % 30.75/5.34 % (3349855)Instructions burned: 541 (million) % 30.75/5.34 % (3349862)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=776462442:s2a=on:i=185:s2at=1.8:fdi=4_2978 on theBenchmark for (2978ds/185Mi) % 30.75/5.34 % (3349865)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1272598287:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2976 on theBenchmark for (2976ds/4850Mi) % 30.75/5.34 % (3349864)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=285933431:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2976 on theBenchmark for (2976ds/193Mi) % 30.75/5.34 % (3349867)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2113150164:i=12111:sd=1:ss=included_2976 on theBenchmark for (2976ds/12111Mi) % 30.75/5.34 % (3349862)Instruction limit reached! % 30.75/5.34 % (3349862)------------------------------ % 30.75/5.34 % (3349862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.75/5.34 % (3349862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/5.34 % (3349862)CaDiCaL version: 2.1.3 % 30.75/5.34 % (3349862)Termination reason: Instruction limit % 30.75/5.34 % (3349862)Termination phase: Saturation % 30.75/5.34 % (3349862)Time elapsed: 0.178 s % 30.75/5.34 % (3349862)Peak memory usage: 90 MB % 30.75/5.34 % (3349862)Instructions burned: 185 (million) % 30.75/5.34 % (3349868)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3800221692:i=319:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/319Mi) % 30.75/5.34 % (3349850)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 30.75/5.34 % (3349850)------------------------------ % 30.75/5.34 % (3349850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.75/5.34 % (3349850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/5.34 % (3349850)CaDiCaL version: 2.1.3 % 30.75/5.34 % (3349850)Termination reason: Unknown % 30.75/5.34 % (3349850)Termination phase: Saturation % 30.75/5.34 % (3349850)Time elapsed: 0.614 s % 30.75/5.34 % (3349850)Peak memory usage: 114 MB % 30.75/5.34 % (3349850)Instructions burned: 541 (million) % 30.75/5.34 % (3349860)------------------------------ % 30.75/5.34 % (3349860)------------------------------ % 30.75/5.34 % (3349864)Instruction limit reached! % 30.75/5.34 % (3349864)------------------------------ % 30.75/5.34 % (3349864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.75/5.34 % (3349864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.75/5.34 % (3349864)CaDiCaL version: 2.1.3 % 30.75/5.34 % (3349864)Termination reason: Instruction limit % 30.75/5.34 % (3349864)Termination phase: Saturation % 30.75/5.34 % (3349864)Time elapsed: 0.175 s % 30.75/5.34 % (3349864)Peak memory usage: 89 MB % 30.75/5.34 % (3349864)Instructions burned: 193 (million) % 30.75/5.34 % (3349868)Instruction limit reached! % 30.75/5.34 % (3349868)------------------------------ % 30.75/5.34 % (3349868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.75/5.34 % (3349868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.93/6.34 % (3349868)CaDiCaL version: 2.1.3 % 37.93/6.34 % (3349868)Termination reason: Instruction limit % 37.93/6.34 % (3349868)Termination phase: Saturation % 37.93/6.34 % (3349868)Time elapsed: 0.160 s % 37.93/6.34 % (3349868)Peak memory usage: 91 MB % 37.93/6.34 % (3349868)Instructions burned: 320 (million) % 37.93/6.34 % (3349874)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3710956336:i=2064:ep=RST_2973 on theBenchmark for (2973ds/2064Mi) % 37.93/6.34 % (3349874)Refutation not found, incomplete strategy % 37.93/6.34 % (3349874)------------------------------ % 37.93/6.34 % (3349874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.93/6.34 % (3349874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.93/6.34 % (3349874)CaDiCaL version: 2.1.3 % 37.93/6.34 % (3349874)Termination reason: Refutation not found, incomplete strategy % 37.93/6.34 % (3349874)Time elapsed: 0.010 s % 37.93/6.34 % (3349874)Peak memory usage: 88 MB % 37.93/6.34 % (3349874)Instructions burned: 9 (million) % 37.93/6.34 % (3349876)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1221952645:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2972 on theBenchmark for (2972ds/757Mi) % 37.93/6.34 % (3349876)Refutation not found, incomplete strategy % 37.93/6.34 % (3349876)------------------------------ % 37.93/6.34 % (3349876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.93/6.34 % (3349876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.93/6.34 % (3349876)CaDiCaL version: 2.1.3 % 37.93/6.34 % (3349876)Termination reason: Refutation not found, incomplete strategy % 37.93/6.34 % (3349876)Time elapsed: 0.006 s % 37.93/6.34 % (3349876)Peak memory usage: 89 MB % 37.93/6.34 % (3349876)Instructions burned: 9 (million) % 37.93/6.34 % (3349875)dis-1011_128_sil=32000:random_seed=719474390:i=3706:ep=RST:av=off_2972 on theBenchmark for (2972ds/3706Mi) % 37.93/6.34 % (3349878)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1243953725:i=9925:aac=none_2971 on theBenchmark for (2971ds/9925Mi) % 37.93/6.34 % (3349877)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1129989999:i=13913:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/13913Mi) % 37.93/6.34 % (3349867)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 37.93/6.34 % (3349867)------------------------------ % 37.93/6.34 % (3349867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.93/6.34 % (3349867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.93/6.34 % (3349867)CaDiCaL version: 2.1.3 % 37.93/6.34 % (3349867)Termination reason: Unknown % 37.93/6.34 % (3349867)Termination phase: Saturation % 37.93/6.34 % (3349867)Time elapsed: 0.569 s % 37.93/6.34 % (3349867)Peak memory usage: 114 MB % 37.93/6.34 % (3349867)Instructions burned: 541 (million) % 37.93/6.34 % (3349878)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 37.93/6.34 % (3349878)------------------------------ % 37.93/6.34 % (3349878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.93/6.34 % (3349878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.93/6.34 % (3349878)CaDiCaL version: 2.1.3 % 37.93/6.34 % (3349878)Termination reason: Unknown % 37.93/6.34 % (3349878)Termination phase: Saturation % 37.93/6.34 % (3349878)Time elapsed: 0.295 s % 37.93/6.34 % (3349878)Peak memory usage: 113 MB % 37.93/6.34 % (3349878)Instructions burned: 541 (million) % 37.93/6.34 % (3349874)------------------------------ % 37.93/6.34 % (3349874)------------------------------ % 37.93/6.34 % (3349876)------------------------------ % 37.93/6.34 % (3349876)------------------------------ % 37.93/6.34 % (3349884)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4175540561:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/2479Mi) % 37.93/6.34 % (3349884)Refutation not found, incomplete strategy % 37.93/6.34 % (3349884)------------------------------ % 37.93/6.34 % (3349884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.93/6.34 % (3349884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.93/6.34 % (3349884)CaDiCaL version: 2.1.3 % 37.93/6.34 % (3349884)Termination reason: Refutation not found, incomplete strategy % 37.93/6.34 % (3349884)Time elapsed: 0.011 s % 37.93/6.34 % (3349884)Peak memory usage: 89 MB % 46.14/7.55 % (3349884)Instructions burned: 10 (million) % 46.14/7.55 % (3349885)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=230470778:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2967 on theBenchmark for (2967ds/440Mi) % 46.14/7.55 % (3349885)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 46.14/7.55 % (3349887)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=3159099262:cts=off:i=3034:av=off:er=known:fsd=on_2966 on theBenchmark for (2966ds/3034Mi) % 46.14/7.55 % (3349886)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1537344607:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2966 on theBenchmark for (2966ds/11145Mi) % 46.14/7.55 % (3349877)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 46.14/7.55 % (3349877)------------------------------ % 46.14/7.55 % (3349877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.14/7.55 % (3349877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.14/7.55 % (3349877)CaDiCaL version: 2.1.3 % 46.14/7.55 % (3349877)Termination reason: Unknown % 46.14/7.55 % (3349877)Termination phase: Saturation % 46.14/7.55 % (3349877)Time elapsed: 0.592 s % 46.14/7.55 % (3349877)Peak memory usage: 114 MB % 46.14/7.55 % (3349877)Instructions burned: 540 (million) % 46.14/7.55 % (3349885)Instruction limit reached! % 46.14/7.55 % (3349885)------------------------------ % 46.14/7.55 % (3349885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.14/7.55 % (3349885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.14/7.55 % (3349885)CaDiCaL version: 2.1.3 % 46.14/7.55 % (3349885)Termination reason: Instruction limit % 46.14/7.55 % (3349885)Termination phase: Saturation % 46.14/7.55 % (3349885)Time elapsed: 0.188 s % 46.14/7.55 % (3349885)Peak memory usage: 92 MB % 46.14/7.55 % (3349885)Instructions burned: 442 (million) % 46.14/7.55 % (3349884)------------------------------ % 46.14/7.55 % (3349884)------------------------------ % 46.14/7.55 % (3349893)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3298877296:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2963 on theBenchmark for (2963ds/1016Mi) % 46.14/7.55 % (3349892)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3832208759:st=2:s2a=on:i=524:s2at=2:ss=axioms_2963 on theBenchmark for (2963ds/524Mi) % 46.14/7.55 % (3349887)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 46.14/7.55 % (3349887)------------------------------ % 46.14/7.55 % (3349887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.14/7.55 % (3349887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.14/7.55 % (3349887)CaDiCaL version: 2.1.3 % 46.14/7.55 % (3349887)Termination reason: Unknown % 46.14/7.55 % (3349887)Termination phase: Saturation % 46.14/7.55 % (3349887)Time elapsed: 0.565 s % 46.14/7.55 % (3349887)Peak memory usage: 113 MB % 46.14/7.55 % (3349887)Instructions burned: 541 (million) % 46.14/7.55 % (3349894)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2148866118:i=14123:bd=preordered:ins=4_2961 on theBenchmark for (2961ds/14123Mi) % 46.14/7.55 % (3349886)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 46.14/7.55 % (3349886)------------------------------ % 46.14/7.55 % (3349886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.14/7.55 % (3349886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.14/7.55 % (3349886)CaDiCaL version: 2.1.3 % 46.14/7.55 % (3349886)Termination reason: Unknown % 46.14/7.55 % (3349886)Termination phase: Saturation % 46.14/7.55 % (3349886)Time elapsed: 0.594 s % 46.14/7.55 % (3349886)Peak memory usage: 113 MB % 46.14/7.55 % (3349886)Instructions burned: 541 (million) % 46.14/7.55 % (3349897)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1518286457:i=5781:kws=precedence:bd=all:rawr=on_2958 on theBenchmark for (2958ds/5781Mi) % 46.14/7.55 % (3349893)Instruction limit reached! % 46.14/7.55 % (3349893)------------------------------ % 46.14/7.55 % (3349893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.14/7.55 % (3349893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.14/7.55 % (3349893)CaDiCaL version: 2.1.3 % 54.34/8.73 % (3349893)Termination reason: Instruction limit % 54.34/8.73 % (3349893)Termination phase: Saturation % 54.34/8.73 % (3349893)Time elapsed: 0.480 s % 54.34/8.73 % (3349893)Peak memory usage: 98 MB % 54.34/8.73 % (3349893)Instructions burned: 1017 (million) % 54.34/8.73 % (3349892)Instruction limit reached! % 54.34/8.73 % (3349892)------------------------------ % 54.34/8.73 % (3349892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.34/8.73 % (3349892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.34/8.73 % (3349892)CaDiCaL version: 2.1.3 % 54.34/8.73 % (3349892)Termination reason: Instruction limit % 54.34/8.73 % (3349892)Termination phase: Saturation % 54.34/8.73 % (3349892)Time elapsed: 0.479 s % 54.34/8.73 % (3349892)Peak memory usage: 92 MB % 54.34/8.73 % (3349892)Instructions burned: 524 (million) % 54.34/8.73 % (3349899)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=515313586:i=2448:gtgl=5:bd=preordered:gtg=all_2958 on theBenchmark for (2958ds/2448Mi) % 54.34/8.73 % (3349901)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=573066435:i=3223:kws=precedence:fgj=on:av=off_2956 on theBenchmark for (2956ds/3223Mi) % 54.34/8.73 % (3349894)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 54.34/8.73 % (3349894)------------------------------ % 54.34/8.73 % (3349894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.34/8.73 % (3349894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.34/8.73 % (3349894)CaDiCaL version: 2.1.3 % 54.34/8.73 % (3349894)Termination reason: Unknown % 54.34/8.73 % (3349894)Termination phase: Saturation % 54.34/8.73 % (3349894)Time elapsed: 0.568 s % 54.34/8.73 % (3349894)Peak memory usage: 114 MB % 54.34/8.73 % (3349894)Instructions burned: 539 (million) % 54.34/8.73 % (3349902)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4171624821:st=5.6:i=2033:sd=3:ss=axioms_2955 on theBenchmark for (2955ds/2033Mi) % 54.34/8.73 % (3349901)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 54.34/8.73 % (3349901)------------------------------ % 54.34/8.73 % (3349901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.34/8.73 % (3349901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.34/8.73 % (3349901)CaDiCaL version: 2.1.3 % 54.34/8.73 % (3349901)Termination reason: Unknown % 54.34/8.73 % (3349901)Termination phase: Saturation % 54.34/8.73 % (3349901)Time elapsed: 0.294 s % 54.34/8.73 % (3349901)Peak memory usage: 114 MB % 54.34/8.73 % (3349901)Instructions burned: 541 (million) % 54.34/8.73 % (3349906)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=366822895:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2952 on theBenchmark for (2952ds/2055Mi) % 54.34/8.73 % (3349899)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 54.34/8.73 % (3349899)------------------------------ % 54.34/8.73 % (3349899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.34/8.73 % (3349899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.34/8.73 % (3349899)CaDiCaL version: 2.1.3 % 54.34/8.73 % (3349899)Termination reason: Unknown % 54.34/8.73 % (3349899)Termination phase: Saturation % 54.34/8.73 % (3349899)Time elapsed: 0.589 s % 54.34/8.73 % (3349899)Peak memory usage: 113 MB % 54.34/8.73 % (3349899)Instructions burned: 543 (million) % 54.34/8.73 % (3349909)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=1255411707:i=21611:sd=3:ss=axioms_2951 on theBenchmark for (2951ds/21611Mi) % 54.34/8.73 % (3349902)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 54.34/8.73 % (3349902)------------------------------ % 54.34/8.73 % (3349902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.34/8.73 % (3349902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.34/8.73 % (3349902)CaDiCaL version: 2.1.3 % 54.34/8.73 % (3349902)Termination reason: Unknown % 54.34/8.73 % (3349902)Termination phase: Saturation % 54.34/8.73 % (3349902)Time elapsed: 0.586 s % 54.34/8.73 % (3349902)Peak memory usage: 114 MB % 54.34/8.73 % (3349902)Instructions burned: 541 (million) % 54.34/8.73 % (3349911)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=254509742:i=4835:sd=13:ss=axioms:sgt=23_2949 on theBenchmark for (2949ds/4835Mi) % 61.93/10.01 % (3349909)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 61.93/10.01 % (3349909)------------------------------ % 61.93/10.01 % (3349909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.93/10.01 % (3349909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.93/10.01 % (3349909)CaDiCaL version: 2.1.3 % 61.93/10.01 % (3349909)Termination reason: Unknown % 61.93/10.01 % (3349909)Termination phase: Saturation % 61.93/10.01 % (3349909)Time elapsed: 0.282 s % 61.93/10.01 % (3349909)Peak memory usage: 113 MB % 61.93/10.01 % (3349909)Instructions burned: 539 (million) % 61.93/10.01 % (3349906)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 61.93/10.01 % (3349906)------------------------------ % 61.93/10.01 % (3349906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.93/10.01 % (3349906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.93/10.01 % (3349906)CaDiCaL version: 2.1.3 % 61.93/10.01 % (3349906)Termination reason: Unknown % 61.93/10.01 % (3349906)Termination phase: Saturation % 61.93/10.01 % (3349906)Time elapsed: 0.563 s % 61.93/10.01 % (3349906)Peak memory usage: 113 MB % 61.93/10.01 % (3349906)Instructions burned: 540 (million) % 61.93/10.01 % (3349915)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3747681562:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2946 on theBenchmark for (2946ds/2326Mi) % 61.93/10.01 % (3349913)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=1598628003:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2946 on theBenchmark for (2946ds/797Mi) % 61.93/10.01 % (3349916)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3240261972:i=6038:nm=6_2944 on theBenchmark for (2944ds/6038Mi) % 61.93/10.01 % (3349913)Instruction limit reached! % 61.93/10.01 % (3349913)------------------------------ % 61.93/10.01 % (3349913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.93/10.01 % (3349913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.93/10.01 % (3349913)CaDiCaL version: 2.1.3 % 61.93/10.01 % (3349913)Termination reason: Instruction limit % 61.93/10.01 % (3349913)Termination phase: Saturation % 61.93/10.01 % (3349913)Time elapsed: 0.753 s % 61.93/10.01 % (3349913)Peak memory usage: 103 MB % 61.93/10.01 % (3349913)Instructions burned: 797 (million) % 61.93/10.01 % (3349915)Instruction limit reached! % 61.93/10.01 % (3349915)------------------------------ % 61.93/10.01 % (3349915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.93/10.01 % (3349915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.93/10.01 % (3349915)CaDiCaL version: 2.1.3 % 61.93/10.01 % (3349915)Termination reason: Instruction limit % 61.93/10.01 % (3349915)Termination phase: Saturation % 61.93/10.01 % (3349915)Time elapsed: 0.765 s % 61.93/10.01 % (3349915)Peak memory usage: 103 MB % 61.93/10.01 % (3349915)Instructions burned: 2328 (million) % 61.93/10.01 % (3349916)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 61.93/10.01 % (3349916)------------------------------ % 61.93/10.01 % (3349916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.93/10.01 % (3349916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.93/10.01 % (3349916)CaDiCaL version: 2.1.3 % 61.93/10.01 % (3349916)Termination reason: Unknown % 61.93/10.01 % (3349916)Termination phase: Saturation % 61.93/10.01 % (3349916)Time elapsed: 0.569 s % 61.93/10.01 % (3349916)Peak memory usage: 113 MB % 61.93/10.01 % (3349916)Instructions burned: 541 (million) % 61.93/10.01 % (3349875)Instruction limit reached! % 61.93/10.01 % (3349875)------------------------------ % 61.93/10.01 % (3349875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.93/10.01 % (3349875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.93/10.01 % (3349875)CaDiCaL version: 2.1.3 % 61.93/10.01 % (3349875)Termination reason: Instruction limit % 61.93/10.01 % (3349875)Termination phase: Saturation % 61.93/10.01 % (3349875)Time elapsed: 3.448 s % 61.93/10.01 % (3349875)Peak memory usage: 112 MB % 61.93/10.01 % (3349875)Instructions burned: 3707 (million) % 61.93/10.01 % (3349923)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1456180093:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2936 on theBenchmark for (2936ds/1008Mi) % 71.77/11.05 % (3349922)lrs+10_1_sil=32000:sp=occurrence:random_seed=55427194:st=2:i=33334:sd=3:ss=included:sgt=32_2936 on theBenchmark for (2936ds/33334Mi) % 71.77/11.05 % (3349925)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=3443753177:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2935 on theBenchmark for (2935ds/1083Mi) % 71.77/11.05 % (3349924)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=2062682903:i=8327:s2at=5:bd=preordered_2935 on theBenchmark for (2935ds/8327Mi) % 71.77/11.05 % (3349865)Instruction limit reached! % 71.77/11.05 % (3349865)------------------------------ % 71.77/11.05 % (3349865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.77/11.05 % (3349865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.77/11.05 % (3349865)CaDiCaL version: 2.1.3 % 71.77/11.05 % (3349865)Termination reason: Instruction limit % 71.77/11.05 % (3349865)Termination phase: Saturation % 71.77/11.05 % (3349865)Time elapsed: 4.117 s % 71.77/11.05 % (3349865)Peak memory usage: 134 MB % 71.77/11.05 % (3349865)Instructions burned: 4850 (million) % 71.77/11.05 % (3349925)Instruction limit reached! % 71.77/11.05 % (3349925)------------------------------ % 71.77/11.05 % (3349925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.77/11.05 % (3349925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.77/11.05 % (3349925)CaDiCaL version: 2.1.3 % 71.77/11.05 % (3349925)Termination reason: Instruction limit % 71.77/11.05 % (3349925)Termination phase: Saturation % 71.77/11.05 % (3349925)Time elapsed: 0.430 s % 71.77/11.05 % (3349925)Peak memory usage: 96 MB % 71.77/11.05 % (3349925)Instructions burned: 1084 (million) % 71.77/11.05 % (3349930)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=4073893187:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2932 on theBenchmark for (2932ds/1084Mi) % 71.77/11.05 % (3349924)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 71.77/11.05 % (3349924)------------------------------ % 71.77/11.05 % (3349924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.77/11.05 % (3349924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.77/11.05 % (3349924)CaDiCaL version: 2.1.3 % 71.77/11.05 % (3349924)Termination reason: Unknown % 71.77/11.05 % (3349924)Termination phase: Saturation % 71.77/11.05 % (3349924)Time elapsed: 0.571 s % 71.77/11.05 % (3349924)Peak memory usage: 114 MB % 71.77/11.05 % (3349924)Instructions burned: 540 (million) % 71.77/11.05 % (3349932)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1290543795:i=6995:s2at=5:gtg=all_2929 on theBenchmark for (2929ds/6995Mi) % 71.77/11.05 % (3349923)Instruction limit reached! % 71.77/11.05 % (3349923)------------------------------ % 71.77/11.05 % (3349923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.77/11.05 % (3349923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.77/11.05 % (3349923)CaDiCaL version: 2.1.3 % 71.77/11.05 % (3349923)Termination reason: Instruction limit % 71.77/11.05 % (3349923)Termination phase: Saturation % 71.77/11.05 % (3349923)Time elapsed: 0.901 s % 71.77/11.05 % (3349923)Peak memory usage: 99 MB % 71.77/11.05 % (3349923)Instructions burned: 1008 (million) % 71.77/11.05 % (3349932)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 71.77/11.05 % (3349932)------------------------------ % 71.77/11.05 % (3349932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.77/11.05 % (3349932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.77/11.05 % (3349932)CaDiCaL version: 2.1.3 % 71.77/11.05 % (3349932)Termination reason: Unknown % 71.77/11.05 % (3349932)Termination phase: Saturation % 71.77/11.05 % (3349932)Time elapsed: 0.286 s % 71.77/11.05 % (3349932)Peak memory usage: 114 MB % 71.77/11.05 % (3349932)Instructions burned: 543 (million) % 71.77/11.05 % (3349934)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=221183168:st=2:i=6225:sd=15:ss=axioms_2927 on theBenchmark for (2927ds/6225Mi) % 71.77/11.05 % (3349935)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=847158158:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2925 on theBenchmark for (2925ds/3372Mi) % 75.96/11.89 % (3349936)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2932207272:st=2.3:i=26457:sd=10:ss=included:sgt=8_2924 on theBenchmark for (2924ds/26457Mi) % 75.96/11.89 % (3349936)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.96/11.89 % (3349936)------------------------------ % 75.96/11.89 % (3349936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.96/11.89 % (3349936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.96/11.89 % (3349936)CaDiCaL version: 2.1.3 % 75.96/11.89 % (3349936)Termination reason: Unknown % 75.96/11.89 % (3349936)Termination phase: Saturation % 75.96/11.89 % (3349936)Time elapsed: 0.283 s % 75.96/11.89 % (3349936)Peak memory usage: 113 MB % 75.96/11.89 % (3349936)Instructions burned: 541 (million) % 75.96/11.89 % (3349930)Instruction limit reached! % 75.96/11.89 % (3349930)------------------------------ % 75.96/11.89 % (3349930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.96/11.89 % (3349930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.96/11.89 % (3349930)CaDiCaL version: 2.1.3 % 75.96/11.89 % (3349930)Termination reason: Instruction limit % 75.96/11.89 % (3349930)Termination phase: Saturation % 75.96/11.89 % (3349930)Time elapsed: 1.038 s % 75.96/11.89 % (3349930)Peak memory usage: 97 MB % 75.96/11.89 % (3349930)Instructions burned: 1084 (million) % 75.96/11.89 % (3349940)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=1689688698:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2919 on theBenchmark for (2919ds/13494Mi) % 75.96/11.89 % (3349935)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.96/11.89 % (3349935)------------------------------ % 75.96/11.89 % (3349935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.96/11.89 % (3349935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.96/11.89 % (3349935)CaDiCaL version: 2.1.3 % 75.96/11.89 % (3349935)Termination reason: Unknown % 75.96/11.89 % (3349935)Termination phase: Saturation % 75.96/11.89 % (3349935)Time elapsed: 0.591 s % 75.96/11.89 % (3349935)Peak memory usage: 113 MB % 75.96/11.89 % (3349935)Instructions burned: 540 (million) % 75.96/11.89 % (3349941)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=977633235:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2919 on theBenchmark for (2919ds/2503Mi) % 75.96/11.89 % (3349941)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 75.96/11.89 % (3349940)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.96/11.89 % (3349940)------------------------------ % 75.96/11.89 % (3349940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.96/11.89 % (3349940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.96/11.89 % (3349940)CaDiCaL version: 2.1.3 % 75.96/11.89 % (3349940)Termination reason: Unknown % 75.96/11.89 % (3349940)Termination phase: Saturation % 75.96/11.89 % (3349940)Time elapsed: 0.276 s % 75.96/11.89 % (3349940)Peak memory usage: 114 MB % 75.96/11.89 % (3349940)Instructions burned: 542 (million) % 75.96/11.89 % (3349943)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=814407324:i=2559:sd=1:ep=RSTC:ss=axioms_2916 on theBenchmark for (2916ds/2559Mi) % 75.96/11.89 % (3349950)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4289965398:i=30753:av=off:ss=included_2914 on theBenchmark for (2914ds/30753Mi) % 75.96/11.89 % (3349941)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.96/11.89 % (3349941)------------------------------ % 75.96/11.89 % (3349941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.96/11.89 % (3349941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.96/11.89 % (3349941)CaDiCaL version: 2.1.3 % 75.96/11.89 % (3349941)Termination reason: Unknown % 75.96/11.89 % (3349941)Termination phase: Saturation % 75.96/11.89 % (3349941)Time elapsed: 0.592 s % 75.96/11.89 % (3349941)Peak memory usage: 113 MB % 75.96/11.89 % (3349941)Instructions burned: 539 (million) % 75.96/11.89 % (3349950)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.96/11.89 % (3349950)------------------------------ % 75.96/11.89 % (3349950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.97/12.83 % (3349950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.97/12.83 % (3349950)CaDiCaL version: 2.1.3 % 78.97/12.83 % (3349950)Termination reason: Unknown % 78.97/12.83 % (3349950)Termination phase: Saturation % 78.97/12.83 % (3349950)Time elapsed: 0.318 s % 78.97/12.83 % (3349950)Peak memory usage: 114 MB % 78.97/12.83 % (3349950)Instructions burned: 541 (million) % 78.97/12.83 % (3349943)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 78.97/12.83 % (3349943)------------------------------ % 78.97/12.83 % (3349943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.97/12.83 % (3349943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.97/12.83 % (3349943)CaDiCaL version: 2.1.3 % 78.97/12.83 % (3349943)Termination reason: Unknown % 78.97/12.83 % (3349943)Termination phase: Saturation % 78.97/12.83 % (3349943)Time elapsed: 0.588 s % 78.97/12.83 % (3349943)Peak memory usage: 113 MB % 78.97/12.83 % (3349943)Instructions burned: 539 (million) % 78.97/12.83 % (3349956)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3539394317:i=26473:ep=RSTC_2910 on theBenchmark for (2910ds/26473Mi) % 78.97/12.83 % (3349957)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=294231775:cts=off:i=2759:kws=inv_arity:fgj=on_2909 on theBenchmark for (2909ds/2759Mi) % 78.97/12.83 % (3349958)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=1476423671:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2907 on theBenchmark for (2907ds/5665Mi) % 78.97/12.83 % (3349958)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 78.97/12.83 % (3349957)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 78.97/12.83 % (3349957)------------------------------ % 78.97/12.83 % (3349957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.97/12.83 % (3349957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.97/12.83 % (3349957)CaDiCaL version: 2.1.3 % 78.97/12.83 % (3349957)Termination reason: Unknown % 78.97/12.83 % (3349957)Termination phase: Saturation % 78.97/12.83 % (3349957)Time elapsed: 0.321 s % 78.97/12.83 % (3349957)Peak memory usage: 114 MB % 78.97/12.83 % (3349957)Instructions burned: 542 (million) % 78.97/12.83 % (3349911)Instruction limit reached! % 78.97/12.83 % (3349911)------------------------------ % 78.97/12.83 % (3349911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.97/12.83 % (3349911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.97/12.83 % (3349911)CaDiCaL version: 2.1.3 % 78.97/12.83 % (3349911)Termination reason: Instruction limit % 78.97/12.83 % (3349911)Termination phase: Saturation % 78.97/12.83 % (3349911)Time elapsed: 4.329 s % 78.97/12.83 % (3349911)Peak memory usage: 111 MB % 78.97/12.83 % (3349911)Instructions burned: 4835 (million) % 78.97/12.83 % (3349962)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=2837477587:i=1532:ep=RS:ss=axioms_2904 on theBenchmark for (2904ds/1532Mi) % 78.97/12.83 % (3349897)Instruction limit reached! % 78.97/12.83 % (3349897)------------------------------ % 78.97/12.83 % (3349897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.97/12.83 % (3349897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.97/12.83 % (3349897)CaDiCaL version: 2.1.3 % 78.97/12.83 % (3349897)Termination reason: Instruction limit % 78.97/12.83 % (3349897)Termination phase: Saturation % 78.97/12.83 % (3349897)Time elapsed: 5.483 s % 78.97/12.83 % (3349897)Peak memory usage: 126 MB % 78.97/12.83 % (3349897)Instructions burned: 5781 (million) % 78.97/12.83 % (3349963)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2612233444:i=1565:sd=2:ss=axioms:sgt=32_2902 on theBenchmark for (2902ds/1565Mi) % 78.97/12.83 % (3349958)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 78.97/12.83 % (3349958)------------------------------ % 78.97/12.83 % (3349958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 78.97/12.83 % (3349958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.53/13.54 % (3349958)CaDiCaL version: 2.1.3 % 88.53/13.54 % (3349958)Termination reason: Unknown % 88.53/13.54 % (3349958)Termination phase: Saturation % 88.53/13.54 % (3349958)Time elapsed: 0.582 s % 88.53/13.54 % (3349958)Peak memory usage: 113 MB % 88.53/13.54 % (3349958)Instructions burned: 540 (million) % 88.53/13.54 % (3349965)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=2996868841:i=1572:fgj=on:gsp=on_2901 on theBenchmark for (2901ds/1572Mi) % 88.53/13.54 % (3349965)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 88.53/13.54 % (3349962)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 88.53/13.54 % (3349962)------------------------------ % 88.53/13.54 % (3349962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.53/13.54 % (3349962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.53/13.54 % (3349962)CaDiCaL version: 2.1.3 % 88.53/13.54 % (3349962)Termination reason: Unknown % 88.53/13.54 % (3349962)Termination phase: Saturation % 88.53/13.54 % (3349962)Time elapsed: 0.316 s % 88.53/13.54 % (3349962)Peak memory usage: 114 MB % 88.53/13.54 % (3349962)Instructions burned: 542 (million) % 88.53/13.54 % (3349967)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1579458531:i=6052:sd=4:ss=axioms:sgt=24_2899 on theBenchmark for (2899ds/6052Mi) % 88.53/13.54 % (3349969)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=679659383:i=3500:sd=1:bd=preordered:sup=off:ss=included_2898 on theBenchmark for (2898ds/3500Mi) % 88.53/13.54 % (3349963)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 88.53/13.54 % (3349963)------------------------------ % 88.53/13.54 % (3349963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.53/13.54 % (3349963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.53/13.54 % (3349963)CaDiCaL version: 2.1.3 % 88.53/13.54 % (3349963)Termination reason: Unknown % 88.53/13.54 % (3349963)Termination phase: Saturation % 88.53/13.54 % (3349963)Time elapsed: 0.589 s % 88.53/13.54 % (3349963)Peak memory usage: 114 MB % 88.53/13.54 % (3349963)Instructions burned: 541 (million) % 88.53/13.54 % (3349969)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 88.53/13.54 % (3349969)------------------------------ % 88.53/13.54 % (3349969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.53/13.54 % (3349969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.53/13.54 % (3349969)CaDiCaL version: 2.1.3 % 88.53/13.54 % (3349969)Termination reason: Unknown % 88.53/13.54 % (3349969)Termination phase: Saturation % 88.53/13.54 % (3349969)Time elapsed: 0.315 s % 88.53/13.54 % (3349969)Peak memory usage: 113 MB % 88.53/13.54 % (3349969)Instructions burned: 542 (million) % 88.53/13.54 % (3349965)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 88.53/13.54 % (3349965)------------------------------ % 88.53/13.54 % (3349965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.53/13.54 % (3349965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.53/13.54 % (3349965)CaDiCaL version: 2.1.3 % 88.53/13.54 % (3349965)Termination reason: Unknown % 88.53/13.54 % (3349965)Termination phase: Saturation % 88.53/13.54 % (3349965)Time elapsed: 0.586 s % 88.53/13.54 % (3349965)Peak memory usage: 114 MB % 88.53/13.54 % (3349965)Instructions burned: 540 (million) % 88.53/13.54 % (3349974)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=3827020368:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2894 on theBenchmark for (2894ds/1842Mi) % 88.53/13.54 % (3349974)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 88.53/13.54 % (3349975)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=243697559:i=66096:add=on_2893 on theBenchmark for (2893ds/66096Mi) % 88.53/13.54 % (3349967)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 88.53/13.54 % (3349967)------------------------------ % 88.53/13.54 % (3349967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.53/13.54 % (3349967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.02/14.22 % (3349967)CaDiCaL version: 2.1.3 % 94.02/14.22 % (3349967)Termination reason: Unknown % 94.02/14.22 % (3349967)Termination phase: Saturation % 94.02/14.22 % (3349967)Time elapsed: 0.601 s % 94.02/14.22 % (3349967)Peak memory usage: 113 MB % 94.02/14.22 % (3349967)Instructions burned: 540 (million) % 94.02/14.22 % (3349976)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2788745970:i=1884:sd=1:nm=60:ss=axioms_2892 on theBenchmark for (2892ds/1884Mi) % 94.02/14.22 % (3349975)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 94.02/14.22 % (3349975)------------------------------ % 94.02/14.22 % (3349975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.02/14.22 % (3349975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.02/14.22 % (3349975)CaDiCaL version: 2.1.3 % 94.02/14.22 % (3349975)Termination reason: Unknown % 94.02/14.22 % (3349975)Termination phase: Saturation % 94.02/14.22 % (3349975)Time elapsed: 0.316 s % 94.02/14.22 % (3349975)Peak memory usage: 113 MB % 94.02/14.22 % (3349975)Instructions burned: 541 (million) % 94.02/14.22 % (3349979)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2008557485:cts=off:i=5469:bs=on:fsr=off_2890 on theBenchmark for (2890ds/5469Mi) % 94.02/14.22 % (3349981)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=59150023:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2888 on theBenchmark for (2888ds/2037Mi) % 94.02/14.22 % (3349974)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 94.02/14.22 % (3349974)------------------------------ % 94.02/14.22 % (3349974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.02/14.22 % (3349974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.02/14.22 % (3349974)CaDiCaL version: 2.1.3 % 94.02/14.22 % (3349974)Termination reason: Unknown % 94.02/14.22 % (3349974)Termination phase: Saturation % 94.02/14.22 % (3349974)Time elapsed: 0.593 s % 94.02/14.22 % (3349974)Peak memory usage: 113 MB % 94.02/14.22 % (3349974)Instructions burned: 541 (million) % 94.02/14.22 % (3349976)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 94.02/14.22 % (3349976)------------------------------ % 94.02/14.22 % (3349976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.02/14.22 % (3349976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.02/14.22 % (3349976)CaDiCaL version: 2.1.3 % 94.02/14.22 % (3349976)Termination reason: Unknown % 94.02/14.22 % (3349976)Termination phase: Saturation % 94.02/14.22 % (3349976)Time elapsed: 0.593 s % 94.02/14.22 % (3349976)Peak memory usage: 113 MB % 94.02/14.22 % (3349976)Instructions burned: 538 (million) % 94.02/14.22 % (3349984)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2125887891:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2885 on theBenchmark for (2885ds/2110Mi) % 94.02/14.22 % (3349981)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 94.02/14.22 % (3349981)------------------------------ % 94.02/14.22 % (3349981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.02/14.22 % (3349981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.02/14.22 % (3349981)CaDiCaL version: 2.1.3 % 94.02/14.22 % (3349981)Termination reason: Unknown % 94.02/14.22 % (3349981)Termination phase: Saturation % 94.02/14.22 % (3349981)Time elapsed: 0.315 s % 94.02/14.22 % (3349981)Peak memory usage: 114 MB % 94.02/14.22 % (3349981)Instructions burned: 546 (million) % 94.02/14.22 % (3349934)Instruction limit reached! % 94.02/14.22 % (3349934)------------------------------ % 94.02/14.22 % (3349934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 94.02/14.22 % (3349934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 94.02/14.22 % (3349934)CaDiCaL version: 2.1.3 % 94.02/14.22 % (3349934)Termination reason: Instruction limit % 94.02/14.22 % (3349934)Termination phase: Saturation % 94.02/14.22 % (3349934)Time elapsed: 4.253 s % 94.02/14.22 % (3349934)Peak memory usage: 98 MB % 94.02/14.22 % (3349934)Instructions burned: 6226 (million) % 94.02/14.22 % (3349985)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=289395420:i=2430:add=off:aac=none:nm=16_2884 on theBenchmark for (2884ds/2430Mi) % 96.53/14.76 % (3349987)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=3587072922:cond=fast:i=4891_2882 on theBenchmark for (2882ds/4891Mi) % 96.53/14.76 % (3349988)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=3996334786:st=2:i=14845:sd=2:ss=included:fsd=on_2881 on theBenchmark for (2881ds/14845Mi) % 96.53/14.76 % (3349984)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 96.53/14.76 % (3349984)------------------------------ % 96.53/14.76 % (3349984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.53/14.76 % (3349984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.53/14.76 % (3349984)CaDiCaL version: 2.1.3 % 96.53/14.76 % (3349984)Termination reason: Unknown % 96.53/14.76 % (3349984)Termination phase: Saturation % 96.53/14.76 % (3349984)Time elapsed: 0.571 s % 96.53/14.76 % (3349984)Peak memory usage: 114 MB % 96.53/14.76 % (3349984)Instructions burned: 544 (million) % 96.53/14.76 % (3349987)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 96.53/14.76 % (3349987)------------------------------ % 96.53/14.76 % (3349987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.53/14.76 % (3349987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.53/14.76 % (3349987)CaDiCaL version: 2.1.3 % 96.53/14.76 % (3349987)Termination reason: Unknown % 96.53/14.76 % (3349987)Termination phase: Saturation % 96.53/14.76 % (3349987)Time elapsed: 0.308 s % 96.53/14.76 % (3349987)Peak memory usage: 114 MB % 96.53/14.76 % (3349987)Instructions burned: 541 (million) % 96.53/14.76 % (3349985)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 96.53/14.76 % (3349985)------------------------------ % 96.53/14.76 % (3349985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.53/14.76 % (3349985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.53/14.76 % (3349985)CaDiCaL version: 2.1.3 % 96.53/14.76 % (3349985)Termination reason: Unknown % 96.53/14.76 % (3349985)Termination phase: Saturation % 96.53/14.76 % (3349985)Time elapsed: 0.518 s % 96.53/14.76 % (3349985)Peak memory usage: 114 MB % 96.53/14.76 % (3349985)Instructions burned: 541 (million) % 96.53/14.76 % (3349996)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=4137646735:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2877 on theBenchmark for (2877ds/10353Mi) % 96.53/14.76 % (3349995)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=1569910152:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2877 on theBenchmark for (2877ds/7534Mi) % 96.53/14.76 % (3349988)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 96.53/14.76 % (3349988)------------------------------ % 96.53/14.76 % (3349988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.53/14.76 % (3349988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.53/14.76 % (3349988)CaDiCaL version: 2.1.3 % 96.53/14.76 % (3349988)Termination reason: Unknown % 96.53/14.76 % (3349988)Termination phase: Saturation % 96.53/14.76 % (3349988)Time elapsed: 0.396 s % 96.53/14.76 % (3349988)Peak memory usage: 114 MB % 96.53/14.76 % (3349988)Instructions burned: 541 (million) % 96.53/14.76 % (3349998)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1659580932:i=7860_2876 on theBenchmark for (2876ds/7860Mi) % 96.53/14.76 % (3349998)Refutation not found, incomplete strategy % 96.53/14.76 % (3349998)------------------------------ % 96.53/14.76 % (3349998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.53/14.76 % (3349998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.53/14.76 % (3349998)CaDiCaL version: 2.1.3 % 96.53/14.76 % (3349998)Termination reason: Refutation not found, incomplete strategy % 96.53/14.76 % (3349998)Time elapsed: 0.006 s % 96.53/14.76 % (3349998)Peak memory usage: 88 MB % 96.53/14.76 % (3349998)Instructions burned: 9 (million) % 96.53/14.76 % (3349996)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 96.53/14.76 % (3349996)------------------------------ % 96.53/14.76 % (3349996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.53/14.76 % (3349996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.54/15.34 % (3349996)CaDiCaL version: 2.1.3 % 101.54/15.34 % (3349996)Termination reason: Unknown % 101.54/15.34 % (3349996)Termination phase: Saturation % 101.54/15.34 % (3349996)Time elapsed: 0.196 s % 101.54/15.34 % (3349996)Peak memory usage: 114 MB % 101.54/15.34 % (3349996)Instructions burned: 540 (million) % 101.54/15.34 % (3350032)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=1771134372:i=7896:sd=2:bs=on:ss=included:sgt=20_2874 on theBenchmark for (2874ds/7896Mi) % 101.54/15.34 % (3350049)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=83583799:i=5812:gtgl=2:gtg=all_2874 on theBenchmark for (2874ds/5812Mi) % 101.54/15.34 % (3349995)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 101.54/15.34 % (3349995)------------------------------ % 101.54/15.34 % (3349995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.54/15.34 % (3349995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.54/15.34 % (3349995)CaDiCaL version: 2.1.3 % 101.54/15.34 % (3349995)Termination reason: Unknown % 101.54/15.34 % (3349995)Termination phase: Saturation % 101.54/15.34 % (3349995)Time elapsed: 0.361 s % 101.54/15.34 % (3349995)Peak memory usage: 114 MB % 101.54/15.34 % (3349995)Instructions burned: 543 (million) % 101.54/15.34 % (3349998)------------------------------ % 101.54/15.34 % (3349998)------------------------------ % 101.54/15.34 % (3350032)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 101.54/15.34 % (3350032)------------------------------ % 101.54/15.34 % (3350032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.54/15.34 % (3350032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.54/15.34 % (3350032)CaDiCaL version: 2.1.3 % 101.54/15.34 % (3350032)Termination reason: Unknown % 101.54/15.34 % (3350032)Termination phase: Saturation % 101.54/15.34 % (3350032)Time elapsed: 0.195 s % 101.54/15.34 % (3350032)Peak memory usage: 113 MB % 101.54/15.34 % (3350032)Instructions burned: 540 (million) % 101.54/15.34 % (3350071)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=1361254921:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2872 on theBenchmark for (2872ds/2965Mi) % 101.54/15.34 % (3350072)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=3849828748:i=2967:kws=precedence:bd=preordered:av=off_2871 on theBenchmark for (2871ds/2967Mi) % 101.54/15.34 % (3350079)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=2010398154:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2871 on theBenchmark for (2871ds/3022Mi) % 101.54/15.34 % (3350049)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 101.54/15.34 % (3350049)------------------------------ % 101.54/15.34 % (3350049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.54/15.34 % (3350049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.54/15.34 % (3350049)CaDiCaL version: 2.1.3 % 101.54/15.34 % (3350049)Termination reason: Unknown % 101.54/15.34 % (3350049)Termination phase: Saturation % 101.54/15.34 % (3350049)Time elapsed: 0.364 s % 101.54/15.34 % (3350049)Peak memory usage: 114 MB % 101.54/15.34 % (3350049)Instructions burned: 544 (million) % 101.54/15.34 % (3350079)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 101.54/15.34 % (3350079)------------------------------ % 101.54/15.34 % (3350079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.54/15.34 % (3350079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.54/15.34 % (3350079)CaDiCaL version: 2.1.3 % 101.54/15.34 % (3350079)Termination reason: Unknown % 101.54/15.34 % (3350079)Termination phase: Saturation % 101.54/15.34 % (3350079)Time elapsed: 0.193 s % 101.54/15.34 % (3350079)Peak memory usage: 113 MB % 101.54/15.34 % (3350079)Instructions burned: 540 (million) % 101.54/15.34 % (3350092)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=632449642:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2869 on theBenchmark for (2869ds/3207Mi) % 107.87/16.17 % (3350071)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 107.87/16.17 % (3350071)------------------------------ % 107.87/16.17 % (3350071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.87/16.17 % (3350071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.87/16.17 % (3350071)CaDiCaL version: 2.1.3 % 107.87/16.17 % (3350071)Termination reason: Unknown % 107.87/16.17 % (3350071)Termination phase: Saturation % 107.87/16.17 % (3350071)Time elapsed: 0.359 s % 107.87/16.17 % (3350071)Peak memory usage: 114 MB % 107.87/16.17 % (3350071)Instructions burned: 540 (million) % 107.87/16.17 % (3350108)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1887868:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2868 on theBenchmark for (2868ds/3289Mi) % 107.87/16.17 % (3350072)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 107.87/16.17 % (3350072)------------------------------ % 107.87/16.17 % (3350072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.87/16.17 % (3350072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.87/16.17 % (3350072)CaDiCaL version: 2.1.3 % 107.87/16.17 % (3350072)Termination reason: Unknown % 107.87/16.17 % (3350072)Termination phase: Saturation % 107.87/16.17 % (3350072)Time elapsed: 0.359 s % 107.87/16.17 % (3350072)Peak memory usage: 114 MB % 107.87/16.17 % (3350072)Instructions burned: 541 (million) % 107.87/16.17 % (3350120)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2154097727:i=38569:sd=3:ss=axioms:sgt=32_2867 on theBenchmark for (2867ds/38569Mi) % 107.87/16.17 % (3350108)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 107.87/16.17 % (3350108)------------------------------ % 107.87/16.17 % (3350108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.87/16.17 % (3350108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.87/16.17 % (3350108)CaDiCaL version: 2.1.3 % 107.87/16.17 % (3350108)Termination reason: Unknown % 107.87/16.17 % (3350108)Termination phase: Saturation % 107.87/16.17 % (3350108)Time elapsed: 0.197 s % 107.87/16.17 % (3350108)Peak memory usage: 113 MB % 107.87/16.17 % (3350108)Instructions burned: 542 (million) % 107.87/16.17 % (3350127)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=955966189:cts=off:i=3394_2866 on theBenchmark for (2866ds/3394Mi) % 107.87/16.17 % (3350172)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=2567969663:i=33824:bd=preordered_2865 on theBenchmark for (2865ds/33824Mi) % 107.87/16.17 % (3350092)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 107.87/16.17 % (3350092)------------------------------ % 107.87/16.17 % (3350092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.87/16.17 % (3350092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.87/16.17 % (3350092)CaDiCaL version: 2.1.3 % 107.87/16.17 % (3350092)Termination reason: Unknown % 107.87/16.17 % (3350092)Termination phase: Saturation % 107.87/16.17 % (3350092)Time elapsed: 0.361 s % 107.87/16.17 % (3350092)Peak memory usage: 114 MB % 107.87/16.17 % (3350092)Instructions burned: 540 (million) % 107.87/16.17 % (3350174)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=512745292:i=20684:bd=all:gtg=exists_sym_2863 on theBenchmark for (2863ds/20684Mi) % 107.87/16.17 % (3350120)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 107.87/16.17 % (3350120)------------------------------ % 107.87/16.17 % (3350120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.87/16.17 % (3350120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.87/16.17 % (3350120)CaDiCaL version: 2.1.3 % 107.87/16.17 % (3350120)Termination reason: Unknown % 107.87/16.17 % (3350120)Termination phase: Saturation % 107.87/16.17 % (3350120)Time elapsed: 0.361 s % 107.87/16.17 % (3350120)Peak memory usage: 113 MB % 107.87/16.17 % (3350120)Instructions burned: 541 (million) % 107.87/16.17 % (3350172)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 107.87/16.17 % (3350172)------------------------------ % 107.87/16.17 % (3350172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.87/16.17 % (3350172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.87/16.17 % (3350172)CaDiCaL version: 2.1.3 % 111.14/16.85 % (3350172)Termination reason: Unknown % 111.14/16.85 % (3350172)Termination phase: Saturation % 111.14/16.85 % (3350172)Time elapsed: 0.194 s % 111.14/16.85 % (3350172)Peak memory usage: 114 MB % 111.14/16.85 % (3350172)Instructions burned: 541 (million) % 111.14/16.85 % (3350127)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.14/16.85 % (3350127)------------------------------ % 111.14/16.85 % (3350127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.14/16.85 % (3350127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/16.85 % (3350127)CaDiCaL version: 2.1.3 % 111.14/16.85 % (3350127)Termination reason: Unknown % 111.14/16.85 % (3350127)Termination phase: Saturation % 111.14/16.85 % (3350127)Time elapsed: 0.359 s % 111.14/16.85 % (3350127)Peak memory usage: 113 MB % 111.14/16.85 % (3350127)Instructions burned: 541 (million) % 111.14/16.85 % (3350176)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=1247898632: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_2862 on theBenchmark for (2862ds/7222Mi) % 111.14/16.85 % (3350177)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2106513566:st=4:i=7295:sd=4:ep=R:ss=axioms_2862 on theBenchmark for (2862ds/7295Mi) % 111.14/16.85 % (3350176)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 111.14/16.85 % (3350178)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=2881253167:i=4036:ins=10_2861 on theBenchmark for (2861ds/4036Mi) % 111.14/16.85 % (3350176)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.14/16.85 % (3350176)------------------------------ % 111.14/16.85 % (3350176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.14/16.85 % (3350176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/16.85 % (3350176)CaDiCaL version: 2.1.3 % 111.14/16.85 % (3350176)Termination reason: Unknown % 111.14/16.85 % (3350176)Termination phase: Saturation % 111.14/16.85 % (3350176)Time elapsed: 0.194 s % 111.14/16.85 % (3350176)Peak memory usage: 114 MB % 111.14/16.85 % (3350176)Instructions burned: 545 (million) % 111.14/16.85 % (3350174)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.14/16.85 % (3350174)------------------------------ % 111.14/16.85 % (3350174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.14/16.85 % (3350174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/16.85 % (3350174)CaDiCaL version: 2.1.3 % 111.14/16.85 % (3350174)Termination reason: Unknown % 111.14/16.85 % (3350174)Termination phase: Saturation % 111.14/16.85 % (3350174)Time elapsed: 0.359 s % 111.14/16.85 % (3350174)Peak memory usage: 114 MB % 111.14/16.85 % (3350174)Instructions burned: 543 (million) % 111.14/16.85 % (3350182)lrs+10_1_sil=128000:lcm=predicate:random_seed=3238154417:st=3:i=43697:sd=5:ss=axioms_2858 on theBenchmark for (2858ds/43697Mi) % 111.14/16.85 % (3350177)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.14/16.85 % (3350177)------------------------------ % 111.14/16.85 % (3350177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.14/16.85 % (3350177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/16.85 % (3350177)CaDiCaL version: 2.1.3 % 111.14/16.85 % (3350177)Termination reason: Unknown % 111.14/16.85 % (3350177)Termination phase: Saturation % 111.14/16.85 % (3350177)Time elapsed: 0.361 s % 111.14/16.85 % (3350177)Peak memory usage: 114 MB % 111.14/16.85 % (3350177)Instructions burned: 543 (million) % 111.14/16.85 % (3350183)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=2534449127:i=17599:gtg=all:ss=axioms:fsd=on_2858 on theBenchmark for (2858ds/17599Mi) % 111.14/16.85 % (3350178)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.14/16.85 % (3350178)------------------------------ % 111.14/16.85 % (3350178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.14/16.85 % (3350178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.14/16.85 % (3350178)CaDiCaL version: 2.1.3 % 111.14/16.85 % (3350178)Termination reason: Unknown % 118.77/17.89 % (3350178)Termination phase: Saturation % 118.77/17.89 % (3350178)Time elapsed: 0.360 s % 118.77/17.89 % (3350178)Peak memory usage: 113 MB % 118.77/17.89 % (3350178)Instructions burned: 540 (million) % 118.77/17.89 % (3350186)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=3543819327:i=4547:bd=preordered_2857 on theBenchmark for (2857ds/4547Mi) % 118.77/17.89 % (3350187)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=3328860849:i=9294:av=off_2856 on theBenchmark for (2856ds/9294Mi) % 118.77/17.89 % (3350183)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 118.77/17.89 % (3350183)------------------------------ % 118.77/17.89 % (3350183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.77/17.89 % (3350183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.77/17.89 % (3350183)CaDiCaL version: 2.1.3 % 118.77/17.89 % (3350183)Termination reason: Unknown % 118.77/17.89 % (3350183)Termination phase: Saturation % 118.77/17.89 % (3350183)Time elapsed: 0.360 s % 118.77/17.89 % (3350183)Peak memory usage: 114 MB % 118.77/17.89 % (3350183)Instructions burned: 542 (million) % 118.77/17.89 % (3350186)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 118.77/17.89 % (3350186)------------------------------ % 118.77/17.89 % (3350186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.77/17.89 % (3350186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.77/17.89 % (3350186)CaDiCaL version: 2.1.3 % 118.77/17.89 % (3350186)Termination reason: Unknown % 118.77/17.89 % (3350186)Termination phase: Saturation % 118.77/17.89 % (3350186)Time elapsed: 0.358 s % 118.77/17.89 % (3350186)Peak memory usage: 114 MB % 118.77/17.89 % (3350186)Instructions burned: 541 (million) % 118.77/17.89 % (3350190)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=996323008:i=32849:add=on_2853 on theBenchmark for (2853ds/32849Mi) % 118.77/17.89 % (3349979)Instruction limit reached! % 118.77/17.89 % (3349979)------------------------------ % 118.77/17.89 % (3349979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.77/17.89 % (3349979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.77/17.89 % (3349979)CaDiCaL version: 2.1.3 % 118.77/17.89 % (3349979)Termination reason: Instruction limit % 118.77/17.89 % (3349979)Termination phase: Saturation % 118.77/17.89 % (3349979)Time elapsed: 3.627 s % 118.77/17.89 % (3349979)Peak memory usage: 115 MB % 118.77/17.89 % (3349979)Instructions burned: 5470 (million) % 118.77/17.89 % (3350187)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 118.77/17.89 % (3350187)------------------------------ % 118.77/17.89 % (3350187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.77/17.89 % (3350187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.77/17.89 % (3350187)CaDiCaL version: 2.1.3 % 118.77/17.89 % (3350187)Termination reason: Unknown % 118.77/17.89 % (3350187)Termination phase: Saturation % 118.77/17.89 % (3350187)Time elapsed: 0.358 s % 118.77/17.89 % (3350187)Peak memory usage: 114 MB % 118.77/17.89 % (3350187)Instructions burned: 541 (million) % 118.77/17.89 % (3350191)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2718152730:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2851 on theBenchmark for (2851ds/4793Mi) % 118.77/17.89 % (3350193)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=1649531585:i=4840:nm=4:av=off_2851 on theBenchmark for (2851ds/4840Mi) % 118.77/17.89 % (3350194)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=3291119828:cts=off:i=5002_2851 on theBenchmark for (2851ds/5002Mi) % 118.77/17.89 % (3350190)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 118.77/17.89 % (3350190)------------------------------ % 118.77/17.89 % (3350190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.77/17.89 % (3350190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.77/17.89 % (3350190)CaDiCaL version: 2.1.3 % 118.77/17.89 % (3350190)Termination reason: Unknown % 118.77/17.89 % (3350190)Termination phase: Saturation % 118.77/17.89 % (3350190)Time elapsed: 0.363 s % 148.33/21.97 % (3350190)Peak memory usage: 113 MB % 148.33/21.97 % (3350190)Instructions burned: 541 (million) % 148.33/21.97 % (3350191)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 148.33/21.97 % (3350191)------------------------------ % 148.33/21.97 % (3350191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.33/21.97 % (3350191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.33/21.97 % (3350191)CaDiCaL version: 2.1.3 % 148.33/21.97 % (3350191)Termination reason: Unknown % 148.33/21.97 % (3350191)Termination phase: Saturation % 148.33/21.97 % (3350191)Time elapsed: 0.359 s % 148.33/21.97 % (3350191)Peak memory usage: 113 MB % 148.33/21.97 % (3350191)Instructions burned: 541 (million) % 148.33/21.97 % (3350198)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=3975734902:i=30479:sd=3:ss=axioms_2848 on theBenchmark for (2848ds/30479Mi) % 148.33/21.97 % (3350193)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 148.33/21.97 % (3350193)------------------------------ % 148.33/21.97 % (3350193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.33/21.97 % (3350193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.33/21.97 % (3350193)CaDiCaL version: 2.1.3 % 148.33/21.97 % (3350193)Termination reason: Unknown % 148.33/21.97 % (3350193)Termination phase: Saturation % 148.33/21.97 % (3350193)Time elapsed: 0.357 s % 148.33/21.97 % (3350193)Peak memory usage: 114 MB % 148.33/21.97 % (3350193)Instructions burned: 541 (million) % 148.33/21.97 % (3350194)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 148.33/21.97 % (3350194)------------------------------ % 148.33/21.97 % (3350194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.33/21.97 % (3350194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.33/21.97 % (3350194)CaDiCaL version: 2.1.3 % 148.33/21.97 % (3350194)Termination reason: Unknown % 148.33/21.97 % (3350194)Termination phase: Saturation % 148.33/21.97 % (3350194)Time elapsed: 0.357 s % 148.33/21.97 % (3350194)Peak memory usage: 114 MB % 148.33/21.97 % (3350194)Instructions burned: 540 (million) % 148.33/21.97 % (3350199)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=1069071618:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2846 on theBenchmark for (2846ds/11035Mi) % 148.33/21.97 % (3350199)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 148.33/21.97 % (3350201)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=478791089:i=5835_2846 on theBenchmark for (2846ds/5835Mi) % 148.33/21.97 % (3350202)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2155122166:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2846 on theBenchmark for (2846ds/5890Mi) % 148.33/21.97 % (3350198)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 148.33/21.97 % (3350198)------------------------------ % 148.33/21.97 % (3350198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.33/21.97 % (3350198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.33/21.97 % (3350198)CaDiCaL version: 2.1.3 % 148.33/21.97 % (3350198)Termination reason: Unknown % 148.33/21.97 % (3350198)Termination phase: Saturation % 148.33/21.97 % (3350198)Time elapsed: 0.362 s % 148.33/21.97 % (3350198)Peak memory usage: 113 MB % 148.33/21.97 % (3350198)Instructions burned: 539 (million) % 148.33/21.97 % (3350199)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 148.33/21.97 % (3350199)------------------------------ % 148.33/21.97 % (3350199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.33/21.97 % (3350199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.33/21.97 % (3350199)CaDiCaL version: 2.1.3 % 148.33/21.97 % (3350199)Termination reason: Unknown % 148.33/21.97 % (3350199)Termination phase: Saturation % 148.33/21.97 % (3350199)Time elapsed: 0.359 s % 148.33/21.97 % (3350199)Peak memory usage: 114 MB % 148.33/21.97 % (3350199)Instructions burned: 543 (million) % 148.33/21.97 % (3350201)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 148.33/21.97 % (3350201)------------------------------ % 148.33/21.97 % (3350201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.00/24.85 % (3350201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.00/24.85 % (3350201)CaDiCaL version: 2.1.3 % 169.00/24.85 % (3350201)Termination reason: Unknown % 169.00/24.85 % (3350201)Termination phase: Saturation % 169.00/24.85 % (3350201)Time elapsed: 0.359 s % 169.00/24.85 % (3350201)Peak memory usage: 113 MB % 169.00/24.85 % (3350201)Instructions burned: 541 (million) % 169.00/24.85 % (3350206)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=1683246119:cts=off:i=19910:ep=RS_2842 on theBenchmark for (2842ds/19910Mi) % 169.00/24.85 % (3350202)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 169.00/24.85 % (3350202)------------------------------ % 169.00/24.85 % (3350202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.00/24.85 % (3350202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.00/24.85 % (3350202)CaDiCaL version: 2.1.3 % 169.00/24.85 % (3350202)Termination reason: Unknown % 169.00/24.85 % (3350202)Termination phase: Saturation % 169.00/24.85 % (3350202)Time elapsed: 0.360 s % 169.00/24.85 % (3350202)Peak memory usage: 114 MB % 169.00/24.85 % (3350202)Instructions burned: 541 (million) % 169.00/24.85 % (3350207)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=1618558866:i=20312:bd=preordered:fsr=off:er=filter_2841 on theBenchmark for (2841ds/20312Mi) % 169.00/24.85 % (3350208)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=4023691635:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2841 on theBenchmark for (2841ds/13822Mi) % 169.00/24.85 % (3350210)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=2616719436:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2840 on theBenchmark for (2840ds/7144Mi) % 169.00/24.85 % (3350207)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 169.00/24.85 % (3350207)------------------------------ % 169.00/24.85 % (3350207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.00/24.85 % (3350207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.00/24.85 % (3350207)CaDiCaL version: 2.1.3 % 169.00/24.85 % (3350207)Termination reason: Unknown % 169.00/24.85 % (3350207)Termination phase: Saturation % 169.00/24.85 % (3350207)Time elapsed: 0.360 s % 169.00/24.85 % (3350207)Peak memory usage: 114 MB % 169.00/24.85 % (3350207)Instructions burned: 541 (million) % 169.00/24.85 % (3350208)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 169.00/24.85 % (3350208)------------------------------ % 169.00/24.85 % (3350208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.00/24.85 % (3350208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.00/24.85 % (3350208)CaDiCaL version: 2.1.3 % 169.00/24.85 % (3350208)Termination reason: Unknown % 169.00/24.85 % (3350208)Termination phase: Saturation % 169.00/24.85 % (3350208)Time elapsed: 0.355 s % 169.00/24.85 % (3350208)Peak memory usage: 114 MB % 169.00/24.85 % (3350208)Instructions burned: 540 (million) % 169.00/24.85 % (3350214)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=983255186:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2836 on theBenchmark for (2836ds/15184Mi) % 169.00/24.85 % (3350215)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=3511883236:i=107375_2836 on theBenchmark for (2836ds/107375Mi) % 169.00/24.85 % (3350214)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 169.00/24.85 % (3350214)------------------------------ % 169.00/24.85 % (3350214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.00/24.85 % (3350214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.00/24.85 % (3350214)CaDiCaL version: 2.1.3 % 169.00/24.85 % (3350214)Termination reason: Unknown % 169.00/24.85 % (3350214)Termination phase: Saturation % 169.00/24.85 % (3350214)Time elapsed: 0.359 s % 169.00/24.85 % (3350214)Peak memory usage: 114 MB % 169.00/24.85 % (3350214)Instructions burned: 540 (million) % 169.00/24.85 % (3350215)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 169.00/24.85 % (3350215)------------------------------ % 169.00/24.85 % (3350215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.25/25.97 % (3350215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.25/25.97 % (3350215)CaDiCaL version: 2.1.3 % 176.25/25.97 % (3350215)Termination reason: Unknown % 176.25/25.97 % (3350215)Termination phase: Saturation % 176.25/25.97 % (3350215)Time elapsed: 0.357 s % 176.25/25.97 % (3350215)Peak memory usage: 114 MB % 176.25/25.97 % (3350215)Instructions burned: 541 (million) % 176.25/25.97 % (3350218)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=54602714:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2831 on theBenchmark for (2831ds/7958Mi) % 176.25/25.97 % (3350219)dis+10_128_sil=16000:nwc=0.7:random_seed=1918315016:i=15999:nm=2:gsp=on_2830 on theBenchmark for (2830ds/15999Mi) % 176.25/25.97 % (3350219)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 176.25/25.97 % (3350218)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 176.25/25.97 % (3350218)------------------------------ % 176.25/25.97 % (3350218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.25/25.97 % (3350218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.25/25.97 % (3350218)CaDiCaL version: 2.1.3 % 176.25/25.97 % (3350218)Termination reason: Unknown % 176.25/25.97 % (3350218)Termination phase: Saturation % 176.25/25.97 % (3350218)Time elapsed: 0.357 s % 176.25/25.97 % (3350218)Peak memory usage: 114 MB % 176.25/25.97 % (3350218)Instructions burned: 541 (million) % 176.25/25.97 % (3350222)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1461082360:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2826 on theBenchmark for (2826ds/8139Mi) % 176.25/25.97 % (3350210)Instruction limit reached! % 176.25/25.97 % (3350210)------------------------------ % 176.25/25.97 % (3350210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.25/25.97 % (3350210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.25/25.97 % (3350210)CaDiCaL version: 2.1.3 % 176.25/25.97 % (3350210)Termination reason: Instruction limit % 176.25/25.97 % (3350210)Termination phase: Saturation % 176.25/25.97 % (3350210)Time elapsed: 3.311 s % 176.25/25.97 % (3350210)Peak memory usage: 118 MB % 176.25/25.97 % (3350210)Instructions burned: 7147 (million) % 176.25/25.97 % (3350224)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=1102737821:st=4:i=8950:sd=5:ss=axioms_2806 on theBenchmark for (2806ds/8950Mi) % 176.25/25.97 % (3350224)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 176.25/25.97 % (3350224)------------------------------ % 176.25/25.97 % (3350224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.25/25.97 % (3350224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.25/25.97 % (3350224)CaDiCaL version: 2.1.3 % 176.25/25.97 % (3350224)Termination reason: Unknown % 176.25/25.97 % (3350224)Termination phase: Saturation % 176.25/25.97 % (3350224)Time elapsed: 0.359 s % 176.25/25.97 % (3350224)Peak memory usage: 114 MB % 176.25/25.97 % (3350224)Instructions burned: 541 (million) % 176.25/25.97 % (3350226)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=2406012711:i=9809:ins=10:av=off_2800 on theBenchmark for (2800ds/9809Mi) % 176.25/25.97 % (3350226)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 176.25/25.97 % (3350226)------------------------------ % 176.25/25.97 % (3350226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.25/25.97 % (3350226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.25/25.97 % (3350226)CaDiCaL version: 2.1.3 % 176.25/25.97 % (3350226)Termination reason: Unknown % 176.25/25.97 % (3350226)Termination phase: Saturation % 176.25/25.97 % (3350226)Time elapsed: 0.359 s % 176.25/25.97 % (3350226)Peak memory usage: 114 MB % 176.25/25.97 % (3350226)Instructions burned: 541 (million) % 176.25/25.97 % (3350228)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=3873937075:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2795 on theBenchmark for (2795ds/9885Mi) % 176.25/25.97 % (3350228)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 176.25/25.97 % (3350228)------------------------------ % 176.25/25.97 % (3350228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.25/25.97 % (3350228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.80 % (3350228)CaDiCaL version: 2.1.3 % 197.03/28.80 % (3350228)Termination reason: Unknown % 197.03/28.80 % (3350228)Termination phase: Saturation % 197.03/28.80 % (3350228)Time elapsed: 0.360 s % 197.03/28.80 % (3350228)Peak memory usage: 114 MB % 197.03/28.80 % (3350228)Instructions burned: 541 (million) % 197.03/28.80 % (3350230)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=574868276:cond=fast:i=32078:fgj=on:av=off_2790 on theBenchmark for (2790ds/32078Mi) % 197.03/28.80 % (3350230)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 197.03/28.80 % (3350230)------------------------------ % 197.03/28.80 % (3350230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.80 % (3350230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.80 % (3350230)CaDiCaL version: 2.1.3 % 197.03/28.80 % (3350230)Termination reason: Unknown % 197.03/28.80 % (3350230)Termination phase: Saturation % 197.03/28.80 % (3350230)Time elapsed: 0.357 s % 197.03/28.80 % (3350230)Peak memory usage: 114 MB % 197.03/28.80 % (3350230)Instructions burned: 540 (million) % 197.03/28.80 % (3350232)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=2517178343:i=11101:bd=all:ss=axioms:sgt=8_2784 on theBenchmark for (2784ds/11101Mi) % 197.03/28.80 % (3350222)Instruction limit reached! % 197.03/28.80 % (3350222)------------------------------ % 197.03/28.80 % (3350222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.80 % (3350222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.80 % (3350222)CaDiCaL version: 2.1.3 % 197.03/28.80 % (3350222)Termination reason: Instruction limit % 197.03/28.80 % (3350222)Termination phase: Saturation % 197.03/28.80 % (3350222)Time elapsed: 4.834 s % 197.03/28.80 % (3350222)Peak memory usage: 130 MB % 197.03/28.80 % (3350222)Instructions burned: 8139 (million) % 197.03/28.80 % (3350234)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=458129677:cond=on:i=13220:s2at=3:aac=none:fsd=on_2776 on theBenchmark for (2776ds/13220Mi) % 197.03/28.80 % (3350234)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 197.03/28.80 % (3350234)------------------------------ % 197.03/28.80 % (3350234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.80 % (3350234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.80 % (3350234)CaDiCaL version: 2.1.3 % 197.03/28.80 % (3350234)Termination reason: Unknown % 197.03/28.80 % (3350234)Termination phase: Saturation % 197.03/28.80 % (3350234)Time elapsed: 0.358 s % 197.03/28.80 % (3350234)Peak memory usage: 114 MB % 197.03/28.80 % (3350234)Instructions burned: 541 (million) % 197.03/28.80 % (3350236)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=2323344073:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2770 on theBenchmark for (2770ds/13528Mi) % 197.03/28.80 % (3350236)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 197.03/28.80 % (3350236)------------------------------ % 197.03/28.80 % (3350236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.80 % (3350236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.80 % (3350236)CaDiCaL version: 2.1.3 % 197.03/28.80 % (3350236)Termination reason: Unknown % 197.03/28.80 % (3350236)Termination phase: Saturation % 197.03/28.80 % (3350236)Time elapsed: 0.359 s % 197.03/28.80 % (3350236)Peak memory usage: 114 MB % 197.03/28.80 % (3350236)Instructions burned: 543 (million) % 197.03/28.80 % (3350238)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=3644046513:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2765 on theBenchmark for (2765ds/14854Mi) % 197.03/28.80 % (3350206)Instruction limit reached! % 197.03/28.80 % (3350206)------------------------------ % 197.03/28.80 % (3350206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.03/28.80 % (3350206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.03/28.80 % (3350206)CaDiCaL version: 2.1.3 % 197.03/28.80 % (3350206)Termination reason: Instruction limit % 197.03/28.80 % (3350206)Termination phase: Saturation % 197.03/28.80 % (3350206)Time elapsed: 7.971 s % 197.03/28.80 % (3350206)Peak memory usage: 146 MB % 197.03/28.80 % (3350206)Instructions burned: 19913 (million) % 209.63/30.56 % (3350238)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 209.63/30.56 % (3350238)------------------------------ % 209.63/30.56 % (3350238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.63/30.56 % (3350238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.63/30.56 % (3350238)CaDiCaL version: 2.1.3 % 209.63/30.56 % (3350238)Termination reason: Unknown % 209.63/30.56 % (3350238)Termination phase: Saturation % 209.63/30.56 % (3350238)Time elapsed: 0.365 s % 209.63/30.56 % (3350238)Peak memory usage: 114 MB % 209.63/30.56 % (3350238)Instructions burned: 551 (million) % 209.63/30.56 % (3350240)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1414909654:i=14974:ss=axioms:sgt=16_2761 on theBenchmark for (2761ds/14974Mi) % 209.63/30.56 % (3350241)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=1585261762:i=33081:aac=none:fgj=on:bd=all:fsr=off_2760 on theBenchmark for (2760ds/33081Mi) % 209.63/30.56 % (3350240)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 209.63/30.56 % (3350240)------------------------------ % 209.63/30.56 % (3350240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.63/30.56 % (3350240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.63/30.56 % (3350240)CaDiCaL version: 2.1.3 % 209.63/30.56 % (3350240)Termination reason: Unknown % 209.63/30.56 % (3350240)Termination phase: Saturation % 209.63/30.56 % (3350240)Time elapsed: 0.359 s % 209.63/30.56 % (3350240)Peak memory usage: 113 MB % 209.63/30.56 % (3350240)Instructions burned: 541 (million) % 209.63/30.56 % (3350241)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 209.63/30.56 % (3350241)------------------------------ % 209.63/30.56 % (3350241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.63/30.56 % (3350241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.63/30.56 % (3350241)CaDiCaL version: 2.1.3 % 209.63/30.56 % (3350241)Termination reason: Unknown % 209.63/30.56 % (3350241)Termination phase: Saturation % 209.63/30.56 % (3350241)Time elapsed: 0.357 s % 209.63/30.56 % (3350241)Peak memory usage: 114 MB % 209.63/30.56 % (3350241)Instructions burned: 541 (million) % 209.63/30.56 % (3350244)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=2447695606:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2755 on theBenchmark for (2755ds/50856Mi) % 209.63/30.56 % (3350245)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2128527825:i=69865_2755 on theBenchmark for (2755ds/69865Mi) % 209.63/30.56 % (3350244)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 209.63/30.56 % (3350244)------------------------------ % 209.63/30.56 % (3350244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.63/30.56 % (3350244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.63/30.56 % (3350244)CaDiCaL version: 2.1.3 % 209.63/30.56 % (3350244)Termination reason: Unknown % 209.63/30.56 % (3350244)Termination phase: Saturation % 209.63/30.56 % (3350244)Time elapsed: 0.357 s % 209.63/30.56 % (3350244)Peak memory usage: 114 MB % 209.63/30.56 % (3350244)Instructions burned: 541 (million) % 209.63/30.56 % (3349956)Instruction limit reached! % 209.63/30.56 % (3349956)------------------------------ % 209.63/30.56 % (3349956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.63/30.56 % (3349956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.63/30.56 % (3349956)CaDiCaL version: 2.1.3 % 209.63/30.56 % (3349956)Termination reason: Instruction limit % 209.63/30.56 % (3349956)Termination phase: Saturation % 209.63/30.56 % (3349956)Time elapsed: 15.728 s % 209.63/30.56 % (3349956)Peak memory usage: 464 MB % 209.63/30.56 % (3349956)Instructions burned: 26474 (million) % 209.63/30.56 % (3350245)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 209.63/30.56 % (3350245)------------------------------ % 209.63/30.56 % (3350245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 209.63/30.56 % (3350245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 209.63/30.56 % (3350245)CaDiCaL version: 2.1.3 % 209.63/30.56 % (3350245)Termination reason: Unknown % 209.63/30.56 % (3350245)Termination phase: Saturation % 224.05/32.58 % (3350245)Time elapsed: 0.358 s % 224.05/32.58 % (3350245)Peak memory usage: 114 MB % 224.05/32.58 % (3350245)Instructions burned: 540 (million) % 224.05/32.58 % (3350248)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=1766211310:cond=fast:i=17802:gtgl=3:gtg=all_2750 on theBenchmark for (2750ds/17802Mi) % 224.05/32.58 % (3350249)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=509715519:i=96644_2749 on theBenchmark for (2749ds/96644Mi) % 224.05/32.58 % (3350250)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 224.05/32.58 % (3350250)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=2230268161:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2749 on theBenchmark for (2749ds/21161Mi) % 224.05/32.58 % (3350248)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 224.05/32.58 % (3350248)------------------------------ % 224.05/32.58 % (3350248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.05/32.58 % (3350248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.05/32.58 % (3350248)CaDiCaL version: 2.1.3 % 224.05/32.58 % (3350248)Termination reason: Unknown % 224.05/32.58 % (3350248)Termination phase: Saturation % 224.05/32.58 % (3350248)Time elapsed: 0.358 s % 224.05/32.58 % (3350248)Peak memory usage: 114 MB % 224.05/32.58 % (3350248)Instructions burned: 543 (million) % 224.05/32.58 % (3350254)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=3427904053:i=22761:gtg=all:ss=axioms:fsd=on_2745 on theBenchmark for (2745ds/22761Mi) % 224.05/32.58 % (3350219)Instruction limit reached! % 224.05/32.58 % (3350219)------------------------------ % 224.05/32.58 % (3350219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.05/32.58 % (3350219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.05/32.58 % (3350219)CaDiCaL version: 2.1.3 % 224.05/32.58 % (3350219)Termination reason: Instruction limit % 224.05/32.58 % (3350219)Termination phase: Saturation % 224.05/32.58 % (3350219)Time elapsed: 8.646 s % 224.05/32.58 % (3350219)Peak memory usage: 170 MB % 224.05/32.58 % (3350219)Instructions burned: 15999 (million) % 224.05/32.58 % (3350256)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=1782095332:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2742 on theBenchmark for (2742ds/23713Mi) % 224.05/32.58 % (3350254)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 224.05/32.58 % (3350254)------------------------------ % 224.05/32.58 % (3350254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.05/32.58 % (3350254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.05/32.58 % (3350254)CaDiCaL version: 2.1.3 % 224.05/32.58 % (3350254)Termination reason: Unknown % 224.05/32.58 % (3350254)Termination phase: Saturation % 224.05/32.58 % (3350254)Time elapsed: 0.359 s % 224.05/32.58 % (3350254)Peak memory usage: 114 MB % 224.05/32.58 % (3350254)Instructions burned: 542 (million) % 224.05/32.58 % (3350258)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=2531883142:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2740 on theBenchmark for (2740ds/26509Mi) % 224.05/32.58 % (3350258)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 224.05/32.58 % (3350258)------------------------------ % 224.05/32.58 % (3350258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.05/32.58 % (3350258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.05/32.58 % (3350258)CaDiCaL version: 2.1.3 % 224.05/32.58 % (3350258)Termination reason: Unknown % 224.05/32.58 % (3350258)Termination phase: Saturation % 224.05/32.58 % (3350258)Time elapsed: 0.355 s % 224.05/32.58 % (3350258)Peak memory usage: 114 MB % 224.05/32.58 % (3350258)Instructions burned: 541 (million) % 224.05/32.58 % (3350260)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=1857368324:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2735 on theBenchmark for (2735ds/28957Mi) % 224.05/32.58 % (3350232)Instruction limit reached! % 224.05/32.58 % (3350232)------------------------------ % 224.05/32.58 % (3350232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.30/34.43 % (3350232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.30/34.43 % (3350232)CaDiCaL version: 2.1.3 % 237.30/34.43 % (3350232)Termination reason: Instruction limit % 237.30/34.43 % (3350232)Termination phase: Saturation % 237.30/34.43 % (3350232)Time elapsed: 6.148 s % 237.30/34.43 % (3350232)Peak memory usage: 200 MB % 237.30/34.43 % (3350232)Instructions burned: 11101 (million) % 237.30/34.43 % (3350262)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=1033761090:i=29246:s2at=-1:kws=inv_arity:ins=10_2721 on theBenchmark for (2721ds/29246Mi) % 237.30/34.43 % (3350262)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.30/34.43 % (3350262)------------------------------ % 237.30/34.43 % (3350262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.30/34.43 % (3350262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.30/34.43 % (3350262)CaDiCaL version: 2.1.3 % 237.30/34.43 % (3350262)Termination reason: Unknown % 237.30/34.43 % (3350262)Termination phase: Saturation % 237.30/34.43 % (3350262)Time elapsed: 0.357 s % 237.30/34.43 % (3350262)Peak memory usage: 114 MB % 237.30/34.43 % (3350262)Instructions burned: 541 (million) % 237.30/34.43 % (3350384)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=3243820065:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2716 on theBenchmark for (2716ds/30082Mi) % 237.30/34.43 % (3350384)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 237.30/34.43 % (3350384)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.30/34.43 % (3350384)------------------------------ % 237.30/34.43 % (3350384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.30/34.43 % (3350384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.30/34.43 % (3350384)CaDiCaL version: 2.1.3 % 237.30/34.43 % (3350384)Termination reason: Unknown % 237.30/34.43 % (3350384)Termination phase: Saturation % 237.30/34.43 % (3350384)Time elapsed: 0.359 s % 237.30/34.43 % (3350384)Peak memory usage: 114 MB % 237.30/34.43 % (3350384)Instructions burned: 544 (million) % 237.30/34.43 % (3350430)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1446158061:i=32262:bd=preordered_2711 on theBenchmark for (2711ds/32262Mi) % 237.30/34.43 % (3349922)Instruction limit reached! % 237.30/34.43 % (3349922)------------------------------ % 237.30/34.43 % (3349922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.30/34.43 % (3349922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.30/34.43 % (3349922)CaDiCaL version: 2.1.3 % 237.30/34.43 % (3349922)Termination reason: Instruction limit % 237.30/34.43 % (3349922)Termination phase: Saturation % 237.30/34.43 % (3349922)Time elapsed: 22.751 s % 237.30/34.43 % (3349922)Peak memory usage: 196 MB % 237.30/34.43 % (3349922)Instructions burned: 33335 (million) % 237.30/34.43 % (3350430)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.30/34.43 % (3350430)------------------------------ % 237.30/34.43 % (3350430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.30/34.43 % (3350430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.30/34.43 % (3350430)CaDiCaL version: 2.1.3 % 237.30/34.43 % (3350430)Termination reason: Unknown % 237.30/34.43 % (3350430)Termination phase: Saturation % 237.30/34.43 % (3350430)Time elapsed: 0.372 s % 237.30/34.43 % (3350430)Peak memory usage: 113 MB % 237.30/34.43 % (3350430)Instructions burned: 541 (million) % 237.30/34.43 % (3350182)Instruction limit reached! % 237.30/34.43 % (3350182)------------------------------ % 237.30/34.43 % (3350182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.30/34.43 % (3350182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.30/34.43 % (3350182)CaDiCaL version: 2.1.3 % 237.30/34.43 % (3350182)Termination reason: Instruction limit % 237.30/34.43 % (3350182)Termination phase: Saturation % 237.30/34.43 % (3350182)Time elapsed: 15.344 s % 237.30/34.43 % (3350182)Peak memory usage: 257 MB % 237.30/34.43 % (3350182)Instructions burned: 43699 (million) % 237.30/34.43 % (3350502)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=130860049:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2706 on theBenchmark for (2706ds/32870Mi) % 250.56/36.28 % (3350515)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=392695667:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2705 on theBenchmark for (2705ds/33295Mi) % 250.56/36.28 % (3350518)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=1843519328:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2704 on theBenchmark for (2704ds/36826Mi) % 250.56/36.28 % (3350515)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 250.56/36.28 % (3350515)------------------------------ % 250.56/36.28 % (3350515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.56/36.28 % (3350515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.56/36.28 % (3350515)CaDiCaL version: 2.1.3 % 250.56/36.28 % (3350515)Termination reason: Unknown % 250.56/36.28 % (3350515)Termination phase: Saturation % 250.56/36.28 % (3350515)Time elapsed: 0.355 s % 250.56/36.28 % (3350515)Peak memory usage: 114 MB % 250.56/36.28 % (3350515)Instructions burned: 541 (million) % 250.56/36.28 % (3350502)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 250.56/36.28 % (3350502)------------------------------ % 250.56/36.28 % (3350502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.56/36.28 % (3350502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.56/36.28 % (3350502)CaDiCaL version: 2.1.3 % 250.56/36.28 % (3350502)Termination reason: Unknown % 250.56/36.28 % (3350502)Termination phase: Saturation % 250.56/36.28 % (3350502)Time elapsed: 0.498 s % 250.56/36.28 % (3350502)Peak memory usage: 113 MB % 250.56/36.28 % (3350502)Instructions burned: 542 (million) % 250.56/36.28 % (3350520)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=1650497308:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2700 on theBenchmark for (2700ds/92981Mi) % 250.56/36.28 % (3350529)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=1568172666:s2pl=on:i=49423_2699 on theBenchmark for (2699ds/49423Mi) % 250.56/36.28 % (3350520)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 250.56/36.28 % (3350520)------------------------------ % 250.56/36.28 % (3350520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.56/36.28 % (3350520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.56/36.28 % (3350520)CaDiCaL version: 2.1.3 % 250.56/36.28 % (3350520)Termination reason: Unknown % 250.56/36.28 % (3350520)Termination phase: Saturation % 250.56/36.28 % (3350520)Time elapsed: 0.579 s % 250.56/36.28 % (3350520)Peak memory usage: 114 MB % 250.56/36.28 % (3350520)Instructions burned: 540 (million) % 250.56/36.28 % (3350529)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 250.56/36.28 % (3350529)------------------------------ % 250.56/36.28 % (3350529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.56/36.28 % (3350529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.56/36.28 % (3350529)CaDiCaL version: 2.1.3 % 250.56/36.28 % (3350529)Termination reason: Unknown % 250.56/36.28 % (3350529)Termination phase: Saturation % 250.56/36.28 % (3350529)Time elapsed: 0.553 s % 250.56/36.28 % (3350529)Peak memory usage: 114 MB % 250.56/36.28 % (3350529)Instructions burned: 542 (million) % 250.56/36.28 % (3350547)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=4284380534:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2692 on theBenchmark for (2692ds/57299Mi) % 250.56/36.28 % (3350553)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=1403857289:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2690 on theBenchmark for (2690ds/127679Mi) % 250.56/36.28 % (3350547)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 250.56/36.28 % (3350547)------------------------------ % 250.56/36.28 % (3350547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.56/36.28 % (3350547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.04/38.16 % (3350547)CaDiCaL version: 2.1.3 % 264.04/38.16 % (3350547)Termination reason: Unknown % 264.04/38.16 % (3350547)Termination phase: Saturation % 264.04/38.16 % (3350547)Time elapsed: 0.527 s % 264.04/38.16 % (3350547)Peak memory usage: 114 MB % 264.04/38.16 % (3350547)Instructions burned: 541 (million) % 264.04/38.16 % (3350553)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 264.04/38.16 % (3350553)------------------------------ % 264.04/38.16 % (3350553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.04/38.16 % (3350553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.04/38.16 % (3350553)CaDiCaL version: 2.1.3 % 264.04/38.16 % (3350553)Termination reason: Unknown % 264.04/38.16 % (3350553)Termination phase: Saturation % 264.04/38.16 % (3350553)Time elapsed: 0.536 s % 264.04/38.16 % (3350553)Peak memory usage: 114 MB % 264.04/38.16 % (3350553)Instructions burned: 541 (million) % 264.04/38.16 % (3350575)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=3152158672:i=69402:add=on:aac=none:fsr=off_2683 on theBenchmark for (2683ds/69402Mi) % 264.04/38.16 % (3350578)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=4253269525:i=100512:doe=on:fgj=on:bd=all:fsd=on_2682 on theBenchmark for (2682ds/100512Mi) % 264.04/38.16 % (3350575)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 264.04/38.16 % (3350575)------------------------------ % 264.04/38.16 % (3350575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.04/38.16 % (3350575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.04/38.16 % (3350575)CaDiCaL version: 2.1.3 % 264.04/38.16 % (3350575)Termination reason: Unknown % 264.04/38.16 % (3350575)Termination phase: Saturation % 264.04/38.16 % (3350575)Time elapsed: 0.541 s % 264.04/38.16 % (3350575)Peak memory usage: 113 MB % 264.04/38.16 % (3350575)Instructions burned: 541 (million) % 264.04/38.16 % (3350578)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 264.04/38.16 % (3350578)------------------------------ % 264.04/38.16 % (3350578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.04/38.16 % (3350578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.04/38.16 % (3350578)CaDiCaL version: 2.1.3 % 264.04/38.16 % (3350578)Termination reason: Unknown % 264.04/38.16 % (3350578)Termination phase: Saturation % 264.04/38.16 % (3350578)Time elapsed: 0.561 s % 264.04/38.16 % (3350578)Peak memory usage: 113 MB % 264.04/38.16 % (3350578)Instructions burned: 541 (million) % 264.04/38.16 % (3350599)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=4144736456:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2675 on theBenchmark for (2675ds/138761Mi) % 264.04/38.16 % (3350604)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=659999306:i=282386:rtra=on_2673 on theBenchmark for (2673ds/282386Mi) % 264.04/38.16 % (3350599)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 264.04/38.16 % (3350599)------------------------------ % 264.04/38.16 % (3350599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.04/38.16 % (3350599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 264.04/38.16 % (3350599)CaDiCaL version: 2.1.3 % 264.04/38.16 % (3350599)Termination reason: Unknown % 264.04/38.16 % (3350599)Termination phase: Saturation % 264.04/38.16 % (3350599)Time elapsed: 0.507 s % 264.04/38.16 % (3350599)Peak memory usage: 114 MB % 264.04/38.16 % (3350599)Instructions burned: 541 (million) % 264.04/38.16 % (3350618)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=2266824143:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2668 on theBenchmark for (2668ds/269354Mi) % 264.04/38.16 % (3350604)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 264.04/38.16 % (3350604)------------------------------ % 264.04/38.16 % (3350604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 264.04/38.16 % (3350604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.97/40.86 % (3350604)CaDiCaL version: 2.1.3 % 282.97/40.86 % (3350604)Termination reason: Unknown % 282.97/40.86 % (3350604)Termination phase: Saturation % 282.97/40.86 % (3350604)Time elapsed: 0.569 s % 282.97/40.86 % (3350604)Peak memory usage: 114 MB % 282.97/40.86 % (3350604)Instructions burned: 541 (million) % 282.97/40.86 % (3350624)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=2825296472:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2665 on theBenchmark for (2665ds/283390Mi) % 282.97/40.86 % (3350624)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 282.97/40.86 % (3350618)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 282.97/40.86 % (3350618)------------------------------ % 282.97/40.86 % (3350618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.97/40.86 % (3350618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.97/40.86 % (3350618)CaDiCaL version: 2.1.3 % 282.97/40.86 % (3350618)Termination reason: Unknown % 282.97/40.86 % (3350618)Termination phase: Saturation % 282.97/40.86 % (3350618)Time elapsed: 0.537 s % 282.97/40.86 % (3350618)Peak memory usage: 114 MB % 282.97/40.86 % (3350618)Instructions burned: 544 (million) % 282.97/40.86 % (3350624)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 282.97/40.86 % (3350624)------------------------------ % 282.97/40.86 % (3350624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.97/40.86 % (3350624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.97/40.86 % (3350624)CaDiCaL version: 2.1.3 % 282.97/40.86 % (3350624)Termination reason: Unknown % 282.97/40.86 % (3350624)Termination phase: Saturation % 282.97/40.86 % (3350624)Time elapsed: 0.548 s % 282.97/40.86 % (3350624)Peak memory usage: 114 MB % 282.97/40.86 % (3350624)Instructions burned: 541 (million) % 282.97/40.86 % (3350634)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=1285138238:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2660 on theBenchmark for (2660ds/218Mi) % 282.97/40.86 % (3350634)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 282.97/40.86 % (3350634)Refutation not found, incomplete strategy % 282.97/40.86 % (3350634)------------------------------ % 282.97/40.86 % (3350634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.97/40.86 % (3350634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.97/40.86 % (3350634)CaDiCaL version: 2.1.3 % 282.97/40.86 % (3350634)Termination reason: Refutation not found, incomplete strategy % 282.97/40.86 % (3350634)Time elapsed: 0.008 s % 282.97/40.86 % (3350634)Peak memory usage: 89 MB % 282.97/40.86 % (3350634)Instructions burned: 6 (million) % 282.97/40.86 % (3350642)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=4291058733:i=238:av=off:rtra=on:ss=axioms_2656 on theBenchmark for (2656ds/238Mi) % 282.97/40.86 % (3350634)------------------------------ % 282.97/40.86 % (3350634)------------------------------ % 282.97/40.86 % (3350642)Instruction limit reached! % 282.97/40.86 % (3350642)------------------------------ % 282.97/40.86 % (3350642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.97/40.86 % (3350642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.97/40.86 % (3350642)CaDiCaL version: 2.1.3 % 282.97/40.86 % (3350642)Termination reason: Instruction limit % 282.97/40.86 % (3350642)Termination phase: Saturation % 282.97/40.86 % (3350642)Time elapsed: 0.211 s % 282.97/40.86 % (3350642)Peak memory usage: 89 MB % 282.97/40.86 % (3350642)Instructions burned: 238 (million) % 282.97/40.86 % (3350647)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=1362470852:s2a=on:i=278:rtra=on:gtg=position_2652 on theBenchmark for (2652ds/278Mi) % 282.97/40.86 % (3350649)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=3887334402:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2651 on theBenchmark for (2651ds/258Mi) % 282.97/40.86 % (3350647)Instruction limit reached! % 282.97/40.86 % (3350647)------------------------------ % 282.97/40.86 % (3350647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.97/40.86 % (3350647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.97/40.86 % (3350647)CaDiCaL version: 2.1.3 % 282.97/40.86 % (3350647)Termination reason: Instruction limit % 282.97/40.86 % (3350647)Termination phase: Saturation % 282.97/40.86 % (3350647)Time elapsed: 0.271 s % 293.51/42.34 % (3350647)Peak memory usage: 91 MB % 293.51/42.34 % (3350647)Instructions burned: 279 (million) % 293.51/42.34 % (3350649)Instruction limit reached! % 293.51/42.34 % (3350649)------------------------------ % 293.51/42.34 % (3350649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.51/42.34 % (3350649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.51/42.34 % (3350649)CaDiCaL version: 2.1.3 % 293.51/42.34 % (3350649)Termination reason: Instruction limit % 293.51/42.34 % (3350649)Termination phase: Saturation % 293.51/42.34 % (3350649)Time elapsed: 0.236 s % 293.51/42.34 % (3350649)Peak memory usage: 90 MB % 293.51/42.34 % (3350649)Instructions burned: 258 (million) % 293.51/42.34 % (3350658)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3425190645:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2646 on theBenchmark for (2646ds/570Mi) % 293.51/42.34 % (3350659)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=1056368585:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2646 on theBenchmark for (2646ds/314Mi) % 293.51/42.34 % (3350659)Instruction limit reached! % 293.51/42.34 % (3350659)------------------------------ % 293.51/42.34 % (3350659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.51/42.34 % (3350659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.51/42.34 % (3350659)CaDiCaL version: 2.1.3 % 293.51/42.34 % (3350659)Termination reason: Instruction limit % 293.51/42.34 % (3350659)Termination phase: Saturation % 293.51/42.34 % (3350659)Time elapsed: 0.245 s % 293.51/42.34 % (3350659)Peak memory usage: 90 MB % 293.51/42.34 % (3350659)Instructions burned: 315 (million) % 293.51/42.34 % (3350658)Instruction limit reached! % 293.51/42.34 % (3350658)------------------------------ % 293.51/42.34 % (3350658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.51/42.34 % (3350658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.51/42.34 % (3350658)CaDiCaL version: 2.1.3 % 293.51/42.34 % (3350658)Termination reason: Instruction limit % 293.51/42.34 % (3350658)Termination phase: Saturation % 293.51/42.34 % (3350658)Time elapsed: 0.510 s % 293.51/42.34 % (3350658)Peak memory usage: 92 MB % 293.51/42.34 % (3350658)Instructions burned: 570 (million) % 293.51/42.34 % (3350667)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=931325086:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2641 on theBenchmark for (2641ds/650Mi) % 293.51/42.34 % (3350670)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=1127150219:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2638 on theBenchmark for (2638ds/496Mi) % 293.51/42.34 % (3350667)Instruction limit reached! % 293.51/42.34 % (3350667)------------------------------ % 293.51/42.34 % (3350667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.51/42.34 % (3350667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.51/42.34 % (3350667)CaDiCaL version: 2.1.3 % 293.51/42.34 % (3350667)Termination reason: Instruction limit % 293.51/42.34 % (3350667)Termination phase: Saturation % 293.51/42.34 % (3350667)Time elapsed: 0.510 s % 293.51/42.34 % (3350667)Peak memory usage: 94 MB % 293.51/42.34 % (3350667)Instructions burned: 651 (million) % 293.51/42.34 % (3350670)Instruction limit reached! % 293.51/42.34 % (3350670)------------------------------ % 293.51/42.34 % (3350670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.51/42.34 % (3350670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.51/42.34 % (3350670)CaDiCaL version: 2.1.3 % 293.51/42.34 % (3350670)Termination reason: Instruction limit % 293.51/42.34 % (3350670)Termination phase: Saturation % 293.51/42.34 % (3350670)Time elapsed: 0.469 s % 293.51/42.34 % (3350670)Peak memory usage: 94 MB % 293.51/42.34 % (3350670)Instructions burned: 497 (million) % 293.51/42.34 % (3350679)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=4254373027:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2633 on theBenchmark for (2633ds/588Mi) % 293.51/42.34 % (3350679)Refutation not found, incomplete strategy % 293.51/42.34 % (3350679)------------------------------ % 293.51/42.34 % (3350679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.51/42.34 % (3350679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.51/42.34 % (3350679)CaDiCaL version: 2.1.3 % 293.51/42.34 % (3350679)Termination reason: Refutation not found, incomplete strategy % 293.51/42.34 % (3350679)Time elapsed: 0.011 s % 293.51/42.34 % (3350679)Peak memory usage: 88 MB % 293.51/42.34 % (3350679)Instructions burned: 10 (million) % 293.51/42.34 % (3350681)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgtTerminated %------------------------------------------------------------------------------