%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM968_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 12:17:43 PM UTC 2026 % Result : Timeout 297.13s 42.76s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM968_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.37 % Computer : n005.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.09/0.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Sun Sep 27 21:48:32 UTC 2026 % 0.09/0.37 % CPUTime : % 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.41 Running first-order theorem proving % 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.60/1.77 % (201118)Detected formulas, will run a generic FOF schedule. % 4.60/1.77 % (201124)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=1253340001:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 4.60/1.77 % (201129)dis-21_1_sil=8000:lcm=predicate:random_seed=1837536218:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 4.60/1.77 % (201125)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=3610804808:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 4.60/1.77 % (201123)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=550801187:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 4.60/1.77 % (201128)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4046440127:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 4.60/1.77 % (201127)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=557987143:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 4.60/1.77 % (201126)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=46233891:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 4.60/1.77 % (201126)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.60/1.77 % (201125)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 4.60/1.77 % (201126)Instruction limit reached! % 4.60/1.77 % (201126)------------------------------ % 4.60/1.77 % (201126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.60/1.77 % (201126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.60/1.77 % (201126)CaDiCaL version: 2.1.3 % 4.60/1.77 % (201126)Termination reason: Instruction limit % 4.60/1.77 % (201126)Termination phase: Saturation % 4.60/1.77 % (201126)Time elapsed: 0.060 s % 4.60/1.77 % (201126)Peak memory usage: 89 MB % 4.60/1.77 % (201126)Instructions burned: 110 (million) % 4.60/1.77 % (201127)Instruction limit reached! % 4.60/1.77 % (201127)------------------------------ % 4.60/1.77 % (201127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.60/1.77 % (201127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.60/1.77 % (201127)CaDiCaL version: 2.1.3 % 4.60/1.77 % (201127)Termination reason: Instruction limit % 4.60/1.77 % (201127)Termination phase: Saturation % 4.60/1.77 % (201127)Time elapsed: 0.065 s % 4.60/1.77 % (201127)Peak memory usage: 88 MB % 4.60/1.77 % (201127)Instructions burned: 120 (million) % 4.60/1.77 % (201129)Instruction limit reached! % 4.60/1.77 % (201129)------------------------------ % 4.60/1.77 % (201129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.60/1.77 % (201129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.60/1.77 % (201129)CaDiCaL version: 2.1.3 % 4.60/1.77 % (201129)Termination reason: Instruction limit % 4.60/1.77 % (201129)Termination phase: Saturation % 4.60/1.77 % (201129)Time elapsed: 0.073 s % 4.60/1.77 % (201129)Peak memory usage: 89 MB % 4.60/1.77 % (201129)Instructions burned: 130 (million) % 4.60/1.77 % (201128)Instruction limit reached! % 4.60/1.77 % (201128)------------------------------ % 4.60/1.77 % (201128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.60/1.77 % (201128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.60/1.77 % (201128)CaDiCaL version: 2.1.3 % 4.60/1.77 % (201128)Termination reason: Instruction limit % 4.60/1.77 % (201128)Termination phase: Saturation % 4.60/1.77 % (201128)Time elapsed: 0.084 s % 4.60/1.77 % (201128)Peak memory usage: 89 MB % 4.60/1.77 % (201128)Instructions burned: 139 (million) % 4.60/1.77 % (201124)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.60/1.77 % (201124)------------------------------ % 4.60/1.77 % (201124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.60/1.77 % (201124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.60/1.77 % (201124)CaDiCaL version: 2.1.3 % 4.60/1.77 % (201124)Termination reason: Unknown % 4.60/1.77 % (201124)Termination phase: Saturation % 4.60/1.77 % (201124)Time elapsed: 0.200 s % 4.60/1.77 % (201124)Peak memory usage: 114 MB % 8.61/2.03 % (201124)Instructions burned: 544 (million) % 8.61/2.03 % (201139)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4123014057:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 8.61/2.03 % (201137)lrs+10_1_sil=8000:sp=occurrence:random_seed=3118515723:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 8.61/2.03 % (201138)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4036506056:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 8.61/2.03 % (201140)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=2584800981:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 8.61/2.03 % (201141)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4024960524:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 8.61/2.03 % (201141)Refutation not found, incomplete strategy % 8.61/2.03 % (201141)------------------------------ % 8.61/2.03 % (201141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.61/2.03 % (201141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/2.03 % (201141)CaDiCaL version: 2.1.3 % 8.61/2.03 % (201141)Termination reason: Refutation not found, incomplete strategy % 8.61/2.03 % (201141)Time elapsed: 0.003 s % 8.61/2.03 % (201141)Peak memory usage: 89 MB % 8.61/2.03 % (201141)Instructions burned: 8 (million) % 8.61/2.03 % (201138)Instruction limit reached! % 8.61/2.03 % (201138)------------------------------ % 8.61/2.03 % (201138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.61/2.03 % (201138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/2.03 % (201138)CaDiCaL version: 2.1.3 % 8.61/2.03 % (201138)Termination reason: Instruction limit % 8.61/2.03 % (201138)Termination phase: Saturation % 8.61/2.03 % (201138)Time elapsed: 0.090 s % 8.61/2.03 % (201138)Peak memory usage: 90 MB % 8.61/2.03 % (201138)Instructions burned: 159 (million) % 8.61/2.03 % (201123)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.61/2.03 % (201125)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.61/2.03 % (201123)------------------------------ % 8.61/2.03 % (201123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.61/2.03 % (201125)------------------------------ % 8.61/2.03 % (201125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.61/2.03 % (201123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/2.03 % (201125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/2.03 % (201123)CaDiCaL version: 2.1.3 % 8.61/2.03 % (201125)CaDiCaL version: 2.1.3 % 8.61/2.03 % (201123)Termination reason: Unknown % 8.61/2.03 % (201123)Termination phase: Saturation % 8.61/2.03 % (201125)Termination reason: Unknown % 8.61/2.03 % (201125)Termination phase: Saturation % 8.61/2.03 % (201123)Time elapsed: 0.364 s % 8.61/2.03 % (201125)Time elapsed: 0.364 s % 8.61/2.03 % (201123)Peak memory usage: 112 MB % 8.61/2.03 % (201125)Peak memory usage: 112 MB % 8.61/2.03 % (201125)Instructions burned: 540 (million) % 8.61/2.03 % (201123)Instructions burned: 541 (million) % 8.61/2.03 % (201137)Instruction limit reached! % 8.61/2.03 % (201137)------------------------------ % 8.61/2.03 % (201137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.61/2.03 % (201137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/2.03 % (201137)CaDiCaL version: 2.1.3 % 8.61/2.03 % (201137)Termination reason: Instruction limit % 8.61/2.03 % (201137)Termination phase: Saturation % 8.61/2.03 % (201137)Time elapsed: 0.166 s % 8.61/2.03 % (201137)Peak memory usage: 90 MB % 8.61/2.03 % (201137)Instructions burned: 285 (million) % 8.61/2.03 % (201140)Instruction limit reached! % 8.61/2.03 % (201140)------------------------------ % 8.61/2.03 % (201140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.61/2.03 % (201140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/2.03 % (201140)CaDiCaL version: 2.1.3 % 8.61/2.03 % (201140)Termination reason: Instruction limit % 8.61/2.03 % (201140)Termination phase: Saturation % 8.61/2.03 % (201140)Time elapsed: 0.145 s % 8.61/2.03 % (201140)Peak memory usage: 90 MB % 8.61/2.03 % (201140)Instructions burned: 248 (million) % 8.61/2.03 % (201139)Instruction limit reached! % 8.61/2.03 % (201139)------------------------------ % 8.61/2.03 % (201139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.31 % (201139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.31 % (201139)CaDiCaL version: 2.1.3 % 9.94/2.31 % (201139)Termination reason: Instruction limit % 9.94/2.31 % (201139)Termination phase: Saturation % 9.94/2.31 % (201139)Time elapsed: 0.182 s % 9.94/2.31 % (201139)Peak memory usage: 90 MB % 9.94/2.31 % (201139)Instructions burned: 326 (million) % 9.94/2.31 % (201141)------------------------------ % 9.94/2.31 % (201141)------------------------------ % 9.94/2.31 % (201147)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4098133252:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 9.94/2.31 % (201149)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3267778184:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 9.94/2.31 % (201148)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3159970502:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 9.94/2.31 % (201149)Refutation not found, incomplete strategy % 9.94/2.31 % (201149)------------------------------ % 9.94/2.31 % (201149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.31 % (201149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.31 % (201149)CaDiCaL version: 2.1.3 % 9.94/2.31 % (201149)Termination reason: Refutation not found, incomplete strategy % 9.94/2.31 % (201149)Time elapsed: 0.006 s % 9.94/2.31 % (201149)Peak memory usage: 88 MB % 9.94/2.31 % (201149)Instructions burned: 9 (million) % 9.94/2.31 % (201152)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3954333841:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi) % 9.94/2.31 % (201151)lrs+10_1_sil=8000:sp=occurrence:random_seed=1268244258:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 9.94/2.31 % (201150)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3104348668:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 9.94/2.31 % (201153)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1389421156:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi) % 9.94/2.31 % (201150)Refutation not found, incomplete strategy % 9.94/2.31 % (201150)------------------------------ % 9.94/2.31 % (201150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.31 % (201150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.31 % (201150)CaDiCaL version: 2.1.3 % 9.94/2.31 % (201150)Termination reason: Refutation not found, incomplete strategy % 9.94/2.31 % (201150)Time elapsed: 0.004 s % 9.94/2.31 % (201150)Peak memory usage: 88 MB % 9.94/2.31 % (201150)Instructions burned: 5 (million) % 9.94/2.31 % (201152)Refutation not found, incomplete strategy % 9.94/2.31 % (201152)------------------------------ % 9.94/2.31 % (201152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.31 % (201152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.31 % (201152)CaDiCaL version: 2.1.3 % 9.94/2.31 % (201152)Termination reason: Refutation not found, incomplete strategy % 9.94/2.31 % (201152)Time elapsed: 0.006 s % 9.94/2.31 % (201152)Peak memory usage: 88 MB % 9.94/2.31 % (201152)Instructions burned: 9 (million) % 9.94/2.31 % (201148)Instruction limit reached! % 9.94/2.31 % (201148)------------------------------ % 9.94/2.31 % (201148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.31 % (201148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.31 % (201148)CaDiCaL version: 2.1.3 % 9.94/2.31 % (201148)Termination reason: Instruction limit % 9.94/2.31 % (201148)Termination phase: Saturation % 9.94/2.31 % (201148)Time elapsed: 0.070 s % 9.94/2.31 % (201148)Peak memory usage: 90 MB % 9.94/2.31 % (201148)Instructions burned: 114 (million) % 9.94/2.31 % (201153)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.94/2.31 % (201153)------------------------------ % 9.94/2.31 % (201153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.94/2.31 % (201153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.94/2.31 % (201153)CaDiCaL version: 2.1.3 % 9.94/2.31 % (201153)Termination reason: Unknown % 9.94/2.31 % (201153)Termination phase: Saturation % 9.94/2.31 % (201153)Time elapsed: 0.200 s % 9.94/2.31 % (201153)Peak memory usage: 113 MB % 11.32/2.66 % (201153)Instructions burned: 543 (million) % 11.32/2.66 % (201161)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3178389010:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 11.32/2.66 % (201149)------------------------------ % 11.32/2.66 % (201149)------------------------------ % 11.32/2.66 % (201152)------------------------------ % 11.32/2.66 % (201152)------------------------------ % 11.32/2.66 % (201150)------------------------------ % 11.32/2.66 % (201150)------------------------------ % 11.32/2.66 % (201147)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.32/2.66 % (201147)------------------------------ % 11.32/2.66 % (201147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.66 % (201147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.66 % (201147)CaDiCaL version: 2.1.3 % 11.32/2.66 % (201147)Termination reason: Unknown % 11.32/2.66 % (201147)Termination phase: Saturation % 11.32/2.66 % (201147)Time elapsed: 0.366 s % 11.32/2.66 % (201147)Peak memory usage: 114 MB % 11.32/2.66 % (201147)Instructions burned: 541 (million) % 11.32/2.66 % (201161)Instruction limit reached! % 11.32/2.66 % (201161)------------------------------ % 11.32/2.66 % (201161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.66 % (201161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.66 % (201161)CaDiCaL version: 2.1.3 % 11.32/2.66 % (201161)Termination reason: Instruction limit % 11.32/2.66 % (201161)Termination phase: Saturation % 11.32/2.66 % (201161)Time elapsed: 0.078 s % 11.32/2.66 % (201161)Peak memory usage: 90 MB % 11.32/2.66 % (201161)Instructions burned: 136 (million) % 11.32/2.66 % (201162)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1002110771:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi) % 11.32/2.66 % (201164)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3918398732:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi) % 11.32/2.66 % (201165)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=3357779961:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 11.32/2.66 % (201166)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1587012775:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 11.32/2.66 % (201165)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.32/2.66 % (201167)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2413422985:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi) % 11.32/2.66 % (201168)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2610896905:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/431Mi) % 11.32/2.66 % (201167)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.32/2.66 % (201167)Refutation not found, incomplete strategy % 11.32/2.66 % (201167)------------------------------ % 11.32/2.66 % (201167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.66 % (201167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.66 % (201167)CaDiCaL version: 2.1.3 % 11.32/2.66 % (201167)Termination reason: Refutation not found, incomplete strategy % 11.32/2.66 % (201167)Time elapsed: 0.002 s % 11.32/2.66 % (201167)Peak memory usage: 88 MB % 11.32/2.66 % (201167)Instructions burned: 2 (million) % 11.32/2.66 % (201168)Refutation not found, incomplete strategy % 11.32/2.66 % (201168)------------------------------ % 11.32/2.66 % (201168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.66 % (201168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.32/2.66 % (201168)CaDiCaL version: 2.1.3 % 11.32/2.66 % (201168)Termination reason: Refutation not found, incomplete strategy % 11.32/2.66 % (201168)Time elapsed: 0.005 s % 11.32/2.66 % (201168)Peak memory usage: 88 MB % 11.32/2.66 % (201168)Instructions burned: 6 (million) % 11.32/2.66 % (201165)Instruction limit reached! % 11.32/2.66 % (201165)------------------------------ % 11.32/2.66 % (201165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.32/2.66 % (201165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.70/3.11 % (201165)CaDiCaL version: 2.1.3 % 15.70/3.11 % (201165)Termination reason: Instruction limit % 15.70/3.11 % (201165)Termination phase: Saturation % 15.70/3.11 % (201165)Time elapsed: 0.070 s % 15.70/3.11 % (201165)Peak memory usage: 90 MB % 15.70/3.11 % (201165)Instructions burned: 125 (million) % 15.70/3.11 % (201166)Instruction limit reached! % 15.70/3.11 % (201166)------------------------------ % 15.70/3.11 % (201166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.70/3.11 % (201166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.70/3.11 % (201166)CaDiCaL version: 2.1.3 % 15.70/3.11 % (201166)Termination reason: Instruction limit % 15.70/3.11 % (201166)Termination phase: Saturation % 15.70/3.11 % (201166)Time elapsed: 0.084 s % 15.70/3.11 % (201166)Peak memory usage: 90 MB % 15.70/3.11 % (201166)Instructions burned: 134 (million) % 15.70/3.11 % (201151)Instruction limit reached! % 15.70/3.11 % (201151)------------------------------ % 15.70/3.11 % (201151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.70/3.11 % (201151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.70/3.11 % (201151)CaDiCaL version: 2.1.3 % 15.70/3.11 % (201151)Termination reason: Instruction limit % 15.70/3.11 % (201151)Termination phase: Saturation % 15.70/3.11 % (201151)Time elapsed: 0.524 s % 15.70/3.11 % (201151)Peak memory usage: 95 MB % 15.70/3.11 % (201151)Instructions burned: 908 (million) % 15.70/3.11 % (201162)Instruction limit reached! % 15.70/3.11 % (201162)------------------------------ % 15.70/3.11 % (201162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.70/3.11 % (201162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.70/3.11 % (201162)CaDiCaL version: 2.1.3 % 15.70/3.11 % (201162)Termination reason: Instruction limit % 15.70/3.11 % (201162)Termination phase: Saturation % 15.70/3.11 % (201162)Time elapsed: 0.227 s % 15.70/3.11 % (201162)Peak memory usage: 94 MB % 15.70/3.11 % (201162)Instructions burned: 594 (million) % 15.70/3.11 % (201175)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=2288193105:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi) % 15.70/3.11 % (201176)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=4138002173:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi) % 15.70/3.11 % (201176)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 15.70/3.11 % (201168)------------------------------ % 15.70/3.11 % (201168)------------------------------ % 15.70/3.11 % (201167)------------------------------ % 15.70/3.11 % (201167)------------------------------ % 15.70/3.11 % (201177)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2841069303:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi) % 15.70/3.11 % (201178)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=106350522:i=667:av=off:fsr=off_2986 on theBenchmark for (2986ds/667Mi) % 15.70/3.11 % (201178)Refutation not found, incomplete strategy % 15.70/3.11 % (201178)------------------------------ % 15.70/3.11 % (201178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.70/3.11 % (201178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.70/3.11 % (201178)CaDiCaL version: 2.1.3 % 15.70/3.11 % (201178)Termination reason: Refutation not found, incomplete strategy % 15.70/3.11 % (201178)Time elapsed: 0.003 s % 15.70/3.11 % (201178)Peak memory usage: 88 MB % 15.70/3.11 % (201178)Instructions burned: 8 (million) % 15.70/3.11 % (201176)Instruction limit reached! % 15.70/3.11 % (201176)------------------------------ % 15.70/3.11 % (201176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.70/3.11 % (201176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.70/3.11 % (201176)CaDiCaL version: 2.1.3 % 15.70/3.11 % (201176)Termination reason: Instruction limit % 15.70/3.11 % (201176)Termination phase: Saturation % 15.70/3.11 % (201176)Time elapsed: 0.092 s % 15.70/3.11 % (201176)Peak memory usage: 90 MB % 15.70/3.11 % (201176)Instructions burned: 151 (million) % 15.70/3.11 % (201164)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.70/3.11 % (201164)------------------------------ % 15.70/3.11 % (201164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.86/3.78 % (201164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.86/3.78 % (201164)CaDiCaL version: 2.1.3 % 18.86/3.78 % (201164)Termination reason: Unknown % 18.86/3.78 % (201164)Termination phase: Saturation % 18.86/3.78 % (201164)Time elapsed: 0.367 s % 18.86/3.78 % (201164)Peak memory usage: 113 MB % 18.86/3.78 % (201164)Instructions burned: 540 (million) % 18.86/3.78 % (201183)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1960367332:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2985 on theBenchmark for (2985ds/193Mi) % 18.86/3.78 % (201182)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=3147920851:s2a=on:i=185:s2at=1.8:fdi=4_2985 on theBenchmark for (2985ds/185Mi) % 18.86/3.78 % (201178)------------------------------ % 18.86/3.78 % (201178)------------------------------ % 18.86/3.78 % (201185)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=308650350:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi) % 18.86/3.78 % (201185)Refutation not found, incomplete strategy % 18.86/3.78 % (201185)------------------------------ % 18.86/3.78 % (201185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.86/3.78 % (201185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.86/3.78 % (201185)CaDiCaL version: 2.1.3 % 18.86/3.78 % (201185)Termination reason: Refutation not found, incomplete strategy % 18.86/3.78 % (201185)Time elapsed: 0.005 s % 18.86/3.78 % (201185)Peak memory usage: 88 MB % 18.86/3.78 % (201185)Instructions burned: 7 (million) % 18.86/3.78 % (201186)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3389790103:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi) % 18.86/3.78 % (201183)Instruction limit reached! % 18.86/3.78 % (201183)------------------------------ % 18.86/3.78 % (201183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.86/3.78 % (201183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.86/3.78 % (201183)CaDiCaL version: 2.1.3 % 18.86/3.78 % (201183)Termination reason: Instruction limit % 18.86/3.78 % (201183)Termination phase: Saturation % 18.86/3.78 % (201183)Time elapsed: 0.100 s % 18.86/3.78 % (201183)Peak memory usage: 89 MB % 18.86/3.78 % (201183)Instructions burned: 194 (million) % 18.86/3.78 % (201182)Instruction limit reached! % 18.86/3.78 % (201182)------------------------------ % 18.86/3.78 % (201182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.86/3.78 % (201182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.86/3.78 % (201182)CaDiCaL version: 2.1.3 % 18.86/3.78 % (201182)Termination reason: Instruction limit % 18.86/3.78 % (201182)Termination phase: Saturation % 18.86/3.78 % (201182)Time elapsed: 0.110 s % 18.86/3.78 % (201182)Peak memory usage: 90 MB % 18.86/3.78 % (201182)Instructions burned: 185 (million) % 18.86/3.78 % (201175)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.86/3.78 % (201175)------------------------------ % 18.86/3.78 % (201175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.86/3.78 % (201175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.86/3.78 % (201175)CaDiCaL version: 2.1.3 % 18.86/3.78 % (201175)Termination reason: Unknown % 18.86/3.78 % (201175)Termination phase: Saturation % 18.86/3.78 % (201175)Time elapsed: 0.369 s % 18.86/3.78 % (201175)Peak memory usage: 114 MB % 18.86/3.78 % (201175)Instructions burned: 541 (million) % 18.86/3.78 % (201189)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=489765040:i=319:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/319Mi) % 18.86/3.78 % (201177)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.86/3.78 % (201177)------------------------------ % 18.86/3.78 % (201177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.86/3.78 % (201177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.86/3.78 % (201177)CaDiCaL version: 2.1.3 % 18.86/3.78 % (201177)Termination reason: Unknown % 18.86/3.78 % (201177)Termination phase: Saturation % 18.86/3.78 % (201177)Time elapsed: 0.371 s % 18.86/3.78 % (201177)Peak memory usage: 114 MB % 18.86/3.78 % (201177)Instructions burned: 541 (million) % 18.86/3.78 % (201192)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1322513587:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi) % 24.29/4.30 % (201189)Instruction limit reached! % 24.29/4.30 % (201189)------------------------------ % 24.29/4.30 % (201189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.29/4.30 % (201189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.29/4.30 % (201189)CaDiCaL version: 2.1.3 % 24.29/4.30 % (201189)Termination reason: Instruction limit % 24.29/4.30 % (201189)Termination phase: Saturation % 24.29/4.30 % (201189)Time elapsed: 0.111 s % 24.29/4.30 % (201189)Peak memory usage: 93 MB % 24.29/4.30 % (201189)Instructions burned: 321 (million) % 24.29/4.30 % (201193)dis-1011_128_sil=32000:random_seed=76387260:i=3706:ep=RST:av=off_2983 on theBenchmark for (2983ds/3706Mi) % 24.29/4.30 % (201185)------------------------------ % 24.29/4.30 % (201185)------------------------------ % 24.29/4.30 % (201194)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1093465093:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2983 on theBenchmark for (2983ds/757Mi) % 24.29/4.30 % (201194)Refutation not found, incomplete strategy % 24.29/4.30 % (201194)------------------------------ % 24.29/4.30 % (201194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.29/4.30 % (201194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.29/4.30 % (201194)CaDiCaL version: 2.1.3 % 24.29/4.30 % (201194)Termination reason: Refutation not found, incomplete strategy % 24.29/4.30 % (201194)Time elapsed: 0.006 s % 24.29/4.30 % (201194)Peak memory usage: 88 MB % 24.29/4.30 % (201194)Instructions burned: 8 (million) % 24.29/4.30 % (201196)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1860200385:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi) % 24.29/4.30 % (201198)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2002622499:i=9925:aac=none_2981 on theBenchmark for (2981ds/9925Mi) % 24.29/4.30 % (201186)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 24.29/4.30 % (201186)------------------------------ % 24.29/4.30 % (201186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.29/4.30 % (201186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.29/4.30 % (201186)CaDiCaL version: 2.1.3 % 24.29/4.30 % (201186)Termination reason: Unknown % 24.29/4.30 % (201186)Termination phase: Saturation % 24.29/4.30 % (201186)Time elapsed: 0.370 s % 24.29/4.30 % (201186)Peak memory usage: 114 MB % 24.29/4.30 % (201186)Instructions burned: 542 (million) % 24.29/4.30 % (201201)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1347532021:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 24.29/4.30 % (201201)Refutation not found, incomplete strategy % 24.29/4.30 % (201201)------------------------------ % 24.29/4.30 % (201201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.29/4.30 % (201201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.29/4.30 % (201201)CaDiCaL version: 2.1.3 % 24.29/4.30 % (201201)Termination reason: Refutation not found, incomplete strategy % 24.29/4.30 % (201201)Time elapsed: 0.006 s % 24.29/4.30 % (201201)Peak memory usage: 89 MB % 24.29/4.30 % (201201)Instructions burned: 8 (million) % 24.29/4.30 % (201194)------------------------------ % 24.29/4.30 % (201194)------------------------------ % 24.29/4.30 % (201198)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 24.29/4.30 % (201198)------------------------------ % 24.29/4.30 % (201198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.29/4.30 % (201198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.29/4.30 % (201198)CaDiCaL version: 2.1.3 % 24.29/4.30 % (201198)Termination reason: Unknown % 24.29/4.30 % (201198)Termination phase: Saturation % 24.29/4.30 % (201198)Time elapsed: 0.199 s % 24.29/4.30 % (201198)Peak memory usage: 113 MB % 24.29/4.30 % (201198)Instructions burned: 541 (million) % 24.29/4.30 % (201204)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3705699154:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/440Mi) % 24.29/4.30 % (201204)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 24.29/4.30 % (201207)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=3428772275:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi) % 26.94/4.88 % (201206)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3735732958:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2978 on theBenchmark for (2978ds/11145Mi) % 26.94/4.88 % (201201)------------------------------ % 26.94/4.88 % (201201)------------------------------ % 26.94/4.88 % (201196)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.94/4.88 % (201196)------------------------------ % 26.94/4.88 % (201196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.88 % (201196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.88 % (201196)CaDiCaL version: 2.1.3 % 26.94/4.88 % (201196)Termination reason: Unknown % 26.94/4.88 % (201196)Termination phase: Saturation % 26.94/4.88 % (201196)Time elapsed: 0.364 s % 26.94/4.88 % (201196)Peak memory usage: 113 MB % 26.94/4.88 % (201196)Instructions burned: 539 (million) % 26.94/4.88 % (201204)Instruction limit reached! % 26.94/4.88 % (201204)------------------------------ % 26.94/4.88 % (201204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.88 % (201204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.88 % (201204)CaDiCaL version: 2.1.3 % 26.94/4.88 % (201204)Termination reason: Instruction limit % 26.94/4.88 % (201204)Termination phase: Saturation % 26.94/4.88 % (201204)Time elapsed: 0.262 s % 26.94/4.88 % (201204)Peak memory usage: 93 MB % 26.94/4.88 % (201204)Instructions burned: 441 (million) % 26.94/4.88 % (201207)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.94/4.88 % (201207)------------------------------ % 26.94/4.88 % (201207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.88 % (201207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.88 % (201207)CaDiCaL version: 2.1.3 % 26.94/4.88 % (201207)Termination reason: Unknown % 26.94/4.88 % (201207)Termination phase: Saturation % 26.94/4.88 % (201207)Time elapsed: 0.198 s % 26.94/4.88 % (201207)Peak memory usage: 113 MB % 26.94/4.88 % (201207)Instructions burned: 541 (million) % 26.94/4.88 % (201211)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3444256257:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi) % 26.94/4.88 % (201212)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=4029396865:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2977 on theBenchmark for (2977ds/1016Mi) % 26.94/4.88 % (201213)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1779249069:i=14123:bd=preordered:ins=4_2975 on theBenchmark for (2975ds/14123Mi) % 26.94/4.88 % (201216)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2711468601:i=5781:kws=precedence:bd=all:rawr=on_2975 on theBenchmark for (2975ds/5781Mi) % 26.94/4.88 % (201206)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.94/4.88 % (201206)------------------------------ % 26.94/4.88 % (201206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.88 % (201206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.88 % (201206)CaDiCaL version: 2.1.3 % 26.94/4.88 % (201206)Termination reason: Unknown % 26.94/4.88 % (201206)Termination phase: Saturation % 26.94/4.88 % (201206)Time elapsed: 0.364 s % 26.94/4.88 % (201206)Peak memory usage: 114 MB % 26.94/4.88 % (201206)Instructions burned: 540 (million) % 26.94/4.88 % (201211)Instruction limit reached! % 26.94/4.88 % (201211)------------------------------ % 26.94/4.88 % (201211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.94/4.88 % (201211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.94/4.88 % (201211)CaDiCaL version: 2.1.3 % 26.94/4.88 % (201211)Termination reason: Instruction limit % 26.94/4.88 % (201211)Termination phase: Saturation % 26.94/4.88 % (201211)Time elapsed: 0.292 s % 26.94/4.88 % (201211)Peak memory usage: 91 MB % 26.94/4.88 % (201211)Instructions burned: 525 (million) % 26.94/4.88 % (201219)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=2054505973:i=2448:gtgl=5:bd=preordered:gtg=all_2973 on theBenchmark for (2973ds/2448Mi) % 26.94/4.88 % (201220)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1244815791:i=3223:kws=precedence:fgj=on:av=off_2972 on theBenchmark for (2972ds/3223Mi) % 31.90/5.41 % (201213)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.90/5.41 % (201213)------------------------------ % 31.90/5.41 % (201213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.90/5.41 % (201213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.90/5.41 % (201213)CaDiCaL version: 2.1.3 % 31.90/5.41 % (201213)Termination reason: Unknown % 31.90/5.41 % (201213)Termination phase: Saturation % 31.90/5.41 % (201213)Time elapsed: 0.361 s % 31.90/5.41 % (201213)Peak memory usage: 114 MB % 31.90/5.41 % (201213)Instructions burned: 540 (million) % 31.90/5.41 % (201192)Instruction limit reached! % 31.90/5.41 % (201192)------------------------------ % 31.90/5.41 % (201192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.90/5.41 % (201192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.90/5.41 % (201192)CaDiCaL version: 2.1.3 % 31.90/5.41 % (201192)Termination reason: Instruction limit % 31.90/5.41 % (201192)Termination phase: Saturation % 31.90/5.41 % (201192)Time elapsed: 1.163 s % 31.90/5.41 % (201192)Peak memory usage: 103 MB % 31.90/5.41 % (201192)Instructions burned: 2064 (million) % 31.90/5.41 % (201212)Instruction limit reached! % 31.90/5.41 % (201212)------------------------------ % 31.90/5.41 % (201212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.90/5.41 % (201212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.90/5.41 % (201212)CaDiCaL version: 2.1.3 % 31.90/5.41 % (201212)Termination reason: Instruction limit % 31.90/5.41 % (201212)Termination phase: Saturation % 31.90/5.41 % (201212)Time elapsed: 0.553 s % 31.90/5.41 % (201212)Peak memory usage: 94 MB % 31.90/5.41 % (201212)Instructions burned: 1017 (million) % 31.90/5.41 % (201223)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3245523724:st=5.6:i=2033:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/2033Mi) % 31.90/5.41 % (201224)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=284348773:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2970 on theBenchmark for (2970ds/2055Mi) % 31.90/5.41 % (201219)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.90/5.41 % (201219)------------------------------ % 31.90/5.41 % (201219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.90/5.41 % (201219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.90/5.41 % (201219)CaDiCaL version: 2.1.3 % 31.90/5.41 % (201219)Termination reason: Unknown % 31.90/5.41 % (201219)Termination phase: Saturation % 31.90/5.41 % (201219)Time elapsed: 0.364 s % 31.90/5.41 % (201219)Peak memory usage: 114 MB % 31.90/5.41 % (201219)Instructions burned: 543 (million) % 31.90/5.41 % (201225)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=2469338322:i=21611:sd=3:ss=axioms_2969 on theBenchmark for (2969ds/21611Mi) % 31.90/5.41 % (201220)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.90/5.41 % (201220)------------------------------ % 31.90/5.41 % (201220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.90/5.41 % (201220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.90/5.41 % (201220)CaDiCaL version: 2.1.3 % 31.90/5.41 % (201220)Termination reason: Unknown % 31.90/5.41 % (201220)Termination phase: Saturation % 31.90/5.41 % (201220)Time elapsed: 0.364 s % 31.90/5.41 % (201220)Peak memory usage: 114 MB % 31.90/5.41 % (201220)Instructions burned: 541 (million) % 31.90/5.41 % (201228)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=280212370:i=4835:sd=13:ss=axioms:sgt=23_2968 on theBenchmark for (2968ds/4835Mi) % 31.90/5.41 % (201228)Refutation not found, incomplete strategy % 31.90/5.41 % (201228)------------------------------ % 31.90/5.41 % (201228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.90/5.41 % (201228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.90/5.41 % (201228)CaDiCaL version: 2.1.3 % 31.90/5.41 % (201228)Termination reason: Refutation not found, incomplete strategy % 31.90/5.41 % (201228)Time elapsed: 0.006 s % 31.90/5.41 % (201228)Peak memory usage: 88 MB % 31.90/5.41 % (201228)Instructions burned: 9 (million) % 31.90/5.41 % (201223)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.93/5.93 % (201223)------------------------------ % 33.93/5.93 % (201223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.93/5.93 % (201223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.93/5.93 % (201223)CaDiCaL version: 2.1.3 % 33.93/5.93 % (201223)Termination reason: Unknown % 33.93/5.93 % (201223)Termination phase: Saturation % 33.93/5.93 % (201223)Time elapsed: 0.363 s % 33.93/5.93 % (201223)Peak memory usage: 113 MB % 33.93/5.93 % (201223)Instructions burned: 541 (million) % 33.93/5.93 % (201230)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=3162145195:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2967 on theBenchmark for (2967ds/797Mi) % 33.93/5.93 % (201224)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.93/5.93 % (201224)------------------------------ % 33.93/5.93 % (201224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.93/5.93 % (201224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.93/5.93 % (201224)CaDiCaL version: 2.1.3 % 33.93/5.93 % (201224)Termination reason: Unknown % 33.93/5.93 % (201224)Termination phase: Saturation % 33.93/5.93 % (201224)Time elapsed: 0.362 s % 33.93/5.93 % (201224)Peak memory usage: 114 MB % 33.93/5.93 % (201224)Instructions burned: 540 (million) % 33.93/5.93 % (201225)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.93/5.93 % (201225)------------------------------ % 33.93/5.93 % (201225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.93/5.93 % (201225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.93/5.93 % (201225)CaDiCaL version: 2.1.3 % 33.93/5.93 % (201225)Termination reason: Unknown % 33.93/5.93 % (201225)Termination phase: Saturation % 33.93/5.93 % (201225)Time elapsed: 0.364 s % 33.93/5.93 % (201225)Peak memory usage: 113 MB % 33.93/5.93 % (201225)Instructions burned: 539 (million) % 33.93/5.93 % (201228)------------------------------ % 33.93/5.93 % (201228)------------------------------ % 33.93/5.93 % (201233)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=4224041498:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2965 on theBenchmark for (2965ds/2326Mi) % 33.93/5.93 % (201233)Refutation not found, incomplete strategy % 33.93/5.93 % (201233)------------------------------ % 33.93/5.93 % (201233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.93/5.93 % (201233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.93/5.93 % (201233)CaDiCaL version: 2.1.3 % 33.93/5.93 % (201233)Termination reason: Refutation not found, incomplete strategy % 33.93/5.93 % (201233)Time elapsed: 0.008 s % 33.93/5.93 % (201233)Peak memory usage: 88 MB % 33.93/5.93 % (201233)Instructions burned: 11 (million) % 33.93/5.93 % (201234)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3543831836:i=6038:nm=6_2964 on theBenchmark for (2964ds/6038Mi) % 33.93/5.93 % (201235)lrs+10_1_sil=32000:sp=occurrence:random_seed=507401140:st=2:i=33334:sd=3:ss=included:sgt=32_2964 on theBenchmark for (2964ds/33334Mi) % 33.93/5.93 % (201236)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1553000977:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2964 on theBenchmark for (2964ds/1008Mi) % 33.93/5.93 % (201233)------------------------------ % 33.93/5.93 % (201233)------------------------------ % 33.93/5.93 % (201230)Instruction limit reached! % 33.93/5.93 % (201230)------------------------------ % 33.93/5.93 % (201230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.93/5.93 % (201230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.93/5.93 % (201230)CaDiCaL version: 2.1.3 % 33.93/5.93 % (201230)Termination reason: Instruction limit % 33.93/5.93 % (201230)Termination phase: Saturation % 33.93/5.93 % (201230)Time elapsed: 0.425 s % 33.93/5.93 % (201230)Peak memory usage: 97 MB % 33.93/5.93 % (201230)Instructions burned: 797 (million) % 33.93/5.93 % (201234)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.93/5.93 % (201234)------------------------------ % 33.93/5.93 % (201234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.93/5.93 % (201234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/6.46 % (201234)CaDiCaL version: 2.1.3 % 39.14/6.46 % (201234)Termination reason: Unknown % 39.14/6.46 % (201234)Termination phase: Saturation % 39.14/6.46 % (201234)Time elapsed: 0.364 s % 39.14/6.46 % (201234)Peak memory usage: 113 MB % 39.14/6.46 % (201234)Instructions burned: 541 (million) % 39.14/6.46 % (201242)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=2499079914:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2961 on theBenchmark for (2961ds/1083Mi) % 39.14/6.46 % (201241)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=3072674960:i=8327:s2at=5:bd=preordered_2961 on theBenchmark for (2961ds/8327Mi) % 39.14/6.46 % (201193)Instruction limit reached! % 39.14/6.46 % (201193)------------------------------ % 39.14/6.46 % (201193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.14/6.46 % (201193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/6.46 % (201193)CaDiCaL version: 2.1.3 % 39.14/6.46 % (201193)Termination reason: Instruction limit % 39.14/6.46 % (201193)Termination phase: Saturation % 39.14/6.46 % (201193)Time elapsed: 2.214 s % 39.14/6.46 % (201193)Peak memory usage: 114 MB % 39.14/6.46 % (201193)Instructions burned: 3707 (million) % 39.14/6.46 % (201246)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2752978651:i=6995:s2at=5:gtg=all_2959 on theBenchmark for (2959ds/6995Mi) % 39.14/6.46 % (201245)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1398487570:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2959 on theBenchmark for (2959ds/1084Mi) % 39.14/6.46 % (201236)Instruction limit reached! % 39.14/6.46 % (201236)------------------------------ % 39.14/6.46 % (201236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.14/6.46 % (201236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/6.46 % (201236)CaDiCaL version: 2.1.3 % 39.14/6.46 % (201236)Termination reason: Instruction limit % 39.14/6.46 % (201236)Termination phase: Saturation % 39.14/6.46 % (201236)Time elapsed: 0.495 s % 39.14/6.46 % (201236)Peak memory usage: 99 MB % 39.14/6.46 % (201236)Instructions burned: 1008 (million) % 39.14/6.46 % (201216)Instruction limit reached! % 39.14/6.46 % (201216)------------------------------ % 39.14/6.46 % (201216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.14/6.46 % (201216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/6.46 % (201216)CaDiCaL version: 2.1.3 % 39.14/6.46 % (201216)Termination reason: Instruction limit % 39.14/6.46 % (201216)Termination phase: Saturation % 39.14/6.46 % (201216)Time elapsed: 1.781 s % 39.14/6.46 % (201216)Peak memory usage: 121 MB % 39.14/6.46 % (201216)Instructions burned: 5782 (million) % 39.14/6.46 % (201249)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=455352773:st=2:i=6225:sd=15:ss=axioms_2957 on theBenchmark for (2957ds/6225Mi) % 39.14/6.46 % (201241)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.14/6.46 % (201241)------------------------------ % 39.14/6.46 % (201241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.14/6.46 % (201241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/6.46 % (201241)CaDiCaL version: 2.1.3 % 39.14/6.46 % (201241)Termination reason: Unknown % 39.14/6.46 % (201241)Termination phase: Saturation % 39.14/6.46 % (201241)Time elapsed: 0.365 s % 39.14/6.46 % (201241)Peak memory usage: 113 MB % 39.14/6.46 % (201241)Instructions burned: 541 (million) % 39.14/6.46 % (201250)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1888928813:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2956 on theBenchmark for (2956ds/3372Mi) % 39.14/6.46 % (201246)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.14/6.46 % (201246)------------------------------ % 39.14/6.46 % (201246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.14/6.46 % (201246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.14/6.46 % (201246)CaDiCaL version: 2.1.3 % 39.14/6.46 % (201246)Termination reason: Unknown % 39.14/6.46 % (201246)Termination phase: Saturation % 39.14/6.46 % (201246)Time elapsed: 0.365 s % 39.14/6.46 % (201246)Peak memory usage: 114 MB % 41.99/6.96 % (201246)Instructions burned: 543 (million) % 41.99/6.96 % (201252)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=723026893:st=2.3:i=26457:sd=10:ss=included:sgt=8_2955 on theBenchmark for (2955ds/26457Mi) % 41.99/6.96 % (201242)Instruction limit reached! % 41.99/6.96 % (201242)------------------------------ % 41.99/6.96 % (201242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.99/6.96 % (201242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.99/6.96 % (201242)CaDiCaL version: 2.1.3 % 41.99/6.96 % (201242)Termination reason: Instruction limit % 41.99/6.96 % (201242)Termination phase: Saturation % 41.99/6.96 % (201242)Time elapsed: 0.543 s % 41.99/6.96 % (201242)Peak memory usage: 95 MB % 41.99/6.96 % (201242)Instructions burned: 1084 (million) % 41.99/6.96 % (201250)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.99/6.96 % (201250)------------------------------ % 41.99/6.96 % (201250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.99/6.96 % (201250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.99/6.96 % (201250)CaDiCaL version: 2.1.3 % 41.99/6.96 % (201250)Termination reason: Unknown % 41.99/6.96 % (201250)Termination phase: Saturation % 41.99/6.96 % (201250)Time elapsed: 0.197 s % 41.99/6.96 % (201250)Peak memory usage: 114 MB % 41.99/6.96 % (201250)Instructions burned: 539 (million) % 41.99/6.96 % (201255)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=1498081537:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2954 on theBenchmark for (2954ds/13494Mi) % 41.99/6.96 % (201256)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=778190225:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2954 on theBenchmark for (2954ds/2503Mi) % 41.99/6.96 % (201256)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 41.99/6.96 % (201245)Instruction limit reached! % 41.99/6.96 % (201245)------------------------------ % 41.99/6.96 % (201245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.99/6.96 % (201245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.99/6.96 % (201245)CaDiCaL version: 2.1.3 % 41.99/6.96 % (201245)Termination reason: Instruction limit % 41.99/6.96 % (201245)Termination phase: Saturation % 41.99/6.96 % (201245)Time elapsed: 0.578 s % 41.99/6.96 % (201245)Peak memory usage: 95 MB % 41.99/6.96 % (201245)Instructions burned: 1086 (million) % 41.99/6.96 % (201257)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3361324137:i=2559:sd=1:ep=RSTC:ss=axioms_2953 on theBenchmark for (2953ds/2559Mi) % 41.99/6.96 % (201252)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.99/6.96 % (201252)------------------------------ % 41.99/6.96 % (201252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.99/6.96 % (201252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.99/6.96 % (201252)CaDiCaL version: 2.1.3 % 41.99/6.96 % (201252)Termination reason: Unknown % 41.99/6.96 % (201252)Termination phase: Saturation % 41.99/6.96 % (201252)Time elapsed: 0.364 s % 41.99/6.96 % (201252)Peak memory usage: 113 MB % 41.99/6.96 % (201252)Instructions burned: 541 (million) % 41.99/6.96 % (201260)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=122552334:i=30753:av=off:ss=included_2952 on theBenchmark for (2952ds/30753Mi) % 41.99/6.96 % (201257)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.99/6.96 % (201257)------------------------------ % 41.99/6.96 % (201257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.99/6.96 % (201257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.99/6.96 % (201257)CaDiCaL version: 2.1.3 % 41.99/6.96 % (201257)Termination reason: Unknown % 41.99/6.96 % (201257)Termination phase: Saturation % 41.99/6.96 % (201257)Time elapsed: 0.196 s % 41.99/6.96 % (201257)Peak memory usage: 113 MB % 41.99/6.96 % (201257)Instructions burned: 538 (million) % 41.99/6.96 % (201255)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.99/6.96 % (201255)------------------------------ % 41.99/6.96 % (201255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.92/7.74 % (201255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.92/7.74 % (201255)CaDiCaL version: 2.1.3 % 47.92/7.74 % (201255)Termination reason: Unknown % 47.92/7.74 % (201255)Termination phase: Saturation % 47.92/7.74 % (201255)Time elapsed: 0.365 s % 47.92/7.74 % (201255)Peak memory usage: 114 MB % 47.92/7.74 % (201255)Instructions burned: 544 (million) % 47.92/7.74 % (201256)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.92/7.74 % (201256)------------------------------ % 47.92/7.74 % (201256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.92/7.74 % (201256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.92/7.74 % (201256)CaDiCaL version: 2.1.3 % 47.92/7.74 % (201256)Termination reason: Unknown % 47.92/7.74 % (201256)Termination phase: Saturation % 47.92/7.74 % (201256)Time elapsed: 0.362 s % 47.92/7.74 % (201256)Peak memory usage: 113 MB % 47.92/7.74 % (201256)Instructions burned: 539 (million) % 47.92/7.74 % (201262)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1935660563:i=26473:ep=RSTC_2950 on theBenchmark for (2950ds/26473Mi) % 47.92/7.74 % (201264)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=3277122719:cts=off:i=2759:kws=inv_arity:fgj=on_2949 on theBenchmark for (2949ds/2759Mi) % 47.92/7.74 % (201265)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=3760402956:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2949 on theBenchmark for (2949ds/5665Mi) % 47.92/7.74 % (201265)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 47.92/7.74 % (201267)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=997159802:i=1532:ep=RS:ss=axioms_2949 on theBenchmark for (2949ds/1532Mi) % 47.92/7.74 % (201260)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.92/7.74 % (201260)------------------------------ % 47.92/7.74 % (201260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.92/7.74 % (201260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.92/7.74 % (201260)CaDiCaL version: 2.1.3 % 47.92/7.74 % (201260)Termination reason: Unknown % 47.92/7.74 % (201260)Termination phase: Saturation % 47.92/7.74 % (201260)Time elapsed: 0.363 s % 47.92/7.74 % (201260)Peak memory usage: 114 MB % 47.92/7.74 % (201260)Instructions burned: 541 (million) % 47.92/7.74 % (201264)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.92/7.74 % (201264)------------------------------ % 47.92/7.74 % (201264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.92/7.74 % (201264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.92/7.74 % (201264)CaDiCaL version: 2.1.3 % 47.92/7.74 % (201264)Termination reason: Unknown % 47.92/7.74 % (201264)Termination phase: Saturation % 47.92/7.74 % (201264)Time elapsed: 0.197 s % 47.92/7.74 % (201264)Peak memory usage: 114 MB % 47.92/7.74 % (201264)Instructions burned: 543 (million) % 47.92/7.74 % (201272)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=4236168201:i=1572:fgj=on:gsp=on_2946 on theBenchmark for (2946ds/1572Mi) % 47.92/7.74 % (201272)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 47.92/7.74 % (201271)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3760430050:i=1565:sd=2:ss=axioms:sgt=32_2946 on theBenchmark for (2946ds/1565Mi) % 47.92/7.74 % (201265)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 47.92/7.74 % (201265)------------------------------ % 47.92/7.74 % (201265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.92/7.74 % (201265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.92/7.74 % (201265)CaDiCaL version: 2.1.3 % 47.92/7.74 % (201265)Termination reason: Unknown % 47.92/7.74 % (201265)Termination phase: Saturation % 47.92/7.74 % (201265)Time elapsed: 0.361 s % 47.92/7.74 % (201265)Peak memory usage: 113 MB % 47.92/7.74 % (201265)Instructions burned: 540 (million) % 47.92/7.74 % (201267)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 52.10/8.27 % (201267)------------------------------ % 52.10/8.27 % (201267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.10/8.27 % (201267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.10/8.27 % (201267)CaDiCaL version: 2.1.3 % 52.10/8.27 % (201267)Termination reason: Unknown % 52.10/8.27 % (201267)Termination phase: Saturation % 52.10/8.27 % (201267)Time elapsed: 0.360 s % 52.10/8.27 % (201267)Peak memory usage: 113 MB % 52.10/8.27 % (201267)Instructions burned: 540 (million) % 52.10/8.27 % (201272)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 52.10/8.27 % (201272)------------------------------ % 52.10/8.27 % (201272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.10/8.27 % (201272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.10/8.27 % (201272)CaDiCaL version: 2.1.3 % 52.10/8.27 % (201272)Termination reason: Unknown % 52.10/8.27 % (201272)Termination phase: Saturation % 52.10/8.27 % (201272)Time elapsed: 0.196 s % 52.10/8.27 % (201272)Peak memory usage: 113 MB % 52.10/8.27 % (201272)Instructions burned: 541 (million) % 52.10/8.27 % (201275)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1324012628:i=6052:sd=4:ss=axioms:sgt=24_2944 on theBenchmark for (2944ds/6052Mi) % 52.10/8.27 % (201277)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=2940168125:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2943 on theBenchmark for (2943ds/1842Mi) % 52.10/8.27 % (201277)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 52.10/8.27 % (201276)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=1219156540:i=3500:sd=1:bd=preordered:sup=off:ss=included_2943 on theBenchmark for (2943ds/3500Mi) % 52.10/8.27 % (201271)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 52.10/8.27 % (201271)------------------------------ % 52.10/8.27 % (201271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.10/8.27 % (201271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.10/8.27 % (201271)CaDiCaL version: 2.1.3 % 52.10/8.27 % (201271)Termination reason: Unknown % 52.10/8.27 % (201271)Termination phase: Saturation % 52.10/8.27 % (201271)Time elapsed: 0.362 s % 52.10/8.27 % (201271)Peak memory usage: 113 MB % 52.10/8.27 % (201271)Instructions burned: 541 (million) % 52.10/8.27 % (201277)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 52.10/8.27 % (201277)------------------------------ % 52.10/8.27 % (201277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.10/8.27 % (201277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.10/8.27 % (201277)CaDiCaL version: 2.1.3 % 52.10/8.27 % (201277)Termination reason: Unknown % 52.10/8.27 % (201277)Termination phase: Saturation % 52.10/8.27 % (201277)Time elapsed: 0.195 s % 52.10/8.27 % (201277)Peak memory usage: 113 MB % 52.10/8.27 % (201277)Instructions burned: 541 (million) % 52.10/8.27 % (201281)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3420956892:i=66096:add=on_2941 on theBenchmark for (2941ds/66096Mi) % 52.10/8.27 % (201282)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=987181279:i=1884:sd=1:nm=60:ss=axioms_2940 on theBenchmark for (2940ds/1884Mi) % 52.10/8.27 % (201275)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 52.10/8.27 % (201275)------------------------------ % 52.10/8.27 % (201275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.10/8.27 % (201275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.10/8.27 % (201275)CaDiCaL version: 2.1.3 % 52.10/8.27 % (201275)Termination reason: Unknown % 52.10/8.27 % (201275)Termination phase: Saturation % 52.10/8.27 % (201275)Time elapsed: 0.361 s % 52.10/8.27 % (201275)Peak memory usage: 113 MB % 52.10/8.27 % (201275)Instructions burned: 540 (million) % 52.10/8.27 % (201276)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 52.10/8.27 % (201276)------------------------------ % 52.10/8.27 % (201276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.56/8.98 % (201276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.56/8.98 % (201276)CaDiCaL version: 2.1.3 % 56.56/8.98 % (201276)Termination reason: Unknown % 56.56/8.98 % (201276)Termination phase: Saturation % 56.56/8.98 % (201276)Time elapsed: 0.357 s % 56.56/8.98 % (201276)Peak memory usage: 113 MB % 56.56/8.98 % (201276)Instructions burned: 541 (million) % 56.56/8.98 % (201285)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3632584038:cts=off:i=5469:bs=on:fsr=off_2938 on theBenchmark for (2938ds/5469Mi) % 56.56/8.98 % (201282)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.56/8.98 % (201282)------------------------------ % 56.56/8.98 % (201282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.56/8.98 % (201282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.56/8.98 % (201282)CaDiCaL version: 2.1.3 % 56.56/8.98 % (201282)Termination reason: Unknown % 56.56/8.98 % (201282)Termination phase: Saturation % 56.56/8.98 % (201282)Time elapsed: 0.197 s % 56.56/8.98 % (201282)Peak memory usage: 113 MB % 56.56/8.98 % (201282)Instructions burned: 537 (million) % 56.56/8.98 % (201286)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=3059952693:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2938 on theBenchmark for (2938ds/2037Mi) % 56.56/8.98 % (201281)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.56/8.98 % (201281)------------------------------ % 56.56/8.98 % (201281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.56/8.98 % (201281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.56/8.98 % (201281)CaDiCaL version: 2.1.3 % 56.56/8.98 % (201281)Termination reason: Unknown % 56.56/8.98 % (201281)Termination phase: Saturation % 56.56/8.98 % (201281)Time elapsed: 0.363 s % 56.56/8.98 % (201281)Peak memory usage: 113 MB % 56.56/8.98 % (201281)Instructions burned: 541 (million) % 56.56/8.98 % (201288)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2500768408:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2937 on theBenchmark for (2937ds/2110Mi) % 56.56/8.98 % (201290)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=2859150818:i=2430:add=off:aac=none:nm=16_2936 on theBenchmark for (2936ds/2430Mi) % 56.56/8.98 % (201288)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.56/8.98 % (201288)------------------------------ % 56.56/8.98 % (201288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.56/8.98 % (201288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.56/8.98 % (201288)CaDiCaL version: 2.1.3 % 56.56/8.98 % (201288)Termination reason: Unknown % 56.56/8.98 % (201288)Termination phase: Saturation % 56.56/8.98 % (201288)Time elapsed: 0.198 s % 56.56/8.98 % (201288)Peak memory usage: 114 MB % 56.56/8.98 % (201288)Instructions burned: 545 (million) % 56.56/8.98 % (201286)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.56/8.98 % (201286)------------------------------ % 56.56/8.98 % (201286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.56/8.98 % (201286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.56/8.98 % (201286)CaDiCaL version: 2.1.3 % 56.56/8.98 % (201286)Termination reason: Unknown % 56.56/8.98 % (201286)Termination phase: Saturation % 56.56/8.98 % (201286)Time elapsed: 0.367 s % 56.56/8.98 % (201286)Peak memory usage: 114 MB % 56.56/8.98 % (201286)Instructions burned: 547 (million) % 56.56/8.98 % (201293)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=1503087866:cond=fast:i=4891_2934 on theBenchmark for (2934ds/4891Mi) % 56.56/8.98 % (201294)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=2969796057:st=2:i=14845:sd=2:ss=included:fsd=on_2933 on theBenchmark for (2933ds/14845Mi) % 56.56/8.98 % (201290)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.56/8.98 % (201290)------------------------------ % 56.56/8.98 % (201290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.50 % (201290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.50 % (201290)CaDiCaL version: 2.1.3 % 61.15/9.50 % (201290)Termination reason: Unknown % 61.15/9.50 % (201290)Termination phase: Saturation % 61.15/9.50 % (201290)Time elapsed: 0.362 s % 61.15/9.50 % (201290)Peak memory usage: 114 MB % 61.15/9.50 % (201290)Instructions burned: 541 (million) % 61.15/9.50 % (201293)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.15/9.50 % (201293)------------------------------ % 61.15/9.50 % (201293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.50 % (201293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.50 % (201293)CaDiCaL version: 2.1.3 % 61.15/9.50 % (201293)Termination reason: Unknown % 61.15/9.50 % (201293)Termination phase: Saturation % 61.15/9.50 % (201293)Time elapsed: 0.197 s % 61.15/9.50 % (201293)Peak memory usage: 114 MB % 61.15/9.50 % (201293)Instructions burned: 541 (million) % 61.15/9.50 % (201297)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3149943722:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2931 on theBenchmark for (2931ds/7534Mi) % 61.15/9.50 % (201298)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=855697207:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2930 on theBenchmark for (2930ds/10353Mi) % 61.15/9.50 % (201294)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.15/9.50 % (201294)------------------------------ % 61.15/9.50 % (201294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.50 % (201294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.50 % (201294)CaDiCaL version: 2.1.3 % 61.15/9.50 % (201294)Termination reason: Unknown % 61.15/9.50 % (201294)Termination phase: Saturation % 61.15/9.50 % (201294)Time elapsed: 0.361 s % 61.15/9.50 % (201294)Peak memory usage: 114 MB % 61.15/9.50 % (201294)Instructions burned: 541 (million) % 61.15/9.50 % (201298)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.15/9.50 % (201298)------------------------------ % 61.15/9.50 % (201298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.50 % (201298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.50 % (201298)CaDiCaL version: 2.1.3 % 61.15/9.50 % (201298)Termination reason: Unknown % 61.15/9.50 % (201298)Termination phase: Saturation % 61.15/9.50 % (201298)Time elapsed: 0.195 s % 61.15/9.50 % (201298)Peak memory usage: 114 MB % 61.15/9.50 % (201298)Instructions burned: 541 (million) % 61.15/9.50 % (201301)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1856255109:i=7860_2928 on theBenchmark for (2928ds/7860Mi) % 61.15/9.50 % (201301)Refutation not found, incomplete strategy % 61.15/9.50 % (201301)------------------------------ % 61.15/9.50 % (201301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.50 % (201301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.50 % (201301)CaDiCaL version: 2.1.3 % 61.15/9.50 % (201301)Termination reason: Refutation not found, incomplete strategy % 61.15/9.50 % (201301)Time elapsed: 0.006 s % 61.15/9.50 % (201301)Peak memory usage: 88 MB % 61.15/9.50 % (201301)Instructions burned: 8 (million) % 61.15/9.50 % (201302)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=1422684608:i=7896:sd=2:bs=on:ss=included:sgt=20_2927 on theBenchmark for (2927ds/7896Mi) % 61.15/9.50 % (201297)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 61.15/9.50 % (201297)------------------------------ % 61.15/9.50 % (201297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.15/9.50 % (201297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.15/9.50 % (201297)CaDiCaL version: 2.1.3 % 61.15/9.50 % (201297)Termination reason: Unknown % 61.15/9.50 % (201297)Termination phase: Saturation % 61.15/9.50 % (201297)Time elapsed: 0.363 s % 61.15/9.50 % (201297)Peak memory usage: 113 MB % 61.15/9.50 % (201297)Instructions burned: 544 (million) % 61.15/9.50 % (201249)Instruction limit reached! % 61.15/9.50 % (201249)------------------------------ % 61.15/9.50 % (201249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.50/10.42 % (201249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.50/10.42 % (201249)CaDiCaL version: 2.1.3 % 67.50/10.42 % (201249)Termination reason: Instruction limit % 67.50/10.42 % (201249)Termination phase: Saturation % 67.50/10.42 % (201249)Time elapsed: 3.030 s % 67.50/10.42 % (201249)Peak memory usage: 187 MB % 67.50/10.42 % (201249)Instructions burned: 6226 (million) % 67.50/10.42 % (201305)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3579613115:i=5812:gtgl=2:gtg=all_2926 on theBenchmark for (2926ds/5812Mi) % 67.50/10.42 % (201302)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.50/10.42 % (201302)------------------------------ % 67.50/10.42 % (201302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.50/10.42 % (201302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.50/10.42 % (201302)CaDiCaL version: 2.1.3 % 67.50/10.42 % (201302)Termination reason: Unknown % 67.50/10.42 % (201302)Termination phase: Saturation % 67.50/10.42 % (201302)Time elapsed: 0.200 s % 67.50/10.42 % (201302)Peak memory usage: 113 MB % 67.50/10.42 % (201302)Instructions burned: 540 (million) % 67.50/10.42 % (201301)------------------------------ % 67.50/10.42 % (201301)------------------------------ % 67.50/10.42 % (201306)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=1909591819:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2925 on theBenchmark for (2925ds/2965Mi) % 67.50/10.42 % (201308)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=3705888189:i=2967:kws=precedence:bd=preordered:av=off_2924 on theBenchmark for (2924ds/2967Mi) % 67.50/10.42 % (201309)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=2163140910:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2923 on theBenchmark for (2923ds/3022Mi) % 67.50/10.42 % (201308)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.50/10.42 % (201308)------------------------------ % 67.50/10.42 % (201308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.50/10.42 % (201308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.50/10.42 % (201308)CaDiCaL version: 2.1.3 % 67.50/10.42 % (201308)Termination reason: Unknown % 67.50/10.42 % (201308)Termination phase: Saturation % 67.50/10.42 % (201308)Time elapsed: 0.196 s % 67.50/10.42 % (201308)Peak memory usage: 114 MB % 67.50/10.42 % (201308)Instructions burned: 541 (million) % 67.50/10.42 % (201305)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.50/10.42 % (201305)------------------------------ % 67.50/10.42 % (201305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.50/10.42 % (201305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.50/10.42 % (201305)CaDiCaL version: 2.1.3 % 67.50/10.42 % (201305)Termination reason: Unknown % 67.50/10.42 % (201305)Termination phase: Saturation % 67.50/10.42 % (201305)Time elapsed: 0.364 s % 67.50/10.42 % (201305)Peak memory usage: 114 MB % 67.50/10.42 % (201305)Instructions burned: 543 (million) % 67.50/10.42 % (201306)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.50/10.42 % (201306)------------------------------ % 67.50/10.42 % (201306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.50/10.42 % (201306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.50/10.42 % (201306)CaDiCaL version: 2.1.3 % 67.50/10.42 % (201306)Termination reason: Unknown % 67.50/10.42 % (201306)Termination phase: Saturation % 67.50/10.42 % (201306)Time elapsed: 0.363 s % 67.50/10.42 % (201306)Peak memory usage: 114 MB % 67.50/10.42 % (201306)Instructions burned: 541 (million) % 67.50/10.42 % (201313)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=1504558449:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2921 on theBenchmark for (2921ds/3207Mi) % 67.50/10.42 % (201314)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2609842528:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2920 on theBenchmark for (2920ds/3289Mi) % 67.50/10.42 % (201309)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.27/11.04 % (201309)------------------------------ % 72.27/11.04 % (201309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.27/11.04 % (201309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.27/11.04 % (201309)CaDiCaL version: 2.1.3 % 72.27/11.04 % (201309)Termination reason: Unknown % 72.27/11.04 % (201309)Termination phase: Saturation % 72.27/11.04 % (201309)Time elapsed: 0.360 s % 72.27/11.04 % (201309)Peak memory usage: 113 MB % 72.27/11.04 % (201309)Instructions burned: 538 (million) % 72.27/11.04 % (201315)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=781958890:i=38569:sd=3:ss=axioms:sgt=32_2920 on theBenchmark for (2920ds/38569Mi) % 72.27/11.04 % (201313)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.27/11.04 % (201313)------------------------------ % 72.27/11.04 % (201313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.27/11.04 % (201313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.27/11.04 % (201313)CaDiCaL version: 2.1.3 % 72.27/11.04 % (201313)Termination reason: Unknown % 72.27/11.04 % (201313)Termination phase: Saturation % 72.27/11.04 % (201313)Time elapsed: 0.198 s % 72.27/11.04 % (201313)Peak memory usage: 114 MB % 72.27/11.04 % (201313)Instructions burned: 539 (million) % 72.27/11.04 % (201318)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1839366073:cts=off:i=3394_2918 on theBenchmark for (2918ds/3394Mi) % 72.27/11.04 % (201320)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=2304919514:i=33824:bd=preordered_2917 on theBenchmark for (2917ds/33824Mi) % 72.27/11.04 % (201314)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.27/11.04 % (201314)------------------------------ % 72.27/11.04 % (201314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.27/11.04 % (201314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.27/11.04 % (201314)CaDiCaL version: 2.1.3 % 72.27/11.04 % (201314)Termination reason: Unknown % 72.27/11.04 % (201314)Termination phase: Saturation % 72.27/11.04 % (201314)Time elapsed: 0.362 s % 72.27/11.04 % (201314)Peak memory usage: 113 MB % 72.27/11.04 % (201314)Instructions burned: 541 (million) % 72.27/11.04 % (201315)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.27/11.04 % (201315)------------------------------ % 72.27/11.04 % (201315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.27/11.04 % (201315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.27/11.04 % (201315)CaDiCaL version: 2.1.3 % 72.27/11.04 % (201315)Termination reason: Unknown % 72.27/11.04 % (201315)Termination phase: Saturation % 72.27/11.04 % (201315)Time elapsed: 0.362 s % 72.27/11.04 % (201315)Peak memory usage: 113 MB % 72.27/11.04 % (201315)Instructions burned: 542 (million) % 72.27/11.04 % (201320)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 72.27/11.04 % (201320)------------------------------ % 72.27/11.04 % (201320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.27/11.04 % (201320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.27/11.04 % (201320)CaDiCaL version: 2.1.3 % 72.27/11.04 % (201320)Termination reason: Unknown % 72.27/11.04 % (201320)Termination phase: Saturation % 72.27/11.04 % (201320)Time elapsed: 0.196 s % 72.27/11.04 % (201320)Peak memory usage: 114 MB % 72.27/11.04 % (201320)Instructions burned: 541 (million) % 72.27/11.04 % (201323)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2921148513:i=20684:bd=all:gtg=exists_sym_2915 on theBenchmark for (2915ds/20684Mi) % 72.27/11.04 % (201325)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2031436175:st=4:i=7295:sd=4:ep=R:ss=axioms_2914 on theBenchmark for (2914ds/7295Mi) % 72.27/11.04 % (201324)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=2444327706: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_2914 on theBenchmark for (2914ds/7222Mi) % 72.27/11.04 % (201324)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 75.65/11.68 % (201318)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.65/11.68 % (201318)------------------------------ % 75.65/11.68 % (201318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.65/11.68 % (201318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.65/11.68 % (201318)CaDiCaL version: 2.1.3 % 75.65/11.68 % (201318)Termination reason: Unknown % 75.65/11.68 % (201318)Termination phase: Saturation % 75.65/11.68 % (201318)Time elapsed: 0.393 s % 75.65/11.68 % (201318)Peak memory usage: 113 MB % 75.65/11.68 % (201318)Instructions burned: 541 (million) % 75.65/11.68 % (201325)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.65/11.68 % (201325)------------------------------ % 75.65/11.68 % (201325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.65/11.68 % (201325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.65/11.68 % (201325)CaDiCaL version: 2.1.3 % 75.65/11.68 % (201325)Termination reason: Unknown % 75.65/11.68 % (201325)Termination phase: Saturation % 75.65/11.68 % (201325)Time elapsed: 0.200 s % 75.65/11.68 % (201325)Peak memory usage: 113 MB % 75.65/11.68 % (201325)Instructions burned: 543 (million) % 75.65/11.68 % (201329)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=294217890:i=4036:ins=10_2913 on theBenchmark for (2913ds/4036Mi) % 75.65/11.68 % (201331)lrs+10_1_sil=128000:lcm=predicate:random_seed=1590808363:st=3:i=43697:sd=5:ss=axioms_2911 on theBenchmark for (2911ds/43697Mi) % 75.65/11.68 % (201324)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.65/11.68 % (201323)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.65/11.68 % (201323)------------------------------ % 75.65/11.68 % (201323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.65/11.68 % (201324)------------------------------ % 75.65/11.68 % (201324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.65/11.68 % (201324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.65/11.68 % (201323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.65/11.68 % (201323)CaDiCaL version: 2.1.3 % 75.65/11.68 % (201324)CaDiCaL version: 2.1.3 % 75.65/11.68 % (201323)Termination reason: Unknown % 75.65/11.68 % (201323)Termination phase: Saturation % 75.65/11.68 % (201324)Termination reason: Unknown % 75.65/11.68 % (201324)Termination phase: Saturation % 75.65/11.68 % (201323)Time elapsed: 0.408 s % 75.65/11.68 % (201324)Time elapsed: 0.385 s % 75.65/11.68 % (201324)Peak memory usage: 113 MB % 75.65/11.68 % (201323)Peak memory usage: 113 MB % 75.65/11.68 % (201324)Instructions burned: 543 (million) % 75.65/11.68 % (201323)Instructions burned: 543 (million) % 75.65/11.68 % (201329)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.65/11.68 % (201329)------------------------------ % 75.65/11.68 % (201329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.65/11.68 % (201329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.65/11.68 % (201329)CaDiCaL version: 2.1.3 % 75.65/11.68 % (201329)Termination reason: Unknown % 75.65/11.68 % (201329)Termination phase: Saturation % 75.65/11.68 % (201329)Time elapsed: 0.359 s % 75.65/11.68 % (201329)Peak memory usage: 113 MB % 75.65/11.68 % (201329)Instructions burned: 540 (million) % 75.65/11.68 % (201334)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=503447020:i=4547:bd=preordered_2909 on theBenchmark for (2909ds/4547Mi) % 75.65/11.68 % (201333)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=2297503322:i=17599:gtg=all:ss=axioms:fsd=on_2909 on theBenchmark for (2909ds/17599Mi) % 75.65/11.68 % (201337)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=130326657:i=9294:av=off_2907 on theBenchmark for (2907ds/9294Mi) % 75.65/11.68 % (201333)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 75.65/11.68 % (201333)------------------------------ % 75.65/11.68 % (201333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.65/11.68 % (201334)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 86.38/13.08 % (201334)------------------------------ % 86.38/13.08 % (201334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.38/13.08 % (201333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.38/13.08 % (201334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.38/13.08 % (201333)CaDiCaL version: 2.1.3 % 86.38/13.08 % (201333)Termination reason: Unknown % 86.38/13.08 % (201333)Termination phase: Saturation % 86.38/13.08 % (201333)Time elapsed: 0.360 s % 86.38/13.08 % (201333)Peak memory usage: 113 MB % 86.38/13.08 % (201334)CaDiCaL version: 2.1.3 % 86.38/13.08 % (201334)Termination reason: Unknown % 86.38/13.08 % (201334)Termination phase: Saturation % 86.38/13.08 % (201333)Instructions burned: 541 (million) % 86.38/13.08 % (201334)Time elapsed: 0.360 s % 86.38/13.08 % (201334)Peak memory usage: 113 MB % 86.38/13.08 % (201334)Instructions burned: 540 (million) % 86.38/13.08 % (201285)Instruction limit reached! % 86.38/13.08 % (201285)------------------------------ % 86.38/13.08 % (201285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.38/13.08 % (201285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.38/13.08 % (201285)CaDiCaL version: 2.1.3 % 86.38/13.08 % (201285)Termination reason: Instruction limit % 86.38/13.08 % (201285)Termination phase: Saturation % 86.38/13.08 % (201285)Time elapsed: 3.413 s % 86.38/13.08 % (201285)Peak memory usage: 116 MB % 86.38/13.08 % (201285)Instructions burned: 5470 (million) % 86.38/13.08 % (201337)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 86.38/13.08 % (201337)------------------------------ % 86.38/13.08 % (201337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.38/13.08 % (201337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.38/13.08 % (201337)CaDiCaL version: 2.1.3 % 86.38/13.08 % (201337)Termination reason: Unknown % 86.38/13.08 % (201337)Termination phase: Saturation % 86.38/13.08 % (201337)Time elapsed: 0.360 s % 86.38/13.08 % (201337)Peak memory usage: 114 MB % 86.38/13.08 % (201337)Instructions burned: 541 (million) % 86.38/13.08 % (201340)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1721136314:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2904 on theBenchmark for (2904ds/4793Mi) % 86.38/13.08 % (201339)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=443381856:i=32849:add=on_2904 on theBenchmark for (2904ds/32849Mi) % 86.38/13.08 % (201341)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=2986583148:i=4840:nm=4:av=off_2903 on theBenchmark for (2903ds/4840Mi) % 86.38/13.08 % (201342)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=1323648485:cts=off:i=5002_2902 on theBenchmark for (2902ds/5002Mi) % 86.38/13.08 % (201340)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 86.38/13.08 % (201340)------------------------------ % 86.38/13.08 % (201340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.38/13.08 % (201339)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 86.38/13.08 % (201340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.38/13.08 % (201339)------------------------------ % 86.38/13.08 % (201339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.38/13.08 % (201339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.38/13.08 % (201340)CaDiCaL version: 2.1.3 % 86.38/13.08 % (201340)Termination reason: Unknown % 86.38/13.08 % (201340)Termination phase: Saturation % 86.38/13.08 % (201339)CaDiCaL version: 2.1.3 % 86.38/13.08 % (201340)Time elapsed: 0.359 s % 86.38/13.08 % (201339)Termination reason: Unknown % 86.38/13.08 % (201339)Termination phase: Saturation % 86.38/13.08 % (201340)Peak memory usage: 113 MB % 86.38/13.08 % (201339)Time elapsed: 0.359 s % 86.38/13.08 % (201340)Instructions burned: 539 (million) % 86.38/13.08 % (201339)Peak memory usage: 113 MB % 86.38/13.08 % (201339)Instructions burned: 541 (million) % 86.38/13.08 % (201341)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 86.38/13.08 % (201341)------------------------------ % 86.38/13.08 % (201341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.38/13.08 % (201341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.38/13.08 % (201341)CaDiCaL version: 2.1.3 % 137.01/20.16 % (201341)Termination reason: Unknown % 137.01/20.16 % (201341)Termination phase: Saturation % 137.01/20.16 % (201341)Time elapsed: 0.359 s % 137.01/20.16 % (201341)Peak memory usage: 113 MB % 137.01/20.16 % (201341)Instructions burned: 540 (million) % 137.01/20.16 % (201342)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.01/20.16 % (201342)------------------------------ % 137.01/20.16 % (201342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.01/20.16 % (201342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.01/20.16 % (201342)CaDiCaL version: 2.1.3 % 137.01/20.16 % (201342)Termination reason: Unknown % 137.01/20.16 % (201342)Termination phase: Saturation % 137.01/20.16 % (201342)Time elapsed: 0.365 s % 137.01/20.16 % (201342)Peak memory usage: 114 MB % 137.01/20.16 % (201342)Instructions burned: 541 (million) % 137.01/20.16 % (201347)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=3571346768:i=30479:sd=3:ss=axioms_2898 on theBenchmark for (2898ds/30479Mi) % 137.01/20.16 % (201348)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=3218721377:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2898 on theBenchmark for (2898ds/11035Mi) % 137.01/20.16 % (201348)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 137.01/20.16 % (201349)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=3781486880:i=5835_2898 on theBenchmark for (2898ds/5835Mi) % 137.01/20.16 % (201350)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2570712280:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2897 on theBenchmark for (2897ds/5890Mi) % 137.01/20.16 % (201348)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.01/20.16 % (201348)------------------------------ % 137.01/20.16 % (201348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.01/20.16 % (201348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.01/20.16 % (201348)CaDiCaL version: 2.1.3 % 137.01/20.16 % (201348)Termination reason: Unknown % 137.01/20.16 % (201348)Termination phase: Saturation % 137.01/20.16 % (201348)Time elapsed: 0.360 s % 137.01/20.16 % (201348)Peak memory usage: 113 MB % 137.01/20.16 % (201348)Instructions burned: 543 (million) % 137.01/20.16 % (201347)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.01/20.16 % (201347)------------------------------ % 137.01/20.16 % (201347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.01/20.16 % (201347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.01/20.16 % (201347)CaDiCaL version: 2.1.3 % 137.01/20.16 % (201347)Termination reason: Unknown % 137.01/20.16 % (201347)Termination phase: Saturation % 137.01/20.16 % (201347)Time elapsed: 0.375 s % 137.01/20.16 % (201347)Peak memory usage: 113 MB % 137.01/20.16 % (201347)Instructions burned: 538 (million) % 137.01/20.16 % (201349)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.01/20.16 % (201349)------------------------------ % 137.01/20.16 % (201349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.01/20.16 % (201349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.01/20.16 % (201349)CaDiCaL version: 2.1.3 % 137.01/20.16 % (201349)Termination reason: Unknown % 137.01/20.16 % (201349)Termination phase: Saturation % 137.01/20.16 % (201349)Time elapsed: 0.362 s % 137.01/20.16 % (201349)Peak memory usage: 113 MB % 137.01/20.16 % (201349)Instructions burned: 541 (million) % 137.01/20.16 % (201355)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=657462779:cts=off:i=19910:ep=RS_2893 on theBenchmark for (2893ds/19910Mi) % 137.01/20.16 % (201356)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=2945670578:i=20312:bd=preordered:fsr=off:er=filter_2893 on theBenchmark for (2893ds/20312Mi) % 137.01/20.16 % (201350)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.01/20.16 % (201350)------------------------------ % 137.01/20.16 % (201350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 137.01/20.16 % (201350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.24/24.63 % (201350)CaDiCaL version: 2.1.3 % 168.24/24.63 % (201350)Termination reason: Unknown % 168.24/24.63 % (201350)Termination phase: Saturation % 168.24/24.63 % (201350)Time elapsed: 0.388 s % 168.24/24.63 % (201350)Peak memory usage: 114 MB % 168.24/24.63 % (201350)Instructions burned: 541 (million) % 168.24/24.63 % (201357)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=3970935437:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2892 on theBenchmark for (2892ds/13822Mi) % 168.24/24.63 % (201360)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=3333103572:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2891 on theBenchmark for (2891ds/7144Mi) % 168.24/24.63 % (201356)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 168.24/24.63 % (201356)------------------------------ % 168.24/24.63 % (201356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.24/24.63 % (201356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.24/24.63 % (201356)CaDiCaL version: 2.1.3 % 168.24/24.63 % (201356)Termination reason: Unknown % 168.24/24.63 % (201356)Termination phase: Saturation % 168.24/24.63 % (201356)Time elapsed: 0.360 s % 168.24/24.63 % (201356)Peak memory usage: 113 MB % 168.24/24.63 % (201356)Instructions burned: 541 (million) % 168.24/24.63 % (201357)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 168.24/24.63 % (201357)------------------------------ % 168.24/24.63 % (201357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.24/24.63 % (201357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.24/24.63 % (201357)CaDiCaL version: 2.1.3 % 168.24/24.63 % (201357)Termination reason: Unknown % 168.24/24.63 % (201357)Termination phase: Saturation % 168.24/24.63 % (201357)Time elapsed: 0.359 s % 168.24/24.63 % (201357)Peak memory usage: 114 MB % 168.24/24.63 % (201357)Instructions burned: 541 (million) % 168.24/24.63 % (201363)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=1722538458:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2888 on theBenchmark for (2888ds/15184Mi) % 168.24/24.63 % (201364)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=2852650066:i=107375_2887 on theBenchmark for (2887ds/107375Mi) % 168.24/24.63 % (201363)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 168.24/24.63 % (201363)------------------------------ % 168.24/24.63 % (201363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.24/24.63 % (201363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.24/24.63 % (201363)CaDiCaL version: 2.1.3 % 168.24/24.63 % (201363)Termination reason: Unknown % 168.24/24.63 % (201363)Termination phase: Saturation % 168.24/24.63 % (201363)Time elapsed: 0.360 s % 168.24/24.63 % (201363)Peak memory usage: 114 MB % 168.24/24.63 % (201363)Instructions burned: 541 (million) % 168.24/24.63 % (201364)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 168.24/24.63 % (201364)------------------------------ % 168.24/24.63 % (201364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.24/24.63 % (201364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.24/24.63 % (201364)CaDiCaL version: 2.1.3 % 168.24/24.63 % (201364)Termination reason: Unknown % 168.24/24.63 % (201364)Termination phase: Saturation % 168.24/24.63 % (201364)Time elapsed: 0.360 s % 168.24/24.63 % (201364)Peak memory usage: 113 MB % 168.24/24.63 % (201364)Instructions burned: 541 (million) % 168.24/24.63 % (201367)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=1815682397:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2882 on theBenchmark for (2882ds/7958Mi) % 168.24/24.63 % (201368)dis+10_128_sil=16000:nwc=0.7:random_seed=3134365832:i=15999:nm=2:gsp=on_2882 on theBenchmark for (2882ds/15999Mi) % 168.24/24.63 % (201368)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 168.24/24.63 % (201367)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 168.24/24.63 % (201367)------------------------------ % 168.24/24.63 % (201367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.54/26.48 % (201367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.54/26.48 % (201367)CaDiCaL version: 2.1.3 % 181.54/26.48 % (201367)Termination reason: Unknown % 181.54/26.48 % (201367)Termination phase: Saturation % 181.54/26.48 % (201367)Time elapsed: 0.358 s % 181.54/26.48 % (201367)Peak memory usage: 114 MB % 181.54/26.48 % (201367)Instructions burned: 540 (million) % 181.54/26.48 % (201371)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2112862123:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2877 on theBenchmark for (2877ds/8139Mi) % 181.54/26.48 % (201360)Instruction limit reached! % 181.54/26.48 % (201360)------------------------------ % 181.54/26.48 % (201360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.54/26.48 % (201360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.54/26.48 % (201360)CaDiCaL version: 2.1.3 % 181.54/26.48 % (201360)Termination reason: Instruction limit % 181.54/26.48 % (201360)Termination phase: Saturation % 181.54/26.48 % (201360)Time elapsed: 4.930 s % 181.54/26.48 % (201360)Peak memory usage: 139 MB % 181.54/26.48 % (201360)Instructions burned: 7144 (million) % 181.54/26.48 % (201661)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=703451445:st=4:i=8950:sd=5:ss=axioms_2840 on theBenchmark for (2840ds/8950Mi) % 181.54/26.48 % (201661)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 181.54/26.48 % (201661)------------------------------ % 181.54/26.48 % (201661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.54/26.48 % (201661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.54/26.48 % (201661)CaDiCaL version: 2.1.3 % 181.54/26.48 % (201661)Termination reason: Unknown % 181.54/26.48 % (201661)Termination phase: Saturation % 181.54/26.48 % (201661)Time elapsed: 0.601 s % 181.54/26.48 % (201661)Peak memory usage: 114 MB % 181.54/26.48 % (201661)Instructions burned: 540 (million) % 181.54/26.48 % (201665)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=542497520:i=9809:ins=10:av=off_2831 on theBenchmark for (2831ds/9809Mi) % 181.54/26.48 % (201665)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 181.54/26.48 % (201665)------------------------------ % 181.54/26.48 % (201665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.54/26.48 % (201665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.54/26.48 % (201665)CaDiCaL version: 2.1.3 % 181.54/26.48 % (201665)Termination reason: Unknown % 181.54/26.48 % (201665)Termination phase: Saturation % 181.54/26.48 % (201665)Time elapsed: 0.606 s % 181.54/26.48 % (201665)Peak memory usage: 114 MB % 181.54/26.48 % (201665)Instructions burned: 542 (million) % 181.54/26.48 % (201671)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=1943172176:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2822 on theBenchmark for (2822ds/9885Mi) % 181.54/26.48 % (201671)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 181.54/26.48 % (201671)------------------------------ % 181.54/26.48 % (201671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.54/26.48 % (201671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.54/26.48 % (201671)CaDiCaL version: 2.1.3 % 181.54/26.48 % (201671)Termination reason: Unknown % 181.54/26.48 % (201671)Termination phase: Saturation % 181.54/26.48 % (201671)Time elapsed: 0.601 s % 181.54/26.48 % (201671)Peak memory usage: 114 MB % 181.54/26.48 % (201671)Instructions burned: 541 (million) % 181.54/26.48 % (201371)Instruction limit reached! % 181.54/26.48 % (201371)------------------------------ % 181.54/26.48 % (201371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.54/26.48 % (201371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.54/26.48 % (201371)CaDiCaL version: 2.1.3 % 181.54/26.48 % (201371)Termination reason: Instruction limit % 181.54/26.48 % (201371)Termination phase: Saturation % 181.54/26.48 % (201371)Time elapsed: 6.587 s % 181.54/26.48 % (201371)Peak memory usage: 139 MB % 181.54/26.48 % (201371)Instructions burned: 8139 (million) % 181.54/26.48 % (201675)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=36236641:cond=fast:i=32078:fgj=on:av=off_2812 on theBenchmark for (2812ds/32078Mi) % 181.54/26.48 % (201676)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=1649365527:i=11101:bd=all:ss=axioms:sgt=8_2809 on theBenchmark for (2809ds/11101Mi) % 201.03/29.17 % (201675)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 201.03/29.17 % (201675)------------------------------ % 201.03/29.17 % (201675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.03/29.17 % (201675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.03/29.17 % (201675)CaDiCaL version: 2.1.3 % 201.03/29.17 % (201675)Termination reason: Unknown % 201.03/29.17 % (201675)Termination phase: Saturation % 201.03/29.17 % (201675)Time elapsed: 0.608 s % 201.03/29.17 % (201675)Peak memory usage: 114 MB % 201.03/29.17 % (201675)Instructions burned: 541 (million) % 201.03/29.17 % (201689)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3977914648:cond=on:i=13220:s2at=3:aac=none:fsd=on_2803 on theBenchmark for (2803ds/13220Mi) % 201.03/29.17 % (201689)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 201.03/29.17 % (201689)------------------------------ % 201.03/29.17 % (201689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.03/29.17 % (201689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.03/29.17 % (201689)CaDiCaL version: 2.1.3 % 201.03/29.17 % (201689)Termination reason: Unknown % 201.03/29.17 % (201689)Termination phase: Saturation % 201.03/29.17 % (201689)Time elapsed: 0.543 s % 201.03/29.17 % (201689)Peak memory usage: 114 MB % 201.03/29.17 % (201689)Instructions burned: 542 (million) % 201.03/29.17 % (201695)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=1404778814:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2795 on theBenchmark for (2795ds/13528Mi) % 201.03/29.17 % (201695)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 201.03/29.17 % (201695)------------------------------ % 201.03/29.17 % (201695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.03/29.17 % (201695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.03/29.17 % (201695)CaDiCaL version: 2.1.3 % 201.03/29.17 % (201695)Termination reason: Unknown % 201.03/29.17 % (201695)Termination phase: Saturation % 201.03/29.17 % (201695)Time elapsed: 0.603 s % 201.03/29.17 % (201695)Peak memory usage: 114 MB % 201.03/29.17 % (201695)Instructions burned: 543 (million) % 201.03/29.17 % (201697)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=556111849:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2786 on theBenchmark for (2786ds/14854Mi) % 201.03/29.17 % (201697)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 201.03/29.17 % (201697)------------------------------ % 201.03/29.17 % (201697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.03/29.17 % (201697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.03/29.17 % (201697)CaDiCaL version: 2.1.3 % 201.03/29.17 % (201697)Termination reason: Unknown % 201.03/29.17 % (201697)Termination phase: Saturation % 201.03/29.17 % (201697)Time elapsed: 0.615 s % 201.03/29.17 % (201697)Peak memory usage: 114 MB % 201.03/29.17 % (201697)Instructions burned: 552 (million) % 201.03/29.17 % (201699)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1223973495:i=14974:ss=axioms:sgt=16_2777 on theBenchmark for (2777ds/14974Mi) % 201.03/29.17 % (201699)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 201.03/29.17 % (201699)------------------------------ % 201.03/29.17 % (201699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.03/29.17 % (201699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.03/29.17 % (201699)CaDiCaL version: 2.1.3 % 201.03/29.17 % (201699)Termination reason: Unknown % 201.03/29.17 % (201699)Termination phase: Saturation % 201.03/29.17 % (201699)Time elapsed: 0.602 s % 201.03/29.17 % (201699)Peak memory usage: 113 MB % 201.03/29.17 % (201699)Instructions burned: 540 (million) % 201.03/29.17 % (201701)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=415857496:i=33081:aac=none:fgj=on:bd=all:fsr=off_2768 on theBenchmark for (2768ds/33081Mi) % 201.03/29.17 % (201262)Instruction limit reached! % 201.03/29.17 % (201262)------------------------------ % 201.03/29.17 % (201262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.67/31.25 % (201262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.67/31.25 % (201262)CaDiCaL version: 2.1.3 % 215.67/31.25 % (201262)Termination reason: Instruction limit % 215.67/31.25 % (201262)Termination phase: Saturation % 215.67/31.25 % (201262)Time elapsed: 18.683 s % 215.67/31.25 % (201262)Peak memory usage: 293 MB % 215.67/31.25 % (201262)Instructions burned: 26474 (million) % 215.67/31.25 % (201701)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 215.67/31.25 % (201701)------------------------------ % 215.67/31.25 % (201701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.67/31.25 % (201701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.67/31.25 % (201701)CaDiCaL version: 2.1.3 % 215.67/31.25 % (201701)Termination reason: Unknown % 215.67/31.25 % (201701)Termination phase: Saturation % 215.67/31.25 % (201701)Time elapsed: 0.605 s % 215.67/31.25 % (201701)Peak memory usage: 114 MB % 215.67/31.25 % (201701)Instructions burned: 541 (million) % 215.67/31.25 % (201703)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=3924475314:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2761 on theBenchmark for (2761ds/50856Mi) % 215.67/31.25 % (201704)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2122765031:i=69865_2758 on theBenchmark for (2758ds/69865Mi) % 215.67/31.25 % (201703)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 215.67/31.25 % (201703)------------------------------ % 215.67/31.25 % (201703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.67/31.25 % (201703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.67/31.25 % (201703)CaDiCaL version: 2.1.3 % 215.67/31.25 % (201703)Termination reason: Unknown % 215.67/31.25 % (201703)Termination phase: Saturation % 215.67/31.25 % (201703)Time elapsed: 0.587 s % 215.67/31.25 % (201703)Peak memory usage: 114 MB % 215.67/31.25 % (201703)Instructions burned: 542 (million) % 215.67/31.25 % (201368)Instruction limit reached! % 215.67/31.25 % (201368)------------------------------ % 215.67/31.25 % (201368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.67/31.25 % (201368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.67/31.25 % (201368)CaDiCaL version: 2.1.3 % 215.67/31.25 % (201368)Termination reason: Instruction limit % 215.67/31.25 % (201368)Termination phase: Saturation % 215.67/31.25 % (201368)Time elapsed: 13.014 s % 215.67/31.25 % (201368)Peak memory usage: 185 MB % 215.67/31.25 % (201368)Instructions burned: 16000 (million) % 215.67/31.25 % (201704)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 215.67/31.25 % (201704)------------------------------ % 215.67/31.25 % (201704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.67/31.25 % (201704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.67/31.25 % (201704)CaDiCaL version: 2.1.3 % 215.67/31.25 % (201704)Termination reason: Unknown % 215.67/31.25 % (201704)Termination phase: Saturation % 215.67/31.25 % (201704)Time elapsed: 0.600 s % 215.67/31.25 % (201704)Peak memory usage: 114 MB % 215.67/31.25 % (201704)Instructions burned: 541 (million) % 215.67/31.25 % (201713)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=3065844471:cond=fast:i=17802:gtgl=3:gtg=all_2752 on theBenchmark for (2752ds/17802Mi) % 215.67/31.25 % (201714)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=458366060:i=96644_2750 on theBenchmark for (2750ds/96644Mi) % 215.67/31.25 % (201715)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 215.67/31.25 % (201715)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=3047818107:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2749 on theBenchmark for (2749ds/21161Mi) % 215.67/31.25 % (201713)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 215.67/31.25 % (201713)------------------------------ % 215.67/31.25 % (201713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 215.67/31.25 % (201713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 215.67/31.25 % (201713)CaDiCaL version: 2.1.3 % 224.59/32.55 % (201713)Termination reason: Unknown % 224.59/32.55 % (201713)Termination phase: Saturation % 224.59/32.55 % (201713)Time elapsed: 0.593 s % 224.59/32.55 % (201713)Peak memory usage: 114 MB % 224.59/32.55 % (201713)Instructions burned: 543 (million) % 224.59/32.55 % (201719)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=2867720667:i=22761:gtg=all:ss=axioms:fsd=on_2743 on theBenchmark for (2743ds/22761Mi) % 224.59/32.55 % (201355)Instruction limit reached! % 224.59/32.55 % (201355)------------------------------ % 224.59/32.55 % (201355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.59/32.55 % (201355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.59/32.55 % (201355)CaDiCaL version: 2.1.3 % 224.59/32.55 % (201355)Termination reason: Instruction limit % 224.59/32.55 % (201355)Termination phase: Saturation % 224.59/32.55 % (201355)Time elapsed: 15.541 s % 224.59/32.55 % (201355)Peak memory usage: 249 MB % 224.59/32.55 % (201355)Instructions burned: 19910 (million) % 224.59/32.55 % (201719)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 224.59/32.55 % (201719)------------------------------ % 224.59/32.55 % (201719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.59/32.55 % (201719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.59/32.55 % (201719)CaDiCaL version: 2.1.3 % 224.59/32.55 % (201719)Termination reason: Unknown % 224.59/32.55 % (201719)Termination phase: Saturation % 224.59/32.55 % (201719)Time elapsed: 0.591 s % 224.59/32.55 % (201719)Peak memory usage: 114 MB % 224.59/32.55 % (201719)Instructions burned: 541 (million) % 224.59/32.55 % (201721)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=3553617654:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2735 on theBenchmark for (2735ds/23713Mi) % 224.59/32.55 % (201721)Refutation not found, incomplete strategy % 224.59/32.55 % (201721)------------------------------ % 224.59/32.55 % (201721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.59/32.55 % (201721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.59/32.55 % (201721)CaDiCaL version: 2.1.3 % 224.59/32.55 % (201721)Termination reason: Refutation not found, incomplete strategy % 224.59/32.55 % (201721)Time elapsed: 0.009 s % 224.59/32.55 % (201721)Peak memory usage: 88 MB % 224.59/32.55 % (201721)Instructions burned: 7 (million) % 224.59/32.55 % (201722)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3362884004:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2734 on theBenchmark for (2734ds/26509Mi) % 224.59/32.55 % (201721)------------------------------ % 224.59/32.55 % (201721)------------------------------ % 224.59/32.55 % (201725)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=2718645216:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2728 on theBenchmark for (2728ds/28957Mi) % 224.59/32.55 % (201722)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 224.59/32.55 % (201722)------------------------------ % 224.59/32.55 % (201722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.59/32.55 % (201722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.59/32.55 % (201722)CaDiCaL version: 2.1.3 % 224.59/32.55 % (201722)Termination reason: Unknown % 224.59/32.55 % (201722)Termination phase: Saturation % 224.59/32.55 % (201722)Time elapsed: 0.591 s % 224.59/32.55 % (201722)Peak memory usage: 114 MB % 224.59/32.55 % (201722)Instructions burned: 541 (million) % 224.59/32.55 % (201727)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=2671846584:i=29246:s2at=-1:kws=inv_arity:ins=10_2725 on theBenchmark for (2725ds/29246Mi) % 224.59/32.55 % (201727)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 224.59/32.55 % (201727)------------------------------ % 224.59/32.55 % (201727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 224.59/32.55 % (201727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 224.59/32.55 % (201727)CaDiCaL version: 2.1.3 % 224.59/32.55 % (201727)Termination reason: Unknown % 224.59/32.55 % (201727)Termination phase: Saturation % 224.59/32.55 % (201727)Time elapsed: 0.587 s % 224.59/32.55 % (201727)Peak memory usage: 114 MB % 224.59/32.55 % (201727)Instructions burned: 541 (million) % 235.76/34.04 % (201731)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=3551406341:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2716 on theBenchmark for (2716ds/30082Mi) % 235.76/34.04 % (201731)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 235.76/34.04 % (201731)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 235.76/34.04 % (201731)------------------------------ % 235.76/34.04 % (201731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.76/34.04 % (201731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/34.04 % (201731)CaDiCaL version: 2.1.3 % 235.76/34.04 % (201731)Termination reason: Unknown % 235.76/34.04 % (201731)Termination phase: Saturation % 235.76/34.04 % (201731)Time elapsed: 0.589 s % 235.76/34.04 % (201731)Peak memory usage: 114 MB % 235.76/34.04 % (201731)Instructions burned: 544 (million) % 235.76/34.04 % (201331)Instruction limit reached! % 235.76/34.04 % (201331)------------------------------ % 235.76/34.04 % (201331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.76/34.04 % (201331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/34.04 % (201331)CaDiCaL version: 2.1.3 % 235.76/34.04 % (201331)Termination reason: Instruction limit % 235.76/34.04 % (201331)Termination phase: Saturation % 235.76/34.04 % (201331)Time elapsed: 20.384 s % 235.76/34.04 % (201331)Peak memory usage: 283 MB % 235.76/34.04 % (201331)Instructions burned: 43698 (million) % 235.76/34.04 % (201733)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=2970806539:i=32262:bd=preordered_2707 on theBenchmark for (2707ds/32262Mi) % 235.76/34.04 % (201734)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=152963409:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2705 on theBenchmark for (2705ds/32870Mi) % 235.76/34.04 % (201676)Instruction limit reached! % 235.76/34.04 % (201676)------------------------------ % 235.76/34.04 % (201676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.76/34.04 % (201676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/34.04 % (201676)CaDiCaL version: 2.1.3 % 235.76/34.04 % (201676)Termination reason: Instruction limit % 235.76/34.04 % (201676)Termination phase: Saturation % 235.76/34.04 % (201676)Time elapsed: 10.493 s % 235.76/34.04 % (201676)Peak memory usage: 213 MB % 235.76/34.04 % (201676)Instructions burned: 11102 (million) % 235.76/34.04 % (201734)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 235.76/34.04 % (201734)------------------------------ % 235.76/34.04 % (201734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.76/34.04 % (201734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/34.04 % (201734)CaDiCaL version: 2.1.3 % 235.76/34.04 % (201734)Termination reason: Unknown % 235.76/34.04 % (201734)Termination phase: Saturation % 235.76/34.04 % (201734)Time elapsed: 0.321 s % 235.76/34.04 % (201734)Peak memory usage: 114 MB % 235.76/34.04 % (201734)Instructions burned: 542 (million) % 235.76/34.04 % (201737)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=1316848287:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2701 on theBenchmark for (2701ds/33295Mi) % 235.76/34.04 % (201733)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 235.76/34.04 % (201733)------------------------------ % 235.76/34.04 % (201733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.76/34.04 % (201733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.76/34.04 % (201733)CaDiCaL version: 2.1.3 % 235.76/34.04 % (201733)Termination reason: Unknown % 235.76/34.04 % (201733)Termination phase: Saturation % 235.76/34.04 % (201733)Time elapsed: 0.587 s % 235.76/34.04 % (201733)Peak memory usage: 113 MB % 235.76/34.04 % (201733)Instructions burned: 541 (million) % 235.76/34.04 % (201738)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=580220252:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2700 on theBenchmark for (2700ds/36826Mi) % 235.76/34.04 % (201740)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=3431488515:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2699 on theBenchmark for (2699ds/92981Mi) % 244.46/35.30 % (201235)Instruction limit reached! % 244.46/35.30 % (201235)------------------------------ % 244.46/35.30 % (201235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.46/35.30 % (201235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/35.30 % (201235)CaDiCaL version: 2.1.3 % 244.46/35.30 % (201235)Termination reason: Instruction limit % 244.46/35.30 % (201235)Termination phase: Saturation % 244.46/35.30 % (201235)Time elapsed: 26.779 s % 244.46/35.30 % (201235)Peak memory usage: 277 MB % 244.46/35.30 % (201235)Instructions burned: 33334 (million) % 244.46/35.30 % (201737)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 244.46/35.30 % (201737)------------------------------ % 244.46/35.30 % (201737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.46/35.30 % (201737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/35.30 % (201737)CaDiCaL version: 2.1.3 % 244.46/35.30 % (201737)Termination reason: Unknown % 244.46/35.30 % (201737)Termination phase: Saturation % 244.46/35.30 % (201737)Time elapsed: 0.582 s % 244.46/35.30 % (201737)Peak memory usage: 113 MB % 244.46/35.30 % (201737)Instructions burned: 540 (million) % 244.46/35.30 % (201745)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=1416467093:s2pl=on:i=49423_2694 on theBenchmark for (2694ds/49423Mi) % 244.46/35.30 % (201746)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=2016081528:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2693 on theBenchmark for (2693ds/57299Mi) % 244.46/35.30 % (201740)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 244.46/35.30 % (201740)------------------------------ % 244.46/35.30 % (201740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.46/35.30 % (201740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/35.30 % (201740)CaDiCaL version: 2.1.3 % 244.46/35.30 % (201740)Termination reason: Unknown % 244.46/35.30 % (201740)Termination phase: Saturation % 244.46/35.30 % (201740)Time elapsed: 0.587 s % 244.46/35.30 % (201740)Peak memory usage: 114 MB % 244.46/35.30 % (201740)Instructions burned: 540 (million) % 244.46/35.30 % (201749)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=2800777003:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2690 on theBenchmark for (2690ds/127679Mi) % 244.46/35.30 % (201745)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 244.46/35.30 % (201745)------------------------------ % 244.46/35.30 % (201745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.46/35.30 % (201745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/35.30 % (201745)CaDiCaL version: 2.1.3 % 244.46/35.30 % (201745)Termination reason: Unknown % 244.46/35.30 % (201745)Termination phase: Saturation % 244.46/35.30 % (201745)Time elapsed: 0.601 s % 244.46/35.30 % (201745)Peak memory usage: 113 MB % 244.46/35.30 % (201745)Instructions burned: 542 (million) % 244.46/35.30 % (201746)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 244.46/35.30 % (201746)------------------------------ % 244.46/35.30 % (201746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.46/35.30 % (201746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.46/35.30 % (201746)CaDiCaL version: 2.1.3 % 244.46/35.30 % (201746)Termination reason: Unknown % 244.46/35.30 % (201746)Termination phase: Saturation % 244.46/35.30 % (201746)Time elapsed: 0.578 s % 244.46/35.30 % (201746)Peak memory usage: 113 MB % 244.46/35.30 % (201746)Instructions burned: 540 (million) % 244.46/35.30 % (201752)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=3645008739:i=100512:doe=on:fgj=on:bd=all:fsd=on_2684 on theBenchmark for (2684ds/100512Mi) % 244.46/35.30 % (201751)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=2790436264:i=69402:add=on:aac=none:fsr=off_2685 on theBenchmark for (2685ds/69402Mi) % 253.15/36.67 % (201749)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 253.15/36.67 % (201749)------------------------------ % 253.15/36.67 % (201749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.15/36.67 % (201749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.15/36.67 % (201749)CaDiCaL version: 2.1.3 % 253.15/36.67 % (201749)Termination reason: Unknown % 253.15/36.67 % (201749)Termination phase: Saturation % 253.15/36.67 % (201749)Time elapsed: 0.584 s % 253.15/36.67 % (201749)Peak memory usage: 114 MB % 253.15/36.67 % (201749)Instructions burned: 542 (million) % 253.15/36.67 % (201755)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=3064047769:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2681 on theBenchmark for (2681ds/138761Mi) % 253.15/36.67 % (201752)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 253.15/36.67 % (201752)------------------------------ % 253.15/36.67 % (201752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.15/36.67 % (201752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.15/36.67 % (201752)CaDiCaL version: 2.1.3 % 253.15/36.67 % (201752)Termination reason: Unknown % 253.15/36.67 % (201752)Termination phase: Saturation % 253.15/36.67 % (201752)Time elapsed: 0.508 s % 253.15/36.67 % (201752)Peak memory usage: 113 MB % 253.15/36.67 % (201752)Instructions burned: 541 (million) % 253.15/36.67 % (201751)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 253.15/36.67 % (201751)------------------------------ % 253.15/36.67 % (201751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.15/36.67 % (201751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.15/36.67 % (201751)CaDiCaL version: 2.1.3 % 253.15/36.67 % (201751)Termination reason: Unknown % 253.15/36.67 % (201751)Termination phase: Saturation % 253.15/36.67 % (201751)Time elapsed: 0.594 s % 253.15/36.67 % (201751)Peak memory usage: 113 MB % 253.15/36.67 % (201751)Instructions burned: 541 (million) % 253.15/36.67 % (201757)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=3080605341:i=282386:rtra=on_2677 on theBenchmark for (2677ds/282386Mi) % 253.15/36.67 % (201758)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=2922771384:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2676 on theBenchmark for (2676ds/269354Mi) % 253.15/36.67 % (201755)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 253.15/36.67 % (201755)------------------------------ % 253.15/36.67 % (201755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.15/36.67 % (201755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.15/36.67 % (201755)CaDiCaL version: 2.1.3 % 253.15/36.67 % (201755)Termination reason: Unknown % 253.15/36.67 % (201755)Termination phase: Saturation % 253.15/36.67 % (201755)Time elapsed: 0.585 s % 253.15/36.67 % (201755)Peak memory usage: 114 MB % 253.15/36.67 % (201755)Instructions burned: 541 (million) % 253.15/36.67 % (201762)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=3852260198:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2672 on theBenchmark for (2672ds/283390Mi) % 253.15/36.67 % (201757)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 253.15/36.67 % (201757)------------------------------ % 253.15/36.67 % (201757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.15/36.67 % (201757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.15/36.67 % (201757)CaDiCaL version: 2.1.3 % 253.15/36.67 % (201757)Termination reason: Unknown % 253.15/36.67 % (201757)Termination phase: Saturation % 253.15/36.67 % (201757)Time elapsed: 0.586 s % 253.15/36.67 % (201757)Peak memory usage: 113 MB % 253.15/36.67 % (201757)Instructions burned: 542 (million) % 253.15/36.67 % (201762)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 253.15/36.67 % (201758)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 253.15/36.67 % (201758)------------------------------ % 253.15/36.67 % (201758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.27/38.29 % (201758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.27/38.29 % (201758)CaDiCaL version: 2.1.3 % 265.27/38.29 % (201758)Termination reason: Unknown % 265.27/38.29 % (201758)Termination phase: Saturation % 265.27/38.29 % (201758)Time elapsed: 0.603 s % 265.27/38.29 % (201758)Peak memory usage: 114 MB % 265.27/38.29 % (201758)Instructions burned: 546 (million) % 265.27/38.29 % (201764)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=196841238:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2669 on theBenchmark for (2669ds/218Mi) % 265.27/38.29 % (201764)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 265.27/38.29 % (201765)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=2322153247:i=238:av=off:rtra=on:ss=axioms_2668 on theBenchmark for (2668ds/238Mi) % 265.27/38.29 % (201764)Instruction limit reached! % 265.27/38.29 % (201764)------------------------------ % 265.27/38.29 % (201764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.27/38.29 % (201764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.27/38.29 % (201764)CaDiCaL version: 2.1.3 % 265.27/38.29 % (201764)Termination reason: Instruction limit % 265.27/38.29 % (201764)Termination phase: Saturation % 265.27/38.29 % (201764)Time elapsed: 0.202 s % 265.27/38.29 % (201764)Peak memory usage: 90 MB % 265.27/38.29 % (201764)Instructions burned: 219 (million) % 265.27/38.29 % (201762)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 265.27/38.29 % (201762)------------------------------ % 265.27/38.29 % (201762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.27/38.29 % (201762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.27/38.29 % (201762)CaDiCaL version: 2.1.3 % 265.27/38.29 % (201762)Termination reason: Unknown % 265.27/38.29 % (201762)Termination phase: Saturation % 265.27/38.29 % (201762)Time elapsed: 0.577 s % 265.27/38.29 % (201762)Peak memory usage: 113 MB % 265.27/38.29 % (201762)Instructions burned: 542 (million) % 265.27/38.29 % (201765)Instruction limit reached! % 265.27/38.29 % (201765)------------------------------ % 265.27/38.29 % (201765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.27/38.29 % (201765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.27/38.29 % (201765)CaDiCaL version: 2.1.3 % 265.27/38.29 % (201765)Termination reason: Instruction limit % 265.27/38.29 % (201765)Termination phase: Saturation % 265.27/38.29 % (201765)Time elapsed: 0.221 s % 265.27/38.29 % (201765)Peak memory usage: 89 MB % 265.27/38.29 % (201765)Instructions burned: 238 (million) % 265.27/38.29 % (201768)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=519740047:s2a=on:i=278:rtra=on:gtg=position_2664 on theBenchmark for (2664ds/278Mi) % 265.27/38.29 % (201769)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=2645434440:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2663 on theBenchmark for (2663ds/258Mi) % 265.27/38.29 % (201770)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2279746425:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2663 on theBenchmark for (2663ds/570Mi) % 265.27/38.29 % (201768)Instruction limit reached! % 265.27/38.29 % (201768)------------------------------ % 265.27/38.29 % (201768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.27/38.29 % (201768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.27/38.29 % (201768)CaDiCaL version: 2.1.3 % 265.27/38.29 % (201768)Termination reason: Instruction limit % 265.27/38.29 % (201768)Termination phase: Saturation % 265.27/38.29 % (201768)Time elapsed: 0.269 s % 265.27/38.29 % (201768)Peak memory usage: 91 MB % 265.27/38.29 % (201768)Instructions burned: 279 (million) % 265.27/38.29 % (201769)Instruction limit reached! % 265.27/38.29 % (201769)------------------------------ % 265.27/38.29 % (201769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 265.27/38.29 % (201769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 265.27/38.29 % (201769)CaDiCaL version: 2.1.3 % 265.27/38.29 % (201769)Termination reason: Instruction limit % 265.27/38.29 % (201769)Termination phase: Saturation % 265.27/38.29 % (201769)Time elapsed: 0.228 s % 265.27/38.29 % (201769)Peak memory usage: 90 MB % 265.27/38.29 % (201769)Instructions burned: 258 (million) % 265.27/38.29 % (201774)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=1565291962:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2659 on theBenchmark for (2659ds/314Mi) % 265.27/38.29 % (201775)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=4038487000:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2658 on theBenchmark for (2658ds/650Mi) % 276.14/39.81 % (201770)Instruction limit reached! % 276.14/39.81 % (201770)------------------------------ % 276.14/39.81 % (201770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.14/39.81 % (201770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.14/39.81 % (201770)CaDiCaL version: 2.1.3 % 276.14/39.81 % (201770)Termination reason: Instruction limit % 276.14/39.81 % (201770)Termination phase: Saturation % 276.14/39.81 % (201770)Time elapsed: 0.578 s % 276.14/39.81 % (201770)Peak memory usage: 92 MB % 276.14/39.81 % (201770)Instructions burned: 570 (million) % 276.14/39.81 % (201774)Instruction limit reached! % 276.14/39.81 % (201774)------------------------------ % 276.14/39.81 % (201774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.14/39.81 % (201774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.14/39.81 % (201774)CaDiCaL version: 2.1.3 % 276.14/39.81 % (201774)Termination reason: Instruction limit % 276.14/39.81 % (201774)Termination phase: Saturation % 276.14/39.81 % (201774)Time elapsed: 0.291 s % 276.14/39.81 % (201774)Peak memory usage: 91 MB % 276.14/39.81 % (201774)Instructions burned: 314 (million) % 276.14/39.81 % (201778)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=1888801109:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2654 on theBenchmark for (2654ds/496Mi) % 276.14/39.81 % (201779)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=1495895080:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2653 on theBenchmark for (2653ds/588Mi) % 276.14/39.81 % (201779)Refutation not found, incomplete strategy % 276.14/39.81 % (201779)------------------------------ % 276.14/39.81 % (201779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.14/39.81 % (201779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.14/39.81 % (201779)CaDiCaL version: 2.1.3 % 276.14/39.81 % (201779)Termination reason: Refutation not found, incomplete strategy % 276.14/39.81 % (201779)Time elapsed: 0.010 s % 276.14/39.81 % (201779)Peak memory usage: 89 MB % 276.14/39.81 % (201779)Instructions burned: 9 (million) % 276.14/39.81 % (201775)Instruction limit reached! % 276.14/39.81 % (201775)------------------------------ % 276.14/39.81 % (201775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.14/39.81 % (201775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.14/39.81 % (201775)CaDiCaL version: 2.1.3 % 276.14/39.81 % (201775)Termination reason: Instruction limit % 276.14/39.81 % (201775)Termination phase: Saturation % 276.14/39.81 % (201775)Time elapsed: 0.596 s % 276.14/39.81 % (201775)Peak memory usage: 93 MB % 276.14/39.81 % (201775)Instructions burned: 651 (million) % 276.14/39.81 % (201778)Instruction limit reached! % 276.14/39.81 % (201778)------------------------------ % 276.14/39.81 % (201778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.14/39.81 % (201778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.14/39.81 % (201778)CaDiCaL version: 2.1.3 % 276.14/39.81 % (201778)Termination reason: Instruction limit % 276.14/39.81 % (201778)Termination phase: Saturation % 276.14/39.81 % (201778)Time elapsed: 0.490 s % 276.14/39.81 % (201778)Peak memory usage: 93 MB % 276.14/39.81 % (201778)Instructions burned: 496 (million) % 276.14/39.81 % (201779)------------------------------ % 276.14/39.81 % (201779)------------------------------ % 276.14/39.81 % (201782)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=3275668495:i=4700:rtra=on_2649 on theBenchmark for (2649ds/4700Mi) % 276.14/39.81 % (201783)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1352313554:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2646 on theBenchmark for (2646ds/226Mi) % 276.14/39.81 % (201784)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4195420221:i=254:av=off:fsr=off:rtra=on:sup=off_2646 on theBenchmark for (2646ds/254Mi) % 276.14/39.81 % (201784)Refutation not found, incomplete strategy % 276.14/39.81 % (201784)------------------------------ % 276.14/39.81 % (201784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.14/39.81 % (201784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.14/39.81 % (201784)CaDiCaL version: 2.1.3 % 276.14/39.81 % (201784)Termination reason: Refutation not found, incomplete strategy % 276.14/39.81 % (201784)Time elapsed: 0.010 s % 276.14/39.81 % (201784)Peak memory usage: 88 MB % 276.14/39.81 % (201784)Instructions burned: 9 (million) % 276.14/39.81 % (201783)Instruction limit reached! % 285.41/41.12 % (201783)------------------------------ % 285.41/41.12 % (201783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.41/41.12 % (201783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.41/41.12 % (201783)CaDiCaL version: 2.1.3 % 285.41/41.12 % (201783)Termination reason: Instruction limit % 285.41/41.12 % (201783)Termination phase: Saturation % 285.41/41.12 % (201783)Time elapsed: 0.233 s % 285.41/41.12 % (201783)Peak memory usage: 91 MB % 285.41/41.12 % (201783)Instructions burned: 226 (million) % 285.41/41.12 % (201782)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 285.41/41.12 % (201782)------------------------------ % 285.41/41.12 % (201782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.41/41.12 % (201782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.41/41.12 % (201782)CaDiCaL version: 2.1.3 % 285.41/41.12 % (201782)Termination reason: Unknown % 285.41/41.12 % (201782)Termination phase: Saturation % 285.41/41.12 % (201782)Time elapsed: 0.606 s % 285.41/41.12 % (201782)Peak memory usage: 114 MB % 285.41/41.12 % (201782)Instructions burned: 541 (million) % 285.41/41.12 % (201784)------------------------------ % 285.41/41.12 % (201784)------------------------------ % 285.41/41.12 % (201790)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=656550031:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2641 on theBenchmark for (2641ds/228Mi) % 285.41/41.12 % (201790)Refutation not found, incomplete strategy % 285.41/41.12 % (201790)------------------------------ % 285.41/41.12 % (201790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.41/41.12 % (201790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.41/41.12 % (201790)CaDiCaL version: 2.1.3 % 285.41/41.12 % (201790)Termination reason: Refutation not found, incomplete strategy % 285.41/41.12 % (201790)Time elapsed: 0.007 s % 285.41/41.12 % (201790)Peak memory usage: 88 MB % 285.41/41.12 % (201790)Instructions burned: 5 (million) % 285.41/41.12 % (201791)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=3244886070:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2640 on theBenchmark for (2640ds/1814Mi) % 285.41/41.12 % (201792)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=1496250195:i=874:sd=1:aac=none:rtra=on:ss=included_2639 on theBenchmark for (2639ds/874Mi) % 285.41/41.12 % (201792)Refutation not found, incomplete strategy % 285.41/41.12 % (201792)------------------------------ % 285.41/41.12 % (201792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.41/41.12 % (201792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.41/41.12 % (201792)CaDiCaL version: 2.1.3 % 285.41/41.12 % (201792)Termination reason: Refutation not found, incomplete strategy % 285.41/41.12 % (201792)Time elapsed: 0.012 s % 285.41/41.12 % (201792)Peak memory usage: 88 MB % 285.41/41.12 % (201792)Instructions burned: 10 (million) % 285.41/41.12 % (201790)------------------------------ % 285.41/41.12 % (201790)------------------------------ % 285.41/41.12 % (201792)------------------------------ % 285.41/41.12 % (201792)------------------------------ % 285.41/41.12 % (201796)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3328825919:i=10404:rtra=on:ss=axioms:sgt=16_2634 on theBenchmark for (2634ds/10404Mi) % 285.41/41.12 % (201799)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2391849298:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2633 on theBenchmark for (2633ds/268Mi) % 285.41/41.12 % (201799)Instruction limit reached! % 285.41/41.12 % (201799)------------------------------ % 285.41/41.12 % (201799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.41/41.12 % (201799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.41/41.12 % (201799)CaDiCaL version: 2.1.3 % 285.41/41.12 % (201799)Termination reason: Instruction limit % 285.41/41.12 % (201799)Termination phase: Saturation % 285.41/41.12 % (201799)Time elapsed: 0.252 s % 285.41/41.12 % (201799)Peak memory usage: 91 MB % 285.41/41.12 % (201799)Instructions burned: 268 (million) % 285.41/41.12 % (201796)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 285.41/41.12 % (201796)------------------------------ % 285.41/41.12 % (201796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 285.41/41.12 % (201796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 285.41/41.12 % (201796)CaDiCaL version: 2.1.3 % 285.41/41.12 % (201796)Termination reason: Unknown % 297.13/42.76 % (201796)Termination phase: Saturation % 297.13/42.76 % (201796)Time elapsed: 0.603 s % 297.13/42.76 % (201796)Peak memory usage: 113 MB % 297.13/42.76 % (201796)Instructions burned: 542 (million) % 297.13/42.76 % (201803)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=1294682987:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2627 on theBenchmark for (2627ds/1184Mi) % 297.13/42.76 % (201807)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=3582212323:st=3:i=26386:sd=3:rtra=on:ss=axioms_2625 on theBenchmark for (2625ds/26386Mi) % 297.13/42.76 % (201791)Instruction limit reached! % 297.13/42.76 % (201791)------------------------------ % 297.13/42.76 % (201791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.13/42.76 % (201791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.13/42.76 % (201791)CaDiCaL version: 2.1.3 % 297.13/42.76 % (201791)Termination reason: Instruction limit % 297.13/42.76 % (201791)Termination phase: Saturation % 297.13/42.76 % (201791)Time elapsed: 1.870 s % 297.13/42.76 % (201791)Peak memory usage: 101 MB % 297.13/42.76 % (201791)Instructions burned: 1815 (million) % 297.13/42.76 % (201807)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 297.13/42.76 % (201807)------------------------------ % 297.13/42.76 % (201807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.13/42.76 % (201807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.13/42.76 % (201807)CaDiCaL version: 2.1.3 % 297.13/42.76 % (201807)Termination reason: Unknown % 297.13/42.76 % (201807)Termination phase: Saturation % 297.13/42.76 % (201807)Time elapsed: 0.595 s % 297.13/42.76 % (201807)Peak memory usage: 113 MB % 297.13/42.76 % (201807)Instructions burned: 540 (million) % 297.13/42.76 % (201810)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=1777327746:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2618 on theBenchmark for (2618ds/250Mi) % 297.13/42.76 % (201810)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 297.13/42.76 % (201811)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=61308413:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2617 on theBenchmark for (2617ds/268Mi) % 297.13/42.76 % (201810)Instruction limit reached! % 297.13/42.76 % (201810)------------------------------ % 297.13/42.76 % (201810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.13/42.76 % (201810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.13/42.76 % (201810)CaDiCaL version: 2.1.3 % 297.13/42.76 % (201810)Termination reason: Instruction limit % 297.13/42.76 % (201810)Termination phase: Saturation % 297.13/42.76 % (201810)Time elapsed: 0.261 s % 297.13/42.76 % (201810)Peak memory usage: 91 MB % 297.13/42.76 % (201810)Instructions burned: 250 (million) % 297.13/42.76 % (201803)Instruction limit reached! % 297.13/42.76 % (201803)------------------------------ % 297.13/42.76 % (201803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.13/42.76 % (201803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.13/42.76 % (201803)CaDiCaL version: 2.1.3 % 297.13/42.76 % (201803)Termination reason: Instruction limit % 297.13/42.76 % (201803)Termination phase: Saturation % 297.13/42.76 % (201803)Time elapsed: 1.212 s % 297.13/42.76 % (201803)Peak memory usage: 100 MB % 297.13/42.76 % (201803)Instructions burned: 1184 (million) % 297.13/42.76 % (201811)Instruction limit reached! % 297.13/42.76 % (201811)------------------------------ % 297.13/42.76 % (201811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.13/42.76 % (201811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.13/42.76 % (201811)CaDiCaL version: 2.1.3 % 297.13/42.76 % (201811)Termination reason: Instruction limit % 297.13/42.76 % (201811)Termination phase: Saturation % 297.13/42.76 % (201811)Time elapsed: 0.244 s % 297.13/42.76 % (201811)Peak memory usage: 115 MB % 297.13/42.76 % (201811)Instructions burned: 268 (million) % 297.13/42.76 % (201815)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=2323027986:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2612 on theBenchmark for (2612ds/862Mi) % 297.13/42.76 % (201814)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3716808920:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2613 on theBenchmark for (2613ds/282Mi) % 297.13/42.76 % (201814)WARNING: Not using GeneralSplitting currently not comTerminated %------------------------------------------------------------------------------