%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM979_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n003.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:44 PM UTC 2026 % Result : Timeout 300.12s 43.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM979_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.40 % Computer : n003.cluster.edu % 0.11/0.40 % Model : x86_64 x86_64 % 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.40 % Memory : 8046.5625MB % 0.11/0.40 % OS : Linux 6.8.0-71-generic % 0.11/0.40 % CPULimit : 300 % 0.11/0.40 % WCLimit : 300 % 0.11/0.40 % DateTime : Sun Sep 27 21:50:56 UTC 2026 % 0.11/0.40 % CPUTime : % 0.11/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.11/0.43 Running first-order theorem proving % 0.11/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 5.79/1.98 % (947184)Detected formulas, will run a generic FOF schedule. % 5.79/1.98 % (947290)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=3737610784:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.79/1.98 % (947294)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2921866537:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.79/1.98 % (947295)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1678136690:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.79/1.98 % (947296)dis-21_1_sil=8000:lcm=predicate:random_seed=2407268834: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.79/1.98 % (947292)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=4247359158:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.79/1.98 % (947291)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=3851760058:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.79/1.98 % (947292)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.79/1.98 % (947293)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1881952002:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.79/1.98 % (947293)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.79/1.98 % (947293)Instruction limit reached! % 5.79/1.98 % (947293)------------------------------ % 5.79/1.98 % (947293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.79/1.98 % (947293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.98 % (947293)CaDiCaL version: 2.1.3 % 5.79/1.98 % (947293)Termination reason: Instruction limit % 5.79/1.98 % (947293)Termination phase: Saturation % 5.79/1.98 % (947293)Time elapsed: 0.031 s % 5.79/1.98 % (947293)Peak memory usage: 89 MB % 5.79/1.98 % (947293)Instructions burned: 112 (million) % 5.79/1.98 % (947294)Instruction limit reached! % 5.79/1.98 % (947294)------------------------------ % 5.79/1.98 % (947294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.79/1.98 % (947294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.98 % (947294)CaDiCaL version: 2.1.3 % 5.79/1.98 % (947294)Termination reason: Instruction limit % 5.79/1.98 % (947294)Termination phase: Saturation % 5.79/1.98 % (947294)Time elapsed: 0.067 s % 5.79/1.98 % (947294)Peak memory usage: 88 MB % 5.79/1.98 % (947294)Instructions burned: 119 (million) % 5.79/1.98 % (947296)Instruction limit reached! % 5.79/1.98 % (947296)------------------------------ % 5.79/1.98 % (947296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.79/1.98 % (947296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.98 % (947296)CaDiCaL version: 2.1.3 % 5.79/1.98 % (947296)Termination reason: Instruction limit % 5.79/1.98 % (947296)Termination phase: Saturation % 5.79/1.98 % (947296)Time elapsed: 0.075 s % 5.79/1.98 % (947296)Peak memory usage: 90 MB % 5.79/1.98 % (947296)Instructions burned: 131 (million) % 5.79/1.98 % (947295)Instruction limit reached! % 5.79/1.98 % (947295)------------------------------ % 5.79/1.98 % (947295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.79/1.98 % (947295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.98 % (947295)CaDiCaL version: 2.1.3 % 5.79/1.98 % (947295)Termination reason: Instruction limit % 5.79/1.98 % (947295)Termination phase: Saturation % 5.79/1.98 % (947295)Time elapsed: 0.087 s % 5.79/1.98 % (947295)Peak memory usage: 89 MB % 5.79/1.98 % (947295)Instructions burned: 140 (million) % 5.79/1.98 % (947312)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3521571179:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 5.79/1.98 % (947312)Refutation not found, incomplete strategy % 5.79/1.98 % (947312)------------------------------ % 5.79/1.98 % (947312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.79/1.98 % (947312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.79/1.98 % (947312)CaDiCaL version: 2.1.3 % 5.79/1.98 % (947312)Termination reason: Refutation not found, incomplete strategy % 9.52/2.31 % (947312)Time elapsed: 0.001 s % 9.52/2.31 % (947312)Peak memory usage: 89 MB % 9.52/2.31 % (947312)Instructions burned: 2 (million) % 9.52/2.31 % (947308)lrs+10_1_sil=8000:sp=occurrence:random_seed=448773753:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 9.52/2.31 % (947315)lrs+1011_1_sil=32000:sp=occurrence:random_seed=465182111:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 9.52/2.31 % (947320)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=759771644:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 9.52/2.31 % (947290)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 9.52/2.31 % (947290)------------------------------ % 9.52/2.31 % (947290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.52/2.31 % (947290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.52/2.31 % (947290)CaDiCaL version: 2.1.3 % 9.52/2.31 % (947290)Termination reason: Unknown % 9.52/2.31 % (947290)Termination phase: Saturation % 9.52/2.31 % (947290)Time elapsed: 0.360 s % 9.52/2.31 % (947290)Peak memory usage: 114 MB % 9.52/2.31 % (947290)Instructions burned: 541 (million) % 9.52/2.31 % (947292)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 9.52/2.31 % (947292)------------------------------ % 9.52/2.31 % (947292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.52/2.31 % (947292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.52/2.31 % (947292)CaDiCaL version: 2.1.3 % 9.52/2.31 % (947292)Termination reason: Unknown % 9.52/2.31 % (947292)Termination phase: Saturation % 9.52/2.31 % (947292)Time elapsed: 0.357 s % 9.52/2.31 % (947292)Peak memory usage: 113 MB % 9.52/2.31 % (947292)Instructions burned: 541 (million) % 9.52/2.31 % (947312)------------------------------ % 9.52/2.31 % (947312)------------------------------ % 9.52/2.31 % (947291)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 9.52/2.31 % (947291)------------------------------ % 9.52/2.31 % (947291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.52/2.31 % (947291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.52/2.31 % (947291)CaDiCaL version: 2.1.3 % 9.52/2.31 % (947291)Termination reason: Unknown % 9.52/2.31 % (947291)Termination phase: Saturation % 9.52/2.31 % (947291)Time elapsed: 0.371 s % 9.52/2.31 % (947291)Peak memory usage: 113 MB % 9.52/2.31 % (947291)Instructions burned: 544 (million) % 9.52/2.31 % (947320)Instruction limit reached! % 9.52/2.31 % (947320)------------------------------ % 9.52/2.31 % (947320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.52/2.31 % (947320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.52/2.31 % (947320)CaDiCaL version: 2.1.3 % 9.52/2.31 % (947320)Termination reason: Instruction limit % 9.52/2.31 % (947320)Termination phase: Saturation % 9.52/2.31 % (947320)Time elapsed: 0.142 s % 9.52/2.31 % (947320)Peak memory usage: 91 MB % 9.52/2.31 % (947320)Instructions burned: 250 (million) % 9.52/2.31 % (947308)Instruction limit reached! % 9.52/2.31 % (947308)------------------------------ % 9.52/2.31 % (947308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.52/2.31 % (947308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.52/2.31 % (947308)CaDiCaL version: 2.1.3 % 9.52/2.31 % (947308)Termination reason: Instruction limit % 9.52/2.31 % (947308)Termination phase: Saturation % 9.52/2.31 % (947308)Time elapsed: 0.180 s % 9.52/2.31 % (947308)Peak memory usage: 90 MB % 9.52/2.31 % (947308)Instructions burned: 285 (million) % 9.52/2.31 % (947315)Instruction limit reached! % 9.52/2.31 % (947315)------------------------------ % 9.52/2.31 % (947315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.52/2.31 % (947315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.52/2.31 % (947315)CaDiCaL version: 2.1.3 % 9.52/2.31 % (947315)Termination reason: Instruction limit % 9.52/2.31 % (947315)Termination phase: Saturation % 9.52/2.31 % (947315)Time elapsed: 0.181 s % 9.52/2.31 % (947315)Peak memory usage: 92 MB % 9.52/2.31 % (947315)Instructions burned: 325 (million) % 9.52/2.31 % (947327)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=888739156:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 9.52/2.31 % (947325)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=81389583:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi) % 11.55/2.64 % (947326)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=441040585:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 11.55/2.64 % (947327)Instruction limit reached! % 11.55/2.64 % (947327)------------------------------ % 11.55/2.64 % (947327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.55/2.64 % (947327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.55/2.64 % (947327)CaDiCaL version: 2.1.3 % 11.55/2.64 % (947327)Termination reason: Instruction limit % 11.55/2.64 % (947327)Termination phase: Saturation % 11.55/2.64 % (947327)Time elapsed: 0.035 s % 11.55/2.64 % (947327)Peak memory usage: 89 MB % 11.55/2.64 % (947327)Instructions burned: 114 (million) % 11.55/2.64 % (947328)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1365743606:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 11.55/2.64 % (947328)Refutation not found, incomplete strategy % 11.55/2.64 % (947328)------------------------------ % 11.55/2.64 % (947328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.55/2.64 % (947328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.55/2.64 % (947328)CaDiCaL version: 2.1.3 % 11.55/2.64 % (947328)Termination reason: Refutation not found, incomplete strategy % 11.55/2.64 % (947328)Time elapsed: 0.005 s % 11.55/2.64 % (947328)Peak memory usage: 88 MB % 11.55/2.64 % (947328)Instructions burned: 7 (million) % 11.55/2.64 % (947329)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2928686076:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 11.55/2.64 % (947330)lrs+10_1_sil=8000:sp=occurrence:random_seed=2830756002:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 11.55/2.64 % (947331)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3283599421:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 11.55/2.64 % (947329)Instruction limit reached! % 11.55/2.64 % (947329)------------------------------ % 11.55/2.64 % (947329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.55/2.64 % (947329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.55/2.64 % (947329)CaDiCaL version: 2.1.3 % 11.55/2.64 % (947329)Termination reason: Instruction limit % 11.55/2.64 % (947329)Termination phase: Saturation % 11.55/2.64 % (947329)Time elapsed: 0.055 s % 11.55/2.64 % (947329)Peak memory usage: 89 MB % 11.55/2.64 % (947329)Instructions burned: 115 (million) % 11.55/2.64 % (947325)Instruction limit reached! % 11.55/2.64 % (947325)------------------------------ % 11.55/2.64 % (947325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.55/2.64 % (947325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.55/2.64 % (947325)CaDiCaL version: 2.1.3 % 11.55/2.64 % (947325)Termination reason: Instruction limit % 11.55/2.64 % (947325)Termination phase: Saturation % 11.55/2.64 % (947325)Time elapsed: 0.148 s % 11.55/2.64 % (947325)Peak memory usage: 90 MB % 11.55/2.64 % (947325)Instructions burned: 295 (million) % 11.55/2.64 % (947335)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3982042340:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 11.55/2.64 % (947331)Instruction limit reached! % 11.55/2.64 % (947331)------------------------------ % 11.55/2.64 % (947331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.55/2.64 % (947331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.55/2.64 % (947331)CaDiCaL version: 2.1.3 % 11.55/2.64 % (947331)Termination reason: Instruction limit % 11.55/2.64 % (947331)Termination phase: Saturation % 11.55/2.64 % (947331)Time elapsed: 0.262 s % 11.55/2.64 % (947331)Peak memory usage: 91 MB % 11.55/2.64 % (947331)Instructions burned: 438 (million) % 11.55/2.64 % (947328)------------------------------ % 11.55/2.64 % (947328)------------------------------ % 11.55/2.64 % (947340)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3833818672:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 11.55/2.64 % (947349)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3493977860:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi) % 11.55/2.64 % (947335)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 13.50/2.95 % (947335)------------------------------ % 13.50/2.95 % (947335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.50/2.95 % (947335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.50/2.95 % (947335)CaDiCaL version: 2.1.3 % 13.50/2.95 % (947335)Termination reason: Unknown % 13.50/2.95 % (947335)Termination phase: Saturation % 13.50/2.95 % (947335)Time elapsed: 0.311 s % 13.50/2.95 % (947335)Peak memory usage: 113 MB % 13.50/2.95 % (947335)Instructions burned: 542 (million) % 13.50/2.95 % (947340)Instruction limit reached! % 13.50/2.95 % (947340)------------------------------ % 13.50/2.95 % (947340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.50/2.95 % (947340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.50/2.95 % (947340)CaDiCaL version: 2.1.3 % 13.50/2.95 % (947340)Termination reason: Instruction limit % 13.50/2.95 % (947340)Termination phase: Saturation % 13.50/2.95 % (947340)Time elapsed: 0.134 s % 13.50/2.95 % (947340)Peak memory usage: 90 MB % 13.50/2.95 % (947340)Instructions burned: 134 (million) % 13.50/2.95 % (947326)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 13.50/2.95 % (947326)------------------------------ % 13.50/2.95 % (947326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.50/2.95 % (947326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.50/2.95 % (947326)CaDiCaL version: 2.1.3 % 13.50/2.95 % (947326)Termination reason: Unknown % 13.50/2.95 % (947326)Termination phase: Saturation % 13.50/2.95 % (947326)Time elapsed: 0.509 s % 13.50/2.95 % (947326)Peak memory usage: 113 MB % 13.50/2.95 % (947326)Instructions burned: 541 (million) % 13.50/2.95 % (947357)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3207957191:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi) % 13.50/2.95 % (947359)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=3830568837:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/125Mi) % 13.50/2.95 % (947359)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.50/2.95 % (947363)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4044421798:i=134:gtgl=5:slsql=off:gtg=exists_sym_2988 on theBenchmark for (2988ds/134Mi) % 13.50/2.95 % (947330)Instruction limit reached! % 13.50/2.95 % (947330)------------------------------ % 13.50/2.95 % (947330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.50/2.95 % (947330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.50/2.95 % (947330)CaDiCaL version: 2.1.3 % 13.50/2.95 % (947330)Termination reason: Instruction limit % 13.50/2.95 % (947330)Termination phase: Saturation % 13.50/2.95 % (947330)Time elapsed: 0.700 s % 13.50/2.95 % (947330)Peak memory usage: 95 MB % 13.50/2.95 % (947330)Instructions burned: 907 (million) % 13.50/2.95 % (947363)Instruction limit reached! % 13.50/2.95 % (947363)------------------------------ % 13.50/2.95 % (947363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.50/2.95 % (947363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.50/2.95 % (947363)CaDiCaL version: 2.1.3 % 13.50/2.95 % (947363)Termination reason: Instruction limit % 13.50/2.95 % (947363)Termination phase: Saturation % 13.50/2.95 % (947363)Time elapsed: 0.073 s % 13.50/2.95 % (947363)Peak memory usage: 90 MB % 13.50/2.95 % (947363)Instructions burned: 134 (million) % 13.50/2.95 % (947359)Instruction limit reached! % 13.50/2.95 % (947359)------------------------------ % 13.50/2.95 % (947359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.50/2.95 % (947359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.50/2.95 % (947359)CaDiCaL version: 2.1.3 % 13.50/2.95 % (947359)Termination reason: Instruction limit % 13.50/2.95 % (947359)Termination phase: Saturation % 13.50/2.95 % (947359)Time elapsed: 0.121 s % 13.50/2.95 % (947359)Peak memory usage: 90 MB % 13.50/2.95 % (947359)Instructions burned: 125 (million) % 13.50/2.95 % (947367)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2749936067:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/431Mi) % 13.50/2.95 % (947367)Refutation not found, incomplete strategy % 13.50/2.95 % (947367)------------------------------ % 13.50/2.95 % (947367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.46 % (947367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.46 % (947367)CaDiCaL version: 2.1.3 % 17.01/3.46 % (947367)Termination reason: Refutation not found, incomplete strategy % 17.01/3.46 % (947367)Time elapsed: 0.009 s % 17.01/3.46 % (947367)Peak memory usage: 88 MB % 17.01/3.46 % (947367)Instructions burned: 8 (million) % 17.01/3.46 % (947366)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=167302076:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/141Mi) % 17.01/3.46 % (947366)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.01/3.46 % (947366)Refutation not found, incomplete strategy % 17.01/3.46 % (947366)------------------------------ % 17.01/3.46 % (947366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.46 % (947366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.46 % (947366)CaDiCaL version: 2.1.3 % 17.01/3.46 % (947366)Termination reason: Refutation not found, incomplete strategy % 17.01/3.46 % (947366)Time elapsed: 0.004 s % 17.01/3.46 % (947366)Peak memory usage: 88 MB % 17.01/3.46 % (947366)Instructions burned: 2 (million) % 17.01/3.46 % (947349)Instruction limit reached! % 17.01/3.46 % (947349)------------------------------ % 17.01/3.46 % (947349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.46 % (947349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.46 % (947349)CaDiCaL version: 2.1.3 % 17.01/3.46 % (947349)Termination reason: Instruction limit % 17.01/3.46 % (947349)Termination phase: Saturation % 17.01/3.46 % (947349)Time elapsed: 0.437 s % 17.01/3.46 % (947349)Peak memory usage: 90 MB % 17.01/3.46 % (947349)Instructions burned: 593 (million) % 17.01/3.46 % (947377)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=2271634011:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2986 on theBenchmark for (2986ds/150Mi) % 17.01/3.46 % (947377)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.01/3.46 % (947376)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=989280861:i=6060:aac=none:ins=25_2986 on theBenchmark for (2986ds/6060Mi) % 17.01/3.46 % (947379)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=636218542:i=14155:bd=all_2985 on theBenchmark for (2985ds/14155Mi) % 17.01/3.46 % (947377)Instruction limit reached! % 17.01/3.46 % (947377)------------------------------ % 17.01/3.46 % (947377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.46 % (947377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.46 % (947377)CaDiCaL version: 2.1.3 % 17.01/3.46 % (947377)Termination reason: Instruction limit % 17.01/3.46 % (947377)Termination phase: Saturation % 17.01/3.46 % (947377)Time elapsed: 0.049 s % 17.01/3.46 % (947377)Peak memory usage: 90 MB % 17.01/3.46 % (947377)Instructions burned: 153 (million) % 17.01/3.46 % (947357)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 17.01/3.46 % (947357)------------------------------ % 17.01/3.46 % (947357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.01/3.46 % (947357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.01/3.46 % (947357)CaDiCaL version: 2.1.3 % 17.01/3.46 % (947357)Termination reason: Unknown % 17.01/3.46 % (947357)Termination phase: Saturation % 17.01/3.46 % (947357)Time elapsed: 0.451 s % 17.01/3.46 % (947357)Peak memory usage: 113 MB % 17.01/3.46 % (947357)Instructions burned: 541 (million) % 17.01/3.46 % (947382)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2335165601:i=667:av=off:fsr=off_2984 on theBenchmark for (2984ds/667Mi) % 17.01/3.46 % (947367)------------------------------ % 17.01/3.46 % (947367)------------------------------ % 17.01/3.46 % (947366)------------------------------ % 17.01/3.46 % (947366)------------------------------ % 17.01/3.46 % (947386)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=95599363:s2a=on:i=185:s2at=1.8:fdi=4_2984 on theBenchmark for (2984ds/185Mi) % 17.01/3.46 % (947386)Instruction limit reached! % 22.63/4.04 % (947386)------------------------------ % 22.63/4.04 % (947386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.63/4.04 % (947386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.63/4.04 % (947386)CaDiCaL version: 2.1.3 % 22.63/4.04 % (947386)Termination reason: Instruction limit % 22.63/4.04 % (947386)Termination phase: Saturation % 22.63/4.04 % (947386)Time elapsed: 0.055 s % 22.63/4.04 % (947386)Peak memory usage: 90 MB % 22.63/4.04 % (947386)Instructions burned: 185 (million) % 22.63/4.04 % (947387)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4105395260:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2983 on theBenchmark for (2983ds/193Mi) % 22.63/4.04 % (947389)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1100897625:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2983 on theBenchmark for (2983ds/4850Mi) % 22.63/4.04 % (947389)Refutation not found, incomplete strategy % 22.63/4.04 % (947389)------------------------------ % 22.63/4.04 % (947389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.63/4.04 % (947389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.63/4.04 % (947389)CaDiCaL version: 2.1.3 % 22.63/4.04 % (947389)Termination reason: Refutation not found, incomplete strategy % 22.63/4.04 % (947389)Time elapsed: 0.005 s % 22.63/4.04 % (947389)Peak memory usage: 88 MB % 22.63/4.04 % (947389)Instructions burned: 7 (million) % 22.63/4.04 % (947391)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1852122013:i=12111:sd=1:ss=included_2983 on theBenchmark for (2983ds/12111Mi) % 22.63/4.04 % (947379)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 22.63/4.04 % (947379)------------------------------ % 22.63/4.04 % (947379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.63/4.04 % (947379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.63/4.04 % (947379)CaDiCaL version: 2.1.3 % 22.63/4.04 % (947379)Termination reason: Unknown % 22.63/4.04 % (947379)Termination phase: Saturation % 22.63/4.04 % (947379)Time elapsed: 0.307 s % 22.63/4.04 % (947379)Peak memory usage: 113 MB % 22.63/4.04 % (947379)Instructions burned: 541 (million) % 22.63/4.04 % (947393)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1017351770:i=319:kws=precedence:fsr=off_2982 on theBenchmark for (2982ds/319Mi) % 22.63/4.04 % (947387)Instruction limit reached! % 22.63/4.04 % (947387)------------------------------ % 22.63/4.04 % (947387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.63/4.04 % (947387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.63/4.04 % (947387)CaDiCaL version: 2.1.3 % 22.63/4.04 % (947387)Termination reason: Instruction limit % 22.63/4.04 % (947387)Termination phase: Saturation % 22.63/4.04 % (947387)Time elapsed: 0.112 s % 22.63/4.04 % (947387)Peak memory usage: 91 MB % 22.63/4.04 % (947387)Instructions burned: 196 (million) % 22.63/4.04 % (947376)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 22.63/4.04 % (947376)------------------------------ % 22.63/4.04 % (947376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.63/4.04 % (947376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.63/4.04 % (947376)CaDiCaL version: 2.1.3 % 22.63/4.04 % (947376)Termination reason: Unknown % 22.63/4.04 % (947376)Termination phase: Saturation % 22.63/4.04 % (947376)Time elapsed: 0.362 s % 22.63/4.04 % (947376)Peak memory usage: 114 MB % 22.63/4.04 % (947376)Instructions burned: 540 (million) % 22.63/4.04 % (947382)Instruction limit reached! % 22.63/4.04 % (947382)------------------------------ % 22.63/4.04 % (947382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.63/4.04 % (947382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.63/4.04 % (947382)CaDiCaL version: 2.1.3 % 22.63/4.04 % (947382)Termination reason: Instruction limit % 22.63/4.04 % (947382)Termination phase: Saturation % 22.63/4.04 % (947382)Time elapsed: 0.325 s % 22.63/4.04 % (947382)Peak memory usage: 89 MB % 22.63/4.04 % (947382)Instructions burned: 668 (million) % 22.63/4.04 % (947399)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4069472056:i=2064:ep=RST_2981 on theBenchmark for (2981ds/2064Mi) % 22.63/4.04 % (947412)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3113406578:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2980 on theBenchmark for (2980ds/757Mi) % 25.76/4.68 % (947409)dis-1011_128_sil=32000:random_seed=3474545264:i=3706:ep=RST:av=off_2980 on theBenchmark for (2980ds/3706Mi) % 25.76/4.68 % (947389)------------------------------ % 25.76/4.68 % (947389)------------------------------ % 25.76/4.68 % (947393)Instruction limit reached! % 25.76/4.68 % (947393)------------------------------ % 25.76/4.68 % (947393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.76/4.68 % (947393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.76/4.68 % (947393)CaDiCaL version: 2.1.3 % 25.76/4.68 % (947393)Termination reason: Instruction limit % 25.76/4.68 % (947393)Termination phase: Saturation % 25.76/4.68 % (947393)Time elapsed: 0.204 s % 25.76/4.68 % (947393)Peak memory usage: 93 MB % 25.76/4.68 % (947393)Instructions burned: 321 (million) % 25.76/4.68 % (947440)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3831363506:i=13913:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/13913Mi) % 25.76/4.68 % (947391)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 25.76/4.68 % (947391)------------------------------ % 25.76/4.68 % (947391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.76/4.68 % (947391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.76/4.68 % (947391)CaDiCaL version: 2.1.3 % 25.76/4.68 % (947391)Termination reason: Unknown % 25.76/4.68 % (947391)Termination phase: Saturation % 25.76/4.68 % (947391)Time elapsed: 0.367 s % 25.76/4.68 % (947391)Peak memory usage: 114 MB % 25.76/4.68 % (947391)Instructions burned: 541 (million) % 25.76/4.68 % (947472)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3457037539:i=9925:aac=none_2979 on theBenchmark for (2979ds/9925Mi) % 25.76/4.68 % (947479)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1525560608:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2978 on theBenchmark for (2978ds/2479Mi) % 25.76/4.68 % (947502)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3863526691:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/440Mi) % 25.76/4.68 % (947502)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 25.76/4.68 % (947412)Instruction limit reached! % 25.76/4.68 % (947412)------------------------------ % 25.76/4.68 % (947412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.76/4.68 % (947412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.76/4.68 % (947412)CaDiCaL version: 2.1.3 % 25.76/4.68 % (947412)Termination reason: Instruction limit % 25.76/4.68 % (947412)Termination phase: Saturation % 25.76/4.68 % (947412)Time elapsed: 0.441 s % 25.76/4.68 % (947412)Peak memory usage: 95 MB % 25.76/4.68 % (947412)Instructions burned: 759 (million) % 25.76/4.68 % (947440)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 25.76/4.68 % (947440)------------------------------ % 25.76/4.68 % (947440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.76/4.68 % (947440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.76/4.68 % (947440)CaDiCaL version: 2.1.3 % 25.76/4.68 % (947440)Termination reason: Unknown % 25.76/4.68 % (947440)Termination phase: Saturation % 25.76/4.68 % (947440)Time elapsed: 0.358 s % 25.76/4.68 % (947440)Peak memory usage: 113 MB % 25.76/4.68 % (947440)Instructions burned: 540 (million) % 25.76/4.68 % (947399)Instruction limit reached! % 25.76/4.68 % (947399)------------------------------ % 25.76/4.68 % (947399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.76/4.68 % (947399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.76/4.68 % (947399)CaDiCaL version: 2.1.3 % 25.76/4.68 % (947399)Termination reason: Instruction limit % 25.76/4.68 % (947399)Termination phase: Saturation % 25.76/4.68 % (947399)Time elapsed: 0.574 s % 25.76/4.68 % (947399)Peak memory usage: 99 MB % 25.76/4.68 % (947399)Instructions burned: 2064 (million) % 25.76/4.68 % (947472)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 25.76/4.68 % (947472)------------------------------ % 25.76/4.68 % (947472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.76/4.68 % (947472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.76/4.68 % (947472)CaDiCaL version: 2.1.3 % 25.76/4.68 % (947472)Termination reason: Unknown % 25.76/4.68 % (947472)Termination phase: Saturation % 30.74/5.27 % (947472)Time elapsed: 0.358 s % 30.74/5.27 % (947472)Peak memory usage: 113 MB % 30.74/5.27 % (947472)Instructions burned: 541 (million) % 30.74/5.27 % (947502)Instruction limit reached! % 30.74/5.27 % (947502)------------------------------ % 30.74/5.27 % (947502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.74/5.27 % (947502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.74/5.27 % (947502)CaDiCaL version: 2.1.3 % 30.74/5.27 % (947502)Termination reason: Instruction limit % 30.74/5.27 % (947502)Termination phase: Saturation % 30.74/5.27 % (947502)Time elapsed: 0.240 s % 30.74/5.27 % (947502)Peak memory usage: 93 MB % 30.74/5.27 % (947502)Instructions burned: 440 (million) % 30.74/5.27 % (947564)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=477108058:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2974 on theBenchmark for (2974ds/11145Mi) % 30.74/5.27 % (947565)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=4118468201:cts=off:i=3034:av=off:er=known:fsd=on_2974 on theBenchmark for (2974ds/3034Mi) % 30.74/5.27 % (947566)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=280520354:st=2:s2a=on:i=524:s2at=2:ss=axioms_2974 on theBenchmark for (2974ds/524Mi) % 30.74/5.27 % (947567)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=80111297:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2974 on theBenchmark for (2974ds/1016Mi) % 30.74/5.27 % (947568)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2333520463:i=14123:bd=preordered:ins=4_2973 on theBenchmark for (2973ds/14123Mi) % 30.74/5.27 % (947566)Instruction limit reached! % 30.74/5.27 % (947566)------------------------------ % 30.74/5.27 % (947566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.74/5.27 % (947566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.74/5.27 % (947566)CaDiCaL version: 2.1.3 % 30.74/5.27 % (947566)Termination reason: Instruction limit % 30.74/5.27 % (947566)Termination phase: Saturation % 30.74/5.27 % (947566)Time elapsed: 0.152 s % 30.74/5.27 % (947566)Peak memory usage: 93 MB % 30.74/5.27 % (947566)Instructions burned: 526 (million) % 30.74/5.27 % (947574)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=138983037:i=5781:kws=precedence:bd=all:rawr=on_2971 on theBenchmark for (2971ds/5781Mi) % 30.74/5.27 % (947564)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 30.74/5.27 % (947564)------------------------------ % 30.74/5.27 % (947564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.74/5.27 % (947564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.74/5.27 % (947564)CaDiCaL version: 2.1.3 % 30.74/5.27 % (947564)Termination reason: Unknown % 30.74/5.27 % (947564)Termination phase: Saturation % 30.74/5.27 % (947564)Time elapsed: 0.359 s % 30.74/5.27 % (947564)Peak memory usage: 113 MB % 30.74/5.27 % (947564)Instructions burned: 540 (million) % 30.74/5.27 % (947565)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 30.74/5.27 % (947565)------------------------------ % 30.74/5.27 % (947565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.74/5.27 % (947565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.74/5.27 % (947565)CaDiCaL version: 2.1.3 % 30.74/5.27 % (947565)Termination reason: Unknown % 30.74/5.27 % (947565)Termination phase: Saturation % 30.74/5.27 % (947565)Time elapsed: 0.360 s % 30.74/5.27 % (947565)Peak memory usage: 113 MB % 30.74/5.27 % (947565)Instructions burned: 541 (million) % 30.74/5.27 % (947568)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 30.74/5.27 % (947568)------------------------------ % 30.74/5.27 % (947568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.74/5.27 % (947568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.74/5.27 % (947568)CaDiCaL version: 2.1.3 % 30.74/5.27 % (947568)Termination reason: Unknown % 30.74/5.27 % (947568)Termination phase: Saturation % 30.74/5.27 % (947568)Time elapsed: 0.359 s % 30.74/5.27 % (947568)Peak memory usage: 114 MB % 30.74/5.27 % (947568)Instructions burned: 541 (million) % 30.74/5.27 % (947576)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=334515250:i=2448:gtgl=5:bd=preordered:gtg=all_2969 on theBenchmark for (2969ds/2448Mi) % 34.94/5.95 % (947577)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3750990325:i=3223:kws=precedence:fgj=on:av=off_2969 on theBenchmark for (2969ds/3223Mi) % 34.94/5.95 % (947567)Instruction limit reached! % 34.94/5.95 % (947567)------------------------------ % 34.94/5.95 % (947567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.94/5.95 % (947567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.95 % (947567)CaDiCaL version: 2.1.3 % 34.94/5.95 % (947567)Termination reason: Instruction limit % 34.94/5.95 % (947567)Termination phase: Saturation % 34.94/5.95 % (947567)Time elapsed: 0.544 s % 34.94/5.95 % (947567)Peak memory usage: 99 MB % 34.94/5.95 % (947567)Instructions burned: 1017 (million) % 34.94/5.95 % (947578)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3362753624:st=5.6:i=2033:sd=3:ss=axioms_2968 on theBenchmark for (2968ds/2033Mi) % 34.94/5.95 % (947582)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3036576366:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2967 on theBenchmark for (2967ds/2055Mi) % 34.94/5.95 % (947576)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 34.94/5.95 % (947576)------------------------------ % 34.94/5.95 % (947576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.94/5.95 % (947576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.95 % (947576)CaDiCaL version: 2.1.3 % 34.94/5.95 % (947576)Termination reason: Unknown % 34.94/5.95 % (947576)Termination phase: Saturation % 34.94/5.95 % (947576)Time elapsed: 0.361 s % 34.94/5.95 % (947576)Peak memory usage: 113 MB % 34.94/5.95 % (947576)Instructions burned: 542 (million) % 34.94/5.95 % (947577)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 34.94/5.95 % (947577)------------------------------ % 34.94/5.95 % (947577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.94/5.95 % (947577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.95 % (947577)CaDiCaL version: 2.1.3 % 34.94/5.95 % (947577)Termination reason: Unknown % 34.94/5.95 % (947577)Termination phase: Saturation % 34.94/5.95 % (947577)Time elapsed: 0.357 s % 34.94/5.95 % (947577)Peak memory usage: 113 MB % 34.94/5.95 % (947577)Instructions burned: 541 (million) % 34.94/5.95 % (947479)Instruction limit reached! % 34.94/5.95 % (947479)------------------------------ % 34.94/5.95 % (947479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.94/5.95 % (947479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.95 % (947479)CaDiCaL version: 2.1.3 % 34.94/5.95 % (947479)Termination reason: Instruction limit % 34.94/5.95 % (947479)Termination phase: Saturation % 34.94/5.95 % (947479)Time elapsed: 1.336 s % 34.94/5.95 % (947479)Peak memory usage: 102 MB % 34.94/5.95 % (947479)Instructions burned: 2481 (million) % 34.94/5.95 % (947578)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 34.94/5.95 % (947578)------------------------------ % 34.94/5.95 % (947578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.94/5.95 % (947578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.94/5.95 % (947578)CaDiCaL version: 2.1.3 % 34.94/5.95 % (947578)Termination reason: Unknown % 34.94/5.95 % (947578)Termination phase: Saturation % 34.94/5.95 % (947578)Time elapsed: 0.361 s % 34.94/5.95 % (947578)Peak memory usage: 114 MB % 34.94/5.95 % (947578)Instructions burned: 541 (million) % 34.94/5.95 % (947585)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=1815622276:i=21611:sd=3:ss=axioms_2964 on theBenchmark for (2964ds/21611Mi) % 34.94/5.95 % (947586)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2835613100:i=4835:sd=13:ss=axioms:sgt=23_2964 on theBenchmark for (2964ds/4835Mi) % 34.94/5.95 % (947587)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=2121517777:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2963 on theBenchmark for (2963ds/797Mi) % 34.94/5.95 % (947582)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 34.94/5.95 % (947582)------------------------------ % 34.94/5.95 % (947582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.60 % (947582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.60 % (947582)CaDiCaL version: 2.1.3 % 39.25/6.60 % (947582)Termination reason: Unknown % 39.25/6.60 % (947582)Termination phase: Saturation % 39.25/6.60 % (947582)Time elapsed: 0.360 s % 39.25/6.60 % (947582)Peak memory usage: 113 MB % 39.25/6.60 % (947582)Instructions burned: 541 (million) % 39.25/6.60 % (947588)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2042665521:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2963 on theBenchmark for (2963ds/2326Mi) % 39.25/6.60 % (947588)Refutation not found, incomplete strategy % 39.25/6.60 % (947588)------------------------------ % 39.25/6.60 % (947588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.60 % (947588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.60 % (947588)CaDiCaL version: 2.1.3 % 39.25/6.60 % (947588)Termination reason: Refutation not found, incomplete strategy % 39.25/6.60 % (947588)Time elapsed: 0.009 s % 39.25/6.60 % (947588)Peak memory usage: 88 MB % 39.25/6.60 % (947588)Instructions burned: 13 (million) % 39.25/6.60 % (947592)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1962555951:i=6038:nm=6_2961 on theBenchmark for (2961ds/6038Mi) % 39.25/6.60 % (947585)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 39.25/6.60 % (947585)------------------------------ % 39.25/6.60 % (947585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.60 % (947585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.60 % (947585)CaDiCaL version: 2.1.3 % 39.25/6.60 % (947585)Termination reason: Unknown % 39.25/6.60 % (947585)Termination phase: Saturation % 39.25/6.60 % (947585)Time elapsed: 0.362 s % 39.25/6.60 % (947585)Peak memory usage: 113 MB % 39.25/6.60 % (947585)Instructions burned: 539 (million) % 39.25/6.60 % (947588)------------------------------ % 39.25/6.60 % (947588)------------------------------ % 39.25/6.60 % (947595)lrs+10_1_sil=32000:sp=occurrence:random_seed=2560703938:st=2:i=33334:sd=3:ss=included:sgt=32_2959 on theBenchmark for (2959ds/33334Mi) % 39.25/6.60 % (947587)Instruction limit reached! % 39.25/6.60 % (947587)------------------------------ % 39.25/6.60 % (947587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.60 % (947587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.60 % (947587)CaDiCaL version: 2.1.3 % 39.25/6.60 % (947587)Termination reason: Instruction limit % 39.25/6.60 % (947587)Termination phase: Saturation % 39.25/6.60 % (947587)Time elapsed: 0.466 s % 39.25/6.60 % (947587)Peak memory usage: 103 MB % 39.25/6.60 % (947587)Instructions burned: 798 (million) % 39.25/6.60 % (947596)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2925199851:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2959 on theBenchmark for (2959ds/1008Mi) % 39.25/6.60 % (947409)Instruction limit reached! % 39.25/6.60 % (947409)------------------------------ % 39.25/6.60 % (947409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.60 % (947409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.60 % (947409)CaDiCaL version: 2.1.3 % 39.25/6.60 % (947409)Termination reason: Instruction limit % 39.25/6.60 % (947409)Termination phase: Saturation % 39.25/6.60 % (947409)Time elapsed: 2.173 s % 39.25/6.60 % (947409)Peak memory usage: 99 MB % 39.25/6.60 % (947409)Instructions burned: 3707 (million) % 39.25/6.60 % (947592)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 39.25/6.60 % (947592)------------------------------ % 39.25/6.60 % (947592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.25/6.60 % (947592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.25/6.60 % (947592)CaDiCaL version: 2.1.3 % 39.25/6.60 % (947592)Termination reason: Unknown % 39.25/6.60 % (947592)Termination phase: Saturation % 39.25/6.60 % (947592)Time elapsed: 0.361 s % 39.25/6.60 % (947592)Peak memory usage: 113 MB % 39.25/6.60 % (947592)Instructions burned: 541 (million) % 39.25/6.60 % (947598)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=4270519746:i=8327:s2at=5:bd=preordered_2957 on theBenchmark for (2957ds/8327Mi) % 39.25/6.60 % (947600)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=4141760160:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2957 on theBenchmark for (2957ds/1083Mi) % 44.99/7.21 % (947601)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=857258923:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2956 on theBenchmark for (2956ds/1084Mi) % 44.99/7.21 % (947596)Instruction limit reached! % 44.99/7.21 % (947596)------------------------------ % 44.99/7.21 % (947596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.99/7.21 % (947596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.99/7.21 % (947596)CaDiCaL version: 2.1.3 % 44.99/7.21 % (947596)Termination reason: Instruction limit % 44.99/7.21 % (947596)Termination phase: Saturation % 44.99/7.21 % (947596)Time elapsed: 0.448 s % 44.99/7.21 % (947596)Peak memory usage: 93 MB % 44.99/7.21 % (947596)Instructions burned: 1009 (million) % 44.99/7.21 % (947598)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 44.99/7.21 % (947598)------------------------------ % 44.99/7.21 % (947598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.99/7.21 % (947598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.99/7.21 % (947598)CaDiCaL version: 2.1.3 % 44.99/7.21 % (947598)Termination reason: Unknown % 44.99/7.21 % (947598)Termination phase: Saturation % 44.99/7.21 % (947598)Time elapsed: 0.359 s % 44.99/7.21 % (947598)Peak memory usage: 114 MB % 44.99/7.21 % (947598)Instructions burned: 542 (million) % 44.99/7.21 % (947574)Instruction limit reached! % 44.99/7.21 % (947574)------------------------------ % 44.99/7.21 % (947574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.99/7.21 % (947574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.99/7.21 % (947574)CaDiCaL version: 2.1.3 % 44.99/7.21 % (947574)Termination reason: Instruction limit % 44.99/7.21 % (947574)Termination phase: Saturation % 44.99/7.21 % (947574)Time elapsed: 1.812 s % 44.99/7.21 % (947574)Peak memory usage: 122 MB % 44.99/7.21 % (947574)Instructions burned: 5784 (million) % 44.99/7.21 % (947605)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=917210529:i=6995:s2at=5:gtg=all_2953 on theBenchmark for (2953ds/6995Mi) % 44.99/7.21 % (947606)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1213634099:st=2:i=6225:sd=15:ss=axioms_2952 on theBenchmark for (2952ds/6225Mi) % 44.99/7.21 % (947607)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1870314263:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2952 on theBenchmark for (2952ds/3372Mi) % 44.99/7.21 % (947600)Instruction limit reached! % 44.99/7.21 % (947600)------------------------------ % 44.99/7.21 % (947600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.99/7.21 % (947600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.99/7.21 % (947600)CaDiCaL version: 2.1.3 % 44.99/7.21 % (947600)Termination reason: Instruction limit % 44.99/7.21 % (947600)Termination phase: Saturation % 44.99/7.21 % (947600)Time elapsed: 0.541 s % 44.99/7.21 % (947600)Peak memory usage: 95 MB % 44.99/7.21 % (947600)Instructions burned: 1084 (million) % 44.99/7.21 % (947601)Instruction limit reached! % 44.99/7.21 % (947601)------------------------------ % 44.99/7.21 % (947601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.99/7.21 % (947601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.99/7.21 % (947601)CaDiCaL version: 2.1.3 % 44.99/7.21 % (947601)Termination reason: Instruction limit % 44.99/7.21 % (947601)Termination phase: Saturation % 44.99/7.21 % (947601)Time elapsed: 0.496 s % 44.99/7.21 % (947601)Peak memory usage: 97 MB % 44.99/7.21 % (947601)Instructions burned: 1084 (million) % 44.99/7.21 % (947607)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 44.99/7.21 % (947607)------------------------------ % 44.99/7.21 % (947607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.99/7.21 % (947607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.99/7.21 % (947607)CaDiCaL version: 2.1.3 % 44.99/7.21 % (947607)Termination reason: Unknown % 44.99/7.21 % (947607)Termination phase: Saturation % 44.99/7.21 % (947607)Time elapsed: 0.193 s % 44.99/7.21 % (947607)Peak memory usage: 113 MB % 48.56/7.85 % (947607)Instructions burned: 538 (million) % 48.56/7.85 % (947611)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2770528822:st=2.3:i=26457:sd=10:ss=included:sgt=8_2950 on theBenchmark for (2950ds/26457Mi) % 48.56/7.85 % (947612)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=1178670532:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2950 on theBenchmark for (2950ds/13494Mi) % 48.56/7.85 % (947605)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 48.56/7.85 % (947605)------------------------------ % 48.56/7.85 % (947605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.56/7.85 % (947605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.56/7.85 % (947605)CaDiCaL version: 2.1.3 % 48.56/7.85 % (947605)Termination reason: Unknown % 48.56/7.85 % (947605)Termination phase: Saturation % 48.56/7.85 % (947605)Time elapsed: 0.363 s % 48.56/7.85 % (947605)Peak memory usage: 114 MB % 48.56/7.85 % (947605)Instructions burned: 545 (million) % 48.56/7.85 % (947613)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=2706032436:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2949 on theBenchmark for (2949ds/2503Mi) % 48.56/7.85 % (947613)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 48.56/7.85 % (947617)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=265887047:i=2559:sd=1:ep=RSTC:ss=axioms_2947 on theBenchmark for (2947ds/2559Mi) % 48.56/7.85 % (947613)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 48.56/7.85 % (947613)------------------------------ % 48.56/7.85 % (947613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.56/7.85 % (947613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.56/7.85 % (947613)CaDiCaL version: 2.1.3 % 48.56/7.85 % (947613)Termination reason: Unknown % 48.56/7.85 % (947613)Termination phase: Saturation % 48.56/7.85 % (947613)Time elapsed: 0.195 s % 48.56/7.85 % (947613)Peak memory usage: 113 MB % 48.56/7.85 % (947613)Instructions burned: 541 (million) % 48.56/7.85 % (947611)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 48.56/7.85 % (947611)------------------------------ % 48.56/7.85 % (947611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.56/7.85 % (947611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.56/7.85 % (947611)CaDiCaL version: 2.1.3 % 48.56/7.85 % (947611)Termination reason: Unknown % 48.56/7.85 % (947611)Termination phase: Saturation % 48.56/7.85 % (947611)Time elapsed: 0.363 s % 48.56/7.85 % (947611)Peak memory usage: 113 MB % 48.56/7.85 % (947611)Instructions burned: 542 (million) % 48.56/7.85 % (947612)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 48.56/7.85 % (947612)------------------------------ % 48.56/7.85 % (947612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.56/7.85 % (947612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.56/7.85 % (947612)CaDiCaL version: 2.1.3 % 48.56/7.85 % (947612)Termination reason: Unknown % 48.56/7.85 % (947612)Termination phase: Saturation % 48.56/7.85 % (947612)Time elapsed: 0.361 s % 48.56/7.85 % (947612)Peak memory usage: 114 MB % 48.56/7.85 % (947612)Instructions burned: 542 (million) % 48.56/7.85 % (947619)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2570501659:i=30753:av=off:ss=included_2945 on theBenchmark for (2945ds/30753Mi) % 48.56/7.85 % (947620)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3988714508:i=26473:ep=RSTC_2945 on theBenchmark for (2945ds/26473Mi) % 48.56/7.85 % (947621)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=558161896:cts=off:i=2759:kws=inv_arity:fgj=on_2944 on theBenchmark for (2944ds/2759Mi) % 48.56/7.85 % (947619)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 48.56/7.85 % (947619)------------------------------ % 48.56/7.85 % (947619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.56/7.85 % (947619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.79/8.50 % (947619)CaDiCaL version: 2.1.3 % 53.79/8.50 % (947619)Termination reason: Unknown % 53.79/8.50 % (947619)Termination phase: Saturation % 53.79/8.50 % (947619)Time elapsed: 0.195 s % 53.79/8.50 % (947619)Peak memory usage: 113 MB % 53.79/8.50 % (947619)Instructions burned: 541 (million) % 53.79/8.50 % (947617)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.79/8.50 % (947617)------------------------------ % 53.79/8.50 % (947617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.79/8.50 % (947617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.79/8.50 % (947617)CaDiCaL version: 2.1.3 % 53.79/8.50 % (947617)Termination reason: Unknown % 53.79/8.50 % (947617)Termination phase: Saturation % 53.79/8.50 % (947617)Time elapsed: 0.359 s % 53.79/8.50 % (947617)Peak memory usage: 113 MB % 53.79/8.50 % (947617)Instructions burned: 539 (million) % 53.79/8.50 % (947625)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=836088156:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2942 on theBenchmark for (2942ds/5665Mi) % 53.79/8.50 % (947625)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 53.79/8.50 % (947626)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=3687105323:i=1532:ep=RS:ss=axioms_2942 on theBenchmark for (2942ds/1532Mi) % 53.79/8.50 % (947621)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.79/8.50 % (947621)------------------------------ % 53.79/8.50 % (947621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.79/8.50 % (947621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.79/8.50 % (947621)CaDiCaL version: 2.1.3 % 53.79/8.50 % (947621)Termination reason: Unknown % 53.79/8.50 % (947621)Termination phase: Saturation % 53.79/8.50 % (947621)Time elapsed: 0.358 s % 53.79/8.50 % (947621)Peak memory usage: 113 MB % 53.79/8.50 % (947621)Instructions burned: 540 (million) % 53.79/8.50 % (947625)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.79/8.51 % (947625)------------------------------ % 53.79/8.51 % (947625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.79/8.51 % (947625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.79/8.51 % (947625)CaDiCaL version: 2.1.3 % 53.79/8.51 % (947625)Termination reason: Unknown % 53.79/8.51 % (947625)Termination phase: Saturation % 53.79/8.51 % (947625)Time elapsed: 0.192 s % 53.79/8.51 % (947625)Peak memory usage: 113 MB % 53.79/8.51 % (947625)Instructions burned: 541 (million) % 53.79/8.51 % (947630)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=3097800797:i=1572:fgj=on:gsp=on_2939 on theBenchmark for (2939ds/1572Mi) % 53.79/8.51 % (947630)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 53.79/8.51 % (947629)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3518415007:i=1565:sd=2:ss=axioms:sgt=32_2939 on theBenchmark for (2939ds/1565Mi) % 53.79/8.51 % (947626)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.79/8.51 % (947626)------------------------------ % 53.79/8.51 % (947626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.79/8.51 % (947626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.79/8.51 % (947626)CaDiCaL version: 2.1.3 % 53.79/8.51 % (947626)Termination reason: Unknown % 53.79/8.51 % (947626)Termination phase: Saturation % 53.79/8.51 % (947626)Time elapsed: 0.358 s % 53.79/8.51 % (947626)Peak memory usage: 113 MB % 53.79/8.51 % (947626)Instructions burned: 541 (million) % 53.79/8.51 % (947630)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.79/8.51 % (947630)------------------------------ % 53.79/8.51 % (947630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.79/8.51 % (947630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.79/8.51 % (947630)CaDiCaL version: 2.1.3 % 53.79/8.51 % (947630)Termination reason: Unknown % 53.79/8.51 % (947630)Termination phase: Saturation % 53.79/8.51 % (947630)Time elapsed: 0.193 s % 53.79/8.51 % (947630)Peak memory usage: 113 MB % 59.96/9.38 % (947630)Instructions burned: 540 (million) % 59.96/9.38 % (947586)Instruction limit reached! % 59.96/9.38 % (947586)------------------------------ % 59.96/9.38 % (947586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.96/9.38 % (947586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.96/9.38 % (947586)CaDiCaL version: 2.1.3 % 59.96/9.38 % (947586)Termination reason: Instruction limit % 59.96/9.38 % (947586)Termination phase: Saturation % 59.96/9.38 % (947586)Time elapsed: 2.680 s % 59.96/9.38 % (947586)Peak memory usage: 115 MB % 59.96/9.38 % (947586)Instructions burned: 4836 (million) % 59.96/9.38 % (947633)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3750464016:i=6052:sd=4:ss=axioms:sgt=24_2937 on theBenchmark for (2937ds/6052Mi) % 59.96/9.38 % (947634)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=3259216274:i=3500:sd=1:bd=preordered:sup=off:ss=included_2936 on theBenchmark for (2936ds/3500Mi) % 59.96/9.38 % (947629)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 59.96/9.38 % (947629)------------------------------ % 59.96/9.38 % (947629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.96/9.38 % (947629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.96/9.38 % (947629)CaDiCaL version: 2.1.3 % 59.96/9.38 % (947629)Termination reason: Unknown % 59.96/9.38 % (947629)Termination phase: Saturation % 59.96/9.38 % (947629)Time elapsed: 0.361 s % 59.96/9.38 % (947629)Peak memory usage: 113 MB % 59.96/9.38 % (947629)Instructions burned: 540 (million) % 59.96/9.38 % (947636)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=1039753587:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2936 on theBenchmark for (2936ds/1842Mi) % 59.96/9.38 % (947636)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 59.96/9.38 % (947634)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 59.96/9.38 % (947634)------------------------------ % 59.96/9.38 % (947634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.96/9.38 % (947634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.96/9.38 % (947634)CaDiCaL version: 2.1.3 % 59.96/9.38 % (947634)Termination reason: Unknown % 59.96/9.38 % (947634)Termination phase: Saturation % 59.96/9.38 % (947634)Time elapsed: 0.194 s % 59.96/9.38 % (947634)Peak memory usage: 113 MB % 59.96/9.38 % (947634)Instructions burned: 540 (million) % 59.96/9.38 % (947639)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=703199700:i=66096:add=on_2934 on theBenchmark for (2934ds/66096Mi) % 59.96/9.38 % (947633)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 59.96/9.38 % (947633)------------------------------ % 59.96/9.38 % (947633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.96/9.38 % (947633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.96/9.38 % (947633)CaDiCaL version: 2.1.3 % 59.96/9.38 % (947633)Termination reason: Unknown % 59.96/9.38 % (947633)Termination phase: Saturation % 59.96/9.38 % (947633)Time elapsed: 0.360 s % 59.96/9.38 % (947633)Peak memory usage: 113 MB % 59.96/9.38 % (947633)Instructions burned: 541 (million) % 59.96/9.38 % (947640)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1589358732:i=1884:sd=1:nm=60:ss=axioms_2933 on theBenchmark for (2933ds/1884Mi) % 59.96/9.38 % (947636)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 59.96/9.38 % (947636)------------------------------ % 59.96/9.38 % (947636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.96/9.38 % (947636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.96/9.38 % (947636)CaDiCaL version: 2.1.3 % 59.96/9.38 % (947636)Termination reason: Unknown % 59.96/9.38 % (947636)Termination phase: Saturation % 59.96/9.38 % (947636)Time elapsed: 0.359 s % 59.96/9.38 % (947636)Peak memory usage: 113 MB % 59.96/9.38 % (947636)Instructions burned: 542 (million) % 59.96/9.38 % (947642)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3541604143:cts=off:i=5469:bs=on:fsr=off_2932 on theBenchmark for (2932ds/5469Mi) % 59.96/9.38 % (947640)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.16/11.05 % (947640)------------------------------ % 70.16/11.05 % (947640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.16/11.05 % (947640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.16/11.05 % (947640)CaDiCaL version: 2.1.3 % 70.16/11.05 % (947640)Termination reason: Unknown % 70.16/11.05 % (947640)Termination phase: Saturation % 70.16/11.05 % (947640)Time elapsed: 0.195 s % 70.16/11.05 % (947640)Peak memory usage: 113 MB % 70.16/11.05 % (947640)Instructions burned: 538 (million) % 70.16/11.05 % (947639)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.16/11.05 % (947639)------------------------------ % 70.16/11.05 % (947639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.16/11.05 % (947639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.16/11.05 % (947639)CaDiCaL version: 2.1.3 % 70.16/11.05 % (947639)Termination reason: Unknown % 70.16/11.05 % (947639)Termination phase: Saturation % 70.16/11.05 % (947639)Time elapsed: 0.361 s % 70.16/11.05 % (947639)Peak memory usage: 113 MB % 70.16/11.05 % (947639)Instructions burned: 541 (million) % 70.16/11.05 % (947645)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=3756540019:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2930 on theBenchmark for (2930ds/2037Mi) % 70.16/11.05 % (947646)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1766626394:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2930 on theBenchmark for (2930ds/2110Mi) % 70.16/11.05 % (947647)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=2176256935:i=2430:add=off:aac=none:nm=16_2929 on theBenchmark for (2929ds/2430Mi) % 70.16/11.05 % (947646)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.16/11.05 % (947646)------------------------------ % 70.16/11.05 % (947646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.16/11.05 % (947646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.16/11.05 % (947646)CaDiCaL version: 2.1.3 % 70.16/11.05 % (947646)Termination reason: Unknown % 70.16/11.05 % (947646)Termination phase: Saturation % 70.16/11.05 % (947646)Time elapsed: 0.195 s % 70.16/11.05 % (947646)Peak memory usage: 114 MB % 70.16/11.05 % (947646)Instructions burned: 544 (million) % 70.16/11.05 % (947651)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=2471083513:cond=fast:i=4891_2927 on theBenchmark for (2927ds/4891Mi) % 70.16/11.05 % (947645)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.16/11.05 % (947645)------------------------------ % 70.16/11.05 % (947645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.16/11.05 % (947645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.16/11.05 % (947645)CaDiCaL version: 2.1.3 % 70.16/11.05 % (947645)Termination reason: Unknown % 70.16/11.05 % (947645)Termination phase: Saturation % 70.16/11.05 % (947645)Time elapsed: 0.364 s % 70.16/11.05 % (947645)Peak memory usage: 114 MB % 70.16/11.05 % (947645)Instructions burned: 547 (million) % 70.16/11.05 % (947647)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.16/11.05 % (947647)------------------------------ % 70.16/11.05 % (947647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.16/11.05 % (947647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.16/11.05 % (947647)CaDiCaL version: 2.1.3 % 70.16/11.05 % (947647)Termination reason: Unknown % 70.16/11.05 % (947647)Termination phase: Saturation % 70.16/11.05 % (947647)Time elapsed: 0.359 s % 70.16/11.05 % (947647)Peak memory usage: 113 MB % 70.16/11.05 % (947647)Instructions burned: 541 (million) % 70.16/11.05 % (947653)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=2796608361:st=2:i=14845:sd=2:ss=included:fsd=on_2925 on theBenchmark for (2925ds/14845Mi) % 70.16/11.05 % (947651)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 70.16/11.05 % (947651)------------------------------ % 70.16/11.05 % (947651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.07/11.56 % (947651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.07/11.56 % (947651)CaDiCaL version: 2.1.3 % 72.07/11.56 % (947651)Termination reason: Unknown % 72.07/11.56 % (947651)Termination phase: Saturation % 72.07/11.56 % (947651)Time elapsed: 0.196 s % 72.07/11.56 % (947651)Peak memory usage: 114 MB % 72.07/11.56 % (947651)Instructions burned: 541 (million) % 72.07/11.56 % (947654)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=4170928519:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2924 on theBenchmark for (2924ds/7534Mi) % 72.07/11.56 % (947656)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=2016279187:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2923 on theBenchmark for (2923ds/10353Mi) % 72.07/11.56 % (947656)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 72.07/11.56 % (947656)------------------------------ % 72.07/11.56 % (947656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.07/11.56 % (947656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.07/11.56 % (947656)CaDiCaL version: 2.1.3 % 72.07/11.56 % (947656)Termination reason: Unknown % 72.07/11.56 % (947656)Termination phase: Saturation % 72.07/11.56 % (947656)Time elapsed: 0.192 s % 72.07/11.56 % (947656)Peak memory usage: 114 MB % 72.07/11.56 % (947656)Instructions burned: 542 (million) % 72.07/11.56 % (947653)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 72.07/11.56 % (947653)------------------------------ % 72.07/11.56 % (947653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.07/11.56 % (947653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.07/11.56 % (947653)CaDiCaL version: 2.1.3 % 72.07/11.56 % (947653)Termination reason: Unknown % 72.07/11.56 % (947653)Termination phase: Saturation % 72.07/11.56 % (947653)Time elapsed: 0.361 s % 72.07/11.56 % (947653)Peak memory usage: 114 MB % 72.07/11.56 % (947653)Instructions burned: 541 (million) % 72.07/11.56 % (947659)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2812848505:i=7860_2920 on theBenchmark for (2920ds/7860Mi) % 72.07/11.56 % (947654)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 72.07/11.56 % (947654)------------------------------ % 72.07/11.56 % (947654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.07/11.56 % (947654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.07/11.56 % (947654)CaDiCaL version: 2.1.3 % 72.07/11.56 % (947654)Termination reason: Unknown % 72.07/11.56 % (947654)Termination phase: Saturation % 72.07/11.56 % (947654)Time elapsed: 0.361 s % 72.07/11.56 % (947654)Peak memory usage: 113 MB % 72.07/11.56 % (947654)Instructions burned: 543 (million) % 72.07/11.56 % (947660)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=2124221808:i=7896:sd=2:bs=on:ss=included:sgt=20_2920 on theBenchmark for (2920ds/7896Mi) % 72.07/11.56 % (947662)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=4059312164:i=5812:gtgl=2:gtg=all_2918 on theBenchmark for (2918ds/5812Mi) % 72.07/11.56 % (947606)Instruction limit reached! % 72.07/11.56 % (947606)------------------------------ % 72.07/11.56 % (947606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.07/11.56 % (947606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.07/11.56 % (947606)CaDiCaL version: 2.1.3 % 72.07/11.56 % (947606)Termination reason: Instruction limit % 72.07/11.56 % (947606)Termination phase: Saturation % 72.07/11.56 % (947606)Time elapsed: 3.556 s % 72.07/11.56 % (947606)Peak memory usage: 120 MB % 72.07/11.56 % (947606)Instructions burned: 6226 (million) % 72.07/11.56 % (947660)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 72.07/11.56 % (947660)------------------------------ % 72.07/11.56 % (947660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.07/11.56 % (947660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.07/11.56 % (947660)CaDiCaL version: 2.1.3 % 72.07/11.56 % (947660)Termination reason: Unknown % 72.07/11.56 % (947660)Termination phase: Saturation % 72.07/11.56 % (947660)Time elapsed: 0.359 s % 72.07/11.56 % (947660)Peak memory usage: 113 MB % 77.20/12.10 % (947660)Instructions burned: 542 (million) % 77.20/12.10 % (947665)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=1299529733:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2915 on theBenchmark for (2915ds/2965Mi) % 77.20/12.10 % (947662)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 77.20/12.10 % (947662)------------------------------ % 77.20/12.10 % (947662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.20/12.10 % (947662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.20/12.10 % (947662)CaDiCaL version: 2.1.3 % 77.20/12.10 % (947662)Termination reason: Unknown % 77.20/12.10 % (947662)Termination phase: Saturation % 77.20/12.10 % (947662)Time elapsed: 0.360 s % 77.20/12.10 % (947662)Peak memory usage: 114 MB % 77.20/12.10 % (947662)Instructions burned: 544 (million) % 77.20/12.10 % (947666)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=2314766979:i=2967:kws=precedence:bd=preordered:av=off_2914 on theBenchmark for (2914ds/2967Mi) % 77.20/12.10 % (947668)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=287046787:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2913 on theBenchmark for (2913ds/3022Mi) % 77.20/12.10 % (947665)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 77.20/12.10 % (947665)------------------------------ % 77.20/12.10 % (947665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.20/12.10 % (947665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.20/12.10 % (947665)CaDiCaL version: 2.1.3 % 77.20/12.10 % (947665)Termination reason: Unknown % 77.20/12.10 % (947665)Termination phase: Saturation % 77.20/12.10 % (947665)Time elapsed: 1.063 s % 77.20/12.10 % (947665)Peak memory usage: 113 MB % 77.20/12.10 % (947665)Instructions burned: 542 (million) % 77.20/12.10 % (947666)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 77.20/12.10 % (947666)------------------------------ % 77.20/12.10 % (947666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.20/12.10 % (947666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.20/12.10 % (947666)CaDiCaL version: 2.1.3 % 77.20/12.10 % (947666)Termination reason: Unknown % 77.20/12.10 % (947666)Termination phase: Saturation % 77.20/12.10 % (947666)Time elapsed: 1.066 s % 77.20/12.10 % (947666)Peak memory usage: 113 MB % 77.20/12.10 % (947666)Instructions burned: 541 (million) % 77.20/12.10 % (947671)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=2476797031:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2903 on theBenchmark for (2903ds/3207Mi) % 77.20/12.10 % (947668)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 77.20/12.10 % (947668)------------------------------ % 77.20/12.10 % (947668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.20/12.10 % (947668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.20/12.10 % (947668)CaDiCaL version: 2.1.3 % 77.20/12.10 % (947668)Termination reason: Unknown % 77.20/12.10 % (947668)Termination phase: Saturation % 77.20/12.10 % (947668)Time elapsed: 1.073 s % 77.20/12.10 % (947668)Peak memory usage: 113 MB % 77.20/12.10 % (947668)Instructions burned: 538 (million) % 77.20/12.10 % (947672)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2033363168:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2902 on theBenchmark for (2902ds/3289Mi) % 77.20/12.10 % (947674)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2912182790:i=38569:sd=3:ss=axioms:sgt=32_2901 on theBenchmark for (2901ds/38569Mi) % 77.20/12.10 % (947671)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 77.20/12.10 % (947671)------------------------------ % 77.20/12.10 % (947671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.20/12.10 % (947671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.20/12.10 % (947671)CaDiCaL version: 2.1.3 % 77.20/12.10 % (947671)Termination reason: Unknown % 77.20/12.10 % (947671)Termination phase: Saturation % 79.93/12.63 % (947671)Time elapsed: 0.357 s % 79.93/12.63 % (947671)Peak memory usage: 113 MB % 79.93/12.63 % (947671)Instructions burned: 539 (million) % 79.93/12.63 % (947642)Instruction limit reached! % 79.93/12.63 % (947642)------------------------------ % 79.93/12.63 % (947642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.93/12.63 % (947642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.93/12.63 % (947642)CaDiCaL version: 2.1.3 % 79.93/12.63 % (947642)Termination reason: Instruction limit % 79.93/12.63 % (947642)Termination phase: Saturation % 79.93/12.63 % (947642)Time elapsed: 3.273 s % 79.93/12.63 % (947642)Peak memory usage: 128 MB % 79.93/12.63 % (947642)Instructions burned: 5470 (million) % 79.93/12.63 % (947672)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 79.93/12.63 % (947672)------------------------------ % 79.93/12.63 % (947672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.93/12.63 % (947672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.93/12.63 % (947672)CaDiCaL version: 2.1.3 % 79.93/12.63 % (947672)Termination reason: Unknown % 79.93/12.63 % (947672)Termination phase: Saturation % 79.93/12.63 % (947672)Time elapsed: 0.359 s % 79.93/12.63 % (947672)Peak memory usage: 113 MB % 79.93/12.63 % (947672)Instructions burned: 543 (million) % 79.93/12.63 % (947659)Instruction limit reached! % 79.93/12.63 % (947659)------------------------------ % 79.93/12.63 % (947659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.93/12.63 % (947659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.93/12.63 % (947659)CaDiCaL version: 2.1.3 % 79.93/12.63 % (947659)Termination reason: Instruction limit % 79.93/12.63 % (947659)Termination phase: Saturation % 79.93/12.63 % (947659)Time elapsed: 2.188 s % 79.93/12.63 % (947659)Peak memory usage: 124 MB % 79.93/12.63 % (947659)Instructions burned: 7861 (million) % 79.93/12.63 % (947677)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3203302789:cts=off:i=3394_2898 on theBenchmark for (2898ds/3394Mi) % 79.93/12.63 % (947678)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=167092437:i=33824:bd=preordered_2898 on theBenchmark for (2898ds/33824Mi) % 79.93/12.63 % (947680)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=2962463024: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_2897 on theBenchmark for (2897ds/7222Mi) % 79.93/12.63 % (947680)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 79.93/12.63 % (947674)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 79.93/12.63 % (947674)------------------------------ % 79.93/12.63 % (947674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.93/12.63 % (947674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.93/12.63 % (947674)CaDiCaL version: 2.1.3 % 79.93/12.63 % (947674)Termination reason: Unknown % 79.93/12.63 % (947674)Termination phase: Saturation % 79.93/12.63 % (947674)Time elapsed: 0.362 s % 79.93/12.63 % (947674)Peak memory usage: 113 MB % 79.93/12.63 % (947674)Instructions burned: 541 (million) % 79.93/12.63 % (947679)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2851902827:i=20684:bd=all:gtg=exists_sym_2897 on theBenchmark for (2897ds/20684Mi) % 79.93/12.63 % (947685)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1053383202:st=4:i=7295:sd=4:ep=R:ss=axioms_2895 on theBenchmark for (2895ds/7295Mi) % 79.93/12.63 % (947680)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 79.93/12.63 % (947680)------------------------------ % 79.93/12.63 % (947680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.93/12.63 % (947680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.93/12.63 % (947680)CaDiCaL version: 2.1.3 % 79.93/12.63 % (947680)Termination reason: Unknown % 79.93/12.63 % (947680)Termination phase: Saturation % 79.93/12.63 % (947680)Time elapsed: 0.196 s % 79.93/12.63 % (947680)Peak memory usage: 113 MB % 79.93/12.63 % (947680)Instructions burned: 541 (million) % 79.93/12.63 % (947677)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 86.00/13.36 % (947677)------------------------------ % 86.00/13.36 % (947677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.00/13.36 % (947677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.00/13.36 % (947677)CaDiCaL version: 2.1.3 % 86.00/13.36 % (947677)Termination reason: Unknown % 86.00/13.36 % (947677)Termination phase: Saturation % 86.00/13.36 % (947677)Time elapsed: 0.360 s % 86.00/13.36 % (947677)Peak memory usage: 113 MB % 86.00/13.36 % (947677)Instructions burned: 541 (million) % 86.00/13.36 % (947678)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 86.00/13.36 % (947678)------------------------------ % 86.00/13.36 % (947678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.00/13.36 % (947678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.00/13.36 % (947678)CaDiCaL version: 2.1.3 % 86.00/13.36 % (947678)Termination reason: Unknown % 86.00/13.36 % (947678)Termination phase: Saturation % 86.00/13.36 % (947678)Time elapsed: 0.360 s % 86.00/13.36 % (947678)Peak memory usage: 114 MB % 86.00/13.36 % (947678)Instructions burned: 541 (million) % 86.00/13.36 % (947687)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=1501471493:i=4036:ins=10_2894 on theBenchmark for (2894ds/4036Mi) % 86.00/13.36 % (947679)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 86.00/13.36 % (947679)------------------------------ % 86.00/13.36 % (947679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.00/13.36 % (947679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.00/13.36 % (947679)CaDiCaL version: 2.1.3 % 86.00/13.36 % (947679)Termination reason: Unknown % 86.00/13.36 % (947679)Termination phase: Saturation % 86.00/13.36 % (947679)Time elapsed: 0.362 s % 86.00/13.36 % (947679)Peak memory usage: 114 MB % 86.00/13.36 % (947679)Instructions burned: 544 (million) % 86.00/13.36 % (947688)lrs+10_1_sil=128000:lcm=predicate:random_seed=3923097585:st=3:i=43697:sd=5:ss=axioms_2893 on theBenchmark for (2893ds/43697Mi) % 86.00/13.36 % (947689)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=4076346477:i=17599:gtg=all:ss=axioms:fsd=on_2892 on theBenchmark for (2892ds/17599Mi) % 86.00/13.36 % (947687)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 86.00/13.36 % (947687)------------------------------ % 86.00/13.36 % (947687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.00/13.36 % (947687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.00/13.36 % (947687)CaDiCaL version: 2.1.3 % 86.00/13.36 % (947687)Termination reason: Unknown % 86.00/13.36 % (947687)Termination phase: Saturation % 86.00/13.36 % (947687)Time elapsed: 0.196 s % 86.00/13.36 % (947687)Peak memory usage: 113 MB % 86.00/13.36 % (947687)Instructions burned: 541 (million) % 86.00/13.36 % (947685)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 86.00/13.36 % (947685)------------------------------ % 86.00/13.36 % (947685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.00/13.36 % (947685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.00/13.36 % (947685)CaDiCaL version: 2.1.3 % 86.00/13.36 % (947685)Termination reason: Unknown % 86.00/13.36 % (947685)Termination phase: Saturation % 86.00/13.36 % (947685)Time elapsed: 0.361 s % 86.00/13.36 % (947685)Peak memory usage: 113 MB % 86.00/13.36 % (947685)Instructions burned: 542 (million) % 86.00/13.36 % (947691)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=1807434758:i=4547:bd=preordered_2892 on theBenchmark for (2892ds/4547Mi) % 86.00/13.36 % (947694)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=2186447101:i=9294:av=off_2890 on theBenchmark for (2890ds/9294Mi) % 86.00/13.36 % (947695)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3249986601:i=32849:add=on_2890 on theBenchmark for (2890ds/32849Mi) % 86.00/13.36 % (947689)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 86.00/13.36 % (947689)------------------------------ % 86.00/13.36 % (947689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.93/18.61 % (947689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.93/18.61 % (947689)CaDiCaL version: 2.1.3 % 123.93/18.61 % (947689)Termination reason: Unknown % 123.93/18.61 % (947689)Termination phase: Saturation % 123.93/18.61 % (947689)Time elapsed: 0.361 s % 123.93/18.61 % (947689)Peak memory usage: 113 MB % 123.93/18.61 % (947689)Instructions burned: 543 (million) % 123.93/18.61 % (947694)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 123.93/18.61 % (947694)------------------------------ % 123.93/18.61 % (947694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.93/18.61 % (947694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.93/18.61 % (947694)CaDiCaL version: 2.1.3 % 123.93/18.61 % (947694)Termination reason: Unknown % 123.93/18.61 % (947694)Termination phase: Saturation % 123.93/18.61 % (947694)Time elapsed: 0.192 s % 123.93/18.61 % (947694)Peak memory usage: 113 MB % 123.93/18.61 % (947694)Instructions burned: 542 (million) % 123.93/18.61 % (947691)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 123.93/18.61 % (947691)------------------------------ % 123.93/18.61 % (947691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.93/18.61 % (947691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.93/18.61 % (947691)CaDiCaL version: 2.1.3 % 123.93/18.61 % (947691)Termination reason: Unknown % 123.93/18.61 % (947691)Termination phase: Saturation % 123.93/18.61 % (947691)Time elapsed: 0.360 s % 123.93/18.61 % (947691)Peak memory usage: 114 MB % 123.93/18.61 % (947691)Instructions burned: 541 (million) % 123.93/18.61 % (947700)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=1008215588:i=4840:nm=4:av=off_2887 on theBenchmark for (2887ds/4840Mi) % 123.93/18.61 % (947699)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2462216671:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2887 on theBenchmark for (2887ds/4793Mi) % 123.93/18.61 % (947695)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 123.93/18.61 % (947695)------------------------------ % 123.93/18.61 % (947695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.93/18.61 % (947695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.93/18.61 % (947695)CaDiCaL version: 2.1.3 % 123.93/18.61 % (947695)Termination reason: Unknown % 123.93/18.61 % (947695)Termination phase: Saturation % 123.93/18.61 % (947695)Time elapsed: 0.359 s % 123.93/18.61 % (947695)Peak memory usage: 113 MB % 123.93/18.61 % (947695)Instructions burned: 541 (million) % 123.93/18.61 % (947701)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=3650029457:cts=off:i=5002_2886 on theBenchmark for (2886ds/5002Mi) % 123.93/18.61 % (947700)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 123.93/18.61 % (947700)------------------------------ % 123.93/18.61 % (947700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.93/18.61 % (947700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.93/18.61 % (947700)CaDiCaL version: 2.1.3 % 123.93/18.61 % (947700)Termination reason: Unknown % 123.93/18.61 % (947700)Termination phase: Saturation % 123.93/18.61 % (947700)Time elapsed: 0.195 s % 123.93/18.61 % (947700)Peak memory usage: 113 MB % 123.93/18.61 % (947700)Instructions burned: 540 (million) % 123.93/18.61 % (947704)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=1731186082:i=30479:sd=3:ss=axioms_2885 on theBenchmark for (2885ds/30479Mi) % 123.93/18.61 % (947706)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=1365173731:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2884 on theBenchmark for (2884ds/11035Mi) % 123.93/18.61 % (947706)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 123.93/18.61 % (947699)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 123.93/18.61 % (947699)------------------------------ % 123.93/18.61 % (947699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.93/18.61 % (947699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.77/21.83 % (947699)CaDiCaL version: 2.1.3 % 145.77/21.83 % (947699)Termination reason: Unknown % 145.77/21.83 % (947699)Termination phase: Saturation % 145.77/21.83 % (947699)Time elapsed: 0.360 s % 145.77/21.83 % (947699)Peak memory usage: 113 MB % 145.77/21.83 % (947699)Instructions burned: 539 (million) % 145.77/21.83 % (947701)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 145.77/21.83 % (947701)------------------------------ % 145.77/21.83 % (947701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.77/21.83 % (947701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.77/21.83 % (947701)CaDiCaL version: 2.1.3 % 145.77/21.83 % (947701)Termination reason: Unknown % 145.77/21.83 % (947701)Termination phase: Saturation % 145.77/21.83 % (947701)Time elapsed: 0.359 s % 145.77/21.83 % (947701)Peak memory usage: 113 MB % 145.77/21.83 % (947701)Instructions burned: 540 (million) % 145.77/21.83 % (947706)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 145.77/21.83 % (947706)------------------------------ % 145.77/21.83 % (947706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.77/21.83 % (947706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.77/21.83 % (947706)CaDiCaL version: 2.1.3 % 145.77/21.83 % (947706)Termination reason: Unknown % 145.77/21.83 % (947706)Termination phase: Saturation % 145.77/21.83 % (947706)Time elapsed: 0.193 s % 145.77/21.83 % (947706)Peak memory usage: 114 MB % 145.77/21.83 % (947706)Instructions burned: 541 (million) % 145.77/21.83 % (947709)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=2188044713:i=5835_2882 on theBenchmark for (2882ds/5835Mi) % 145.77/21.83 % (947711)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=1005241215:cts=off:i=19910:ep=RS_2881 on theBenchmark for (2881ds/19910Mi) % 145.77/21.83 % (947710)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=487618090:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2881 on theBenchmark for (2881ds/5890Mi) % 145.77/21.83 % (947704)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 145.77/21.83 % (947704)------------------------------ % 145.77/21.83 % (947704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.77/21.83 % (947704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.77/21.83 % (947704)CaDiCaL version: 2.1.3 % 145.77/21.83 % (947704)Termination reason: Unknown % 145.77/21.83 % (947704)Termination phase: Saturation % 145.77/21.83 % (947704)Time elapsed: 0.360 s % 145.77/21.83 % (947704)Peak memory usage: 113 MB % 145.77/21.83 % (947704)Instructions burned: 539 (million) % 145.77/21.83 % (947715)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=120051329:i=20312:bd=preordered:fsr=off:er=filter_2880 on theBenchmark for (2880ds/20312Mi) % 145.77/21.83 % (947709)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 145.77/21.83 % (947709)------------------------------ % 145.77/21.83 % (947709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.77/21.83 % (947709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.77/21.83 % (947709)CaDiCaL version: 2.1.3 % 145.77/21.83 % (947709)Termination reason: Unknown % 145.77/21.83 % (947709)Termination phase: Saturation % 145.77/21.83 % (947709)Time elapsed: 0.360 s % 145.77/21.83 % (947709)Peak memory usage: 113 MB % 145.77/21.83 % (947709)Instructions burned: 541 (million) % 145.77/21.83 % (947710)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 145.77/21.83 % (947710)------------------------------ % 145.77/21.83 % (947710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.77/21.83 % (947710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.77/21.83 % (947710)CaDiCaL version: 2.1.3 % 145.77/21.83 % (947710)Termination reason: Unknown % 145.77/21.83 % (947710)Termination phase: Saturation % 145.77/21.83 % (947710)Time elapsed: 0.357 s % 145.77/21.83 % (947710)Peak memory usage: 114 MB % 145.77/21.83 % (947710)Instructions burned: 541 (million) % 145.77/21.83 % (947717)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=2121268808:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2877 on theBenchmark for (2877ds/13822Mi) % 145.77/21.83 % (947718)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=1632391241:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2876 on theBenchmark for (2876ds/7144Mi) % 158.73/23.55 % (947715)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 158.73/23.55 % (947715)------------------------------ % 158.73/23.55 % (947715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.73/23.55 % (947715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.73/23.55 % (947715)CaDiCaL version: 2.1.3 % 158.73/23.55 % (947715)Termination reason: Unknown % 158.73/23.55 % (947715)Termination phase: Saturation % 158.73/23.55 % (947715)Time elapsed: 0.360 s % 158.73/23.55 % (947715)Peak memory usage: 113 MB % 158.73/23.55 % (947715)Instructions burned: 541 (million) % 158.73/23.55 % (947721)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=1517163396:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2875 on theBenchmark for (2875ds/15184Mi) % 158.73/23.55 % (947717)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 158.73/23.55 % (947717)------------------------------ % 158.73/23.55 % (947717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.73/23.55 % (947717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.73/23.55 % (947717)CaDiCaL version: 2.1.3 % 158.73/23.55 % (947717)Termination reason: Unknown % 158.73/23.55 % (947717)Termination phase: Saturation % 158.73/23.55 % (947717)Time elapsed: 0.358 s % 158.73/23.55 % (947717)Peak memory usage: 114 MB % 158.73/23.55 % (947717)Instructions burned: 541 (million) % 158.73/23.55 % (947723)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=391916176:i=107375_2872 on theBenchmark for (2872ds/107375Mi) % 158.73/23.55 % (947721)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 158.73/23.55 % (947721)------------------------------ % 158.73/23.55 % (947721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.73/23.55 % (947721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.73/23.55 % (947721)CaDiCaL version: 2.1.3 % 158.73/23.55 % (947721)Termination reason: Unknown % 158.73/23.55 % (947721)Termination phase: Saturation % 158.73/23.55 % (947721)Time elapsed: 0.358 s % 158.73/23.55 % (947721)Peak memory usage: 114 MB % 158.73/23.55 % (947721)Instructions burned: 541 (million) % 158.73/23.55 % (947725)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=3487906654:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2869 on theBenchmark for (2869ds/7958Mi) % 158.73/23.55 % (947723)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 158.73/23.55 % (947723)------------------------------ % 158.73/23.55 % (947723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.73/23.55 % (947723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.73/23.55 % (947723)CaDiCaL version: 2.1.3 % 158.73/23.55 % (947723)Termination reason: Unknown % 158.73/23.55 % (947723)Termination phase: Saturation % 158.73/23.55 % (947723)Time elapsed: 0.361 s % 158.73/23.55 % (947723)Peak memory usage: 113 MB % 158.73/23.55 % (947723)Instructions burned: 541 (million) % 158.73/23.55 % (947766)dis+10_128_sil=16000:nwc=0.7:random_seed=2829462552:i=15999:nm=2:gsp=on_2866 on theBenchmark for (2866ds/15999Mi) % 158.73/23.55 % (947766)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 158.73/23.55 % (947725)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 158.73/23.55 % (947725)------------------------------ % 158.73/23.55 % (947725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 158.73/23.55 % (947725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 158.73/23.55 % (947725)CaDiCaL version: 2.1.3 % 158.73/23.55 % (947725)Termination reason: Unknown % 158.73/23.55 % (947725)Termination phase: Saturation % 158.73/23.55 % (947725)Time elapsed: 0.357 s % 158.73/23.55 % (947725)Peak memory usage: 114 MB % 158.73/23.55 % (947725)Instructions burned: 540 (million) % 158.73/23.55 % (947838)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2522114106:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2864 on theBenchmark for (2864ds/8139Mi) % 158.73/23.55 % (947718)Instruction limit reached! % 158.73/23.55 % (947718)------------------------------ % 158.73/23.55 % (947718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.57/25.34 % (947718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.57/25.34 % (947718)CaDiCaL version: 2.1.3 % 171.57/25.34 % (947718)Termination reason: Instruction limit % 171.57/25.34 % (947718)Termination phase: Saturation % 171.57/25.34 % (947718)Time elapsed: 5.257 s % 171.57/25.34 % (947718)Peak memory usage: 162 MB % 171.57/25.34 % (947718)Instructions burned: 7144 (million) % 171.57/25.34 % (948041)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=833230850:st=4:i=8950:sd=5:ss=axioms_2822 on theBenchmark for (2822ds/8950Mi) % 171.57/25.34 % (948041)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 171.57/25.34 % (948041)------------------------------ % 171.57/25.34 % (948041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.57/25.34 % (948041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.57/25.34 % (948041)CaDiCaL version: 2.1.3 % 171.57/25.34 % (948041)Termination reason: Unknown % 171.57/25.34 % (948041)Termination phase: Saturation % 171.57/25.34 % (948041)Time elapsed: 0.593 s % 171.57/25.34 % (948041)Peak memory usage: 113 MB % 171.57/25.34 % (948041)Instructions burned: 541 (million) % 171.57/25.34 % (948045)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=1678036577:i=9809:ins=10:av=off_2813 on theBenchmark for (2813ds/9809Mi) % 171.57/25.34 % (948045)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 171.57/25.34 % (948045)------------------------------ % 171.57/25.34 % (948045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.57/25.34 % (948045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.57/25.34 % (948045)CaDiCaL version: 2.1.3 % 171.57/25.34 % (948045)Termination reason: Unknown % 171.57/25.34 % (948045)Termination phase: Saturation % 171.57/25.34 % (948045)Time elapsed: 0.594 s % 171.57/25.34 % (948045)Peak memory usage: 114 MB % 171.57/25.34 % (948045)Instructions burned: 541 (million) % 171.57/25.34 % (948049)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=508145810:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2804 on theBenchmark for (2804ds/9885Mi) % 171.57/25.34 % (947711)Instruction limit reached! % 171.57/25.34 % (947711)------------------------------ % 171.57/25.34 % (947711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.57/25.34 % (947711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.57/25.34 % (947711)CaDiCaL version: 2.1.3 % 171.57/25.34 % (947711)Termination reason: Instruction limit % 171.57/25.34 % (947711)Termination phase: Saturation % 171.57/25.34 % (947711)Time elapsed: 8.448 s % 171.57/25.34 % (947711)Peak memory usage: 196 MB % 171.57/25.34 % (947711)Instructions burned: 19911 (million) % 171.57/25.34 % (948049)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 171.57/25.34 % (948049)------------------------------ % 171.57/25.34 % (948049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.57/25.34 % (948049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.57/25.34 % (948049)CaDiCaL version: 2.1.3 % 171.57/25.34 % (948049)Termination reason: Unknown % 171.57/25.34 % (948049)Termination phase: Saturation % 171.57/25.34 % (948049)Time elapsed: 0.577 s % 171.57/25.34 % (948049)Peak memory usage: 114 MB % 171.57/25.34 % (948049)Instructions burned: 541 (million) % 171.57/25.34 % (948062)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1252038783:cond=fast:i=32078:fgj=on:av=off_2795 on theBenchmark for (2795ds/32078Mi) % 171.57/25.34 % (948064)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=35330535:i=11101:bd=all:ss=axioms:sgt=8_2795 on theBenchmark for (2795ds/11101Mi) % 171.57/25.34 % (947838)Instruction limit reached! % 171.57/25.34 % (947838)------------------------------ % 171.57/25.34 % (947838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.57/25.34 % (947838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.57/25.34 % (947838)CaDiCaL version: 2.1.3 % 171.57/25.34 % (947838)Termination reason: Instruction limit % 171.57/25.34 % (947838)Termination phase: Saturation % 171.57/25.34 % (947838)Time elapsed: 7.204 s % 171.57/25.34 % (947838)Peak memory usage: 140 MB % 171.57/25.34 % (947838)Instructions burned: 8140 (million) % 171.57/25.34 % (948062)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 212.55/31.11 % (948062)------------------------------ % 212.55/31.11 % (948062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.55/31.11 % (948062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.55/31.11 % (948062)CaDiCaL version: 2.1.3 % 212.55/31.11 % (948062)Termination reason: Unknown % 212.55/31.11 % (948062)Termination phase: Saturation % 212.55/31.11 % (948062)Time elapsed: 0.311 s % 212.55/31.11 % (948062)Peak memory usage: 113 MB % 212.55/31.11 % (948062)Instructions burned: 540 (million) % 212.55/31.11 % (948068)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3119450848:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2790 on theBenchmark for (2790ds/13528Mi) % 212.55/31.11 % (948067)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3863709095:cond=on:i=13220:s2at=3:aac=none:fsd=on_2790 on theBenchmark for (2790ds/13220Mi) % 212.55/31.11 % (948068)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 212.55/31.11 % (948068)------------------------------ % 212.55/31.11 % (948068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.55/31.11 % (948068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.55/31.11 % (948068)CaDiCaL version: 2.1.3 % 212.55/31.11 % (948068)Termination reason: Unknown % 212.55/31.11 % (948068)Termination phase: Saturation % 212.55/31.11 % (948068)Time elapsed: 0.308 s % 212.55/31.11 % (948068)Peak memory usage: 113 MB % 212.55/31.11 % (948068)Instructions burned: 541 (million) % 212.55/31.11 % (948071)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=300582818:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2785 on theBenchmark for (2785ds/14854Mi) % 212.55/31.11 % (948067)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 212.55/31.11 % (948067)------------------------------ % 212.55/31.11 % (948067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.55/31.11 % (948067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.55/31.11 % (948067)CaDiCaL version: 2.1.3 % 212.55/31.11 % (948067)Termination reason: Unknown % 212.55/31.11 % (948067)Termination phase: Saturation % 212.55/31.11 % (948067)Time elapsed: 0.598 s % 212.55/31.11 % (948067)Peak memory usage: 114 MB % 212.55/31.11 % (948067)Instructions burned: 541 (million) % 212.55/31.11 % (948071)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 212.55/31.11 % (948071)------------------------------ % 212.55/31.11 % (948071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.55/31.11 % (948071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.55/31.11 % (948071)CaDiCaL version: 2.1.3 % 212.55/31.11 % (948071)Termination reason: Unknown % 212.55/31.11 % (948071)Termination phase: Saturation % 212.55/31.11 % (948071)Time elapsed: 0.315 s % 212.55/31.11 % (948071)Peak memory usage: 114 MB % 212.55/31.11 % (948071)Instructions burned: 553 (million) % 212.55/31.11 % (948073)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1988917547:i=14974:ss=axioms:sgt=16_2782 on theBenchmark for (2782ds/14974Mi) % 212.55/31.11 % (948074)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=3359539933:i=33081:aac=none:fgj=on:bd=all:fsr=off_2779 on theBenchmark for (2779ds/33081Mi) % 212.55/31.11 % (948074)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 212.55/31.11 % (948074)------------------------------ % 212.55/31.11 % (948074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.55/31.11 % (948074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.55/31.11 % (948074)CaDiCaL version: 2.1.3 % 212.55/31.11 % (948074)Termination reason: Unknown % 212.55/31.11 % (948074)Termination phase: Saturation % 212.55/31.11 % (948074)Time elapsed: 0.307 s % 212.55/31.11 % (948074)Peak memory usage: 114 MB % 212.55/31.11 % (948074)Instructions burned: 541 (million) % 212.55/31.11 % (948073)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 212.55/31.11 % (948073)------------------------------ % 212.55/31.11 % (948073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.66/34.66 % (948073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.66/34.66 % (948073)CaDiCaL version: 2.1.3 % 237.66/34.66 % (948073)Termination reason: Unknown % 237.66/34.66 % (948073)Termination phase: Saturation % 237.66/34.66 % (948073)Time elapsed: 0.595 s % 237.66/34.66 % (948073)Peak memory usage: 113 MB % 237.66/34.66 % (948073)Instructions burned: 542 (million) % 237.66/34.66 % (948077)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=481151858:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2774 on theBenchmark for (2774ds/50856Mi) % 237.66/34.66 % (948078)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=835831395:i=69865_2773 on theBenchmark for (2773ds/69865Mi) % 237.66/34.66 % (948077)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.66/34.66 % (948077)------------------------------ % 237.66/34.66 % (948077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.66/34.66 % (948077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.66/34.66 % (948077)CaDiCaL version: 2.1.3 % 237.66/34.66 % (948077)Termination reason: Unknown % 237.66/34.66 % (948077)Termination phase: Saturation % 237.66/34.66 % (948077)Time elapsed: 0.308 s % 237.66/34.66 % (948077)Peak memory usage: 113 MB % 237.66/34.66 % (948077)Instructions burned: 541 (million) % 237.66/34.66 % (948081)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=3138191184:cond=fast:i=17802:gtgl=3:gtg=all_2769 on theBenchmark for (2769ds/17802Mi) % 237.66/34.66 % (948078)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.66/34.66 % (948078)------------------------------ % 237.66/34.66 % (948078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.66/34.66 % (948078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.66/34.66 % (948078)CaDiCaL version: 2.1.3 % 237.66/34.66 % (948078)Termination reason: Unknown % 237.66/34.66 % (948078)Termination phase: Saturation % 237.66/34.66 % (948078)Time elapsed: 0.595 s % 237.66/34.66 % (948078)Peak memory usage: 113 MB % 237.66/34.66 % (948078)Instructions burned: 541 (million) % 237.66/34.66 % (947620)Instruction limit reached! % 237.66/34.66 % (947620)------------------------------ % 237.66/34.66 % (947620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.66/34.66 % (947620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.66/34.66 % (947620)CaDiCaL version: 2.1.3 % 237.66/34.66 % (947620)Termination reason: Instruction limit % 237.66/34.66 % (947620)Termination phase: Saturation % 237.66/34.66 % (947620)Time elapsed: 17.942 s % 237.66/34.66 % (947620)Peak memory usage: 264 MB % 237.66/34.66 % (947620)Instructions burned: 26473 (million) % 237.66/34.66 % (948081)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.66/34.66 % (948081)------------------------------ % 237.66/34.66 % (948081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.66/34.66 % (948081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.66/34.66 % (948081)CaDiCaL version: 2.1.3 % 237.66/34.66 % (948081)Termination reason: Unknown % 237.66/34.66 % (948081)Termination phase: Saturation % 237.66/34.66 % (948081)Time elapsed: 0.308 s % 237.66/34.66 % (948081)Peak memory usage: 113 MB % 237.66/34.66 % (948081)Instructions burned: 544 (million) % 237.66/34.66 % (948084)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 237.66/34.66 % (948084)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=3131918276:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2763 on theBenchmark for (2763ds/21161Mi) % 237.66/34.66 % (948083)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=2306135690:i=96644_2764 on theBenchmark for (2764ds/96644Mi) % 237.66/34.66 % (948085)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=3085784637:i=22761:gtg=all:ss=axioms:fsd=on_2763 on theBenchmark for (2763ds/22761Mi) % 237.66/34.66 % (948085)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.66/34.66 % (948085)------------------------------ % 237.66/34.66 % (948085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.31/36.40 % (948085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.31/36.40 % (948085)CaDiCaL version: 2.1.3 % 250.31/36.40 % (948085)Termination reason: Unknown % 250.31/36.40 % (948085)Termination phase: Saturation % 250.31/36.40 % (948085)Time elapsed: 0.566 s % 250.31/36.40 % (948085)Peak memory usage: 113 MB % 250.31/36.40 % (948085)Instructions burned: 542 (million) % 250.31/36.40 % (948091)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=3548690579:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2755 on theBenchmark for (2755ds/23713Mi) % 250.31/36.40 % (947766)Instruction limit reached! % 250.31/36.40 % (947766)------------------------------ % 250.31/36.40 % (947766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.31/36.40 % (947766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.31/36.40 % (947766)CaDiCaL version: 2.1.3 % 250.31/36.40 % (947766)Termination reason: Instruction limit % 250.31/36.40 % (947766)Termination phase: Saturation % 250.31/36.40 % (947766)Time elapsed: 13.452 s % 250.31/36.40 % (947766)Peak memory usage: 199 MB % 250.31/36.40 % (947766)Instructions burned: 15999 (million) % 250.31/36.40 % (948093)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=196663910:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2730 on theBenchmark for (2730ds/26509Mi) % 250.31/36.40 % (948093)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 250.31/36.40 % (948093)------------------------------ % 250.31/36.40 % (948093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.31/36.40 % (948093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.31/36.40 % (948093)CaDiCaL version: 2.1.3 % 250.31/36.40 % (948093)Termination reason: Unknown % 250.31/36.40 % (948093)Termination phase: Saturation % 250.31/36.40 % (948093)Time elapsed: 0.597 s % 250.31/36.40 % (948093)Peak memory usage: 113 MB % 250.31/36.40 % (948093)Instructions burned: 541 (million) % 250.31/36.40 % (948098)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=3168584785:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2721 on theBenchmark for (2721ds/28957Mi) % 250.31/36.40 % (947595)Instruction limit reached! % 250.31/36.40 % (947595)------------------------------ % 250.31/36.40 % (947595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.31/36.40 % (947595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.31/36.40 % (947595)CaDiCaL version: 2.1.3 % 250.31/36.40 % (947595)Termination reason: Instruction limit % 250.31/36.40 % (947595)Termination phase: Saturation % 250.31/36.40 % (947595)Time elapsed: 24.180 s % 250.31/36.40 % (947595)Peak memory usage: 274 MB % 250.31/36.40 % (947595)Instructions burned: 33334 (million) % 250.31/36.40 % (948103)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=924788111:i=29246:s2at=-1:kws=inv_arity:ins=10_2715 on theBenchmark for (2715ds/29246Mi) % 250.31/36.40 % (948103)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 250.31/36.40 % (948103)------------------------------ % 250.31/36.40 % (948103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.31/36.40 % (948103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.31/36.40 % (948103)CaDiCaL version: 2.1.3 % 250.31/36.40 % (948103)Termination reason: Unknown % 250.31/36.40 % (948103)Termination phase: Saturation % 250.31/36.40 % (948103)Time elapsed: 0.593 s % 250.31/36.40 % (948103)Peak memory usage: 114 MB % 250.31/36.40 % (948103)Instructions burned: 541 (million) % 250.31/36.40 % (948107)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=2727552419:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2706 on theBenchmark for (2706ds/30082Mi) % 250.31/36.40 % (948107)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 250.31/36.40 % (948107)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 250.31/36.40 % (948107)------------------------------ % 250.31/36.40 % (948107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.31/36.40 % (948107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.56/37.84 % (948107)CaDiCaL version: 2.1.3 % 259.56/37.84 % (948107)Termination reason: Unknown % 259.56/37.84 % (948107)Termination phase: Saturation % 259.56/37.84 % (948107)Time elapsed: 0.600 s % 259.56/37.84 % (948107)Peak memory usage: 114 MB % 259.56/37.84 % (948107)Instructions burned: 541 (million) % 259.56/37.84 % (948109)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=434278608:i=32262:bd=preordered_2697 on theBenchmark for (2697ds/32262Mi) % 259.56/37.84 % (948109)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 259.56/37.84 % (948109)------------------------------ % 259.56/37.84 % (948109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.56/37.84 % (948109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.56/37.84 % (948109)CaDiCaL version: 2.1.3 % 259.56/37.84 % (948109)Termination reason: Unknown % 259.56/37.84 % (948109)Termination phase: Saturation % 259.56/37.84 % (948109)Time elapsed: 0.601 s % 259.56/37.84 % (948109)Peak memory usage: 113 MB % 259.56/37.84 % (948109)Instructions burned: 541 (million) % 259.56/37.84 % (948111)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=4144750157:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2688 on theBenchmark for (2688ds/32870Mi) % 259.56/37.84 % (948064)Instruction limit reached! % 259.56/37.84 % (948064)------------------------------ % 259.56/37.84 % (948064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.56/37.84 % (948064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.56/37.84 % (948064)CaDiCaL version: 2.1.3 % 259.56/37.84 % (948064)Termination reason: Instruction limit % 259.56/37.84 % (948064)Termination phase: Saturation % 259.56/37.84 % (948064)Time elapsed: 11.254 s % 259.56/37.84 % (948064)Peak memory usage: 223 MB % 259.56/37.84 % (948064)Instructions burned: 11101 (million) % 259.56/37.84 % (948111)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 259.56/37.84 % (948111)------------------------------ % 259.56/37.84 % (948111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.56/37.84 % (948111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.56/37.84 % (948111)CaDiCaL version: 2.1.3 % 259.56/37.84 % (948111)Termination reason: Unknown % 259.56/37.84 % (948111)Termination phase: Saturation % 259.56/37.84 % (948111)Time elapsed: 0.601 s % 259.56/37.84 % (948111)Peak memory usage: 114 MB % 259.56/37.84 % (948111)Instructions burned: 542 (million) % 259.56/37.84 % (948113)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=3547266407:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2679 on theBenchmark for (2679ds/33295Mi) % 259.56/37.84 % (948114)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=1819243785:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2679 on theBenchmark for (2679ds/36826Mi) % 259.56/37.84 % (948113)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 259.56/37.84 % (948113)------------------------------ % 259.56/37.84 % (948113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.56/37.84 % (948113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.56/37.84 % (948113)CaDiCaL version: 2.1.3 % 259.56/37.84 % (948113)Termination reason: Unknown % 259.56/37.84 % (948113)Termination phase: Saturation % 259.56/37.84 % (948113)Time elapsed: 0.599 s % 259.56/37.84 % (948113)Peak memory usage: 113 MB % 259.56/37.84 % (948113)Instructions burned: 541 (million) % 259.56/37.84 % (948117)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=124225961:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2671 on theBenchmark for (2671ds/92981Mi) % 259.56/37.84 % (948084)Instruction limit reached! % 259.56/37.84 % (948084)------------------------------ % 259.56/37.84 % (948084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.56/37.84 % (948084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.56/37.84 % (948084)CaDiCaL version: 2.1.3 % 259.56/37.84 % (948084)Termination reason: Instruction limit % 259.56/37.84 % (948084)Termination phase: Saturation % 259.56/37.84 % (948084)Time elapsed: 9.777 s % 259.56/37.84 % (948084)Peak memory usage: 248 MB % 259.56/37.84 % (948084)Instructions burned: 21162 (million) % 259.56/37.84 % (948117)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 271.27/39.43 % (948117)------------------------------ % 271.27/39.43 % (948117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.27/39.43 % (948117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.27/39.43 % (948117)CaDiCaL version: 2.1.3 % 271.27/39.43 % (948117)Termination reason: Unknown % 271.27/39.43 % (948117)Termination phase: Saturation % 271.27/39.43 % (948117)Time elapsed: 0.597 s % 271.27/39.43 % (948117)Peak memory usage: 114 MB % 271.27/39.43 % (948117)Instructions burned: 541 (million) % 271.27/39.43 % (948119)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=667324299:s2pl=on:i=49423_2663 on theBenchmark for (2663ds/49423Mi) % 271.27/39.43 % (948120)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=4182295138:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2662 on theBenchmark for (2662ds/57299Mi) % 271.27/39.43 % (948119)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 271.27/39.43 % (948119)------------------------------ % 271.27/39.43 % (948119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.27/39.43 % (948119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.27/39.43 % (948119)CaDiCaL version: 2.1.3 % 271.27/39.43 % (948119)Termination reason: Unknown % 271.27/39.43 % (948119)Termination phase: Saturation % 271.27/39.43 % (948119)Time elapsed: 0.323 s % 271.27/39.43 % (948119)Peak memory usage: 114 MB % 271.27/39.43 % (948119)Instructions burned: 543 (million) % 271.27/39.43 % (948123)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=3629867788:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2658 on theBenchmark for (2658ds/127679Mi) % 271.27/39.43 % (948120)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 271.27/39.43 % (948120)------------------------------ % 271.27/39.43 % (948120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.27/39.43 % (948120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.27/39.43 % (948120)CaDiCaL version: 2.1.3 % 271.27/39.43 % (948120)Termination reason: Unknown % 271.27/39.43 % (948120)Termination phase: Saturation % 271.27/39.43 % (948120)Time elapsed: 0.600 s % 271.27/39.43 % (948120)Peak memory usage: 113 MB % 271.27/39.43 % (948120)Instructions burned: 541 (million) % 271.27/39.43 % (948123)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 271.27/39.43 % (948123)------------------------------ % 271.27/39.43 % (948123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.27/39.43 % (948123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.27/39.43 % (948123)CaDiCaL version: 2.1.3 % 271.27/39.43 % (948123)Termination reason: Unknown % 271.27/39.43 % (948123)Termination phase: Saturation % 271.27/39.43 % (948123)Time elapsed: 0.321 s % 271.27/39.43 % (948123)Peak memory usage: 114 MB % 271.27/39.43 % (948123)Instructions burned: 542 (million) % 271.27/39.43 % (948126)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=3153781033:i=100512:doe=on:fgj=on:bd=all:fsd=on_2652 on theBenchmark for (2652ds/100512Mi) % 271.27/39.43 % (948125)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=437517520:i=69402:add=on:aac=none:fsr=off_2653 on theBenchmark for (2653ds/69402Mi) % 271.27/39.43 % (948126)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 271.27/39.43 % (948126)------------------------------ % 271.27/39.43 % (948126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 271.27/39.43 % (948126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 271.27/39.43 % (948126)CaDiCaL version: 2.1.3 % 271.27/39.43 % (948126)Termination reason: Unknown % 271.27/39.43 % (948126)Termination phase: Saturation % 271.27/39.43 % (948126)Time elapsed: 0.323 s % 271.27/39.43 % (948126)Peak memory usage: 113 MB % 271.27/39.43 % (948126)Instructions burned: 541 (million) % 271.27/39.43 % (948129)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=932125685:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2647 on theBenchmark for (2647ds/138761Mi) % 283.64/41.11 % (948125)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 283.64/41.11 % (948125)------------------------------ % 283.64/41.11 % (948125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.64/41.11 % (948125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.64/41.11 % (948125)CaDiCaL version: 2.1.3 % 283.64/41.11 % (948125)Termination reason: Unknown % 283.64/41.11 % (948125)Termination phase: Saturation % 283.64/41.11 % (948125)Time elapsed: 0.598 s % 283.64/41.11 % (948125)Peak memory usage: 113 MB % 283.64/41.11 % (948125)Instructions burned: 541 (million) % 283.64/41.11 % (948129)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 283.64/41.11 % (948129)------------------------------ % 283.64/41.11 % (948129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.64/41.11 % (948129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.64/41.11 % (948129)CaDiCaL version: 2.1.3 % 283.64/41.11 % (948129)Termination reason: Unknown % 283.64/41.11 % (948129)Termination phase: Saturation % 283.64/41.11 % (948129)Time elapsed: 0.323 s % 283.64/41.11 % (948129)Peak memory usage: 114 MB % 283.64/41.11 % (948129)Instructions burned: 541 (million) % 283.64/41.11 % (948131)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=3925097644:i=282386:rtra=on_2644 on theBenchmark for (2644ds/282386Mi) % 283.64/41.11 % (948132)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=510127541:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2641 on theBenchmark for (2641ds/269354Mi) % 283.64/41.11 % (948132)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 283.64/41.11 % (948132)------------------------------ % 283.64/41.11 % (948132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.64/41.11 % (948132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.64/41.11 % (948132)CaDiCaL version: 2.1.3 % 283.64/41.11 % (948132)Termination reason: Unknown % 283.64/41.11 % (948132)Termination phase: Saturation % 283.64/41.11 % (948132)Time elapsed: 0.323 s % 283.64/41.11 % (948132)Peak memory usage: 114 MB % 283.64/41.11 % (948132)Instructions burned: 544 (million) % 283.64/41.11 % (948131)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 283.64/41.11 % (948131)------------------------------ % 283.64/41.11 % (948131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.64/41.11 % (948131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.64/41.11 % (948131)CaDiCaL version: 2.1.3 % 283.64/41.11 % (948131)Termination reason: Unknown % 283.64/41.11 % (948131)Termination phase: Saturation % 283.64/41.11 % (948131)Time elapsed: 0.598 s % 283.64/41.11 % (948131)Peak memory usage: 114 MB % 283.64/41.11 % (948131)Instructions burned: 541 (million) % 283.64/41.11 % (948137)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=2124225130:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2636 on theBenchmark for (2636ds/283390Mi) % 283.64/41.11 % (948137)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 283.64/41.11 % (948138)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=1868867812:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2635 on theBenchmark for (2635ds/218Mi) % 283.64/41.11 % (948138)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 283.64/41.11 % (948137)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 283.64/41.11 % (948137)------------------------------ % 283.64/41.11 % (948137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 283.64/41.11 % (948137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 283.64/41.11 % (948137)CaDiCaL version: 2.1.3 % 283.64/41.11 % (948137)Termination reason: Unknown % 283.64/41.11 % (948137)Termination phase: Saturation % 283.64/41.11 % (948137)Time elapsed: 0.321 s % 283.64/41.11 % (948137)Peak memory usage: 114 MB % 283.64/41.11 % (948137)Instructions burned: 542 (million) % 283.64/41.11 % (948138)Instruction limit reached! % 283.64/41.11 % (948138)----------------------------Terminated %------------------------------------------------------------------------------