%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW501_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 : n020.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 01:30:42 PM UTC 2026 % Result : Timeout 299.92s 43.29s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW501_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.23 % Computer : n020.cluster.edu % 0.09/0.23 % Model : x86_64 x86_64 % 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.23 % Memory : 8046.5625MB % 0.09/0.23 % OS : Linux 6.8.0-71-generic % 0.09/0.23 % CPULimit : 300 % 0.09/0.23 % WCLimit : 300 % 0.09/0.23 % DateTime : Mon Sep 28 14:16:04 UTC 2026 % 0.09/0.23 % CPUTime : % 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.24/0.29 Running first-order theorem proving % 0.24/0.29 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 % 10.11/2.41 % (188103)Detected formulas, will run a generic FOF schedule. % 10.11/2.41 % (188109)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=1063126006:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.11/2.41 % (188113)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1521540597:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.11/2.41 % (188112)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4228457974:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.11/2.41 % (188114)dis-21_1_sil=8000:lcm=predicate:random_seed=26933159: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) % 10.11/2.41 % (188110)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=75345830:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.11/2.41 % (188111)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1076728643:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.11/2.41 % (188111)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.11/2.41 % (188111)Refutation not found, incomplete strategy % 10.11/2.41 % (188111)------------------------------ % 10.11/2.41 % (188111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.41 % (188111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.41 % (188111)CaDiCaL version: 2.1.3 % 10.11/2.41 % (188111)Termination reason: Refutation not found, incomplete strategy % 10.11/2.41 % (188111)Time elapsed: 0.003 s % 10.11/2.41 % (188111)Peak memory usage: 88 MB % 10.11/2.41 % (188112)Refutation not found, incomplete strategy % 10.11/2.41 % (188112)------------------------------ % 10.11/2.41 % (188112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.41 % (188111)Instructions burned: 1 (million) % 10.11/2.41 % (188112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.41 % (188112)CaDiCaL version: 2.1.3 % 10.11/2.41 % (188112)Termination reason: Refutation not found, incomplete strategy % 10.11/2.41 % (188112)Time elapsed: 0.003 s % 10.11/2.41 % (188112)Peak memory usage: 88 MB % 10.11/2.41 % (188112)Instructions burned: 1 (million) % 10.11/2.41 % (188110)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.11/2.41 % (188113)Instruction limit reached! % 10.11/2.41 % (188113)------------------------------ % 10.11/2.41 % (188113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.41 % (188113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.41 % (188113)CaDiCaL version: 2.1.3 % 10.11/2.41 % (188113)Termination reason: Instruction limit % 10.11/2.41 % (188113)Termination phase: Saturation % 10.11/2.41 % (188113)Time elapsed: 0.136 s % 10.11/2.41 % (188113)Peak memory usage: 90 MB % 10.11/2.41 % (188113)Instructions burned: 139 (million) % 10.11/2.41 % (188108)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=299117630:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.11/2.41 % (188114)Instruction limit reached! % 10.11/2.41 % (188114)------------------------------ % 10.11/2.41 % (188114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.41 % (188114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.41 % (188114)CaDiCaL version: 2.1.3 % 10.11/2.41 % (188114)Termination reason: Instruction limit % 10.11/2.41 % (188114)Termination phase: Saturation % 10.11/2.41 % (188114)Time elapsed: 0.100 s % 10.11/2.41 % (188114)Peak memory usage: 89 MB % 10.11/2.41 % (188114)Instructions burned: 129 (million) % 10.11/2.41 % (188109)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.11/2.41 % (188109)------------------------------ % 10.11/2.41 % (188109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.11/2.41 % (188109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.11/2.41 % (188109)CaDiCaL version: 2.1.3 % 10.11/2.41 % (188109)Termination reason: Unknown % 10.11/2.41 % (188109)Termination phase: Saturation % 10.11/2.41 % (188109)Time elapsed: 0.313 s % 10.11/2.41 % (188109)Peak memory usage: 114 MB % 11.88/2.86 % (188109)Instructions burned: 546 (million) % 11.88/2.86 % (188121)lrs+10_1_sil=8000:sp=occurrence:random_seed=211355095:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 11.88/2.86 % (188121)Refutation not found, incomplete strategy % 11.88/2.86 % (188121)------------------------------ % 11.88/2.86 % (188121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.86 % (188121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.86 % (188121)CaDiCaL version: 2.1.3 % 11.88/2.86 % (188121)Termination reason: Refutation not found, incomplete strategy % 11.88/2.86 % (188121)Time elapsed: 0.005 s % 11.88/2.86 % (188121)Peak memory usage: 88 MB % 11.88/2.86 % (188121)Instructions burned: 2 (million) % 11.88/2.86 % (188123)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1196562384:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 11.88/2.86 % (188111)------------------------------ % 11.88/2.86 % (188111)------------------------------ % 11.88/2.86 % (188112)------------------------------ % 11.88/2.86 % (188112)------------------------------ % 11.88/2.86 % (188124)lrs+1011_1_sil=32000:sp=occurrence:random_seed=876451839:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 11.88/2.86 % (188124)Refutation not found, incomplete strategy % 11.88/2.86 % (188124)------------------------------ % 11.88/2.86 % (188124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.86 % (188124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.86 % (188124)CaDiCaL version: 2.1.3 % 11.88/2.86 % (188124)Termination reason: Refutation not found, incomplete strategy % 11.88/2.86 % (188124)Time elapsed: 0.003 s % 11.88/2.86 % (188124)Peak memory usage: 89 MB % 11.88/2.86 % (188124)Instructions burned: 3 (million) % 11.88/2.86 % (188123)Instruction limit reached! % 11.88/2.86 % (188123)------------------------------ % 11.88/2.86 % (188123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.86 % (188123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.86 % (188123)CaDiCaL version: 2.1.3 % 11.88/2.86 % (188123)Termination reason: Instruction limit % 11.88/2.86 % (188123)Termination phase: Saturation % 11.88/2.86 % (188123)Time elapsed: 0.117 s % 11.88/2.86 % (188123)Peak memory usage: 89 MB % 11.88/2.86 % (188123)Instructions burned: 158 (million) % 11.88/2.86 % (188110)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.88/2.86 % (188110)------------------------------ % 11.88/2.86 % (188110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.86 % (188110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.86 % (188110)CaDiCaL version: 2.1.3 % 11.88/2.86 % (188110)Termination reason: Unknown % 11.88/2.86 % (188110)Termination phase: Saturation % 11.88/2.86 % (188110)Time elapsed: 0.562 s % 11.88/2.86 % (188110)Peak memory usage: 114 MB % 11.88/2.86 % (188110)Instructions burned: 542 (million) % 11.88/2.86 % (188127)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=1153914771:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi) % 11.88/2.86 % (188108)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.88/2.86 % (188108)------------------------------ % 11.88/2.86 % (188108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.86 % (188108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.86 % (188108)CaDiCaL version: 2.1.3 % 11.88/2.86 % (188108)Termination reason: Unknown % 11.88/2.86 % (188108)Termination phase: Saturation % 11.88/2.86 % (188108)Time elapsed: 0.595 s % 11.88/2.86 % (188108)Peak memory usage: 113 MB % 11.88/2.86 % (188108)Instructions burned: 541 (million) % 11.88/2.86 % (188124)------------------------------ % 11.88/2.86 % (188124)------------------------------ % 11.88/2.86 % (188130)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=63060093:i=2350_2992 on theBenchmark for (2992ds/2350Mi) % 11.88/2.86 % (188121)------------------------------ % 11.88/2.86 % (188121)------------------------------ % 11.88/2.86 % (188128)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=632171470:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 11.88/2.86 % (188131)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3522238808:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi) % 16.45/3.29 % (188127)Instruction limit reached! % 16.45/3.29 % (188127)------------------------------ % 16.45/3.29 % (188127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.45/3.29 % (188127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.45/3.29 % (188127)CaDiCaL version: 2.1.3 % 16.45/3.29 % (188127)Termination reason: Instruction limit % 16.45/3.29 % (188127)Termination phase: Saturation % 16.45/3.29 % (188127)Time elapsed: 0.192 s % 16.45/3.29 % (188127)Peak memory usage: 89 MB % 16.45/3.29 % (188127)Instructions burned: 249 (million) % 16.45/3.29 % (188131)Instruction limit reached! % 16.45/3.29 % (188131)------------------------------ % 16.45/3.29 % (188131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.45/3.29 % (188131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.45/3.29 % (188131)CaDiCaL version: 2.1.3 % 16.45/3.29 % (188131)Termination reason: Instruction limit % 16.45/3.29 % (188131)Termination phase: Saturation % 16.45/3.29 % (188131)Time elapsed: 0.094 s % 16.45/3.29 % (188131)Peak memory usage: 91 MB % 16.45/3.29 % (188131)Instructions burned: 113 (million) % 16.45/3.29 % (188133)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3729022358:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi) % 16.45/3.29 % (188133)Instruction limit reached! % 16.45/3.29 % (188133)------------------------------ % 16.45/3.29 % (188133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.45/3.29 % (188133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.45/3.29 % (188133)CaDiCaL version: 2.1.3 % 16.45/3.29 % (188133)Termination reason: Instruction limit % 16.45/3.29 % (188133)Termination phase: Saturation % 16.45/3.29 % (188133)Time elapsed: 0.053 s % 16.45/3.29 % (188133)Peak memory usage: 88 MB % 16.45/3.29 % (188133)Instructions burned: 129 (million) % 16.45/3.29 % (188134)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2761922005:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi) % 16.45/3.29 % (188128)Instruction limit reached! % 16.45/3.29 % (188128)------------------------------ % 16.45/3.29 % (188128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.45/3.29 % (188128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.45/3.29 % (188128)CaDiCaL version: 2.1.3 % 16.45/3.29 % (188128)Termination reason: Instruction limit % 16.45/3.29 % (188128)Termination phase: Saturation % 16.45/3.29 % (188128)Time elapsed: 0.270 s % 16.45/3.29 % (188128)Peak memory usage: 91 MB % 16.45/3.29 % (188128)Instructions burned: 295 (million) % 16.45/3.29 % (188137)lrs+10_1_sil=8000:sp=occurrence:random_seed=2727854773:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 16.45/3.29 % (188139)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1595494460:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 16.45/3.29 % (188134)Instruction limit reached! % 16.45/3.29 % (188134)------------------------------ % 16.45/3.29 % (188134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.45/3.29 % (188134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.45/3.29 % (188134)CaDiCaL version: 2.1.3 % 16.45/3.29 % (188134)Termination reason: Instruction limit % 16.45/3.29 % (188134)Termination phase: Saturation % 16.45/3.29 % (188134)Time elapsed: 0.114 s % 16.45/3.29 % (188134)Peak memory usage: 88 MB % 16.45/3.29 % (188134)Instructions burned: 114 (million) % 16.45/3.29 % (188140)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=423353481:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 16.45/3.29 % (188142)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=307244335:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 16.45/3.29 % (188145)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1913410478:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi) % 16.45/3.29 % (188145)Refutation not found, incomplete strategy % 16.45/3.29 % (188145)------------------------------ % 16.45/3.29 % (188145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.45/3.29 % (188145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.45/3.29 % (188145)CaDiCaL version: 2.1.3 % 16.45/3.29 % (188145)Termination reason: Refutation not found, incomplete strategy % 16.45/3.29 % (188145)Time elapsed: 0.006 s % 18.90/3.83 % (188145)Peak memory usage: 88 MB % 18.90/3.83 % (188145)Instructions burned: 10 (million) % 18.90/3.83 % (188130)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.90/3.83 % (188130)------------------------------ % 18.90/3.83 % (188130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.83 % (188130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.83 % (188130)CaDiCaL version: 2.1.3 % 18.90/3.83 % (188130)Termination reason: Unknown % 18.90/3.83 % (188130)Termination phase: Saturation % 18.90/3.83 % (188130)Time elapsed: 0.554 s % 18.90/3.83 % (188130)Peak memory usage: 113 MB % 18.90/3.83 % (188130)Instructions burned: 541 (million) % 18.90/3.83 % (188142)Instruction limit reached! % 18.90/3.83 % (188142)------------------------------ % 18.90/3.83 % (188142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.83 % (188142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.83 % (188142)CaDiCaL version: 2.1.3 % 18.90/3.83 % (188142)Termination reason: Instruction limit % 18.90/3.83 % (188142)Termination phase: Saturation % 18.90/3.83 % (188142)Time elapsed: 0.132 s % 18.90/3.83 % (188142)Peak memory usage: 90 MB % 18.90/3.83 % (188142)Instructions burned: 134 (million) % 18.90/3.83 % (188149)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3507826177:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 18.90/3.83 % (188139)Instruction limit reached! % 18.90/3.83 % (188139)------------------------------ % 18.90/3.83 % (188139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.83 % (188139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.83 % (188139)CaDiCaL version: 2.1.3 % 18.90/3.83 % (188139)Termination reason: Instruction limit % 18.90/3.83 % (188139)Termination phase: Saturation % 18.90/3.83 % (188139)Time elapsed: 0.322 s % 18.90/3.83 % (188139)Peak memory usage: 89 MB % 18.90/3.83 % (188139)Instructions burned: 438 (million) % 18.90/3.83 % (188145)------------------------------ % 18.90/3.83 % (188145)------------------------------ % 18.90/3.83 % (188153)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=272504396:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi) % 18.90/3.83 % (188153)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.90/3.83 % (188153)Instruction limit reached! % 18.90/3.83 % (188153)------------------------------ % 18.90/3.83 % (188153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.83 % (188153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.83 % (188153)CaDiCaL version: 2.1.3 % 18.90/3.83 % (188153)Termination reason: Instruction limit % 18.90/3.83 % (188153)Termination phase: Saturation % 18.90/3.83 % (188153)Time elapsed: 0.079 s % 18.90/3.83 % (188153)Peak memory usage: 90 MB % 18.90/3.83 % (188153)Instructions burned: 125 (million) % 18.90/3.83 % (188154)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=163088827:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi) % 18.90/3.83 % (188156)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3861334079:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi) % 18.90/3.83 % (188140)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.90/3.83 % (188140)------------------------------ % 18.90/3.83 % (188140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.83 % (188140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.83 % (188140)CaDiCaL version: 2.1.3 % 18.90/3.83 % (188140)Termination reason: Unknown % 18.90/3.83 % (188140)Termination phase: Saturation % 18.90/3.83 % (188140)Time elapsed: 0.564 s % 18.90/3.83 % (188140)Peak memory usage: 113 MB % 18.90/3.83 % (188140)Instructions burned: 539 (million) % 18.90/3.83 % (188156)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.90/3.83 % (188156)Refutation not found, incomplete strategy % 18.90/3.83 % (188156)------------------------------ % 18.90/3.83 % (188156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.90/3.83 % (188156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.90/3.83 % (188156)CaDiCaL version: 2.1.3 % 25.56/4.74 % (188156)Termination reason: Refutation not found, incomplete strategy % 25.56/4.74 % (188156)Time elapsed: 0.003 s % 25.56/4.74 % (188156)Peak memory usage: 88 MB % 25.56/4.74 % (188156)Instructions burned: 1 (million) % 25.56/4.74 % (188154)Instruction limit reached! % 25.56/4.74 % (188154)------------------------------ % 25.56/4.74 % (188154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.56/4.74 % (188154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.56/4.74 % (188154)CaDiCaL version: 2.1.3 % 25.56/4.74 % (188154)Termination reason: Instruction limit % 25.56/4.74 % (188154)Termination phase: Saturation % 25.56/4.74 % (188154)Time elapsed: 0.122 s % 25.56/4.74 % (188154)Peak memory usage: 90 MB % 25.56/4.74 % (188154)Instructions burned: 134 (million) % 25.56/4.74 % (188157)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1428261853:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi) % 25.56/4.74 % (188159)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=1355910263:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi) % 25.56/4.74 % (188137)Instruction limit reached! % 25.56/4.74 % (188137)------------------------------ % 25.56/4.74 % (188137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.56/4.74 % (188137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.56/4.74 % (188137)CaDiCaL version: 2.1.3 % 25.56/4.74 % (188137)Termination reason: Instruction limit % 25.56/4.74 % (188137)Termination phase: Saturation % 25.56/4.74 % (188137)Time elapsed: 0.769 s % 25.56/4.74 % (188137)Peak memory usage: 100 MB % 25.56/4.74 % (188137)Instructions burned: 908 (million) % 25.56/4.74 % (188162)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=523208848:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi) % 25.56/4.74 % (188162)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 25.56/4.74 % (188162)Instruction limit reached! % 25.56/4.74 % (188162)------------------------------ % 25.56/4.74 % (188162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.56/4.74 % (188162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.56/4.74 % (188162)CaDiCaL version: 2.1.3 % 25.56/4.74 % (188162)Termination reason: Instruction limit % 25.56/4.74 % (188162)Termination phase: Saturation % 25.56/4.74 % (188162)Time elapsed: 0.044 s % 25.56/4.74 % (188162)Peak memory usage: 90 MB % 25.56/4.74 % (188162)Instructions burned: 151 (million) % 25.56/4.74 % (188149)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.56/4.74 % (188149)------------------------------ % 25.56/4.74 % (188149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.56/4.74 % (188149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.56/4.74 % (188149)CaDiCaL version: 2.1.3 % 25.56/4.74 % (188149)Termination reason: Unknown % 25.56/4.74 % (188149)Termination phase: Saturation % 25.56/4.74 % (188149)Time elapsed: 0.597 s % 25.56/4.74 % (188149)Peak memory usage: 114 MB % 25.56/4.74 % (188149)Instructions burned: 539 (million) % 25.56/4.74 % (188165)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=670837025:i=14155:bd=all_2980 on theBenchmark for (2980ds/14155Mi) % 25.56/4.74 % (188170)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=4033154997:s2a=on:i=185:s2at=1.8:fdi=4_2978 on theBenchmark for (2978ds/185Mi) % 25.56/4.74 % (188168)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=946157181:i=667:av=off:fsr=off_2979 on theBenchmark for (2979ds/667Mi) % 25.56/4.74 % (188156)------------------------------ % 25.56/4.74 % (188156)------------------------------ % 25.56/4.74 % (188157)Instruction limit reached! % 25.56/4.74 % (188157)------------------------------ % 25.56/4.74 % (188157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.56/4.74 % (188157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.56/4.74 % (188157)CaDiCaL version: 2.1.3 % 25.56/4.74 % (188157)Termination reason: Instruction limit % 25.56/4.74 % (188157)Termination phase: Saturation % 32.67/5.62 % (188157)Time elapsed: 0.373 s % 32.67/5.62 % (188157)Peak memory usage: 92 MB % 32.67/5.62 % (188157)Instructions burned: 431 (million) % 32.67/5.62 % (188171)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3608140712:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2977 on theBenchmark for (2977ds/193Mi) % 32.67/5.62 % (188171)Refutation not found, incomplete strategy % 32.67/5.62 % (188171)------------------------------ % 32.67/5.62 % (188171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.67/5.62 % (188171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.67/5.62 % (188171)CaDiCaL version: 2.1.3 % 32.67/5.62 % (188171)Termination reason: Refutation not found, incomplete strategy % 32.67/5.62 % (188171)Time elapsed: 0.004 s % 32.67/5.62 % (188171)Peak memory usage: 88 MB % 32.67/5.62 % (188171)Instructions burned: 2 (million) % 32.67/5.62 % (188170)Instruction limit reached! % 32.67/5.62 % (188170)------------------------------ % 32.67/5.62 % (188170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.67/5.62 % (188170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.67/5.62 % (188170)CaDiCaL version: 2.1.3 % 32.67/5.62 % (188170)Termination reason: Instruction limit % 32.67/5.62 % (188170)Termination phase: Saturation % 32.67/5.62 % (188170)Time elapsed: 0.096 s % 32.67/5.62 % (188170)Peak memory usage: 91 MB % 32.67/5.62 % (188170)Instructions burned: 186 (million) % 32.67/5.62 % (188159)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.67/5.62 % (188159)------------------------------ % 32.67/5.62 % (188159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.67/5.62 % (188159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.67/5.62 % (188159)CaDiCaL version: 2.1.3 % 32.67/5.62 % (188159)Termination reason: Unknown % 32.67/5.62 % (188159)Termination phase: Saturation % 32.67/5.62 % (188159)Time elapsed: 0.529 s % 32.67/5.62 % (188159)Peak memory usage: 114 MB % 32.67/5.62 % (188159)Instructions burned: 541 (million) % 32.67/5.62 % (188176)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1093644553:i=12111:sd=1:ss=included_2976 on theBenchmark for (2976ds/12111Mi) % 32.67/5.62 % (188175)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3500914543:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2976 on theBenchmark for (2976ds/4850Mi) % 32.67/5.62 % (188178)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=210259294:i=319:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/319Mi) % 32.67/5.62 % (188179)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2489722620:i=2064:ep=RST_2974 on theBenchmark for (2974ds/2064Mi) % 32.67/5.62 % (188179)Refutation not found, incomplete strategy % 32.67/5.62 % (188179)------------------------------ % 32.67/5.62 % (188179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.67/5.62 % (188179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.67/5.62 % (188179)CaDiCaL version: 2.1.3 % 32.67/5.62 % (188179)Termination reason: Refutation not found, incomplete strategy % 32.67/5.62 % (188179)Time elapsed: 0.006 s % 32.67/5.62 % (188179)Peak memory usage: 88 MB % 32.67/5.62 % (188179)Instructions burned: 10 (million) % 32.67/5.62 % (188171)------------------------------ % 32.67/5.62 % (188171)------------------------------ % 32.67/5.62 % (188165)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.67/5.62 % (188165)------------------------------ % 32.67/5.62 % (188165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.67/5.62 % (188165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.67/5.62 % (188165)CaDiCaL version: 2.1.3 % 32.67/5.62 % (188165)Termination reason: Unknown % 32.67/5.62 % (188165)Termination phase: Saturation % 32.67/5.62 % (188165)Time elapsed: 0.554 s % 32.67/5.62 % (188165)Peak memory usage: 114 MB % 32.67/5.62 % (188165)Instructions burned: 541 (million) % 32.67/5.62 % (188168)Instruction limit reached! % 32.67/5.62 % (188168)------------------------------ % 32.67/5.62 % (188168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.67/5.62 % (188168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.67/5.62 % (188168)CaDiCaL version: 2.1.3 % 32.67/5.62 % (188168)Termination reason: Instruction limit % 32.67/5.62 % (188168)Termination phase: Saturation % 32.67/5.62 % (188168)Time elapsed: 0.591 s % 40.86/6.81 % (188168)Peak memory usage: 90 MB % 40.86/6.81 % (188168)Instructions burned: 667 (million) % 40.86/6.81 % (188184)dis-1011_128_sil=32000:random_seed=423446909:i=3706:ep=RST:av=off_2972 on theBenchmark for (2972ds/3706Mi) % 40.86/6.81 % (188178)Instruction limit reached! % 40.86/6.81 % (188178)------------------------------ % 40.86/6.81 % (188178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.86/6.81 % (188178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.86/6.81 % (188178)CaDiCaL version: 2.1.3 % 40.86/6.81 % (188178)Termination reason: Instruction limit % 40.86/6.81 % (188178)Termination phase: Saturation % 40.86/6.81 % (188178)Time elapsed: 0.328 s % 40.86/6.81 % (188178)Peak memory usage: 92 MB % 40.86/6.81 % (188178)Instructions burned: 319 (million) % 40.86/6.81 % (188185)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3532854878:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2971 on theBenchmark for (2971ds/757Mi) % 40.86/6.81 % (188179)------------------------------ % 40.86/6.81 % (188179)------------------------------ % 40.86/6.81 % (188176)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.86/6.81 % (188176)------------------------------ % 40.86/6.81 % (188176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.86/6.81 % (188176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.86/6.81 % (188176)CaDiCaL version: 2.1.3 % 40.86/6.81 % (188176)Termination reason: Unknown % 40.86/6.81 % (188176)Termination phase: Saturation % 40.86/6.81 % (188176)Time elapsed: 0.567 s % 40.86/6.81 % (188176)Peak memory usage: 113 MB % 40.86/6.81 % (188176)Instructions burned: 542 (million) % 40.86/6.81 % (188186)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1417075798:i=13913:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/13913Mi) % 40.86/6.81 % (188188)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3740747834:i=9925:aac=none_2969 on theBenchmark for (2969ds/9925Mi) % 40.86/6.81 % (188185)Instruction limit reached! % 40.86/6.81 % (188185)------------------------------ % 40.86/6.81 % (188185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.86/6.81 % (188185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.86/6.81 % (188185)CaDiCaL version: 2.1.3 % 40.86/6.81 % (188185)Termination reason: Instruction limit % 40.86/6.81 % (188185)Termination phase: Saturation % 40.86/6.81 % (188185)Time elapsed: 0.314 s % 40.86/6.81 % (188185)Peak memory usage: 91 MB % 40.86/6.81 % (188185)Instructions burned: 759 (million) % 40.86/6.81 % (188190)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2284337263:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/2479Mi) % 40.86/6.81 % (188190)Refutation not found, incomplete strategy % 40.86/6.81 % (188190)------------------------------ % 40.86/6.81 % (188190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.86/6.81 % (188190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.86/6.81 % (188190)CaDiCaL version: 2.1.3 % 40.86/6.81 % (188190)Termination reason: Refutation not found, incomplete strategy % 40.86/6.81 % (188190)Time elapsed: 0.004 s % 40.86/6.81 % (188190)Peak memory usage: 88 MB % 40.86/6.81 % (188190)Instructions burned: 2 (million) % 40.86/6.81 % (188191)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1879658814:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2968 on theBenchmark for (2968ds/440Mi) % 40.86/6.81 % (188191)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 40.86/6.81 % (188194)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3182888729:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2966 on theBenchmark for (2966ds/11145Mi) % 40.86/6.81 % (188190)------------------------------ % 40.86/6.81 % (188190)------------------------------ % 40.86/6.81 % (188186)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.86/6.81 % (188186)------------------------------ % 40.86/6.81 % (188186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.86/6.81 % (188186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.86/6.81 % (188186)CaDiCaL version: 2.1.3 % 40.86/6.81 % (188186)Termination reason: Unknown % 40.86/6.81 % (188186)Termination phase: Saturation % 50.77/8.09 % (188186)Time elapsed: 0.605 s % 50.77/8.09 % (188186)Peak memory usage: 113 MB % 50.77/8.09 % (188186)Instructions burned: 537 (million) % 50.77/8.09 % (188191)Instruction limit reached! % 50.77/8.09 % (188191)------------------------------ % 50.77/8.09 % (188191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.77/8.09 % (188191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.77/8.09 % (188191)CaDiCaL version: 2.1.3 % 50.77/8.09 % (188191)Termination reason: Instruction limit % 50.77/8.09 % (188191)Termination phase: Saturation % 50.77/8.09 % (188191)Time elapsed: 0.421 s % 50.77/8.09 % (188191)Peak memory usage: 92 MB % 50.77/8.09 % (188191)Instructions burned: 442 (million) % 50.77/8.09 % (188194)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 50.77/8.09 % (188194)------------------------------ % 50.77/8.09 % (188194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.77/8.09 % (188194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.77/8.09 % (188194)CaDiCaL version: 2.1.3 % 50.77/8.09 % (188194)Termination reason: Unknown % 50.77/8.09 % (188194)Termination phase: Saturation % 50.77/8.09 % (188194)Time elapsed: 0.301 s % 50.77/8.09 % (188194)Peak memory usage: 113 MB % 50.77/8.09 % (188194)Instructions burned: 537 (million) % 50.77/8.09 % (188188)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 50.77/8.09 % (188188)------------------------------ % 50.77/8.09 % (188188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.77/8.09 % (188188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.77/8.09 % (188188)CaDiCaL version: 2.1.3 % 50.77/8.09 % (188188)Termination reason: Unknown % 50.77/8.09 % (188188)Termination phase: Saturation % 50.77/8.09 % (188188)Time elapsed: 0.595 s % 50.77/8.09 % (188188)Peak memory usage: 114 MB % 50.77/8.09 % (188188)Instructions burned: 540 (million) % 50.77/8.09 % (188201)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=411757302:i=14123:bd=preordered:ins=4_2961 on theBenchmark for (2961ds/14123Mi) % 50.77/8.09 % (188198)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=4227663446:cts=off:i=3034:av=off:er=known:fsd=on_2961 on theBenchmark for (2961ds/3034Mi) % 50.77/8.09 % (188199)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3461511290:st=2:s2a=on:i=524:s2at=2:ss=axioms_2961 on theBenchmark for (2961ds/524Mi) % 50.77/8.09 % (188202)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=4006724082:i=5781:kws=precedence:bd=all:rawr=on_2960 on theBenchmark for (2960ds/5781Mi) % 50.77/8.09 % (188200)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=913355692:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2961 on theBenchmark for (2961ds/1016Mi) % 50.77/8.09 % (188199)Instruction limit reached! % 50.77/8.09 % (188199)------------------------------ % 50.77/8.09 % (188199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.77/8.09 % (188199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.77/8.09 % (188199)CaDiCaL version: 2.1.3 % 50.77/8.09 % (188199)Termination reason: Instruction limit % 50.77/8.09 % (188199)Termination phase: Saturation % 50.77/8.09 % (188199)Time elapsed: 0.447 s % 50.77/8.09 % (188199)Peak memory usage: 91 MB % 50.77/8.09 % (188199)Instructions burned: 525 (million) % 50.77/8.09 % (188201)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 50.77/8.09 % (188201)------------------------------ % 50.77/8.09 % (188201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.77/8.09 % (188201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.77/8.09 % (188201)CaDiCaL version: 2.1.3 % 50.77/8.09 % (188201)Termination reason: Unknown % 50.77/8.09 % (188201)Termination phase: Saturation % 50.77/8.09 % (188201)Time elapsed: 0.604 s % 50.77/8.09 % (188201)Peak memory usage: 113 MB % 50.77/8.09 % (188201)Instructions burned: 541 (million) % 50.77/8.09 % (188198)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 50.77/8.09 % (188198)------------------------------ % 50.77/8.09 % (188198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.77/8.09 % (188198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.77/8.09 % (188198)CaDiCaL version: 2.1.3 % 50.77/8.09 % (188198)Termination reason: Unknown % 56.24/9.01 % (188198)Termination phase: Saturation % 56.24/9.01 % (188198)Time elapsed: 0.604 s % 56.24/9.01 % (188198)Peak memory usage: 113 MB % 56.24/9.01 % (188198)Instructions burned: 542 (million) % 56.24/9.01 % (188208)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=1142635312:i=2448:gtgl=5:bd=preordered:gtg=all_2954 on theBenchmark for (2954ds/2448Mi) % 56.24/9.01 % (188200)Instruction limit reached! % 56.24/9.01 % (188200)------------------------------ % 56.24/9.01 % (188200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.24/9.01 % (188200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.24/9.01 % (188200)CaDiCaL version: 2.1.3 % 56.24/9.01 % (188200)Termination reason: Instruction limit % 56.24/9.01 % (188200)Termination phase: Saturation % 56.24/9.01 % (188200)Time elapsed: 0.747 s % 56.24/9.01 % (188200)Peak memory usage: 91 MB % 56.24/9.01 % (188200)Instructions burned: 1016 (million) % 56.24/9.01 % (188210)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=595395910:st=5.6:i=2033:sd=3:ss=axioms_2953 on theBenchmark for (2953ds/2033Mi) % 56.24/9.01 % (188209)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=845539166:i=3223:kws=precedence:fgj=on:av=off_2953 on theBenchmark for (2953ds/3223Mi) % 56.24/9.01 % (188212)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4091404974:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2951 on theBenchmark for (2951ds/2055Mi) % 56.24/9.01 % (188208)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.24/9.01 % (188208)------------------------------ % 56.24/9.01 % (188208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.24/9.01 % (188208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.24/9.01 % (188208)CaDiCaL version: 2.1.3 % 56.24/9.01 % (188208)Termination reason: Unknown % 56.24/9.01 % (188208)Termination phase: Saturation % 56.24/9.01 % (188208)Time elapsed: 0.599 s % 56.24/9.01 % (188208)Peak memory usage: 114 MB % 56.24/9.01 % (188208)Instructions burned: 543 (million) % 56.24/9.01 % (188210)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.24/9.01 % (188210)------------------------------ % 56.24/9.01 % (188210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.24/9.01 % (188210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.24/9.01 % (188210)CaDiCaL version: 2.1.3 % 56.24/9.01 % (188210)Termination reason: Unknown % 56.24/9.01 % (188210)Termination phase: Saturation % 56.24/9.01 % (188210)Time elapsed: 0.544 s % 56.24/9.01 % (188210)Peak memory usage: 113 MB % 56.24/9.01 % (188210)Instructions burned: 541 (million) % 56.24/9.01 % (188209)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.24/9.01 % (188209)------------------------------ % 56.24/9.01 % (188209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.24/9.01 % (188209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.24/9.01 % (188209)CaDiCaL version: 2.1.3 % 56.24/9.01 % (188209)Termination reason: Unknown % 56.24/9.01 % (188209)Termination phase: Saturation % 56.24/9.01 % (188209)Time elapsed: 0.599 s % 56.24/9.01 % (188209)Peak memory usage: 114 MB % 56.24/9.01 % (188209)Instructions burned: 541 (million) % 56.24/9.01 % (188217)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1467972206:i=4835:sd=13:ss=axioms:sgt=23_2945 on theBenchmark for (2945ds/4835Mi) % 56.24/9.01 % (188216)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=3277810496:i=21611:sd=3:ss=axioms_2945 on theBenchmark for (2945ds/21611Mi) % 56.24/9.01 % (188212)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.24/9.01 % (188212)------------------------------ % 56.24/9.01 % (188212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.24/9.01 % (188212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.24/9.01 % (188212)CaDiCaL version: 2.1.3 % 56.24/9.01 % (188212)Termination reason: Unknown % 56.24/9.01 % (188212)Termination phase: Saturation % 56.24/9.01 % (188212)Time elapsed: 0.596 s % 56.24/9.01 % (188212)Peak memory usage: 113 MB % 56.24/9.01 % (188212)Instructions burned: 537 (million) % 56.24/9.01 % (188218)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=3035235429:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2944 on theBenchmark for (2944ds/797Mi) % 61.51/9.96 % (188221)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3007235314:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2942 on theBenchmark for (2942ds/2326Mi) % 61.51/9.96 % (188184)Instruction limit reached! % 61.51/9.96 % (188184)------------------------------ % 61.51/9.96 % (188184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.51/9.96 % (188184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.51/9.96 % (188184)CaDiCaL version: 2.1.3 % 61.51/9.96 % (188184)Termination reason: Instruction limit % 61.51/9.96 % (188184)Termination phase: Saturation % 61.51/9.96 % (188184)Time elapsed: 3.341 s % 61.51/9.96 % (188184)Peak memory usage: 126 MB % 61.51/9.96 % (188184)Instructions burned: 3706 (million) % 61.51/9.96 % (188216)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.51/9.96 % (188216)------------------------------ % 61.51/9.96 % (188216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.51/9.96 % (188216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.51/9.96 % (188216)CaDiCaL version: 2.1.3 % 61.51/9.96 % (188216)Termination reason: Unknown % 61.51/9.96 % (188216)Termination phase: Saturation % 61.51/9.96 % (188216)Time elapsed: 0.600 s % 61.51/9.96 % (188216)Peak memory usage: 113 MB % 61.51/9.96 % (188216)Instructions burned: 537 (million) % 61.51/9.96 % (188224)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=4100667891:i=6038:nm=6_2936 on theBenchmark for (2936ds/6038Mi) % 61.51/9.96 % (188202)Instruction limit reached! % 61.51/9.96 % (188202)------------------------------ % 61.51/9.96 % (188202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.51/9.96 % (188202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.51/9.96 % (188202)CaDiCaL version: 2.1.3 % 61.51/9.96 % (188202)Termination reason: Instruction limit % 61.51/9.96 % (188202)Termination phase: Saturation % 61.51/9.96 % (188202)Time elapsed: 2.518 s % 61.51/9.96 % (188202)Peak memory usage: 118 MB % 61.51/9.96 % (188202)Instructions burned: 5782 (million) % 61.51/9.96 % (188225)lrs+10_1_sil=32000:sp=occurrence:random_seed=3783165303:st=2:i=33334:sd=3:ss=included:sgt=32_2936 on theBenchmark for (2936ds/33334Mi) % 61.51/9.96 % (188218)Instruction limit reached! % 61.51/9.96 % (188218)------------------------------ % 61.51/9.96 % (188218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.51/9.96 % (188218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.51/9.96 % (188218)CaDiCaL version: 2.1.3 % 61.51/9.96 % (188218)Termination reason: Instruction limit % 61.51/9.96 % (188218)Termination phase: Saturation % 61.51/9.96 % (188218)Time elapsed: 0.810 s % 61.51/9.96 % (188218)Peak memory usage: 99 MB % 61.51/9.96 % (188218)Instructions burned: 797 (million) % 61.51/9.96 % (188228)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=4033336827:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2933 on theBenchmark for (2933ds/1008Mi) % 61.51/9.96 % (188175)Instruction limit reached! % 61.51/9.96 % (188175)------------------------------ % 61.51/9.96 % (188175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.51/9.96 % (188175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.51/9.96 % (188175)CaDiCaL version: 2.1.3 % 61.51/9.96 % (188175)Termination reason: Instruction limit % 61.51/9.96 % (188175)Termination phase: Saturation % 61.51/9.96 % (188175)Time elapsed: 4.339 s % 61.51/9.96 % (188175)Peak memory usage: 110 MB % 61.51/9.96 % (188175)Instructions burned: 4850 (million) % 61.51/9.96 % (188229)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=1369889167:i=8327:s2at=5:bd=preordered_2933 on theBenchmark for (2933ds/8327Mi) % 61.51/9.96 % (188224)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.51/9.96 % (188224)------------------------------ % 61.51/9.96 % (188224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.51/9.96 % (188224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.91 % (188224)CaDiCaL version: 2.1.3 % 69.07/10.91 % (188224)Termination reason: Unknown % 69.07/10.91 % (188224)Termination phase: Saturation % 69.07/10.91 % (188224)Time elapsed: 0.561 s % 69.07/10.91 % (188224)Peak memory usage: 114 MB % 69.07/10.91 % (188224)Instructions burned: 542 (million) % 69.07/10.91 % (188231)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=3858983208:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2930 on theBenchmark for (2930ds/1083Mi) % 69.07/10.91 % (188228)Instruction limit reached! % 69.07/10.91 % (188228)------------------------------ % 69.07/10.91 % (188228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.91 % (188228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.91 % (188228)CaDiCaL version: 2.1.3 % 69.07/10.91 % (188228)Termination reason: Instruction limit % 69.07/10.91 % (188228)Termination phase: Saturation % 69.07/10.91 % (188228)Time elapsed: 0.442 s % 69.07/10.91 % (188228)Peak memory usage: 95 MB % 69.07/10.91 % (188228)Instructions burned: 1009 (million) % 69.07/10.91 % (188233)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=274090579:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2928 on theBenchmark for (2928ds/1084Mi) % 69.07/10.91 % (188233)Refutation not found, incomplete strategy % 69.07/10.91 % (188233)------------------------------ % 69.07/10.91 % (188233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.91 % (188233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.91 % (188233)CaDiCaL version: 2.1.3 % 69.07/10.91 % (188233)Termination reason: Refutation not found, incomplete strategy % 69.07/10.91 % (188233)Time elapsed: 0.003 s % 69.07/10.91 % (188233)Peak memory usage: 88 MB % 69.07/10.91 % (188233)Instructions burned: 2 (million) % 69.07/10.91 % (188235)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1274685594:i=6995:s2at=5:gtg=all_2926 on theBenchmark for (2926ds/6995Mi) % 69.07/10.91 % (188229)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 69.07/10.91 % (188229)------------------------------ % 69.07/10.91 % (188229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.91 % (188229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.91 % (188229)CaDiCaL version: 2.1.3 % 69.07/10.91 % (188229)Termination reason: Unknown % 69.07/10.91 % (188229)Termination phase: Saturation % 69.07/10.91 % (188229)Time elapsed: 0.602 s % 69.07/10.91 % (188229)Peak memory usage: 114 MB % 69.07/10.91 % (188229)Instructions burned: 541 (million) % 69.07/10.91 % (188233)------------------------------ % 69.07/10.91 % (188233)------------------------------ % 69.07/10.91 % (188235)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 69.07/10.91 % (188235)------------------------------ % 69.07/10.91 % (188235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.91 % (188235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.91 % (188235)CaDiCaL version: 2.1.3 % 69.07/10.91 % (188235)Termination reason: Unknown % 69.07/10.91 % (188235)Termination phase: Saturation % 69.07/10.91 % (188235)Time elapsed: 0.306 s % 69.07/10.91 % (188235)Peak memory usage: 114 MB % 69.07/10.91 % (188235)Instructions burned: 545 (million) % 69.07/10.91 % (188238)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3224268923:st=2:i=6225:sd=15:ss=axioms_2923 on theBenchmark for (2923ds/6225Mi) % 69.07/10.91 % (188238)Refutation not found, incomplete strategy % 69.07/10.91 % (188238)------------------------------ % 69.07/10.91 % (188238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.07/10.91 % (188238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.07/10.91 % (188238)CaDiCaL version: 2.1.3 % 69.07/10.91 % (188238)Termination reason: Refutation not found, incomplete strategy % 69.07/10.91 % (188238)Time elapsed: 0.006 s % 69.07/10.91 % (188238)Peak memory usage: 88 MB % 69.07/10.91 % (188238)Instructions burned: 4 (million) % 69.07/10.91 % (188239)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=385648863:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2922 on theBenchmark for (2922ds/3372Mi) % 69.07/10.91 % (188240)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1046229824:st=2.3:i=26457:sd=10:ss=included:sgt=8_2921 on theBenchmark for (2921ds/26457Mi) % 75.20/11.73 % (188231)Instruction limit reached! % 75.20/11.73 % (188231)------------------------------ % 75.20/11.73 % (188231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.20/11.73 % (188231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.20/11.73 % (188231)CaDiCaL version: 2.1.3 % 75.20/11.73 % (188231)Termination reason: Instruction limit % 75.20/11.73 % (188231)Termination phase: Saturation % 75.20/11.73 % (188231)Time elapsed: 0.883 s % 75.20/11.73 % (188231)Peak memory usage: 96 MB % 75.20/11.73 % (188231)Instructions burned: 1083 (million) % 75.20/11.73 % (188238)------------------------------ % 75.20/11.73 % (188238)------------------------------ % 75.20/11.73 % (188221)Instruction limit reached! % 75.20/11.73 % (188221)------------------------------ % 75.20/11.73 % (188221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.20/11.73 % (188221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.20/11.73 % (188221)CaDiCaL version: 2.1.3 % 75.20/11.73 % (188221)Termination reason: Instruction limit % 75.20/11.73 % (188221)Termination phase: Saturation % 75.20/11.73 % (188221)Time elapsed: 2.276 s % 75.20/11.73 % (188221)Peak memory usage: 100 MB % 75.20/11.73 % (188221)Instructions burned: 2327 (million) % 75.20/11.73 % (188240)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.20/11.73 % (188240)------------------------------ % 75.20/11.73 % (188240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.20/11.73 % (188240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.20/11.73 % (188240)CaDiCaL version: 2.1.3 % 75.20/11.73 % (188240)Termination reason: Unknown % 75.20/11.73 % (188240)Termination phase: Saturation % 75.20/11.73 % (188240)Time elapsed: 0.307 s % 75.20/11.73 % (188240)Peak memory usage: 114 MB % 75.20/11.73 % (188240)Instructions burned: 542 (million) % 75.20/11.73 % (188244)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=1506045012:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2918 on theBenchmark for (2918ds/13494Mi) % 75.20/11.73 % (188245)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=3968743695:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2916 on theBenchmark for (2916ds/2503Mi) % 75.20/11.73 % (188245)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 75.20/11.73 % (188239)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.20/11.73 % (188239)------------------------------ % 75.20/11.73 % (188239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.20/11.73 % (188239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.20/11.73 % (188239)CaDiCaL version: 2.1.3 % 75.20/11.73 % (188239)Termination reason: Unknown % 75.20/11.73 % (188239)Termination phase: Saturation % 75.20/11.73 % (188239)Time elapsed: 0.552 s % 75.20/11.73 % (188239)Peak memory usage: 113 MB % 75.20/11.73 % (188239)Instructions burned: 538 (million) % 75.20/11.73 % (188247)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1575774650:i=30753:av=off:ss=included_2916 on theBenchmark for (2916ds/30753Mi) % 75.20/11.73 % (188246)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=830055700:i=2559:sd=1:ep=RSTC:ss=axioms_2916 on theBenchmark for (2916ds/2559Mi) % 75.20/11.73 % (188250)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3463978456:i=26473:ep=RSTC_2913 on theBenchmark for (2913ds/26473Mi) % 75.20/11.73 % (188247)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.20/11.73 % (188247)------------------------------ % 75.20/11.73 % (188247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.20/11.73 % (188247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.20/11.73 % (188247)CaDiCaL version: 2.1.3 % 75.20/11.73 % (188247)Termination reason: Unknown % 75.20/11.73 % (188247)Termination phase: Saturation % 75.20/11.73 % (188247)Time elapsed: 0.294 s % 75.20/11.73 % (188247)Peak memory usage: 114 MB % 75.20/11.73 % (188247)Instructions burned: 542 (million) % 75.20/11.73 % (188244)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.20/11.73 % (188244)------------------------------ % 75.20/11.73 % (188244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.61/12.71 % (188244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.61/12.71 % (188244)CaDiCaL version: 2.1.3 % 83.61/12.71 % (188244)Termination reason: Unknown % 83.61/12.71 % (188244)Termination phase: Saturation % 83.61/12.71 % (188244)Time elapsed: 0.604 s % 83.61/12.71 % (188244)Peak memory usage: 114 MB % 83.61/12.71 % (188244)Instructions burned: 543 (million) % 83.61/12.71 % (188254)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=2065720197:cts=off:i=2759:kws=inv_arity:fgj=on_2910 on theBenchmark for (2910ds/2759Mi) % 83.61/12.71 % (188245)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.61/12.71 % (188245)------------------------------ % 83.61/12.71 % (188245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.61/12.71 % (188245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.61/12.71 % (188245)CaDiCaL version: 2.1.3 % 83.61/12.71 % (188245)Termination reason: Unknown % 83.61/12.71 % (188245)Termination phase: Saturation % 83.61/12.71 % (188245)Time elapsed: 0.587 s % 83.61/12.71 % (188245)Peak memory usage: 114 MB % 83.61/12.71 % (188245)Instructions burned: 538 (million) % 83.61/12.71 % (188246)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.61/12.71 % (188246)------------------------------ % 83.61/12.71 % (188246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.61/12.71 % (188246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.61/12.71 % (188246)CaDiCaL version: 2.1.3 % 83.61/12.71 % (188246)Termination reason: Unknown % 83.61/12.71 % (188246)Termination phase: Saturation % 83.61/12.71 % (188246)Time elapsed: 0.595 s % 83.61/12.71 % (188246)Peak memory usage: 113 MB % 83.61/12.71 % (188246)Instructions burned: 536 (million) % 83.61/12.71 % (188255)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=1460265590:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2909 on theBenchmark for (2909ds/5665Mi) % 83.61/12.71 % (188255)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 83.61/12.71 % (188254)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.61/12.71 % (188254)------------------------------ % 83.61/12.71 % (188254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.61/12.71 % (188254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.61/12.71 % (188254)CaDiCaL version: 2.1.3 % 83.61/12.71 % (188254)Termination reason: Unknown % 83.61/12.71 % (188254)Termination phase: Saturation % 83.61/12.71 % (188254)Time elapsed: 0.306 s % 83.61/12.71 % (188254)Peak memory usage: 114 MB % 83.61/12.71 % (188254)Instructions burned: 544 (million) % 83.61/12.71 % (188257)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=508783608:i=1532:ep=RS:ss=axioms_2908 on theBenchmark for (2908ds/1532Mi) % 83.61/12.71 % (188258)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1794976718:i=1565:sd=2:ss=axioms:sgt=32_2907 on theBenchmark for (2907ds/1565Mi) % 83.61/12.71 % (188260)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=344491631:i=1572:fgj=on:gsp=on_2905 on theBenchmark for (2905ds/1572Mi) % 83.61/12.71 % (188260)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 83.61/12.71 % (188255)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.61/12.71 % (188255)------------------------------ % 83.61/12.71 % (188255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.61/12.71 % (188255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.61/12.71 % (188255)CaDiCaL version: 2.1.3 % 83.61/12.71 % (188255)Termination reason: Unknown % 83.61/12.71 % (188255)Termination phase: Saturation % 83.61/12.71 % (188255)Time elapsed: 0.600 s % 83.61/12.71 % (188255)Peak memory usage: 113 MB % 83.61/12.71 % (188255)Instructions burned: 537 (million) % 83.61/12.71 % (188260)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.61/12.71 % (188260)------------------------------ % 87.99/13.40 % (188260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.99/13.40 % (188260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.99/13.40 % (188260)CaDiCaL version: 2.1.3 % 87.99/13.40 % (188260)Termination reason: Unknown % 87.99/13.40 % (188260)Termination phase: Saturation % 87.99/13.40 % (188260)Time elapsed: 0.301 s % 87.99/13.40 % (188260)Peak memory usage: 114 MB % 87.99/13.40 % (188260)Instructions burned: 539 (million) % 87.99/13.40 % (188217)Instruction limit reached! % 87.99/13.40 % (188217)------------------------------ % 87.99/13.40 % (188217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.99/13.40 % (188217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.99/13.40 % (188217)CaDiCaL version: 2.1.3 % 87.99/13.40 % (188217)Termination reason: Instruction limit % 87.99/13.40 % (188217)Termination phase: Saturation % 87.99/13.40 % (188217)Time elapsed: 4.414 s % 87.99/13.40 % (188217)Peak memory usage: 110 MB % 87.99/13.40 % (188217)Instructions burned: 4835 (million) % 87.99/13.40 % (188257)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 87.99/13.40 % (188257)------------------------------ % 87.99/13.40 % (188257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.99/13.40 % (188257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.99/13.40 % (188257)CaDiCaL version: 2.1.3 % 87.99/13.40 % (188257)Termination reason: Unknown % 87.99/13.40 % (188257)Termination phase: Saturation % 87.99/13.40 % (188257)Time elapsed: 0.597 s % 87.99/13.40 % (188257)Peak memory usage: 113 MB % 87.99/13.40 % (188257)Instructions burned: 537 (million) % 87.99/13.40 % (188258)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 87.99/13.40 % (188258)------------------------------ % 87.99/13.40 % (188258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.99/13.40 % (188258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.99/13.40 % (188258)CaDiCaL version: 2.1.3 % 87.99/13.40 % (188258)Termination reason: Unknown % 87.99/13.40 % (188258)Termination phase: Saturation % 87.99/13.40 % (188258)Time elapsed: 0.589 s % 87.99/13.40 % (188258)Peak memory usage: 114 MB % 87.99/13.40 % (188258)Instructions burned: 539 (million) % 87.99/13.40 % (188265)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=2869841542:i=3500:sd=1:bd=preordered:sup=off:ss=included_2900 on theBenchmark for (2900ds/3500Mi) % 87.99/13.40 % (188264)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1412333078:i=6052:sd=4:ss=axioms:sgt=24_2900 on theBenchmark for (2900ds/6052Mi) % 87.99/13.40 % (188267)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=4074280974:i=66096:add=on_2899 on theBenchmark for (2899ds/66096Mi) % 87.99/13.40 % (188266)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=3471060621:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2899 on theBenchmark for (2899ds/1842Mi) % 87.99/13.40 % (188266)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 87.99/13.40 % (188268)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=712285189:i=1884:sd=1:nm=60:ss=axioms_2898 on theBenchmark for (2898ds/1884Mi) % 87.99/13.40 % (188265)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 87.99/13.40 % (188265)------------------------------ % 87.99/13.40 % (188265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 87.99/13.40 % (188265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 87.99/13.40 % (188265)CaDiCaL version: 2.1.3 % 87.99/13.40 % (188265)Termination reason: Unknown % 87.99/13.40 % (188265)Termination phase: Saturation % 87.99/13.40 % (188265)Time elapsed: 0.302 s % 87.99/13.40 % (188265)Peak memory usage: 113 MB % 87.99/13.40 % (188265)Instructions burned: 539 (million) % 87.99/13.40 % (188274)lrs-1011_4:1_sil=16000:bsr=on:random_seed=164414689:cts=off:i=5469:bs=on:fsr=off_2894 on theBenchmark for (2894ds/5469Mi) % 87.99/13.40 % (188264)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 87.99/13.40 % (188264)------------------------------ % 87.99/13.40 % (188264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.13/14.09 % (188264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.13/14.09 % (188264)CaDiCaL version: 2.1.3 % 93.13/14.09 % (188264)Termination reason: Unknown % 93.13/14.09 % (188264)Termination phase: Saturation % 93.13/14.09 % (188264)Time elapsed: 0.597 s % 93.13/14.09 % (188264)Peak memory usage: 114 MB % 93.13/14.09 % (188264)Instructions burned: 539 (million) % 93.13/14.09 % (188266)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.13/14.09 % (188266)------------------------------ % 93.13/14.09 % (188266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.13/14.09 % (188266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.13/14.09 % (188266)CaDiCaL version: 2.1.3 % 93.13/14.09 % (188266)Termination reason: Unknown % 93.13/14.09 % (188266)Termination phase: Saturation % 93.13/14.09 % (188266)Time elapsed: 0.561 s % 93.13/14.09 % (188266)Peak memory usage: 114 MB % 93.13/14.09 % (188266)Instructions burned: 540 (million) % 93.13/14.09 % (188267)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.13/14.09 % (188267)------------------------------ % 93.13/14.09 % (188267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.13/14.09 % (188267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.13/14.09 % (188267)CaDiCaL version: 2.1.3 % 93.13/14.09 % (188267)Termination reason: Unknown % 93.13/14.09 % (188267)Termination phase: Saturation % 93.13/14.09 % (188267)Time elapsed: 0.599 s % 93.13/14.09 % (188267)Peak memory usage: 114 MB % 93.13/14.09 % (188267)Instructions burned: 541 (million) % 93.13/14.09 % (188276)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=2495466692:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2891 on theBenchmark for (2891ds/2037Mi) % 93.13/14.09 % (188268)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.13/14.09 % (188268)------------------------------ % 93.13/14.09 % (188268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.13/14.09 % (188268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.13/14.09 % (188268)CaDiCaL version: 2.1.3 % 93.13/14.09 % (188268)Termination reason: Unknown % 93.13/14.09 % (188268)Termination phase: Saturation % 93.13/14.09 % (188268)Time elapsed: 0.586 s % 93.13/14.09 % (188268)Peak memory usage: 113 MB % 93.13/14.09 % (188268)Instructions burned: 537 (million) % 93.13/14.09 % (188278)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=2616336063:i=2430:add=off:aac=none:nm=16_2890 on theBenchmark for (2890ds/2430Mi) % 93.13/14.09 % (188277)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2652822357:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2891 on theBenchmark for (2891ds/2110Mi) % 93.13/14.09 % (188280)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=2591912038:cond=fast:i=4891_2889 on theBenchmark for (2889ds/4891Mi) % 93.13/14.09 % (188276)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.13/14.09 % (188276)------------------------------ % 93.13/14.09 % (188276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.13/14.09 % (188276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.13/14.09 % (188276)CaDiCaL version: 2.1.3 % 93.13/14.09 % (188276)Termination reason: Unknown % 93.13/14.09 % (188276)Termination phase: Saturation % 93.13/14.09 % (188276)Time elapsed: 0.572 s % 93.13/14.09 % (188276)Peak memory usage: 114 MB % 93.13/14.09 % (188276)Instructions burned: 548 (million) % 93.13/14.09 % (188278)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.13/14.09 % (188277)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.13/14.09 % (188277)------------------------------ % 93.13/14.09 % (188277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.13/14.09 % (188278)------------------------------ % 93.13/14.09 % (188278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.13/14.09 % (188278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.13/14.09 % (188277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.12/14.56 % (188278)CaDiCaL version: 2.1.3 % 96.12/14.56 % (188277)CaDiCaL version: 2.1.3 % 96.12/14.56 % (188277)Termination reason: Unknown % 96.12/14.56 % (188277)Termination phase: Saturation % 96.12/14.56 % (188278)Termination reason: Unknown % 96.12/14.56 % (188278)Termination phase: Saturation % 96.12/14.56 % (188277)Time elapsed: 0.601 s % 96.12/14.56 % (188278)Time elapsed: 0.601 s % 96.12/14.56 % (188277)Peak memory usage: 112 MB % 96.12/14.56 % (188278)Peak memory usage: 112 MB % 96.12/14.56 % (188277)Instructions burned: 546 (million) % 96.12/14.56 % (188278)Instructions burned: 541 (million) % 96.12/14.56 % (188291)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=2571080032:st=2:i=14845:sd=2:ss=included:fsd=on_2883 on theBenchmark for (2883ds/14845Mi) % 96.12/14.56 % (188280)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.12/14.56 % (188280)------------------------------ % 96.12/14.56 % (188280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.12/14.56 % (188280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.12/14.56 % (188280)CaDiCaL version: 2.1.3 % 96.12/14.56 % (188280)Termination reason: Unknown % 96.12/14.56 % (188280)Termination phase: Saturation % 96.12/14.56 % (188280)Time elapsed: 0.574 s % 96.12/14.56 % (188280)Peak memory usage: 114 MB % 96.12/14.56 % (188280)Instructions burned: 541 (million) % 96.12/14.56 % (188294)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=3453695964:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2882 on theBenchmark for (2882ds/10353Mi) % 96.12/14.56 % (188293)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2530096069:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2882 on theBenchmark for (2882ds/7534Mi) % 96.12/14.56 % (188296)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=420075867:i=7860_2880 on theBenchmark for (2880ds/7860Mi) % 96.12/14.56 % (188296)Refutation not found, incomplete strategy % 96.12/14.56 % (188296)------------------------------ % 96.12/14.56 % (188296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.12/14.56 % (188296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.12/14.56 % (188296)CaDiCaL version: 2.1.3 % 96.12/14.56 % (188296)Termination reason: Refutation not found, incomplete strategy % 96.12/14.56 % (188296)Time elapsed: 0.006 s % 96.12/14.56 % (188296)Peak memory usage: 88 MB % 96.12/14.56 % (188296)Instructions burned: 10 (million) % 96.12/14.56 % (188294)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.12/14.56 % (188294)------------------------------ % 96.12/14.56 % (188294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.12/14.56 % (188294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.12/14.56 % (188294)CaDiCaL version: 2.1.3 % 96.12/14.56 % (188294)Termination reason: Unknown % 96.12/14.56 % (188294)Termination phase: Saturation % 96.12/14.56 % (188294)Time elapsed: 0.410 s % 96.12/14.56 % (188294)Peak memory usage: 113 MB % 96.12/14.56 % (188294)Instructions burned: 542 (million) % 96.12/14.56 % (188291)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.12/14.56 % (188291)------------------------------ % 96.12/14.56 % (188291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.12/14.56 % (188291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.12/14.56 % (188291)CaDiCaL version: 2.1.3 % 96.12/14.56 % (188291)Termination reason: Unknown % 96.12/14.56 % (188291)Termination phase: Saturation % 96.12/14.56 % (188291)Time elapsed: 0.524 s % 96.12/14.56 % (188291)Peak memory usage: 114 MB % 96.12/14.56 % (188291)Instructions burned: 541 (million) % 96.12/14.56 % (188296)------------------------------ % 96.12/14.56 % (188296)------------------------------ % 96.12/14.56 % (188293)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.12/14.56 % (188293)------------------------------ % 96.12/14.56 % (188293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.12/14.56 % (188293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.12/14.56 % (188293)CaDiCaL version: 2.1.3 % 96.12/14.56 % (188293)Termination reason: Unknown % 96.12/14.56 % (188293)Termination phase: Saturation % 96.12/14.56 % (188293)Time elapsed: 0.394 s % 100.22/15.08 % (188293)Peak memory usage: 114 MB % 100.22/15.08 % (188293)Instructions burned: 543 (million) % 100.22/15.08 % (188301)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=193560659:i=7896:sd=2:bs=on:ss=included:sgt=20_2876 on theBenchmark for (2876ds/7896Mi) % 100.22/15.08 % (188302)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2145087486:i=5812:gtgl=2:gtg=all_2875 on theBenchmark for (2875ds/5812Mi) % 100.22/15.08 % (188303)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=258724178:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2875 on theBenchmark for (2875ds/2965Mi) % 100.22/15.08 % (188304)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=890936736:i=2967:kws=precedence:bd=preordered:av=off_2875 on theBenchmark for (2875ds/2967Mi) % 100.22/15.08 % (188301)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 100.22/15.08 % (188301)------------------------------ % 100.22/15.08 % (188301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.22/15.08 % (188301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.22/15.08 % (188301)CaDiCaL version: 2.1.3 % 100.22/15.08 % (188301)Termination reason: Unknown % 100.22/15.08 % (188301)Termination phase: Saturation % 100.22/15.08 % (188301)Time elapsed: 0.359 s % 100.22/15.08 % (188301)Peak memory usage: 114 MB % 100.22/15.08 % (188301)Instructions burned: 542 (million) % 100.22/15.08 % (188302)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 100.22/15.08 % (188302)------------------------------ % 100.22/15.08 % (188302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.22/15.08 % (188302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.22/15.08 % (188302)CaDiCaL version: 2.1.3 % 100.22/15.08 % (188302)Termination reason: Unknown % 100.22/15.08 % (188302)Termination phase: Saturation % 100.22/15.08 % (188302)Time elapsed: 0.358 s % 100.22/15.08 % (188302)Peak memory usage: 114 MB % 100.22/15.08 % (188302)Instructions burned: 543 (million) % 100.22/15.08 % (188303)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 100.22/15.08 % (188303)------------------------------ % 100.22/15.08 % (188303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.22/15.08 % (188303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.22/15.08 % (188303)CaDiCaL version: 2.1.3 % 100.22/15.08 % (188303)Termination reason: Unknown % 100.22/15.08 % (188303)Termination phase: Saturation % 100.22/15.08 % (188303)Time elapsed: 0.358 s % 100.22/15.08 % (188303)Peak memory usage: 114 MB % 100.22/15.08 % (188303)Instructions burned: 541 (million) % 100.22/15.08 % (188304)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 100.22/15.08 % (188304)------------------------------ % 100.22/15.08 % (188304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 100.22/15.08 % (188304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 100.22/15.08 % (188304)CaDiCaL version: 2.1.3 % 100.22/15.08 % (188304)Termination reason: Unknown % 100.22/15.08 % (188304)Termination phase: Saturation % 100.22/15.08 % (188304)Time elapsed: 0.360 s % 100.22/15.08 % (188304)Peak memory usage: 114 MB % 100.22/15.08 % (188304)Instructions burned: 541 (million) % 100.22/15.08 % (188381)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=4253741756:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2870 on theBenchmark for (2870ds/3022Mi) % 100.22/15.08 % (188382)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=3560740277:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2870 on theBenchmark for (2870ds/3207Mi) % 100.22/15.08 % (188389)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1900719782:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2870 on theBenchmark for (2870ds/3289Mi) % 100.22/15.08 % (188399)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2793961668:i=38569:sd=3:ss=axioms:sgt=32_2869 on theBenchmark for (2869ds/38569Mi) % 105.08/15.90 % (188274)Instruction limit reached! % 105.08/15.90 % (188274)------------------------------ % 105.08/15.90 % (188274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.08/15.90 % (188274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.08/15.90 % (188274)CaDiCaL version: 2.1.3 % 105.08/15.90 % (188274)Termination reason: Instruction limit % 105.08/15.90 % (188274)Termination phase: Saturation % 105.08/15.90 % (188274)Time elapsed: 2.513 s % 105.08/15.90 % (188274)Peak memory usage: 113 MB % 105.08/15.90 % (188274)Instructions burned: 5471 (million) % 105.08/15.90 % (188423)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=4016103770:cts=off:i=3394_2867 on theBenchmark for (2867ds/3394Mi) % 105.08/15.90 % (188381)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 105.08/15.90 % (188381)------------------------------ % 105.08/15.90 % (188381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.08/15.90 % (188381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.08/15.90 % (188381)CaDiCaL version: 2.1.3 % 105.08/15.90 % (188381)Termination reason: Unknown % 105.08/15.90 % (188381)Termination phase: Saturation % 105.08/15.90 % (188381)Time elapsed: 0.356 s % 105.08/15.90 % (188381)Peak memory usage: 113 MB % 105.08/15.90 % (188381)Instructions burned: 537 (million) % 105.08/15.90 % (188382)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 105.08/15.90 % (188382)------------------------------ % 105.08/15.90 % (188382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.08/15.90 % (188382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.08/15.90 % (188382)CaDiCaL version: 2.1.3 % 105.08/15.90 % (188382)Termination reason: Unknown % 105.08/15.90 % (188382)Termination phase: Saturation % 105.08/15.90 % (188382)Time elapsed: 0.356 s % 105.08/15.90 % (188382)Peak memory usage: 114 MB % 105.08/15.90 % (188382)Instructions burned: 537 (million) % 105.08/15.90 % (188389)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 105.08/15.90 % (188389)------------------------------ % 105.08/15.90 % (188389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.08/15.90 % (188389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.08/15.90 % (188389)CaDiCaL version: 2.1.3 % 105.08/15.90 % (188389)Termination reason: Unknown % 105.08/15.90 % (188389)Termination phase: Saturation % 105.08/15.90 % (188389)Time elapsed: 0.362 s % 105.08/15.90 % (188389)Peak memory usage: 114 MB % 105.08/15.90 % (188389)Instructions burned: 542 (million) % 105.08/15.90 % (188399)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 105.08/15.90 % (188399)------------------------------ % 105.08/15.90 % (188399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.08/15.90 % (188399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.08/15.90 % (188399)CaDiCaL version: 2.1.3 % 105.08/15.90 % (188399)Termination reason: Unknown % 105.08/15.90 % (188399)Termination phase: Saturation % 105.08/15.90 % (188399)Time elapsed: 0.359 s % 105.08/15.90 % (188399)Peak memory usage: 114 MB % 105.08/15.90 % (188399)Instructions burned: 540 (million) % 105.08/15.90 % (188423)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 105.08/15.90 % (188423)------------------------------ % 105.08/15.90 % (188423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.08/15.90 % (188423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.08/15.90 % (188423)CaDiCaL version: 2.1.3 % 105.08/15.90 % (188423)Termination reason: Unknown % 105.08/15.90 % (188423)Termination phase: Saturation % 105.08/15.90 % (188423)Time elapsed: 0.198 s % 105.08/15.90 % (188423)Peak memory usage: 114 MB % 105.08/15.90 % (188423)Instructions burned: 541 (million) % 105.08/15.90 % (188472)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=1916782914:i=33824:bd=preordered_2865 on theBenchmark for (2865ds/33824Mi) % 105.08/15.90 % (188473)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=305642854:i=20684:bd=all:gtg=exists_sym_2865 on theBenchmark for (2865ds/20684Mi) % 105.08/15.90 % (188474)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=2099119547: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_2865 on theBenchmark for (2865ds/7222Mi) % 110.06/16.58 % (188474)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 110.06/16.58 % (188476)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=1623441373:i=4036:ins=10_2864 on theBenchmark for (2864ds/4036Mi) % 110.06/16.58 % (188475)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1231844437:st=4:i=7295:sd=4:ep=R:ss=axioms_2864 on theBenchmark for (2864ds/7295Mi) % 110.06/16.58 % (188476)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 110.06/16.58 % (188476)------------------------------ % 110.06/16.58 % (188476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.06/16.58 % (188476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.06/16.58 % (188476)CaDiCaL version: 2.1.3 % 110.06/16.58 % (188476)Termination reason: Unknown % 110.06/16.58 % (188476)Termination phase: Saturation % 110.06/16.58 % (188476)Time elapsed: 0.192 s % 110.06/16.58 % (188476)Peak memory usage: 114 MB % 110.06/16.58 % (188476)Instructions burned: 541 (million) % 110.06/16.58 % (188472)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 110.06/16.58 % (188472)------------------------------ % 110.06/16.58 % (188472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.06/16.58 % (188472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.06/16.58 % (188472)CaDiCaL version: 2.1.3 % 110.06/16.58 % (188472)Termination reason: Unknown % 110.06/16.58 % (188472)Termination phase: Saturation % 110.06/16.58 % (188472)Time elapsed: 0.360 s % 110.06/16.58 % (188472)Peak memory usage: 114 MB % 110.06/16.58 % (188472)Instructions burned: 541 (million) % 110.06/16.58 % (188473)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 110.06/16.58 % (188473)------------------------------ % 110.06/16.58 % (188473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.06/16.58 % (188473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.06/16.58 % (188473)CaDiCaL version: 2.1.3 % 110.06/16.58 % (188473)Termination reason: Unknown % 110.06/16.58 % (188473)Termination phase: Saturation % 110.06/16.58 % (188473)Time elapsed: 0.361 s % 110.06/16.58 % (188473)Peak memory usage: 114 MB % 110.06/16.58 % (188473)Instructions burned: 544 (million) % 110.06/16.58 % (188482)lrs+10_1_sil=128000:lcm=predicate:random_seed=2405561354:st=3:i=43697:sd=5:ss=axioms_2861 on theBenchmark for (2861ds/43697Mi) % 110.06/16.58 % (188474)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 110.06/16.58 % (188474)------------------------------ % 110.06/16.58 % (188474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.06/16.58 % (188474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.06/16.58 % (188474)CaDiCaL version: 2.1.3 % 110.06/16.58 % (188474)Termination reason: Unknown % 110.06/16.58 % (188474)Termination phase: Saturation % 110.06/16.58 % (188474)Time elapsed: 0.360 s % 110.06/16.58 % (188474)Peak memory usage: 114 MB % 110.06/16.58 % (188474)Instructions burned: 542 (million) % 110.06/16.58 % (188475)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 110.06/16.58 % (188475)------------------------------ % 110.06/16.58 % (188475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.06/16.58 % (188475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.06/16.58 % (188475)CaDiCaL version: 2.1.3 % 110.06/16.58 % (188475)Termination reason: Unknown % 110.06/16.58 % (188475)Termination phase: Saturation % 110.06/16.58 % (188475)Time elapsed: 0.358 s % 110.06/16.58 % (188475)Peak memory usage: 113 MB % 110.06/16.58 % (188475)Instructions burned: 541 (million) % 110.06/16.58 % (188483)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=1530118398:i=17599:gtg=all:ss=axioms:fsd=on_2860 on theBenchmark for (2860ds/17599Mi) % 110.06/16.58 % (188484)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=1208809975:i=4547:bd=preordered_2860 on theBenchmark for (2860ds/4547Mi) % 110.06/16.58 % (188486)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=3834133702:i=9294:av=off_2859 on theBenchmark for (2859ds/9294Mi) % 119.72/17.97 % (188487)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3367654782:i=32849:add=on_2859 on theBenchmark for (2859ds/32849Mi) % 119.72/17.97 % (188483)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 119.72/17.97 % (188483)------------------------------ % 119.72/17.97 % (188483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.72/17.97 % (188483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.72/17.97 % (188483)CaDiCaL version: 2.1.3 % 119.72/17.97 % (188483)Termination reason: Unknown % 119.72/17.97 % (188483)Termination phase: Saturation % 119.72/17.97 % (188483)Time elapsed: 0.358 s % 119.72/17.97 % (188483)Peak memory usage: 113 MB % 119.72/17.97 % (188483)Instructions burned: 539 (million) % 119.72/17.97 % (188484)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 119.72/17.97 % (188484)------------------------------ % 119.72/17.97 % (188484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.72/17.97 % (188484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.72/17.97 % (188484)CaDiCaL version: 2.1.3 % 119.72/17.97 % (188484)Termination reason: Unknown % 119.72/17.97 % (188484)Termination phase: Saturation % 119.72/17.97 % (188484)Time elapsed: 0.356 s % 119.72/17.97 % (188484)Peak memory usage: 114 MB % 119.72/17.97 % (188484)Instructions burned: 541 (million) % 119.72/17.97 % (188486)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 119.72/17.97 % (188486)------------------------------ % 119.72/17.97 % (188486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.72/17.97 % (188486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.72/17.97 % (188486)CaDiCaL version: 2.1.3 % 119.72/17.97 % (188486)Termination reason: Unknown % 119.72/17.97 % (188486)Termination phase: Saturation % 119.72/17.97 % (188486)Time elapsed: 0.357 s % 119.72/17.97 % (188486)Peak memory usage: 114 MB % 119.72/17.97 % (188486)Instructions burned: 540 (million) % 119.72/17.97 % (188487)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 119.72/17.97 % (188487)------------------------------ % 119.72/17.97 % (188487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.72/17.97 % (188487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.72/17.97 % (188487)CaDiCaL version: 2.1.3 % 119.72/17.97 % (188487)Termination reason: Unknown % 119.72/17.97 % (188487)Termination phase: Saturation % 119.72/17.97 % (188487)Time elapsed: 0.357 s % 119.72/17.97 % (188487)Peak memory usage: 114 MB % 119.72/17.97 % (188487)Instructions burned: 541 (million) % 119.72/17.97 % (188492)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1402579303:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2855 on theBenchmark for (2855ds/4793Mi) % 119.72/17.97 % (188493)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=3804525202:i=4840:nm=4:av=off_2855 on theBenchmark for (2855ds/4840Mi) % 119.72/17.97 % (188494)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2296716496:cts=off:i=5002_2854 on theBenchmark for (2854ds/5002Mi) % 119.72/17.97 % (188495)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=204036706:i=30479:sd=3:ss=axioms_2854 on theBenchmark for (2854ds/30479Mi) % 119.72/17.97 % (188492)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 119.72/17.97 % (188492)------------------------------ % 119.72/17.97 % (188492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.72/17.97 % (188492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.72/17.97 % (188492)CaDiCaL version: 2.1.3 % 119.72/17.97 % (188492)Termination reason: Unknown % 119.72/17.97 % (188492)Termination phase: Saturation % 119.72/17.97 % (188492)Time elapsed: 0.358 s % 119.72/17.97 % (188492)Peak memory usage: 113 MB % 119.72/17.97 % (188492)Instructions burned: 538 (million) % 119.72/17.97 % (188493)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 119.72/17.97 % (188493)------------------------------ % 119.72/17.97 % (188493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.90/22.07 % (188493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.90/22.07 % (188493)CaDiCaL version: 2.1.3 % 149.90/22.07 % (188493)Termination reason: Unknown % 149.90/22.07 % (188493)Termination phase: Saturation % 149.90/22.07 % (188493)Time elapsed: 0.356 s % 149.90/22.07 % (188493)Peak memory usage: 114 MB % 149.90/22.07 % (188493)Instructions burned: 540 (million) % 149.90/22.07 % (188494)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 149.90/22.07 % (188494)------------------------------ % 149.90/22.07 % (188494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.90/22.07 % (188494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.90/22.07 % (188494)CaDiCaL version: 2.1.3 % 149.90/22.07 % (188494)Termination reason: Unknown % 149.90/22.07 % (188494)Termination phase: Saturation % 149.90/22.07 % (188494)Time elapsed: 0.358 s % 149.90/22.07 % (188494)Peak memory usage: 114 MB % 149.90/22.07 % (188494)Instructions burned: 541 (million) % 149.90/22.07 % (188495)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 149.90/22.07 % (188495)------------------------------ % 149.90/22.07 % (188495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.90/22.07 % (188495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.90/22.07 % (188495)CaDiCaL version: 2.1.3 % 149.90/22.07 % (188495)Termination reason: Unknown % 149.90/22.07 % (188495)Termination phase: Saturation % 149.90/22.07 % (188495)Time elapsed: 0.356 s % 149.90/22.07 % (188495)Peak memory usage: 113 MB % 149.90/22.07 % (188495)Instructions burned: 536 (million) % 149.90/22.07 % (188500)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=878998370:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2850 on theBenchmark for (2850ds/11035Mi) % 149.90/22.07 % (188500)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 149.90/22.07 % (188501)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=903556611:i=5835_2850 on theBenchmark for (2850ds/5835Mi) % 149.90/22.07 % (188502)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=4098984648:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2849 on theBenchmark for (2849ds/5890Mi) % 149.90/22.07 % (188503)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2323500914:cts=off:i=19910:ep=RS_2849 on theBenchmark for (2849ds/19910Mi) % 149.90/22.07 % (188500)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 149.90/22.07 % (188500)------------------------------ % 149.90/22.07 % (188500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.90/22.07 % (188500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.90/22.07 % (188500)CaDiCaL version: 2.1.3 % 149.90/22.07 % (188500)Termination reason: Unknown % 149.90/22.07 % (188500)Termination phase: Saturation % 149.90/22.07 % (188500)Time elapsed: 0.362 s % 149.90/22.07 % (188500)Peak memory usage: 114 MB % 149.90/22.07 % (188500)Instructions burned: 544 (million) % 149.90/22.07 % (188501)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 149.90/22.07 % (188501)------------------------------ % 149.90/22.07 % (188501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.90/22.07 % (188501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.90/22.07 % (188501)CaDiCaL version: 2.1.3 % 149.90/22.07 % (188501)Termination reason: Unknown % 149.90/22.07 % (188501)Termination phase: Saturation % 149.90/22.07 % (188501)Time elapsed: 0.357 s % 149.90/22.07 % (188501)Peak memory usage: 114 MB % 149.90/22.07 % (188501)Instructions burned: 541 (million) % 149.90/22.07 % (188502)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 149.90/22.07 % (188502)------------------------------ % 149.90/22.07 % (188502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.90/22.07 % (188502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.90/22.07 % (188502)CaDiCaL version: 2.1.3 % 149.90/22.07 % (188502)Termination reason: Unknown % 149.90/22.07 % (188502)Termination phase: Saturation % 149.90/22.07 % (188502)Time elapsed: 0.356 s % 149.90/22.07 % (188502)Peak memory usage: 114 MB % 149.90/22.07 % (188502)Instructions burned: 541 (million) % 149.90/22.07 % (188509)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=445599910:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2844 on theBenchmark for (2844ds/13822Mi) % 159.39/23.49 % (188508)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=1660952316:i=20312:bd=preordered:fsr=off:er=filter_2845 on theBenchmark for (2845ds/20312Mi) % 159.39/23.49 % (188510)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=227996491:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2844 on theBenchmark for (2844ds/7144Mi) % 159.39/23.49 % (188508)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 159.39/23.49 % (188509)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 159.39/23.49 % (188508)------------------------------ % 159.39/23.49 % (188508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.39/23.49 % (188509)------------------------------ % 159.39/23.49 % (188509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.39/23.49 % (188508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.39/23.49 % (188509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.39/23.49 % (188508)CaDiCaL version: 2.1.3 % 159.39/23.49 % (188509)CaDiCaL version: 2.1.3 % 159.39/23.49 % (188508)Termination reason: Unknown % 159.39/23.49 % (188508)Termination phase: Saturation % 159.39/23.49 % (188509)Termination reason: Unknown % 159.39/23.49 % (188509)Termination phase: Saturation % 159.39/23.49 % (188508)Time elapsed: 0.356 s % 159.39/23.49 % (188509)Time elapsed: 0.356 s % 159.39/23.49 % (188509)Peak memory usage: 112 MB % 159.39/23.49 % (188508)Peak memory usage: 112 MB % 159.39/23.49 % (188508)Instructions burned: 541 (million) % 159.39/23.49 % (188509)Instructions burned: 541 (million) % 159.39/23.49 % (188514)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=2368961376:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2839 on theBenchmark for (2839ds/15184Mi) % 159.39/23.49 % (188515)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=2939044014:i=107375_2839 on theBenchmark for (2839ds/107375Mi) % 159.39/23.49 % (188514)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 159.39/23.49 % (188515)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 159.39/23.49 % (188515)------------------------------ % 159.39/23.49 % (188515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.39/23.49 % (188514)------------------------------ % 159.39/23.49 % (188514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.39/23.49 % (188514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.39/23.49 % (188515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.39/23.49 % (188514)CaDiCaL version: 2.1.3 % 159.39/23.49 % (188515)CaDiCaL version: 2.1.3 % 159.39/23.49 % (188515)Termination reason: Unknown % 159.39/23.49 % (188515)Termination phase: Saturation % 159.39/23.49 % (188514)Termination reason: Unknown % 159.39/23.49 % (188514)Termination phase: Saturation % 159.39/23.49 % (188515)Time elapsed: 0.356 s % 159.39/23.49 % (188514)Time elapsed: 0.356 s % 159.39/23.49 % (188514)Peak memory usage: 113 MB % 159.39/23.49 % (188515)Peak memory usage: 112 MB % 159.39/23.49 % (188514)Instructions burned: 541 (million) % 159.39/23.49 % (188515)Instructions burned: 541 (million) % 159.39/23.49 % (188518)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=1957066282:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2834 on theBenchmark for (2834ds/7958Mi) % 159.39/23.49 % (188519)dis+10_128_sil=16000:nwc=0.7:random_seed=2544961830:i=15999:nm=2:gsp=on_2834 on theBenchmark for (2834ds/15999Mi) % 159.39/23.49 % (188519)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 159.39/23.49 % (188518)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 159.39/23.49 % (188518)------------------------------ % 159.39/23.49 % (188518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.39/23.49 % (188518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.83/25.41 % (188518)CaDiCaL version: 2.1.3 % 173.83/25.41 % (188518)Termination reason: Unknown % 173.83/25.41 % (188518)Termination phase: Saturation % 173.83/25.41 % (188518)Time elapsed: 0.356 s % 173.83/25.41 % (188518)Peak memory usage: 114 MB % 173.83/25.41 % (188518)Instructions burned: 541 (million) % 173.83/25.41 % (188522)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1472731498:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2829 on theBenchmark for (2829ds/8139Mi) % 173.83/25.41 % (188510)Instruction limit reached! % 173.83/25.41 % (188510)------------------------------ % 173.83/25.41 % (188510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.83/25.41 % (188510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.83/25.41 % (188510)CaDiCaL version: 2.1.3 % 173.83/25.41 % (188510)Termination reason: Instruction limit % 173.83/25.41 % (188510)Termination phase: Saturation % 173.83/25.41 % (188510)Time elapsed: 3.275 s % 173.83/25.41 % (188510)Peak memory usage: 129 MB % 173.83/25.41 % (188510)Instructions burned: 7144 (million) % 173.83/25.41 % (188524)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=1976215543:st=4:i=8950:sd=5:ss=axioms_2810 on theBenchmark for (2810ds/8950Mi) % 173.83/25.41 % (188524)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.83/25.41 % (188524)------------------------------ % 173.83/25.41 % (188524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.83/25.41 % (188524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.83/25.41 % (188524)CaDiCaL version: 2.1.3 % 173.83/25.41 % (188524)Termination reason: Unknown % 173.83/25.41 % (188524)Termination phase: Saturation % 173.83/25.41 % (188524)Time elapsed: 0.355 s % 173.83/25.41 % (188524)Peak memory usage: 114 MB % 173.83/25.41 % (188524)Instructions burned: 540 (million) % 173.83/25.41 % (188526)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=1513397648:i=9809:ins=10:av=off_2804 on theBenchmark for (2804ds/9809Mi) % 173.83/25.41 % (188526)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.83/25.41 % (188526)------------------------------ % 173.83/25.41 % (188526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.83/25.41 % (188526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.83/25.41 % (188526)CaDiCaL version: 2.1.3 % 173.83/25.41 % (188526)Termination reason: Unknown % 173.83/25.41 % (188526)Termination phase: Saturation % 173.83/25.41 % (188526)Time elapsed: 0.359 s % 173.83/25.41 % (188526)Peak memory usage: 114 MB % 173.83/25.41 % (188526)Instructions burned: 541 (million) % 173.83/25.41 % (188528)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=77587343:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2799 on theBenchmark for (2799ds/9885Mi) % 173.83/25.41 % (188528)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.83/25.41 % (188528)------------------------------ % 173.83/25.41 % (188528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.83/25.41 % (188528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.83/25.41 % (188528)CaDiCaL version: 2.1.3 % 173.83/25.41 % (188528)Termination reason: Unknown % 173.83/25.41 % (188528)Termination phase: Saturation % 173.83/25.41 % (188528)Time elapsed: 0.356 s % 173.83/25.41 % (188528)Peak memory usage: 114 MB % 173.83/25.41 % (188528)Instructions burned: 541 (million) % 173.83/25.41 % (188530)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1718364842:cond=fast:i=32078:fgj=on:av=off_2794 on theBenchmark for (2794ds/32078Mi) % 173.83/25.41 % (188530)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.83/25.41 % (188530)------------------------------ % 173.83/25.41 % (188530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 173.83/25.41 % (188530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 173.83/25.41 % (188530)CaDiCaL version: 2.1.3 % 173.83/25.41 % (188530)Termination reason: Unknown % 173.83/25.41 % (188530)Termination phase: Saturation % 173.83/25.41 % (188530)Time elapsed: 0.357 s % 173.83/25.41 % (188530)Peak memory usage: 114 MB % 173.83/25.41 % (188530)Instructions burned: 541 (million) % 173.83/25.41 % (188522)Instruction limit reached! % 173.83/25.41 % (188522)------------------------------ % 173.83/25.41 % (188522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.98/27.66 % (188522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.98/27.66 % (188522)CaDiCaL version: 2.1.3 % 188.98/27.66 % (188522)Termination reason: Instruction limit % 188.98/27.66 % (188522)Termination phase: Saturation % 188.98/27.66 % (188522)Time elapsed: 3.936 s % 188.98/27.66 % (188522)Peak memory usage: 106 MB % 188.98/27.66 % (188522)Instructions burned: 8141 (million) % 188.98/27.66 % (188532)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3714171126:i=11101:bd=all:ss=axioms:sgt=8_2789 on theBenchmark for (2789ds/11101Mi) % 188.98/27.66 % (188532)Refutation not found, incomplete strategy % 188.98/27.66 % (188532)------------------------------ % 188.98/27.66 % (188532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.98/27.66 % (188532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.98/27.66 % (188532)CaDiCaL version: 2.1.3 % 188.98/27.66 % (188532)Termination reason: Refutation not found, incomplete strategy % 188.98/27.66 % (188532)Time elapsed: 0.004 s % 188.98/27.66 % (188532)Peak memory usage: 89 MB % 188.98/27.66 % (188532)Instructions burned: 4 (million) % 188.98/27.67 % (188533)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=4139336532:cond=on:i=13220:s2at=3:aac=none:fsd=on_2788 on theBenchmark for (2788ds/13220Mi) % 188.98/27.67 % (188532)------------------------------ % 188.98/27.67 % (188532)------------------------------ % 188.98/27.67 % (188536)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=214659656:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2785 on theBenchmark for (2785ds/13528Mi) % 188.98/27.67 % (188533)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 188.98/27.67 % (188533)------------------------------ % 188.98/27.67 % (188533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.98/27.67 % (188533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.98/27.67 % (188533)CaDiCaL version: 2.1.3 % 188.98/27.67 % (188533)Termination reason: Unknown % 188.98/27.67 % (188533)Termination phase: Saturation % 188.98/27.67 % (188533)Time elapsed: 0.362 s % 188.98/27.67 % (188533)Peak memory usage: 114 MB % 188.98/27.67 % (188533)Instructions burned: 542 (million) % 188.98/27.67 % (188538)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=2837622876:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2783 on theBenchmark for (2783ds/14854Mi) % 188.98/27.67 % (188536)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 188.98/27.67 % (188536)------------------------------ % 188.98/27.67 % (188536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.98/27.67 % (188536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.98/27.67 % (188536)CaDiCaL version: 2.1.3 % 188.98/27.67 % (188536)Termination reason: Unknown % 188.98/27.67 % (188536)Termination phase: Saturation % 188.98/27.67 % (188536)Time elapsed: 0.360 s % 188.98/27.67 % (188536)Peak memory usage: 114 MB % 188.98/27.67 % (188536)Instructions burned: 541 (million) % 188.98/27.67 % (188538)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 188.98/27.67 % (188538)------------------------------ % 188.98/27.67 % (188538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 188.98/27.67 % (188538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 188.98/27.67 % (188538)CaDiCaL version: 2.1.3 % 188.98/27.67 % (188538)Termination reason: Unknown % 188.98/27.67 % (188538)Termination phase: Saturation % 188.98/27.67 % (188538)Time elapsed: 0.367 s % 188.98/27.67 % (188538)Peak memory usage: 114 MB % 188.98/27.67 % (188538)Instructions burned: 555 (million) % 188.98/27.67 % (188540)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=3241167608:i=14974:ss=axioms:sgt=16_2779 on theBenchmark for (2779ds/14974Mi) % 188.98/27.67 % (188542)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=1051582456:i=33081:aac=none:fgj=on:bd=all:fsr=off_2777 on theBenchmark for (2777ds/33081Mi) % 188.98/27.67 % (188540)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 188.98/27.67 % (188540)------------------------------ % 188.98/27.67 % (188540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.84/28.93 % (188540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.84/28.93 % (188540)CaDiCaL version: 2.1.3 % 197.84/28.93 % (188540)Termination reason: Unknown % 197.84/28.93 % (188540)Termination phase: Saturation % 197.84/28.93 % (188540)Time elapsed: 0.359 s % 197.84/28.93 % (188540)Peak memory usage: 114 MB % 197.84/28.93 % (188540)Instructions burned: 539 (million) % 197.84/28.93 % (188542)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 197.84/28.93 % (188542)------------------------------ % 197.84/28.93 % (188542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.84/28.93 % (188542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.84/28.93 % (188542)CaDiCaL version: 2.1.3 % 197.84/28.93 % (188542)Termination reason: Unknown % 197.84/28.93 % (188542)Termination phase: Saturation % 197.84/28.93 % (188542)Time elapsed: 0.360 s % 197.84/28.93 % (188542)Peak memory usage: 114 MB % 197.84/28.93 % (188542)Instructions burned: 542 (million) % 197.84/28.93 % (188544)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=2478573640:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2774 on theBenchmark for (2774ds/50856Mi) % 197.84/28.93 % (188545)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2454454809:i=69865_2772 on theBenchmark for (2772ds/69865Mi) % 197.84/28.93 % (188544)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 197.84/28.93 % (188544)------------------------------ % 197.84/28.93 % (188544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.84/28.93 % (188544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.84/28.93 % (188544)CaDiCaL version: 2.1.3 % 197.84/28.93 % (188544)Termination reason: Unknown % 197.84/28.93 % (188544)Termination phase: Saturation % 197.84/28.93 % (188544)Time elapsed: 0.361 s % 197.84/28.93 % (188544)Peak memory usage: 114 MB % 197.84/28.93 % (188544)Instructions burned: 542 (million) % 197.84/28.93 % (188545)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 197.84/28.93 % (188545)------------------------------ % 197.84/28.93 % (188545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.84/28.93 % (188545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.84/28.93 % (188545)CaDiCaL version: 2.1.3 % 197.84/28.93 % (188545)Termination reason: Unknown % 197.84/28.93 % (188545)Termination phase: Saturation % 197.84/28.93 % (188545)Time elapsed: 0.359 s % 197.84/28.93 % (188545)Peak memory usage: 114 MB % 197.84/28.93 % (188545)Instructions burned: 542 (million) % 197.84/28.93 % (188548)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=991071991:cond=fast:i=17802:gtgl=3:gtg=all_2768 on theBenchmark for (2768ds/17802Mi) % 197.84/28.93 % (188549)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3941949876:i=96644_2767 on theBenchmark for (2767ds/96644Mi) % 197.84/28.93 % (188548)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 197.84/28.93 % (188548)------------------------------ % 197.84/28.93 % (188548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.84/28.93 % (188548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.84/28.93 % (188548)CaDiCaL version: 2.1.3 % 197.84/28.93 % (188548)Termination reason: Unknown % 197.84/28.93 % (188548)Termination phase: Saturation % 197.84/28.93 % (188548)Time elapsed: 0.360 s % 197.84/28.93 % (188548)Peak memory usage: 114 MB % 197.84/28.93 % (188548)Instructions burned: 543 (million) % 197.84/28.93 % (188552)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 197.84/28.93 % (188552)dis+1011_1_to=kbo:ncem=casc2026/models/loop8.pt:tgt=ground:irw=on:drc=off:sp=unary_first:bce=on:bsr=unit_only:kmz=on:sac=on:random_seed=949616951:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2763 on theBenchmark for (2763ds/21161Mi) % 197.84/28.93 % (188250)Instruction limit reached! % 197.84/28.93 % (188250)------------------------------ % 197.84/28.93 % (188250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 197.84/28.93 % (188250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 197.84/28.93 % (188250)CaDiCaL version: 2.1.3 % 207.63/30.25 % (188250)Termination reason: Instruction limit % 207.63/30.25 % (188250)Termination phase: Saturation % 207.63/30.25 % (188250)Time elapsed: 15.586 s % 207.63/30.25 % (188250)Peak memory usage: 431 MB % 207.63/30.25 % (188250)Instructions burned: 26473 (million) % 207.63/30.25 % (188554)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=4176156228:i=22761:gtg=all:ss=axioms:fsd=on_2754 on theBenchmark for (2754ds/22761Mi) % 207.63/30.25 % (188554)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.63/30.25 % (188554)------------------------------ % 207.63/30.25 % (188554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.63/30.25 % (188554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/30.25 % (188554)CaDiCaL version: 2.1.3 % 207.63/30.25 % (188554)Termination reason: Unknown % 207.63/30.25 % (188554)Termination phase: Saturation % 207.63/30.25 % (188554)Time elapsed: 0.357 s % 207.63/30.25 % (188554)Peak memory usage: 113 MB % 207.63/30.25 % (188554)Instructions burned: 539 (million) % 207.63/30.25 % (188556)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2937183902:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2749 on theBenchmark for (2749ds/23713Mi) % 207.63/30.25 % (188556)Refutation not found, incomplete strategy % 207.63/30.25 % (188556)------------------------------ % 207.63/30.25 % (188556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.63/30.25 % (188556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/30.25 % (188556)CaDiCaL version: 2.1.3 % 207.63/30.25 % (188556)Termination reason: Refutation not found, incomplete strategy % 207.63/30.25 % (188556)Time elapsed: 0.004 s % 207.63/30.25 % (188556)Peak memory usage: 88 MB % 207.63/30.25 % (188556)Instructions burned: 5 (million) % 207.63/30.25 % (188556)------------------------------ % 207.63/30.25 % (188556)------------------------------ % 207.63/30.25 % (188558)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3152502784:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2745 on theBenchmark for (2745ds/26509Mi) % 207.63/30.25 % (188558)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.63/30.25 % (188558)------------------------------ % 207.63/30.25 % (188558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.63/30.25 % (188558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/30.25 % (188558)CaDiCaL version: 2.1.3 % 207.63/30.25 % (188558)Termination reason: Unknown % 207.63/30.25 % (188558)Termination phase: Saturation % 207.63/30.25 % (188558)Time elapsed: 0.370 s % 207.63/30.25 % (188558)Peak memory usage: 114 MB % 207.63/30.25 % (188558)Instructions burned: 541 (million) % 207.63/30.25 % (188560)dis+1011_1_to=kbo:ncem=casc2026/models/loop6.pt:tgt=ground:drc=off:fde=unused:sp=const_frequency:spb=units:bsr=on:sac=on:random_seed=2500987973:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2739 on theBenchmark for (2739ds/28957Mi) % 207.63/30.25 % (188519)Instruction limit reached! % 207.63/30.25 % (188519)------------------------------ % 207.63/30.25 % (188519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.63/30.25 % (188519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/30.25 % (188519)CaDiCaL version: 2.1.3 % 207.63/30.25 % (188519)Termination reason: Instruction limit % 207.63/30.25 % (188519)Termination phase: Saturation % 207.63/30.25 % (188519)Time elapsed: 9.518 s % 207.63/30.25 % (188519)Peak memory usage: 153 MB % 207.63/30.25 % (188519)Instructions burned: 16000 (million) % 207.63/30.25 % (188562)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:drc=off:sp=const_max:spb=goal_then_units:lcm=predicate:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=4087560320:i=29246:s2at=-1:kws=inv_arity:ins=10_2737 on theBenchmark for (2737ds/29246Mi) % 207.63/30.25 % (188562)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.63/30.25 % (188562)------------------------------ % 207.63/30.25 % (188562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.63/30.25 % (188562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.63/30.25 % (188562)CaDiCaL version: 2.1.3 % 207.63/30.25 % (188562)Termination reason: Unknown % 207.63/30.25 % (188562)Termination phase: Saturation % 207.63/30.25 % (188562)Time elapsed: 0.358 s % 207.63/30.25 % (188562)Peak memory usage: 114 MB % 207.63/30.25 % (188562)Instructions burned: 542 (million) % 216.53/31.56 % (188503)Instruction limit reached! % 216.53/31.56 % (188503)------------------------------ % 216.53/31.56 % (188503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.53/31.56 % (188503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.53/31.56 % (188503)CaDiCaL version: 2.1.3 % 216.53/31.56 % (188503)Termination reason: Instruction limit % 216.53/31.56 % (188503)Termination phase: Saturation % 216.53/31.56 % (188503)Time elapsed: 11.674 s % 216.53/31.56 % (188503)Peak memory usage: 170 MB % 216.53/31.56 % (188503)Instructions burned: 19910 (million) % 216.53/31.56 % (188564)ott+1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:sp=weighted_frequency:urr=on:gs=on:s2agt=32:sac=on:random_seed=271618473:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2732 on theBenchmark for (2732ds/30082Mi) % 216.53/31.56 % (188564)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 216.53/31.56 % (188565)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=2059433695:i=32262:bd=preordered_2730 on theBenchmark for (2730ds/32262Mi) % 216.53/31.56 % (188564)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 216.53/31.56 % (188564)------------------------------ % 216.53/31.56 % (188564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.53/31.56 % (188564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.53/31.56 % (188564)CaDiCaL version: 2.1.3 % 216.53/31.56 % (188564)Termination reason: Unknown % 216.53/31.56 % (188564)Termination phase: Saturation % 216.53/31.56 % (188564)Time elapsed: 0.361 s % 216.53/31.56 % (188564)Peak memory usage: 114 MB % 216.53/31.56 % (188564)Instructions burned: 544 (million) % 216.53/31.56 % (188568)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=3975885179:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2726 on theBenchmark for (2726ds/32870Mi) % 216.53/31.56 % (188565)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 216.53/31.56 % (188565)------------------------------ % 216.53/31.56 % (188565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.53/31.56 % (188565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.53/31.56 % (188565)CaDiCaL version: 2.1.3 % 216.53/31.56 % (188565)Termination reason: Unknown % 216.53/31.56 % (188565)Termination phase: Saturation % 216.53/31.56 % (188565)Time elapsed: 0.360 s % 216.53/31.56 % (188565)Peak memory usage: 114 MB % 216.53/31.56 % (188565)Instructions burned: 542 (million) % 216.53/31.56 % (188570)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:prc=on:sp=reverse_frequency:spb=goal:acc=on:kmz=on:random_seed=14257153:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2724 on theBenchmark for (2724ds/33295Mi) % 216.53/31.56 % (188482)Instruction limit reached! % 216.53/31.56 % (188482)------------------------------ % 216.53/31.56 % (188482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.53/31.56 % (188482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.53/31.56 % (188482)CaDiCaL version: 2.1.3 % 216.53/31.56 % (188482)Termination reason: Instruction limit % 216.53/31.56 % (188482)Termination phase: Saturation % 216.53/31.56 % (188482)Time elapsed: 13.798 s % 216.53/31.56 % (188482)Peak memory usage: 324 MB % 216.53/31.56 % (188482)Instructions burned: 43698 (million) % 216.53/31.56 % (188568)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 216.53/31.56 % (188568)------------------------------ % 216.53/31.56 % (188568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.53/31.56 % (188568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.53/31.56 % (188568)CaDiCaL version: 2.1.3 % 216.53/31.56 % (188568)Termination reason: Unknown % 216.53/31.56 % (188568)Termination phase: Saturation % 216.53/31.56 % (188568)Time elapsed: 0.360 s % 216.53/31.56 % (188568)Peak memory usage: 114 MB % 216.53/31.56 % (188568)Instructions burned: 542 (million) % 216.53/31.56 % (188572)dis+11_1_anc=none:sfv=off:to=kbo:ncem=casc2026/models/loop6.pt:lma=off:bsr=unit_only:s2agt=8:kmz=on:sac=on:random_seed=2580607209:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2721 on theBenchmark for (2721ds/36826Mi) % 216.53/31.56 % (188573)lrs-1003_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:spb=goal:bsr=unit_only:gs=on:br=off:flr=on:sac=on:random_seed=4016151333:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2721 on theBenchmark for (2721ds/92981Mi) % 221.71/32.24 % (188570)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.71/32.24 % (188570)------------------------------ % 221.71/32.24 % (188570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.71/32.24 % (188570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.71/32.24 % (188570)CaDiCaL version: 2.1.3 % 221.71/32.24 % (188570)Termination reason: Unknown % 221.71/32.24 % (188570)Termination phase: Saturation % 221.71/32.24 % (188570)Time elapsed: 0.360 s % 221.71/32.24 % (188570)Peak memory usage: 114 MB % 221.71/32.24 % (188570)Instructions burned: 541 (million) % 221.71/32.24 % (188576)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=3821838523:s2pl=on:i=49423_2718 on theBenchmark for (2718ds/49423Mi) % 221.71/32.24 % (188573)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.71/32.24 % (188573)------------------------------ % 221.71/32.24 % (188573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.71/32.24 % (188573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.71/32.24 % (188573)CaDiCaL version: 2.1.3 % 221.71/32.24 % (188573)Termination reason: Unknown % 221.71/32.24 % (188573)Termination phase: Saturation % 221.71/32.24 % (188573)Time elapsed: 0.355 s % 221.71/32.24 % (188573)Peak memory usage: 114 MB % 221.71/32.24 % (188573)Instructions burned: 538 (million) % 221.71/32.24 % (188587)lrs+1002_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:tgt=ground:npcc=on:prc=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:rp=on:updr=off:sac=on:random_seed=2555975181:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2716 on theBenchmark for (2716ds/57299Mi) % 221.71/32.24 % (188576)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.71/32.24 % (188576)------------------------------ % 221.71/32.24 % (188576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.71/32.24 % (188576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.71/32.24 % (188576)CaDiCaL version: 2.1.3 % 221.71/32.24 % (188576)Termination reason: Unknown % 221.71/32.24 % (188576)Termination phase: Saturation % 221.71/32.24 % (188576)Time elapsed: 0.360 s % 221.71/32.24 % (188576)Peak memory usage: 114 MB % 221.71/32.24 % (188576)Instructions burned: 542 (million) % 221.71/32.24 % (188673)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3239734515:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2713 on theBenchmark for (2713ds/127679Mi) % 221.71/32.24 % (188587)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.71/32.24 % (188587)------------------------------ % 221.71/32.24 % (188587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.71/32.24 % (188587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.71/32.24 % (188587)CaDiCaL version: 2.1.3 % 221.71/32.24 % (188587)Termination reason: Unknown % 221.71/32.24 % (188587)Termination phase: Saturation % 221.71/32.24 % (188587)Time elapsed: 0.356 s % 221.71/32.24 % (188587)Peak memory usage: 114 MB % 221.71/32.24 % (188587)Instructions burned: 539 (million) % 221.71/32.24 % (188698)lrs+31_1_anc=all:to=lpo:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_arity:fs=off:lcm=predicate:alpa=false:flr=on:random_seed=2411430698:i=69402:add=on:aac=none:fsr=off_2711 on theBenchmark for (2711ds/69402Mi) % 221.71/32.24 % (188673)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.71/32.24 % (188673)------------------------------ % 221.71/32.24 % (188673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.71/32.24 % (188673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.71/32.24 % (188673)CaDiCaL version: 2.1.3 % 221.71/32.24 % (188673)Termination reason: Unknown % 221.71/32.24 % (188673)Termination phase: Saturation % 221.71/32.24 % (188673)Time elapsed: 0.357 s % 221.71/32.24 % (188673)Peak memory usage: 114 MB % 221.71/32.24 % (188673)Instructions burned: 541 (million) % 221.71/32.24 % (188714)lrs-2_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:drc=off:sas=cadical:sp=reverse_frequency:lcm=predicate:acc=on:bsr=unit_only:fd=preordered:sac=on:random_seed=2743265426:i=100512:doe=on:fgj=on:bd=all:fsd=on_2708 on theBenchmark for (2708ds/100512Mi) % 227.77/33.09 % (188698)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 227.77/33.09 % (188698)------------------------------ % 227.77/33.09 % (188698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.77/33.09 % (188698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.77/33.09 % (188698)CaDiCaL version: 2.1.3 % 227.77/33.09 % (188698)Termination reason: Unknown % 227.77/33.09 % (188698)Termination phase: Saturation % 227.77/33.09 % (188698)Time elapsed: 0.362 s % 227.77/33.09 % (188698)Peak memory usage: 113 MB % 227.77/33.09 % (188698)Instructions burned: 541 (million) % 227.77/33.09 % (188779)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=4214473073:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2706 on theBenchmark for (2706ds/138761Mi) % 227.77/33.09 % (188714)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 227.77/33.09 % (188714)------------------------------ % 227.77/33.09 % (188714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.77/33.09 % (188714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.77/33.09 % (188714)CaDiCaL version: 2.1.3 % 227.77/33.09 % (188714)Termination reason: Unknown % 227.77/33.09 % (188714)Termination phase: Saturation % 227.77/33.09 % (188714)Time elapsed: 0.390 s % 227.77/33.09 % (188714)Peak memory usage: 114 MB % 227.77/33.09 % (188714)Instructions burned: 541 (million) % 227.77/33.09 % (188850)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:si=on:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2410535964:i=282386:rtra=on_2702 on theBenchmark for (2702ds/282386Mi) % 227.77/33.09 % (188779)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 227.77/33.09 % (188779)------------------------------ % 227.77/33.09 % (188779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.77/33.09 % (188779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.77/33.09 % (188779)CaDiCaL version: 2.1.3 % 227.77/33.09 % (188779)Termination reason: Unknown % 227.77/33.09 % (188779)Termination phase: Saturation % 227.77/33.09 % (188779)Time elapsed: 0.374 s % 227.77/33.09 % (188779)Peak memory usage: 114 MB % 227.77/33.09 % (188779)Instructions burned: 541 (million) % 227.77/33.09 % (188915)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:si=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2721048413:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2700 on theBenchmark for (2700ds/269354Mi) % 227.77/33.09 % (188850)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 227.77/33.09 % (188850)------------------------------ % 227.77/33.09 % (188850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.77/33.09 % (188850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.77/33.09 % (188850)CaDiCaL version: 2.1.3 % 227.77/33.09 % (188850)Termination reason: Unknown % 227.77/33.09 % (188850)Termination phase: Saturation % 227.77/33.09 % (188850)Time elapsed: 0.359 s % 227.77/33.09 % (188850)Peak memory usage: 114 MB % 227.77/33.09 % (188850)Instructions burned: 541 (million) % 227.77/33.09 % (188959)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:si=on:sos=all:bsr=unit_only:sac=on:random_seed=4192360155:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2697 on theBenchmark for (2697ds/283390Mi) % 227.77/33.09 % (188959)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 227.77/33.09 % (188915)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 227.77/33.09 % (188915)------------------------------ % 227.77/33.09 % (188915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 227.77/33.09 % (188915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 227.77/33.09 % (188915)CaDiCaL version: 2.1.3 % 227.77/33.09 % (188915)Termination reason: Unknown % 227.77/33.09 % (188915)Termination phase: Saturation % 227.77/33.09 % (188915)Time elapsed: 0.362 s % 227.77/33.09 % (188915)Peak memory usage: 114 MB % 227.77/33.09 % (188915)Instructions burned: 547 (million) % 227.77/33.09 % (189008)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=451540918:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2695 on theBenchmark for (2695ds/218Mi) % 227.77/33.09 % (189008)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 232.41/33.94 % (189008)Refutation not found, incomplete strategy % 232.41/33.94 % (189008)------------------------------ % 232.41/33.94 % (189008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.41/33.94 % (189008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.41/33.94 % (189008)CaDiCaL version: 2.1.3 % 232.41/33.94 % (189008)Termination reason: Refutation not found, incomplete strategy % 232.41/33.94 % (189008)Time elapsed: 0.002 s % 232.41/33.94 % (189008)Peak memory usage: 88 MB % 232.41/33.94 % (189008)Instructions burned: 1 (million) % 232.41/33.94 % (188959)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 232.41/33.94 % (188959)------------------------------ % 232.41/33.94 % (188959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.41/33.94 % (188959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.41/33.94 % (188959)CaDiCaL version: 2.1.3 % 232.41/33.94 % (188959)Termination reason: Unknown % 232.41/33.94 % (188959)Termination phase: Saturation % 232.41/33.94 % (188959)Time elapsed: 0.359 s % 232.41/33.94 % (188959)Peak memory usage: 114 MB % 232.41/33.94 % (188959)Instructions burned: 542 (million) % 232.41/33.94 % (189008)------------------------------ % 232.41/33.94 % (189008)------------------------------ % 232.41/33.94 % (188225)Instruction limit reached! % 232.41/33.94 % (188225)------------------------------ % 232.41/33.94 % (188225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.41/33.94 % (188225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.41/33.94 % (188225)CaDiCaL version: 2.1.3 % 232.41/33.94 % (188225)Termination reason: Instruction limit % 232.41/33.94 % (188225)Termination phase: Saturation % 232.41/33.94 % (188225)Time elapsed: 24.263 s % 232.41/33.94 % (188225)Peak memory usage: 211 MB % 232.41/33.94 % (188225)Instructions burned: 33335 (million) % 232.41/33.94 % (189010)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=3510773987:i=238:av=off:rtra=on:ss=axioms_2692 on theBenchmark for (2692ds/238Mi) % 232.41/33.94 % (189010)Refutation not found, incomplete strategy % 232.41/33.94 % (189010)------------------------------ % 232.41/33.94 % (189010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.41/33.94 % (189010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.41/33.94 % (189010)CaDiCaL version: 2.1.3 % 232.41/33.94 % (189010)Termination reason: Refutation not found, incomplete strategy % 232.41/33.94 % (189010)Time elapsed: 0.002 s % 232.41/33.94 % (189010)Peak memory usage: 88 MB % 232.41/33.94 % (189010)Instructions burned: 2 (million) % 232.41/33.94 % (189011)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=964076779:s2a=on:i=278:rtra=on:gtg=position_2691 on theBenchmark for (2691ds/278Mi) % 232.41/33.94 % (189013)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=793876830:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2690 on theBenchmark for (2690ds/258Mi) % 232.41/33.94 % (189010)------------------------------ % 232.41/33.94 % (189010)------------------------------ % 232.41/33.94 % (189013)Instruction limit reached! % 232.41/33.94 % (189013)------------------------------ % 232.41/33.94 % (189013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.41/33.94 % (189013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.41/33.94 % (189013)CaDiCaL version: 2.1.3 % 232.41/33.94 % (189013)Termination reason: Instruction limit % 232.41/33.94 % (189013)Termination phase: Saturation % 232.41/33.94 % (189013)Time elapsed: 0.117 s % 232.41/33.94 % (189013)Peak memory usage: 90 MB % 232.41/33.94 % (189013)Instructions burned: 258 (million) % 232.41/33.94 % (189011)Instruction limit reached! % 232.41/33.94 % (189011)------------------------------ % 232.41/33.94 % (189011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.41/33.94 % (189011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.41/33.94 % (189011)CaDiCaL version: 2.1.3 % 232.41/33.94 % (189011)Termination reason: Instruction limit % 232.41/33.94 % (189011)Termination phase: Saturation % 232.41/33.94 % (189011)Time elapsed: 0.175 s % 232.41/33.94 % (189011)Peak memory usage: 91 MB % 232.41/33.94 % (189011)Instructions burned: 279 (million) % 232.41/33.94 % (189016)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3645168541:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2688 on theBenchmark for (2688ds/570Mi) % 232.41/33.94 % (189016)Refutation not found, incomplete strategy % 232.41/33.94 % (189016)------------------------------ % 232.41/33.94 % (189016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.46/34.64 % (189016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.46/34.64 % (189016)CaDiCaL version: 2.1.3 % 238.46/34.64 % (189016)Termination reason: Refutation not found, incomplete strategy % 238.46/34.64 % (189016)Time elapsed: 0.003 s % 238.46/34.64 % (189016)Peak memory usage: 89 MB % 238.46/34.64 % (189016)Instructions burned: 3 (million) % 238.46/34.64 % (189018)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=2389687219:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2687 on theBenchmark for (2687ds/650Mi) % 238.46/34.64 % (189017)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=899918445:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2687 on theBenchmark for (2687ds/314Mi) % 238.46/34.64 % (189018)Refutation not found, incomplete strategy % 238.46/34.64 % (189018)------------------------------ % 238.46/34.64 % (189018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.46/34.64 % (189018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.46/34.64 % (189018)CaDiCaL version: 2.1.3 % 238.46/34.64 % (189018)Termination reason: Refutation not found, incomplete strategy % 238.46/34.64 % (189018)Time elapsed: 0.003 s % 238.46/34.64 % (189018)Peak memory usage: 89 MB % 238.46/34.64 % (189018)Instructions burned: 3 (million) % 238.46/34.64 % (189017)Instruction limit reached! % 238.46/34.64 % (189017)------------------------------ % 238.46/34.64 % (189017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.46/34.64 % (189017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.46/34.64 % (189017)CaDiCaL version: 2.1.3 % 238.46/34.64 % (189017)Termination reason: Instruction limit % 238.46/34.64 % (189017)Termination phase: Saturation % 238.46/34.64 % (189017)Time elapsed: 0.141 s % 238.46/34.64 % (189017)Peak memory usage: 89 MB % 238.46/34.64 % (189017)Instructions burned: 316 (million) % 238.46/34.64 % (189016)------------------------------ % 238.46/34.64 % (189016)------------------------------ % 238.46/34.64 % (189018)------------------------------ % 238.46/34.64 % (189018)------------------------------ % 238.46/34.64 % (189022)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:si=on:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3896764387:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2684 on theBenchmark for (2684ds/496Mi) % 238.46/34.64 % (189023)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=3321429075:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2684 on theBenchmark for (2684ds/588Mi) % 238.46/34.64 % (189024)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=1241755356:i=4700:rtra=on_2683 on theBenchmark for (2683ds/4700Mi) % 238.46/34.64 % (189022)Instruction limit reached! % 238.46/34.64 % (189022)------------------------------ % 238.46/34.64 % (189022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.46/34.64 % (189022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.46/34.64 % (189022)CaDiCaL version: 2.1.3 % 238.46/34.64 % (189022)Termination reason: Instruction limit % 238.46/34.64 % (189022)Termination phase: Saturation % 238.46/34.64 % (189022)Time elapsed: 0.223 s % 238.46/34.64 % (189022)Peak memory usage: 90 MB % 238.46/34.64 % (189022)Instructions burned: 498 (million) % 238.46/34.64 % (189023)Instruction limit reached! % 238.46/34.64 % (189023)------------------------------ % 238.46/34.64 % (189023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.46/34.64 % (189023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.46/34.64 % (189023)CaDiCaL version: 2.1.3 % 238.46/34.64 % (189023)Termination reason: Instruction limit % 238.46/34.64 % (189023)Termination phase: Saturation % 238.46/34.64 % (189023)Time elapsed: 0.303 s % 238.46/34.64 % (189023)Peak memory usage: 94 MB % 238.46/34.64 % (189023)Instructions burned: 589 (million) % 238.46/34.64 % (189028)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=195402168:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2680 on theBenchmark for (2680ds/226Mi) % 238.46/34.64 % (189024)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 238.46/34.64 % (189024)------------------------------ % 238.46/34.64 % (189024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.46/34.64 % (189024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.46/34.64 % (189024)CaDiCaL version: 2.1.3 % 238.46/34.64 % (189024)Termination reason: Unknown % 238.46/34.64 % (189024)Termination phase: Saturation % 238.46/34.64 % (189024)Time elapsed: 0.360 s % 244.27/35.58 % (189024)Peak memory usage: 114 MB % 244.27/35.58 % (189024)Instructions burned: 541 (million) % 244.27/35.58 % (189029)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=32552740:i=254:av=off:fsr=off:rtra=on:sup=off_2679 on theBenchmark for (2679ds/254Mi) % 244.27/35.58 % (189028)Instruction limit reached! % 244.27/35.58 % (189028)------------------------------ % 244.27/35.58 % (189028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.27/35.58 % (189028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.27/35.58 % (189028)CaDiCaL version: 2.1.3 % 244.27/35.58 % (189028)Termination reason: Instruction limit % 244.27/35.58 % (189028)Termination phase: Saturation % 244.27/35.58 % (189028)Time elapsed: 0.137 s % 244.27/35.58 % (189028)Peak memory usage: 93 MB % 244.27/35.58 % (189028)Instructions burned: 226 (million) % 244.27/35.58 % (189029)Instruction limit reached! % 244.27/35.58 % (189029)------------------------------ % 244.27/35.58 % (189029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.27/35.58 % (189029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.27/35.58 % (189029)CaDiCaL version: 2.1.3 % 244.27/35.58 % (189029)Termination reason: Instruction limit % 244.27/35.58 % (189029)Termination phase: Saturation % 244.27/35.58 % (189029)Time elapsed: 0.114 s % 244.27/35.58 % (189029)Peak memory usage: 89 MB % 244.27/35.58 % (189029)Instructions burned: 254 (million) % 244.27/35.58 % (189031)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=1936846908:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2678 on theBenchmark for (2678ds/228Mi) % 244.27/35.58 % (189033)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3527435279:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2678 on theBenchmark for (2678ds/1814Mi) % 244.27/35.58 % (189031)Instruction limit reached! % 244.27/35.58 % (189031)------------------------------ % 244.27/35.58 % (189031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.27/35.58 % (189031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.27/35.58 % (189031)CaDiCaL version: 2.1.3 % 244.27/35.58 % (189031)Termination reason: Instruction limit % 244.27/35.58 % (189031)Termination phase: Saturation % 244.27/35.58 % (189031)Time elapsed: 0.132 s % 244.27/35.58 % (189031)Peak memory usage: 89 MB % 244.27/35.58 % (189031)Instructions burned: 229 (million) % 244.27/35.58 % (189034)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=3784733294:i=874:sd=1:aac=none:rtra=on:ss=included_2676 on theBenchmark for (2676ds/874Mi) % 244.27/35.58 % (189034)Refutation not found, incomplete strategy % 244.27/35.58 % (189034)------------------------------ % 244.27/35.58 % (189034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.27/35.58 % (189034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.27/35.58 % (189034)CaDiCaL version: 2.1.3 % 244.27/35.58 % (189034)Termination reason: Refutation not found, incomplete strategy % 244.27/35.58 % (189034)Time elapsed: 0.008 s % 244.27/35.58 % (189034)Peak memory usage: 89 MB % 244.27/35.58 % (189034)Instructions burned: 12 (million) % 244.27/35.58 % (189037)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=2004047335:i=10404:rtra=on:ss=axioms:sgt=16_2675 on theBenchmark for (2675ds/10404Mi) % 244.27/35.58 % (189034)------------------------------ % 244.27/35.58 % (189034)------------------------------ % 244.27/35.58 % (189040)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3187980387:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2672 on theBenchmark for (2672ds/268Mi) % 244.27/35.58 % (189037)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 244.27/35.58 % (189037)------------------------------ % 244.27/35.58 % (189037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.27/35.58 % (189037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.27/35.58 % (189037)CaDiCaL version: 2.1.3 % 244.27/35.58 % (189037)Termination reason: Unknown % 244.27/35.58 % (189037)Termination phase: Saturation % 244.27/35.58 % (189037)Time elapsed: 0.358 s % 244.27/35.58 % (189037)Peak memory usage: 114 MB % 244.27/35.58 % (189037)Instructions burned: 540 (million) % 244.27/35.58 % (189040)Instruction limit reached! % 244.27/35.58 % (189040)------------------------------ % 244.27/35.58 % (189040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.27/35.58 % (189040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.27/35.58 % (189040)CaDiCaL version: 2.1.3 % 252.93/36.62 % (189040)Termination reason: Instruction limit % 252.93/36.62 % (189040)Termination phase: Saturation % 252.93/36.62 % (189040)Time elapsed: 0.142 s % 252.93/36.62 % (189040)Peak memory usage: 91 MB % 252.93/36.62 % (189040)Instructions burned: 269 (million) % 252.93/36.62 % (189042)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=2594066443:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2670 on theBenchmark for (2670ds/1184Mi) % 252.93/36.62 % (189042)Refutation not found, incomplete strategy % 252.93/36.62 % (189042)------------------------------ % 252.93/36.62 % (189042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.93/36.62 % (189042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.93/36.62 % (189042)CaDiCaL version: 2.1.3 % 252.93/36.62 % (189042)Termination reason: Refutation not found, incomplete strategy % 252.93/36.62 % (189042)Time elapsed: 0.007 s % 252.93/36.62 % (189042)Peak memory usage: 88 MB % 252.93/36.62 % (189042)Instructions burned: 11 (million) % 252.93/36.62 % (189043)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=700305601:st=3:i=26386:sd=3:rtra=on:ss=axioms_2669 on theBenchmark for (2669ds/26386Mi) % 252.93/36.62 % (189033)Instruction limit reached! % 252.93/36.62 % (189033)------------------------------ % 252.93/36.62 % (189033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.93/36.62 % (189033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.93/36.62 % (189033)CaDiCaL version: 2.1.3 % 252.93/36.62 % (189033)Termination reason: Instruction limit % 252.93/36.62 % (189033)Termination phase: Saturation % 252.93/36.62 % (189033)Time elapsed: 0.927 s % 252.93/36.62 % (189033)Peak memory usage: 113 MB % 252.93/36.62 % (189033)Instructions burned: 1815 (million) % 252.93/36.62 % (189042)------------------------------ % 252.93/36.62 % (189042)------------------------------ % 252.93/36.62 % (189046)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:si=on:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1712125982:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2667 on theBenchmark for (2667ds/250Mi) % 252.93/36.62 % (189046)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 252.93/36.62 % (189047)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=4106647987:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2666 on theBenchmark for (2666ds/268Mi) % 252.93/36.62 % (189043)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 252.93/36.62 % (189043)------------------------------ % 252.93/36.62 % (189043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.93/36.62 % (189043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.93/36.62 % (189043)CaDiCaL version: 2.1.3 % 252.93/36.62 % (189043)Termination reason: Unknown % 252.93/36.62 % (189043)Termination phase: Saturation % 252.93/36.62 % (189043)Time elapsed: 0.363 s % 252.93/36.62 % (189043)Peak memory usage: 114 MB % 252.93/36.62 % (189043)Instructions burned: 539 (million) % 252.93/36.62 % (189046)Instruction limit reached! % 252.93/36.62 % (189046)------------------------------ % 252.93/36.62 % (189046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.93/36.62 % (189046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.93/36.62 % (189046)CaDiCaL version: 2.1.3 % 252.93/36.62 % (189046)Termination reason: Instruction limit % 252.93/36.62 % (189046)Termination phase: Saturation % 252.93/36.62 % (189046)Time elapsed: 0.153 s % 252.93/36.62 % (189046)Peak memory usage: 91 MB % 252.93/36.62 % (189046)Instructions burned: 250 (million) % 252.93/36.62 % (189047)Instruction limit reached! % 252.93/36.62 % (189047)------------------------------ % 252.93/36.62 % (189047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.93/36.62 % (189047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.93/36.62 % (189047)CaDiCaL version: 2.1.3 % 252.93/36.62 % (189047)Termination reason: Instruction limit % 252.93/36.62 % (189047)Termination phase: Saturation % 252.93/36.62 % (189047)Time elapsed: 0.137 s % 252.93/36.62 % (189047)Peak memory usage: 90 MB % 252.93/36.62 % (189047)Instructions burned: 269 (million) % 252.93/36.62 % (189050)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=365857690:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2664 on theBenchmark for (2664ds/282Mi) % 252.93/36.62 % (189050)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 265.15/38.39 % (189050)Refutation not found, incomplete strategy % 265.15/38.39 % (189050)------------------------------ % 265.15/38.39 % (189050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.15/38.39 % (189050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.15/38.39 % (189050)CaDiCaL version: 2.1.3 % 265.15/38.39 % (189050)Termination reason: Refutation not found, incomplete strategy % 265.15/38.39 % (189050)Time elapsed: 0.002 s % 265.15/38.39 % (189050)Peak memory usage: 88 MB % 265.15/38.39 % (189050)Instructions burned: 1 (million) % 265.15/38.39 % (189051)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=1550474995:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2663 on theBenchmark for (2663ds/862Mi) % 265.15/38.39 % (189052)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:si=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2049833437:i=12120:aac=none:ins=25:rtra=on_2663 on theBenchmark for (2663ds/12120Mi) % 265.15/38.39 % (189050)------------------------------ % 265.15/38.39 % (189050)------------------------------ % 265.15/38.39 % (189056)lrs+10_16_anc=all:slsqr=32,1:sil=8000:si=on:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=571306025:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2660 on theBenchmark for (2660ds/300Mi) % 265.15/38.39 % (189056)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 265.15/38.39 % (189051)Instruction limit reached! % 265.15/38.39 % (189051)------------------------------ % 265.15/38.39 % (189051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.15/38.39 % (189051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.15/38.39 % (189051)CaDiCaL version: 2.1.3 % 265.15/38.39 % (189051)Termination reason: Instruction limit % 265.15/38.39 % (189051)Termination phase: Saturation % 265.15/38.39 % (189051)Time elapsed: 0.436 s % 265.15/38.39 % (189051)Peak memory usage: 96 MB % 265.15/38.39 % (189051)Instructions burned: 862 (million) % 265.15/38.39 % (189052)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 265.15/38.39 % (189052)------------------------------ % 265.15/38.39 % (189052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.15/38.39 % (189052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.15/38.39 % (189052)CaDiCaL version: 2.1.3 % 265.15/38.39 % (189052)Termination reason: Unknown % 265.15/38.39 % (189052)Termination phase: Saturation % 265.15/38.39 % (189052)Time elapsed: 0.360 s % 265.15/38.39 % (189052)Peak memory usage: 114 MB % 265.15/38.39 % (189052)Instructions burned: 542 (million) % 265.15/38.39 % (189056)Instruction limit reached! % 265.15/38.39 % (189056)------------------------------ % 265.15/38.39 % (189056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.15/38.39 % (189056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.15/38.39 % (189056)CaDiCaL version: 2.1.3 % 265.15/38.39 % (189056)Termination reason: Instruction limit % 265.15/38.39 % (189056)Termination phase: Saturation % 265.15/38.39 % (189056)Time elapsed: 0.142 s % 265.15/38.39 % (189056)Peak memory usage: 90 MB % 265.15/38.39 % (189056)Instructions burned: 301 (million) % 265.15/38.39 % (189058)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=3492910225:i=28310:bd=all:rtra=on_2658 on theBenchmark for (2658ds/28310Mi) % 265.15/38.39 % (189059)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3669370216:i=1334:av=off:fsr=off:rtra=on_2657 on theBenchmark for (2657ds/1334Mi) % 265.15/38.39 % (189060)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:si=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2742616311:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2657 on theBenchmark for (2657ds/370Mi) % 265.15/38.39 % (189060)Instruction limit reached! % 265.15/38.39 % (189060)------------------------------ % 265.15/38.39 % (189060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.15/38.39 % (189060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.15/38.39 % (189060)CaDiCaL version: 2.1.3 % 265.15/38.39 % (189060)Termination reason: Instruction limit % 265.15/38.39 % (189060)Termination phase: Saturation % 265.15/38.39 % (189060)Time elapsed: 0.224 s % 265.15/38.39 % (189060)Peak memory usage: 92 MB % 265.15/38.39 % (189060)Instructions burned: 370 (million) % 279.13/40.35 % (189058)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 279.13/40.35 % (189058)------------------------------ % 279.13/40.35 % (189058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.13/40.35 % (189058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.13/40.35 % (189058)CaDiCaL version: 2.1.3 % 279.13/40.35 % (189058)Termination reason: Unknown % 279.13/40.35 % (189058)Termination phase: Saturation % 279.13/40.35 % (189058)Time elapsed: 0.359 s % 279.13/40.35 % (189058)Peak memory usage: 114 MB % 279.13/40.35 % (189058)Instructions burned: 541 (million) % 279.13/40.35 % (189064)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=1800236350:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2653 on theBenchmark for (2653ds/386Mi) % 279.13/40.35 % (189064)Refutation not found, incomplete strategy % 279.13/40.35 % (189064)------------------------------ % 279.13/40.35 % (189064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.13/40.35 % (189064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.13/40.35 % (189064)CaDiCaL version: 2.1.3 % 279.13/40.35 % (189064)Termination reason: Refutation not found, incomplete strategy % 279.13/40.35 % (189064)Time elapsed: 0.003 s % 279.13/40.35 % (189064)Peak memory usage: 89 MB % 279.13/40.35 % (189064)Instructions burned: 2 (million) % 279.13/40.35 % (189065)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=1228540947:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2652 on theBenchmark for (2652ds/9700Mi) % 279.13/40.35 % (189059)Instruction limit reached! % 279.13/40.35 % (189059)------------------------------ % 279.13/40.35 % (189059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.13/40.35 % (189059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.13/40.35 % (189059)CaDiCaL version: 2.1.3 % 279.13/40.35 % (189059)Termination reason: Instruction limit % 279.13/40.35 % (189059)Termination phase: Saturation % 279.13/40.35 % (189059)Time elapsed: 0.636 s % 279.13/40.35 % (189059)Peak memory usage: 96 MB % 279.13/40.35 % (189059)Instructions burned: 1335 (million) % 279.13/40.35 % (189064)------------------------------ % 279.13/40.35 % (189064)------------------------------ % 279.13/40.35 % (189068)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:random_seed=1930067932:i=24222:sd=1:rtra=on:ss=included_2650 on theBenchmark for (2650ds/24222Mi) % 279.13/40.35 % (189069)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=770670619:i=638:kws=precedence:fsr=off:rtra=on_2649 on theBenchmark for (2649ds/638Mi) % 279.13/40.35 % (189068)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 279.13/40.35 % (189068)------------------------------ % 279.13/40.35 % (189068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.13/40.35 % (189068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.13/40.35 % (189068)CaDiCaL version: 2.1.3 % 279.13/40.35 % (189068)Termination reason: Unknown % 279.13/40.35 % (189068)Termination phase: Saturation % 279.13/40.35 % (189068)Time elapsed: 0.359 s % 279.13/40.35 % (189068)Peak memory usage: 114 MB % 279.13/40.35 % (189068)Instructions burned: 542 (million) % 279.13/40.35 % (189069)Instruction limit reached! % 279.13/40.35 % (189069)------------------------------ % 279.13/40.35 % (189069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.13/40.35 % (189069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.13/40.35 % (189069)CaDiCaL version: 2.1.3 % 279.13/40.35 % (189069)Termination reason: Instruction limit % 279.13/40.35 % (189069)Termination phase: Saturation % 279.13/40.35 % (189069)Time elapsed: 0.384 s % 279.13/40.35 % (189069)Peak memory usage: 95 MB % 279.13/40.35 % (189069)Instructions burned: 638 (million) % 279.13/40.35 % (189072)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1996714483:i=4128:ep=RST:rtra=on_2644 on theBenchmark for (2644ds/4128Mi) % 279.13/40.35 % (189072)Refutation not found, incomplete strategy % 279.13/40.35 % (189072)------------------------------ % 279.13/40.35 % (189072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 279.13/40.35 % (189072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 279.13/40.35 % (189072)CaDiCaL version: 2.1.3 % 279.13/40.35 % (189072)Termination reason: Refutation not found, incomplete strategy % 279.13/40.35 % (189072)Time elapsed: 0.007 s % 279.13/40.35 % (189072)Peak memory usage: 88 MB % 284.51/41.13 % (189072)Instructions burned: 11 (million) % 284.51/41.13 % (189073)dis-1011_128_sil=32000:si=on:random_seed=1229030932:i=7412:ep=RST:av=off:rtra=on_2643 on theBenchmark for (2643ds/7412Mi) % 284.51/41.13 % (189072)------------------------------ % 284.51/41.13 % (189072)------------------------------ % 284.51/41.13 % (189076)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2241208066:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2640 on theBenchmark for (2640ds/1514Mi) % 284.51/41.13 % (189076)Refutation not found, incomplete strategy % 284.51/41.13 % (189076)------------------------------ % 284.51/41.13 % (189076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.51/41.13 % (189076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.51/41.13 % (189076)CaDiCaL version: 2.1.3 % 284.51/41.13 % (189076)Termination reason: Refutation not found, incomplete strategy % 284.51/41.13 % (189076)Time elapsed: 0.008 s % 284.51/41.13 % (189076)Peak memory usage: 89 MB % 284.51/41.13 % (189076)Instructions burned: 12 (million) % 284.51/41.13 % (189076)------------------------------ % 284.51/41.13 % (189076)------------------------------ % 284.51/41.13 % (189078)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=4189412978:i=27826:rtra=on:ss=axioms:sgt=8_2636 on theBenchmark for (2636ds/27826Mi) % 284.51/41.13 % (188552)Instruction limit reached! % 284.51/41.13 % (188552)------------------------------ % 284.51/41.13 % (188552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.51/41.13 % (188552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.51/41.13 % (188552)CaDiCaL version: 2.1.3 % 284.51/41.13 % (188552)Termination reason: Instruction limit % 284.51/41.13 % (188552)Termination phase: Saturation % 284.51/41.13 % (188552)Time elapsed: 13.071 s % 284.51/41.13 % (188552)Peak memory usage: 217 MB % 284.51/41.13 % (188552)Instructions burned: 21161 (million) % 284.51/41.13 % (189078)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 284.51/41.13 % (189078)------------------------------ % 284.51/41.13 % (189078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.51/41.13 % (189078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.51/41.13 % (189078)CaDiCaL version: 2.1.3 % 284.51/41.13 % (189078)Termination reason: Unknown % 284.51/41.13 % (189078)Termination phase: Saturation % 284.51/41.13 % (189078)Time elapsed: 0.355 s % 284.51/41.13 % (189078)Peak memory usage: 113 MB % 284.51/41.13 % (189078)Instructions burned: 538 (million) % 284.51/41.13 % (189081)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=965064941:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2631 on theBenchmark for (2631ds/4958Mi) % 284.51/41.13 % (189080)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=4118519212:i=19850:aac=none:rtra=on_2631 on theBenchmark for (2631ds/19850Mi) % 284.51/41.13 % (189081)Refutation not found, incomplete strategy % 284.51/41.13 % (189081)------------------------------ % 284.51/41.13 % (189081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.51/41.13 % (189081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.51/41.13 % (189081)CaDiCaL version: 2.1.3 % 284.51/41.13 % (189081)Termination reason: Refutation not found, incomplete strategy % 284.51/41.13 % (189081)Time elapsed: 0.002 s % 284.51/41.13 % (189081)Peak memory usage: 88 MB % 284.51/41.13 % (189081)Instructions burned: 2 (million) % 284.51/41.13 % (189081)------------------------------ % 284.51/41.13 % (189081)------------------------------ % 284.51/41.13 % (189080)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 284.51/41.13 % (189080)------------------------------ % 284.51/41.13 % (189080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.51/41.13 % (189080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.51/41.13 % (189080)CaDiCaL version: 2.1.3 % 284.51/41.13 % (189080)Termination reason: Unknown % 284.51/41.13 % (189080)Termination phase: Saturation % 284.51/41.13 % (189080)Time elapsed: 0.359 s % 284.51/41.13 % (189080)Peak memory usage: 114 MB % 284.51/41.13 % (189080)Instructions burned: 541 (million) % 284.51/41.13 % (189084)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=696752150:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2627 on theBenchmark for (2627ds/880Mi) % 284.51/41.13 % (189084)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 299.92/43.29 % (189085)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:si=on:erd=off:lsd=100:bsr=unit_only:random_seed=2341142204:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2625 on theBenchmark for (2625ds/22290Mi) % 299.92/43.29 % (189085)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 299.92/43.29 % (189085)------------------------------ % 299.92/43.29 % (189085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.92/43.29 % (189085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.92/43.29 % (189085)CaDiCaL version: 2.1.3 % 299.92/43.29 % (189085)Termination reason: Unknown % 299.92/43.29 % (189085)Termination phase: Saturation % 299.92/43.29 % (189085)Time elapsed: 0.354 s % 299.92/43.29 % (189085)Peak memory usage: 113 MB % 299.92/43.29 % (189085)Instructions burned: 537 (million) % 299.92/43.29 % (189084)Instruction limit reached! % 299.92/43.29 % (189084)------------------------------ % 299.92/43.29 % (189084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.92/43.29 % (189084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.92/43.29 % (189084)CaDiCaL version: 2.1.3 % 299.92/43.29 % (189084)Termination reason: Instruction limit % 299.92/43.29 % (189084)Termination phase: Saturation % 299.92/43.29 % (189084)Time elapsed: 0.475 s % 299.92/43.29 % (189084)Peak memory usage: 94 MB % 299.92/43.29 % (189084)Instructions burned: 881 (million) % 299.92/43.29 % (189089)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=3459788810:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2620 on theBenchmark for (2620ds/1048Mi) % 299.92/43.29 % (189088)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3119887638:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2620 on theBenchmark for (2620ds/6068Mi) % 299.92/43.29 % (189088)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 299.92/43.29 % (189088)------------------------------ % 299.92/43.29 % (189088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.92/43.29 % (189088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.92/43.29 % (189088)CaDiCaL version: 2.1.3 % 299.92/43.29 % (189088)Termination reason: Unknown % 299.92/43.29 % (189088)Termination phase: Saturation % 299.92/43.29 % (189088)Time elapsed: 0.359 s % 299.92/43.29 % (189088)Peak memory usage: 113 MB % 299.92/43.29 % (189088)Instructions burned: 543 (million) % 299.92/43.29 % (189089)Instruction limit reached! % 299.92/43.29 % (189089)------------------------------ % 299.92/43.29 % (189089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.92/43.29 % (189089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.92/43.29 % (189089)CaDiCaL version: 2.1.3 % 299.92/43.29 % (189089)Termination reason: Instruction limit % 299.92/43.29 % (189089)Termination phase: Saturation % 299.92/43.29 % (189089)Time elapsed: 0.508 s % 299.92/43.29 % (189089)Peak memory usage: 95 MB % 299.92/43.29 % (189089)Instructions burned: 1049 (million) % 299.92/43.29 % (189092)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=1848929923:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2615 on theBenchmark for (2615ds/2032Mi) % 299.92/43.29 % (189093)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=1859200623:i=28246:bd=preordered:ins=4:rtra=on_2613 on theBenchmark for (2613ds/28246Mi) % 299.92/43.29 % (189093)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 299.92/43.29 % (189093)------------------------------ % 299.92/43.29 % (189093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 299.92/43.29 % (189093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 299.92/43.29 % (189093)CaDiCaL version: 2.1.3 % 299.92/43.29 % (189093)Termination reason: Unknown % 299.92/43.29 % (189093)Termination phase: Saturation % 299.92/43.29 % (189093)Time elapsed: 0.356 s % 299.92/43.29 % (189093)Peak memory usage: 114 MB % 299.92/43.29 % (189093)Instructions burned: 541 (million) % 299.92/43.29 % (189096)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=4293457648:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2608 on theBenchmark for (2608ds/11562Mi) % 299.92/43.29 % (188572)Instruction limit reached! % 299.92/43.29 % (188572)------------------------------ % 299.92/43.29 % (188572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.33 % (188572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.33 % (188572)CaDiCaL version: 2.1.3 % 300.68/43.33 % (188572)Termination reason: Instruction limit % 300.68/43.33 % (188572)Termination phase: Saturation % 300.68/43.33 % (188572)Time elapsed: 11.490 s % 300.68/43.33 % (188572)Peak memory usage: 256 MB % 300.68/43.33 % (188572)Instructions burned: 36829 (million) % 300.68/43.33 % (189092)Instruction limit reached! % 300.68/43.33 % (189092)------------------------------ % 300.68/43.33 % (189092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.33 % (189092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.33 % (189092)CaDiCaL version: 2.1.3 % 300.68/43.33 % (189092)Termination reason: Instruction limit % 300.68/43.33 % (189092)Termination phase: Saturation % 300.68/43.33 % (189092)Time elapsed: 0.892 s % 300.68/43.33 % (189092)Peak memory usage: 94 MB % 300.68/43.33 % (189092)Instructions burned: 2034 (million) % 300.68/43.33 % (189098)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:si=on:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2870917038:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2605 on theBenchmark for (2605ds/4896Mi) % 300.68/43.34 % (189099)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=3178539001:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2604 on theBenchmark for (2604ds/6446Mi) % 300.68/43.34 % (189098)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.68/43.34 % (189098)------------------------------ % 300.68/43.34 % (189098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.34 % (189098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.34 % (189098)CaDiCaL version: 2.1.3 % 300.68/43.34 % (189098)Termination reason: Unknown % 300.68/43.34 % (189098)Termination phase: Saturation % 300.68/43.34 % (189098)Time elapsed: 0.196 s % 300.68/43.34 % (189098)Peak memory usage: 114 MB % 300.68/43.34 % (189098)Instructions burned: 543 (million) % 300.68/43.34 % (189102)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=2030167247:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2602 on theBenchmark for (2602ds/4066Mi) % 300.68/43.34 % (189099)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.68/43.34 % (189099)------------------------------ % 300.68/43.34 % (189099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.34 % (189099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.34 % (189099)CaDiCaL version: 2.1.3 % 300.68/43.34 % (189099)Termination reason: Unknown % 300.68/43.34 % (189099)Termination phase: Saturation % 300.68/43.34 % (189099)Time elapsed: 0.358 s % 300.68/43.34 % (189099)Peak memory usage: 114 MB % 300.68/43.34 % (189099)Instructions burned: 542 (million) % 300.68/43.34 % (189102)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.68/43.34 % (189102)------------------------------ % 300.68/43.34 % (189102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.34 % (189102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.34 % (189102)CaDiCaL version: 2.1.3 % 300.68/43.34 % (189102)Termination reason: Unknown % 300.68/43.34 % (189102)Termination phase: Saturation % 300.68/43.34 % (189102)Time elapsed: 0.194 s % 300.68/43.34 % (189102)Peak memory usage: 114 MB % 300.68/43.34 % (189102)Instructions burned: 541 (million) % 300.68/43.34 % (189073)Instruction limit reached! % 300.68/43.34 % (189073)------------------------------ % 300.68/43.34 % (189073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.34 % (189073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.34 % (189073)CaDiCaL version: 2.1.3 % 300.68/43.34 % (189073)Termination reason: Instruction limit % 300.68/43.34 % (189073)Termination phase: Saturation % 300.68/43.34 % (189073)Time elapsed: 4.334 s % 300.68/43.34 % (189073)Peak memory usage: 156 MB % 300.68/43.34 % (189073)Instructions burned: 7412 (million) % 300.68/43.34 % (189105)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:si=on:sp=const_frequency:spb=goal:acc=on:random_seed=1101149627:i=43222:sd=3:rtra=on:ss=axioms_2599 on theBenchmark for (2599ds/43222Mi) % 300.68/43.34 % (189104)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=4183463507:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2599 on theBenchmark for (2599ds/4110Mi) % 300.68/43.34 % (189106)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=1792040775:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2598 on theBenchmark for (2598ds/9670Mi) % 300.68/43.34 % (189105)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.68/43.34 % (189105)------------------------------ % 300.68/43.34 % (189105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.34 % (189105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.34 % (189105)CaDiCaL version: 2.1.3 % 300.68/43.34 % (189105)Termination reason: Unknown % 300.68/43.34 % (189105)Termination phase: Saturation % 300.68/43.34 % (189105)Time elapsed: 0.194 s % 300.68/43.34 % (189105)Peak memory usage: 113 MB % 300.68/43.34 % (189105)Instructions burned: 536 (million) % 300.68/43.34 % (189110)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:si=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1814227583:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2596 on theBenchmark for (2596ds/1594Mi) % 300.68/43.34 % (189104)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.68/43.34 % (189104)------------------------------ % 300.68/43.34 % (189104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.34 % (189104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.34 % (189104)CaDiCaL version: 2.1.3 % 300.68/43.34 % (189104)Termination reason: Unknown % 300.68/43.34 % (189104)Termination phase: Saturation % 300.68/43.34 % (189104)Time elapsed: 0.357 s % 300.68/43.34 % (189104)Peak memory usage: 113 MB % 300.68/43.34 % (189104)Instructions burned: 537 (million) % 300.68/43.34 % (189065)Instruction limit reached! % 300.68/43.34 % (189065)------------------------------ % 300.68/43.34 % (189065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.34 % (189065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.34 % (189065)CaDiCaL version: 2.1.3 % 300.68/43.34 % (189065)Termination reason: Instruction limit % 300.68/43.34 % (189065)Termination phase: Saturation % 300.68/43.34 % (189065)Time elapsed: 5.707 s % 300.68/43.34 % (189065)Peak memory usage: 130 MB % 300.68/43.34 % (189065)Instructions burned: 9701 (million) % 300.68/43.34 % (189112)lrs-1011_5_sil=8000:si=on:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1005447618:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2594 on theBenchmark for (2594ds/4652Mi) % 300.68/43.34 % (189113)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=420303817:i=12076:nm=6:rtra=on_2594 on theBenchmark for (2594ds/12076Mi) % 300.68/43.34 % (189110)Instruction limit reached! % 300.68/43.34 % (189110)------------------------------ % 300.68/43.34 % (189110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.34 % (189110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.34 % (189110)CaDiCaL version: 2.1.3 % 300.68/43.34 % (189110)Termination reason: Instruction limit % 300.68/43.34 % (189110)Termination phase: Saturation % 300.68/43.34 % (189110)Time elapsed: 0.549 s % 300.68/43.34 % (189110)Peak memory usage: 109 MB % 300.68/43.34 % (189110)Instructions burned: 1595 (million) % 300.68/43.34 % (189113)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.68/43.34 % (189113)------------------------------ % 300.68/43.34 % (189113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.68/43.34 % (189113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.68/43.34 % (189113)CaDiCaL version: 2.1.3 % 300.68/43.34 % (189113)Termination reason: Unknown % 300.68/43.34 % (189113)Termination phase: Saturation % 300.68/43.34 % (189113)Time elapsed: 0.358 s % 300.68/43.34 % (189113)Peak memory usage: 114 MB % 300.68/43.34 % (189113)Instructions burned: 542 (million) % 300.68/43.34 % (189116)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=1260343050:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2589 on theBenchmark for (2589ds/66668Mi) % 300.68/43.34 % (189117)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1761248544:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2588 on theBenchmark for (2588ds/2016Mi) % 300.68/43.34 % (189117)Instruction limit reached! % 300.68/43.34 % (189117)------------------------------ % 300.68/43.34 % (189117)Version: Vampire 5.0.1 (Release build, commit % 300.68/43.34 Terminated % 300.68/43.34 % Vampire exiting % 300.68/43.34 Terminated %------------------------------------------------------------------------------