%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM959_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:17:42 PM UTC 2026 % Result : Timeout 299.12s 43.09s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM959_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.38 % Computer : n002.cluster.edu % 0.12/0.38 % Model : x86_64 x86_64 % 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.38 % Memory : 8046.5625MB % 0.12/0.38 % OS : Linux 6.8.0-71-generic % 0.12/0.38 % CPULimit : 300 % 0.12/0.38 % WCLimit : 300 % 0.12/0.38 % DateTime : Sun Sep 27 21:50:37 UTC 2026 % 0.12/0.38 % CPUTime : % 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.42 Running first-order theorem proving % 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.34/2.26 % (3918468)Detected formulas, will run a generic FOF schedule. % 9.34/2.26 % (3918528)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=834720043:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 9.34/2.26 % (3918533)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2358167968:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 9.34/2.26 % (3918530)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=639898584:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 9.34/2.26 % (3918531)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2161686873:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 9.34/2.26 % (3918529)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=3995728579:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 9.34/2.26 % (3918531)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 9.34/2.26 % (3918530)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 9.34/2.26 % (3918534)dis-21_1_sil=8000:lcm=predicate:random_seed=2513643445:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 9.34/2.26 % (3918532)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=800756178:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 9.34/2.26 % (3918531)Instruction limit reached! % 9.34/2.26 % (3918531)------------------------------ % 9.34/2.26 % (3918531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.34/2.26 % (3918531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/2.26 % (3918531)CaDiCaL version: 2.1.3 % 9.34/2.26 % (3918531)Termination reason: Instruction limit % 9.34/2.26 % (3918531)Termination phase: Saturation % 9.34/2.26 % (3918531)Time elapsed: 0.091 s % 9.34/2.26 % (3918531)Peak memory usage: 89 MB % 9.34/2.26 % (3918531)Instructions burned: 109 (million) % 9.34/2.26 % (3918533)Instruction limit reached! % 9.34/2.26 % (3918533)------------------------------ % 9.34/2.26 % (3918533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.34/2.26 % (3918533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/2.26 % (3918533)CaDiCaL version: 2.1.3 % 9.34/2.26 % (3918533)Termination reason: Instruction limit % 9.34/2.26 % (3918533)Termination phase: Saturation % 9.34/2.26 % (3918533)Time elapsed: 0.155 s % 9.34/2.26 % (3918533)Peak memory usage: 89 MB % 9.34/2.26 % (3918533)Instructions burned: 139 (million) % 9.34/2.26 % (3918534)Instruction limit reached! % 9.34/2.26 % (3918534)------------------------------ % 9.34/2.26 % (3918534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.34/2.26 % (3918534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/2.26 % (3918534)CaDiCaL version: 2.1.3 % 9.34/2.26 % (3918534)Termination reason: Instruction limit % 9.34/2.26 % (3918534)Termination phase: Saturation % 9.34/2.26 % (3918534)Time elapsed: 0.129 s % 9.34/2.26 % (3918534)Peak memory usage: 89 MB % 9.34/2.26 % (3918534)Instructions burned: 129 (million) % 9.34/2.26 % (3918532)Instruction limit reached! % 9.34/2.26 % (3918532)------------------------------ % 9.34/2.26 % (3918532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.34/2.26 % (3918532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/2.26 % (3918532)CaDiCaL version: 2.1.3 % 9.34/2.26 % (3918532)Termination reason: Instruction limit % 9.34/2.26 % (3918532)Termination phase: Saturation % 9.34/2.26 % (3918532)Time elapsed: 0.109 s % 9.34/2.26 % (3918532)Peak memory usage: 88 MB % 9.34/2.26 % (3918532)Instructions burned: 119 (million) % 9.34/2.26 % (3918528)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.34/2.26 % (3918528)------------------------------ % 9.34/2.26 % (3918528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.34/2.26 % (3918528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.34/2.26 % (3918528)CaDiCaL version: 2.1.3 % 9.34/2.26 % (3918528)Termination reason: Unknown % 9.34/2.26 % (3918528)Termination phase: Saturation % 10.68/2.67 % (3918528)Time elapsed: 0.302 s % 10.68/2.67 % (3918528)Peak memory usage: 114 MB % 10.68/2.67 % (3918528)Instructions burned: 542 (million) % 10.68/2.67 % (3918584)lrs+10_1_sil=8000:sp=occurrence:random_seed=3501970903:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 10.68/2.67 % (3918591)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=226585795:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 10.68/2.67 % (3918589)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1362287572:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 10.68/2.67 % (3918588)lrs+10_1_sil=32000:urr=on:br=off:random_seed=146071117:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 10.68/2.67 % (3918593)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=345949571:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 10.68/2.67 % (3918588)Instruction limit reached! % 10.68/2.67 % (3918588)------------------------------ % 10.68/2.67 % (3918588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.68/2.67 % (3918588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.68/2.67 % (3918588)CaDiCaL version: 2.1.3 % 10.68/2.67 % (3918588)Termination reason: Instruction limit % 10.68/2.67 % (3918588)Termination phase: Saturation % 10.68/2.67 % (3918588)Time elapsed: 0.162 s % 10.68/2.67 % (3918588)Peak memory usage: 90 MB % 10.68/2.67 % (3918588)Instructions burned: 157 (million) % 10.68/2.67 % (3918593)Refutation not found, incomplete strategy % 10.68/2.67 % (3918593)------------------------------ % 10.68/2.67 % (3918593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.68/2.67 % (3918593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.68/2.67 % (3918593)CaDiCaL version: 2.1.3 % 10.68/2.67 % (3918593)Termination reason: Refutation not found, incomplete strategy % 10.68/2.67 % (3918593)Time elapsed: 0.014 s % 10.68/2.67 % (3918593)Peak memory usage: 89 MB % 10.68/2.67 % (3918593)Instructions burned: 16 (million) % 10.68/2.67 % (3918529)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.68/2.67 % (3918529)------------------------------ % 10.68/2.67 % (3918529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.68/2.67 % (3918529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.68/2.67 % (3918529)CaDiCaL version: 2.1.3 % 10.68/2.67 % (3918529)Termination reason: Unknown % 10.68/2.67 % (3918529)Termination phase: Saturation % 10.68/2.67 % (3918529)Time elapsed: 0.582 s % 10.68/2.67 % (3918529)Peak memory usage: 113 MB % 10.68/2.67 % (3918529)Instructions burned: 545 (million) % 10.68/2.67 % (3918591)Instruction limit reached! % 10.68/2.67 % (3918591)------------------------------ % 10.68/2.67 % (3918591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.68/2.67 % (3918591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.68/2.67 % (3918591)CaDiCaL version: 2.1.3 % 10.68/2.67 % (3918591)Termination reason: Instruction limit % 10.68/2.67 % (3918591)Termination phase: Saturation % 10.68/2.67 % (3918591)Time elapsed: 0.224 s % 10.68/2.67 % (3918591)Peak memory usage: 91 MB % 10.68/2.67 % (3918591)Instructions burned: 248 (million) % 10.68/2.67 % (3918530)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.68/2.67 % (3918530)------------------------------ % 10.68/2.67 % (3918530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.68/2.67 % (3918530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.68/2.67 % (3918530)CaDiCaL version: 2.1.3 % 10.68/2.67 % (3918530)Termination reason: Unknown % 10.68/2.67 % (3918530)Termination phase: Saturation % 10.68/2.67 % (3918530)Time elapsed: 0.594 s % 10.68/2.67 % (3918530)Peak memory usage: 113 MB % 10.68/2.67 % (3918530)Instructions burned: 541 (million) % 10.68/2.67 % (3918584)Instruction limit reached! % 10.68/2.67 % (3918584)------------------------------ % 10.68/2.67 % (3918584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.68/2.67 % (3918584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.68/2.67 % (3918584)CaDiCaL version: 2.1.3 % 10.68/2.67 % (3918584)Termination reason: Instruction limit % 10.68/2.67 % (3918584)Termination phase: Saturation % 10.68/2.67 % (3918584)Time elapsed: 0.293 s % 10.68/2.67 % (3918584)Peak memory usage: 91 MB % 10.68/2.67 % (3918584)Instructions burned: 285 (million) % 10.68/2.67 % (3918589)Instruction limit reached! % 15.72/3.10 % (3918589)------------------------------ % 15.72/3.10 % (3918589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.72/3.10 % (3918589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.72/3.10 % (3918589)CaDiCaL version: 2.1.3 % 15.72/3.10 % (3918589)Termination reason: Instruction limit % 15.72/3.10 % (3918589)Termination phase: Saturation % 15.72/3.10 % (3918589)Time elapsed: 0.228 s % 15.72/3.10 % (3918589)Peak memory usage: 91 MB % 15.72/3.10 % (3918589)Instructions burned: 325 (million) % 15.72/3.10 % (3918606)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3694178447:i=2350_2992 on theBenchmark for (2992ds/2350Mi) % 15.72/3.10 % (3918613)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3786543822:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 15.72/3.10 % (3918616)lrs+10_1_sil=8000:sp=occurrence:random_seed=4036740459:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi) % 15.72/3.10 % (3918612)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1954443438:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 15.72/3.10 % (3918615)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3669764845:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 15.72/3.10 % (3918617)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3991100094:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi) % 15.72/3.10 % (3918617)Refutation not found, incomplete strategy % 15.72/3.10 % (3918617)------------------------------ % 15.72/3.10 % (3918617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.72/3.10 % (3918617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.72/3.10 % (3918617)CaDiCaL version: 2.1.3 % 15.72/3.10 % (3918617)Termination reason: Refutation not found, incomplete strategy % 15.72/3.10 % (3918617)Time elapsed: 0.012 s % 15.72/3.10 % (3918617)Peak memory usage: 88 MB % 15.72/3.10 % (3918617)Instructions burned: 11 (million) % 15.72/3.10 % (3918613)Instruction limit reached! % 15.72/3.10 % (3918613)------------------------------ % 15.72/3.10 % (3918613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.72/3.10 % (3918613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.72/3.10 % (3918613)CaDiCaL version: 2.1.3 % 15.72/3.10 % (3918613)Termination reason: Instruction limit % 15.72/3.10 % (3918613)Termination phase: Saturation % 15.72/3.10 % (3918613)Time elapsed: 0.103 s % 15.72/3.10 % (3918613)Peak memory usage: 88 MB % 15.72/3.10 % (3918613)Instructions burned: 128 (million) % 15.72/3.10 % (3918612)Instruction limit reached! % 15.72/3.10 % (3918612)------------------------------ % 15.72/3.10 % (3918612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.72/3.10 % (3918612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.72/3.10 % (3918612)CaDiCaL version: 2.1.3 % 15.72/3.10 % (3918612)Termination reason: Instruction limit % 15.72/3.10 % (3918612)Termination phase: Saturation % 15.72/3.10 % (3918612)Time elapsed: 0.117 s % 15.72/3.10 % (3918612)Peak memory usage: 89 MB % 15.72/3.10 % (3918612)Instructions burned: 113 (million) % 15.72/3.10 % (3918593)------------------------------ % 15.72/3.10 % (3918593)------------------------------ % 15.72/3.10 % (3918615)Instruction limit reached! % 15.72/3.10 % (3918615)------------------------------ % 15.72/3.10 % (3918615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.72/3.10 % (3918615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.72/3.10 % (3918615)CaDiCaL version: 2.1.3 % 15.72/3.10 % (3918615)Termination reason: Instruction limit % 15.72/3.10 % (3918615)Termination phase: Saturation % 15.72/3.10 % (3918615)Time elapsed: 0.099 s % 15.72/3.10 % (3918615)Peak memory usage: 88 MB % 15.72/3.10 % (3918615)Instructions burned: 115 (million) % 15.72/3.10 % (3918629)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2199853288:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 15.72/3.10 % (3918617)------------------------------ % 15.72/3.10 % (3918617)------------------------------ % 15.72/3.10 % (3918630)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2894258263:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 15.72/3.10 % (3918632)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3595938027:st=3:i=13193:sd=3:ss=axioms_2988 on theBenchmark for (2988ds/13193Mi) % 17.82/3.61 % (3918631)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1051705677:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi) % 17.82/3.61 % (3918631)Refutation not found, incomplete strategy % 17.82/3.61 % (3918631)------------------------------ % 17.82/3.61 % (3918631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.61 % (3918631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.61 % (3918631)CaDiCaL version: 2.1.3 % 17.82/3.61 % (3918631)Termination reason: Refutation not found, incomplete strategy % 17.82/3.61 % (3918631)Time elapsed: 0.012 s % 17.82/3.61 % (3918631)Peak memory usage: 88 MB % 17.82/3.61 % (3918631)Instructions burned: 11 (million) % 17.82/3.61 % (3918616)Instruction limit reached! % 17.82/3.61 % (3918616)------------------------------ % 17.82/3.61 % (3918616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.61 % (3918616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.61 % (3918616)CaDiCaL version: 2.1.3 % 17.82/3.61 % (3918616)Termination reason: Instruction limit % 17.82/3.61 % (3918616)Termination phase: Saturation % 17.82/3.61 % (3918616)Time elapsed: 0.482 s % 17.82/3.61 % (3918616)Peak memory usage: 95 MB % 17.82/3.61 % (3918616)Instructions burned: 907 (million) % 17.82/3.61 % (3918630)Instruction limit reached! % 17.82/3.61 % (3918630)------------------------------ % 17.82/3.61 % (3918630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.61 % (3918630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.61 % (3918630)CaDiCaL version: 2.1.3 % 17.82/3.61 % (3918630)Termination reason: Instruction limit % 17.82/3.61 % (3918630)Termination phase: Saturation % 17.82/3.61 % (3918630)Time elapsed: 0.139 s % 17.82/3.61 % (3918630)Peak memory usage: 90 MB % 17.82/3.61 % (3918630)Instructions burned: 135 (million) % 17.82/3.61 % (3918606)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.82/3.61 % (3918606)------------------------------ % 17.82/3.61 % (3918606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.61 % (3918606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.61 % (3918606)CaDiCaL version: 2.1.3 % 17.82/3.61 % (3918606)Termination reason: Unknown % 17.82/3.61 % (3918606)Termination phase: Saturation % 17.82/3.61 % (3918606)Time elapsed: 0.603 s % 17.82/3.61 % (3918606)Peak memory usage: 113 MB % 17.82/3.61 % (3918606)Instructions burned: 542 (million) % 17.82/3.61 % (3918640)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=4060485394:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi) % 17.82/3.61 % (3918640)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 17.82/3.61 % (3918642)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2513485913:i=134:gtgl=5:slsql=off:gtg=exists_sym_2985 on theBenchmark for (2985ds/134Mi) % 17.82/3.61 % (3918642)Instruction limit reached! % 17.82/3.61 % (3918642)------------------------------ % 17.82/3.61 % (3918642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.61 % (3918642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.61 % (3918642)CaDiCaL version: 2.1.3 % 17.82/3.61 % (3918642)Termination reason: Instruction limit % 17.82/3.61 % (3918642)Termination phase: Saturation % 17.82/3.61 % (3918642)Time elapsed: 0.077 s % 17.82/3.61 % (3918642)Peak memory usage: 90 MB % 17.82/3.61 % (3918642)Instructions burned: 135 (million) % 17.82/3.61 % (3918640)Instruction limit reached! % 17.82/3.61 % (3918640)------------------------------ % 17.82/3.61 % (3918640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.61 % (3918640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.61 % (3918640)CaDiCaL version: 2.1.3 % 17.82/3.61 % (3918640)Termination reason: Instruction limit % 17.82/3.61 % (3918640)Termination phase: Saturation % 17.82/3.61 % (3918640)Time elapsed: 0.121 s % 17.82/3.61 % (3918640)Peak memory usage: 89 MB % 17.82/3.61 % (3918640)Instructions burned: 125 (million) % 17.82/3.61 % (3918643)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3601423350:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi) % 23.62/4.29 % (3918643)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 23.62/4.29 % (3918643)Refutation not found, incomplete strategy % 23.62/4.29 % (3918643)------------------------------ % 23.62/4.29 % (3918643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.62/4.29 % (3918643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.62/4.29 % (3918643)CaDiCaL version: 2.1.3 % 23.62/4.29 % (3918643)Termination reason: Refutation not found, incomplete strategy % 23.62/4.29 % (3918643)Time elapsed: 0.006 s % 23.62/4.29 % (3918643)Peak memory usage: 88 MB % 23.62/4.29 % (3918643)Instructions burned: 4 (million) % 23.62/4.29 % (3918631)------------------------------ % 23.62/4.29 % (3918631)------------------------------ % 23.62/4.29 % (3918645)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3817553167:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/431Mi) % 23.62/4.29 % (3918650)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=1157838892:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2982 on theBenchmark for (2982ds/150Mi) % 23.62/4.29 % (3918649)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=3636951779:i=6060:aac=none:ins=25_2982 on theBenchmark for (2982ds/6060Mi) % 23.62/4.29 % (3918650)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 23.62/4.29 % (3918629)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.62/4.29 % (3918629)------------------------------ % 23.62/4.29 % (3918629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.62/4.29 % (3918629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.62/4.29 % (3918629)CaDiCaL version: 2.1.3 % 23.62/4.29 % (3918629)Termination reason: Unknown % 23.62/4.29 % (3918629)Termination phase: Saturation % 23.62/4.29 % (3918629)Time elapsed: 0.601 s % 23.62/4.29 % (3918629)Peak memory usage: 113 MB % 23.62/4.29 % (3918629)Instructions burned: 542 (million) % 23.62/4.29 % (3918632)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.62/4.29 % (3918632)------------------------------ % 23.62/4.29 % (3918632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.62/4.29 % (3918632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.62/4.29 % (3918632)CaDiCaL version: 2.1.3 % 23.62/4.29 % (3918632)Termination reason: Unknown % 23.62/4.29 % (3918632)Termination phase: Saturation % 23.62/4.29 % (3918632)Time elapsed: 0.601 s % 23.62/4.29 % (3918632)Peak memory usage: 113 MB % 23.62/4.29 % (3918632)Instructions burned: 543 (million) % 23.62/4.29 % (3918650)Instruction limit reached! % 23.62/4.29 % (3918650)------------------------------ % 23.62/4.29 % (3918650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.62/4.29 % (3918650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.62/4.29 % (3918650)CaDiCaL version: 2.1.3 % 23.62/4.29 % (3918650)Termination reason: Instruction limit % 23.62/4.29 % (3918650)Termination phase: Saturation % 23.62/4.29 % (3918650)Time elapsed: 0.093 s % 23.62/4.29 % (3918650)Peak memory usage: 90 MB % 23.62/4.29 % (3918650)Instructions burned: 151 (million) % 23.62/4.29 % (3918653)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1714180181:i=14155:bd=all_2981 on theBenchmark for (2981ds/14155Mi) % 23.62/4.29 % (3918643)------------------------------ % 23.62/4.29 % (3918643)------------------------------ % 23.62/4.29 % (3918645)Instruction limit reached! % 23.62/4.29 % (3918645)------------------------------ % 23.62/4.29 % (3918645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.62/4.29 % (3918645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.62/4.29 % (3918645)CaDiCaL version: 2.1.3 % 23.62/4.29 % (3918645)Termination reason: Instruction limit % 23.62/4.29 % (3918645)Termination phase: Saturation % 23.62/4.29 % (3918645)Time elapsed: 0.383 s % 23.62/4.29 % (3918645)Peak memory usage: 90 MB % 23.62/4.29 % (3918645)Instructions burned: 431 (million) % 23.62/4.29 % (3918656)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3648149174:i=667:av=off:fsr=off_2980 on theBenchmark for (2980ds/667Mi) % 30.93/5.28 % (3918656)Refutation not found, incomplete strategy % 30.93/5.28 % (3918656)------------------------------ % 30.93/5.28 % (3918656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.93/5.28 % (3918656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.93/5.28 % (3918656)CaDiCaL version: 2.1.3 % 30.93/5.28 % (3918656)Termination reason: Refutation not found, incomplete strategy % 30.93/5.28 % (3918656)Time elapsed: 0.014 s % 30.93/5.28 % (3918656)Peak memory usage: 88 MB % 30.93/5.28 % (3918656)Instructions burned: 13 (million) % 30.93/5.28 % (3918660)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3394466007:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2979 on theBenchmark for (2979ds/193Mi) % 30.93/5.28 % (3918658)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=2385446148:s2a=on:i=185:s2at=1.8:fdi=4_2979 on theBenchmark for (2979ds/185Mi) % 30.93/5.28 % (3918660)Instruction limit reached! % 30.93/5.28 % (3918660)------------------------------ % 30.93/5.28 % (3918660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.93/5.28 % (3918660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.93/5.28 % (3918660)CaDiCaL version: 2.1.3 % 30.93/5.28 % (3918660)Termination reason: Instruction limit % 30.93/5.28 % (3918660)Termination phase: Saturation % 30.93/5.28 % (3918660)Time elapsed: 0.098 s % 30.93/5.28 % (3918660)Peak memory usage: 90 MB % 30.93/5.28 % (3918660)Instructions burned: 194 (million) % 30.93/5.28 % (3918662)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1240370539:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2977 on theBenchmark for (2977ds/4850Mi) % 30.93/5.28 % (3918658)Instruction limit reached! % 30.93/5.28 % (3918658)------------------------------ % 30.93/5.28 % (3918658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.93/5.28 % (3918658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.93/5.28 % (3918658)CaDiCaL version: 2.1.3 % 30.93/5.28 % (3918658)Termination reason: Instruction limit % 30.93/5.28 % (3918658)Termination phase: Saturation % 30.93/5.28 % (3918658)Time elapsed: 0.198 s % 30.93/5.28 % (3918658)Peak memory usage: 91 MB % 30.93/5.28 % (3918658)Instructions burned: 185 (million) % 30.93/5.28 % (3918649)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 30.93/5.28 % (3918649)------------------------------ % 30.93/5.28 % (3918649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.93/5.28 % (3918649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.93/5.28 % (3918649)CaDiCaL version: 2.1.3 % 30.93/5.28 % (3918649)Termination reason: Unknown % 30.93/5.28 % (3918649)Termination phase: Saturation % 30.93/5.28 % (3918649)Time elapsed: 0.547 s % 30.93/5.28 % (3918649)Peak memory usage: 114 MB % 30.93/5.28 % (3918649)Instructions burned: 542 (million) % 30.93/5.28 % (3918664)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2616337689:i=12111:sd=1:ss=included_2977 on theBenchmark for (2977ds/12111Mi) % 30.93/5.28 % (3918667)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2044658227:i=319:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/319Mi) % 30.93/5.28 % (3918656)------------------------------ % 30.93/5.28 % (3918656)------------------------------ % 30.93/5.28 % (3918653)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 30.93/5.28 % (3918653)------------------------------ % 30.93/5.28 % (3918653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.93/5.28 % (3918653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.93/5.28 % (3918653)CaDiCaL version: 2.1.3 % 30.93/5.28 % (3918653)Termination reason: Unknown % 30.93/5.28 % (3918653)Termination phase: Saturation % 30.93/5.28 % (3918653)Time elapsed: 0.601 s % 30.93/5.28 % (3918653)Peak memory usage: 114 MB % 30.93/5.28 % (3918653)Instructions burned: 541 (million) % 30.93/5.28 % (3918669)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3232237278:i=2064:ep=RST_2975 on theBenchmark for (2975ds/2064Mi) % 30.93/5.28 % (3918669)Refutation not found, incomplete strategy % 30.93/5.28 % (3918669)------------------------------ % 30.93/5.28 % (3918669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.93/5.28 % (3918669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/6.38 % (3918669)CaDiCaL version: 2.1.3 % 38.61/6.38 % (3918669)Termination reason: Refutation not found, incomplete strategy % 38.61/6.38 % (3918669)Time elapsed: 0.011 s % 38.61/6.38 % (3918669)Peak memory usage: 88 MB % 38.61/6.38 % (3918669)Instructions burned: 10 (million) % 38.61/6.38 % (3918667)Instruction limit reached! % 38.61/6.38 % (3918667)------------------------------ % 38.61/6.38 % (3918667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.61/6.38 % (3918667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/6.38 % (3918667)CaDiCaL version: 2.1.3 % 38.61/6.38 % (3918667)Termination reason: Instruction limit % 38.61/6.38 % (3918667)Termination phase: Saturation % 38.61/6.38 % (3918667)Time elapsed: 0.174 s % 38.61/6.38 % (3918667)Peak memory usage: 92 MB % 38.61/6.38 % (3918667)Instructions burned: 321 (million) % 38.61/6.38 % (3918671)dis-1011_128_sil=32000:random_seed=3777260180:i=3706:ep=RST:av=off_2974 on theBenchmark for (2974ds/3706Mi) % 38.61/6.38 % (3918673)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=612414697:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2973 on theBenchmark for (2973ds/757Mi) % 38.61/6.38 % (3918673)Refutation not found, incomplete strategy % 38.61/6.38 % (3918673)------------------------------ % 38.61/6.38 % (3918673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.61/6.38 % (3918673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/6.38 % (3918673)CaDiCaL version: 2.1.3 % 38.61/6.38 % (3918673)Termination reason: Refutation not found, incomplete strategy % 38.61/6.38 % (3918673)Time elapsed: 0.008 s % 38.61/6.38 % (3918673)Peak memory usage: 89 MB % 38.61/6.38 % (3918673)Instructions burned: 10 (million) % 38.61/6.38 % (3918676)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1948033616:i=9925:aac=none_2972 on theBenchmark for (2972ds/9925Mi) % 38.61/6.38 % (3918675)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4169221595:i=13913:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/13913Mi) % 38.61/6.38 % (3918664)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.61/6.38 % (3918664)------------------------------ % 38.61/6.38 % (3918664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.61/6.38 % (3918664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/6.38 % (3918664)CaDiCaL version: 2.1.3 % 38.61/6.38 % (3918664)Termination reason: Unknown % 38.61/6.38 % (3918664)Termination phase: Saturation % 38.61/6.38 % (3918664)Time elapsed: 0.608 s % 38.61/6.38 % (3918664)Peak memory usage: 114 MB % 38.61/6.38 % (3918664)Instructions burned: 542 (million) % 38.61/6.38 % (3918669)------------------------------ % 38.61/6.38 % (3918669)------------------------------ % 38.61/6.38 % (3918673)------------------------------ % 38.61/6.38 % (3918673)------------------------------ % 38.61/6.38 % (3918676)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.61/6.38 % (3918676)------------------------------ % 38.61/6.38 % (3918676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.61/6.38 % (3918676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/6.39 % (3918676)CaDiCaL version: 2.1.3 % 38.61/6.39 % (3918676)Termination reason: Unknown % 38.61/6.39 % (3918676)Termination phase: Saturation % 38.61/6.39 % (3918676)Time elapsed: 0.321 s % 38.61/6.39 % (3918676)Peak memory usage: 114 MB % 38.61/6.39 % (3918676)Instructions burned: 541 (million) % 38.61/6.39 % (3918681)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1406255407:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/2479Mi) % 38.61/6.39 % (3918681)Refutation not found, incomplete strategy % 38.61/6.39 % (3918681)------------------------------ % 38.61/6.39 % (3918681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.61/6.39 % (3918681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.61/6.39 % (3918681)CaDiCaL version: 2.1.3 % 38.61/6.39 % (3918681)Termination reason: Refutation not found, incomplete strategy % 38.61/6.39 % (3918681)Time elapsed: 0.013 s % 38.61/6.39 % (3918681)Peak memory usage: 89 MB % 38.61/6.39 % (3918681)Instructions burned: 11 (million) % 38.61/6.39 % (3918683)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2130802360:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2968 on theBenchmark for (2968ds/440Mi) % 46.43/7.57 % (3918683)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 46.43/7.57 % (3918687)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4097465471:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/11145Mi) % 46.43/7.57 % (3918688)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=2646409934:cts=off:i=3034:av=off:er=known:fsd=on_2967 on theBenchmark for (2967ds/3034Mi) % 46.43/7.57 % (3918675)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 46.43/7.57 % (3918675)------------------------------ % 46.43/7.57 % (3918675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.43/7.57 % (3918675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.43/7.57 % (3918675)CaDiCaL version: 2.1.3 % 46.43/7.57 % (3918675)Termination reason: Unknown % 46.43/7.57 % (3918675)Termination phase: Saturation % 46.43/7.57 % (3918675)Time elapsed: 0.603 s % 46.43/7.57 % (3918675)Peak memory usage: 113 MB % 46.43/7.57 % (3918675)Instructions burned: 541 (million) % 46.43/7.57 % (3918681)------------------------------ % 46.43/7.57 % (3918681)------------------------------ % 46.43/7.57 % (3918688)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 46.43/7.57 % (3918688)------------------------------ % 46.43/7.57 % (3918688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.43/7.57 % (3918688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.43/7.57 % (3918688)CaDiCaL version: 2.1.3 % 46.43/7.57 % (3918688)Termination reason: Unknown % 46.43/7.57 % (3918688)Termination phase: Saturation % 46.43/7.57 % (3918688)Time elapsed: 0.321 s % 46.43/7.57 % (3918688)Peak memory usage: 113 MB % 46.43/7.57 % (3918688)Instructions burned: 541 (million) % 46.43/7.57 % (3918683)Instruction limit reached! % 46.43/7.57 % (3918683)------------------------------ % 46.43/7.57 % (3918683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.43/7.57 % (3918683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.43/7.57 % (3918683)CaDiCaL version: 2.1.3 % 46.43/7.57 % (3918683)Termination reason: Instruction limit % 46.43/7.57 % (3918683)Termination phase: Saturation % 46.43/7.57 % (3918683)Time elapsed: 0.431 s % 46.43/7.57 % (3918683)Peak memory usage: 93 MB % 46.43/7.57 % (3918683)Instructions burned: 441 (million) % 46.43/7.57 % (3918693)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=572319330:st=2:s2a=on:i=524:s2at=2:ss=axioms_2963 on theBenchmark for (2963ds/524Mi) % 46.43/7.57 % (3918694)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2015733741:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2962 on theBenchmark for (2962ds/1016Mi) % 46.43/7.57 % (3918687)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 46.43/7.57 % (3918687)------------------------------ % 46.43/7.57 % (3918687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.43/7.57 % (3918687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.43/7.57 % (3918687)CaDiCaL version: 2.1.3 % 46.43/7.57 % (3918687)Termination reason: Unknown % 46.43/7.57 % (3918687)Termination phase: Saturation % 46.43/7.57 % (3918687)Time elapsed: 0.598 s % 46.43/7.57 % (3918687)Peak memory usage: 113 MB % 46.43/7.57 % (3918687)Instructions burned: 541 (million) % 46.43/7.57 % (3918696)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3725250351:i=5781:kws=precedence:bd=all:rawr=on_2961 on theBenchmark for (2961ds/5781Mi) % 46.43/7.57 % (3918695)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2213242368:i=14123:bd=preordered:ins=4_2961 on theBenchmark for (2961ds/14123Mi) % 46.43/7.57 % (3918693)Instruction limit reached! % 46.43/7.57 % (3918693)------------------------------ % 46.43/7.57 % (3918693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.43/7.57 % (3918693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.43/7.57 % (3918693)CaDiCaL version: 2.1.3 % 46.43/7.57 % (3918693)Termination reason: Instruction limit % 46.43/7.57 % (3918693)Termination phase: Saturation % 46.43/7.57 % (3918693)Time elapsed: 0.491 s % 46.43/7.57 % (3918693)Peak memory usage: 93 MB % 54.94/8.80 % (3918693)Instructions burned: 524 (million) % 54.94/8.80 % (3918701)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=1555496990:i=2448:gtgl=5:bd=preordered:gtg=all_2958 on theBenchmark for (2958ds/2448Mi) % 54.94/8.80 % (3918694)Instruction limit reached! % 54.94/8.80 % (3918694)------------------------------ % 54.94/8.80 % (3918694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.94/8.80 % (3918694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.94/8.80 % (3918694)CaDiCaL version: 2.1.3 % 54.94/8.80 % (3918694)Termination reason: Instruction limit % 54.94/8.80 % (3918694)Termination phase: Saturation % 54.94/8.80 % (3918694)Time elapsed: 0.440 s % 54.94/8.80 % (3918694)Peak memory usage: 99 MB % 54.94/8.80 % (3918694)Instructions burned: 1016 (million) % 54.94/8.80 % (3918706)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1048433560:st=5.6:i=2033:sd=3:ss=axioms_2955 on theBenchmark for (2955ds/2033Mi) % 54.94/8.80 % (3918704)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3602040820:i=3223:kws=precedence:fgj=on:av=off_2955 on theBenchmark for (2955ds/3223Mi) % 54.94/8.80 % (3918695)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.94/8.80 % (3918695)------------------------------ % 54.94/8.80 % (3918695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.94/8.80 % (3918695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.94/8.80 % (3918695)CaDiCaL version: 2.1.3 % 54.94/8.80 % (3918695)Termination reason: Unknown % 54.94/8.80 % (3918695)Termination phase: Saturation % 54.94/8.80 % (3918695)Time elapsed: 0.591 s % 54.94/8.80 % (3918695)Peak memory usage: 114 MB % 54.94/8.80 % (3918695)Instructions burned: 541 (million) % 54.94/8.80 % (3918706)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.94/8.80 % (3918706)------------------------------ % 54.94/8.80 % (3918706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.94/8.80 % (3918706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.94/8.80 % (3918706)CaDiCaL version: 2.1.3 % 54.94/8.80 % (3918706)Termination reason: Unknown % 54.94/8.80 % (3918706)Termination phase: Saturation % 54.94/8.80 % (3918706)Time elapsed: 0.325 s % 54.94/8.80 % (3918706)Peak memory usage: 113 MB % 54.94/8.80 % (3918706)Instructions burned: 542 (million) % 54.94/8.80 % (3918711)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2397431117:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2952 on theBenchmark for (2952ds/2055Mi) % 54.94/8.80 % (3918701)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.94/8.80 % (3918701)------------------------------ % 54.94/8.80 % (3918701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.94/8.80 % (3918701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.94/8.80 % (3918701)CaDiCaL version: 2.1.3 % 54.94/8.80 % (3918701)Termination reason: Unknown % 54.94/8.80 % (3918701)Termination phase: Saturation % 54.94/8.80 % (3918701)Time elapsed: 0.601 s % 54.94/8.80 % (3918701)Peak memory usage: 114 MB % 54.94/8.80 % (3918701)Instructions burned: 544 (million) % 54.94/8.80 % (3918722)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=3293038014:i=21611:sd=3:ss=axioms_2950 on theBenchmark for (2950ds/21611Mi) % 54.94/8.80 % (3918724)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1491389272:i=4835:sd=13:ss=axioms:sgt=23_2949 on theBenchmark for (2949ds/4835Mi) % 54.94/8.80 % (3918704)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.94/8.80 % (3918704)------------------------------ % 54.94/8.80 % (3918704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.94/8.80 % (3918704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.94/8.80 % (3918704)CaDiCaL version: 2.1.3 % 54.94/8.80 % (3918704)Termination reason: Unknown % 54.94/8.80 % (3918704)Termination phase: Saturation % 54.94/8.80 % (3918704)Time elapsed: 0.601 s % 54.94/8.80 % (3918704)Peak memory usage: 114 MB % 54.94/8.80 % (3918704)Instructions burned: 541 (million) % 54.94/8.80 % (3918722)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.94/8.80 % (3918722)------------------------------ % 66.24/10.23 % (3918722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.24/10.23 % (3918722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.24/10.23 % (3918722)CaDiCaL version: 2.1.3 % 66.24/10.23 % (3918722)Termination reason: Unknown % 66.24/10.23 % (3918722)Termination phase: Saturation % 66.24/10.23 % (3918722)Time elapsed: 0.323 s % 66.24/10.23 % (3918722)Peak memory usage: 113 MB % 66.24/10.23 % (3918722)Instructions burned: 540 (million) % 66.24/10.23 % (3918727)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=3233088345:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2946 on theBenchmark for (2946ds/797Mi) % 66.24/10.23 % (3918711)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 66.24/10.23 % (3918711)------------------------------ % 66.24/10.23 % (3918711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.24/10.23 % (3918711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.24/10.23 % (3918711)CaDiCaL version: 2.1.3 % 66.24/10.23 % (3918711)Termination reason: Unknown % 66.24/10.23 % (3918711)Termination phase: Saturation % 66.24/10.23 % (3918711)Time elapsed: 0.600 s % 66.24/10.23 % (3918711)Peak memory usage: 114 MB % 66.24/10.23 % (3918711)Instructions burned: 542 (million) % 66.24/10.23 % (3918728)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3656279743:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2944 on theBenchmark for (2944ds/2326Mi) % 66.24/10.23 % (3918730)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1779590641:i=6038:nm=6_2943 on theBenchmark for (2943ds/6038Mi) % 66.24/10.23 % (3918671)Instruction limit reached! % 66.24/10.23 % (3918671)------------------------------ % 66.24/10.23 % (3918671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.24/10.23 % (3918671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.24/10.23 % (3918671)CaDiCaL version: 2.1.3 % 66.24/10.23 % (3918671)Termination reason: Instruction limit % 66.24/10.23 % (3918671)Termination phase: Saturation % 66.24/10.23 % (3918671)Time elapsed: 3.400 s % 66.24/10.23 % (3918671)Peak memory usage: 109 MB % 66.24/10.23 % (3918671)Instructions burned: 3706 (million) % 66.24/10.23 % (3918733)lrs+10_1_sil=32000:sp=occurrence:random_seed=2999030716:st=2:i=33334:sd=3:ss=included:sgt=32_2938 on theBenchmark for (2938ds/33334Mi) % 66.24/10.23 % (3918727)Instruction limit reached! % 66.24/10.23 % (3918727)------------------------------ % 66.24/10.23 % (3918727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.24/10.23 % (3918727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.24/10.23 % (3918727)CaDiCaL version: 2.1.3 % 66.24/10.23 % (3918727)Termination reason: Instruction limit % 66.24/10.23 % (3918727)Termination phase: Saturation % 66.24/10.23 % (3918727)Time elapsed: 0.870 s % 66.24/10.23 % (3918727)Peak memory usage: 100 MB % 66.24/10.23 % (3918727)Instructions burned: 797 (million) % 66.24/10.23 % (3918662)Instruction limit reached! % 66.24/10.23 % (3918662)------------------------------ % 66.24/10.23 % (3918662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.24/10.23 % (3918662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.24/10.23 % (3918662)CaDiCaL version: 2.1.3 % 66.24/10.23 % (3918662)Termination reason: Instruction limit % 66.24/10.23 % (3918662)Termination phase: Saturation % 66.24/10.23 % (3918662)Time elapsed: 4.041 s % 66.24/10.23 % (3918662)Peak memory usage: 132 MB % 66.24/10.23 % (3918662)Instructions burned: 4851 (million) % 66.24/10.23 % (3918730)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 66.24/10.23 % (3918730)------------------------------ % 66.24/10.23 % (3918730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.24/10.23 % (3918730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.24/10.23 % (3918730)CaDiCaL version: 2.1.3 % 66.24/10.23 % (3918730)Termination reason: Unknown % 66.24/10.23 % (3918730)Termination phase: Saturation % 66.24/10.23 % (3918730)Time elapsed: 0.588 s % 66.24/10.23 % (3918730)Peak memory usage: 113 MB % 66.24/10.23 % (3918730)Instructions burned: 542 (million) % 66.24/10.23 % (3918728)Instruction limit reached! % 66.24/10.23 % (3918728)------------------------------ % 66.24/10.23 % (3918728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.87/11.19 % (3918728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.87/11.19 % (3918728)CaDiCaL version: 2.1.3 % 72.87/11.19 % (3918728)Termination reason: Instruction limit % 72.87/11.19 % (3918728)Termination phase: Saturation % 72.87/11.19 % (3918728)Time elapsed: 0.959 s % 72.87/11.19 % (3918728)Peak memory usage: 150 MB % 72.87/11.19 % (3918728)Instructions burned: 2330 (million) % 72.87/11.19 % (3918735)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2051908368:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2934 on theBenchmark for (2934ds/1008Mi) % 72.87/11.19 % (3918736)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=1646817618:i=8327:s2at=5:bd=preordered_2934 on theBenchmark for (2934ds/8327Mi) % 72.87/11.19 % (3918737)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=581774518:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2934 on theBenchmark for (2934ds/1083Mi) % 72.87/11.19 % (3918740)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1789317735:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2932 on theBenchmark for (2932ds/1084Mi) % 72.87/11.19 % (3918736)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.87/11.19 % (3918736)------------------------------ % 72.87/11.19 % (3918736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.87/11.19 % (3918736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.87/11.19 % (3918736)CaDiCaL version: 2.1.3 % 72.87/11.19 % (3918736)Termination reason: Unknown % 72.87/11.19 % (3918736)Termination phase: Saturation % 72.87/11.19 % (3918736)Time elapsed: 0.573 s % 72.87/11.19 % (3918736)Peak memory usage: 113 MB % 72.87/11.19 % (3918736)Instructions burned: 541 (million) % 72.87/11.19 % (3918740)Instruction limit reached! % 72.87/11.19 % (3918740)------------------------------ % 72.87/11.19 % (3918740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.87/11.19 % (3918740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.87/11.19 % (3918740)CaDiCaL version: 2.1.3 % 72.87/11.19 % (3918740)Termination reason: Instruction limit % 72.87/11.19 % (3918740)Termination phase: Saturation % 72.87/11.19 % (3918740)Time elapsed: 0.559 s % 72.87/11.19 % (3918740)Peak memory usage: 96 MB % 72.87/11.19 % (3918740)Instructions burned: 1084 (million) % 72.87/11.19 % (3918747)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=626353905:i=6995:s2at=5:gtg=all_2926 on theBenchmark for (2926ds/6995Mi) % 72.87/11.19 % (3918735)Instruction limit reached! % 72.87/11.19 % (3918735)------------------------------ % 72.87/11.19 % (3918735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.87/11.19 % (3918735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.87/11.19 % (3918735)CaDiCaL version: 2.1.3 % 72.87/11.19 % (3918735)Termination reason: Instruction limit % 72.87/11.19 % (3918735)Termination phase: Saturation % 72.87/11.19 % (3918735)Time elapsed: 0.891 s % 72.87/11.19 % (3918735)Peak memory usage: 97 MB % 72.87/11.19 % (3918735)Instructions burned: 1009 (million) % 72.87/11.19 % (3918748)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1572842747:st=2:i=6225:sd=15:ss=axioms_2925 on theBenchmark for (2925ds/6225Mi) % 72.87/11.19 % (3918737)Instruction limit reached! % 72.87/11.19 % (3918737)------------------------------ % 72.87/11.19 % (3918737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.87/11.19 % (3918737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.87/11.19 % (3918737)CaDiCaL version: 2.1.3 % 72.87/11.19 % (3918737)Termination reason: Instruction limit % 72.87/11.19 % (3918737)Termination phase: Saturation % 72.87/11.19 % (3918737)Time elapsed: 0.929 s % 72.87/11.19 % (3918737)Peak memory usage: 94 MB % 72.87/11.19 % (3918737)Instructions burned: 1084 (million) % 72.87/11.19 % (3918750)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=265287280:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2923 on theBenchmark for (2923ds/3372Mi) % 72.87/11.19 % (3918747)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.87/11.19 % (3918747)------------------------------ % 72.87/11.19 % (3918747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.16/12.29 % (3918747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.16/12.29 % (3918747)CaDiCaL version: 2.1.3 % 80.16/12.29 % (3918747)Termination reason: Unknown % 80.16/12.29 % (3918747)Termination phase: Saturation % 80.16/12.29 % (3918747)Time elapsed: 0.326 s % 80.16/12.29 % (3918747)Peak memory usage: 114 MB % 80.16/12.29 % (3918747)Instructions burned: 544 (million) % 80.16/12.29 % (3918752)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2781745135:st=2.3:i=26457:sd=10:ss=included:sgt=8_2922 on theBenchmark for (2922ds/26457Mi) % 80.16/12.29 % (3918755)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=833151962:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2920 on theBenchmark for (2920ds/13494Mi) % 80.16/12.29 % (3918755)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.16/12.29 % (3918755)------------------------------ % 80.16/12.29 % (3918755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.16/12.29 % (3918755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.16/12.29 % (3918755)CaDiCaL version: 2.1.3 % 80.16/12.29 % (3918755)Termination reason: Unknown % 80.16/12.29 % (3918755)Termination phase: Saturation % 80.16/12.29 % (3918755)Time elapsed: 0.325 s % 80.16/12.29 % (3918755)Peak memory usage: 114 MB % 80.16/12.29 % (3918755)Instructions burned: 546 (million) % 80.16/12.29 % (3918750)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.16/12.29 % (3918750)------------------------------ % 80.16/12.29 % (3918750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.16/12.29 % (3918750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.16/12.29 % (3918750)CaDiCaL version: 2.1.3 % 80.16/12.29 % (3918750)Termination reason: Unknown % 80.16/12.29 % (3918750)Termination phase: Saturation % 80.16/12.29 % (3918750)Time elapsed: 0.575 s % 80.16/12.29 % (3918750)Peak memory usage: 113 MB % 80.16/12.29 % (3918750)Instructions burned: 540 (million) % 80.16/12.29 % (3918752)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.16/12.29 % (3918752)------------------------------ % 80.16/12.29 % (3918752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.16/12.29 % (3918752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.16/12.29 % (3918752)CaDiCaL version: 2.1.3 % 80.16/12.29 % (3918752)Termination reason: Unknown % 80.16/12.29 % (3918752)Termination phase: Saturation % 80.16/12.29 % (3918752)Time elapsed: 0.564 s % 80.16/12.29 % (3918752)Peak memory usage: 113 MB % 80.16/12.29 % (3918752)Instructions burned: 542 (million) % 80.16/12.29 % (3918758)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3078248183:i=2559:sd=1:ep=RSTC:ss=axioms_2914 on theBenchmark for (2914ds/2559Mi) % 80.16/12.29 % (3918759)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3868765257:i=30753:av=off:ss=included_2914 on theBenchmark for (2914ds/30753Mi) % 80.16/12.29 % (3918757)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=2162235002:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2914 on theBenchmark for (2914ds/2503Mi) % 80.16/12.29 % (3918757)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 80.16/12.29 % (3918758)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.16/12.29 % (3918758)------------------------------ % 80.16/12.29 % (3918758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.16/12.29 % (3918758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.16/12.29 % (3918758)CaDiCaL version: 2.1.3 % 80.16/12.29 % (3918758)Termination reason: Unknown % 80.16/12.29 % (3918758)Termination phase: Saturation % 80.16/12.29 % (3918758)Time elapsed: 0.328 s % 80.16/12.29 % (3918758)Peak memory usage: 113 MB % 80.16/12.29 % (3918758)Instructions burned: 541 (million) % 80.16/12.29 % (3918763)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3877726865:i=26473:ep=RSTC_2909 on theBenchmark for (2909ds/26473Mi) % 80.16/12.29 % (3918759)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.16/12.29 % (3918759)------------------------------ % 90.42/13.71 % (3918759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.42/13.71 % (3918759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.42/13.71 % (3918759)CaDiCaL version: 2.1.3 % 90.42/13.71 % (3918759)Termination reason: Unknown % 90.42/13.71 % (3918759)Termination phase: Saturation % 90.42/13.71 % (3918759)Time elapsed: 0.578 s % 90.42/13.71 % (3918759)Peak memory usage: 113 MB % 90.42/13.71 % (3918759)Instructions burned: 542 (million) % 90.42/13.71 % (3918757)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 90.42/13.71 % (3918757)------------------------------ % 90.42/13.71 % (3918757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.42/13.71 % (3918757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.42/13.71 % (3918757)CaDiCaL version: 2.1.3 % 90.42/13.71 % (3918757)Termination reason: Unknown % 90.42/13.71 % (3918757)Termination phase: Saturation % 90.42/13.71 % (3918757)Time elapsed: 0.602 s % 90.42/13.71 % (3918757)Peak memory usage: 113 MB % 90.42/13.71 % (3918757)Instructions burned: 540 (million) % 90.42/13.71 % (3918765)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=2048533949:cts=off:i=2759:kws=inv_arity:fgj=on_2906 on theBenchmark for (2906ds/2759Mi) % 90.42/13.71 % (3918766)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=1179588995:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2905 on theBenchmark for (2905ds/5665Mi) % 90.42/13.71 % (3918766)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 90.42/13.71 % (3918696)Instruction limit reached! % 90.42/13.71 % (3918696)------------------------------ % 90.42/13.71 % (3918696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.42/13.71 % (3918696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.42/13.71 % (3918696)CaDiCaL version: 2.1.3 % 90.42/13.71 % (3918696)Termination reason: Instruction limit % 90.42/13.71 % (3918696)Termination phase: Saturation % 90.42/13.71 % (3918696)Time elapsed: 5.628 s % 90.42/13.71 % (3918696)Peak memory usage: 120 MB % 90.42/13.71 % (3918696)Instructions burned: 5782 (million) % 90.42/13.71 % (3918724)Instruction limit reached! % 90.42/13.71 % (3918724)------------------------------ % 90.42/13.71 % (3918724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.42/13.71 % (3918724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.42/13.71 % (3918724)CaDiCaL version: 2.1.3 % 90.42/13.71 % (3918724)Termination reason: Instruction limit % 90.42/13.71 % (3918724)Termination phase: Saturation % 90.42/13.71 % (3918724)Time elapsed: 4.520 s % 90.42/13.71 % (3918724)Peak memory usage: 129 MB % 90.42/13.71 % (3918724)Instructions burned: 4835 (million) % 90.42/13.71 % (3918769)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=1231751326:i=1532:ep=RS:ss=axioms_2902 on theBenchmark for (2902ds/1532Mi) % 90.42/13.71 % (3918770)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=413222404:i=1565:sd=2:ss=axioms:sgt=32_2901 on theBenchmark for (2901ds/1565Mi) % 90.42/13.71 % (3918765)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 90.42/13.71 % (3918765)------------------------------ % 90.42/13.71 % (3918765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.42/13.71 % (3918765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.42/13.71 % (3918765)CaDiCaL version: 2.1.3 % 90.42/13.71 % (3918765)Termination reason: Unknown % 90.42/13.71 % (3918765)Termination phase: Saturation % 90.42/13.71 % (3918765)Time elapsed: 0.554 s % 90.42/13.71 % (3918765)Peak memory usage: 114 MB % 90.42/13.71 % (3918765)Instructions burned: 544 (million) % 90.42/13.71 % (3918766)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 90.42/13.71 % (3918766)------------------------------ % 90.42/13.71 % (3918766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.42/13.71 % (3918766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.42/13.71 % (3918766)CaDiCaL version: 2.1.3 % 90.42/13.71 % (3918766)Termination reason: Unknown % 90.42/13.71 % (3918766)Termination phase: Saturation % 96.72/14.76 % (3918766)Time elapsed: 0.602 s % 96.72/14.76 % (3918766)Peak memory usage: 113 MB % 96.72/14.76 % (3918766)Instructions burned: 541 (million) % 96.72/14.76 % (3918773)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=4278302757:i=1572:fgj=on:gsp=on_2898 on theBenchmark for (2898ds/1572Mi) % 96.72/14.76 % (3918773)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 96.72/14.76 % (3918774)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3762999682:i=6052:sd=4:ss=axioms:sgt=24_2896 on theBenchmark for (2896ds/6052Mi) % 96.72/14.76 % (3918770)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.72/14.76 % (3918770)------------------------------ % 96.72/14.76 % (3918770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.72/14.76 % (3918770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.72/14.76 % (3918770)CaDiCaL version: 2.1.3 % 96.72/14.76 % (3918770)Termination reason: Unknown % 96.72/14.76 % (3918770)Termination phase: Saturation % 96.72/14.76 % (3918770)Time elapsed: 0.562 s % 96.72/14.76 % (3918770)Peak memory usage: 113 MB % 96.72/14.76 % (3918770)Instructions burned: 542 (million) % 96.72/14.76 % (3918769)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.72/14.76 % (3918769)------------------------------ % 96.72/14.76 % (3918769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.72/14.76 % (3918769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.72/14.76 % (3918769)CaDiCaL version: 2.1.3 % 96.72/14.76 % (3918769)Termination reason: Unknown % 96.72/14.76 % (3918769)Termination phase: Saturation % 96.72/14.76 % (3918769)Time elapsed: 0.614 s % 96.72/14.76 % (3918769)Peak memory usage: 113 MB % 96.72/14.76 % (3918769)Instructions burned: 542 (million) % 96.72/14.76 % (3918778)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=30568945:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2893 on theBenchmark for (2893ds/1842Mi) % 96.72/14.76 % (3918777)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=1285072032:i=3500:sd=1:bd=preordered:sup=off:ss=included_2893 on theBenchmark for (2893ds/3500Mi) % 96.72/14.76 % (3918778)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 96.72/14.76 % (3918773)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.72/14.76 % (3918773)------------------------------ % 96.72/14.76 % (3918773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.72/14.76 % (3918773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.72/14.76 % (3918773)CaDiCaL version: 2.1.3 % 96.72/14.76 % (3918773)Termination reason: Unknown % 96.72/14.76 % (3918773)Termination phase: Saturation % 96.72/14.76 % (3918773)Time elapsed: 0.596 s % 96.72/14.76 % (3918773)Peak memory usage: 113 MB % 96.72/14.76 % (3918773)Instructions burned: 541 (million) % 96.72/14.76 % (3918774)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.72/14.76 % (3918774)------------------------------ % 96.72/14.76 % (3918774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.72/14.76 % (3918774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.72/14.76 % (3918774)CaDiCaL version: 2.1.3 % 96.72/14.76 % (3918774)Termination reason: Unknown % 96.72/14.76 % (3918774)Termination phase: Saturation % 96.72/14.76 % (3918774)Time elapsed: 0.598 s % 96.72/14.76 % (3918774)Peak memory usage: 113 MB % 96.72/14.76 % (3918774)Instructions burned: 540 (million) % 96.72/14.76 % (3918785)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1715566004:i=66096:add=on_2889 on theBenchmark for (2889ds/66096Mi) % 96.72/14.76 % (3918777)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.72/14.76 % (3918777)------------------------------ % 96.72/14.76 % (3918777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.72/14.76 % (3918777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.72/14.76 % (3918777)CaDiCaL version: 2.1.3 % 103.98/15.79 % (3918777)Termination reason: Unknown % 103.98/15.79 % (3918777)Termination phase: Saturation % 103.98/15.79 % (3918777)Time elapsed: 0.570 s % 103.98/15.79 % (3918777)Peak memory usage: 114 MB % 103.98/15.79 % (3918777)Instructions burned: 541 (million) % 103.98/15.79 % (3918778)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 103.98/15.79 % (3918778)------------------------------ % 103.98/15.79 % (3918778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.98/15.79 % (3918778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.98/15.79 % (3918778)CaDiCaL version: 2.1.3 % 103.98/15.79 % (3918778)Termination reason: Unknown % 103.98/15.79 % (3918778)Termination phase: Saturation % 103.98/15.79 % (3918778)Time elapsed: 0.590 s % 103.98/15.79 % (3918778)Peak memory usage: 113 MB % 103.98/15.79 % (3918778)Instructions burned: 541 (million) % 103.98/15.79 % (3918786)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2285255880:i=1884:sd=1:nm=60:ss=axioms_2887 on theBenchmark for (2887ds/1884Mi) % 103.98/15.79 % (3918789)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=2161150268:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2885 on theBenchmark for (2885ds/2037Mi) % 103.98/15.79 % (3918788)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3089252616:cts=off:i=5469:bs=on:fsr=off_2885 on theBenchmark for (2885ds/5469Mi) % 103.98/15.79 % (3918785)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 103.98/15.79 % (3918785)------------------------------ % 103.98/15.79 % (3918785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.98/15.79 % (3918785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.98/15.79 % (3918785)CaDiCaL version: 2.1.3 % 103.98/15.79 % (3918785)Termination reason: Unknown % 103.98/15.79 % (3918785)Termination phase: Saturation % 103.98/15.79 % (3918785)Time elapsed: 0.604 s % 103.98/15.79 % (3918785)Peak memory usage: 114 MB % 103.98/15.79 % (3918785)Instructions burned: 542 (million) % 103.98/15.79 % (3918786)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 103.98/15.79 % (3918786)------------------------------ % 103.98/15.79 % (3918786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.98/15.79 % (3918786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.98/15.79 % (3918786)CaDiCaL version: 2.1.3 % 103.98/15.79 % (3918786)Termination reason: Unknown % 103.98/15.79 % (3918786)Termination phase: Saturation % 103.98/15.79 % (3918786)Time elapsed: 0.605 s % 103.98/15.79 % (3918786)Peak memory usage: 113 MB % 103.98/15.79 % (3918786)Instructions burned: 539 (million) % 103.98/15.79 % (3918793)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4262290681:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2880 on theBenchmark for (2880ds/2110Mi) % 103.98/15.79 % (3918789)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 103.98/15.79 % (3918789)------------------------------ % 103.98/15.79 % (3918789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.98/15.79 % (3918789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.98/15.79 % (3918789)CaDiCaL version: 2.1.3 % 103.98/15.79 % (3918789)Termination reason: Unknown % 103.98/15.79 % (3918789)Termination phase: Saturation % 103.98/15.79 % (3918789)Time elapsed: 0.619 s % 103.98/15.79 % (3918789)Peak memory usage: 114 MB % 103.98/15.79 % (3918789)Instructions burned: 548 (million) % 103.98/15.79 % (3918794)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=2712224635:i=2430:add=off:aac=none:nm=16_2879 on theBenchmark for (2879ds/2430Mi) % 103.98/15.79 % (3918796)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=3383939800:cond=fast:i=4891_2876 on theBenchmark for (2876ds/4891Mi) % 103.98/15.79 % (3918793)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 103.98/15.79 % (3918793)------------------------------ % 103.98/15.79 % (3918793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.98/15.79 % (3918793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.98/15.79 % (3918793)CaDiCaL version: 2.1.3 % 103.98/15.79 % (3918793)Termination reason: Unknown % 103.98/15.79 % (3918793)Termination phase: Saturation % 112.32/17.00 % (3918793)Time elapsed: 0.608 s % 112.32/17.00 % (3918793)Peak memory usage: 114 MB % 112.32/17.00 % (3918793)Instructions burned: 546 (million) % 112.32/17.00 % (3918794)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 112.32/17.00 % (3918794)------------------------------ % 112.32/17.00 % (3918794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.32/17.00 % (3918794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.32/17.00 % (3918794)CaDiCaL version: 2.1.3 % 112.32/17.00 % (3918794)Termination reason: Unknown % 112.32/17.00 % (3918794)Termination phase: Saturation % 112.32/17.00 % (3918794)Time elapsed: 0.601 s % 112.32/17.00 % (3918794)Peak memory usage: 114 MB % 112.32/17.00 % (3918794)Instructions burned: 541 (million) % 112.32/17.00 % (3918801)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=3574509837:st=2:i=14845:sd=2:ss=included:fsd=on_2871 on theBenchmark for (2871ds/14845Mi) % 112.32/17.00 % (3918748)Instruction limit reached! % 112.32/17.00 % (3918748)------------------------------ % 112.32/17.00 % (3918748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.32/17.00 % (3918748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.32/17.00 % (3918748)CaDiCaL version: 2.1.3 % 112.32/17.00 % (3918748)Termination reason: Instruction limit % 112.32/17.00 % (3918748)Termination phase: Saturation % 112.32/17.00 % (3918748)Time elapsed: 5.487 s % 112.32/17.00 % (3918748)Peak memory usage: 155 MB % 112.32/17.00 % (3918748)Instructions burned: 6226 (million) % 112.32/17.00 % (3918796)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 112.32/17.00 % (3918796)------------------------------ % 112.32/17.00 % (3918796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.32/17.00 % (3918796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.32/17.00 % (3918796)CaDiCaL version: 2.1.3 % 112.32/17.00 % (3918796)Termination reason: Unknown % 112.32/17.00 % (3918796)Termination phase: Saturation % 112.32/17.00 % (3918796)Time elapsed: 0.618 s % 112.32/17.00 % (3918796)Peak memory usage: 114 MB % 112.32/17.00 % (3918796)Instructions burned: 542 (million) % 112.32/17.00 % (3918802)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3255939933:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2870 on theBenchmark for (2870ds/7534Mi) % 112.32/17.00 % (3918804)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=122596353:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2868 on theBenchmark for (2868ds/10353Mi) % 112.32/17.00 % (3918805)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1834768787:i=7860_2867 on theBenchmark for (2867ds/7860Mi) % 112.32/17.00 % (3918805)Refutation not found, incomplete strategy % 112.32/17.00 % (3918805)------------------------------ % 112.32/17.00 % (3918805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.32/17.00 % (3918805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.32/17.00 % (3918805)CaDiCaL version: 2.1.3 % 112.32/17.00 % (3918805)Termination reason: Refutation not found, incomplete strategy % 112.32/17.00 % (3918805)Time elapsed: 0.012 s % 112.32/17.00 % (3918805)Peak memory usage: 88 MB % 112.32/17.00 % (3918805)Instructions burned: 11 (million) % 112.32/17.00 % (3918801)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 112.32/17.00 % (3918801)------------------------------ % 112.32/17.00 % (3918801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.32/17.00 % (3918801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.32/17.00 % (3918801)CaDiCaL version: 2.1.3 % 112.32/17.00 % (3918801)Termination reason: Unknown % 112.32/17.00 % (3918801)Termination phase: Saturation % 112.32/17.00 % (3918801)Time elapsed: 0.602 s % 112.32/17.00 % (3918801)Peak memory usage: 114 MB % 112.32/17.00 % (3918801)Instructions burned: 541 (million) % 112.32/17.00 % (3918802)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 112.32/17.00 % (3918802)------------------------------ % 112.32/17.00 % (3918802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.32/17.00 % (3918802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.07/18.16 % (3918802)CaDiCaL version: 2.1.3 % 122.07/18.16 % (3918802)Termination reason: Unknown % 122.07/18.16 % (3918802)Termination phase: Saturation % 122.07/18.16 % (3918802)Time elapsed: 0.608 s % 122.07/18.16 % (3918802)Peak memory usage: 113 MB % 122.07/18.16 % (3918802)Instructions burned: 544 (million) % 122.07/18.16 % (3918805)------------------------------ % 122.07/18.16 % (3918805)------------------------------ % 122.07/18.16 % (3918804)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 122.07/18.16 % (3918804)------------------------------ % 122.07/18.16 % (3918804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.07/18.16 % (3918804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.07/18.16 % (3918804)CaDiCaL version: 2.1.3 % 122.07/18.16 % (3918804)Termination reason: Unknown % 122.07/18.16 % (3918804)Termination phase: Saturation % 122.07/18.16 % (3918804)Time elapsed: 0.606 s % 122.07/18.16 % (3918804)Peak memory usage: 113 MB % 122.07/18.16 % (3918804)Instructions burned: 541 (million) % 122.07/18.16 % (3918809)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=3904792069:i=7896:sd=2:bs=on:ss=included:sgt=20_2862 on theBenchmark for (2862ds/7896Mi) % 122.07/18.16 % (3918810)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1306160378:i=5812:gtgl=2:gtg=all_2860 on theBenchmark for (2860ds/5812Mi) % 122.07/18.16 % (3918811)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=1714163461:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2860 on theBenchmark for (2860ds/2965Mi) % 122.07/18.16 % (3918813)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=2116283754:i=2967:kws=precedence:bd=preordered:av=off_2859 on theBenchmark for (2859ds/2967Mi) % 122.07/18.16 % (3918809)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 122.07/18.16 % (3918809)------------------------------ % 122.07/18.16 % (3918809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.07/18.16 % (3918809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.07/18.16 % (3918809)CaDiCaL version: 2.1.3 % 122.07/18.16 % (3918809)Termination reason: Unknown % 122.07/18.16 % (3918809)Termination phase: Saturation % 122.07/18.16 % (3918809)Time elapsed: 0.616 s % 122.07/18.16 % (3918809)Peak memory usage: 114 MB % 122.07/18.16 % (3918809)Instructions burned: 541 (million) % 122.07/18.16 % (3918810)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 122.07/18.16 % (3918810)------------------------------ % 122.07/18.16 % (3918810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.07/18.16 % (3918810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.07/18.16 % (3918810)CaDiCaL version: 2.1.3 % 122.07/18.16 % (3918810)Termination reason: Unknown % 122.07/18.16 % (3918810)Termination phase: Saturation % 122.07/18.16 % (3918810)Time elapsed: 0.608 s % 122.07/18.16 % (3918810)Peak memory usage: 114 MB % 122.07/18.16 % (3918810)Instructions burned: 544 (million) % 122.07/18.16 % (3918811)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 122.07/18.16 % (3918811)------------------------------ % 122.07/18.16 % (3918811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.07/18.16 % (3918811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.07/18.16 % (3918811)CaDiCaL version: 2.1.3 % 122.07/18.16 % (3918811)Termination reason: Unknown % 122.07/18.16 % (3918811)Termination phase: Saturation % 122.07/18.16 % (3918811)Time elapsed: 0.600 s % 122.07/18.16 % (3918811)Peak memory usage: 113 MB % 122.07/18.16 % (3918811)Instructions burned: 542 (million) % 122.07/18.16 % (3918813)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 122.07/18.16 % (3918813)------------------------------ % 122.07/18.16 % (3918813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.07/18.16 % (3918813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.07/18.16 % (3918813)CaDiCaL version: 2.1.3 % 122.07/18.16 % (3918813)Termination reason: Unknown % 122.07/18.16 % (3918813)Termination phase: Saturation % 122.07/18.16 % (3918813)Time elapsed: 0.605 s % 122.07/18.16 % (3918813)Peak memory usage: 114 MB % 122.07/18.16 % (3918813)Instructions burned: 541 (million) % 122.07/18.16 % (3918817)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=2509849662:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2853 on theBenchmark for (2853ds/3022Mi) % 130.00/19.32 % (3918818)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=490054512:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2852 on theBenchmark for (2852ds/3207Mi) % 130.00/19.32 % (3918819)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1000234318:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2851 on theBenchmark for (2851ds/3289Mi) % 130.00/19.32 % (3918820)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2379983603:i=38569:sd=3:ss=axioms:sgt=32_2850 on theBenchmark for (2850ds/38569Mi) % 130.00/19.32 % (3918817)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.00/19.32 % (3918817)------------------------------ % 130.00/19.32 % (3918817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.00/19.32 % (3918817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.00/19.32 % (3918817)CaDiCaL version: 2.1.3 % 130.00/19.32 % (3918817)Termination reason: Unknown % 130.00/19.32 % (3918817)Termination phase: Saturation % 130.00/19.32 % (3918817)Time elapsed: 0.620 s % 130.00/19.32 % (3918817)Peak memory usage: 113 MB % 130.00/19.32 % (3918817)Instructions burned: 542 (million) % 130.00/19.32 % (3918818)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.00/19.32 % (3918819)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.00/19.32 % (3918819)------------------------------ % 130.00/19.32 % (3918819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.00/19.32 % (3918818)------------------------------ % 130.00/19.32 % (3918818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.00/19.32 % (3918819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.00/19.32 % (3918818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.00/19.32 % (3918818)CaDiCaL version: 2.1.3 % 130.00/19.32 % (3918819)CaDiCaL version: 2.1.3 % 130.00/19.32 % (3918819)Termination reason: Unknown % 130.00/19.32 % (3918819)Termination phase: Saturation % 130.00/19.32 % (3918819)Time elapsed: 0.617 s % 130.00/19.32 % (3918818)Termination reason: Unknown % 130.00/19.32 % (3918818)Termination phase: Saturation % 130.00/19.32 % (3918818)Time elapsed: 0.668 s % 130.00/19.32 % (3918819)Peak memory usage: 113 MB % 130.00/19.32 % (3918818)Peak memory usage: 113 MB % 130.00/19.32 % (3918819)Instructions burned: 542 (million) % 130.00/19.32 % (3918818)Instructions burned: 540 (million) % 130.00/19.32 % (3918825)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3864552838:cts=off:i=3394_2844 on theBenchmark for (2844ds/3394Mi) % 130.00/19.32 % (3918820)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.00/19.32 % (3918820)------------------------------ % 130.00/19.32 % (3918820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.00/19.32 % (3918820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.00/19.32 % (3918820)CaDiCaL version: 2.1.3 % 130.00/19.32 % (3918820)Termination reason: Unknown % 130.00/19.32 % (3918820)Termination phase: Saturation % 130.00/19.32 % (3918820)Time elapsed: 0.609 s % 130.00/19.32 % (3918820)Peak memory usage: 113 MB % 130.00/19.32 % (3918820)Instructions burned: 542 (million) % 130.00/19.32 % (3918827)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=3421833560:i=20684:bd=all:gtg=exists_sym_2842 on theBenchmark for (2842ds/20684Mi) % 130.00/19.32 % (3918826)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=2792497556:i=33824:bd=preordered_2842 on theBenchmark for (2842ds/33824Mi) % 130.00/19.32 % (3918829)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=3505265535: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_2841 on theBenchmark for (2841ds/7222Mi) % 130.00/19.32 % (3918829)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 137.65/20.50 % (3918825)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.65/20.50 % (3918825)------------------------------ % 137.65/20.50 % (3918825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.65/20.50 % (3918825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.65/20.50 % (3918825)CaDiCaL version: 2.1.3 % 137.65/20.50 % (3918825)Termination reason: Unknown % 137.65/20.50 % (3918825)Termination phase: Saturation % 137.65/20.50 % (3918825)Time elapsed: 0.615 s % 137.65/20.50 % (3918825)Peak memory usage: 113 MB % 137.65/20.50 % (3918825)Instructions burned: 541 (million) % 137.65/20.50 % (3918833)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1450690992:st=4:i=7295:sd=4:ep=R:ss=axioms_2835 on theBenchmark for (2835ds/7295Mi) % 137.65/20.50 % (3918827)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.65/20.50 % (3918827)------------------------------ % 137.65/20.50 % (3918827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.65/20.50 % (3918827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.65/20.50 % (3918827)CaDiCaL version: 2.1.3 % 137.65/20.50 % (3918827)Termination reason: Unknown % 137.65/20.50 % (3918827)Termination phase: Saturation % 137.65/20.50 % (3918827)Time elapsed: 0.694 s % 137.65/20.50 % (3918827)Peak memory usage: 113 MB % 137.65/20.50 % (3918827)Instructions burned: 544 (million) % 137.65/20.50 % (3918826)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.65/20.50 % (3918826)------------------------------ % 137.65/20.50 % (3918826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.65/20.50 % (3918826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.65/20.50 % (3918826)CaDiCaL version: 2.1.3 % 137.65/20.50 % (3918826)Termination reason: Unknown % 137.65/20.50 % (3918826)Termination phase: Saturation % 137.65/20.50 % (3918826)Time elapsed: 0.599 s % 137.65/20.50 % (3918826)Peak memory usage: 114 MB % 137.65/20.50 % (3918826)Instructions burned: 541 (million) % 137.65/20.50 % (3918829)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.65/20.50 % (3918829)------------------------------ % 137.65/20.50 % (3918829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.65/20.50 % (3918829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.65/20.50 % (3918829)CaDiCaL version: 2.1.3 % 137.65/20.50 % (3918829)Termination reason: Unknown % 137.65/20.50 % (3918829)Termination phase: Saturation % 137.65/20.50 % (3918829)Time elapsed: 0.714 s % 137.65/20.50 % (3918829)Peak memory usage: 114 MB % 137.65/20.50 % (3918829)Instructions burned: 548 (million) % 137.65/20.50 % (3918835)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=2056179875:i=4036:ins=10_2833 on theBenchmark for (2833ds/4036Mi) % 137.65/20.50 % (3918836)lrs+10_1_sil=128000:lcm=predicate:random_seed=1181072589:st=3:i=43697:sd=5:ss=axioms_2833 on theBenchmark for (2833ds/43697Mi) % 137.65/20.50 % (3918837)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=953399526:i=17599:gtg=all:ss=axioms:fsd=on_2831 on theBenchmark for (2831ds/17599Mi) % 137.65/20.50 % (3918833)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.65/20.50 % (3918833)------------------------------ % 137.65/20.50 % (3918833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.65/20.50 % (3918833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.65/20.50 % (3918833)CaDiCaL version: 2.1.3 % 137.65/20.50 % (3918833)Termination reason: Unknown % 137.65/20.50 % (3918833)Termination phase: Saturation % 137.65/20.50 % (3918833)Time elapsed: 0.608 s % 137.65/20.50 % (3918833)Peak memory usage: 113 MB % 137.65/20.50 % (3918833)Instructions burned: 545 (million) % 137.65/20.50 % (3918788)Instruction limit reached! % 137.65/20.50 % (3918788)------------------------------ % 137.65/20.50 % (3918788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.65/20.50 % (3918788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.65/20.50 % (3918788)CaDiCaL version: 2.1.3 % 137.65/20.50 % (3918788)Termination reason: Instruction limit % 137.65/20.50 % (3918788)Termination phase: Saturation % 137.65/20.50 % (3918788)Time elapsed: 5.569 s % 137.65/20.50 % (3918788)Peak memory usage: 111 MB % 151.26/22.33 % (3918788)Instructions burned: 5469 (million) % 151.26/22.33 % (3918841)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=2904259704:i=4547:bd=preordered_2827 on theBenchmark for (2827ds/4547Mi) % 151.26/22.33 % (3918835)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 151.26/22.33 % (3918835)------------------------------ % 151.26/22.33 % (3918835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.26/22.33 % (3918835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.26/22.33 % (3918835)CaDiCaL version: 2.1.3 % 151.26/22.33 % (3918835)Termination reason: Unknown % 151.26/22.33 % (3918835)Termination phase: Saturation % 151.26/22.33 % (3918835)Time elapsed: 0.602 s % 151.26/22.33 % (3918835)Peak memory usage: 113 MB % 151.26/22.33 % (3918835)Instructions burned: 540 (million) % 151.26/22.33 % (3918842)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=4027393049:i=9294:av=off_2826 on theBenchmark for (2826ds/9294Mi) % 151.26/22.33 % (3918837)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 151.26/22.33 % (3918837)------------------------------ % 151.26/22.33 % (3918837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.26/22.33 % (3918837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.26/22.33 % (3918837)CaDiCaL version: 2.1.3 % 151.26/22.33 % (3918837)Termination reason: Unknown % 151.26/22.33 % (3918837)Termination phase: Saturation % 151.26/22.33 % (3918837)Time elapsed: 0.617 s % 151.26/22.33 % (3918837)Peak memory usage: 114 MB % 151.26/22.33 % (3918837)Instructions burned: 544 (million) % 151.26/22.33 % (3918846)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2185082082:i=32849:add=on_2824 on theBenchmark for (2824ds/32849Mi) % 151.26/22.33 % (3918848)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2856707934:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2822 on theBenchmark for (2822ds/4793Mi) % 151.26/22.33 % (3918841)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 151.26/22.33 % (3918841)------------------------------ % 151.26/22.33 % (3918841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.26/22.33 % (3918841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.26/22.33 % (3918841)CaDiCaL version: 2.1.3 % 151.26/22.33 % (3918841)Termination reason: Unknown % 151.26/22.33 % (3918841)Termination phase: Saturation % 151.26/22.33 % (3918841)Time elapsed: 0.566 s % 151.26/22.33 % (3918841)Peak memory usage: 114 MB % 151.26/22.33 % (3918841)Instructions burned: 541 (million) % 151.26/22.33 % (3918842)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 151.26/22.33 % (3918842)------------------------------ % 151.26/22.33 % (3918842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.26/22.33 % (3918842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.26/22.33 % (3918842)CaDiCaL version: 2.1.3 % 151.26/22.33 % (3918842)Termination reason: Unknown % 151.26/22.33 % (3918842)Termination phase: Saturation % 151.26/22.33 % (3918842)Time elapsed: 0.595 s % 151.26/22.33 % (3918842)Peak memory usage: 114 MB % 151.26/22.33 % (3918842)Instructions burned: 541 (million) % 151.26/22.33 % (3918851)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=1864424956:i=4840:nm=4:av=off_2819 on theBenchmark for (2819ds/4840Mi) % 151.26/22.33 % (3918846)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 151.26/22.33 % (3918846)------------------------------ % 151.26/22.33 % (3918846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.26/22.33 % (3918846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.26/22.33 % (3918846)CaDiCaL version: 2.1.3 % 151.26/22.33 % (3918846)Termination reason: Unknown % 151.26/22.33 % (3918846)Termination phase: Saturation % 151.26/22.33 % (3918846)Time elapsed: 0.595 s % 151.26/22.33 % (3918846)Peak memory usage: 113 MB % 151.26/22.33 % (3918846)Instructions burned: 541 (million) % 151.26/22.33 % (3918852)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=797293335:cts=off:i=5002_2817 on theBenchmark for (2817ds/5002Mi) % 173.61/25.45 % (3918848)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.61/25.45 % (3918848)------------------------------ % 173.61/25.45 % (3918848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.61/25.45 % (3918848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.61/25.45 % (3918848)CaDiCaL version: 2.1.3 % 173.61/25.45 % (3918848)Termination reason: Unknown % 173.61/25.45 % (3918848)Termination phase: Saturation % 173.61/25.45 % (3918848)Time elapsed: 0.605 s % 173.61/25.45 % (3918848)Peak memory usage: 113 MB % 173.61/25.45 % (3918848)Instructions burned: 541 (million) % 173.61/25.45 % (3918854)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=1193473294:i=30479:sd=3:ss=axioms_2815 on theBenchmark for (2815ds/30479Mi) % 173.61/25.45 % (3918856)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=1586556687:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2814 on theBenchmark for (2814ds/11035Mi) % 173.61/25.45 % (3918856)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 173.61/25.45 % (3918851)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.61/25.45 % (3918851)------------------------------ % 173.61/25.45 % (3918851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.61/25.45 % (3918851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.61/25.45 % (3918851)CaDiCaL version: 2.1.3 % 173.61/25.45 % (3918851)Termination reason: Unknown % 173.61/25.45 % (3918851)Termination phase: Saturation % 173.61/25.45 % (3918851)Time elapsed: 0.562 s % 173.61/25.45 % (3918851)Peak memory usage: 113 MB % 173.61/25.45 % (3918851)Instructions burned: 541 (million) % 173.61/25.45 % (3918852)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.61/25.45 % (3918852)------------------------------ % 173.61/25.45 % (3918852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.61/25.45 % (3918852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.61/25.45 % (3918852)CaDiCaL version: 2.1.3 % 173.61/25.45 % (3918852)Termination reason: Unknown % 173.61/25.45 % (3918852)Termination phase: Saturation % 173.61/25.45 % (3918852)Time elapsed: 0.595 s % 173.61/25.45 % (3918852)Peak memory usage: 113 MB % 173.61/25.45 % (3918852)Instructions burned: 541 (million) % 173.61/25.45 % (3918859)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1101872486:i=5835_2810 on theBenchmark for (2810ds/5835Mi) % 173.61/25.45 % (3918854)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.61/25.45 % (3918854)------------------------------ % 173.61/25.45 % (3918854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.61/25.45 % (3918854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.61/25.45 % (3918854)CaDiCaL version: 2.1.3 % 173.61/25.45 % (3918854)Termination reason: Unknown % 173.61/25.45 % (3918854)Termination phase: Saturation % 173.61/25.45 % (3918854)Time elapsed: 0.602 s % 173.61/25.45 % (3918854)Peak memory usage: 113 MB % 173.61/25.45 % (3918854)Instructions burned: 540 (million) % 173.61/25.45 % (3918860)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2888403992:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2809 on theBenchmark for (2809ds/5890Mi) % 173.61/25.45 % (3918856)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.61/25.45 % (3918856)------------------------------ % 173.61/25.45 % (3918856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.61/25.45 % (3918856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.61/25.45 % (3918856)CaDiCaL version: 2.1.3 % 173.61/25.45 % (3918856)Termination reason: Unknown % 173.61/25.45 % (3918856)Termination phase: Saturation % 173.61/25.45 % (3918856)Time elapsed: 0.595 s % 173.61/25.45 % (3918856)Peak memory usage: 114 MB % 173.61/25.45 % (3918856)Instructions burned: 543 (million) % 173.61/25.45 % (3918862)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2549951507:cts=off:i=19910:ep=RS_2806 on theBenchmark for (2806ds/19910Mi) % 173.61/25.45 % (3918864)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=947723941:i=20312:bd=preordered:fsr=off:er=filter_2806 on theBenchmark for (2806ds/20312Mi) % 211.06/30.73 % (3918859)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.06/30.73 % (3918859)------------------------------ % 211.06/30.73 % (3918859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.06/30.73 % (3918859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.06/30.73 % (3918859)CaDiCaL version: 2.1.3 % 211.06/30.73 % (3918859)Termination reason: Unknown % 211.06/30.73 % (3918859)Termination phase: Saturation % 211.06/30.73 % (3918859)Time elapsed: 0.572 s % 211.06/30.73 % (3918859)Peak memory usage: 113 MB % 211.06/30.73 % (3918859)Instructions burned: 542 (million) % 211.06/30.73 % (3918860)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.06/30.73 % (3918860)------------------------------ % 211.06/30.73 % (3918860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.06/30.73 % (3918860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.06/30.73 % (3918860)CaDiCaL version: 2.1.3 % 211.06/30.73 % (3918860)Termination reason: Unknown % 211.06/30.73 % (3918860)Termination phase: Saturation % 211.06/30.73 % (3918860)Time elapsed: 0.605 s % 211.06/30.73 % (3918860)Peak memory usage: 114 MB % 211.06/30.73 % (3918860)Instructions burned: 542 (million) % 211.06/30.73 % (3918867)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=2714099916:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2802 on theBenchmark for (2802ds/13822Mi) % 211.06/30.73 % (3918864)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.06/30.73 % (3918864)------------------------------ % 211.06/30.73 % (3918864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.06/30.73 % (3918864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.06/30.73 % (3918864)CaDiCaL version: 2.1.3 % 211.06/30.73 % (3918864)Termination reason: Unknown % 211.06/30.73 % (3918864)Termination phase: Saturation % 211.06/30.73 % (3918864)Time elapsed: 0.615 s % 211.06/30.73 % (3918864)Peak memory usage: 113 MB % 211.06/30.73 % (3918864)Instructions burned: 541 (million) % 211.06/30.73 % (3918868)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=1913743801:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2800 on theBenchmark for (2800ds/7144Mi) % 211.06/30.73 % (3918870)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=1677320310:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2797 on theBenchmark for (2797ds/15184Mi) % 211.06/30.73 % (3918867)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.06/30.73 % (3918867)------------------------------ % 211.06/30.73 % (3918867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.06/30.73 % (3918867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.06/30.73 % (3918867)CaDiCaL version: 2.1.3 % 211.06/30.73 % (3918867)Termination reason: Unknown % 211.06/30.73 % (3918867)Termination phase: Saturation % 211.06/30.73 % (3918867)Time elapsed: 0.571 s % 211.06/30.73 % (3918867)Peak memory usage: 114 MB % 211.06/30.73 % (3918867)Instructions burned: 542 (million) % 211.06/30.73 % (3918873)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=594324714:i=107375_2793 on theBenchmark for (2793ds/107375Mi) % 211.06/30.73 % (3918870)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.06/30.73 % (3918870)------------------------------ % 211.06/30.73 % (3918870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.06/30.73 % (3918870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.06/30.73 % (3918870)CaDiCaL version: 2.1.3 % 211.06/30.73 % (3918870)Termination reason: Unknown % 211.06/30.73 % (3918870)Termination phase: Saturation % 211.06/30.73 % (3918870)Time elapsed: 0.609 s % 211.06/30.73 % (3918870)Peak memory usage: 114 MB % 211.06/30.73 % (3918870)Instructions burned: 541 (million) % 211.06/30.73 % (3918875)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=4149114176:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2788 on theBenchmark for (2788ds/7958Mi) % 223.81/32.53 % (3918873)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 223.81/32.53 % (3918873)------------------------------ % 223.81/32.53 % (3918873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.81/32.53 % (3918873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.81/32.53 % (3918873)CaDiCaL version: 2.1.3 % 223.81/32.53 % (3918873)Termination reason: Unknown % 223.81/32.53 % (3918873)Termination phase: Saturation % 223.81/32.53 % (3918873)Time elapsed: 0.571 s % 223.81/32.53 % (3918873)Peak memory usage: 113 MB % 223.81/32.53 % (3918873)Instructions burned: 542 (million) % 223.81/32.53 % (3918877)dis+10_128_sil=16000:nwc=0.7:random_seed=859717660:i=15999:nm=2:gsp=on_2784 on theBenchmark for (2784ds/15999Mi) % 223.81/32.53 % (3918877)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 223.81/32.53 % (3918875)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 223.81/32.53 % (3918875)------------------------------ % 223.81/32.53 % (3918875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.81/32.53 % (3918875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.81/32.53 % (3918875)CaDiCaL version: 2.1.3 % 223.81/32.53 % (3918875)Termination reason: Unknown % 223.81/32.53 % (3918875)Termination phase: Saturation % 223.81/32.53 % (3918875)Time elapsed: 0.608 s % 223.81/32.53 % (3918875)Peak memory usage: 114 MB % 223.81/32.53 % (3918875)Instructions burned: 541 (million) % 223.81/32.53 % (3918879)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=782246685:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2779 on theBenchmark for (2779ds/8139Mi) % 223.81/32.53 % (3918763)Instruction limit reached! % 223.81/32.53 % (3918763)------------------------------ % 223.81/32.53 % (3918763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.81/32.53 % (3918763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.81/32.53 % (3918763)CaDiCaL version: 2.1.3 % 223.81/32.53 % (3918763)Termination reason: Instruction limit % 223.81/32.53 % (3918763)Termination phase: Saturation % 223.81/32.53 % (3918763)Time elapsed: 13.472 s % 223.81/32.53 % (3918763)Peak memory usage: 551 MB % 223.81/32.53 % (3918763)Instructions burned: 26474 (million) % 223.81/32.53 % (3918881)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=2529482562:st=4:i=8950:sd=5:ss=axioms_2771 on theBenchmark for (2771ds/8950Mi) % 223.81/32.53 % (3918881)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 223.81/32.53 % (3918881)------------------------------ % 223.81/32.53 % (3918881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.81/32.53 % (3918881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.81/32.53 % (3918881)CaDiCaL version: 2.1.3 % 223.81/32.53 % (3918881)Termination reason: Unknown % 223.81/32.53 % (3918881)Termination phase: Saturation % 223.81/32.53 % (3918881)Time elapsed: 0.328 s % 223.81/32.53 % (3918881)Peak memory usage: 114 MB % 223.81/32.53 % (3918881)Instructions burned: 542 (million) % 223.81/32.53 % (3918883)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=206551549:i=9809:ins=10:av=off_2765 on theBenchmark for (2765ds/9809Mi) % 223.81/32.53 % (3918883)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 223.81/32.53 % (3918883)------------------------------ % 223.81/32.53 % (3918883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.81/32.53 % (3918883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.81/32.53 % (3918883)CaDiCaL version: 2.1.3 % 223.81/32.53 % (3918883)Termination reason: Unknown % 223.81/32.53 % (3918883)Termination phase: Saturation % 223.81/32.53 % (3918883)Time elapsed: 0.329 s % 223.81/32.53 % (3918883)Peak memory usage: 114 MB % 223.81/32.53 % (3918883)Instructions burned: 543 (million) % 223.81/32.53 % (3918885)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=3309271592:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2759 on theBenchmark for (2759ds/9885Mi) % 223.81/32.53 % (3918885)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 223.81/32.53 % (3918885)------------------------------ % 223.81/32.53 % (3918885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.81/32.53 % (3918885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.97/39.55 % (3918885)CaDiCaL version: 2.1.3 % 273.97/39.55 % (3918885)Termination reason: Unknown % 273.97/39.55 % (3918885)Termination phase: Saturation % 273.97/39.55 % (3918885)Time elapsed: 0.329 s % 273.97/39.55 % (3918885)Peak memory usage: 113 MB % 273.97/39.55 % (3918885)Instructions burned: 542 (million) % 273.97/39.55 % (3918887)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1703006462:cond=fast:i=32078:fgj=on:av=off_2754 on theBenchmark for (2754ds/32078Mi) % 273.97/39.55 % (3918887)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 273.97/39.55 % (3918887)------------------------------ % 273.97/39.55 % (3918887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.97/39.55 % (3918887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.97/39.55 % (3918887)CaDiCaL version: 2.1.3 % 273.97/39.55 % (3918887)Termination reason: Unknown % 273.97/39.55 % (3918887)Termination phase: Saturation % 273.97/39.55 % (3918887)Time elapsed: 0.295 s % 273.97/39.55 % (3918887)Peak memory usage: 114 MB % 273.97/39.55 % (3918887)Instructions burned: 541 (million) % 273.97/39.55 % (3918891)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=622264065:i=11101:bd=all:ss=axioms:sgt=8_2748 on theBenchmark for (2748ds/11101Mi) % 273.97/39.55 % (3918868)Instruction limit reached! % 273.97/39.55 % (3918868)------------------------------ % 273.97/39.55 % (3918868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.97/39.55 % (3918868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.97/39.55 % (3918868)CaDiCaL version: 2.1.3 % 273.97/39.55 % (3918868)Termination reason: Instruction limit % 273.97/39.55 % (3918868)Termination phase: Saturation % 273.97/39.55 % (3918868)Time elapsed: 6.882 s % 273.97/39.55 % (3918868)Peak memory usage: 152 MB % 273.97/39.55 % (3918868)Instructions burned: 7144 (million) % 273.97/39.55 % (3918899)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3181102494:cond=on:i=13220:s2at=3:aac=none:fsd=on_2728 on theBenchmark for (2728ds/13220Mi) % 273.97/39.55 % (3918899)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 273.97/39.55 % (3918899)------------------------------ % 273.97/39.55 % (3918899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.97/39.55 % (3918899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.97/39.55 % (3918899)CaDiCaL version: 2.1.3 % 273.97/39.55 % (3918899)Termination reason: Unknown % 273.97/39.55 % (3918899)Termination phase: Saturation % 273.97/39.55 % (3918899)Time elapsed: 0.603 s % 273.97/39.55 % (3918899)Peak memory usage: 114 MB % 273.97/39.55 % (3918899)Instructions burned: 543 (million) % 273.97/39.55 % (3918901)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=706845206:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2719 on theBenchmark for (2719ds/13528Mi) % 273.97/39.55 % (3918901)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 273.97/39.55 % (3918901)------------------------------ % 273.97/39.55 % (3918901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.97/39.55 % (3918901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.97/39.55 % (3918901)CaDiCaL version: 2.1.3 % 273.97/39.55 % (3918901)Termination reason: Unknown % 273.97/39.55 % (3918901)Termination phase: Saturation % 273.97/39.55 % (3918901)Time elapsed: 0.606 s % 273.97/39.55 % (3918901)Peak memory usage: 113 MB % 273.97/39.55 % (3918901)Instructions burned: 544 (million) % 273.97/39.55 % (3918903)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=865627321:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2709 on theBenchmark for (2709ds/14854Mi) % 273.97/39.55 % (3918879)Instruction limit reached! % 273.97/39.55 % (3918879)------------------------------ % 273.97/39.55 % (3918879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.97/39.55 % (3918879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.97/39.55 % (3918879)CaDiCaL version: 2.1.3 % 273.97/39.55 % (3918879)Termination reason: Instruction limit % 273.97/39.55 % (3918879)Termination phase: Saturation % 273.97/39.55 % (3918879)Time elapsed: 7.224 s % 273.97/39.55 % (3918879)Peak memory usage: 112 MB % 273.97/39.55 % (3918879)Instructions burned: 8139 (million) % 273.97/39.55 % (3918919)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=2848038737:i=14974:ss=axioms:sgt=16_2703 on theBenchmark for (2703ds/14974Mi) % 299.12/43.09 % (3918903)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 299.12/43.09 % (3918903)------------------------------ % 299.12/43.09 % (3918903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.12/43.09 % (3918903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.12/43.09 % (3918903)CaDiCaL version: 2.1.3 % 299.12/43.09 % (3918903)Termination reason: Unknown % 299.12/43.09 % (3918903)Termination phase: Saturation % 299.12/43.09 % (3918903)Time elapsed: 0.615 s % 299.12/43.09 % (3918903)Peak memory usage: 114 MB % 299.12/43.09 % (3918903)Instructions burned: 552 (million) % 299.12/43.09 % (3918921)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=1448985766:i=33081:aac=none:fgj=on:bd=all:fsr=off_2700 on theBenchmark for (2700ds/33081Mi) % 299.12/43.09 % (3918919)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 299.12/43.09 % (3918919)------------------------------ % 299.12/43.09 % (3918919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.12/43.09 % (3918919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.12/43.09 % (3918919)CaDiCaL version: 2.1.3 % 299.12/43.09 % (3918919)Termination reason: Unknown % 299.12/43.09 % (3918919)Termination phase: Saturation % 299.12/43.09 % (3918919)Time elapsed: 0.579 s % 299.12/43.09 % (3918919)Peak memory usage: 113 MB % 299.12/43.09 % (3918919)Instructions burned: 541 (million) % 299.12/43.09 % (3918925)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=4051623131:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2695 on theBenchmark for (2695ds/50856Mi) % 299.12/43.09 % (3918921)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 299.12/43.09 % (3918921)------------------------------ % 299.12/43.09 % (3918921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.12/43.09 % (3918921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.12/43.09 % (3918921)CaDiCaL version: 2.1.3 % 299.12/43.09 % (3918921)Termination reason: Unknown % 299.12/43.09 % (3918921)Termination phase: Saturation % 299.12/43.09 % (3918921)Time elapsed: 0.603 s % 299.12/43.09 % (3918921)Peak memory usage: 114 MB % 299.12/43.09 % (3918921)Instructions burned: 541 (million) % 299.12/43.09 % (3918891)Instruction limit reached! % 299.12/43.09 % (3918891)------------------------------ % 299.12/43.09 % (3918891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.12/43.09 % (3918891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.12/43.09 % (3918891)CaDiCaL version: 2.1.3 % 299.12/43.09 % (3918891)Termination reason: Instruction limit % 299.12/43.09 % (3918891)Termination phase: Saturation % 299.12/43.09 % (3918891)Time elapsed: 5.736 s % 299.12/43.09 % (3918891)Peak memory usage: 169 MB % 299.12/43.09 % (3918891)Instructions burned: 11101 (million) % 299.12/43.09 % (3918927)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=1586891713:i=69865_2691 on theBenchmark for (2691ds/69865Mi) % 299.12/43.09 % (3918925)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 299.12/43.09 % (3918925)------------------------------ % 299.12/43.09 % (3918925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.12/43.09 % (3918925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.12/43.09 % (3918925)CaDiCaL version: 2.1.3 % 299.12/43.09 % (3918925)Termination reason: Unknown % 299.12/43.09 % (3918925)Termination phase: Saturation % 299.12/43.09 % (3918925)Time elapsed: 0.590 s % 299.12/43.09 % (3918925)Peak memory usage: 114 MB % 299.12/43.09 % (3918925)Instructions burned: 542 (million) % 299.12/43.09 % (3918928)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=749403129:cond=fast:i=17802:gtgl=3:gtg=all_2688 on theBenchmark for (2688ds/17802Mi) % 299.12/43.09 % (3918930)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3063118286:i=96644_2686 on theBenchmark for (2686ds/96644Mi) % 299.12/43.09 % (3918928)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 299.12/43.09 % (3918Terminated %------------------------------------------------------------------------------