%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV601_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 : n005.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:04 PM UTC 2026 % Result : Timeout 294.06s 42.58s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWV601_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.26 % Computer : n005.cluster.edu % 0.10/0.26 % Model : x86_64 x86_64 % 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.26 % Memory : 8046.5625MB % 0.10/0.26 % OS : Linux 6.8.0-71-generic % 0.10/0.26 % CPULimit : 300 % 0.10/0.27 % WCLimit : 300 % 0.10/0.27 % DateTime : Mon Sep 28 11:59:46 UTC 2026 % 0.10/0.27 % CPUTime : % 0.10/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.25/0.32 Running first-order theorem proving % 0.25/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.29/2.50 % (741425)Detected formulas, will run a generic FOF schedule. % 10.29/2.50 % (741433)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=2661240734:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.29/2.50 % (741436)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3034074694:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.29/2.50 % (741435)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3074018938:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.29/2.50 % (741434)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=1796992315:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.29/2.50 % (741432)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=515107279:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.29/2.50 % (741437)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2478291562:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.29/2.50 % (741435)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.29/2.50 % (741434)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 10.29/2.50 % (741438)dis-21_1_sil=8000:lcm=predicate:random_seed=3142856144:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 10.29/2.50 % (741436)Instruction limit reached! % 10.29/2.50 % (741436)------------------------------ % 10.29/2.50 % (741436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.50 % (741436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.50 % (741436)CaDiCaL version: 2.1.3 % 10.29/2.50 % (741436)Termination reason: Instruction limit % 10.29/2.50 % (741436)Termination phase: Saturation % 10.29/2.50 % (741436)Time elapsed: 0.104 s % 10.29/2.50 % (741436)Peak memory usage: 88 MB % 10.29/2.50 % (741436)Instructions burned: 119 (million) % 10.29/2.50 % (741435)Instruction limit reached! % 10.29/2.50 % (741435)------------------------------ % 10.29/2.50 % (741435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.50 % (741435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.50 % (741435)CaDiCaL version: 2.1.3 % 10.29/2.50 % (741435)Termination reason: Instruction limit % 10.29/2.50 % (741435)Termination phase: Saturation % 10.29/2.50 % (741435)Time elapsed: 0.109 s % 10.29/2.50 % (741435)Peak memory usage: 89 MB % 10.29/2.50 % (741435)Instructions burned: 109 (million) % 10.29/2.50 % (741437)Instruction limit reached! % 10.29/2.50 % (741437)------------------------------ % 10.29/2.50 % (741437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.50 % (741437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.50 % (741437)CaDiCaL version: 2.1.3 % 10.29/2.50 % (741437)Termination reason: Instruction limit % 10.29/2.50 % (741437)Termination phase: Saturation % 10.29/2.50 % (741437)Time elapsed: 0.133 s % 10.29/2.50 % (741437)Peak memory usage: 89 MB % 10.29/2.50 % (741437)Instructions burned: 139 (million) % 10.29/2.50 % (741438)Instruction limit reached! % 10.29/2.50 % (741438)------------------------------ % 10.29/2.50 % (741438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.50 % (741438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.50 % (741438)CaDiCaL version: 2.1.3 % 10.29/2.50 % (741438)Termination reason: Instruction limit % 10.29/2.50 % (741438)Termination phase: Saturation % 10.29/2.50 % (741438)Time elapsed: 0.130 s % 10.29/2.50 % (741438)Peak memory usage: 89 MB % 10.29/2.50 % (741438)Instructions burned: 129 (million) % 10.29/2.50 % (741433)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.29/2.50 % (741433)------------------------------ % 10.29/2.50 % (741433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.29/2.50 % (741433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.29/2.50 % (741433)CaDiCaL version: 2.1.3 % 10.29/2.50 % (741433)Termination reason: Unknown % 10.29/2.50 % (741433)Termination phase: Saturation % 10.29/2.50 % (741433)Time elapsed: 0.304 s % 10.29/2.50 % (741433)Peak memory usage: 113 MB % 11.57/2.81 % (741433)Instructions burned: 544 (million) % 11.57/2.81 % (741446)lrs+10_1_sil=8000:sp=occurrence:random_seed=3797515554:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 11.57/2.81 % (741446)Instruction limit reached! % 11.57/2.81 % (741446)------------------------------ % 11.57/2.81 % (741446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.81 % (741446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.81 % (741446)CaDiCaL version: 2.1.3 % 11.57/2.81 % (741446)Termination reason: Instruction limit % 11.57/2.81 % (741446)Termination phase: Saturation % 11.57/2.81 % (741446)Time elapsed: 0.139 s % 11.57/2.81 % (741446)Peak memory usage: 90 MB % 11.57/2.81 % (741446)Instructions burned: 287 (million) % 11.57/2.81 % (741447)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1278947505:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 11.57/2.81 % (741448)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1008943270:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 11.57/2.81 % (741449)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=444165748:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 11.57/2.81 % (741450)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4206978805:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 11.57/2.81 % (741447)Instruction limit reached! % 11.57/2.81 % (741447)------------------------------ % 11.57/2.81 % (741447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.81 % (741447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.81 % (741447)CaDiCaL version: 2.1.3 % 11.57/2.81 % (741447)Termination reason: Instruction limit % 11.57/2.81 % (741447)Termination phase: Saturation % 11.57/2.81 % (741447)Time elapsed: 0.147 s % 11.57/2.81 % (741447)Peak memory usage: 90 MB % 11.57/2.81 % (741447)Instructions burned: 157 (million) % 11.57/2.81 % (741434)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.57/2.81 % (741432)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.57/2.81 % (741432)------------------------------ % 11.57/2.81 % (741432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.81 % (741434)------------------------------ % 11.57/2.81 % (741434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.81 % (741432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.81 % (741434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.81 % (741432)CaDiCaL version: 2.1.3 % 11.57/2.81 % (741434)CaDiCaL version: 2.1.3 % 11.57/2.81 % (741432)Termination reason: Unknown % 11.57/2.81 % (741432)Termination phase: Saturation % 11.57/2.81 % (741434)Termination reason: Unknown % 11.57/2.81 % (741434)Termination phase: Saturation % 11.57/2.81 % (741432)Time elapsed: 0.594 s % 11.57/2.81 % (741434)Time elapsed: 0.594 s % 11.57/2.81 % (741434)Peak memory usage: 112 MB % 11.57/2.81 % (741432)Peak memory usage: 112 MB % 11.57/2.81 % (741432)Instructions burned: 541 (million) % 11.57/2.81 % (741434)Instructions burned: 541 (million) % 11.57/2.81 % (741453)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=58598211:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 11.57/2.81 % (741448)Instruction limit reached! % 11.57/2.81 % (741448)------------------------------ % 11.57/2.81 % (741448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.81 % (741448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.81 % (741448)CaDiCaL version: 2.1.3 % 11.57/2.81 % (741448)Termination reason: Instruction limit % 11.57/2.81 % (741448)Termination phase: Saturation % 11.57/2.81 % (741448)Time elapsed: 0.259 s % 11.57/2.81 % (741448)Peak memory usage: 91 MB % 11.57/2.81 % (741448)Instructions burned: 325 (million) % 11.57/2.81 % (741450)Instruction limit reached! % 11.57/2.81 % (741450)------------------------------ % 11.57/2.81 % (741450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.57/2.81 % (741450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.57/2.81 % (741450)CaDiCaL version: 2.1.3 % 11.57/2.81 % (741450)Termination reason: Instruction limit % 11.57/2.81 % (741450)Termination phase: Saturation % 11.57/2.81 % (741450)Time elapsed: 0.166 s % 11.57/2.81 % (741450)Peak memory usage: 89 MB % 11.57/2.81 % (741450)Instructions burned: 294 (million) % 16.65/3.34 % (741449)Instruction limit reached! % 16.65/3.34 % (741449)------------------------------ % 16.65/3.34 % (741449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.65/3.34 % (741449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.65/3.34 % (741449)CaDiCaL version: 2.1.3 % 16.65/3.34 % (741449)Termination reason: Instruction limit % 16.65/3.34 % (741449)Termination phase: Saturation % 16.65/3.34 % (741449)Time elapsed: 0.222 s % 16.65/3.34 % (741449)Peak memory usage: 90 MB % 16.65/3.34 % (741449)Instructions burned: 248 (million) % 16.65/3.34 % (741457)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3577108870:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi) % 16.65/3.34 % (741458)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=90475168:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi) % 16.65/3.34 % (741458)Refutation not found, incomplete strategy % 16.65/3.34 % (741458)------------------------------ % 16.65/3.34 % (741458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.65/3.34 % (741458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.65/3.34 % (741458)CaDiCaL version: 2.1.3 % 16.65/3.34 % (741458)Termination reason: Refutation not found, incomplete strategy % 16.65/3.34 % (741458)Time elapsed: 0.007 s % 16.65/3.34 % (741458)Peak memory usage: 87 MB % 16.65/3.34 % (741458)Instructions burned: 6 (million) % 16.65/3.34 % (741461)lrs+10_1_sil=8000:sp=occurrence:random_seed=4211475087:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 16.65/3.34 % (741459)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1908586798:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 16.65/3.34 % (741463)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2771640181:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi) % 16.65/3.34 % (741457)Instruction limit reached! % 16.65/3.34 % (741457)------------------------------ % 16.65/3.34 % (741457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.65/3.34 % (741457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.65/3.34 % (741457)CaDiCaL version: 2.1.3 % 16.65/3.34 % (741457)Termination reason: Instruction limit % 16.65/3.34 % (741457)Termination phase: Saturation % 16.65/3.34 % (741457)Time elapsed: 0.110 s % 16.65/3.34 % (741457)Peak memory usage: 90 MB % 16.65/3.34 % (741457)Instructions burned: 113 (million) % 16.65/3.34 % (741462)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1948171951:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 16.65/3.34 % (741459)Instruction limit reached! % 16.65/3.34 % (741459)------------------------------ % 16.65/3.34 % (741459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.65/3.34 % (741459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.65/3.34 % (741459)CaDiCaL version: 2.1.3 % 16.65/3.34 % (741459)Termination reason: Instruction limit % 16.65/3.34 % (741459)Termination phase: Saturation % 16.65/3.34 % (741459)Time elapsed: 0.099 s % 16.65/3.34 % (741459)Peak memory usage: 89 MB % 16.65/3.34 % (741459)Instructions burned: 114 (million) % 16.65/3.34 % (741469)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3682112553:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 16.65/3.34 % (741471)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1172979036:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi) % 16.65/3.34 % (741458)------------------------------ % 16.65/3.34 % (741458)------------------------------ % 16.65/3.34 % (741471)Refutation not found, incomplete strategy % 16.65/3.34 % (741471)------------------------------ % 16.65/3.34 % (741471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.65/3.34 % (741471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.65/3.34 % (741471)CaDiCaL version: 2.1.3 % 16.65/3.34 % (741471)Termination reason: Refutation not found, incomplete strategy % 16.65/3.34 % (741471)Time elapsed: 0.011 s % 16.65/3.34 % (741471)Peak memory usage: 88 MB % 16.65/3.34 % (741471)Instructions burned: 11 (million) % 16.65/3.34 % (741453)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.65/3.34 % (741453)------------------------------ % 16.65/3.34 % (741453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.32/3.74 % (741453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.32/3.74 % (741453)CaDiCaL version: 2.1.3 % 18.32/3.74 % (741453)Termination reason: Unknown % 18.32/3.74 % (741453)Termination phase: Saturation % 18.32/3.74 % (741453)Time elapsed: 0.600 s % 18.32/3.74 % (741453)Peak memory usage: 113 MB % 18.32/3.74 % (741453)Instructions burned: 541 (million) % 18.32/3.74 % (741469)Instruction limit reached! % 18.32/3.74 % (741469)------------------------------ % 18.32/3.74 % (741469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.32/3.74 % (741461)Instruction limit reached! % 18.32/3.74 % (741461)------------------------------ % 18.32/3.74 % (741461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.32/3.74 % (741461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.32/3.74 % (741469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.32/3.74 % (741461)CaDiCaL version: 2.1.3 % 18.32/3.74 % (741469)CaDiCaL version: 2.1.3 % 18.32/3.74 % (741469)Termination reason: Instruction limit % 18.32/3.74 % (741469)Termination phase: Saturation % 18.32/3.74 % (741461)Termination reason: Instruction limit % 18.32/3.74 % (741461)Termination phase: Saturation % 18.32/3.74 % (741461)Time elapsed: 0.427 s % 18.32/3.74 % (741469)Time elapsed: 0.120 s % 18.32/3.74 % (741461)Peak memory usage: 93 MB % 18.32/3.74 % (741469)Peak memory usage: 90 MB % 18.32/3.74 % (741461)Instructions burned: 908 (million) % 18.32/3.74 % (741469)Instructions burned: 136 (million) % 18.32/3.74 % (741462)Instruction limit reached! % 18.32/3.74 % (741462)------------------------------ % 18.32/3.74 % (741462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.32/3.74 % (741462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.32/3.74 % (741462)CaDiCaL version: 2.1.3 % 18.32/3.74 % (741462)Termination reason: Instruction limit % 18.32/3.74 % (741462)Termination phase: Saturation % 18.32/3.74 % (741462)Time elapsed: 0.382 s % 18.32/3.74 % (741462)Peak memory usage: 90 MB % 18.32/3.74 % (741462)Instructions burned: 437 (million) % 18.32/3.74 % (741463)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.32/3.74 % (741463)------------------------------ % 18.32/3.74 % (741463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.32/3.74 % (741463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.32/3.74 % (741463)CaDiCaL version: 2.1.3 % 18.32/3.74 % (741463)Termination reason: Unknown % 18.32/3.74 % (741463)Termination phase: Saturation % 18.32/3.74 % (741463)Time elapsed: 0.595 s % 18.32/3.74 % (741463)Peak memory usage: 113 MB % 18.32/3.74 % (741463)Instructions burned: 543 (million) % 18.32/3.74 % (741474)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2779650408:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi) % 18.32/3.74 % (741476)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1045094877:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi) % 18.32/3.74 % (741475)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=2000407867:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi) % 18.32/3.74 % (741477)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=120555377:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi) % 18.32/3.74 % (741477)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.32/3.74 % (741475)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 18.32/3.74 % (741477)Refutation not found, incomplete strategy % 18.32/3.74 % (741477)------------------------------ % 18.32/3.74 % (741477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.32/3.74 % (741477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.32/3.74 % (741477)CaDiCaL version: 2.1.3 % 18.32/3.74 % (741477)Termination reason: Refutation not found, incomplete strategy % 18.32/3.74 % (741477)Time elapsed: 0.005 s % 18.32/3.74 % (741477)Peak memory usage: 87 MB % 18.32/3.74 % (741477)Instructions burned: 2 (million) % 18.32/3.74 % (741476)Instruction limit reached! % 18.32/3.74 % (741476)------------------------------ % 18.32/3.74 % (741476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.64/4.73 % (741476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.64/4.73 % (741476)CaDiCaL version: 2.1.3 % 25.64/4.73 % (741476)Termination reason: Instruction limit % 25.64/4.73 % (741476)Termination phase: Saturation % 25.64/4.73 % (741476)Time elapsed: 0.069 s % 25.64/4.73 % (741476)Peak memory usage: 89 MB % 25.64/4.73 % (741476)Instructions burned: 136 (million) % 25.64/4.73 % (741478)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=204469400:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/431Mi) % 25.64/4.73 % (741471)------------------------------ % 25.64/4.73 % (741471)------------------------------ % 25.64/4.73 % (741478)Refutation not found, incomplete strategy % 25.64/4.73 % (741478)------------------------------ % 25.64/4.73 % (741478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.64/4.73 % (741478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.64/4.73 % (741478)CaDiCaL version: 2.1.3 % 25.64/4.73 % (741478)Termination reason: Refutation not found, incomplete strategy % 25.64/4.73 % (741478)Time elapsed: 0.011 s % 25.64/4.73 % (741478)Peak memory usage: 88 MB % 25.64/4.73 % (741478)Instructions burned: 10 (million) % 25.64/4.73 % (741475)Instruction limit reached! % 25.64/4.73 % (741475)------------------------------ % 25.64/4.73 % (741475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.64/4.73 % (741475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.64/4.73 % (741475)CaDiCaL version: 2.1.3 % 25.64/4.73 % (741475)Termination reason: Instruction limit % 25.64/4.73 % (741475)Termination phase: Saturation % 25.64/4.73 % (741475)Time elapsed: 0.121 s % 25.64/4.73 % (741475)Peak memory usage: 90 MB % 25.64/4.73 % (741475)Instructions burned: 125 (million) % 25.64/4.73 % (741479)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=1097579821:i=6060:aac=none:ins=25_2982 on theBenchmark for (2982ds/6060Mi) % 25.64/4.73 % (741484)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=1912341394:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2981 on theBenchmark for (2981ds/150Mi) % 25.64/4.73 % (741484)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 25.64/4.73 % (741484)Instruction limit reached! % 25.64/4.73 % (741484)------------------------------ % 25.64/4.73 % (741484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.64/4.73 % (741484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.64/4.73 % (741484)CaDiCaL version: 2.1.3 % 25.64/4.73 % (741484)Termination reason: Instruction limit % 25.64/4.73 % (741484)Termination phase: Saturation % 25.64/4.73 % (741484)Time elapsed: 0.081 s % 25.64/4.73 % (741484)Peak memory usage: 90 MB % 25.64/4.73 % (741484)Instructions burned: 151 (million) % 25.64/4.73 % (741487)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=303599790:i=667:av=off:fsr=off_2981 on theBenchmark for (2981ds/667Mi) % 25.64/4.73 % (741477)------------------------------ % 25.64/4.73 % (741477)------------------------------ % 25.64/4.73 % (741486)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1563205739:i=14155:bd=all_2981 on theBenchmark for (2981ds/14155Mi) % 25.64/4.73 % (741478)------------------------------ % 25.64/4.73 % (741478)------------------------------ % 25.64/4.73 % (741474)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 25.64/4.73 % (741474)------------------------------ % 25.64/4.73 % (741474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.64/4.73 % (741474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.64/4.73 % (741474)CaDiCaL version: 2.1.3 % 25.64/4.73 % (741474)Termination reason: Unknown % 25.64/4.73 % (741474)Termination phase: Saturation % 25.64/4.73 % (741474)Time elapsed: 0.598 s % 25.64/4.73 % (741474)Peak memory usage: 113 MB % 25.64/4.73 % (741474)Instructions burned: 542 (million) % 25.64/4.73 % (741493)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=3454421687:s2a=on:i=185:s2at=1.8:fdi=4_2978 on theBenchmark for (2978ds/185Mi) % 25.64/4.73 % (741496)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=962567512:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2978 on theBenchmark for (2978ds/193Mi) % 30.83/5.37 % (741493)Instruction limit reached! % 30.83/5.37 % (741493)------------------------------ % 30.83/5.37 % (741493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.83/5.37 % (741493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.83/5.37 % (741493)CaDiCaL version: 2.1.3 % 30.83/5.37 % (741493)Termination reason: Instruction limit % 30.83/5.37 % (741493)Termination phase: Saturation % 30.83/5.37 % (741493)Time elapsed: 0.096 s % 30.83/5.37 % (741493)Peak memory usage: 91 MB % 30.83/5.37 % (741493)Instructions burned: 187 (million) % 30.83/5.37 % (741496)Instruction limit reached! % 30.83/5.37 % (741496)------------------------------ % 30.83/5.37 % (741496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.83/5.37 % (741496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.83/5.37 % (741496)CaDiCaL version: 2.1.3 % 30.83/5.37 % (741496)Termination reason: Instruction limit % 30.83/5.37 % (741496)Termination phase: Saturation % 30.83/5.37 % (741496)Time elapsed: 0.115 s % 30.83/5.37 % (741496)Peak memory usage: 90 MB % 30.83/5.37 % (741496)Instructions burned: 194 (million) % 30.83/5.37 % (741498)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1015446820:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2977 on theBenchmark for (2977ds/4850Mi) % 30.83/5.37 % (741498)Refutation not found, incomplete strategy % 30.83/5.37 % (741498)------------------------------ % 30.83/5.37 % (741498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.83/5.37 % (741498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.83/5.37 % (741498)CaDiCaL version: 2.1.3 % 30.83/5.37 % (741498)Termination reason: Refutation not found, incomplete strategy % 30.83/5.37 % (741498)Time elapsed: 0.008 s % 30.83/5.37 % (741498)Peak memory usage: 87 MB % 30.83/5.37 % (741498)Instructions burned: 8 (million) % 30.83/5.37 % (741479)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 30.83/5.37 % (741479)------------------------------ % 30.83/5.37 % (741479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.83/5.37 % (741479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.83/5.37 % (741479)CaDiCaL version: 2.1.3 % 30.83/5.37 % (741479)Termination reason: Unknown % 30.83/5.37 % (741479)Termination phase: Saturation % 30.83/5.37 % (741479)Time elapsed: 0.586 s % 30.83/5.37 % (741479)Peak memory usage: 113 MB % 30.83/5.37 % (741479)Instructions burned: 541 (million) % 30.83/5.37 % (741500)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2069009173:i=12111:sd=1:ss=included_2976 on theBenchmark for (2976ds/12111Mi) % 30.83/5.37 % (741487)Instruction limit reached! % 30.83/5.37 % (741487)------------------------------ % 30.83/5.37 % (741487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.83/5.37 % (741487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.83/5.37 % (741487)CaDiCaL version: 2.1.3 % 30.83/5.37 % (741487)Termination reason: Instruction limit % 30.83/5.37 % (741487)Termination phase: Saturation % 30.83/5.37 % (741487)Time elapsed: 0.535 s % 30.83/5.37 % (741487)Peak memory usage: 88 MB % 30.83/5.37 % (741487)Instructions burned: 667 (million) % 30.83/5.37 % (741503)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=442030650:i=2064:ep=RST_2975 on theBenchmark for (2975ds/2064Mi) % 30.83/5.37 % (741502)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3221049262:i=319:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/319Mi) % 30.83/5.37 % (741503)Refutation not found, incomplete strategy % 30.83/5.37 % (741503)------------------------------ % 30.83/5.37 % (741503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.83/5.37 % (741503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.83/5.37 % (741503)CaDiCaL version: 2.1.3 % 30.83/5.37 % (741503)Termination reason: Refutation not found, incomplete strategy % 30.83/5.37 % (741503)Time elapsed: 0.006 s % 30.83/5.37 % (741503)Peak memory usage: 88 MB % 30.83/5.37 % (741503)Instructions burned: 10 (million) % 30.83/5.37 % (741486)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 30.83/5.37 % (741486)------------------------------ % 30.83/5.37 % (741486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.15/6.22 % (741486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.15/6.22 % (741486)CaDiCaL version: 2.1.3 % 37.15/6.22 % (741486)Termination reason: Unknown % 37.15/6.22 % (741486)Termination phase: Saturation % 37.15/6.22 % (741486)Time elapsed: 0.594 s % 37.15/6.22 % (741486)Peak memory usage: 113 MB % 37.15/6.22 % (741486)Instructions burned: 542 (million) % 37.15/6.22 % (741505)dis-1011_128_sil=32000:random_seed=586238548:i=3706:ep=RST:av=off_2974 on theBenchmark for (2974ds/3706Mi) % 37.15/6.22 % (741498)------------------------------ % 37.15/6.22 % (741498)------------------------------ % 37.15/6.22 % (741503)------------------------------ % 37.15/6.22 % (741503)------------------------------ % 37.15/6.22 % (741507)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2069988557:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2973 on theBenchmark for (2973ds/757Mi) % 37.15/6.22 % (741502)Instruction limit reached! % 37.15/6.22 % (741502)------------------------------ % 37.15/6.22 % (741502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.15/6.22 % (741502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.15/6.22 % (741502)CaDiCaL version: 2.1.3 % 37.15/6.22 % (741502)Termination reason: Instruction limit % 37.15/6.22 % (741502)Termination phase: Saturation % 37.15/6.22 % (741502)Time elapsed: 0.312 s % 37.15/6.22 % (741502)Peak memory usage: 92 MB % 37.15/6.22 % (741502)Instructions burned: 319 (million) % 37.15/6.22 % (741510)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1379868639:i=13913:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/13913Mi) % 37.15/6.22 % (741514)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2722969376:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2970 on theBenchmark for (2970ds/2479Mi) % 37.15/6.22 % (741500)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 37.15/6.22 % (741500)------------------------------ % 37.15/6.22 % (741500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.15/6.22 % (741500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.15/6.22 % (741500)CaDiCaL version: 2.1.3 % 37.15/6.22 % (741500)Termination reason: Unknown % 37.15/6.22 % (741500)Termination phase: Saturation % 37.15/6.22 % (741500)Time elapsed: 0.598 s % 37.15/6.22 % (741500)Peak memory usage: 113 MB % 37.15/6.22 % (741500)Instructions burned: 542 (million) % 37.15/6.22 % (741513)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=557357087:i=9925:aac=none_2970 on theBenchmark for (2970ds/9925Mi) % 37.15/6.22 % (741515)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2235406272:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2969 on theBenchmark for (2969ds/440Mi) % 37.15/6.22 % (741515)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 37.15/6.22 % (741519)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2117472701:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/11145Mi) % 37.15/6.22 % (741510)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 37.15/6.22 % (741510)------------------------------ % 37.15/6.22 % (741510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.15/6.22 % (741510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.15/6.22 % (741510)CaDiCaL version: 2.1.3 % 37.15/6.22 % (741510)Termination reason: Unknown % 37.15/6.22 % (741510)Termination phase: Saturation % 37.15/6.22 % (741510)Time elapsed: 0.590 s % 37.15/6.22 % (741510)Peak memory usage: 113 MB % 37.15/6.22 % (741510)Instructions burned: 538 (million) % 37.15/6.22 % (741507)Instruction limit reached! % 37.15/6.22 % (741507)------------------------------ % 37.15/6.22 % (741507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.15/6.22 % (741507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.15/6.22 % (741507)CaDiCaL version: 2.1.3 % 37.15/6.22 % (741507)Termination reason: Instruction limit % 37.15/6.22 % (741507)Termination phase: Saturation % 37.15/6.22 % (741507)Time elapsed: 0.729 s % 37.15/6.22 % (741507)Peak memory usage: 96 MB % 37.15/6.22 % (741507)Instructions burned: 758 (million) % 37.15/6.22 % (741515)Instruction limit reached! % 37.15/6.22 % (741515)------------------------------ % 37.15/6.22 % (741515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.97/7.69 % (741515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.97/7.69 % (741515)CaDiCaL version: 2.1.3 % 46.97/7.69 % (741515)Termination reason: Instruction limit % 46.97/7.69 % (741515)Termination phase: Saturation % 46.97/7.69 % (741515)Time elapsed: 0.434 s % 46.97/7.69 % (741515)Peak memory usage: 92 MB % 46.97/7.69 % (741515)Instructions burned: 440 (million) % 46.97/7.69 % (741513)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 46.97/7.69 % (741513)------------------------------ % 46.97/7.69 % (741513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.97/7.69 % (741513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.97/7.69 % (741513)CaDiCaL version: 2.1.3 % 46.97/7.69 % (741513)Termination reason: Unknown % 46.97/7.69 % (741513)Termination phase: Saturation % 46.97/7.69 % (741513)Time elapsed: 0.538 s % 46.97/7.69 % (741513)Peak memory usage: 113 MB % 46.97/7.69 % (741513)Instructions burned: 542 (million) % 46.97/7.69 % (741525)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=820080953:cts=off:i=3034:av=off:er=known:fsd=on_2963 on theBenchmark for (2963ds/3034Mi) % 46.97/7.69 % (741526)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2424570104:st=2:s2a=on:i=524:s2at=2:ss=axioms_2963 on theBenchmark for (2963ds/524Mi) % 46.97/7.69 % (741528)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2329958807:i=14123:bd=preordered:ins=4_2962 on theBenchmark for (2962ds/14123Mi) % 46.97/7.69 % (741527)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3422646208:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2962 on theBenchmark for (2962ds/1016Mi) % 46.97/7.69 % (741514)Instruction limit reached! % 46.97/7.69 % (741514)------------------------------ % 46.97/7.69 % (741514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.97/7.69 % (741514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.97/7.69 % (741514)CaDiCaL version: 2.1.3 % 46.97/7.69 % (741514)Termination reason: Instruction limit % 46.97/7.69 % (741514)Termination phase: Saturation % 46.97/7.69 % (741514)Time elapsed: 0.839 s % 46.97/7.69 % (741514)Peak memory usage: 94 MB % 46.97/7.69 % (741514)Instructions burned: 2481 (million) % 46.97/7.69 % (741519)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 46.97/7.69 % (741519)------------------------------ % 46.97/7.69 % (741519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.97/7.69 % (741519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.97/7.69 % (741519)CaDiCaL version: 2.1.3 % 46.97/7.69 % (741519)Termination reason: Unknown % 46.97/7.69 % (741519)Termination phase: Saturation % 46.97/7.69 % (741519)Time elapsed: 0.590 s % 46.97/7.69 % (741519)Peak memory usage: 114 MB % 46.97/7.69 % (741519)Instructions burned: 542 (million) % 46.97/7.69 % (741534)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=2375366299:i=2448:gtgl=5:bd=preordered:gtg=all_2959 on theBenchmark for (2959ds/2448Mi) % 46.97/7.69 % (741533)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1878710106:i=5781:kws=precedence:bd=all:rawr=on_2959 on theBenchmark for (2959ds/5781Mi) % 46.97/7.69 % (741528)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 46.97/7.69 % (741528)------------------------------ % 46.97/7.69 % (741528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.97/7.69 % (741528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.97/7.69 % (741528)CaDiCaL version: 2.1.3 % 46.97/7.69 % (741528)Termination reason: Unknown % 46.97/7.69 % (741528)Termination phase: Saturation % 46.97/7.69 % (741528)Time elapsed: 0.349 s % 46.97/7.69 % (741528)Peak memory usage: 113 MB % 46.97/7.69 % (741528)Instructions burned: 542 (million) % 46.97/7.69 % (741526)Instruction limit reached! % 46.97/7.69 % (741526)------------------------------ % 46.97/7.69 % (741526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.97/7.69 % (741526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.97/7.69 % (741526)CaDiCaL version: 2.1.3 % 46.97/7.69 % (741526)Termination reason: Instruction limit % 46.97/7.69 % (741526)Termination phase: Saturation % 55.21/8.95 % (741526)Time elapsed: 0.438 s % 55.21/8.95 % (741526)Peak memory usage: 91 MB % 55.21/8.95 % (741526)Instructions burned: 525 (million) % 55.21/8.95 % (741525)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 55.21/8.95 % (741525)------------------------------ % 55.21/8.95 % (741525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.21/8.95 % (741525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.21/8.95 % (741525)CaDiCaL version: 2.1.3 % 55.21/8.95 % (741525)Termination reason: Unknown % 55.21/8.95 % (741525)Termination phase: Saturation % 55.21/8.95 % (741525)Time elapsed: 0.581 s % 55.21/8.95 % (741525)Peak memory usage: 113 MB % 55.21/8.95 % (741525)Instructions burned: 541 (million) % 55.21/8.95 % (741537)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=399637544:i=3223:kws=precedence:fgj=on:av=off_2956 on theBenchmark for (2956ds/3223Mi) % 55.21/8.95 % (741538)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2622504125:st=5.6:i=2033:sd=3:ss=axioms_2956 on theBenchmark for (2956ds/2033Mi) % 55.21/8.95 % (741539)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=612011119:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2955 on theBenchmark for (2955ds/2055Mi) % 55.21/8.95 % (741527)Instruction limit reached! % 55.21/8.95 % (741527)------------------------------ % 55.21/8.95 % (741527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.21/8.95 % (741527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.21/8.95 % (741527)CaDiCaL version: 2.1.3 % 55.21/8.95 % (741527)Termination reason: Instruction limit % 55.21/8.95 % (741527)Termination phase: Saturation % 55.21/8.95 % (741527)Time elapsed: 0.831 s % 55.21/8.95 % (741527)Peak memory usage: 96 MB % 55.21/8.95 % (741527)Instructions burned: 1017 (million) % 55.21/8.95 % (741534)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 55.21/8.95 % (741534)------------------------------ % 55.21/8.95 % (741534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.21/8.95 % (741534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.21/8.95 % (741534)CaDiCaL version: 2.1.3 % 55.21/8.95 % (741534)Termination reason: Unknown % 55.21/8.95 % (741534)Termination phase: Saturation % 55.21/8.95 % (741534)Time elapsed: 0.537 s % 55.21/8.95 % (741534)Peak memory usage: 113 MB % 55.21/8.95 % (741534)Instructions burned: 542 (million) % 55.21/8.95 % (741539)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 55.21/8.95 % (741539)------------------------------ % 55.21/8.95 % (741539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.21/8.95 % (741539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.21/8.95 % (741539)CaDiCaL version: 2.1.3 % 55.21/8.95 % (741539)Termination reason: Unknown % 55.21/8.95 % (741539)Termination phase: Saturation % 55.21/8.95 % (741539)Time elapsed: 0.372 s % 55.21/8.95 % (741539)Peak memory usage: 113 MB % 55.21/8.95 % (741539)Instructions burned: 539 (million) % 55.21/8.95 % (741544)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=4248942874:i=21611:sd=3:ss=axioms_2951 on theBenchmark for (2951ds/21611Mi) % 55.21/8.95 % (741545)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1240232864:i=4835:sd=13:ss=axioms:sgt=23_2951 on theBenchmark for (2951ds/4835Mi) % 55.21/8.95 % (741537)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 55.21/8.95 % (741537)------------------------------ % 55.21/8.95 % (741537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.21/8.95 % (741537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.21/8.95 % (741537)CaDiCaL version: 2.1.3 % 55.21/8.95 % (741537)Termination reason: Unknown % 55.21/8.95 % (741537)Termination phase: Saturation % 55.21/8.95 % (741537)Time elapsed: 0.587 s % 55.21/8.95 % (741537)Peak memory usage: 113 MB % 55.21/8.95 % (741537)Instructions burned: 541 (million) % 55.21/8.95 % (741538)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 55.21/8.95 % (741538)------------------------------ % 55.21/8.95 % (741538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.21/8.95 % (741538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.74 % (741538)CaDiCaL version: 2.1.3 % 61.66/9.74 % (741538)Termination reason: Unknown % 61.66/9.74 % (741538)Termination phase: Saturation % 61.66/9.74 % (741538)Time elapsed: 0.603 s % 61.66/9.74 % (741538)Peak memory usage: 113 MB % 61.66/9.74 % (741538)Instructions burned: 542 (million) % 61.66/9.74 % (741547)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=2783170350:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2949 on theBenchmark for (2949ds/797Mi) % 61.66/9.74 % (741547)Refutation not found, incomplete strategy % 61.66/9.74 % (741547)------------------------------ % 61.66/9.74 % (741547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.66/9.74 % (741547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.74 % (741547)CaDiCaL version: 2.1.3 % 61.66/9.74 % (741547)Termination reason: Refutation not found, incomplete strategy % 61.66/9.74 % (741547)Time elapsed: 0.020 s % 61.66/9.74 % (741547)Peak memory usage: 88 MB % 61.66/9.74 % (741547)Instructions burned: 19 (million) % 61.66/9.74 % (741550)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1047057681:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2948 on theBenchmark for (2948ds/2326Mi) % 61.66/9.74 % (741551)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3746679864:i=6038:nm=6_2947 on theBenchmark for (2947ds/6038Mi) % 61.66/9.74 % (741544)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.66/9.74 % (741544)------------------------------ % 61.66/9.74 % (741544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.66/9.74 % (741544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.74 % (741544)CaDiCaL version: 2.1.3 % 61.66/9.74 % (741544)Termination reason: Unknown % 61.66/9.74 % (741544)Termination phase: Saturation % 61.66/9.74 % (741544)Time elapsed: 0.592 s % 61.66/9.74 % (741544)Peak memory usage: 113 MB % 61.66/9.74 % (741544)Instructions burned: 538 (million) % 61.66/9.74 % (741547)------------------------------ % 61.66/9.74 % (741547)------------------------------ % 61.66/9.74 % (741551)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.66/9.74 % (741551)------------------------------ % 61.66/9.74 % (741551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.66/9.74 % (741551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.74 % (741551)CaDiCaL version: 2.1.3 % 61.66/9.74 % (741551)Termination reason: Unknown % 61.66/9.74 % (741551)Termination phase: Saturation % 61.66/9.74 % (741551)Time elapsed: 0.449 s % 61.66/9.74 % (741551)Peak memory usage: 113 MB % 61.66/9.74 % (741551)Instructions burned: 542 (million) % 61.66/9.74 % (741555)lrs+10_1_sil=32000:sp=occurrence:random_seed=3393569854:st=2:i=33334:sd=3:ss=included:sgt=32_2943 on theBenchmark for (2943ds/33334Mi) % 61.66/9.74 % (741556)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1152602398:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2942 on theBenchmark for (2942ds/1008Mi) % 61.66/9.74 % (741557)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=633587932:i=8327:s2at=5:bd=preordered_2941 on theBenchmark for (2941ds/8327Mi) % 61.66/9.74 % (741505)Instruction limit reached! % 61.66/9.74 % (741505)------------------------------ % 61.66/9.74 % (741505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.66/9.74 % (741505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.66/9.74 % (741505)CaDiCaL version: 2.1.3 % 61.66/9.74 % (741505)Termination reason: Instruction limit % 61.66/9.74 % (741505)Termination phase: Saturation % 61.66/9.74 % (741505)Time elapsed: 3.562 s % 61.66/9.74 % (741505)Peak memory usage: 115 MB % 61.66/9.74 % (741505)Instructions burned: 3706 (million) % 61.66/9.74 % (741564)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=589368803:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2935 on theBenchmark for (2935ds/1083Mi) % 61.66/9.74 % (741557)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.66/9.74 % (741557)------------------------------ % 61.66/9.74 % (741557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.39/10.71 % (741557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.39/10.71 % (741557)CaDiCaL version: 2.1.3 % 68.39/10.71 % (741557)Termination reason: Unknown % 68.39/10.71 % (741557)Termination phase: Saturation % 68.39/10.71 % (741557)Time elapsed: 0.592 s % 68.39/10.71 % (741557)Peak memory usage: 113 MB % 68.39/10.71 % (741557)Instructions burned: 542 (million) % 68.39/10.71 % (741556)Instruction limit reached! % 68.39/10.71 % (741556)------------------------------ % 68.39/10.71 % (741556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.39/10.71 % (741556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.39/10.71 % (741556)CaDiCaL version: 2.1.3 % 68.39/10.71 % (741556)Termination reason: Instruction limit % 68.39/10.71 % (741556)Termination phase: Saturation % 68.39/10.71 % (741556)Time elapsed: 0.796 s % 68.39/10.71 % (741556)Peak memory usage: 93 MB % 68.39/10.71 % (741556)Instructions burned: 1008 (million) % 68.39/10.71 % (741567)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2068012182:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2932 on theBenchmark for (2932ds/1084Mi) % 68.39/10.71 % (741568)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2799271865:i=6995:s2at=5:gtg=all_2931 on theBenchmark for (2931ds/6995Mi) % 68.39/10.71 % (741550)Instruction limit reached! % 68.39/10.71 % (741550)------------------------------ % 68.39/10.71 % (741550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.39/10.71 % (741550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.39/10.71 % (741550)CaDiCaL version: 2.1.3 % 68.39/10.71 % (741550)Termination reason: Instruction limit % 68.39/10.71 % (741550)Termination phase: Saturation % 68.39/10.71 % (741550)Time elapsed: 2.084 s % 68.39/10.71 % (741550)Peak memory usage: 98 MB % 68.39/10.71 % (741550)Instructions burned: 2327 (million) % 68.39/10.71 % (741564)Instruction limit reached! % 68.39/10.71 % (741564)------------------------------ % 68.39/10.71 % (741564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.39/10.71 % (741564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.39/10.71 % (741564)CaDiCaL version: 2.1.3 % 68.39/10.71 % (741564)Termination reason: Instruction limit % 68.39/10.71 % (741564)Termination phase: Saturation % 68.39/10.71 % (741564)Time elapsed: 0.880 s % 68.39/10.71 % (741564)Peak memory usage: 94 MB % 68.39/10.71 % (741564)Instructions burned: 1084 (million) % 68.39/10.71 % (741533)Instruction limit reached! % 68.39/10.71 % (741533)------------------------------ % 68.39/10.71 % (741533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.39/10.71 % (741533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.39/10.71 % (741533)CaDiCaL version: 2.1.3 % 68.39/10.71 % (741533)Termination reason: Instruction limit % 68.39/10.71 % (741533)Termination phase: Saturation % 68.39/10.71 % (741533)Time elapsed: 3.320 s % 68.39/10.71 % (741533)Peak memory usage: 98 MB % 68.39/10.71 % (741533)Instructions burned: 5784 (million) % 68.39/10.71 % (741568)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 68.39/10.71 % (741568)------------------------------ % 68.39/10.71 % (741568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.39/10.71 % (741568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.39/10.71 % (741568)CaDiCaL version: 2.1.3 % 68.39/10.71 % (741568)Termination reason: Unknown % 68.39/10.71 % (741568)Termination phase: Saturation % 68.39/10.71 % (741568)Time elapsed: 0.590 s % 68.39/10.71 % (741568)Peak memory usage: 114 MB % 68.39/10.71 % (741568)Instructions burned: 545 (million) % 68.39/10.71 % (741571)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2565414797:st=2:i=6225:sd=15:ss=axioms_2925 on theBenchmark for (2925ds/6225Mi) % 68.39/10.71 % (741573)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1611790163:st=2.3:i=26457:sd=10:ss=included:sgt=8_2923 on theBenchmark for (2923ds/26457Mi) % 68.39/10.71 % (741572)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3966916785:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2924 on theBenchmark for (2924ds/3372Mi) % 68.39/10.71 % (741545)Instruction limit reached! % 68.39/10.71 % (741545)------------------------------ % 68.39/10.71 % (741545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.95/11.60 % (741545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.95/11.60 % (741545)CaDiCaL version: 2.1.3 % 74.95/11.60 % (741545)Termination reason: Instruction limit % 74.95/11.60 % (741545)Termination phase: Saturation % 74.95/11.60 % (741545)Time elapsed: 2.866 s % 74.95/11.60 % (741545)Peak memory usage: 107 MB % 74.95/11.60 % (741545)Instructions burned: 4836 (million) % 74.95/11.60 % (741567)Instruction limit reached! % 74.95/11.60 % (741567)------------------------------ % 74.95/11.60 % (741567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.95/11.60 % (741567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.95/11.60 % (741567)CaDiCaL version: 2.1.3 % 74.95/11.60 % (741567)Termination reason: Instruction limit % 74.95/11.60 % (741567)Termination phase: Saturation % 74.95/11.60 % (741567)Time elapsed: 0.972 s % 74.95/11.60 % (741567)Peak memory usage: 95 MB % 74.95/11.60 % (741567)Instructions burned: 1086 (million) % 74.95/11.60 % (741574)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=284885738:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2922 on theBenchmark for (2922ds/13494Mi) % 74.95/11.61 % (741573)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.95/11.61 % (741573)------------------------------ % 74.95/11.61 % (741573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.95/11.61 % (741573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.95/11.61 % (741573)CaDiCaL version: 2.1.3 % 74.95/11.61 % (741573)Termination reason: Unknown % 74.95/11.61 % (741573)Termination phase: Saturation % 74.95/11.61 % (741573)Time elapsed: 0.313 s % 74.95/11.61 % (741573)Peak memory usage: 113 MB % 74.95/11.61 % (741573)Instructions burned: 542 (million) % 74.95/11.61 % (741579)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2882483912:i=2559:sd=1:ep=RSTC:ss=axioms_2920 on theBenchmark for (2920ds/2559Mi) % 74.95/11.61 % (741578)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=1846410724:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2920 on theBenchmark for (2920ds/2503Mi) % 74.95/11.61 % (741578)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 74.95/11.61 % (741581)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3436853005:i=30753:av=off:ss=included_2918 on theBenchmark for (2918ds/30753Mi) % 74.95/11.61 % (741572)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.95/11.61 % (741572)------------------------------ % 74.95/11.61 % (741572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.95/11.61 % (741572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.95/11.61 % (741572)CaDiCaL version: 2.1.3 % 74.95/11.61 % (741572)Termination reason: Unknown % 74.95/11.61 % (741572)Termination phase: Saturation % 74.95/11.61 % (741572)Time elapsed: 0.593 s % 74.95/11.61 % (741572)Peak memory usage: 113 MB % 74.95/11.61 % (741572)Instructions burned: 539 (million) % 74.95/11.61 % (741574)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.95/11.61 % (741574)------------------------------ % 74.95/11.61 % (741574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.95/11.61 % (741574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.95/11.61 % (741574)CaDiCaL version: 2.1.3 % 74.95/11.61 % (741574)Termination reason: Unknown % 74.95/11.61 % (741574)Termination phase: Saturation % 74.95/11.61 % (741574)Time elapsed: 0.589 s % 74.95/11.61 % (741574)Peak memory usage: 114 MB % 74.95/11.61 % (741574)Instructions burned: 542 (million) % 74.95/11.61 % (741581)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.95/11.61 % (741581)------------------------------ % 74.95/11.61 % (741581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.95/11.61 % (741581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.95/11.61 % (741581)CaDiCaL version: 2.1.3 % 74.95/11.61 % (741581)Termination reason: Unknown % 74.95/11.61 % (741581)Termination phase: Saturation % 74.95/11.61 % (741581)Time elapsed: 0.313 s % 74.95/11.61 % (741581)Peak memory usage: 113 MB % 74.95/11.61 % (741581)Instructions burned: 541 (million) % 74.95/11.61 % (741586)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2807518457:i=26473:ep=RSTC_2915 on theBenchmark for (2915ds/26473Mi) % 83.07/12.71 % (741579)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.07/12.71 % (741579)------------------------------ % 83.07/12.71 % (741579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.07/12.71 % (741579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.07/12.71 % (741579)CaDiCaL version: 2.1.3 % 83.07/12.71 % (741579)Termination reason: Unknown % 83.07/12.71 % (741579)Termination phase: Saturation % 83.07/12.71 % (741579)Time elapsed: 0.590 s % 83.07/12.71 % (741579)Peak memory usage: 113 MB % 83.07/12.71 % (741579)Instructions burned: 539 (million) % 83.07/12.71 % (741578)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.07/12.71 % (741578)------------------------------ % 83.07/12.71 % (741578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.07/12.71 % (741578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.07/12.71 % (741578)CaDiCaL version: 2.1.3 % 83.07/12.71 % (741578)Termination reason: Unknown % 83.07/12.71 % (741578)Termination phase: Saturation % 83.07/12.71 % (741578)Time elapsed: 0.594 s % 83.07/12.71 % (741578)Peak memory usage: 113 MB % 83.07/12.71 % (741578)Instructions burned: 541 (million) % 83.07/12.71 % (741588)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=2754351772:cts=off:i=2759:kws=inv_arity:fgj=on_2914 on theBenchmark for (2914ds/2759Mi) % 83.07/12.71 % (741589)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=49164772:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2913 on theBenchmark for (2913ds/5665Mi) % 83.07/12.71 % (741589)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 83.07/12.71 % (741591)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=626815484:i=1532:ep=RS:ss=axioms_2911 on theBenchmark for (2911ds/1532Mi) % 83.07/12.71 % (741592)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3760777740:i=1565:sd=2:ss=axioms:sgt=32_2911 on theBenchmark for (2911ds/1565Mi) % 83.07/12.71 % (741589)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.07/12.71 % (741589)------------------------------ % 83.07/12.71 % (741589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.07/12.71 % (741589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.07/12.71 % (741589)CaDiCaL version: 2.1.3 % 83.07/12.71 % (741589)Termination reason: Unknown % 83.07/12.71 % (741589)Termination phase: Saturation % 83.07/12.71 % (741589)Time elapsed: 0.312 s % 83.07/12.71 % (741589)Peak memory usage: 113 MB % 83.07/12.71 % (741589)Instructions burned: 540 (million) % 83.07/12.71 % (741597)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=3565414982:i=1572:fgj=on:gsp=on_2907 on theBenchmark for (2907ds/1572Mi) % 83.07/12.71 % (741597)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 83.07/12.71 % (741588)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.07/12.71 % (741588)------------------------------ % 83.07/12.71 % (741588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.07/12.71 % (741588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.07/12.71 % (741588)CaDiCaL version: 2.1.3 % 83.07/12.71 % (741588)Termination reason: Unknown % 83.07/12.71 % (741588)Termination phase: Saturation % 83.07/12.71 % (741588)Time elapsed: 0.592 s % 83.07/12.71 % (741588)Peak memory usage: 113 MB % 83.07/12.71 % (741588)Instructions burned: 544 (million) % 83.07/12.71 % (741591)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.07/12.71 % (741591)------------------------------ % 83.07/12.71 % (741591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.07/12.71 % (741591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.07/12.71 % (741591)CaDiCaL version: 2.1.3 % 83.07/12.71 % (741591)Termination reason: Unknown % 83.07/12.71 % (741591)Termination phase: Saturation % 93.77/14.28 % (741591)Time elapsed: 0.583 s % 93.77/14.28 % (741591)Peak memory usage: 113 MB % 93.77/14.28 % (741591)Instructions burned: 539 (million) % 93.77/14.28 % (741592)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.77/14.28 % (741592)------------------------------ % 93.77/14.28 % (741592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.77/14.28 % (741592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.77/14.28 % (741592)CaDiCaL version: 2.1.3 % 93.77/14.28 % (741592)Termination reason: Unknown % 93.77/14.28 % (741592)Termination phase: Saturation % 93.77/14.28 % (741592)Time elapsed: 0.593 s % 93.77/14.28 % (741592)Peak memory usage: 113 MB % 93.77/14.28 % (741592)Instructions burned: 539 (million) % 93.77/14.28 % (741597)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.77/14.28 % (741597)------------------------------ % 93.77/14.28 % (741597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.77/14.28 % (741597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.77/14.28 % (741597)CaDiCaL version: 2.1.3 % 93.77/14.28 % (741597)Termination reason: Unknown % 93.77/14.28 % (741597)Termination phase: Saturation % 93.77/14.28 % (741597)Time elapsed: 0.314 s % 93.77/14.28 % (741597)Peak memory usage: 113 MB % 93.77/14.28 % (741597)Instructions burned: 540 (million) % 93.77/14.28 % (741601)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2728339391:i=6052:sd=4:ss=axioms:sgt=24_2905 on theBenchmark for (2905ds/6052Mi) % 93.77/14.28 % (741606)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1542950646:i=66096:add=on_2902 on theBenchmark for (2902ds/66096Mi) % 93.77/14.28 % (741604)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=188529351:i=3500:sd=1:bd=preordered:sup=off:ss=included_2902 on theBenchmark for (2902ds/3500Mi) % 93.77/14.28 % (741605)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=2464983336:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2902 on theBenchmark for (2902ds/1842Mi) % 93.77/14.28 % (741605)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 93.77/14.28 % (741606)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.77/14.28 % (741606)------------------------------ % 93.77/14.28 % (741606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.77/14.28 % (741606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.77/14.28 % (741606)CaDiCaL version: 2.1.3 % 93.77/14.28 % (741606)Termination reason: Unknown % 93.77/14.28 % (741606)Termination phase: Saturation % 93.77/14.28 % (741606)Time elapsed: 0.309 s % 93.77/14.28 % (741606)Peak memory usage: 113 MB % 93.77/14.28 % (741606)Instructions burned: 540 (million) % 93.77/14.28 % (741601)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.77/14.28 % (741601)------------------------------ % 93.77/14.28 % (741601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.77/14.28 % (741601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.77/14.28 % (741601)CaDiCaL version: 2.1.3 % 93.77/14.28 % (741601)Termination reason: Unknown % 93.77/14.28 % (741601)Termination phase: Saturation % 93.77/14.28 % (741601)Time elapsed: 0.593 s % 93.77/14.28 % (741601)Peak memory usage: 113 MB % 93.77/14.28 % (741601)Instructions burned: 542 (million) % 93.77/14.28 % (741612)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2794944189:i=1884:sd=1:nm=60:ss=axioms_2897 on theBenchmark for (2897ds/1884Mi) % 93.77/14.28 % (741604)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 93.77/14.28 % (741604)------------------------------ % 93.77/14.28 % (741604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.77/14.28 % (741604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.77/14.28 % (741604)CaDiCaL version: 2.1.3 % 93.77/14.28 % (741604)Termination reason: Unknown % 93.77/14.28 % (741604)Termination phase: Saturation % 93.77/14.28 % (741604)Time elapsed: 0.584 s % 93.77/14.28 % (741604)Peak memory usage: 113 MB % 93.77/14.28 % (741604)Instructions burned: 539 (million) % 93.77/14.28 % (741605)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.78/15.69 % (741605)------------------------------ % 102.78/15.69 % (741605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.78/15.69 % (741605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.78/15.69 % (741605)CaDiCaL version: 2.1.3 % 102.78/15.69 % (741605)Termination reason: Unknown % 102.78/15.69 % (741605)Termination phase: Saturation % 102.78/15.69 % (741605)Time elapsed: 0.595 s % 102.78/15.69 % (741605)Peak memory usage: 113 MB % 102.78/15.69 % (741605)Instructions burned: 541 (million) % 102.78/15.69 % (741613)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3742366969:cts=off:i=5469:bs=on:fsr=off_2896 on theBenchmark for (2896ds/5469Mi) % 102.78/15.69 % (741617)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1053554329:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2893 on theBenchmark for (2893ds/2110Mi) % 102.78/15.69 % (741612)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.78/15.69 % (741612)------------------------------ % 102.78/15.69 % (741612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.78/15.69 % (741612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.78/15.69 % (741612)CaDiCaL version: 2.1.3 % 102.78/15.69 % (741612)Termination reason: Unknown % 102.78/15.69 % (741612)Termination phase: Saturation % 102.78/15.69 % (741612)Time elapsed: 0.310 s % 102.78/15.69 % (741612)Peak memory usage: 113 MB % 102.78/15.69 % (741612)Instructions burned: 538 (million) % 102.78/15.69 % (741616)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=920777179:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2894 on theBenchmark for (2894ds/2037Mi) % 102.78/15.69 % (741621)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=4085914062:i=2430:add=off:aac=none:nm=16_2891 on theBenchmark for (2891ds/2430Mi) % 102.78/15.69 % (741617)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.78/15.69 % (741617)------------------------------ % 102.78/15.69 % (741617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.78/15.69 % (741617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.78/15.69 % (741617)CaDiCaL version: 2.1.3 % 102.78/15.69 % (741617)Termination reason: Unknown % 102.78/15.69 % (741617)Termination phase: Saturation % 102.78/15.69 % (741617)Time elapsed: 0.334 s % 102.78/15.69 % (741617)Peak memory usage: 113 MB % 102.78/15.69 % (741617)Instructions burned: 544 (million) % 102.78/15.69 % (741625)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=946367851:cond=fast:i=4891_2888 on theBenchmark for (2888ds/4891Mi) % 102.78/15.69 % (741616)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.78/15.69 % (741616)------------------------------ % 102.78/15.69 % (741616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.78/15.69 % (741616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.78/15.69 % (741616)CaDiCaL version: 2.1.3 % 102.78/15.69 % (741616)Termination reason: Unknown % 102.78/15.69 % (741616)Termination phase: Saturation % 102.78/15.69 % (741616)Time elapsed: 0.588 s % 102.78/15.69 % (741616)Peak memory usage: 114 MB % 102.78/15.69 % (741616)Instructions burned: 546 (million) % 102.78/15.69 % (741625)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.78/15.69 % (741625)------------------------------ % 102.78/15.69 % (741625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.78/15.69 % (741625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.78/15.69 % (741625)CaDiCaL version: 2.1.3 % 102.78/15.69 % (741625)Termination reason: Unknown % 102.78/15.69 % (741625)Termination phase: Saturation % 102.78/15.69 % (741625)Time elapsed: 0.312 s % 102.78/15.69 % (741625)Peak memory usage: 113 MB % 102.78/15.69 % (741625)Instructions burned: 541 (million) % 102.78/15.69 % (741621)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.78/15.69 % (741621)------------------------------ % 102.78/15.69 % (741621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.78/15.69 % (741621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.97/16.87 % (741621)CaDiCaL version: 2.1.3 % 109.97/16.87 % (741621)Termination reason: Unknown % 109.97/16.87 % (741621)Termination phase: Saturation % 109.97/16.87 % (741621)Time elapsed: 0.593 s % 109.97/16.87 % (741621)Peak memory usage: 113 MB % 109.97/16.87 % (741621)Instructions burned: 541 (million) % 109.97/16.87 % (741627)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=3750353651:st=2:i=14845:sd=2:ss=included:fsd=on_2885 on theBenchmark for (2885ds/14845Mi) % 109.97/16.87 % (741628)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3777364737:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2882 on theBenchmark for (2882ds/7534Mi) % 109.97/16.87 % (741629)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=2190820909:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2882 on theBenchmark for (2882ds/10353Mi) % 109.97/16.87 % (741628)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 109.97/16.88 % (741628)------------------------------ % 109.97/16.88 % (741628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.97/16.88 % (741628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.97/16.88 % (741628)CaDiCaL version: 2.1.3 % 109.97/16.88 % (741628)Termination reason: Unknown % 109.97/16.88 % (741628)Termination phase: Saturation % 109.97/16.88 % (741628)Time elapsed: 0.321 s % 109.97/16.88 % (741628)Peak memory usage: 113 MB % 109.97/16.88 % (741628)Instructions burned: 543 (million) % 109.97/16.88 % (741627)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 109.97/16.88 % (741627)------------------------------ % 109.97/16.88 % (741627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.97/16.88 % (741627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.97/16.88 % (741627)CaDiCaL version: 2.1.3 % 109.97/16.88 % (741627)Termination reason: Unknown % 109.97/16.88 % (741627)Termination phase: Saturation % 109.97/16.88 % (741627)Time elapsed: 0.663 s % 109.97/16.88 % (741627)Peak memory usage: 114 MB % 109.97/16.88 % (741627)Instructions burned: 541 (million) % 109.97/16.88 % (741633)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2197846785:i=7860_2877 on theBenchmark for (2877ds/7860Mi) % 109.97/16.88 % (741629)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 109.97/16.88 % (741629)------------------------------ % 109.97/16.88 % (741629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.97/16.88 % (741629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.97/16.88 % (741629)CaDiCaL version: 2.1.3 % 109.97/16.88 % (741629)Termination reason: Unknown % 109.97/16.88 % (741629)Termination phase: Saturation % 109.97/16.88 % (741629)Time elapsed: 0.608 s % 109.97/16.88 % (741629)Peak memory usage: 113 MB % 109.97/16.88 % (741629)Instructions burned: 541 (million) % 109.97/16.88 % (741634)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=2319406071:i=7896:sd=2:bs=on:ss=included:sgt=20_2875 on theBenchmark for (2875ds/7896Mi) % 109.97/16.88 % (741637)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1646570398:i=5812:gtgl=2:gtg=all_2874 on theBenchmark for (2874ds/5812Mi) % 109.97/16.88 % (741571)Instruction limit reached! % 109.97/16.88 % (741571)------------------------------ % 109.97/16.88 % (741571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 109.97/16.88 % (741571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 109.97/16.88 % (741571)CaDiCaL version: 2.1.3 % 109.97/16.88 % (741571)Termination reason: Instruction limit % 109.97/16.88 % (741571)Termination phase: Saturation % 109.97/16.88 % (741571)Time elapsed: 5.109 s % 109.97/16.88 % (741571)Peak memory usage: 126 MB % 109.97/16.88 % (741571)Instructions burned: 6225 (million) % 109.97/16.88 % (741641)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=983160354:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2870 on theBenchmark for (2870ds/2965Mi) % 109.97/16.88 % (741634)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 109.97/16.88 % (741634)------------------------------ % 117.81/17.74 % (741634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.81/17.74 % (741634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.81/17.74 % (741634)CaDiCaL version: 2.1.3 % 117.81/17.74 % (741634)Termination reason: Unknown % 117.81/17.74 % (741634)Termination phase: Saturation % 117.81/17.74 % (741634)Time elapsed: 0.586 s % 117.81/17.74 % (741634)Peak memory usage: 113 MB % 117.81/17.74 % (741634)Instructions burned: 542 (million) % 117.81/17.74 % (741637)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 117.81/17.74 % (741637)------------------------------ % 117.81/17.74 % (741637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.81/17.74 % (741637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.81/17.74 % (741637)CaDiCaL version: 2.1.3 % 117.81/17.74 % (741637)Termination reason: Unknown % 117.81/17.74 % (741637)Termination phase: Saturation % 117.81/17.74 % (741637)Time elapsed: 0.525 s % 117.81/17.74 % (741637)Peak memory usage: 114 MB % 117.81/17.74 % (741637)Instructions burned: 544 (million) % 117.81/17.74 % (741647)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=2891998621:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2866 on theBenchmark for (2866ds/3022Mi) % 117.81/17.74 % (741645)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=4282306771:i=2967:kws=precedence:bd=preordered:av=off_2866 on theBenchmark for (2866ds/2967Mi) % 117.81/17.74 % (741641)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 117.81/17.74 % (741641)------------------------------ % 117.81/17.74 % (741641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.81/17.74 % (741641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.81/17.74 % (741641)CaDiCaL version: 2.1.3 % 117.81/17.74 % (741641)Termination reason: Unknown % 117.81/17.74 % (741641)Termination phase: Saturation % 117.81/17.74 % (741641)Time elapsed: 0.583 s % 117.81/17.74 % (741641)Peak memory usage: 113 MB % 117.81/17.74 % (741641)Instructions burned: 542 (million) % 117.81/17.74 % (741647)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 117.81/17.74 % (741647)------------------------------ % 117.81/17.74 % (741647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.81/17.74 % (741647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.81/17.74 % (741647)CaDiCaL version: 2.1.3 % 117.81/17.74 % (741647)Termination reason: Unknown % 117.81/17.74 % (741647)Termination phase: Saturation % 117.81/17.74 % (741647)Time elapsed: 0.547 s % 117.81/17.74 % (741647)Peak memory usage: 113 MB % 117.81/17.74 % (741647)Instructions burned: 539 (million) % 117.81/17.74 % (741651)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=4225967802:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2861 on theBenchmark for (2861ds/3207Mi) % 117.81/17.74 % (741645)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 117.81/17.74 % (741645)------------------------------ % 117.81/17.74 % (741645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.81/17.74 % (741645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.81/17.74 % (741645)CaDiCaL version: 2.1.3 % 117.81/17.74 % (741645)Termination reason: Unknown % 117.81/17.74 % (741645)Termination phase: Saturation % 117.81/17.74 % (741645)Time elapsed: 0.591 s % 117.81/17.74 % (741645)Peak memory usage: 113 MB % 117.81/17.74 % (741645)Instructions burned: 541 (million) % 117.81/17.74 % (741653)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3355491726:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2858 on theBenchmark for (2858ds/3289Mi) % 117.81/17.74 % (741654)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=4152562007:i=38569:sd=3:ss=axioms:sgt=32_2858 on theBenchmark for (2858ds/38569Mi) % 117.81/17.74 % (741651)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 117.81/17.74 % (741651)------------------------------ % 117.81/17.74 % (741651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.81/17.74 % (741651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/18.87 % (741651)CaDiCaL version: 2.1.3 % 124.93/18.87 % (741651)Termination reason: Unknown % 124.93/18.87 % (741651)Termination phase: Saturation % 124.93/18.87 % (741651)Time elapsed: 0.585 s % 124.93/18.87 % (741651)Peak memory usage: 113 MB % 124.93/18.87 % (741651)Instructions burned: 538 (million) % 124.93/18.87 % (741657)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=659854534:cts=off:i=3394_2852 on theBenchmark for (2852ds/3394Mi) % 124.93/18.87 % (741653)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.93/18.87 % (741653)------------------------------ % 124.93/18.87 % (741653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.93/18.87 % (741653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/18.87 % (741653)CaDiCaL version: 2.1.3 % 124.93/18.87 % (741653)Termination reason: Unknown % 124.93/18.87 % (741653)Termination phase: Saturation % 124.93/18.87 % (741653)Time elapsed: 0.588 s % 124.93/18.87 % (741653)Peak memory usage: 113 MB % 124.93/18.87 % (741653)Instructions burned: 541 (million) % 124.93/18.87 % (741654)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.93/18.87 % (741654)------------------------------ % 124.93/18.87 % (741654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.93/18.87 % (741654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/18.87 % (741654)CaDiCaL version: 2.1.3 % 124.93/18.87 % (741654)Termination reason: Unknown % 124.93/18.87 % (741654)Termination phase: Saturation % 124.93/18.87 % (741654)Time elapsed: 0.553 s % 124.93/18.87 % (741654)Peak memory usage: 113 MB % 124.93/18.87 % (741654)Instructions burned: 542 (million) % 124.93/18.87 % (741660)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=688716538:i=33824:bd=preordered_2849 on theBenchmark for (2849ds/33824Mi) % 124.93/18.87 % (741661)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1695721418:i=20684:bd=all:gtg=exists_sym_2849 on theBenchmark for (2849ds/20684Mi) % 124.93/18.87 % (741613)Instruction limit reached! % 124.93/18.87 % (741613)------------------------------ % 124.93/18.87 % (741613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.93/18.87 % (741613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/18.87 % (741613)CaDiCaL version: 2.1.3 % 124.93/18.87 % (741613)Termination reason: Instruction limit % 124.93/18.87 % (741613)Termination phase: Saturation % 124.93/18.87 % (741613)Time elapsed: 4.703 s % 124.93/18.87 % (741613)Peak memory usage: 103 MB % 124.93/18.87 % (741613)Instructions burned: 5470 (million) % 124.93/18.87 % (741657)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.93/18.87 % (741657)------------------------------ % 124.93/18.87 % (741657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.93/18.87 % (741657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/18.87 % (741657)CaDiCaL version: 2.1.3 % 124.93/18.87 % (741657)Termination reason: Unknown % 124.93/18.87 % (741657)Termination phase: Saturation % 124.93/18.87 % (741657)Time elapsed: 0.595 s % 124.93/18.87 % (741657)Peak memory usage: 113 MB % 124.93/18.87 % (741657)Instructions burned: 541 (million) % 124.93/18.87 % (741665)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=986131283: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_2846 on theBenchmark for (2846ds/7222Mi) % 124.93/18.87 % (741665)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 124.93/18.87 % (741666)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3420858823:st=4:i=7295:sd=4:ep=R:ss=axioms_2844 on theBenchmark for (2844ds/7295Mi) % 124.93/18.87 % (741660)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.93/18.87 % (741660)------------------------------ % 124.93/18.87 % (741660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.93/18.87 % (741660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.93/18.87 % (741660)CaDiCaL version: 2.1.3 % 124.93/18.87 % (741660)Termination reason: Unknown % 124.93/18.87 % (741660)Termination phase: Saturation % 124.93/18.87 % (741660)Time elapsed: 0.594 s % 130.89/19.72 % (741660)Peak memory usage: 114 MB % 130.89/19.72 % (741660)Instructions burned: 542 (million) % 130.89/19.72 % (741661)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.89/19.72 % (741661)------------------------------ % 130.89/19.72 % (741661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.89/19.72 % (741661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.89/19.72 % (741661)CaDiCaL version: 2.1.3 % 130.89/19.72 % (741661)Termination reason: Unknown % 130.89/19.72 % (741661)Termination phase: Saturation % 130.89/19.72 % (741661)Time elapsed: 0.574 s % 130.89/19.72 % (741661)Peak memory usage: 114 MB % 130.89/19.72 % (741661)Instructions burned: 544 (million) % 130.89/19.72 % (741633)Instruction limit reached! % 130.89/19.72 % (741633)------------------------------ % 130.89/19.72 % (741633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.89/19.72 % (741633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.89/19.72 % (741633)CaDiCaL version: 2.1.3 % 130.89/19.72 % (741633)Termination reason: Instruction limit % 130.89/19.72 % (741633)Termination phase: Saturation % 130.89/19.72 % (741633)Time elapsed: 3.670 s % 130.89/19.72 % (741633)Peak memory usage: 117 MB % 130.89/19.72 % (741633)Instructions burned: 7862 (million) % 130.89/19.72 % (741670)lrs+10_1_sil=128000:lcm=predicate:random_seed=1599078489:st=3:i=43697:sd=5:ss=axioms_2840 on theBenchmark for (2840ds/43697Mi) % 130.89/19.72 % (741669)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=578528329:i=4036:ins=10_2841 on theBenchmark for (2841ds/4036Mi) % 130.89/19.72 % (741665)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.89/19.72 % (741665)------------------------------ % 130.89/19.72 % (741665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.89/19.72 % (741665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.89/19.72 % (741665)CaDiCaL version: 2.1.3 % 130.89/19.72 % (741665)Termination reason: Unknown % 130.89/19.72 % (741665)Termination phase: Saturation % 130.89/19.72 % (741665)Time elapsed: 0.590 s % 130.89/19.72 % (741665)Peak memory usage: 114 MB % 130.89/19.72 % (741665)Instructions burned: 544 (million) % 130.89/19.72 % (741671)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=891021378:i=17599:gtg=all:ss=axioms:fsd=on_2838 on theBenchmark for (2838ds/17599Mi) % 130.89/19.72 % (741666)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.89/19.72 % (741666)------------------------------ % 130.89/19.72 % (741666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.89/19.72 % (741666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.89/19.72 % (741666)CaDiCaL version: 2.1.3 % 130.89/19.72 % (741666)Termination reason: Unknown % 130.89/19.72 % (741666)Termination phase: Saturation % 130.89/19.72 % (741666)Time elapsed: 0.595 s % 130.89/19.72 % (741666)Peak memory usage: 113 MB % 130.89/19.72 % (741666)Instructions burned: 544 (million) % 130.89/19.72 % (741674)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=2629278770:i=4547:bd=preordered_2837 on theBenchmark for (2837ds/4547Mi) % 130.89/19.72 % (741671)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.89/19.72 % (741671)------------------------------ % 130.89/19.72 % (741671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.89/19.72 % (741671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.89/19.72 % (741671)CaDiCaL version: 2.1.3 % 130.89/19.72 % (741671)Termination reason: Unknown % 130.89/19.72 % (741671)Termination phase: Saturation % 130.89/19.72 % (741671)Time elapsed: 0.272 s % 130.89/19.72 % (741671)Peak memory usage: 113 MB % 130.89/19.72 % (741671)Instructions burned: 541 (million) % 130.89/19.72 % (741669)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 130.89/19.72 % (741669)------------------------------ % 130.89/19.72 % (741669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.89/19.72 % (741669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.89/19.72 % (741669)CaDiCaL version: 2.1.3 % 130.89/19.72 % (741669)Termination reason: Unknown % 130.89/19.72 % (741669)Termination phase: Saturation % 130.89/19.72 % (741669)Time elapsed: 0.589 s % 130.89/19.72 % (741669)Peak memory usage: 113 MB % 142.16/21.11 % (741669)Instructions burned: 541 (million) % 142.16/21.11 % (741676)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=2342680906:i=9294:av=off_2835 on theBenchmark for (2835ds/9294Mi) % 142.16/21.11 % (741678)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2207448132:i=32849:add=on_2833 on theBenchmark for (2833ds/32849Mi) % 142.16/21.11 % (741679)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4092172281:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2832 on theBenchmark for (2832ds/4793Mi) % 142.16/21.11 % (741674)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 142.16/21.11 % (741674)------------------------------ % 142.16/21.11 % (741674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.16/21.11 % (741674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.16/21.11 % (741674)CaDiCaL version: 2.1.3 % 142.16/21.11 % (741674)Termination reason: Unknown % 142.16/21.11 % (741674)Termination phase: Saturation % 142.16/21.11 % (741674)Time elapsed: 0.586 s % 142.16/21.11 % (741674)Peak memory usage: 113 MB % 142.16/21.11 % (741674)Instructions burned: 541 (million) % 142.16/21.11 % (741678)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 142.16/21.11 % (741678)------------------------------ % 142.16/21.11 % (741678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.16/21.11 % (741678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.16/21.11 % (741678)CaDiCaL version: 2.1.3 % 142.16/21.11 % (741678)Termination reason: Unknown % 142.16/21.11 % (741678)Termination phase: Saturation % 142.16/21.11 % (741678)Time elapsed: 0.308 s % 142.16/21.11 % (741678)Peak memory usage: 113 MB % 142.16/21.11 % (741678)Instructions burned: 541 (million) % 142.16/21.11 % (741676)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 142.16/21.11 % (741676)------------------------------ % 142.16/21.11 % (741676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.16/21.11 % (741676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.16/21.11 % (741676)CaDiCaL version: 2.1.3 % 142.16/21.11 % (741676)Termination reason: Unknown % 142.16/21.11 % (741676)Termination phase: Saturation % 142.16/21.11 % (741676)Time elapsed: 0.502 s % 142.16/21.11 % (741676)Peak memory usage: 114 MB % 142.16/21.11 % (741676)Instructions burned: 541 (million) % 142.16/21.11 % (741685)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=502585783:i=4840:nm=4:av=off_2828 on theBenchmark for (2828ds/4840Mi) % 142.16/21.11 % (741686)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=4158730696:cts=off:i=5002_2828 on theBenchmark for (2828ds/5002Mi) % 142.16/21.11 % (741687)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=2007922543:i=30479:sd=3:ss=axioms_2827 on theBenchmark for (2827ds/30479Mi) % 142.16/21.11 % (741679)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 142.16/21.11 % (741679)------------------------------ % 142.16/21.11 % (741679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.16/21.11 % (741679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.16/21.11 % (741679)CaDiCaL version: 2.1.3 % 142.16/21.11 % (741679)Termination reason: Unknown % 142.16/21.11 % (741679)Termination phase: Saturation % 142.16/21.11 % (741679)Time elapsed: 0.590 s % 142.16/21.11 % (741679)Peak memory usage: 113 MB % 142.16/21.11 % (741679)Instructions burned: 542 (million) % 142.16/21.11 % (741685)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 142.16/21.11 % (741685)------------------------------ % 142.16/21.11 % (741685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.16/21.11 % (741685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.16/21.11 % (741685)CaDiCaL version: 2.1.3 % 142.16/21.11 % (741685)Termination reason: Unknown % 142.16/21.11 % (741685)Termination phase: Saturation % 142.16/21.11 % (741685)Time elapsed: 0.314 s % 142.16/21.11 % (741685)Peak memory usage: 113 MB % 142.16/21.11 % (741685)Instructions burned: 540 (million) % 142.16/21.11 % (741692)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=3474988431:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2823 on theBenchmark for (2823ds/11035Mi) % 178.47/26.14 % (741692)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 178.47/26.14 % (741693)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1752501235:i=5835_2822 on theBenchmark for (2822ds/5835Mi) % 178.47/26.14 % (741686)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 178.47/26.14 % (741686)------------------------------ % 178.47/26.14 % (741686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.47/26.14 % (741686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.47/26.14 % (741686)CaDiCaL version: 2.1.3 % 178.47/26.14 % (741686)Termination reason: Unknown % 178.47/26.14 % (741686)Termination phase: Saturation % 178.47/26.14 % (741686)Time elapsed: 0.597 s % 178.47/26.14 % (741686)Peak memory usage: 113 MB % 178.47/26.14 % (741686)Instructions burned: 541 (million) % 178.47/26.14 % (741687)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 178.47/26.14 % (741687)------------------------------ % 178.47/26.14 % (741687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.47/26.14 % (741687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.47/26.14 % (741687)CaDiCaL version: 2.1.3 % 178.47/26.14 % (741687)Termination reason: Unknown % 178.47/26.14 % (741687)Termination phase: Saturation % 178.47/26.14 % (741687)Time elapsed: 0.557 s % 178.47/26.14 % (741687)Peak memory usage: 113 MB % 178.47/26.14 % (741687)Instructions burned: 539 (million) % 178.47/26.14 % (741692)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 178.47/26.14 % (741692)------------------------------ % 178.47/26.14 % (741692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.47/26.14 % (741692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.47/26.14 % (741692)CaDiCaL version: 2.1.3 % 178.47/26.14 % (741692)Termination reason: Unknown % 178.47/26.14 % (741692)Termination phase: Saturation % 178.47/26.14 % (741692)Time elapsed: 0.312 s % 178.47/26.14 % (741692)Peak memory usage: 113 MB % 178.47/26.14 % (741692)Instructions burned: 544 (million) % 178.47/26.14 % (741697)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=784279780:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2819 on theBenchmark for (2819ds/5890Mi) % 178.47/26.14 % (741698)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=1417710188:cts=off:i=19910:ep=RS_2818 on theBenchmark for (2818ds/19910Mi) % 178.47/26.14 % (741698)Refutation not found, incomplete strategy % 178.47/26.14 % (741698)------------------------------ % 178.47/26.14 % (741698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.47/26.14 % (741698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.47/26.14 % (741698)CaDiCaL version: 2.1.3 % 178.47/26.14 % (741698)Termination reason: Refutation not found, incomplete strategy % 178.47/26.14 % (741698)Time elapsed: 0.011 s % 178.47/26.14 % (741698)Peak memory usage: 88 MB % 178.47/26.14 % (741698)Instructions burned: 10 (million) % 178.47/26.14 % (741699)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=2657859973:i=20312:bd=preordered:fsr=off:er=filter_2817 on theBenchmark for (2817ds/20312Mi) % 178.47/26.14 % (741693)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 178.47/26.14 % (741693)------------------------------ % 178.47/26.14 % (741693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.47/26.14 % (741693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 178.47/26.14 % (741693)CaDiCaL version: 2.1.3 % 178.47/26.14 % (741693)Termination reason: Unknown % 178.47/26.14 % (741693)Termination phase: Saturation % 178.47/26.14 % (741693)Time elapsed: 0.593 s % 178.47/26.14 % (741693)Peak memory usage: 113 MB % 178.47/26.14 % (741693)Instructions burned: 542 (million) % 178.47/26.14 % (741699)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 178.47/26.14 % (741699)------------------------------ % 178.47/26.14 % (741699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 178.47/26.14 % (741699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.99/29.05 % (741699)CaDiCaL version: 2.1.3 % 198.99/29.05 % (741699)Termination reason: Unknown % 198.99/29.05 % (741699)Termination phase: Saturation % 198.99/29.05 % (741699)Time elapsed: 0.312 s % 198.99/29.05 % (741699)Peak memory usage: 113 MB % 198.99/29.05 % (741699)Instructions burned: 542 (million) % 198.99/29.05 % (741698)------------------------------ % 198.99/29.05 % (741698)------------------------------ % 198.99/29.05 % (741703)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=2686802742:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2813 on theBenchmark for (2813ds/13822Mi) % 198.99/29.05 % (741697)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 198.99/29.05 % (741697)------------------------------ % 198.99/29.05 % (741697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.99/29.05 % (741697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.99/29.05 % (741697)CaDiCaL version: 2.1.3 % 198.99/29.05 % (741697)Termination reason: Unknown % 198.99/29.05 % (741697)Termination phase: Saturation % 198.99/29.05 % (741697)Time elapsed: 0.591 s % 198.99/29.05 % (741697)Peak memory usage: 113 MB % 198.99/29.05 % (741697)Instructions burned: 542 (million) % 198.99/29.05 % (741704)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=1830576752:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2812 on theBenchmark for (2812ds/7144Mi) % 198.99/29.05 % (741705)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=3986422536:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2811 on theBenchmark for (2811ds/15184Mi) % 198.99/29.05 % (741707)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=324437608:i=107375_2810 on theBenchmark for (2810ds/107375Mi) % 198.99/29.05 % (741703)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 198.99/29.05 % (741703)------------------------------ % 198.99/29.05 % (741703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.99/29.05 % (741703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.99/29.05 % (741703)CaDiCaL version: 2.1.3 % 198.99/29.05 % (741703)Termination reason: Unknown % 198.99/29.05 % (741703)Termination phase: Saturation % 198.99/29.05 % (741703)Time elapsed: 0.590 s % 198.99/29.05 % (741703)Peak memory usage: 114 MB % 198.99/29.05 % (741703)Instructions burned: 541 (million) % 198.99/29.05 % (741705)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 198.99/29.05 % (741705)------------------------------ % 198.99/29.05 % (741705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.99/29.05 % (741705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.99/29.05 % (741705)CaDiCaL version: 2.1.3 % 198.99/29.05 % (741705)Termination reason: Unknown % 198.99/29.05 % (741705)Termination phase: Saturation % 198.99/29.05 % (741705)Time elapsed: 0.603 s % 198.99/29.05 % (741705)Peak memory usage: 113 MB % 198.99/29.05 % (741705)Instructions burned: 541 (million) % 198.99/29.05 % (741713)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=777008326:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2805 on theBenchmark for (2805ds/7958Mi) % 198.99/29.05 % (741707)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 198.99/29.05 % (741707)------------------------------ % 198.99/29.05 % (741707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 198.99/29.05 % (741707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 198.99/29.05 % (741707)CaDiCaL version: 2.1.3 % 198.99/29.05 % (741707)Termination reason: Unknown % 198.99/29.05 % (741707)Termination phase: Saturation % 198.99/29.05 % (741707)Time elapsed: 0.596 s % 198.99/29.05 % (741707)Peak memory usage: 113 MB % 198.99/29.05 % (741707)Instructions burned: 542 (million) % 198.99/29.05 % (741714)dis+10_128_sil=16000:nwc=0.7:random_seed=2818756168:i=15999:nm=2:gsp=on_2803 on theBenchmark for (2803ds/15999Mi) % 198.99/29.05 % (741714)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 198.99/29.05 % (741716)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2462205403:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2801 on theBenchmark for (2801ds/8139Mi) % 218.50/31.82 % (741713)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 218.50/31.82 % (741713)------------------------------ % 218.50/31.82 % (741713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.50/31.82 % (741713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.50/31.82 % (741713)CaDiCaL version: 2.1.3 % 218.50/31.82 % (741713)Termination reason: Unknown % 218.50/31.82 % (741713)Termination phase: Saturation % 218.50/31.82 % (741713)Time elapsed: 0.588 s % 218.50/31.82 % (741713)Peak memory usage: 113 MB % 218.50/31.82 % (741713)Instructions burned: 542 (million) % 218.50/31.82 % (741720)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3947422298:st=4:i=8950:sd=5:ss=axioms_2796 on theBenchmark for (2796ds/8950Mi) % 218.50/31.82 % (741720)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 218.50/31.82 % (741720)------------------------------ % 218.50/31.82 % (741720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.50/31.82 % (741720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.50/31.82 % (741720)CaDiCaL version: 2.1.3 % 218.50/31.82 % (741720)Termination reason: Unknown % 218.50/31.82 % (741720)Termination phase: Saturation % 218.50/31.82 % (741720)Time elapsed: 0.591 s % 218.50/31.82 % (741720)Peak memory usage: 113 MB % 218.50/31.82 % (741720)Instructions burned: 543 (million) % 218.50/31.82 % (741724)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=113658952:i=9809:ins=10:av=off_2787 on theBenchmark for (2787ds/9809Mi) % 218.50/31.82 % (741724)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 218.50/31.82 % (741724)------------------------------ % 218.50/31.82 % (741724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.50/31.82 % (741724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.50/31.82 % (741724)CaDiCaL version: 2.1.3 % 218.50/31.82 % (741724)Termination reason: Unknown % 218.50/31.82 % (741724)Termination phase: Saturation % 218.50/31.82 % (741724)Time elapsed: 0.590 s % 218.50/31.82 % (741724)Peak memory usage: 113 MB % 218.50/31.82 % (741724)Instructions burned: 542 (million) % 218.50/31.82 % (741727)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=942600746:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2778 on theBenchmark for (2778ds/9885Mi) % 218.50/31.82 % (741727)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 218.50/31.82 % (741727)------------------------------ % 218.50/31.82 % (741727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.50/31.82 % (741727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.50/31.82 % (741727)CaDiCaL version: 2.1.3 % 218.50/31.82 % (741727)Termination reason: Unknown % 218.50/31.82 % (741727)Termination phase: Saturation % 218.50/31.82 % (741727)Time elapsed: 0.593 s % 218.50/31.82 % (741727)Peak memory usage: 114 MB % 218.50/31.82 % (741727)Instructions burned: 542 (million) % 218.50/31.82 % (741730)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=576010169:cond=fast:i=32078:fgj=on:av=off_2769 on theBenchmark for (2769ds/32078Mi) % 218.50/31.82 % (741730)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 218.50/31.82 % (741730)------------------------------ % 218.50/31.82 % (741730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.50/31.82 % (741730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.50/31.82 % (741730)CaDiCaL version: 2.1.3 % 218.50/31.82 % (741730)Termination reason: Unknown % 218.50/31.82 % (741730)Termination phase: Saturation % 218.50/31.82 % (741730)Time elapsed: 0.595 s % 218.50/31.82 % (741730)Peak memory usage: 113 MB % 218.50/31.82 % (741730)Instructions burned: 542 (million) % 218.50/31.82 % (741733)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=2550106272:i=11101:bd=all:ss=axioms:sgt=8_2760 on theBenchmark for (2760ds/11101Mi) % 218.50/31.82 % (741704)Instruction limit reached! % 218.50/31.82 % (741704)------------------------------ % 218.50/31.82 % (741704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.50/31.82 % (741704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.09/32.99 % (741704)CaDiCaL version: 2.1.3 % 226.09/32.99 % (741704)Termination reason: Instruction limit % 226.09/32.99 % (741704)Termination phase: Saturation % 226.09/32.99 % (741704)Time elapsed: 6.169 s % 226.09/32.99 % (741704)Peak memory usage: 135 MB % 226.09/32.99 % (741704)Instructions burned: 7145 (million) % 226.09/32.99 % (741739)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=863182835:cond=on:i=13220:s2at=3:aac=none:fsd=on_2748 on theBenchmark for (2748ds/13220Mi) % 226.09/32.99 % (741739)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 226.09/32.99 % (741739)------------------------------ % 226.09/32.99 % (741739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.09/32.99 % (741739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.09/32.99 % (741739)CaDiCaL version: 2.1.3 % 226.09/32.99 % (741739)Termination reason: Unknown % 226.09/32.99 % (741739)Termination phase: Saturation % 226.09/32.99 % (741739)Time elapsed: 0.588 s % 226.09/32.99 % (741739)Peak memory usage: 113 MB % 226.09/32.99 % (741739)Instructions burned: 542 (million) % 226.09/32.99 % (741743)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=1881025703:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2739 on theBenchmark for (2739ds/13528Mi) % 226.09/33.00 % (741743)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 226.09/33.00 % (741743)------------------------------ % 226.09/33.00 % (741743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.09/33.00 % (741743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.09/33.00 % (741743)CaDiCaL version: 2.1.3 % 226.09/33.00 % (741743)Termination reason: Unknown % 226.09/33.00 % (741743)Termination phase: Saturation % 226.09/33.00 % (741743)Time elapsed: 0.587 s % 226.09/33.00 % (741743)Peak memory usage: 114 MB % 226.09/33.00 % (741743)Instructions burned: 542 (million) % 226.09/33.00 % (741745)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=844620628:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2730 on theBenchmark for (2730ds/14854Mi) % 226.09/33.00 % (741716)Instruction limit reached! % 226.09/33.00 % (741716)------------------------------ % 226.09/33.00 % (741716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.09/33.00 % (741716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.09/33.00 % (741716)CaDiCaL version: 2.1.3 % 226.09/33.00 % (741716)Termination reason: Instruction limit % 226.09/33.00 % (741716)Termination phase: Saturation % 226.09/33.00 % (741716)Time elapsed: 7.415 s % 226.09/33.00 % (741716)Peak memory usage: 108 MB % 226.09/33.00 % (741716)Instructions burned: 8139 (million) % 226.09/33.00 % (741745)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 226.09/33.00 % (741745)------------------------------ % 226.09/33.00 % (741745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.09/33.00 % (741745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.09/33.00 % (741745)CaDiCaL version: 2.1.3 % 226.09/33.00 % (741745)Termination reason: Unknown % 226.09/33.00 % (741745)Termination phase: Saturation % 226.09/33.00 % (741745)Time elapsed: 0.397 s % 226.09/33.00 % (741745)Peak memory usage: 114 MB % 226.09/33.00 % (741745)Instructions burned: 552 (million) % 226.09/33.00 % (741751)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=2156770626:i=14974:ss=axioms:sgt=16_2724 on theBenchmark for (2724ds/14974Mi) % 226.09/33.00 % (741791)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=1412713001:i=33081:aac=none:fgj=on:bd=all:fsr=off_2723 on theBenchmark for (2723ds/33081Mi) % 226.09/33.00 % (741751)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 226.09/33.00 % (741751)------------------------------ % 226.09/33.00 % (741751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 226.09/33.00 % (741751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 226.09/33.00 % (741751)CaDiCaL version: 2.1.3 % 226.09/33.00 % (741751)Termination reason: Unknown % 226.09/33.00 % (741751)Termination phase: Saturation % 226.09/33.00 % (741751)Time elapsed: 0.362 s % 226.09/33.00 % (741751)Peak memory usage: 113 MB % 226.09/33.00 % (741751)Instructions burned: 541 (million) % 232.72/34.02 % (741791)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 232.72/34.02 % (741791)------------------------------ % 232.72/34.02 % (741791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.72/34.02 % (741791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.72/34.02 % (741791)CaDiCaL version: 2.1.3 % 232.72/34.02 % (741791)Termination reason: Unknown % 232.72/34.02 % (741791)Termination phase: Saturation % 232.72/34.02 % (741791)Time elapsed: 0.366 s % 232.72/34.02 % (741791)Peak memory usage: 113 MB % 232.72/34.02 % (741791)Instructions burned: 541 (million) % 232.72/34.02 % (741890)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=720212792:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2719 on theBenchmark for (2719ds/50856Mi) % 232.72/34.02 % (741906)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=1255207632:i=69865_2718 on theBenchmark for (2718ds/69865Mi) % 232.72/34.02 % (741890)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 232.72/34.02 % (741890)------------------------------ % 232.72/34.02 % (741890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.72/34.02 % (741890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.72/34.02 % (741890)CaDiCaL version: 2.1.3 % 232.72/34.02 % (741890)Termination reason: Unknown % 232.72/34.02 % (741890)Termination phase: Saturation % 232.72/34.02 % (741890)Time elapsed: 0.360 s % 232.72/34.02 % (741890)Peak memory usage: 113 MB % 232.72/34.02 % (741890)Instructions burned: 540 (million) % 232.72/34.02 % (741906)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 232.72/34.02 % (741906)------------------------------ % 232.72/34.02 % (741906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.72/34.02 % (741906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.72/34.02 % (741906)CaDiCaL version: 2.1.3 % 232.72/34.02 % (741906)Termination reason: Unknown % 232.72/34.02 % (741906)Termination phase: Saturation % 232.72/34.02 % (741906)Time elapsed: 0.361 s % 232.72/34.02 % (741906)Peak memory usage: 113 MB % 232.72/34.02 % (741906)Instructions burned: 541 (million) % 232.72/34.02 % (741909)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=2912191367:cond=fast:i=17802:gtgl=3:gtg=all_2714 on theBenchmark for (2714ds/17802Mi) % 232.72/34.02 % (741910)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=3193596627:i=96644_2713 on theBenchmark for (2713ds/96644Mi) % 232.72/34.02 % (741909)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 232.72/34.02 % (741909)------------------------------ % 232.72/34.02 % (741909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.72/34.02 % (741909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.72/34.02 % (741909)CaDiCaL version: 2.1.3 % 232.72/34.02 % (741909)Termination reason: Unknown % 232.72/34.02 % (741909)Termination phase: Saturation % 232.72/34.02 % (741909)Time elapsed: 0.363 s % 232.72/34.02 % (741909)Peak memory usage: 113 MB % 232.72/34.02 % (741909)Instructions burned: 543 (million) % 232.72/34.02 % (741913)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 232.72/34.02 % (741913)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=3944713078:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2708 on theBenchmark for (2708ds/21161Mi) % 232.72/34.02 % (741733)Instruction limit reached! % 232.72/34.02 % (741733)------------------------------ % 232.72/34.02 % (741733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 232.72/34.02 % (741733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 232.72/34.02 % (741733)CaDiCaL version: 2.1.3 % 232.72/34.02 % (741733)Termination reason: Instruction limit % 232.72/34.02 % (741733)Termination phase: Saturation % 232.72/34.02 % (741733)Time elapsed: 6.370 s % 232.72/34.02 % (741733)Peak memory usage: 118 MB % 232.72/34.02 % (741733)Instructions burned: 11103 (million) % 232.72/34.02 % (741915)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=589262429:i=22761:gtg=all:ss=axioms:fsd=on_2693 on theBenchmark for (2693ds/22761Mi) % 243.84/35.47 % (741915)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 243.84/35.47 % (741915)------------------------------ % 243.84/35.47 % (741915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.84/35.47 % (741915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.84/35.47 % (741915)CaDiCaL version: 2.1.3 % 243.84/35.47 % (741915)Termination reason: Unknown % 243.84/35.47 % (741915)Termination phase: Saturation % 243.84/35.47 % (741915)Time elapsed: 0.362 s % 243.84/35.47 % (741915)Peak memory usage: 113 MB % 243.84/35.47 % (741915)Instructions burned: 541 (million) % 243.84/35.47 % (741555)Instruction limit reached! % 243.84/35.47 % (741555)------------------------------ % 243.84/35.47 % (741555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.84/35.47 % (741555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.84/35.47 % (741555)CaDiCaL version: 2.1.3 % 243.84/35.47 % (741555)Termination reason: Instruction limit % 243.84/35.47 % (741555)Termination phase: Saturation % 243.84/35.47 % (741555)Time elapsed: 25.309 s % 243.84/35.47 % (741555)Peak memory usage: 154 MB % 243.84/35.47 % (741555)Instructions burned: 33334 (million) % 243.84/35.47 % (741918)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=2213949266:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2687 on theBenchmark for (2687ds/23713Mi) % 243.84/35.47 % (741918)Refutation not found, incomplete strategy % 243.84/35.47 % (741918)------------------------------ % 243.84/35.47 % (741918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.84/35.47 % (741918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.84/35.47 % (741918)CaDiCaL version: 2.1.3 % 243.84/35.47 % (741918)Termination reason: Refutation not found, incomplete strategy % 243.84/35.47 % (741918)Time elapsed: 0.007 s % 243.84/35.47 % (741918)Peak memory usage: 88 MB % 243.84/35.47 % (741918)Instructions burned: 11 (million) % 243.84/35.47 % (741919)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=2497782585:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2687 on theBenchmark for (2687ds/26509Mi) % 243.84/35.47 % (741918)------------------------------ % 243.84/35.47 % (741918)------------------------------ % 243.84/35.47 % (741922)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=2893514746:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2683 on theBenchmark for (2683ds/28957Mi) % 243.84/35.47 % (741919)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 243.84/35.47 % (741919)------------------------------ % 243.84/35.47 % (741919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.84/35.47 % (741919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.84/35.47 % (741919)CaDiCaL version: 2.1.3 % 243.84/35.47 % (741919)Termination reason: Unknown % 243.84/35.47 % (741919)Termination phase: Saturation % 243.84/35.47 % (741919)Time elapsed: 0.368 s % 243.84/35.47 % (741919)Peak memory usage: 113 MB % 243.84/35.47 % (741919)Instructions burned: 541 (million) % 243.84/35.47 % (741586)Instruction limit reached! % 243.84/35.47 % (741586)------------------------------ % 243.84/35.47 % (741586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.84/35.47 % (741586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.84/35.47 % (741586)CaDiCaL version: 2.1.3 % 243.84/35.47 % (741586)Termination reason: Instruction limit % 243.84/35.47 % (741586)Termination phase: Saturation % 243.84/35.47 % (741586)Time elapsed: 23.194 s % 243.84/35.47 % (741586)Peak memory usage: 257 MB % 243.84/35.47 % (741586)Instructions burned: 26474 (million) % 243.84/35.47 % (741714)Instruction limit reached! % 243.84/35.47 % (741714)------------------------------ % 243.84/35.47 % (741714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.84/35.47 % (741714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.84/35.47 % (741714)CaDiCaL version: 2.1.3 % 243.84/35.47 % (741714)Termination reason: Instruction limit % 243.84/35.47 % (741714)Termination phase: Saturation % 243.84/35.47 % (741714)Time elapsed: 12.012 s % 243.84/35.47 % (741714)Peak memory usage: 180 MB % 243.84/35.47 % (741714)Instructions burned: 16000 (million) % 243.84/35.47 % (741924)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=3999154251:i=29246:s2at=-1:kws=inv_arity:ins=10_2681 on theBenchmark for (2681ds/29246Mi) % 252.16/36.69 % (741926)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1214308098:i=32262:bd=preordered_2680 on theBenchmark for (2680ds/32262Mi) % 252.16/36.69 % (741925)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=3737267783:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2680 on theBenchmark for (2680ds/30082Mi) % 252.16/36.69 % (741925)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 252.16/36.69 % (741924)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 252.16/36.69 % (741924)------------------------------ % 252.16/36.69 % (741924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.16/36.69 % (741924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.16/36.69 % (741924)CaDiCaL version: 2.1.3 % 252.16/36.69 % (741924)Termination reason: Unknown % 252.16/36.69 % (741924)Termination phase: Saturation % 252.16/36.69 % (741924)Time elapsed: 0.360 s % 252.16/36.69 % (741924)Peak memory usage: 114 MB % 252.16/36.69 % (741924)Instructions burned: 541 (million) % 252.16/36.69 % (741925)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 252.16/36.69 % (741926)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 252.16/36.69 % (741925)------------------------------ % 252.16/36.69 % (741925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.16/36.69 % (741926)------------------------------ % 252.16/36.69 % (741926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.16/36.69 % (741925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.16/36.69 % (741926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.16/36.69 % (741925)CaDiCaL version: 2.1.3 % 252.16/36.69 % (741925)Termination reason: Unknown % 252.16/36.69 % (741925)Termination phase: Saturation % 252.16/36.69 % (741926)CaDiCaL version: 2.1.3 % 252.16/36.69 % (741925)Time elapsed: 0.358 s % 252.16/36.69 % (741926)Termination reason: Unknown % 252.16/36.69 % (741926)Termination phase: Saturation % 252.16/36.69 % (741926)Time elapsed: 0.358 s % 252.16/36.69 % (741925)Peak memory usage: 113 MB % 252.16/36.69 % (741926)Peak memory usage: 112 MB % 252.16/36.69 % (741925)Instructions burned: 545 (million) % 252.16/36.69 % (741926)Instructions burned: 541 (million) % 252.16/36.69 % (741930)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=2426952137:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2676 on theBenchmark for (2676ds/32870Mi) % 252.16/36.69 % (741932)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=2441124604:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2674 on theBenchmark for (2674ds/36826Mi) % 252.16/36.69 % (741931)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=2448440838:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2674 on theBenchmark for (2674ds/33295Mi) % 252.16/36.69 % (741930)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 252.16/36.69 % (741930)------------------------------ % 252.16/36.69 % (741930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.16/36.69 % (741930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.16/36.69 % (741930)CaDiCaL version: 2.1.3 % 252.16/36.69 % (741930)Termination reason: Unknown % 252.16/36.69 % (741930)Termination phase: Saturation % 252.16/36.69 % (741930)Time elapsed: 0.360 s % 252.16/36.69 % (741930)Peak memory usage: 113 MB % 252.16/36.69 % (741930)Instructions burned: 542 (million) % 252.16/36.69 % (741931)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 252.16/36.69 % (741931)------------------------------ % 252.16/36.69 % (741931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.16/36.69 % (741931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.16/36.69 % (741931)CaDiCaL version: 2.1.3 % 252.16/36.69 % (741931)Termination reason: Unknown % 252.16/36.69 % (741931)Termination phase: Saturation % 252.16/36.69 % (741931)Time elapsed: 0.360 s % 252.16/36.69 % (741931)Peak memory usage: 113 MB % 252.16/36.69 % (741931)Instructions burned: 542 (million) % 256.69/37.21 % (741936)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=4175744266:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2671 on theBenchmark for (2671ds/92981Mi) % 256.69/37.21 % (741937)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=3808143748:s2pl=on:i=49423_2669 on theBenchmark for (2669ds/49423Mi) % 256.69/37.21 % (741936)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 256.69/37.21 % (741936)------------------------------ % 256.69/37.21 % (741936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.69/37.21 % (741936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.69/37.21 % (741936)CaDiCaL version: 2.1.3 % 256.69/37.21 % (741936)Termination reason: Unknown % 256.69/37.21 % (741936)Termination phase: Saturation % 256.69/37.21 % (741936)Time elapsed: 0.359 s % 256.69/37.21 % (741936)Peak memory usage: 114 MB % 256.69/37.21 % (741936)Instructions burned: 542 (million) % 256.69/37.21 % (741937)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 256.69/37.21 % (741937)------------------------------ % 256.69/37.21 % (741937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.69/37.21 % (741937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.69/37.21 % (741937)CaDiCaL version: 2.1.3 % 256.69/37.21 % (741937)Termination reason: Unknown % 256.69/37.21 % (741937)Termination phase: Saturation % 256.69/37.21 % (741937)Time elapsed: 0.360 s % 256.69/37.21 % (741937)Peak memory usage: 114 MB % 256.69/37.21 % (741937)Instructions burned: 542 (million) % 256.69/37.21 % (741940)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=368590814:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2665 on theBenchmark for (2665ds/57299Mi) % 256.69/37.21 % (741941)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=4246920596:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2664 on theBenchmark for (2664ds/127679Mi) % 256.69/37.21 % (741940)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 256.69/37.21 % (741940)------------------------------ % 256.69/37.21 % (741940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.69/37.21 % (741940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.69/37.21 % (741940)CaDiCaL version: 2.1.3 % 256.69/37.21 % (741940)Termination reason: Unknown % 256.69/37.21 % (741940)Termination phase: Saturation % 256.69/37.21 % (741940)Time elapsed: 0.360 s % 256.69/37.21 % (741940)Peak memory usage: 113 MB % 256.69/37.21 % (741940)Instructions burned: 542 (million) % 256.69/37.21 % (741941)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 256.69/37.21 % (741941)------------------------------ % 256.69/37.21 % (741941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.69/37.21 % (741941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.69/37.21 % (741941)CaDiCaL version: 2.1.3 % 256.69/37.21 % (741941)Termination reason: Unknown % 256.69/37.21 % (741941)Termination phase: Saturation % 256.69/37.21 % (741941)Time elapsed: 0.357 s % 256.69/37.21 % (741941)Peak memory usage: 114 MB % 256.69/37.21 % (741941)Instructions burned: 541 (million) % 256.69/37.21 % (741944)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=1141234706:i=69402:add=on:aac=none:fsr=off_2660 on theBenchmark for (2660ds/69402Mi) % 256.69/37.21 % (741945)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=2319039342:i=100512:doe=on:fgj=on:bd=all:fsd=on_2659 on theBenchmark for (2659ds/100512Mi) % 256.69/37.21 % (741944)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 256.69/37.21 % (741944)------------------------------ % 256.69/37.21 % (741944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 256.69/37.21 % (741944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 256.69/37.21 % (741944)CaDiCaL version: 2.1.3 % 261.47/37.91 % (741944)Termination reason: Unknown % 261.47/37.91 % (741944)Termination phase: Saturation % 261.47/37.91 % (741944)Time elapsed: 0.359 s % 261.47/37.91 % (741944)Peak memory usage: 113 MB % 261.47/37.91 % (741944)Instructions burned: 541 (million) % 261.47/37.91 % (741945)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 261.47/37.91 % (741945)------------------------------ % 261.47/37.91 % (741945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.47/37.91 % (741945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.47/37.91 % (741945)CaDiCaL version: 2.1.3 % 261.47/37.91 % (741945)Termination reason: Unknown % 261.47/37.91 % (741945)Termination phase: Saturation % 261.47/37.91 % (741945)Time elapsed: 0.358 s % 261.47/37.91 % (741945)Peak memory usage: 113 MB % 261.47/37.91 % (741945)Instructions burned: 542 (million) % 261.47/37.91 % (741948)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=1691768513:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2655 on theBenchmark for (2655ds/138761Mi) % 261.47/37.91 % (741949)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=4018163186:i=282386:rtra=on_2653 on theBenchmark for (2653ds/282386Mi) % 261.47/37.91 % (741948)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 261.47/37.91 % (741948)------------------------------ % 261.47/37.91 % (741948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.47/37.91 % (741948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.47/37.91 % (741948)CaDiCaL version: 2.1.3 % 261.47/37.91 % (741948)Termination reason: Unknown % 261.47/37.91 % (741948)Termination phase: Saturation % 261.47/37.91 % (741948)Time elapsed: 0.359 s % 261.47/37.91 % (741948)Peak memory usage: 113 MB % 261.47/37.91 % (741948)Instructions burned: 541 (million) % 261.47/37.91 % (741949)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 261.47/37.91 % (741949)------------------------------ % 261.47/37.91 % (741949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.47/37.91 % (741949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.47/37.91 % (741949)CaDiCaL version: 2.1.3 % 261.47/37.91 % (741949)Termination reason: Unknown % 261.47/37.91 % (741949)Termination phase: Saturation % 261.47/37.91 % (741949)Time elapsed: 0.359 s % 261.47/37.91 % (741949)Peak memory usage: 114 MB % 261.47/37.91 % (741949)Instructions burned: 541 (million) % 261.47/37.91 % (741952)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=3492401291:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2649 on theBenchmark for (2649ds/269354Mi) % 261.47/37.91 % (741953)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=2595831802:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2648 on theBenchmark for (2648ds/283390Mi) % 261.47/37.91 % (741953)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 261.47/37.91 % (741952)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 261.47/37.91 % (741952)------------------------------ % 261.47/37.91 % (741952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.47/37.91 % (741952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.47/37.91 % (741952)CaDiCaL version: 2.1.3 % 261.47/37.91 % (741952)Termination reason: Unknown % 261.47/37.91 % (741952)Termination phase: Saturation % 261.47/37.91 % (741952)Time elapsed: 0.359 s % 261.47/37.91 % (741952)Peak memory usage: 114 MB % 261.47/37.91 % (741952)Instructions burned: 544 (million) % 261.47/37.91 % (741953)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 261.47/37.91 % (741953)------------------------------ % 261.47/37.91 % (741953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.47/37.91 % (741953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.47/37.91 % (741953)CaDiCaL version: 2.1.3 % 261.47/37.91 % (741953)Termination reason: Unknown % 261.47/37.91 % (741953)Termination phase: Saturation % 261.47/37.91 % (741953)Time elapsed: 0.359 s % 261.47/37.91 % (741953)Peak memory usage: 114 MB % 261.47/37.91 % (741953)Instructions burned: 542 (million) % 261.47/37.91 % (741956)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2179626226:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2644 on theBenchmark for (2644ds/218Mi) % 267.41/38.75 % (741956)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 267.41/38.75 % (741957)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=3482539733:i=238:av=off:rtra=on:ss=axioms_2643 on theBenchmark for (2643ds/238Mi) % 267.41/38.75 % (741670)Instruction limit reached! % 267.41/38.75 % (741670)------------------------------ % 267.41/38.75 % (741670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.41/38.75 % (741670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.41/38.75 % (741670)CaDiCaL version: 2.1.3 % 267.41/38.75 % (741670)Termination reason: Instruction limit % 267.41/38.75 % (741670)Termination phase: Saturation % 267.41/38.75 % (741670)Time elapsed: 19.654 s % 267.41/38.75 % (741670)Peak memory usage: 204 MB % 267.41/38.75 % (741670)Instructions burned: 43699 (million) % 267.41/38.75 % (741956)Instruction limit reached! % 267.41/38.75 % (741956)------------------------------ % 267.41/38.75 % (741956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.41/38.75 % (741956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.41/38.75 % (741956)CaDiCaL version: 2.1.3 % 267.41/38.75 % (741956)Termination reason: Instruction limit % 267.41/38.75 % (741956)Termination phase: Saturation % 267.41/38.75 % (741956)Time elapsed: 0.134 s % 267.41/38.75 % (741956)Peak memory usage: 90 MB % 267.41/38.75 % (741956)Instructions burned: 219 (million) % 267.41/38.75 % (741957)Instruction limit reached! % 267.41/38.75 % (741957)------------------------------ % 267.41/38.75 % (741957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.41/38.75 % (741957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.41/38.75 % (741957)CaDiCaL version: 2.1.3 % 267.41/38.75 % (741957)Termination reason: Instruction limit % 267.41/38.75 % (741957)Termination phase: Saturation % 267.41/38.75 % (741957)Time elapsed: 0.116 s % 267.41/38.75 % (741957)Peak memory usage: 89 MB % 267.41/38.75 % (741957)Instructions burned: 239 (million) % 267.41/38.75 % (741960)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=452366009:s2a=on:i=278:rtra=on:gtg=position_2641 on theBenchmark for (2641ds/278Mi) % 267.41/38.75 % (741961)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=3945334213:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2641 on theBenchmark for (2641ds/258Mi) % 267.41/38.75 % (741960)Instruction limit reached! % 267.41/38.75 % (741960)------------------------------ % 267.41/38.75 % (741960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.41/38.75 % (741960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.41/38.75 % (741960)CaDiCaL version: 2.1.3 % 267.41/38.75 % (741960)Termination reason: Instruction limit % 267.41/38.75 % (741960)Termination phase: Saturation % 267.41/38.75 % (741960)Time elapsed: 0.077 s % 267.41/38.75 % (741960)Peak memory usage: 91 MB % 267.41/38.75 % (741960)Instructions burned: 279 (million) % 267.41/38.75 % (741962)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=71380694:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2640 on theBenchmark for (2640ds/570Mi) % 267.41/38.75 % (741965)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=2480385895:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2639 on theBenchmark for (2639ds/314Mi) % 267.41/38.75 % (741961)Instruction limit reached! % 267.41/38.75 % (741961)------------------------------ % 267.41/38.75 % (741961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.41/38.75 % (741961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.41/38.75 % (741961)CaDiCaL version: 2.1.3 % 267.41/38.75 % (741961)Termination reason: Instruction limit % 267.41/38.75 % (741961)Termination phase: Saturation % 267.41/38.75 % (741961)Time elapsed: 0.150 s % 267.41/38.75 % (741961)Peak memory usage: 90 MB % 267.41/38.75 % (741961)Instructions burned: 259 (million) % 267.41/38.75 % (741965)Instruction limit reached! % 267.41/38.75 % (741965)------------------------------ % 267.41/38.75 % (741965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 267.41/38.75 % (741965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 267.41/38.75 % (741965)CaDiCaL version: 2.1.3 % 267.41/38.75 % (741965)Termination reason: Instruction limit % 267.41/38.75 % (741965)Termination phase: Saturation % 267.41/38.75 % (741965)Time elapsed: 0.090 s % 267.41/38.75 % (741965)Peak memory usage: 91 MB % 267.41/38.75 % (741965)Instructions burned: 316 (million) % 270.91/39.29 % (741968)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=2922370099:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2638 on theBenchmark for (2638ds/650Mi) % 270.91/39.29 % (741969)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=1423134443:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2637 on theBenchmark for (2637ds/496Mi) % 270.91/39.29 % (741962)Instruction limit reached! % 270.91/39.29 % (741962)------------------------------ % 270.91/39.29 % (741962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.91/39.29 % (741962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.91/39.29 % (741962)CaDiCaL version: 2.1.3 % 270.91/39.29 % (741962)Termination reason: Instruction limit % 270.91/39.29 % (741962)Termination phase: Saturation % 270.91/39.29 % (741962)Time elapsed: 0.287 s % 270.91/39.29 % (741962)Peak memory usage: 91 MB % 270.91/39.29 % (741962)Instructions burned: 571 (million) % 270.91/39.29 % (741969)Instruction limit reached! % 270.91/39.29 % (741969)------------------------------ % 270.91/39.29 % (741969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.91/39.29 % (741969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.91/39.29 % (741969)CaDiCaL version: 2.1.3 % 270.91/39.29 % (741969)Termination reason: Instruction limit % 270.91/39.29 % (741969)Termination phase: Saturation % 270.91/39.29 % (741969)Time elapsed: 0.141 s % 270.91/39.29 % (741969)Peak memory usage: 93 MB % 270.91/39.29 % (741969)Instructions burned: 496 (million) % 270.91/39.29 % (741972)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=248505170:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2636 on theBenchmark for (2636ds/588Mi) % 270.91/39.29 % (741973)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=3055864666:i=4700:rtra=on_2635 on theBenchmark for (2635ds/4700Mi) % 270.91/39.29 % (741968)Instruction limit reached! % 270.91/39.29 % (741968)------------------------------ % 270.91/39.29 % (741968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.91/39.29 % (741968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.91/39.29 % (741968)CaDiCaL version: 2.1.3 % 270.91/39.29 % (741968)Termination reason: Instruction limit % 270.91/39.29 % (741968)Termination phase: Saturation % 270.91/39.29 % (741968)Time elapsed: 0.331 s % 270.91/39.29 % (741968)Peak memory usage: 92 MB % 270.91/39.29 % (741968)Instructions burned: 651 (million) % 270.91/39.29 % (741976)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2700814001:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2633 on theBenchmark for (2633ds/226Mi) % 270.91/39.29 % (741973)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 270.91/39.29 % (741973)------------------------------ % 270.91/39.29 % (741973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.91/39.29 % (741973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.91/39.29 % (741973)CaDiCaL version: 2.1.3 % 270.91/39.29 % (741973)Termination reason: Unknown % 270.91/39.29 % (741973)Termination phase: Saturation % 270.91/39.29 % (741973)Time elapsed: 0.198 s % 270.91/39.29 % (741973)Peak memory usage: 114 MB % 270.91/39.29 % (741973)Instructions burned: 541 (million) % 270.91/39.29 % (741972)Instruction limit reached! % 270.91/39.29 % (741972)------------------------------ % 270.91/39.29 % (741972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.91/39.29 % (741972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.91/39.29 % (741972)CaDiCaL version: 2.1.3 % 270.91/39.29 % (741972)Termination reason: Instruction limit % 270.91/39.29 % (741972)Termination phase: Saturation % 270.91/39.29 % (741972)Time elapsed: 0.307 s % 270.91/39.29 % (741972)Peak memory usage: 90 MB % 270.91/39.29 % (741972)Instructions burned: 588 (million) % 270.91/39.29 % (741978)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1310733433:i=254:av=off:fsr=off:rtra=on:sup=off_2631 on theBenchmark for (2631ds/254Mi) % 270.91/39.29 % (741978)Refutation not found, incomplete strategy % 270.91/39.29 % (741978)------------------------------ % 270.91/39.29 % (741978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 270.91/39.29 % (741978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 270.91/39.29 % (741978)CaDiCaL version: 2.1.3 % 270.91/39.29 % (741978)Termination reason: Refutation not found, incomplete strategy % 270.91/39.29 % (741978)Time elapsed: 0.002 s % 270.91/39.29 % (741978)Peak memory usage: 88 MB % 277.63/40.15 % (741978)Instructions burned: 7 (million) % 277.63/40.15 % (741976)Instruction limit reached! % 277.63/40.15 % (741976)------------------------------ % 277.63/40.15 % (741976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.63/40.15 % (741976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.63/40.15 % (741976)CaDiCaL version: 2.1.3 % 277.63/40.15 % (741976)Termination reason: Instruction limit % 277.63/40.15 % (741976)Termination phase: Saturation % 277.63/40.15 % (741976)Time elapsed: 0.131 s % 277.63/40.15 % (741976)Peak memory usage: 91 MB % 277.63/40.15 % (741976)Instructions burned: 226 (million) % 277.63/40.15 % (741979)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=150680359:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2631 on theBenchmark for (2631ds/228Mi) % 277.63/40.15 % (741978)------------------------------ % 277.63/40.15 % (741978)------------------------------ % 277.63/40.15 % (741981)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2864531150:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2630 on theBenchmark for (2630ds/1814Mi) % 277.63/40.15 % (741979)Instruction limit reached! % 277.63/40.15 % (741979)------------------------------ % 277.63/40.15 % (741979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.63/40.15 % (741979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.63/40.15 % (741979)CaDiCaL version: 2.1.3 % 277.63/40.15 % (741979)Termination reason: Instruction limit % 277.63/40.15 % (741979)Termination phase: Saturation % 277.63/40.15 % (741979)Time elapsed: 0.112 s % 277.63/40.15 % (741979)Peak memory usage: 89 MB % 277.63/40.15 % (741979)Instructions burned: 229 (million) % 277.63/40.15 % (741983)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=2726888934:i=874:sd=1:aac=none:rtra=on:ss=included_2629 on theBenchmark for (2629ds/874Mi) % 277.63/40.15 % (741985)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3423233856:i=10404:rtra=on:ss=axioms:sgt=16_2628 on theBenchmark for (2628ds/10404Mi) % 277.63/40.15 % (741983)Instruction limit reached! % 277.63/40.15 % (741983)------------------------------ % 277.63/40.15 % (741983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.63/40.15 % (741983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.63/40.15 % (741983)CaDiCaL version: 2.1.3 % 277.63/40.15 % (741983)Termination reason: Instruction limit % 277.63/40.15 % (741983)Termination phase: Saturation % 277.63/40.15 % (741983)Time elapsed: 0.246 s % 277.63/40.15 % (741983)Peak memory usage: 91 MB % 277.63/40.15 % (741983)Instructions burned: 877 (million) % 277.63/40.15 % (741988)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=933231310:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2625 on theBenchmark for (2625ds/268Mi) % 277.63/40.15 % (741985)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 277.63/40.15 % (741985)------------------------------ % 277.63/40.15 % (741985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.63/40.15 % (741985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.63/40.15 % (741985)CaDiCaL version: 2.1.3 % 277.63/40.15 % (741985)Termination reason: Unknown % 277.63/40.15 % (741985)Termination phase: Saturation % 277.63/40.15 % (741985)Time elapsed: 0.358 s % 277.63/40.15 % (741985)Peak memory usage: 113 MB % 277.63/40.15 % (741985)Instructions burned: 543 (million) % 277.63/40.15 % (741988)Instruction limit reached! % 277.63/40.15 % (741988)------------------------------ % 277.63/40.15 % (741988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.63/40.15 % (741988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.63/40.15 % (741988)CaDiCaL version: 2.1.3 % 277.63/40.15 % (741988)Termination reason: Instruction limit % 277.63/40.15 % (741988)Termination phase: Saturation % 277.63/40.15 % (741988)Time elapsed: 0.070 s % 277.63/40.15 % (741988)Peak memory usage: 91 MB % 277.63/40.15 % (741988)Instructions burned: 268 (million) % 277.63/40.15 % (741990)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=2683312193:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2623 on theBenchmark for (2623ds/1184Mi) % 277.63/40.15 % (741990)Refutation not found, incomplete strategy % 277.63/40.15 % (741990)------------------------------ % 277.63/40.15 % (741990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.63/40.15 % (741990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.63/40.15 % (741990)CaDiCaL version: 2.1.3 % 281.77/40.85 % (741990)Termination reason: Refutation not found, incomplete strategy % 281.77/40.85 % (741990)Time elapsed: 0.007 s % 281.77/40.85 % (741990)Peak memory usage: 88 MB % 281.77/40.85 % (741990)Instructions burned: 12 (million) % 281.77/40.85 % (741991)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=2460936637:st=3:i=26386:sd=3:rtra=on:ss=axioms_2623 on theBenchmark for (2623ds/26386Mi) % 281.77/40.85 % (741991)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 281.77/40.85 % (741991)------------------------------ % 281.77/40.85 % (741991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.77/40.85 % (741991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.77/40.85 % (741991)CaDiCaL version: 2.1.3 % 281.77/40.85 % (741991)Termination reason: Unknown % 281.77/40.85 % (741991)Termination phase: Saturation % 281.77/40.85 % (741991)Time elapsed: 0.197 s % 281.77/40.85 % (741991)Peak memory usage: 113 MB % 281.77/40.85 % (741991)Instructions burned: 542 (million) % 281.77/40.85 % (741990)------------------------------ % 281.77/40.85 % (741990)------------------------------ % 281.77/40.85 % (741981)Instruction limit reached! % 281.77/40.85 % (741981)------------------------------ % 281.77/40.85 % (741981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.77/40.85 % (741981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.77/40.85 % (741981)CaDiCaL version: 2.1.3 % 281.77/40.85 % (741981)Termination reason: Instruction limit % 281.77/40.85 % (741981)Termination phase: Saturation % 281.77/40.85 % (741981)Time elapsed: 0.953 s % 281.77/40.85 % (741981)Peak memory usage: 96 MB % 281.77/40.85 % (741981)Instructions burned: 1815 (million) % 281.77/40.85 % (741994)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=450681788:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2620 on theBenchmark for (2620ds/250Mi) % 281.77/40.85 % (741994)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 281.77/40.85 % (741995)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=3043714133:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2619 on theBenchmark for (2619ds/268Mi) % 281.77/40.85 % (741994)Instruction limit reached! % 281.77/40.85 % (741994)------------------------------ % 281.77/40.85 % (741994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.77/40.85 % (741994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.77/40.85 % (741994)CaDiCaL version: 2.1.3 % 281.77/40.85 % (741994)Termination reason: Instruction limit % 281.77/40.85 % (741994)Termination phase: Saturation % 281.77/40.85 % (741994)Time elapsed: 0.078 s % 281.77/40.85 % (741994)Peak memory usage: 90 MB % 281.77/40.85 % (741994)Instructions burned: 252 (million) % 281.77/40.85 % (741996)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3188288785:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2619 on theBenchmark for (2619ds/282Mi) % 281.77/40.85 % (741996)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 281.77/40.85 % (741996)Refutation not found, incomplete strategy % 281.77/40.85 % (741996)------------------------------ % 281.77/40.85 % (741996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.77/40.85 % (741996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.77/40.85 % (741996)CaDiCaL version: 2.1.3 % 281.77/40.85 % (741996)Termination reason: Refutation not found, incomplete strategy % 281.77/40.85 % (741996)Time elapsed: 0.003 s % 281.77/40.85 % (741996)Peak memory usage: 88 MB % 281.77/40.85 % (741996)Instructions burned: 3 (million) % 281.77/40.85 % (741995)Instruction limit reached! % 281.77/40.85 % (741995)------------------------------ % 281.77/40.85 % (741995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.77/40.85 % (741995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.77/40.85 % (741995)CaDiCaL version: 2.1.3 % 281.77/40.85 % (741995)Termination reason: Instruction limit % 281.77/40.85 % (741995)Termination phase: Saturation % 281.77/40.85 % (741995)Time elapsed: 0.142 s % 281.77/40.85 % (741995)Peak memory usage: 90 MB % 281.77/40.85 % (741995)Instructions burned: 268 (million) % 281.77/40.85 % (741999)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=2127957843:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2618 on theBenchmark for (2618ds/862Mi) % 281.77/40.85 % (741999)Refutation not found, incomplete strategy % 294.06/42.58 % (741999)------------------------------ % 294.06/42.58 % (741999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.06/42.58 % (741999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.06/42.58 % (741999)CaDiCaL version: 2.1.3 % 294.06/42.58 % (741999)Termination reason: Refutation not found, incomplete strategy % 294.06/42.58 % (741999)Time elapsed: 0.004 s % 294.06/42.58 % (741999)Peak memory usage: 88 MB % 294.06/42.58 % (741999)Instructions burned: 11 (million) % 294.06/42.58 % (741999)------------------------------ % 294.06/42.58 % (741999)------------------------------ % 294.06/42.58 % (742001)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=3468289494:i=12120:aac=none:ins=25:rtra=on_2617 on theBenchmark for (2617ds/12120Mi) % 294.06/42.58 % (741996)------------------------------ % 294.06/42.58 % (741996)------------------------------ % 294.06/42.58 % (742004)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=286081577:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2615 on theBenchmark for (2615ds/300Mi) % 294.06/42.58 % (742004)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 294.06/42.58 % (742005)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=3296355124:i=28310:bd=all:rtra=on_2615 on theBenchmark for (2615ds/28310Mi) % 294.06/42.58 % (742004)Instruction limit reached! % 294.06/42.58 % (742004)------------------------------ % 294.06/42.58 % (742004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.06/42.58 % (742004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.06/42.58 % (742004)CaDiCaL version: 2.1.3 % 294.06/42.58 % (742004)Termination reason: Instruction limit % 294.06/42.58 % (742004)Termination phase: Saturation % 294.06/42.58 % (742004)Time elapsed: 0.095 s % 294.06/42.58 % (742004)Peak memory usage: 92 MB % 294.06/42.58 % (742004)Instructions burned: 302 (million) % 294.06/42.58 % (742008)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1958256701:i=1334:av=off:fsr=off:rtra=on_2613 on theBenchmark for (2613ds/1334Mi) % 294.06/42.58 % (742001)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 294.06/42.58 % (742001)------------------------------ % 294.06/42.58 % (742001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.06/42.58 % (742001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.06/42.58 % (742001)CaDiCaL version: 2.1.3 % 294.06/42.58 % (742001)Termination reason: Unknown % 294.06/42.58 % (742001)Termination phase: Saturation % 294.06/42.58 % (742001)Time elapsed: 0.363 s % 294.06/42.58 % (742001)Peak memory usage: 114 MB % 294.06/42.58 % (742001)Instructions burned: 541 (million) % 294.06/42.58 % (742010)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=2883536640:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2611 on theBenchmark for (2611ds/370Mi) % 294.06/42.58 % (742005)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 294.06/42.58 % (742005)------------------------------ % 294.06/42.58 % (742005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.06/42.58 % (742005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.06/42.58 % (742005)CaDiCaL version: 2.1.3 % 294.06/42.58 % (742005)Termination reason: Unknown % 294.06/42.58 % (742005)Termination phase: Saturation % 294.06/42.58 % (742005)Time elapsed: 0.365 s % 294.06/42.58 % (742005)Peak memory usage: 113 MB % 294.06/42.58 % (742005)Instructions burned: 541 (million) % 294.06/42.58 % (742008)Instruction limit reached! % 294.06/42.58 % (742008)------------------------------ % 294.06/42.58 % (742008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 294.06/42.58 % (742008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 294.06/42.58 % (742008)CaDiCaL version: 2.1.3 % 294.06/42.58 % (742008)Termination reason: Instruction limit % 294.06/42.58 % (742008)Termination phase: Saturation % 294.06/42.58 % (742008)Time elapsed: 0.313 s % 294.06/42.58 % (742008)Peak memory usage: 89 MB % 294.06/42.58 % (742008)Instructions burned: 1336 (million) % 294.06/42.58 % (742012)dis+1010_14_anc=all:to=lpo:sil=Terminated %------------------------------------------------------------------------------