%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM964_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n013.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:17:42 PM UTC 2026 % Result : Timeout 296.43s 42.86s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM964_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.37 % Computer : n013.cluster.edu % 0.12/0.37 % Model : x86_64 x86_64 % 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.37 % Memory : 8046.5625MB % 0.12/0.37 % OS : Linux 6.8.0-71-generic % 0.12/0.37 % CPULimit : 300 % 0.12/0.37 % WCLimit : 300 % 0.12/0.37 % DateTime : Sun Sep 27 21:47:51 UTC 2026 % 0.12/0.38 % CPUTime : % 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.41 Running first-order theorem proving % 0.12/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.01/1.75 % (582642)Detected formulas, will run a generic FOF schedule. % 5.01/1.75 % (582648)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=3888805725:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.01/1.75 % (582652)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1905780786:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.01/1.75 % (582654)dis-21_1_sil=8000:lcm=predicate:random_seed=1329510381: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) % 5.01/1.75 % (582651)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=85372036:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.01/1.75 % (582653)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=902438334:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.01/1.75 % (582650)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=2220700311:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.01/1.75 % (582649)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=1318749058:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.01/1.75 % (582651)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.01/1.75 % (582650)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.01/1.75 % (582651)Instruction limit reached! % 5.01/1.75 % (582651)------------------------------ % 5.01/1.75 % (582651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.01/1.75 % (582651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.01/1.75 % (582651)CaDiCaL version: 2.1.3 % 5.01/1.75 % (582651)Termination reason: Instruction limit % 5.01/1.75 % (582651)Termination phase: Saturation % 5.01/1.75 % (582651)Time elapsed: 0.058 s % 5.01/1.75 % (582651)Peak memory usage: 89 MB % 5.01/1.75 % (582651)Instructions burned: 110 (million) % 5.01/1.75 % (582652)Instruction limit reached! % 5.01/1.75 % (582652)------------------------------ % 5.01/1.75 % (582652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.01/1.75 % (582652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.01/1.75 % (582652)CaDiCaL version: 2.1.3 % 5.01/1.75 % (582652)Termination reason: Instruction limit % 5.01/1.75 % (582652)Termination phase: Saturation % 5.01/1.75 % (582652)Time elapsed: 0.064 s % 5.01/1.75 % (582652)Peak memory usage: 88 MB % 5.01/1.75 % (582652)Instructions burned: 120 (million) % 5.01/1.75 % (582654)Instruction limit reached! % 5.01/1.75 % (582654)------------------------------ % 5.01/1.75 % (582654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.01/1.75 % (582654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.01/1.75 % (582654)CaDiCaL version: 2.1.3 % 5.01/1.75 % (582654)Termination reason: Instruction limit % 5.01/1.75 % (582654)Termination phase: Saturation % 5.01/1.75 % (582654)Time elapsed: 0.068 s % 5.01/1.75 % (582654)Peak memory usage: 89 MB % 5.01/1.75 % (582654)Instructions burned: 129 (million) % 5.01/1.75 % (582653)Instruction limit reached! % 5.01/1.75 % (582653)------------------------------ % 5.01/1.75 % (582653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.01/1.75 % (582653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.01/1.75 % (582653)CaDiCaL version: 2.1.3 % 5.01/1.75 % (582653)Termination reason: Instruction limit % 5.01/1.75 % (582653)Termination phase: Saturation % 5.01/1.75 % (582653)Time elapsed: 0.087 s % 5.01/1.75 % (582653)Peak memory usage: 89 MB % 5.01/1.75 % (582653)Instructions burned: 139 (million) % 5.01/1.75 % (582648)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.01/1.75 % (582648)------------------------------ % 5.01/1.75 % (582648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.01/1.75 % (582648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.01/1.75 % (582648)CaDiCaL version: 2.1.3 % 5.01/1.75 % (582648)Termination reason: Unknown % 5.01/1.75 % (582648)Termination phase: Saturation % 5.01/1.75 % (582648)Time elapsed: 0.199 s % 5.01/1.75 % (582648)Peak memory usage: 113 MB % 6.51/2.01 % (582648)Instructions burned: 542 (million) % 6.51/2.01 % (582664)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1105881448:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 6.51/2.01 % (582663)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2503038218:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 6.51/2.01 % (582662)lrs+10_1_sil=8000:sp=occurrence:random_seed=3731870477:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 6.51/2.01 % (582665)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=4280923966:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 6.51/2.01 % (582666)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=213069999:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 6.51/2.01 % (582666)Refutation not found, incomplete strategy % 6.51/2.01 % (582666)------------------------------ % 6.51/2.01 % (582666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/2.01 % (582666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/2.01 % (582666)CaDiCaL version: 2.1.3 % 6.51/2.01 % (582666)Termination reason: Refutation not found, incomplete strategy % 6.51/2.01 % (582666)Time elapsed: 0.004 s % 6.51/2.01 % (582666)Peak memory usage: 88 MB % 6.51/2.01 % (582666)Instructions burned: 10 (million) % 6.51/2.01 % (582663)Instruction limit reached! % 6.51/2.01 % (582663)------------------------------ % 6.51/2.01 % (582663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/2.01 % (582663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/2.01 % (582663)CaDiCaL version: 2.1.3 % 6.51/2.01 % (582663)Termination reason: Instruction limit % 6.51/2.01 % (582663)Termination phase: Saturation % 6.51/2.01 % (582663)Time elapsed: 0.083 s % 6.51/2.01 % (582663)Peak memory usage: 89 MB % 6.51/2.01 % (582663)Instructions burned: 157 (million) % 6.51/2.01 % (582649)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.51/2.01 % (582649)------------------------------ % 6.51/2.01 % (582649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/2.01 % (582649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/2.01 % (582649)CaDiCaL version: 2.1.3 % 6.51/2.01 % (582649)Termination reason: Unknown % 6.51/2.01 % (582649)Termination phase: Saturation % 6.51/2.01 % (582649)Time elapsed: 0.365 s % 6.51/2.01 % (582649)Peak memory usage: 112 MB % 6.51/2.01 % (582650)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.51/2.01 % (582649)Instructions burned: 545 (million) % 6.51/2.01 % (582650)------------------------------ % 6.51/2.01 % (582650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/2.01 % (582650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/2.01 % (582650)CaDiCaL version: 2.1.3 % 6.51/2.01 % (582650)Termination reason: Unknown % 6.51/2.01 % (582650)Termination phase: Saturation % 6.51/2.01 % (582650)Time elapsed: 0.365 s % 6.51/2.01 % (582650)Peak memory usage: 112 MB % 6.51/2.01 % (582650)Instructions burned: 542 (million) % 6.51/2.01 % (582662)Instruction limit reached! % 6.51/2.01 % (582662)------------------------------ % 6.51/2.01 % (582662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/2.01 % (582662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/2.01 % (582662)CaDiCaL version: 2.1.3 % 6.51/2.01 % (582662)Termination reason: Instruction limit % 6.51/2.01 % (582662)Termination phase: Saturation % 6.51/2.01 % (582662)Time elapsed: 0.159 s % 6.51/2.01 % (582662)Peak memory usage: 90 MB % 6.51/2.01 % (582662)Instructions burned: 286 (million) % 6.51/2.01 % (582665)Instruction limit reached! % 6.51/2.01 % (582665)------------------------------ % 6.51/2.01 % (582665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.51/2.01 % (582665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.51/2.01 % (582665)CaDiCaL version: 2.1.3 % 6.51/2.01 % (582665)Termination reason: Instruction limit % 6.51/2.01 % (582665)Termination phase: Saturation % 6.51/2.01 % (582665)Time elapsed: 0.152 s % 6.51/2.01 % (582665)Peak memory usage: 91 MB % 6.51/2.01 % (582665)Instructions burned: 249 (million) % 6.51/2.01 % (582664)Instruction limit reached! % 6.51/2.01 % (582664)------------------------------ % 6.51/2.01 % (582664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.45/2.24 % (582664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.45/2.24 % (582664)CaDiCaL version: 2.1.3 % 9.45/2.24 % (582664)Termination reason: Instruction limit % 9.45/2.24 % (582664)Termination phase: Saturation % 9.45/2.24 % (582664)Time elapsed: 0.189 s % 9.45/2.24 % (582664)Peak memory usage: 91 MB % 9.45/2.24 % (582664)Instructions burned: 326 (million) % 9.45/2.24 % (582666)------------------------------ % 9.45/2.24 % (582666)------------------------------ % 9.45/2.24 % (582672)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2083994431:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 9.45/2.24 % (582673)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=665901150:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 9.45/2.24 % (582675)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2983671383:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 9.45/2.24 % (582674)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1257524180:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 9.45/2.24 % (582678)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2936028012:i=5202:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/5202Mi) % 9.45/2.24 % (582676)lrs+10_1_sil=8000:sp=occurrence:random_seed=3138141805:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 9.45/2.24 % (582677)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2581850500:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 9.45/2.24 % (582677)Refutation not found, incomplete strategy % 9.45/2.24 % (582677)------------------------------ % 9.45/2.24 % (582677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.45/2.24 % (582677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.45/2.24 % (582677)CaDiCaL version: 2.1.3 % 9.45/2.24 % (582677)Termination reason: Refutation not found, incomplete strategy % 9.45/2.24 % (582677)Time elapsed: 0.005 s % 9.45/2.24 % (582677)Peak memory usage: 88 MB % 9.45/2.24 % (582677)Instructions burned: 8 (million) % 9.45/2.24 % (582675)Instruction limit reached! % 9.45/2.24 % (582675)------------------------------ % 9.45/2.24 % (582675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.45/2.24 % (582675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.45/2.24 % (582675)CaDiCaL version: 2.1.3 % 9.45/2.24 % (582675)Termination reason: Instruction limit % 9.45/2.24 % (582675)Termination phase: Saturation % 9.45/2.24 % (582675)Time elapsed: 0.055 s % 9.45/2.24 % (582675)Peak memory usage: 88 MB % 9.45/2.24 % (582675)Instructions burned: 116 (million) % 9.45/2.24 % (582674)Instruction limit reached! % 9.45/2.24 % (582674)------------------------------ % 9.45/2.24 % (582674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.45/2.24 % (582674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.45/2.24 % (582674)CaDiCaL version: 2.1.3 % 9.45/2.24 % (582674)Termination reason: Instruction limit % 9.45/2.24 % (582674)Termination phase: Saturation % 9.45/2.24 % (582674)Time elapsed: 0.056 s % 9.45/2.24 % (582674)Peak memory usage: 88 MB % 9.45/2.24 % (582674)Instructions burned: 129 (million) % 9.45/2.24 % (582673)Instruction limit reached! % 9.45/2.24 % (582673)------------------------------ % 9.45/2.24 % (582673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.45/2.24 % (582673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.45/2.24 % (582673)CaDiCaL version: 2.1.3 % 9.45/2.24 % (582673)Termination reason: Instruction limit % 9.45/2.24 % (582673)Termination phase: Saturation % 9.45/2.24 % (582673)Time elapsed: 0.069 s % 9.45/2.24 % (582673)Peak memory usage: 89 MB % 9.45/2.24 % (582673)Instructions burned: 113 (million) % 9.45/2.24 % (582678)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.45/2.24 % (582678)------------------------------ % 9.45/2.24 % (582678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.45/2.24 % (582678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.45/2.24 % (582678)CaDiCaL version: 2.1.3 % 9.45/2.24 % (582678)Termination reason: Unknown % 9.45/2.24 % (582678)Termination phase: Saturation % 9.45/2.24 % (582678)Time elapsed: 0.199 s % 10.77/2.59 % (582678)Peak memory usage: 113 MB % 10.77/2.59 % (582678)Instructions burned: 542 (million) % 10.77/2.59 % (582687)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=871262594:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 10.77/2.59 % (582686)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3567674134:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 10.77/2.59 % (582687)Refutation not found, incomplete strategy % 10.77/2.59 % (582687)------------------------------ % 10.77/2.59 % (582687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.77/2.59 % (582687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.77/2.59 % (582687)CaDiCaL version: 2.1.3 % 10.77/2.59 % (582687)Termination reason: Refutation not found, incomplete strategy % 10.77/2.59 % (582687)Time elapsed: 0.006 s % 10.77/2.59 % (582687)Peak memory usage: 88 MB % 10.77/2.59 % (582687)Instructions burned: 10 (million) % 10.77/2.59 % (582688)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=472712072:st=3:i=13193:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/13193Mi) % 10.77/2.59 % (582686)Instruction limit reached! % 10.77/2.59 % (582686)------------------------------ % 10.77/2.59 % (582686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.77/2.59 % (582686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.77/2.59 % (582686)CaDiCaL version: 2.1.3 % 10.77/2.59 % (582686)Termination reason: Instruction limit % 10.77/2.59 % (582686)Termination phase: Saturation % 10.77/2.59 % (582686)Time elapsed: 0.077 s % 10.77/2.59 % (582686)Peak memory usage: 90 MB % 10.77/2.59 % (582686)Instructions burned: 134 (million) % 10.77/2.59 % (582677)------------------------------ % 10.77/2.59 % (582677)------------------------------ % 10.77/2.59 % (582672)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.77/2.59 % (582672)------------------------------ % 10.77/2.59 % (582672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.77/2.59 % (582672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.77/2.59 % (582672)CaDiCaL version: 2.1.3 % 10.77/2.59 % (582672)Termination reason: Unknown % 10.77/2.59 % (582672)Termination phase: Saturation % 10.77/2.59 % (582672)Time elapsed: 0.367 s % 10.77/2.59 % (582672)Peak memory usage: 113 MB % 10.77/2.59 % (582672)Instructions burned: 542 (million) % 10.77/2.59 % (582691)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=492723149:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/125Mi) % 10.77/2.59 % (582691)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.77/2.59 % (582691)Instruction limit reached! % 10.77/2.59 % (582691)------------------------------ % 10.77/2.59 % (582691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.77/2.59 % (582691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.77/2.59 % (582691)CaDiCaL version: 2.1.3 % 10.77/2.59 % (582691)Termination reason: Instruction limit % 10.77/2.59 % (582691)Termination phase: Saturation % 10.77/2.59 % (582691)Time elapsed: 0.038 s % 10.77/2.59 % (582691)Peak memory usage: 90 MB % 10.77/2.59 % (582691)Instructions burned: 126 (million) % 10.77/2.59 % (582693)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=599948045:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 10.77/2.59 % (582687)------------------------------ % 10.77/2.59 % (582687)------------------------------ % 10.77/2.59 % (582694)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=806185714:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi) % 10.77/2.59 % (582695)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3693231463:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 10.77/2.59 % (582694)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.77/2.59 % (582694)Refutation not found, incomplete strategy % 10.77/2.59 % (582694)------------------------------ % 10.77/2.59 % (582694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.77/2.59 % (582694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.77/2.59 % (582694)CaDiCaL version: 2.1.3 % 15.79/3.11 % (582694)Termination reason: Refutation not found, incomplete strategy % 15.79/3.11 % (582694)Time elapsed: 0.003 s % 15.79/3.11 % (582694)Peak memory usage: 88 MB % 15.79/3.11 % (582694)Instructions burned: 4 (million) % 15.79/3.11 % (582697)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=4220777005:i=6060:aac=none:ins=25_2989 on theBenchmark for (2989ds/6060Mi) % 15.79/3.11 % (582693)Instruction limit reached! % 15.79/3.11 % (582693)------------------------------ % 15.79/3.11 % (582693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.79/3.11 % (582693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.79/3.11 % (582693)CaDiCaL version: 2.1.3 % 15.79/3.11 % (582693)Termination reason: Instruction limit % 15.79/3.11 % (582693)Termination phase: Saturation % 15.79/3.11 % (582693)Time elapsed: 0.082 s % 15.79/3.11 % (582693)Peak memory usage: 90 MB % 15.79/3.11 % (582693)Instructions burned: 135 (million) % 15.79/3.11 % (582676)Instruction limit reached! % 15.79/3.11 % (582676)------------------------------ % 15.79/3.11 % (582676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.79/3.11 % (582676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.79/3.11 % (582676)CaDiCaL version: 2.1.3 % 15.79/3.11 % (582676)Termination reason: Instruction limit % 15.79/3.11 % (582676)Termination phase: Saturation % 15.79/3.11 % (582676)Time elapsed: 0.526 s % 15.79/3.11 % (582676)Peak memory usage: 94 MB % 15.79/3.11 % (582676)Instructions burned: 907 (million) % 15.79/3.11 % (582688)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.79/3.11 % (582688)------------------------------ % 15.79/3.11 % (582688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.79/3.11 % (582688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.79/3.11 % (582688)CaDiCaL version: 2.1.3 % 15.79/3.11 % (582688)Termination reason: Unknown % 15.79/3.11 % (582688)Termination phase: Saturation % 15.79/3.11 % (582688)Time elapsed: 0.370 s % 15.79/3.11 % (582688)Peak memory usage: 113 MB % 15.79/3.11 % (582688)Instructions burned: 541 (million) % 15.79/3.11 % (582701)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=2190695168:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi) % 15.79/3.11 % (582701)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 15.79/3.11 % (582695)Instruction limit reached! % 15.79/3.11 % (582695)------------------------------ % 15.79/3.11 % (582695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.79/3.11 % (582695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.79/3.11 % (582695)CaDiCaL version: 2.1.3 % 15.79/3.11 % (582695)Termination reason: Instruction limit % 15.79/3.11 % (582695)Termination phase: Saturation % 15.79/3.11 % (582695)Time elapsed: 0.170 s % 15.79/3.11 % (582695)Peak memory usage: 89 MB % 15.79/3.11 % (582695)Instructions burned: 432 (million) % 15.79/3.11 % (582703)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3439350218:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi) % 15.79/3.11 % (582704)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1722083604:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi) % 15.79/3.11 % (582697)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.79/3.11 % (582697)------------------------------ % 15.79/3.11 % (582697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.79/3.11 % (582697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.79/3.11 % (582697)CaDiCaL version: 2.1.3 % 15.79/3.11 % (582697)Termination reason: Unknown % 15.79/3.11 % (582697)Termination phase: Saturation % 15.79/3.11 % (582697)Time elapsed: 0.200 s % 15.79/3.11 % (582697)Peak memory usage: 114 MB % 15.79/3.11 % (582697)Instructions burned: 541 (million) % 15.79/3.11 % (582704)Refutation not found, incomplete strategy % 15.79/3.11 % (582704)------------------------------ % 15.79/3.11 % (582704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.79/3.11 % (582704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.79/3.11 % (582704)CaDiCaL version: 2.1.3 % 16.95/3.61 % (582704)Termination reason: Refutation not found, incomplete strategy % 16.95/3.61 % (582704)Time elapsed: 0.006 s % 16.95/3.61 % (582704)Peak memory usage: 88 MB % 16.95/3.61 % (582704)Instructions burned: 10 (million) % 16.95/3.61 % (582694)------------------------------ % 16.95/3.61 % (582694)------------------------------ % 16.95/3.61 % (582701)Instruction limit reached! % 16.95/3.61 % (582701)------------------------------ % 16.95/3.61 % (582701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.95/3.61 % (582701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/3.61 % (582701)CaDiCaL version: 2.1.3 % 16.95/3.61 % (582701)Termination reason: Instruction limit % 16.95/3.61 % (582701)Termination phase: Saturation % 16.95/3.61 % (582701)Time elapsed: 0.093 s % 16.95/3.61 % (582701)Peak memory usage: 90 MB % 16.95/3.61 % (582701)Instructions burned: 151 (million) % 16.95/3.61 % (582705)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=538039909:s2a=on:i=185:s2at=1.8:fdi=4_2986 on theBenchmark for (2986ds/185Mi) % 16.95/3.61 % (582707)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2972317448:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi) % 16.95/3.61 % (582710)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3999857860:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2986 on theBenchmark for (2986ds/4850Mi) % 16.95/3.61 % (582712)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=578604230:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 16.95/3.61 % (582711)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1073539839:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi) % 16.95/3.61 % (582705)Instruction limit reached! % 16.95/3.61 % (582705)------------------------------ % 16.95/3.61 % (582705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.95/3.61 % (582705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/3.61 % (582705)CaDiCaL version: 2.1.3 % 16.95/3.61 % (582705)Termination reason: Instruction limit % 16.95/3.61 % (582705)Termination phase: Saturation % 16.95/3.61 % (582705)Time elapsed: 0.104 s % 16.95/3.61 % (582705)Peak memory usage: 91 MB % 16.95/3.61 % (582705)Instructions burned: 186 (million) % 16.95/3.61 % (582707)Instruction limit reached! % 16.95/3.61 % (582707)------------------------------ % 16.95/3.61 % (582707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.95/3.61 % (582707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/3.61 % (582707)CaDiCaL version: 2.1.3 % 16.95/3.61 % (582707)Termination reason: Instruction limit % 16.95/3.61 % (582707)Termination phase: Saturation % 16.95/3.61 % (582707)Time elapsed: 0.097 s % 16.95/3.61 % (582707)Peak memory usage: 89 MB % 16.95/3.61 % (582707)Instructions burned: 194 (million) % 16.95/3.61 % (582704)------------------------------ % 16.95/3.61 % (582704)------------------------------ % 16.95/3.61 % (582718)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1315002744:i=2064:ep=RST_2984 on theBenchmark for (2984ds/2064Mi) % 16.95/3.61 % (582703)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.95/3.61 % (582703)------------------------------ % 16.95/3.62 % (582703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.95/3.62 % (582703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/3.62 % (582703)CaDiCaL version: 2.1.3 % 16.95/3.62 % (582703)Termination reason: Unknown % 16.95/3.62 % (582703)Termination phase: Saturation % 16.95/3.62 % (582703)Time elapsed: 0.368 s % 16.95/3.62 % (582703)Peak memory usage: 114 MB % 16.95/3.62 % (582703)Instructions burned: 542 (million) % 16.95/3.62 % (582718)Refutation not found, incomplete strategy % 16.95/3.62 % (582718)------------------------------ % 16.95/3.62 % (582718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.95/3.62 % (582718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.95/3.62 % (582718)CaDiCaL version: 2.1.3 % 16.95/3.62 % (582718)Termination reason: Refutation not found, incomplete strategy % 16.95/3.62 % (582718)Time elapsed: 0.006 s % 16.95/3.62 % (582718)Peak memory usage: 88 MB % 16.95/3.62 % (582718)Instructions burned: 10 (million) % 16.95/3.62 % (582719)dis-1011_128_sil=32000:random_seed=1267846903:i=3706:ep=RST:av=off_2984 on theBenchmark for (2984ds/3706Mi) % 23.88/4.22 % (582712)Instruction limit reached! % 23.88/4.22 % (582712)------------------------------ % 23.88/4.22 % (582712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.22 % (582712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.22 % (582712)CaDiCaL version: 2.1.3 % 23.88/4.22 % (582712)Termination reason: Instruction limit % 23.88/4.22 % (582712)Termination phase: Saturation % 23.88/4.22 % (582712)Time elapsed: 0.179 s % 23.88/4.22 % (582712)Peak memory usage: 92 MB % 23.88/4.22 % (582712)Instructions burned: 319 (million) % 23.88/4.22 % (582720)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3855625114:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2983 on theBenchmark for (2983ds/757Mi) % 23.88/4.22 % (582720)Refutation not found, incomplete strategy % 23.88/4.22 % (582720)------------------------------ % 23.88/4.22 % (582720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.22 % (582720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.22 % (582720)CaDiCaL version: 2.1.3 % 23.88/4.22 % (582720)Termination reason: Refutation not found, incomplete strategy % 23.88/4.22 % (582720)Time elapsed: 0.006 s % 23.88/4.22 % (582720)Peak memory usage: 89 MB % 23.88/4.22 % (582720)Instructions burned: 9 (million) % 23.88/4.22 % (582722)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3324148063:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi) % 23.88/4.22 % (582724)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=797352277:i=9925:aac=none_2982 on theBenchmark for (2982ds/9925Mi) % 23.88/4.22 % (582711)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.88/4.22 % (582711)------------------------------ % 23.88/4.22 % (582711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.22 % (582711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.22 % (582711)CaDiCaL version: 2.1.3 % 23.88/4.22 % (582711)Termination reason: Unknown % 23.88/4.22 % (582711)Termination phase: Saturation % 23.88/4.22 % (582711)Time elapsed: 0.365 s % 23.88/4.22 % (582711)Peak memory usage: 114 MB % 23.88/4.22 % (582711)Instructions burned: 542 (million) % 23.88/4.22 % (582718)------------------------------ % 23.88/4.22 % (582718)------------------------------ % 23.88/4.22 % (582720)------------------------------ % 23.88/4.22 % (582720)------------------------------ % 23.88/4.22 % (582728)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=218426559:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2980 on theBenchmark for (2980ds/2479Mi) % 23.88/4.22 % (582728)Refutation not found, incomplete strategy % 23.88/4.22 % (582728)------------------------------ % 23.88/4.22 % (582728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.22 % (582728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.22 % (582728)CaDiCaL version: 2.1.3 % 23.88/4.22 % (582728)Termination reason: Refutation not found, incomplete strategy % 23.88/4.22 % (582728)Time elapsed: 0.007 s % 23.88/4.22 % (582728)Peak memory usage: 88 MB % 23.88/4.22 % (582728)Instructions burned: 10 (million) % 23.88/4.22 % (582729)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2788801619:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/440Mi) % 23.88/4.22 % (582729)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 23.88/4.22 % (582730)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3107616844:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi) % 23.88/4.22 % (582722)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.88/4.22 % (582722)------------------------------ % 23.88/4.22 % (582722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.88/4.22 % (582722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.88/4.22 % (582722)CaDiCaL version: 2.1.3 % 23.88/4.22 % (582722)Termination reason: Unknown % 23.88/4.22 % (582722)Termination phase: Saturation % 23.88/4.22 % (582722)Time elapsed: 0.362 s % 23.88/4.22 % (582722)Peak memory usage: 113 MB % 23.88/4.22 % (582722)Instructions burned: 541 (million) % 23.88/4.22 % (582724)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 30.69/5.20 % (582724)------------------------------ % 30.69/5.20 % (582724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.69/5.20 % (582724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.69/5.20 % (582724)CaDiCaL version: 2.1.3 % 30.69/5.20 % (582724)Termination reason: Unknown % 30.69/5.20 % (582724)Termination phase: Saturation % 30.69/5.20 % (582724)Time elapsed: 0.362 s % 30.69/5.20 % (582724)Peak memory usage: 114 MB % 30.69/5.20 % (582724)Instructions burned: 541 (million) % 30.69/5.20 % (582728)------------------------------ % 30.69/5.20 % (582728)------------------------------ % 30.69/5.20 % (582729)Instruction limit reached! % 30.69/5.20 % (582729)------------------------------ % 30.69/5.20 % (582729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.69/5.20 % (582729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.69/5.20 % (582729)CaDiCaL version: 2.1.3 % 30.69/5.20 % (582729)Termination reason: Instruction limit % 30.69/5.20 % (582729)Termination phase: Saturation % 30.69/5.20 % (582729)Time elapsed: 0.218 s % 30.69/5.20 % (582729)Peak memory usage: 93 MB % 30.69/5.20 % (582729)Instructions burned: 442 (million) % 30.69/5.20 % (582734)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=844451714:cts=off:i=3034:av=off:er=known:fsd=on_2977 on theBenchmark for (2977ds/3034Mi) % 30.69/5.20 % (582735)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3545725445:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi) % 30.69/5.20 % (582736)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1905284934:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2976 on theBenchmark for (2976ds/1016Mi) % 30.69/5.20 % (582737)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=563880586:i=14123:bd=preordered:ins=4_2976 on theBenchmark for (2976ds/14123Mi) % 30.69/5.20 % (582730)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 30.69/5.20 % (582730)------------------------------ % 30.69/5.20 % (582730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.69/5.20 % (582730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.69/5.20 % (582730)CaDiCaL version: 2.1.3 % 30.69/5.20 % (582730)Termination reason: Unknown % 30.69/5.20 % (582730)Termination phase: Saturation % 30.69/5.20 % (582730)Time elapsed: 0.364 s % 30.69/5.20 % (582730)Peak memory usage: 113 MB % 30.69/5.20 % (582730)Instructions burned: 541 (million) % 30.69/5.20 % (582735)Instruction limit reached! % 30.69/5.20 % (582735)------------------------------ % 30.69/5.20 % (582735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.69/5.20 % (582735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.69/5.20 % (582735)CaDiCaL version: 2.1.3 % 30.69/5.20 % (582735)Termination reason: Instruction limit % 30.69/5.20 % (582735)Termination phase: Saturation % 30.69/5.20 % (582735)Time elapsed: 0.274 s % 30.69/5.20 % (582735)Peak memory usage: 92 MB % 30.69/5.20 % (582735)Instructions burned: 526 (million) % 30.69/5.20 % (582742)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3776183091:i=5781:kws=precedence:bd=all:rawr=on_2974 on theBenchmark for (2974ds/5781Mi) % 30.69/5.20 % (582710)Instruction limit reached! % 30.69/5.20 % (582710)------------------------------ % 30.69/5.20 % (582710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.69/5.20 % (582710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.69/5.20 % (582710)CaDiCaL version: 2.1.3 % 30.69/5.20 % (582710)Termination reason: Instruction limit % 30.69/5.20 % (582710)Termination phase: Saturation % 30.69/5.20 % (582710)Time elapsed: 1.250 s % 30.69/5.20 % (582710)Peak memory usage: 133 MB % 30.69/5.20 % (582710)Instructions burned: 4851 (million) % 30.69/5.20 % (582734)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 30.69/5.20 % (582734)------------------------------ % 30.69/5.20 % (582734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.69/5.20 % (582734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.69/5.20 % (582734)CaDiCaL version: 2.1.3 % 30.69/5.20 % (582734)Termination reason: Unknown % 30.69/5.20 % (582734)Termination phase: Saturation % 30.69/5.20 % (582734)Time elapsed: 0.364 s % 30.69/5.20 % (582734)Peak memory usage: 113 MB % 32.78/5.79 % (582734)Instructions burned: 542 (million) % 32.78/5.79 % (582743)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=1024730900:i=2448:gtgl=5:bd=preordered:gtg=all_2973 on theBenchmark for (2973ds/2448Mi) % 32.78/5.79 % (582745)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2248177:i=3223:kws=precedence:fgj=on:av=off_2972 on theBenchmark for (2972ds/3223Mi) % 32.78/5.79 % (582737)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.78/5.79 % (582737)------------------------------ % 32.78/5.79 % (582737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.78/5.79 % (582737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.78/5.79 % (582737)CaDiCaL version: 2.1.3 % 32.78/5.79 % (582737)Termination reason: Unknown % 32.78/5.79 % (582737)Termination phase: Saturation % 32.78/5.79 % (582737)Time elapsed: 0.360 s % 32.78/5.79 % (582737)Peak memory usage: 113 MB % 32.78/5.79 % (582737)Instructions burned: 540 (million) % 32.78/5.79 % (582746)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2770688971:st=5.6:i=2033:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/2033Mi) % 32.78/5.79 % (582749)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=472195131:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2971 on theBenchmark for (2971ds/2055Mi) % 32.78/5.79 % (582736)Instruction limit reached! % 32.78/5.79 % (582736)------------------------------ % 32.78/5.79 % (582736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.78/5.79 % (582736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.78/5.79 % (582736)CaDiCaL version: 2.1.3 % 32.78/5.79 % (582736)Termination reason: Instruction limit % 32.78/5.79 % (582736)Termination phase: Saturation % 32.78/5.79 % (582736)Time elapsed: 0.546 s % 32.78/5.79 % (582736)Peak memory usage: 96 MB % 32.78/5.79 % (582736)Instructions burned: 1018 (million) % 32.78/5.79 % (582745)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.78/5.79 % (582745)------------------------------ % 32.78/5.79 % (582745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.78/5.79 % (582745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.78/5.79 % (582745)CaDiCaL version: 2.1.3 % 32.78/5.79 % (582745)Termination reason: Unknown % 32.78/5.79 % (582745)Termination phase: Saturation % 32.78/5.79 % (582745)Time elapsed: 0.196 s % 32.78/5.79 % (582745)Peak memory usage: 114 MB % 32.78/5.79 % (582745)Instructions burned: 541 (million) % 32.78/5.79 % (582753)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2910486221:i=4835:sd=13:ss=axioms:sgt=23_2969 on theBenchmark for (2969ds/4835Mi) % 32.78/5.79 % (582752)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=923204109:i=21611:sd=3:ss=axioms_2969 on theBenchmark for (2969ds/21611Mi) % 32.78/5.79 % (582743)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.78/5.79 % (582743)------------------------------ % 32.78/5.79 % (582743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.78/5.79 % (582743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.78/5.79 % (582743)CaDiCaL version: 2.1.3 % 32.78/5.79 % (582743)Termination reason: Unknown % 32.78/5.79 % (582743)Termination phase: Saturation % 32.78/5.79 % (582743)Time elapsed: 0.361 s % 32.78/5.79 % (582743)Peak memory usage: 113 MB % 32.78/5.79 % (582743)Instructions burned: 544 (million) % 32.78/5.79 % (582746)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.78/5.79 % (582746)------------------------------ % 32.78/5.79 % (582746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.78/5.79 % (582746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.78/5.79 % (582746)CaDiCaL version: 2.1.3 % 32.78/5.79 % (582746)Termination reason: Unknown % 32.78/5.79 % (582746)Termination phase: Saturation % 32.78/5.79 % (582746)Time elapsed: 0.360 s % 32.78/5.79 % (582746)Peak memory usage: 114 MB % 32.78/5.79 % (582746)Instructions burned: 542 (million) % 32.78/5.79 % (582756)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=891260245:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2967 on theBenchmark for (2967ds/797Mi) % 39.21/6.43 % (582749)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.21/6.43 % (582749)------------------------------ % 39.21/6.43 % (582749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.21/6.43 % (582749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.21/6.43 % (582749)CaDiCaL version: 2.1.3 % 39.21/6.43 % (582749)Termination reason: Unknown % 39.21/6.43 % (582749)Termination phase: Saturation % 39.21/6.43 % (582749)Time elapsed: 0.361 s % 39.21/6.43 % (582749)Peak memory usage: 114 MB % 39.21/6.43 % (582749)Instructions burned: 541 (million) % 39.21/6.43 % (582757)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2885981456:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2967 on theBenchmark for (2967ds/2326Mi) % 39.21/6.43 % (582752)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.21/6.43 % (582752)------------------------------ % 39.21/6.43 % (582752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.21/6.43 % (582752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.21/6.43 % (582752)CaDiCaL version: 2.1.3 % 39.21/6.43 % (582752)Termination reason: Unknown % 39.21/6.43 % (582752)Termination phase: Saturation % 39.21/6.43 % (582752)Time elapsed: 0.362 s % 39.21/6.43 % (582752)Peak memory usage: 113 MB % 39.21/6.43 % (582752)Instructions burned: 540 (million) % 39.21/6.43 % (582759)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1479165649:i=6038:nm=6_2966 on theBenchmark for (2966ds/6038Mi) % 39.21/6.43 % (582761)lrs+10_1_sil=32000:sp=occurrence:random_seed=1678617166:st=2:i=33334:sd=3:ss=included:sgt=32_2964 on theBenchmark for (2964ds/33334Mi) % 39.21/6.43 % (582756)Instruction limit reached! % 39.21/6.43 % (582756)------------------------------ % 39.21/6.43 % (582756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.21/6.43 % (582756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.21/6.43 % (582756)CaDiCaL version: 2.1.3 % 39.21/6.43 % (582756)Termination reason: Instruction limit % 39.21/6.43 % (582756)Termination phase: Saturation % 39.21/6.43 % (582756)Time elapsed: 0.444 s % 39.21/6.43 % (582756)Peak memory usage: 103 MB % 39.21/6.43 % (582756)Instructions burned: 799 (million) % 39.21/6.43 % (582719)Instruction limit reached! % 39.21/6.43 % (582719)------------------------------ % 39.21/6.43 % (582719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.21/6.43 % (582719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.21/6.43 % (582719)CaDiCaL version: 2.1.3 % 39.21/6.43 % (582719)Termination reason: Instruction limit % 39.21/6.43 % (582719)Termination phase: Saturation % 39.21/6.43 % (582719)Time elapsed: 2.090 s % 39.21/6.43 % (582719)Peak memory usage: 112 MB % 39.21/6.43 % (582719)Instructions burned: 3707 (million) % 39.21/6.43 % (582759)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.21/6.43 % (582759)------------------------------ % 39.21/6.43 % (582759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.21/6.43 % (582759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.21/6.43 % (582759)CaDiCaL version: 2.1.3 % 39.21/6.43 % (582759)Termination reason: Unknown % 39.21/6.43 % (582759)Termination phase: Saturation % 39.21/6.43 % (582759)Time elapsed: 0.359 s % 39.21/6.43 % (582759)Peak memory usage: 113 MB % 39.21/6.43 % (582759)Instructions burned: 542 (million) % 39.21/6.43 % (582764)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3744029845:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2961 on theBenchmark for (2961ds/1008Mi) % 39.21/6.43 % (582765)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=2117909189:i=8327:s2at=5:bd=preordered_2961 on theBenchmark for (2961ds/8327Mi) % 39.21/6.43 % (582766)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=4005743098:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2960 on theBenchmark for (2960ds/1083Mi) % 39.21/6.43 % (582765)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.30/6.99 % (582765)------------------------------ % 41.30/6.99 % (582765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.30/6.99 % (582765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.30/6.99 % (582765)CaDiCaL version: 2.1.3 % 41.30/6.99 % (582765)Termination reason: Unknown % 41.30/6.99 % (582765)Termination phase: Saturation % 41.30/6.99 % (582765)Time elapsed: 0.356 s % 41.30/6.99 % (582765)Peak memory usage: 113 MB % 41.30/6.99 % (582765)Instructions burned: 540 (million) % 41.30/6.99 % (582757)Instruction limit reached! % 41.30/6.99 % (582757)------------------------------ % 41.30/6.99 % (582757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.30/6.99 % (582757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.30/6.99 % (582757)CaDiCaL version: 2.1.3 % 41.30/6.99 % (582757)Termination reason: Instruction limit % 41.30/6.99 % (582757)Termination phase: Saturation % 41.30/6.99 % (582757)Time elapsed: 0.978 s % 41.30/6.99 % (582757)Peak memory usage: 97 MB % 41.30/6.99 % (582757)Instructions burned: 2328 (million) % 41.30/6.99 % (582764)Instruction limit reached! % 41.30/6.99 % (582764)------------------------------ % 41.30/6.99 % (582764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.30/6.99 % (582764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.30/6.99 % (582764)CaDiCaL version: 2.1.3 % 41.30/6.99 % (582764)Termination reason: Instruction limit % 41.30/6.99 % (582764)Termination phase: Saturation % 41.30/6.99 % (582764)Time elapsed: 0.447 s % 41.30/6.99 % (582764)Peak memory usage: 93 MB % 41.30/6.99 % (582764)Instructions burned: 1009 (million) % 41.30/6.99 % (582770)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1161786521:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2956 on theBenchmark for (2956ds/1084Mi) % 41.30/6.99 % (582753)Instruction limit reached! % 41.30/6.99 % (582753)------------------------------ % 41.30/6.99 % (582753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.30/6.99 % (582753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.30/6.99 % (582753)CaDiCaL version: 2.1.3 % 41.30/6.99 % (582753)Termination reason: Instruction limit % 41.30/6.99 % (582753)Termination phase: Saturation % 41.30/6.99 % (582753)Time elapsed: 1.368 s % 41.30/6.99 % (582753)Peak memory usage: 112 MB % 41.30/6.99 % (582753)Instructions burned: 4836 (million) % 41.30/6.99 % (582766)Instruction limit reached! % 41.30/6.99 % (582766)------------------------------ % 41.30/6.99 % (582766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.30/6.99 % (582766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.30/6.99 % (582766)CaDiCaL version: 2.1.3 % 41.30/6.99 % (582766)Termination reason: Instruction limit % 41.30/6.99 % (582766)Termination phase: Saturation % 41.30/6.99 % (582766)Time elapsed: 0.488 s % 41.30/6.99 % (582766)Peak memory usage: 96 MB % 41.30/6.99 % (582766)Instructions burned: 1083 (million) % 41.30/6.99 % (582771)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2279124852:i=6995:s2at=5:gtg=all_2955 on theBenchmark for (2955ds/6995Mi) % 41.30/6.99 % (582772)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=4118360436:st=2:i=6225:sd=15:ss=axioms_2955 on theBenchmark for (2955ds/6225Mi) % 41.30/6.99 % (582774)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3231448812:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2954 on theBenchmark for (2954ds/3372Mi) % 41.30/6.99 % (582775)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3165921866:st=2.3:i=26457:sd=10:ss=included:sgt=8_2954 on theBenchmark for (2954ds/26457Mi) % 41.30/6.99 % (582774)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.30/6.99 % (582774)------------------------------ % 41.30/6.99 % (582774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.30/6.99 % (582774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.30/6.99 % (582774)CaDiCaL version: 2.1.3 % 41.30/6.99 % (582774)Termination reason: Unknown % 41.30/6.99 % (582774)Termination phase: Saturation % 41.30/6.99 % (582774)Time elapsed: 0.193 s % 41.30/6.99 % (582774)Peak memory usage: 113 MB % 41.30/6.99 % (582774)Instructions burned: 539 (million) % 41.30/6.99 % (582771)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 48.07/7.88 % (582771)------------------------------ % 48.07/7.88 % (582771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.07/7.88 % (582771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.07/7.88 % (582771)CaDiCaL version: 2.1.3 % 48.07/7.88 % (582771)Termination reason: Unknown % 48.07/7.88 % (582771)Termination phase: Saturation % 48.07/7.88 % (582771)Time elapsed: 0.360 s % 48.07/7.88 % (582771)Peak memory usage: 114 MB % 48.07/7.88 % (582771)Instructions burned: 544 (million) % 48.07/7.88 % (582780)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=612170029:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2951 on theBenchmark for (2951ds/13494Mi) % 48.07/7.88 % (582775)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 48.07/7.88 % (582775)------------------------------ % 48.07/7.88 % (582775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.07/7.88 % (582775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.07/7.88 % (582775)CaDiCaL version: 2.1.3 % 48.07/7.88 % (582775)Termination reason: Unknown % 48.07/7.88 % (582775)Termination phase: Saturation % 48.07/7.88 % (582775)Time elapsed: 0.358 s % 48.07/7.88 % (582775)Peak memory usage: 113 MB % 48.07/7.88 % (582775)Instructions burned: 541 (million) % 48.07/7.88 % (582770)Instruction limit reached! % 48.07/7.88 % (582770)------------------------------ % 48.07/7.88 % (582770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.07/7.88 % (582770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.07/7.88 % (582770)CaDiCaL version: 2.1.3 % 48.07/7.88 % (582770)Termination reason: Instruction limit % 48.07/7.88 % (582770)Termination phase: Saturation % 48.07/7.88 % (582770)Time elapsed: 0.562 s % 48.07/7.88 % (582770)Peak memory usage: 96 MB % 48.07/7.88 % (582770)Instructions burned: 1085 (million) % 48.07/7.88 % (582781)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=2108820387:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2950 on theBenchmark for (2950ds/2503Mi) % 48.07/7.88 % (582781)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 48.07/7.88 % (582780)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 48.07/7.88 % (582780)------------------------------ % 48.07/7.88 % (582780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.07/7.88 % (582780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.07/7.88 % (582780)CaDiCaL version: 2.1.3 % 48.07/7.88 % (582780)Termination reason: Unknown % 48.07/7.88 % (582780)Termination phase: Saturation % 48.07/7.88 % (582780)Time elapsed: 0.197 s % 48.07/7.88 % (582780)Peak memory usage: 114 MB % 48.07/7.88 % (582780)Instructions burned: 543 (million) % 48.07/7.88 % (582784)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3976993689:i=30753:av=off:ss=included_2949 on theBenchmark for (2949ds/30753Mi) % 48.07/7.88 % (582783)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3655693319:i=2559:sd=1:ep=RSTC:ss=axioms_2949 on theBenchmark for (2949ds/2559Mi) % 48.07/7.88 % (582786)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=42853029:i=26473:ep=RSTC_2948 on theBenchmark for (2948ds/26473Mi) % 48.07/7.88 % (582781)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 48.07/7.88 % (582781)------------------------------ % 48.07/7.88 % (582781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.07/7.88 % (582781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.07/7.88 % (582781)CaDiCaL version: 2.1.3 % 48.07/7.88 % (582781)Termination reason: Unknown % 48.07/7.88 % (582781)Termination phase: Saturation % 48.07/7.88 % (582781)Time elapsed: 0.359 s % 48.07/7.88 % (582781)Peak memory usage: 113 MB % 48.07/7.88 % (582781)Instructions burned: 540 (million) % 48.07/7.88 % (582783)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 48.07/7.88 % (582783)------------------------------ % 48.07/7.88 % (582783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.07/7.88 % (582783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.07/7.88 % (582783)CaDiCaL version: 2.1.3 % 53.44/8.41 % (582783)Termination reason: Unknown % 53.44/8.41 % (582783)Termination phase: Saturation % 53.44/8.41 % (582783)Time elapsed: 0.357 s % 53.44/8.41 % (582783)Peak memory usage: 113 MB % 53.44/8.41 % (582783)Instructions burned: 539 (million) % 53.44/8.41 % (582784)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.44/8.41 % (582784)------------------------------ % 53.44/8.41 % (582784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.44/8.41 % (582784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.44/8.41 % (582784)CaDiCaL version: 2.1.3 % 53.44/8.41 % (582784)Termination reason: Unknown % 53.44/8.41 % (582784)Termination phase: Saturation % 53.44/8.41 % (582784)Time elapsed: 0.357 s % 53.44/8.41 % (582784)Peak memory usage: 113 MB % 53.44/8.41 % (582784)Instructions burned: 542 (million) % 53.44/8.41 % (582790)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=1900869288:cts=off:i=2759:kws=inv_arity:fgj=on_2945 on theBenchmark for (2945ds/2759Mi) % 53.44/8.41 % (582792)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=2581778107:i=1532:ep=RS:ss=axioms_2944 on theBenchmark for (2944ds/1532Mi) % 53.44/8.41 % (582791)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=2156917034:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/5665Mi) % 53.44/8.41 % (582791)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 53.44/8.41 % (582742)Instruction limit reached! % 53.44/8.41 % (582742)------------------------------ % 53.44/8.41 % (582742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.44/8.41 % (582742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.44/8.41 % (582742)CaDiCaL version: 2.1.3 % 53.44/8.41 % (582742)Termination reason: Instruction limit % 53.44/8.41 % (582742)Termination phase: Saturation % 53.44/8.41 % (582742)Time elapsed: 3.244 s % 53.44/8.41 % (582742)Peak memory usage: 113 MB % 53.44/8.41 % (582742)Instructions burned: 5783 (million) % 53.44/8.41 % (582790)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.44/8.41 % (582790)------------------------------ % 53.44/8.41 % (582790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.44/8.41 % (582790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.44/8.41 % (582790)CaDiCaL version: 2.1.3 % 53.44/8.41 % (582790)Termination reason: Unknown % 53.44/8.41 % (582790)Termination phase: Saturation % 53.44/8.41 % (582790)Time elapsed: 0.359 s % 53.44/8.41 % (582790)Peak memory usage: 114 MB % 53.44/8.41 % (582790)Instructions burned: 543 (million) % 53.44/8.41 % (582791)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.44/8.41 % (582792)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.44/8.41 % (582792)------------------------------ % 53.44/8.41 % (582792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.44/8.41 % (582791)------------------------------ % 53.44/8.41 % (582791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.44/8.41 % (582791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.44/8.41 % (582792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.44/8.41 % (582792)CaDiCaL version: 2.1.3 % 53.44/8.41 % (582791)CaDiCaL version: 2.1.3 % 53.44/8.41 % (582791)Termination reason: Unknown % 53.44/8.41 % (582791)Termination phase: Saturation % 53.44/8.41 % (582792)Termination reason: Unknown % 53.44/8.41 % (582792)Termination phase: Saturation % 53.44/8.41 % (582791)Time elapsed: 0.359 s % 53.44/8.41 % (582792)Time elapsed: 0.359 s % 53.44/8.41 % (582791)Peak memory usage: 112 MB % 53.44/8.41 % (582792)Peak memory usage: 112 MB % 53.44/8.41 % (582792)Instructions burned: 542 (million) % 53.44/8.41 % (582791)Instructions burned: 541 (million) % 53.44/8.41 % (582796)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3683533020:i=1565:sd=2:ss=axioms:sgt=32_2940 on theBenchmark for (2940ds/1565Mi) % 53.44/8.41 % (582797)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=510352551:i=1572:fgj=on:gsp=on_2940 on theBenchmark for (2940ds/1572Mi) % 58.26/9.05 % (582797)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 58.26/9.05 % (582798)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=127869464:i=6052:sd=4:ss=axioms:sgt=24_2938 on theBenchmark for (2938ds/6052Mi) % 58.26/9.05 % (582799)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=923123121:i=3500:sd=1:bd=preordered:sup=off:ss=included_2938 on theBenchmark for (2938ds/3500Mi) % 58.26/9.05 % (582796)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 58.26/9.05 % (582796)------------------------------ % 58.26/9.05 % (582796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.26/9.05 % (582797)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 58.26/9.05 % (582796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.26/9.05 % (582797)------------------------------ % 58.26/9.05 % (582797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.26/9.05 % (582797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.26/9.05 % (582796)CaDiCaL version: 2.1.3 % 58.26/9.05 % (582796)Termination reason: Unknown % 58.26/9.05 % (582796)Termination phase: Saturation % 58.26/9.05 % (582796)Time elapsed: 0.359 s % 58.26/9.05 % (582797)CaDiCaL version: 2.1.3 % 58.26/9.05 % (582796)Peak memory usage: 112 MB % 58.26/9.05 % (582797)Termination reason: Unknown % 58.26/9.05 % (582797)Termination phase: Saturation % 58.26/9.05 % (582797)Time elapsed: 0.359 s % 58.26/9.05 % (582796)Instructions burned: 541 (million) % 58.26/9.05 % (582797)Peak memory usage: 112 MB % 58.26/9.05 % (582797)Instructions burned: 542 (million) % 58.26/9.05 % (582798)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 58.26/9.05 % (582799)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 58.26/9.05 % (582798)------------------------------ % 58.26/9.05 % (582798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.26/9.05 % (582799)------------------------------ % 58.26/9.05 % (582799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.26/9.05 % (582799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.26/9.05 % (582798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.26/9.05 % (582798)CaDiCaL version: 2.1.3 % 58.26/9.05 % (582799)CaDiCaL version: 2.1.3 % 58.26/9.05 % (582799)Termination reason: Unknown % 58.26/9.05 % (582799)Termination phase: Saturation % 58.26/9.05 % (582799)Time elapsed: 0.357 s % 58.26/9.05 % (582798)Termination reason: Unknown % 58.26/9.05 % (582798)Termination phase: Saturation % 58.26/9.05 % (582799)Peak memory usage: 112 MB % 58.26/9.05 % (582798)Time elapsed: 0.357 s % 58.26/9.05 % (582799)Instructions burned: 542 (million) % 58.26/9.05 % (582798)Peak memory usage: 112 MB % 58.26/9.05 % (582798)Instructions burned: 540 (million) % 58.26/9.05 % (582805)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=389332466:i=66096:add=on_2935 on theBenchmark for (2935ds/66096Mi) % 58.26/9.05 % (582804)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=4251063970:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2935 on theBenchmark for (2935ds/1842Mi) % 58.26/9.05 % (582804)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 58.26/9.05 % (582807)lrs-1011_4:1_sil=16000:bsr=on:random_seed=598070007:cts=off:i=5469:bs=on:fsr=off_2933 on theBenchmark for (2933ds/5469Mi) % 58.26/9.05 % (582806)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2298017053:i=1884:sd=1:nm=60:ss=axioms_2933 on theBenchmark for (2933ds/1884Mi) % 58.26/9.05 % (582804)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 58.26/9.05 % (582805)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 58.26/9.05 % (582804)------------------------------ % 58.26/9.05 % (582804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.26/9.05 % (582805)------------------------------ % 58.26/9.05 % (582805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.63/9.92 % (582804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.63/9.92 % (582805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.63/9.92 % (582804)CaDiCaL version: 2.1.3 % 62.63/9.92 % (582805)CaDiCaL version: 2.1.3 % 62.63/9.92 % (582804)Termination reason: Unknown % 62.63/9.92 % (582804)Termination phase: Saturation % 62.63/9.92 % (582805)Termination reason: Unknown % 62.63/9.92 % (582805)Termination phase: Saturation % 62.63/9.92 % (582804)Time elapsed: 0.360 s % 62.63/9.92 % (582805)Time elapsed: 0.360 s % 62.63/9.92 % (582804)Peak memory usage: 112 MB % 62.63/9.92 % (582805)Peak memory usage: 112 MB % 62.63/9.92 % (582804)Instructions burned: 541 (million) % 62.63/9.92 % (582805)Instructions burned: 542 (million) % 62.63/9.92 % (582772)Instruction limit reached! % 62.63/9.92 % (582772)------------------------------ % 62.63/9.92 % (582772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.63/9.92 % (582772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.63/9.92 % (582772)CaDiCaL version: 2.1.3 % 62.63/9.92 % (582772)Termination reason: Instruction limit % 62.63/9.92 % (582772)Termination phase: Saturation % 62.63/9.92 % (582772)Time elapsed: 2.462 s % 62.63/9.92 % (582772)Peak memory usage: 99 MB % 62.63/9.92 % (582772)Instructions burned: 6225 (million) % 62.63/9.92 % (582806)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 62.63/9.92 % (582806)------------------------------ % 62.63/9.92 % (582806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.63/9.92 % (582806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.63/9.92 % (582806)CaDiCaL version: 2.1.3 % 62.63/9.92 % (582806)Termination reason: Unknown % 62.63/9.92 % (582806)Termination phase: Saturation % 62.63/9.92 % (582806)Time elapsed: 0.357 s % 62.63/9.92 % (582806)Peak memory usage: 113 MB % 62.63/9.92 % (582806)Instructions burned: 539 (million) % 62.63/9.92 % (582812)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=1331392812:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2929 on theBenchmark for (2929ds/2037Mi) % 62.63/9.92 % (582813)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1236576928:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2929 on theBenchmark for (2929ds/2110Mi) % 62.63/9.92 % (582814)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=3350554605:i=2430:add=off:aac=none:nm=16_2929 on theBenchmark for (2929ds/2430Mi) % 62.63/9.92 % (582815)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=3632762703:cond=fast:i=4891_2928 on theBenchmark for (2928ds/4891Mi) % 62.63/9.92 % (582812)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 62.63/9.92 % (582812)------------------------------ % 62.63/9.92 % (582812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.63/9.92 % (582812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.63/9.92 % (582812)CaDiCaL version: 2.1.3 % 62.63/9.92 % (582812)Termination reason: Unknown % 62.63/9.92 % (582812)Termination phase: Saturation % 62.63/9.92 % (582812)Time elapsed: 0.360 s % 62.63/9.92 % (582812)Peak memory usage: 114 MB % 62.63/9.92 % (582812)Instructions burned: 547 (million) % 62.63/9.92 % (582813)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 62.63/9.92 % (582813)------------------------------ % 62.63/9.92 % (582813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.63/9.92 % (582813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.63/9.92 % (582813)CaDiCaL version: 2.1.3 % 62.63/9.92 % (582813)Termination reason: Unknown % 62.63/9.92 % (582813)Termination phase: Saturation % 62.63/9.92 % (582813)Time elapsed: 0.361 s % 62.63/9.92 % (582813)Peak memory usage: 113 MB % 62.63/9.92 % (582813)Instructions burned: 546 (million) % 62.63/9.92 % (582814)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 62.63/9.92 % (582814)------------------------------ % 62.63/9.92 % (582814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.63/9.92 % (582814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.61/10.43 % (582814)CaDiCaL version: 2.1.3 % 67.61/10.43 % (582814)Termination reason: Unknown % 67.61/10.43 % (582814)Termination phase: Saturation % 67.61/10.43 % (582814)Time elapsed: 0.360 s % 67.61/10.43 % (582814)Peak memory usage: 114 MB % 67.61/10.43 % (582814)Instructions burned: 541 (million) % 67.61/10.43 % (582815)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.61/10.43 % (582815)------------------------------ % 67.61/10.43 % (582815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.61/10.43 % (582815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.61/10.43 % (582815)CaDiCaL version: 2.1.3 % 67.61/10.43 % (582815)Termination reason: Unknown % 67.61/10.43 % (582815)Termination phase: Saturation % 67.61/10.43 % (582815)Time elapsed: 0.359 s % 67.61/10.43 % (582815)Peak memory usage: 114 MB % 67.61/10.43 % (582815)Instructions burned: 542 (million) % 67.61/10.43 % (582820)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=2269443435:st=2:i=14845:sd=2:ss=included:fsd=on_2924 on theBenchmark for (2924ds/14845Mi) % 67.61/10.43 % (582821)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2412554673:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2924 on theBenchmark for (2924ds/7534Mi) % 67.61/10.43 % (582822)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=471905854:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2924 on theBenchmark for (2924ds/10353Mi) % 67.61/10.43 % (582823)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1312156238:i=7860_2923 on theBenchmark for (2923ds/7860Mi) % 67.61/10.43 % (582823)Refutation not found, incomplete strategy % 67.61/10.43 % (582823)------------------------------ % 67.61/10.43 % (582823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.61/10.43 % (582823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.61/10.43 % (582823)CaDiCaL version: 2.1.3 % 67.61/10.43 % (582823)Termination reason: Refutation not found, incomplete strategy % 67.61/10.43 % (582823)Time elapsed: 0.006 s % 67.61/10.43 % (582823)Peak memory usage: 88 MB % 67.61/10.43 % (582823)Instructions burned: 10 (million) % 67.61/10.43 % (582821)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.61/10.43 % (582820)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.61/10.43 % (582820)------------------------------ % 67.61/10.43 % (582820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.61/10.43 % (582821)------------------------------ % 67.61/10.43 % (582821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.61/10.43 % (582820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.61/10.43 % (582821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.61/10.43 % (582820)CaDiCaL version: 2.1.3 % 67.61/10.43 % (582821)CaDiCaL version: 2.1.3 % 67.61/10.43 % (582820)Termination reason: Unknown % 67.61/10.43 % (582820)Termination phase: Saturation % 67.61/10.43 % (582820)Time elapsed: 0.361 s % 67.61/10.43 % (582820)Peak memory usage: 113 MB % 67.61/10.43 % (582820)Instructions burned: 541 (million) % 67.61/10.43 % (582821)Termination reason: Unknown % 67.61/10.43 % (582821)Termination phase: Saturation % 67.61/10.43 % (582821)Time elapsed: 0.361 s % 67.61/10.43 % (582821)Peak memory usage: 113 MB % 67.61/10.43 % (582821)Instructions burned: 543 (million) % 67.61/10.43 % (582823)------------------------------ % 67.61/10.43 % (582823)------------------------------ % 67.61/10.43 % (582822)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.61/10.43 % (582822)------------------------------ % 67.61/10.43 % (582822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.61/10.43 % (582822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.61/10.43 % (582822)CaDiCaL version: 2.1.3 % 67.61/10.43 % (582822)Termination reason: Unknown % 67.61/10.43 % (582822)Termination phase: Saturation % 67.61/10.43 % (582822)Time elapsed: 0.362 s % 67.61/10.43 % (582822)Peak memory usage: 113 MB % 67.61/10.43 % (582822)Instructions burned: 541 (million) % 67.61/10.43 % (582828)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=2048560250:i=7896:sd=2:bs=on:ss=included:sgt=20_2919 on theBenchmark for (2919ds/7896Mi) % 72.48/11.04 % (582829)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1162708472:i=5812:gtgl=2:gtg=all_2919 on theBenchmark for (2919ds/5812Mi) % 72.48/11.04 % (582830)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=242955390:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2919 on theBenchmark for (2919ds/2965Mi) % 72.48/11.04 % (582831)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=1577658021:i=2967:kws=precedence:bd=preordered:av=off_2919 on theBenchmark for (2919ds/2967Mi) % 72.48/11.04 % (582829)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.48/11.04 % (582829)------------------------------ % 72.48/11.04 % (582829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.48/11.04 % (582829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.48/11.04 % (582828)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.48/11.04 % (582828)------------------------------ % 72.48/11.04 % (582828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.48/11.04 % (582829)CaDiCaL version: 2.1.3 % 72.48/11.04 % (582829)Termination reason: Unknown % 72.48/11.04 % (582829)Termination phase: Saturation % 72.48/11.04 % (582828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.48/11.04 % (582829)Time elapsed: 0.356 s % 72.48/11.04 % (582829)Peak memory usage: 113 MB % 72.48/11.04 % (582829)Instructions burned: 544 (million) % 72.48/11.04 % (582828)CaDiCaL version: 2.1.3 % 72.48/11.04 % (582828)Termination reason: Unknown % 72.48/11.04 % (582828)Termination phase: Saturation % 72.48/11.04 % (582828)Time elapsed: 0.356 s % 72.48/11.04 % (582828)Peak memory usage: 112 MB % 72.48/11.04 % (582828)Instructions burned: 540 (million) % 72.48/11.04 % (582830)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.48/11.04 % (582830)------------------------------ % 72.48/11.04 % (582830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.48/11.04 % (582830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.48/11.04 % (582830)CaDiCaL version: 2.1.3 % 72.48/11.04 % (582830)Termination reason: Unknown % 72.48/11.04 % (582830)Termination phase: Saturation % 72.48/11.04 % (582830)Time elapsed: 0.356 s % 72.48/11.04 % (582830)Peak memory usage: 114 MB % 72.48/11.04 % (582830)Instructions burned: 542 (million) % 72.48/11.04 % (582831)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.48/11.04 % (582831)------------------------------ % 72.48/11.04 % (582831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.48/11.04 % (582831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.48/11.04 % (582831)CaDiCaL version: 2.1.3 % 72.48/11.04 % (582831)Termination reason: Unknown % 72.48/11.04 % (582831)Termination phase: Saturation % 72.48/11.04 % (582831)Time elapsed: 0.359 s % 72.48/11.04 % (582831)Peak memory usage: 114 MB % 72.48/11.04 % (582831)Instructions burned: 541 (million) % 72.48/11.04 % (582836)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=4275749163:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2914 on theBenchmark for (2914ds/3022Mi) % 72.48/11.04 % (582837)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=2448418071:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2914 on theBenchmark for (2914ds/3207Mi) % 72.48/11.04 % (582838)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=4066284426:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2914 on theBenchmark for (2914ds/3289Mi) % 72.48/11.04 % (582839)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2100352987:i=38569:sd=3:ss=axioms:sgt=32_2913 on theBenchmark for (2913ds/38569Mi) % 72.48/11.04 % (582836)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.48/11.04 % (582836)------------------------------ % 72.48/11.04 % (582836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.60/11.86 % (582836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.60/11.86 % (582836)CaDiCaL version: 2.1.3 % 76.60/11.86 % (582836)Termination reason: Unknown % 76.60/11.86 % (582836)Termination phase: Saturation % 76.60/11.86 % (582836)Time elapsed: 0.357 s % 76.60/11.86 % (582836)Peak memory usage: 112 MB % 76.60/11.86 % (582836)Instructions burned: 540 (million) % 76.60/11.86 % (582837)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 76.60/11.86 % (582837)------------------------------ % 76.60/11.86 % (582837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.60/11.86 % (582837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.60/11.86 % (582837)CaDiCaL version: 2.1.3 % 76.60/11.86 % (582837)Termination reason: Unknown % 76.60/11.86 % (582837)Termination phase: Saturation % 76.60/11.86 % (582837)Time elapsed: 0.357 s % 76.60/11.86 % (582837)Peak memory usage: 112 MB % 76.60/11.86 % (582837)Instructions burned: 541 (million) % 76.60/11.86 % (582838)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 76.60/11.86 % (582838)------------------------------ % 76.60/11.86 % (582838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.60/11.86 % (582838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.60/11.86 % (582838)CaDiCaL version: 2.1.3 % 76.60/11.86 % (582838)Termination reason: Unknown % 76.60/11.86 % (582838)Termination phase: Saturation % 76.60/11.86 % (582838)Time elapsed: 0.356 s % 76.60/11.86 % (582838)Peak memory usage: 113 MB % 76.60/11.86 % (582838)Instructions burned: 541 (million) % 76.60/11.86 % (582839)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 76.60/11.86 % (582839)------------------------------ % 76.60/11.86 % (582839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.60/11.86 % (582839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.60/11.86 % (582839)CaDiCaL version: 2.1.3 % 76.60/11.86 % (582839)Termination reason: Unknown % 76.60/11.86 % (582839)Termination phase: Saturation % 76.60/11.86 % (582839)Time elapsed: 0.360 s % 76.60/11.86 % (582839)Peak memory usage: 114 MB % 76.60/11.86 % (582839)Instructions burned: 542 (million) % 76.60/11.86 % (582844)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3432245735:cts=off:i=3394_2909 on theBenchmark for (2909ds/3394Mi) % 76.60/11.86 % (582845)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=1657679173:i=33824:bd=preordered_2909 on theBenchmark for (2909ds/33824Mi) % 76.60/11.86 % (582846)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2213976392:i=20684:bd=all:gtg=exists_sym_2909 on theBenchmark for (2909ds/20684Mi) % 76.60/11.86 % (582847)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=1563698155: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_2908 on theBenchmark for (2908ds/7222Mi) % 76.60/11.86 % (582847)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 76.60/11.86 % (582844)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 76.60/11.86 % (582845)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 76.60/11.86 % (582844)------------------------------ % 76.60/11.86 % (582844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.60/11.86 % (582845)------------------------------ % 76.60/11.86 % (582845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.60/11.86 % (582845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.60/11.86 % (582844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.60/11.86 % (582845)CaDiCaL version: 2.1.3 % 76.60/11.86 % (582844)CaDiCaL version: 2.1.3 % 76.60/11.86 % (582845)Termination reason: Unknown % 76.60/11.86 % (582845)Termination phase: Saturation % 76.60/11.86 % (582844)Termination reason: Unknown % 76.60/11.86 % (582844)Termination phase: Saturation % 76.60/11.86 % (582845)Time elapsed: 0.358 s % 76.60/11.86 % (582844)Time elapsed: 0.358 s % 76.60/11.86 % (582845)Peak memory usage: 113 MB % 76.60/11.86 % (582844)Peak memory usage: 112 MB % 76.60/11.86 % (582844)Instructions burned: 541 (million) % 81.40/12.57 % (582845)Instructions burned: 542 (million) % 81.40/12.57 % (582846)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.40/12.57 % (582846)------------------------------ % 81.40/12.57 % (582846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.40/12.57 % (582846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.40/12.57 % (582846)CaDiCaL version: 2.1.3 % 81.40/12.57 % (582846)Termination reason: Unknown % 81.40/12.57 % (582846)Termination phase: Saturation % 81.40/12.57 % (582846)Time elapsed: 0.357 s % 81.40/12.57 % (582846)Peak memory usage: 114 MB % 81.40/12.57 % (582846)Instructions burned: 544 (million) % 81.40/12.57 % (582847)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.40/12.57 % (582847)------------------------------ % 81.40/12.57 % (582847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.40/12.57 % (582847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.40/12.57 % (582847)CaDiCaL version: 2.1.3 % 81.40/12.57 % (582847)Termination reason: Unknown % 81.40/12.57 % (582847)Termination phase: Saturation % 81.40/12.57 % (582847)Time elapsed: 0.362 s % 81.40/12.57 % (582847)Peak memory usage: 114 MB % 81.40/12.57 % (582847)Instructions burned: 546 (million) % 81.40/12.57 % (582853)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=3462898133:i=4036:ins=10_2904 on theBenchmark for (2904ds/4036Mi) % 81.40/12.57 % (582852)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3390218307:st=4:i=7295:sd=4:ep=R:ss=axioms_2904 on theBenchmark for (2904ds/7295Mi) % 81.40/12.57 % (582854)lrs+10_1_sil=128000:lcm=predicate:random_seed=1341097231:st=3:i=43697:sd=5:ss=axioms_2904 on theBenchmark for (2904ds/43697Mi) % 81.40/12.57 % (582855)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=1457092996:i=17599:gtg=all:ss=axioms:fsd=on_2903 on theBenchmark for (2903ds/17599Mi) % 81.40/12.57 % (582807)Instruction limit reached! % 81.40/12.57 % (582807)------------------------------ % 81.40/12.57 % (582807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.40/12.57 % (582807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.40/12.57 % (582807)CaDiCaL version: 2.1.3 % 81.40/12.57 % (582807)Termination reason: Instruction limit % 81.40/12.57 % (582807)Termination phase: Saturation % 81.40/12.57 % (582807)Time elapsed: 3.173 s % 81.40/12.57 % (582807)Peak memory usage: 116 MB % 81.40/12.57 % (582807)Instructions burned: 5469 (million) % 81.40/12.57 % (582852)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.40/12.57 % (582852)------------------------------ % 81.40/12.57 % (582852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.40/12.57 % (582852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.40/12.57 % (582852)CaDiCaL version: 2.1.3 % 81.40/12.57 % (582852)Termination reason: Unknown % 81.40/12.57 % (582852)Termination phase: Saturation % 81.40/12.57 % (582852)Time elapsed: 0.359 s % 81.40/12.57 % (582852)Peak memory usage: 113 MB % 81.40/12.57 % (582852)Instructions burned: 543 (million) % 81.40/12.57 % (582853)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.40/12.57 % (582853)------------------------------ % 81.40/12.57 % (582853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.40/12.57 % (582853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.40/12.57 % (582853)CaDiCaL version: 2.1.3 % 81.40/12.57 % (582853)Termination reason: Unknown % 81.40/12.57 % (582853)Termination phase: Saturation % 81.40/12.57 % (582853)Time elapsed: 0.359 s % 81.40/12.57 % (582853)Peak memory usage: 113 MB % 81.40/12.57 % (582853)Instructions burned: 540 (million) % 81.40/12.57 % (582860)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=1164323986:i=4547:bd=preordered_2900 on theBenchmark for (2900ds/4547Mi) % 81.40/12.57 % (582855)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.40/12.57 % (582855)------------------------------ % 81.40/12.57 % (582855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.40/12.57 % (582855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.06/13.67 % (582855)CaDiCaL version: 2.1.3 % 90.06/13.67 % (582855)Termination reason: Unknown % 90.06/13.67 % (582855)Termination phase: Saturation % 90.06/13.67 % (582855)Time elapsed: 0.362 s % 90.06/13.67 % (582855)Peak memory usage: 114 MB % 90.06/13.67 % (582855)Instructions burned: 543 (million) % 90.06/13.67 % (582862)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3767076760:i=32849:add=on_2899 on theBenchmark for (2899ds/32849Mi) % 90.06/13.67 % (582861)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=3463827208:i=9294:av=off_2899 on theBenchmark for (2899ds/9294Mi) % 90.06/13.67 % (582864)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1350932641:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2898 on theBenchmark for (2898ds/4793Mi) % 90.06/13.67 % (582860)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 90.06/13.67 % (582860)------------------------------ % 90.06/13.67 % (582860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.06/13.67 % (582860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.06/13.67 % (582860)CaDiCaL version: 2.1.3 % 90.06/13.67 % (582860)Termination reason: Unknown % 90.06/13.67 % (582860)Termination phase: Saturation % 90.06/13.67 % (582860)Time elapsed: 0.363 s % 90.06/13.67 % (582860)Peak memory usage: 114 MB % 90.06/13.67 % (582860)Instructions burned: 542 (million) % 90.06/13.67 % (582861)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 90.06/13.67 % (582862)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 90.06/13.67 % (582861)------------------------------ % 90.06/13.67 % (582861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.06/13.67 % (582862)------------------------------ % 90.06/13.67 % (582862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.06/13.67 % (582862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.06/13.67 % (582861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.06/13.67 % (582861)CaDiCaL version: 2.1.3 % 90.06/13.67 % (582862)CaDiCaL version: 2.1.3 % 90.06/13.67 % (582861)Termination reason: Unknown % 90.06/13.67 % (582861)Termination phase: Saturation % 90.06/13.67 % (582862)Termination reason: Unknown % 90.06/13.67 % (582862)Termination phase: Saturation % 90.06/13.67 % (582861)Time elapsed: 0.361 s % 90.06/13.67 % (582862)Time elapsed: 0.361 s % 90.06/13.67 % (582861)Peak memory usage: 112 MB % 90.06/13.67 % (582862)Peak memory usage: 112 MB % 90.06/13.67 % (582861)Instructions burned: 542 (million) % 90.06/13.67 % (582862)Instructions burned: 541 (million) % 90.06/13.67 % (582868)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=1285232077:i=4840:nm=4:av=off_2895 on theBenchmark for (2895ds/4840Mi) % 90.06/13.67 % (582864)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 90.06/13.67 % (582864)------------------------------ % 90.06/13.67 % (582864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.06/13.67 % (582864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.06/13.67 % (582864)CaDiCaL version: 2.1.3 % 90.06/13.67 % (582864)Termination reason: Unknown % 90.06/13.67 % (582864)Termination phase: Saturation % 90.06/13.67 % (582864)Time elapsed: 0.361 s % 90.06/13.67 % (582864)Peak memory usage: 113 MB % 90.06/13.67 % (582864)Instructions burned: 541 (million) % 90.06/13.67 % (582869)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2167073516:cts=off:i=5002_2893 on theBenchmark for (2893ds/5002Mi) % 90.06/13.67 % (582870)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=3618052178:i=30479:sd=3:ss=axioms_2893 on theBenchmark for (2893ds/30479Mi) % 90.06/13.67 % (582872)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=2308804684:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2892 on theBenchmark for (2892ds/11035Mi) % 90.06/13.67 % (582872)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 90.06/13.67 % (582868)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 114.12/16.92 % (582868)------------------------------ % 114.12/16.92 % (582868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.12/16.92 % (582868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.12/16.92 % (582868)CaDiCaL version: 2.1.3 % 114.12/16.92 % (582868)Termination reason: Unknown % 114.12/16.92 % (582868)Termination phase: Saturation % 114.12/16.92 % (582868)Time elapsed: 0.361 s % 114.12/16.92 % (582868)Peak memory usage: 113 MB % 114.12/16.92 % (582868)Instructions burned: 542 (million) % 114.12/16.92 % (582869)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 114.12/16.92 % (582870)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 114.12/16.92 % (582869)------------------------------ % 114.12/16.92 % (582869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.12/16.92 % (582870)------------------------------ % 114.12/16.92 % (582870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.12/16.92 % (582869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.12/16.92 % (582870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.12/16.92 % (582870)CaDiCaL version: 2.1.3 % 114.12/16.92 % (582869)CaDiCaL version: 2.1.3 % 114.12/16.92 % (582869)Termination reason: Unknown % 114.12/16.92 % (582869)Termination phase: Saturation % 114.12/16.92 % (582870)Termination reason: Unknown % 114.12/16.92 % (582870)Termination phase: Saturation % 114.12/16.92 % (582869)Time elapsed: 0.359 s % 114.12/16.92 % (582870)Time elapsed: 0.359 s % 114.12/16.92 % (582869)Peak memory usage: 112 MB % 114.12/16.92 % (582870)Peak memory usage: 112 MB % 114.12/16.92 % (582870)Instructions burned: 540 (million) % 114.12/16.92 % (582869)Instructions burned: 541 (million) % 114.12/16.92 % (582876)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1475650940:i=5835_2889 on theBenchmark for (2889ds/5835Mi) % 114.12/16.92 % (582872)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 114.12/16.92 % (582872)------------------------------ % 114.12/16.92 % (582872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.12/16.92 % (582872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.12/16.92 % (582872)CaDiCaL version: 2.1.3 % 114.12/16.92 % (582872)Termination reason: Unknown % 114.12/16.92 % (582872)Termination phase: Saturation % 114.12/16.92 % (582872)Time elapsed: 0.360 s % 114.12/16.92 % (582872)Peak memory usage: 113 MB % 114.12/16.92 % (582872)Instructions burned: 543 (million) % 114.12/16.92 % (582877)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2293439532:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2888 on theBenchmark for (2888ds/5890Mi) % 114.12/16.92 % (582878)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2059676353:cts=off:i=19910:ep=RS_2888 on theBenchmark for (2888ds/19910Mi) % 114.12/16.92 % (582880)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=1065896712:i=20312:bd=preordered:fsr=off:er=filter_2887 on theBenchmark for (2887ds/20312Mi) % 114.12/16.92 % (582876)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 114.12/16.92 % (582876)------------------------------ % 114.12/16.92 % (582876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.12/16.92 % (582876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.12/16.92 % (582876)CaDiCaL version: 2.1.3 % 114.12/16.92 % (582876)Termination reason: Unknown % 114.12/16.92 % (582876)Termination phase: Saturation % 114.12/16.92 % (582876)Time elapsed: 0.363 s % 114.12/16.92 % (582876)Peak memory usage: 114 MB % 114.12/16.92 % (582876)Instructions burned: 542 (million) % 114.12/16.92 % (582877)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 114.12/16.92 % (582877)------------------------------ % 114.12/16.92 % (582877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.12/16.92 % (582877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.12/16.92 % (582877)CaDiCaL version: 2.1.3 % 114.12/16.92 % (582877)Termination reason: Unknown % 114.12/16.92 % (582877)Termination phase: Saturation % 114.12/16.92 % (582877)Time elapsed: 0.359 s % 114.12/16.92 % (582877)Peak memory usage: 114 MB % 114.12/16.92 % (582877)Instructions burned: 542 (million) % 114.12/16.92 % (582884)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=3064531270:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2884 on theBenchmark for (2884ds/13822Mi) % 140.76/20.71 % (582880)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 140.76/20.71 % (582880)------------------------------ % 140.76/20.71 % (582880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.76/20.71 % (582880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.76/20.71 % (582880)CaDiCaL version: 2.1.3 % 140.76/20.71 % (582880)Termination reason: Unknown % 140.76/20.71 % (582880)Termination phase: Saturation % 140.76/20.71 % (582880)Time elapsed: 0.362 s % 140.76/20.71 % (582880)Peak memory usage: 114 MB % 140.76/20.71 % (582880)Instructions burned: 542 (million) % 140.76/20.71 % (582885)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=110525931:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2883 on theBenchmark for (2883ds/7144Mi) % 140.76/20.71 % (582887)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=780055957:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2882 on theBenchmark for (2882ds/15184Mi) % 140.76/20.71 % (582884)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 140.76/20.71 % (582884)------------------------------ % 140.76/20.71 % (582884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.76/20.71 % (582884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.76/20.71 % (582884)CaDiCaL version: 2.1.3 % 140.76/20.71 % (582884)Termination reason: Unknown % 140.76/20.71 % (582884)Termination phase: Saturation % 140.76/20.71 % (582884)Time elapsed: 0.362 s % 140.76/20.71 % (582884)Peak memory usage: 114 MB % 140.76/20.71 % (582884)Instructions burned: 542 (million) % 140.76/20.71 % (582890)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=3768180288:i=107375_2879 on theBenchmark for (2879ds/107375Mi) % 140.76/20.71 % (582887)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 140.76/20.71 % (582887)------------------------------ % 140.76/20.71 % (582887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.76/20.71 % (582887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.76/20.71 % (582887)CaDiCaL version: 2.1.3 % 140.76/20.71 % (582887)Termination reason: Unknown % 140.76/20.71 % (582887)Termination phase: Saturation % 140.76/20.71 % (582887)Time elapsed: 0.359 s % 140.76/20.71 % (582887)Peak memory usage: 114 MB % 140.76/20.71 % (582887)Instructions burned: 542 (million) % 140.76/20.71 % (582892)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=2573353232:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2877 on theBenchmark for (2877ds/7958Mi) % 140.76/20.71 % (582890)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 140.76/20.71 % (582890)------------------------------ % 140.76/20.71 % (582890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.76/20.71 % (582890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.76/20.71 % (582890)CaDiCaL version: 2.1.3 % 140.76/20.71 % (582890)Termination reason: Unknown % 140.76/20.71 % (582890)Termination phase: Saturation % 140.76/20.71 % (582890)Time elapsed: 0.359 s % 140.76/20.71 % (582890)Peak memory usage: 114 MB % 140.76/20.71 % (582890)Instructions burned: 541 (million) % 140.76/20.71 % (582894)dis+10_128_sil=16000:nwc=0.7:random_seed=3131746599:i=15999:nm=2:gsp=on_2873 on theBenchmark for (2873ds/15999Mi) % 140.76/20.71 % (582894)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 140.76/20.71 % (582892)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 140.76/20.71 % (582892)------------------------------ % 140.76/20.71 % (582892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.76/20.71 % (582892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.76/20.71 % (582892)CaDiCaL version: 2.1.3 % 140.76/20.71 % (582892)Termination reason: Unknown % 140.76/20.71 % (582892)Termination phase: Saturation % 140.76/20.71 % (582892)Time elapsed: 0.361 s % 140.76/20.71 % (582892)Peak memory usage: 114 MB % 140.76/20.71 % (582892)Instructions burned: 541 (million) % 153.58/22.58 % (582896)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1919484871:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2871 on theBenchmark for (2871ds/8139Mi) % 153.58/22.58 % (582786)Instruction limit reached! % 153.58/22.58 % (582786)------------------------------ % 153.58/22.58 % (582786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.58 % (582786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.58 % (582786)CaDiCaL version: 2.1.3 % 153.58/22.58 % (582786)Termination reason: Instruction limit % 153.58/22.58 % (582786)Termination phase: Saturation % 153.58/22.58 % (582786)Time elapsed: 7.865 s % 153.58/22.58 % (582786)Peak memory usage: 470 MB % 153.58/22.58 % (582786)Instructions burned: 26474 (million) % 153.58/22.58 % (582899)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3805310658:st=4:i=8950:sd=5:ss=axioms_2868 on theBenchmark for (2868ds/8950Mi) % 153.58/22.58 % (582899)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 153.58/22.58 % (582899)------------------------------ % 153.58/22.58 % (582899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.58 % (582899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.58 % (582899)CaDiCaL version: 2.1.3 % 153.58/22.58 % (582899)Termination reason: Unknown % 153.58/22.58 % (582899)Termination phase: Saturation % 153.58/22.58 % (582899)Time elapsed: 0.196 s % 153.58/22.58 % (582899)Peak memory usage: 113 MB % 153.58/22.58 % (582899)Instructions burned: 541 (million) % 153.58/22.58 % (582955)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=2662800373:i=9809:ins=10:av=off_2864 on theBenchmark for (2864ds/9809Mi) % 153.58/22.58 % (582955)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 153.58/22.58 % (582955)------------------------------ % 153.58/22.58 % (582955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.58 % (582955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.58 % (582955)CaDiCaL version: 2.1.3 % 153.58/22.58 % (582955)Termination reason: Unknown % 153.58/22.58 % (582955)Termination phase: Saturation % 153.58/22.58 % (582955)Time elapsed: 0.195 s % 153.58/22.58 % (582955)Peak memory usage: 114 MB % 153.58/22.58 % (582955)Instructions burned: 541 (million) % 153.58/22.58 % (583018)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2692651926:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2861 on theBenchmark for (2861ds/9885Mi) % 153.58/22.58 % (583018)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 153.58/22.58 % (583018)------------------------------ % 153.58/22.58 % (583018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.58 % (583018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.58 % (583018)CaDiCaL version: 2.1.3 % 153.58/22.58 % (583018)Termination reason: Unknown % 153.58/22.58 % (583018)Termination phase: Saturation % 153.58/22.58 % (583018)Time elapsed: 0.195 s % 153.58/22.58 % (583018)Peak memory usage: 113 MB % 153.58/22.58 % (583018)Instructions burned: 542 (million) % 153.58/22.58 % (583054)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1927776493:cond=fast:i=32078:fgj=on:av=off_2858 on theBenchmark for (2858ds/32078Mi) % 153.58/22.58 % (583054)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 153.58/22.58 % (583054)------------------------------ % 153.58/22.58 % (583054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.58 % (583054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.58/22.58 % (583054)CaDiCaL version: 2.1.3 % 153.58/22.58 % (583054)Termination reason: Unknown % 153.58/22.58 % (583054)Termination phase: Saturation % 153.58/22.58 % (583054)Time elapsed: 0.208 s % 153.58/22.58 % (583054)Peak memory usage: 114 MB % 153.58/22.58 % (583054)Instructions burned: 541 (million) % 153.58/22.58 % (583123)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3319543999:i=11101:bd=all:ss=axioms:sgt=8_2855 on theBenchmark for (2855ds/11101Mi) % 153.58/22.58 % (582885)Instruction limit reached! % 153.58/22.58 % (582885)------------------------------ % 153.58/22.58 % (582885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.58/22.58 % (582885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.49/27.71 % (582885)CaDiCaL version: 2.1.3 % 190.49/27.71 % (582885)Termination reason: Instruction limit % 190.49/27.71 % (582885)Termination phase: Saturation % 190.49/27.71 % (582885)Time elapsed: 4.249 s % 190.49/27.71 % (582885)Peak memory usage: 114 MB % 190.49/27.71 % (582885)Instructions burned: 7145 (million) % 190.49/27.71 % (583194)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=4069207832:cond=on:i=13220:s2at=3:aac=none:fsd=on_2839 on theBenchmark for (2839ds/13220Mi) % 190.49/27.71 % (583194)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 190.49/27.71 % (583194)------------------------------ % 190.49/27.71 % (583194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.49/27.71 % (583194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.49/27.71 % (583194)CaDiCaL version: 2.1.3 % 190.49/27.71 % (583194)Termination reason: Unknown % 190.49/27.71 % (583194)Termination phase: Saturation % 190.49/27.71 % (583194)Time elapsed: 0.593 s % 190.49/27.71 % (583194)Peak memory usage: 114 MB % 190.49/27.71 % (583194)Instructions burned: 542 (million) % 190.49/27.71 % (583200)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=2240011392:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2830 on theBenchmark for (2830ds/13528Mi) % 190.49/27.71 % (583200)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 190.49/27.71 % (583200)------------------------------ % 190.49/27.71 % (583200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.49/27.71 % (583200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.49/27.71 % (583200)CaDiCaL version: 2.1.3 % 190.49/27.71 % (583200)Termination reason: Unknown % 190.49/27.71 % (583200)Termination phase: Saturation % 190.49/27.71 % (583200)Time elapsed: 0.604 s % 190.49/27.71 % (583200)Peak memory usage: 114 MB % 190.49/27.71 % (583200)Instructions burned: 543 (million) % 190.49/27.71 % (583202)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=573117204:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2821 on theBenchmark for (2821ds/14854Mi) % 190.49/27.71 % (583202)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 190.49/27.71 % (583202)------------------------------ % 190.49/27.71 % (583202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.49/27.71 % (583202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.49/27.71 % (583202)CaDiCaL version: 2.1.3 % 190.49/27.71 % (583202)Termination reason: Unknown % 190.49/27.71 % (583202)Termination phase: Saturation % 190.49/27.71 % (583202)Time elapsed: 0.615 s % 190.49/27.71 % (583202)Peak memory usage: 114 MB % 190.49/27.71 % (583202)Instructions burned: 552 (million) % 190.49/27.71 % (583204)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=474946520:i=14974:ss=axioms:sgt=16_2813 on theBenchmark for (2813ds/14974Mi) % 190.49/27.71 % (583204)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 190.49/27.71 % (583204)------------------------------ % 190.49/27.71 % (583204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.49/27.71 % (583204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.49/27.71 % (583204)CaDiCaL version: 2.1.3 % 190.49/27.71 % (583204)Termination reason: Unknown % 190.49/27.71 % (583204)Termination phase: Saturation % 190.49/27.71 % (583204)Time elapsed: 0.511 s % 190.49/27.71 % (583204)Peak memory usage: 113 MB % 190.49/27.71 % (583204)Instructions burned: 541 (million) % 190.49/27.71 % (583212)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=2987892729:i=33081:aac=none:fgj=on:bd=all:fsr=off_2805 on theBenchmark for (2805ds/33081Mi) % 190.49/27.71 % (582896)Instruction limit reached! % 190.49/27.71 % (582896)------------------------------ % 190.49/27.71 % (582896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.49/27.71 % (582896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.49/27.71 % (582896)CaDiCaL version: 2.1.3 % 190.49/27.71 % (582896)Termination reason: Instruction limit % 190.49/27.71 % (582896)Termination phase: Saturation % 190.49/27.71 % (582896)Time elapsed: 6.870 s % 219.79/31.82 % (582896)Peak memory usage: 132 MB % 219.79/31.82 % (582896)Instructions burned: 8139 (million) % 219.79/31.82 % (583212)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 219.79/31.82 % (583212)------------------------------ % 219.79/31.82 % (583212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.79/31.82 % (583212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.79/31.82 % (583212)CaDiCaL version: 2.1.3 % 219.79/31.82 % (583212)Termination reason: Unknown % 219.79/31.82 % (583212)Termination phase: Saturation % 219.79/31.82 % (583212)Time elapsed: 0.498 s % 219.79/31.82 % (583212)Peak memory usage: 114 MB % 219.79/31.82 % (583212)Instructions burned: 541 (million) % 219.79/31.82 % (583215)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=960946714:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2801 on theBenchmark for (2801ds/50856Mi) % 219.79/31.82 % (583225)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=4241406527:i=69865_2798 on theBenchmark for (2798ds/69865Mi) % 219.79/31.82 % (583123)Instruction limit reached! % 219.79/31.82 % (583123)------------------------------ % 219.79/31.82 % (583123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.79/31.82 % (583123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.79/31.82 % (583123)CaDiCaL version: 2.1.3 % 219.79/31.82 % (583123)Termination reason: Instruction limit % 219.79/31.82 % (583123)Termination phase: Saturation % 219.79/31.82 % (583123)Time elapsed: 6.044 s % 219.79/31.82 % (583123)Peak memory usage: 258 MB % 219.79/31.82 % (583123)Instructions burned: 11101 (million) % 219.79/31.82 % (583215)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 219.79/31.82 % (583215)------------------------------ % 219.79/31.82 % (583215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.79/31.82 % (583215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.79/31.82 % (583215)CaDiCaL version: 2.1.3 % 219.79/31.82 % (583215)Termination reason: Unknown % 219.79/31.82 % (583215)Termination phase: Saturation % 219.79/31.82 % (583215)Time elapsed: 0.601 s % 219.79/31.82 % (583215)Peak memory usage: 114 MB % 219.79/31.82 % (583215)Instructions burned: 542 (million) % 219.79/31.82 % (583228)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=95964770:cond=fast:i=17802:gtgl=3:gtg=all_2793 on theBenchmark for (2793ds/17802Mi) % 219.79/31.82 % (583229)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=4126196920:i=96644_2792 on theBenchmark for (2792ds/96644Mi) % 219.79/31.82 % (583225)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 219.79/31.82 % (583225)------------------------------ % 219.79/31.82 % (583225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.79/31.82 % (583225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.79/31.82 % (583225)CaDiCaL version: 2.1.3 % 219.79/31.82 % (583225)Termination reason: Unknown % 219.79/31.82 % (583225)Termination phase: Saturation % 219.79/31.82 % (583225)Time elapsed: 0.582 s % 219.79/31.82 % (583225)Peak memory usage: 113 MB % 219.79/31.82 % (583225)Instructions burned: 541 (million) % 219.79/31.82 % (583234)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 219.79/31.82 % (583234)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=3824727249:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2789 on theBenchmark for (2789ds/21161Mi) % 219.79/31.82 % (583228)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 219.79/31.82 % (583228)------------------------------ % 219.79/31.82 % (583228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.79/31.82 % (583228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.79/31.82 % (583228)CaDiCaL version: 2.1.3 % 219.79/31.82 % (583228)Termination reason: Unknown % 219.79/31.82 % (583228)Termination phase: Saturation % 219.79/31.82 % (583228)Time elapsed: 0.571 s % 219.79/31.82 % (583228)Peak memory usage: 113 MB % 219.79/31.82 % (583228)Instructions burned: 544 (million) % 219.79/31.82 % (583236)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=1597665902:i=22761:gtg=all:ss=axioms:fsd=on_2785 on theBenchmark for (2785ds/22761Mi) % 253.40/36.64 % (583236)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 253.40/36.64 % (583236)------------------------------ % 253.40/36.64 % (583236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.40/36.64 % (583236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.40/36.64 % (583236)CaDiCaL version: 2.1.3 % 253.40/36.64 % (583236)Termination reason: Unknown % 253.40/36.64 % (583236)Termination phase: Saturation % 253.40/36.64 % (583236)Time elapsed: 0.582 s % 253.40/36.64 % (583236)Peak memory usage: 114 MB % 253.40/36.64 % (583236)Instructions burned: 543 (million) % 253.40/36.64 % (583238)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2995626074:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2776 on theBenchmark for (2776ds/23713Mi) % 253.40/36.64 % (582878)Instruction limit reached! % 253.40/36.64 % (582878)------------------------------ % 253.40/36.64 % (582878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.40/36.64 % (582878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.40/36.64 % (582878)CaDiCaL version: 2.1.3 % 253.40/36.64 % (582878)Termination reason: Instruction limit % 253.40/36.64 % (582878)Termination phase: Saturation % 253.40/36.64 % (582878)Time elapsed: 11.504 s % 253.40/36.64 % (582878)Peak memory usage: 148 MB % 253.40/36.64 % (582878)Instructions burned: 19910 (million) % 253.40/36.64 % (583242)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=22850616:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2771 on theBenchmark for (2771ds/26509Mi) % 253.40/36.64 % (583242)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 253.40/36.64 % (583242)------------------------------ % 253.40/36.64 % (583242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.40/36.64 % (583242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.40/36.64 % (583242)CaDiCaL version: 2.1.3 % 253.40/36.64 % (583242)Termination reason: Unknown % 253.40/36.64 % (583242)Termination phase: Saturation % 253.40/36.64 % (583242)Time elapsed: 0.597 s % 253.40/36.64 % (583242)Peak memory usage: 113 MB % 253.40/36.64 % (583242)Instructions burned: 542 (million) % 253.40/36.64 % (583244)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=2327872538:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2763 on theBenchmark for (2763ds/28957Mi) % 253.40/36.64 % (582894)Instruction limit reached! % 253.40/36.64 % (582894)------------------------------ % 253.40/36.64 % (582894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.40/36.64 % (582894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.40/36.64 % (582894)CaDiCaL version: 2.1.3 % 253.40/36.64 % (582894)Termination reason: Instruction limit % 253.40/36.64 % (582894)Termination phase: Saturation % 253.40/36.64 % (582894)Time elapsed: 12.994 s % 253.40/36.64 % (582894)Peak memory usage: 168 MB % 253.40/36.64 % (582894)Instructions burned: 15999 (million) % 253.40/36.64 % (583248)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=2747513057:i=29246:s2at=-1:kws=inv_arity:ins=10_2742 on theBenchmark for (2742ds/29246Mi) % 253.40/36.64 % (583248)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 253.40/36.64 % (583248)------------------------------ % 253.40/36.64 % (583248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.40/36.64 % (583248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.40/36.64 % (583248)CaDiCaL version: 2.1.3 % 253.40/36.64 % (583248)Termination reason: Unknown % 253.40/36.64 % (583248)Termination phase: Saturation % 253.40/36.64 % (583248)Time elapsed: 0.563 s % 253.40/36.64 % (583248)Peak memory usage: 114 MB % 253.40/36.64 % (583248)Instructions burned: 542 (million) % 253.40/36.64 % (583250)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=998517099:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2734 on theBenchmark for (2734ds/30082Mi) % 253.40/36.64 % (583250)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 281.34/40.67 % (583250)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 281.34/40.67 % (583250)------------------------------ % 281.34/40.67 % (583250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.34/40.67 % (583250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.34/40.67 % (583250)CaDiCaL version: 2.1.3 % 281.34/40.67 % (583250)Termination reason: Unknown % 281.34/40.67 % (583250)Termination phase: Saturation % 281.34/40.67 % (583250)Time elapsed: 0.582 s % 281.34/40.67 % (583250)Peak memory usage: 114 MB % 281.34/40.67 % (583250)Instructions burned: 546 (million) % 281.34/40.67 % (583252)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=2734766524:i=32262:bd=preordered_2725 on theBenchmark for (2725ds/32262Mi) % 281.34/40.67 % (583252)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 281.34/40.67 % (583252)------------------------------ % 281.34/40.67 % (583252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.34/40.67 % (583252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.34/40.67 % (583252)CaDiCaL version: 2.1.3 % 281.34/40.67 % (583252)Termination reason: Unknown % 281.34/40.67 % (583252)Termination phase: Saturation % 281.34/40.67 % (583252)Time elapsed: 0.576 s % 281.34/40.67 % (583252)Peak memory usage: 113 MB % 281.34/40.67 % (583252)Instructions burned: 541 (million) % 281.34/40.67 % (583254)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=4204920621:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2716 on theBenchmark for (2716ds/32870Mi) % 281.34/40.67 % (583254)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 281.34/40.67 % (583254)------------------------------ % 281.34/40.67 % (583254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.34/40.67 % (583254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.34/40.67 % (583254)CaDiCaL version: 2.1.3 % 281.34/40.67 % (583254)Termination reason: Unknown % 281.34/40.67 % (583254)Termination phase: Saturation % 281.34/40.67 % (583254)Time elapsed: 0.580 s % 281.34/40.67 % (583254)Peak memory usage: 113 MB % 281.34/40.67 % (583254)Instructions burned: 542 (million) % 281.34/40.67 % (583257)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=1066724477:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2708 on theBenchmark for (2708ds/33295Mi) % 281.34/40.67 % (583257)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 281.34/40.67 % (583257)------------------------------ % 281.34/40.67 % (583257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.34/40.67 % (583257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.34/40.67 % (583257)CaDiCaL version: 2.1.3 % 281.34/40.67 % (583257)Termination reason: Unknown % 281.34/40.67 % (583257)Termination phase: Saturation % 281.34/40.67 % (583257)Time elapsed: 0.520 s % 281.34/40.67 % (583257)Peak memory usage: 114 MB % 281.34/40.67 % (583257)Instructions burned: 542 (million) % 281.34/40.67 % (582761)Instruction limit reached! % 281.34/40.67 % (582761)------------------------------ % 281.34/40.67 % (582761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.34/40.67 % (582761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.34/40.67 % (582761)CaDiCaL version: 2.1.3 % 281.34/40.67 % (582761)Termination reason: Instruction limit % 281.34/40.67 % (582761)Termination phase: Saturation % 281.34/40.67 % (582761)Time elapsed: 26.343 s % 281.34/40.67 % (582761)Peak memory usage: 199 MB % 281.34/40.67 % (582761)Instructions burned: 33335 (million) % 281.34/40.67 % (583262)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=688242618:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2700 on theBenchmark for (2700ds/36826Mi) % 281.34/40.67 % (583263)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=614288911:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2699 on theBenchmark for (2699ds/92981Mi) % 281.34/40.67 % (583263)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 281.34/40.67 % (583263)------------------------------ % 281.34/40.67 % (583263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.43/42.86 % (583263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.86 % (583263)CaDiCaL version: 2.1.3 % 296.43/42.86 % (583263)Termination reason: Unknown % 296.43/42.86 % (583263)Termination phase: Saturation % 296.43/42.86 % (583263)Time elapsed: 0.593 s % 296.43/42.86 % (583263)Peak memory usage: 113 MB % 296.43/42.86 % (583263)Instructions burned: 541 (million) % 296.43/42.86 % (583268)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=2219599737:s2pl=on:i=49423_2690 on theBenchmark for (2690ds/49423Mi) % 296.43/42.86 % (583268)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 296.43/42.86 % (583268)------------------------------ % 296.43/42.86 % (583268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.43/42.86 % (583268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.86 % (583268)CaDiCaL version: 2.1.3 % 296.43/42.86 % (583268)Termination reason: Unknown % 296.43/42.86 % (583268)Termination phase: Saturation % 296.43/42.86 % (583268)Time elapsed: 0.622 s % 296.43/42.86 % (583268)Peak memory usage: 114 MB % 296.43/42.86 % (583268)Instructions burned: 542 (million) % 296.43/42.86 % (583270)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=263268089:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2681 on theBenchmark for (2681ds/57299Mi) % 296.43/42.86 % (583270)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 296.43/42.86 % (583270)------------------------------ % 296.43/42.86 % (583270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.43/42.86 % (583270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.86 % (583270)CaDiCaL version: 2.1.3 % 296.43/42.86 % (583270)Termination reason: Unknown % 296.43/42.86 % (583270)Termination phase: Saturation % 296.43/42.86 % (583270)Time elapsed: 1.079 s % 296.43/42.86 % (583270)Peak memory usage: 113 MB % 296.43/42.86 % (583270)Instructions burned: 542 (million) % 296.43/42.86 % (583272)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=3956752560:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2667 on theBenchmark for (2667ds/127679Mi) % 296.43/42.86 % (583272)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 296.43/42.86 % (583272)------------------------------ % 296.43/42.86 % (583272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.43/42.86 % (583272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.86 % (583272)CaDiCaL version: 2.1.3 % 296.43/42.86 % (583272)Termination reason: Unknown % 296.43/42.86 % (583272)Termination phase: Saturation % 296.43/42.86 % (583272)Time elapsed: 0.597 s % 296.43/42.86 % (583272)Peak memory usage: 114 MB % 296.43/42.86 % (583272)Instructions burned: 542 (million) % 296.43/42.86 % (583274)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=2726743336:i=69402:add=on:aac=none:fsr=off_2659 on theBenchmark for (2659ds/69402Mi) % 296.43/42.86 % (583274)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 296.43/42.86 % (583274)------------------------------ % 296.43/42.86 % (583274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.43/42.86 % (583274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 296.43/42.86 % (583274)CaDiCaL version: 2.1.3 % 296.43/42.86 % (583274)Termination reason: Unknown % 296.43/42.86 % (583274)Termination phase: Saturation % 296.43/42.86 % (583274)Time elapsed: 0.595 s % 296.43/42.86 % (583274)Peak memory usage: 113 MB % 296.43/42.86 % (583274)Instructions burned: 541 (million) % 296.43/42.86 % (583276)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=1525398752:i=100512:doe=on:fgj=on:bd=all:fsd=on_2650 on theBenchmark for (2650ds/100512Mi) % 296.43/42.86 % (583276)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 296.43/42.86 % (583276)------------------------------ % 296.43/42.86 % (583276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 296.43/42.86 % (583276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/43.23 % (583276)CaDiCaL version: 2.1.3 % 300.17/43.23 % (583276)Termination reason: Unknown % 300.17/43.23 % (583276)Termination phase: Saturation % 300.17/43.23 % (583276)Time elapsed: 0.594 s % 300.17/43.23 % (583276)Peak memory usage: 113 MB % 300.17/43.23 % (583276)Instructions burned: 542 (million) % 300.17/43.23 % (583278)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=3903624159:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2642 on theBenchmark for (2642ds/138761Mi) % 300.17/43.23 % (583278)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.17/43.23 % (583278)------------------------------ % 300.17/43.23 % (583278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/43.23 % (583278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/43.23 % (583278)CaDiCaL version: 2.1.3 % 300.17/43.23 % (583278)Termination reason: Unknown % 300.17/43.23 % (583278)Termination phase: Saturation % 300.17/43.23 % (583278)Time elapsed: 0.604 s % 300.17/43.23 % (583278)Peak memory usage: 114 MB % 300.17/43.23 % (583278)Instructions burned: 542 (million) % 300.17/43.23 % (583282)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=1564639095:i=282386:rtra=on_2633 on theBenchmark for (2633ds/282386Mi) % 300.17/43.23 % (583282)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.17/43.23 % (583282)------------------------------ % 300.17/43.23 % (583282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/43.23 % (583282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/43.23 % (583282)CaDiCaL version: 2.1.3 % 300.17/43.23 % (583282)Termination reason: Unknown % 300.17/43.23 % (583282)Termination phase: Saturation % 300.17/43.23 % (583282)Time elapsed: 0.598 s % 300.17/43.23 % (583282)Peak memory usage: 114 MB % 300.17/43.23 % (583282)Instructions burned: 542 (million) % 300.17/43.23 % (583284)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=164839400:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2624 on theBenchmark for (2624ds/269354Mi) % 300.17/43.23 % (583284)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.17/43.23 % (583284)------------------------------ % 300.17/43.23 % (583284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/43.23 % (583284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/43.23 % (583284)CaDiCaL version: 2.1.3 % 300.17/43.23 % (583284)Termination reason: Unknown % 300.17/43.23 % (583284)Termination phase: Saturation % 300.17/43.23 % (583284)Time elapsed: 0.601 s % 300.17/43.23 % (583284)Peak memory usage: 114 MB % 300.17/43.23 % (583284)Instructions burned: 546 (million) % 300.17/43.23 % (583286)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=3057085249:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2615 on theBenchmark for (2615ds/283390Mi) % 300.17/43.23 % (583286)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.17/43.23 % (583286)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.17/43.23 % (583286)------------------------------ % 300.17/43.23 % (583286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/43.23 % (583286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.17/43.23 % (583286)CaDiCaL version: 2.1.3 % 300.17/43.23 % (583286)Termination reason: Unknown % 300.17/43.23 % (583286)Termination phase: Saturation % 300.17/43.23 % (583286)Time elapsed: 0.599 s % 300.17/43.23 % (583286)Peak memory usage: 114 MB % 300.17/43.23 % (583286)Instructions burned: 543 (million) % 300.17/43.23 % (583288)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=1860943430:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2606 on theBenchmark for (2606ds/218Mi) % 300.17/43.23 % (583288)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.17/43.23 % (583288)Instruction limit reached! % 300.17/43.23 % (583288)------------------------------ % 300.17/43.23 % (583288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.17/43.23 % (583288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 % 300.17/43.24 Terminated %------------------------------------------------------------------------------