%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM975_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:17:43 PM UTC 2026 % Result : Timeout 289.43s 41.92s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : NUM975_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.18/0.44 % Computer : n009.cluster.edu % 0.18/0.44 % Model : x86_64 x86_64 % 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.44 % Memory : 8046.5625MB % 0.18/0.44 % OS : Linux 6.8.0-71-generic % 0.18/0.44 % CPULimit : 300 % 0.18/0.44 % WCLimit : 300 % 0.18/0.44 % DateTime : Sun Sep 27 21:48:45 UTC 2026 % 0.18/0.45 % CPUTime : % 0.18/0.45 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.22/0.49 Running first-order theorem proving % 0.22/0.49 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 11.01/2.61 % (2430582)Detected formulas, will run a generic FOF schedule. % 11.01/2.61 % (2430587)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=3631708733:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 11.01/2.61 % (2430590)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1169280548:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 11.01/2.61 % (2430588)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=817886:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 11.01/2.61 % (2430591)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=922394450:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 11.01/2.61 % (2430592)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=608433037:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 11.01/2.61 % (2430593)dis-21_1_sil=8000:lcm=predicate:random_seed=3906770401: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) % 11.01/2.61 % (2430589)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=3397210500:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 11.01/2.61 % (2430590)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.01/2.61 % (2430589)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.01/2.61 % (2430593)Refutation not found, incomplete strategy % 11.01/2.61 % (2430593)------------------------------ % 11.01/2.61 % (2430593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.61 % (2430593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.61 % (2430593)CaDiCaL version: 2.1.3 % 11.01/2.61 % (2430593)Termination reason: Refutation not found, incomplete strategy % 11.01/2.61 % (2430593)Time elapsed: 0.018 s % 11.01/2.61 % (2430593)Peak memory usage: 88 MB % 11.01/2.61 % (2430593)Instructions burned: 16 (million) % 11.01/2.61 % (2430590)Instruction limit reached! % 11.01/2.61 % (2430590)------------------------------ % 11.01/2.61 % (2430590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.61 % (2430590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.61 % (2430590)CaDiCaL version: 2.1.3 % 11.01/2.61 % (2430590)Termination reason: Instruction limit % 11.01/2.61 % (2430590)Termination phase: Saturation % 11.01/2.61 % (2430590)Time elapsed: 0.089 s % 11.01/2.61 % (2430590)Peak memory usage: 89 MB % 11.01/2.61 % (2430590)Instructions burned: 110 (million) % 11.01/2.61 % (2430591)Instruction limit reached! % 11.01/2.61 % (2430591)------------------------------ % 11.01/2.61 % (2430591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.61 % (2430591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.61 % (2430591)CaDiCaL version: 2.1.3 % 11.01/2.61 % (2430591)Termination reason: Instruction limit % 11.01/2.61 % (2430591)Termination phase: Saturation % 11.01/2.61 % (2430591)Time elapsed: 0.112 s % 11.01/2.61 % (2430591)Peak memory usage: 88 MB % 11.01/2.61 % (2430591)Instructions burned: 119 (million) % 11.01/2.61 % (2430592)Instruction limit reached! % 11.01/2.61 % (2430592)------------------------------ % 11.01/2.61 % (2430592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.61 % (2430592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.61 % (2430592)CaDiCaL version: 2.1.3 % 11.01/2.61 % (2430592)Termination reason: Instruction limit % 11.01/2.61 % (2430592)Termination phase: Saturation % 11.01/2.61 % (2430592)Time elapsed: 0.138 s % 11.01/2.61 % (2430592)Peak memory usage: 89 MB % 11.01/2.61 % (2430592)Instructions burned: 139 (million) % 11.01/2.61 % (2430587)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 11.01/2.61 % (2430587)------------------------------ % 11.01/2.61 % (2430587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.01/2.61 % (2430587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.01/2.61 % (2430587)CaDiCaL version: 2.1.3 % 11.01/2.61 % (2430587)Termination reason: Unknown % 11.01/2.61 % (2430587)Termination phase: Saturation % 12.39/2.91 % (2430587)Time elapsed: 0.320 s % 12.39/2.91 % (2430587)Peak memory usage: 113 MB % 12.39/2.91 % (2430587)Instructions burned: 542 (million) % 12.39/2.91 % (2430601)lrs+10_1_sil=8000:sp=occurrence:random_seed=3059406164:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 12.39/2.91 % (2430602)lrs+10_1_sil=32000:urr=on:br=off:random_seed=208310194:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 12.39/2.91 % (2430603)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1933915098:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 12.39/2.91 % (2430593)------------------------------ % 12.39/2.91 % (2430593)------------------------------ % 12.39/2.91 % (2430604)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=3459861608:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi) % 12.39/2.91 % (2430602)Instruction limit reached! % 12.39/2.91 % (2430602)------------------------------ % 12.39/2.91 % (2430602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.91 % (2430602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.91 % (2430602)CaDiCaL version: 2.1.3 % 12.39/2.91 % (2430602)Termination reason: Instruction limit % 12.39/2.91 % (2430602)Termination phase: Saturation % 12.39/2.91 % (2430602)Time elapsed: 0.156 s % 12.39/2.91 % (2430602)Peak memory usage: 90 MB % 12.39/2.91 % (2430602)Instructions burned: 158 (million) % 12.39/2.91 % (2430588)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 12.39/2.91 % (2430588)------------------------------ % 12.39/2.91 % (2430588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.91 % (2430588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.91 % (2430588)CaDiCaL version: 2.1.3 % 12.39/2.91 % (2430588)Termination reason: Unknown % 12.39/2.91 % (2430588)Termination phase: Saturation % 12.39/2.91 % (2430588)Time elapsed: 0.579 s % 12.39/2.91 % (2430588)Peak memory usage: 113 MB % 12.39/2.91 % (2430588)Instructions burned: 543 (million) % 12.39/2.91 % (2430604)Instruction limit reached! % 12.39/2.91 % (2430604)------------------------------ % 12.39/2.91 % (2430604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.91 % (2430604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.91 % (2430604)CaDiCaL version: 2.1.3 % 12.39/2.91 % (2430604)Termination reason: Instruction limit % 12.39/2.91 % (2430604)Termination phase: Saturation % 12.39/2.91 % (2430604)Time elapsed: 0.129 s % 12.39/2.91 % (2430604)Peak memory usage: 90 MB % 12.39/2.91 % (2430604)Instructions burned: 249 (million) % 12.39/2.91 % (2430589)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 12.39/2.91 % (2430589)------------------------------ % 12.39/2.91 % (2430589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.91 % (2430589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.91 % (2430589)CaDiCaL version: 2.1.3 % 12.39/2.91 % (2430589)Termination reason: Unknown % 12.39/2.91 % (2430589)Termination phase: Saturation % 12.39/2.91 % (2430589)Time elapsed: 0.593 s % 12.39/2.91 % (2430589)Peak memory usage: 113 MB % 12.39/2.91 % (2430589)Instructions burned: 540 (million) % 12.39/2.91 % (2430601)Instruction limit reached! % 12.39/2.91 % (2430601)------------------------------ % 12.39/2.91 % (2430601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.91 % (2430601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.91 % (2430601)CaDiCaL version: 2.1.3 % 12.39/2.91 % (2430601)Termination reason: Instruction limit % 12.39/2.91 % (2430601)Termination phase: Saturation % 12.39/2.91 % (2430601)Time elapsed: 0.273 s % 12.39/2.91 % (2430601)Peak memory usage: 90 MB % 12.39/2.91 % (2430601)Instructions burned: 285 (million) % 12.39/2.91 % (2430603)Instruction limit reached! % 12.39/2.91 % (2430603)------------------------------ % 12.39/2.91 % (2430603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.39/2.91 % (2430603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.39/2.91 % (2430603)CaDiCaL version: 2.1.3 % 12.39/2.91 % (2430603)Termination reason: Instruction limit % 12.39/2.91 % (2430603)Termination phase: Saturation % 12.39/2.91 % (2430603)Time elapsed: 0.293 s % 12.39/2.91 % (2430603)Peak memory usage: 91 MB % 12.39/2.91 % (2430603)Instructions burned: 325 (million) % 12.39/2.91 % (2430608)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4001753348:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 16.04/3.40 % (2430608)Refutation not found, incomplete strategy % 16.04/3.40 % (2430608)------------------------------ % 16.04/3.40 % (2430608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.04/3.40 % (2430608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.04/3.40 % (2430608)CaDiCaL version: 2.1.3 % 16.04/3.40 % (2430608)Termination reason: Refutation not found, incomplete strategy % 16.04/3.40 % (2430608)Time elapsed: 0.010 s % 16.04/3.40 % (2430608)Peak memory usage: 88 MB % 16.04/3.40 % (2430608)Instructions burned: 8 (million) % 16.04/3.40 % (2430613)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3986658940:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi) % 16.04/3.40 % (2430610)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3638928498:i=2350_2991 on theBenchmark for (2991ds/2350Mi) % 16.04/3.40 % (2430616)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3699836656:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 16.04/3.40 % (2430614)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3358835013:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi) % 16.04/3.40 % (2430614)Refutation not found, incomplete strategy % 16.04/3.40 % (2430614)------------------------------ % 16.04/3.40 % (2430614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.04/3.40 % (2430614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.04/3.40 % (2430614)CaDiCaL version: 2.1.3 % 16.04/3.40 % (2430614)Termination reason: Refutation not found, incomplete strategy % 16.04/3.40 % (2430614)Time elapsed: 0.007 s % 16.04/3.40 % (2430614)Peak memory usage: 88 MB % 16.04/3.40 % (2430614)Instructions burned: 7 (million) % 16.04/3.40 % (2430616)Refutation not found, incomplete strategy % 16.04/3.40 % (2430616)------------------------------ % 16.04/3.40 % (2430616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.04/3.40 % (2430616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.04/3.40 % (2430616)CaDiCaL version: 2.1.3 % 16.04/3.40 % (2430616)Termination reason: Refutation not found, incomplete strategy % 16.04/3.40 % (2430616)Time elapsed: 0.009 s % 16.04/3.40 % (2430616)Peak memory usage: 88 MB % 16.04/3.40 % (2430616)Instructions burned: 7 (million) % 16.04/3.40 % (2430613)Instruction limit reached! % 16.04/3.40 % (2430613)------------------------------ % 16.04/3.40 % (2430613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.04/3.40 % (2430613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.04/3.40 % (2430613)CaDiCaL version: 2.1.3 % 16.04/3.40 % (2430613)Termination reason: Instruction limit % 16.04/3.40 % (2430613)Termination phase: Saturation % 16.04/3.40 % (2430613)Time elapsed: 0.060 s % 16.04/3.40 % (2430613)Peak memory usage: 90 MB % 16.04/3.40 % (2430613)Instructions burned: 115 (million) % 16.04/3.40 % (2430617)lrs+10_1_sil=8000:sp=occurrence:random_seed=3784739346:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 16.04/3.40 % (2430619)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2762859366:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 16.04/3.40 % (2430619)Refutation not found, incomplete strategy % 16.04/3.40 % (2430619)------------------------------ % 16.04/3.40 % (2430619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.04/3.40 % (2430619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.04/3.40 % (2430619)CaDiCaL version: 2.1.3 % 16.04/3.40 % (2430619)Termination reason: Refutation not found, incomplete strategy % 16.04/3.40 % (2430619)Time elapsed: 0.009 s % 16.04/3.40 % (2430619)Peak memory usage: 88 MB % 16.04/3.40 % (2430619)Instructions burned: 7 (million) % 16.04/3.40 % (2430625)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=942270683:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 16.04/3.40 % (2430608)------------------------------ % 16.04/3.40 % (2430608)------------------------------ % 16.04/3.40 % (2430616)------------------------------ % 16.04/3.40 % (2430616)------------------------------ % 16.04/3.40 % (2430614)------------------------------ % 16.04/3.40 % (2430614)------------------------------ % 16.04/3.40 % (2430619)------------------------------ % 16.04/3.40 % (2430619)------------------------------ % 18.41/3.81 % (2430625)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 18.41/3.81 % (2430625)------------------------------ % 18.41/3.81 % (2430625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.41/3.81 % (2430625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.41/3.81 % (2430625)CaDiCaL version: 2.1.3 % 18.41/3.81 % (2430625)Termination reason: Unknown % 18.41/3.81 % (2430625)Termination phase: Saturation % 18.41/3.81 % (2430625)Time elapsed: 0.312 s % 18.41/3.81 % (2430625)Peak memory usage: 113 MB % 18.41/3.81 % (2430625)Instructions burned: 540 (million) % 18.41/3.81 % (2430610)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 18.41/3.81 % (2430610)------------------------------ % 18.41/3.81 % (2430610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.41/3.81 % (2430610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.41/3.81 % (2430610)CaDiCaL version: 2.1.3 % 18.41/3.81 % (2430610)Termination reason: Unknown % 18.41/3.81 % (2430610)Termination phase: Saturation % 18.41/3.81 % (2430610)Time elapsed: 0.605 s % 18.41/3.81 % (2430610)Peak memory usage: 113 MB % 18.41/3.81 % (2430610)Instructions burned: 540 (million) % 18.41/3.81 % (2430629)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3878852981:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi) % 18.41/3.81 % (2430633)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=743365716:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi) % 18.41/3.81 % (2430634)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=112804236:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi) % 18.41/3.81 % (2430633)Refutation not found, incomplete strategy % 18.41/3.81 % (2430633)------------------------------ % 18.41/3.81 % (2430633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.41/3.81 % (2430633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.41/3.81 % (2430633)CaDiCaL version: 2.1.3 % 18.41/3.81 % (2430633)Termination reason: Refutation not found, incomplete strategy % 18.41/3.81 % (2430633)Time elapsed: 0.009 s % 18.41/3.81 % (2430633)Peak memory usage: 88 MB % 18.41/3.81 % (2430633)Instructions burned: 8 (million) % 18.41/3.81 % (2430629)Instruction limit reached! % 18.41/3.81 % (2430629)------------------------------ % 18.41/3.81 % (2430629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.41/3.81 % (2430629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.41/3.81 % (2430629)CaDiCaL version: 2.1.3 % 18.41/3.81 % (2430629)Termination reason: Instruction limit % 18.41/3.81 % (2430629)Termination phase: Saturation % 18.41/3.81 % (2430629)Time elapsed: 0.121 s % 18.41/3.81 % (2430629)Peak memory usage: 89 MB % 18.41/3.81 % (2430629)Instructions burned: 134 (million) % 18.41/3.81 % (2430641)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=1635136735:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi) % 18.41/3.81 % (2430641)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.41/3.81 % (2430643)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2126442447:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi) % 18.41/3.81 % (2430646)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4043361943:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi) % 18.41/3.81 % (2430646)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.41/3.81 % (2430646)Refutation not found, incomplete strategy % 18.41/3.81 % (2430646)------------------------------ % 18.41/3.81 % (2430646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.41/3.81 % (2430646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.41/3.81 % (2430646)CaDiCaL version: 2.1.3 % 18.41/3.81 % (2430646)Termination reason: Refutation not found, incomplete strategy % 18.41/3.81 % (2430646)Time elapsed: 0.005 s % 18.41/3.81 % (2430646)Peak memory usage: 88 MB % 18.41/3.81 % (2430646)Instructions burned: 3 (million) % 18.41/3.81 % (2430617)Instruction limit reached! % 18.41/3.81 % (2430617)------------------------------ % 18.41/3.81 % (2430617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.52/4.34 % (2430617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.52/4.34 % (2430617)CaDiCaL version: 2.1.3 % 23.52/4.34 % (2430617)Termination reason: Instruction limit % 23.52/4.34 % (2430617)Termination phase: Saturation % 23.52/4.34 % (2430617)Time elapsed: 0.751 s % 23.52/4.34 % (2430617)Peak memory usage: 95 MB % 23.52/4.34 % (2430617)Instructions burned: 907 (million) % 23.52/4.34 % (2430643)Instruction limit reached! % 23.52/4.34 % (2430643)------------------------------ % 23.52/4.34 % (2430643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.52/4.34 % (2430643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.52/4.34 % (2430643)CaDiCaL version: 2.1.3 % 23.52/4.34 % (2430643)Termination reason: Instruction limit % 23.52/4.34 % (2430643)Termination phase: Saturation % 23.52/4.34 % (2430643)Time elapsed: 0.070 s % 23.52/4.34 % (2430643)Peak memory usage: 90 MB % 23.52/4.34 % (2430643)Instructions burned: 134 (million) % 23.52/4.34 % (2430641)Instruction limit reached! % 23.52/4.34 % (2430641)------------------------------ % 23.52/4.34 % (2430641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.52/4.34 % (2430641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.52/4.34 % (2430641)CaDiCaL version: 2.1.3 % 23.52/4.34 % (2430641)Termination reason: Instruction limit % 23.52/4.34 % (2430641)Termination phase: Saturation % 23.52/4.34 % (2430641)Time elapsed: 0.116 s % 23.52/4.34 % (2430641)Peak memory usage: 89 MB % 23.52/4.34 % (2430641)Instructions burned: 125 (million) % 23.52/4.34 % (2430654)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1460407756:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi) % 23.52/4.34 % (2430659)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=22413656:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi) % 23.52/4.34 % (2430659)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 23.52/4.34 % (2430658)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=3152523054:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi) % 23.52/4.34 % (2430633)------------------------------ % 23.52/4.34 % (2430633)------------------------------ % 23.52/4.34 % (2430659)Instruction limit reached! % 23.52/4.34 % (2430659)------------------------------ % 23.52/4.34 % (2430659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.52/4.34 % (2430659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.52/4.34 % (2430659)CaDiCaL version: 2.1.3 % 23.52/4.34 % (2430659)Termination reason: Instruction limit % 23.52/4.34 % (2430659)Termination phase: Saturation % 23.52/4.34 % (2430659)Time elapsed: 0.088 s % 23.52/4.34 % (2430659)Peak memory usage: 90 MB % 23.52/4.34 % (2430659)Instructions burned: 152 (million) % 23.52/4.34 % (2430660)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=276601513:i=14155:bd=all_2980 on theBenchmark for (2980ds/14155Mi) % 23.52/4.34 % (2430646)------------------------------ % 23.52/4.34 % (2430646)------------------------------ % 23.52/4.34 % (2430634)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 23.52/4.34 % (2430634)------------------------------ % 23.52/4.34 % (2430634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.52/4.34 % (2430634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.52/4.34 % (2430634)CaDiCaL version: 2.1.3 % 23.52/4.34 % (2430634)Termination reason: Unknown % 23.52/4.34 % (2430634)Termination phase: Saturation % 23.52/4.34 % (2430634)Time elapsed: 0.596 s % 23.52/4.34 % (2430634)Peak memory usage: 113 MB % 23.52/4.34 % (2430634)Instructions burned: 540 (million) % 23.52/4.34 % (2430654)Instruction limit reached! % 23.52/4.34 % (2430654)------------------------------ % 23.52/4.34 % (2430654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.52/4.34 % (2430654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.52/4.34 % (2430654)CaDiCaL version: 2.1.3 % 23.52/4.34 % (2430654)Termination reason: Instruction limit % 23.52/4.34 % (2430654)Termination phase: Saturation % 23.52/4.34 % (2430654)Time elapsed: 0.343 s % 26.27/5.02 % (2430654)Peak memory usage: 94 MB % 26.27/5.02 % (2430654)Instructions burned: 431 (million) % 26.27/5.02 % (2430665)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=684521820:s2a=on:i=185:s2at=1.8:fdi=4_2977 on theBenchmark for (2977ds/185Mi) % 26.27/5.02 % (2430664)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3488696798:i=667:av=off:fsr=off_2978 on theBenchmark for (2978ds/667Mi) % 26.27/5.02 % (2430664)Refutation not found, incomplete strategy % 26.27/5.02 % (2430664)------------------------------ % 26.27/5.02 % (2430664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/5.02 % (2430664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/5.02 % (2430664)CaDiCaL version: 2.1.3 % 26.27/5.02 % (2430664)Termination reason: Refutation not found, incomplete strategy % 26.27/5.02 % (2430664)Time elapsed: 0.009 s % 26.27/5.02 % (2430664)Peak memory usage: 88 MB % 26.27/5.02 % (2430664)Instructions burned: 8 (million) % 26.27/5.02 % (2430667)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=865709404:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2976 on theBenchmark for (2976ds/193Mi) % 26.27/5.02 % (2430665)Instruction limit reached! % 26.27/5.02 % (2430665)------------------------------ % 26.27/5.02 % (2430665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/5.02 % (2430665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/5.02 % (2430665)CaDiCaL version: 2.1.3 % 26.27/5.02 % (2430665)Termination reason: Instruction limit % 26.27/5.02 % (2430665)Termination phase: Saturation % 26.27/5.02 % (2430665)Time elapsed: 0.099 s % 26.27/5.02 % (2430665)Peak memory usage: 91 MB % 26.27/5.02 % (2430665)Instructions burned: 185 (million) % 26.27/5.02 % (2430667)Instruction limit reached! % 26.27/5.02 % (2430667)------------------------------ % 26.27/5.02 % (2430667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/5.02 % (2430667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/5.02 % (2430667)CaDiCaL version: 2.1.3 % 26.27/5.02 % (2430667)Termination reason: Instruction limit % 26.27/5.02 % (2430667)Termination phase: Saturation % 26.27/5.02 % (2430667)Time elapsed: 0.116 s % 26.27/5.02 % (2430667)Peak memory usage: 90 MB % 26.27/5.02 % (2430667)Instructions burned: 193 (million) % 26.27/5.02 % (2430668)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=463623:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2976 on theBenchmark for (2976ds/4850Mi) % 26.27/5.02 % (2430668)Refutation not found, incomplete strategy % 26.27/5.02 % (2430668)------------------------------ % 26.27/5.02 % (2430668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/5.02 % (2430668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/5.02 % (2430668)CaDiCaL version: 2.1.3 % 26.27/5.02 % (2430668)Termination reason: Refutation not found, incomplete strategy % 26.27/5.02 % (2430668)Time elapsed: 0.007 s % 26.27/5.02 % (2430668)Peak memory usage: 88 MB % 26.27/5.02 % (2430668)Instructions burned: 6 (million) % 26.27/5.02 % (2430669)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2813179877:i=12111:sd=1:ss=included_2975 on theBenchmark for (2975ds/12111Mi) % 26.27/5.02 % (2430658)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 26.27/5.02 % (2430658)------------------------------ % 26.27/5.02 % (2430658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/5.02 % (2430658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.27/5.02 % (2430658)CaDiCaL version: 2.1.3 % 26.27/5.02 % (2430658)Termination reason: Unknown % 26.27/5.02 % (2430658)Termination phase: Saturation % 26.27/5.02 % (2430658)Time elapsed: 0.570 s % 26.27/5.02 % (2430658)Peak memory usage: 114 MB % 26.27/5.02 % (2430658)Instructions burned: 540 (million) % 26.27/5.02 % (2430673)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3127758564:i=319:kws=precedence:fsr=off_2974 on theBenchmark for (2974ds/319Mi) % 26.27/5.02 % (2430660)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 26.27/5.02 % (2430660)------------------------------ % 26.27/5.02 % (2430660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.27/5.02 % (2430660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.63/5.99 % (2430660)CaDiCaL version: 2.1.3 % 33.63/5.99 % (2430660)Termination reason: Unknown % 33.63/5.99 % (2430660)Termination phase: Saturation % 33.63/5.99 % (2430660)Time elapsed: 0.595 s % 33.63/5.99 % (2430660)Peak memory usage: 114 MB % 33.63/5.99 % (2430660)Instructions burned: 540 (million) % 33.63/5.99 % (2430674)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=875865199:i=2064:ep=RST_2973 on theBenchmark for (2973ds/2064Mi) % 33.63/5.99 % (2430664)------------------------------ % 33.63/5.99 % (2430664)------------------------------ % 33.63/5.99 % (2430674)Refutation not found, incomplete strategy % 33.63/5.99 % (2430674)------------------------------ % 33.63/5.99 % (2430674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.63/5.99 % (2430674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.63/5.99 % (2430674)CaDiCaL version: 2.1.3 % 33.63/5.99 % (2430674)Termination reason: Refutation not found, incomplete strategy % 33.63/5.99 % (2430674)Time elapsed: 0.009 s % 33.63/5.99 % (2430674)Peak memory usage: 88 MB % 33.63/5.99 % (2430674)Instructions burned: 8 (million) % 33.63/5.99 % (2430673)Instruction limit reached! % 33.63/5.99 % (2430673)------------------------------ % 33.63/5.99 % (2430673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.63/5.99 % (2430673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.63/5.99 % (2430673)CaDiCaL version: 2.1.3 % 33.63/5.99 % (2430673)Termination reason: Instruction limit % 33.63/5.99 % (2430673)Termination phase: Saturation % 33.63/5.99 % (2430673)Time elapsed: 0.174 s % 33.63/5.99 % (2430673)Peak memory usage: 92 MB % 33.63/5.99 % (2430673)Instructions burned: 320 (million) % 33.63/5.99 % (2430677)dis-1011_128_sil=32000:random_seed=2909623982:i=3706:ep=RST:av=off_2972 on theBenchmark for (2972ds/3706Mi) % 33.63/5.99 % (2430668)------------------------------ % 33.63/5.99 % (2430668)------------------------------ % 33.63/5.99 % (2430680)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4252855875:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2971 on theBenchmark for (2971ds/757Mi) % 33.63/5.99 % (2430680)Refutation not found, incomplete strategy % 33.63/5.99 % (2430680)------------------------------ % 33.63/5.99 % (2430680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.63/5.99 % (2430680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.63/5.99 % (2430680)CaDiCaL version: 2.1.3 % 33.63/5.99 % (2430680)Termination reason: Refutation not found, incomplete strategy % 33.63/5.99 % (2430680)Time elapsed: 0.010 s % 33.63/5.99 % (2430680)Peak memory usage: 88 MB % 33.63/5.99 % (2430680)Instructions burned: 8 (million) % 33.63/5.99 % (2430682)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1291771782:i=9925:aac=none_2970 on theBenchmark for (2970ds/9925Mi) % 33.63/5.99 % (2430681)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3703661638:i=13913:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/13913Mi) % 33.63/5.99 % (2430674)------------------------------ % 33.63/5.99 % (2430674)------------------------------ % 33.63/5.99 % (2430669)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 33.63/5.99 % (2430669)------------------------------ % 33.63/5.99 % (2430669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.63/5.99 % (2430669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.63/5.99 % (2430669)CaDiCaL version: 2.1.3 % 33.63/5.99 % (2430669)Termination reason: Unknown % 33.63/5.99 % (2430669)Termination phase: Saturation % 33.63/5.99 % (2430669)Time elapsed: 0.579 s % 33.63/5.99 % (2430669)Peak memory usage: 114 MB % 33.63/5.99 % (2430669)Instructions burned: 541 (million) % 33.63/5.99 % (2430684)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1184181135:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2969 on theBenchmark for (2969ds/2479Mi) % 33.63/5.99 % (2430684)Refutation not found, incomplete strategy % 33.63/5.99 % (2430684)------------------------------ % 33.63/5.99 % (2430684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.63/5.99 % (2430684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.63/5.99 % (2430684)CaDiCaL version: 2.1.3 % 33.63/5.99 % (2430684)Termination reason: Refutation not found, incomplete strategy % 33.63/5.99 % (2430684)Time elapsed: 0.011 s % 37.32/6.37 % (2430684)Peak memory usage: 89 MB % 37.32/6.37 % (2430684)Instructions burned: 10 (million) % 37.32/6.37 % (2430682)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 37.32/6.37 % (2430682)------------------------------ % 37.32/6.37 % (2430682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.32/6.37 % (2430682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.32/6.37 % (2430682)CaDiCaL version: 2.1.3 % 37.32/6.37 % (2430682)Termination reason: Unknown % 37.32/6.37 % (2430682)Termination phase: Saturation % 37.32/6.37 % (2430682)Time elapsed: 0.323 s % 37.32/6.37 % (2430682)Peak memory usage: 113 MB % 37.32/6.37 % (2430682)Instructions burned: 540 (million) % 37.32/6.37 % (2430689)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1580312700:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/11145Mi) % 37.32/6.37 % (2430688)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=385803583:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2967 on theBenchmark for (2967ds/440Mi) % 37.32/6.37 % (2430688)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 37.32/6.37 % (2430680)------------------------------ % 37.32/6.37 % (2430680)------------------------------ % 37.32/6.37 % (2430692)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=1188240411:cts=off:i=3034:av=off:er=known:fsd=on_2965 on theBenchmark for (2965ds/3034Mi) % 37.32/6.37 % (2430694)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=251123690:st=2:s2a=on:i=524:s2at=2:ss=axioms_2964 on theBenchmark for (2964ds/524Mi) % 37.32/6.37 % (2430681)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 37.32/6.37 % (2430681)------------------------------ % 37.32/6.37 % (2430681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.32/6.37 % (2430681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.32/6.37 % (2430681)CaDiCaL version: 2.1.3 % 37.32/6.37 % (2430681)Termination reason: Unknown % 37.32/6.37 % (2430681)Termination phase: Saturation % 37.32/6.37 % (2430681)Time elapsed: 0.591 s % 37.32/6.37 % (2430681)Peak memory usage: 113 MB % 37.32/6.37 % (2430681)Instructions burned: 540 (million) % 37.32/6.37 % (2430684)------------------------------ % 37.32/6.37 % (2430684)------------------------------ % 37.32/6.37 % (2430688)Instruction limit reached! % 37.32/6.37 % (2430688)------------------------------ % 37.32/6.37 % (2430688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.32/6.37 % (2430688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.32/6.37 % (2430688)CaDiCaL version: 2.1.3 % 37.32/6.37 % (2430688)Termination reason: Instruction limit % 37.32/6.37 % (2430688)Termination phase: Saturation % 37.32/6.37 % (2430688)Time elapsed: 0.367 s % 37.32/6.37 % (2430688)Peak memory usage: 92 MB % 37.32/6.37 % (2430688)Instructions burned: 440 (million) % 37.32/6.37 % (2430692)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 37.32/6.37 % (2430692)------------------------------ % 37.32/6.37 % (2430692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.32/6.37 % (2430692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.32/6.37 % (2430692)CaDiCaL version: 2.1.3 % 37.32/6.37 % (2430692)Termination reason: Unknown % 37.32/6.37 % (2430692)Termination phase: Saturation % 37.32/6.37 % (2430692)Time elapsed: 0.322 s % 37.32/6.37 % (2430692)Peak memory usage: 113 MB % 37.32/6.37 % (2430692)Instructions burned: 540 (million) % 37.32/6.37 % (2430689)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 37.32/6.37 % (2430689)------------------------------ % 37.32/6.37 % (2430689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.32/6.37 % (2430689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.32/6.37 % (2430689)CaDiCaL version: 2.1.3 % 37.32/6.37 % (2430689)Termination reason: Unknown % 37.32/6.37 % (2430689)Termination phase: Saturation % 37.32/6.37 % (2430689)Time elapsed: 0.556 s % 37.32/6.37 % (2430689)Peak memory usage: 113 MB % 37.32/6.37 % (2430689)Instructions burned: 539 (million) % 37.32/6.37 % (2430697)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2328636588:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2962 on theBenchmark for (2962ds/1016Mi) % 37.32/6.37 % (2430698)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3260895974:i=14123:bd=preordered:ins=4_2962 on theBenchmark for (2962ds/14123Mi) % 46.36/7.65 % (2430699)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1941825681:i=5781:kws=precedence:bd=all:rawr=on_2961 on theBenchmark for (2961ds/5781Mi) % 46.36/7.65 % (2430694)Instruction limit reached! % 46.36/7.65 % (2430694)------------------------------ % 46.36/7.65 % (2430694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.36/7.65 % (2430694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.36/7.65 % (2430694)CaDiCaL version: 2.1.3 % 46.36/7.65 % (2430694)Termination reason: Instruction limit % 46.36/7.65 % (2430694)Termination phase: Saturation % 46.36/7.65 % (2430694)Time elapsed: 0.434 s % 46.36/7.65 % (2430694)Peak memory usage: 92 MB % 46.36/7.65 % (2430694)Instructions burned: 524 (million) % 46.36/7.65 % (2430700)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=3852626304:i=2448:gtgl=5:bd=preordered:gtg=all_2960 on theBenchmark for (2960ds/2448Mi) % 46.36/7.65 % (2430702)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3310592416:i=3223:kws=precedence:fgj=on:av=off_2959 on theBenchmark for (2959ds/3223Mi) % 46.36/7.65 % (2430705)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3788587006:st=5.6:i=2033:sd=3:ss=axioms_2958 on theBenchmark for (2958ds/2033Mi) % 46.36/7.65 % (2430698)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 46.36/7.65 % (2430698)------------------------------ % 46.36/7.65 % (2430698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.36/7.65 % (2430698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.36/7.65 % (2430698)CaDiCaL version: 2.1.3 % 46.36/7.65 % (2430698)Termination reason: Unknown % 46.36/7.65 % (2430698)Termination phase: Saturation % 46.36/7.65 % (2430698)Time elapsed: 0.484 s % 46.36/7.65 % (2430698)Peak memory usage: 113 MB % 46.36/7.65 % (2430698)Instructions burned: 539 (million) % 46.36/7.65 % (2430700)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 46.36/7.65 % (2430700)------------------------------ % 46.36/7.65 % (2430700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.36/7.65 % (2430700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.36/7.65 % (2430700)CaDiCaL version: 2.1.3 % 46.36/7.65 % (2430700)Termination reason: Unknown % 46.36/7.65 % (2430700)Termination phase: Saturation % 46.36/7.65 % (2430700)Time elapsed: 0.318 s % 46.36/7.65 % (2430700)Peak memory usage: 113 MB % 46.36/7.65 % (2430700)Instructions burned: 542 (million) % 46.36/7.65 % (2430714)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=1895305149:i=21611:sd=3:ss=axioms_2954 on theBenchmark for (2954ds/21611Mi) % 46.36/7.65 % (2430713)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2478340302:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2954 on theBenchmark for (2954ds/2055Mi) % 46.36/7.65 % (2430702)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 46.36/7.65 % (2430702)------------------------------ % 46.36/7.65 % (2430702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.36/7.65 % (2430702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.36/7.65 % (2430702)CaDiCaL version: 2.1.3 % 46.36/7.65 % (2430702)Termination reason: Unknown % 46.36/7.65 % (2430702)Termination phase: Saturation % 46.36/7.65 % (2430702)Time elapsed: 0.570 s % 46.36/7.65 % (2430702)Peak memory usage: 114 MB % 46.36/7.65 % (2430702)Instructions burned: 540 (million) % 46.36/7.65 % (2430697)Instruction limit reached! % 46.36/7.65 % (2430697)------------------------------ % 46.36/7.65 % (2430697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.36/7.65 % (2430697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.36/7.65 % (2430697)CaDiCaL version: 2.1.3 % 46.36/7.65 % (2430697)Termination reason: Instruction limit % 46.36/7.65 % (2430697)Termination phase: Saturation % 46.36/7.65 % (2430697)Time elapsed: 0.928 s % 46.36/7.65 % (2430697)Peak memory usage: 97 MB % 46.36/7.65 % (2430697)Instructions burned: 1016 (million) % 46.36/7.65 % (2430705)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.27/8.50 % (2430705)------------------------------ % 53.27/8.50 % (2430705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.50 % (2430705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.50 % (2430705)CaDiCaL version: 2.1.3 % 53.27/8.50 % (2430705)Termination reason: Unknown % 53.27/8.50 % (2430705)Termination phase: Saturation % 53.27/8.50 % (2430705)Time elapsed: 0.595 s % 53.27/8.50 % (2430705)Peak memory usage: 113 MB % 53.27/8.50 % (2430705)Instructions burned: 540 (million) % 53.27/8.50 % (2430714)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.27/8.50 % (2430714)------------------------------ % 53.27/8.50 % (2430714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.50 % (2430714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.50 % (2430714)CaDiCaL version: 2.1.3 % 53.27/8.50 % (2430714)Termination reason: Unknown % 53.27/8.50 % (2430714)Termination phase: Saturation % 53.27/8.50 % (2430714)Time elapsed: 0.317 s % 53.27/8.50 % (2430714)Peak memory usage: 113 MB % 53.27/8.50 % (2430714)Instructions burned: 539 (million) % 53.27/8.50 % (2430719)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2134201553:i=4835:sd=13:ss=axioms:sgt=23_2951 on theBenchmark for (2951ds/4835Mi) % 53.27/8.50 % (2430713)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 53.27/8.50 % (2430713)------------------------------ % 53.27/8.50 % (2430713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.50 % (2430713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.50 % (2430713)CaDiCaL version: 2.1.3 % 53.27/8.50 % (2430713)Termination reason: Unknown % 53.27/8.50 % (2430713)Termination phase: Saturation % 53.27/8.50 % (2430713)Time elapsed: 0.426 s % 53.27/8.50 % (2430713)Peak memory usage: 114 MB % 53.27/8.50 % (2430713)Instructions burned: 540 (million) % 53.27/8.50 % (2430719)Refutation not found, incomplete strategy % 53.27/8.50 % (2430719)------------------------------ % 53.27/8.50 % (2430719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.50 % (2430719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.50 % (2430719)CaDiCaL version: 2.1.3 % 53.27/8.50 % (2430719)Termination reason: Refutation not found, incomplete strategy % 53.27/8.50 % (2430719)Time elapsed: 0.010 s % 53.27/8.50 % (2430719)Peak memory usage: 88 MB % 53.27/8.50 % (2430719)Instructions burned: 9 (million) % 53.27/8.50 % (2430722)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=1943331121:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2950 on theBenchmark for (2950ds/797Mi) % 53.27/8.50 % (2430722)Refutation not found, incomplete strategy % 53.27/8.50 % (2430722)------------------------------ % 53.27/8.50 % (2430722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.50 % (2430722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.50 % (2430722)CaDiCaL version: 2.1.3 % 53.27/8.50 % (2430722)Termination reason: Refutation not found, incomplete strategy % 53.27/8.50 % (2430722)Time elapsed: 0.017 s % 53.27/8.50 % (2430722)Peak memory usage: 88 MB % 53.27/8.50 % (2430722)Instructions burned: 15 (million) % 53.27/8.50 % (2430724)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=72377195:i=6038:nm=6_2949 on theBenchmark for (2949ds/6038Mi) % 53.27/8.50 % (2430723)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=779835081:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2949 on theBenchmark for (2949ds/2326Mi) % 53.27/8.50 % (2430723)Refutation not found, incomplete strategy % 53.27/8.50 % (2430723)------------------------------ % 53.27/8.50 % (2430723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.27/8.50 % (2430723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.27/8.50 % (2430723)CaDiCaL version: 2.1.3 % 53.27/8.50 % (2430723)Termination reason: Refutation not found, incomplete strategy % 53.27/8.50 % (2430723)Time elapsed: 0.012 s % 53.27/8.50 % (2430723)Peak memory usage: 89 MB % 53.27/8.50 % (2430723)Instructions burned: 10 (million) % 53.27/8.50 % (2430726)lrs+10_1_sil=32000:sp=occurrence:random_seed=3828481745:st=2:i=33334:sd=3:ss=included:sgt=32_2948 on theBenchmark for (2948ds/33334Mi) % 58.55/9.29 % (2430719)------------------------------ % 58.55/9.29 % (2430719)------------------------------ % 58.55/9.29 % (2430724)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 58.55/9.29 % (2430724)------------------------------ % 58.55/9.29 % (2430724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.55/9.29 % (2430724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.55/9.29 % (2430724)CaDiCaL version: 2.1.3 % 58.55/9.29 % (2430724)Termination reason: Unknown % 58.55/9.29 % (2430724)Termination phase: Saturation % 58.55/9.29 % (2430724)Time elapsed: 0.325 s % 58.55/9.29 % (2430724)Peak memory usage: 113 MB % 58.55/9.29 % (2430724)Instructions burned: 540 (million) % 58.55/9.29 % (2430722)------------------------------ % 58.55/9.29 % (2430722)------------------------------ % 58.55/9.29 % (2430723)------------------------------ % 58.55/9.29 % (2430723)------------------------------ % 58.55/9.29 % (2430738)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=1616066156:i=8327:s2at=5:bd=preordered_2944 on theBenchmark for (2944ds/8327Mi) % 58.55/9.29 % (2430737)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2161512407:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2944 on theBenchmark for (2944ds/1008Mi) % 58.55/9.29 % (2430739)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=170100454:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2943 on theBenchmark for (2943ds/1083Mi) % 58.55/9.29 % (2430740)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2568612513:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2943 on theBenchmark for (2943ds/1084Mi) % 58.55/9.29 % (2430738)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 58.55/9.29 % (2430738)------------------------------ % 58.55/9.29 % (2430738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.55/9.29 % (2430738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.55/9.29 % (2430738)CaDiCaL version: 2.1.3 % 58.55/9.29 % (2430738)Termination reason: Unknown % 58.55/9.29 % (2430738)Termination phase: Saturation % 58.55/9.29 % (2430738)Time elapsed: 0.322 s % 58.55/9.29 % (2430738)Peak memory usage: 114 MB % 58.55/9.29 % (2430738)Instructions burned: 540 (million) % 58.55/9.29 % (2430677)Instruction limit reached! % 58.55/9.29 % (2430677)------------------------------ % 58.55/9.29 % (2430677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.55/9.29 % (2430677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.55/9.29 % (2430677)CaDiCaL version: 2.1.3 % 58.55/9.29 % (2430677)Termination reason: Instruction limit % 58.55/9.29 % (2430677)Termination phase: Saturation % 58.55/9.29 % (2430677)Time elapsed: 3.282 s % 58.55/9.29 % (2430677)Peak memory usage: 110 MB % 58.55/9.29 % (2430677)Instructions burned: 3707 (million) % 58.55/9.29 % (2430745)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=415810212:i=6995:s2at=5:gtg=all_2938 on theBenchmark for (2938ds/6995Mi) % 58.55/9.29 % (2430746)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3952475970:st=2:i=6225:sd=15:ss=axioms_2937 on theBenchmark for (2937ds/6225Mi) % 58.55/9.29 % (2430746)Refutation not found, incomplete strategy % 58.55/9.29 % (2430746)------------------------------ % 58.55/9.29 % (2430746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.55/9.29 % (2430746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.55/9.29 % (2430746)CaDiCaL version: 2.1.3 % 58.55/9.29 % (2430746)Termination reason: Refutation not found, incomplete strategy % 58.55/9.29 % (2430746)Time elapsed: 0.009 s % 58.55/9.29 % (2430746)Peak memory usage: 89 MB % 58.55/9.29 % (2430746)Instructions burned: 8 (million) % 58.55/9.29 % (2430745)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 58.55/9.29 % (2430745)------------------------------ % 58.55/9.29 % (2430745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.55/9.29 % (2430745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.55/9.29 % (2430745)CaDiCaL version: 2.1.3 % 66.35/10.32 % (2430745)Termination reason: Unknown % 66.35/10.32 % (2430745)Termination phase: Saturation % 66.35/10.32 % (2430745)Time elapsed: 0.323 s % 66.35/10.32 % (2430745)Peak memory usage: 114 MB % 66.35/10.32 % (2430745)Instructions burned: 542 (million) % 66.35/10.32 % (2430737)Instruction limit reached! % 66.35/10.32 % (2430737)------------------------------ % 66.35/10.32 % (2430737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.35/10.32 % (2430737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.35/10.32 % (2430737)CaDiCaL version: 2.1.3 % 66.35/10.32 % (2430737)Termination reason: Instruction limit % 66.35/10.32 % (2430737)Termination phase: Saturation % 66.35/10.32 % (2430737)Time elapsed: 0.877 s % 66.35/10.32 % (2430737)Peak memory usage: 100 MB % 66.35/10.32 % (2430737)Instructions burned: 1008 (million) % 66.35/10.32 % (2430739)Instruction limit reached! % 66.35/10.32 % (2430739)------------------------------ % 66.35/10.32 % (2430739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.35/10.32 % (2430739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.35/10.32 % (2430739)CaDiCaL version: 2.1.3 % 66.35/10.32 % (2430739)Termination reason: Instruction limit % 66.35/10.32 % (2430739)Termination phase: Saturation % 66.35/10.32 % (2430739)Time elapsed: 0.791 s % 66.35/10.32 % (2430739)Peak memory usage: 91 MB % 66.35/10.32 % (2430739)Instructions burned: 1084 (million) % 66.35/10.32 % (2430749)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=907605557:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2933 on theBenchmark for (2933ds/3372Mi) % 66.35/10.32 % (2430746)------------------------------ % 66.35/10.32 % (2430746)------------------------------ % 66.35/10.32 % (2430750)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=177783444:st=2.3:i=26457:sd=10:ss=included:sgt=8_2933 on theBenchmark for (2933ds/26457Mi) % 66.35/10.32 % (2430740)Instruction limit reached! % 66.35/10.32 % (2430740)------------------------------ % 66.35/10.32 % (2430740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.35/10.32 % (2430740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.35/10.32 % (2430740)CaDiCaL version: 2.1.3 % 66.35/10.32 % (2430740)Termination reason: Instruction limit % 66.35/10.32 % (2430740)Termination phase: Saturation % 66.35/10.32 % (2430740)Time elapsed: 0.997 s % 66.35/10.32 % (2430740)Peak memory usage: 95 MB % 66.35/10.32 % (2430740)Instructions burned: 1085 (million) % 66.35/10.32 % (2430752)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=736293823:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2932 on theBenchmark for (2932ds/13494Mi) % 66.35/10.32 % (2430755)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=1461577291:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2930 on theBenchmark for (2930ds/2503Mi) % 66.35/10.32 % (2430755)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 66.35/10.32 % (2430749)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 66.35/10.32 % (2430749)------------------------------ % 66.35/10.32 % (2430749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.35/10.32 % (2430749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.35/10.32 % (2430749)CaDiCaL version: 2.1.3 % 66.35/10.32 % (2430749)Termination reason: Unknown % 66.35/10.32 % (2430749)Termination phase: Saturation % 66.35/10.32 % (2430749)Time elapsed: 0.320 s % 66.35/10.32 % (2430749)Peak memory usage: 113 MB % 66.35/10.32 % (2430749)Instructions burned: 539 (million) % 66.35/10.32 % (2430757)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3109941737:i=2559:sd=1:ep=RSTC:ss=axioms_2930 on theBenchmark for (2930ds/2559Mi) % 66.35/10.32 % (2430762)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=894283945:i=30753:av=off:ss=included_2927 on theBenchmark for (2927ds/30753Mi) % 66.35/10.32 % (2430750)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 66.35/10.32 % (2430750)------------------------------ % 66.35/10.32 % (2430750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.35/10.32 % (2430750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.56/11.12 % (2430750)CaDiCaL version: 2.1.3 % 71.56/11.12 % (2430750)Termination reason: Unknown % 71.56/11.12 % (2430750)Termination phase: Saturation % 71.56/11.12 % (2430750)Time elapsed: 0.571 s % 71.56/11.12 % (2430750)Peak memory usage: 113 MB % 71.56/11.12 % (2430750)Instructions burned: 541 (million) % 71.56/11.12 % (2430752)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 71.56/11.12 % (2430752)------------------------------ % 71.56/11.12 % (2430752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.56/11.12 % (2430752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.56/11.12 % (2430752)CaDiCaL version: 2.1.3 % 71.56/11.12 % (2430752)Termination reason: Unknown % 71.56/11.12 % (2430752)Termination phase: Saturation % 71.56/11.12 % (2430752)Time elapsed: 0.595 s % 71.56/11.12 % (2430752)Peak memory usage: 114 MB % 71.56/11.12 % (2430752)Instructions burned: 542 (million) % 71.56/11.12 % (2430755)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 71.56/11.12 % (2430755)------------------------------ % 71.56/11.12 % (2430755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.56/11.12 % (2430755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.56/11.12 % (2430755)CaDiCaL version: 2.1.3 % 71.56/11.12 % (2430755)Termination reason: Unknown % 71.56/11.12 % (2430755)Termination phase: Saturation % 71.56/11.12 % (2430755)Time elapsed: 0.563 s % 71.56/11.12 % (2430755)Peak memory usage: 113 MB % 71.56/11.12 % (2430755)Instructions burned: 539 (million) % 71.56/11.12 % (2430762)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 71.56/11.12 % (2430762)------------------------------ % 71.56/11.12 % (2430762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.56/11.12 % (2430762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.56/11.12 % (2430762)CaDiCaL version: 2.1.3 % 71.56/11.12 % (2430762)Termination reason: Unknown % 71.56/11.12 % (2430762)Termination phase: Saturation % 71.56/11.12 % (2430762)Time elapsed: 0.322 s % 71.56/11.12 % (2430762)Peak memory usage: 113 MB % 71.56/11.12 % (2430762)Instructions burned: 541 (million) % 71.56/11.12 % (2430765)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2502485452:i=26473:ep=RSTC_2924 on theBenchmark for (2924ds/26473Mi) % 71.56/11.12 % (2430757)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 71.56/11.12 % (2430757)------------------------------ % 71.56/11.12 % (2430757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.56/11.12 % (2430757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.56/11.12 % (2430757)CaDiCaL version: 2.1.3 % 71.56/11.12 % (2430757)Termination reason: Unknown % 71.56/11.12 % (2430757)Termination phase: Saturation % 71.56/11.12 % (2430757)Time elapsed: 0.598 s % 71.56/11.12 % (2430757)Peak memory usage: 113 MB % 71.56/11.12 % (2430757)Instructions burned: 541 (million) % 71.56/11.12 % (2430766)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=1210777839:cts=off:i=2759:kws=inv_arity:fgj=on_2924 on theBenchmark for (2924ds/2759Mi) % 71.56/11.12 % (2430768)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=2047549500:i=1532:ep=RS:ss=axioms_2922 on theBenchmark for (2922ds/1532Mi) % 71.56/11.12 % (2430767)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=3840011570:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2922 on theBenchmark for (2922ds/5665Mi) % 71.56/11.12 % (2430767)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 71.56/11.12 % (2430770)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=456033705:i=1565:sd=2:ss=axioms:sgt=32_2921 on theBenchmark for (2921ds/1565Mi) % 71.56/11.12 % (2430768)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 71.56/11.12 % (2430768)------------------------------ % 71.56/11.12 % (2430768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.56/11.12 % (2430768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.56/11.12 % (2430768)CaDiCaL version: 2.1.3 % 71.56/11.12 % (2430768)Termination reason: Unknown % 71.56/11.12 % (2430768)Termination phase: Saturation % 75.38/11.97 % (2430768)Time elapsed: 0.317 s % 75.38/11.97 % (2430768)Peak memory usage: 113 MB % 75.38/11.97 % (2430768)Instructions burned: 541 (million) % 75.38/11.97 % (2430766)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.38/11.97 % (2430766)------------------------------ % 75.38/11.97 % (2430766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.38/11.97 % (2430766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.38/11.97 % (2430766)CaDiCaL version: 2.1.3 % 75.38/11.97 % (2430766)Termination reason: Unknown % 75.38/11.97 % (2430766)Termination phase: Saturation % 75.38/11.97 % (2430766)Time elapsed: 0.591 s % 75.38/11.97 % (2430766)Peak memory usage: 113 MB % 75.38/11.97 % (2430766)Instructions burned: 542 (million) % 75.38/11.97 % (2430767)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.38/11.97 % (2430767)------------------------------ % 75.38/11.97 % (2430767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.38/11.97 % (2430767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.38/11.97 % (2430767)CaDiCaL version: 2.1.3 % 75.38/11.97 % (2430767)Termination reason: Unknown % 75.38/11.97 % (2430767)Termination phase: Saturation % 75.38/11.97 % (2430767)Time elapsed: 0.553 s % 75.38/11.97 % (2430767)Peak memory usage: 113 MB % 75.38/11.97 % (2430767)Instructions burned: 540 (million) % 75.38/11.97 % (2430779)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=815529871:i=1572:fgj=on:gsp=on_2916 on theBenchmark for (2916ds/1572Mi) % 75.38/11.97 % (2430779)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 75.38/11.97 % (2430770)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.38/11.97 % (2430770)------------------------------ % 75.38/11.97 % (2430770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.38/11.97 % (2430770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.38/11.97 % (2430770)CaDiCaL version: 2.1.3 % 75.38/11.97 % (2430770)Termination reason: Unknown % 75.38/11.97 % (2430770)Termination phase: Saturation % 75.38/11.97 % (2430770)Time elapsed: 0.589 s % 75.38/11.97 % (2430770)Peak memory usage: 113 MB % 75.38/11.97 % (2430770)Instructions burned: 540 (million) % 75.38/11.97 % (2430780)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=554384291:i=6052:sd=4:ss=axioms:sgt=24_2915 on theBenchmark for (2915ds/6052Mi) % 75.38/11.97 % (2430781)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=3784938068:i=3500:sd=1:bd=preordered:sup=off:ss=included_2914 on theBenchmark for (2914ds/3500Mi) % 75.38/11.97 % (2430779)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.38/11.97 % (2430779)------------------------------ % 75.38/11.97 % (2430779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.38/11.97 % (2430779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.38/11.97 % (2430779)CaDiCaL version: 2.1.3 % 75.38/11.97 % (2430779)Termination reason: Unknown % 75.38/11.97 % (2430779)Termination phase: Saturation % 75.38/11.97 % (2430779)Time elapsed: 0.319 s % 75.38/11.97 % (2430779)Peak memory usage: 114 MB % 75.38/11.97 % (2430779)Instructions burned: 540 (million) % 75.38/11.97 % (2430783)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=867319983:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2912 on theBenchmark for (2912ds/1842Mi) % 75.38/11.97 % (2430783)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 75.38/11.97 % (2430786)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2514516160:i=66096:add=on_2911 on theBenchmark for (2911ds/66096Mi) % 75.38/11.97 % (2430780)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 75.38/11.97 % (2430780)------------------------------ % 75.38/11.97 % (2430780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.38/11.97 % (2430780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.38/11.97 % (2430780)CaDiCaL version: 2.1.3 % 82.61/12.88 % (2430780)Termination reason: Unknown % 82.61/12.88 % (2430780)Termination phase: Saturation % 82.61/12.88 % (2430780)Time elapsed: 0.591 s % 82.61/12.88 % (2430780)Peak memory usage: 113 MB % 82.61/12.88 % (2430780)Instructions burned: 539 (million) % 82.61/12.88 % (2430781)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.61/12.88 % (2430781)------------------------------ % 82.61/12.88 % (2430781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.61/12.88 % (2430781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.61/12.88 % (2430781)CaDiCaL version: 2.1.3 % 82.61/12.88 % (2430781)Termination reason: Unknown % 82.61/12.88 % (2430781)Termination phase: Saturation % 82.61/12.88 % (2430781)Time elapsed: 0.552 s % 82.61/12.88 % (2430781)Peak memory usage: 113 MB % 82.61/12.88 % (2430781)Instructions burned: 542 (million) % 82.61/12.88 % (2430699)Instruction limit reached! % 82.61/12.88 % (2430699)------------------------------ % 82.61/12.88 % (2430699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.61/12.88 % (2430699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.61/12.88 % (2430699)CaDiCaL version: 2.1.3 % 82.61/12.88 % (2430699)Termination reason: Instruction limit % 82.61/12.88 % (2430699)Termination phase: Saturation % 82.61/12.88 % (2430699)Time elapsed: 5.277 s % 82.61/12.88 % (2430699)Peak memory usage: 112 MB % 82.61/12.88 % (2430699)Instructions burned: 5782 (million) % 82.61/12.88 % (2430786)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.61/12.88 % (2430786)------------------------------ % 82.61/12.88 % (2430786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.61/12.88 % (2430786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.61/12.88 % (2430786)CaDiCaL version: 2.1.3 % 82.61/12.88 % (2430786)Termination reason: Unknown % 82.61/12.88 % (2430786)Termination phase: Saturation % 82.61/12.88 % (2430786)Time elapsed: 0.321 s % 82.61/12.88 % (2430786)Peak memory usage: 113 MB % 82.61/12.88 % (2430786)Instructions burned: 540 (million) % 82.61/12.88 % (2430783)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.61/12.88 % (2430783)------------------------------ % 82.61/12.88 % (2430783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.61/12.88 % (2430783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.61/12.88 % (2430783)CaDiCaL version: 2.1.3 % 82.61/12.88 % (2430783)Termination reason: Unknown % 82.61/12.88 % (2430783)Termination phase: Saturation % 82.61/12.88 % (2430783)Time elapsed: 0.596 s % 82.61/12.88 % (2430783)Peak memory usage: 113 MB % 82.61/12.88 % (2430783)Instructions burned: 540 (million) % 82.61/12.88 % (2430789)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=735543277:i=1884:sd=1:nm=60:ss=axioms_2906 on theBenchmark for (2906ds/1884Mi) % 82.61/12.88 % (2430790)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2152716504:cts=off:i=5469:bs=on:fsr=off_2906 on theBenchmark for (2906ds/5469Mi) % 82.61/12.88 % (2430792)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3189542532:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2905 on theBenchmark for (2905ds/2110Mi) % 82.61/12.88 % (2430791)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=3092327253:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2906 on theBenchmark for (2906ds/2037Mi) % 82.61/12.88 % (2430793)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=1238917641:i=2430:add=off:aac=none:nm=16_2904 on theBenchmark for (2904ds/2430Mi) % 82.61/12.88 % (2430792)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.61/12.88 % (2430792)------------------------------ % 82.61/12.88 % (2430792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.61/12.88 % (2430792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.61/12.88 % (2430792)CaDiCaL version: 2.1.3 % 82.61/12.88 % (2430792)Termination reason: Unknown % 82.61/12.88 % (2430792)Termination phase: Saturation % 82.61/12.88 % (2430792)Time elapsed: 0.321 s % 82.61/12.88 % (2430792)Peak memory usage: 113 MB % 82.61/12.88 % (2430792)Instructions burned: 543 (million) % 82.61/12.88 % (2430789)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 82.61/12.88 % (2430789)------------------------------ % 90.59/13.94 % (2430789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.59/13.94 % (2430789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.59/13.94 % (2430789)CaDiCaL version: 2.1.3 % 90.59/13.94 % (2430789)Termination reason: Unknown % 90.59/13.94 % (2430789)Termination phase: Saturation % 90.59/13.94 % (2430789)Time elapsed: 0.565 s % 90.59/13.94 % (2430789)Peak memory usage: 113 MB % 90.59/13.94 % (2430789)Instructions burned: 538 (million) % 90.59/13.94 % (2430799)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=598141607:cond=fast:i=4891_2900 on theBenchmark for (2900ds/4891Mi) % 90.59/13.94 % (2430791)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 90.59/13.94 % (2430791)------------------------------ % 90.59/13.94 % (2430791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.59/13.94 % (2430791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.59/13.94 % (2430791)CaDiCaL version: 2.1.3 % 90.59/13.94 % (2430791)Termination reason: Unknown % 90.59/13.94 % (2430791)Termination phase: Saturation % 90.59/13.94 % (2430791)Time elapsed: 0.597 s % 90.59/13.94 % (2430791)Peak memory usage: 114 MB % 90.59/13.94 % (2430791)Instructions burned: 544 (million) % 90.59/13.94 % (2430793)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 90.59/13.94 % (2430793)------------------------------ % 90.59/13.94 % (2430793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.59/13.94 % (2430793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.59/13.94 % (2430793)CaDiCaL version: 2.1.3 % 90.59/13.94 % (2430793)Termination reason: Unknown % 90.59/13.94 % (2430793)Termination phase: Saturation % 90.59/13.94 % (2430793)Time elapsed: 0.594 s % 90.59/13.94 % (2430793)Peak memory usage: 114 MB % 90.59/13.94 % (2430793)Instructions burned: 541 (million) % 90.59/13.94 % (2430800)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=1098807614:st=2:i=14845:sd=2:ss=included:fsd=on_2898 on theBenchmark for (2898ds/14845Mi) % 90.59/13.94 % (2430799)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 90.59/13.94 % (2430799)------------------------------ % 90.59/13.94 % (2430799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.59/13.94 % (2430799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.59/13.94 % (2430799)CaDiCaL version: 2.1.3 % 90.59/13.94 % (2430799)Termination reason: Unknown % 90.59/13.94 % (2430799)Termination phase: Saturation % 90.59/13.94 % (2430799)Time elapsed: 0.323 s % 90.59/13.94 % (2430799)Peak memory usage: 114 MB % 90.59/13.94 % (2430799)Instructions burned: 540 (million) % 90.59/13.94 % (2430802)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=353670757:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2897 on theBenchmark for (2897ds/7534Mi) % 90.59/13.94 % (2430807)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=484568763:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2895 on theBenchmark for (2895ds/10353Mi) % 90.59/13.94 % (2430809)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2255300830:i=7860_2894 on theBenchmark for (2894ds/7860Mi) % 90.59/13.94 % (2430809)Refutation not found, incomplete strategy % 90.59/13.94 % (2430809)------------------------------ % 90.59/13.94 % (2430809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.59/13.94 % (2430809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 90.59/13.94 % (2430809)CaDiCaL version: 2.1.3 % 90.59/13.94 % (2430809)Termination reason: Refutation not found, incomplete strategy % 90.59/13.94 % (2430809)Time elapsed: 0.005 s % 90.59/13.94 % (2430809)Peak memory usage: 89 MB % 90.59/13.94 % (2430809)Instructions burned: 8 (million) % 90.59/13.94 % (2430809)------------------------------ % 90.59/13.94 % (2430809)------------------------------ % 90.59/13.94 % (2430800)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 90.59/13.94 % (2430800)------------------------------ % 90.59/13.94 % (2430800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 90.59/13.94 % (2430800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.23/14.85 % (2430800)CaDiCaL version: 2.1.3 % 97.23/14.85 % (2430800)Termination reason: Unknown % 97.23/14.85 % (2430800)Termination phase: Saturation % 97.23/14.85 % (2430800)Time elapsed: 0.558 s % 97.23/14.85 % (2430800)Peak memory usage: 114 MB % 97.23/14.85 % (2430800)Instructions burned: 540 (million) % 97.23/14.85 % (2430802)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 97.23/14.85 % (2430802)------------------------------ % 97.23/14.85 % (2430802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.23/14.85 % (2430802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.23/14.85 % (2430802)CaDiCaL version: 2.1.3 % 97.23/14.85 % (2430802)Termination reason: Unknown % 97.23/14.85 % (2430802)Termination phase: Saturation % 97.23/14.85 % (2430802)Time elapsed: 0.603 s % 97.23/14.85 % (2430802)Peak memory usage: 113 MB % 97.23/14.85 % (2430802)Instructions burned: 542 (million) % 97.23/14.85 % (2430814)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3453169442:i=5812:gtgl=2:gtg=all_2890 on theBenchmark for (2890ds/5812Mi) % 97.23/14.85 % (2430813)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=1364601111:i=7896:sd=2:bs=on:ss=included:sgt=20_2890 on theBenchmark for (2890ds/7896Mi) % 97.23/14.85 % (2430807)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 97.23/14.85 % (2430807)------------------------------ % 97.23/14.85 % (2430807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.23/14.85 % (2430807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.23/14.85 % (2430807)CaDiCaL version: 2.1.3 % 97.23/14.85 % (2430807)Termination reason: Unknown % 97.23/14.85 % (2430807)Termination phase: Saturation % 97.23/14.85 % (2430807)Time elapsed: 0.595 s % 97.23/14.85 % (2430807)Peak memory usage: 113 MB % 97.23/14.85 % (2430807)Instructions burned: 540 (million) % 97.23/14.85 % (2430815)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=3139819280:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2888 on theBenchmark for (2888ds/2965Mi) % 97.23/14.85 % (2430814)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 97.23/14.85 % (2430814)------------------------------ % 97.23/14.85 % (2430814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.23/14.85 % (2430814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.23/14.85 % (2430814)CaDiCaL version: 2.1.3 % 97.23/14.85 % (2430814)Termination reason: Unknown % 97.23/14.85 % (2430814)Termination phase: Saturation % 97.23/14.85 % (2430814)Time elapsed: 0.323 s % 97.23/14.85 % (2430814)Peak memory usage: 114 MB % 97.23/14.85 % (2430814)Instructions burned: 542 (million) % 97.23/14.85 % (2430818)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=3839466808:i=2967:kws=precedence:bd=preordered:av=off_2887 on theBenchmark for (2887ds/2967Mi) % 97.23/14.85 % (2430821)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=634984067:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2884 on theBenchmark for (2884ds/3022Mi) % 97.23/14.85 % (2430813)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 97.23/14.85 % (2430813)------------------------------ % 97.23/14.85 % (2430813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.23/14.85 % (2430813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.23/14.85 % (2430813)CaDiCaL version: 2.1.3 % 97.23/14.85 % (2430813)Termination reason: Unknown % 97.23/14.85 % (2430813)Termination phase: Saturation % 97.23/14.85 % (2430813)Time elapsed: 0.559 s % 97.23/14.85 % (2430813)Peak memory usage: 113 MB % 97.23/14.85 % (2430813)Instructions burned: 540 (million) % 97.23/14.85 % (2430815)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 97.23/14.85 % (2430815)------------------------------ % 97.23/14.85 % (2430815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.23/14.85 % (2430815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.23/14.85 % (2430815)CaDiCaL version: 2.1.3 % 97.23/14.85 % (2430815)Termination reason: Unknown % 104.87/15.97 % (2430815)Termination phase: Saturation % 104.87/15.97 % (2430815)Time elapsed: 0.473 s % 104.87/15.97 % (2430815)Peak memory usage: 114 MB % 104.87/15.97 % (2430815)Instructions burned: 541 (million) % 104.87/15.97 % (2430825)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=2682363771:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2881 on theBenchmark for (2881ds/3207Mi) % 104.87/15.97 % (2430818)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 104.87/15.97 % (2430818)------------------------------ % 104.87/15.97 % (2430818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.87/15.97 % (2430818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.87/15.97 % (2430818)CaDiCaL version: 2.1.3 % 104.87/15.97 % (2430818)Termination reason: Unknown % 104.87/15.97 % (2430818)Termination phase: Saturation % 104.87/15.97 % (2430818)Time elapsed: 0.590 s % 104.87/15.97 % (2430818)Peak memory usage: 113 MB % 104.87/15.97 % (2430818)Instructions burned: 542 (million) % 104.87/15.97 % (2430826)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2798732576:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2881 on theBenchmark for (2881ds/3289Mi) % 104.87/15.97 % (2430821)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 104.87/15.97 % (2430821)------------------------------ % 104.87/15.97 % (2430821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.87/15.97 % (2430821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.87/15.97 % (2430821)CaDiCaL version: 2.1.3 % 104.87/15.97 % (2430821)Termination reason: Unknown % 104.87/15.97 % (2430821)Termination phase: Saturation % 104.87/15.97 % (2430821)Time elapsed: 0.396 s % 104.87/15.97 % (2430821)Peak memory usage: 113 MB % 104.87/15.97 % (2430821)Instructions burned: 540 (million) % 104.87/15.97 % (2430829)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1706968099:i=38569:sd=3:ss=axioms:sgt=32_2878 on theBenchmark for (2878ds/38569Mi) % 104.87/15.97 % (2430830)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=4219063794:cts=off:i=3394_2877 on theBenchmark for (2877ds/3394Mi) % 104.87/15.97 % (2430825)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 104.87/15.97 % (2430825)------------------------------ % 104.87/15.97 % (2430825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.87/15.97 % (2430825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.87/15.97 % (2430825)CaDiCaL version: 2.1.3 % 104.87/15.97 % (2430825)Termination reason: Unknown % 104.87/15.97 % (2430825)Termination phase: Saturation % 104.87/15.97 % (2430825)Time elapsed: 0.567 s % 104.87/15.97 % (2430825)Peak memory usage: 114 MB % 104.87/15.97 % (2430825)Instructions burned: 540 (million) % 104.87/15.97 % (2430830)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 104.87/15.97 % (2430830)------------------------------ % 104.87/15.97 % (2430830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.87/15.97 % (2430830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.87/15.97 % (2430830)CaDiCaL version: 2.1.3 % 104.87/15.97 % (2430830)Termination reason: Unknown % 104.87/15.97 % (2430830)Termination phase: Saturation % 104.87/15.97 % (2430830)Time elapsed: 0.319 s % 104.87/15.97 % (2430830)Peak memory usage: 113 MB % 104.87/15.97 % (2430830)Instructions burned: 541 (million) % 104.87/15.97 % (2430826)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 104.87/15.97 % (2430826)------------------------------ % 104.87/15.97 % (2430826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.87/15.97 % (2430826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.87/15.97 % (2430826)CaDiCaL version: 2.1.3 % 104.87/15.97 % (2430826)Termination reason: Unknown % 104.87/15.97 % (2430826)Termination phase: Saturation % 104.87/15.97 % (2430826)Time elapsed: 0.598 s % 104.87/15.97 % (2430826)Peak memory usage: 113 MB % 104.87/15.97 % (2430826)Instructions burned: 540 (million) % 104.87/15.97 % (2430833)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=1179593739:i=33824:bd=preordered_2873 on theBenchmark for (2873ds/33824Mi) % 104.87/15.97 % (2430834)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=3888092851:i=20684:bd=all:gtg=exists_sym_2872 on theBenchmark for (2872ds/20684Mi) % 111.55/16.91 % (2430829)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.55/16.91 % (2430829)------------------------------ % 111.55/16.91 % (2430829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.55/16.91 % (2430829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.55/16.91 % (2430829)CaDiCaL version: 2.1.3 % 111.55/16.91 % (2430829)Termination reason: Unknown % 111.55/16.91 % (2430829)Termination phase: Saturation % 111.55/16.91 % (2430829)Time elapsed: 0.593 s % 111.55/16.91 % (2430829)Peak memory usage: 113 MB % 111.55/16.91 % (2430829)Instructions burned: 540 (million) % 111.55/16.91 % (2430835)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=1867551735: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_2872 on theBenchmark for (2872ds/7222Mi) % 111.55/16.91 % (2430835)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 111.55/16.91 % (2430834)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.55/16.91 % (2430834)------------------------------ % 111.55/16.91 % (2430834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.55/16.91 % (2430834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.55/16.91 % (2430834)CaDiCaL version: 2.1.3 % 111.55/16.91 % (2430834)Termination reason: Unknown % 111.55/16.91 % (2430834)Termination phase: Saturation % 111.55/16.91 % (2430834)Time elapsed: 0.323 s % 111.55/16.91 % (2430834)Peak memory usage: 114 MB % 111.55/16.91 % (2430834)Instructions burned: 543 (million) % 111.55/16.91 % (2430838)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3932410758:st=4:i=7295:sd=4:ep=R:ss=axioms_2870 on theBenchmark for (2870ds/7295Mi) % 111.55/16.91 % (2430833)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.55/16.91 % (2430833)------------------------------ % 111.55/16.91 % (2430833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.55/16.91 % (2430833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.55/16.91 % (2430833)CaDiCaL version: 2.1.3 % 111.55/16.91 % (2430833)Termination reason: Unknown % 111.55/16.91 % (2430833)Termination phase: Saturation % 111.55/16.91 % (2430833)Time elapsed: 0.562 s % 111.55/16.91 % (2430833)Peak memory usage: 114 MB % 111.55/16.91 % (2430833)Instructions burned: 541 (million) % 111.55/16.91 % (2430848)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=4035639838:i=4036:ins=10_2867 on theBenchmark for (2867ds/4036Mi) % 111.55/16.91 % (2430835)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.55/16.91 % (2430835)------------------------------ % 111.55/16.91 % (2430835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.55/16.91 % (2430835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.55/16.91 % (2430835)CaDiCaL version: 2.1.3 % 111.55/16.91 % (2430835)Termination reason: Unknown % 111.55/16.91 % (2430835)Termination phase: Saturation % 111.55/16.91 % (2430835)Time elapsed: 0.582 s % 111.55/16.91 % (2430835)Peak memory usage: 114 MB % 111.55/16.91 % (2430835)Instructions burned: 543 (million) % 111.55/16.91 % (2430850)lrs+10_1_sil=128000:lcm=predicate:random_seed=2627936178:st=3:i=43697:sd=5:ss=axioms_2865 on theBenchmark for (2865ds/43697Mi) % 111.55/16.91 % (2430848)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 111.55/16.91 % (2430848)------------------------------ % 111.55/16.91 % (2430848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.55/16.91 % (2430848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.55/16.91 % (2430848)CaDiCaL version: 2.1.3 % 111.55/16.91 % (2430848)Termination reason: Unknown % 111.55/16.91 % (2430848)Termination phase: Saturation % 111.55/16.91 % (2430848)Time elapsed: 0.320 s % 111.55/16.91 % (2430848)Peak memory usage: 113 MB % 111.55/16.91 % (2430848)Instructions burned: 539 (million) % 111.55/16.91 % (2430852)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=1319684183:i=17599:gtg=all:ss=axioms:fsd=on_2863 on theBenchmark for (2863ds/17599Mi) % 118.63/17.81 % (2430838)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 118.63/17.81 % (2430838)------------------------------ % 118.63/17.81 % (2430838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.63/17.81 % (2430838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.63/17.81 % (2430838)CaDiCaL version: 2.1.3 % 118.63/17.81 % (2430838)Termination reason: Unknown % 118.63/17.81 % (2430838)Termination phase: Saturation % 118.63/17.81 % (2430838)Time elapsed: 0.594 s % 118.63/17.81 % (2430838)Peak memory usage: 113 MB % 118.63/17.81 % (2430838)Instructions burned: 541 (million) % 118.63/17.81 % (2430854)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=492024907:i=4547:bd=preordered_2861 on theBenchmark for (2861ds/4547Mi) % 118.63/17.81 % (2430856)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=1875163221:i=9294:av=off_2860 on theBenchmark for (2860ds/9294Mi) % 118.63/17.81 % (2430854)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 118.63/17.81 % (2430854)------------------------------ % 118.63/17.81 % (2430854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.63/17.81 % (2430854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.63/17.81 % (2430854)CaDiCaL version: 2.1.3 % 118.63/17.81 % (2430854)Termination reason: Unknown % 118.63/17.81 % (2430854)Termination phase: Saturation % 118.63/17.81 % (2430854)Time elapsed: 0.331 s % 118.63/17.81 % (2430854)Peak memory usage: 113 MB % 118.63/17.81 % (2430854)Instructions burned: 540 (million) % 118.63/17.81 % (2430852)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 118.63/17.81 % (2430852)------------------------------ % 118.63/17.81 % (2430852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.63/17.81 % (2430852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.63/17.81 % (2430852)CaDiCaL version: 2.1.3 % 118.63/17.81 % (2430852)Termination reason: Unknown % 118.63/17.81 % (2430852)Termination phase: Saturation % 118.63/17.81 % (2430852)Time elapsed: 0.597 s % 118.63/17.81 % (2430852)Peak memory usage: 113 MB % 118.63/17.81 % (2430852)Instructions burned: 542 (million) % 118.63/17.81 % (2430859)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=4193829900:i=32849:add=on_2856 on theBenchmark for (2856ds/32849Mi) % 118.63/17.81 % (2430860)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1624689730:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2855 on theBenchmark for (2855ds/4793Mi) % 118.63/17.81 % (2430856)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 118.63/17.81 % (2430856)------------------------------ % 118.63/17.81 % (2430856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.63/17.81 % (2430856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.63/17.81 % (2430856)CaDiCaL version: 2.1.3 % 118.63/17.81 % (2430856)Termination reason: Unknown % 118.63/17.81 % (2430856)Termination phase: Saturation % 118.63/17.81 % (2430856)Time elapsed: 0.592 s % 118.63/17.81 % (2430856)Peak memory usage: 114 MB % 118.63/17.81 % (2430856)Instructions burned: 540 (million) % 118.63/17.81 % (2430790)Instruction limit reached! % 118.63/17.81 % (2430790)------------------------------ % 118.63/17.81 % (2430790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.63/17.81 % (2430790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.63/17.81 % (2430790)CaDiCaL version: 2.1.3 % 118.63/17.81 % (2430790)Termination reason: Instruction limit % 118.63/17.81 % (2430790)Termination phase: Saturation % 118.63/17.81 % (2430790)Time elapsed: 5.228 s % 118.63/17.81 % (2430790)Peak memory usage: 113 MB % 118.63/17.81 % (2430790)Instructions burned: 5469 (million) % 118.63/17.81 % (2430860)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 118.63/17.81 % (2430860)------------------------------ % 118.63/17.81 % (2430860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.63/17.81 % (2430860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.63/17.81 % (2430860)CaDiCaL version: 2.1.3 % 118.63/17.81 % (2430860)Termination reason: Unknown % 118.63/17.81 % (2430860)Termination phase: Saturation % 135.91/20.19 % (2430860)Time elapsed: 0.319 s % 135.91/20.19 % (2430860)Peak memory usage: 113 MB % 135.91/20.19 % (2430860)Instructions burned: 540 (million) % 135.91/20.19 % (2430863)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=3908859085:i=4840:nm=4:av=off_2852 on theBenchmark for (2852ds/4840Mi) % 135.91/20.19 % (2430864)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=1655595990:cts=off:i=5002_2851 on theBenchmark for (2851ds/5002Mi) % 135.91/20.19 % (2430859)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 135.91/20.19 % (2430859)------------------------------ % 135.91/20.19 % (2430859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.91/20.19 % (2430859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.91/20.19 % (2430859)CaDiCaL version: 2.1.3 % 135.91/20.19 % (2430859)Termination reason: Unknown % 135.91/20.19 % (2430859)Termination phase: Saturation % 135.91/20.19 % (2430859)Time elapsed: 0.596 s % 135.91/20.19 % (2430859)Peak memory usage: 113 MB % 135.91/20.19 % (2430859)Instructions burned: 540 (million) % 135.91/20.19 % (2430865)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=639376810:i=30479:sd=3:ss=axioms_2850 on theBenchmark for (2850ds/30479Mi) % 135.91/20.19 % (2430863)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 135.91/20.19 % (2430863)------------------------------ % 135.91/20.19 % (2430863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.91/20.19 % (2430863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.91/20.19 % (2430863)CaDiCaL version: 2.1.3 % 135.91/20.19 % (2430863)Termination reason: Unknown % 135.91/20.19 % (2430863)Termination phase: Saturation % 135.91/20.19 % (2430863)Time elapsed: 0.322 s % 135.91/20.19 % (2430863)Peak memory usage: 113 MB % 135.91/20.19 % (2430863)Instructions burned: 542 (million) % 135.91/20.19 % (2430868)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=2026674020:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2847 on theBenchmark for (2847ds/11035Mi) % 135.91/20.19 % (2430868)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 135.91/20.19 % (2430870)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=2027156331:i=5835_2846 on theBenchmark for (2846ds/5835Mi) % 135.91/20.19 % (2430864)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 135.91/20.19 % (2430864)------------------------------ % 135.91/20.19 % (2430864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.91/20.19 % (2430864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.91/20.19 % (2430864)CaDiCaL version: 2.1.3 % 135.91/20.19 % (2430864)Termination reason: Unknown % 135.91/20.19 % (2430864)Termination phase: Saturation % 135.91/20.19 % (2430864)Time elapsed: 0.565 s % 135.91/20.19 % (2430864)Peak memory usage: 113 MB % 135.91/20.19 % (2430864)Instructions burned: 540 (million) % 135.91/20.19 % (2430865)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 135.91/20.19 % (2430865)------------------------------ % 135.91/20.19 % (2430865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.91/20.19 % (2430865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 135.91/20.19 % (2430865)CaDiCaL version: 2.1.3 % 135.91/20.19 % (2430865)Termination reason: Unknown % 135.91/20.19 % (2430865)Termination phase: Saturation % 135.91/20.19 % (2430865)Time elapsed: 0.593 s % 135.91/20.19 % (2430865)Peak memory usage: 113 MB % 135.91/20.19 % (2430865)Instructions burned: 539 (million) % 135.91/20.19 % (2430873)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2101458316:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2843 on theBenchmark for (2843ds/5890Mi) % 135.91/20.19 % (2430870)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 135.91/20.19 % (2430870)------------------------------ % 135.91/20.19 % (2430870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 135.91/20.19 % (2430870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.64/25.90 % (2430870)CaDiCaL version: 2.1.3 % 176.64/25.90 % (2430870)Termination reason: Unknown % 176.64/25.90 % (2430870)Termination phase: Saturation % 176.64/25.90 % (2430870)Time elapsed: 0.318 s % 176.64/25.90 % (2430870)Peak memory usage: 113 MB % 176.64/25.90 % (2430870)Instructions burned: 540 (million) % 176.64/25.90 % (2430868)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 176.64/25.90 % (2430868)------------------------------ % 176.64/25.90 % (2430868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.64/25.90 % (2430868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.64/25.90 % (2430868)CaDiCaL version: 2.1.3 % 176.64/25.90 % (2430868)Termination reason: Unknown % 176.64/25.90 % (2430868)Termination phase: Saturation % 176.64/25.90 % (2430868)Time elapsed: 0.596 s % 176.64/25.90 % (2430868)Peak memory usage: 114 MB % 176.64/25.90 % (2430868)Instructions burned: 542 (million) % 176.64/25.90 % (2430876)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=216553336:i=20312:bd=preordered:fsr=off:er=filter_2840 on theBenchmark for (2840ds/20312Mi) % 176.64/25.90 % (2430874)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=124269884:cts=off:i=19910:ep=RS_2841 on theBenchmark for (2841ds/19910Mi) % 176.64/25.90 % (2430874)Refutation not found, incomplete strategy % 176.64/25.90 % (2430874)------------------------------ % 176.64/25.90 % (2430874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.64/25.90 % (2430874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.64/25.90 % (2430874)CaDiCaL version: 2.1.3 % 176.64/25.90 % (2430874)Termination reason: Refutation not found, incomplete strategy % 176.64/25.90 % (2430874)Time elapsed: 0.008 s % 176.64/25.90 % (2430874)Peak memory usage: 88 MB % 176.64/25.90 % (2430874)Instructions burned: 8 (million) % 176.64/25.90 % (2430877)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=1164041429:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2838 on theBenchmark for (2838ds/13822Mi) % 176.64/25.90 % (2430873)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 176.64/25.90 % (2430873)------------------------------ % 176.64/25.90 % (2430873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.64/25.90 % (2430873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.64/25.90 % (2430873)CaDiCaL version: 2.1.3 % 176.64/25.90 % (2430873)Termination reason: Unknown % 176.64/25.90 % (2430873)Termination phase: Saturation % 176.64/25.90 % (2430873)Time elapsed: 0.543 s % 176.64/25.90 % (2430873)Peak memory usage: 114 MB % 176.64/25.90 % (2430873)Instructions burned: 540 (million) % 176.64/25.90 % (2430874)------------------------------ % 176.64/25.90 % (2430874)------------------------------ % 176.64/25.90 % (2430881)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=2548210853:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2835 on theBenchmark for (2835ds/7144Mi) % 176.64/25.90 % (2430877)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 176.64/25.90 % (2430877)------------------------------ % 176.64/25.90 % (2430877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.64/25.90 % (2430877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.64/25.91 % (2430877)CaDiCaL version: 2.1.3 % 176.64/25.91 % (2430877)Termination reason: Unknown % 176.64/25.91 % (2430877)Termination phase: Saturation % 176.64/25.91 % (2430877)Time elapsed: 0.322 s % 176.64/25.91 % (2430877)Peak memory usage: 114 MB % 176.64/25.91 % (2430877)Instructions burned: 541 (million) % 176.64/25.91 % (2430876)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 176.64/25.91 % (2430876)------------------------------ % 176.64/25.91 % (2430876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.64/25.91 % (2430876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.64/25.91 % (2430876)CaDiCaL version: 2.1.3 % 176.64/25.91 % (2430876)Termination reason: Unknown % 176.64/25.91 % (2430876)Termination phase: Saturation % 176.64/25.91 % (2430876)Time elapsed: 0.596 s % 176.64/25.91 % (2430876)Peak memory usage: 113 MB % 176.64/25.91 % (2430876)Instructions burned: 540 (million) % 176.64/25.91 % (2430882)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=726971604:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2834 on theBenchmark for (2834ds/15184Mi) % 187.37/27.48 % (2430884)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=2537790140:i=107375_2832 on theBenchmark for (2832ds/107375Mi) % 187.37/27.48 % (2430885)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=1056669091:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2832 on theBenchmark for (2832ds/7958Mi) % 187.37/27.48 % (2430885)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 187.37/27.48 % (2430885)------------------------------ % 187.37/27.48 % (2430885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.37/27.48 % (2430885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.37/27.48 % (2430885)CaDiCaL version: 2.1.3 % 187.37/27.48 % (2430885)Termination reason: Unknown % 187.37/27.48 % (2430885)Termination phase: Saturation % 187.37/27.48 % (2430885)Time elapsed: 0.325 s % 187.37/27.48 % (2430885)Peak memory usage: 114 MB % 187.37/27.48 % (2430885)Instructions burned: 540 (million) % 187.37/27.48 % (2430882)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 187.37/27.48 % (2430882)------------------------------ % 187.37/27.48 % (2430882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.37/27.48 % (2430882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.37/27.48 % (2430882)CaDiCaL version: 2.1.3 % 187.37/27.48 % (2430882)Termination reason: Unknown % 187.37/27.48 % (2430882)Termination phase: Saturation % 187.37/27.48 % (2430882)Time elapsed: 0.595 s % 187.37/27.48 % (2430882)Peak memory usage: 114 MB % 187.37/27.48 % (2430882)Instructions burned: 541 (million) % 187.37/27.48 % (2430884)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 187.37/27.48 % (2430884)------------------------------ % 187.37/27.48 % (2430884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.37/27.48 % (2430884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.37/27.48 % (2430884)CaDiCaL version: 2.1.3 % 187.37/27.48 % (2430884)Termination reason: Unknown % 187.37/27.48 % (2430884)Termination phase: Saturation % 187.37/27.48 % (2430884)Time elapsed: 0.539 s % 187.37/27.48 % (2430884)Peak memory usage: 113 MB % 187.37/27.48 % (2430884)Instructions burned: 540 (million) % 187.37/27.48 % (2430889)dis+10_128_sil=16000:nwc=0.7:random_seed=4210323720:i=15999:nm=2:gsp=on_2826 on theBenchmark for (2826ds/15999Mi) % 187.37/27.48 % (2430889)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 187.37/27.48 % (2430890)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1953511245:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2825 on theBenchmark for (2825ds/8139Mi) % 187.37/27.48 % (2430891)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=2599643328:st=4:i=8950:sd=5:ss=axioms_2825 on theBenchmark for (2825ds/8950Mi) % 187.37/27.48 % (2430891)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 187.37/27.48 % (2430891)------------------------------ % 187.37/27.48 % (2430891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.37/27.48 % (2430891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.37/27.48 % (2430891)CaDiCaL version: 2.1.3 % 187.37/27.48 % (2430891)Termination reason: Unknown % 187.37/27.48 % (2430891)Termination phase: Saturation % 187.37/27.48 % (2430891)Time elapsed: 0.598 s % 187.37/27.48 % (2430891)Peak memory usage: 113 MB % 187.37/27.48 % (2430891)Instructions burned: 540 (million) % 187.37/27.48 % (2430895)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=444294080:i=9809:ins=10:av=off_2816 on theBenchmark for (2816ds/9809Mi) % 187.37/27.48 % (2430895)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 187.37/27.48 % (2430895)------------------------------ % 187.37/27.48 % (2430895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 187.37/27.48 % (2430895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 187.37/27.48 % (2430895)CaDiCaL version: 2.1.3 % 187.37/27.48 % (2430895)Termination reason: Unknown % 187.37/27.48 % (2430895)Termination phase: Saturation % 187.37/27.48 % (2430895)Time elapsed: 0.597 s % 187.37/27.48 % (2430895)Peak memory usage: 114 MB % 214.43/31.26 % (2430895)Instructions burned: 540 (million) % 214.43/31.26 % (2430897)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2331193797:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2807 on theBenchmark for (2807ds/9885Mi) % 214.43/31.26 % (2430897)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 214.43/31.26 % (2430897)------------------------------ % 214.43/31.26 % (2430897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.43/31.26 % (2430897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.43/31.26 % (2430897)CaDiCaL version: 2.1.3 % 214.43/31.26 % (2430897)Termination reason: Unknown % 214.43/31.26 % (2430897)Termination phase: Saturation % 214.43/31.26 % (2430897)Time elapsed: 0.601 s % 214.43/31.26 % (2430897)Peak memory usage: 114 MB % 214.43/31.26 % (2430897)Instructions burned: 540 (million) % 214.43/31.26 % (2430899)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1000643261:cond=fast:i=32078:fgj=on:av=off_2799 on theBenchmark for (2799ds/32078Mi) % 214.43/31.26 % (2430899)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 214.43/31.26 % (2430899)------------------------------ % 214.43/31.26 % (2430899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.43/31.26 % (2430899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.43/31.26 % (2430899)CaDiCaL version: 2.1.3 % 214.43/31.26 % (2430899)Termination reason: Unknown % 214.43/31.26 % (2430899)Termination phase: Saturation % 214.43/31.26 % (2430899)Time elapsed: 0.602 s % 214.43/31.26 % (2430899)Peak memory usage: 114 MB % 214.43/31.26 % (2430899)Instructions burned: 541 (million) % 214.43/31.26 % (2430901)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=1044682758:i=11101:bd=all:ss=axioms:sgt=8_2791 on theBenchmark for (2791ds/11101Mi) % 214.43/31.26 % (2430881)Instruction limit reached! % 214.43/31.26 % (2430881)------------------------------ % 214.43/31.26 % (2430881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.43/31.26 % (2430881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.43/31.26 % (2430881)CaDiCaL version: 2.1.3 % 214.43/31.26 % (2430881)Termination reason: Instruction limit % 214.43/31.26 % (2430881)Termination phase: Saturation % 214.43/31.26 % (2430881)Time elapsed: 6.258 s % 214.43/31.26 % (2430881)Peak memory usage: 138 MB % 214.43/31.26 % (2430881)Instructions burned: 7144 (million) % 214.43/31.26 % (2430905)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3602577466:cond=on:i=13220:s2at=3:aac=none:fsd=on_2770 on theBenchmark for (2770ds/13220Mi) % 214.43/31.26 % (2430905)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 214.43/31.26 % (2430905)------------------------------ % 214.43/31.26 % (2430905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.43/31.26 % (2430905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.43/31.26 % (2430905)CaDiCaL version: 2.1.3 % 214.43/31.26 % (2430905)Termination reason: Unknown % 214.43/31.26 % (2430905)Termination phase: Saturation % 214.43/31.26 % (2430905)Time elapsed: 0.541 s % 214.43/31.26 % (2430905)Peak memory usage: 114 MB % 214.43/31.26 % (2430905)Instructions burned: 541 (million) % 214.43/31.26 % (2430907)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=1004714284:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2761 on theBenchmark for (2761ds/13528Mi) % 214.43/31.26 % (2430907)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 214.43/31.26 % (2430907)------------------------------ % 214.43/31.26 % (2430907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.43/31.26 % (2430907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.43/31.26 % (2430907)CaDiCaL version: 2.1.3 % 214.43/31.26 % (2430907)Termination reason: Unknown % 214.43/31.26 % (2430907)Termination phase: Saturation % 214.43/31.26 % (2430907)Time elapsed: 0.543 s % 214.43/31.26 % (2430907)Peak memory usage: 114 MB % 214.43/31.26 % (2430907)Instructions burned: 541 (million) % 214.43/31.26 % (2430909)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=4288715464:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2753 on theBenchmark for (2753ds/14854Mi) % 237.71/34.66 % (2430889)Instruction limit reached! % 237.71/34.66 % (2430889)------------------------------ % 237.71/34.66 % (2430889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.71/34.66 % (2430889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/34.66 % (2430889)CaDiCaL version: 2.1.3 % 237.71/34.66 % (2430889)Termination reason: Instruction limit % 237.71/34.66 % (2430889)Termination phase: Saturation % 237.71/34.66 % (2430889)Time elapsed: 7.877 s % 237.71/34.66 % (2430889)Peak memory usage: 182 MB % 237.71/34.66 % (2430889)Instructions burned: 16000 (million) % 237.71/34.66 % (2430909)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.71/34.66 % (2430909)------------------------------ % 237.71/34.66 % (2430909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.71/34.66 % (2430909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/34.66 % (2430909)CaDiCaL version: 2.1.3 % 237.71/34.66 % (2430909)Termination reason: Unknown % 237.71/34.66 % (2430909)Termination phase: Saturation % 237.71/34.66 % (2430909)Time elapsed: 0.535 s % 237.71/34.66 % (2430909)Peak memory usage: 114 MB % 237.71/34.66 % (2430909)Instructions burned: 547 (million) % 237.71/34.66 % (2430917)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=296727881:i=14974:ss=axioms:sgt=16_2745 on theBenchmark for (2745ds/14974Mi) % 237.71/34.66 % (2430890)Instruction limit reached! % 237.71/34.66 % (2430890)------------------------------ % 237.71/34.66 % (2430890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.71/34.66 % (2430890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/34.66 % (2430890)CaDiCaL version: 2.1.3 % 237.71/34.66 % (2430890)Termination reason: Instruction limit % 237.71/34.66 % (2430890)Termination phase: Saturation % 237.71/34.66 % (2430890)Time elapsed: 8.057 s % 237.71/34.66 % (2430890)Peak memory usage: 136 MB % 237.71/34.66 % (2430890)Instructions burned: 8140 (million) % 237.71/34.66 % (2430918)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=3516933173:i=33081:aac=none:fgj=on:bd=all:fsr=off_2745 on theBenchmark for (2745ds/33081Mi) % 237.71/34.66 % (2430917)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.71/34.66 % (2430917)------------------------------ % 237.71/34.66 % (2430917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.71/34.66 % (2430917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/34.66 % (2430917)CaDiCaL version: 2.1.3 % 237.71/34.66 % (2430917)Termination reason: Unknown % 237.71/34.66 % (2430917)Termination phase: Saturation % 237.71/34.66 % (2430917)Time elapsed: 0.324 s % 237.71/34.66 % (2430917)Peak memory usage: 113 MB % 237.71/34.66 % (2430917)Instructions burned: 540 (million) % 237.71/34.66 % (2430921)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=2322722810:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2742 on theBenchmark for (2742ds/50856Mi) % 237.71/34.66 % (2430922)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3186470728:i=69865_2740 on theBenchmark for (2740ds/69865Mi) % 237.71/34.66 % (2430918)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.71/34.66 % (2430918)------------------------------ % 237.71/34.66 % (2430918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.71/34.66 % (2430918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/34.66 % (2430918)CaDiCaL version: 2.1.3 % 237.71/34.66 % (2430918)Termination reason: Unknown % 237.71/34.66 % (2430918)Termination phase: Saturation % 237.71/34.66 % (2430918)Time elapsed: 0.541 s % 237.71/34.66 % (2430918)Peak memory usage: 114 MB % 237.71/34.66 % (2430918)Instructions burned: 540 (million) % 237.71/34.66 % (2430922)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 237.71/34.66 % (2430922)------------------------------ % 237.71/34.66 % (2430922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.71/34.66 % (2430922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.71/34.66 % (2430922)CaDiCaL version: 2.1.3 % 237.71/34.66 % (2430922)Termination reason: Unknown % 237.71/34.66 % (2430922)Termination phase: Saturation % 256.52/37.26 % (2430922)Time elapsed: 0.326 s % 256.52/37.26 % (2430922)Peak memory usage: 113 MB % 256.52/37.26 % (2430922)Instructions burned: 540 (million) % 256.52/37.26 % (2430925)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=3739077290:cond=fast:i=17802:gtgl=3:gtg=all_2737 on theBenchmark for (2737ds/17802Mi) % 256.52/37.26 % (2430921)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 256.52/37.26 % (2430921)------------------------------ % 256.52/37.26 % (2430921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.52/37.26 % (2430921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.52/37.26 % (2430921)CaDiCaL version: 2.1.3 % 256.52/37.26 % (2430921)Termination reason: Unknown % 256.52/37.26 % (2430921)Termination phase: Saturation % 256.52/37.26 % (2430921)Time elapsed: 0.593 s % 256.52/37.26 % (2430921)Peak memory usage: 114 MB % 256.52/37.26 % (2430921)Instructions burned: 540 (million) % 256.52/37.26 % (2430926)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=1271242930:i=96644_2735 on theBenchmark for (2735ds/96644Mi) % 256.52/37.26 % (2430930)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 256.52/37.26 % (2430930)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=29781833:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2733 on theBenchmark for (2733ds/21161Mi) % 256.52/37.26 % (2430925)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 256.52/37.26 % (2430925)------------------------------ % 256.52/37.26 % (2430925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.52/37.26 % (2430925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.52/37.26 % (2430925)CaDiCaL version: 2.1.3 % 256.52/37.26 % (2430925)Termination reason: Unknown % 256.52/37.26 % (2430925)Termination phase: Saturation % 256.52/37.26 % (2430925)Time elapsed: 0.407 s % 256.52/37.26 % (2430925)Peak memory usage: 113 MB % 256.52/37.26 % (2430925)Instructions burned: 543 (million) % 256.52/37.26 % (2431002)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=209380304:i=22761:gtg=all:ss=axioms:fsd=on_2730 on theBenchmark for (2730ds/22761Mi) % 256.52/37.26 % (2431002)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 256.52/37.26 % (2431002)------------------------------ % 256.52/37.26 % (2431002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.52/37.26 % (2431002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.52/37.26 % (2431002)CaDiCaL version: 2.1.3 % 256.52/37.26 % (2431002)Termination reason: Unknown % 256.52/37.26 % (2431002)Termination phase: Saturation % 256.52/37.26 % (2431002)Time elapsed: 0.362 s % 256.52/37.26 % (2431002)Peak memory usage: 113 MB % 256.52/37.26 % (2431002)Instructions burned: 542 (million) % 256.52/37.26 % (2431088)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=910754530:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2725 on theBenchmark for (2725ds/23713Mi) % 256.52/37.26 % (2430901)Instruction limit reached! % 256.52/37.26 % (2430901)------------------------------ % 256.52/37.26 % (2430901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.52/37.26 % (2430901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.52/37.26 % (2430901)CaDiCaL version: 2.1.3 % 256.52/37.26 % (2430901)Termination reason: Instruction limit % 256.52/37.26 % (2430901)Termination phase: Saturation % 256.52/37.26 % (2430901)Time elapsed: 8.535 s % 256.52/37.26 % (2430901)Peak memory usage: 193 MB % 256.52/37.26 % (2430901)Instructions burned: 11102 (million) % 256.52/37.26 % (2431091)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3793695582:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2702 on theBenchmark for (2702ds/26509Mi) % 256.52/37.26 % (2431091)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 256.52/37.26 % (2431091)------------------------------ % 256.52/37.26 % (2431091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.52/37.26 % (2431091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.52/37.26 % (2431091)CaDiCaL version: 2.1.3 % 256.52/37.26 % (2431091)Termination reason: Unknown % 272.66/39.51 % (2431091)Termination phase: Saturation % 272.66/39.51 % (2431091)Time elapsed: 0.359 s % 272.66/39.51 % (2431091)Peak memory usage: 113 MB % 272.66/39.51 % (2431091)Instructions burned: 540 (million) % 272.66/39.51 % (2431093)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=3198138433:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2697 on theBenchmark for (2697ds/28957Mi) % 272.66/39.51 % (2430765)Instruction limit reached! % 272.66/39.51 % (2430765)------------------------------ % 272.66/39.51 % (2430765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.66/39.51 % (2430765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.66/39.51 % (2430765)CaDiCaL version: 2.1.3 % 272.66/39.51 % (2430765)Termination reason: Instruction limit % 272.66/39.51 % (2430765)Termination phase: Saturation % 272.66/39.51 % (2430765)Time elapsed: 24.260 s % 272.66/39.51 % (2430765)Peak memory usage: 412 MB % 272.66/39.51 % (2430765)Instructions burned: 26473 (million) % 272.66/39.51 % (2431095)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=1089425936:i=29246:s2at=-1:kws=inv_arity:ins=10_2678 on theBenchmark for (2678ds/29246Mi) % 272.66/39.51 % (2431095)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 272.66/39.51 % (2431095)------------------------------ % 272.66/39.51 % (2431095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.66/39.51 % (2431095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.66/39.51 % (2431095)CaDiCaL version: 2.1.3 % 272.66/39.51 % (2431095)Termination reason: Unknown % 272.66/39.51 % (2431095)Termination phase: Saturation % 272.66/39.51 % (2431095)Time elapsed: 0.359 s % 272.66/39.51 % (2431095)Peak memory usage: 114 MB % 272.66/39.51 % (2431095)Instructions burned: 541 (million) % 272.66/39.51 % (2431097)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=1596171916:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2673 on theBenchmark for (2673ds/30082Mi) % 272.66/39.51 % (2431097)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 272.66/39.51 % (2431097)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 272.66/39.51 % (2431097)------------------------------ % 272.66/39.51 % (2431097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.66/39.51 % (2431097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.66/39.51 % (2431097)CaDiCaL version: 2.1.3 % 272.66/39.51 % (2431097)Termination reason: Unknown % 272.66/39.51 % (2431097)Termination phase: Saturation % 272.66/39.51 % (2431097)Time elapsed: 0.358 s % 272.66/39.51 % (2431097)Peak memory usage: 114 MB % 272.66/39.51 % (2431097)Instructions burned: 543 (million) % 272.66/39.51 % (2430726)Instruction limit reached! % 272.66/39.51 % (2430726)------------------------------ % 272.66/39.51 % (2430726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.66/39.51 % (2430726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.66/39.51 % (2430726)CaDiCaL version: 2.1.3 % 272.66/39.51 % (2430726)Termination reason: Instruction limit % 272.66/39.51 % (2430726)Termination phase: Saturation % 272.66/39.51 % (2430726)Time elapsed: 27.794 s % 272.66/39.51 % (2430726)Peak memory usage: 170 MB % 272.66/39.51 % (2430726)Instructions burned: 33334 (million) % 272.66/39.51 % (2431099)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=4173522922:i=32262:bd=preordered_2668 on theBenchmark for (2668ds/32262Mi) % 272.66/39.51 % (2431100)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=850251247:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2668 on theBenchmark for (2668ds/32870Mi) % 272.66/39.51 % (2431099)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 272.66/39.51 % (2431099)------------------------------ % 272.66/39.51 % (2431099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.66/39.51 % (2431099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.66/39.51 % (2431099)CaDiCaL version: 2.1.3 % 272.66/39.51 % (2431099)Termination reason: Unknown % 272.66/39.51 % (2431099)Termination phase: Saturation % 272.66/39.51 % (2431099)Time elapsed: 0.359 s % 278.83/40.42 % (2431099)Peak memory usage: 113 MB % 278.83/40.42 % (2431099)Instructions burned: 540 (million) % 278.83/40.42 % (2431100)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 278.83/40.42 % (2431100)------------------------------ % 278.83/40.42 % (2431100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.83/40.42 % (2431100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.83/40.42 % (2431100)CaDiCaL version: 2.1.3 % 278.83/40.42 % (2431100)Termination reason: Unknown % 278.83/40.42 % (2431100)Termination phase: Saturation % 278.83/40.42 % (2431100)Time elapsed: 0.359 s % 278.83/40.42 % (2431100)Peak memory usage: 113 MB % 278.83/40.42 % (2431100)Instructions burned: 541 (million) % 278.83/40.42 % (2431103)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=3219161220:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2663 on theBenchmark for (2663ds/33295Mi) % 278.83/40.42 % (2431104)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=2139167903:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2662 on theBenchmark for (2662ds/36826Mi) % 278.83/40.42 % (2431103)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 278.83/40.42 % (2431103)------------------------------ % 278.83/40.42 % (2431103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.83/40.42 % (2431103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.83/40.42 % (2431103)CaDiCaL version: 2.1.3 % 278.83/40.42 % (2431103)Termination reason: Unknown % 278.83/40.42 % (2431103)Termination phase: Saturation % 278.83/40.42 % (2431103)Time elapsed: 0.358 s % 278.83/40.42 % (2431103)Peak memory usage: 114 MB % 278.83/40.42 % (2431103)Instructions burned: 541 (million) % 278.83/40.42 % (2431107)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=2293501586:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2658 on theBenchmark for (2658ds/92981Mi) % 278.83/40.42 % (2431107)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 278.83/40.42 % (2431107)------------------------------ % 278.83/40.42 % (2431107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.83/40.42 % (2431107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.83/40.42 % (2431107)CaDiCaL version: 2.1.3 % 278.83/40.42 % (2431107)Termination reason: Unknown % 278.83/40.42 % (2431107)Termination phase: Saturation % 278.83/40.42 % (2431107)Time elapsed: 0.358 s % 278.83/40.42 % (2431107)Peak memory usage: 113 MB % 278.83/40.42 % (2431107)Instructions burned: 541 (million) % 278.83/40.42 % (2431109)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=256451232:s2pl=on:i=49423_2652 on theBenchmark for (2652ds/49423Mi) % 278.83/40.42 % (2431109)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 278.83/40.42 % (2431109)------------------------------ % 278.83/40.42 % (2431109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.83/40.42 % (2431109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.83/40.42 % (2431109)CaDiCaL version: 2.1.3 % 278.83/40.42 % (2431109)Termination reason: Unknown % 278.83/40.42 % (2431109)Termination phase: Saturation % 278.83/40.42 % (2431109)Time elapsed: 0.358 s % 278.83/40.42 % (2431109)Peak memory usage: 113 MB % 278.83/40.42 % (2431109)Instructions burned: 542 (million) % 278.83/40.42 % (2431111)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=3435046976:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2647 on theBenchmark for (2647ds/57299Mi) % 278.83/40.42 % (2431111)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 278.83/40.42 % (2431111)------------------------------ % 278.83/40.42 % (2431111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.83/40.42 % (2431111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.83/40.42 % (2431111)CaDiCaL version: 2.1.3 % 278.83/40.42 % (2431111)Termination reason: Unknown % 278.83/40.42 % (2431111)Termination phase: Saturation % 278.83/40.42 % (2431111)Time elapsed: 0.356 s % 278.83/40.42 % (2431111)Peak memory usage: 113 MB % 284.92/41.29 % (2431111)Instructions burned: 540 (million) % 284.92/41.29 % (2431113)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=1813403132:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2637 on theBenchmark for (2637ds/127679Mi) % 284.92/41.29 % (2431113)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 284.92/41.29 % (2431113)------------------------------ % 284.92/41.29 % (2431113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.92/41.29 % (2431113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.92/41.29 % (2431113)CaDiCaL version: 2.1.3 % 284.92/41.29 % (2431113)Termination reason: Unknown % 284.92/41.29 % (2431113)Termination phase: Saturation % 284.92/41.29 % (2431113)Time elapsed: 0.358 s % 284.92/41.29 % (2431113)Peak memory usage: 114 MB % 284.92/41.29 % (2431113)Instructions burned: 541 (million) % 284.92/41.29 % (2431115)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=744056064:i=69402:add=on:aac=none:fsr=off_2631 on theBenchmark for (2631ds/69402Mi) % 284.92/41.29 % (2431115)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 284.92/41.29 % (2431115)------------------------------ % 284.92/41.29 % (2431115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.92/41.29 % (2431115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.92/41.29 % (2431115)CaDiCaL version: 2.1.3 % 284.92/41.29 % (2431115)Termination reason: Unknown % 284.92/41.29 % (2431115)Termination phase: Saturation % 284.92/41.29 % (2431115)Time elapsed: 0.358 s % 284.92/41.29 % (2431115)Peak memory usage: 113 MB % 284.92/41.29 % (2431115)Instructions burned: 540 (million) % 284.92/41.29 % (2431117)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=3515688993:i=100512:doe=on:fgj=on:bd=all:fsd=on_2626 on theBenchmark for (2626ds/100512Mi) % 284.92/41.29 % (2431117)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 284.92/41.29 % (2431117)------------------------------ % 284.92/41.29 % (2431117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.92/41.29 % (2431117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.92/41.29 % (2431117)CaDiCaL version: 2.1.3 % 284.92/41.29 % (2431117)Termination reason: Unknown % 284.92/41.29 % (2431117)Termination phase: Saturation % 284.92/41.29 % (2431117)Time elapsed: 0.358 s % 284.92/41.29 % (2431117)Peak memory usage: 113 MB % 284.92/41.29 % (2431117)Instructions burned: 542 (million) % 284.92/41.29 % (2431119)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=2799912235:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2621 on theBenchmark for (2621ds/138761Mi) % 284.92/41.29 % (2431119)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 284.92/41.29 % (2431119)------------------------------ % 284.92/41.29 % (2431119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.92/41.29 % (2431119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.92/41.29 % (2431119)CaDiCaL version: 2.1.3 % 284.92/41.29 % (2431119)Termination reason: Unknown % 284.92/41.29 % (2431119)Termination phase: Saturation % 284.92/41.29 % (2431119)Time elapsed: 0.357 s % 284.92/41.29 % (2431119)Peak memory usage: 114 MB % 284.92/41.29 % (2431119)Instructions burned: 541 (million) % 284.92/41.29 % (2430930)Instruction limit reached! % 284.92/41.29 % (2430930)------------------------------ % 284.92/41.29 % (2430930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.92/41.29 % (2430930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.92/41.29 % (2430930)CaDiCaL version: 2.1.3 % 284.92/41.29 % (2430930)Termination reason: Instruction limit % 284.92/41.29 % (2430930)Termination phase: Saturation % 284.92/41.29 % (2430930)Time elapsed: 11.639 s % 284.92/41.29 % (2430930)Peak memory usage: 214 MB % 284.92/41.29 % (2430930)Instructions burned: 21162 (million) % 284.92/41.29 % (2431121)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=3910996775:i=282386:rtra=on_2616 on theBenchmark for (2616ds/282386Mi) % 289.43/41.92 % (2431122)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=2428691529:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2615 on theBenchmark for (2615ds/269354Mi) % 289.43/41.92 % (2431121)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 289.43/41.92 % (2431121)------------------------------ % 289.43/41.92 % (2431121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.92 % (2431121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.92 % (2431121)CaDiCaL version: 2.1.3 % 289.43/41.92 % (2431121)Termination reason: Unknown % 289.43/41.92 % (2431121)Termination phase: Saturation % 289.43/41.92 % (2431121)Time elapsed: 0.358 s % 289.43/41.92 % (2431121)Peak memory usage: 114 MB % 289.43/41.92 % (2431121)Instructions burned: 540 (million) % 289.43/41.92 % (2431122)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 289.43/41.92 % (2431122)------------------------------ % 289.43/41.92 % (2431122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.92 % (2431122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.92 % (2431122)CaDiCaL version: 2.1.3 % 289.43/41.92 % (2431122)Termination reason: Unknown % 289.43/41.92 % (2431122)Termination phase: Saturation % 289.43/41.92 % (2431122)Time elapsed: 0.362 s % 289.43/41.92 % (2431122)Peak memory usage: 114 MB % 289.43/41.92 % (2431122)Instructions burned: 543 (million) % 289.43/41.92 % (2431125)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=259666586:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2611 on theBenchmark for (2611ds/283390Mi) % 289.43/41.92 % (2431125)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 289.43/41.92 % (2431088)Instruction limit reached! % 289.43/41.92 % (2431088)------------------------------ % 289.43/41.92 % (2431088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.92 % (2431088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.92 % (2431088)CaDiCaL version: 2.1.3 % 289.43/41.92 % (2431088)Termination reason: Instruction limit % 289.43/41.92 % (2431088)Termination phase: Saturation % 289.43/41.92 % (2431088)Time elapsed: 11.477 s % 289.43/41.92 % (2431088)Peak memory usage: 363 MB % 289.43/41.92 % (2431088)Instructions burned: 23713 (million) % 289.43/41.92 % (2431126)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=3864427100:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2610 on theBenchmark for (2610ds/218Mi) % 289.43/41.92 % (2431126)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 289.43/41.92 % (2431126)Instruction limit reached! % 289.43/41.92 % (2431126)------------------------------ % 289.43/41.92 % (2431126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.92 % (2431126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.92 % (2431126)CaDiCaL version: 2.1.3 % 289.43/41.92 % (2431126)Termination reason: Instruction limit % 289.43/41.92 % (2431126)Termination phase: Saturation % 289.43/41.92 % (2431126)Time elapsed: 0.109 s % 289.43/41.92 % (2431126)Peak memory usage: 90 MB % 289.43/41.92 % (2431126)Instructions burned: 218 (million) % 289.43/41.92 % (2431129)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=3939492049:i=238:av=off:rtra=on:ss=axioms_2608 on theBenchmark for (2608ds/238Mi) % 289.43/41.92 % (2431125)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p % 289.43/41.92 % (2431125)------------------------------ % 289.43/41.92 % (2431125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.43/41.92 % (2431125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.43/41.92 % (2431125)CaDiCaL version: 2.1.3 % 289.43/41.92 % (2431125)Termination reason: Unknown % 289.43/41.92 % (2431125)Termination phase: Saturation % 289.43/41.92 % (2431125)Time elapsed: 0.362 s % 289.43/41.92 % (2431125)Peak memory usage: 114 MB % 289.43/41.92 % (2431125)Instructions burned: 540 (million) % 289.43/41.92 % (2431130)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=3365401431:s2a=on:i=278:rtra=on:gtg=position_2607 on theBenchmark for (2607ds/278Mi) % 289.43/41.92 % (2431129)Instruction limit reached! % 289.43/41.92 % (2431129)------------------------------ % 289.43/41.92 % (2431129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.93/43.09 % (2431129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.93/43.09 % (2431129)CaDiCaL version: 2.1.3 % 297.93/43.09 % (2431129)Termination reason: Instruction limit % 297.93/43.09 % (2431129)Termination phase: Saturation % 297.93/43.09 % (2431129)Time elapsed: 0.130 s % 297.93/43.09 % (2431129)Peak memory usage: 89 MB % 297.93/43.09 % (2431129)Instructions burned: 238 (million) % 297.93/43.09 % (2431132)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=1689267331:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2605 on theBenchmark for (2605ds/258Mi) % 297.93/43.09 % (2431130)Instruction limit reached! % 297.93/43.09 % (2431130)------------------------------ % 297.93/43.09 % (2431130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.93/43.09 % (2431130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.93/43.09 % (2431130)CaDiCaL version: 2.1.3 % 297.93/43.09 % (2431130)Termination reason: Instruction limit % 297.93/43.09 % (2431130)Termination phase: Saturation % 297.93/43.09 % (2431130)Time elapsed: 0.162 s % 297.93/43.09 % (2431130)Peak memory usage: 91 MB % 297.93/43.09 % (2431130)Instructions burned: 279 (million) % 297.93/43.09 % (2431132)Refutation not found, incomplete strategy % 297.93/43.09 % (2431132)------------------------------ % 297.93/43.09 % (2431132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.93/43.09 % (2431132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.93/43.09 % (2431132)CaDiCaL version: 2.1.3 % 297.93/43.09 % (2431132)Termination reason: Refutation not found, incomplete strategy % 297.93/43.09 % (2431132)Time elapsed: 0.011 s % 297.93/43.09 % (2431132)Peak memory usage: 89 MB % 297.93/43.09 % (2431132)Instructions burned: 16 (million) % 297.93/43.09 % (2431134)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3835388881:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2605 on theBenchmark for (2605ds/570Mi) % 297.93/43.09 % (2431136)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=2023007529:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2604 on theBenchmark for (2604ds/314Mi) % 297.93/43.09 % (2431132)------------------------------ % 297.93/43.09 % (2431132)------------------------------ % 297.93/43.09 % (2431136)Instruction limit reached! % 297.93/43.09 % (2431136)------------------------------ % 297.93/43.09 % (2431136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.93/43.09 % (2431136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.93/43.09 % (2431136)CaDiCaL version: 2.1.3 % 297.93/43.09 % (2431136)Termination reason: Instruction limit % 297.93/43.09 % (2431136)Termination phase: Saturation % 297.93/43.09 % (2431136)Time elapsed: 0.179 s % 297.93/43.09 % (2431136)Peak memory usage: 91 MB % 297.93/43.09 % (2431136)Instructions burned: 314 (million) % 297.93/43.09 % (2431134)Instruction limit reached! % 297.93/43.09 % (2431134)------------------------------ % 297.93/43.09 % (2431134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.93/43.09 % (2431134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.93/43.09 % (2431134)CaDiCaL version: 2.1.3 % 297.93/43.09 % (2431134)Termination reason: Instruction limit % 297.93/43.09 % (2431134)Termination phase: Saturation % 297.93/43.09 % (2431134)Time elapsed: 0.326 s % 297.93/43.09 % (2431134)Peak memory usage: 93 MB % 297.93/43.09 % (2431134)Instructions burned: 571 (million) % 297.93/43.09 % (2431139)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1823393841:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2601 on theBenchmark for (2601ds/650Mi) % 297.93/43.09 % (2431140)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=3261767933:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2600 on theBenchmark for (2600ds/496Mi) % 297.93/43.09 % (2431141)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=47790869:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2600 on theBenchmark for (2600ds/588Mi) % 297.93/43.09 % (2431141)Refutation not found, incomplete strategy % 297.93/43.09 % (2431141)------------------------------ % 297.93/43.09 % (2431141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.93/43.09 % (2431141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.93/43.09 % (2431141)CaDiCaL version: 2.1.3 % 297.93/43.09 % (2431141)Termination reason: Refutation not found, incomplete strategy % 297.93/43.09 % (2431141)Time elapsed: 0.006 s % 297.93/43.09 % (2431141)Peak memory usage: 88 MB % 297.93/43.09 % (2431141)Instructions burned: 10 (million) % 297.93/43.09 % (2431141)------------------------------ % 300.41/43.53 Terminated %------------------------------------------------------------------------------