%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV625_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:19:07 PM UTC 2026 % Result : Timeout 297.97s 42.82s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV625_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.21 % Computer : n011.cluster.edu % 0.08/0.21 % Model : x86_64 x86_64 % 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.21 % Memory : 8046.5625MB % 0.08/0.21 % OS : Linux 6.8.0-71-generic % 0.08/0.21 % CPULimit : 300 % 0.08/0.21 % WCLimit : 300 % 0.08/0.21 % DateTime : Mon Sep 28 12:05:01 UTC 2026 % 0.08/0.21 % CPUTime : % 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.25 Running first-order theorem proving % 0.08/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.95/1.65 % (3347221)Detected formulas, will run a generic FOF schedule. % 4.95/1.65 % (3347230)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=801053387:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 4.95/1.65 % (3347230)Instruction limit reached! % 4.95/1.65 % (3347230)------------------------------ % 4.95/1.65 % (3347230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.95/1.65 % (3347230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.95/1.65 % (3347230)CaDiCaL version: 2.1.3 % 4.95/1.65 % (3347230)Termination reason: Instruction limit % 4.95/1.65 % (3347230)Termination phase: Saturation % 4.95/1.65 % (3347230)Time elapsed: 0.037 s % 4.95/1.65 % (3347230)Peak memory usage: 88 MB % 4.95/1.65 % (3347230)Instructions burned: 121 (million) % 4.95/1.65 % (3347227)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=2105765051:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 4.95/1.65 % (3347226)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=3666796048:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 4.95/1.65 % (3347228)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=1951486165:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 4.95/1.65 % (3347229)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=942206588:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 4.95/1.65 % (3347229)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.95/1.65 % (3347228)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.95/1.65 % (3347229)Refutation not found, incomplete strategy % 4.95/1.65 % (3347229)------------------------------ % 4.95/1.65 % (3347229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.95/1.65 % (3347229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.95/1.65 % (3347229)CaDiCaL version: 2.1.3 % 4.95/1.65 % (3347229)Termination reason: Refutation not found, incomplete strategy % 4.95/1.65 % (3347229)Time elapsed: 0.004 s % 4.95/1.65 % (3347229)Peak memory usage: 88 MB % 4.95/1.65 % (3347229)Instructions burned: 4 (million) % 4.95/1.65 % (3347232)dis-21_1_sil=8000:lcm=predicate:random_seed=1061093616: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) % 4.95/1.65 % (3347231)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2786007825:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 4.95/1.65 % (3347232)Instruction limit reached! % 4.95/1.65 % (3347232)------------------------------ % 4.95/1.65 % (3347232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.95/1.65 % (3347232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.95/1.65 % (3347232)CaDiCaL version: 2.1.3 % 4.95/1.65 % (3347232)Termination reason: Instruction limit % 4.95/1.65 % (3347232)Termination phase: Saturation % 4.95/1.65 % (3347232)Time elapsed: 0.074 s % 4.95/1.65 % (3347232)Peak memory usage: 89 MB % 4.95/1.65 % (3347232)Instructions burned: 130 (million) % 4.95/1.65 % (3347231)Instruction limit reached! % 4.95/1.65 % (3347231)------------------------------ % 4.95/1.65 % (3347231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.95/1.65 % (3347231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.95/1.65 % (3347231)CaDiCaL version: 2.1.3 % 4.95/1.65 % (3347231)Termination reason: Instruction limit % 4.95/1.65 % (3347231)Termination phase: Saturation % 4.95/1.65 % (3347231)Time elapsed: 0.089 s % 4.95/1.65 % (3347231)Peak memory usage: 90 MB % 4.95/1.65 % (3347231)Instructions burned: 140 (million) % 4.95/1.65 % (3347234)lrs+10_1_sil=8000:sp=occurrence:random_seed=3605907030:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 4.95/1.65 % (3347234)Instruction limit reached! % 4.95/1.65 % (3347234)------------------------------ % 4.95/1.65 % (3347234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.95/1.65 % (3347234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.95/1.65 % (3347234)CaDiCaL version: 2.1.3 % 7.34/1.88 % (3347234)Termination reason: Instruction limit % 7.34/1.88 % (3347234)Termination phase: Saturation % 7.34/1.88 % (3347234)Time elapsed: 0.088 s % 7.34/1.88 % (3347234)Peak memory usage: 91 MB % 7.34/1.88 % (3347234)Instructions burned: 288 (million) % 7.34/1.88 % (3347241)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1316693425:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 7.34/1.88 % (3347229)------------------------------ % 7.34/1.88 % (3347229)------------------------------ % 7.34/1.88 % (3347242)lrs+1011_1_sil=32000:sp=occurrence:random_seed=11690399:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 7.34/1.88 % (3347241)Instruction limit reached! % 7.34/1.88 % (3347241)------------------------------ % 7.34/1.88 % (3347241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.88 % (3347241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.88 % (3347241)CaDiCaL version: 2.1.3 % 7.34/1.88 % (3347241)Termination reason: Instruction limit % 7.34/1.88 % (3347241)Termination phase: Saturation % 7.34/1.88 % (3347241)Time elapsed: 0.084 s % 7.34/1.88 % (3347241)Peak memory usage: 89 MB % 7.34/1.88 % (3347241)Instructions burned: 159 (million) % 7.34/1.88 % (3347244)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=1956917133:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 7.34/1.88 % (3347228)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.34/1.88 % (3347226)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.34/1.88 % (3347227)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.34/1.88 % (3347226)------------------------------ % 7.34/1.88 % (3347226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.88 % (3347228)------------------------------ % 7.34/1.88 % (3347228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.88 % (3347227)------------------------------ % 7.34/1.88 % (3347227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.88 % (3347226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.88 % (3347228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.88 % (3347227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.88 % (3347228)CaDiCaL version: 2.1.3 % 7.34/1.88 % (3347227)CaDiCaL version: 2.1.3 % 7.34/1.88 % (3347226)CaDiCaL version: 2.1.3 % 7.34/1.88 % (3347227)Termination reason: Unknown % 7.34/1.88 % (3347227)Termination phase: Saturation % 7.34/1.88 % (3347226)Termination reason: Unknown % 7.34/1.88 % (3347226)Termination phase: Saturation % 7.34/1.88 % (3347228)Termination reason: Unknown % 7.34/1.88 % (3347228)Termination phase: Saturation % 7.34/1.88 % (3347227)Time elapsed: 0.365 s % 7.34/1.88 % (3347226)Time elapsed: 0.365 s % 7.34/1.88 % (3347228)Time elapsed: 0.365 s % 7.34/1.88 % (3347227)Peak memory usage: 112 MB % 7.34/1.88 % (3347226)Peak memory usage: 112 MB % 7.34/1.88 % (3347228)Peak memory usage: 111 MB % 7.34/1.88 % (3347226)Instructions burned: 544 (million) % 7.34/1.88 % (3347228)Instructions burned: 544 (million) % 7.34/1.88 % (3347227)Instructions burned: 549 (million) % 7.34/1.88 % (3347244)Instruction limit reached! % 7.34/1.88 % (3347244)------------------------------ % 7.34/1.88 % (3347244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.88 % (3347244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.88 % (3347244)CaDiCaL version: 2.1.3 % 7.34/1.88 % (3347244)Termination reason: Instruction limit % 7.34/1.88 % (3347244)Termination phase: Saturation % 7.34/1.88 % (3347244)Time elapsed: 0.079 s % 7.34/1.88 % (3347244)Peak memory usage: 90 MB % 7.34/1.88 % (3347244)Instructions burned: 250 (million) % 7.34/1.88 % (3347246)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1169632026:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 7.34/1.88 % (3347246)Refutation not found, incomplete strategy % 7.34/1.88 % (3347246)------------------------------ % 7.34/1.88 % (3347246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.34/1.88 % (3347246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.34/1.88 % (3347246)CaDiCaL version: 2.1.3 % 7.34/1.88 % (3347246)Termination reason: Refutation not found, incomplete strategy % 7.34/1.88 % (3347246)Time elapsed: 0.007 s % 7.34/1.88 % (3347246)Peak memory usage: 88 MB % 10.13/2.18 % (3347246)Instructions burned: 10 (million) % 10.13/2.18 % (3347242)Instruction limit reached! % 10.13/2.18 % (3347242)------------------------------ % 10.13/2.18 % (3347242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.13/2.18 % (3347242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.13/2.18 % (3347242)CaDiCaL version: 2.1.3 % 10.13/2.18 % (3347242)Termination reason: Instruction limit % 10.13/2.18 % (3347242)Termination phase: Saturation % 10.13/2.18 % (3347242)Time elapsed: 0.167 s % 10.13/2.18 % (3347242)Peak memory usage: 90 MB % 10.13/2.18 % (3347242)Instructions burned: 325 (million) % 10.13/2.18 % (3347249)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3622239098:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 10.13/2.18 % (3347250)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4000055984:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 10.13/2.18 % (3347252)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3242428475:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 10.13/2.18 % (3347251)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2349250765:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 10.13/2.18 % (3347253)lrs+10_1_sil=8000:sp=occurrence:random_seed=1728407615:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 10.13/2.18 % (3347252)Refutation not found, incomplete strategy % 10.13/2.18 % (3347252)------------------------------ % 10.13/2.18 % (3347252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.13/2.18 % (3347252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.13/2.18 % (3347252)CaDiCaL version: 2.1.3 % 10.13/2.18 % (3347252)Termination reason: Refutation not found, incomplete strategy % 10.13/2.18 % (3347252)Time elapsed: 0.005 s % 10.13/2.18 % (3347252)Peak memory usage: 88 MB % 10.13/2.18 % (3347252)Instructions burned: 7 (million) % 10.13/2.18 % (3347251)Refutation not found, incomplete strategy % 10.13/2.18 % (3347251)------------------------------ % 10.13/2.18 % (3347251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.13/2.18 % (3347251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.13/2.18 % (3347251)CaDiCaL version: 2.1.3 % 10.13/2.18 % (3347251)Termination reason: Refutation not found, incomplete strategy % 10.13/2.18 % (3347251)Time elapsed: 0.007 s % 10.13/2.18 % (3347251)Peak memory usage: 88 MB % 10.13/2.18 % (3347251)Instructions burned: 12 (million) % 10.13/2.18 % (3347250)Instruction limit reached! % 10.13/2.18 % (3347250)------------------------------ % 10.13/2.18 % (3347250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.13/2.18 % (3347250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.13/2.18 % (3347250)CaDiCaL version: 2.1.3 % 10.13/2.18 % (3347250)Termination reason: Instruction limit % 10.13/2.18 % (3347250)Termination phase: Saturation % 10.13/2.18 % (3347250)Time elapsed: 0.067 s % 10.13/2.18 % (3347250)Peak memory usage: 90 MB % 10.13/2.18 % (3347250)Instructions burned: 113 (million) % 10.13/2.18 % (3347255)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1252821341:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 10.13/2.18 % (3347255)Refutation not found, incomplete strategy % 10.13/2.18 % (3347255)------------------------------ % 10.13/2.18 % (3347255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.13/2.18 % (3347255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.13/2.18 % (3347255)CaDiCaL version: 2.1.3 % 10.13/2.18 % (3347255)Termination reason: Refutation not found, incomplete strategy % 10.13/2.18 % (3347255)Time elapsed: 0.008 s % 10.13/2.18 % (3347255)Peak memory usage: 88 MB % 10.13/2.18 % (3347255)Instructions burned: 13 (million) % 10.13/2.18 % (3347246)------------------------------ % 10.13/2.18 % (3347246)------------------------------ % 10.13/2.18 % (3347261)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1976864914:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 10.13/2.18 % (3347252)------------------------------ % 10.13/2.18 % (3347252)------------------------------ % 10.13/2.18 % (3347251)------------------------------ % 10.13/2.18 % (3347251)------------------------------ % 10.13/2.18 % (3347253)Instruction limit reached! % 10.13/2.18 % (3347253)------------------------------ % 11.16/2.44 % (3347253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.16/2.44 % (3347253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.16/2.44 % (3347253)CaDiCaL version: 2.1.3 % 11.16/2.44 % (3347253)Termination reason: Instruction limit % 11.16/2.44 % (3347253)Termination phase: Saturation % 11.16/2.44 % (3347253)Time elapsed: 0.275 s % 11.16/2.44 % (3347253)Peak memory usage: 96 MB % 11.16/2.44 % (3347253)Instructions burned: 909 (million) % 11.16/2.44 % (3347249)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.16/2.44 % (3347249)------------------------------ % 11.16/2.44 % (3347249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.16/2.44 % (3347249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.16/2.44 % (3347249)CaDiCaL version: 2.1.3 % 11.16/2.44 % (3347249)Termination reason: Unknown % 11.16/2.44 % (3347249)Termination phase: Saturation % 11.16/2.44 % (3347249)Time elapsed: 0.371 s % 11.16/2.44 % (3347249)Peak memory usage: 114 MB % 11.16/2.44 % (3347249)Instructions burned: 543 (million) % 11.16/2.44 % (3347263)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3412089950:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi) % 11.16/2.44 % (3347255)------------------------------ % 11.16/2.44 % (3347255)------------------------------ % 11.16/2.44 % (3347267)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=3096199064:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 11.16/2.44 % (3347267)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.16/2.44 % (3347265)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2774023392:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi) % 11.16/2.44 % (3347266)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=646585424:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi) % 11.16/2.44 % (3347265)Refutation not found, incomplete strategy % 11.16/2.44 % (3347265)------------------------------ % 11.16/2.44 % (3347265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.16/2.44 % (3347265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.16/2.44 % (3347265)CaDiCaL version: 2.1.3 % 11.16/2.44 % (3347265)Termination reason: Refutation not found, incomplete strategy % 11.16/2.44 % (3347265)Time elapsed: 0.007 s % 11.16/2.44 % (3347265)Peak memory usage: 88 MB % 11.16/2.44 % (3347265)Instructions burned: 13 (million) % 11.16/2.44 % (3347263)Instruction limit reached! % 11.16/2.44 % (3347263)------------------------------ % 11.16/2.44 % (3347263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.16/2.44 % (3347263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.16/2.44 % (3347263)CaDiCaL version: 2.1.3 % 11.16/2.44 % (3347263)Termination reason: Instruction limit % 11.16/2.44 % (3347263)Termination phase: Saturation % 11.16/2.44 % (3347263)Time elapsed: 0.077 s % 11.16/2.44 % (3347263)Peak memory usage: 90 MB % 11.16/2.44 % (3347263)Instructions burned: 136 (million) % 11.16/2.44 % (3347267)Instruction limit reached! % 11.16/2.44 % (3347267)------------------------------ % 11.16/2.44 % (3347267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.16/2.44 % (3347267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.16/2.44 % (3347267)CaDiCaL version: 2.1.3 % 11.16/2.44 % (3347267)Termination reason: Instruction limit % 11.16/2.44 % (3347267)Termination phase: Saturation % 11.16/2.44 % (3347267)Time elapsed: 0.041 s % 11.16/2.44 % (3347267)Peak memory usage: 90 MB % 11.16/2.44 % (3347267)Instructions burned: 128 (million) % 11.16/2.44 % (3347268)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=536309234:i=134:gtgl=5:slsql=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/134Mi) % 11.16/2.44 % (3347270)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=320607079:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi) % 11.16/2.44 % (3347270)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.16/2.44 % (3347270)Refutation not found, incomplete strategy % 11.16/2.44 % (3347270)------------------------------ % 11.16/2.44 % (3347270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.71 % (3347270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.71 % (3347270)CaDiCaL version: 2.1.3 % 13.02/2.71 % (3347270)Termination reason: Refutation not found, incomplete strategy % 13.02/2.71 % (3347270)Time elapsed: 0.003 s % 13.02/2.71 % (3347270)Peak memory usage: 88 MB % 13.02/2.71 % (3347270)Instructions burned: 2 (million) % 13.02/2.71 % (3347268)Instruction limit reached! % 13.02/2.71 % (3347268)------------------------------ % 13.02/2.71 % (3347268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.71 % (3347275)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=128039813:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi) % 13.02/2.71 % (3347268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.71 % (3347268)CaDiCaL version: 2.1.3 % 13.02/2.71 % (3347268)Termination reason: Instruction limit % 13.02/2.71 % (3347268)Termination phase: Saturation % 13.02/2.71 % (3347268)Time elapsed: 0.074 s % 13.02/2.71 % (3347268)Peak memory usage: 90 MB % 13.02/2.71 % (3347268)Instructions burned: 134 (million) % 13.02/2.71 % (3347274)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1041477905:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/431Mi) % 13.02/2.71 % (3347261)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.02/2.71 % (3347261)------------------------------ % 13.02/2.71 % (3347261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.71 % (3347261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.71 % (3347261)CaDiCaL version: 2.1.3 % 13.02/2.71 % (3347261)Termination reason: Unknown % 13.02/2.71 % (3347261)Termination phase: Saturation % 13.02/2.71 % (3347261)Time elapsed: 0.370 s % 13.02/2.71 % (3347261)Peak memory usage: 114 MB % 13.02/2.71 % (3347261)Instructions burned: 544 (million) % 13.02/2.71 % (3347265)------------------------------ % 13.02/2.71 % (3347265)------------------------------ % 13.02/2.71 % (3347280)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=178610215:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2987 on theBenchmark for (2987ds/150Mi) % 13.02/2.71 % (3347280)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.02/2.71 % (3347275)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.02/2.71 % (3347275)------------------------------ % 13.02/2.71 % (3347275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.71 % (3347275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.71 % (3347275)CaDiCaL version: 2.1.3 % 13.02/2.71 % (3347275)Termination reason: Unknown % 13.02/2.71 % (3347275)Termination phase: Saturation % 13.02/2.71 % (3347275)Time elapsed: 0.199 s % 13.02/2.71 % (3347275)Peak memory usage: 114 MB % 13.02/2.71 % (3347275)Instructions burned: 543 (million) % 13.02/2.71 % (3347270)------------------------------ % 13.02/2.71 % (3347270)------------------------------ % 13.02/2.71 % (3347266)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.02/2.71 % (3347266)------------------------------ % 13.02/2.71 % (3347266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.71 % (3347266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.71 % (3347266)CaDiCaL version: 2.1.3 % 13.02/2.71 % (3347266)Termination reason: Unknown % 13.02/2.71 % (3347266)Termination phase: Saturation % 13.02/2.71 % (3347266)Time elapsed: 0.369 s % 13.02/2.71 % (3347266)Peak memory usage: 114 MB % 13.02/2.71 % (3347266)Instructions burned: 543 (million) % 13.02/2.71 % (3347281)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1566708416:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi) % 13.02/2.71 % (3347274)Instruction limit reached! % 13.02/2.71 % (3347274)------------------------------ % 13.02/2.71 % (3347274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.02/2.71 % (3347274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.02/2.71 % (3347274)CaDiCaL version: 2.1.3 % 13.02/2.71 % (3347274)Termination reason: Instruction limit % 13.02/2.71 % (3347274)Termination phase: Saturation % 17.82/3.25 % (3347274)Time elapsed: 0.247 s % 17.82/3.25 % (3347274)Peak memory usage: 93 MB % 17.82/3.25 % (3347274)Instructions burned: 432 (million) % 17.82/3.25 % (3347282)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1600679657:i=667:av=off:fsr=off_2986 on theBenchmark for (2986ds/667Mi) % 17.82/3.25 % (3347282)Refutation not found, incomplete strategy % 17.82/3.25 % (3347282)------------------------------ % 17.82/3.25 % (3347282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.25 % (3347282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.25 % (3347282)CaDiCaL version: 2.1.3 % 17.82/3.25 % (3347282)Termination reason: Refutation not found, incomplete strategy % 17.82/3.25 % (3347282)Time elapsed: 0.008 s % 17.82/3.25 % (3347282)Peak memory usage: 88 MB % 17.82/3.25 % (3347282)Instructions burned: 13 (million) % 17.82/3.25 % (3347280)Instruction limit reached! % 17.82/3.25 % (3347280)------------------------------ % 17.82/3.25 % (3347280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.25 % (3347280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.25 % (3347280)CaDiCaL version: 2.1.3 % 17.82/3.25 % (3347280)Termination reason: Instruction limit % 17.82/3.25 % (3347280)Termination phase: Saturation % 17.82/3.25 % (3347280)Time elapsed: 0.102 s % 17.82/3.25 % (3347280)Peak memory usage: 91 MB % 17.82/3.25 % (3347280)Instructions burned: 151 (million) % 17.82/3.25 % (3347284)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=4152531531:s2a=on:i=185:s2at=1.8:fdi=4_2985 on theBenchmark for (2985ds/185Mi) % 17.82/3.25 % (3347287)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=548984972:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi) % 17.82/3.25 % (3347285)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=376884125:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2985 on theBenchmark for (2985ds/193Mi) % 17.82/3.25 % (3347287)Refutation not found, incomplete strategy % 17.82/3.25 % (3347287)------------------------------ % 17.82/3.25 % (3347287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.25 % (3347287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.25 % (3347287)CaDiCaL version: 2.1.3 % 17.82/3.25 % (3347287)Termination reason: Refutation not found, incomplete strategy % 17.82/3.25 % (3347287)Time elapsed: 0.006 s % 17.82/3.25 % (3347287)Peak memory usage: 88 MB % 17.82/3.25 % (3347287)Instructions burned: 10 (million) % 17.82/3.25 % (3347284)Instruction limit reached! % 17.82/3.25 % (3347284)------------------------------ % 17.82/3.25 % (3347284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.25 % (3347284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.25 % (3347284)CaDiCaL version: 2.1.3 % 17.82/3.25 % (3347284)Termination reason: Instruction limit % 17.82/3.25 % (3347284)Termination phase: Saturation % 17.82/3.25 % (3347284)Time elapsed: 0.068 s % 17.82/3.25 % (3347284)Peak memory usage: 91 MB % 17.82/3.25 % (3347284)Instructions burned: 186 (million) % 17.82/3.25 % (3347289)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=881073109:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi) % 17.82/3.25 % (3347290)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3229712230:i=319:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/319Mi) % 17.82/3.25 % (3347285)Instruction limit reached! % 17.82/3.25 % (3347285)------------------------------ % 17.82/3.25 % (3347285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.82/3.25 % (3347285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.82/3.25 % (3347285)CaDiCaL version: 2.1.3 % 17.82/3.25 % (3347285)Termination reason: Instruction limit % 17.82/3.25 % (3347285)Termination phase: Saturation % 17.82/3.25 % (3347285)Time elapsed: 0.112 s % 17.82/3.25 % (3347285)Peak memory usage: 90 MB % 17.82/3.25 % (3347285)Instructions burned: 195 (million) % 17.82/3.25 % (3347282)------------------------------ % 17.82/3.25 % (3347282)------------------------------ % 17.82/3.25 % (3347294)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2817535746:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi) % 17.82/3.25 % (3347294)Refutation not found, incomplete strategy % 19.79/3.78 % (3347294)------------------------------ % 19.79/3.78 % (3347294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.79/3.78 % (3347294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.79/3.78 % (3347294)CaDiCaL version: 2.1.3 % 19.79/3.78 % (3347294)Termination reason: Refutation not found, incomplete strategy % 19.79/3.78 % (3347294)Time elapsed: 0.004 s % 19.79/3.78 % (3347294)Peak memory usage: 88 MB % 19.79/3.78 % (3347294)Instructions burned: 12 (million) % 19.79/3.78 % (3347281)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.79/3.78 % (3347281)------------------------------ % 19.79/3.78 % (3347281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.79/3.78 % (3347281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.79/3.78 % (3347281)CaDiCaL version: 2.1.3 % 19.79/3.78 % (3347281)Termination reason: Unknown % 19.79/3.78 % (3347281)Termination phase: Saturation % 19.79/3.78 % (3347281)Time elapsed: 0.372 s % 19.79/3.78 % (3347281)Peak memory usage: 114 MB % 19.79/3.78 % (3347281)Instructions burned: 543 (million) % 19.79/3.78 % (3347290)Instruction limit reached! % 19.79/3.78 % (3347290)------------------------------ % 19.79/3.78 % (3347290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.79/3.78 % (3347290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.79/3.78 % (3347290)CaDiCaL version: 2.1.3 % 19.79/3.78 % (3347290)Termination reason: Instruction limit % 19.79/3.78 % (3347290)Termination phase: Saturation % 19.79/3.78 % (3347290)Time elapsed: 0.193 s % 19.79/3.78 % (3347290)Peak memory usage: 93 MB % 19.79/3.78 % (3347290)Instructions burned: 319 (million) % 19.79/3.78 % (3347287)------------------------------ % 19.79/3.78 % (3347287)------------------------------ % 19.79/3.78 % (3347297)dis-1011_128_sil=32000:random_seed=4272077839:i=3706:ep=RST:av=off_2982 on theBenchmark for (2982ds/3706Mi) % 19.79/3.78 % (3347299)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4188908096:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2982 on theBenchmark for (2982ds/757Mi) % 19.79/3.78 % (3347294)------------------------------ % 19.79/3.78 % (3347294)------------------------------ % 19.79/3.78 % (3347299)Refutation not found, incomplete strategy % 19.79/3.78 % (3347299)------------------------------ % 19.79/3.78 % (3347299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.79/3.78 % (3347299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.79/3.78 % (3347299)CaDiCaL version: 2.1.3 % 19.79/3.78 % (3347299)Termination reason: Refutation not found, incomplete strategy % 19.79/3.78 % (3347299)Time elapsed: 0.009 s % 19.79/3.78 % (3347299)Peak memory usage: 89 MB % 19.79/3.78 % (3347299)Instructions burned: 13 (million) % 19.79/3.78 % (3347300)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4113648339:i=13913:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/13913Mi) % 19.79/3.78 % (3347301)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3553752990:i=9925:aac=none_2981 on theBenchmark for (2981ds/9925Mi) % 19.79/3.78 % (3347302)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1346965321:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 19.79/3.78 % (3347302)Refutation not found, incomplete strategy % 19.79/3.78 % (3347302)------------------------------ % 19.79/3.78 % (3347302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.79/3.78 % (3347302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.79/3.78 % (3347302)CaDiCaL version: 2.1.3 % 19.79/3.78 % (3347302)Termination reason: Refutation not found, incomplete strategy % 19.79/3.78 % (3347302)Time elapsed: 0.005 s % 19.79/3.78 % (3347302)Peak memory usage: 88 MB % 19.79/3.78 % (3347302)Instructions burned: 7 (million) % 19.79/3.78 % (3347305)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=139459223:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/440Mi) % 19.79/3.78 % (3347289)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.79/3.78 % (3347289)------------------------------ % 19.79/3.78 % (3347289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.79/3.78 % (3347289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.32 % (3347289)CaDiCaL version: 2.1.3 % 25.52/4.32 % (3347289)Termination reason: Unknown % 25.52/4.32 % (3347289)Termination phase: Saturation % 25.52/4.32 % (3347289)Time elapsed: 0.373 s % 25.52/4.32 % (3347289)Peak memory usage: 114 MB % 25.52/4.32 % (3347289)Instructions burned: 543 (million) % 25.52/4.32 % (3347305)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 25.52/4.32 % (3347305)Instruction limit reached! % 25.52/4.32 % (3347305)------------------------------ % 25.52/4.32 % (3347305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.52/4.32 % (3347305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.32 % (3347305)CaDiCaL version: 2.1.3 % 25.52/4.32 % (3347305)Termination reason: Instruction limit % 25.52/4.32 % (3347305)Termination phase: Saturation % 25.52/4.32 % (3347305)Time elapsed: 0.120 s % 25.52/4.32 % (3347305)Peak memory usage: 92 MB % 25.52/4.32 % (3347305)Instructions burned: 444 (million) % 25.52/4.32 % (3347299)------------------------------ % 25.52/4.32 % (3347299)------------------------------ % 25.52/4.32 % (3347310)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=871265288:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi) % 25.52/4.32 % (3347302)------------------------------ % 25.52/4.32 % (3347302)------------------------------ % 25.52/4.32 % (3347311)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=277039338:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi) % 25.52/4.32 % (3347312)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2276046682:st=2:s2a=on:i=524:s2at=2:ss=axioms_2978 on theBenchmark for (2978ds/524Mi) % 25.52/4.32 % (3347300)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.52/4.32 % (3347300)------------------------------ % 25.52/4.32 % (3347300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.52/4.32 % (3347300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.32 % (3347300)CaDiCaL version: 2.1.3 % 25.52/4.32 % (3347300)Termination reason: Unknown % 25.52/4.32 % (3347300)Termination phase: Saturation % 25.52/4.32 % (3347300)Time elapsed: 0.364 s % 25.52/4.32 % (3347300)Peak memory usage: 113 MB % 25.52/4.32 % (3347300)Instructions burned: 541 (million) % 25.52/4.32 % (3347301)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.52/4.32 % (3347301)------------------------------ % 25.52/4.32 % (3347301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.52/4.32 % (3347301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.32 % (3347301)CaDiCaL version: 2.1.3 % 25.52/4.32 % (3347301)Termination reason: Unknown % 25.52/4.32 % (3347301)Termination phase: Saturation % 25.52/4.32 % (3347301)Time elapsed: 0.365 s % 25.52/4.32 % (3347301)Peak memory usage: 114 MB % 25.52/4.32 % (3347301)Instructions burned: 543 (million) % 25.52/4.32 % (3347315)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3781335545:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2977 on theBenchmark for (2977ds/1016Mi) % 25.52/4.32 % (3347311)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.52/4.32 % (3347311)------------------------------ % 25.52/4.32 % (3347311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.52/4.32 % (3347311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.52/4.32 % (3347311)CaDiCaL version: 2.1.3 % 25.52/4.32 % (3347311)Termination reason: Unknown % 25.52/4.32 % (3347311)Termination phase: Saturation % 25.52/4.32 % (3347311)Time elapsed: 0.197 s % 25.52/4.32 % (3347311)Peak memory usage: 113 MB % 25.52/4.32 % (3347311)Instructions burned: 543 (million) % 25.52/4.32 % (3347317)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2813836969:i=14123:bd=preordered:ins=4_2976 on theBenchmark for (2976ds/14123Mi) % 25.52/4.32 % (3347318)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3297875429:i=5781:kws=precedence:bd=all:rawr=on_2976 on theBenchmark for (2976ds/5781Mi) % 25.52/4.32 % (3347310)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.52/4.32 % (3347310)------------------------------ % 25.52/4.32 % (3347310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.16/5.02 % (3347310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.16/5.02 % (3347310)CaDiCaL version: 2.1.3 % 28.16/5.02 % (3347310)Termination reason: Unknown % 28.16/5.02 % (3347310)Termination phase: Saturation % 28.16/5.02 % (3347310)Time elapsed: 0.367 s % 28.16/5.02 % (3347310)Peak memory usage: 113 MB % 28.16/5.02 % (3347310)Instructions burned: 542 (million) % 28.16/5.02 % (3347320)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=1954633820:i=2448:gtgl=5:bd=preordered:gtg=all_2975 on theBenchmark for (2975ds/2448Mi) % 28.16/5.02 % (3347312)Instruction limit reached! % 28.16/5.02 % (3347312)------------------------------ % 28.16/5.02 % (3347312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.16/5.02 % (3347312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.16/5.02 % (3347312)CaDiCaL version: 2.1.3 % 28.16/5.02 % (3347312)Termination reason: Instruction limit % 28.16/5.02 % (3347312)Termination phase: Saturation % 28.16/5.02 % (3347312)Time elapsed: 0.292 s % 28.16/5.03 % (3347312)Peak memory usage: 92 MB % 28.16/5.03 % (3347312)Instructions burned: 526 (million) % 28.16/5.03 % (3347323)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3427235754:i=3223:kws=precedence:fgj=on:av=off_2974 on theBenchmark for (2974ds/3223Mi) % 28.16/5.03 % (3347325)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2866402382:st=5.6:i=2033:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/2033Mi) % 28.16/5.03 % (3347320)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 28.16/5.03 % (3347320)------------------------------ % 28.16/5.03 % (3347320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.16/5.03 % (3347320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.16/5.03 % (3347320)CaDiCaL version: 2.1.3 % 28.16/5.03 % (3347320)Termination reason: Unknown % 28.16/5.03 % (3347320)Termination phase: Saturation % 28.16/5.03 % (3347320)Time elapsed: 0.198 s % 28.16/5.03 % (3347320)Peak memory usage: 114 MB % 28.16/5.03 % (3347320)Instructions burned: 545 (million) % 28.16/5.03 % (3347317)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 28.16/5.03 % (3347317)------------------------------ % 28.16/5.03 % (3347317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.16/5.03 % (3347317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.16/5.03 % (3347317)CaDiCaL version: 2.1.3 % 28.16/5.03 % (3347317)Termination reason: Unknown % 28.16/5.03 % (3347317)Termination phase: Saturation % 28.16/5.03 % (3347317)Time elapsed: 0.363 s % 28.16/5.03 % (3347317)Peak memory usage: 113 MB % 28.16/5.03 % (3347317)Instructions burned: 542 (million) % 28.16/5.03 % (3347328)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4255419037:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2972 on theBenchmark for (2972ds/2055Mi) % 28.16/5.03 % (3347315)Instruction limit reached! % 28.16/5.03 % (3347315)------------------------------ % 28.16/5.03 % (3347315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.16/5.03 % (3347315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.16/5.03 % (3347315)CaDiCaL version: 2.1.3 % 28.16/5.03 % (3347315)Termination reason: Instruction limit % 28.16/5.03 % (3347315)Termination phase: Saturation % 28.16/5.03 % (3347315)Time elapsed: 0.491 s % 28.16/5.03 % (3347315)Peak memory usage: 92 MB % 28.16/5.03 % (3347315)Instructions burned: 1017 (million) % 28.16/5.03 % (3347329)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=1720339209:i=21611:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/21611Mi) % 28.16/5.03 % (3347331)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=954681615:i=4835:sd=13:ss=axioms:sgt=23_2971 on theBenchmark for (2971ds/4835Mi) % 28.16/5.03 % (3347323)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 28.16/5.03 % (3347323)------------------------------ % 28.16/5.03 % (3347323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.16/5.03 % (3347323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.16/5.03 % (3347323)CaDiCaL version: 2.1.3 % 28.16/5.03 % (3347323)Termination reason: Unknown % 28.16/5.03 % (3347323)Termination phase: Saturation % 34.91/5.79 % (3347323)Time elapsed: 0.363 s % 34.91/5.79 % (3347323)Peak memory usage: 114 MB % 34.91/5.79 % (3347323)Instructions burned: 543 (million) % 34.91/5.79 % (3347328)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.91/5.79 % (3347328)------------------------------ % 34.91/5.79 % (3347328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.91/5.79 % (3347328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.91/5.79 % (3347328)CaDiCaL version: 2.1.3 % 34.91/5.79 % (3347328)Termination reason: Unknown % 34.91/5.79 % (3347328)Termination phase: Saturation % 34.91/5.79 % (3347328)Time elapsed: 0.196 s % 34.91/5.79 % (3347328)Peak memory usage: 113 MB % 34.91/5.79 % (3347328)Instructions burned: 540 (million) % 34.91/5.79 % (3347325)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.91/5.79 % (3347325)------------------------------ % 34.91/5.79 % (3347325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.91/5.79 % (3347325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.91/5.79 % (3347325)CaDiCaL version: 2.1.3 % 34.91/5.79 % (3347325)Termination reason: Unknown % 34.91/5.79 % (3347325)Termination phase: Saturation % 34.91/5.79 % (3347325)Time elapsed: 0.361 s % 34.91/5.79 % (3347325)Peak memory usage: 114 MB % 34.91/5.79 % (3347325)Instructions burned: 544 (million) % 34.91/5.79 % (3347335)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1158341752:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2969 on theBenchmark for (2969ds/2326Mi) % 34.91/5.79 % (3347335)Refutation not found, incomplete strategy % 34.91/5.79 % (3347335)------------------------------ % 34.91/5.79 % (3347335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.91/5.79 % (3347335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.91/5.79 % (3347335)CaDiCaL version: 2.1.3 % 34.91/5.79 % (3347335)Termination reason: Refutation not found, incomplete strategy % 34.91/5.79 % (3347335)Time elapsed: 0.006 s % 34.91/5.79 % (3347335)Peak memory usage: 89 MB % 34.91/5.79 % (3347335)Instructions burned: 17 (million) % 34.91/5.79 % (3347334)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=3103862253:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2969 on theBenchmark for (2969ds/797Mi) % 34.91/5.79 % (3347336)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=4075701434:i=6038:nm=6_2968 on theBenchmark for (2968ds/6038Mi) % 34.91/5.79 % (3347335)------------------------------ % 34.91/5.79 % (3347335)------------------------------ % 34.91/5.79 % (3347329)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.91/5.79 % (3347329)------------------------------ % 34.91/5.79 % (3347329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.91/5.79 % (3347329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.91/5.79 % (3347329)CaDiCaL version: 2.1.3 % 34.91/5.79 % (3347329)Termination reason: Unknown % 34.91/5.79 % (3347329)Termination phase: Saturation % 34.91/5.79 % (3347329)Time elapsed: 0.364 s % 34.91/5.79 % (3347329)Peak memory usage: 113 MB % 34.91/5.79 % (3347329)Instructions burned: 539 (million) % 34.91/5.79 % (3347340)lrs+10_1_sil=32000:sp=occurrence:random_seed=4058939650:st=2:i=33334:sd=3:ss=included:sgt=32_2966 on theBenchmark for (2966ds/33334Mi) % 34.91/5.79 % (3347341)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2656992979:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2966 on theBenchmark for (2966ds/1008Mi) % 34.91/5.79 % (3347336)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.91/5.79 % (3347336)------------------------------ % 34.91/5.79 % (3347336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.91/5.79 % (3347336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.91/5.79 % (3347336)CaDiCaL version: 2.1.3 % 34.91/5.79 % (3347336)Termination reason: Unknown % 34.91/5.79 % (3347336)Termination phase: Saturation % 34.91/5.79 % (3347336)Time elapsed: 0.358 s % 34.91/5.79 % (3347336)Peak memory usage: 114 MB % 34.91/5.79 % (3347336)Instructions burned: 542 (million) % 34.91/5.79 % (3347297)Instruction limit reached! % 34.91/5.79 % (3347297)------------------------------ % 39.88/6.33 % (3347297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.88/6.33 % (3347297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.88/6.33 % (3347297)CaDiCaL version: 2.1.3 % 39.88/6.33 % (3347297)Termination reason: Instruction limit % 39.88/6.33 % (3347297)Termination phase: Saturation % 39.88/6.33 % (3347297)Time elapsed: 1.765 s % 39.88/6.33 % (3347297)Peak memory usage: 100 MB % 39.88/6.33 % (3347297)Instructions burned: 3707 (million) % 39.88/6.33 % (3347334)Instruction limit reached! % 39.88/6.33 % (3347334)------------------------------ % 39.88/6.33 % (3347334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.88/6.33 % (3347334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.88/6.33 % (3347334)CaDiCaL version: 2.1.3 % 39.88/6.33 % (3347334)Termination reason: Instruction limit % 39.88/6.33 % (3347334)Termination phase: Saturation % 39.88/6.33 % (3347334)Time elapsed: 0.470 s % 39.88/6.33 % (3347334)Peak memory usage: 98 MB % 39.88/6.33 % (3347334)Instructions burned: 797 (million) % 39.88/6.33 % (3347344)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=3349701167:i=8327:s2at=5:bd=preordered_2963 on theBenchmark for (2963ds/8327Mi) % 39.88/6.33 % (3347345)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=1112239995:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2963 on theBenchmark for (2963ds/1083Mi) % 39.88/6.33 % (3347346)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1575831479:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2962 on theBenchmark for (2962ds/1084Mi) % 39.88/6.33 % (3347341)Instruction limit reached! % 39.88/6.33 % (3347341)------------------------------ % 39.88/6.33 % (3347341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.88/6.33 % (3347341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.88/6.33 % (3347341)CaDiCaL version: 2.1.3 % 39.88/6.33 % (3347341)Termination reason: Instruction limit % 39.88/6.33 % (3347341)Termination phase: Saturation % 39.88/6.33 % (3347341)Time elapsed: 0.519 s % 39.88/6.33 % (3347341)Peak memory usage: 96 MB % 39.88/6.33 % (3347341)Instructions burned: 1010 (million) % 39.88/6.33 % (3347344)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.88/6.33 % (3347344)------------------------------ % 39.88/6.33 % (3347344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.88/6.33 % (3347344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.88/6.33 % (3347344)CaDiCaL version: 2.1.3 % 39.88/6.33 % (3347344)Termination reason: Unknown % 39.88/6.33 % (3347344)Termination phase: Saturation % 39.88/6.33 % (3347344)Time elapsed: 0.360 s % 39.88/6.33 % (3347344)Peak memory usage: 113 MB % 39.88/6.33 % (3347344)Instructions burned: 543 (million) % 39.88/6.33 % (3347350)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4134457827:i=6995:s2at=5:gtg=all_2959 on theBenchmark for (2959ds/6995Mi) % 39.88/6.33 % (3347351)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1438543261:st=2:i=6225:sd=15:ss=axioms_2958 on theBenchmark for (2958ds/6225Mi) % 39.88/6.33 % (3347351)Refutation not found, incomplete strategy % 39.88/6.33 % (3347351)------------------------------ % 39.88/6.33 % (3347351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.88/6.33 % (3347351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.88/6.33 % (3347351)CaDiCaL version: 2.1.3 % 39.88/6.33 % (3347351)Termination reason: Refutation not found, incomplete strategy % 39.88/6.33 % (3347351)Time elapsed: 0.009 s % 39.88/6.33 % (3347351)Peak memory usage: 88 MB % 39.88/6.33 % (3347351)Instructions burned: 13 (million) % 39.88/6.33 % (3347345)Instruction limit reached! % 39.88/6.33 % (3347345)------------------------------ % 39.88/6.33 % (3347345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.88/6.33 % (3347345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.88/6.33 % (3347345)CaDiCaL version: 2.1.3 % 39.88/6.33 % (3347345)Termination reason: Instruction limit % 39.88/6.33 % (3347345)Termination phase: Saturation % 39.88/6.33 % (3347345)Time elapsed: 0.553 s % 39.88/6.33 % (3347345)Peak memory usage: 96 MB % 42.42/6.85 % (3347345)Instructions burned: 1083 (million) % 42.42/6.85 % (3347346)Instruction limit reached! % 42.42/6.85 % (3347346)------------------------------ % 42.42/6.85 % (3347346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.42/6.85 % (3347346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.42/6.85 % (3347346)CaDiCaL version: 2.1.3 % 42.42/6.85 % (3347346)Termination reason: Instruction limit % 42.42/6.85 % (3347346)Termination phase: Saturation % 42.42/6.85 % (3347346)Time elapsed: 0.572 s % 42.42/6.85 % (3347346)Peak memory usage: 96 MB % 42.42/6.85 % (3347346)Instructions burned: 1085 (million) % 42.42/6.85 % (3347354)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3713283584:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2956 on theBenchmark for (2956ds/3372Mi) % 42.42/6.85 % (3347351)------------------------------ % 42.42/6.85 % (3347351)------------------------------ % 42.42/6.85 % (3347350)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 42.42/6.85 % (3347350)------------------------------ % 42.42/6.85 % (3347350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.42/6.85 % (3347350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.42/6.85 % (3347350)CaDiCaL version: 2.1.3 % 42.42/6.85 % (3347350)Termination reason: Unknown % 42.42/6.85 % (3347350)Termination phase: Saturation % 42.42/6.85 % (3347350)Time elapsed: 0.364 s % 42.42/6.85 % (3347350)Peak memory usage: 114 MB % 42.42/6.85 % (3347350)Instructions burned: 546 (million) % 42.42/6.85 % (3347355)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3435493096:st=2.3:i=26457:sd=10:ss=included:sgt=8_2955 on theBenchmark for (2955ds/26457Mi) % 42.42/6.85 % (3347357)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=935132965:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2954 on theBenchmark for (2954ds/13494Mi) % 42.42/6.85 % (3347358)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=493198158:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2954 on theBenchmark for (2954ds/2503Mi) % 42.42/6.85 % (3347358)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 42.42/6.85 % (3347354)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 42.42/6.85 % (3347354)------------------------------ % 42.42/6.85 % (3347354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.42/6.85 % (3347354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.42/6.85 % (3347354)CaDiCaL version: 2.1.3 % 42.42/6.85 % (3347354)Termination reason: Unknown % 42.42/6.85 % (3347354)Termination phase: Saturation % 42.42/6.85 % (3347354)Time elapsed: 0.361 s % 42.42/6.85 % (3347354)Peak memory usage: 113 MB % 42.42/6.85 % (3347354)Instructions burned: 539 (million) % 42.42/6.85 % (3347355)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 42.42/6.85 % (3347355)------------------------------ % 42.42/6.85 % (3347355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.42/6.85 % (3347355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.42/6.85 % (3347355)CaDiCaL version: 2.1.3 % 42.42/6.85 % (3347355)Termination reason: Unknown % 42.42/6.85 % (3347355)Termination phase: Saturation % 42.42/6.85 % (3347355)Time elapsed: 0.363 s % 42.42/6.85 % (3347355)Peak memory usage: 114 MB % 42.42/6.85 % (3347355)Instructions burned: 543 (million) % 42.42/6.85 % (3347362)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1048493133:i=2559:sd=1:ep=RSTC:ss=axioms_2951 on theBenchmark for (2951ds/2559Mi) % 42.42/6.85 % (3347357)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 42.42/6.85 % (3347357)------------------------------ % 42.42/6.85 % (3347357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.42/6.85 % (3347357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.42/6.85 % (3347357)CaDiCaL version: 2.1.3 % 42.42/6.85 % (3347357)Termination reason: Unknown % 42.42/6.85 % (3347357)Termination phase: Saturation % 42.42/6.85 % (3347357)Time elapsed: 0.361 s % 42.42/6.85 % (3347357)Peak memory usage: 114 MB % 42.42/6.85 % (3347357)Instructions burned: 545 (million) % 42.42/6.85 % (3347318)Instruction limit reached! % 47.65/7.50 % (3347318)------------------------------ % 47.65/7.50 % (3347318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.65/7.50 % (3347318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.65/7.50 % (3347318)CaDiCaL version: 2.1.3 % 47.65/7.50 % (3347318)Termination reason: Instruction limit % 47.65/7.50 % (3347318)Termination phase: Saturation % 47.65/7.50 % (3347318)Time elapsed: 2.596 s % 47.65/7.50 % (3347318)Peak memory usage: 118 MB % 47.65/7.50 % (3347318)Instructions burned: 5782 (million) % 47.65/7.50 % (3347358)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.65/7.50 % (3347358)------------------------------ % 47.65/7.50 % (3347358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.65/7.50 % (3347358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.65/7.50 % (3347358)CaDiCaL version: 2.1.3 % 47.65/7.50 % (3347358)Termination reason: Unknown % 47.65/7.50 % (3347358)Termination phase: Saturation % 47.65/7.50 % (3347358)Time elapsed: 0.361 s % 47.65/7.50 % (3347358)Peak memory usage: 113 MB % 47.65/7.50 % (3347358)Instructions burned: 543 (million) % 47.65/7.50 % (3347363)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=655947736:i=30753:av=off:ss=included_2950 on theBenchmark for (2950ds/30753Mi) % 47.65/7.50 % (3347366)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=2636267443:cts=off:i=2759:kws=inv_arity:fgj=on_2948 on theBenchmark for (2948ds/2759Mi) % 47.65/7.50 % (3347365)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2362768149:i=26473:ep=RSTC_2949 on theBenchmark for (2949ds/26473Mi) % 47.65/7.50 % (3347367)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=4184794060:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2948 on theBenchmark for (2948ds/5665Mi) % 47.65/7.50 % (3347367)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 47.65/7.50 % (3347362)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.65/7.50 % (3347362)------------------------------ % 47.65/7.50 % (3347362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.65/7.50 % (3347362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.65/7.50 % (3347362)CaDiCaL version: 2.1.3 % 47.65/7.50 % (3347362)Termination reason: Unknown % 47.65/7.50 % (3347362)Termination phase: Saturation % 47.65/7.50 % (3347362)Time elapsed: 0.362 s % 47.65/7.50 % (3347362)Peak memory usage: 113 MB % 47.65/7.50 % (3347362)Instructions burned: 540 (million) % 47.65/7.50 % (3347363)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.65/7.50 % (3347363)------------------------------ % 47.65/7.50 % (3347363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.65/7.50 % (3347363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.65/7.50 % (3347363)CaDiCaL version: 2.1.3 % 47.65/7.50 % (3347363)Termination reason: Unknown % 47.65/7.50 % (3347363)Termination phase: Saturation % 47.65/7.50 % (3347363)Time elapsed: 0.364 s % 47.65/7.50 % (3347363)Peak memory usage: 113 MB % 47.65/7.50 % (3347363)Instructions burned: 543 (million) % 47.65/7.50 % (3347372)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=3486184779:i=1532:ep=RS:ss=axioms_2945 on theBenchmark for (2945ds/1532Mi) % 47.65/7.50 % (3347366)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.65/7.50 % (3347366)------------------------------ % 47.65/7.50 % (3347366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.65/7.50 % (3347366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.65/7.50 % (3347366)CaDiCaL version: 2.1.3 % 47.65/7.50 % (3347366)Termination reason: Unknown % 47.65/7.50 % (3347366)Termination phase: Saturation % 47.65/7.50 % (3347366)Time elapsed: 0.362 s % 47.65/7.50 % (3347366)Peak memory usage: 114 MB % 47.65/7.50 % (3347366)Instructions burned: 544 (million) % 47.65/7.50 % (3347367)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.65/7.50 % (3347367)------------------------------ % 47.65/7.50 % (3347367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.14/8.20 % (3347367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.14/8.20 % (3347367)CaDiCaL version: 2.1.3 % 53.14/8.20 % (3347367)Termination reason: Unknown % 53.14/8.20 % (3347367)Termination phase: Saturation % 53.14/8.20 % (3347367)Time elapsed: 0.360 s % 53.14/8.20 % (3347367)Peak memory usage: 113 MB % 53.14/8.20 % (3347367)Instructions burned: 543 (million) % 53.14/8.20 % (3347373)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3209803598:i=1565:sd=2:ss=axioms:sgt=32_2944 on theBenchmark for (2944ds/1565Mi) % 53.14/8.20 % (3347375)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=497395437:i=1572:fgj=on:gsp=on_2943 on theBenchmark for (2943ds/1572Mi) % 53.14/8.20 % (3347375)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 53.14/8.20 % (3347376)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2699386800:i=6052:sd=4:ss=axioms:sgt=24_2943 on theBenchmark for (2943ds/6052Mi) % 53.14/8.20 % (3347372)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.14/8.20 % (3347372)------------------------------ % 53.14/8.20 % (3347372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.14/8.20 % (3347372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.14/8.20 % (3347372)CaDiCaL version: 2.1.3 % 53.14/8.20 % (3347372)Termination reason: Unknown % 53.14/8.20 % (3347372)Termination phase: Saturation % 53.14/8.20 % (3347372)Time elapsed: 0.362 s % 53.14/8.20 % (3347372)Peak memory usage: 113 MB % 53.14/8.20 % (3347372)Instructions burned: 540 (million) % 53.14/8.20 % (3347331)Instruction limit reached! % 53.14/8.20 % (3347331)------------------------------ % 53.14/8.20 % (3347331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.14/8.20 % (3347331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.14/8.20 % (3347331)CaDiCaL version: 2.1.3 % 53.14/8.20 % (3347331)Termination reason: Instruction limit % 53.14/8.20 % (3347331)Termination phase: Saturation % 53.14/8.20 % (3347331)Time elapsed: 2.938 s % 53.14/8.20 % (3347331)Peak memory usage: 113 MB % 53.14/8.20 % (3347331)Instructions burned: 4836 (million) % 53.14/8.20 % (3347373)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.14/8.20 % (3347373)------------------------------ % 53.14/8.20 % (3347373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.14/8.20 % (3347373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.14/8.20 % (3347373)CaDiCaL version: 2.1.3 % 53.14/8.20 % (3347373)Termination reason: Unknown % 53.14/8.20 % (3347373)Termination phase: Saturation % 53.14/8.20 % (3347373)Time elapsed: 0.361 s % 53.14/8.20 % (3347373)Peak memory usage: 113 MB % 53.14/8.20 % (3347373)Instructions burned: 540 (million) % 53.14/8.20 % (3347380)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=1803906839:i=3500:sd=1:bd=preordered:sup=off:ss=included_2940 on theBenchmark for (2940ds/3500Mi) % 53.14/8.20 % (3347375)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.14/8.20 % (3347375)------------------------------ % 53.14/8.20 % (3347375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.14/8.20 % (3347375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.14/8.20 % (3347375)CaDiCaL version: 2.1.3 % 53.14/8.20 % (3347375)Termination reason: Unknown % 53.14/8.20 % (3347375)Termination phase: Saturation % 53.14/8.20 % (3347375)Time elapsed: 0.363 s % 53.14/8.20 % (3347375)Peak memory usage: 113 MB % 53.14/8.20 % (3347375)Instructions burned: 542 (million) % 53.14/8.20 % (3347381)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=3872690238:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2940 on theBenchmark for (2940ds/1842Mi) % 53.14/8.20 % (3347381)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 53.14/8.20 % (3347376)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 53.14/8.20 % (3347376)------------------------------ % 56.75/8.81 % (3347376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.75/8.81 % (3347376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.75/8.81 % (3347376)CaDiCaL version: 2.1.3 % 56.75/8.81 % (3347376)Termination reason: Unknown % 56.75/8.81 % (3347376)Termination phase: Saturation % 56.75/8.81 % (3347376)Time elapsed: 0.362 s % 56.75/8.81 % (3347376)Peak memory usage: 113 MB % 56.75/8.81 % (3347376)Instructions burned: 543 (million) % 56.75/8.81 % (3347382)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=154230045:i=66096:add=on_2939 on theBenchmark for (2939ds/66096Mi) % 56.75/8.81 % (3347384)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2337322566:i=1884:sd=1:nm=60:ss=axioms_2938 on theBenchmark for (2938ds/1884Mi) % 56.75/8.81 % (3347386)lrs-1011_4:1_sil=16000:bsr=on:random_seed=4080658590:cts=off:i=5469:bs=on:fsr=off_2938 on theBenchmark for (2938ds/5469Mi) % 56.75/8.81 % (3347380)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.75/8.81 % (3347380)------------------------------ % 56.75/8.81 % (3347380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.75/8.81 % (3347380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.75/8.81 % (3347380)CaDiCaL version: 2.1.3 % 56.75/8.81 % (3347380)Termination reason: Unknown % 56.75/8.81 % (3347380)Termination phase: Saturation % 56.75/8.81 % (3347380)Time elapsed: 0.361 s % 56.75/8.81 % (3347380)Peak memory usage: 113 MB % 56.75/8.81 % (3347380)Instructions burned: 543 (million) % 56.75/8.81 % (3347381)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.75/8.81 % (3347381)------------------------------ % 56.75/8.81 % (3347381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.75/8.81 % (3347381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.75/8.81 % (3347381)CaDiCaL version: 2.1.3 % 56.75/8.81 % (3347381)Termination reason: Unknown % 56.75/8.81 % (3347381)Termination phase: Saturation % 56.75/8.81 % (3347381)Time elapsed: 0.362 s % 56.75/8.81 % (3347381)Peak memory usage: 113 MB % 56.75/8.81 % (3347381)Instructions burned: 543 (million) % 56.75/8.81 % (3347382)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.75/8.81 % (3347382)------------------------------ % 56.75/8.81 % (3347382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.75/8.81 % (3347382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.75/8.81 % (3347382)CaDiCaL version: 2.1.3 % 56.75/8.81 % (3347382)Termination reason: Unknown % 56.75/8.81 % (3347382)Termination phase: Saturation % 56.75/8.81 % (3347382)Time elapsed: 0.360 s % 56.75/8.81 % (3347382)Peak memory usage: 114 MB % 56.75/8.81 % (3347382)Instructions burned: 542 (million) % 56.75/8.81 % (3347390)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=300824387:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2935 on theBenchmark for (2935ds/2037Mi) % 56.75/8.81 % (3347384)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.75/8.81 % (3347384)------------------------------ % 56.75/8.81 % (3347384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.75/8.81 % (3347384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.75/8.81 % (3347384)CaDiCaL version: 2.1.3 % 56.75/8.81 % (3347384)Termination reason: Unknown % 56.75/8.81 % (3347384)Termination phase: Saturation % 56.75/8.81 % (3347384)Time elapsed: 0.358 s % 56.75/8.81 % (3347384)Peak memory usage: 113 MB % 56.75/8.81 % (3347384)Instructions burned: 538 (million) % 56.75/8.81 % (3347391)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1942698735:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2934 on theBenchmark for (2934ds/2110Mi) % 56.75/8.81 % (3347392)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=3321657569:i=2430:add=off:aac=none:nm=16_2934 on theBenchmark for (2934ds/2430Mi) % 56.75/8.81 % (3347394)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=263289940:cond=fast:i=4891_2933 on theBenchmark for (2933ds/4891Mi) % 61.73/9.50 % (3347390)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.73/9.50 % (3347390)------------------------------ % 61.73/9.50 % (3347390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.50 % (3347390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.50 % (3347390)CaDiCaL version: 2.1.3 % 61.73/9.50 % (3347390)Termination reason: Unknown % 61.73/9.50 % (3347390)Termination phase: Saturation % 61.73/9.50 % (3347390)Time elapsed: 0.364 s % 61.73/9.50 % (3347390)Peak memory usage: 114 MB % 61.73/9.50 % (3347390)Instructions burned: 550 (million) % 61.73/9.50 % (3347391)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.73/9.50 % (3347391)------------------------------ % 61.73/9.50 % (3347391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.50 % (3347391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.50 % (3347391)CaDiCaL version: 2.1.3 % 61.73/9.50 % (3347391)Termination reason: Unknown % 61.73/9.50 % (3347391)Termination phase: Saturation % 61.73/9.50 % (3347391)Time elapsed: 0.363 s % 61.73/9.50 % (3347391)Peak memory usage: 114 MB % 61.73/9.50 % (3347391)Instructions burned: 548 (million) % 61.73/9.50 % (3347392)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.73/9.50 % (3347392)------------------------------ % 61.73/9.50 % (3347392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.50 % (3347392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.50 % (3347392)CaDiCaL version: 2.1.3 % 61.73/9.50 % (3347392)Termination reason: Unknown % 61.73/9.50 % (3347392)Termination phase: Saturation % 61.73/9.50 % (3347392)Time elapsed: 0.360 s % 61.73/9.50 % (3347392)Peak memory usage: 113 MB % 61.73/9.50 % (3347392)Instructions burned: 543 (million) % 61.73/9.50 % (3347398)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=2141505772:st=2:i=14845:sd=2:ss=included:fsd=on_2930 on theBenchmark for (2930ds/14845Mi) % 61.73/9.50 % (3347394)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.73/9.50 % (3347394)------------------------------ % 61.73/9.50 % (3347394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.50 % (3347394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.50 % (3347394)CaDiCaL version: 2.1.3 % 61.73/9.50 % (3347394)Termination reason: Unknown % 61.73/9.50 % (3347394)Termination phase: Saturation % 61.73/9.50 % (3347394)Time elapsed: 0.360 s % 61.73/9.50 % (3347394)Peak memory usage: 114 MB % 61.73/9.50 % (3347394)Instructions burned: 543 (million) % 61.73/9.50 % (3347399)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=221528295:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2929 on theBenchmark for (2929ds/7534Mi) % 61.73/9.50 % (3347400)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=3510669459:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2929 on theBenchmark for (2929ds/10353Mi) % 61.73/9.50 % (3347402)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1598164709:i=7860_2928 on theBenchmark for (2928ds/7860Mi) % 61.73/9.50 % (3347402)Refutation not found, incomplete strategy % 61.73/9.50 % (3347402)------------------------------ % 61.73/9.50 % (3347402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.50 % (3347402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.50 % (3347402)CaDiCaL version: 2.1.3 % 61.73/9.50 % (3347402)Termination reason: Refutation not found, incomplete strategy % 61.73/9.50 % (3347402)Time elapsed: 0.007 s % 61.73/9.50 % (3347402)Peak memory usage: 88 MB % 61.73/9.50 % (3347402)Instructions burned: 12 (million) % 61.73/9.50 % (3347398)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.73/9.50 % (3347398)------------------------------ % 61.73/9.50 % (3347398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.73/9.50 % (3347398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.73/9.50 % (3347398)CaDiCaL version: 2.1.3 % 61.73/9.50 % (3347398)Termination reason: Unknown % 61.73/9.50 % (3347398)Termination phase: Saturation % 67.78/10.26 % (3347398)Time elapsed: 0.365 s % 67.78/10.26 % (3347398)Peak memory usage: 114 MB % 67.78/10.26 % (3347398)Instructions burned: 544 (million) % 67.78/10.26 % (3347399)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.78/10.26 % (3347399)------------------------------ % 67.78/10.26 % (3347399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.78/10.26 % (3347399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.78/10.26 % (3347399)CaDiCaL version: 2.1.3 % 67.78/10.26 % (3347399)Termination reason: Unknown % 67.78/10.26 % (3347399)Termination phase: Saturation % 67.78/10.26 % (3347399)Time elapsed: 0.362 s % 67.78/10.26 % (3347399)Peak memory usage: 114 MB % 67.78/10.26 % (3347399)Instructions burned: 545 (million) % 67.78/10.26 % (3347400)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.78/10.26 % (3347400)------------------------------ % 67.78/10.26 % (3347400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.78/10.26 % (3347400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.78/10.26 % (3347400)CaDiCaL version: 2.1.3 % 67.78/10.26 % (3347400)Termination reason: Unknown % 67.78/10.26 % (3347400)Termination phase: Saturation % 67.78/10.26 % (3347400)Time elapsed: 0.362 s % 67.78/10.26 % (3347400)Peak memory usage: 114 MB % 67.78/10.26 % (3347400)Instructions burned: 543 (million) % 67.78/10.26 % (3347402)------------------------------ % 67.78/10.26 % (3347402)------------------------------ % 67.78/10.26 % (3347406)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=2519750987:i=7896:sd=2:bs=on:ss=included:sgt=20_2924 on theBenchmark for (2924ds/7896Mi) % 67.78/10.26 % (3347407)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=428565923:i=5812:gtgl=2:gtg=all_2924 on theBenchmark for (2924ds/5812Mi) % 67.78/10.26 % (3347408)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=2147896320:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2924 on theBenchmark for (2924ds/2965Mi) % 67.78/10.26 % (3347409)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=4187129327:i=2967:kws=precedence:bd=preordered:av=off_2923 on theBenchmark for (2923ds/2967Mi) % 67.78/10.26 % (3347406)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.78/10.26 % (3347406)------------------------------ % 67.78/10.26 % (3347406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.78/10.26 % (3347406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.78/10.26 % (3347406)CaDiCaL version: 2.1.3 % 67.78/10.26 % (3347406)Termination reason: Unknown % 67.78/10.26 % (3347406)Termination phase: Saturation % 67.78/10.26 % (3347406)Time elapsed: 0.360 s % 67.78/10.26 % (3347406)Peak memory usage: 113 MB % 67.78/10.26 % (3347406)Instructions burned: 543 (million) % 67.78/10.26 % (3347407)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.78/10.26 % (3347407)------------------------------ % 67.78/10.26 % (3347407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.78/10.26 % (3347407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.78/10.26 % (3347407)CaDiCaL version: 2.1.3 % 67.78/10.26 % (3347407)Termination reason: Unknown % 67.78/10.26 % (3347407)Termination phase: Saturation % 67.78/10.26 % (3347407)Time elapsed: 0.360 s % 67.78/10.26 % (3347407)Peak memory usage: 114 MB % 67.78/10.26 % (3347407)Instructions burned: 546 (million) % 67.78/10.26 % (3347408)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.78/10.26 % (3347408)------------------------------ % 67.78/10.26 % (3347408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.78/10.26 % (3347408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.78/10.26 % (3347408)CaDiCaL version: 2.1.3 % 67.78/10.26 % (3347408)Termination reason: Unknown % 67.78/10.26 % (3347408)Termination phase: Saturation % 67.78/10.26 % (3347408)Time elapsed: 0.360 s % 67.78/10.26 % (3347408)Peak memory usage: 114 MB % 67.78/10.26 % (3347408)Instructions burned: 543 (million) % 67.78/10.26 % (3347409)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.78/10.26 % (3347409)------------------------------ % 67.78/10.26 % (3347409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.13/10.82 % (3347409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.13/10.82 % (3347409)CaDiCaL version: 2.1.3 % 71.13/10.82 % (3347409)Termination reason: Unknown % 71.13/10.82 % (3347409)Termination phase: Saturation % 71.13/10.82 % (3347409)Time elapsed: 0.358 s % 71.13/10.82 % (3347409)Peak memory usage: 114 MB % 71.13/10.82 % (3347409)Instructions burned: 543 (million) % 71.13/10.82 % (3347414)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=163693192:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2919 on theBenchmark for (2919ds/3022Mi) % 71.13/10.82 % (3347415)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=1069160207:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2919 on theBenchmark for (2919ds/3207Mi) % 71.13/10.82 % (3347416)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3788909256:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2918 on theBenchmark for (2918ds/3289Mi) % 71.13/10.82 % (3347417)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2169659255:i=38569:sd=3:ss=axioms:sgt=32_2918 on theBenchmark for (2918ds/38569Mi) % 71.13/10.82 % (3347414)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 71.13/10.82 % (3347414)------------------------------ % 71.13/10.82 % (3347414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.13/10.82 % (3347414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.13/10.82 % (3347414)CaDiCaL version: 2.1.3 % 71.13/10.82 % (3347414)Termination reason: Unknown % 71.13/10.82 % (3347414)Termination phase: Saturation % 71.13/10.82 % (3347414)Time elapsed: 0.359 s % 71.13/10.82 % (3347414)Peak memory usage: 113 MB % 71.13/10.82 % (3347414)Instructions burned: 539 (million) % 71.13/10.82 % (3347415)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 71.13/10.82 % (3347415)------------------------------ % 71.13/10.82 % (3347415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.13/10.82 % (3347415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.13/10.82 % (3347415)CaDiCaL version: 2.1.3 % 71.13/10.82 % (3347415)Termination reason: Unknown % 71.13/10.82 % (3347415)Termination phase: Saturation % 71.13/10.82 % (3347415)Time elapsed: 0.359 s % 71.13/10.82 % (3347415)Peak memory usage: 114 MB % 71.13/10.82 % (3347415)Instructions burned: 541 (million) % 71.13/10.82 % (3347416)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 71.13/10.82 % (3347416)------------------------------ % 71.13/10.82 % (3347416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.13/10.82 % (3347416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.13/10.82 % (3347416)CaDiCaL version: 2.1.3 % 71.13/10.82 % (3347416)Termination reason: Unknown % 71.13/10.82 % (3347416)Termination phase: Saturation % 71.13/10.82 % (3347416)Time elapsed: 0.361 s % 71.13/10.82 % (3347416)Peak memory usage: 113 MB % 71.13/10.82 % (3347416)Instructions burned: 543 (million) % 71.13/10.82 % (3347417)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 71.13/10.82 % (3347417)------------------------------ % 71.13/10.82 % (3347417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.13/10.82 % (3347417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.13/10.82 % (3347417)CaDiCaL version: 2.1.3 % 71.13/10.82 % (3347417)Termination reason: Unknown % 71.13/10.82 % (3347417)Termination phase: Saturation % 71.13/10.82 % (3347417)Time elapsed: 0.357 s % 71.13/10.82 % (3347417)Peak memory usage: 114 MB % 71.13/10.82 % (3347417)Instructions burned: 543 (million) % 71.13/10.82 % (3347422)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1130714204:cts=off:i=3394_2914 on theBenchmark for (2914ds/3394Mi) % 71.13/10.82 % (3347423)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=3141490324:i=33824:bd=preordered_2914 on theBenchmark for (2914ds/33824Mi) % 71.13/10.82 % (3347424)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2656496496:i=20684:bd=all:gtg=exists_sym_2913 on theBenchmark for (2913ds/20684Mi) % 76.06/11.45 % (3347425)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=1666069592: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_2913 on theBenchmark for (2913ds/7222Mi) % 76.06/11.45 % (3347425)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 76.06/11.45 % (3347422)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 76.06/11.45 % (3347422)------------------------------ % 76.06/11.45 % (3347422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.06/11.45 % (3347422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.06/11.45 % (3347422)CaDiCaL version: 2.1.3 % 76.06/11.45 % (3347422)Termination reason: Unknown % 76.06/11.45 % (3347422)Termination phase: Saturation % 76.06/11.45 % (3347422)Time elapsed: 0.360 s % 76.06/11.45 % (3347422)Peak memory usage: 113 MB % 76.06/11.45 % (3347422)Instructions burned: 543 (million) % 76.06/11.45 % (3347423)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 76.06/11.45 % (3347423)------------------------------ % 76.06/11.45 % (3347423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.06/11.45 % (3347423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.06/11.45 % (3347423)CaDiCaL version: 2.1.3 % 76.06/11.45 % (3347423)Termination reason: Unknown % 76.06/11.45 % (3347423)Termination phase: Saturation % 76.06/11.45 % (3347423)Time elapsed: 0.359 s % 76.06/11.45 % (3347423)Peak memory usage: 114 MB % 76.06/11.45 % (3347423)Instructions burned: 543 (million) % 76.06/11.45 % (3347425)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 76.06/11.45 % (3347424)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 76.06/11.45 % (3347424)------------------------------ % 76.06/11.45 % (3347424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.06/11.45 % (3347425)------------------------------ % 76.06/11.45 % (3347425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.06/11.45 % (3347424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.06/11.45 % (3347425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.06/11.45 % (3347425)CaDiCaL version: 2.1.3 % 76.06/11.45 % (3347424)CaDiCaL version: 2.1.3 % 76.06/11.45 % (3347424)Termination reason: Unknown % 76.06/11.45 % (3347424)Termination phase: Saturation % 76.06/11.45 % (3347425)Termination reason: Unknown % 76.06/11.45 % (3347425)Termination phase: Saturation % 76.06/11.45 % (3347424)Time elapsed: 0.362 s % 76.06/11.45 % (3347425)Time elapsed: 0.362 s % 76.06/11.45 % (3347425)Peak memory usage: 112 MB % 76.06/11.45 % (3347424)Peak memory usage: 112 MB % 76.06/11.45 % (3347424)Instructions burned: 545 (million) % 76.06/11.45 % (3347425)Instructions burned: 549 (million) % 76.06/11.45 % (3347430)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1001075935:st=4:i=7295:sd=4:ep=R:ss=axioms_2909 on theBenchmark for (2909ds/7295Mi) % 76.06/11.45 % (3347431)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=3985513228:i=4036:ins=10_2908 on theBenchmark for (2908ds/4036Mi) % 76.06/11.45 % (3347433)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=689658185:i=17599:gtg=all:ss=axioms:fsd=on_2908 on theBenchmark for (2908ds/17599Mi) % 76.06/11.45 % (3347432)lrs+10_1_sil=128000:lcm=predicate:random_seed=4176258244:st=3:i=43697:sd=5:ss=axioms_2908 on theBenchmark for (2908ds/43697Mi) % 76.06/11.45 % (3347386)Instruction limit reached! % 76.06/11.45 % (3347386)------------------------------ % 76.06/11.45 % (3347386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.06/11.45 % (3347386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.06/11.45 % (3347386)CaDiCaL version: 2.1.3 % 76.06/11.45 % (3347386)Termination reason: Instruction limit % 76.06/11.45 % (3347386)Termination phase: Saturation % 76.06/11.45 % (3347386)Time elapsed: 3.241 s % 76.06/11.45 % (3347386)Peak memory usage: 116 MB % 76.06/11.45 % (3347386)Instructions burned: 5470 (million) % 76.06/11.45 % (3347430)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.92/12.27 % (3347430)------------------------------ % 81.92/12.27 % (3347430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.92/12.27 % (3347430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.92/12.27 % (3347430)CaDiCaL version: 2.1.3 % 81.92/12.27 % (3347430)Termination reason: Unknown % 81.92/12.27 % (3347430)Termination phase: Saturation % 81.92/12.27 % (3347430)Time elapsed: 0.359 s % 81.92/12.27 % (3347430)Peak memory usage: 113 MB % 81.92/12.27 % (3347430)Instructions burned: 545 (million) % 81.92/12.27 % (3347431)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.92/12.27 % (3347431)------------------------------ % 81.92/12.27 % (3347431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.92/12.27 % (3347431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.92/12.27 % (3347431)CaDiCaL version: 2.1.3 % 81.92/12.27 % (3347431)Termination reason: Unknown % 81.92/12.27 % (3347431)Termination phase: Saturation % 81.92/12.27 % (3347431)Time elapsed: 0.361 s % 81.92/12.27 % (3347431)Peak memory usage: 113 MB % 81.92/12.27 % (3347431)Instructions burned: 543 (million) % 81.92/12.27 % (3347433)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.92/12.27 % (3347433)------------------------------ % 81.92/12.27 % (3347433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.92/12.27 % (3347433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.92/12.27 % (3347433)CaDiCaL version: 2.1.3 % 81.92/12.27 % (3347433)Termination reason: Unknown % 81.92/12.27 % (3347433)Termination phase: Saturation % 81.92/12.27 % (3347433)Time elapsed: 0.359 s % 81.92/12.27 % (3347433)Peak memory usage: 113 MB % 81.92/12.27 % (3347433)Instructions burned: 542 (million) % 81.92/12.27 % (3347438)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=544893837:i=4547:bd=preordered_2904 on theBenchmark for (2904ds/4547Mi) % 81.92/12.27 % (3347439)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=1641176934:i=9294:av=off_2904 on theBenchmark for (2904ds/9294Mi) % 81.92/12.27 % (3347440)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3566624440:i=32849:add=on_2903 on theBenchmark for (2903ds/32849Mi) % 81.92/12.27 % (3347441)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=648127403:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2903 on theBenchmark for (2903ds/4793Mi) % 81.92/12.27 % (3347439)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.92/12.27 % (3347439)------------------------------ % 81.92/12.27 % (3347439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.92/12.27 % (3347439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.92/12.27 % (3347439)CaDiCaL version: 2.1.3 % 81.92/12.27 % (3347439)Termination reason: Unknown % 81.92/12.27 % (3347439)Termination phase: Saturation % 81.92/12.27 % (3347439)Time elapsed: 0.359 s % 81.92/12.27 % (3347439)Peak memory usage: 113 MB % 81.92/12.27 % (3347439)Instructions burned: 543 (million) % 81.92/12.27 % (3347438)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.92/12.27 % (3347438)------------------------------ % 81.92/12.27 % (3347438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.92/12.27 % (3347438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.92/12.27 % (3347438)CaDiCaL version: 2.1.3 % 81.92/12.27 % (3347438)Termination reason: Unknown % 81.92/12.27 % (3347438)Termination phase: Saturation % 81.92/12.27 % (3347438)Time elapsed: 0.359 s % 81.92/12.27 % (3347438)Peak memory usage: 113 MB % 81.92/12.27 % (3347438)Instructions burned: 543 (million) % 81.92/12.27 % (3347440)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 81.92/12.27 % (3347440)------------------------------ % 81.92/12.27 % (3347440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.92/12.27 % (3347440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.92/12.27 % (3347440)CaDiCaL version: 2.1.3 % 81.92/12.27 % (3347440)Termination reason: Unknown % 81.92/12.27 % (3347440)Termination phase: Saturation % 81.92/12.27 % (3347440)Time elapsed: 0.357 s % 81.92/12.27 % (3347440)Peak memory usage: 114 MB % 92.83/13.83 % (3347440)Instructions burned: 543 (million) % 92.83/13.83 % (3347441)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 92.83/13.83 % (3347441)------------------------------ % 92.83/13.83 % (3347441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.83/13.83 % (3347441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.83/13.83 % (3347441)CaDiCaL version: 2.1.3 % 92.83/13.83 % (3347441)Termination reason: Unknown % 92.83/13.83 % (3347441)Termination phase: Saturation % 92.83/13.83 % (3347441)Time elapsed: 0.359 s % 92.83/13.83 % (3347441)Peak memory usage: 113 MB % 92.83/13.83 % (3347441)Instructions burned: 542 (million) % 92.83/13.83 % (3347446)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=668105426:i=4840:nm=4:av=off_2899 on theBenchmark for (2899ds/4840Mi) % 92.83/13.83 % (3347447)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2869785724:cts=off:i=5002_2899 on theBenchmark for (2899ds/5002Mi) % 92.83/13.83 % (3347448)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=2059755408:i=30479:sd=3:ss=axioms_2898 on theBenchmark for (2898ds/30479Mi) % 92.83/13.83 % (3347449)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=822851764:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2897 on theBenchmark for (2897ds/11035Mi) % 92.83/13.83 % (3347449)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 92.83/13.83 % (3347447)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 92.83/13.83 % (3347447)------------------------------ % 92.83/13.83 % (3347447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.83/13.83 % (3347447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.83/13.83 % (3347447)CaDiCaL version: 2.1.3 % 92.83/13.83 % (3347447)Termination reason: Unknown % 92.83/13.83 % (3347447)Termination phase: Saturation % 92.83/13.83 % (3347447)Time elapsed: 0.357 s % 92.83/13.83 % (3347447)Peak memory usage: 112 MB % 92.83/13.83 % (3347447)Instructions burned: 543 (million) % 92.83/13.83 % (3347446)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 92.83/13.83 % (3347446)------------------------------ % 92.83/13.83 % (3347446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.83/13.83 % (3347446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.83/13.83 % (3347446)CaDiCaL version: 2.1.3 % 92.83/13.83 % (3347446)Termination reason: Unknown % 92.83/13.83 % (3347446)Termination phase: Saturation % 92.83/13.83 % (3347446)Time elapsed: 0.357 s % 92.83/13.83 % (3347446)Peak memory usage: 112 MB % 92.83/13.83 % (3347446)Instructions burned: 542 (million) % 92.83/13.83 % (3347448)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 92.83/13.83 % (3347448)------------------------------ % 92.83/13.83 % (3347448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.83/13.83 % (3347448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.83/13.83 % (3347448)CaDiCaL version: 2.1.3 % 92.83/13.83 % (3347448)Termination reason: Unknown % 92.83/13.83 % (3347448)Termination phase: Saturation % 92.83/13.83 % (3347448)Time elapsed: 0.357 s % 92.83/13.83 % (3347448)Peak memory usage: 113 MB % 92.83/13.83 % (3347448)Instructions burned: 540 (million) % 92.83/13.83 % (3347449)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 92.83/13.83 % (3347449)------------------------------ % 92.83/13.83 % (3347449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.83/13.83 % (3347449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.83/13.83 % (3347449)CaDiCaL version: 2.1.3 % 92.83/13.83 % (3347449)Termination reason: Unknown % 92.83/13.83 % (3347449)Termination phase: Saturation % 92.83/13.83 % (3347449)Time elapsed: 0.362 s % 92.83/13.83 % (3347449)Peak memory usage: 113 MB % 92.83/13.83 % (3347449)Instructions burned: 548 (million) % 92.83/13.83 % (3347454)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=2210573436:i=5835_2893 on theBenchmark for (2893ds/5835Mi) % 92.83/13.83 % (3347455)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=1912842628:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2893 on theBenchmark for (2893ds/5890Mi) % 109.88/16.16 % (3347456)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2786726532:cts=off:i=19910:ep=RS_2893 on theBenchmark for (2893ds/19910Mi) % 109.88/16.16 % (3347456)Refutation not found, incomplete strategy % 109.88/16.16 % (3347456)------------------------------ % 109.88/16.16 % (3347456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.88/16.16 % (3347456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.88/16.16 % (3347456)CaDiCaL version: 2.1.3 % 109.88/16.16 % (3347456)Termination reason: Refutation not found, incomplete strategy % 109.88/16.16 % (3347456)Time elapsed: 0.007 s % 109.88/16.16 % (3347456)Peak memory usage: 88 MB % 109.88/16.16 % (3347456)Instructions burned: 12 (million) % 109.88/16.16 % (3347457)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=2605585351:i=20312:bd=preordered:fsr=off:er=filter_2892 on theBenchmark for (2892ds/20312Mi) % 109.88/16.16 % (3347456)------------------------------ % 109.88/16.16 % (3347456)------------------------------ % 109.88/16.16 % (3347455)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 109.88/16.16 % (3347455)------------------------------ % 109.88/16.16 % (3347455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.88/16.16 % (3347455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.88/16.16 % (3347454)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 109.88/16.16 % (3347455)CaDiCaL version: 2.1.3 % 109.88/16.16 % (3347455)Termination reason: Unknown % 109.88/16.16 % (3347455)Termination phase: Saturation % 109.88/16.16 % (3347454)------------------------------ % 109.88/16.16 % (3347454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.88/16.16 % (3347455)Time elapsed: 0.360 s % 109.88/16.16 % (3347455)Peak memory usage: 112 MB % 109.88/16.16 % (3347454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.88/16.16 % (3347455)Instructions burned: 543 (million) % 109.88/16.16 % (3347454)CaDiCaL version: 2.1.3 % 109.88/16.16 % (3347454)Termination reason: Unknown % 109.88/16.16 % (3347454)Termination phase: Saturation % 109.88/16.16 % (3347454)Time elapsed: 0.360 s % 109.88/16.16 % (3347454)Peak memory usage: 112 MB % 109.88/16.16 % (3347454)Instructions burned: 543 (million) % 109.88/16.16 % (3347462)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=2722974674:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2889 on theBenchmark for (2889ds/13822Mi) % 109.88/16.16 % (3347457)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 109.88/16.16 % (3347457)------------------------------ % 109.88/16.16 % (3347457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.88/16.16 % (3347457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.88/16.16 % (3347457)CaDiCaL version: 2.1.3 % 109.88/16.16 % (3347457)Termination reason: Unknown % 109.88/16.16 % (3347457)Termination phase: Saturation % 109.88/16.16 % (3347457)Time elapsed: 0.364 s % 109.88/16.16 % (3347457)Peak memory usage: 114 MB % 109.88/16.16 % (3347457)Instructions burned: 543 (million) % 109.88/16.16 % (3347464)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=2433305395:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2888 on theBenchmark for (2888ds/15184Mi) % 109.88/16.16 % (3347463)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=925159481:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2888 on theBenchmark for (2888ds/7144Mi) % 109.88/16.16 % (3347466)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=722773670:i=107375_2887 on theBenchmark for (2887ds/107375Mi) % 109.88/16.16 % (3347462)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 109.88/16.16 % (3347462)------------------------------ % 109.88/16.16 % (3347462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.88/16.16 % (3347462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.88/16.16 % (3347462)CaDiCaL version: 2.1.3 % 115.74/17.12 % (3347462)Termination reason: Unknown % 115.74/17.12 % (3347462)Termination phase: Saturation % 115.74/17.12 % (3347462)Time elapsed: 0.359 s % 115.74/17.12 % (3347462)Peak memory usage: 114 MB % 115.74/17.12 % (3347462)Instructions burned: 543 (million) % 115.74/17.12 % (3347464)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 115.74/17.12 % (3347464)------------------------------ % 115.74/17.12 % (3347464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.74/17.12 % (3347464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.74/17.12 % (3347464)CaDiCaL version: 2.1.3 % 115.74/17.12 % (3347464)Termination reason: Unknown % 115.74/17.12 % (3347464)Termination phase: Saturation % 115.74/17.12 % (3347464)Time elapsed: 0.359 s % 115.74/17.12 % (3347464)Peak memory usage: 113 MB % 115.74/17.12 % (3347464)Instructions burned: 543 (million) % 115.74/17.12 % (3347470)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=771432219:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2884 on theBenchmark for (2884ds/7958Mi) % 115.74/17.12 % (3347466)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 115.74/17.12 % (3347466)------------------------------ % 115.74/17.12 % (3347466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.74/17.12 % (3347466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.74/17.12 % (3347466)CaDiCaL version: 2.1.3 % 115.74/17.12 % (3347466)Termination reason: Unknown % 115.74/17.12 % (3347466)Termination phase: Saturation % 115.74/17.12 % (3347466)Time elapsed: 0.359 s % 115.74/17.12 % (3347466)Peak memory usage: 114 MB % 115.74/17.12 % (3347466)Instructions burned: 543 (million) % 115.74/17.12 % (3347471)dis+10_128_sil=16000:nwc=0.7:random_seed=926858863:i=15999:nm=2:gsp=on_2883 on theBenchmark for (2883ds/15999Mi) % 115.74/17.12 % (3347471)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 115.74/17.12 % (3347473)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=183560526:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2882 on theBenchmark for (2882ds/8139Mi) % 115.74/17.12 % (3347470)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 115.74/17.12 % (3347470)------------------------------ % 115.74/17.12 % (3347470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.74/17.12 % (3347470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.74/17.12 % (3347470)CaDiCaL version: 2.1.3 % 115.74/17.12 % (3347470)Termination reason: Unknown % 115.74/17.12 % (3347470)Termination phase: Saturation % 115.74/17.12 % (3347470)Time elapsed: 0.360 s % 115.74/17.12 % (3347470)Peak memory usage: 113 MB % 115.74/17.12 % (3347470)Instructions burned: 543 (million) % 115.74/17.12 % (3347476)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=4247327815:st=4:i=8950:sd=5:ss=axioms_2878 on theBenchmark for (2878ds/8950Mi) % 115.74/17.12 % (3347476)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 115.74/17.12 % (3347476)------------------------------ % 115.74/17.12 % (3347476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.74/17.12 % (3347476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.74/17.12 % (3347476)CaDiCaL version: 2.1.3 % 115.74/17.12 % (3347476)Termination reason: Unknown % 115.74/17.12 % (3347476)Termination phase: Saturation % 115.74/17.12 % (3347476)Time elapsed: 0.357 s % 115.74/17.12 % (3347476)Peak memory usage: 114 MB % 115.74/17.12 % (3347476)Instructions burned: 543 (million) % 115.74/17.12 % (3347478)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=4188493415:i=9809:ins=10:av=off_2873 on theBenchmark for (2873ds/9809Mi) % 115.74/17.12 % (3347478)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 115.74/17.12 % (3347478)------------------------------ % 115.74/17.12 % (3347478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 115.74/17.12 % (3347478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 115.74/17.12 % (3347478)CaDiCaL version: 2.1.3 % 115.74/17.12 % (3347478)Termination reason: Unknown % 115.74/17.12 % (3347478)Termination phase: Saturation % 115.74/17.12 % (3347478)Time elapsed: 0.358 s % 115.74/17.12 % (3347478)Peak memory usage: 114 MB % 115.74/17.12 % (3347478)Instructions burned: 543 (million) % 149.03/21.72 % (3347480)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=1626632696:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2868 on theBenchmark for (2868ds/9885Mi) % 149.03/21.72 % (3347480)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 149.03/21.72 % (3347480)------------------------------ % 149.03/21.72 % (3347480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.03/21.72 % (3347480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.03/21.72 % (3347480)CaDiCaL version: 2.1.3 % 149.03/21.72 % (3347480)Termination reason: Unknown % 149.03/21.72 % (3347480)Termination phase: Saturation % 149.03/21.72 % (3347480)Time elapsed: 0.360 s % 149.03/21.72 % (3347480)Peak memory usage: 114 MB % 149.03/21.72 % (3347480)Instructions burned: 544 (million) % 149.03/21.72 % (3347482)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=315286015:cond=fast:i=32078:fgj=on:av=off_2863 on theBenchmark for (2863ds/32078Mi) % 149.03/21.72 % (3347482)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 149.03/21.72 % (3347482)------------------------------ % 149.03/21.72 % (3347482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.03/21.72 % (3347482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.03/21.72 % (3347482)CaDiCaL version: 2.1.3 % 149.03/21.72 % (3347482)Termination reason: Unknown % 149.03/21.72 % (3347482)Termination phase: Saturation % 149.03/21.72 % (3347482)Time elapsed: 0.359 s % 149.03/21.72 % (3347482)Peak memory usage: 114 MB % 149.03/21.72 % (3347482)Instructions burned: 543 (million) % 149.03/21.72 % (3347484)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=4043489605:i=11101:bd=all:ss=axioms:sgt=8_2857 on theBenchmark for (2857ds/11101Mi) % 149.03/21.72 % (3347340)Instruction limit reached! % 149.03/21.72 % (3347340)------------------------------ % 149.03/21.72 % (3347340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.03/21.72 % (3347340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.03/21.72 % (3347340)CaDiCaL version: 2.1.3 % 149.03/21.72 % (3347340)Termination reason: Instruction limit % 149.03/21.72 % (3347340)Termination phase: Saturation % 149.03/21.72 % (3347340)Time elapsed: 11.345 s % 149.03/21.72 % (3347340)Peak memory usage: 214 MB % 149.03/21.72 % (3347340)Instructions burned: 33336 (million) % 149.03/21.72 % (3347486)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=1220411851:cond=on:i=13220:s2at=3:aac=none:fsd=on_2851 on theBenchmark for (2851ds/13220Mi) % 149.03/21.72 % (3347486)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 149.03/21.72 % (3347486)------------------------------ % 149.03/21.72 % (3347486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.03/21.72 % (3347486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.03/21.72 % (3347486)CaDiCaL version: 2.1.3 % 149.03/21.72 % (3347486)Termination reason: Unknown % 149.03/21.72 % (3347486)Termination phase: Saturation % 149.03/21.72 % (3347486)Time elapsed: 0.195 s % 149.03/21.72 % (3347486)Peak memory usage: 114 MB % 149.03/21.72 % (3347486)Instructions burned: 543 (million) % 149.03/21.72 % (3347463)Instruction limit reached! % 149.03/21.72 % (3347463)------------------------------ % 149.03/21.72 % (3347463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 149.03/21.72 % (3347463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 149.03/21.72 % (3347463)CaDiCaL version: 2.1.3 % 149.03/21.72 % (3347463)Termination reason: Instruction limit % 149.03/21.72 % (3347463)Termination phase: Saturation % 149.03/21.72 % (3347463)Time elapsed: 3.967 s % 149.03/21.72 % (3347463)Peak memory usage: 136 MB % 149.03/21.72 % (3347463)Instructions burned: 7145 (million) % 149.03/21.72 % (3347488)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=7904350:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2848 on theBenchmark for (2848ds/13528Mi) % 149.03/21.72 % (3347489)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=3870892597:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2847 on theBenchmark for (2847ds/14854Mi) % 149.03/21.72 % (3347488)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 156.40/22.87 % (3347488)------------------------------ % 156.40/22.87 % (3347488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.40/22.87 % (3347488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.40/22.87 % (3347488)CaDiCaL version: 2.1.3 % 156.40/22.87 % (3347488)Termination reason: Unknown % 156.40/22.87 % (3347488)Termination phase: Saturation % 156.40/22.87 % (3347488)Time elapsed: 0.197 s % 156.40/22.87 % (3347488)Peak memory usage: 114 MB % 156.40/22.87 % (3347488)Instructions burned: 546 (million) % 156.40/22.87 % (3347492)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=3998522970:i=14974:ss=axioms:sgt=16_2845 on theBenchmark for (2845ds/14974Mi) % 156.40/22.87 % (3347492)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 156.40/22.87 % (3347492)------------------------------ % 156.40/22.87 % (3347492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.40/22.87 % (3347492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.40/22.87 % (3347492)CaDiCaL version: 2.1.3 % 156.40/22.87 % (3347492)Termination reason: Unknown % 156.40/22.87 % (3347492)Termination phase: Saturation % 156.40/22.87 % (3347492)Time elapsed: 0.194 s % 156.40/22.87 % (3347492)Peak memory usage: 113 MB % 156.40/22.87 % (3347492)Instructions burned: 543 (million) % 156.40/22.87 % (3347489)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 156.40/22.87 % (3347489)------------------------------ % 156.40/22.87 % (3347489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.40/22.87 % (3347489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.40/22.87 % (3347489)CaDiCaL version: 2.1.3 % 156.40/22.87 % (3347489)Termination reason: Unknown % 156.40/22.87 % (3347489)Termination phase: Saturation % 156.40/22.87 % (3347489)Time elapsed: 0.370 s % 156.40/22.87 % (3347489)Peak memory usage: 114 MB % 156.40/22.87 % (3347489)Instructions burned: 562 (million) % 156.40/22.87 % (3347494)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=3635265554:i=33081:aac=none:fgj=on:bd=all:fsr=off_2842 on theBenchmark for (2842ds/33081Mi) % 156.40/22.87 % (3347495)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=2586673425:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2841 on theBenchmark for (2841ds/50856Mi) % 156.40/22.87 % (3347494)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 156.40/22.87 % (3347494)------------------------------ % 156.40/22.87 % (3347494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.40/22.87 % (3347494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.40/22.87 % (3347494)CaDiCaL version: 2.1.3 % 156.40/22.87 % (3347494)Termination reason: Unknown % 156.40/22.87 % (3347494)Termination phase: Saturation % 156.40/22.87 % (3347494)Time elapsed: 0.196 s % 156.40/22.87 % (3347494)Peak memory usage: 114 MB % 156.40/22.87 % (3347494)Instructions burned: 543 (million) % 156.40/22.87 % (3347498)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=536628924:i=69865_2838 on theBenchmark for (2838ds/69865Mi) % 156.40/22.87 % (3347495)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 156.40/22.87 % (3347495)------------------------------ % 156.40/22.87 % (3347495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.40/22.87 % (3347495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.40/22.87 % (3347495)CaDiCaL version: 2.1.3 % 156.40/22.87 % (3347495)Termination reason: Unknown % 156.40/22.87 % (3347495)Termination phase: Saturation % 156.40/22.87 % (3347495)Time elapsed: 0.362 s % 156.40/22.87 % (3347495)Peak memory usage: 114 MB % 156.40/22.87 % (3347495)Instructions burned: 543 (million) % 156.40/22.87 % (3347498)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 156.40/22.87 % (3347498)------------------------------ % 156.40/22.87 % (3347498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.40/22.87 % (3347498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.40/22.87 % (3347498)CaDiCaL version: 2.1.3 % 156.40/22.87 % (3347498)Termination reason: Unknown % 156.40/22.87 % (3347498)Termination phase: Saturation % 171.71/25.01 % (3347498)Time elapsed: 0.195 s % 171.71/25.01 % (3347498)Peak memory usage: 114 MB % 171.71/25.01 % (3347498)Instructions burned: 543 (million) % 171.71/25.01 % (3347500)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=4258339223:cond=fast:i=17802:gtgl=3:gtg=all_2836 on theBenchmark for (2836ds/17802Mi) % 171.71/25.01 % (3347501)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3155410997:i=96644_2835 on theBenchmark for (2835ds/96644Mi) % 171.71/25.01 % (3347473)Instruction limit reached! % 171.71/25.01 % (3347473)------------------------------ % 171.71/25.01 % (3347473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.71/25.01 % (3347473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/25.01 % (3347473)CaDiCaL version: 2.1.3 % 171.71/25.01 % (3347473)Termination reason: Instruction limit % 171.71/25.01 % (3347473)Termination phase: Saturation % 171.71/25.01 % (3347473)Time elapsed: 4.711 s % 171.71/25.01 % (3347473)Peak memory usage: 126 MB % 171.71/25.01 % (3347473)Instructions burned: 8140 (million) % 171.71/25.01 % (3347504)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 171.71/25.01 % (3347504)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=1424143207:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2833 on theBenchmark for (2833ds/21161Mi) % 171.71/25.01 % (3347500)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 171.71/25.01 % (3347500)------------------------------ % 171.71/25.01 % (3347500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.71/25.01 % (3347500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/25.01 % (3347500)CaDiCaL version: 2.1.3 % 171.71/25.01 % (3347500)Termination reason: Unknown % 171.71/25.01 % (3347500)Termination phase: Saturation % 171.71/25.01 % (3347500)Time elapsed: 0.361 s % 171.71/25.01 % (3347500)Peak memory usage: 114 MB % 171.71/25.01 % (3347500)Instructions burned: 546 (million) % 171.71/25.01 % (3347506)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=1459621492:i=22761:gtg=all:ss=axioms:fsd=on_2831 on theBenchmark for (2831ds/22761Mi) % 171.71/25.01 % (3347506)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 171.71/25.01 % (3347506)------------------------------ % 171.71/25.01 % (3347506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.71/25.01 % (3347506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/25.01 % (3347506)CaDiCaL version: 2.1.3 % 171.71/25.01 % (3347506)Termination reason: Unknown % 171.71/25.01 % (3347506)Termination phase: Saturation % 171.71/25.01 % (3347506)Time elapsed: 0.357 s % 171.71/25.01 % (3347506)Peak memory usage: 113 MB % 171.71/25.01 % (3347506)Instructions burned: 542 (million) % 171.71/25.01 % (3347508)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=4138846251:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2826 on theBenchmark for (2826ds/23713Mi) % 171.71/25.01 % (3347484)Instruction limit reached! % 171.71/25.01 % (3347484)------------------------------ % 171.71/25.01 % (3347484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.71/25.01 % (3347484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/25.01 % (3347484)CaDiCaL version: 2.1.3 % 171.71/25.01 % (3347484)Termination reason: Instruction limit % 171.71/25.01 % (3347484)Termination phase: Saturation % 171.71/25.01 % (3347484)Time elapsed: 6.245 s % 171.71/25.01 % (3347484)Peak memory usage: 154 MB % 171.71/25.01 % (3347484)Instructions burned: 11102 (million) % 171.71/25.01 % (3347510)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3833277090:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2793 on theBenchmark for (2793ds/26509Mi) % 171.71/25.01 % (3347471)Instruction limit reached! % 171.71/25.01 % (3347471)------------------------------ % 171.71/25.01 % (3347471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.71/25.01 % (3347471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.71/25.01 % (3347471)CaDiCaL version: 2.1.3 % 171.71/25.01 % (3347471)Termination reason: Instruction limit % 171.71/25.01 % (3347471)Termination phase: Saturation % 171.71/25.01 % (3347471)Time elapsed: 9.213 s % 190.79/27.64 % (3347471)Peak memory usage: 162 MB % 190.79/27.64 % (3347471)Instructions burned: 16001 (million) % 190.79/27.64 % (3347510)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 190.79/27.64 % (3347510)------------------------------ % 190.79/27.64 % (3347510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.79/27.64 % (3347510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.64 % (3347510)CaDiCaL version: 2.1.3 % 190.79/27.64 % (3347510)Termination reason: Unknown % 190.79/27.64 % (3347510)Termination phase: Saturation % 190.79/27.64 % (3347510)Time elapsed: 0.365 s % 190.79/27.64 % (3347510)Peak memory usage: 114 MB % 190.79/27.64 % (3347510)Instructions burned: 543 (million) % 190.79/27.64 % (3347365)Instruction limit reached! % 190.79/27.64 % (3347365)------------------------------ % 190.79/27.64 % (3347365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.79/27.64 % (3347365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.64 % (3347365)CaDiCaL version: 2.1.3 % 190.79/27.64 % (3347365)Termination reason: Instruction limit % 190.79/27.64 % (3347365)Termination phase: Saturation % 190.79/27.64 % (3347365)Time elapsed: 15.940 s % 190.79/27.64 % (3347365)Peak memory usage: 284 MB % 190.79/27.64 % (3347365)Instructions burned: 26474 (million) % 190.79/27.64 % (3347512)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=2639623014:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2789 on theBenchmark for (2789ds/28957Mi) % 190.79/27.64 % (3347513)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=4293741688:i=29246:s2at=-1:kws=inv_arity:ins=10_2788 on theBenchmark for (2788ds/29246Mi) % 190.79/27.64 % (3347515)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=1499245614:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2787 on theBenchmark for (2787ds/30082Mi) % 190.79/27.64 % (3347515)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 190.79/27.64 % (3347513)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 190.79/27.64 % (3347513)------------------------------ % 190.79/27.64 % (3347513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.79/27.64 % (3347513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.64 % (3347513)CaDiCaL version: 2.1.3 % 190.79/27.64 % (3347513)Termination reason: Unknown % 190.79/27.64 % (3347513)Termination phase: Saturation % 190.79/27.64 % (3347513)Time elapsed: 0.359 s % 190.79/27.64 % (3347513)Peak memory usage: 114 MB % 190.79/27.64 % (3347513)Instructions burned: 543 (million) % 190.79/27.64 % (3347515)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 190.79/27.64 % (3347515)------------------------------ % 190.79/27.64 % (3347515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.79/27.64 % (3347515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.64 % (3347515)CaDiCaL version: 2.1.3 % 190.79/27.64 % (3347515)Termination reason: Unknown % 190.79/27.64 % (3347515)Termination phase: Saturation % 190.79/27.64 % (3347515)Time elapsed: 0.359 s % 190.79/27.64 % (3347515)Peak memory usage: 114 MB % 190.79/27.64 % (3347515)Instructions burned: 547 (million) % 190.79/27.64 % (3347518)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=4117834821:i=32262:bd=preordered_2783 on theBenchmark for (2783ds/32262Mi) % 190.79/27.64 % (3347519)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=3781309216:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2782 on theBenchmark for (2782ds/32870Mi) % 190.79/27.64 % (3347518)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 190.79/27.64 % (3347518)------------------------------ % 190.79/27.64 % (3347518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 190.79/27.64 % (3347518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 190.79/27.64 % (3347518)CaDiCaL version: 2.1.3 % 190.79/27.64 % (3347518)Termination reason: Unknown % 190.79/27.64 % (3347518)Termination phase: Saturation % 190.79/27.64 % (3347518)Time elapsed: 0.358 s % 190.79/27.64 % (3347518)Peak memory usage: 113 MB % 207.47/29.92 % (3347518)Instructions burned: 542 (million) % 207.47/29.92 % (3347519)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.47/29.92 % (3347519)------------------------------ % 207.47/29.92 % (3347519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.47/29.92 % (3347519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.47/29.92 % (3347519)CaDiCaL version: 2.1.3 % 207.47/29.92 % (3347519)Termination reason: Unknown % 207.47/29.92 % (3347519)Termination phase: Saturation % 207.47/29.92 % (3347519)Time elapsed: 0.359 s % 207.47/29.92 % (3347519)Peak memory usage: 114 MB % 207.47/29.92 % (3347519)Instructions burned: 543 (million) % 207.47/29.92 % (3347522)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=2752663878:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2778 on theBenchmark for (2778ds/33295Mi) % 207.47/29.92 % (3347523)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=240313096:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2777 on theBenchmark for (2777ds/36826Mi) % 207.47/29.92 % (3347522)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.47/29.92 % (3347522)------------------------------ % 207.47/29.92 % (3347522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.47/29.92 % (3347522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.47/29.92 % (3347522)CaDiCaL version: 2.1.3 % 207.47/29.92 % (3347522)Termination reason: Unknown % 207.47/29.92 % (3347522)Termination phase: Saturation % 207.47/29.92 % (3347522)Time elapsed: 0.359 s % 207.47/29.92 % (3347522)Peak memory usage: 114 MB % 207.47/29.92 % (3347522)Instructions burned: 542 (million) % 207.47/29.92 % (3347526)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=3261545956:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2772 on theBenchmark for (2772ds/92981Mi) % 207.47/29.92 % (3347526)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.47/29.92 % (3347526)------------------------------ % 207.47/29.92 % (3347526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.47/29.92 % (3347526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.47/29.92 % (3347526)CaDiCaL version: 2.1.3 % 207.47/29.92 % (3347526)Termination reason: Unknown % 207.47/29.92 % (3347526)Termination phase: Saturation % 207.47/29.92 % (3347526)Time elapsed: 0.358 s % 207.47/29.92 % (3347526)Peak memory usage: 114 MB % 207.47/29.92 % (3347526)Instructions burned: 543 (million) % 207.47/29.92 % (3347528)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=24976029:s2pl=on:i=49423_2767 on theBenchmark for (2767ds/49423Mi) % 207.47/29.92 % (3347528)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.47/29.92 % (3347528)------------------------------ % 207.47/29.92 % (3347528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.47/29.92 % (3347528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.47/29.92 % (3347528)CaDiCaL version: 2.1.3 % 207.47/29.92 % (3347528)Termination reason: Unknown % 207.47/29.92 % (3347528)Termination phase: Saturation % 207.47/29.92 % (3347528)Time elapsed: 0.359 s % 207.47/29.92 % (3347528)Peak memory usage: 114 MB % 207.47/29.92 % (3347528)Instructions burned: 544 (million) % 207.47/29.92 % (3347530)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=2667142161:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2762 on theBenchmark for (2762ds/57299Mi) % 207.47/29.92 % (3347530)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.47/29.92 % (3347530)------------------------------ % 207.47/29.92 % (3347530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.47/29.92 % (3347530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.47/29.92 % (3347530)CaDiCaL version: 2.1.3 % 207.47/29.92 % (3347530)Termination reason: Unknown % 207.47/29.92 % (3347530)Termination phase: Saturation % 207.47/29.92 % (3347530)Time elapsed: 0.361 s % 207.47/29.92 % (3347530)Peak memory usage: 113 MB % 207.47/29.92 % (3347530)Instructions burned: 544 (million) % 214.25/31.03 % (3347532)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=65539764:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2756 on theBenchmark for (2756ds/127679Mi) % 214.25/31.03 % (3347532)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 214.25/31.03 % (3347532)------------------------------ % 214.25/31.03 % (3347532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.25/31.03 % (3347532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.25/31.03 % (3347532)CaDiCaL version: 2.1.3 % 214.25/31.03 % (3347532)Termination reason: Unknown % 214.25/31.03 % (3347532)Termination phase: Saturation % 214.25/31.03 % (3347532)Time elapsed: 0.358 s % 214.25/31.03 % (3347532)Peak memory usage: 114 MB % 214.25/31.03 % (3347532)Instructions burned: 543 (million) % 214.25/31.03 % (3347534)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=3060214359:i=69402:add=on:aac=none:fsr=off_2751 on theBenchmark for (2751ds/69402Mi) % 214.25/31.03 % (3347534)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 214.25/31.03 % (3347534)------------------------------ % 214.25/31.03 % (3347534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.25/31.03 % (3347534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.25/31.03 % (3347534)CaDiCaL version: 2.1.3 % 214.25/31.03 % (3347534)Termination reason: Unknown % 214.25/31.03 % (3347534)Termination phase: Saturation % 214.25/31.03 % (3347534)Time elapsed: 0.360 s % 214.25/31.03 % (3347534)Peak memory usage: 113 MB % 214.25/31.03 % (3347534)Instructions burned: 542 (million) % 214.25/31.03 % (3347536)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=2965812068:i=100512:doe=on:fgj=on:bd=all:fsd=on_2746 on theBenchmark for (2746ds/100512Mi) % 214.25/31.03 % (3347536)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 214.25/31.03 % (3347536)------------------------------ % 214.25/31.03 % (3347536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.25/31.03 % (3347536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.25/31.03 % (3347536)CaDiCaL version: 2.1.3 % 214.25/31.03 % (3347536)Termination reason: Unknown % 214.25/31.03 % (3347536)Termination phase: Saturation % 214.25/31.03 % (3347536)Time elapsed: 0.358 s % 214.25/31.03 % (3347536)Peak memory usage: 114 MB % 214.25/31.03 % (3347536)Instructions burned: 543 (million) % 214.25/31.03 % (3347538)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=2664306080:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2741 on theBenchmark for (2741ds/138761Mi) % 214.25/31.03 % (3347538)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 214.25/31.03 % (3347538)------------------------------ % 214.25/31.03 % (3347538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.25/31.03 % (3347538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.25/31.03 % (3347538)CaDiCaL version: 2.1.3 % 214.25/31.03 % (3347538)Termination reason: Unknown % 214.25/31.03 % (3347538)Termination phase: Saturation % 214.25/31.03 % (3347538)Time elapsed: 0.361 s % 214.25/31.03 % (3347538)Peak memory usage: 114 MB % 214.25/31.03 % (3347538)Instructions burned: 543 (million) % 214.25/31.03 % (3347540)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=1019741740:i=282386:rtra=on_2735 on theBenchmark for (2735ds/282386Mi) % 214.25/31.03 % (3347540)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 214.25/31.03 % (3347540)------------------------------ % 214.25/31.03 % (3347540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.25/31.03 % (3347540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.25/31.03 % (3347540)CaDiCaL version: 2.1.3 % 214.25/31.03 % (3347540)Termination reason: Unknown % 214.25/31.03 % (3347540)Termination phase: Saturation % 214.25/31.03 % (3347540)Time elapsed: 0.360 s % 214.25/31.03 % (3347540)Peak memory usage: 114 MB % 214.25/31.03 % (3347540)Instructions burned: 543 (million) % 222.50/32.05 % (3347542)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=738315785:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2730 on theBenchmark for (2730ds/269354Mi) % 222.50/32.05 % (3347542)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 222.50/32.05 % (3347542)------------------------------ % 222.50/32.05 % (3347542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.50/32.05 % (3347542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.50/32.05 % (3347542)CaDiCaL version: 2.1.3 % 222.50/32.05 % (3347542)Termination reason: Unknown % 222.50/32.05 % (3347542)Termination phase: Saturation % 222.50/32.05 % (3347542)Time elapsed: 0.365 s % 222.50/32.05 % (3347542)Peak memory usage: 114 MB % 222.50/32.05 % (3347542)Instructions burned: 549 (million) % 222.50/32.05 % (3347544)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=2185089883:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2725 on theBenchmark for (2725ds/283390Mi) % 222.50/32.05 % (3347544)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 222.50/32.05 % (3347544)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 222.50/32.05 % (3347544)------------------------------ % 222.50/32.05 % (3347544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.50/32.05 % (3347544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.50/32.05 % (3347544)CaDiCaL version: 2.1.3 % 222.50/32.05 % (3347544)Termination reason: Unknown % 222.50/32.05 % (3347544)Termination phase: Saturation % 222.50/32.05 % (3347544)Time elapsed: 0.361 s % 222.50/32.05 % (3347544)Peak memory usage: 114 MB % 222.50/32.05 % (3347544)Instructions burned: 544 (million) % 222.50/32.05 % (3347546)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2878055433:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2719 on theBenchmark for (2719ds/218Mi) % 222.50/32.05 % (3347546)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 222.50/32.05 % (3347546)Refutation not found, incomplete strategy % 222.50/32.05 % (3347546)------------------------------ % 222.50/32.05 % (3347546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.50/32.05 % (3347546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.50/32.05 % (3347546)CaDiCaL version: 2.1.3 % 222.50/32.05 % (3347546)Termination reason: Refutation not found, incomplete strategy % 222.50/32.05 % (3347546)Time elapsed: 0.004 s % 222.50/32.05 % (3347546)Peak memory usage: 89 MB % 222.50/32.05 % (3347546)Instructions burned: 5 (million) % 222.50/32.05 % (3347546)------------------------------ % 222.50/32.05 % (3347546)------------------------------ % 222.50/32.05 % (3347548)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=321542744:i=238:av=off:rtra=on:ss=axioms_2715 on theBenchmark for (2715ds/238Mi) % 222.50/32.05 % (3347548)Instruction limit reached! % 222.50/32.05 % (3347548)------------------------------ % 222.50/32.05 % (3347548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.50/32.05 % (3347548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.50/32.05 % (3347548)CaDiCaL version: 2.1.3 % 222.50/32.05 % (3347548)Termination reason: Instruction limit % 222.50/32.05 % (3347548)Termination phase: Saturation % 222.50/32.05 % (3347548)Time elapsed: 0.132 s % 222.50/32.05 % (3347548)Peak memory usage: 89 MB % 222.50/32.05 % (3347548)Instructions burned: 238 (million) % 222.50/32.05 % (3347577)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=2077401341:s2a=on:i=278:rtra=on:gtg=position_2712 on theBenchmark for (2712ds/278Mi) % 222.50/32.05 % (3347577)Instruction limit reached! % 222.50/32.05 % (3347577)------------------------------ % 222.50/32.05 % (3347577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.50/32.05 % (3347577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.50/32.05 % (3347577)CaDiCaL version: 2.1.3 % 222.50/32.05 % (3347577)Termination reason: Instruction limit % 222.50/32.05 % (3347577)Termination phase: Saturation % 222.50/32.05 % (3347577)Time elapsed: 0.167 s % 222.50/32.05 % (3347577)Peak memory usage: 91 MB % 222.50/32.05 % (3347577)Instructions burned: 280 (million) % 222.50/32.05 % (3347591)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=317887003:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2709 on theBenchmark for (2709ds/258Mi) % 230.97/33.31 % (3347504)Instruction limit reached! % 230.97/33.31 % (3347504)------------------------------ % 230.97/33.31 % (3347504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.97/33.31 % (3347504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.97/33.31 % (3347504)CaDiCaL version: 2.1.3 % 230.97/33.31 % (3347504)Termination reason: Instruction limit % 230.97/33.31 % (3347504)Termination phase: Saturation % 230.97/33.31 % (3347504)Time elapsed: 12.451 s % 230.97/33.31 % (3347504)Peak memory usage: 192 MB % 230.97/33.31 % (3347504)Instructions burned: 21162 (million) % 230.97/33.31 % (3347591)Instruction limit reached! % 230.97/33.31 % (3347591)------------------------------ % 230.97/33.31 % (3347591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.97/33.31 % (3347591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.97/33.31 % (3347591)CaDiCaL version: 2.1.3 % 230.97/33.31 % (3347591)Termination reason: Instruction limit % 230.97/33.31 % (3347591)Termination phase: Saturation % 230.97/33.31 % (3347591)Time elapsed: 0.154 s % 230.97/33.31 % (3347591)Peak memory usage: 91 MB % 230.97/33.31 % (3347591)Instructions burned: 259 (million) % 230.97/33.31 % (3347593)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3787901482:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2707 on theBenchmark for (2707ds/570Mi) % 230.97/33.31 % (3347594)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=2972828890:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2706 on theBenchmark for (2706ds/314Mi) % 230.97/33.31 % (3347594)Instruction limit reached! % 230.97/33.31 % (3347594)------------------------------ % 230.97/33.31 % (3347594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.97/33.31 % (3347594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.97/33.31 % (3347594)CaDiCaL version: 2.1.3 % 230.97/33.31 % (3347594)Termination reason: Instruction limit % 230.97/33.31 % (3347594)Termination phase: Saturation % 230.97/33.31 % (3347594)Time elapsed: 0.160 s % 230.97/33.31 % (3347594)Peak memory usage: 90 MB % 230.97/33.31 % (3347594)Instructions burned: 316 (million) % 230.97/33.31 % (3347593)Instruction limit reached! % 230.97/33.31 % (3347593)------------------------------ % 230.97/33.31 % (3347593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.97/33.31 % (3347593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.97/33.31 % (3347593)CaDiCaL version: 2.1.3 % 230.97/33.31 % (3347593)Termination reason: Instruction limit % 230.97/33.31 % (3347593)Termination phase: Saturation % 230.97/33.31 % (3347593)Time elapsed: 0.320 s % 230.97/33.31 % (3347593)Peak memory usage: 94 MB % 230.97/33.31 % (3347593)Instructions burned: 571 (million) % 230.97/33.31 % (3347597)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=389959360:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2702 on theBenchmark for (2702ds/650Mi) % 230.97/33.31 % (3347598)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=2224830285:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2702 on theBenchmark for (2702ds/496Mi) % 230.97/33.31 % (3347597)Instruction limit reached! % 230.97/33.31 % (3347597)------------------------------ % 230.97/33.31 % (3347597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.97/33.31 % (3347597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.97/33.31 % (3347597)CaDiCaL version: 2.1.3 % 230.97/33.31 % (3347597)Termination reason: Instruction limit % 230.97/33.31 % (3347597)Termination phase: Saturation % 230.97/33.31 % (3347597)Time elapsed: 0.302 s % 230.97/33.31 % (3347597)Peak memory usage: 90 MB % 230.97/33.31 % (3347597)Instructions burned: 651 (million) % 230.97/33.31 % (3347598)Instruction limit reached! % 230.97/33.31 % (3347598)------------------------------ % 230.97/33.31 % (3347598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.97/33.31 % (3347598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.97/33.31 % (3347598)CaDiCaL version: 2.1.3 % 230.97/33.31 % (3347598)Termination reason: Instruction limit % 230.97/33.31 % (3347598)Termination phase: Saturation % 230.97/33.31 % (3347598)Time elapsed: 0.287 s % 230.97/33.31 % (3347598)Peak memory usage: 93 MB % 230.97/33.31 % (3347598)Instructions burned: 496 (million) % 230.97/33.31 % (3347601)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=1476195008:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2698 on theBenchmark for (2698ds/588Mi) % 230.97/33.31 % (3347601)Refutation not found, incomplete strategy % 230.97/33.31 % (3347601)------------------------------ % 234.53/34.01 % (3347601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.53/34.01 % (3347601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.53/34.01 % (3347601)CaDiCaL version: 2.1.3 % 234.53/34.01 % (3347601)Termination reason: Refutation not found, incomplete strategy % 234.53/34.01 % (3347601)Time elapsed: 0.008 s % 234.53/34.01 % (3347601)Peak memory usage: 89 MB % 234.53/34.01 % (3347601)Instructions burned: 11 (million) % 234.53/34.01 % (3347602)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=4226083184:i=4700:rtra=on_2697 on theBenchmark for (2697ds/4700Mi) % 234.53/34.01 % (3347601)------------------------------ % 234.53/34.01 % (3347601)------------------------------ % 234.53/34.01 % (3347605)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1570073444:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2693 on theBenchmark for (2693ds/226Mi) % 234.53/34.01 % (3347602)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 234.53/34.01 % (3347602)------------------------------ % 234.53/34.01 % (3347602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.53/34.01 % (3347602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.53/34.01 % (3347602)CaDiCaL version: 2.1.3 % 234.53/34.01 % (3347602)Termination reason: Unknown % 234.53/34.01 % (3347602)Termination phase: Saturation % 234.53/34.01 % (3347602)Time elapsed: 0.514 s % 234.53/34.01 % (3347602)Peak memory usage: 114 MB % 234.53/34.01 % (3347602)Instructions burned: 543 (million) % 234.53/34.01 % (3347605)Instruction limit reached! % 234.53/34.01 % (3347605)------------------------------ % 234.53/34.01 % (3347605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.53/34.01 % (3347605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.53/34.01 % (3347605)CaDiCaL version: 2.1.3 % 234.53/34.01 % (3347605)Termination reason: Instruction limit % 234.53/34.01 % (3347605)Termination phase: Saturation % 234.53/34.01 % (3347605)Time elapsed: 0.144 s % 234.53/34.01 % (3347605)Peak memory usage: 91 MB % 234.53/34.01 % (3347605)Instructions burned: 226 (million) % 234.53/34.01 % (3347607)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=130063823:i=254:av=off:fsr=off:rtra=on:sup=off_2691 on theBenchmark for (2691ds/254Mi) % 234.53/34.01 % (3347607)Refutation not found, incomplete strategy % 234.53/34.01 % (3347607)------------------------------ % 234.53/34.01 % (3347607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.53/34.01 % (3347607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.53/34.01 % (3347607)CaDiCaL version: 2.1.3 % 234.53/34.01 % (3347607)Termination reason: Refutation not found, incomplete strategy % 234.53/34.01 % (3347607)Time elapsed: 0.008 s % 234.53/34.01 % (3347607)Peak memory usage: 88 MB % 234.53/34.01 % (3347607)Instructions burned: 13 (million) % 234.53/34.01 % (3347608)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=742765719:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2690 on theBenchmark for (2690ds/228Mi) % 234.53/34.01 % (3347608)Refutation not found, incomplete strategy % 234.53/34.01 % (3347608)------------------------------ % 234.53/34.01 % (3347608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.53/34.01 % (3347608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.53/34.01 % (3347608)CaDiCaL version: 2.1.3 % 234.53/34.01 % (3347608)Termination reason: Refutation not found, incomplete strategy % 234.53/34.01 % (3347608)Time elapsed: 0.005 s % 234.53/34.01 % (3347608)Peak memory usage: 88 MB % 234.53/34.01 % (3347608)Instructions burned: 8 (million) % 234.53/34.01 % (3347508)Instruction limit reached! % 234.53/34.01 % (3347508)------------------------------ % 234.53/34.01 % (3347508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.53/34.01 % (3347508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.53/34.01 % (3347508)CaDiCaL version: 2.1.3 % 234.53/34.01 % (3347508)Termination reason: Instruction limit % 234.53/34.01 % (3347508)Termination phase: Saturation % 234.53/34.01 % (3347508)Time elapsed: 13.642 s % 234.53/34.01 % (3347508)Peak memory usage: 156 MB % 234.53/34.01 % (3347508)Instructions burned: 23715 (million) % 234.53/34.01 % (3347607)------------------------------ % 234.53/34.01 % (3347607)------------------------------ % 234.53/34.01 % (3347611)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1189850464:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2688 on theBenchmark for (2688ds/1814Mi) % 240.67/34.71 % (3347608)------------------------------ % 240.67/34.71 % (3347608)------------------------------ % 240.67/34.71 % (3347612)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=2373310504:i=874:sd=1:aac=none:rtra=on:ss=included_2687 on theBenchmark for (2687ds/874Mi) % 240.67/34.71 % (3347612)Refutation not found, incomplete strategy % 240.67/34.71 % (3347612)------------------------------ % 240.67/34.71 % (3347612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.67/34.71 % (3347612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.71 % (3347612)CaDiCaL version: 2.1.3 % 240.67/34.71 % (3347612)Termination reason: Refutation not found, incomplete strategy % 240.67/34.71 % (3347612)Time elapsed: 0.008 s % 240.67/34.71 % (3347612)Peak memory usage: 89 MB % 240.67/34.71 % (3347612)Instructions burned: 13 (million) % 240.67/34.71 % (3347614)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=1954204426:i=10404:rtra=on:ss=axioms:sgt=16_2685 on theBenchmark for (2685ds/10404Mi) % 240.67/34.71 % (3347612)------------------------------ % 240.67/34.71 % (3347612)------------------------------ % 240.67/34.71 % (3347614)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 240.67/34.71 % (3347614)------------------------------ % 240.67/34.71 % (3347614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.67/34.71 % (3347614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.71 % (3347614)CaDiCaL version: 2.1.3 % 240.67/34.71 % (3347614)Termination reason: Unknown % 240.67/34.71 % (3347614)Termination phase: Saturation % 240.67/34.71 % (3347614)Time elapsed: 0.368 s % 240.67/34.71 % (3347614)Peak memory usage: 114 MB % 240.67/34.71 % (3347614)Instructions burned: 545 (million) % 240.67/34.71 % (3347617)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1212969820:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2682 on theBenchmark for (2682ds/268Mi) % 240.67/34.71 % (3347617)Instruction limit reached! % 240.67/34.71 % (3347617)------------------------------ % 240.67/34.71 % (3347617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.67/34.71 % (3347617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.71 % (3347617)CaDiCaL version: 2.1.3 % 240.67/34.71 % (3347617)Termination reason: Instruction limit % 240.67/34.71 % (3347617)Termination phase: Saturation % 240.67/34.71 % (3347617)Time elapsed: 0.140 s % 240.67/34.71 % (3347617)Peak memory usage: 91 MB % 240.67/34.71 % (3347617)Instructions burned: 268 (million) % 240.67/34.71 % (3347618)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=137371962:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2680 on theBenchmark for (2680ds/1184Mi) % 240.67/34.71 % (3347618)Refutation not found, incomplete strategy % 240.67/34.71 % (3347618)------------------------------ % 240.67/34.71 % (3347618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.67/34.71 % (3347618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.71 % (3347618)CaDiCaL version: 2.1.3 % 240.67/34.71 % (3347618)Termination reason: Refutation not found, incomplete strategy % 240.67/34.71 % (3347618)Time elapsed: 0.008 s % 240.67/34.71 % (3347618)Peak memory usage: 88 MB % 240.67/34.71 % (3347618)Instructions burned: 13 (million) % 240.67/34.71 % (3347620)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=1527966097:st=3:i=26386:sd=3:rtra=on:ss=axioms_2679 on theBenchmark for (2679ds/26386Mi) % 240.67/34.71 % (3347618)------------------------------ % 240.67/34.71 % (3347618)------------------------------ % 240.67/34.71 % (3347611)Instruction limit reached! % 240.67/34.71 % (3347611)------------------------------ % 240.67/34.71 % (3347611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.67/34.71 % (3347611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.67/34.71 % (3347611)CaDiCaL version: 2.1.3 % 240.67/34.71 % (3347611)Termination reason: Instruction limit % 240.67/34.71 % (3347611)Termination phase: Saturation % 240.67/34.71 % (3347611)Time elapsed: 1.031 s % 240.67/34.71 % (3347611)Peak memory usage: 100 MB % 240.67/34.71 % (3347611)Instructions burned: 1815 (million) % 240.67/34.71 % (3347623)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:si=on:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2365984117:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2676 on theBenchmark for (2676ds/250Mi) % 240.67/34.71 % (3347624)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=613162531:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2676 on theBenchmark for (2676ds/268Mi) % 247.07/35.79 % (3347623)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 247.07/35.79 % (3347620)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 247.07/35.79 % (3347620)------------------------------ % 247.07/35.79 % (3347620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.07/35.79 % (3347620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.07/35.79 % (3347620)CaDiCaL version: 2.1.3 % 247.07/35.79 % (3347620)Termination reason: Unknown % 247.07/35.79 % (3347620)Termination phase: Saturation % 247.07/35.79 % (3347620)Time elapsed: 0.390 s % 247.07/35.79 % (3347620)Peak memory usage: 114 MB % 247.07/35.79 % (3347620)Instructions burned: 544 (million) % 247.07/35.79 % (3347624)Instruction limit reached! % 247.07/35.79 % (3347624)------------------------------ % 247.07/35.79 % (3347624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.07/35.79 % (3347624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.07/35.79 % (3347624)CaDiCaL version: 2.1.3 % 247.07/35.79 % (3347624)Termination reason: Instruction limit % 247.07/35.79 % (3347624)Termination phase: Saturation % 247.07/35.79 % (3347624)Time elapsed: 0.138 s % 247.07/35.79 % (3347624)Peak memory usage: 90 MB % 247.07/35.79 % (3347624)Instructions burned: 269 (million) % 247.07/35.79 % (3347623)Instruction limit reached! % 247.07/35.79 % (3347623)------------------------------ % 247.07/35.79 % (3347623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.07/35.79 % (3347623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.07/35.79 % (3347623)CaDiCaL version: 2.1.3 % 247.07/35.79 % (3347623)Termination reason: Instruction limit % 247.07/35.79 % (3347623)Termination phase: Saturation % 247.07/35.79 % (3347623)Time elapsed: 0.153 s % 247.07/35.79 % (3347623)Peak memory usage: 91 MB % 247.07/35.79 % (3347623)Instructions burned: 250 (million) % 247.07/35.79 % (3347627)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1805681477:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2673 on theBenchmark for (2673ds/282Mi) % 247.07/35.79 % (3347627)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 247.07/35.79 % (3347627)Refutation not found, incomplete strategy % 247.07/35.79 % (3347627)------------------------------ % 247.07/35.79 % (3347627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.07/35.79 % (3347627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.07/35.79 % (3347627)CaDiCaL version: 2.1.3 % 247.07/35.79 % (3347627)Termination reason: Refutation not found, incomplete strategy % 247.07/35.79 % (3347627)Time elapsed: 0.003 s % 247.07/35.79 % (3347627)Peak memory usage: 88 MB % 247.07/35.79 % (3347627)Instructions burned: 3 (million) % 247.07/35.79 % (3347628)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=4233780450:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2672 on theBenchmark for (2672ds/862Mi) % 247.07/35.79 % (3347629)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:si=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1310009553:i=12120:aac=none:ins=25:rtra=on_2672 on theBenchmark for (2672ds/12120Mi) % 247.07/35.79 % (3347627)------------------------------ % 247.07/35.79 % (3347627)------------------------------ % 247.07/35.79 % (3347633)lrs+10_16_anc=all:slsqr=32,1:sil=8000:si=on:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3454595038:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2669 on theBenchmark for (2669ds/300Mi) % 247.07/35.79 % (3347633)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 247.07/35.79 % (3347629)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 247.07/35.79 % (3347629)------------------------------ % 247.07/35.79 % (3347629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 247.07/35.79 % (3347629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.07/35.79 % (3347629)CaDiCaL version: 2.1.3 % 247.07/35.79 % (3347629)Termination reason: Unknown % 247.07/35.79 % (3347629)Termination phase: Saturation % 247.07/35.79 % (3347629)Time elapsed: 0.366 s % 247.07/35.79 % (3347629)Peak memory usage: 114 MB % 257.71/37.09 % (3347629)Instructions burned: 543 (million) % 257.71/37.09 % (3347628)Instruction limit reached! % 257.71/37.09 % (3347628)------------------------------ % 257.71/37.09 % (3347628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.71/37.09 % (3347628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.71/37.09 % (3347628)CaDiCaL version: 2.1.3 % 257.71/37.09 % (3347628)Termination reason: Instruction limit % 257.71/37.09 % (3347628)Termination phase: Saturation % 257.71/37.09 % (3347628)Time elapsed: 0.432 s % 257.71/37.09 % (3347628)Peak memory usage: 95 MB % 257.71/37.09 % (3347628)Instructions burned: 862 (million) % 257.71/37.09 % (3347633)Instruction limit reached! % 257.71/37.09 % (3347633)------------------------------ % 257.71/37.09 % (3347633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.71/37.09 % (3347633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.71/37.09 % (3347633)CaDiCaL version: 2.1.3 % 257.71/37.09 % (3347633)Termination reason: Instruction limit % 257.71/37.09 % (3347633)Termination phase: Saturation % 257.71/37.09 % (3347633)Time elapsed: 0.194 s % 257.71/37.09 % (3347633)Peak memory usage: 93 MB % 257.71/37.09 % (3347633)Instructions burned: 301 (million) % 257.71/37.09 % (3347635)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=118768823:i=28310:bd=all:rtra=on_2666 on theBenchmark for (2666ds/28310Mi) % 257.71/37.09 % (3347636)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2417949947:i=1334:av=off:fsr=off:rtra=on_2666 on theBenchmark for (2666ds/1334Mi) % 257.71/37.09 % (3347636)Refutation not found, incomplete strategy % 257.71/37.09 % (3347636)------------------------------ % 257.71/37.09 % (3347636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.71/37.09 % (3347636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.71/37.09 % (3347636)CaDiCaL version: 2.1.3 % 257.71/37.09 % (3347636)Termination reason: Refutation not found, incomplete strategy % 257.71/37.09 % (3347636)Time elapsed: 0.008 s % 257.71/37.09 % (3347636)Peak memory usage: 88 MB % 257.71/37.09 % (3347636)Instructions burned: 13 (million) % 257.71/37.09 % (3347637)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:si=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2211718886:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2665 on theBenchmark for (2665ds/370Mi) % 257.71/37.09 % (3347636)------------------------------ % 257.71/37.09 % (3347636)------------------------------ % 257.71/37.09 % (3347635)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 257.71/37.09 % (3347635)------------------------------ % 257.71/37.09 % (3347635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.71/37.09 % (3347635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.71/37.09 % (3347635)CaDiCaL version: 2.1.3 % 257.71/37.09 % (3347635)Termination reason: Unknown % 257.71/37.09 % (3347635)Termination phase: Saturation % 257.71/37.09 % (3347635)Time elapsed: 0.366 s % 257.71/37.09 % (3347635)Peak memory usage: 114 MB % 257.71/37.09 % (3347635)Instructions burned: 543 (million) % 257.71/37.09 % (3347637)Instruction limit reached! % 257.71/37.09 % (3347637)------------------------------ % 257.71/37.09 % (3347637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.71/37.09 % (3347637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.71/37.09 % (3347637)CaDiCaL version: 2.1.3 % 257.71/37.09 % (3347637)Termination reason: Instruction limit % 257.71/37.09 % (3347637)Termination phase: Saturation % 257.71/37.09 % (3347637)Time elapsed: 0.234 s % 257.71/37.09 % (3347637)Peak memory usage: 93 MB % 257.71/37.09 % (3347637)Instructions burned: 370 (million) % 257.71/37.09 % (3347641)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=4207639499:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2662 on theBenchmark for (2662ds/386Mi) % 257.71/37.09 % (3347642)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=817454971:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2661 on theBenchmark for (2661ds/9700Mi) % 257.71/37.09 % (3347642)Refutation not found, incomplete strategy % 257.71/37.09 % (3347642)------------------------------ % 257.71/37.09 % (3347642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.71/37.09 % (3347642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.71/37.09 % (3347642)CaDiCaL version: 2.1.3 % 268.87/38.72 % (3347642)Termination reason: Refutation not found, incomplete strategy % 268.87/38.72 % (3347642)Time elapsed: 0.007 s % 268.87/38.72 % (3347642)Peak memory usage: 88 MB % 268.87/38.72 % (3347642)Instructions burned: 11 (million) % 268.87/38.72 % (3347643)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:random_seed=4125124590:i=24222:sd=1:rtra=on:ss=included_2661 on theBenchmark for (2661ds/24222Mi) % 268.87/38.72 % (3347641)Instruction limit reached! % 268.87/38.72 % (3347641)------------------------------ % 268.87/38.72 % (3347641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.87/38.72 % (3347641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.87/38.72 % (3347641)CaDiCaL version: 2.1.3 % 268.87/38.72 % (3347641)Termination reason: Instruction limit % 268.87/38.72 % (3347641)Termination phase: Saturation % 268.87/38.72 % (3347641)Time elapsed: 0.209 s % 268.87/38.72 % (3347641)Peak memory usage: 91 MB % 268.87/38.72 % (3347641)Instructions burned: 386 (million) % 268.87/38.72 % (3347642)------------------------------ % 268.87/38.72 % (3347642)------------------------------ % 268.87/38.72 % (3347647)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=2390401127:i=638:kws=precedence:fsr=off:rtra=on_2658 on theBenchmark for (2658ds/638Mi) % 268.87/38.72 % (3347643)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 268.87/38.72 % (3347643)------------------------------ % 268.87/38.72 % (3347643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.87/38.72 % (3347643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.87/38.72 % (3347643)CaDiCaL version: 2.1.3 % 268.87/38.72 % (3347643)Termination reason: Unknown % 268.87/38.72 % (3347643)Termination phase: Saturation % 268.87/38.72 % (3347643)Time elapsed: 0.365 s % 268.87/38.72 % (3347643)Peak memory usage: 114 MB % 268.87/38.72 % (3347643)Instructions burned: 543 (million) % 268.87/38.72 % (3347648)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4160644196:i=4128:ep=RST:rtra=on_2657 on theBenchmark for (2657ds/4128Mi) % 268.87/38.72 % (3347648)Refutation not found, incomplete strategy % 268.87/38.72 % (3347648)------------------------------ % 268.87/38.72 % (3347648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.87/38.72 % (3347648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.87/38.72 % (3347648)CaDiCaL version: 2.1.3 % 268.87/38.72 % (3347648)Termination reason: Refutation not found, incomplete strategy % 268.87/38.72 % (3347648)Time elapsed: 0.008 s % 268.87/38.72 % (3347648)Peak memory usage: 88 MB % 268.87/38.72 % (3347648)Instructions burned: 13 (million) % 268.87/38.72 % (3347650)dis-1011_128_sil=32000:si=on:random_seed=333201902:i=7412:ep=RST:av=off:rtra=on_2655 on theBenchmark for (2655ds/7412Mi) % 268.87/38.72 % (3347647)Instruction limit reached! % 268.87/38.72 % (3347647)------------------------------ % 268.87/38.72 % (3347647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.87/38.72 % (3347647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.87/38.72 % (3347647)CaDiCaL version: 2.1.3 % 268.87/38.72 % (3347647)Termination reason: Instruction limit % 268.87/38.72 % (3347647)Termination phase: Saturation % 268.87/38.72 % (3347647)Time elapsed: 0.373 s % 268.87/38.72 % (3347647)Peak memory usage: 96 MB % 268.87/38.72 % (3347647)Instructions burned: 638 (million) % 268.87/38.72 % (3347648)------------------------------ % 268.87/38.72 % (3347648)------------------------------ % 268.87/38.72 % (3347653)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1906561357:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2653 on theBenchmark for (2653ds/1514Mi) % 268.87/38.72 % (3347654)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=3820673955:i=27826:rtra=on:ss=axioms:sgt=8_2652 on theBenchmark for (2652ds/27826Mi) % 268.87/38.72 % (3347653)Refutation not found, incomplete strategy % 268.87/38.72 % (3347653)------------------------------ % 268.87/38.72 % (3347653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 268.87/38.72 % (3347653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 268.87/38.72 % (3347653)CaDiCaL version: 2.1.3 % 268.87/38.72 % (3347653)Termination reason: Refutation not found, incomplete strategy % 268.87/38.72 % (3347653)Time elapsed: 0.011 s % 268.87/38.72 % (3347653)Peak memory usage: 89 MB % 268.87/38.72 % (3347653)Instructions burned: 16 (million) % 268.87/38.72 % (3347653)------------------------------ % 273.42/39.40 % (3347653)------------------------------ % 273.42/39.40 % (3347654)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 273.42/39.40 % (3347654)------------------------------ % 273.42/39.40 % (3347654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.42/39.40 % (3347654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.42/39.40 % (3347654)CaDiCaL version: 2.1.3 % 273.42/39.40 % (3347654)Termination reason: Unknown % 273.42/39.40 % (3347654)Termination phase: Saturation % 273.42/39.40 % (3347654)Time elapsed: 0.363 s % 273.42/39.40 % (3347654)Peak memory usage: 113 MB % 273.42/39.40 % (3347654)Instructions burned: 541 (million) % 273.42/39.40 % (3347657)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=176332334:i=19850:aac=none:rtra=on_2648 on theBenchmark for (2648ds/19850Mi) % 273.42/39.40 % (3347658)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=96892621:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2647 on theBenchmark for (2647ds/4958Mi) % 273.42/39.40 % (3347658)Refutation not found, incomplete strategy % 273.42/39.40 % (3347658)------------------------------ % 273.42/39.40 % (3347658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.42/39.40 % (3347658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.42/39.40 % (3347658)CaDiCaL version: 2.1.3 % 273.42/39.40 % (3347658)Termination reason: Refutation not found, incomplete strategy % 273.42/39.40 % (3347658)Time elapsed: 0.005 s % 273.42/39.40 % (3347658)Peak memory usage: 88 MB % 273.42/39.40 % (3347658)Instructions burned: 7 (million) % 273.42/39.40 % (3347658)------------------------------ % 273.42/39.40 % (3347658)------------------------------ % 273.42/39.40 % (3347657)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 273.42/39.40 % (3347657)------------------------------ % 273.42/39.40 % (3347657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.42/39.40 % (3347657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.42/39.40 % (3347657)CaDiCaL version: 2.1.3 % 273.42/39.40 % (3347657)Termination reason: Unknown % 273.42/39.40 % (3347657)Termination phase: Saturation % 273.42/39.40 % (3347657)Time elapsed: 0.364 s % 273.42/39.40 % (3347657)Peak memory usage: 114 MB % 273.42/39.40 % (3347657)Instructions burned: 543 (million) % 273.42/39.40 % (3347661)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=3784253818:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2643 on theBenchmark for (2643ds/880Mi) % 273.42/39.40 % (3347662)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:si=on:erd=off:lsd=100:bsr=unit_only:random_seed=1600610006:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2643 on theBenchmark for (2643ds/22290Mi) % 273.42/39.40 % (3347661)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 273.42/39.40 % (3347662)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 273.42/39.40 % (3347662)------------------------------ % 273.42/39.40 % (3347662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.42/39.40 % (3347662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.42/39.40 % (3347662)CaDiCaL version: 2.1.3 % 273.42/39.40 % (3347662)Termination reason: Unknown % 273.42/39.40 % (3347662)Termination phase: Saturation % 273.42/39.40 % (3347662)Time elapsed: 0.360 s % 273.42/39.40 % (3347662)Peak memory usage: 114 MB % 273.42/39.40 % (3347662)Instructions burned: 542 (million) % 273.42/39.40 % (3347661)Instruction limit reached! % 273.42/39.40 % (3347661)------------------------------ % 273.42/39.40 % (3347661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 273.42/39.40 % (3347661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 273.42/39.40 % (3347661)CaDiCaL version: 2.1.3 % 273.42/39.40 % (3347661)Termination reason: Instruction limit % 273.42/39.40 % (3347661)Termination phase: Saturation % 273.42/39.40 % (3347661)Time elapsed: 0.430 s % 273.42/39.40 % (3347661)Peak memory usage: 95 MB % 273.42/39.40 % (3347661)Instructions burned: 881 (million) % 273.42/39.40 % (3347665)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1908434646:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2638 on theBenchmark for (2638ds/6068Mi) % 273.42/39.40 % (3347666)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=3673690038:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2637 on theBenchmark for (2637ds/1048Mi) % 284.39/41.02 % (3347665)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 284.39/41.02 % (3347665)------------------------------ % 284.39/41.02 % (3347665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.39/41.02 % (3347665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.39/41.02 % (3347665)CaDiCaL version: 2.1.3 % 284.39/41.02 % (3347665)Termination reason: Unknown % 284.39/41.02 % (3347665)Termination phase: Saturation % 284.39/41.02 % (3347665)Time elapsed: 0.361 s % 284.39/41.02 % (3347665)Peak memory usage: 114 MB % 284.39/41.02 % (3347665)Instructions burned: 543 (million) % 284.39/41.02 % (3347670)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=1044702653:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2632 on theBenchmark for (2632ds/2032Mi) % 284.39/41.02 % (3347666)Instruction limit reached! % 284.39/41.02 % (3347666)------------------------------ % 284.39/41.02 % (3347666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.39/41.02 % (3347666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.39/41.02 % (3347666)CaDiCaL version: 2.1.3 % 284.39/41.02 % (3347666)Termination reason: Instruction limit % 284.39/41.02 % (3347666)Termination phase: Saturation % 284.39/41.02 % (3347666)Time elapsed: 0.572 s % 284.39/41.02 % (3347666)Peak memory usage: 96 MB % 284.39/41.02 % (3347666)Instructions burned: 1049 (million) % 284.39/41.02 % (3347672)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=3007334034:i=28246:bd=preordered:ins=4:rtra=on_2630 on theBenchmark for (2630ds/28246Mi) % 284.39/41.02 % (3347672)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 284.39/41.02 % (3347672)------------------------------ % 284.39/41.02 % (3347672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.39/41.02 % (3347672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.39/41.02 % (3347672)CaDiCaL version: 2.1.3 % 284.39/41.02 % (3347672)Termination reason: Unknown % 284.39/41.02 % (3347672)Termination phase: Saturation % 284.39/41.02 % (3347672)Time elapsed: 0.361 s % 284.39/41.02 % (3347672)Peak memory usage: 114 MB % 284.39/41.02 % (3347672)Instructions burned: 543 (million) % 284.39/41.02 % (3347674)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:si=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3581499594:i=11562:kws=precedence:bd=all:rtra=on:rawr=on_2624 on theBenchmark for (2624ds/11562Mi) % 284.39/41.02 % (3347670)Instruction limit reached! % 284.39/41.02 % (3347670)------------------------------ % 284.39/41.02 % (3347670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.39/41.02 % (3347670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.39/41.02 % (3347670)CaDiCaL version: 2.1.3 % 284.39/41.02 % (3347670)Termination reason: Instruction limit % 284.39/41.02 % (3347670)Termination phase: Saturation % 284.39/41.02 % (3347670)Time elapsed: 0.988 s % 284.39/41.02 % (3347670)Peak memory usage: 93 MB % 284.39/41.02 % (3347670)Instructions burned: 2034 (million) % 284.39/41.02 % (3347432)Instruction limit reached! % 284.39/41.02 % (3347432)------------------------------ % 284.39/41.02 % (3347432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.39/41.02 % (3347432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.39/41.02 % (3347432)CaDiCaL version: 2.1.3 % 284.39/41.02 % (3347432)Termination reason: Instruction limit % 284.39/41.02 % (3347432)Termination phase: Saturation % 284.39/41.02 % (3347432)Time elapsed: 28.583 s % 284.39/41.02 % (3347432)Peak memory usage: 325 MB % 284.39/41.02 % (3347432)Instructions burned: 43698 (million) % 284.39/41.02 % (3347512)Instruction limit reached! % 284.39/41.02 % (3347512)------------------------------ % 284.39/41.02 % (3347512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.39/41.02 % (3347512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.39/41.02 % (3347512)CaDiCaL version: 2.1.3 % 284.39/41.02 % (3347512)Termination reason: Instruction limit % 284.39/41.02 % (3347512)Termination phase: Saturation % 284.39/41.02 % (3347512)Time elapsed: 16.783 s % 284.39/41.02 % (3347512)Peak memory usage: 222 MB % 284.39/41.02 % (3347512)Instructions burned: 28958 (million) % 284.39/41.02 % (3347676)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:si=on:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1824808080:i=4896:gtgl=5:bd=preordered:rtra=on:gtg=all_2621 on theBenchmark for (2621ds/4896Mi) % 297.97/42.82 % (3347677)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:si=on:lcm=reverse:random_seed=3547574926:i=6446:kws=precedence:fgj=on:av=off:rtra=on_2620 on theBenchmark for (2620ds/6446Mi) % 297.97/42.82 % (3347650)Instruction limit reached! % 297.97/42.82 % (3347650)------------------------------ % 297.97/42.82 % (3347650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.97/42.82 % (3347650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.97/42.82 % (3347650)CaDiCaL version: 2.1.3 % 297.97/42.82 % (3347650)Termination reason: Instruction limit % 297.97/42.82 % (3347650)Termination phase: Saturation % 297.97/42.82 % (3347650)Time elapsed: 3.534 s % 297.97/42.82 % (3347650)Peak memory usage: 110 MB % 297.97/42.82 % (3347650)Instructions burned: 7412 (million) % 297.97/42.82 % (3347678)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:si=on:sp=occurrence:sos=on:random_seed=1059794209:st=5.6:i=4066:sd=3:rtra=on:ss=axioms_2619 on theBenchmark for (2619ds/4066Mi) % 297.97/42.82 % (3347681)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:si=on:random_seed=219688794:i=4110:nm=16:rtra=on:gtg=position:ss=axioms:fsd=on_2618 on theBenchmark for (2618ds/4110Mi) % 297.97/42.82 % (3347676)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 297.97/42.82 % (3347676)------------------------------ % 297.97/42.82 % (3347676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.97/42.82 % (3347676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.97/42.82 % (3347676)CaDiCaL version: 2.1.3 % 297.97/42.82 % (3347676)Termination reason: Unknown % 297.97/42.82 % (3347676)Termination phase: Saturation % 297.97/42.82 % (3347676)Time elapsed: 0.365 s % 297.97/42.82 % (3347676)Peak memory usage: 114 MB % 297.97/42.82 % (3347676)Instructions burned: 546 (million) % 297.97/42.82 % (3347677)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 297.97/42.82 % (3347677)------------------------------ % 297.97/42.82 % (3347677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.97/42.82 % (3347677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.97/42.82 % (3347677)CaDiCaL version: 2.1.3 % 297.97/42.82 % (3347677)Termination reason: Unknown % 297.97/42.82 % (3347677)Termination phase: Saturation % 297.97/42.82 % (3347677)Time elapsed: 0.364 s % 297.97/42.82 % (3347677)Peak memory usage: 114 MB % 297.97/42.82 % (3347677)Instructions burned: 543 (million) % 297.97/42.82 % (3347678)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 297.97/42.82 % (3347678)------------------------------ % 297.97/42.82 % (3347678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.97/42.82 % (3347678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.97/42.82 % (3347678)CaDiCaL version: 2.1.3 % 297.97/42.82 % (3347678)Termination reason: Unknown % 297.97/42.82 % (3347678)Termination phase: Saturation % 297.97/42.82 % (3347678)Time elapsed: 0.363 s % 297.97/42.82 % (3347678)Peak memory usage: 114 MB % 297.97/42.82 % (3347678)Instructions burned: 544 (million) % 297.97/42.82 % (3347684)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:si=on:sp=const_frequency:spb=goal:acc=on:random_seed=1507478392:i=43222:sd=3:rtra=on:ss=axioms_2615 on theBenchmark for (2615ds/43222Mi) % 297.97/42.82 % (3347685)lrs+10_1_sil=8000:si=on:sp=occurrence:sos=all:lma=off:random_seed=4158200347:i=9670:sd=13:rtra=on:ss=axioms:sgt=23_2615 on theBenchmark for (2615ds/9670Mi) % 297.97/42.82 % (3347681)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 297.97/42.82 % (3347681)------------------------------ % 297.97/42.82 % (3347681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.97/42.82 % (3347681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.97/42.82 % (3347681)CaDiCaL version: 2.1.3 % 297.97/42.82 % (3347681)Termination reason: Unknown % 297.97/42.82 % (3347681)Termination phase: Saturation % 297.97/42.82 % (3347681)Time elapsed: 0.360 s % 297.97/42.82 % (3347681)Peak memory usage: 113 MB % 297.97/42.82 % (3347681)Instructions burned: 541 (million) % 297.97/42.82 % (3347686)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:si=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=597135500:st=5:i=1594:s2at=3:sd=4:bs=unit_only:av=off:rtra=on:sup=off:ss=included_2614 on theBenchmark for (2614ds/1594Mi) % 300.32/43.08 % (3347689)lrs-1011_5_sil=8000:si=on:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3262413044:i=4652:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:rtra=on:fsd=on_2613 on theBenchmark for (2613ds/4652Mi) % 300.32/43.08 % (3347689)Refutation not found, incomplete strategy % 300.32/43.08 % (3347689)------------------------------ % 300.32/43.08 % (3347689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.32/43.08 % (3347689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/43.08 % (3347689)CaDiCaL version: 2.1.3 % 300.32/43.08 % (3347689)Termination reason: Refutation not found, incomplete strategy % 300.32/43.08 % (3347689)Time elapsed: 0.012 s % 300.32/43.08 % (3347689)Peak memory usage: 89 MB % 300.32/43.08 % (3347689)Instructions burned: 17 (million) % 300.32/43.08 % (3347684)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.32/43.08 % (3347684)------------------------------ % 300.32/43.08 % (3347684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.32/43.08 % (3347684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/43.08 % (3347684)CaDiCaL version: 2.1.3 % 300.32/43.08 % (3347684)Termination reason: Unknown % 300.32/43.08 % (3347684)Termination phase: Saturation % 300.32/43.08 % (3347684)Time elapsed: 0.364 s % 300.32/43.08 % (3347684)Peak memory usage: 113 MB % 300.32/43.08 % (3347684)Instructions burned: 540 (million) % 300.32/43.08 % (3347689)------------------------------ % 300.32/43.08 % (3347689)------------------------------ % 300.32/43.08 % (3347694)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:si=on:sos=all:urr=on:br=off:random_seed=1294739557:i=12076:nm=6:rtra=on_2610 on theBenchmark for (2610ds/12076Mi) % 300.32/43.08 % (3347695)lrs+10_1_sil=32000:si=on:sp=occurrence:random_seed=1583412481:st=2:i=66668:sd=3:rtra=on:ss=included:sgt=32_2609 on theBenchmark for (2609ds/66668Mi) % 300.32/43.08 % (3347694)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.32/43.08 % (3347694)------------------------------ % 300.32/43.08 % (3347694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.32/43.08 % (3347694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/43.08 % (3347694)CaDiCaL version: 2.1.3 % 300.32/43.08 % (3347694)Termination reason: Unknown % 300.32/43.08 % (3347694)Termination phase: Saturation % 300.32/43.08 % (3347694)Time elapsed: 0.360 s % 300.32/43.08 % (3347694)Peak memory usage: 114 MB % 300.32/43.08 % (3347694)Instructions burned: 543 (million) % 300.32/43.08 % (3347698)lrs+10_4_sil=8000:plsq=on:si=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1525231330:st=3.7:s2a=on:i=2016:s2at=1.2:sd=3:bd=all:av=off:rtra=on:fdi=8:sup=off:ss=axioms_2605 on theBenchmark for (2605ds/2016Mi) % 300.32/43.08 % (3347686)Instruction limit reached! % 300.32/43.08 % (3347686)------------------------------ % 300.32/43.08 % (3347686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.32/43.08 % (3347686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/43.08 % (3347686)CaDiCaL version: 2.1.3 % 300.32/43.08 % (3347686)Termination reason: Instruction limit % 300.32/43.08 % (3347686)Termination phase: Saturation % 300.32/43.08 % (3347686)Time elapsed: 0.928 s % 300.32/43.08 % (3347686)Peak memory usage: 109 MB % 300.32/43.08 % (3347686)Instructions burned: 1595 (million) % 300.32/43.08 % (3347700)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:si=on:sp=const_frequency:spb=intro:gs=on:random_seed=3549083982:i=16654:s2at=5:bd=preordered:rtra=on_2603 on theBenchmark for (2603ds/16654Mi) % 300.32/43.08 % (3347700)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.32/43.08 % (3347700)------------------------------ % 300.32/43.08 % (3347700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.32/43.08 % (3347700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.32/43.08 % (3347700)CaDiCaL version: 2.1.3 % 300.32/43.08 % (3347700)Termination reason: Unknown % 300.32/43.08 % (3347700)Termination phase: Saturation % 300.32/43.08 % (3347700)Time elapsed: 0.360 s % 300.32/43.08 % (3347700)Peak memory usage: 114 MB % 300.32/43.08 % (3347700)Instructions burned: 543 (million) % 300.32/43.08 % (3347702)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:si=on:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=3578481282:s2a=on:i=2166:s2at=1.87328:slsql=off:ep=RST % 300.32/43.08 Terminated %------------------------------------------------------------------------------